2 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
23 (*external c_counter : unit -> int = "c_counter"*)
25 (* Optimize triples_conj by first extracting the intersection of the two sets,
26 which can certainly be in the intersection *)
27 let pTRIPLES_CONJ_OPT = ref true
28 (* For complement, make NegState for the negation of a single state *)
29 let pTRIPLES_COMPLEMENT_OPT = ref true
30 (* For complement, do something special for the case where the environment
31 and witnesses are empty *)
32 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
33 (* "Double negate" the arguments of the path operators *)
34 let pDOUBLE_NEGATE_OPT = ref true
35 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
36 let pNEW_INFO_OPT = ref true
37 (* Filter the result of the label function to drop entries that aren't
38 compatible with any of the available environments *)
39 let pREQUIRED_ENV_OPT = ref true
40 (* Memoize the raw result of the label function *)
41 let pSATLABEL_MEMO_OPT = ref true
42 (* Filter results according to the required states *)
43 let pREQUIRED_STATES_OPT = ref true
44 (* Drop negative witnesses at Uncheck *)
45 let pUNCHECK_OPT = ref true
46 let pANY_NEG_OPT = ref true
47 let pLazyOpt = ref true
49 (* Nico: This stack is use for graphical traces *)
50 let graph_stack = ref ([] : string list
)
51 let graph_hash = (Hashtbl.create
101)
54 let pTRIPLES_CONJ_OPT = ref false
55 let pTRIPLES_COMPLEMENT_OPT = ref false
56 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
57 let pDOUBLE_NEGATE_OPT = ref false
58 let pNEW_INFO_OPT = ref false
59 let pREQUIRED_ENV_OPT = ref false
60 let pSATLABEL_MEMO_OPT = ref false
61 let pREQUIRED_STATES_OPT = ref false
62 let pUNCHECK_OPT = ref false
63 let pANY_NEG_OPT = ref false
64 let pLazyOpt = ref false
68 let step_count = ref 0
71 if not
(!step_count = 0)
74 step_count := !step_count - 1;
75 if !step_count = 0 then raise Steps
78 let inc cell
= cell
:= !cell
+ 1
80 let satEU_calls = ref 0
81 let satAW_calls = ref 0
82 let satAU_calls = ref 0
83 let satEF_calls = ref 0
84 let satAF_calls = ref 0
85 let satEG_calls = ref 0
86 let satAG_calls = ref 0
94 Printf.sprintf
"_fresh_r_%d" c
96 (* **********************************************************************
98 * Implementation of a Witness Tree model checking engine for CTL-FVex
101 * **********************************************************************)
103 (* ********************************************************************** *)
104 (* Module: SUBST (substitutions: meta. vars and values) *)
105 (* ********************************************************************** *)
111 val eq_mvar
: mvar
-> mvar
-> bool
112 val eq_val
: value -> value -> bool
113 val merge_val
: value -> value -> value
114 val print_mvar
: mvar
-> unit
115 val print_value
: value -> unit
119 (* ********************************************************************** *)
120 (* Module: GRAPH (control flow graphs / model) *)
121 (* ********************************************************************** *)
127 val predecessors
: cfg
-> node
-> node list
128 val successors
: cfg
-> node
-> node list
129 val extract_is_loop
: cfg
-> node
-> bool
130 val print_node
: node
-> unit
131 val size
: cfg
-> int
132 val print_graph
: cfg
-> string option ->
133 (node
* string) list
-> (node
* string) list
-> string -> unit
137 module OGRAPHEXT_GRAPH
=
140 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
141 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
142 let print_node i
= Format.print_string
(Common.i_to_s i
)
146 (* ********************************************************************** *)
147 (* Module: PREDICATE (predicates for CTL formulae) *)
148 (* ********************************************************************** *)
150 module type PREDICATE
=
153 val print_predicate
: t
-> unit
157 (* ********************************************************************** *)
159 (* ---------------------------------------------------------------------- *)
160 (* Misc. useful generic functions *)
161 (* ---------------------------------------------------------------------- *)
163 let get_graph_files () = !graph_stack
164 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
174 let foldl = List.fold_left
;;
176 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
178 type 'a esc
= ESC
of 'a
| CONT
of 'a
180 let foldr = List.fold_right
;;
182 let concat = List.concat;;
186 let filter = List.filter;;
188 let partition = List.partition;;
190 let concatmap f l
= List.concat (List.map f l
);;
198 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
200 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
202 let rec some_tolist opts
=
205 | (Some x
)::rest
-> x
::(some_tolist rest
)
206 | _
::rest
-> some_tolist rest
209 let rec groupBy eq l
=
213 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
214 (x
::xs1
)::(groupBy eq xs2
)
217 let group l
= groupBy (=) l
;;
219 let rec memBy eq x l
=
222 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
225 let rec nubBy eq ls
=
228 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
229 | (x
::xs
) -> x
::(nubBy eq xs
)
235 | (x
::xs
) when (List.mem x xs
) -> nub xs
236 | (x
::xs
) -> x
::(nub xs
)
239 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
241 let setifyBy eq xs
= nubBy eq xs
;;
243 let setify xs
= nub xs
;;
245 let inner_setify xs
= List.sort compare
(nub xs
);;
247 let unionBy compare eq xs
= function
250 let rec loop = function
252 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
253 List.sort compare
(loop xs
)
256 let union xs ys
= unionBy state_compare (=) xs ys
;;
258 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
260 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
262 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
263 let supseteq xs ys
= subseteq ys xs
265 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
267 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
269 (* Fix point calculation *)
271 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
274 (* Fix point calculation on set-valued functions *)
275 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
276 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
278 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
280 (* ********************************************************************** *)
281 (* Module: CTL_ENGINE *)
282 (* ********************************************************************** *)
285 functor (SUB
: SUBST
) ->
286 functor (G
: GRAPH
) ->
287 functor (P
: PREDICATE
) ->
292 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
294 type ('pred
,'anno
) witness
=
295 (G.node
, substitution
,
296 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
297 Ast_ctl.generic_witnesstree
299 type ('pred
,'anno
) triples =
300 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
302 (* ---------------------------------------------------------------------- *)
303 (* Pretty printing functions *)
304 (* ---------------------------------------------------------------------- *)
306 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
307 let print_generic_subst = function
309 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
310 | A.NegSubst
(mvar
, v
) ->
311 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
312 Format.print_string
"[";
313 Common.print_between
(fun () -> Format.print_string
";" )
314 print_generic_subst substxs
;
315 Format.print_string
"]"
317 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
319 | A.Wit
(state
, subst
, anno
, childrens
) ->
320 Format.print_string
"wit ";
322 print_generic_substitution subst
;
323 (match childrens
with
324 [] -> Format.print_string
"{}"
326 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
327 print_generic_witnesstree childrens
; Format.close_box
())
329 Format.print_string
"!";
330 print_generic_witness wit
332 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
335 Format.print_string
"{";
337 (fun () -> Format.print_string
";"; Format.force_newline
() )
338 print_generic_witness witnesstree
;
339 Format.print_string
"}";
342 and print_generic_triple
(node
,subst
,tree
) =
344 print_generic_substitution subst
;
345 print_generic_witnesstree tree
347 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
348 Format.print_string
"<";
350 (fun () -> Format.print_string
";"; Format.force_newline
())
351 print_generic_triple xs
;
352 Format.print_string
">"
355 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
356 Printf.printf
"%s\n" str
;
357 List.iter
(function x ->
358 print_generic_triple
x; Format.print_newline
(); flush stdout
)
359 (List.sort compare l
);
362 let print_required_states = function
363 None
-> Printf.printf
"no required states\n"
365 Printf.printf
"required states: ";
368 G.print_node x; Format.print_string
" "; Format.print_flush
())
372 let mkstates states
= function
374 | Some states
-> states
376 let print_graph grp required_states res str
= function
377 A.Exists
(keep
,v
,phi
) -> ()
379 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
382 | A.Exists
(keep
,v
,phi
) -> ()
385 Printf.sprintf
"%s%s"
387 (Common.format_to_string
389 Pretty_print_ctl.pp_ctl
390 (P.print_predicate
, SUB.print_mvar
)
393 let file = (match !Flag.currentfile
with
394 None
-> "graphical_trace"
397 (if not
(List.mem
file !graph_stack) then
398 graph_stack := file :: !graph_stack);
399 let filename = Filename.temp_file
(file^
":") ".dot" in
400 Hashtbl.add
graph_hash file filename;
402 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
403 (match required_states
with
405 | Some required_states
->
406 (List.map (function s
-> (s
,"blue")) required_states
))
407 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
409 let print_graph_c grp required_states res
ctr phi
=
410 let str = "iter: "^
(string_of_int
!ctr) in
411 print_graph grp required_states res
str phi
413 (* ---------------------------------------------------------------------- *)
415 (* ---------------------------------------------------------------------- *)
418 (* ************************* *)
420 (* ************************* *)
425 | A.NegSubst
(x,_
) -> x
431 | A.NegSubst
(_
,x) -> x
434 let eq_subBy eqx eqv sub sub'
=
435 match (sub
,sub'
) with
436 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
437 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
442 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
444 let eq_subst th th'
= setequalBy eq_sub th th'
;;
446 let merge_subBy eqx
(===) (>+<) sub sub'
=
447 (* variable part is guaranteed to be the same *)
448 match (sub
,sub'
) with
449 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
451 then Some
[A.Subst
(x, v
>+< v'
)]
453 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
455 then Some
[A.Subst
(x'
,v'
)]
457 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
459 then Some
[A.Subst
(x,v
)]
461 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
464 let merged = v
>+< v'
in
465 if merged = v
&& merged = v'
466 then Some
[A.NegSubst
(x,v
>+< v'
)]
468 (* positions are compatible, but not identical. keep apart. *)
469 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
470 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
474 let merge_sub sub sub'
=
475 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
477 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
479 (* NOTE: we sort by using the generic "compare" on (meta-)variable
480 * names; we could also require a definition of compare for meta-variables
481 * or substitutions but that seems like overkill for sorting
483 let clean_subst theta
=
487 let res = compare
(dom_sub s
) (dom_sub s'
) in
491 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
492 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
493 | _
-> compare
(ran_sub s
) (ran_sub s'
)
496 let rec loop = function
498 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
499 loop (A.Subst
(x,v
)::rest
)
500 | x::xs
-> x::(loop xs
) in
503 let top_subst = [];; (* Always TRUE subst. *)
505 (* Split a theta in two parts: one with (only) "x" and one without *)
507 let split_subst theta
x =
508 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
510 exception SUBST_MISMATCH
511 let conj_subst theta theta'
=
512 match (theta
,theta'
) with
513 | ([],_
) -> Some theta'
514 | (_
,[]) -> Some theta
516 let rec classify = function
518 | [x] -> [(dom_sub x,[x])]
520 (match classify xs
with
521 ((nm
,y
)::ys
) as res ->
524 else (dom_sub x,[x])::res
525 | _
-> failwith
"not possible") in
526 let merge_all theta theta'
=
533 match (merge_sub sub sub'
) with
534 Some subs
-> subs
@ rest
535 | _
-> raise SUBST_MISMATCH
)
538 let rec loop = function
540 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
542 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
543 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
544 (match compare
x y
with
545 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
546 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
547 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
548 | _
-> failwith
"not possible") in
549 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
550 with SUBST_MISMATCH
-> None
553 (* theta' must be a subset of theta *)
554 let conj_subst_none theta theta'
=
555 match (theta
,theta'
) with
556 | (_
,[]) -> Some theta
559 let rec classify = function
561 | [x] -> [(dom_sub x,[x])]
563 (match classify xs
with
564 ((nm
,y
)::ys
) as res ->
567 else (dom_sub x,[x])::res
568 | _
-> failwith
"not possible") in
569 let merge_all theta theta'
=
576 match (merge_sub sub sub'
) with
577 Some subs
-> subs
@ rest
578 | _
-> raise SUBST_MISMATCH
)
581 let rec loop = function
583 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
584 | ([],ctheta'
) -> raise SUBST_MISMATCH
585 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
586 (match compare
x y
with
587 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
588 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
589 | 1 -> raise SUBST_MISMATCH
590 | _
-> failwith
"not possible") in
591 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
592 with SUBST_MISMATCH
-> None
597 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
598 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
601 (* Turn a (big) theta into a list of (small) thetas *)
602 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
605 (* ************************* *)
607 (* ************************* *)
609 (* Always TRUE witness *)
610 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
612 let eq_wit wit wit'
= wit
= wit'
;;
614 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
615 let res = unionBy compare
(=) wit wit'
in
616 let anynegwit = (* if any is neg, then all are *)
617 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
619 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
622 let negate_wit wit
= A.NegWit wit
(*
624 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
625 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
628 let negate_wits wits
=
629 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
632 let anynegwit = (* if any is neg, then all are *)
633 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
637 function (s
,th
,wit
) ->
638 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
641 (* ************************* *)
643 (* ************************* *)
645 (* Triples are equal when the constituents are equal *)
646 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
647 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
649 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
651 let normalize trips
=
653 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
657 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
658 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
659 let triples_conj trips trips'
=
660 let (trips
,shared
,trips'
) =
661 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
664 List.partition (function t
-> List.mem t trips'
) trips
in
666 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
667 (trips,shared
,trips'
)
668 else (trips,[],trips'
) in
669 foldl (* returns a set - setify inlined *)
671 function (s1
,th1
,wit1
) ->
674 function (s2
,th2
,wit2
) ->
676 (match (conj_subst th1 th2
) with
678 let t = (s1
,th
,union_wit wit1 wit2
) in
679 if List.mem
t rest
then rest
else t::rest
686 (* ignore the state in the right argument. always pretend it is the same as
688 (* env on right has to be a subset of env on left *)
689 let triples_conj_none trips trips'
=
690 let (trips,shared
,trips'
) =
691 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
694 List.partition (function t -> List.mem
t trips'
) trips in
696 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
697 (trips,shared
,trips'
)
698 else (trips,[],trips'
) in
699 foldl (* returns a set - setify inlined *)
701 function (s1
,th1
,wit1
) ->
704 function (s2
,th2
,wit2
) ->
705 match (conj_subst_none th1 th2
) with
707 let t = (s1
,th
,union_wit wit1 wit2
) in
708 if List.mem
t rest
then rest
else t::rest
716 let triples_conj_AW trips trips'
=
717 let (trips,shared
,trips'
) =
718 if false && !pTRIPLES_CONJ_OPT
721 List.partition (function t -> List.mem
t trips'
) trips in
723 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
724 (trips,shared
,trips'
)
725 else (trips,[],trips'
) in
726 foldl (* returns a set - setify inlined *)
728 function (s1
,th1
,wit1
) ->
731 function (s2
,th2
,wit2
) ->
733 (match (conj_subst th1 th2
) with
735 let t = (s1
,th
,union_wit wit1 wit2
) in
736 if List.mem
t rest
then rest
else t::rest
743 (* *************************** *)
744 (* NEGATION (NegState style) *)
745 (* *************************** *)
747 (* Constructive negation at the state level *)
750 | NegState
of 'a list
753 let compatible_states = function
754 (PosState s1
, PosState s2
) ->
755 if s1
= s2
then Some
(PosState s1
) else None
756 | (PosState s1
, NegState s2
) ->
757 if List.mem s1 s2
then None
else Some
(PosState s1
)
758 | (NegState s1
, PosState s2
) ->
759 if List.mem s2 s1
then None
else Some
(PosState s2
)
760 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
763 (* Conjunction on triples with "special states" *)
764 let triples_state_conj trips trips'
=
765 let (trips,shared
,trips'
) =
766 if !pTRIPLES_CONJ_OPT
769 List.partition (function t -> List.mem
t trips'
) trips in
771 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
772 (trips,shared
,trips'
)
773 else (trips,[],trips'
) in
776 function (s1
,th1
,wit1
) ->
779 function (s2
,th2
,wit2
) ->
780 match compatible_states(s1
,s2
) with
782 (match (conj_subst th1 th2
) with
784 let t = (s
,th
,union_wit wit1 wit2
) in
785 if List.mem
t rest
then rest
else t::rest
792 let triple_negate (s
,th
,wits
) =
793 let negstates = (NegState
[s
],top_subst,top_wit) in
794 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
795 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
796 negstates :: (negths @ negwits) (* all different *)
798 (* FIX ME: it is not necessary to do full conjunction *)
799 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
800 if !pTRIPLES_COMPLEMENT_OPT
802 (let cleanup (s
,th
,wit
) =
804 PosState s'
-> [(s'
,th
,wit
)]
806 assert (th
=top_subst);
807 assert (wit
=top_wit);
808 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
809 let (simple
,complex
) =
810 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
812 let (simple
,complex
) =
813 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
815 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
816 top_subst,top_wit)] in
818 else ([(NegState
[],top_subst,top_wit)],trips) in
819 let rec compl trips =
822 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
823 let compld = (compl complex
) in
824 let compld = concatmap cleanup compld in
827 let negstates (st
,th
,wits
) =
828 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
829 let negths (st
,th
,wits
) =
830 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
831 let negwits (st
,th
,wits
) =
832 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
834 [] -> map (function st
-> (st
,top_subst,top_wit)) states
840 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
841 (negstates x @ negths x @ negwits x) xs
)
844 let triple_negate (s
,th
,wits
) =
845 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
846 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
847 ([s
], negths @ negwits) (* all different *)
849 let print_compl_state str (n
,p
) =
850 Printf.printf
"%s neg: " str;
852 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
857 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
859 then map (function st
-> (st
,top_subst,top_wit)) states
861 let cleanup (neg
,pos
) =
863 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
864 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
866 let trips = List.sort
state_compare trips in
867 let all_negated = List.map triple_negate trips in
868 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
869 let (pos1conj
,pos1keep
) =
870 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
871 let (pos2conj
,pos2keep
) =
872 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
873 (Common.union_set neg1 neg2
,
874 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
875 let rec inner_loop = function
876 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
878 let rec outer_loop = function
880 | l
-> outer_loop (inner_loop l
) in
881 cleanup (outer_loop all_negated)
883 (* ********************************** *)
884 (* END OF NEGATION (NegState style) *)
885 (* ********************************** *)
887 (* now this is always true, so we could get rid of it *)
888 let something_dropped = ref true
890 let triples_union trips trips'
=
891 (*unionBy compare eq_trip trips trips';;*)
892 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
894 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
895 Then, the following says that since the first is a more restrictive
896 environment and has fewer witnesses, then it should be dropped. But having
897 fewer witnesses is not necessarily less informative than having more,
898 because fewer witnesses can mean the absence of the witness-causing thing.
899 So the fewer witnesses have to be kept around.
900 subseteq changed to = to make it hopefully work
905 something_dropped := false;
907 then (something_dropped := true; trips)
909 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
912 (match conj_subst th1 th2
with
915 then if (*subseteq*) wit1
= wit2
then 1 else 0
918 then if (*subseteq*) wit2
= wit1
then (-1) else 0
922 let rec first_loop second
= function
924 | x::xs
-> first_loop (second_loop
x second
) xs
925 and second_loop
x = function
928 match subsumes x y
with
929 1 -> something_dropped := true; all
930 | (-1) -> second_loop
x ys
931 | _
-> y
::(second_loop
x ys
) in
932 first_loop trips trips'
934 else unionBy compare
eq_trip trips trips'
937 let triples_witness x unchecked not_keep
trips =
938 let anyneg = (* if any is neg, then all are *)
939 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
940 let anynegwit = (* if any is neg, then all are *)
941 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
942 let allnegwit = (* if any is neg, then all are *)
943 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
945 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
949 function (s
,th
,wit
) as t ->
950 let (th_x
,newth
) = split_subst th
x in
953 (* one consider whether if not not_keep is true, then we should
954 fail. but it could be that the variable is a used_after and
955 then it is the later rule that should fail and not this one *)
956 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
958 (SUB.print_mvar
x; Format.print_flush
();
959 print_state ": empty witness from" [t]);
961 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
962 (* see tests/nestseq for how neg bindings can come up even
963 without eg partial matches
964 (* negated substitution only allowed with negwits.
966 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
969 (print_generic_substitution l
; Format.print_newline
();
970 failwith
"unexpected negative binding with positive witnesses")*)
973 if unchecked
or not_keep
976 if anynegwit wit
&& allnegwit wit
977 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
978 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
981 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
987 (* ---------------------------------------------------------------------- *)
988 (* SAT - Model Checking Algorithm for CTL-FVex *)
990 (* TODO: Implement _all_ operators (directly) *)
991 (* ---------------------------------------------------------------------- *)
994 (* ************************************* *)
995 (* The SAT algorithm and special helpers *)
996 (* ************************************* *)
998 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1000 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1001 let exp (s
,th
,wit
) =
1003 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1005 A.FORWARD
-> G.predecessors grp s
1006 | A.BACKWARD
-> G.successors grp s
) in
1007 setify (concatmap exp y
)
1012 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1015 None
-> true | Some reqst
-> List.mem s reqst
in
1018 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1021 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1024 (function p
-> (p
,succ grp p
))
1027 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1028 (* would a hash table be more efficient? *)
1029 let all = List.sort
state_compare all in
1030 let rec up_nodes child s
= function
1032 | (s1
,th
,wit
)::xs
->
1033 (match compare s1 child
with
1034 -1 -> up_nodes child s xs
1035 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1037 let neighbor_triples =
1040 function (s
,children
) ->
1044 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1048 match neighbor_triples with
1052 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1054 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1057 None
-> true | Some reqst
-> List.mem s reqst
in
1060 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1063 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1066 (function p
-> (p
,succ grp p
))
1069 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1070 (* would a hash table be more efficient? *)
1071 let all = List.sort
state_compare all in
1072 let rec up_nodes child s
= function
1074 | (s1
,th
,wit
)::xs
->
1075 (match compare s1 child
with
1076 -1 -> up_nodes child s xs
1077 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1079 let neighbor_triples =
1082 function (s
,children
) ->
1085 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1088 match neighbor_triples with
1090 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1092 (* drop_negwits will call setify *)
1093 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1095 let satAX dir m s reqst
= pre_forall dir m s s reqst
1098 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1099 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1100 (*Printf.printf "EU\n";
1101 let ctr = ref 0 in*)
1106 (*let ctr = ref 0 in*)
1109 let rec f y new_info
=
1115 print_graph y ctr;*)
1116 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1117 let res = triples_union first y
in
1118 let new_info = setdiff res y
in
1119 (*Printf.printf "iter %d res %d new_info %d\n"
1120 !ctr (List.length res) (List.length new_info);
1121 print_state "res" res;
1122 print_state "new_info" new_info;
1130 print_graph y ctr;*)
1131 let pre = pre_exist dir m y reqst
in
1132 triples_union s2
(triples_conj s1
pre) in
1136 (* EF phi == E[true U phi] *)
1137 let satEF dir m s2 reqst
=
1139 (*let ctr = ref 0 in*)
1142 let rec f y
new_info =
1148 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1149 let first = pre_exist dir m
new_info reqst
in
1150 let res = triples_union first y
in
1151 let new_info = setdiff res y
in
1152 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1153 (if dir = A.BACKWARD then "reachable" else "real ef")
1154 !ctr (List.length res) (List.length new_info);
1155 print_state "new info" new_info;
1162 let pre = pre_exist dir m y reqst
in
1163 triples_union s2
pre in
1167 type ('
pred,'anno
) auok
=
1168 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1170 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1171 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1177 (*let ctr = ref 0 in*)
1179 if !Flag_ctl.loop_in_src_code
1184 let rec f y newinfo
=
1190 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1194 try Some
(pre_forall dir m
new_info y reqst
)
1199 match triples_conj s1
pre with
1202 (*print_state "s1" s1;
1203 print_state "pre" pre;
1204 print_state "first" first;*)
1205 let res = triples_union first y
in
1207 if not
!something_dropped
1209 else setdiff res y
in
1211 "iter %d res %d new_info %d\n"
1212 !ctr (List.length res) (List.length new_info);
1217 if !Flag_ctl.loop_in_src_code
1221 fix (function s1 -> function s2 ->
1222 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1223 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1224 subseteq s1 s2) in for popl *)
1229 let pre = pre_forall dir m y y reqst
in
1230 triples_union s2 (triples_conj s1 pre) in
1235 (* reqst could be the states of s1 *)
1237 let lstates = mkstates states reqst in
1238 let initial_removed =
1239 triples_complement lstates (triples_union s1 s2) in
1240 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1241 let rec loop base removed =
1243 triples_conj base (pre_exist dir m removed reqst) in
1245 triples_conj base (triples_complement lstates new_removed) in
1246 if supseteq new_base base
1247 then triples_union base s2
1248 else loop new_base new_removed in
1249 loop initial_base initial_removed *)
1251 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1257 This works extremely badly when the region is small and the end of the
1258 region is very ambiguous, eg free(x) ... x
1262 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1263 let ostates = Common.union_set (get_states s1) (get_states s2) in
1266 A.FORWARD -> G.successors grp
1267 | A.BACKWARD -> G.predecessors grp) in
1269 List.fold_left Common.union_set ostates (List.map succ ostates) in
1270 let negphi = triples_complement states s1 in
1271 let negpsi = triples_complement states s2 in
1272 triples_complement ostates
1273 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1276 (*let ctr = ref 0 in*)
1280 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1283 let pre = pre_forall dir m y y reqst
in
1284 (*print_state "pre" pre;*)
1285 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1286 triples_union s2 conj in
1287 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1288 (* drop wits on s1 represents that we don't want any witnesses from
1289 the case that infinitely loops, only from the case that gets
1290 out of the loop. s1 is like a guard. To see the problem, consider
1291 an example where both s1 and s2 match some code after the loop.
1292 we only want the witness from s2. *)
1293 setgfix f (triples_union (drop_wits s1) s2)
1296 let satAF dir m s reqst
=
1300 let rec f y newinfo
=
1305 let first = pre_forall dir m
new_info y reqst
in
1306 let res = triples_union first y
in
1307 let new_info = setdiff res y
in
1313 let pre = pre_forall dir m y y reqst
in
1314 triples_union s
pre in
1317 let satAG dir
((_
,_
,states) as m
) s reqst
=
1321 let pre = pre_forall dir m y y reqst
in
1322 triples_conj y
pre in
1325 let satEG dir
((_
,_
,states) as m
) s reqst
=
1329 let pre = pre_exist dir m y reqst
in
1330 triples_conj y
pre in
1333 (* **************************************************************** *)
1334 (* Inner And - a way of dealing with multiple matches within a node *)
1335 (* **************************************************************** *)
1336 (* applied to the result of matching a node. collect witnesses when the
1337 states and environments are the same *)
1339 let inner_and trips =
1340 let rec loop = function
1342 | (s
,th
,w
)::trips ->
1343 let (cur
,acc
) = loop trips in
1345 (s'
,_
,_
)::_
when s
= s'
->
1346 let rec loop'
= function
1348 | ((_
,th'
,w'
) as t'
)::ts'
->
1349 (match conj_subst th th'
with
1350 Some th''
-> (s
,th''
,union_wit w w'
)::ts'
1351 | None
-> t'
::(loop' ts'
)) in
1353 | _
-> ([(s
,th
,w
)],cur
@acc
)) in
1355 loop (List.sort
state_compare trips) (* is this sort needed? *) in
1358 (* *************** *)
1359 (* Partial matches *)
1360 (* *************** *)
1362 let filter_conj states unwanted partial_matches
=
1364 triples_conj (triples_complement states (unwitify unwanted
))
1366 triples_conj (unwitify x) (triples_complement states x)
1368 let strict_triples_conj strict
states trips trips'
=
1369 let res = triples_conj trips trips'
in
1370 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1372 let fail_left = filter_conj states trips trips'
in
1373 let fail_right = filter_conj states trips'
trips in
1374 let ors = triples_union fail_left fail_right in
1375 triples_union res ors
1378 let strict_triples_conj_none strict
states trips trips'
=
1379 let res = triples_conj_none trips trips'
in
1380 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1382 let fail_left = filter_conj states trips trips'
in
1383 let fail_right = filter_conj states trips'
trips in
1384 let ors = triples_union fail_left fail_right in
1385 triples_union res ors
1388 let left_strict_triples_conj strict
states trips trips'
=
1389 let res = triples_conj trips trips'
in
1390 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1392 let fail_left = filter_conj states trips trips'
in
1393 triples_union res fail_left
1396 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1397 let res = op dir m
trips required_states
in
1398 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1400 let states = mkstates states required_states
in
1401 let fail = filter_conj states res (failop dir m
trips required_states
) in
1402 triples_union res fail
1405 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1407 let res = op dir m
trips trips' required_states
in
1408 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1410 let states = mkstates states required_states
in
1411 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1412 triples_union res fail
1415 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1416 required_states
print_graph =
1417 match op dir m
trips trips' required_states
print_graph with
1419 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1421 let states = mkstates states required_states
in
1423 filter_conj states res (failop dir m
trips' required_states
) in
1424 AUok
(triples_union res fail)
1426 | AUfailed
res -> AUfailed
res
1428 (* ********************* *)
1429 (* Environment functions *)
1430 (* ********************* *)
1432 let drop_wits required_states s phi
=
1433 match required_states
with
1435 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1438 let print_required required
=
1441 Format.print_string
"{";
1444 print_generic_substitution reqd
; Format.print_newline
())
1446 Format.print_string
"}";
1447 Format.print_newline
())
1452 let extend_required trips required
=
1453 if !Flag_ctl.partial_match
1456 if !pREQUIRED_ENV_OPT
1462 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1464 let envs = if List.mem
[] envs then [] else envs in
1465 match (envs,required
) with
1469 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1474 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1481 match conj_subst t r
with
1482 None
-> rest
| Some th
-> add th rest
)
1486 with Too_long
-> envs :: required
)
1487 | (envs,_
) -> envs :: required
1490 let drop_required v required
=
1491 if !pREQUIRED_ENV_OPT
1498 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1500 (* check whether an entry has become useless *)
1501 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1504 (* no idea how to write this function ... *)
1506 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1508 let satLabel label required p
=
1510 if !pSATLABEL_MEMO_OPT
1513 let states_subs = Hashtbl.find
memo_label p
in
1514 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1517 let triples = setify(label p
) in
1518 Hashtbl.add memo_label p
1519 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1521 else setify(label p
) in
1523 (if !pREQUIRED_ENV_OPT
1527 function ((s
,th
,_
) as t) ->
1529 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1536 let get_required_states l
=
1537 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1539 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1542 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1543 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1545 match required_states
with
1550 A.FORWARD
-> G.successors
1551 | A.BACKWARD
-> G.predecessors in
1552 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1555 let reachable_table =
1556 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1558 (* like satEF, but specialized for get_reachable *)
1559 let reachsatEF dir
(grp
,_
,_
) s2 =
1561 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1562 let union = unionBy compare
(=) in
1563 let rec f y
= function
1566 let (pre_collected
,new_info) =
1567 List.partition (function Common.Left
x -> true | _
-> false)
1570 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1571 with Not_found
-> Common.Right
x)
1576 function Common.Left
x -> union x rest
1577 | _
-> failwith
"not possible")
1581 (function Common.Right
x -> x | _
-> failwith
"not possible")
1583 let first = inner_setify (concatmap (dirop grp
) new_info) in
1584 let new_info = setdiff first y in
1585 let res = new_info @ y in
1587 List.rev
(f s2 s2) (* put root first *)
1589 let get_reachable dir m required_states
=
1590 match required_states
with
1597 if List.mem cur rest
1601 (try Hashtbl.find
reachable_table (cur
,dir
)
1604 let states = reachsatEF dir m
[cur
] in
1605 Hashtbl.add reachable_table (cur
,dir
) states;
1614 Printf.sprintf
"_c%d" c
1616 (* **************************** *)
1617 (* End of environment functions *)
1618 (* **************************** *)
1620 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1622 let rec satloop unchecked required required_states
1623 ((grp
,label,states) as m
) phi env
=
1624 let rec loop unchecked required required_states phi
=
1625 (*Common.profile_code "satloop" (fun _ -> *)
1629 | A.True
-> triples_top states
1630 | A.Pred
(p
) -> satLabel label required p
1631 | A.Uncheck
(phi1
) ->
1632 let unchecked = if !pUNCHECK_OPT then true else false in
1633 loop unchecked required required_states phi1
1635 let phires = loop unchecked required required_states phi
in
1637 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1638 triples_complement (mkstates states required_states
)
1640 | A.Or
(phi1
,phi2
) ->
1642 (loop unchecked required required_states phi1
)
1643 (loop unchecked required required_states phi2
)
1644 | A.SeqOr
(phi1
,phi2
) ->
1645 let res1 = loop unchecked required required_states phi1
in
1646 let res2 = loop unchecked required required_states phi2
in
1647 let res1neg = unwitify res1 in
1650 (triples_complement (mkstates states required_states
) res1neg)
1652 | A.And
(strict
,phi1
,phi2
) ->
1653 (* phi1 is considered to be more likely to be [], because of the
1654 definition of asttoctl. Could use heuristics such as the size of
1656 let pm = !Flag_ctl.partial_match
in
1657 (match (pm,loop unchecked required required_states phi1
) with
1658 (false,[]) when !pLazyOpt -> []
1660 let new_required = extend_required phi1res required
in
1661 let new_required_states = get_required_states phi1res
in
1662 (match (pm,loop unchecked new_required new_required_states phi2
)
1664 (false,[]) when !pLazyOpt -> []
1666 strict_triples_conj strict
1667 (mkstates states required_states
)
1669 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1670 (* phi2 can appear anywhere that is reachable *)
1671 let pm = !Flag_ctl.partial_match
in
1672 (match (pm,loop unchecked required required_states phi1
) with
1675 let new_required = extend_required phi1res required
in
1676 let new_required_states = get_required_states phi1res
in
1677 let new_required_states =
1678 get_reachable dir m
new_required_states in
1679 (match (pm,loop unchecked new_required new_required_states phi2
)
1681 (false,[]) -> phi1res
1684 [] -> (* !Flag_ctl.partial_match must be true *)
1688 let s = mkstates states required_states
in
1690 (function a
-> function b
->
1691 strict_triples_conj strict
s a
[b
])
1692 [List.hd phi2res
] (List.tl phi2res
)
1695 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1696 let s = mkstates states required_states
in
1698 (function a
-> function b
->
1699 strict_triples_conj strict
s a b
)
1703 "only one result allowed for the left arg of AndAny")))
1704 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1705 (* phi2 can appear anywhere that is reachable *)
1706 let pm = !Flag_ctl.partial_match
in
1707 (match (pm,loop unchecked required required_states phi1
) with
1710 let new_required = extend_required phi1res required
in
1711 let new_required_states = get_required_states phi1res
in
1712 let new_required_states =
1713 get_reachable dir m
new_required_states in
1714 (match (pm,loop unchecked new_required new_required_states phi2
)
1716 (false,[]) -> phi1res
1718 (* if there is more than one state, something about the
1719 environment has to ensure that the right triples of
1720 phi2 get associated with the triples of phi1.
1721 the asttoctl2 has to ensure that that is the case.
1722 these should thus be structural properties.
1723 env of phi2 has to be a proper subset of env of phi1
1724 to ensure all end up being consistent. no new triples
1725 should be generated. strict_triples_conj_none takes
1728 let s = mkstates states required_states
in
1731 function (st
,th
,_
) as phi2_elem
->
1733 triples_complement [st
] [(st
,th
,[])] in
1734 strict_triples_conj_none strict
s acc
1735 (phi2_elem
::inverse))
1737 | A.InnerAnd
(phi
) ->
1738 inner_and(loop unchecked required required_states phi
)
1740 let new_required_states =
1741 get_children_required_states dir m required_states
in
1742 satEX dir m
(loop unchecked required
new_required_states phi
)
1744 | A.AX
(dir
,strict
,phi
) ->
1745 let new_required_states =
1746 get_children_required_states dir m required_states
in
1747 let res = loop unchecked required
new_required_states phi
in
1748 strict_A1 strict
satAX satEX dir m
res required_states
1750 let new_required_states = get_reachable dir m required_states
in
1751 satEF dir m
(loop unchecked required
new_required_states phi
)
1753 | A.AF
(dir
,strict
,phi
) ->
1754 if !Flag_ctl.loop_in_src_code
1756 loop unchecked required required_states
1757 (A.AU
(dir
,strict
,A.True
,phi
))
1759 let new_required_states = get_reachable dir m required_states
in
1760 let res = loop unchecked required
new_required_states phi
in
1761 strict_A1 strict
satAF satEF dir m
res new_required_states
1763 let new_required_states = get_reachable dir m required_states
in
1764 satEG dir m
(loop unchecked required
new_required_states phi
)
1766 | A.AG
(dir
,strict
,phi
) ->
1767 let new_required_states = get_reachable dir m required_states
in
1768 let res = loop unchecked required
new_required_states phi
in
1769 strict_A1 strict
satAG satEF dir m
res new_required_states
1770 | A.EU
(dir
,phi1
,phi2
) ->
1771 let new_required_states = get_reachable dir m required_states
in
1772 (match loop unchecked required
new_required_states phi2
with
1773 [] when !pLazyOpt -> []
1775 let new_required = extend_required s2 required
in
1776 let s1 = loop unchecked new_required new_required_states phi1
in
1777 satEU dir m
s1 s2 new_required_states
1778 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1779 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1780 let new_required_states = get_reachable dir m required_states
in
1781 (match loop unchecked required
new_required_states phi2
with
1782 [] when !pLazyOpt -> []
1784 let new_required = extend_required s2 required
in
1785 let s1 = loop unchecked new_required new_required_states phi1
in
1786 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1787 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1788 (*Printf.printf "using AU\n"; flush stdout;*)
1789 let new_required_states = get_reachable dir m required_states
in
1790 (match loop unchecked required
new_required_states phi2
with
1791 [] when !pLazyOpt -> []
1793 let new_required = extend_required s2 required
in
1794 let s1 = loop unchecked new_required new_required_states phi1
in
1796 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1798 print_graph_c grp
new_required_states y ctr phi
) in
1801 | AUfailed tmp_res
->
1802 (* found a loop, have to try AW *)
1804 A[E[phi1 U phi2] & phi1 W phi2]
1805 the and is nonstrict *)
1806 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1807 (*Printf.printf "using AW\n"; flush stdout;*)
1810 (satEU dir m
s1 tmp_res
new_required_states
1811 (* no graph, for the moment *)
1814 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1816 | A.Implies
(phi1
,phi2
) ->
1817 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1818 | A.Exists
(keep
,v
,phi
) ->
1819 let new_required = drop_required v required
in
1820 triples_witness v
unchecked (not keep
)
1821 (loop unchecked new_required required_states phi
)
1822 | A.Let
(v
,phi1
,phi2
) ->
1823 (* should only be used when the properties unchecked, required,
1824 and required_states are known to be the same or at least
1825 compatible between all the uses. this is not checked. *)
1826 let res = loop unchecked required required_states phi1
in
1827 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1828 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1829 (* should only be used when the properties unchecked, required,
1830 and required_states are known to be the same or at least
1831 compatible between all the uses. this is not checked. *)
1832 (* doesn't seem to be used any more *)
1833 let new_required_states = get_reachable dir m required_states
in
1834 let res = loop unchecked required
new_required_states phi1
in
1835 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1837 let res = List.assoc v env
in
1839 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1841 | A.XX
(phi
) -> failwith
"should have been removed" in
1842 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1843 let res = drop_wits required_states
res phi
(* ) *) in
1844 print_graph grp required_states
res "" phi
;
1847 loop unchecked required required_states phi
1851 (* SAT with tracking *)
1852 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1853 ((_
,label,states) as m
) phi env
=
1854 let anno res children
= (annot lvl phi
res children
,res) in
1855 let satv unchecked required required_states phi0 env
=
1856 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1858 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1859 anno (satloop unchecked required required_states m phi env
) []
1863 A.False
-> anno [] []
1864 | A.True
-> anno (triples_top states) []
1866 Printf.printf
"label\n"; flush stdout
;
1867 anno (satLabel label required p
) []
1868 | A.Uncheck
(phi1
) ->
1869 let unchecked = if !pUNCHECK_OPT then true else false in
1870 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1871 Printf.printf
"uncheck\n"; flush stdout
;
1875 satv unchecked required required_states phi1 env
in
1876 Printf.printf
"not\n"; flush stdout
;
1877 anno (triples_complement (mkstates states required_states
) res) [child
]
1878 | A.Or
(phi1
,phi2
) ->
1880 satv unchecked required required_states phi1 env
in
1882 satv unchecked required required_states phi2 env
in
1883 Printf.printf
"or\n"; flush stdout
;
1884 anno (triples_union res1 res2) [child1
; child2
]
1885 | A.SeqOr
(phi1
,phi2
) ->
1887 satv unchecked required required_states phi1 env
in
1889 satv unchecked required required_states phi2 env
in
1891 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1892 Printf.printf
"seqor\n"; flush stdout
;
1893 anno (triples_union res1
1895 (triples_complement (mkstates states required_states
)
1899 | A.And
(strict
,phi1
,phi2
) ->
1900 let pm = !Flag_ctl.partial_match
in
1901 (match (pm,satv unchecked required required_states phi1 env
) with
1902 (false,(child1
,[])) ->
1903 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1904 | (_
,(child1
,res1)) ->
1905 let new_required = extend_required res1 required
in
1906 let new_required_states = get_required_states res1 in
1907 (match (pm,satv unchecked new_required new_required_states phi2
1909 (false,(child2
,[])) ->
1910 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1911 | (_
,(child2
,res2)) ->
1912 Printf.printf
"and\n"; flush stdout
;
1914 strict_triples_conj strict
1915 (mkstates states required_states
)
1917 anno res [child1
; child2
]))
1918 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1919 let pm = !Flag_ctl.partial_match
in
1920 (match (pm,satv unchecked required required_states phi1 env
) with
1921 (false,(child1
,[])) ->
1922 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1923 | (_
,(child1
,res1)) ->
1924 let new_required = extend_required res1 required
in
1925 let new_required_states = get_required_states res1 in
1926 let new_required_states =
1927 get_reachable dir m
new_required_states in
1928 (match (pm,satv unchecked new_required new_required_states phi2
1930 (false,(child2
,[])) ->
1931 Printf.printf
"andany\n"; flush stdout
;
1932 anno res1 [child1
;child2
]
1933 | (_
,(child2
,res2)) ->
1935 [] -> (* !Flag_ctl.partial_match must be true *)
1937 then anno [] [child1
; child2
]
1940 let s = mkstates states required_states
in
1942 (function a
-> function b
->
1943 strict_triples_conj strict
s a
[b
])
1944 [List.hd
res2] (List.tl
res2) in
1945 anno res [child1
; child2
]
1948 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1949 Printf.printf
"andany\n"; flush stdout
;
1951 let s = mkstates states required_states
in
1953 (function a
-> function b
->
1954 strict_triples_conj strict
s a b
)
1956 anno res [child1
; child2
]
1959 "only one result allowed for the left arg of AndAny")))
1960 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1961 let pm = !Flag_ctl.partial_match
in
1962 (match (pm,satv unchecked required required_states phi1 env
) with
1963 (false,(child1
,[])) ->
1964 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1965 | (_
,(child1
,res1)) ->
1966 let new_required = extend_required res1 required
in
1967 let new_required_states = get_required_states res1 in
1968 let new_required_states =
1969 get_reachable dir m
new_required_states in
1970 (match (pm,satv unchecked new_required new_required_states phi2
1972 (false,(child2
,[])) ->
1973 Printf.printf
"andany\n"; flush stdout
;
1974 anno res1 [child1
;child2
]
1975 | (_
,(child2
,res2)) ->
1977 let s = mkstates states required_states
in
1980 function (st
,th
,_
) as phi2_elem
->
1982 triples_complement [st
] [(st
,th
,[])] in
1983 strict_triples_conj_none strict
s acc
1984 (phi2_elem
::inverse))
1986 anno res [child1
; child2
]))
1987 | A.InnerAnd
(phi1
) ->
1988 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1989 Printf.printf
"uncheck\n"; flush stdout
;
1990 anno (inner_and res1) [child1
]
1992 let new_required_states =
1993 get_children_required_states dir m required_states
in
1995 satv unchecked required
new_required_states phi1 env
in
1996 Printf.printf
"EX\n"; flush stdout
;
1997 anno (satEX dir m
res required_states
) [child
]
1998 | A.AX
(dir
,strict
,phi1
) ->
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
"AX\n"; flush stdout
;
2004 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2007 let new_required_states = get_reachable dir m required_states
in
2009 satv unchecked required
new_required_states phi1 env
in
2010 Printf.printf
"EF\n"; flush stdout
;
2011 anno (satEF dir m
res new_required_states) [child
]
2012 | A.AF
(dir
,strict
,phi1
) ->
2013 if !Flag_ctl.loop_in_src_code
2015 satv unchecked required required_states
2016 (A.AU
(dir
,strict
,A.True
,phi1
))
2019 (let new_required_states = get_reachable dir m required_states
in
2021 satv unchecked required
new_required_states phi1 env
in
2022 Printf.printf
"AF\n"; flush stdout
;
2024 strict_A1 strict
satAF satEF dir m
res new_required_states in
2027 let new_required_states = get_reachable dir m required_states
in
2029 satv unchecked required
new_required_states phi1 env
in
2030 Printf.printf
"EG\n"; flush stdout
;
2031 anno (satEG dir m
res new_required_states) [child
]
2032 | A.AG
(dir
,strict
,phi1
) ->
2033 let new_required_states = get_reachable dir m required_states
in
2035 satv unchecked required
new_required_states phi1 env
in
2036 Printf.printf
"AG\n"; flush stdout
;
2037 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2040 | A.EU
(dir
,phi1
,phi2
) ->
2041 let new_required_states = get_reachable dir m required_states
in
2042 (match satv unchecked required
new_required_states phi2 env
with
2044 Printf.printf
"EU\n"; flush stdout
;
2047 let new_required = extend_required res2 required
in
2049 satv unchecked new_required new_required_states phi1 env
in
2050 Printf.printf
"EU\n"; flush stdout
;
2051 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2053 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2054 failwith
"should not be used" (*
2055 let new_required_states = get_reachable dir m required_states in
2056 (match satv unchecked required new_required_states phi2 env with
2058 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2060 let new_required = extend_required res2 required in
2062 satv unchecked new_required new_required_states phi1 env in
2063 Printf.printf "AW %b\n" unchecked; flush stdout;
2065 strict_A2 strict satAW satEF dir m res1 res2
2066 new_required_states in
2067 anno res [child1; child2]) *)
2068 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2069 let new_required_states = get_reachable dir m required_states
in
2070 (match satv unchecked required
new_required_states phi2 env
with
2072 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2074 let new_required = extend_required s2 required
in
2076 satv unchecked new_required new_required_states phi1 env
in
2077 Printf.printf
"AU\n"; flush stdout
;
2079 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2080 (fun y str -> ()) in
2083 anno res [child1
; child2
]
2084 | AUfailed tmp_res
->
2085 (* found a loop, have to try AW *)
2087 A[E[phi1 U phi2] & phi1 W phi2]
2088 the and is nonstrict *)
2089 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2090 Printf.printf
"AW\n"; flush stdout
;
2093 (satEU dir m
s1 tmp_res
new_required_states
2094 (* no graph, for the moment *)
2098 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2099 anno res [child1
; child2
]))
2100 | A.Implies
(phi1
,phi2
) ->
2101 satv unchecked required required_states
2102 (A.Or
(A.Not phi1
,phi2
))
2104 | A.Exists
(keep
,v
,phi1
) ->
2105 let new_required = drop_required v required
in
2107 satv unchecked new_required required_states phi1 env
in
2108 Printf.printf
"exists\n"; flush stdout
;
2109 anno (triples_witness v
unchecked (not keep
) res) [child
]
2110 | A.Let
(v
,phi1
,phi2
) ->
2112 satv unchecked required required_states phi1 env
in
2114 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2115 anno res2 [child1
;child2
]
2116 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2117 let new_required_states = get_reachable dir m required_states
in
2119 satv unchecked required
new_required_states phi1 env
in
2121 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2122 anno res2 [child1
;child2
]
2124 Printf.printf
"Ref\n"; flush stdout
;
2125 let res = List.assoc v env
in
2128 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2131 | A.XX
(phi
) -> failwith
"should have been removed" in
2132 let res1 = drop_wits required_states
res phi
in
2136 print_required_states required_states
;
2137 print_state "after drop_wits" res1 end;
2142 let sat_verbose annotate maxlvl lvl m phi
=
2143 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2145 (* Type for annotations collected in a tree *)
2146 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2148 let sat_annotree annotate m phi
=
2149 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2150 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2154 let sat m phi = satloop m phi []
2158 let simpleanno l phi
res =
2160 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2161 print_generic_algo
(List.sort compare
res);
2162 Format.print_string
"\n------------------------------\n\n" in
2163 let pp_dir = function
2165 | A.BACKWARD
-> pp "^" in
2167 | A.False
-> pp "False"
2168 | A.True
-> pp "True"
2169 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2170 | A.Not
(phi
) -> pp "Not"
2171 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2172 | A.And
(_
,phi1
,phi2
) -> pp "And"
2173 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2174 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2175 | A.Or
(phi1
,phi2
) -> pp "Or"
2176 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2177 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2178 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2179 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2180 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2181 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2182 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2183 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2184 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2185 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2186 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2187 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2188 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2189 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2190 | A.Uncheck
(s) -> pp "Uncheck"
2191 | A.InnerAnd
(s) -> pp "InnerAnd"
2192 | A.XX
(phi1
) -> pp "XX"
2196 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2197 print a ctl formula more accurately if you want.
2198 Use the print_xxx provided in the different module to call
2199 Pretty_print_ctl.pp_ctl.
2202 let simpleanno2 l phi
res =
2204 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2205 Format.print_newline
();
2206 Format.print_string
"----------------------------------------------------";
2207 Format.print_newline
();
2208 print_generic_algo
(List.sort compare
res);
2209 Format.print_newline
();
2210 Format.print_string
"----------------------------------------------------";
2211 Format.print_newline
();
2212 Format.print_newline
();
2216 (* ---------------------------------------------------------------------- *)
2218 (* ---------------------------------------------------------------------- *)
2220 type optentry
= bool ref * string
2221 type options
= {label : optentry
; unch
: optentry
;
2222 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2224 reqenv
: optentry
; reqstates
: optentry
}
2227 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2228 unch
= (pUNCHECK_OPT,"uncheck_opt");
2229 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2230 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2231 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2232 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2233 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2234 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2238 ("label ",[options.label]);
2239 ("unch ",[options.unch
]);
2240 ("unch and label ",[options.label;options.unch
])]
2243 [("conj ", [options.conj]);
2244 ("compl1 ", [options.compl1
]);
2245 ("compl12 ", [options.compl1
;options.compl2
]);
2246 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2247 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2249 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2250 ("compl12 unch satl ",
2251 [options.compl1;options.compl2;options.unch;options.label]); *)
2252 ("conj/compl12 unch satl ",
2253 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2256 [("newinfo ", [options.newinfo
]);
2257 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2260 [("reqenv ", [options.reqenv
]);
2261 ("reqstates ", [options.reqstates
]);
2262 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2263 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2264 ("reqstates unch satl ",
2265 [options.reqstates;options.unch;options.label]);*)
2266 ("reqenv/states unch satl ",
2267 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2270 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2271 options.newinfo
;options.reqenv
;options.reqstates
]
2274 [("all ",all_options)]
2276 let all_options_but_path =
2277 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2278 options.reqenv
;options.reqstates
]
2280 let all_but_path = ("all but path ",all_options_but_path)
2283 [(satAW_calls, "satAW", ref 0);
2284 (satAU_calls, "satAU", ref 0);
2285 (satEF_calls, "satEF", ref 0);
2286 (satAF_calls, "satAF", ref 0);
2287 (satEG_calls, "satEG", ref 0);
2288 (satAG_calls, "satAG", ref 0);
2289 (satEU_calls, "satEU", ref 0)]
2293 (function (opt
,x) ->
2294 (opt
,x,ref 0.0,ref 0,
2295 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2296 [List.hd
all;all_but_path]
2297 (*(all@baseline@conjneg@path@required)*)
2301 let rec iter fn = function
2303 | n
-> let _ = fn() in
2304 (Hashtbl.clear
reachable_table;
2305 Hashtbl.clear
memo_label;
2309 let copy_to_stderr fl
=
2310 let i = open_in fl
in
2312 Printf.fprintf stderr
"%s\n" (input_line
i);
2314 try loop() with _ -> ();
2317 let bench_sat (_,_,states) fn =
2318 List.iter (function (opt
,_) -> opt
:= false) all_options;
2321 (function (name
,options,time
,trips,counter_info
) ->
2322 let iterct = !Flag_ctl.bench
in
2323 if !time
> float_of_int
timeout then time
:= -100.0;
2324 if not
(!time
= -100.0)
2327 Hashtbl.clear
reachable_table;
2328 Hashtbl.clear
memo_label;
2329 List.iter (function (opt
,_) -> opt
:= true) options;
2330 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2334 let bef = Sys.time
() in
2336 Common.timeout_function
timeout
2338 let bef = Sys.time
() in
2339 let res = iter fn iterct in
2340 let aft = Sys.time
() in
2341 time
:= !time
+. (aft -. bef);
2342 trips := !trips + !triples;
2344 (function (calls
,_,save_calls
) ->
2345 function (current_calls
,current_cfg
,current_max_cfg
) ->
2347 !current_calls
+ (!calls
- !save_calls
);
2348 if (!calls
- !save_calls
) > 0
2350 (let st = List.length
states in
2351 current_cfg
:= !current_cfg
+ st;
2352 if st > !current_max_cfg
2353 then current_max_cfg
:= st))
2354 counters counter_info
;
2359 let aft = Sys.time
() in
2361 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2365 List.iter (function (opt
,_) -> opt
:= false) options;
2370 Printf.fprintf stderr
"\n";
2374 (if not
(List.for_all
(function x -> x = res) rest
)
2376 (List.iter (print_state "a state") answers;
2377 Printf.printf
"something doesn't work\n");
2381 let iterct = !Flag_ctl.bench
in
2385 (function (name
,options,time
,trips,counter_info
) ->
2386 Printf.fprintf stderr
"%s Numbers: %f %d "
2387 name
(!time
/. (float_of_int
iterct)) !trips;
2389 (function (calls
,cfg
,max_cfg
) ->
2390 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2392 Printf.fprintf stderr
"\n")
2395 (* ---------------------------------------------------------------------- *)
2396 (* preprocessing: ignore irrelevant functions *)
2398 let preprocess (cfg
,_,_) label = function
2399 [] -> true (* no information, try everything *)
2401 let sz = G.size cfg
in
2402 let verbose_output pred = function
2404 Printf.printf
"did not find:\n";
2405 P.print_predicate
pred; Format.print_newline
()
2407 Printf.printf
"found:\n";
2408 P.print_predicate
pred; Format.print_newline
();
2409 Printf.printf
"but it was not enough\n" in
2410 let get_any verbose
x =
2412 try Hashtbl.find
memo_label x
2415 (let triples = label x in
2417 List.map (function (st,th
,_) -> (st,th
)) triples in
2418 Hashtbl.add memo_label x filtered;
2420 if verbose
then verbose_output x res;
2423 (* don't bother testing when there are more patterns than nodes *)
2424 if List.length l
> sz-2
2426 else List.for_all
(get_any false) l
in
2427 if List.exists
get_all l
2430 (if !Flag_ctl.verbose_match
2432 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2436 let filter_partial_matches trips =
2437 if !Flag_ctl.partial_match
2439 let anynegwit = (* if any is neg, then all are *)
2440 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2442 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2445 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2449 (* ---------------------------------------------------------------------- *)
2450 (* Main entry point for engine *)
2451 let sat m phi reqopt
=
2453 (match !Flag_ctl.steps
with
2454 None
-> step_count := 0
2455 | Some
x -> step_count := x);
2456 Hashtbl.clear
reachable_table;
2457 Hashtbl.clear
memo_label;
2458 let (x,label,states) = m
in
2459 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2461 ((* to drop when Yoann initialized this flag *)
2462 if List.exists
(G.extract_is_loop
x) states
2463 then Flag_ctl.loop_in_src_code
:= true;
2464 let m = (x,label,List.sort compare
states) in
2466 if(!Flag_ctl.verbose_ctl_engine
)
2468 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2469 if !Flag_ctl.bench
> 0
2473 let fn _ = satloop false [] None
m phi
[] in
2474 if !Flag_ctl.bench
> 0
2476 else Common.profile_code
"ctl" (fun _ -> fn()) in
2477 let res = filter_partial_matches res in
2479 Printf.printf "steps: start %d, stop %d\n"
2480 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2482 Printf.printf "triples: %d\n" !triples;
2483 print_state "final result" res;
2485 List.sort compare
res)
2487 (if !Flag_ctl.verbose_ctl_engine
2488 then Common.pr2
"missing something required";
2493 (* ********************************************************************** *)
2494 (* End of Module: CTL_ENGINE *)
2495 (* ********************************************************************** *)