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 *)
1341 (* not a good idea, poses problem for unparsing, because don't realize that
1342 adjacent things come from different matches, leading to loss of newlines etc.
1343 exple struct I { ... - int x; + int y; ...} *)
1345 let inner_and trips = trips (*
1346 let rec loop = function
1348 | (s,th,w)::trips ->
1349 let (cur,acc) = loop trips in
1351 (s',_,_)::_ when s = s' ->
1352 let rec loop' = function
1354 | ((_,th',w') as t')::ts' ->
1355 (match conj_subst th th' with
1356 Some th'' -> (s,th'',union_wit w w')::ts'
1357 | None -> t'::(loop' ts')) in
1359 | _ -> ([(s,th,w)],cur@acc)) in
1361 loop (List.sort state_compare trips) (* is this sort needed? *) in
1364 (* *************** *)
1365 (* Partial matches *)
1366 (* *************** *)
1368 let filter_conj states unwanted partial_matches
=
1370 triples_conj (triples_complement states (unwitify unwanted
))
1372 triples_conj (unwitify x) (triples_complement states x)
1374 let strict_triples_conj strict
states trips trips'
=
1375 let res = triples_conj trips trips'
in
1376 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1378 let fail_left = filter_conj states trips trips'
in
1379 let fail_right = filter_conj states trips'
trips in
1380 let ors = triples_union fail_left fail_right in
1381 triples_union res ors
1384 let strict_triples_conj_none strict
states trips trips'
=
1385 let res = triples_conj_none trips trips'
in
1386 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1388 let fail_left = filter_conj states trips trips'
in
1389 let fail_right = filter_conj states trips'
trips in
1390 let ors = triples_union fail_left fail_right in
1391 triples_union res ors
1394 let left_strict_triples_conj strict
states trips trips'
=
1395 let res = triples_conj trips trips'
in
1396 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1398 let fail_left = filter_conj states trips trips'
in
1399 triples_union res fail_left
1402 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1403 let res = op dir m
trips required_states
in
1404 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1406 let states = mkstates states required_states
in
1407 let fail = filter_conj states res (failop dir m
trips required_states
) in
1408 triples_union res fail
1411 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1413 let res = op dir m
trips trips' required_states
in
1414 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1416 let states = mkstates states required_states
in
1417 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1418 triples_union res fail
1421 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1422 required_states
print_graph =
1423 match op dir m
trips trips' required_states
print_graph with
1425 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1427 let states = mkstates states required_states
in
1429 filter_conj states res (failop dir m
trips' required_states
) in
1430 AUok
(triples_union res fail)
1432 | AUfailed
res -> AUfailed
res
1434 (* ********************* *)
1435 (* Environment functions *)
1436 (* ********************* *)
1438 let drop_wits required_states s phi
=
1439 match required_states
with
1441 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1444 let print_required required
=
1447 Format.print_string
"{";
1450 print_generic_substitution reqd
; Format.print_newline
())
1452 Format.print_string
"}";
1453 Format.print_newline
())
1458 let extend_required trips required
=
1459 if !Flag_ctl.partial_match
1462 if !pREQUIRED_ENV_OPT
1468 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1470 let envs = if List.mem
[] envs then [] else envs in
1471 match (envs,required
) with
1475 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1480 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1487 match conj_subst t r
with
1488 None
-> rest
| Some th
-> add th rest
)
1492 with Too_long
-> envs :: required
)
1493 | (envs,_
) -> envs :: required
1496 let drop_required v required
=
1497 if !pREQUIRED_ENV_OPT
1504 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1506 (* check whether an entry has become useless *)
1507 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1510 (* no idea how to write this function ... *)
1512 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1514 let satLabel label required p
=
1516 if !pSATLABEL_MEMO_OPT
1519 let states_subs = Hashtbl.find
memo_label p
in
1520 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1523 let triples = setify(label p
) in
1524 Hashtbl.add memo_label p
1525 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1527 else setify(label p
) in
1528 (* normalize first; conj_subst relies on sorting *)
1529 let ntriples = normalize triples in
1530 if !pREQUIRED_ENV_OPT
1534 function ((s
,th
,_
) as t) ->
1536 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1543 let get_required_states l
=
1544 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1546 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1549 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1550 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1552 match required_states
with
1557 A.FORWARD
-> G.successors
1558 | A.BACKWARD
-> G.predecessors in
1559 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1562 let reachable_table =
1563 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1565 (* like satEF, but specialized for get_reachable *)
1566 let reachsatEF dir
(grp
,_
,_
) s2 =
1568 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1569 let union = unionBy compare
(=) in
1570 let rec f y
= function
1573 let (pre_collected
,new_info) =
1574 List.partition (function Common.Left
x -> true | _
-> false)
1577 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1578 with Not_found
-> Common.Right
x)
1583 function Common.Left
x -> union x rest
1584 | _
-> failwith
"not possible")
1588 (function Common.Right
x -> x | _
-> failwith
"not possible")
1590 let first = inner_setify (concatmap (dirop grp
) new_info) in
1591 let new_info = setdiff first y in
1592 let res = new_info @ y in
1594 List.rev
(f s2 s2) (* put root first *)
1596 let get_reachable dir m required_states
=
1597 match required_states
with
1604 if List.mem cur rest
1608 (try Hashtbl.find
reachable_table (cur
,dir
)
1611 let states = reachsatEF dir m
[cur
] in
1612 Hashtbl.add reachable_table (cur
,dir
) states;
1621 Printf.sprintf
"_c%d" c
1623 (* **************************** *)
1624 (* End of environment functions *)
1625 (* **************************** *)
1627 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1629 let rec satloop unchecked required required_states
1630 ((grp
,label,states) as m
) phi env
=
1631 let rec loop unchecked required required_states phi
=
1632 (*Common.profile_code "satloop" (fun _ -> *)
1636 | A.True
-> triples_top states
1637 | A.Pred
(p
) -> satLabel label required p
1638 | A.Uncheck
(phi1
) ->
1639 let unchecked = if !pUNCHECK_OPT then true else false in
1640 loop unchecked required required_states phi1
1642 let phires = loop unchecked required required_states phi
in
1644 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1645 triples_complement (mkstates states required_states
)
1647 | A.Or
(phi1
,phi2
) ->
1649 (loop unchecked required required_states phi1
)
1650 (loop unchecked required required_states phi2
)
1651 | A.SeqOr
(phi1
,phi2
) ->
1652 let res1 = loop unchecked required required_states phi1
in
1653 let res2 = loop unchecked required required_states phi2
in
1654 let res1neg = unwitify res1 in
1657 (triples_complement (mkstates states required_states
) res1neg)
1659 | A.And
(strict
,phi1
,phi2
) ->
1660 (* phi1 is considered to be more likely to be [], because of the
1661 definition of asttoctl. Could use heuristics such as the size of
1663 let pm = !Flag_ctl.partial_match
in
1664 (match (pm,loop unchecked required required_states phi1
) with
1665 (false,[]) when !pLazyOpt -> []
1667 let new_required = extend_required phi1res required
in
1668 let new_required_states = get_required_states phi1res
in
1669 (match (pm,loop unchecked new_required new_required_states phi2
)
1671 (false,[]) when !pLazyOpt -> []
1673 strict_triples_conj strict
1674 (mkstates states required_states
)
1676 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1677 (* phi2 can appear anywhere that is reachable *)
1678 let pm = !Flag_ctl.partial_match
in
1679 (match (pm,loop unchecked required required_states phi1
) with
1682 let new_required = extend_required phi1res required
in
1683 let new_required_states = get_required_states phi1res
in
1684 let new_required_states =
1685 get_reachable dir m
new_required_states in
1686 (match (pm,loop unchecked new_required new_required_states phi2
)
1688 (false,[]) -> phi1res
1691 [] -> (* !Flag_ctl.partial_match must be true *)
1695 let s = mkstates states required_states
in
1697 (function a
-> function b
->
1698 strict_triples_conj strict
s a
[b
])
1699 [List.hd phi2res
] (List.tl phi2res
)
1702 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1703 let s = mkstates states required_states
in
1705 (function a
-> function b
->
1706 strict_triples_conj strict
s a b
)
1710 "only one result allowed for the left arg of AndAny")))
1711 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1712 (* phi2 can appear anywhere that is reachable *)
1713 let pm = !Flag_ctl.partial_match
in
1714 (match (pm,loop unchecked required required_states phi1
) with
1717 let new_required = extend_required phi1res required
in
1718 let new_required_states = get_required_states phi1res
in
1719 let new_required_states =
1720 get_reachable dir m
new_required_states in
1721 (match (pm,loop unchecked new_required new_required_states phi2
)
1723 (false,[]) -> phi1res
1725 (* if there is more than one state, something about the
1726 environment has to ensure that the right triples of
1727 phi2 get associated with the triples of phi1.
1728 the asttoctl2 has to ensure that that is the case.
1729 these should thus be structural properties.
1730 env of phi2 has to be a proper subset of env of phi1
1731 to ensure all end up being consistent. no new triples
1732 should be generated. strict_triples_conj_none takes
1735 let s = mkstates states required_states
in
1738 function (st
,th
,_
) as phi2_elem
->
1740 triples_complement [st
] [(st
,th
,[])] in
1741 strict_triples_conj_none strict
s acc
1742 (phi2_elem
::inverse))
1744 | A.InnerAnd
(phi
) ->
1745 inner_and(loop unchecked required required_states phi
)
1747 let new_required_states =
1748 get_children_required_states dir m required_states
in
1749 satEX dir m
(loop unchecked required
new_required_states phi
)
1751 | A.AX
(dir
,strict
,phi
) ->
1752 let new_required_states =
1753 get_children_required_states dir m required_states
in
1754 let res = loop unchecked required
new_required_states phi
in
1755 strict_A1 strict
satAX satEX dir m
res required_states
1757 let new_required_states = get_reachable dir m required_states
in
1758 satEF dir m
(loop unchecked required
new_required_states phi
)
1760 | A.AF
(dir
,strict
,phi
) ->
1761 if !Flag_ctl.loop_in_src_code
1763 loop unchecked required required_states
1764 (A.AU
(dir
,strict
,A.True
,phi
))
1766 let new_required_states = get_reachable dir m required_states
in
1767 let res = loop unchecked required
new_required_states phi
in
1768 strict_A1 strict
satAF satEF dir m
res new_required_states
1770 let new_required_states = get_reachable dir m required_states
in
1771 satEG dir m
(loop unchecked required
new_required_states phi
)
1773 | A.AG
(dir
,strict
,phi
) ->
1774 let new_required_states = get_reachable dir m required_states
in
1775 let res = loop unchecked required
new_required_states phi
in
1776 strict_A1 strict
satAG satEF dir m
res new_required_states
1777 | A.EU
(dir
,phi1
,phi2
) ->
1778 let new_required_states = get_reachable dir m required_states
in
1779 (match loop unchecked required
new_required_states phi2
with
1780 [] when !pLazyOpt -> []
1782 let new_required = extend_required s2 required
in
1783 let s1 = loop unchecked new_required new_required_states phi1
in
1784 satEU dir m
s1 s2 new_required_states
1785 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1786 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1787 let new_required_states = get_reachable dir m required_states
in
1788 (match loop unchecked required
new_required_states phi2
with
1789 [] when !pLazyOpt -> []
1791 let new_required = extend_required s2 required
in
1792 let s1 = loop unchecked new_required new_required_states phi1
in
1793 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1794 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1795 (*Printf.printf "using AU\n"; flush stdout;*)
1796 let new_required_states = get_reachable dir m required_states
in
1797 (match loop unchecked required
new_required_states phi2
with
1798 [] when !pLazyOpt -> []
1800 let new_required = extend_required s2 required
in
1801 let s1 = loop unchecked new_required new_required_states phi1
in
1803 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1805 print_graph_c grp
new_required_states y ctr phi
) in
1808 | AUfailed tmp_res
->
1809 (* found a loop, have to try AW *)
1811 A[E[phi1 U phi2] & phi1 W phi2]
1812 the and is nonstrict *)
1813 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1814 (*Printf.printf "using AW\n"; flush stdout;*)
1817 (satEU dir m
s1 tmp_res
new_required_states
1818 (* no graph, for the moment *)
1821 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1823 | A.Implies
(phi1
,phi2
) ->
1824 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1825 | A.Exists
(keep
,v
,phi
) ->
1826 let new_required = drop_required v required
in
1827 triples_witness v
unchecked (not keep
)
1828 (loop unchecked new_required required_states phi
)
1829 | A.Let
(v
,phi1
,phi2
) ->
1830 (* should only be used when the properties unchecked, required,
1831 and required_states are known to be the same or at least
1832 compatible between all the uses. this is not checked. *)
1833 let res = loop unchecked required required_states phi1
in
1834 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1835 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1836 (* should only be used when the properties unchecked, required,
1837 and required_states are known to be the same or at least
1838 compatible between all the uses. this is not checked. *)
1839 (* doesn't seem to be used any more *)
1840 let new_required_states = get_reachable dir m required_states
in
1841 let res = loop unchecked required
new_required_states phi1
in
1842 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1844 let res = List.assoc v env
in
1846 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1848 | A.XX
(phi
) -> failwith
"should have been removed" in
1849 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1850 let res = drop_wits required_states
res phi
(* ) *) in
1851 print_graph grp required_states
res "" phi
;
1854 loop unchecked required required_states phi
1858 (* SAT with tracking *)
1859 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1860 ((_
,label,states) as m
) phi env
=
1861 let anno res children
= (annot lvl phi
res children
,res) in
1862 let satv unchecked required required_states phi0 env
=
1863 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1865 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1866 anno (satloop unchecked required required_states m phi env
) []
1870 A.False
-> anno [] []
1871 | A.True
-> anno (triples_top states) []
1873 Printf.printf
"label\n"; flush stdout
;
1874 anno (satLabel label required p
) []
1875 | A.Uncheck
(phi1
) ->
1876 let unchecked = if !pUNCHECK_OPT then true else false in
1877 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1878 Printf.printf
"uncheck\n"; flush stdout
;
1882 satv unchecked required required_states phi1 env
in
1883 Printf.printf
"not\n"; flush stdout
;
1884 anno (triples_complement (mkstates states required_states
) res) [child
]
1885 | A.Or
(phi1
,phi2
) ->
1887 satv unchecked required required_states phi1 env
in
1889 satv unchecked required required_states phi2 env
in
1890 Printf.printf
"or\n"; flush stdout
;
1891 anno (triples_union res1 res2) [child1
; child2
]
1892 | A.SeqOr
(phi1
,phi2
) ->
1894 satv unchecked required required_states phi1 env
in
1896 satv unchecked required required_states phi2 env
in
1898 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1899 Printf.printf
"seqor\n"; flush stdout
;
1900 anno (triples_union res1
1902 (triples_complement (mkstates states required_states
)
1906 | A.And
(strict
,phi1
,phi2
) ->
1907 let pm = !Flag_ctl.partial_match
in
1908 (match (pm,satv unchecked required required_states phi1 env
) with
1909 (false,(child1
,[])) ->
1910 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1911 | (_
,(child1
,res1)) ->
1912 let new_required = extend_required res1 required
in
1913 let new_required_states = get_required_states res1 in
1914 (match (pm,satv unchecked new_required new_required_states phi2
1916 (false,(child2
,[])) ->
1917 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1918 | (_
,(child2
,res2)) ->
1919 Printf.printf
"and\n"; flush stdout
;
1921 strict_triples_conj strict
1922 (mkstates states required_states
)
1924 anno res [child1
; child2
]))
1925 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1926 let pm = !Flag_ctl.partial_match
in
1927 (match (pm,satv unchecked required required_states phi1 env
) with
1928 (false,(child1
,[])) ->
1929 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1930 | (_
,(child1
,res1)) ->
1931 let new_required = extend_required res1 required
in
1932 let new_required_states = get_required_states res1 in
1933 let new_required_states =
1934 get_reachable dir m
new_required_states in
1935 (match (pm,satv unchecked new_required new_required_states phi2
1937 (false,(child2
,[])) ->
1938 Printf.printf
"andany\n"; flush stdout
;
1939 anno res1 [child1
;child2
]
1940 | (_
,(child2
,res2)) ->
1942 [] -> (* !Flag_ctl.partial_match must be true *)
1944 then anno [] [child1
; child2
]
1947 let s = mkstates states required_states
in
1949 (function a
-> function b
->
1950 strict_triples_conj strict
s a
[b
])
1951 [List.hd
res2] (List.tl
res2) in
1952 anno res [child1
; child2
]
1955 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1956 Printf.printf
"andany\n"; flush stdout
;
1958 let s = mkstates states required_states
in
1960 (function a
-> function b
->
1961 strict_triples_conj strict
s a b
)
1963 anno res [child1
; child2
]
1966 "only one result allowed for the left arg of AndAny")))
1967 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1968 let pm = !Flag_ctl.partial_match
in
1969 (match (pm,satv unchecked required required_states phi1 env
) with
1970 (false,(child1
,[])) ->
1971 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1972 | (_
,(child1
,res1)) ->
1973 let new_required = extend_required res1 required
in
1974 let new_required_states = get_required_states res1 in
1975 let new_required_states =
1976 get_reachable dir m
new_required_states in
1977 (match (pm,satv unchecked new_required new_required_states phi2
1979 (false,(child2
,[])) ->
1980 Printf.printf
"andany\n"; flush stdout
;
1981 anno res1 [child1
;child2
]
1982 | (_
,(child2
,res2)) ->
1984 let s = mkstates states required_states
in
1987 function (st
,th
,_
) as phi2_elem
->
1989 triples_complement [st
] [(st
,th
,[])] in
1990 strict_triples_conj_none strict
s acc
1991 (phi2_elem
::inverse))
1993 anno res [child1
; child2
]))
1994 | A.InnerAnd
(phi1
) ->
1995 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1996 Printf.printf
"uncheck\n"; flush stdout
;
1997 anno (inner_and res1) [child1
]
1999 let new_required_states =
2000 get_children_required_states dir m required_states
in
2002 satv unchecked required
new_required_states phi1 env
in
2003 Printf.printf
"EX\n"; flush stdout
;
2004 anno (satEX dir m
res required_states
) [child
]
2005 | A.AX
(dir
,strict
,phi1
) ->
2006 let new_required_states =
2007 get_children_required_states dir m required_states
in
2009 satv unchecked required
new_required_states phi1 env
in
2010 Printf.printf
"AX\n"; flush stdout
;
2011 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2014 let new_required_states = get_reachable dir m required_states
in
2016 satv unchecked required
new_required_states phi1 env
in
2017 Printf.printf
"EF\n"; flush stdout
;
2018 anno (satEF dir m
res new_required_states) [child
]
2019 | A.AF
(dir
,strict
,phi1
) ->
2020 if !Flag_ctl.loop_in_src_code
2022 satv unchecked required required_states
2023 (A.AU
(dir
,strict
,A.True
,phi1
))
2026 (let new_required_states = get_reachable dir m required_states
in
2028 satv unchecked required
new_required_states phi1 env
in
2029 Printf.printf
"AF\n"; flush stdout
;
2031 strict_A1 strict
satAF satEF dir m
res new_required_states in
2034 let new_required_states = get_reachable dir m required_states
in
2036 satv unchecked required
new_required_states phi1 env
in
2037 Printf.printf
"EG\n"; flush stdout
;
2038 anno (satEG dir m
res new_required_states) [child
]
2039 | A.AG
(dir
,strict
,phi1
) ->
2040 let new_required_states = get_reachable dir m required_states
in
2042 satv unchecked required
new_required_states phi1 env
in
2043 Printf.printf
"AG\n"; flush stdout
;
2044 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2047 | A.EU
(dir
,phi1
,phi2
) ->
2048 let new_required_states = get_reachable dir m required_states
in
2049 (match satv unchecked required
new_required_states phi2 env
with
2051 Printf.printf
"EU\n"; flush stdout
;
2054 let new_required = extend_required res2 required
in
2056 satv unchecked new_required new_required_states phi1 env
in
2057 Printf.printf
"EU\n"; flush stdout
;
2058 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2060 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2061 failwith
"should not be used" (*
2062 let new_required_states = get_reachable dir m required_states in
2063 (match satv unchecked required new_required_states phi2 env with
2065 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2067 let new_required = extend_required res2 required in
2069 satv unchecked new_required new_required_states phi1 env in
2070 Printf.printf "AW %b\n" unchecked; flush stdout;
2072 strict_A2 strict satAW satEF dir m res1 res2
2073 new_required_states in
2074 anno res [child1; child2]) *)
2075 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2076 let new_required_states = get_reachable dir m required_states
in
2077 (match satv unchecked required
new_required_states phi2 env
with
2079 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2081 let new_required = extend_required s2 required
in
2083 satv unchecked new_required new_required_states phi1 env
in
2084 Printf.printf
"AU\n"; flush stdout
;
2086 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2087 (fun y str -> ()) in
2090 anno res [child1
; child2
]
2091 | AUfailed tmp_res
->
2092 (* found a loop, have to try AW *)
2094 A[E[phi1 U phi2] & phi1 W phi2]
2095 the and is nonstrict *)
2096 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2097 Printf.printf
"AW\n"; flush stdout
;
2100 (satEU dir m
s1 tmp_res
new_required_states
2101 (* no graph, for the moment *)
2105 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2106 anno res [child1
; child2
]))
2107 | A.Implies
(phi1
,phi2
) ->
2108 satv unchecked required required_states
2109 (A.Or
(A.Not phi1
,phi2
))
2111 | A.Exists
(keep
,v
,phi1
) ->
2112 let new_required = drop_required v required
in
2114 satv unchecked new_required required_states phi1 env
in
2115 Printf.printf
"exists\n"; flush stdout
;
2116 anno (triples_witness v
unchecked (not keep
) res) [child
]
2117 | A.Let
(v
,phi1
,phi2
) ->
2119 satv unchecked required required_states phi1 env
in
2121 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2122 anno res2 [child1
;child2
]
2123 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2124 let new_required_states = get_reachable dir m required_states
in
2126 satv unchecked required
new_required_states phi1 env
in
2128 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2129 anno res2 [child1
;child2
]
2131 Printf.printf
"Ref\n"; flush stdout
;
2132 let res = List.assoc v env
in
2135 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2138 | A.XX
(phi
) -> failwith
"should have been removed" in
2139 let res1 = drop_wits required_states
res phi
in
2143 print_required_states required_states
;
2144 print_state "after drop_wits" res1 end;
2149 let sat_verbose annotate maxlvl lvl m phi
=
2150 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2152 (* Type for annotations collected in a tree *)
2153 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2155 let sat_annotree annotate m phi
=
2156 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2157 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2161 let sat m phi = satloop m phi []
2165 let simpleanno l phi
res =
2167 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2168 print_generic_algo
(List.sort compare
res);
2169 Format.print_string
"\n------------------------------\n\n" in
2170 let pp_dir = function
2172 | A.BACKWARD
-> pp "^" in
2174 | A.False
-> pp "False"
2175 | A.True
-> pp "True"
2176 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2177 | A.Not
(phi
) -> pp "Not"
2178 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2179 | A.And
(_
,phi1
,phi2
) -> pp "And"
2180 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2181 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2182 | A.Or
(phi1
,phi2
) -> pp "Or"
2183 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2184 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2185 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2186 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2187 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2188 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2189 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2190 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2191 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2192 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2193 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2194 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2195 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2196 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2197 | A.Uncheck
(s) -> pp "Uncheck"
2198 | A.InnerAnd
(s) -> pp "InnerAnd"
2199 | A.XX
(phi1
) -> pp "XX"
2203 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2204 print a ctl formula more accurately if you want.
2205 Use the print_xxx provided in the different module to call
2206 Pretty_print_ctl.pp_ctl.
2209 let simpleanno2 l phi
res =
2211 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2212 Format.print_newline
();
2213 Format.print_string
"----------------------------------------------------";
2214 Format.print_newline
();
2215 print_generic_algo
(List.sort compare
res);
2216 Format.print_newline
();
2217 Format.print_string
"----------------------------------------------------";
2218 Format.print_newline
();
2219 Format.print_newline
();
2223 (* ---------------------------------------------------------------------- *)
2225 (* ---------------------------------------------------------------------- *)
2227 type optentry
= bool ref * string
2228 type options
= {label : optentry
; unch
: optentry
;
2229 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2231 reqenv
: optentry
; reqstates
: optentry
}
2234 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2235 unch
= (pUNCHECK_OPT,"uncheck_opt");
2236 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2237 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2238 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2239 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2240 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2241 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2245 ("label ",[options.label]);
2246 ("unch ",[options.unch
]);
2247 ("unch and label ",[options.label;options.unch
])]
2250 [("conj ", [options.conj]);
2251 ("compl1 ", [options.compl1
]);
2252 ("compl12 ", [options.compl1
;options.compl2
]);
2253 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2254 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2256 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2257 ("compl12 unch satl ",
2258 [options.compl1;options.compl2;options.unch;options.label]); *)
2259 ("conj/compl12 unch satl ",
2260 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2263 [("newinfo ", [options.newinfo
]);
2264 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2267 [("reqenv ", [options.reqenv
]);
2268 ("reqstates ", [options.reqstates
]);
2269 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2270 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2271 ("reqstates unch satl ",
2272 [options.reqstates;options.unch;options.label]);*)
2273 ("reqenv/states unch satl ",
2274 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2277 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2278 options.newinfo
;options.reqenv
;options.reqstates
]
2281 [("all ",all_options)]
2283 let all_options_but_path =
2284 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2285 options.reqenv
;options.reqstates
]
2287 let all_but_path = ("all but path ",all_options_but_path)
2290 [(satAW_calls, "satAW", ref 0);
2291 (satAU_calls, "satAU", ref 0);
2292 (satEF_calls, "satEF", ref 0);
2293 (satAF_calls, "satAF", ref 0);
2294 (satEG_calls, "satEG", ref 0);
2295 (satAG_calls, "satAG", ref 0);
2296 (satEU_calls, "satEU", ref 0)]
2300 (function (opt
,x) ->
2301 (opt
,x,ref 0.0,ref 0,
2302 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2303 [List.hd
all;all_but_path]
2304 (*(all@baseline@conjneg@path@required)*)
2308 let rec iter fn = function
2310 | n
-> let _ = fn() in
2311 (Hashtbl.clear
reachable_table;
2312 Hashtbl.clear
memo_label;
2316 let copy_to_stderr fl
=
2317 let i = open_in fl
in
2319 Printf.fprintf stderr
"%s\n" (input_line
i);
2321 try loop() with _ -> ();
2324 let bench_sat (_,_,states) fn =
2325 List.iter (function (opt
,_) -> opt
:= false) all_options;
2328 (function (name
,options,time
,trips,counter_info
) ->
2329 let iterct = !Flag_ctl.bench
in
2330 if !time
> float_of_int
timeout then time
:= -100.0;
2331 if not
(!time
= -100.0)
2334 Hashtbl.clear
reachable_table;
2335 Hashtbl.clear
memo_label;
2336 List.iter (function (opt
,_) -> opt
:= true) options;
2337 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2341 let bef = Sys.time
() in
2343 Common.timeout_function
timeout
2345 let bef = Sys.time
() in
2346 let res = iter fn iterct in
2347 let aft = Sys.time
() in
2348 time
:= !time
+. (aft -. bef);
2349 trips := !trips + !triples;
2351 (function (calls
,_,save_calls
) ->
2352 function (current_calls
,current_cfg
,current_max_cfg
) ->
2354 !current_calls
+ (!calls
- !save_calls
);
2355 if (!calls
- !save_calls
) > 0
2357 (let st = List.length
states in
2358 current_cfg
:= !current_cfg
+ st;
2359 if st > !current_max_cfg
2360 then current_max_cfg
:= st))
2361 counters counter_info
;
2366 let aft = Sys.time
() in
2368 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2372 List.iter (function (opt
,_) -> opt
:= false) options;
2377 Printf.fprintf stderr
"\n";
2381 (if not
(List.for_all
(function x -> x = res) rest
)
2383 (List.iter (print_state "a state") answers;
2384 Printf.printf
"something doesn't work\n");
2388 let iterct = !Flag_ctl.bench
in
2392 (function (name
,options,time
,trips,counter_info
) ->
2393 Printf.fprintf stderr
"%s Numbers: %f %d "
2394 name
(!time
/. (float_of_int
iterct)) !trips;
2396 (function (calls
,cfg
,max_cfg
) ->
2397 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2399 Printf.fprintf stderr
"\n")
2402 (* ---------------------------------------------------------------------- *)
2403 (* preprocessing: ignore irrelevant functions *)
2405 let preprocess (cfg
,_,_) label = function
2406 [] -> true (* no information, try everything *)
2408 let sz = G.size cfg
in
2409 let verbose_output pred = function
2411 Printf.printf
"did not find:\n";
2412 P.print_predicate
pred; Format.print_newline
()
2414 Printf.printf
"found:\n";
2415 P.print_predicate
pred; Format.print_newline
();
2416 Printf.printf
"but it was not enough\n" in
2417 let get_any verbose
x =
2419 try Hashtbl.find
memo_label x
2422 (let triples = label x in
2424 List.map (function (st,th
,_) -> (st,th
)) triples in
2425 Hashtbl.add memo_label x filtered;
2427 if verbose
then verbose_output x res;
2430 (* don't bother testing when there are more patterns than nodes *)
2431 if List.length l
> sz-2
2433 else List.for_all
(get_any false) l
in
2434 if List.exists
get_all l
2437 (if !Flag_ctl.verbose_match
2439 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2443 let filter_partial_matches trips =
2444 if !Flag_ctl.partial_match
2446 let anynegwit = (* if any is neg, then all are *)
2447 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2449 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2452 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2456 (* ---------------------------------------------------------------------- *)
2457 (* Main entry point for engine *)
2458 let sat m phi reqopt
=
2460 (match !Flag_ctl.steps
with
2461 None
-> step_count := 0
2462 | Some
x -> step_count := x);
2463 Hashtbl.clear
reachable_table;
2464 Hashtbl.clear
memo_label;
2465 let (x,label,states) = m
in
2466 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2468 ((* to drop when Yoann initialized this flag *)
2469 if List.exists
(G.extract_is_loop
x) states
2470 then Flag_ctl.loop_in_src_code
:= true;
2471 let m = (x,label,List.sort compare
states) in
2473 if(!Flag_ctl.verbose_ctl_engine
)
2475 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2476 if !Flag_ctl.bench
> 0
2480 let fn _ = satloop false [] None
m phi
[] in
2481 if !Flag_ctl.bench
> 0
2483 else Common.profile_code
"ctl" (fun _ -> fn()) in
2484 let res = filter_partial_matches res in
2486 Printf.printf "steps: start %d, stop %d\n"
2487 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2489 Printf.printf "triples: %d\n" !triples;
2490 print_state "final result" res;
2492 List.sort compare
res)
2494 (if !Flag_ctl.verbose_ctl_engine
2495 then Common.pr2
"missing something required";
2500 (* ********************************************************************** *)
2501 (* End of Module: CTL_ENGINE *)
2502 (* ********************************************************************** *)