2 * Copyright 2005-2008, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
23 (*external c_counter : unit -> int = "c_counter"*)
25 (* Optimize triples_conj by first extracting the intersection of the two sets,
26 which can certainly be in the intersection *)
27 let pTRIPLES_CONJ_OPT = ref true
28 (* For complement, make NegState for the negation of a single state *)
29 let pTRIPLES_COMPLEMENT_OPT = ref true
30 (* For complement, do something special for the case where the environment
31 and witnesses are empty *)
32 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
33 (* "Double negate" the arguments of the path operators *)
34 let pDOUBLE_NEGATE_OPT = ref true
35 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
36 let pNEW_INFO_OPT = ref true
37 (* Filter the result of the label function to drop entries that aren't
38 compatible with any of the available environments *)
39 let pREQUIRED_ENV_OPT = ref true
40 (* Memoize the raw result of the label function *)
41 let pSATLABEL_MEMO_OPT = ref true
42 (* Filter results according to the required states *)
43 let pREQUIRED_STATES_OPT = ref true
44 (* Drop negative witnesses at Uncheck *)
45 let pUNCHECK_OPT = ref true
46 let pANY_NEG_OPT = ref true
47 let pLazyOpt = ref true
50 let pTRIPLES_CONJ_OPT = ref false
51 let pTRIPLES_COMPLEMENT_OPT = ref false
52 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
53 let pDOUBLE_NEGATE_OPT = ref false
54 let pNEW_INFO_OPT = ref false
55 let pREQUIRED_ENV_OPT = ref false
56 let pSATLABEL_MEMO_OPT = ref false
57 let pREQUIRED_STATES_OPT = ref false
58 let pUNCHECK_OPT = ref false
59 let pANY_NEG_OPT = ref false
60 let pLazyOpt = ref false
64 let step_count = ref 0
67 if not (!step_count = 0)
70 step_count := !step_count - 1;
71 if !step_count = 0 then raise Steps
74 let inc cell = cell := !cell + 1
76 let satEU_calls = ref 0
77 let satAW_calls = ref 0
78 let satAU_calls = ref 0
79 let satEF_calls = ref 0
80 let satAF_calls = ref 0
81 let satEG_calls = ref 0
82 let satAG_calls = ref 0
90 Printf.sprintf "_fresh_r_%d" c
92 (* **********************************************************************
94 * Implementation of a Witness Tree model checking engine for CTL-FVex
97 * **********************************************************************)
99 (* ********************************************************************** *)
100 (* Module: SUBST (substitutions: meta. vars and values) *)
101 (* ********************************************************************** *)
107 val eq_mvar: mvar -> mvar -> bool
108 val eq_val: value -> value -> bool
109 val merge_val: value -> value -> value
110 val print_mvar : mvar -> unit
111 val print_value : value -> unit
115 (* ********************************************************************** *)
116 (* Module: GRAPH (control flow graphs / model) *)
117 (* ********************************************************************** *)
123 val predecessors: cfg -> node -> node list
124 val successors: cfg -> node -> node list
125 val extract_is_loop : cfg -> node -> bool
126 val print_node : node -> unit
127 val size : cfg -> int
131 module OGRAPHEXT_GRAPH =
134 type cfg = (string,unit) Ograph_extended.ograph_mutable;;
135 let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist);;
136 let print_node i = Format.print_string (Common.i_to_s i)
140 (* ********************************************************************** *)
141 (* Module: PREDICATE (predicates for CTL formulae) *)
142 (* ********************************************************************** *)
144 module type PREDICATE =
147 val print_predicate : t -> unit
151 (* ********************************************************************** *)
153 (* ---------------------------------------------------------------------- *)
154 (* Misc. useful generic functions *)
155 (* ---------------------------------------------------------------------- *)
165 let foldl = List.fold_left;;
167 let foldl1 f xs = foldl f (head xs) (tail xs)
169 type 'a esc = ESC of 'a | CONT of 'a
171 let foldr = List.fold_right;;
173 let concat = List.concat;;
177 let filter = List.filter;;
179 let partition = List.partition;;
181 let concatmap f l = List.concat (List.map f l);;
189 let some_map f opts = map (maybe (fun x -> Some (f x)) None) opts
191 let some_tolist_alt opts = concatmap (maybe (fun x -> [x]) []) opts
193 let rec some_tolist opts =
196 | (Some x)::rest -> x::(some_tolist rest)
197 | _::rest -> some_tolist rest
200 let rec groupBy eq l =
204 let (xs1,xs2) = partition (fun x' -> eq x x') xs in
205 (x::xs1)::(groupBy eq xs2)
208 let group l = groupBy (=) l;;
210 let rec memBy eq x l =
213 | (y::ys) -> if (eq x y) then true else (memBy eq x ys)
216 let rec nubBy eq ls =
219 | (x::xs) when (memBy eq x xs) -> nubBy eq xs
220 | (x::xs) -> x::(nubBy eq xs)
226 | (x::xs) when (List.mem x xs) -> nub xs
227 | (x::xs) -> x::(nub xs)
230 let state_compare (s1,_,_) (s2,_,_) = compare s1 s2
232 let setifyBy eq xs = nubBy eq xs;;
234 let setify xs = nub xs;;
236 let inner_setify xs = List.sort compare (nub xs);;
238 let unionBy compare eq xs = function
241 let rec loop = function
243 | x::xs -> if memBy eq x ys then loop xs else x::(loop xs) in
244 List.sort compare (loop xs)
247 let union xs ys = unionBy state_compare (=) xs ys;;
249 let setdiff xs ys = filter (fun x -> not (List.mem x ys)) xs;;
251 let subseteqBy eq xs ys = List.for_all (fun x -> memBy eq x ys) xs;;
253 let subseteq xs ys = List.for_all (fun x -> List.mem x ys) xs;;
254 let supseteq xs ys = subseteq ys xs
256 let setequalBy eq xs ys = (subseteqBy eq xs ys) & (subseteqBy eq ys xs);;
258 let setequal xs ys = (subseteq xs ys) & (subseteq ys xs);;
260 (* Fix point calculation *)
262 let x' = f x in if (eq x' x) then x' else fix eq f x'
265 (* Fix point calculation on set-valued functions *)
266 let setfix f x = (fix subseteq f x) (*if new is a subset of old, stop*)
267 let setgfix f x = (fix supseteq f x) (*if new is a supset of old, stop*)
269 let get_states l = nub (List.map (function (s,_,_) -> s) l)
271 (* ********************************************************************** *)
272 (* Module: CTL_ENGINE *)
273 (* ********************************************************************** *)
276 functor (SUB : SUBST) ->
277 functor (G : GRAPH) ->
278 functor (P : PREDICATE) ->
283 type substitution = (SUB.mvar, SUB.value) Ast_ctl.generic_substitution
285 type ('pred,'anno) witness =
286 (G.node, substitution,
287 ('pred, SUB.mvar, 'anno) Ast_ctl.generic_ctl list)
288 Ast_ctl.generic_witnesstree
290 type ('pred,'anno) triples =
291 (G.node * substitution * ('pred,'anno) witness list) list
293 (* ---------------------------------------------------------------------- *)
294 (* Pretty printing functions *)
295 (* ---------------------------------------------------------------------- *)
297 let (print_generic_substitution : substitution -> unit) = fun substxs ->
298 let print_generic_subst = function
300 SUB.print_mvar mvar; Format.print_string " --> "; SUB.print_value v
301 | A.NegSubst (mvar, v) ->
302 SUB.print_mvar mvar; Format.print_string " -/-> "; SUB.print_value v in
303 Format.print_string "[";
304 Common.print_between (fun () -> Format.print_string ";" )
305 print_generic_subst substxs;
306 Format.print_string "]"
308 let rec (print_generic_witness: ('pred, 'anno) witness -> unit) =
310 | A.Wit (state, subst, anno, childrens) ->
311 Format.print_string "wit ";
313 print_generic_substitution subst;
314 (match childrens with
315 [] -> Format.print_string "{}"
317 Format.force_newline(); Format.print_string " "; Format.open_box 0;
318 print_generic_witnesstree childrens; Format.close_box())
320 Format.print_string "!";
321 print_generic_witness wit
323 and (print_generic_witnesstree: ('pred,'anno) witness list -> unit) =
326 Format.print_string "{";
328 (fun () -> Format.print_string ";"; Format.force_newline() )
329 print_generic_witness witnesstree;
330 Format.print_string "}";
333 and print_generic_triple (node,subst,tree) =
335 print_generic_substitution subst;
336 print_generic_witnesstree tree
338 and (print_generic_algo : ('pred,'anno) triples -> unit) = fun xs ->
339 Format.print_string "<";
341 (fun () -> Format.print_string ";"; Format.force_newline())
342 print_generic_triple xs;
343 Format.print_string ">"
346 let print_state (str : string) (l : ('pred,'anno) triples) =
347 Printf.printf "%s\n" str;
348 List.iter (function x ->
349 print_generic_triple x; Format.print_newline(); flush stdout)
350 (List.sort compare l);
353 let print_required_states = function
354 None -> Printf.printf "no required states\n"
356 Printf.printf "required states: ";
359 G.print_node x; Format.print_string " "; Format.print_flush())
363 let mkstates states = function
365 | Some states -> states
367 (* ---------------------------------------------------------------------- *)
369 (* ---------------------------------------------------------------------- *)
372 (* ************************* *)
374 (* ************************* *)
379 | A.NegSubst(x,_) -> x
385 | A.NegSubst(_,x) -> x
388 let eq_subBy eqx eqv sub sub' =
389 match (sub,sub') with
390 | (A.Subst(x,v),A.Subst(x',v')) -> (eqx x x') && (eqv v v')
391 | (A.NegSubst(x,v),A.NegSubst(x',v')) -> (eqx x x') && (eqv v v')
396 let eq_sub sub sub' = eq_subBy SUB.eq_mvar SUB.eq_val sub sub'
398 let eq_subst th th' = setequalBy eq_sub th th';;
400 let merge_subBy eqx (===) (>+<) sub sub' =
401 (* variable part is guaranteed to be the same *)
402 match (sub,sub') with
403 (A.Subst (x,v),A.Subst (x',v')) ->
405 then Some [A.Subst(x, v >+< v')]
407 | (A.NegSubst(x,v),A.Subst(x',v')) ->
409 then Some [A.Subst(x',v')]
411 | (A.Subst(x,v),A.NegSubst(x',v')) ->
413 then Some [A.Subst(x,v)]
415 | (A.NegSubst(x,v),A.NegSubst(x',v')) ->
418 let merged = v >+< v' in
419 if merged = v && merged = v'
420 then Some [A.NegSubst(x,v >+< v')]
422 (* positions are compatible, but not identical. keep apart. *)
423 Some [A.NegSubst(x,v);A.NegSubst(x',v')]
424 else Some [A.NegSubst(x,v);A.NegSubst(x',v')]
428 let merge_sub sub sub' =
429 merge_subBy SUB.eq_mvar SUB.eq_val SUB.merge_val sub sub'
431 let clean_substBy eq cmp theta = List.sort cmp (nubBy eq theta);;
433 (* NOTE: we sort by using the generic "compare" on (meta-)variable
434 * names; we could also require a definition of compare for meta-variables
435 * or substitutions but that seems like overkill for sorting
437 let clean_subst theta =
441 let res = compare (dom_sub s) (dom_sub s') in
445 (A.Subst(_,_),A.NegSubst(_,_)) -> -1
446 | (A.NegSubst(_,_),A.Subst(_,_)) -> 1
447 | _ -> compare (ran_sub s) (ran_sub s')
450 let rec loop = function
452 | (A.Subst(x,v)::A.NegSubst(y,v')::rest) when SUB.eq_mvar x y ->
453 loop (A.Subst(x,v)::rest)
454 | x::xs -> x::(loop xs) in
457 let top_subst = [];; (* Always TRUE subst. *)
459 (* Split a theta in two parts: one with (only) "x" and one without *)
461 let split_subst theta x =
462 partition (fun sub -> SUB.eq_mvar (dom_sub sub) x) theta;;
464 exception SUBST_MISMATCH
465 let conj_subst theta theta' =
466 match (theta,theta') with
467 | ([],_) -> Some theta'
468 | (_,[]) -> Some theta
470 let rec classify = function
472 | [x] -> [(dom_sub x,[x])]
474 (match classify xs with
475 ((nm,y)::ys) as res ->
478 else (dom_sub x,[x])::res
479 | _ -> failwith "not possible") in
480 let merge_all theta theta' =
487 match (merge_sub sub sub') with
488 Some subs -> subs @ rest
489 | _ -> raise SUBST_MISMATCH)
492 let rec loop = function
494 List.concat (List.map (function (_,ths) -> ths) ctheta')
496 List.concat (List.map (function (_,ths) -> ths) ctheta)
497 | ((x,ths)::xs,(y,ths')::ys) ->
498 (match compare x y with
499 0 -> (merge_all ths ths') @ loop (xs,ys)
500 | -1 -> ths @ loop (xs,((y,ths')::ys))
501 | 1 -> ths' @ loop (((x,ths)::xs),ys)
502 | _ -> failwith "not possible") in
503 try Some (clean_subst(loop (classify theta, classify theta')))
504 with SUBST_MISMATCH -> None
507 (* theta' must be a subset of theta *)
508 let conj_subst_none theta theta' =
509 match (theta,theta') with
510 | (_,[]) -> Some theta
513 let rec classify = function
515 | [x] -> [(dom_sub x,[x])]
517 (match classify xs with
518 ((nm,y)::ys) as res ->
521 else (dom_sub x,[x])::res
522 | _ -> failwith "not possible") in
523 let merge_all theta theta' =
530 match (merge_sub sub sub') with
531 Some subs -> subs @ rest
532 | _ -> raise SUBST_MISMATCH)
535 let rec loop = function
537 List.concat (List.map (function (_,ths) -> ths) ctheta)
538 | ([],ctheta') -> raise SUBST_MISMATCH
539 | ((x,ths)::xs,(y,ths')::ys) ->
540 (match compare x y with
541 0 -> (merge_all ths ths') @ loop (xs,ys)
542 | -1 -> ths @ loop (xs,((y,ths')::ys))
543 | 1 -> raise SUBST_MISMATCH
544 | _ -> failwith "not possible") in
545 try Some (clean_subst(loop (classify theta, classify theta')))
546 with SUBST_MISMATCH -> None
551 | A.Subst(x,v) -> A.NegSubst (x,v)
552 | A.NegSubst(x,v) -> A.Subst(x,v)
555 (* Turn a (big) theta into a list of (small) thetas *)
556 let negate_subst theta = (map (fun sub -> [negate_sub sub]) theta);;
559 (* ************************* *)
561 (* ************************* *)
563 (* Always TRUE witness *)
564 let top_wit = ([] : (('pred, 'anno) witness list));;
566 let eq_wit wit wit' = wit = wit';;
568 let union_wit wit wit' = (*List.sort compare (wit' @ wit) for popl*)
569 let res = unionBy compare (=) wit wit' in
570 let anynegwit = (* if any is neg, then all are *)
571 List.exists (function A.NegWit _ -> true | A.Wit _ -> false) in
573 then List.filter (function A.NegWit _ -> true | A.Wit _ -> false) res
576 let negate_wit wit = A.NegWit wit (*
578 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
579 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
582 let negate_wits wits =
583 List.sort compare (map (fun wit -> [negate_wit wit]) wits);;
586 let anynegwit = (* if any is neg, then all are *)
587 List.exists (function A.NegWit _ -> true | A.Wit _ -> false) in
591 function (s,th,wit) ->
592 if anynegwit wit then prev else (s,th,top_wit)::prev)
595 (* ************************* *)
597 (* ************************* *)
599 (* Triples are equal when the constituents are equal *)
600 let eq_trip (s,th,wit) (s',th',wit') =
601 (s = s') && (eq_wit wit wit') && (eq_subst th th');;
603 let triples_top states = map (fun s -> (s,top_subst,top_wit)) states;;
605 let normalize trips =
607 (function (st,th,wit) -> (st,List.sort compare th,List.sort compare wit))
611 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
612 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
613 let triples_conj trips trips' =
614 let (trips,shared,trips') =
615 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
618 List.partition (function t -> List.mem t trips') trips in
620 List.filter (function t -> not(List.mem t shared)) trips' in
621 (trips,shared,trips')
622 else (trips,[],trips') in
623 foldl (* returns a set - setify inlined *)
625 function (s1,th1,wit1) ->
628 function (s2,th2,wit2) ->
630 (match (conj_subst th1 th2) with
632 let t = (s1,th,union_wit wit1 wit2) in
633 if List.mem t rest then rest else t::rest
640 (* ignore the state in the right argument. always pretend it is the same as
642 (* env on right has to be a subset of env on left *)
643 let triples_conj_none trips trips' =
644 let (trips,shared,trips') =
645 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
648 List.partition (function t -> List.mem t trips') trips in
650 List.filter (function t -> not(List.mem t shared)) trips' in
651 (trips,shared,trips')
652 else (trips,[],trips') in
653 foldl (* returns a set - setify inlined *)
655 function (s1,th1,wit1) ->
658 function (s2,th2,wit2) ->
659 match (conj_subst_none th1 th2) with
661 let t = (s1,th,union_wit wit1 wit2) in
662 if List.mem t rest then rest else t::rest
670 let triples_conj_AW trips trips' =
671 let (trips,shared,trips') =
672 if false && !pTRIPLES_CONJ_OPT
675 List.partition (function t -> List.mem t trips') trips in
677 List.filter (function t -> not(List.mem t shared)) trips' in
678 (trips,shared,trips')
679 else (trips,[],trips') in
680 foldl (* returns a set - setify inlined *)
682 function (s1,th1,wit1) ->
685 function (s2,th2,wit2) ->
687 (match (conj_subst th1 th2) with
689 let t = (s1,th,union_wit wit1 wit2) in
690 if List.mem t rest then rest else t::rest
697 (* *************************** *)
698 (* NEGATION (NegState style) *)
699 (* *************************** *)
701 (* Constructive negation at the state level *)
704 | NegState of 'a list
707 let compatible_states = function
708 (PosState s1, PosState s2) ->
709 if s1 = s2 then Some (PosState s1) else None
710 | (PosState s1, NegState s2) ->
711 if List.mem s1 s2 then None else Some (PosState s1)
712 | (NegState s1, PosState s2) ->
713 if List.mem s2 s1 then None else Some (PosState s2)
714 | (NegState s1, NegState s2) -> Some (NegState (s1 @ s2))
717 (* Conjunction on triples with "special states" *)
718 let triples_state_conj trips trips' =
719 let (trips,shared,trips') =
720 if !pTRIPLES_CONJ_OPT
723 List.partition (function t -> List.mem t trips') trips in
725 List.filter (function t -> not(List.mem t shared)) trips' in
726 (trips,shared,trips')
727 else (trips,[],trips') in
730 function (s1,th1,wit1) ->
733 function (s2,th2,wit2) ->
734 match compatible_states(s1,s2) with
736 (match (conj_subst th1 th2) with
738 let t = (s,th,union_wit wit1 wit2) in
739 if List.mem t rest then rest else t::rest
746 let triple_negate (s,th,wits) =
747 let negstates = (NegState [s],top_subst,top_wit) in
748 let negths = map (fun th -> (PosState s,th,top_wit)) (negate_subst th) in
749 let negwits = map (fun nwit -> (PosState s,th,nwit)) (negate_wits wits) in
750 negstates :: (negths @ negwits) (* all different *)
752 (* FIX ME: it is not necessary to do full conjunction *)
753 let triples_complement states (trips : ('pred, 'anno) triples) =
754 if !pTRIPLES_COMPLEMENT_OPT
756 (let cleanup (s,th,wit) =
758 PosState s' -> [(s',th,wit)]
760 assert (th=top_subst);
761 assert (wit=top_wit);
762 map (fun st -> (st,top_subst,top_wit)) (setdiff states ss) in
763 let (simple,complex) =
764 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
766 let (simple,complex) =
767 List.partition (function (s,[],[]) -> true | _ -> false) trips in
769 [(NegState(List.map (function (s,_,_) -> s) simple),
770 top_subst,top_wit)] in
772 else ([(NegState [],top_subst,top_wit)],trips) in
773 let rec compl trips =
776 | (t::ts) -> triples_state_conj (triple_negate t) (compl ts) in
777 let compld = (compl complex) in
778 let compld = concatmap cleanup compld in
781 let negstates (st,th,wits) =
782 map (function st -> (st,top_subst,top_wit)) (setdiff states [st]) in
783 let negths (st,th,wits) =
784 map (function th -> (st,th,top_wit)) (negate_subst th) in
785 let negwits (st,th,wits) =
786 map (function nwit -> (st,th,nwit)) (negate_wits wits) in
788 [] -> map (function st -> (st,top_subst,top_wit)) states
794 triples_conj (negstates cur @ negths cur @ negwits cur) prev)
795 (negstates x @ negths x @ negwits x) xs)
798 let triple_negate (s,th,wits) =
799 let negths = map (fun th -> (s,th,top_wit)) (negate_subst th) in
800 let negwits = map (fun nwit -> (s,th,nwit)) (negate_wits wits) in
801 ([s], negths @ negwits) (* all different *)
803 let print_compl_state str (n,p) =
804 Printf.printf "%s neg: " str;
806 (function x -> G.print_node x; Format.print_flush(); Printf.printf " ")
811 let triples_complement states (trips : ('pred, 'anno) triples) =
813 then map (function st -> (st,top_subst,top_wit)) states
815 let cleanup (neg,pos) =
817 List.filter (function (s,_,_) -> List.mem s neg) pos in
818 (map (fun st -> (st,top_subst,top_wit)) (setdiff states neg)) @
820 let trips = List.sort state_compare trips in
821 let all_negated = List.map triple_negate trips in
822 let merge_one (neg1,pos1) (neg2,pos2) =
823 let (pos1conj,pos1keep) =
824 List.partition (function (s,_,_) -> List.mem s neg2) pos1 in
825 let (pos2conj,pos2keep) =
826 List.partition (function (s,_,_) -> List.mem s neg1) pos2 in
827 (Common.union_set neg1 neg2,
828 (triples_conj pos1conj pos2conj) @ pos1keep @ pos2keep) in
829 let rec inner_loop = function
830 x1::x2::rest -> (merge_one x1 x2) :: (inner_loop rest)
832 let rec outer_loop = function
834 | l -> outer_loop (inner_loop l) in
835 cleanup (outer_loop all_negated)
837 (* ********************************** *)
838 (* END OF NEGATION (NegState style) *)
839 (* ********************************** *)
841 (* now this is always true, so we could get rid of it *)
842 let something_dropped = ref true
844 let triples_union trips trips' =
845 (*unionBy compare eq_trip trips trips';;*)
846 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
848 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
849 Then, the following says that since the first is a more restrictive
850 environment and has fewer witnesses, then it should be dropped. But having
851 fewer witnesses is not necessarily less informative than having more,
852 because fewer witnesses can mean the absence of the witness-causing thing.
853 So the fewer witnesses have to be kept around.
854 subseteq changed to = to make it hopefully work
859 something_dropped := false;
861 then (something_dropped := true; trips)
863 let subsumes (s1,th1,wit1) (s2,th2,wit2) =
866 (match conj_subst th1 th2 with
869 then if (*subseteq*) wit1 = wit2 then 1 else 0
872 then if (*subseteq*) wit2 = wit1 then (-1) else 0
876 let rec first_loop second = function
878 | x::xs -> first_loop (second_loop x second) xs
879 and second_loop x = function
882 match subsumes x y with
883 1 -> something_dropped := true; all
884 | (-1) -> second_loop x ys
885 | _ -> y::(second_loop x ys) in
886 first_loop trips trips'
888 else unionBy compare eq_trip trips trips'
891 let triples_witness x unchecked not_keep trips =
892 let anyneg = (* if any is neg, then all are *)
893 List.exists (function A.NegSubst _ -> true | A.Subst _ -> false) in
894 let anynegwit = (* if any is neg, then all are *)
895 List.exists (function A.NegWit _ -> true | A.Wit _ -> false) in
896 let allnegwit = (* if any is neg, then all are *)
897 List.for_all (function A.NegWit _ -> true | A.Wit _ -> false) in
899 List.map (function A.NegWit w -> w | A.Wit _ -> failwith "bad wit")in
903 function (s,th,wit) as t ->
904 let (th_x,newth) = split_subst th x in
907 (* one consider whether if not not_keep is true, then we should
908 fail. but it could be that the variable is a used_after and
909 then it is the later rule that should fail and not this one *)
910 if not not_keep && !Flag_ctl.verbose_ctl_engine
912 (SUB.print_mvar x; Format.print_flush();
913 print_state ": empty witness from" [t]);
915 | l when anyneg l && !pANY_NEG_OPT -> prev
916 (* see tests/nestseq for how neg bindings can come up even
917 without eg partial matches
918 (* negated substitution only allowed with negwits.
920 if anynegwit wit && allnegwit wit (* nonempty negwit list *)
923 (print_generic_substitution l; Format.print_newline();
924 failwith"unexpected negative binding with positive witnesses")*)
927 if unchecked or not_keep
930 if anynegwit wit && allnegwit wit
931 then (s,newth,[A.NegWit(A.Wit(s,th_x,[],negtopos wit))])
932 else (s,newth,[A.Wit(s,th_x,[],wit)]) in
935 if unchecked || !Flag_ctl.partial_match (* the only way to have a NegWit *)
941 (* ---------------------------------------------------------------------- *)
942 (* SAT - Model Checking Algorithm for CTL-FVex *)
944 (* TODO: Implement _all_ operators (directly) *)
945 (* ---------------------------------------------------------------------- *)
948 (* ************************************* *)
949 (* The SAT algorithm and special helpers *)
950 (* ************************************* *)
952 let rec pre_exist dir (grp,_,_) y reqst =
954 match reqst with None -> true | Some reqst -> List.mem s reqst in
957 (fun s' -> if check s' then [(s',th,wit)] else [])
959 A.FORWARD -> G.predecessors grp s
960 | A.BACKWARD -> G.successors grp s) in
961 setify (concatmap exp y)
966 let pre_forall dir (grp,_,states) y all reqst =
969 None -> true | Some reqst -> List.mem s reqst in
972 A.FORWARD -> G.predecessors | A.BACKWARD -> G.successors in
975 A.FORWARD -> G.successors | A.BACKWARD -> G.predecessors in
978 (function p -> (p,succ grp p))
981 (function (s,_,_) -> List.filter check (pred grp s)) y)) in
982 (* would a hash table be more efficient? *)
983 let all = List.sort state_compare all in
984 let rec up_nodes child s = function
987 (match compare s1 child with
988 -1 -> up_nodes child s xs
989 | 0 -> (s,th,wit)::(up_nodes child s xs)
991 let neighbor_triples =
994 function (s,children) ->
998 match up_nodes child s all with [] -> raise Empty | l -> l)
1002 match neighbor_triples with
1006 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1008 let pre_forall_AW dir (grp,_,states) y all reqst =
1011 None -> true | Some reqst -> List.mem s reqst in
1014 A.FORWARD -> G.predecessors | A.BACKWARD -> G.successors in
1017 A.FORWARD -> G.successors | A.BACKWARD -> G.predecessors in
1020 (function p -> (p,succ grp p))
1023 (function (s,_,_) -> List.filter check (pred grp s)) y)) in
1024 (* would a hash table be more efficient? *)
1025 let all = List.sort state_compare all in
1026 let rec up_nodes child s = function
1028 | (s1,th,wit)::xs ->
1029 (match compare s1 child with
1030 -1 -> up_nodes child s xs
1031 | 0 -> (s,th,wit)::(up_nodes child s xs)
1033 let neighbor_triples =
1036 function (s,children) ->
1039 match up_nodes child s all with [] -> raise AW | l -> l)
1042 match neighbor_triples with
1044 | _ -> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1046 (* drop_negwits will call setify *)
1047 let satEX dir m s reqst = pre_exist dir m s reqst;;
1049 let satAX dir m s reqst = pre_forall dir m s s reqst
1052 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1053 let satEU dir ((_,_,states) as m) s1 s2 reqst =
1058 (*let ctr = ref 0 in*)
1061 let rec f y new_info =
1067 let first = triples_conj s1 (pre_exist dir m new_info reqst) in
1068 let res = triples_union first y in
1069 let new_info = setdiff res y in
1070 (*Printf.printf "iter %d res %d new_info %d\n"
1071 !ctr (List.length res) (List.length new_info);
1078 let pre = pre_exist dir m y reqst in
1079 triples_union s2 (triples_conj s1 pre) in
1083 (* EF phi == E[true U phi] *)
1084 let satEF dir m s2 reqst =
1086 (*let ctr = ref 0 in*)
1089 let rec f y new_info =
1095 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1096 let first = pre_exist dir m new_info reqst in
1097 let res = triples_union first y in
1098 let new_info = setdiff res y in
1099 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1100 (if dir = A.BACKWARD then "reachable" else "real ef")
1101 !ctr (List.length res) (List.length new_info);
1102 print_state "new info" new_info;
1109 let pre = pre_exist dir m y reqst in
1110 triples_union s2 pre in
1114 type ('pred,'anno) auok =
1115 AUok of ('pred,'anno) triples | AUfailed of ('pred,'anno) triples
1117 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1118 let satAU dir ((cfg,_,states) as m) s1 s2 reqst =
1123 (*let ctr = ref 0 in*)
1125 if !Flag_ctl.loop_in_src_code
1130 let rec f y newinfo =
1136 print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1139 try Some (pre_forall dir m new_info y reqst)
1144 match triples_conj s1 pre with
1147 (*print_state "s1" s1;
1148 print_state "pre" pre;
1149 print_state "first" first;*)
1150 let res = triples_union first y in
1152 if not !something_dropped
1154 else setdiff res y in
1156 "iter %d res %d new_info %d\n"
1157 !ctr (List.length res) (List.length new_info);
1162 if !Flag_ctl.loop_in_src_code
1166 fix (function s1 -> function s2 ->
1167 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1168 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1169 subseteq s1 s2) in for popl *)
1172 let pre = pre_forall dir m y y reqst in
1173 triples_union s2 (triples_conj s1 pre) in
1178 (* reqst could be the states of s1 *)
1180 let lstates = mkstates states reqst in
1181 let initial_removed =
1182 triples_complement lstates (triples_union s1 s2) in
1183 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1184 let rec loop base removed =
1186 triples_conj base (pre_exist dir m removed reqst) in
1188 triples_conj base (triples_complement lstates new_removed) in
1189 if supseteq new_base base
1190 then triples_union base s2
1191 else loop new_base new_removed in
1192 loop initial_base initial_removed *)
1194 let satAW dir ((grp,_,states) as m) s1 s2 reqst =
1200 This works extremely badly when the region is small and the end of the
1201 region is very ambiguous, eg free(x) ... x
1205 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1206 let ostates = Common.union_set (get_states s1) (get_states s2) in
1209 A.FORWARD -> G.successors grp
1210 | A.BACKWARD -> G.predecessors grp) in
1212 List.fold_left Common.union_set ostates (List.map succ ostates) in
1213 let negphi = triples_complement states s1 in
1214 let negpsi = triples_complement states s2 in
1215 triples_complement ostates
1216 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1219 (*let ctr = ref 0 in*)
1223 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1226 let pre = pre_forall dir m y y reqst in
1227 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1228 triples_union s2 conj in
1229 setgfix f (triples_union s1 s2)
1232 let satAF dir m s reqst =
1236 let rec f y newinfo =
1241 let first = pre_forall dir m new_info y reqst in
1242 let res = triples_union first y in
1243 let new_info = setdiff res y in
1249 let pre = pre_forall dir m y y reqst in
1250 triples_union s pre in
1253 let satAG dir ((_,_,states) as m) s reqst =
1257 let pre = pre_forall dir m y y reqst in
1258 triples_conj y pre in
1261 let satEG dir ((_,_,states) as m) s reqst =
1265 let pre = pre_exist dir m y reqst in
1266 triples_conj y pre in
1269 (* **************************************************************** *)
1270 (* Inner And - a way of dealing with multiple matches within a node *)
1271 (* **************************************************************** *)
1272 (* applied to the result of matching a node. collect witnesses when the
1273 states and environments are the same *)
1275 let inner_and trips =
1276 let rec loop = function
1278 | (s,th,w)::trips ->
1279 let (cur,acc) = loop trips in
1281 (s',_,_)::_ when s = s' ->
1282 let rec loop' = function
1284 | ((_,th',w') as t')::ts' ->
1285 (match conj_subst th th' with
1286 Some th'' -> (s,th'',union_wit w w')::ts'
1287 | None -> t'::(loop' ts')) in
1289 | _ -> ([(s,th,w)],cur@acc)) in
1291 loop (List.sort state_compare trips) (* is this sort needed? *) in
1294 (* *************** *)
1295 (* Partial matches *)
1296 (* *************** *)
1298 let filter_conj states unwanted partial_matches =
1300 triples_conj (triples_complement states (unwitify unwanted))
1302 triples_conj (unwitify x) (triples_complement states x)
1304 let strict_triples_conj strict states trips trips' =
1305 let res = triples_conj trips trips' in
1306 if !Flag_ctl.partial_match && strict = A.STRICT
1308 let fail_left = filter_conj states trips trips' in
1309 let fail_right = filter_conj states trips' trips in
1310 let ors = triples_union fail_left fail_right in
1311 triples_union res ors
1314 let strict_triples_conj_none strict states trips trips' =
1315 let res = triples_conj_none trips trips' in
1316 if !Flag_ctl.partial_match && strict = A.STRICT
1318 let fail_left = filter_conj states trips trips' in
1319 let fail_right = filter_conj states trips' trips in
1320 let ors = triples_union fail_left fail_right in
1321 triples_union res ors
1324 let left_strict_triples_conj strict states trips trips' =
1325 let res = triples_conj trips trips' in
1326 if !Flag_ctl.partial_match && strict = A.STRICT
1328 let fail_left = filter_conj states trips trips' in
1329 triples_union res fail_left
1332 let strict_A1 strict op failop dir ((_,_,states) as m) trips required_states =
1333 let res = op dir m trips required_states in
1334 if !Flag_ctl.partial_match && strict = A.STRICT
1336 let states = mkstates states required_states in
1337 let fail = filter_conj states res (failop dir m trips required_states) in
1338 triples_union res fail
1341 let strict_A2 strict op failop dir ((_,_,states) as m) trips trips'
1343 let res = op dir m trips trips' required_states in
1344 if !Flag_ctl.partial_match && strict = A.STRICT
1346 let states = mkstates states required_states in
1347 let fail = filter_conj states res (failop dir m trips' required_states) in
1348 triples_union res fail
1351 let strict_A2au strict op failop dir ((_,_,states) as m) trips trips'
1353 match op dir m trips trips' required_states with
1355 if !Flag_ctl.partial_match && strict = A.STRICT
1357 let states = mkstates states required_states in
1359 filter_conj states res (failop dir m trips' required_states) in
1360 AUok (triples_union res fail)
1362 | AUfailed res -> AUfailed res
1364 (* ********************* *)
1365 (* Environment functions *)
1366 (* ********************* *)
1368 let drop_wits required_states s phi =
1369 match required_states with
1371 | Some states -> List.filter (function (s,_,_) -> List.mem s states) s
1374 let print_required required =
1377 Format.print_string "{";
1380 print_generic_substitution reqd; Format.print_newline())
1382 Format.print_string "}";
1383 Format.print_newline())
1388 let extend_required trips required =
1389 if !Flag_ctl.partial_match
1392 if !pREQUIRED_ENV_OPT
1398 function (_,t,_) -> if List.mem t rest then rest else t::rest)
1400 let envs = if List.mem [] envs then [] else envs in
1401 match (envs,required) with
1405 let hdln = List.length hd + 5 (* let it grow a little bit *) in
1410 else if ln + 1 > hdln then raise Too_long else (ln+1,x::y) in
1417 match conj_subst t r with
1418 None -> rest | Some th -> add th rest)
1422 with Too_long -> envs :: required)
1423 | (envs,_) -> envs :: required
1426 let drop_required v required =
1427 if !pREQUIRED_ENV_OPT
1434 (List.map (List.filter (function sub -> not(dom_sub sub = v))) l))
1436 (* check whether an entry has become useless *)
1437 List.filter (function l -> not (List.exists (function x -> x = []) l)) res
1440 (* no idea how to write this function ... *)
1442 (Hashtbl.create(50) : (P.t, (G.node * substitution) list) Hashtbl.t)
1444 let satLabel label required p =
1446 if !pSATLABEL_MEMO_OPT
1449 let states_subs = Hashtbl.find memo_label p in
1450 List.map (function (st,th) -> (st,th,[])) states_subs
1453 let triples = setify(label p) in
1454 Hashtbl.add memo_label p
1455 (List.map (function (st,th,_) -> (st,th)) triples);
1457 else setify(label p) in
1459 (if !pREQUIRED_ENV_OPT
1463 function ((s,th,_) as t) ->
1465 (List.exists (function th' -> not(conj_subst th th' = None)))
1472 let get_required_states l =
1473 if !pREQUIRED_STATES_OPT && not !Flag_ctl.partial_match
1475 Some(inner_setify (List.map (function (s,_,_) -> s) l))
1478 let get_children_required_states dir (grp,_,_) required_states =
1479 if !pREQUIRED_STATES_OPT && not !Flag_ctl.partial_match
1481 match required_states with
1486 A.FORWARD -> G.successors
1487 | A.BACKWARD -> G.predecessors in
1488 Some (inner_setify (List.concat (List.map (fn grp) states)))
1491 let reachable_table =
1492 (Hashtbl.create(50) : (G.node * A.direction, G.node list) Hashtbl.t)
1494 (* like satEF, but specialized for get_reachable *)
1495 let reachsatEF dir (grp,_,_) s2 =
1497 match dir with A.FORWARD -> G.successors | A.BACKWARD -> G.predecessors in
1498 let union = unionBy compare (=) in
1499 let rec f y = function
1502 let (pre_collected,new_info) =
1503 List.partition (function Common.Left x -> true | _ -> false)
1506 try Common.Left (Hashtbl.find reachable_table (x,dir))
1507 with Not_found -> Common.Right x)
1512 function Common.Left x -> union x rest
1513 | _ -> failwith "not possible")
1517 (function Common.Right x -> x | _ -> failwith "not possible")
1519 let first = inner_setify (concatmap (dirop grp) new_info) in
1520 let new_info = setdiff first y in
1521 let res = new_info @ y in
1523 List.rev(f s2 s2) (* put root first *)
1525 let get_reachable dir m required_states =
1526 match required_states with
1533 if List.mem cur rest
1537 (try Hashtbl.find reachable_table (cur,dir)
1540 let states = reachsatEF dir m [cur] in
1541 Hashtbl.add reachable_table (cur,dir) states;
1550 Printf.sprintf "_c%d" c
1552 (* **************************** *)
1553 (* End of environment functions *)
1554 (* **************************** *)
1556 type ('code,'value) cell = Frozen of 'code | Thawed of 'value
1558 let rec satloop unchecked required required_states
1559 ((grp,label,states) as m) phi env =
1560 let rec loop unchecked required required_states phi =
1561 (*Common.profile_code "satloop" (fun _ -> *)
1565 | A.True -> triples_top states
1566 | A.Pred(p) -> satLabel label required p
1567 | A.Uncheck(phi1) ->
1568 let unchecked = if !pUNCHECK_OPT then true else false in
1569 loop unchecked required required_states phi1
1571 let phires = loop unchecked required required_states phi in
1573 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1574 triples_complement (mkstates states required_states)
1576 | A.Or(phi1,phi2) ->
1578 (loop unchecked required required_states phi1)
1579 (loop unchecked required required_states phi2)
1580 | A.SeqOr(phi1,phi2) ->
1581 let res1 = loop unchecked required required_states phi1 in
1582 let res2 = loop unchecked required required_states phi2 in
1583 let res1neg = unwitify res1 in
1586 (triples_complement (mkstates states required_states) res1neg)
1588 | A.And(strict,phi1,phi2) ->
1589 (* phi1 is considered to be more likely to be [], because of the
1590 definition of asttoctl. Could use heuristics such as the size of
1592 let pm = !Flag_ctl.partial_match in
1593 (match (pm,loop unchecked required required_states phi1) with
1594 (false,[]) when !pLazyOpt -> []
1596 let new_required = extend_required phi1res required in
1597 let new_required_states = get_required_states phi1res in
1598 (match (pm,loop unchecked new_required new_required_states phi2)
1600 (false,[]) when !pLazyOpt -> []
1602 strict_triples_conj strict
1603 (mkstates states required_states)
1605 | A.AndAny(dir,strict,phi1,phi2) ->
1606 (* phi2 can appear anywhere that is reachable *)
1607 let pm = !Flag_ctl.partial_match in
1608 (match (pm,loop unchecked required required_states phi1) with
1611 let new_required = extend_required phi1res required in
1612 let new_required_states = get_required_states phi1res in
1613 let new_required_states =
1614 get_reachable dir m new_required_states in
1615 (match (pm,loop unchecked new_required new_required_states phi2)
1617 (false,[]) -> phi1res
1620 [] -> (* !Flag_ctl.partial_match must be true *)
1624 let s = mkstates states required_states in
1626 (function a -> function b ->
1627 strict_triples_conj strict s a [b])
1628 [List.hd phi2res] (List.tl phi2res)
1631 List.map (function (s,e,w) -> [(state,e,w)]) phi2res in
1632 let s = mkstates states required_states in
1634 (function a -> function b ->
1635 strict_triples_conj strict s a b)
1639 "only one result allowed for the left arg of AndAny")))
1640 | A.HackForStmt(dir,strict,phi1,phi2) ->
1641 (* phi2 can appear anywhere that is reachable *)
1642 let pm = !Flag_ctl.partial_match in
1643 (match (pm,loop unchecked required required_states phi1) with
1646 let new_required = extend_required phi1res required in
1647 let new_required_states = get_required_states phi1res in
1648 let new_required_states =
1649 get_reachable dir m new_required_states in
1650 (match (pm,loop unchecked new_required new_required_states phi2)
1652 (false,[]) -> phi1res
1654 (* if there is more than one state, something about the
1655 environment has to ensure that the right triples of
1656 phi2 get associated with the triples of phi1.
1657 the asttoctl2 has to ensure that that is the case.
1658 these should thus be structural properties.
1659 env of phi2 has to be a proper subset of env of phi1
1660 to ensure all end up being consistent. no new triples
1661 should be generated. strict_triples_conj_none takes
1664 let s = mkstates states required_states in
1667 function (st,th,_) as phi2_elem ->
1669 triples_complement [st] [(st,th,[])] in
1670 strict_triples_conj_none strict s acc
1671 (phi2_elem::inverse))
1673 | A.InnerAnd(phi) ->
1674 inner_and(loop unchecked required required_states phi)
1676 let new_required_states =
1677 get_children_required_states dir m required_states in
1678 satEX dir m (loop unchecked required new_required_states phi)
1680 | A.AX(dir,strict,phi) ->
1681 let new_required_states =
1682 get_children_required_states dir m required_states in
1683 let res = loop unchecked required new_required_states phi in
1684 strict_A1 strict satAX satEX dir m res required_states
1686 let new_required_states = get_reachable dir m required_states in
1687 satEF dir m (loop unchecked required new_required_states phi)
1689 | A.AF(dir,strict,phi) ->
1690 if !Flag_ctl.loop_in_src_code
1692 loop unchecked required required_states
1693 (A.AU(dir,strict,A.True,phi))
1695 let new_required_states = get_reachable dir m required_states in
1696 let res = loop unchecked required new_required_states phi in
1697 strict_A1 strict satAF satEF dir m res new_required_states
1699 let new_required_states = get_reachable dir m required_states in
1700 satEG dir m (loop unchecked required new_required_states phi)
1702 | A.AG(dir,strict,phi) ->
1703 let new_required_states = get_reachable dir m required_states in
1704 let res = loop unchecked required new_required_states phi in
1705 strict_A1 strict satAG satEF dir m res new_required_states
1706 | A.EU(dir,phi1,phi2) ->
1707 let new_required_states = get_reachable dir m required_states in
1708 (match loop unchecked required new_required_states phi2 with
1709 [] when !pLazyOpt -> []
1711 let new_required = extend_required s2 required in
1712 let s1 = loop unchecked new_required new_required_states phi1 in
1713 satEU dir m s1 s2 new_required_states)
1714 | A.AW(dir,strict,phi1,phi2) ->
1715 let new_required_states = get_reachable dir m required_states in
1716 (match loop unchecked required new_required_states phi2 with
1717 [] when !pLazyOpt -> []
1719 let new_required = extend_required s2 required in
1720 let s1 = loop unchecked new_required new_required_states phi1 in
1721 strict_A2 strict satAW satEF dir m s1 s2 new_required_states)
1722 | A.AU(dir,strict,phi1,phi2) ->
1723 (*Printf.printf "using AU\n"; flush stdout;*)
1724 let new_required_states = get_reachable dir m required_states in
1725 (match loop unchecked required new_required_states phi2 with
1726 [] when !pLazyOpt -> []
1728 let new_required = extend_required s2 required in
1729 let s1 = loop unchecked new_required new_required_states phi1 in
1731 strict_A2au strict satAU satEF dir m s1 s2 new_required_states in
1734 | AUfailed tmp_res ->
1735 (* found a loop, have to try AW *)
1737 A[E[phi1 U phi2] & phi1 W phi2]
1738 the and is nonstrict *)
1739 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1740 (*Printf.printf "using AW\n"; flush stdout;*)
1742 triples_conj (satEU dir m s1 tmp_res new_required_states)
1744 strict_A2 strict satAW satEF dir m s1 s2 new_required_states)
1745 | A.Implies(phi1,phi2) ->
1746 loop unchecked required required_states (A.Or(A.Not phi1,phi2))
1747 | A.Exists (keep,v,phi) ->
1748 let new_required = drop_required v required in
1749 triples_witness v unchecked (not keep)
1750 (loop unchecked new_required required_states phi)
1751 | A.Let(v,phi1,phi2) ->
1752 (* should only be used when the properties unchecked, required,
1753 and required_states are known to be the same or at least
1754 compatible between all the uses. this is not checked. *)
1755 let res = loop unchecked required required_states phi1 in
1756 satloop unchecked required required_states m phi2 ((v,res) :: env)
1757 | A.LetR(dir,v,phi1,phi2) ->
1758 (* should only be used when the properties unchecked, required,
1759 and required_states are known to be the same or at least
1760 compatible between all the uses. this is not checked. *)
1761 let new_required_states = get_reachable dir m required_states in
1762 let res = loop unchecked required new_required_states phi1 in
1763 satloop unchecked required required_states m phi2 ((v,res) :: env)
1765 let res = List.assoc v env in
1767 then List.map (function (s,th,_) -> (s,th,[])) res
1769 | A.XX(phi) -> failwith "should have been removed" in
1770 if !Flag_ctl.bench > 0 then triples := !triples + (List.length res);
1771 drop_wits required_states res phi (* ) *) in
1773 loop unchecked required required_states phi
1777 (* SAT with tracking *)
1778 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1779 ((_,label,states) as m) phi env =
1780 let anno res children = (annot lvl phi res children,res) in
1781 let satv unchecked required required_states phi0 env =
1782 sat_verbose_loop unchecked required required_states annot maxlvl (lvl+1)
1784 if (lvl > maxlvl) && (maxlvl > -1) then
1785 anno (satloop unchecked required required_states m phi env) []
1789 A.False -> anno [] []
1790 | A.True -> anno (triples_top states) []
1792 Printf.printf "label\n"; flush stdout;
1793 anno (satLabel label required p) []
1794 | A.Uncheck(phi1) ->
1795 let unchecked = if !pUNCHECK_OPT then true else false in
1796 let (child1,res1) = satv unchecked required required_states phi1 env in
1797 Printf.printf "uncheck\n"; flush stdout;
1801 satv unchecked required required_states phi1 env in
1802 Printf.printf "not\n"; flush stdout;
1803 anno (triples_complement (mkstates states required_states) res) [child]
1804 | A.Or(phi1,phi2) ->
1806 satv unchecked required required_states phi1 env in
1808 satv unchecked required required_states phi2 env in
1809 Printf.printf "or\n"; flush stdout;
1810 anno (triples_union res1 res2) [child1; child2]
1811 | A.SeqOr(phi1,phi2) ->
1813 satv unchecked required required_states phi1 env in
1815 satv unchecked required required_states phi2 env in
1817 List.map (function (s,th,_) -> (s,th,[])) res1 in
1818 Printf.printf "seqor\n"; flush stdout;
1819 anno (triples_union res1
1821 (triples_complement (mkstates states required_states)
1825 | A.And(strict,phi1,phi2) ->
1826 let pm = !Flag_ctl.partial_match in
1827 (match (pm,satv unchecked required required_states phi1 env) with
1828 (false,(child1,[])) ->
1829 Printf.printf "and\n"; flush stdout; anno [] [child1]
1830 | (_,(child1,res1)) ->
1831 let new_required = extend_required res1 required in
1832 let new_required_states = get_required_states res1 in
1833 (match (pm,satv unchecked new_required new_required_states phi2
1835 (false,(child2,[])) ->
1836 Printf.printf "and\n"; flush stdout; anno [] [child1;child2]
1837 | (_,(child2,res2)) ->
1838 Printf.printf "and\n"; flush stdout;
1840 strict_triples_conj strict
1841 (mkstates states required_states)
1843 anno res [child1; child2]))
1844 | A.AndAny(dir,strict,phi1,phi2) ->
1845 let pm = !Flag_ctl.partial_match in
1846 (match (pm,satv unchecked required required_states phi1 env) with
1847 (false,(child1,[])) ->
1848 Printf.printf "and\n"; flush stdout; anno [] [child1]
1849 | (_,(child1,res1)) ->
1850 let new_required = extend_required res1 required in
1851 let new_required_states = get_required_states res1 in
1852 let new_required_states =
1853 get_reachable dir m new_required_states in
1854 (match (pm,satv unchecked new_required new_required_states phi2
1856 (false,(child2,[])) ->
1857 Printf.printf "andany\n"; flush stdout;
1858 anno res1 [child1;child2]
1859 | (_,(child2,res2)) ->
1861 [] -> (* !Flag_ctl.partial_match must be true *)
1863 then anno [] [child1; child2]
1866 let s = mkstates states required_states in
1868 (function a -> function b ->
1869 strict_triples_conj strict s a [b])
1870 [List.hd res2] (List.tl res2) in
1871 anno res [child1; child2]
1874 List.map (function (s,e,w) -> [(state,e,w)]) res2 in
1875 Printf.printf "andany\n"; flush stdout;
1877 let s = mkstates states required_states in
1879 (function a -> function b ->
1880 strict_triples_conj strict s a b)
1882 anno res [child1; child2]
1885 "only one result allowed for the left arg of AndAny")))
1886 | A.HackForStmt(dir,strict,phi1,phi2) ->
1887 let pm = !Flag_ctl.partial_match in
1888 (match (pm,satv unchecked required required_states phi1 env) with
1889 (false,(child1,[])) ->
1890 Printf.printf "and\n"; flush stdout; anno [] [child1]
1891 | (_,(child1,res1)) ->
1892 let new_required = extend_required res1 required in
1893 let new_required_states = get_required_states res1 in
1894 let new_required_states =
1895 get_reachable dir m new_required_states in
1896 (match (pm,satv unchecked new_required new_required_states phi2
1898 (false,(child2,[])) ->
1899 Printf.printf "andany\n"; flush stdout;
1900 anno res1 [child1;child2]
1901 | (_,(child2,res2)) ->
1903 let s = mkstates states required_states in
1906 function (st,th,_) as phi2_elem ->
1908 triples_complement [st] [(st,th,[])] in
1909 strict_triples_conj_none strict s acc
1910 (phi2_elem::inverse))
1912 anno res [child1; child2]))
1913 | A.InnerAnd(phi1) ->
1914 let (child1,res1) = satv unchecked required required_states phi1 env in
1915 Printf.printf "uncheck\n"; flush stdout;
1916 anno (inner_and res1) [child1]
1918 let new_required_states =
1919 get_children_required_states dir m required_states in
1921 satv unchecked required new_required_states phi1 env in
1922 Printf.printf "EX\n"; flush stdout;
1923 anno (satEX dir m res required_states) [child]
1924 | A.AX(dir,strict,phi1) ->
1925 let new_required_states =
1926 get_children_required_states dir m required_states in
1928 satv unchecked required new_required_states phi1 env in
1929 Printf.printf "AX\n"; flush stdout;
1930 let res = strict_A1 strict satAX satEX dir m res required_states in
1933 let new_required_states = get_reachable dir m required_states in
1935 satv unchecked required new_required_states phi1 env in
1936 Printf.printf "EF\n"; flush stdout;
1937 anno (satEF dir m res new_required_states) [child]
1938 | A.AF(dir,strict,phi1) ->
1939 if !Flag_ctl.loop_in_src_code
1941 satv unchecked required required_states
1942 (A.AU(dir,strict,A.True,phi1))
1945 (let new_required_states = get_reachable dir m required_states in
1947 satv unchecked required new_required_states phi1 env in
1948 Printf.printf "AF\n"; flush stdout;
1950 strict_A1 strict satAF satEF dir m res new_required_states in
1953 let new_required_states = get_reachable dir m required_states in
1955 satv unchecked required new_required_states phi1 env in
1956 Printf.printf "EG\n"; flush stdout;
1957 anno (satEG dir m res new_required_states) [child]
1958 | A.AG(dir,strict,phi1) ->
1959 let new_required_states = get_reachable dir m required_states in
1961 satv unchecked required new_required_states phi1 env in
1962 Printf.printf "AG\n"; flush stdout;
1963 let res = strict_A1 strict satAG satEF dir m res new_required_states in
1966 | A.EU(dir,phi1,phi2) ->
1967 let new_required_states = get_reachable dir m required_states in
1968 (match satv unchecked required new_required_states phi2 env with
1970 Printf.printf "EU\n"; flush stdout;
1973 let new_required = extend_required res2 required in
1975 satv unchecked new_required new_required_states phi1 env in
1976 Printf.printf "EU\n"; flush stdout;
1977 anno (satEU dir m res1 res2 new_required_states) [child1; child2])
1978 | A.AW(dir,strict,phi1,phi2) ->
1979 failwith "should not be used" (*
1980 let new_required_states = get_reachable dir m required_states in
1981 (match satv unchecked required new_required_states phi2 env with
1983 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
1985 let new_required = extend_required res2 required in
1987 satv unchecked new_required new_required_states phi1 env in
1988 Printf.printf "AW %b\n" unchecked; flush stdout;
1990 strict_A2 strict satAW satEF dir m res1 res2
1991 new_required_states in
1992 anno res [child1; child2]) *)
1993 | A.AU(dir,strict,phi1,phi2) ->
1994 let new_required_states = get_reachable dir m required_states in
1995 (match satv unchecked required new_required_states phi2 env with
1997 Printf.printf "AU\n"; flush stdout; anno [] [child2]
1999 let new_required = extend_required s2 required in
2001 satv unchecked new_required new_required_states phi1 env in
2002 Printf.printf "AU\n"; flush stdout;
2004 strict_A2au strict satAU satEF dir m s1 s2 new_required_states in
2007 anno res [child1; child2]
2008 | AUfailed tmp_res ->
2009 (* found a loop, have to try AW *)
2011 A[E[phi1 U phi2] & phi1 W phi2]
2012 the and is nonstrict *)
2013 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2014 Printf.printf "AW\n"; flush stdout;
2016 triples_conj (satEU dir m s1 tmp_res new_required_states) s1 in
2018 strict_A2 strict satAW satEF dir m s1 s2 new_required_states in
2019 anno res [child1; child2]))
2020 | A.Implies(phi1,phi2) ->
2021 satv unchecked required required_states
2022 (A.Or(A.Not phi1,phi2))
2024 | A.Exists (keep,v,phi1) ->
2025 let new_required = drop_required v required in
2027 satv unchecked new_required required_states phi1 env in
2028 Printf.printf "exists\n"; flush stdout;
2029 anno (triples_witness v unchecked (not keep) res) [child]
2030 | A.Let(v,phi1,phi2) ->
2032 satv unchecked required required_states phi1 env in
2034 satv unchecked required required_states phi2 ((v,res1) :: env) in
2035 anno res2 [child1;child2]
2036 | A.LetR(dir,v,phi1,phi2) ->
2037 let new_required_states = get_reachable dir m required_states in
2039 satv unchecked required new_required_states phi1 env in
2041 satv unchecked required required_states phi2 ((v,res1) :: env) in
2042 anno res2 [child1;child2]
2044 Printf.printf "Ref\n"; flush stdout;
2045 let res = List.assoc v env in
2048 then List.map (function (s,th,_) -> (s,th,[])) res
2051 | A.XX(phi) -> failwith "should have been removed" in
2052 let res1 = drop_wits required_states res phi in
2056 print_required_states required_states;
2057 print_state "after drop_wits" res1 end;
2062 let sat_verbose annotate maxlvl lvl m phi =
2063 sat_verbose_loop false [] None annotate maxlvl lvl m phi []
2065 (* Type for annotations collected in a tree *)
2066 type ('a) witAnnoTree = WitAnno of ('a * ('a witAnnoTree) list);;
2068 let sat_annotree annotate m phi =
2069 let tree_anno l phi res chld = WitAnno(annotate l phi res,chld) in
2070 sat_verbose_loop false [] None tree_anno (-1) 0 m phi []
2074 let sat m phi = satloop m phi []
2078 let simpleanno l phi res =
2080 Format.print_string ("\n" ^ s ^ "\n------------------------------\n");
2081 print_generic_algo (List.sort compare res);
2082 Format.print_string "\n------------------------------\n\n" in
2083 let pp_dir = function
2085 | A.BACKWARD -> pp "^" in
2087 | A.False -> pp "False"
2088 | A.True -> pp "True"
2089 | A.Pred(p) -> pp ("Pred" ^ (Common.dump p))
2090 | A.Not(phi) -> pp "Not"
2091 | A.Exists(_,v,phi) -> pp ("Exists " ^ (Common.dump(v)))
2092 | A.And(_,phi1,phi2) -> pp "And"
2093 | A.AndAny(dir,_,phi1,phi2) -> pp "AndAny"
2094 | A.HackForStmt(dir,_,phi1,phi2) -> pp "HackForStmt"
2095 | A.Or(phi1,phi2) -> pp "Or"
2096 | A.SeqOr(phi1,phi2) -> pp "SeqOr"
2097 | A.Implies(phi1,phi2) -> pp "Implies"
2098 | A.AF(dir,_,phi1) -> pp "AF"; pp_dir dir
2099 | A.AX(dir,_,phi1) -> pp "AX"; pp_dir dir
2100 | A.AG(dir,_,phi1) -> pp "AG"; pp_dir dir
2101 | A.AW(dir,_,phi1,phi2)-> pp "AW"; pp_dir dir
2102 | A.AU(dir,_,phi1,phi2)-> pp "AU"; pp_dir dir
2103 | A.EF(dir,phi1) -> pp "EF"; pp_dir dir
2104 | A.EX(dir,phi1) -> pp "EX"; pp_dir dir
2105 | A.EG(dir,phi1) -> pp "EG"; pp_dir dir
2106 | A.EU(dir,phi1,phi2) -> pp "EU"; pp_dir dir
2107 | A.Let (x,phi1,phi2) -> pp ("Let"^" "^x)
2108 | A.LetR (dir,x,phi1,phi2) -> pp ("LetR"^" "^x); pp_dir dir
2109 | A.Ref(s) -> pp ("Ref("^s^")")
2110 | A.Uncheck(s) -> pp "Uncheck"
2111 | A.InnerAnd(s) -> pp "InnerAnd"
2112 | A.XX(phi1) -> pp "XX"
2116 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2117 print a ctl formula more accurately if you want.
2118 Use the print_xxx provided in the different module to call
2119 Pretty_print_ctl.pp_ctl.
2122 let simpleanno2 l phi res =
2124 Pretty_print_ctl.pp_ctl (P.print_predicate, SUB.print_mvar) false phi;
2125 Format.print_newline ();
2126 Format.print_string "----------------------------------------------------";
2127 Format.print_newline ();
2128 print_generic_algo (List.sort compare res);
2129 Format.print_newline ();
2130 Format.print_string "----------------------------------------------------";
2131 Format.print_newline ();
2132 Format.print_newline ();
2136 (* ---------------------------------------------------------------------- *)
2138 (* ---------------------------------------------------------------------- *)
2140 type optentry = bool ref * string
2141 type options = {label : optentry; unch : optentry;
2142 conj : optentry; compl1 : optentry; compl2 : optentry;
2144 reqenv : optentry; reqstates : optentry}
2147 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2148 unch = (pUNCHECK_OPT,"uncheck_opt");
2149 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2150 compl1 = (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2151 compl2 = (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2152 newinfo = (pNEW_INFO_OPT,"new_info_opt");
2153 reqenv = (pREQUIRED_ENV_OPT,"required_env_opt");
2154 reqstates = (pREQUIRED_STATES_OPT,"required_states_opt")}
2158 ("label ",[options.label]);
2159 ("unch ",[options.unch]);
2160 ("unch and label ",[options.label;options.unch])]
2163 [("conj ", [options.conj]);
2164 ("compl1 ", [options.compl1]);
2165 ("compl12 ", [options.compl1;options.compl2]);
2166 ("conj/compl12 ", [options.conj;options.compl1;options.compl2]);
2167 ("conj unch satl ", [options.conj;options.unch;options.label]);
2169 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2170 ("compl12 unch satl ",
2171 [options.compl1;options.compl2;options.unch;options.label]); *)
2172 ("conj/compl12 unch satl ",
2173 [options.conj;options.compl1;options.compl2;options.unch;options.label])]
2176 [("newinfo ", [options.newinfo]);
2177 ("newinfo unch satl ", [options.newinfo;options.unch;options.label])]
2180 [("reqenv ", [options.reqenv]);
2181 ("reqstates ", [options.reqstates]);
2182 ("reqenv/states ", [options.reqenv;options.reqstates]);
2183 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2184 ("reqstates unch satl ",
2185 [options.reqstates;options.unch;options.label]);*)
2186 ("reqenv/states unch satl ",
2187 [options.reqenv;options.reqstates;options.unch;options.label])]
2190 [options.label;options.unch;options.conj;options.compl1;options.compl2;
2191 options.newinfo;options.reqenv;options.reqstates]
2194 [("all ",all_options)]
2196 let all_options_but_path =
2197 [options.label;options.unch;options.conj;options.compl1;options.compl2;
2198 options.reqenv;options.reqstates]
2200 let all_but_path = ("all but path ",all_options_but_path)
2203 [(satAW_calls, "satAW", ref 0);
2204 (satAU_calls, "satAU", ref 0);
2205 (satEF_calls, "satEF", ref 0);
2206 (satAF_calls, "satAF", ref 0);
2207 (satEG_calls, "satEG", ref 0);
2208 (satAG_calls, "satAG", ref 0);
2209 (satEU_calls, "satEU", ref 0)]
2213 (function (opt,x) ->
2214 (opt,x,ref 0.0,ref 0,
2215 List.map (function _ -> (ref 0, ref 0, ref 0)) counters))
2216 [List.hd all;all_but_path]
2217 (*(all@baseline@conjneg@path@required)*)
2221 let rec iter fn = function
2223 | n -> let _ = fn() in
2224 (Hashtbl.clear reachable_table;
2225 Hashtbl.clear memo_label;
2229 let copy_to_stderr fl =
2230 let i = open_in fl in
2232 Printf.fprintf stderr "%s\n" (input_line i);
2234 try loop() with _ -> ();
2237 let bench_sat (_,_,states) fn =
2238 List.iter (function (opt,_) -> opt := false) all_options;
2241 (function (name,options,time,trips,counter_info) ->
2242 let iterct = !Flag_ctl.bench in
2243 if !time > float_of_int timeout then time := -100.0;
2244 if not (!time = -100.0)
2247 Hashtbl.clear reachable_table;
2248 Hashtbl.clear memo_label;
2249 List.iter (function (opt,_) -> opt := true) options;
2250 List.iter (function (calls,_,save_calls) -> save_calls := !calls)
2254 let bef = Sys.time() in
2256 Common.timeout_function timeout
2258 let bef = Sys.time() in
2259 let res = iter fn iterct in
2260 let aft = Sys.time() in
2261 time := !time +. (aft -. bef);
2262 trips := !trips + !triples;
2264 (function (calls,_,save_calls) ->
2265 function (current_calls,current_cfg,current_max_cfg) ->
2267 !current_calls + (!calls - !save_calls);
2268 if (!calls - !save_calls) > 0
2270 (let st = List.length states in
2271 current_cfg := !current_cfg + st;
2272 if st > !current_max_cfg
2273 then current_max_cfg := st))
2274 counters counter_info;
2279 let aft = Sys.time() in
2281 Printf.fprintf stderr "Timeout at %f on: %s\n"
2285 List.iter (function (opt,_) -> opt := false) options;
2290 Printf.fprintf stderr "\n";
2294 (if not(List.for_all (function x -> x = res) rest)
2296 (List.iter (print_state "a state") answers;
2297 Printf.printf "something doesn't work\n");
2301 let iterct = !Flag_ctl.bench in
2305 (function (name,options,time,trips,counter_info) ->
2306 Printf.fprintf stderr "%s Numbers: %f %d "
2307 name (!time /. (float_of_int iterct)) !trips;
2309 (function (calls,cfg,max_cfg) ->
2310 Printf.fprintf stderr "%d %d %d " (!calls / iterct) !cfg !max_cfg)
2312 Printf.fprintf stderr "\n")
2315 (* ---------------------------------------------------------------------- *)
2316 (* preprocessing: ignore irrelevant functions *)
2318 let preprocess (cfg,_,_) label = function
2319 [] -> true (* no information, try everything *)
2321 let sz = G.size cfg in
2322 let verbose_output pred = function
2324 Printf.printf "did not find:\n";
2325 P.print_predicate pred; Format.print_newline()
2327 Printf.printf "found:\n";
2328 P.print_predicate pred; Format.print_newline();
2329 Printf.printf "but it was not enough\n" in
2330 let get_any verbose x =
2332 try Hashtbl.find memo_label x
2335 (let triples = label x in
2337 List.map (function (st,th,_) -> (st,th)) triples in
2338 Hashtbl.add memo_label x filtered;
2340 if verbose then verbose_output x res;
2343 (* don't bother testing when there are more patterns than nodes *)
2344 if List.length l > sz-2
2346 else List.for_all (get_any false) l in
2347 if List.exists get_all l
2350 (if !Flag_ctl.verbose_match
2352 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2356 let filter_partial_matches trips =
2357 if !Flag_ctl.partial_match
2359 let anynegwit = (* if any is neg, then all are *)
2360 List.exists (function A.NegWit _ -> true | A.Wit _ -> false) in
2362 List.partition (function (s,th,wit) -> anynegwit wit) trips in
2365 | _ -> print_state "partial matches" bad; Format.print_newline());
2369 (* ---------------------------------------------------------------------- *)
2370 (* Main entry point for engine *)
2371 let sat m phi reqopt =
2373 (match !Flag_ctl.steps with
2374 None -> step_count := 0
2375 | Some x -> step_count := x);
2376 Hashtbl.clear reachable_table;
2377 Hashtbl.clear memo_label;
2378 let (x,label,states) = m in
2379 if (!Flag_ctl.bench > 0) or (preprocess m label reqopt)
2381 ((* to drop when Yoann initialized this flag *)
2382 if List.exists (G.extract_is_loop x) states
2383 then Flag_ctl.loop_in_src_code := true;
2384 let m = (x,label,List.sort compare states) in
2386 if(!Flag_ctl.verbose_ctl_engine)
2388 let fn _ = snd (sat_annotree simpleanno2 m phi) in
2389 if !Flag_ctl.bench > 0
2393 let fn _ = satloop false [] None m phi [] in
2394 if !Flag_ctl.bench > 0
2396 else Common.profile_code "ctl" (fun _ -> fn()) in
2397 let res = filter_partial_matches res in
2399 Printf.printf "steps: start %d, stop %d\n"
2400 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2402 Printf.printf "triples: %d\n" !triples;
2403 print_state "final result" res;
2407 (if !Flag_ctl.verbose_ctl_engine
2408 then Common.pr2 "missing something required";
2413 (* ********************************************************************** *)
2414 (* End of Module: CTL_ENGINE *)
2415 (* ********************************************************************** *)