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
1529 (if !pREQUIRED_ENV_OPT
1533 function ((s
,th
,_
) as t) ->
1535 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1542 let get_required_states l
=
1543 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1545 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1548 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1549 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1551 match required_states
with
1556 A.FORWARD
-> G.successors
1557 | A.BACKWARD
-> G.predecessors in
1558 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1561 let reachable_table =
1562 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1564 (* like satEF, but specialized for get_reachable *)
1565 let reachsatEF dir
(grp
,_
,_
) s2 =
1567 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1568 let union = unionBy compare
(=) in
1569 let rec f y
= function
1572 let (pre_collected
,new_info) =
1573 List.partition (function Common.Left
x -> true | _
-> false)
1576 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1577 with Not_found
-> Common.Right
x)
1582 function Common.Left
x -> union x rest
1583 | _
-> failwith
"not possible")
1587 (function Common.Right
x -> x | _
-> failwith
"not possible")
1589 let first = inner_setify (concatmap (dirop grp
) new_info) in
1590 let new_info = setdiff first y in
1591 let res = new_info @ y in
1593 List.rev
(f s2 s2) (* put root first *)
1595 let get_reachable dir m required_states
=
1596 match required_states
with
1603 if List.mem cur rest
1607 (try Hashtbl.find
reachable_table (cur
,dir
)
1610 let states = reachsatEF dir m
[cur
] in
1611 Hashtbl.add reachable_table (cur
,dir
) states;
1620 Printf.sprintf
"_c%d" c
1622 (* **************************** *)
1623 (* End of environment functions *)
1624 (* **************************** *)
1626 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1628 let rec satloop unchecked required required_states
1629 ((grp
,label,states) as m
) phi env
=
1630 let rec loop unchecked required required_states phi
=
1631 (*Common.profile_code "satloop" (fun _ -> *)
1635 | A.True
-> triples_top states
1636 | A.Pred
(p
) -> satLabel label required p
1637 | A.Uncheck
(phi1
) ->
1638 let unchecked = if !pUNCHECK_OPT then true else false in
1639 loop unchecked required required_states phi1
1641 let phires = loop unchecked required required_states phi
in
1643 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1644 triples_complement (mkstates states required_states
)
1646 | A.Or
(phi1
,phi2
) ->
1648 (loop unchecked required required_states phi1
)
1649 (loop unchecked required required_states phi2
)
1650 | A.SeqOr
(phi1
,phi2
) ->
1651 let res1 = loop unchecked required required_states phi1
in
1652 let res2 = loop unchecked required required_states phi2
in
1653 let res1neg = unwitify res1 in
1656 (triples_complement (mkstates states required_states
) res1neg)
1658 | A.And
(strict
,phi1
,phi2
) ->
1659 (* phi1 is considered to be more likely to be [], because of the
1660 definition of asttoctl. Could use heuristics such as the size of
1662 let pm = !Flag_ctl.partial_match
in
1663 (match (pm,loop unchecked required required_states phi1
) with
1664 (false,[]) when !pLazyOpt -> []
1666 let new_required = extend_required phi1res required
in
1667 let new_required_states = get_required_states phi1res
in
1668 (match (pm,loop unchecked new_required new_required_states phi2
)
1670 (false,[]) when !pLazyOpt -> []
1672 strict_triples_conj strict
1673 (mkstates states required_states
)
1675 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1676 (* phi2 can appear anywhere that is reachable *)
1677 let pm = !Flag_ctl.partial_match
in
1678 (match (pm,loop unchecked required required_states phi1
) with
1681 let new_required = extend_required phi1res required
in
1682 let new_required_states = get_required_states phi1res
in
1683 let new_required_states =
1684 get_reachable dir m
new_required_states in
1685 (match (pm,loop unchecked new_required new_required_states phi2
)
1687 (false,[]) -> phi1res
1690 [] -> (* !Flag_ctl.partial_match must be true *)
1694 let s = mkstates states required_states
in
1696 (function a
-> function b
->
1697 strict_triples_conj strict
s a
[b
])
1698 [List.hd phi2res
] (List.tl phi2res
)
1701 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1702 let s = mkstates states required_states
in
1704 (function a
-> function b
->
1705 strict_triples_conj strict
s a b
)
1709 "only one result allowed for the left arg of AndAny")))
1710 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1711 (* phi2 can appear anywhere that is reachable *)
1712 let pm = !Flag_ctl.partial_match
in
1713 (match (pm,loop unchecked required required_states phi1
) with
1716 let new_required = extend_required phi1res required
in
1717 let new_required_states = get_required_states phi1res
in
1718 let new_required_states =
1719 get_reachable dir m
new_required_states in
1720 (match (pm,loop unchecked new_required new_required_states phi2
)
1722 (false,[]) -> phi1res
1724 (* if there is more than one state, something about the
1725 environment has to ensure that the right triples of
1726 phi2 get associated with the triples of phi1.
1727 the asttoctl2 has to ensure that that is the case.
1728 these should thus be structural properties.
1729 env of phi2 has to be a proper subset of env of phi1
1730 to ensure all end up being consistent. no new triples
1731 should be generated. strict_triples_conj_none takes
1734 let s = mkstates states required_states
in
1737 function (st
,th
,_
) as phi2_elem
->
1739 triples_complement [st
] [(st
,th
,[])] in
1740 strict_triples_conj_none strict
s acc
1741 (phi2_elem
::inverse))
1743 | A.InnerAnd
(phi
) ->
1744 inner_and(loop unchecked required required_states phi
)
1746 let new_required_states =
1747 get_children_required_states dir m required_states
in
1748 satEX dir m
(loop unchecked required
new_required_states phi
)
1750 | A.AX
(dir
,strict
,phi
) ->
1751 let new_required_states =
1752 get_children_required_states dir m required_states
in
1753 let res = loop unchecked required
new_required_states phi
in
1754 strict_A1 strict
satAX satEX dir m
res required_states
1756 let new_required_states = get_reachable dir m required_states
in
1757 satEF dir m
(loop unchecked required
new_required_states phi
)
1759 | A.AF
(dir
,strict
,phi
) ->
1760 if !Flag_ctl.loop_in_src_code
1762 loop unchecked required required_states
1763 (A.AU
(dir
,strict
,A.True
,phi
))
1765 let new_required_states = get_reachable dir m required_states
in
1766 let res = loop unchecked required
new_required_states phi
in
1767 strict_A1 strict
satAF satEF dir m
res new_required_states
1769 let new_required_states = get_reachable dir m required_states
in
1770 satEG dir m
(loop unchecked required
new_required_states phi
)
1772 | A.AG
(dir
,strict
,phi
) ->
1773 let new_required_states = get_reachable dir m required_states
in
1774 let res = loop unchecked required
new_required_states phi
in
1775 strict_A1 strict
satAG satEF dir m
res new_required_states
1776 | A.EU
(dir
,phi1
,phi2
) ->
1777 let new_required_states = get_reachable dir m required_states
in
1778 (match loop unchecked required
new_required_states phi2
with
1779 [] when !pLazyOpt -> []
1781 let new_required = extend_required s2 required
in
1782 let s1 = loop unchecked new_required new_required_states phi1
in
1783 satEU dir m
s1 s2 new_required_states
1784 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1785 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1786 let new_required_states = get_reachable dir m required_states
in
1787 (match loop unchecked required
new_required_states phi2
with
1788 [] when !pLazyOpt -> []
1790 let new_required = extend_required s2 required
in
1791 let s1 = loop unchecked new_required new_required_states phi1
in
1792 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1793 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1794 (*Printf.printf "using AU\n"; flush stdout;*)
1795 let new_required_states = get_reachable dir m required_states
in
1796 (match loop unchecked required
new_required_states phi2
with
1797 [] when !pLazyOpt -> []
1799 let new_required = extend_required s2 required
in
1800 let s1 = loop unchecked new_required new_required_states phi1
in
1802 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1804 print_graph_c grp
new_required_states y ctr phi
) in
1807 | AUfailed tmp_res
->
1808 (* found a loop, have to try AW *)
1810 A[E[phi1 U phi2] & phi1 W phi2]
1811 the and is nonstrict *)
1812 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1813 (*Printf.printf "using AW\n"; flush stdout;*)
1816 (satEU dir m
s1 tmp_res
new_required_states
1817 (* no graph, for the moment *)
1820 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1822 | A.Implies
(phi1
,phi2
) ->
1823 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1824 | A.Exists
(keep
,v
,phi
) ->
1825 let new_required = drop_required v required
in
1826 triples_witness v
unchecked (not keep
)
1827 (loop unchecked new_required required_states phi
)
1828 | A.Let
(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 let res = loop unchecked required required_states phi1
in
1833 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1834 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1835 (* should only be used when the properties unchecked, required,
1836 and required_states are known to be the same or at least
1837 compatible between all the uses. this is not checked. *)
1838 (* doesn't seem to be used any more *)
1839 let new_required_states = get_reachable dir m required_states
in
1840 let res = loop unchecked required
new_required_states phi1
in
1841 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1843 let res = List.assoc v env
in
1845 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1847 | A.XX
(phi
) -> failwith
"should have been removed" in
1848 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1849 let res = drop_wits required_states
res phi
(* ) *) in
1850 print_graph grp required_states
res "" phi
;
1853 loop unchecked required required_states phi
1857 (* SAT with tracking *)
1858 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1859 ((_
,label,states) as m
) phi env
=
1860 let anno res children
= (annot lvl phi
res children
,res) in
1861 let satv unchecked required required_states phi0 env
=
1862 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1864 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1865 anno (satloop unchecked required required_states m phi env
) []
1869 A.False
-> anno [] []
1870 | A.True
-> anno (triples_top states) []
1872 Printf.printf
"label\n"; flush stdout
;
1873 anno (satLabel label required p
) []
1874 | A.Uncheck
(phi1
) ->
1875 let unchecked = if !pUNCHECK_OPT then true else false in
1876 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1877 Printf.printf
"uncheck\n"; flush stdout
;
1881 satv unchecked required required_states phi1 env
in
1882 Printf.printf
"not\n"; flush stdout
;
1883 anno (triples_complement (mkstates states required_states
) res) [child
]
1884 | A.Or
(phi1
,phi2
) ->
1886 satv unchecked required required_states phi1 env
in
1888 satv unchecked required required_states phi2 env
in
1889 Printf.printf
"or\n"; flush stdout
;
1890 anno (triples_union res1 res2) [child1
; child2
]
1891 | A.SeqOr
(phi1
,phi2
) ->
1893 satv unchecked required required_states phi1 env
in
1895 satv unchecked required required_states phi2 env
in
1897 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1898 Printf.printf
"seqor\n"; flush stdout
;
1899 anno (triples_union res1
1901 (triples_complement (mkstates states required_states
)
1905 | A.And
(strict
,phi1
,phi2
) ->
1906 let pm = !Flag_ctl.partial_match
in
1907 (match (pm,satv unchecked required required_states phi1 env
) with
1908 (false,(child1
,[])) ->
1909 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1910 | (_
,(child1
,res1)) ->
1911 let new_required = extend_required res1 required
in
1912 let new_required_states = get_required_states res1 in
1913 (match (pm,satv unchecked new_required new_required_states phi2
1915 (false,(child2
,[])) ->
1916 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1917 | (_
,(child2
,res2)) ->
1918 Printf.printf
"and\n"; flush stdout
;
1920 strict_triples_conj strict
1921 (mkstates states required_states
)
1923 anno res [child1
; child2
]))
1924 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1925 let pm = !Flag_ctl.partial_match
in
1926 (match (pm,satv unchecked required required_states phi1 env
) with
1927 (false,(child1
,[])) ->
1928 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1929 | (_
,(child1
,res1)) ->
1930 let new_required = extend_required res1 required
in
1931 let new_required_states = get_required_states res1 in
1932 let new_required_states =
1933 get_reachable dir m
new_required_states in
1934 (match (pm,satv unchecked new_required new_required_states phi2
1936 (false,(child2
,[])) ->
1937 Printf.printf
"andany\n"; flush stdout
;
1938 anno res1 [child1
;child2
]
1939 | (_
,(child2
,res2)) ->
1941 [] -> (* !Flag_ctl.partial_match must be true *)
1943 then anno [] [child1
; child2
]
1946 let s = mkstates states required_states
in
1948 (function a
-> function b
->
1949 strict_triples_conj strict
s a
[b
])
1950 [List.hd
res2] (List.tl
res2) in
1951 anno res [child1
; child2
]
1954 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1955 Printf.printf
"andany\n"; flush stdout
;
1957 let s = mkstates states required_states
in
1959 (function a
-> function b
->
1960 strict_triples_conj strict
s a b
)
1962 anno res [child1
; child2
]
1965 "only one result allowed for the left arg of AndAny")))
1966 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1967 let pm = !Flag_ctl.partial_match
in
1968 (match (pm,satv unchecked required required_states phi1 env
) with
1969 (false,(child1
,[])) ->
1970 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1971 | (_
,(child1
,res1)) ->
1972 let new_required = extend_required res1 required
in
1973 let new_required_states = get_required_states res1 in
1974 let new_required_states =
1975 get_reachable dir m
new_required_states in
1976 (match (pm,satv unchecked new_required new_required_states phi2
1978 (false,(child2
,[])) ->
1979 Printf.printf
"andany\n"; flush stdout
;
1980 anno res1 [child1
;child2
]
1981 | (_
,(child2
,res2)) ->
1983 let s = mkstates states required_states
in
1986 function (st
,th
,_
) as phi2_elem
->
1988 triples_complement [st
] [(st
,th
,[])] in
1989 strict_triples_conj_none strict
s acc
1990 (phi2_elem
::inverse))
1992 anno res [child1
; child2
]))
1993 | A.InnerAnd
(phi1
) ->
1994 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1995 Printf.printf
"uncheck\n"; flush stdout
;
1996 anno (inner_and res1) [child1
]
1998 let new_required_states =
1999 get_children_required_states dir m required_states
in
2001 satv unchecked required
new_required_states phi1 env
in
2002 Printf.printf
"EX\n"; flush stdout
;
2003 anno (satEX dir m
res required_states
) [child
]
2004 | A.AX
(dir
,strict
,phi1
) ->
2005 let new_required_states =
2006 get_children_required_states dir m required_states
in
2008 satv unchecked required
new_required_states phi1 env
in
2009 Printf.printf
"AX\n"; flush stdout
;
2010 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2013 let new_required_states = get_reachable dir m required_states
in
2015 satv unchecked required
new_required_states phi1 env
in
2016 Printf.printf
"EF\n"; flush stdout
;
2017 anno (satEF dir m
res new_required_states) [child
]
2018 | A.AF
(dir
,strict
,phi1
) ->
2019 if !Flag_ctl.loop_in_src_code
2021 satv unchecked required required_states
2022 (A.AU
(dir
,strict
,A.True
,phi1
))
2025 (let new_required_states = get_reachable dir m required_states
in
2027 satv unchecked required
new_required_states phi1 env
in
2028 Printf.printf
"AF\n"; flush stdout
;
2030 strict_A1 strict
satAF satEF dir m
res new_required_states in
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
"EG\n"; flush stdout
;
2037 anno (satEG dir m
res new_required_states) [child
]
2038 | A.AG
(dir
,strict
,phi1
) ->
2039 let new_required_states = get_reachable dir m required_states
in
2041 satv unchecked required
new_required_states phi1 env
in
2042 Printf.printf
"AG\n"; flush stdout
;
2043 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2046 | A.EU
(dir
,phi1
,phi2
) ->
2047 let new_required_states = get_reachable dir m required_states
in
2048 (match satv unchecked required
new_required_states phi2 env
with
2050 Printf.printf
"EU\n"; flush stdout
;
2053 let new_required = extend_required res2 required
in
2055 satv unchecked new_required new_required_states phi1 env
in
2056 Printf.printf
"EU\n"; flush stdout
;
2057 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2059 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2060 failwith
"should not be used" (*
2061 let new_required_states = get_reachable dir m required_states in
2062 (match satv unchecked required new_required_states phi2 env with
2064 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2066 let new_required = extend_required res2 required in
2068 satv unchecked new_required new_required_states phi1 env in
2069 Printf.printf "AW %b\n" unchecked; flush stdout;
2071 strict_A2 strict satAW satEF dir m res1 res2
2072 new_required_states in
2073 anno res [child1; child2]) *)
2074 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2075 let new_required_states = get_reachable dir m required_states
in
2076 (match satv unchecked required
new_required_states phi2 env
with
2078 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2080 let new_required = extend_required s2 required
in
2082 satv unchecked new_required new_required_states phi1 env
in
2083 Printf.printf
"AU\n"; flush stdout
;
2085 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2086 (fun y str -> ()) in
2089 anno res [child1
; child2
]
2090 | AUfailed tmp_res
->
2091 (* found a loop, have to try AW *)
2093 A[E[phi1 U phi2] & phi1 W phi2]
2094 the and is nonstrict *)
2095 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2096 Printf.printf
"AW\n"; flush stdout
;
2099 (satEU dir m
s1 tmp_res
new_required_states
2100 (* no graph, for the moment *)
2104 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2105 anno res [child1
; child2
]))
2106 | A.Implies
(phi1
,phi2
) ->
2107 satv unchecked required required_states
2108 (A.Or
(A.Not phi1
,phi2
))
2110 | A.Exists
(keep
,v
,phi1
) ->
2111 let new_required = drop_required v required
in
2113 satv unchecked new_required required_states phi1 env
in
2114 Printf.printf
"exists\n"; flush stdout
;
2115 anno (triples_witness v
unchecked (not keep
) res) [child
]
2116 | A.Let
(v
,phi1
,phi2
) ->
2118 satv unchecked required required_states phi1 env
in
2120 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2121 anno res2 [child1
;child2
]
2122 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2123 let new_required_states = get_reachable dir m required_states
in
2125 satv unchecked required
new_required_states phi1 env
in
2127 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2128 anno res2 [child1
;child2
]
2130 Printf.printf
"Ref\n"; flush stdout
;
2131 let res = List.assoc v env
in
2134 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2137 | A.XX
(phi
) -> failwith
"should have been removed" in
2138 let res1 = drop_wits required_states
res phi
in
2142 print_required_states required_states
;
2143 print_state "after drop_wits" res1 end;
2148 let sat_verbose annotate maxlvl lvl m phi
=
2149 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2151 (* Type for annotations collected in a tree *)
2152 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2154 let sat_annotree annotate m phi
=
2155 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2156 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2160 let sat m phi = satloop m phi []
2164 let simpleanno l phi
res =
2166 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2167 print_generic_algo
(List.sort compare
res);
2168 Format.print_string
"\n------------------------------\n\n" in
2169 let pp_dir = function
2171 | A.BACKWARD
-> pp "^" in
2173 | A.False
-> pp "False"
2174 | A.True
-> pp "True"
2175 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2176 | A.Not
(phi
) -> pp "Not"
2177 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2178 | A.And
(_
,phi1
,phi2
) -> pp "And"
2179 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2180 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2181 | A.Or
(phi1
,phi2
) -> pp "Or"
2182 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2183 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2184 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2185 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2186 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2187 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2188 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2189 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2190 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2191 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2192 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2193 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2194 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2195 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2196 | A.Uncheck
(s) -> pp "Uncheck"
2197 | A.InnerAnd
(s) -> pp "InnerAnd"
2198 | A.XX
(phi1
) -> pp "XX"
2202 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2203 print a ctl formula more accurately if you want.
2204 Use the print_xxx provided in the different module to call
2205 Pretty_print_ctl.pp_ctl.
2208 let simpleanno2 l phi
res =
2210 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2211 Format.print_newline
();
2212 Format.print_string
"----------------------------------------------------";
2213 Format.print_newline
();
2214 print_generic_algo
(List.sort compare
res);
2215 Format.print_newline
();
2216 Format.print_string
"----------------------------------------------------";
2217 Format.print_newline
();
2218 Format.print_newline
();
2222 (* ---------------------------------------------------------------------- *)
2224 (* ---------------------------------------------------------------------- *)
2226 type optentry
= bool ref * string
2227 type options
= {label : optentry
; unch
: optentry
;
2228 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2230 reqenv
: optentry
; reqstates
: optentry
}
2233 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2234 unch
= (pUNCHECK_OPT,"uncheck_opt");
2235 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2236 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2237 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2238 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2239 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2240 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2244 ("label ",[options.label]);
2245 ("unch ",[options.unch
]);
2246 ("unch and label ",[options.label;options.unch
])]
2249 [("conj ", [options.conj]);
2250 ("compl1 ", [options.compl1
]);
2251 ("compl12 ", [options.compl1
;options.compl2
]);
2252 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2253 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2255 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2256 ("compl12 unch satl ",
2257 [options.compl1;options.compl2;options.unch;options.label]); *)
2258 ("conj/compl12 unch satl ",
2259 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2262 [("newinfo ", [options.newinfo
]);
2263 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2266 [("reqenv ", [options.reqenv
]);
2267 ("reqstates ", [options.reqstates
]);
2268 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2269 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2270 ("reqstates unch satl ",
2271 [options.reqstates;options.unch;options.label]);*)
2272 ("reqenv/states unch satl ",
2273 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2276 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2277 options.newinfo
;options.reqenv
;options.reqstates
]
2280 [("all ",all_options)]
2282 let all_options_but_path =
2283 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2284 options.reqenv
;options.reqstates
]
2286 let all_but_path = ("all but path ",all_options_but_path)
2289 [(satAW_calls, "satAW", ref 0);
2290 (satAU_calls, "satAU", ref 0);
2291 (satEF_calls, "satEF", ref 0);
2292 (satAF_calls, "satAF", ref 0);
2293 (satEG_calls, "satEG", ref 0);
2294 (satAG_calls, "satAG", ref 0);
2295 (satEU_calls, "satEU", ref 0)]
2299 (function (opt
,x) ->
2300 (opt
,x,ref 0.0,ref 0,
2301 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2302 [List.hd
all;all_but_path]
2303 (*(all@baseline@conjneg@path@required)*)
2307 let rec iter fn = function
2309 | n
-> let _ = fn() in
2310 (Hashtbl.clear
reachable_table;
2311 Hashtbl.clear
memo_label;
2315 let copy_to_stderr fl
=
2316 let i = open_in fl
in
2318 Printf.fprintf stderr
"%s\n" (input_line
i);
2320 try loop() with _ -> ();
2323 let bench_sat (_,_,states) fn =
2324 List.iter (function (opt
,_) -> opt
:= false) all_options;
2327 (function (name
,options,time
,trips,counter_info
) ->
2328 let iterct = !Flag_ctl.bench
in
2329 if !time
> float_of_int
timeout then time
:= -100.0;
2330 if not
(!time
= -100.0)
2333 Hashtbl.clear
reachable_table;
2334 Hashtbl.clear
memo_label;
2335 List.iter (function (opt
,_) -> opt
:= true) options;
2336 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2340 let bef = Sys.time
() in
2342 Common.timeout_function
timeout
2344 let bef = Sys.time
() in
2345 let res = iter fn iterct in
2346 let aft = Sys.time
() in
2347 time
:= !time
+. (aft -. bef);
2348 trips := !trips + !triples;
2350 (function (calls
,_,save_calls
) ->
2351 function (current_calls
,current_cfg
,current_max_cfg
) ->
2353 !current_calls
+ (!calls
- !save_calls
);
2354 if (!calls
- !save_calls
) > 0
2356 (let st = List.length
states in
2357 current_cfg
:= !current_cfg
+ st;
2358 if st > !current_max_cfg
2359 then current_max_cfg
:= st))
2360 counters counter_info
;
2365 let aft = Sys.time
() in
2367 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2371 List.iter (function (opt
,_) -> opt
:= false) options;
2376 Printf.fprintf stderr
"\n";
2380 (if not
(List.for_all
(function x -> x = res) rest
)
2382 (List.iter (print_state "a state") answers;
2383 Printf.printf
"something doesn't work\n");
2387 let iterct = !Flag_ctl.bench
in
2391 (function (name
,options,time
,trips,counter_info
) ->
2392 Printf.fprintf stderr
"%s Numbers: %f %d "
2393 name
(!time
/. (float_of_int
iterct)) !trips;
2395 (function (calls
,cfg
,max_cfg
) ->
2396 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2398 Printf.fprintf stderr
"\n")
2401 (* ---------------------------------------------------------------------- *)
2402 (* preprocessing: ignore irrelevant functions *)
2404 let preprocess (cfg
,_,_) label = function
2405 [] -> true (* no information, try everything *)
2407 let sz = G.size cfg
in
2408 let verbose_output pred = function
2410 Printf.printf
"did not find:\n";
2411 P.print_predicate
pred; Format.print_newline
()
2413 Printf.printf
"found:\n";
2414 P.print_predicate
pred; Format.print_newline
();
2415 Printf.printf
"but it was not enough\n" in
2416 let get_any verbose
x =
2418 try Hashtbl.find
memo_label x
2421 (let triples = label x in
2423 List.map (function (st,th
,_) -> (st,th
)) triples in
2424 Hashtbl.add memo_label x filtered;
2426 if verbose
then verbose_output x res;
2429 (* don't bother testing when there are more patterns than nodes *)
2430 if List.length l
> sz-2
2432 else List.for_all
(get_any false) l
in
2433 if List.exists
get_all l
2436 (if !Flag_ctl.verbose_match
2438 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2442 let filter_partial_matches trips =
2443 if !Flag_ctl.partial_match
2445 let anynegwit = (* if any is neg, then all are *)
2446 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2448 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2451 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2455 (* ---------------------------------------------------------------------- *)
2456 (* Main entry point for engine *)
2457 let sat m phi reqopt
=
2459 (match !Flag_ctl.steps
with
2460 None
-> step_count := 0
2461 | Some
x -> step_count := x);
2462 Hashtbl.clear
reachable_table;
2463 Hashtbl.clear
memo_label;
2464 let (x,label,states) = m
in
2465 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2467 ((* to drop when Yoann initialized this flag *)
2468 if List.exists
(G.extract_is_loop
x) states
2469 then Flag_ctl.loop_in_src_code
:= true;
2470 let m = (x,label,List.sort compare
states) in
2472 if(!Flag_ctl.verbose_ctl_engine
)
2474 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2475 if !Flag_ctl.bench
> 0
2479 let fn _ = satloop false [] None
m phi
[] in
2480 if !Flag_ctl.bench
> 0
2482 else Common.profile_code
"ctl" (fun _ -> fn()) in
2483 let res = filter_partial_matches res in
2485 Printf.printf "steps: start %d, stop %d\n"
2486 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2488 Printf.printf "triples: %d\n" !triples;
2489 print_state "final result" res;
2491 List.sort compare
res)
2493 (if !Flag_ctl.verbose_ctl_engine
2494 then Common.pr2
"missing something required";
2499 (* ********************************************************************** *)
2500 (* End of Module: CTL_ENGINE *)
2501 (* ********************************************************************** *)