2 * Copyright 2010, INRIA, University of Copenhagen
3 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
4 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
5 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
6 * This file is part of Coccinelle.
8 * Coccinelle is free software: you can redistribute it and/or modify
9 * it under the terms of the GNU General Public License as published by
10 * the Free Software Foundation, according to version 2 of the License.
12 * Coccinelle is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
25 (*external c_counter : unit -> int = "c_counter"*)
27 (* Optimize triples_conj by first extracting the intersection of the two sets,
28 which can certainly be in the intersection *)
29 let pTRIPLES_CONJ_OPT = ref true
30 (* For complement, make NegState for the negation of a single state *)
31 let pTRIPLES_COMPLEMENT_OPT = ref true
32 (* For complement, do something special for the case where the environment
33 and witnesses are empty *)
34 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
35 (* "Double negate" the arguments of the path operators *)
36 let pDOUBLE_NEGATE_OPT = ref true
37 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
38 let pNEW_INFO_OPT = ref true
39 (* Filter the result of the label function to drop entries that aren't
40 compatible with any of the available environments *)
41 let pREQUIRED_ENV_OPT = ref true
42 (* Memoize the raw result of the label function *)
43 let pSATLABEL_MEMO_OPT = ref true
44 (* Filter results according to the required states *)
45 let pREQUIRED_STATES_OPT = ref true
46 (* Drop negative witnesses at Uncheck *)
47 let pUNCHECK_OPT = ref true
48 let pANY_NEG_OPT = ref true
49 let pLazyOpt = ref true
51 (* Nico: This stack is use for graphical traces *)
52 let graph_stack = ref ([] : string list
)
53 let graph_hash = (Hashtbl.create
101)
56 let pTRIPLES_CONJ_OPT = ref false
57 let pTRIPLES_COMPLEMENT_OPT = ref false
58 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
59 let pDOUBLE_NEGATE_OPT = ref false
60 let pNEW_INFO_OPT = ref false
61 let pREQUIRED_ENV_OPT = ref false
62 let pSATLABEL_MEMO_OPT = ref false
63 let pREQUIRED_STATES_OPT = ref false
64 let pUNCHECK_OPT = ref false
65 let pANY_NEG_OPT = ref false
66 let pLazyOpt = ref false
70 let step_count = ref 0
73 if not
(!step_count = 0)
76 step_count := !step_count - 1;
77 if !step_count = 0 then raise Steps
80 let inc cell
= cell
:= !cell
+ 1
82 let satEU_calls = ref 0
83 let satAW_calls = ref 0
84 let satAU_calls = ref 0
85 let satEF_calls = ref 0
86 let satAF_calls = ref 0
87 let satEG_calls = ref 0
88 let satAG_calls = ref 0
96 Printf.sprintf
"_fresh_r_%d" c
98 (* **********************************************************************
100 * Implementation of a Witness Tree model checking engine for CTL-FVex
103 * **********************************************************************)
105 (* ********************************************************************** *)
106 (* Module: SUBST (substitutions: meta. vars and values) *)
107 (* ********************************************************************** *)
113 val eq_mvar
: mvar
-> mvar
-> bool
114 val eq_val
: value -> value -> bool
115 val merge_val
: value -> value -> value
116 val print_mvar
: mvar
-> unit
117 val print_value
: value -> unit
121 (* ********************************************************************** *)
122 (* Module: GRAPH (control flow graphs / model) *)
123 (* ********************************************************************** *)
129 val predecessors
: cfg
-> node
-> node list
130 val successors
: cfg
-> node
-> node list
131 val extract_is_loop
: cfg
-> node
-> bool
132 val print_node
: node
-> unit
133 val size
: cfg
-> int
134 val print_graph
: cfg
-> string option ->
135 (node
* string) list
-> (node
* string) list
-> string -> unit
139 module OGRAPHEXT_GRAPH
=
142 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
143 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
144 let print_node i
= Format.print_string
(Common.i_to_s i
)
148 (* ********************************************************************** *)
149 (* Module: PREDICATE (predicates for CTL formulae) *)
150 (* ********************************************************************** *)
152 module type PREDICATE
=
155 val print_predicate
: t
-> unit
159 (* ********************************************************************** *)
161 (* ---------------------------------------------------------------------- *)
162 (* Misc. useful generic functions *)
163 (* ---------------------------------------------------------------------- *)
165 let get_graph_files () = !graph_stack
166 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
176 let foldl = List.fold_left
;;
178 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
180 type 'a esc
= ESC
of 'a
| CONT
of 'a
182 let foldr = List.fold_right
;;
184 let concat = List.concat;;
188 let filter = List.filter;;
190 let partition = List.partition;;
192 let concatmap f l
= List.concat (List.map f l
);;
200 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
202 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
204 let rec some_tolist opts
=
207 | (Some x
)::rest
-> x
::(some_tolist rest
)
208 | _
::rest
-> some_tolist rest
211 let rec groupBy eq l
=
215 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
216 (x
::xs1
)::(groupBy eq xs2
)
219 let group l
= groupBy (=) l
;;
221 let rec memBy eq x l
=
224 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
227 let rec nubBy eq ls
=
230 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
231 | (x
::xs
) -> x
::(nubBy eq xs
)
237 | (x
::xs
) when (List.mem x xs
) -> nub xs
238 | (x
::xs
) -> x
::(nub xs
)
241 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
243 let setifyBy eq xs
= nubBy eq xs
;;
245 let setify xs
= nub xs
;;
247 let inner_setify xs
= List.sort compare
(nub xs
);;
249 let unionBy compare eq xs
= function
252 let rec loop = function
254 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
255 List.sort compare
(loop xs
)
258 let union xs ys
= unionBy state_compare (=) xs ys
;;
260 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
262 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
264 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
265 let supseteq xs ys
= subseteq ys xs
267 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
269 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
271 (* Fix point calculation *)
273 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
276 (* Fix point calculation on set-valued functions *)
277 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
278 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
280 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
282 (* ********************************************************************** *)
283 (* Module: CTL_ENGINE *)
284 (* ********************************************************************** *)
287 functor (SUB
: SUBST
) ->
288 functor (G
: GRAPH
) ->
289 functor (P
: PREDICATE
) ->
294 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
296 type ('pred
,'anno
) witness
=
297 (G.node
, substitution
,
298 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
299 Ast_ctl.generic_witnesstree
301 type ('pred
,'anno
) triples =
302 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
304 (* ---------------------------------------------------------------------- *)
305 (* Pretty printing functions *)
306 (* ---------------------------------------------------------------------- *)
308 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
309 let print_generic_subst = function
311 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
312 | A.NegSubst
(mvar
, v
) ->
313 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
314 Format.print_string
"[";
315 Common.print_between
(fun () -> Format.print_string
";" )
316 print_generic_subst substxs
;
317 Format.print_string
"]"
319 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
321 | A.Wit
(state
, subst
, anno
, childrens
) ->
322 Format.print_string
"wit ";
324 print_generic_substitution subst
;
325 (match childrens
with
326 [] -> Format.print_string
"{}"
328 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
329 print_generic_witnesstree childrens
; Format.close_box
())
331 Format.print_string
"!";
332 print_generic_witness wit
334 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
337 Format.print_string
"{";
339 (fun () -> Format.print_string
";"; Format.force_newline
() )
340 print_generic_witness witnesstree
;
341 Format.print_string
"}";
344 and print_generic_triple
(node
,subst
,tree
) =
346 print_generic_substitution subst
;
347 print_generic_witnesstree tree
349 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
350 Format.print_string
"<";
352 (fun () -> Format.print_string
";"; Format.force_newline
())
353 print_generic_triple xs
;
354 Format.print_string
">"
357 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
358 Printf.printf
"%s\n" str
;
359 List.iter
(function x ->
360 print_generic_triple
x; Format.print_newline
(); flush stdout
)
361 (List.sort compare l
);
364 let print_required_states = function
365 None
-> Printf.printf
"no required states\n"
367 Printf.printf
"required states: ";
370 G.print_node x; Format.print_string
" "; Format.print_flush
())
374 let mkstates states
= function
376 | Some states
-> states
378 let print_graph grp required_states res str
= function
379 A.Exists
(keep
,v
,phi
) -> ()
381 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
384 | A.Exists
(keep
,v
,phi
) -> ()
387 Printf.sprintf
"%s%s"
389 (Common.format_to_string
391 Pretty_print_ctl.pp_ctl
392 (P.print_predicate
, SUB.print_mvar
)
395 let file = (match !Flag.currentfile
with
396 None
-> "graphical_trace"
399 (if not
(List.mem
file !graph_stack) then
400 graph_stack := file :: !graph_stack);
401 let filename = Filename.temp_file
(file^
":") ".dot" in
402 Hashtbl.add
graph_hash file filename;
404 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
405 (match required_states
with
407 | Some required_states
->
408 (List.map (function s
-> (s
,"blue")) required_states
))
409 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
411 let print_graph_c grp required_states res
ctr phi
=
412 let str = "iter: "^
(string_of_int
!ctr) in
413 print_graph grp required_states res
str phi
415 (* ---------------------------------------------------------------------- *)
417 (* ---------------------------------------------------------------------- *)
420 (* ************************* *)
422 (* ************************* *)
427 | A.NegSubst
(x,_
) -> x
433 | A.NegSubst
(_
,x) -> x
436 let eq_subBy eqx eqv sub sub'
=
437 match (sub
,sub'
) with
438 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
439 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
444 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
446 let eq_subst th th'
= setequalBy eq_sub th th'
;;
448 let merge_subBy eqx
(===) (>+<) sub sub'
=
449 (* variable part is guaranteed to be the same *)
450 match (sub
,sub'
) with
451 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
453 then Some
[A.Subst
(x, v
>+< v'
)]
455 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
457 then Some
[A.Subst
(x'
,v'
)]
459 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
461 then Some
[A.Subst
(x,v
)]
463 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
466 let merged = v
>+< v'
in
467 if merged = v
&& merged = v'
468 then Some
[A.NegSubst
(x,v
>+< v'
)]
470 (* positions are compatible, but not identical. keep apart. *)
471 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
472 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
476 (* How could we accomadate subterm constraints here??? *)
477 let merge_sub sub sub'
=
478 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
480 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
482 (* NOTE: we sort by using the generic "compare" on (meta-)variable
483 * names; we could also require a definition of compare for meta-variables
484 * or substitutions but that seems like overkill for sorting
486 let clean_subst theta
=
490 let res = compare
(dom_sub s
) (dom_sub s'
) in
494 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
495 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
496 | _
-> compare
(ran_sub s
) (ran_sub s'
)
499 let rec loop = function
501 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
502 loop (A.Subst
(x,v
)::rest
)
503 | x::xs
-> x::(loop xs
) in
506 let top_subst = [];; (* Always TRUE subst. *)
508 (* Split a theta in two parts: one with (only) "x" and one without *)
510 let split_subst theta
x =
511 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
513 exception SUBST_MISMATCH
514 let conj_subst theta theta'
=
515 match (theta
,theta'
) with
516 | ([],_
) -> Some theta'
517 | (_
,[]) -> Some theta
519 let rec classify = function
521 | [x] -> [(dom_sub x,[x])]
523 (match classify xs
with
524 ((nm
,y
)::ys
) as res ->
527 else (dom_sub x,[x])::res
528 | _
-> failwith
"not possible") in
529 let merge_all theta theta'
=
536 match (merge_sub sub sub'
) with
537 Some subs
-> subs
@ rest
538 | _
-> raise SUBST_MISMATCH
)
541 let rec loop = function
543 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
545 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
546 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
547 (match compare
x y
with
548 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
549 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
550 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
551 | _
-> failwith
"not possible") in
552 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
553 with SUBST_MISMATCH
-> None
556 (* theta' must be a subset of theta *)
557 let conj_subst_none theta theta'
=
558 match (theta
,theta'
) with
559 | (_
,[]) -> Some theta
562 let rec classify = function
564 | [x] -> [(dom_sub x,[x])]
566 (match classify xs
with
567 ((nm
,y
)::ys
) as res ->
570 else (dom_sub x,[x])::res
571 | _
-> failwith
"not possible") in
572 let merge_all theta theta'
=
579 match (merge_sub sub sub'
) with
580 Some subs
-> subs
@ rest
581 | _
-> raise SUBST_MISMATCH
)
584 let rec loop = function
586 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
587 | ([],ctheta'
) -> raise SUBST_MISMATCH
588 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
589 (match compare
x y
with
590 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
591 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
592 | 1 -> raise SUBST_MISMATCH
593 | _
-> failwith
"not possible") in
594 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
595 with SUBST_MISMATCH
-> None
600 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
601 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
604 (* Turn a (big) theta into a list of (small) thetas *)
605 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
608 (* ************************* *)
610 (* ************************* *)
612 (* Always TRUE witness *)
613 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
615 let eq_wit wit wit'
= wit
= wit'
;;
617 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
618 let res = unionBy compare
(=) wit wit'
in
619 let anynegwit = (* if any is neg, then all are *)
620 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
622 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
625 let negate_wit wit
= A.NegWit wit
(*
627 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
628 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
631 let negate_wits wits
=
632 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
635 let anynegwit = (* if any is neg, then all are *)
636 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
640 function (s
,th
,wit
) ->
641 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
644 (* ************************* *)
646 (* ************************* *)
648 (* Triples are equal when the constituents are equal *)
649 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
650 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
652 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
654 let normalize trips
=
656 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
660 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
661 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
662 let triples_conj trips trips'
=
663 let (trips
,shared
,trips'
) =
664 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
667 List.partition (function t
-> List.mem t trips'
) trips
in
669 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
670 (trips,shared
,trips'
)
671 else (trips,[],trips'
) in
672 foldl (* returns a set - setify inlined *)
674 function (s1
,th1
,wit1
) ->
677 function (s2
,th2
,wit2
) ->
679 (match (conj_subst th1 th2
) with
681 let t = (s1
,th
,union_wit wit1 wit2
) in
682 if List.mem
t rest
then rest
else t::rest
689 (* ignore the state in the right argument. always pretend it is the same as
691 (* env on right has to be a subset of env on left *)
692 let triples_conj_none trips trips'
=
693 let (trips,shared
,trips'
) =
694 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
697 List.partition (function t -> List.mem
t trips'
) trips in
699 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
700 (trips,shared
,trips'
)
701 else (trips,[],trips'
) in
702 foldl (* returns a set - setify inlined *)
704 function (s1
,th1
,wit1
) ->
707 function (s2
,th2
,wit2
) ->
708 match (conj_subst_none th1 th2
) with
710 let t = (s1
,th
,union_wit wit1 wit2
) in
711 if List.mem
t rest
then rest
else t::rest
719 let triples_conj_AW trips trips'
=
720 let (trips,shared
,trips'
) =
721 if false && !pTRIPLES_CONJ_OPT
724 List.partition (function t -> List.mem
t trips'
) trips in
726 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
727 (trips,shared
,trips'
)
728 else (trips,[],trips'
) in
729 foldl (* returns a set - setify inlined *)
731 function (s1
,th1
,wit1
) ->
734 function (s2
,th2
,wit2
) ->
736 (match (conj_subst th1 th2
) with
738 let t = (s1
,th
,union_wit wit1 wit2
) in
739 if List.mem
t rest
then rest
else t::rest
746 (* *************************** *)
747 (* NEGATION (NegState style) *)
748 (* *************************** *)
750 (* Constructive negation at the state level *)
753 | NegState
of 'a list
756 let compatible_states = function
757 (PosState s1
, PosState s2
) ->
758 if s1
= s2
then Some
(PosState s1
) else None
759 | (PosState s1
, NegState s2
) ->
760 if List.mem s1 s2
then None
else Some
(PosState s1
)
761 | (NegState s1
, PosState s2
) ->
762 if List.mem s2 s1
then None
else Some
(PosState s2
)
763 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
766 (* Conjunction on triples with "special states" *)
767 let triples_state_conj trips trips'
=
768 let (trips,shared
,trips'
) =
769 if !pTRIPLES_CONJ_OPT
772 List.partition (function t -> List.mem
t trips'
) trips in
774 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
775 (trips,shared
,trips'
)
776 else (trips,[],trips'
) in
779 function (s1
,th1
,wit1
) ->
782 function (s2
,th2
,wit2
) ->
783 match compatible_states(s1
,s2
) with
785 (match (conj_subst th1 th2
) with
787 let t = (s
,th
,union_wit wit1 wit2
) in
788 if List.mem
t rest
then rest
else t::rest
795 let triple_negate (s
,th
,wits
) =
796 let negstates = (NegState
[s
],top_subst,top_wit) in
797 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
798 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
799 negstates :: (negths @ negwits) (* all different *)
801 (* FIX ME: it is not necessary to do full conjunction *)
802 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
803 if !pTRIPLES_COMPLEMENT_OPT
805 (let cleanup (s
,th
,wit
) =
807 PosState s'
-> [(s'
,th
,wit
)]
809 assert (th
=top_subst);
810 assert (wit
=top_wit);
811 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
812 let (simple
,complex
) =
813 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
815 let (simple
,complex
) =
816 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
818 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
819 top_subst,top_wit)] in
821 else ([(NegState
[],top_subst,top_wit)],trips) in
822 let rec compl trips =
825 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
826 let compld = (compl complex
) in
827 let compld = concatmap cleanup compld in
830 let negstates (st
,th
,wits
) =
831 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
832 let negths (st
,th
,wits
) =
833 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
834 let negwits (st
,th
,wits
) =
835 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
837 [] -> map (function st
-> (st
,top_subst,top_wit)) states
843 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
844 (negstates x @ negths x @ negwits x) xs
)
847 let triple_negate (s
,th
,wits
) =
848 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
849 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
850 ([s
], negths @ negwits) (* all different *)
852 let print_compl_state str (n
,p
) =
853 Printf.printf
"%s neg: " str;
855 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
860 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
862 then map (function st
-> (st
,top_subst,top_wit)) states
864 let cleanup (neg
,pos
) =
866 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
867 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
869 let trips = List.sort
state_compare trips in
870 let all_negated = List.map triple_negate trips in
871 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
872 let (pos1conj
,pos1keep
) =
873 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
874 let (pos2conj
,pos2keep
) =
875 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
876 (Common.union_set neg1 neg2
,
877 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
878 let rec inner_loop = function
879 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
881 let rec outer_loop = function
883 | l
-> outer_loop (inner_loop l
) in
884 cleanup (outer_loop all_negated)
886 (* ********************************** *)
887 (* END OF NEGATION (NegState style) *)
888 (* ********************************** *)
890 (* now this is always true, so we could get rid of it *)
891 let something_dropped = ref true
893 let triples_union trips trips'
=
894 (*unionBy compare eq_trip trips trips';;*)
895 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
897 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
898 Then, the following says that since the first is a more restrictive
899 environment and has fewer witnesses, then it should be dropped. But having
900 fewer witnesses is not necessarily less informative than having more,
901 because fewer witnesses can mean the absence of the witness-causing thing.
902 So the fewer witnesses have to be kept around.
903 subseteq changed to = to make it hopefully work
908 something_dropped := false;
910 then (something_dropped := true; trips)
912 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
915 (match conj_subst th1 th2
with
918 then if (*subseteq*) wit1
= wit2
then 1 else 0
921 then if (*subseteq*) wit2
= wit1
then (-1) else 0
925 let rec first_loop second
= function
927 | x::xs
-> first_loop (second_loop
x second
) xs
928 and second_loop
x = function
931 match subsumes x y
with
932 1 -> something_dropped := true; all
933 | (-1) -> second_loop
x ys
934 | _
-> y
::(second_loop
x ys
) in
935 first_loop trips trips'
937 else unionBy compare
eq_trip trips trips'
940 let triples_witness x unchecked not_keep
trips =
941 let anyneg = (* if any is neg, then all are *)
942 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
943 let anynegwit = (* if any is neg, then all are *)
944 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
945 let allnegwit = (* if any is neg, then all are *)
946 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
948 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
952 function (s
,th
,wit
) as t ->
953 let (th_x
,newth
) = split_subst th
x in
956 (* one consider whether if not not_keep is true, then we should
957 fail. but it could be that the variable is a used_after and
958 then it is the later rule that should fail and not this one *)
959 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
961 (SUB.print_mvar
x; Format.print_flush
();
962 print_state ": empty witness from" [t]);
964 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
965 (* see tests/nestseq for how neg bindings can come up even
966 without eg partial matches
967 (* negated substitution only allowed with negwits.
969 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
972 (print_generic_substitution l
; Format.print_newline
();
973 failwith
"unexpected negative binding with positive witnesses")*)
976 if unchecked
or not_keep
979 if anynegwit wit
&& allnegwit wit
980 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
981 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
984 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
990 (* ---------------------------------------------------------------------- *)
991 (* SAT - Model Checking Algorithm for CTL-FVex *)
993 (* TODO: Implement _all_ operators (directly) *)
994 (* ---------------------------------------------------------------------- *)
997 (* ************************************* *)
998 (* The SAT algorithm and special helpers *)
999 (* ************************************* *)
1001 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1003 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1004 let exp (s
,th
,wit
) =
1006 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1008 A.FORWARD
-> G.predecessors grp s
1009 | A.BACKWARD
-> G.successors grp s
) in
1010 setify (concatmap exp y
)
1015 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1018 None
-> true | Some reqst
-> List.mem s reqst
in
1021 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1024 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1027 (function p
-> (p
,succ grp p
))
1030 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1031 (* would a hash table be more efficient? *)
1032 let all = List.sort
state_compare all in
1033 let rec up_nodes child s
= function
1035 | (s1
,th
,wit
)::xs
->
1036 (match compare s1 child
with
1037 -1 -> up_nodes child s xs
1038 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1040 let neighbor_triples =
1043 function (s
,children
) ->
1047 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1051 match neighbor_triples with
1055 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1057 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1060 None
-> true | Some reqst
-> List.mem s reqst
in
1063 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1066 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1069 (function p
-> (p
,succ grp p
))
1072 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1073 (* would a hash table be more efficient? *)
1074 let all = List.sort
state_compare all in
1075 let rec up_nodes child s
= function
1077 | (s1
,th
,wit
)::xs
->
1078 (match compare s1 child
with
1079 -1 -> up_nodes child s xs
1080 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1082 let neighbor_triples =
1085 function (s
,children
) ->
1088 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1091 match neighbor_triples with
1093 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1095 (* drop_negwits will call setify *)
1096 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1098 let satAX dir m s reqst
= pre_forall dir m s s reqst
1101 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1102 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1103 (*Printf.printf "EU\n";
1104 let ctr = ref 0 in*)
1109 (*let ctr = ref 0 in*)
1112 let rec f y new_info
=
1118 print_graph y ctr;*)
1119 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1120 let res = triples_union first y
in
1121 let new_info = setdiff res y
in
1122 (*Printf.printf "iter %d res %d new_info %d\n"
1123 !ctr (List.length res) (List.length new_info);
1124 print_state "res" res;
1125 print_state "new_info" new_info;
1133 print_graph y ctr;*)
1134 let pre = pre_exist dir m y reqst
in
1135 triples_union s2
(triples_conj s1
pre) in
1139 (* EF phi == E[true U phi] *)
1140 let satEF dir m s2 reqst
=
1142 (*let ctr = ref 0 in*)
1145 let rec f y
new_info =
1151 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1152 let first = pre_exist dir m
new_info reqst
in
1153 let res = triples_union first y
in
1154 let new_info = setdiff res y
in
1155 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1156 (if dir = A.BACKWARD then "reachable" else "real ef")
1157 !ctr (List.length res) (List.length new_info);
1158 print_state "new info" new_info;
1165 let pre = pre_exist dir m y reqst
in
1166 triples_union s2
pre in
1170 type ('
pred,'anno
) auok
=
1171 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1173 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1174 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1180 (*let ctr = ref 0 in*)
1182 if !Flag_ctl.loop_in_src_code
1187 let rec f y newinfo
=
1193 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1197 try Some
(pre_forall dir m
new_info y reqst
)
1202 match triples_conj s1
pre with
1205 (*print_state "s1" s1;
1206 print_state "pre" pre;
1207 print_state "first" first;*)
1208 let res = triples_union first y
in
1210 if not
!something_dropped
1212 else setdiff res y
in
1214 "iter %d res %d new_info %d\n"
1215 !ctr (List.length res) (List.length new_info);
1220 if !Flag_ctl.loop_in_src_code
1224 fix (function s1 -> function s2 ->
1225 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1226 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1227 subseteq s1 s2) in for popl *)
1232 let pre = pre_forall dir m y y reqst
in
1233 triples_union s2 (triples_conj s1 pre) in
1238 (* reqst could be the states of s1 *)
1240 let lstates = mkstates states reqst in
1241 let initial_removed =
1242 triples_complement lstates (triples_union s1 s2) in
1243 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1244 let rec loop base removed =
1246 triples_conj base (pre_exist dir m removed reqst) in
1248 triples_conj base (triples_complement lstates new_removed) in
1249 if supseteq new_base base
1250 then triples_union base s2
1251 else loop new_base new_removed in
1252 loop initial_base initial_removed *)
1254 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1260 This works extremely badly when the region is small and the end of the
1261 region is very ambiguous, eg free(x) ... x
1265 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1266 let ostates = Common.union_set (get_states s1) (get_states s2) in
1269 A.FORWARD -> G.successors grp
1270 | A.BACKWARD -> G.predecessors grp) in
1272 List.fold_left Common.union_set ostates (List.map succ ostates) in
1273 let negphi = triples_complement states s1 in
1274 let negpsi = triples_complement states s2 in
1275 triples_complement ostates
1276 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1279 (*let ctr = ref 0 in*)
1283 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1286 let pre = pre_forall dir m y y reqst
in
1287 (*print_state "pre" pre;*)
1288 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1289 triples_union s2 conj in
1290 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1291 (* drop wits on s1 represents that we don't want any witnesses from
1292 the case that infinitely loops, only from the case that gets
1293 out of the loop. s1 is like a guard. To see the problem, consider
1294 an example where both s1 and s2 match some code after the loop.
1295 we only want the witness from s2. *)
1296 setgfix f (triples_union (nub(drop_wits s1)) s2)
1299 let satAF dir m s reqst
=
1303 let rec f y newinfo
=
1308 let first = pre_forall dir m
new_info y reqst
in
1309 let res = triples_union first y
in
1310 let new_info = setdiff res y
in
1316 let pre = pre_forall dir m y y reqst
in
1317 triples_union s
pre in
1320 let satAG dir
((_
,_
,states) as m
) s reqst
=
1324 let pre = pre_forall dir m y y reqst
in
1325 triples_conj y
pre in
1328 let satEG dir
((_
,_
,states) as m
) s reqst
=
1332 let pre = pre_exist dir m y reqst
in
1333 triples_conj y
pre in
1336 (* **************************************************************** *)
1337 (* Inner And - a way of dealing with multiple matches within a node *)
1338 (* **************************************************************** *)
1339 (* applied to the result of matching a node. collect witnesses when the
1340 states and environments are the same *)
1342 let inner_and trips =
1343 let rec loop = function
1345 | (s
,th
,w
)::trips ->
1346 let (cur
,acc
) = loop trips in
1348 (s'
,_
,_
)::_
when s
= s'
->
1349 let rec loop'
= function
1351 | ((_
,th'
,w'
) as t'
)::ts'
->
1352 (match conj_subst th th'
with
1353 Some th''
-> (s
,th''
,union_wit w w'
)::ts'
1354 | None
-> t'
::(loop' ts'
)) in
1356 | _
-> ([(s
,th
,w
)],cur
@acc
)) in
1358 loop (List.sort
state_compare trips) (* is this sort needed? *) in
1361 (* *************** *)
1362 (* Partial matches *)
1363 (* *************** *)
1365 let filter_conj states unwanted partial_matches
=
1367 triples_conj (triples_complement states (unwitify unwanted
))
1369 triples_conj (unwitify x) (triples_complement states x)
1371 let strict_triples_conj strict
states trips trips'
=
1372 let res = triples_conj trips trips'
in
1373 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1375 let fail_left = filter_conj states trips trips'
in
1376 let fail_right = filter_conj states trips'
trips in
1377 let ors = triples_union fail_left fail_right in
1378 triples_union res ors
1381 let strict_triples_conj_none strict
states trips trips'
=
1382 let res = triples_conj_none trips trips'
in
1383 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1385 let fail_left = filter_conj states trips trips'
in
1386 let fail_right = filter_conj states trips'
trips in
1387 let ors = triples_union fail_left fail_right in
1388 triples_union res ors
1391 let left_strict_triples_conj strict
states trips trips'
=
1392 let res = triples_conj trips trips'
in
1393 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1395 let fail_left = filter_conj states trips trips'
in
1396 triples_union res fail_left
1399 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1400 let res = op dir m
trips required_states
in
1401 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1403 let states = mkstates states required_states
in
1404 let fail = filter_conj states res (failop dir m
trips required_states
) in
1405 triples_union res fail
1408 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1410 let res = op dir m
trips trips' required_states
in
1411 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1413 let states = mkstates states required_states
in
1414 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1415 triples_union res fail
1418 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1419 required_states
print_graph =
1420 match op dir m
trips trips' required_states
print_graph with
1422 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1424 let states = mkstates states required_states
in
1426 filter_conj states res (failop dir m
trips' required_states
) in
1427 AUok
(triples_union res fail)
1429 | AUfailed
res -> AUfailed
res
1431 (* ********************* *)
1432 (* Environment functions *)
1433 (* ********************* *)
1435 let drop_wits required_states s phi
=
1436 match required_states
with
1438 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1441 let print_required required
=
1444 Format.print_string
"{";
1447 print_generic_substitution reqd
; Format.print_newline
())
1449 Format.print_string
"}";
1450 Format.print_newline
())
1455 let extend_required trips required
=
1456 if !Flag_ctl.partial_match
1459 if !pREQUIRED_ENV_OPT
1465 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1467 let envs = if List.mem
[] envs then [] else envs in
1468 match (envs,required
) with
1472 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1477 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1484 match conj_subst t r
with
1485 None
-> rest
| Some th
-> add th rest
)
1489 with Too_long
-> envs :: required
)
1490 | (envs,_
) -> envs :: required
1493 let drop_required v required
=
1494 if !pREQUIRED_ENV_OPT
1501 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1503 (* check whether an entry has become useless *)
1504 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1507 (* no idea how to write this function ... *)
1509 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1511 let satLabel label required p
=
1513 if !pSATLABEL_MEMO_OPT
1516 let states_subs = Hashtbl.find
memo_label p
in
1517 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1520 let triples = setify(label p
) in
1521 Hashtbl.add memo_label p
1522 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1524 else setify(label p
) in
1526 (if !pREQUIRED_ENV_OPT
1530 function ((s
,th
,_
) as t) ->
1532 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1539 let get_required_states l
=
1540 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1542 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1545 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1546 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1548 match required_states
with
1553 A.FORWARD
-> G.successors
1554 | A.BACKWARD
-> G.predecessors in
1555 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1558 let reachable_table =
1559 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1561 (* like satEF, but specialized for get_reachable *)
1562 let reachsatEF dir
(grp
,_
,_
) s2 =
1564 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1565 let union = unionBy compare
(=) in
1566 let rec f y
= function
1569 let (pre_collected
,new_info) =
1570 List.partition (function Common.Left
x -> true | _
-> false)
1573 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1574 with Not_found
-> Common.Right
x)
1579 function Common.Left
x -> union x rest
1580 | _
-> failwith
"not possible")
1584 (function Common.Right
x -> x | _
-> failwith
"not possible")
1586 let first = inner_setify (concatmap (dirop grp
) new_info) in
1587 let new_info = setdiff first y in
1588 let res = new_info @ y in
1590 List.rev
(f s2 s2) (* put root first *)
1592 let get_reachable dir m required_states
=
1593 match required_states
with
1600 if List.mem cur rest
1604 (try Hashtbl.find
reachable_table (cur
,dir
)
1607 let states = reachsatEF dir m
[cur
] in
1608 Hashtbl.add reachable_table (cur
,dir
) states;
1617 Printf.sprintf
"_c%d" c
1619 (* **************************** *)
1620 (* End of environment functions *)
1621 (* **************************** *)
1623 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1625 let rec satloop unchecked required required_states
1626 ((grp
,label,states) as m
) phi env
=
1627 let rec loop unchecked required required_states phi
=
1628 (*Common.profile_code "satloop" (fun _ -> *)
1632 | A.True
-> triples_top states
1633 | A.Pred
(p
) -> satLabel label required p
1634 | A.Uncheck
(phi1
) ->
1635 let unchecked = if !pUNCHECK_OPT then true else false in
1636 loop unchecked required required_states phi1
1638 let phires = loop unchecked required required_states phi
in
1640 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1641 triples_complement (mkstates states required_states
)
1643 | A.Or
(phi1
,phi2
) ->
1645 (loop unchecked required required_states phi1
)
1646 (loop unchecked required required_states phi2
)
1647 | A.SeqOr
(phi1
,phi2
) ->
1648 let res1 = loop unchecked required required_states phi1
in
1649 let res2 = loop unchecked required required_states phi2
in
1650 let res1neg = unwitify res1 in
1653 (triples_complement (mkstates states required_states
) res1neg)
1655 | A.And
(strict
,phi1
,phi2
) ->
1656 (* phi1 is considered to be more likely to be [], because of the
1657 definition of asttoctl. Could use heuristics such as the size of
1659 let pm = !Flag_ctl.partial_match
in
1660 (match (pm,loop unchecked required required_states phi1
) with
1661 (false,[]) when !pLazyOpt -> []
1663 let new_required = extend_required phi1res required
in
1664 let new_required_states = get_required_states phi1res
in
1665 (match (pm,loop unchecked new_required new_required_states phi2
)
1667 (false,[]) when !pLazyOpt -> []
1669 strict_triples_conj strict
1670 (mkstates states required_states
)
1672 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1673 (* phi2 can appear anywhere that is reachable *)
1674 let pm = !Flag_ctl.partial_match
in
1675 (match (pm,loop unchecked required required_states phi1
) with
1678 let new_required = extend_required phi1res required
in
1679 let new_required_states = get_required_states phi1res
in
1680 let new_required_states =
1681 get_reachable dir m
new_required_states in
1682 (match (pm,loop unchecked new_required new_required_states phi2
)
1684 (false,[]) -> phi1res
1687 [] -> (* !Flag_ctl.partial_match must be true *)
1691 let s = mkstates states required_states
in
1693 (function a
-> function b
->
1694 strict_triples_conj strict
s a
[b
])
1695 [List.hd phi2res
] (List.tl phi2res
)
1698 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1699 let s = mkstates states required_states
in
1701 (function a
-> function b
->
1702 strict_triples_conj strict
s a b
)
1706 "only one result allowed for the left arg of AndAny")))
1707 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1708 (* phi2 can appear anywhere that is reachable *)
1709 let pm = !Flag_ctl.partial_match
in
1710 (match (pm,loop unchecked required required_states phi1
) with
1713 let new_required = extend_required phi1res required
in
1714 let new_required_states = get_required_states phi1res
in
1715 let new_required_states =
1716 get_reachable dir m
new_required_states in
1717 (match (pm,loop unchecked new_required new_required_states phi2
)
1719 (false,[]) -> phi1res
1721 (* if there is more than one state, something about the
1722 environment has to ensure that the right triples of
1723 phi2 get associated with the triples of phi1.
1724 the asttoctl2 has to ensure that that is the case.
1725 these should thus be structural properties.
1726 env of phi2 has to be a proper subset of env of phi1
1727 to ensure all end up being consistent. no new triples
1728 should be generated. strict_triples_conj_none takes
1731 let s = mkstates states required_states
in
1734 function (st
,th
,_
) as phi2_elem
->
1736 triples_complement [st
] [(st
,th
,[])] in
1737 strict_triples_conj_none strict
s acc
1738 (phi2_elem
::inverse))
1740 | A.InnerAnd
(phi
) ->
1741 inner_and(loop unchecked required required_states phi
)
1743 let new_required_states =
1744 get_children_required_states dir m required_states
in
1745 satEX dir m
(loop unchecked required
new_required_states phi
)
1747 | A.AX
(dir
,strict
,phi
) ->
1748 let new_required_states =
1749 get_children_required_states dir m required_states
in
1750 let res = loop unchecked required
new_required_states phi
in
1751 strict_A1 strict
satAX satEX dir m
res required_states
1753 let new_required_states = get_reachable dir m required_states
in
1754 satEF dir m
(loop unchecked required
new_required_states phi
)
1756 | A.AF
(dir
,strict
,phi
) ->
1757 if !Flag_ctl.loop_in_src_code
1759 loop unchecked required required_states
1760 (A.AU
(dir
,strict
,A.True
,phi
))
1762 let new_required_states = get_reachable dir m required_states
in
1763 let res = loop unchecked required
new_required_states phi
in
1764 strict_A1 strict
satAF satEF dir m
res new_required_states
1766 let new_required_states = get_reachable dir m required_states
in
1767 satEG dir m
(loop unchecked required
new_required_states phi
)
1769 | A.AG
(dir
,strict
,phi
) ->
1770 let new_required_states = get_reachable dir m required_states
in
1771 let res = loop unchecked required
new_required_states phi
in
1772 strict_A1 strict
satAG satEF dir m
res new_required_states
1773 | A.EU
(dir
,phi1
,phi2
) ->
1774 let new_required_states = get_reachable dir m required_states
in
1775 (match loop unchecked required
new_required_states phi2
with
1776 [] when !pLazyOpt -> []
1778 let new_required = extend_required s2 required
in
1779 let s1 = loop unchecked new_required new_required_states phi1
in
1780 satEU dir m
s1 s2 new_required_states
1781 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1782 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1783 let new_required_states = get_reachable dir m required_states
in
1784 (match loop unchecked required
new_required_states phi2
with
1785 [] when !pLazyOpt -> []
1787 let new_required = extend_required s2 required
in
1788 let s1 = loop unchecked new_required new_required_states phi1
in
1789 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1790 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1791 (*Printf.printf "using AU\n"; flush stdout;*)
1792 let new_required_states = get_reachable dir m required_states
in
1793 (match loop unchecked required
new_required_states phi2
with
1794 [] when !pLazyOpt -> []
1796 let new_required = extend_required s2 required
in
1797 let s1 = loop unchecked new_required new_required_states phi1
in
1799 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1801 print_graph_c grp
new_required_states y ctr phi
) in
1804 | AUfailed tmp_res
->
1805 (* found a loop, have to try AW *)
1807 A[E[phi1 U phi2] & phi1 W phi2]
1808 the and is nonstrict *)
1809 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1810 (*Printf.printf "using AW\n"; flush stdout;*)
1813 (satEU dir m
s1 tmp_res
new_required_states
1814 (* no graph, for the moment *)
1817 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1819 | A.Implies
(phi1
,phi2
) ->
1820 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1821 | A.Exists
(keep
,v
,phi
) ->
1822 let new_required = drop_required v required
in
1823 triples_witness v
unchecked (not keep
)
1824 (loop unchecked new_required required_states phi
)
1825 | A.Let
(v
,phi1
,phi2
) ->
1826 (* should only be used when the properties unchecked, required,
1827 and required_states are known to be the same or at least
1828 compatible between all the uses. this is not checked. *)
1829 let res = loop unchecked required required_states phi1
in
1830 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1831 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1832 (* should only be used when the properties unchecked, required,
1833 and required_states are known to be the same or at least
1834 compatible between all the uses. this is not checked. *)
1835 (* doesn't seem to be used any more *)
1836 let new_required_states = get_reachable dir m required_states
in
1837 let res = loop unchecked required
new_required_states phi1
in
1838 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1840 let res = List.assoc v env
in
1842 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1844 | A.XX
(phi
) -> failwith
"should have been removed" in
1845 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1846 let res = drop_wits required_states
res phi
(* ) *) in
1847 print_graph grp required_states
res "" phi
;
1850 loop unchecked required required_states phi
1854 (* SAT with tracking *)
1855 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1856 ((_
,label,states) as m
) phi env
=
1857 let anno res children
= (annot lvl phi
res children
,res) in
1858 let satv unchecked required required_states phi0 env
=
1859 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1861 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1862 anno (satloop unchecked required required_states m phi env
) []
1866 A.False
-> anno [] []
1867 | A.True
-> anno (triples_top states) []
1869 Printf.printf
"label\n"; flush stdout
;
1870 anno (satLabel label required p
) []
1871 | A.Uncheck
(phi1
) ->
1872 let unchecked = if !pUNCHECK_OPT then true else false in
1873 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1874 Printf.printf
"uncheck\n"; flush stdout
;
1878 satv unchecked required required_states phi1 env
in
1879 Printf.printf
"not\n"; flush stdout
;
1880 anno (triples_complement (mkstates states required_states
) res) [child
]
1881 | A.Or
(phi1
,phi2
) ->
1883 satv unchecked required required_states phi1 env
in
1885 satv unchecked required required_states phi2 env
in
1886 Printf.printf
"or\n"; flush stdout
;
1887 anno (triples_union res1 res2) [child1
; child2
]
1888 | A.SeqOr
(phi1
,phi2
) ->
1890 satv unchecked required required_states phi1 env
in
1892 satv unchecked required required_states phi2 env
in
1894 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1895 Printf.printf
"seqor\n"; flush stdout
;
1896 anno (triples_union res1
1898 (triples_complement (mkstates states required_states
)
1902 | A.And
(strict
,phi1
,phi2
) ->
1903 let pm = !Flag_ctl.partial_match
in
1904 (match (pm,satv unchecked required required_states phi1 env
) with
1905 (false,(child1
,[])) ->
1906 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1907 | (_
,(child1
,res1)) ->
1908 let new_required = extend_required res1 required
in
1909 let new_required_states = get_required_states res1 in
1910 (match (pm,satv unchecked new_required new_required_states phi2
1912 (false,(child2
,[])) ->
1913 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1914 | (_
,(child2
,res2)) ->
1915 Printf.printf
"and\n"; flush stdout
;
1917 strict_triples_conj strict
1918 (mkstates states required_states
)
1920 anno res [child1
; child2
]))
1921 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1922 let pm = !Flag_ctl.partial_match
in
1923 (match (pm,satv unchecked required required_states phi1 env
) with
1924 (false,(child1
,[])) ->
1925 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1926 | (_
,(child1
,res1)) ->
1927 let new_required = extend_required res1 required
in
1928 let new_required_states = get_required_states res1 in
1929 let new_required_states =
1930 get_reachable dir m
new_required_states in
1931 (match (pm,satv unchecked new_required new_required_states phi2
1933 (false,(child2
,[])) ->
1934 Printf.printf
"andany\n"; flush stdout
;
1935 anno res1 [child1
;child2
]
1936 | (_
,(child2
,res2)) ->
1938 [] -> (* !Flag_ctl.partial_match must be true *)
1940 then anno [] [child1
; child2
]
1943 let s = mkstates states required_states
in
1945 (function a
-> function b
->
1946 strict_triples_conj strict
s a
[b
])
1947 [List.hd
res2] (List.tl
res2) in
1948 anno res [child1
; child2
]
1951 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1952 Printf.printf
"andany\n"; flush stdout
;
1954 let s = mkstates states required_states
in
1956 (function a
-> function b
->
1957 strict_triples_conj strict
s a b
)
1959 anno res [child1
; child2
]
1962 "only one result allowed for the left arg of AndAny")))
1963 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1964 let pm = !Flag_ctl.partial_match
in
1965 (match (pm,satv unchecked required required_states phi1 env
) with
1966 (false,(child1
,[])) ->
1967 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1968 | (_
,(child1
,res1)) ->
1969 let new_required = extend_required res1 required
in
1970 let new_required_states = get_required_states res1 in
1971 let new_required_states =
1972 get_reachable dir m
new_required_states in
1973 (match (pm,satv unchecked new_required new_required_states phi2
1975 (false,(child2
,[])) ->
1976 Printf.printf
"andany\n"; flush stdout
;
1977 anno res1 [child1
;child2
]
1978 | (_
,(child2
,res2)) ->
1980 let s = mkstates states required_states
in
1983 function (st
,th
,_
) as phi2_elem
->
1985 triples_complement [st
] [(st
,th
,[])] in
1986 strict_triples_conj_none strict
s acc
1987 (phi2_elem
::inverse))
1989 anno res [child1
; child2
]))
1990 | A.InnerAnd
(phi1
) ->
1991 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1992 Printf.printf
"uncheck\n"; flush stdout
;
1993 anno (inner_and res1) [child1
]
1995 let new_required_states =
1996 get_children_required_states dir m required_states
in
1998 satv unchecked required
new_required_states phi1 env
in
1999 Printf.printf
"EX\n"; flush stdout
;
2000 anno (satEX dir m
res required_states
) [child
]
2001 | A.AX
(dir
,strict
,phi1
) ->
2002 let new_required_states =
2003 get_children_required_states dir m required_states
in
2005 satv unchecked required
new_required_states phi1 env
in
2006 Printf.printf
"AX\n"; flush stdout
;
2007 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2010 let new_required_states = get_reachable dir m required_states
in
2012 satv unchecked required
new_required_states phi1 env
in
2013 Printf.printf
"EF\n"; flush stdout
;
2014 anno (satEF dir m
res new_required_states) [child
]
2015 | A.AF
(dir
,strict
,phi1
) ->
2016 if !Flag_ctl.loop_in_src_code
2018 satv unchecked required required_states
2019 (A.AU
(dir
,strict
,A.True
,phi1
))
2022 (let new_required_states = get_reachable dir m required_states
in
2024 satv unchecked required
new_required_states phi1 env
in
2025 Printf.printf
"AF\n"; flush stdout
;
2027 strict_A1 strict
satAF satEF dir m
res new_required_states in
2030 let new_required_states = get_reachable dir m required_states
in
2032 satv unchecked required
new_required_states phi1 env
in
2033 Printf.printf
"EG\n"; flush stdout
;
2034 anno (satEG dir m
res new_required_states) [child
]
2035 | A.AG
(dir
,strict
,phi1
) ->
2036 let new_required_states = get_reachable dir m required_states
in
2038 satv unchecked required
new_required_states phi1 env
in
2039 Printf.printf
"AG\n"; flush stdout
;
2040 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2043 | A.EU
(dir
,phi1
,phi2
) ->
2044 let new_required_states = get_reachable dir m required_states
in
2045 (match satv unchecked required
new_required_states phi2 env
with
2047 Printf.printf
"EU\n"; flush stdout
;
2050 let new_required = extend_required res2 required
in
2052 satv unchecked new_required new_required_states phi1 env
in
2053 Printf.printf
"EU\n"; flush stdout
;
2054 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2056 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2057 failwith
"should not be used" (*
2058 let new_required_states = get_reachable dir m required_states in
2059 (match satv unchecked required new_required_states phi2 env with
2061 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2063 let new_required = extend_required res2 required in
2065 satv unchecked new_required new_required_states phi1 env in
2066 Printf.printf "AW %b\n" unchecked; flush stdout;
2068 strict_A2 strict satAW satEF dir m res1 res2
2069 new_required_states in
2070 anno res [child1; child2]) *)
2071 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2072 let new_required_states = get_reachable dir m required_states
in
2073 (match satv unchecked required
new_required_states phi2 env
with
2075 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2077 let new_required = extend_required s2 required
in
2079 satv unchecked new_required new_required_states phi1 env
in
2080 Printf.printf
"AU\n"; flush stdout
;
2082 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2083 (fun y str -> ()) in
2086 anno res [child1
; child2
]
2087 | AUfailed tmp_res
->
2088 (* found a loop, have to try AW *)
2090 A[E[phi1 U phi2] & phi1 W phi2]
2091 the and is nonstrict *)
2092 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2093 Printf.printf
"AW\n"; flush stdout
;
2096 (satEU dir m
s1 tmp_res
new_required_states
2097 (* no graph, for the moment *)
2101 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2102 anno res [child1
; child2
]))
2103 | A.Implies
(phi1
,phi2
) ->
2104 satv unchecked required required_states
2105 (A.Or
(A.Not phi1
,phi2
))
2107 | A.Exists
(keep
,v
,phi1
) ->
2108 let new_required = drop_required v required
in
2110 satv unchecked new_required required_states phi1 env
in
2111 Printf.printf
"exists\n"; flush stdout
;
2112 anno (triples_witness v
unchecked (not keep
) res) [child
]
2113 | A.Let
(v
,phi1
,phi2
) ->
2115 satv unchecked required required_states phi1 env
in
2117 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2118 anno res2 [child1
;child2
]
2119 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2120 let new_required_states = get_reachable dir m required_states
in
2122 satv unchecked required
new_required_states phi1 env
in
2124 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2125 anno res2 [child1
;child2
]
2127 Printf.printf
"Ref\n"; flush stdout
;
2128 let res = List.assoc v env
in
2131 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2134 | A.XX
(phi
) -> failwith
"should have been removed" in
2135 let res1 = drop_wits required_states
res phi
in
2139 print_required_states required_states
;
2140 print_state "after drop_wits" res1 end;
2145 let sat_verbose annotate maxlvl lvl m phi
=
2146 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2148 (* Type for annotations collected in a tree *)
2149 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2151 let sat_annotree annotate m phi
=
2152 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2153 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2157 let sat m phi = satloop m phi []
2161 let simpleanno l phi
res =
2163 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2164 print_generic_algo
(List.sort compare
res);
2165 Format.print_string
"\n------------------------------\n\n" in
2166 let pp_dir = function
2168 | A.BACKWARD
-> pp "^" in
2170 | A.False
-> pp "False"
2171 | A.True
-> pp "True"
2172 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2173 | A.Not
(phi
) -> pp "Not"
2174 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2175 | A.And
(_
,phi1
,phi2
) -> pp "And"
2176 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2177 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2178 | A.Or
(phi1
,phi2
) -> pp "Or"
2179 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2180 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2181 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2182 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2183 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2184 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2185 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2186 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2187 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2188 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2189 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2190 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2191 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2192 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2193 | A.Uncheck
(s) -> pp "Uncheck"
2194 | A.InnerAnd
(s) -> pp "InnerAnd"
2195 | A.XX
(phi1
) -> pp "XX"
2199 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2200 print a ctl formula more accurately if you want.
2201 Use the print_xxx provided in the different module to call
2202 Pretty_print_ctl.pp_ctl.
2205 let simpleanno2 l phi
res =
2207 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2208 Format.print_newline
();
2209 Format.print_string
"----------------------------------------------------";
2210 Format.print_newline
();
2211 print_generic_algo
(List.sort compare
res);
2212 Format.print_newline
();
2213 Format.print_string
"----------------------------------------------------";
2214 Format.print_newline
();
2215 Format.print_newline
();
2219 (* ---------------------------------------------------------------------- *)
2221 (* ---------------------------------------------------------------------- *)
2223 type optentry
= bool ref * string
2224 type options
= {label : optentry
; unch
: optentry
;
2225 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2227 reqenv
: optentry
; reqstates
: optentry
}
2230 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2231 unch
= (pUNCHECK_OPT,"uncheck_opt");
2232 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2233 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2234 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2235 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2236 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2237 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2241 ("label ",[options.label]);
2242 ("unch ",[options.unch
]);
2243 ("unch and label ",[options.label;options.unch
])]
2246 [("conj ", [options.conj]);
2247 ("compl1 ", [options.compl1
]);
2248 ("compl12 ", [options.compl1
;options.compl2
]);
2249 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2250 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2252 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2253 ("compl12 unch satl ",
2254 [options.compl1;options.compl2;options.unch;options.label]); *)
2255 ("conj/compl12 unch satl ",
2256 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2259 [("newinfo ", [options.newinfo
]);
2260 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2263 [("reqenv ", [options.reqenv
]);
2264 ("reqstates ", [options.reqstates
]);
2265 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2266 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2267 ("reqstates unch satl ",
2268 [options.reqstates;options.unch;options.label]);*)
2269 ("reqenv/states unch satl ",
2270 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2273 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2274 options.newinfo
;options.reqenv
;options.reqstates
]
2277 [("all ",all_options)]
2279 let all_options_but_path =
2280 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2281 options.reqenv
;options.reqstates
]
2283 let all_but_path = ("all but path ",all_options_but_path)
2286 [(satAW_calls, "satAW", ref 0);
2287 (satAU_calls, "satAU", ref 0);
2288 (satEF_calls, "satEF", ref 0);
2289 (satAF_calls, "satAF", ref 0);
2290 (satEG_calls, "satEG", ref 0);
2291 (satAG_calls, "satAG", ref 0);
2292 (satEU_calls, "satEU", ref 0)]
2296 (function (opt
,x) ->
2297 (opt
,x,ref 0.0,ref 0,
2298 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2299 [List.hd
all;all_but_path]
2300 (*(all@baseline@conjneg@path@required)*)
2304 let rec iter fn = function
2306 | n
-> let _ = fn() in
2307 (Hashtbl.clear
reachable_table;
2308 Hashtbl.clear
memo_label;
2312 let copy_to_stderr fl
=
2313 let i = open_in fl
in
2315 Printf.fprintf stderr
"%s\n" (input_line
i);
2317 try loop() with _ -> ();
2320 let bench_sat (_,_,states) fn =
2321 List.iter (function (opt
,_) -> opt
:= false) all_options;
2324 (function (name
,options,time
,trips,counter_info
) ->
2325 let iterct = !Flag_ctl.bench
in
2326 if !time
> float_of_int
timeout then time
:= -100.0;
2327 if not
(!time
= -100.0)
2330 Hashtbl.clear
reachable_table;
2331 Hashtbl.clear
memo_label;
2332 List.iter (function (opt
,_) -> opt
:= true) options;
2333 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2337 let bef = Sys.time
() in
2339 Common.timeout_function
timeout
2341 let bef = Sys.time
() in
2342 let res = iter fn iterct in
2343 let aft = Sys.time
() in
2344 time
:= !time
+. (aft -. bef);
2345 trips := !trips + !triples;
2347 (function (calls
,_,save_calls
) ->
2348 function (current_calls
,current_cfg
,current_max_cfg
) ->
2350 !current_calls
+ (!calls
- !save_calls
);
2351 if (!calls
- !save_calls
) > 0
2353 (let st = List.length
states in
2354 current_cfg
:= !current_cfg
+ st;
2355 if st > !current_max_cfg
2356 then current_max_cfg
:= st))
2357 counters counter_info
;
2362 let aft = Sys.time
() in
2364 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2368 List.iter (function (opt
,_) -> opt
:= false) options;
2373 Printf.fprintf stderr
"\n";
2377 (if not
(List.for_all
(function x -> x = res) rest
)
2379 (List.iter (print_state "a state") answers;
2380 Printf.printf
"something doesn't work\n");
2384 let iterct = !Flag_ctl.bench
in
2388 (function (name
,options,time
,trips,counter_info
) ->
2389 Printf.fprintf stderr
"%s Numbers: %f %d "
2390 name
(!time
/. (float_of_int
iterct)) !trips;
2392 (function (calls
,cfg
,max_cfg
) ->
2393 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2395 Printf.fprintf stderr
"\n")
2398 (* ---------------------------------------------------------------------- *)
2399 (* preprocessing: ignore irrelevant functions *)
2401 let preprocess (cfg
,_,_) label = function
2402 [] -> true (* no information, try everything *)
2404 let sz = G.size cfg
in
2405 let verbose_output pred = function
2407 Printf.printf
"did not find:\n";
2408 P.print_predicate
pred; Format.print_newline
()
2410 Printf.printf
"found:\n";
2411 P.print_predicate
pred; Format.print_newline
();
2412 Printf.printf
"but it was not enough\n" in
2413 let get_any verbose
x =
2415 try Hashtbl.find
memo_label x
2418 (let triples = label x in
2420 List.map (function (st,th
,_) -> (st,th
)) triples in
2421 Hashtbl.add memo_label x filtered;
2423 if verbose
then verbose_output x res;
2426 (* don't bother testing when there are more patterns than nodes *)
2427 if List.length l
> sz-2
2429 else List.for_all
(get_any false) l
in
2430 if List.exists
get_all l
2433 (if !Flag_ctl.verbose_match
2435 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2439 let filter_partial_matches trips =
2440 if !Flag_ctl.partial_match
2442 let anynegwit = (* if any is neg, then all are *)
2443 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2445 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2448 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2452 (* ---------------------------------------------------------------------- *)
2453 (* Main entry point for engine *)
2454 let sat m phi reqopt
=
2456 (match !Flag_ctl.steps
with
2457 None
-> step_count := 0
2458 | Some
x -> step_count := x);
2459 Hashtbl.clear
reachable_table;
2460 Hashtbl.clear
memo_label;
2461 let (x,label,states) = m
in
2462 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2464 ((* to drop when Yoann initialized this flag *)
2465 if List.exists
(G.extract_is_loop
x) states
2466 then Flag_ctl.loop_in_src_code
:= true;
2467 let m = (x,label,List.sort compare
states) in
2469 if(!Flag_ctl.verbose_ctl_engine
)
2471 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2472 if !Flag_ctl.bench
> 0
2476 let fn _ = satloop false [] None
m phi
[] in
2477 if !Flag_ctl.bench
> 0
2479 else Common.profile_code
"ctl" (fun _ -> fn()) in
2480 let res = filter_partial_matches res in
2482 Printf.printf "steps: start %d, stop %d\n"
2483 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2485 Printf.printf "triples: %d\n" !triples;
2486 print_state "final result" res;
2488 List.sort compare
res)
2490 (if !Flag_ctl.verbose_ctl_engine
2491 then Common.pr2
"missing something required";
2496 (* ********************************************************************** *)
2497 (* End of Module: CTL_ENGINE *)
2498 (* ********************************************************************** *)