(*
-* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
-* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
-* This file is part of Coccinelle.
-*
-* Coccinelle is free software: you can redistribute it and/or modify
-* it under the terms of the GNU General Public License as published by
-* the Free Software Foundation, according to version 2 of the License.
-*
-* Coccinelle is distributed in the hope that it will be useful,
-* but WITHOUT ANY WARRANTY; without even the implied warranty of
-* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-* GNU General Public License for more details.
-*
-* You should have received a copy of the GNU General Public License
-* along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
-*
-* The authors reserve the right to distribute this or future versions of
-* Coccinelle under other licenses.
-*)
+ * Copyright 2010, INRIA, University of Copenhagen
+ * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
+ * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
+ * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
+ * This file is part of Coccinelle.
+ *
+ * Coccinelle is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, according to version 2 of the License.
+ *
+ * Coccinelle is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * The authors reserve the right to distribute this or future versions of
+ * Coccinelle under other licenses.
+ *)
(*external c_counter : unit -> int = "c_counter"*)
(* **********************************************************************
*
- * Implementation of a Witness Tree model checking engine for CTL-FVex
- *
+ * Implementation of a Witness Tree model checking engine for CTL-FVex
+ *
*
* **********************************************************************)
end
;;
-module OGRAPHEXT_GRAPH =
+module OGRAPHEXT_GRAPH =
struct
type node = int;;
type cfg = (string,unit) Ograph_extended.ograph_mutable;;
let head = List.hd
-let tail l =
+let tail l =
match l with
[] -> []
| (x::xs) -> xs
match opts with
| [] -> []
| (Some x)::rest -> x::(some_tolist rest)
- | _::rest -> some_tolist rest
+ | _::rest -> some_tolist rest
;;
let rec groupBy eq l =
match l with
[] -> []
- | (x::xs) ->
+ | (x::xs) ->
let (xs1,xs2) = partition (fun x' -> eq x x') xs in
(x::xs1)::(groupBy eq xs2)
;;
(* ********************************************************************** *)
module CTL_ENGINE =
- functor (SUB : SUBST) ->
+ functor (SUB : SUBST) ->
functor (G : GRAPH) ->
functor (P : PREDICATE) ->
struct
let print_generic_subst = function
A.Subst (mvar, v) ->
SUB.print_mvar mvar; Format.print_string " --> "; SUB.print_value v
- | A.NegSubst (mvar, v) ->
+ | A.NegSubst (mvar, v) ->
SUB.print_mvar mvar; Format.print_string " -/-> "; SUB.print_value v in
Format.print_string "[";
Common.print_between (fun () -> Format.print_string ";" )
let rec (print_generic_witness: ('pred, 'anno) witness -> unit) =
function
- | A.Wit (state, subst, anno, childrens) ->
+ | A.Wit (state, subst, anno, childrens) ->
Format.print_string "wit ";
G.print_node state;
print_generic_substitution subst;
(match childrens with
[] -> Format.print_string "{}"
- | _ ->
+ | _ ->
Format.force_newline(); Format.print_string " "; Format.open_box 0;
print_generic_witnesstree childrens; Format.close_box())
- | A.NegWit(wit) ->
+ | A.NegWit(wit) ->
Format.print_string "!";
print_generic_witness wit
Format.open_box 1;
Format.print_string "{";
Common.print_between
- (fun () -> Format.print_string ";"; Format.force_newline() )
+ (fun () -> Format.print_string ";"; Format.force_newline() )
print_generic_witness witnesstree;
Format.print_string "}";
Format.close_box()
-
+
and print_generic_triple (node,subst,tree) =
G.print_node node;
print_generic_substitution subst;
print_generic_witnesstree tree
-and (print_generic_algo : ('pred,'anno) triples -> unit) = fun xs ->
+and (print_generic_algo : ('pred,'anno) triples -> unit) = fun xs ->
Format.print_string "<";
Common.print_between
(fun () -> Format.print_string ";"; Format.force_newline())
print_generic_triple x; Format.print_newline(); flush stdout)
(List.sort compare l);
Printf.printf "\n"
-
+
let print_required_states = function
None -> Printf.printf "no required states\n"
| Some states ->
) in
(if not (List.mem file !graph_stack) then
graph_stack := file :: !graph_stack);
- let filename = Filename.temp_file (file^":") ".dot" in
- Hashtbl.add graph_hash file filename;
+ let filename = Filename.temp_file (file^":") ".dot" in
+ Hashtbl.add graph_hash file filename;
G.print_graph grp
(if !Flag_ctl.gt_without_label then None else (Some label))
(match required_states with
(* ---------------------------------------------------------------------- *)
(* *)
(* ---------------------------------------------------------------------- *)
-
-
+
+
(* ************************* *)
(* Substitutions *)
(* ************************* *)
-
+
let dom_sub sub =
match sub with
| A.Subst(x,_) -> x
| A.NegSubst(x,_) -> x
;;
-
+
let ran_sub sub =
match sub with
| A.Subst(_,x) -> x
| A.NegSubst(_,x) -> x
;;
-
+
let eq_subBy eqx eqv sub sub' =
- match (sub,sub') with
+ match (sub,sub') with
| (A.Subst(x,v),A.Subst(x',v')) -> (eqx x x') && (eqv v v')
| (A.NegSubst(x,v),A.NegSubst(x',v')) -> (eqx x x') && (eqv v v')
| _ -> false
let merge_subBy eqx (===) (>+<) sub sub' =
(* variable part is guaranteed to be the same *)
match (sub,sub') with
- (A.Subst (x,v),A.Subst (x',v')) ->
+ (A.Subst (x,v),A.Subst (x',v')) ->
if (v === v')
then Some [A.Subst(x, v >+< v')]
else None
;;
(* NOTE: functor *)
-let merge_sub sub sub' =
+(* How could we accomadate subterm constraints here??? *)
+let merge_sub sub sub' =
merge_subBy SUB.eq_mvar SUB.eq_val SUB.merge_val sub sub'
let clean_substBy eq cmp theta = List.sort cmp (nubBy eq theta);;
(* NOTE: we sort by using the generic "compare" on (meta-)variable
- * names; we could also require a definition of compare for meta-variables
+ * names; we could also require a definition of compare for meta-variables
* or substitutions but that seems like overkill for sorting
*)
-let clean_subst theta =
- let res =
+let clean_subst theta =
+ let res =
clean_substBy eq_sub
(fun s s' ->
let res = compare (dom_sub s) (dom_sub s') in
(* Split a theta in two parts: one with (only) "x" and one without *)
(* NOTE: functor *)
-let split_subst theta x =
+let split_subst theta x =
partition (fun sub -> SUB.eq_mvar (dom_sub sub) x) theta;;
exception SUBST_MISMATCH
List.map
(function (st,th,wit) -> (st,List.sort compare th,List.sort compare wit))
trips
-
+
(* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
(1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
;;
let compatible_states = function
- (PosState s1, PosState s2) ->
+ (PosState s1, PosState s2) ->
if s1 = s2 then Some (PosState s1) else None
- | (PosState s1, NegState s2) ->
+ | (PosState s1, NegState s2) ->
if List.mem s1 s2 then None else Some (PosState s1)
- | (NegState s1, PosState s2) ->
+ | (NegState s1, PosState s2) ->
if List.mem s2 s1 then None else Some (PosState s2)
| (NegState s1, NegState s2) -> Some (NegState (s1 @ s2))
;;
shared trips
;;
-let triple_negate (s,th,wits) =
+let triple_negate (s,th,wits) =
let negstates = (NegState [s],top_subst,top_wit) in
let negths = map (fun th -> (PosState s,th,top_wit)) (negate_subst th) in
let negwits = map (fun nwit -> (PosState s,th,nwit)) (negate_wits wits) in
(negstates x @ negths x @ negwits x) xs)
;;
-let triple_negate (s,th,wits) =
+let triple_negate (s,th,wits) =
let negths = map (fun th -> (s,th,top_wit)) (negate_subst th) in
let negwits = map (fun nwit -> (s,th,nwit)) (negate_wits wits) in
([s], negths @ negwits) (* all different *)
List.for_all (function A.NegWit _ -> true | A.Wit _ -> false) in
let negtopos =
List.map (function A.NegWit w -> w | A.Wit _ -> failwith "bad wit")in
- let res =
+ let res =
List.fold_left
(function prev ->
function (s,th,wit) as t ->
| _ ->
(*normalize*)
(foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
-
+
let pre_forall_AW dir (grp,_,states) y all reqst =
let check s =
match reqst with
match neighbor_triples with
[] -> []
| _ -> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
-
+
(* drop_negwits will call setify *)
let satEX dir m s reqst = pre_exist dir m s reqst;;
-
+
let satAX dir m s reqst = pre_forall dir m s s reqst
;;
(* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
-let satEU dir ((_,_,states) as m) s1 s2 reqst print_graph =
- let ctr = ref 0 in
+let satEU dir ((_,_,states) as m) s1 s2 reqst print_graph =
+ (*Printf.printf "EU\n";
+ let ctr = ref 0 in*)
inc satEU_calls;
if s1 = []
then s2
match new_info with
[] -> y
| new_info ->
- ctr := !ctr + 1;
- print_graph y ctr;
+ (*ctr := !ctr + 1;
+ print_graph y ctr;*)
let first = triples_conj s1 (pre_exist dir m new_info reqst) in
let res = triples_union first y in
let new_info = setdiff res y in
(*Printf.printf "iter %d res %d new_info %d\n"
!ctr (List.length res) (List.length new_info);
+ print_state "res" res;
+ print_state "new_info" new_info;
flush stdout;*)
f res new_info in
f s2 s2
else
let f y =
inc_step();
- ctr := !ctr + 1;
- print_graph y ctr;
+ (*ctr := !ctr + 1;
+ print_graph y ctr;*)
let pre = pre_exist dir m y reqst in
triples_union s2 (triples_conj s1 pre) in
setfix f s2
;;
(* EF phi == E[true U phi] *)
-let satEF dir m s2 reqst =
+let satEF dir m s2 reqst =
inc satEF_calls;
(*let ctr = ref 0 in*)
if !pNEW_INFO_OPT
print_state "y" y;
flush stdout;*)
let pre = pre_forall dir m y y reqst in
+ (*print_state "pre" pre;*)
let conj = triples_conj s1 pre in (* or triples_conj_AW *)
triples_union s2 conj in
- setgfix f (triples_union s1 s2)
+ let drop_wits = List.map (function (s,e,_) -> (s,e,[])) in
+ (* drop wits on s1 represents that we don't want any witnesses from
+ the case that infinitely loops, only from the case that gets
+ out of the loop. s1 is like a guard. To see the problem, consider
+ an example where both s1 and s2 match some code after the loop.
+ we only want the witness from s2. *)
+ setgfix f (triples_union (nub(drop_wits s1)) s2)
;;
-let satAF dir m s reqst =
+let satAF dir m s reqst =
inc satAF_calls;
if !pNEW_INFO_OPT
then
(* **************************************************************** *)
(* applied to the result of matching a node. collect witnesses when the
states and environments are the same *)
+(* not a good idea, poses problem for unparsing, because don't realize that
+adjacent things come from different matches, leading to loss of newlines etc.
+exple struct I { ... - int x; + int y; ...} *)
-let inner_and trips =
+let inner_and trips = trips (*
let rec loop = function
[] -> ([],[])
| (s,th,w)::trips ->
| _ -> ([(s,th,w)],cur@acc)) in
let (cur,acc) =
loop (List.sort state_compare trips) (* is this sort needed? *) in
- cur@acc
+ cur@acc *)
(* *************** *)
(* Partial matches *)
triples_union res fail_left
else res
-let strict_A1 strict op failop dir ((_,_,states) as m) trips required_states =
+let strict_A1 strict op failop dir ((_,_,states) as m) trips required_states =
let res = op dir m trips required_states in
if !Flag_ctl.partial_match && strict = A.STRICT
then
else res
let strict_A2 strict op failop dir ((_,_,states) as m) trips trips'
- required_states =
+ required_states =
let res = op dir m trips trips' required_states in
if !Flag_ctl.partial_match && strict = A.STRICT
then
let fail = filter_conj states res (failop dir m trips' required_states) in
triples_union res fail
else res
-
+
let strict_A2au strict op failop dir ((_,_,states) as m) trips trips'
- required_states print_graph =
+ required_states print_graph =
match op dir m trips trips' required_states print_graph with
AUok res ->
if !Flag_ctl.partial_match && strict = A.STRICT
AUok (triples_union res fail)
else AUok res
| AUfailed res -> AUfailed res
-
+
(* ********************* *)
(* Environment functions *)
(* ********************* *)
(* no graph, for the moment *)
(fun y str -> ()))
s1 in
- strict_A2 strict satAW satEF dir m s1 s2 new_required_states)
+ strict_A2 strict satAW satEF dir m s1 s2 new_required_states
+ )
| A.Implies(phi1,phi2) ->
loop unchecked required required_states (A.Or(A.Not phi1,phi2))
| A.Exists (keep,v,phi) ->
let res = drop_wits required_states res phi (* ) *) in
print_graph grp required_states res "" phi;
res in
-
+
loop unchecked required required_states phi
-;;
+;;
(* SAT with tracking *)
let (child1,res1) = satv unchecked required required_states phi1 env in
Printf.printf "uncheck\n"; flush stdout;
anno res1 [child1]
- | A.Not(phi1) ->
+ | A.Not(phi1) ->
let (child,res) =
satv unchecked required required_states phi1 env in
Printf.printf "not\n"; flush stdout;
anno (triples_complement (mkstates states required_states) res) [child]
- | A.Or(phi1,phi2) ->
+ | A.Or(phi1,phi2) ->
let (child1,res1) =
satv unchecked required required_states phi1 env in
let (child2,res2) =
satv unchecked required required_states phi2 env in
Printf.printf "or\n"; flush stdout;
anno (triples_union res1 res2) [child1; child2]
- | A.SeqOr(phi1,phi2) ->
+ | A.SeqOr(phi1,phi2) ->
let (child1,res1) =
satv unchecked required required_states phi1 env in
let (child2,res2) =
res1neg)
res2))
[child1; child2]
- | A.And(strict,phi1,phi2) ->
+ | A.And(strict,phi1,phi2) ->
let pm = !Flag_ctl.partial_match in
(match (pm,satv unchecked required required_states phi1 env) with
(false,(child1,[])) ->
res1 res2 in
anno res [child1; child2]))
| A.AndAny(dir,strict,phi1,phi2) ->
- let pm = !Flag_ctl.partial_match in
+ let pm = !Flag_ctl.partial_match in
(match (pm,satv unchecked required required_states phi1 env) with
(false,(child1,[])) ->
Printf.printf "and\n"; flush stdout; anno [] [child1]
[] -> (* !Flag_ctl.partial_match must be true *)
if res2 = []
then anno [] [child1; child2]
- else
+ else
let res =
let s = mkstates states required_states in
List.fold_left
failwith
"only one result allowed for the left arg of AndAny")))
| A.HackForStmt(dir,strict,phi1,phi2) ->
- let pm = !Flag_ctl.partial_match in
+ let pm = !Flag_ctl.partial_match in
(match (pm,satv unchecked required required_states phi1 env) with
(false,(child1,[])) ->
Printf.printf "and\n"; flush stdout; anno [] [child1]
let (child1,res1) = satv unchecked required required_states phi1 env in
Printf.printf "uncheck\n"; flush stdout;
anno (inner_and res1) [child1]
- | A.EX(dir,phi1) ->
+ | A.EX(dir,phi1) ->
let new_required_states =
get_children_required_states dir m required_states in
let (child,res) =
satv unchecked required new_required_states phi1 env in
Printf.printf "EX\n"; flush stdout;
anno (satEX dir m res required_states) [child]
- | A.AX(dir,strict,phi1) ->
+ | A.AX(dir,strict,phi1) ->
let new_required_states =
get_children_required_states dir m required_states in
let (child,res) =
Printf.printf "AX\n"; flush stdout;
let res = strict_A1 strict satAX satEX dir m res required_states in
anno res [child]
- | A.EF(dir,phi1) ->
+ | A.EF(dir,phi1) ->
let new_required_states = get_reachable dir m required_states in
let (child,res) =
satv unchecked required new_required_states phi1 env in
Printf.printf "EF\n"; flush stdout;
anno (satEF dir m res new_required_states) [child]
- | A.AF(dir,strict,phi1) ->
+ | A.AF(dir,strict,phi1) ->
if !Flag_ctl.loop_in_src_code
then
satv unchecked required required_states
let res =
strict_A1 strict satAF satEF dir m res new_required_states in
anno res [child])
- | A.EG(dir,phi1) ->
+ | A.EG(dir,phi1) ->
let new_required_states = get_reachable dir m required_states in
let (child,res) =
satv unchecked required new_required_states phi1 env in
Printf.printf "EG\n"; flush stdout;
anno (satEG dir m res new_required_states) [child]
- | A.AG(dir,strict,phi1) ->
+ | A.AG(dir,strict,phi1) ->
let new_required_states = get_reachable dir m required_states in
let (child,res) =
satv unchecked required new_required_states phi1 env in
Printf.printf "AG\n"; flush stdout;
let res = strict_A1 strict satAG satEF dir m res new_required_states in
anno res [child]
-
- | A.EU(dir,phi1,phi2) ->
+
+ | A.EU(dir,phi1,phi2) ->
let new_required_states = get_reachable dir m required_states in
(match satv unchecked required new_required_states phi2 env with
(child2,[]) ->
Printf.printf "EU\n"; flush stdout;
anno (satEU dir m res1 res2 new_required_states (fun y str -> ()))
[child1; child2])
- | A.AW(dir,strict,phi1,phi2) ->
+ | A.AW(dir,strict,phi1,phi2) ->
failwith "should not be used" (*
let new_required_states = get_reachable dir m required_states in
(match satv unchecked required new_required_states phi2 env with
strict_A2 strict satAW satEF dir m res1 res2
new_required_states in
anno res [child1; child2]) *)
- | A.AU(dir,strict,phi1,phi2) ->
+ | A.AU(dir,strict,phi1,phi2) ->
let new_required_states = get_reachable dir m required_states in
(match satv unchecked required new_required_states phi2 env with
(child2,[]) ->
let res =
strict_A2 strict satAW satEF dir m s1 s2 new_required_states in
anno res [child1; child2]))
- | A.Implies(phi1,phi2) ->
+ | A.Implies(phi1,phi2) ->
satv unchecked required required_states
(A.Or(A.Not phi1,phi2))
env
- | A.Exists (keep,v,phi1) ->
+ | A.Exists (keep,v,phi1) ->
let new_required = drop_required v required in
let (child,res) =
satv unchecked new_required required_states phi1 env in
print_required_states required_states;
print_state "after drop_wits" res1 end;
(child,res1)
-
+
;;
let sat_verbose annotate maxlvl lvl m phi =
*)
let simpleanno l phi res =
- let pp s =
- Format.print_string ("\n" ^ s ^ "\n------------------------------\n");
+ let pp s =
+ Format.print_string ("\n" ^ s ^ "\n------------------------------\n");
print_generic_algo (List.sort compare res);
Format.print_string "\n------------------------------\n\n" in
let pp_dir = function
(* pad: Rene, you can now use the module pretty_print_ctl.ml to
print a ctl formula more accurately if you want.
- Use the print_xxx provided in the different module to call
+ Use the print_xxx provided in the different module to call
Pretty_print_ctl.pp_ctl.
*)
-let simpleanno2 l phi res =
+let simpleanno2 l phi res =
begin
Pretty_print_ctl.pp_ctl (P.print_predicate, SUB.print_mvar) false phi;
Format.print_newline ();
(List.iter (print_state "a state") answers;
Printf.printf "something doesn't work\n");
res)
-
+
let print_bench _ =
let iterct = !Flag_ctl.bench in
if iterct > 0
Printf.printf "triples: %d\n" !triples;
print_state "final result" res;
*)
- res)
+ List.sort compare res)
else
(if !Flag_ctl.verbose_ctl_engine
then Common.pr2 "missing something required";
(* ********************************************************************** *)
end
;;
-
HCoop / bpt / coccinelle.git / blobdiff