2 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
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.
24 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
25 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
26 * This file is part of Coccinelle.
28 * Coccinelle is free software: you can redistribute it and/or modify
29 * it under the terms of the GNU General Public License as published by
30 * the Free Software Foundation, according to version 2 of the License.
32 * Coccinelle is distributed in the hope that it will be useful,
33 * but WITHOUT ANY WARRANTY; without even the implied warranty of
34 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
35 * GNU General Public License for more details.
37 * You should have received a copy of the GNU General Public License
38 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
40 * The authors reserve the right to distribute this or future versions of
41 * Coccinelle under other licenses.
45 (*external c_counter : unit -> int = "c_counter"*)
47 (* Optimize triples_conj by first extracting the intersection of the two sets,
48 which can certainly be in the intersection *)
49 let pTRIPLES_CONJ_OPT = ref true
50 (* For complement, make NegState for the negation of a single state *)
51 let pTRIPLES_COMPLEMENT_OPT = ref true
52 (* For complement, do something special for the case where the environment
53 and witnesses are empty *)
54 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
55 (* "Double negate" the arguments of the path operators *)
56 let pDOUBLE_NEGATE_OPT = ref true
57 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
58 let pNEW_INFO_OPT = ref true
59 (* Filter the result of the label function to drop entries that aren't
60 compatible with any of the available environments *)
61 let pREQUIRED_ENV_OPT = ref true
62 (* Memoize the raw result of the label function *)
63 let pSATLABEL_MEMO_OPT = ref true
64 (* Filter results according to the required states *)
65 let pREQUIRED_STATES_OPT = ref true
66 (* Drop negative witnesses at Uncheck *)
67 let pUNCHECK_OPT = ref true
68 let pANY_NEG_OPT = ref true
69 let pLazyOpt = ref true
71 (* Nico: This stack is use for graphical traces *)
72 let graph_stack = ref ([] : string list
)
73 let graph_hash = (Hashtbl.create
101)
76 let pTRIPLES_CONJ_OPT = ref false
77 let pTRIPLES_COMPLEMENT_OPT = ref false
78 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
79 let pDOUBLE_NEGATE_OPT = ref false
80 let pNEW_INFO_OPT = ref false
81 let pREQUIRED_ENV_OPT = ref false
82 let pSATLABEL_MEMO_OPT = ref false
83 let pREQUIRED_STATES_OPT = ref false
84 let pUNCHECK_OPT = ref false
85 let pANY_NEG_OPT = ref false
86 let pLazyOpt = ref false
90 let step_count = ref 0
93 if not
(!step_count = 0)
96 step_count := !step_count - 1;
97 if !step_count = 0 then raise Steps
100 let inc cell
= cell
:= !cell
+ 1
102 let satEU_calls = ref 0
103 let satAW_calls = ref 0
104 let satAU_calls = ref 0
105 let satEF_calls = ref 0
106 let satAF_calls = ref 0
107 let satEG_calls = ref 0
108 let satAG_calls = ref 0
116 Printf.sprintf
"_fresh_r_%d" c
118 (* **********************************************************************
120 * Implementation of a Witness Tree model checking engine for CTL-FVex
123 * **********************************************************************)
125 (* ********************************************************************** *)
126 (* Module: SUBST (substitutions: meta. vars and values) *)
127 (* ********************************************************************** *)
133 val eq_mvar
: mvar
-> mvar
-> bool
134 val eq_val
: value -> value -> bool
135 val merge_val
: value -> value -> value
136 val print_mvar
: mvar
-> unit
137 val print_value
: value -> unit
141 (* ********************************************************************** *)
142 (* Module: GRAPH (control flow graphs / model) *)
143 (* ********************************************************************** *)
149 val predecessors
: cfg
-> node
-> node list
150 val successors
: cfg
-> node
-> node list
151 val extract_is_loop
: cfg
-> node
-> bool
152 val print_node
: node
-> unit
153 val size
: cfg
-> int
154 val print_graph
: cfg
-> string option ->
155 (node
* string) list
-> (node
* string) list
-> string -> unit
159 module OGRAPHEXT_GRAPH
=
162 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
163 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
164 let print_node i
= Format.print_string
(Common.i_to_s i
)
168 (* ********************************************************************** *)
169 (* Module: PREDICATE (predicates for CTL formulae) *)
170 (* ********************************************************************** *)
172 module type PREDICATE
=
175 val print_predicate
: t
-> unit
179 (* ********************************************************************** *)
181 (* ---------------------------------------------------------------------- *)
182 (* Misc. useful generic functions *)
183 (* ---------------------------------------------------------------------- *)
185 let get_graph_files () = !graph_stack
186 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
196 let foldl = List.fold_left
;;
198 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
200 type 'a esc
= ESC
of 'a
| CONT
of 'a
202 let foldr = List.fold_right
;;
204 let concat = List.concat;;
208 let filter = List.filter;;
210 let partition = List.partition;;
212 let concatmap f l
= List.concat (List.map f l
);;
220 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
222 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
224 let rec some_tolist opts
=
227 | (Some x
)::rest
-> x
::(some_tolist rest
)
228 | _
::rest
-> some_tolist rest
231 let rec groupBy eq l
=
235 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
236 (x
::xs1
)::(groupBy eq xs2
)
239 let group l
= groupBy (=) l
;;
241 let rec memBy eq x l
=
244 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
247 let rec nubBy eq ls
=
250 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
251 | (x
::xs
) -> x
::(nubBy eq xs
)
257 | (x
::xs
) when (List.mem x xs
) -> nub xs
258 | (x
::xs
) -> x
::(nub xs
)
261 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
263 let setifyBy eq xs
= nubBy eq xs
;;
265 let setify xs
= nub xs
;;
267 let inner_setify xs
= List.sort compare
(nub xs
);;
269 let unionBy compare eq xs
= function
272 let rec loop = function
274 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
275 List.sort compare
(loop xs
)
278 let union xs ys
= unionBy state_compare (=) xs ys
;;
280 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
282 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
284 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
285 let supseteq xs ys
= subseteq ys xs
287 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
289 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
291 (* Fix point calculation *)
293 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
296 (* Fix point calculation on set-valued functions *)
297 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
298 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
300 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
302 (* ********************************************************************** *)
303 (* Module: CTL_ENGINE *)
304 (* ********************************************************************** *)
307 functor (SUB
: SUBST
) ->
308 functor (G
: GRAPH
) ->
309 functor (P
: PREDICATE
) ->
314 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
316 type ('pred
,'anno
) witness
=
317 (G.node
, substitution
,
318 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
319 Ast_ctl.generic_witnesstree
321 type ('pred
,'anno
) triples =
322 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
324 (* ---------------------------------------------------------------------- *)
325 (* Pretty printing functions *)
326 (* ---------------------------------------------------------------------- *)
328 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
329 let print_generic_subst = function
331 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
332 | A.NegSubst
(mvar
, v
) ->
333 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
334 Format.print_string
"[";
335 Common.print_between
(fun () -> Format.print_string
";" )
336 print_generic_subst substxs
;
337 Format.print_string
"]"
339 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
341 | A.Wit
(state
, subst
, anno
, childrens
) ->
342 Format.print_string
"wit ";
344 print_generic_substitution subst
;
345 (match childrens
with
346 [] -> Format.print_string
"{}"
348 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
349 print_generic_witnesstree childrens
; Format.close_box
())
351 Format.print_string
"!";
352 print_generic_witness wit
354 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
357 Format.print_string
"{";
359 (fun () -> Format.print_string
";"; Format.force_newline
() )
360 print_generic_witness witnesstree
;
361 Format.print_string
"}";
364 and print_generic_triple
(node
,subst
,tree
) =
366 print_generic_substitution subst
;
367 print_generic_witnesstree tree
369 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
370 Format.print_string
"<";
372 (fun () -> Format.print_string
";"; Format.force_newline
())
373 print_generic_triple xs
;
374 Format.print_string
">"
377 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
378 Printf.printf
"%s\n" str
;
379 List.iter
(function x ->
380 print_generic_triple
x; Format.print_newline
(); flush stdout
)
381 (List.sort compare l
);
384 let print_required_states = function
385 None
-> Printf.printf
"no required states\n"
387 Printf.printf
"required states: ";
390 G.print_node x; Format.print_string
" "; Format.print_flush
())
394 let mkstates states
= function
396 | Some states
-> states
398 let print_graph grp required_states res str
= function
399 A.Exists
(keep
,v
,phi
) -> ()
401 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
404 | A.Exists
(keep
,v
,phi
) -> ()
407 Printf.sprintf
"%s%s"
409 (Common.format_to_string
411 Pretty_print_ctl.pp_ctl
412 (P.print_predicate
, SUB.print_mvar
)
415 let file = (match !Flag.currentfile
with
416 None
-> "graphical_trace"
419 (if not
(List.mem
file !graph_stack) then
420 graph_stack := file :: !graph_stack);
421 let filename = Filename.temp_file
(file^
":") ".dot" in
422 Hashtbl.add
graph_hash file filename;
424 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
425 (match required_states
with
427 | Some required_states
->
428 (List.map (function s
-> (s
,"blue")) required_states
))
429 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
431 let print_graph_c grp required_states res
ctr phi
=
432 let str = "iter: "^
(string_of_int
!ctr) in
433 print_graph grp required_states res
str phi
435 (* ---------------------------------------------------------------------- *)
437 (* ---------------------------------------------------------------------- *)
440 (* ************************* *)
442 (* ************************* *)
447 | A.NegSubst
(x,_
) -> x
453 | A.NegSubst
(_
,x) -> x
456 let eq_subBy eqx eqv sub sub'
=
457 match (sub
,sub'
) with
458 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
459 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
464 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
466 let eq_subst th th'
= setequalBy eq_sub th th'
;;
468 let merge_subBy eqx
(===) (>+<) sub sub'
=
469 (* variable part is guaranteed to be the same *)
470 match (sub
,sub'
) with
471 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
473 then Some
[A.Subst
(x, v
>+< v'
)]
475 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
477 then Some
[A.Subst
(x'
,v'
)]
479 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
481 then Some
[A.Subst
(x,v
)]
483 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
486 let merged = v
>+< v'
in
487 if merged = v
&& merged = v'
488 then Some
[A.NegSubst
(x,v
>+< v'
)]
490 (* positions are compatible, but not identical. keep apart. *)
491 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
492 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
496 (* How could we accomadate subterm constraints here??? *)
497 let merge_sub sub sub'
=
498 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
500 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
502 (* NOTE: we sort by using the generic "compare" on (meta-)variable
503 * names; we could also require a definition of compare for meta-variables
504 * or substitutions but that seems like overkill for sorting
506 let clean_subst theta
=
510 let res = compare
(dom_sub s
) (dom_sub s'
) in
514 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
515 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
516 | _
-> compare
(ran_sub s
) (ran_sub s'
)
519 let rec loop = function
521 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
522 loop (A.Subst
(x,v
)::rest
)
523 | x::xs
-> x::(loop xs
) in
526 let top_subst = [];; (* Always TRUE subst. *)
528 (* Split a theta in two parts: one with (only) "x" and one without *)
530 let split_subst theta
x =
531 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
533 exception SUBST_MISMATCH
534 let conj_subst theta theta'
=
535 match (theta
,theta'
) with
536 | ([],_
) -> Some theta'
537 | (_
,[]) -> Some theta
539 let rec classify = function
541 | [x] -> [(dom_sub x,[x])]
543 (match classify xs
with
544 ((nm
,y
)::ys
) as res ->
547 else (dom_sub x,[x])::res
548 | _
-> failwith
"not possible") in
549 let merge_all theta theta'
=
556 match (merge_sub sub sub'
) with
557 Some subs
-> subs
@ rest
558 | _
-> raise SUBST_MISMATCH
)
561 let rec loop = function
563 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
565 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
566 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
567 (match compare
x y
with
568 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
569 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
570 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
571 | _
-> failwith
"not possible") in
572 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
573 with SUBST_MISMATCH
-> None
576 (* theta' must be a subset of theta *)
577 let conj_subst_none theta theta'
=
578 match (theta
,theta'
) with
579 | (_
,[]) -> Some theta
582 let rec classify = function
584 | [x] -> [(dom_sub x,[x])]
586 (match classify xs
with
587 ((nm
,y
)::ys
) as res ->
590 else (dom_sub x,[x])::res
591 | _
-> failwith
"not possible") in
592 let merge_all theta theta'
=
599 match (merge_sub sub sub'
) with
600 Some subs
-> subs
@ rest
601 | _
-> raise SUBST_MISMATCH
)
604 let rec loop = function
606 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
607 | ([],ctheta'
) -> raise SUBST_MISMATCH
608 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
609 (match compare
x y
with
610 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
611 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
612 | 1 -> raise SUBST_MISMATCH
613 | _
-> failwith
"not possible") in
614 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
615 with SUBST_MISMATCH
-> None
620 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
621 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
624 (* Turn a (big) theta into a list of (small) thetas *)
625 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
628 (* ************************* *)
630 (* ************************* *)
632 (* Always TRUE witness *)
633 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
635 let eq_wit wit wit'
= wit
= wit'
;;
637 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
638 let res = unionBy compare
(=) wit wit'
in
639 let anynegwit = (* if any is neg, then all are *)
640 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
642 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
645 let negate_wit wit
= A.NegWit wit
(*
647 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
648 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
651 let negate_wits wits
=
652 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
655 let anynegwit = (* if any is neg, then all are *)
656 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
660 function (s
,th
,wit
) ->
661 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
664 (* ************************* *)
666 (* ************************* *)
668 (* Triples are equal when the constituents are equal *)
669 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
670 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
672 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
674 let normalize trips
=
676 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
680 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
681 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
682 let triples_conj trips trips'
=
683 let (trips
,shared
,trips'
) =
684 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
687 List.partition (function t
-> List.mem t trips'
) trips
in
689 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
690 (trips,shared
,trips'
)
691 else (trips,[],trips'
) in
692 foldl (* returns a set - setify inlined *)
694 function (s1
,th1
,wit1
) ->
697 function (s2
,th2
,wit2
) ->
699 (match (conj_subst th1 th2
) with
701 let t = (s1
,th
,union_wit wit1 wit2
) in
702 if List.mem
t rest
then rest
else t::rest
709 (* ignore the state in the right argument. always pretend it is the same as
711 (* env on right has to be a subset of env on left *)
712 let triples_conj_none trips trips'
=
713 let (trips,shared
,trips'
) =
714 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
717 List.partition (function t -> List.mem
t trips'
) trips in
719 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
720 (trips,shared
,trips'
)
721 else (trips,[],trips'
) in
722 foldl (* returns a set - setify inlined *)
724 function (s1
,th1
,wit1
) ->
727 function (s2
,th2
,wit2
) ->
728 match (conj_subst_none th1 th2
) with
730 let t = (s1
,th
,union_wit wit1 wit2
) in
731 if List.mem
t rest
then rest
else t::rest
739 let triples_conj_AW trips trips'
=
740 let (trips,shared
,trips'
) =
741 if false && !pTRIPLES_CONJ_OPT
744 List.partition (function t -> List.mem
t trips'
) trips in
746 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
747 (trips,shared
,trips'
)
748 else (trips,[],trips'
) in
749 foldl (* returns a set - setify inlined *)
751 function (s1
,th1
,wit1
) ->
754 function (s2
,th2
,wit2
) ->
756 (match (conj_subst th1 th2
) with
758 let t = (s1
,th
,union_wit wit1 wit2
) in
759 if List.mem
t rest
then rest
else t::rest
766 (* *************************** *)
767 (* NEGATION (NegState style) *)
768 (* *************************** *)
770 (* Constructive negation at the state level *)
773 | NegState
of 'a list
776 let compatible_states = function
777 (PosState s1
, PosState s2
) ->
778 if s1
= s2
then Some
(PosState s1
) else None
779 | (PosState s1
, NegState s2
) ->
780 if List.mem s1 s2
then None
else Some
(PosState s1
)
781 | (NegState s1
, PosState s2
) ->
782 if List.mem s2 s1
then None
else Some
(PosState s2
)
783 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
786 (* Conjunction on triples with "special states" *)
787 let triples_state_conj trips trips'
=
788 let (trips,shared
,trips'
) =
789 if !pTRIPLES_CONJ_OPT
792 List.partition (function t -> List.mem
t trips'
) trips in
794 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
795 (trips,shared
,trips'
)
796 else (trips,[],trips'
) in
799 function (s1
,th1
,wit1
) ->
802 function (s2
,th2
,wit2
) ->
803 match compatible_states(s1
,s2
) with
805 (match (conj_subst th1 th2
) with
807 let t = (s
,th
,union_wit wit1 wit2
) in
808 if List.mem
t rest
then rest
else t::rest
815 let triple_negate (s
,th
,wits
) =
816 let negstates = (NegState
[s
],top_subst,top_wit) in
817 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
818 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
819 negstates :: (negths @ negwits) (* all different *)
821 (* FIX ME: it is not necessary to do full conjunction *)
822 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
823 if !pTRIPLES_COMPLEMENT_OPT
825 (let cleanup (s
,th
,wit
) =
827 PosState s'
-> [(s'
,th
,wit
)]
829 assert (th
=top_subst);
830 assert (wit
=top_wit);
831 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
832 let (simple
,complex
) =
833 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
835 let (simple
,complex
) =
836 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
838 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
839 top_subst,top_wit)] in
841 else ([(NegState
[],top_subst,top_wit)],trips) in
842 let rec compl trips =
845 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
846 let compld = (compl complex
) in
847 let compld = concatmap cleanup compld in
850 let negstates (st
,th
,wits
) =
851 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
852 let negths (st
,th
,wits
) =
853 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
854 let negwits (st
,th
,wits
) =
855 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
857 [] -> map (function st
-> (st
,top_subst,top_wit)) states
863 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
864 (negstates x @ negths x @ negwits x) xs
)
867 let triple_negate (s
,th
,wits
) =
868 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
869 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
870 ([s
], negths @ negwits) (* all different *)
872 let print_compl_state str (n
,p
) =
873 Printf.printf
"%s neg: " str;
875 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
880 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
882 then map (function st
-> (st
,top_subst,top_wit)) states
884 let cleanup (neg
,pos
) =
886 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
887 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
889 let trips = List.sort
state_compare trips in
890 let all_negated = List.map triple_negate trips in
891 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
892 let (pos1conj
,pos1keep
) =
893 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
894 let (pos2conj
,pos2keep
) =
895 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
896 (Common.union_set neg1 neg2
,
897 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
898 let rec inner_loop = function
899 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
901 let rec outer_loop = function
903 | l
-> outer_loop (inner_loop l
) in
904 cleanup (outer_loop all_negated)
906 (* ********************************** *)
907 (* END OF NEGATION (NegState style) *)
908 (* ********************************** *)
910 (* now this is always true, so we could get rid of it *)
911 let something_dropped = ref true
913 let triples_union trips trips'
=
914 (*unionBy compare eq_trip trips trips';;*)
915 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
917 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
918 Then, the following says that since the first is a more restrictive
919 environment and has fewer witnesses, then it should be dropped. But having
920 fewer witnesses is not necessarily less informative than having more,
921 because fewer witnesses can mean the absence of the witness-causing thing.
922 So the fewer witnesses have to be kept around.
923 subseteq changed to = to make it hopefully work
928 something_dropped := false;
930 then (something_dropped := true; trips)
932 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
935 (match conj_subst th1 th2
with
938 then if (*subseteq*) wit1
= wit2
then 1 else 0
941 then if (*subseteq*) wit2
= wit1
then (-1) else 0
945 let rec first_loop second
= function
947 | x::xs
-> first_loop (second_loop
x second
) xs
948 and second_loop
x = function
951 match subsumes x y
with
952 1 -> something_dropped := true; all
953 | (-1) -> second_loop
x ys
954 | _
-> y
::(second_loop
x ys
) in
955 first_loop trips trips'
957 else unionBy compare
eq_trip trips trips'
960 let triples_witness x unchecked not_keep
trips =
961 let anyneg = (* if any is neg, then all are *)
962 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
963 let anynegwit = (* if any is neg, then all are *)
964 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
965 let allnegwit = (* if any is neg, then all are *)
966 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
968 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
972 function (s
,th
,wit
) as t ->
973 let (th_x
,newth
) = split_subst th
x in
976 (* one consider whether if not not_keep is true, then we should
977 fail. but it could be that the variable is a used_after and
978 then it is the later rule that should fail and not this one *)
979 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
981 (SUB.print_mvar
x; Format.print_flush
();
982 print_state ": empty witness from" [t]);
984 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
985 (* see tests/nestseq for how neg bindings can come up even
986 without eg partial matches
987 (* negated substitution only allowed with negwits.
989 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
992 (print_generic_substitution l
; Format.print_newline
();
993 failwith
"unexpected negative binding with positive witnesses")*)
996 if unchecked
or not_keep
999 if anynegwit wit
&& allnegwit wit
1000 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
1001 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
1004 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
1010 (* ---------------------------------------------------------------------- *)
1011 (* SAT - Model Checking Algorithm for CTL-FVex *)
1013 (* TODO: Implement _all_ operators (directly) *)
1014 (* ---------------------------------------------------------------------- *)
1017 (* ************************************* *)
1018 (* The SAT algorithm and special helpers *)
1019 (* ************************************* *)
1021 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1023 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1024 let exp (s
,th
,wit
) =
1026 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1028 A.FORWARD
-> G.predecessors grp s
1029 | A.BACKWARD
-> G.successors grp s
) in
1030 setify (concatmap exp y
)
1035 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1038 None
-> true | Some reqst
-> List.mem s reqst
in
1041 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1044 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1047 (function p
-> (p
,succ grp p
))
1050 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1051 (* would a hash table be more efficient? *)
1052 let all = List.sort
state_compare all in
1053 let rec up_nodes child s
= function
1055 | (s1
,th
,wit
)::xs
->
1056 (match compare s1 child
with
1057 -1 -> up_nodes child s xs
1058 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1060 let neighbor_triples =
1063 function (s
,children
) ->
1067 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1071 match neighbor_triples with
1075 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1077 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1080 None
-> true | Some reqst
-> List.mem s reqst
in
1083 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1086 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1089 (function p
-> (p
,succ grp p
))
1092 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1093 (* would a hash table be more efficient? *)
1094 let all = List.sort
state_compare all in
1095 let rec up_nodes child s
= function
1097 | (s1
,th
,wit
)::xs
->
1098 (match compare s1 child
with
1099 -1 -> up_nodes child s xs
1100 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1102 let neighbor_triples =
1105 function (s
,children
) ->
1108 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1111 match neighbor_triples with
1113 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1115 (* drop_negwits will call setify *)
1116 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1118 let satAX dir m s reqst
= pre_forall dir m s s reqst
1121 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1122 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1123 (*Printf.printf "EU\n";
1124 let ctr = ref 0 in*)
1129 (*let ctr = ref 0 in*)
1132 let rec f y new_info
=
1138 print_graph y ctr;*)
1139 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1140 let res = triples_union first y
in
1141 let new_info = setdiff res y
in
1142 (*Printf.printf "iter %d res %d new_info %d\n"
1143 !ctr (List.length res) (List.length new_info);
1144 print_state "res" res;
1145 print_state "new_info" new_info;
1153 print_graph y ctr;*)
1154 let pre = pre_exist dir m y reqst
in
1155 triples_union s2
(triples_conj s1
pre) in
1159 (* EF phi == E[true U phi] *)
1160 let satEF dir m s2 reqst
=
1162 (*let ctr = ref 0 in*)
1165 let rec f y
new_info =
1171 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1172 let first = pre_exist dir m
new_info reqst
in
1173 let res = triples_union first y
in
1174 let new_info = setdiff res y
in
1175 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1176 (if dir = A.BACKWARD then "reachable" else "real ef")
1177 !ctr (List.length res) (List.length new_info);
1178 print_state "new info" new_info;
1185 let pre = pre_exist dir m y reqst
in
1186 triples_union s2
pre in
1190 type ('
pred,'anno
) auok
=
1191 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1193 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1194 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1200 (*let ctr = ref 0 in*)
1202 if !Flag_ctl.loop_in_src_code
1207 let rec f y newinfo
=
1213 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1217 try Some
(pre_forall dir m
new_info y reqst
)
1222 match triples_conj s1
pre with
1225 (*print_state "s1" s1;
1226 print_state "pre" pre;
1227 print_state "first" first;*)
1228 let res = triples_union first y
in
1230 if not
!something_dropped
1232 else setdiff res y
in
1234 "iter %d res %d new_info %d\n"
1235 !ctr (List.length res) (List.length new_info);
1240 if !Flag_ctl.loop_in_src_code
1244 fix (function s1 -> function s2 ->
1245 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1246 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1247 subseteq s1 s2) in for popl *)
1252 let pre = pre_forall dir m y y reqst
in
1253 triples_union s2 (triples_conj s1 pre) in
1258 (* reqst could be the states of s1 *)
1260 let lstates = mkstates states reqst in
1261 let initial_removed =
1262 triples_complement lstates (triples_union s1 s2) in
1263 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1264 let rec loop base removed =
1266 triples_conj base (pre_exist dir m removed reqst) in
1268 triples_conj base (triples_complement lstates new_removed) in
1269 if supseteq new_base base
1270 then triples_union base s2
1271 else loop new_base new_removed in
1272 loop initial_base initial_removed *)
1274 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1280 This works extremely badly when the region is small and the end of the
1281 region is very ambiguous, eg free(x) ... x
1285 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1286 let ostates = Common.union_set (get_states s1) (get_states s2) in
1289 A.FORWARD -> G.successors grp
1290 | A.BACKWARD -> G.predecessors grp) in
1292 List.fold_left Common.union_set ostates (List.map succ ostates) in
1293 let negphi = triples_complement states s1 in
1294 let negpsi = triples_complement states s2 in
1295 triples_complement ostates
1296 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1299 (*let ctr = ref 0 in*)
1303 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1306 let pre = pre_forall dir m y y reqst
in
1307 (*print_state "pre" pre;*)
1308 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1309 triples_union s2 conj in
1310 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1311 (* drop wits on s1 represents that we don't want any witnesses from
1312 the case that infinitely loops, only from the case that gets
1313 out of the loop. s1 is like a guard. To see the problem, consider
1314 an example where both s1 and s2 match some code after the loop.
1315 we only want the witness from s2. *)
1316 setgfix f (triples_union (nub(drop_wits s1)) s2)
1319 let satAF dir m s reqst
=
1323 let rec f y newinfo
=
1328 let first = pre_forall dir m
new_info y reqst
in
1329 let res = triples_union first y
in
1330 let new_info = setdiff res y
in
1336 let pre = pre_forall dir m y y reqst
in
1337 triples_union s
pre in
1340 let satAG dir
((_
,_
,states) as m
) s reqst
=
1344 let pre = pre_forall dir m y y reqst
in
1345 triples_conj y
pre in
1348 let satEG dir
((_
,_
,states) as m
) s reqst
=
1352 let pre = pre_exist dir m y reqst
in
1353 triples_conj y
pre in
1356 (* **************************************************************** *)
1357 (* Inner And - a way of dealing with multiple matches within a node *)
1358 (* **************************************************************** *)
1359 (* applied to the result of matching a node. collect witnesses when the
1360 states and environments are the same *)
1362 let inner_and trips =
1363 let rec loop = function
1365 | (s
,th
,w
)::trips ->
1366 let (cur
,acc
) = loop trips in
1368 (s'
,_
,_
)::_
when s
= s'
->
1369 let rec loop'
= function
1371 | ((_
,th'
,w'
) as t'
)::ts'
->
1372 (match conj_subst th th'
with
1373 Some th''
-> (s
,th''
,union_wit w w'
)::ts'
1374 | None
-> t'
::(loop' ts'
)) in
1376 | _
-> ([(s
,th
,w
)],cur
@acc
)) in
1378 loop (List.sort
state_compare trips) (* is this sort needed? *) in
1381 (* *************** *)
1382 (* Partial matches *)
1383 (* *************** *)
1385 let filter_conj states unwanted partial_matches
=
1387 triples_conj (triples_complement states (unwitify unwanted
))
1389 triples_conj (unwitify x) (triples_complement states x)
1391 let strict_triples_conj strict
states trips trips'
=
1392 let res = triples_conj trips trips'
in
1393 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1395 let fail_left = filter_conj states trips trips'
in
1396 let fail_right = filter_conj states trips'
trips in
1397 let ors = triples_union fail_left fail_right in
1398 triples_union res ors
1401 let strict_triples_conj_none strict
states trips trips'
=
1402 let res = triples_conj_none trips trips'
in
1403 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1405 let fail_left = filter_conj states trips trips'
in
1406 let fail_right = filter_conj states trips'
trips in
1407 let ors = triples_union fail_left fail_right in
1408 triples_union res ors
1411 let left_strict_triples_conj strict
states trips trips'
=
1412 let res = triples_conj trips trips'
in
1413 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1415 let fail_left = filter_conj states trips trips'
in
1416 triples_union res fail_left
1419 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1420 let res = op dir m
trips required_states
in
1421 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1423 let states = mkstates states required_states
in
1424 let fail = filter_conj states res (failop dir m
trips required_states
) in
1425 triples_union res fail
1428 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1430 let res = op dir m
trips trips' required_states
in
1431 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1433 let states = mkstates states required_states
in
1434 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1435 triples_union res fail
1438 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1439 required_states
print_graph =
1440 match op dir m
trips trips' required_states
print_graph with
1442 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1444 let states = mkstates states required_states
in
1446 filter_conj states res (failop dir m
trips' required_states
) in
1447 AUok
(triples_union res fail)
1449 | AUfailed
res -> AUfailed
res
1451 (* ********************* *)
1452 (* Environment functions *)
1453 (* ********************* *)
1455 let drop_wits required_states s phi
=
1456 match required_states
with
1458 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1461 let print_required required
=
1464 Format.print_string
"{";
1467 print_generic_substitution reqd
; Format.print_newline
())
1469 Format.print_string
"}";
1470 Format.print_newline
())
1475 let extend_required trips required
=
1476 if !Flag_ctl.partial_match
1479 if !pREQUIRED_ENV_OPT
1485 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1487 let envs = if List.mem
[] envs then [] else envs in
1488 match (envs,required
) with
1492 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1497 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1504 match conj_subst t r
with
1505 None
-> rest
| Some th
-> add th rest
)
1509 with Too_long
-> envs :: required
)
1510 | (envs,_
) -> envs :: required
1513 let drop_required v required
=
1514 if !pREQUIRED_ENV_OPT
1521 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1523 (* check whether an entry has become useless *)
1524 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1527 (* no idea how to write this function ... *)
1529 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1531 let satLabel label required p
=
1533 if !pSATLABEL_MEMO_OPT
1536 let states_subs = Hashtbl.find
memo_label p
in
1537 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1540 let triples = setify(label p
) in
1541 Hashtbl.add memo_label p
1542 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1544 else setify(label p
) in
1546 (if !pREQUIRED_ENV_OPT
1550 function ((s
,th
,_
) as t) ->
1552 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1559 let get_required_states l
=
1560 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1562 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1565 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1566 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1568 match required_states
with
1573 A.FORWARD
-> G.successors
1574 | A.BACKWARD
-> G.predecessors in
1575 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1578 let reachable_table =
1579 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1581 (* like satEF, but specialized for get_reachable *)
1582 let reachsatEF dir
(grp
,_
,_
) s2 =
1584 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1585 let union = unionBy compare
(=) in
1586 let rec f y
= function
1589 let (pre_collected
,new_info) =
1590 List.partition (function Common.Left
x -> true | _
-> false)
1593 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1594 with Not_found
-> Common.Right
x)
1599 function Common.Left
x -> union x rest
1600 | _
-> failwith
"not possible")
1604 (function Common.Right
x -> x | _
-> failwith
"not possible")
1606 let first = inner_setify (concatmap (dirop grp
) new_info) in
1607 let new_info = setdiff first y in
1608 let res = new_info @ y in
1610 List.rev
(f s2 s2) (* put root first *)
1612 let get_reachable dir m required_states
=
1613 match required_states
with
1620 if List.mem cur rest
1624 (try Hashtbl.find
reachable_table (cur
,dir
)
1627 let states = reachsatEF dir m
[cur
] in
1628 Hashtbl.add reachable_table (cur
,dir
) states;
1637 Printf.sprintf
"_c%d" c
1639 (* **************************** *)
1640 (* End of environment functions *)
1641 (* **************************** *)
1643 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1645 let rec satloop unchecked required required_states
1646 ((grp
,label,states) as m
) phi env
=
1647 let rec loop unchecked required required_states phi
=
1648 (*Common.profile_code "satloop" (fun _ -> *)
1652 | A.True
-> triples_top states
1653 | A.Pred
(p
) -> satLabel label required p
1654 | A.Uncheck
(phi1
) ->
1655 let unchecked = if !pUNCHECK_OPT then true else false in
1656 loop unchecked required required_states phi1
1658 let phires = loop unchecked required required_states phi
in
1660 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1661 triples_complement (mkstates states required_states
)
1663 | A.Or
(phi1
,phi2
) ->
1665 (loop unchecked required required_states phi1
)
1666 (loop unchecked required required_states phi2
)
1667 | A.SeqOr
(phi1
,phi2
) ->
1668 let res1 = loop unchecked required required_states phi1
in
1669 let res2 = loop unchecked required required_states phi2
in
1670 let res1neg = unwitify res1 in
1673 (triples_complement (mkstates states required_states
) res1neg)
1675 | A.And
(strict
,phi1
,phi2
) ->
1676 (* phi1 is considered to be more likely to be [], because of the
1677 definition of asttoctl. Could use heuristics such as the size of
1679 let pm = !Flag_ctl.partial_match
in
1680 (match (pm,loop unchecked required required_states phi1
) with
1681 (false,[]) when !pLazyOpt -> []
1683 let new_required = extend_required phi1res required
in
1684 let new_required_states = get_required_states phi1res
in
1685 (match (pm,loop unchecked new_required new_required_states phi2
)
1687 (false,[]) when !pLazyOpt -> []
1689 strict_triples_conj strict
1690 (mkstates states required_states
)
1692 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1693 (* phi2 can appear anywhere that is reachable *)
1694 let pm = !Flag_ctl.partial_match
in
1695 (match (pm,loop unchecked required required_states phi1
) with
1698 let new_required = extend_required phi1res required
in
1699 let new_required_states = get_required_states phi1res
in
1700 let new_required_states =
1701 get_reachable dir m
new_required_states in
1702 (match (pm,loop unchecked new_required new_required_states phi2
)
1704 (false,[]) -> phi1res
1707 [] -> (* !Flag_ctl.partial_match must be true *)
1711 let s = mkstates states required_states
in
1713 (function a
-> function b
->
1714 strict_triples_conj strict
s a
[b
])
1715 [List.hd phi2res
] (List.tl phi2res
)
1718 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1719 let s = mkstates states required_states
in
1721 (function a
-> function b
->
1722 strict_triples_conj strict
s a b
)
1726 "only one result allowed for the left arg of AndAny")))
1727 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1728 (* phi2 can appear anywhere that is reachable *)
1729 let pm = !Flag_ctl.partial_match
in
1730 (match (pm,loop unchecked required required_states phi1
) with
1733 let new_required = extend_required phi1res required
in
1734 let new_required_states = get_required_states phi1res
in
1735 let new_required_states =
1736 get_reachable dir m
new_required_states in
1737 (match (pm,loop unchecked new_required new_required_states phi2
)
1739 (false,[]) -> phi1res
1741 (* if there is more than one state, something about the
1742 environment has to ensure that the right triples of
1743 phi2 get associated with the triples of phi1.
1744 the asttoctl2 has to ensure that that is the case.
1745 these should thus be structural properties.
1746 env of phi2 has to be a proper subset of env of phi1
1747 to ensure all end up being consistent. no new triples
1748 should be generated. strict_triples_conj_none takes
1751 let s = mkstates states required_states
in
1754 function (st
,th
,_
) as phi2_elem
->
1756 triples_complement [st
] [(st
,th
,[])] in
1757 strict_triples_conj_none strict
s acc
1758 (phi2_elem
::inverse))
1760 | A.InnerAnd
(phi
) ->
1761 inner_and(loop unchecked required required_states phi
)
1763 let new_required_states =
1764 get_children_required_states dir m required_states
in
1765 satEX dir m
(loop unchecked required
new_required_states phi
)
1767 | A.AX
(dir
,strict
,phi
) ->
1768 let new_required_states =
1769 get_children_required_states dir m required_states
in
1770 let res = loop unchecked required
new_required_states phi
in
1771 strict_A1 strict
satAX satEX dir m
res required_states
1773 let new_required_states = get_reachable dir m required_states
in
1774 satEF dir m
(loop unchecked required
new_required_states phi
)
1776 | A.AF
(dir
,strict
,phi
) ->
1777 if !Flag_ctl.loop_in_src_code
1779 loop unchecked required required_states
1780 (A.AU
(dir
,strict
,A.True
,phi
))
1782 let new_required_states = get_reachable dir m required_states
in
1783 let res = loop unchecked required
new_required_states phi
in
1784 strict_A1 strict
satAF satEF dir m
res new_required_states
1786 let new_required_states = get_reachable dir m required_states
in
1787 satEG dir m
(loop unchecked required
new_required_states phi
)
1789 | A.AG
(dir
,strict
,phi
) ->
1790 let new_required_states = get_reachable dir m required_states
in
1791 let res = loop unchecked required
new_required_states phi
in
1792 strict_A1 strict
satAG satEF dir m
res new_required_states
1793 | A.EU
(dir
,phi1
,phi2
) ->
1794 let new_required_states = get_reachable dir m required_states
in
1795 (match loop unchecked required
new_required_states phi2
with
1796 [] when !pLazyOpt -> []
1798 let new_required = extend_required s2 required
in
1799 let s1 = loop unchecked new_required new_required_states phi1
in
1800 satEU dir m
s1 s2 new_required_states
1801 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1802 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1803 let new_required_states = get_reachable dir m required_states
in
1804 (match loop unchecked required
new_required_states phi2
with
1805 [] when !pLazyOpt -> []
1807 let new_required = extend_required s2 required
in
1808 let s1 = loop unchecked new_required new_required_states phi1
in
1809 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1810 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1811 (*Printf.printf "using AU\n"; flush stdout;*)
1812 let new_required_states = get_reachable dir m required_states
in
1813 (match loop unchecked required
new_required_states phi2
with
1814 [] when !pLazyOpt -> []
1816 let new_required = extend_required s2 required
in
1817 let s1 = loop unchecked new_required new_required_states phi1
in
1819 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1821 print_graph_c grp
new_required_states y ctr phi
) in
1824 | AUfailed tmp_res
->
1825 (* found a loop, have to try AW *)
1827 A[E[phi1 U phi2] & phi1 W phi2]
1828 the and is nonstrict *)
1829 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1830 (*Printf.printf "using AW\n"; flush stdout;*)
1833 (satEU dir m
s1 tmp_res
new_required_states
1834 (* no graph, for the moment *)
1837 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1839 | A.Implies
(phi1
,phi2
) ->
1840 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1841 | A.Exists
(keep
,v
,phi
) ->
1842 let new_required = drop_required v required
in
1843 triples_witness v
unchecked (not keep
)
1844 (loop unchecked new_required required_states phi
)
1845 | A.Let
(v
,phi1
,phi2
) ->
1846 (* should only be used when the properties unchecked, required,
1847 and required_states are known to be the same or at least
1848 compatible between all the uses. this is not checked. *)
1849 let res = loop unchecked required required_states phi1
in
1850 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1851 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1852 (* should only be used when the properties unchecked, required,
1853 and required_states are known to be the same or at least
1854 compatible between all the uses. this is not checked. *)
1855 (* doesn't seem to be used any more *)
1856 let new_required_states = get_reachable dir m required_states
in
1857 let res = loop unchecked required
new_required_states phi1
in
1858 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1860 let res = List.assoc v env
in
1862 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1864 | A.XX
(phi
) -> failwith
"should have been removed" in
1865 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1866 let res = drop_wits required_states
res phi
(* ) *) in
1867 print_graph grp required_states
res "" phi
;
1870 loop unchecked required required_states phi
1874 (* SAT with tracking *)
1875 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1876 ((_
,label,states) as m
) phi env
=
1877 let anno res children
= (annot lvl phi
res children
,res) in
1878 let satv unchecked required required_states phi0 env
=
1879 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1881 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1882 anno (satloop unchecked required required_states m phi env
) []
1886 A.False
-> anno [] []
1887 | A.True
-> anno (triples_top states) []
1889 Printf.printf
"label\n"; flush stdout
;
1890 anno (satLabel label required p
) []
1891 | A.Uncheck
(phi1
) ->
1892 let unchecked = if !pUNCHECK_OPT then true else false in
1893 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1894 Printf.printf
"uncheck\n"; flush stdout
;
1898 satv unchecked required required_states phi1 env
in
1899 Printf.printf
"not\n"; flush stdout
;
1900 anno (triples_complement (mkstates states required_states
) res) [child
]
1901 | A.Or
(phi1
,phi2
) ->
1903 satv unchecked required required_states phi1 env
in
1905 satv unchecked required required_states phi2 env
in
1906 Printf.printf
"or\n"; flush stdout
;
1907 anno (triples_union res1 res2) [child1
; child2
]
1908 | A.SeqOr
(phi1
,phi2
) ->
1910 satv unchecked required required_states phi1 env
in
1912 satv unchecked required required_states phi2 env
in
1914 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1915 Printf.printf
"seqor\n"; flush stdout
;
1916 anno (triples_union res1
1918 (triples_complement (mkstates states required_states
)
1922 | A.And
(strict
,phi1
,phi2
) ->
1923 let pm = !Flag_ctl.partial_match
in
1924 (match (pm,satv unchecked required required_states phi1 env
) with
1925 (false,(child1
,[])) ->
1926 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1927 | (_
,(child1
,res1)) ->
1928 let new_required = extend_required res1 required
in
1929 let new_required_states = get_required_states res1 in
1930 (match (pm,satv unchecked new_required new_required_states phi2
1932 (false,(child2
,[])) ->
1933 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1934 | (_
,(child2
,res2)) ->
1935 Printf.printf
"and\n"; flush stdout
;
1937 strict_triples_conj strict
1938 (mkstates states required_states
)
1940 anno res [child1
; child2
]))
1941 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1942 let pm = !Flag_ctl.partial_match
in
1943 (match (pm,satv unchecked required required_states phi1 env
) with
1944 (false,(child1
,[])) ->
1945 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1946 | (_
,(child1
,res1)) ->
1947 let new_required = extend_required res1 required
in
1948 let new_required_states = get_required_states res1 in
1949 let new_required_states =
1950 get_reachable dir m
new_required_states in
1951 (match (pm,satv unchecked new_required new_required_states phi2
1953 (false,(child2
,[])) ->
1954 Printf.printf
"andany\n"; flush stdout
;
1955 anno res1 [child1
;child2
]
1956 | (_
,(child2
,res2)) ->
1958 [] -> (* !Flag_ctl.partial_match must be true *)
1960 then anno [] [child1
; child2
]
1963 let s = mkstates states required_states
in
1965 (function a
-> function b
->
1966 strict_triples_conj strict
s a
[b
])
1967 [List.hd
res2] (List.tl
res2) in
1968 anno res [child1
; child2
]
1971 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1972 Printf.printf
"andany\n"; flush stdout
;
1974 let s = mkstates states required_states
in
1976 (function a
-> function b
->
1977 strict_triples_conj strict
s a b
)
1979 anno res [child1
; child2
]
1982 "only one result allowed for the left arg of AndAny")))
1983 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1984 let pm = !Flag_ctl.partial_match
in
1985 (match (pm,satv unchecked required required_states phi1 env
) with
1986 (false,(child1
,[])) ->
1987 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1988 | (_
,(child1
,res1)) ->
1989 let new_required = extend_required res1 required
in
1990 let new_required_states = get_required_states res1 in
1991 let new_required_states =
1992 get_reachable dir m
new_required_states in
1993 (match (pm,satv unchecked new_required new_required_states phi2
1995 (false,(child2
,[])) ->
1996 Printf.printf
"andany\n"; flush stdout
;
1997 anno res1 [child1
;child2
]
1998 | (_
,(child2
,res2)) ->
2000 let s = mkstates states required_states
in
2003 function (st
,th
,_
) as phi2_elem
->
2005 triples_complement [st
] [(st
,th
,[])] in
2006 strict_triples_conj_none strict
s acc
2007 (phi2_elem
::inverse))
2009 anno res [child1
; child2
]))
2010 | A.InnerAnd
(phi1
) ->
2011 let (child1
,res1) = satv unchecked required required_states phi1 env
in
2012 Printf.printf
"uncheck\n"; flush stdout
;
2013 anno (inner_and res1) [child1
]
2015 let new_required_states =
2016 get_children_required_states dir m required_states
in
2018 satv unchecked required
new_required_states phi1 env
in
2019 Printf.printf
"EX\n"; flush stdout
;
2020 anno (satEX dir m
res required_states
) [child
]
2021 | A.AX
(dir
,strict
,phi1
) ->
2022 let new_required_states =
2023 get_children_required_states dir m required_states
in
2025 satv unchecked required
new_required_states phi1 env
in
2026 Printf.printf
"AX\n"; flush stdout
;
2027 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2030 let new_required_states = get_reachable dir m required_states
in
2032 satv unchecked required
new_required_states phi1 env
in
2033 Printf.printf
"EF\n"; flush stdout
;
2034 anno (satEF dir m
res new_required_states) [child
]
2035 | A.AF
(dir
,strict
,phi1
) ->
2036 if !Flag_ctl.loop_in_src_code
2038 satv unchecked required required_states
2039 (A.AU
(dir
,strict
,A.True
,phi1
))
2042 (let new_required_states = get_reachable dir m required_states
in
2044 satv unchecked required
new_required_states phi1 env
in
2045 Printf.printf
"AF\n"; flush stdout
;
2047 strict_A1 strict
satAF satEF dir m
res new_required_states in
2050 let new_required_states = get_reachable dir m required_states
in
2052 satv unchecked required
new_required_states phi1 env
in
2053 Printf.printf
"EG\n"; flush stdout
;
2054 anno (satEG dir m
res new_required_states) [child
]
2055 | A.AG
(dir
,strict
,phi1
) ->
2056 let new_required_states = get_reachable dir m required_states
in
2058 satv unchecked required
new_required_states phi1 env
in
2059 Printf.printf
"AG\n"; flush stdout
;
2060 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2063 | A.EU
(dir
,phi1
,phi2
) ->
2064 let new_required_states = get_reachable dir m required_states
in
2065 (match satv unchecked required
new_required_states phi2 env
with
2067 Printf.printf
"EU\n"; flush stdout
;
2070 let new_required = extend_required res2 required
in
2072 satv unchecked new_required new_required_states phi1 env
in
2073 Printf.printf
"EU\n"; flush stdout
;
2074 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2076 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2077 failwith
"should not be used" (*
2078 let new_required_states = get_reachable dir m required_states in
2079 (match satv unchecked required new_required_states phi2 env with
2081 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2083 let new_required = extend_required res2 required in
2085 satv unchecked new_required new_required_states phi1 env in
2086 Printf.printf "AW %b\n" unchecked; flush stdout;
2088 strict_A2 strict satAW satEF dir m res1 res2
2089 new_required_states in
2090 anno res [child1; child2]) *)
2091 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2092 let new_required_states = get_reachable dir m required_states
in
2093 (match satv unchecked required
new_required_states phi2 env
with
2095 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2097 let new_required = extend_required s2 required
in
2099 satv unchecked new_required new_required_states phi1 env
in
2100 Printf.printf
"AU\n"; flush stdout
;
2102 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2103 (fun y str -> ()) in
2106 anno res [child1
; child2
]
2107 | AUfailed tmp_res
->
2108 (* found a loop, have to try AW *)
2110 A[E[phi1 U phi2] & phi1 W phi2]
2111 the and is nonstrict *)
2112 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2113 Printf.printf
"AW\n"; flush stdout
;
2116 (satEU dir m
s1 tmp_res
new_required_states
2117 (* no graph, for the moment *)
2121 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2122 anno res [child1
; child2
]))
2123 | A.Implies
(phi1
,phi2
) ->
2124 satv unchecked required required_states
2125 (A.Or
(A.Not phi1
,phi2
))
2127 | A.Exists
(keep
,v
,phi1
) ->
2128 let new_required = drop_required v required
in
2130 satv unchecked new_required required_states phi1 env
in
2131 Printf.printf
"exists\n"; flush stdout
;
2132 anno (triples_witness v
unchecked (not keep
) res) [child
]
2133 | A.Let
(v
,phi1
,phi2
) ->
2135 satv unchecked required required_states phi1 env
in
2137 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2138 anno res2 [child1
;child2
]
2139 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2140 let new_required_states = get_reachable dir m required_states
in
2142 satv unchecked required
new_required_states phi1 env
in
2144 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2145 anno res2 [child1
;child2
]
2147 Printf.printf
"Ref\n"; flush stdout
;
2148 let res = List.assoc v env
in
2151 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2154 | A.XX
(phi
) -> failwith
"should have been removed" in
2155 let res1 = drop_wits required_states
res phi
in
2159 print_required_states required_states
;
2160 print_state "after drop_wits" res1 end;
2165 let sat_verbose annotate maxlvl lvl m phi
=
2166 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2168 (* Type for annotations collected in a tree *)
2169 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2171 let sat_annotree annotate m phi
=
2172 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2173 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2177 let sat m phi = satloop m phi []
2181 let simpleanno l phi
res =
2183 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2184 print_generic_algo
(List.sort compare
res);
2185 Format.print_string
"\n------------------------------\n\n" in
2186 let pp_dir = function
2188 | A.BACKWARD
-> pp "^" in
2190 | A.False
-> pp "False"
2191 | A.True
-> pp "True"
2192 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2193 | A.Not
(phi
) -> pp "Not"
2194 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2195 | A.And
(_
,phi1
,phi2
) -> pp "And"
2196 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2197 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2198 | A.Or
(phi1
,phi2
) -> pp "Or"
2199 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2200 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2201 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2202 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2203 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2204 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2205 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2206 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2207 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2208 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2209 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2210 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2211 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2212 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2213 | A.Uncheck
(s) -> pp "Uncheck"
2214 | A.InnerAnd
(s) -> pp "InnerAnd"
2215 | A.XX
(phi1
) -> pp "XX"
2219 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2220 print a ctl formula more accurately if you want.
2221 Use the print_xxx provided in the different module to call
2222 Pretty_print_ctl.pp_ctl.
2225 let simpleanno2 l phi
res =
2227 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2228 Format.print_newline
();
2229 Format.print_string
"----------------------------------------------------";
2230 Format.print_newline
();
2231 print_generic_algo
(List.sort compare
res);
2232 Format.print_newline
();
2233 Format.print_string
"----------------------------------------------------";
2234 Format.print_newline
();
2235 Format.print_newline
();
2239 (* ---------------------------------------------------------------------- *)
2241 (* ---------------------------------------------------------------------- *)
2243 type optentry
= bool ref * string
2244 type options
= {label : optentry
; unch
: optentry
;
2245 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2247 reqenv
: optentry
; reqstates
: optentry
}
2250 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2251 unch
= (pUNCHECK_OPT,"uncheck_opt");
2252 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2253 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2254 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2255 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2256 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2257 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2261 ("label ",[options.label]);
2262 ("unch ",[options.unch
]);
2263 ("unch and label ",[options.label;options.unch
])]
2266 [("conj ", [options.conj]);
2267 ("compl1 ", [options.compl1
]);
2268 ("compl12 ", [options.compl1
;options.compl2
]);
2269 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2270 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2272 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2273 ("compl12 unch satl ",
2274 [options.compl1;options.compl2;options.unch;options.label]); *)
2275 ("conj/compl12 unch satl ",
2276 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2279 [("newinfo ", [options.newinfo
]);
2280 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2283 [("reqenv ", [options.reqenv
]);
2284 ("reqstates ", [options.reqstates
]);
2285 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2286 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2287 ("reqstates unch satl ",
2288 [options.reqstates;options.unch;options.label]);*)
2289 ("reqenv/states unch satl ",
2290 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2293 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2294 options.newinfo
;options.reqenv
;options.reqstates
]
2297 [("all ",all_options)]
2299 let all_options_but_path =
2300 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2301 options.reqenv
;options.reqstates
]
2303 let all_but_path = ("all but path ",all_options_but_path)
2306 [(satAW_calls, "satAW", ref 0);
2307 (satAU_calls, "satAU", ref 0);
2308 (satEF_calls, "satEF", ref 0);
2309 (satAF_calls, "satAF", ref 0);
2310 (satEG_calls, "satEG", ref 0);
2311 (satAG_calls, "satAG", ref 0);
2312 (satEU_calls, "satEU", ref 0)]
2316 (function (opt
,x) ->
2317 (opt
,x,ref 0.0,ref 0,
2318 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2319 [List.hd
all;all_but_path]
2320 (*(all@baseline@conjneg@path@required)*)
2324 let rec iter fn = function
2326 | n
-> let _ = fn() in
2327 (Hashtbl.clear
reachable_table;
2328 Hashtbl.clear
memo_label;
2332 let copy_to_stderr fl
=
2333 let i = open_in fl
in
2335 Printf.fprintf stderr
"%s\n" (input_line
i);
2337 try loop() with _ -> ();
2340 let bench_sat (_,_,states) fn =
2341 List.iter (function (opt
,_) -> opt
:= false) all_options;
2344 (function (name
,options,time
,trips,counter_info
) ->
2345 let iterct = !Flag_ctl.bench
in
2346 if !time
> float_of_int
timeout then time
:= -100.0;
2347 if not
(!time
= -100.0)
2350 Hashtbl.clear
reachable_table;
2351 Hashtbl.clear
memo_label;
2352 List.iter (function (opt
,_) -> opt
:= true) options;
2353 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2357 let bef = Sys.time
() in
2359 Common.timeout_function
timeout
2361 let bef = Sys.time
() in
2362 let res = iter fn iterct in
2363 let aft = Sys.time
() in
2364 time
:= !time
+. (aft -. bef);
2365 trips := !trips + !triples;
2367 (function (calls
,_,save_calls
) ->
2368 function (current_calls
,current_cfg
,current_max_cfg
) ->
2370 !current_calls
+ (!calls
- !save_calls
);
2371 if (!calls
- !save_calls
) > 0
2373 (let st = List.length
states in
2374 current_cfg
:= !current_cfg
+ st;
2375 if st > !current_max_cfg
2376 then current_max_cfg
:= st))
2377 counters counter_info
;
2382 let aft = Sys.time
() in
2384 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2388 List.iter (function (opt
,_) -> opt
:= false) options;
2393 Printf.fprintf stderr
"\n";
2397 (if not
(List.for_all
(function x -> x = res) rest
)
2399 (List.iter (print_state "a state") answers;
2400 Printf.printf
"something doesn't work\n");
2404 let iterct = !Flag_ctl.bench
in
2408 (function (name
,options,time
,trips,counter_info
) ->
2409 Printf.fprintf stderr
"%s Numbers: %f %d "
2410 name
(!time
/. (float_of_int
iterct)) !trips;
2412 (function (calls
,cfg
,max_cfg
) ->
2413 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2415 Printf.fprintf stderr
"\n")
2418 (* ---------------------------------------------------------------------- *)
2419 (* preprocessing: ignore irrelevant functions *)
2421 let preprocess (cfg
,_,_) label = function
2422 [] -> true (* no information, try everything *)
2424 let sz = G.size cfg
in
2425 let verbose_output pred = function
2427 Printf.printf
"did not find:\n";
2428 P.print_predicate
pred; Format.print_newline
()
2430 Printf.printf
"found:\n";
2431 P.print_predicate
pred; Format.print_newline
();
2432 Printf.printf
"but it was not enough\n" in
2433 let get_any verbose
x =
2435 try Hashtbl.find
memo_label x
2438 (let triples = label x in
2440 List.map (function (st,th
,_) -> (st,th
)) triples in
2441 Hashtbl.add memo_label x filtered;
2443 if verbose
then verbose_output x res;
2446 (* don't bother testing when there are more patterns than nodes *)
2447 if List.length l
> sz-2
2449 else List.for_all
(get_any false) l
in
2450 if List.exists
get_all l
2453 (if !Flag_ctl.verbose_match
2455 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2459 let filter_partial_matches trips =
2460 if !Flag_ctl.partial_match
2462 let anynegwit = (* if any is neg, then all are *)
2463 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2465 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2468 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2472 (* ---------------------------------------------------------------------- *)
2473 (* Main entry point for engine *)
2474 let sat m phi reqopt
=
2476 (match !Flag_ctl.steps
with
2477 None
-> step_count := 0
2478 | Some
x -> step_count := x);
2479 Hashtbl.clear
reachable_table;
2480 Hashtbl.clear
memo_label;
2481 let (x,label,states) = m
in
2482 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2484 ((* to drop when Yoann initialized this flag *)
2485 if List.exists
(G.extract_is_loop
x) states
2486 then Flag_ctl.loop_in_src_code
:= true;
2487 let m = (x,label,List.sort compare
states) in
2489 if(!Flag_ctl.verbose_ctl_engine
)
2491 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2492 if !Flag_ctl.bench
> 0
2496 let fn _ = satloop false [] None
m phi
[] in
2497 if !Flag_ctl.bench
> 0
2499 else Common.profile_code
"ctl" (fun _ -> fn()) in
2500 let res = filter_partial_matches res in
2502 Printf.printf "steps: start %d, stop %d\n"
2503 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2505 Printf.printf "triples: %d\n" !triples;
2506 print_state "final result" res;
2508 List.sort compare
res)
2510 (if !Flag_ctl.verbose_ctl_engine
2511 then Common.pr2
"missing something required";
2516 (* ********************************************************************** *)
2517 (* End of Module: CTL_ENGINE *)
2518 (* ********************************************************************** *)