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.
26 * Copyright 2010, INRIA, University of Copenhagen
27 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
28 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
29 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
30 * This file is part of Coccinelle.
32 * Coccinelle is free software: you can redistribute it and/or modify
33 * it under the terms of the GNU General Public License as published by
34 * the Free Software Foundation, according to version 2 of the License.
36 * Coccinelle is distributed in the hope that it will be useful,
37 * but WITHOUT ANY WARRANTY; without even the implied warranty of
38 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
39 * GNU General Public License for more details.
41 * You should have received a copy of the GNU General Public License
42 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
44 * The authors reserve the right to distribute this or future versions of
45 * Coccinelle under other licenses.
49 (*external c_counter : unit -> int = "c_counter"*)
51 (* Optimize triples_conj by first extracting the intersection of the two sets,
52 which can certainly be in the intersection *)
53 let pTRIPLES_CONJ_OPT = ref true
54 (* For complement, make NegState for the negation of a single state *)
55 let pTRIPLES_COMPLEMENT_OPT = ref true
56 (* For complement, do something special for the case where the environment
57 and witnesses are empty *)
58 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
59 (* "Double negate" the arguments of the path operators *)
60 let pDOUBLE_NEGATE_OPT = ref true
61 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
62 let pNEW_INFO_OPT = ref true
63 (* Filter the result of the label function to drop entries that aren't
64 compatible with any of the available environments *)
65 let pREQUIRED_ENV_OPT = ref true
66 (* Memoize the raw result of the label function *)
67 let pSATLABEL_MEMO_OPT = ref true
68 (* Filter results according to the required states *)
69 let pREQUIRED_STATES_OPT = ref true
70 (* Drop negative witnesses at Uncheck *)
71 let pUNCHECK_OPT = ref true
72 let pANY_NEG_OPT = ref true
73 let pLazyOpt = ref true
75 (* Nico: This stack is use for graphical traces *)
76 let graph_stack = ref ([] : string list
)
77 let graph_hash = (Hashtbl.create
101)
80 let pTRIPLES_CONJ_OPT = ref false
81 let pTRIPLES_COMPLEMENT_OPT = ref false
82 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
83 let pDOUBLE_NEGATE_OPT = ref false
84 let pNEW_INFO_OPT = ref false
85 let pREQUIRED_ENV_OPT = ref false
86 let pSATLABEL_MEMO_OPT = ref false
87 let pREQUIRED_STATES_OPT = ref false
88 let pUNCHECK_OPT = ref false
89 let pANY_NEG_OPT = ref false
90 let pLazyOpt = ref false
94 let step_count = ref 0
97 if not
(!step_count = 0)
100 step_count := !step_count - 1;
101 if !step_count = 0 then raise Steps
104 let inc cell
= cell
:= !cell
+ 1
106 let satEU_calls = ref 0
107 let satAW_calls = ref 0
108 let satAU_calls = ref 0
109 let satEF_calls = ref 0
110 let satAF_calls = ref 0
111 let satEG_calls = ref 0
112 let satAG_calls = ref 0
120 Printf.sprintf
"_fresh_r_%d" c
122 (* **********************************************************************
124 * Implementation of a Witness Tree model checking engine for CTL-FVex
127 * **********************************************************************)
129 (* ********************************************************************** *)
130 (* Module: SUBST (substitutions: meta. vars and values) *)
131 (* ********************************************************************** *)
137 val eq_mvar
: mvar
-> mvar
-> bool
138 val eq_val
: value -> value -> bool
139 val merge_val
: value -> value -> value
140 val print_mvar
: mvar
-> unit
141 val print_value
: value -> unit
145 (* ********************************************************************** *)
146 (* Module: GRAPH (control flow graphs / model) *)
147 (* ********************************************************************** *)
153 val predecessors
: cfg
-> node
-> node list
154 val successors
: cfg
-> node
-> node list
155 val extract_is_loop
: cfg
-> node
-> bool
156 val print_node
: node
-> unit
157 val size
: cfg
-> int
158 val print_graph
: cfg
-> string option ->
159 (node
* string) list
-> (node
* string) list
-> string -> unit
163 module OGRAPHEXT_GRAPH
=
166 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
167 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
168 let print_node i
= Format.print_string
(Common.i_to_s i
)
172 (* ********************************************************************** *)
173 (* Module: PREDICATE (predicates for CTL formulae) *)
174 (* ********************************************************************** *)
176 module type PREDICATE
=
179 val print_predicate
: t
-> unit
183 (* ********************************************************************** *)
185 (* ---------------------------------------------------------------------- *)
186 (* Misc. useful generic functions *)
187 (* ---------------------------------------------------------------------- *)
189 let get_graph_files () = !graph_stack
190 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
200 let foldl = List.fold_left
;;
202 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
204 type 'a esc
= ESC
of 'a
| CONT
of 'a
206 let foldr = List.fold_right
;;
208 let concat = List.concat;;
212 let filter = List.filter;;
214 let partition = List.partition;;
216 let concatmap f l
= List.concat (List.map f l
);;
224 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
226 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
228 let rec some_tolist opts
=
231 | (Some x
)::rest
-> x
::(some_tolist rest
)
232 | _
::rest
-> some_tolist rest
235 let rec groupBy eq l
=
239 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
240 (x
::xs1
)::(groupBy eq xs2
)
243 let group l
= groupBy (=) l
;;
245 let rec memBy eq x l
=
248 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
251 let rec nubBy eq ls
=
254 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
255 | (x
::xs
) -> x
::(nubBy eq xs
)
261 | (x
::xs
) when (List.mem x xs
) -> nub xs
262 | (x
::xs
) -> x
::(nub xs
)
265 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
267 let setifyBy eq xs
= nubBy eq xs
;;
269 let setify xs
= nub xs
;;
271 let inner_setify xs
= List.sort compare
(nub xs
);;
273 let unionBy compare eq xs
= function
276 let rec loop = function
278 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
279 List.sort compare
(loop xs
)
282 let union xs ys
= unionBy state_compare (=) xs ys
;;
284 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
286 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
288 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
289 let supseteq xs ys
= subseteq ys xs
291 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
293 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
295 (* Fix point calculation *)
297 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
300 (* Fix point calculation on set-valued functions *)
301 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
302 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
304 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
306 (* ********************************************************************** *)
307 (* Module: CTL_ENGINE *)
308 (* ********************************************************************** *)
311 functor (SUB
: SUBST
) ->
312 functor (G
: GRAPH
) ->
313 functor (P
: PREDICATE
) ->
318 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
320 type ('pred
,'anno
) witness
=
321 (G.node
, substitution
,
322 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
323 Ast_ctl.generic_witnesstree
325 type ('pred
,'anno
) triples =
326 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
328 (* ---------------------------------------------------------------------- *)
329 (* Pretty printing functions *)
330 (* ---------------------------------------------------------------------- *)
332 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
333 let print_generic_subst = function
335 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
336 | A.NegSubst
(mvar
, v
) ->
337 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
338 Format.print_string
"[";
339 Common.print_between
(fun () -> Format.print_string
";" )
340 print_generic_subst substxs
;
341 Format.print_string
"]"
343 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
345 | A.Wit
(state
, subst
, anno
, childrens
) ->
346 Format.print_string
"wit ";
348 print_generic_substitution subst
;
349 (match childrens
with
350 [] -> Format.print_string
"{}"
352 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
353 print_generic_witnesstree childrens
; Format.close_box
())
355 Format.print_string
"!";
356 print_generic_witness wit
358 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
361 Format.print_string
"{";
363 (fun () -> Format.print_string
";"; Format.force_newline
() )
364 print_generic_witness witnesstree
;
365 Format.print_string
"}";
368 and print_generic_triple
(node
,subst
,tree
) =
370 print_generic_substitution subst
;
371 print_generic_witnesstree tree
373 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
374 Format.print_string
"<";
376 (fun () -> Format.print_string
";"; Format.force_newline
())
377 print_generic_triple xs
;
378 Format.print_string
">"
381 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
382 Printf.printf
"%s\n" str
;
383 List.iter
(function x ->
384 print_generic_triple
x; Format.print_newline
(); flush stdout
)
385 (List.sort compare l
);
388 let print_required_states = function
389 None
-> Printf.printf
"no required states\n"
391 Printf.printf
"required states: ";
394 G.print_node x; Format.print_string
" "; Format.print_flush
())
398 let mkstates states
= function
400 | Some states
-> states
402 let print_graph grp required_states res str
= function
403 A.Exists
(keep
,v
,phi
) -> ()
405 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
408 | A.Exists
(keep
,v
,phi
) -> ()
411 Printf.sprintf
"%s%s"
413 (Common.format_to_string
415 Pretty_print_ctl.pp_ctl
416 (P.print_predicate
, SUB.print_mvar
)
419 let file = (match !Flag.currentfile
with
420 None
-> "graphical_trace"
423 (if not
(List.mem
file !graph_stack) then
424 graph_stack := file :: !graph_stack);
425 let filename = Filename.temp_file
(file^
":") ".dot" in
426 Hashtbl.add
graph_hash file filename;
428 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
429 (match required_states
with
431 | Some required_states
->
432 (List.map (function s
-> (s
,"blue")) required_states
))
433 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
435 let print_graph_c grp required_states res
ctr phi
=
436 let str = "iter: "^
(string_of_int
!ctr) in
437 print_graph grp required_states res
str phi
439 (* ---------------------------------------------------------------------- *)
441 (* ---------------------------------------------------------------------- *)
444 (* ************************* *)
446 (* ************************* *)
451 | A.NegSubst
(x,_
) -> x
457 | A.NegSubst
(_
,x) -> x
460 let eq_subBy eqx eqv sub sub'
=
461 match (sub
,sub'
) with
462 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
463 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
468 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
470 let eq_subst th th'
= setequalBy eq_sub th th'
;;
472 let merge_subBy eqx
(===) (>+<) sub sub'
=
473 (* variable part is guaranteed to be the same *)
474 match (sub
,sub'
) with
475 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
477 then Some
[A.Subst
(x, v
>+< v'
)]
479 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
481 then Some
[A.Subst
(x'
,v'
)]
483 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
485 then Some
[A.Subst
(x,v
)]
487 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
490 let merged = v
>+< v'
in
491 if merged = v
&& merged = v'
492 then Some
[A.NegSubst
(x,v
>+< v'
)]
494 (* positions are compatible, but not identical. keep apart. *)
495 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
496 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
500 (* How could we accomadate subterm constraints here??? *)
501 let merge_sub sub sub'
=
502 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
504 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
506 (* NOTE: we sort by using the generic "compare" on (meta-)variable
507 * names; we could also require a definition of compare for meta-variables
508 * or substitutions but that seems like overkill for sorting
510 let clean_subst theta
=
514 let res = compare
(dom_sub s
) (dom_sub s'
) in
518 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
519 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
520 | _
-> compare
(ran_sub s
) (ran_sub s'
)
523 let rec loop = function
525 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
526 loop (A.Subst
(x,v
)::rest
)
527 | x::xs
-> x::(loop xs
) in
530 let top_subst = [];; (* Always TRUE subst. *)
532 (* Split a theta in two parts: one with (only) "x" and one without *)
534 let split_subst theta
x =
535 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
537 exception SUBST_MISMATCH
538 let conj_subst theta theta'
=
539 match (theta
,theta'
) with
540 | ([],_
) -> Some theta'
541 | (_
,[]) -> Some theta
543 let rec classify = function
545 | [x] -> [(dom_sub x,[x])]
547 (match classify xs
with
548 ((nm
,y
)::ys
) as res ->
551 else (dom_sub x,[x])::res
552 | _
-> failwith
"not possible") in
553 let merge_all theta theta'
=
560 match (merge_sub sub sub'
) with
561 Some subs
-> subs
@ rest
562 | _
-> raise SUBST_MISMATCH
)
565 let rec loop = function
567 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
569 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
570 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
571 (match compare
x y
with
572 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
573 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
574 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
575 | _
-> failwith
"not possible") in
576 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
577 with SUBST_MISMATCH
-> None
580 (* theta' must be a subset of theta *)
581 let conj_subst_none theta theta'
=
582 match (theta
,theta'
) with
583 | (_
,[]) -> Some theta
586 let rec classify = function
588 | [x] -> [(dom_sub x,[x])]
590 (match classify xs
with
591 ((nm
,y
)::ys
) as res ->
594 else (dom_sub x,[x])::res
595 | _
-> failwith
"not possible") in
596 let merge_all theta theta'
=
603 match (merge_sub sub sub'
) with
604 Some subs
-> subs
@ rest
605 | _
-> raise SUBST_MISMATCH
)
608 let rec loop = function
610 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
611 | ([],ctheta'
) -> raise SUBST_MISMATCH
612 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
613 (match compare
x y
with
614 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
615 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
616 | 1 -> raise SUBST_MISMATCH
617 | _
-> failwith
"not possible") in
618 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
619 with SUBST_MISMATCH
-> None
624 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
625 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
628 (* Turn a (big) theta into a list of (small) thetas *)
629 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
632 (* ************************* *)
634 (* ************************* *)
636 (* Always TRUE witness *)
637 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
639 let eq_wit wit wit'
= wit
= wit'
;;
641 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
642 let res = unionBy compare
(=) wit wit'
in
643 let anynegwit = (* if any is neg, then all are *)
644 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
646 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
649 let negate_wit wit
= A.NegWit wit
(*
651 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
652 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
655 let negate_wits wits
=
656 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
659 let anynegwit = (* if any is neg, then all are *)
660 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
664 function (s
,th
,wit
) ->
665 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
668 (* ************************* *)
670 (* ************************* *)
672 (* Triples are equal when the constituents are equal *)
673 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
674 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
676 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
678 let normalize trips
=
680 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
684 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
685 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
686 let triples_conj trips trips'
=
687 let (trips
,shared
,trips'
) =
688 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
691 List.partition (function t
-> List.mem t trips'
) trips
in
693 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
694 (trips,shared
,trips'
)
695 else (trips,[],trips'
) in
696 foldl (* returns a set - setify inlined *)
698 function (s1
,th1
,wit1
) ->
701 function (s2
,th2
,wit2
) ->
703 (match (conj_subst th1 th2
) with
705 let t = (s1
,th
,union_wit wit1 wit2
) in
706 if List.mem
t rest
then rest
else t::rest
713 (* ignore the state in the right argument. always pretend it is the same as
715 (* env on right has to be a subset of env on left *)
716 let triples_conj_none trips trips'
=
717 let (trips,shared
,trips'
) =
718 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
721 List.partition (function t -> List.mem
t trips'
) trips in
723 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
724 (trips,shared
,trips'
)
725 else (trips,[],trips'
) in
726 foldl (* returns a set - setify inlined *)
728 function (s1
,th1
,wit1
) ->
731 function (s2
,th2
,wit2
) ->
732 match (conj_subst_none th1 th2
) with
734 let t = (s1
,th
,union_wit wit1 wit2
) in
735 if List.mem
t rest
then rest
else t::rest
743 let triples_conj_AW trips trips'
=
744 let (trips,shared
,trips'
) =
745 if false && !pTRIPLES_CONJ_OPT
748 List.partition (function t -> List.mem
t trips'
) trips in
750 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
751 (trips,shared
,trips'
)
752 else (trips,[],trips'
) in
753 foldl (* returns a set - setify inlined *)
755 function (s1
,th1
,wit1
) ->
758 function (s2
,th2
,wit2
) ->
760 (match (conj_subst th1 th2
) with
762 let t = (s1
,th
,union_wit wit1 wit2
) in
763 if List.mem
t rest
then rest
else t::rest
770 (* *************************** *)
771 (* NEGATION (NegState style) *)
772 (* *************************** *)
774 (* Constructive negation at the state level *)
777 | NegState
of 'a list
780 let compatible_states = function
781 (PosState s1
, PosState s2
) ->
782 if s1
= s2
then Some
(PosState s1
) else None
783 | (PosState s1
, NegState s2
) ->
784 if List.mem s1 s2
then None
else Some
(PosState s1
)
785 | (NegState s1
, PosState s2
) ->
786 if List.mem s2 s1
then None
else Some
(PosState s2
)
787 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
790 (* Conjunction on triples with "special states" *)
791 let triples_state_conj trips trips'
=
792 let (trips,shared
,trips'
) =
793 if !pTRIPLES_CONJ_OPT
796 List.partition (function t -> List.mem
t trips'
) trips in
798 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
799 (trips,shared
,trips'
)
800 else (trips,[],trips'
) in
803 function (s1
,th1
,wit1
) ->
806 function (s2
,th2
,wit2
) ->
807 match compatible_states(s1
,s2
) with
809 (match (conj_subst th1 th2
) with
811 let t = (s
,th
,union_wit wit1 wit2
) in
812 if List.mem
t rest
then rest
else t::rest
819 let triple_negate (s
,th
,wits
) =
820 let negstates = (NegState
[s
],top_subst,top_wit) in
821 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
822 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
823 negstates :: (negths @ negwits) (* all different *)
825 (* FIX ME: it is not necessary to do full conjunction *)
826 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
827 if !pTRIPLES_COMPLEMENT_OPT
829 (let cleanup (s
,th
,wit
) =
831 PosState s'
-> [(s'
,th
,wit
)]
833 assert (th
=top_subst);
834 assert (wit
=top_wit);
835 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
836 let (simple
,complex
) =
837 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
839 let (simple
,complex
) =
840 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
842 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
843 top_subst,top_wit)] in
845 else ([(NegState
[],top_subst,top_wit)],trips) in
846 let rec compl trips =
849 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
850 let compld = (compl complex
) in
851 let compld = concatmap cleanup compld in
854 let negstates (st
,th
,wits
) =
855 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
856 let negths (st
,th
,wits
) =
857 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
858 let negwits (st
,th
,wits
) =
859 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
861 [] -> map (function st
-> (st
,top_subst,top_wit)) states
867 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
868 (negstates x @ negths x @ negwits x) xs
)
871 let triple_negate (s
,th
,wits
) =
872 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
873 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
874 ([s
], negths @ negwits) (* all different *)
876 let print_compl_state str (n
,p
) =
877 Printf.printf
"%s neg: " str;
879 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
884 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
886 then map (function st
-> (st
,top_subst,top_wit)) states
888 let cleanup (neg
,pos
) =
890 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
891 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
893 let trips = List.sort
state_compare trips in
894 let all_negated = List.map triple_negate trips in
895 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
896 let (pos1conj
,pos1keep
) =
897 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
898 let (pos2conj
,pos2keep
) =
899 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
900 (Common.union_set neg1 neg2
,
901 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
902 let rec inner_loop = function
903 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
905 let rec outer_loop = function
907 | l
-> outer_loop (inner_loop l
) in
908 cleanup (outer_loop all_negated)
910 (* ********************************** *)
911 (* END OF NEGATION (NegState style) *)
912 (* ********************************** *)
914 (* now this is always true, so we could get rid of it *)
915 let something_dropped = ref true
917 let triples_union trips trips'
=
918 (*unionBy compare eq_trip trips trips';;*)
919 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
921 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
922 Then, the following says that since the first is a more restrictive
923 environment and has fewer witnesses, then it should be dropped. But having
924 fewer witnesses is not necessarily less informative than having more,
925 because fewer witnesses can mean the absence of the witness-causing thing.
926 So the fewer witnesses have to be kept around.
927 subseteq changed to = to make it hopefully work
932 something_dropped := false;
934 then (something_dropped := true; trips)
936 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
939 (match conj_subst th1 th2
with
942 then if (*subseteq*) wit1
= wit2
then 1 else 0
945 then if (*subseteq*) wit2
= wit1
then (-1) else 0
949 let rec first_loop second
= function
951 | x::xs
-> first_loop (second_loop
x second
) xs
952 and second_loop
x = function
955 match subsumes x y
with
956 1 -> something_dropped := true; all
957 | (-1) -> second_loop
x ys
958 | _
-> y
::(second_loop
x ys
) in
959 first_loop trips trips'
961 else unionBy compare
eq_trip trips trips'
964 let triples_witness x unchecked not_keep
trips =
965 let anyneg = (* if any is neg, then all are *)
966 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
967 let anynegwit = (* if any is neg, then all are *)
968 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
969 let allnegwit = (* if any is neg, then all are *)
970 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
972 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
976 function (s
,th
,wit
) as t ->
977 let (th_x
,newth
) = split_subst th
x in
980 (* one consider whether if not not_keep is true, then we should
981 fail. but it could be that the variable is a used_after and
982 then it is the later rule that should fail and not this one *)
983 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
985 (SUB.print_mvar
x; Format.print_flush
();
986 print_state ": empty witness from" [t]);
988 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
989 (* see tests/nestseq for how neg bindings can come up even
990 without eg partial matches
991 (* negated substitution only allowed with negwits.
993 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
996 (print_generic_substitution l
; Format.print_newline
();
997 failwith
"unexpected negative binding with positive witnesses")*)
1000 if unchecked
or not_keep
1003 if anynegwit wit
&& allnegwit wit
1004 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
1005 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
1008 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
1014 (* ---------------------------------------------------------------------- *)
1015 (* SAT - Model Checking Algorithm for CTL-FVex *)
1017 (* TODO: Implement _all_ operators (directly) *)
1018 (* ---------------------------------------------------------------------- *)
1021 (* ************************************* *)
1022 (* The SAT algorithm and special helpers *)
1023 (* ************************************* *)
1025 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1027 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1028 let exp (s
,th
,wit
) =
1030 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1032 A.FORWARD
-> G.predecessors grp s
1033 | A.BACKWARD
-> G.successors grp s
) in
1034 setify (concatmap exp y
)
1039 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1042 None
-> true | Some reqst
-> List.mem s reqst
in
1045 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1048 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1051 (function p
-> (p
,succ grp p
))
1054 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1055 (* would a hash table be more efficient? *)
1056 let all = List.sort
state_compare all in
1057 let rec up_nodes child s
= function
1059 | (s1
,th
,wit
)::xs
->
1060 (match compare s1 child
with
1061 -1 -> up_nodes child s xs
1062 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1064 let neighbor_triples =
1067 function (s
,children
) ->
1071 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1075 match neighbor_triples with
1079 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1081 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1084 None
-> true | Some reqst
-> List.mem s reqst
in
1087 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1090 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1093 (function p
-> (p
,succ grp p
))
1096 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1097 (* would a hash table be more efficient? *)
1098 let all = List.sort
state_compare all in
1099 let rec up_nodes child s
= function
1101 | (s1
,th
,wit
)::xs
->
1102 (match compare s1 child
with
1103 -1 -> up_nodes child s xs
1104 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1106 let neighbor_triples =
1109 function (s
,children
) ->
1112 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1115 match neighbor_triples with
1117 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1119 (* drop_negwits will call setify *)
1120 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1122 let satAX dir m s reqst
= pre_forall dir m s s reqst
1125 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1126 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1127 (*Printf.printf "EU\n";
1128 let ctr = ref 0 in*)
1133 (*let ctr = ref 0 in*)
1136 let rec f y new_info
=
1142 print_graph y ctr;*)
1143 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1144 let res = triples_union first y
in
1145 let new_info = setdiff res y
in
1146 (*Printf.printf "iter %d res %d new_info %d\n"
1147 !ctr (List.length res) (List.length new_info);
1148 print_state "res" res;
1149 print_state "new_info" new_info;
1157 print_graph y ctr;*)
1158 let pre = pre_exist dir m y reqst
in
1159 triples_union s2
(triples_conj s1
pre) in
1163 (* EF phi == E[true U phi] *)
1164 let satEF dir m s2 reqst
=
1166 (*let ctr = ref 0 in*)
1169 let rec f y
new_info =
1175 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1176 let first = pre_exist dir m
new_info reqst
in
1177 let res = triples_union first y
in
1178 let new_info = setdiff res y
in
1179 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1180 (if dir = A.BACKWARD then "reachable" else "real ef")
1181 !ctr (List.length res) (List.length new_info);
1182 print_state "new info" new_info;
1189 let pre = pre_exist dir m y reqst
in
1190 triples_union s2
pre in
1194 type ('
pred,'anno
) auok
=
1195 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1197 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1198 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1204 (*let ctr = ref 0 in*)
1206 if !Flag_ctl.loop_in_src_code
1211 let rec f y newinfo
=
1217 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1221 try Some
(pre_forall dir m
new_info y reqst
)
1226 match triples_conj s1
pre with
1229 (*print_state "s1" s1;
1230 print_state "pre" pre;
1231 print_state "first" first;*)
1232 let res = triples_union first y
in
1234 if not
!something_dropped
1236 else setdiff res y
in
1238 "iter %d res %d new_info %d\n"
1239 !ctr (List.length res) (List.length new_info);
1244 if !Flag_ctl.loop_in_src_code
1248 fix (function s1 -> function s2 ->
1249 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1250 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1251 subseteq s1 s2) in for popl *)
1256 let pre = pre_forall dir m y y reqst
in
1257 triples_union s2 (triples_conj s1 pre) in
1262 (* reqst could be the states of s1 *)
1264 let lstates = mkstates states reqst in
1265 let initial_removed =
1266 triples_complement lstates (triples_union s1 s2) in
1267 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1268 let rec loop base removed =
1270 triples_conj base (pre_exist dir m removed reqst) in
1272 triples_conj base (triples_complement lstates new_removed) in
1273 if supseteq new_base base
1274 then triples_union base s2
1275 else loop new_base new_removed in
1276 loop initial_base initial_removed *)
1278 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1284 This works extremely badly when the region is small and the end of the
1285 region is very ambiguous, eg free(x) ... x
1289 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1290 let ostates = Common.union_set (get_states s1) (get_states s2) in
1293 A.FORWARD -> G.successors grp
1294 | A.BACKWARD -> G.predecessors grp) in
1296 List.fold_left Common.union_set ostates (List.map succ ostates) in
1297 let negphi = triples_complement states s1 in
1298 let negpsi = triples_complement states s2 in
1299 triples_complement ostates
1300 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1303 (*let ctr = ref 0 in*)
1307 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1310 let pre = pre_forall dir m y y reqst
in
1311 (*print_state "pre" pre;*)
1312 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1313 triples_union s2 conj in
1314 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1315 (* drop wits on s1 represents that we don't want any witnesses from
1316 the case that infinitely loops, only from the case that gets
1317 out of the loop. s1 is like a guard. To see the problem, consider
1318 an example where both s1 and s2 match some code after the loop.
1319 we only want the witness from s2. *)
1320 setgfix f (triples_union (nub(drop_wits s1)) s2)
1323 let satAF dir m s reqst
=
1327 let rec f y newinfo
=
1332 let first = pre_forall dir m
new_info y reqst
in
1333 let res = triples_union first y
in
1334 let new_info = setdiff res y
in
1340 let pre = pre_forall dir m y y reqst
in
1341 triples_union s
pre in
1344 let satAG dir
((_
,_
,states) as m
) s reqst
=
1348 let pre = pre_forall dir m y y reqst
in
1349 triples_conj y
pre in
1352 let satEG dir
((_
,_
,states) as m
) s reqst
=
1356 let pre = pre_exist dir m y reqst
in
1357 triples_conj y
pre in
1360 (* **************************************************************** *)
1361 (* Inner And - a way of dealing with multiple matches within a node *)
1362 (* **************************************************************** *)
1363 (* applied to the result of matching a node. collect witnesses when the
1364 states and environments are the same *)
1365 (* not a good idea, poses problem for unparsing, because don't realize that
1366 adjacent things come from different matches, leading to loss of newlines etc.
1367 exple struct I { ... - int x; + int y; ...} *)
1369 let inner_and trips = trips (*
1370 let rec loop = function
1372 | (s,th,w)::trips ->
1373 let (cur,acc) = loop trips in
1375 (s',_,_)::_ when s = s' ->
1376 let rec loop' = function
1378 | ((_,th',w') as t')::ts' ->
1379 (match conj_subst th th' with
1380 Some th'' -> (s,th'',union_wit w w')::ts'
1381 | None -> t'::(loop' ts')) in
1383 | _ -> ([(s,th,w)],cur@acc)) in
1385 loop (List.sort state_compare trips) (* is this sort needed? *) in
1388 (* *************** *)
1389 (* Partial matches *)
1390 (* *************** *)
1392 let filter_conj states unwanted partial_matches
=
1394 triples_conj (triples_complement states (unwitify unwanted
))
1396 triples_conj (unwitify x) (triples_complement states x)
1398 let strict_triples_conj strict
states trips trips'
=
1399 let res = triples_conj trips trips'
in
1400 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1402 let fail_left = filter_conj states trips trips'
in
1403 let fail_right = filter_conj states trips'
trips in
1404 let ors = triples_union fail_left fail_right in
1405 triples_union res ors
1408 let strict_triples_conj_none strict
states trips trips'
=
1409 let res = triples_conj_none trips trips'
in
1410 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1412 let fail_left = filter_conj states trips trips'
in
1413 let fail_right = filter_conj states trips'
trips in
1414 let ors = triples_union fail_left fail_right in
1415 triples_union res ors
1418 let left_strict_triples_conj strict
states trips trips'
=
1419 let res = triples_conj trips trips'
in
1420 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1422 let fail_left = filter_conj states trips trips'
in
1423 triples_union res fail_left
1426 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1427 let res = op dir m
trips required_states
in
1428 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1430 let states = mkstates states required_states
in
1431 let fail = filter_conj states res (failop dir m
trips required_states
) in
1432 triples_union res fail
1435 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1437 let res = op dir m
trips trips' required_states
in
1438 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1440 let states = mkstates states required_states
in
1441 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1442 triples_union res fail
1445 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1446 required_states
print_graph =
1447 match op dir m
trips trips' required_states
print_graph with
1449 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1451 let states = mkstates states required_states
in
1453 filter_conj states res (failop dir m
trips' required_states
) in
1454 AUok
(triples_union res fail)
1456 | AUfailed
res -> AUfailed
res
1458 (* ********************* *)
1459 (* Environment functions *)
1460 (* ********************* *)
1462 let drop_wits required_states s phi
=
1463 match required_states
with
1465 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1468 let print_required required
=
1471 Format.print_string
"{";
1474 print_generic_substitution reqd
; Format.print_newline
())
1476 Format.print_string
"}";
1477 Format.print_newline
())
1482 let extend_required trips required
=
1483 if !Flag_ctl.partial_match
1486 if !pREQUIRED_ENV_OPT
1492 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1494 let envs = if List.mem
[] envs then [] else envs in
1495 match (envs,required
) with
1499 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1504 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1511 match conj_subst t r
with
1512 None
-> rest
| Some th
-> add th rest
)
1516 with Too_long
-> envs :: required
)
1517 | (envs,_
) -> envs :: required
1520 let drop_required v required
=
1521 if !pREQUIRED_ENV_OPT
1528 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1530 (* check whether an entry has become useless *)
1531 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1534 (* no idea how to write this function ... *)
1536 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1538 let satLabel label required p
=
1540 if !pSATLABEL_MEMO_OPT
1543 let states_subs = Hashtbl.find
memo_label p
in
1544 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1547 let triples = setify(label p
) in
1548 Hashtbl.add memo_label p
1549 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1551 else setify(label p
) in
1553 (if !pREQUIRED_ENV_OPT
1557 function ((s
,th
,_
) as t) ->
1559 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1566 let get_required_states l
=
1567 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1569 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1572 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1573 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1575 match required_states
with
1580 A.FORWARD
-> G.successors
1581 | A.BACKWARD
-> G.predecessors in
1582 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1585 let reachable_table =
1586 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1588 (* like satEF, but specialized for get_reachable *)
1589 let reachsatEF dir
(grp
,_
,_
) s2 =
1591 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1592 let union = unionBy compare
(=) in
1593 let rec f y
= function
1596 let (pre_collected
,new_info) =
1597 List.partition (function Common.Left
x -> true | _
-> false)
1600 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1601 with Not_found
-> Common.Right
x)
1606 function Common.Left
x -> union x rest
1607 | _
-> failwith
"not possible")
1611 (function Common.Right
x -> x | _
-> failwith
"not possible")
1613 let first = inner_setify (concatmap (dirop grp
) new_info) in
1614 let new_info = setdiff first y in
1615 let res = new_info @ y in
1617 List.rev
(f s2 s2) (* put root first *)
1619 let get_reachable dir m required_states
=
1620 match required_states
with
1627 if List.mem cur rest
1631 (try Hashtbl.find
reachable_table (cur
,dir
)
1634 let states = reachsatEF dir m
[cur
] in
1635 Hashtbl.add reachable_table (cur
,dir
) states;
1644 Printf.sprintf
"_c%d" c
1646 (* **************************** *)
1647 (* End of environment functions *)
1648 (* **************************** *)
1650 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1652 let rec satloop unchecked required required_states
1653 ((grp
,label,states) as m
) phi env
=
1654 let rec loop unchecked required required_states phi
=
1655 (*Common.profile_code "satloop" (fun _ -> *)
1659 | A.True
-> triples_top states
1660 | A.Pred
(p
) -> satLabel label required p
1661 | A.Uncheck
(phi1
) ->
1662 let unchecked = if !pUNCHECK_OPT then true else false in
1663 loop unchecked required required_states phi1
1665 let phires = loop unchecked required required_states phi
in
1667 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1668 triples_complement (mkstates states required_states
)
1670 | A.Or
(phi1
,phi2
) ->
1672 (loop unchecked required required_states phi1
)
1673 (loop unchecked required required_states phi2
)
1674 | A.SeqOr
(phi1
,phi2
) ->
1675 let res1 = loop unchecked required required_states phi1
in
1676 let res2 = loop unchecked required required_states phi2
in
1677 let res1neg = unwitify res1 in
1680 (triples_complement (mkstates states required_states
) res1neg)
1682 | A.And
(strict
,phi1
,phi2
) ->
1683 (* phi1 is considered to be more likely to be [], because of the
1684 definition of asttoctl. Could use heuristics such as the size of
1686 let pm = !Flag_ctl.partial_match
in
1687 (match (pm,loop unchecked required required_states phi1
) with
1688 (false,[]) when !pLazyOpt -> []
1690 let new_required = extend_required phi1res required
in
1691 let new_required_states = get_required_states phi1res
in
1692 (match (pm,loop unchecked new_required new_required_states phi2
)
1694 (false,[]) when !pLazyOpt -> []
1696 strict_triples_conj strict
1697 (mkstates states required_states
)
1699 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1700 (* phi2 can appear anywhere that is reachable *)
1701 let pm = !Flag_ctl.partial_match
in
1702 (match (pm,loop unchecked required required_states phi1
) with
1705 let new_required = extend_required phi1res required
in
1706 let new_required_states = get_required_states phi1res
in
1707 let new_required_states =
1708 get_reachable dir m
new_required_states in
1709 (match (pm,loop unchecked new_required new_required_states phi2
)
1711 (false,[]) -> phi1res
1714 [] -> (* !Flag_ctl.partial_match must be true *)
1718 let s = mkstates states required_states
in
1720 (function a
-> function b
->
1721 strict_triples_conj strict
s a
[b
])
1722 [List.hd phi2res
] (List.tl phi2res
)
1725 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1726 let s = mkstates states required_states
in
1728 (function a
-> function b
->
1729 strict_triples_conj strict
s a b
)
1733 "only one result allowed for the left arg of AndAny")))
1734 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1735 (* phi2 can appear anywhere that is reachable *)
1736 let pm = !Flag_ctl.partial_match
in
1737 (match (pm,loop unchecked required required_states phi1
) with
1740 let new_required = extend_required phi1res required
in
1741 let new_required_states = get_required_states phi1res
in
1742 let new_required_states =
1743 get_reachable dir m
new_required_states in
1744 (match (pm,loop unchecked new_required new_required_states phi2
)
1746 (false,[]) -> phi1res
1748 (* if there is more than one state, something about the
1749 environment has to ensure that the right triples of
1750 phi2 get associated with the triples of phi1.
1751 the asttoctl2 has to ensure that that is the case.
1752 these should thus be structural properties.
1753 env of phi2 has to be a proper subset of env of phi1
1754 to ensure all end up being consistent. no new triples
1755 should be generated. strict_triples_conj_none takes
1758 let s = mkstates states required_states
in
1761 function (st
,th
,_
) as phi2_elem
->
1763 triples_complement [st
] [(st
,th
,[])] in
1764 strict_triples_conj_none strict
s acc
1765 (phi2_elem
::inverse))
1767 | A.InnerAnd
(phi
) ->
1768 inner_and(loop unchecked required required_states phi
)
1770 let new_required_states =
1771 get_children_required_states dir m required_states
in
1772 satEX dir m
(loop unchecked required
new_required_states phi
)
1774 | A.AX
(dir
,strict
,phi
) ->
1775 let new_required_states =
1776 get_children_required_states dir m required_states
in
1777 let res = loop unchecked required
new_required_states phi
in
1778 strict_A1 strict
satAX satEX dir m
res required_states
1780 let new_required_states = get_reachable dir m required_states
in
1781 satEF dir m
(loop unchecked required
new_required_states phi
)
1783 | A.AF
(dir
,strict
,phi
) ->
1784 if !Flag_ctl.loop_in_src_code
1786 loop unchecked required required_states
1787 (A.AU
(dir
,strict
,A.True
,phi
))
1789 let new_required_states = get_reachable dir m required_states
in
1790 let res = loop unchecked required
new_required_states phi
in
1791 strict_A1 strict
satAF satEF dir m
res new_required_states
1793 let new_required_states = get_reachable dir m required_states
in
1794 satEG dir m
(loop unchecked required
new_required_states phi
)
1796 | A.AG
(dir
,strict
,phi
) ->
1797 let new_required_states = get_reachable dir m required_states
in
1798 let res = loop unchecked required
new_required_states phi
in
1799 strict_A1 strict
satAG satEF dir m
res new_required_states
1800 | A.EU
(dir
,phi1
,phi2
) ->
1801 let new_required_states = get_reachable dir m required_states
in
1802 (match loop unchecked required
new_required_states phi2
with
1803 [] when !pLazyOpt -> []
1805 let new_required = extend_required s2 required
in
1806 let s1 = loop unchecked new_required new_required_states phi1
in
1807 satEU dir m
s1 s2 new_required_states
1808 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1809 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1810 let new_required_states = get_reachable dir m required_states
in
1811 (match loop unchecked required
new_required_states phi2
with
1812 [] when !pLazyOpt -> []
1814 let new_required = extend_required s2 required
in
1815 let s1 = loop unchecked new_required new_required_states phi1
in
1816 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1817 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1818 (*Printf.printf "using AU\n"; flush stdout;*)
1819 let new_required_states = get_reachable dir m required_states
in
1820 (match loop unchecked required
new_required_states phi2
with
1821 [] when !pLazyOpt -> []
1823 let new_required = extend_required s2 required
in
1824 let s1 = loop unchecked new_required new_required_states phi1
in
1826 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1828 print_graph_c grp
new_required_states y ctr phi
) in
1831 | AUfailed tmp_res
->
1832 (* found a loop, have to try AW *)
1834 A[E[phi1 U phi2] & phi1 W phi2]
1835 the and is nonstrict *)
1836 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1837 (*Printf.printf "using AW\n"; flush stdout;*)
1840 (satEU dir m
s1 tmp_res
new_required_states
1841 (* no graph, for the moment *)
1844 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1846 | A.Implies
(phi1
,phi2
) ->
1847 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1848 | A.Exists
(keep
,v
,phi
) ->
1849 let new_required = drop_required v required
in
1850 triples_witness v
unchecked (not keep
)
1851 (loop unchecked new_required required_states phi
)
1852 | A.Let
(v
,phi1
,phi2
) ->
1853 (* should only be used when the properties unchecked, required,
1854 and required_states are known to be the same or at least
1855 compatible between all the uses. this is not checked. *)
1856 let res = loop unchecked required required_states phi1
in
1857 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1858 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1859 (* should only be used when the properties unchecked, required,
1860 and required_states are known to be the same or at least
1861 compatible between all the uses. this is not checked. *)
1862 (* doesn't seem to be used any more *)
1863 let new_required_states = get_reachable dir m required_states
in
1864 let res = loop unchecked required
new_required_states phi1
in
1865 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1867 let res = List.assoc v env
in
1869 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1871 | A.XX
(phi
) -> failwith
"should have been removed" in
1872 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1873 let res = drop_wits required_states
res phi
(* ) *) in
1874 print_graph grp required_states
res "" phi
;
1877 loop unchecked required required_states phi
1881 (* SAT with tracking *)
1882 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1883 ((_
,label,states) as m
) phi env
=
1884 let anno res children
= (annot lvl phi
res children
,res) in
1885 let satv unchecked required required_states phi0 env
=
1886 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1888 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1889 anno (satloop unchecked required required_states m phi env
) []
1893 A.False
-> anno [] []
1894 | A.True
-> anno (triples_top states) []
1896 Printf.printf
"label\n"; flush stdout
;
1897 anno (satLabel label required p
) []
1898 | A.Uncheck
(phi1
) ->
1899 let unchecked = if !pUNCHECK_OPT then true else false in
1900 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1901 Printf.printf
"uncheck\n"; flush stdout
;
1905 satv unchecked required required_states phi1 env
in
1906 Printf.printf
"not\n"; flush stdout
;
1907 anno (triples_complement (mkstates states required_states
) res) [child
]
1908 | A.Or
(phi1
,phi2
) ->
1910 satv unchecked required required_states phi1 env
in
1912 satv unchecked required required_states phi2 env
in
1913 Printf.printf
"or\n"; flush stdout
;
1914 anno (triples_union res1 res2) [child1
; child2
]
1915 | A.SeqOr
(phi1
,phi2
) ->
1917 satv unchecked required required_states phi1 env
in
1919 satv unchecked required required_states phi2 env
in
1921 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1922 Printf.printf
"seqor\n"; flush stdout
;
1923 anno (triples_union res1
1925 (triples_complement (mkstates states required_states
)
1929 | A.And
(strict
,phi1
,phi2
) ->
1930 let pm = !Flag_ctl.partial_match
in
1931 (match (pm,satv unchecked required required_states phi1 env
) with
1932 (false,(child1
,[])) ->
1933 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1934 | (_
,(child1
,res1)) ->
1935 let new_required = extend_required res1 required
in
1936 let new_required_states = get_required_states res1 in
1937 (match (pm,satv unchecked new_required new_required_states phi2
1939 (false,(child2
,[])) ->
1940 Printf.printf
"and\n"; flush stdout
; anno [] [child1
;child2
]
1941 | (_
,(child2
,res2)) ->
1942 Printf.printf
"and\n"; flush stdout
;
1944 strict_triples_conj strict
1945 (mkstates states required_states
)
1947 anno res [child1
; child2
]))
1948 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1949 let pm = !Flag_ctl.partial_match
in
1950 (match (pm,satv unchecked required required_states phi1 env
) with
1951 (false,(child1
,[])) ->
1952 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1953 | (_
,(child1
,res1)) ->
1954 let new_required = extend_required res1 required
in
1955 let new_required_states = get_required_states res1 in
1956 let new_required_states =
1957 get_reachable dir m
new_required_states in
1958 (match (pm,satv unchecked new_required new_required_states phi2
1960 (false,(child2
,[])) ->
1961 Printf.printf
"andany\n"; flush stdout
;
1962 anno res1 [child1
;child2
]
1963 | (_
,(child2
,res2)) ->
1965 [] -> (* !Flag_ctl.partial_match must be true *)
1967 then anno [] [child1
; child2
]
1970 let s = mkstates states required_states
in
1972 (function a
-> function b
->
1973 strict_triples_conj strict
s a
[b
])
1974 [List.hd
res2] (List.tl
res2) in
1975 anno res [child1
; child2
]
1978 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1979 Printf.printf
"andany\n"; flush stdout
;
1981 let s = mkstates states required_states
in
1983 (function a
-> function b
->
1984 strict_triples_conj strict
s a b
)
1986 anno res [child1
; child2
]
1989 "only one result allowed for the left arg of AndAny")))
1990 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1991 let pm = !Flag_ctl.partial_match
in
1992 (match (pm,satv unchecked required required_states phi1 env
) with
1993 (false,(child1
,[])) ->
1994 Printf.printf
"and\n"; flush stdout
; anno [] [child1
]
1995 | (_
,(child1
,res1)) ->
1996 let new_required = extend_required res1 required
in
1997 let new_required_states = get_required_states res1 in
1998 let new_required_states =
1999 get_reachable dir m
new_required_states in
2000 (match (pm,satv unchecked new_required new_required_states phi2
2002 (false,(child2
,[])) ->
2003 Printf.printf
"andany\n"; flush stdout
;
2004 anno res1 [child1
;child2
]
2005 | (_
,(child2
,res2)) ->
2007 let s = mkstates states required_states
in
2010 function (st
,th
,_
) as phi2_elem
->
2012 triples_complement [st
] [(st
,th
,[])] in
2013 strict_triples_conj_none strict
s acc
2014 (phi2_elem
::inverse))
2016 anno res [child1
; child2
]))
2017 | A.InnerAnd
(phi1
) ->
2018 let (child1
,res1) = satv unchecked required required_states phi1 env
in
2019 Printf.printf
"uncheck\n"; flush stdout
;
2020 anno (inner_and res1) [child1
]
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
"EX\n"; flush stdout
;
2027 anno (satEX dir m
res required_states
) [child
]
2028 | A.AX
(dir
,strict
,phi1
) ->
2029 let new_required_states =
2030 get_children_required_states dir m required_states
in
2032 satv unchecked required
new_required_states phi1 env
in
2033 Printf.printf
"AX\n"; flush stdout
;
2034 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2037 let new_required_states = get_reachable dir m required_states
in
2039 satv unchecked required
new_required_states phi1 env
in
2040 Printf.printf
"EF\n"; flush stdout
;
2041 anno (satEF dir m
res new_required_states) [child
]
2042 | A.AF
(dir
,strict
,phi1
) ->
2043 if !Flag_ctl.loop_in_src_code
2045 satv unchecked required required_states
2046 (A.AU
(dir
,strict
,A.True
,phi1
))
2049 (let new_required_states = get_reachable dir m required_states
in
2051 satv unchecked required
new_required_states phi1 env
in
2052 Printf.printf
"AF\n"; flush stdout
;
2054 strict_A1 strict
satAF satEF dir m
res new_required_states in
2057 let new_required_states = get_reachable dir m required_states
in
2059 satv unchecked required
new_required_states phi1 env
in
2060 Printf.printf
"EG\n"; flush stdout
;
2061 anno (satEG dir m
res new_required_states) [child
]
2062 | A.AG
(dir
,strict
,phi1
) ->
2063 let new_required_states = get_reachable dir m required_states
in
2065 satv unchecked required
new_required_states phi1 env
in
2066 Printf.printf
"AG\n"; flush stdout
;
2067 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2070 | A.EU
(dir
,phi1
,phi2
) ->
2071 let new_required_states = get_reachable dir m required_states
in
2072 (match satv unchecked required
new_required_states phi2 env
with
2074 Printf.printf
"EU\n"; flush stdout
;
2077 let new_required = extend_required res2 required
in
2079 satv unchecked new_required new_required_states phi1 env
in
2080 Printf.printf
"EU\n"; flush stdout
;
2081 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2083 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2084 failwith
"should not be used" (*
2085 let new_required_states = get_reachable dir m required_states in
2086 (match satv unchecked required new_required_states phi2 env with
2088 Printf.printf "AW %b\n" unchecked; flush stdout; anno [] [child2]
2090 let new_required = extend_required res2 required in
2092 satv unchecked new_required new_required_states phi1 env in
2093 Printf.printf "AW %b\n" unchecked; flush stdout;
2095 strict_A2 strict satAW satEF dir m res1 res2
2096 new_required_states in
2097 anno res [child1; child2]) *)
2098 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2099 let new_required_states = get_reachable dir m required_states
in
2100 (match satv unchecked required
new_required_states phi2 env
with
2102 Printf.printf
"AU\n"; flush stdout
; anno [] [child2
]
2104 let new_required = extend_required s2 required
in
2106 satv unchecked new_required new_required_states phi1 env
in
2107 Printf.printf
"AU\n"; flush stdout
;
2109 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2110 (fun y str -> ()) in
2113 anno res [child1
; child2
]
2114 | AUfailed tmp_res
->
2115 (* found a loop, have to try AW *)
2117 A[E[phi1 U phi2] & phi1 W phi2]
2118 the and is nonstrict *)
2119 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2120 Printf.printf
"AW\n"; flush stdout
;
2123 (satEU dir m
s1 tmp_res
new_required_states
2124 (* no graph, for the moment *)
2128 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2129 anno res [child1
; child2
]))
2130 | A.Implies
(phi1
,phi2
) ->
2131 satv unchecked required required_states
2132 (A.Or
(A.Not phi1
,phi2
))
2134 | A.Exists
(keep
,v
,phi1
) ->
2135 let new_required = drop_required v required
in
2137 satv unchecked new_required required_states phi1 env
in
2138 Printf.printf
"exists\n"; flush stdout
;
2139 anno (triples_witness v
unchecked (not keep
) res) [child
]
2140 | A.Let
(v
,phi1
,phi2
) ->
2142 satv unchecked required required_states phi1 env
in
2144 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2145 anno res2 [child1
;child2
]
2146 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2147 let new_required_states = get_reachable dir m required_states
in
2149 satv unchecked required
new_required_states phi1 env
in
2151 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2152 anno res2 [child1
;child2
]
2154 Printf.printf
"Ref\n"; flush stdout
;
2155 let res = List.assoc v env
in
2158 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2161 | A.XX
(phi
) -> failwith
"should have been removed" in
2162 let res1 = drop_wits required_states
res phi
in
2166 print_required_states required_states
;
2167 print_state "after drop_wits" res1 end;
2172 let sat_verbose annotate maxlvl lvl m phi
=
2173 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2175 (* Type for annotations collected in a tree *)
2176 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2178 let sat_annotree annotate m phi
=
2179 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2180 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2184 let sat m phi = satloop m phi []
2188 let simpleanno l phi
res =
2190 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2191 print_generic_algo
(List.sort compare
res);
2192 Format.print_string
"\n------------------------------\n\n" in
2193 let pp_dir = function
2195 | A.BACKWARD
-> pp "^" in
2197 | A.False
-> pp "False"
2198 | A.True
-> pp "True"
2199 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2200 | A.Not
(phi
) -> pp "Not"
2201 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2202 | A.And
(_
,phi1
,phi2
) -> pp "And"
2203 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2204 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2205 | A.Or
(phi1
,phi2
) -> pp "Or"
2206 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2207 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2208 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2209 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2210 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2211 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2212 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2213 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2214 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2215 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2216 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2217 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2218 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2219 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2220 | A.Uncheck
(s) -> pp "Uncheck"
2221 | A.InnerAnd
(s) -> pp "InnerAnd"
2222 | A.XX
(phi1
) -> pp "XX"
2226 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2227 print a ctl formula more accurately if you want.
2228 Use the print_xxx provided in the different module to call
2229 Pretty_print_ctl.pp_ctl.
2232 let simpleanno2 l phi
res =
2234 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2235 Format.print_newline
();
2236 Format.print_string
"----------------------------------------------------";
2237 Format.print_newline
();
2238 print_generic_algo
(List.sort compare
res);
2239 Format.print_newline
();
2240 Format.print_string
"----------------------------------------------------";
2241 Format.print_newline
();
2242 Format.print_newline
();
2246 (* ---------------------------------------------------------------------- *)
2248 (* ---------------------------------------------------------------------- *)
2250 type optentry
= bool ref * string
2251 type options
= {label : optentry
; unch
: optentry
;
2252 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2254 reqenv
: optentry
; reqstates
: optentry
}
2257 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2258 unch
= (pUNCHECK_OPT,"uncheck_opt");
2259 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2260 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2261 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2262 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2263 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2264 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2268 ("label ",[options.label]);
2269 ("unch ",[options.unch
]);
2270 ("unch and label ",[options.label;options.unch
])]
2273 [("conj ", [options.conj]);
2274 ("compl1 ", [options.compl1
]);
2275 ("compl12 ", [options.compl1
;options.compl2
]);
2276 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2277 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2279 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2280 ("compl12 unch satl ",
2281 [options.compl1;options.compl2;options.unch;options.label]); *)
2282 ("conj/compl12 unch satl ",
2283 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2286 [("newinfo ", [options.newinfo
]);
2287 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2290 [("reqenv ", [options.reqenv
]);
2291 ("reqstates ", [options.reqstates
]);
2292 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2293 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2294 ("reqstates unch satl ",
2295 [options.reqstates;options.unch;options.label]);*)
2296 ("reqenv/states unch satl ",
2297 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2300 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2301 options.newinfo
;options.reqenv
;options.reqstates
]
2304 [("all ",all_options)]
2306 let all_options_but_path =
2307 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2308 options.reqenv
;options.reqstates
]
2310 let all_but_path = ("all but path ",all_options_but_path)
2313 [(satAW_calls, "satAW", ref 0);
2314 (satAU_calls, "satAU", ref 0);
2315 (satEF_calls, "satEF", ref 0);
2316 (satAF_calls, "satAF", ref 0);
2317 (satEG_calls, "satEG", ref 0);
2318 (satAG_calls, "satAG", ref 0);
2319 (satEU_calls, "satEU", ref 0)]
2323 (function (opt
,x) ->
2324 (opt
,x,ref 0.0,ref 0,
2325 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2326 [List.hd
all;all_but_path]
2327 (*(all@baseline@conjneg@path@required)*)
2331 let rec iter fn = function
2333 | n
-> let _ = fn() in
2334 (Hashtbl.clear
reachable_table;
2335 Hashtbl.clear
memo_label;
2339 let copy_to_stderr fl
=
2340 let i = open_in fl
in
2342 Printf.fprintf stderr
"%s\n" (input_line
i);
2344 try loop() with _ -> ();
2347 let bench_sat (_,_,states) fn =
2348 List.iter (function (opt
,_) -> opt
:= false) all_options;
2351 (function (name
,options,time
,trips,counter_info
) ->
2352 let iterct = !Flag_ctl.bench
in
2353 if !time
> float_of_int
timeout then time
:= -100.0;
2354 if not
(!time
= -100.0)
2357 Hashtbl.clear
reachable_table;
2358 Hashtbl.clear
memo_label;
2359 List.iter (function (opt
,_) -> opt
:= true) options;
2360 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2364 let bef = Sys.time
() in
2366 Common.timeout_function
timeout
2368 let bef = Sys.time
() in
2369 let res = iter fn iterct in
2370 let aft = Sys.time
() in
2371 time
:= !time
+. (aft -. bef);
2372 trips := !trips + !triples;
2374 (function (calls
,_,save_calls
) ->
2375 function (current_calls
,current_cfg
,current_max_cfg
) ->
2377 !current_calls
+ (!calls
- !save_calls
);
2378 if (!calls
- !save_calls
) > 0
2380 (let st = List.length
states in
2381 current_cfg
:= !current_cfg
+ st;
2382 if st > !current_max_cfg
2383 then current_max_cfg
:= st))
2384 counters counter_info
;
2389 let aft = Sys.time
() in
2391 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2395 List.iter (function (opt
,_) -> opt
:= false) options;
2400 Printf.fprintf stderr
"\n";
2404 (if not
(List.for_all
(function x -> x = res) rest
)
2406 (List.iter (print_state "a state") answers;
2407 Printf.printf
"something doesn't work\n");
2411 let iterct = !Flag_ctl.bench
in
2415 (function (name
,options,time
,trips,counter_info
) ->
2416 Printf.fprintf stderr
"%s Numbers: %f %d "
2417 name
(!time
/. (float_of_int
iterct)) !trips;
2419 (function (calls
,cfg
,max_cfg
) ->
2420 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2422 Printf.fprintf stderr
"\n")
2425 (* ---------------------------------------------------------------------- *)
2426 (* preprocessing: ignore irrelevant functions *)
2428 let preprocess (cfg
,_,_) label = function
2429 [] -> true (* no information, try everything *)
2431 let sz = G.size cfg
in
2432 let verbose_output pred = function
2434 Printf.printf
"did not find:\n";
2435 P.print_predicate
pred; Format.print_newline
()
2437 Printf.printf
"found:\n";
2438 P.print_predicate
pred; Format.print_newline
();
2439 Printf.printf
"but it was not enough\n" in
2440 let get_any verbose
x =
2442 try Hashtbl.find
memo_label x
2445 (let triples = label x in
2447 List.map (function (st,th
,_) -> (st,th
)) triples in
2448 Hashtbl.add memo_label x filtered;
2450 if verbose
then verbose_output x res;
2453 (* don't bother testing when there are more patterns than nodes *)
2454 if List.length l
> sz-2
2456 else List.for_all
(get_any false) l
in
2457 if List.exists
get_all l
2460 (if !Flag_ctl.verbose_match
2462 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2466 let filter_partial_matches trips =
2467 if !Flag_ctl.partial_match
2469 let anynegwit = (* if any is neg, then all are *)
2470 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2472 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2475 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2479 (* ---------------------------------------------------------------------- *)
2480 (* Main entry point for engine *)
2481 let sat m phi reqopt
=
2483 (match !Flag_ctl.steps
with
2484 None
-> step_count := 0
2485 | Some
x -> step_count := x);
2486 Hashtbl.clear
reachable_table;
2487 Hashtbl.clear
memo_label;
2488 let (x,label,states) = m
in
2489 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2491 ((* to drop when Yoann initialized this flag *)
2492 if List.exists
(G.extract_is_loop
x) states
2493 then Flag_ctl.loop_in_src_code
:= true;
2494 let m = (x,label,List.sort compare
states) in
2496 if(!Flag_ctl.verbose_ctl_engine
)
2498 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2499 if !Flag_ctl.bench
> 0
2503 let fn _ = satloop false [] None
m phi
[] in
2504 if !Flag_ctl.bench
> 0
2506 else Common.profile_code
"ctl" (fun _ -> fn()) in
2507 let res = filter_partial_matches res in
2509 Printf.printf "steps: start %d, stop %d\n"
2510 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2512 Printf.printf "triples: %d\n" !triples;
2513 print_state "final result" res;
2515 List.sort compare
res)
2517 (if !Flag_ctl.verbose_ctl_engine
2518 then Common.pr2
"missing something required";
2523 (* ********************************************************************** *)
2524 (* End of Module: CTL_ENGINE *)
2525 (* ********************************************************************** *)