2 * Copyright 2012, INRIA
3 * Julia Lawall, Gilles Muller
4 * Copyright 2010-2011, INRIA, University of Copenhagen
5 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
6 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
7 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
8 * This file is part of Coccinelle.
10 * Coccinelle is free software: you can redistribute it and/or modify
11 * it under the terms of the GNU General Public License as published by
12 * the Free Software Foundation, according to version 2 of the License.
14 * Coccinelle is distributed in the hope that it will be useful,
15 * but WITHOUT ANY WARRANTY; without even the implied warranty of
16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 * GNU General Public License for more details.
19 * You should have received a copy of the GNU General Public License
20 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
22 * The authors reserve the right to distribute this or future versions of
23 * Coccinelle under other licenses.
27 (*external c_counter : unit -> int = "c_counter"*)
29 (* Optimize triples_conj by first extracting the intersection of the two sets,
30 which can certainly be in the intersection *)
31 let pTRIPLES_CONJ_OPT = ref true
32 (* For complement, make NegState for the negation of a single state *)
33 let pTRIPLES_COMPLEMENT_OPT = ref true
34 (* For complement, do something special for the case where the environment
35 and witnesses are empty *)
36 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
37 (* "Double negate" the arguments of the path operators *)
38 let pDOUBLE_NEGATE_OPT = ref true
39 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
40 let pNEW_INFO_OPT = ref true
41 (* Filter the result of the label function to drop entries that aren't
42 compatible with any of the available environments *)
43 let pREQUIRED_ENV_OPT = ref true
44 (* Memoize the raw result of the label function *)
45 let pSATLABEL_MEMO_OPT = ref true
46 (* Filter results according to the required states *)
47 let pREQUIRED_STATES_OPT = ref true
48 (* Drop negative witnesses at Uncheck *)
49 let pUNCHECK_OPT = ref true
50 let pANY_NEG_OPT = ref true
51 let pLazyOpt = ref true
53 (* Nico: This stack is use for graphical traces *)
54 let graph_stack = ref ([] : string list
)
55 let graph_hash = (Hashtbl.create
101)
58 let pTRIPLES_CONJ_OPT = ref false
59 let pTRIPLES_COMPLEMENT_OPT = ref false
60 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
61 let pDOUBLE_NEGATE_OPT = ref false
62 let pNEW_INFO_OPT = ref false
63 let pREQUIRED_ENV_OPT = ref false
64 let pSATLABEL_MEMO_OPT = ref false
65 let pREQUIRED_STATES_OPT = ref false
66 let pUNCHECK_OPT = ref false
67 let pANY_NEG_OPT = ref false
68 let pLazyOpt = ref false
72 let step_count = ref 0
75 if not
(!step_count = 0)
78 step_count := !step_count - 1;
79 if !step_count = 0 then raise Steps
82 let inc cell
= cell
:= !cell
+ 1
84 let satEU_calls = ref 0
85 let satAW_calls = ref 0
86 let satAU_calls = ref 0
87 let satEF_calls = ref 0
88 let satAF_calls = ref 0
89 let satEG_calls = ref 0
90 let satAG_calls = ref 0
98 Printf.sprintf
"_fresh_r_%d" c
100 (* **********************************************************************
102 * Implementation of a Witness Tree model checking engine for CTL-FVex
105 * **********************************************************************)
107 (* ********************************************************************** *)
108 (* Module: SUBST (substitutions: meta. vars and values) *)
109 (* ********************************************************************** *)
115 val eq_mvar
: mvar
-> mvar
-> bool
116 val eq_val
: value -> value -> bool
117 val merge_val
: value -> value -> value
118 val print_mvar
: mvar
-> unit
119 val print_value
: value -> unit
123 (* ********************************************************************** *)
124 (* Module: GRAPH (control flow graphs / model) *)
125 (* ********************************************************************** *)
131 val predecessors
: cfg
-> node
-> node list
132 val successors
: cfg
-> node
-> node list
133 val extract_is_loop
: cfg
-> node
-> bool
134 val print_node
: node
-> unit
135 val size
: cfg
-> int
136 val print_graph
: cfg
-> string option ->
137 (node
* string) list
-> (node
* string) list
-> string -> unit
141 module OGRAPHEXT_GRAPH
=
144 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
145 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
146 let print_node i
= Format.print_string
(Common.i_to_s i
)
150 (* ********************************************************************** *)
151 (* Module: PREDICATE (predicates for CTL formulae) *)
152 (* ********************************************************************** *)
154 module type PREDICATE
=
157 val print_predicate
: t
-> unit
161 (* ********************************************************************** *)
163 (* ---------------------------------------------------------------------- *)
164 (* Misc. useful generic functions *)
165 (* ---------------------------------------------------------------------- *)
167 let get_graph_files () = !graph_stack
168 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
178 let foldl = List.fold_left
;;
180 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
182 type 'a esc
= ESC
of 'a
| CONT
of 'a
184 let foldr = List.fold_right
;;
186 let concat = List.concat;;
190 let filter = List.filter;;
192 let partition = List.partition;;
194 let concatmap f l
= List.concat (List.map f l
);;
202 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
204 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
206 let rec some_tolist opts
=
209 | (Some x
)::rest
-> x
::(some_tolist rest
)
210 | _
::rest
-> some_tolist rest
213 let rec groupBy eq l
=
217 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
218 (x
::xs1
)::(groupBy eq xs2
)
221 let group l
= groupBy (=) l
;;
223 let rec memBy eq x l
=
226 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
229 let rec nubBy eq ls
=
232 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
233 | (x
::xs
) -> x
::(nubBy eq xs
)
239 | (x
::xs
) when (List.mem x xs
) -> nub xs
240 | (x
::xs
) -> x
::(nub xs
)
243 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
245 let setifyBy eq xs
= nubBy eq xs
;;
247 let setify xs
= nub xs
;;
249 let inner_setify xs
= List.sort compare
(nub xs
);;
251 let unionBy compare eq xs
= function
254 let rec loop = function
256 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
257 List.sort compare
(loop xs
)
260 let union xs ys
= unionBy state_compare (=) xs ys
;;
262 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
264 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
266 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
267 let supseteq xs ys
= subseteq ys xs
269 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
271 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
273 (* Fix point calculation *)
275 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
278 (* Fix point calculation on set-valued functions *)
279 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
280 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
282 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
284 (* ********************************************************************** *)
285 (* Module: CTL_ENGINE *)
286 (* ********************************************************************** *)
289 functor (SUB
: SUBST
) ->
290 functor (G
: GRAPH
) ->
291 functor (P
: PREDICATE
) ->
296 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
298 type ('pred
,'anno
) witness
=
299 (G.node
, substitution
,
300 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
301 Ast_ctl.generic_witnesstree
303 type ('pred
,'anno
) triples =
304 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
306 (* ---------------------------------------------------------------------- *)
307 (* Pretty printing functions *)
308 (* ---------------------------------------------------------------------- *)
310 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
311 let print_generic_subst = function
313 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
314 | A.NegSubst
(mvar
, v
) ->
315 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
316 Format.print_string
"[";
317 Common.print_between
(fun () -> Format.print_string
";" )
318 print_generic_subst substxs
;
319 Format.print_string
"]"
321 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
323 | A.Wit
(state
, subst
, anno
, childrens
) ->
324 Format.print_string
"wit ";
326 print_generic_substitution subst
;
327 (match childrens
with
328 [] -> Format.print_string
"{}"
330 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
331 print_generic_witnesstree childrens
; Format.close_box
())
333 Format.print_string
"!";
334 print_generic_witness wit
336 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
339 Format.print_string
"{";
341 (fun () -> Format.print_string
";"; Format.force_newline
() )
342 print_generic_witness witnesstree
;
343 Format.print_string
"}";
346 and print_generic_triple
(node
,subst
,tree
) =
348 print_generic_substitution subst
;
349 print_generic_witnesstree tree
351 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
352 Format.print_string
"<";
354 (fun () -> Format.print_string
";"; Format.force_newline
())
355 print_generic_triple xs
;
356 Format.print_string
">"
359 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
360 Printf.printf
"%s\n" str
;
361 List.iter
(function x ->
362 print_generic_triple
x; Format.print_newline
(); flush stdout
)
363 (List.sort compare l
);
366 let print_required_states = function
367 None
-> Printf.printf
"no required states\n"
369 Printf.printf
"required states: ";
372 G.print_node x; Format.print_string
" "; Format.print_flush
())
376 let mkstates states
= function
378 | Some states
-> states
380 let print_graph grp required_states res str
= function
381 A.Exists
(keep
,v
,phi
) -> ()
383 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
386 | A.Exists
(keep
,v
,phi
) -> ()
389 Printf.sprintf
"%s%s"
391 (Common.format_to_string
393 Pretty_print_ctl.pp_ctl
394 (P.print_predicate
, SUB.print_mvar
)
397 let file = (match !Flag.currentfile
with
398 None
-> "graphical_trace"
401 (if not
(List.mem
file !graph_stack) then
402 graph_stack := file :: !graph_stack);
403 let filename = Filename.temp_file
(file^
":") ".dot" in
404 Hashtbl.add
graph_hash file filename;
406 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
407 (match required_states
with
409 | Some required_states
->
410 (List.map (function s
-> (s
,"blue")) required_states
))
411 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
413 let print_graph_c grp required_states res
ctr phi
=
414 let str = "iter: "^
(string_of_int
!ctr) in
415 print_graph grp required_states res
str phi
417 (* ---------------------------------------------------------------------- *)
419 (* ---------------------------------------------------------------------- *)
422 (* ************************* *)
424 (* ************************* *)
429 | A.NegSubst
(x,_
) -> x
435 | A.NegSubst
(_
,x) -> x
438 let eq_subBy eqx eqv sub sub'
=
439 match (sub
,sub'
) with
440 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
441 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
446 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
448 let eq_subst th th'
= setequalBy eq_sub th th'
;;
450 let merge_subBy eqx
(===) (>+<) sub sub'
=
451 (* variable part is guaranteed to be the same *)
452 match (sub
,sub'
) with
453 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
455 then Some
[A.Subst
(x, v
>+< v'
)]
457 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
459 then Some
[A.Subst
(x'
,v'
)]
461 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
463 then Some
[A.Subst
(x,v
)]
465 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
468 let merged = v
>+< v'
in
469 if merged = v
&& merged = v'
470 then Some
[A.NegSubst
(x,v
>+< v'
)]
472 (* positions are compatible, but not identical. keep apart. *)
473 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
474 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
478 (* How could we accomadate subterm constraints here??? *)
479 let merge_sub sub sub'
=
480 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
482 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
484 (* NOTE: we sort by using the generic "compare" on (meta-)variable
485 * names; we could also require a definition of compare for meta-variables
486 * or substitutions but that seems like overkill for sorting
488 let clean_subst theta
=
492 let res = compare
(dom_sub s
) (dom_sub s'
) in
496 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
497 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
498 | _
-> compare
(ran_sub s
) (ran_sub s'
)
501 let rec loop = function
503 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
504 loop (A.Subst
(x,v
)::rest
)
505 | x::xs
-> x::(loop xs
) in
508 let top_subst = [];; (* Always TRUE subst. *)
510 (* Split a theta in two parts: one with (only) "x" and one without *)
512 let split_subst theta
x =
513 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
515 exception SUBST_MISMATCH
516 let conj_subst theta theta'
=
517 match (theta
,theta'
) with
518 | ([],_
) -> Some theta'
519 | (_
,[]) -> Some theta
521 let rec classify = function
523 | [x] -> [(dom_sub x,[x])]
525 (match classify xs
with
526 ((nm
,y
)::ys
) as res ->
529 else (dom_sub x,[x])::res
530 | _
-> failwith
"not possible") in
531 let merge_all theta theta'
=
538 match (merge_sub sub sub'
) with
539 Some subs
-> subs
@ rest
540 | _
-> raise SUBST_MISMATCH
)
543 let rec loop = function
545 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
547 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
548 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
549 (match compare
x y
with
550 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
551 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
552 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
553 | _
-> failwith
"not possible") in
554 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
555 with SUBST_MISMATCH
-> None
558 (* theta' must be a subset of theta *)
559 let conj_subst_none theta theta'
=
560 match (theta
,theta'
) with
561 | (_
,[]) -> Some theta
564 let rec classify = function
566 | [x] -> [(dom_sub x,[x])]
568 (match classify xs
with
569 ((nm
,y
)::ys
) as res ->
572 else (dom_sub x,[x])::res
573 | _
-> failwith
"not possible") in
574 let merge_all theta theta'
=
581 match (merge_sub sub sub'
) with
582 Some subs
-> subs
@ rest
583 | _
-> raise SUBST_MISMATCH
)
586 let rec loop = function
588 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
589 | ([],ctheta'
) -> raise SUBST_MISMATCH
590 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
591 (match compare
x y
with
592 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
593 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
594 | 1 -> raise SUBST_MISMATCH
595 | _
-> failwith
"not possible") in
596 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
597 with SUBST_MISMATCH
-> None
602 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
603 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
606 (* Turn a (big) theta into a list of (small) thetas *)
607 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
610 (* ************************* *)
612 (* ************************* *)
614 (* Always TRUE witness *)
615 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
617 let eq_wit wit wit'
= wit
= wit'
;;
619 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
620 let res = unionBy compare
(=) wit wit'
in
621 let anynegwit = (* if any is neg, then all are *)
622 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
624 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
627 let negate_wit wit
= A.NegWit wit
(*
629 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
630 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
633 let negate_wits wits
=
634 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
637 let anynegwit = (* if any is neg, then all are *)
638 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
642 function (s
,th
,wit
) ->
643 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
646 (* ************************* *)
648 (* ************************* *)
650 (* Triples are equal when the constituents are equal *)
651 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
652 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
654 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
656 let normalize trips
=
658 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
662 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
663 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
664 let triples_conj trips trips'
=
665 let (trips
,shared
,trips'
) =
666 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
669 List.partition (function t
-> List.mem t trips'
) trips
in
671 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
672 (trips,shared
,trips'
)
673 else (trips,[],trips'
) in
674 foldl (* returns a set - setify inlined *)
676 function (s1
,th1
,wit1
) ->
679 function (s2
,th2
,wit2
) ->
681 (match (conj_subst th1 th2
) with
683 let t = (s1
,th
,union_wit wit1 wit2
) in
684 if List.mem
t rest
then rest
else t::rest
691 (* ignore the state in the right argument. always pretend it is the same as
693 (* env on right has to be a subset of env on left *)
694 let triples_conj_none trips trips'
=
695 let (trips,shared
,trips'
) =
696 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
699 List.partition (function t -> List.mem
t trips'
) trips in
701 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
702 (trips,shared
,trips'
)
703 else (trips,[],trips'
) in
704 foldl (* returns a set - setify inlined *)
706 function (s1
,th1
,wit1
) ->
709 function (s2
,th2
,wit2
) ->
710 match (conj_subst_none th1 th2
) with
712 let t = (s1
,th
,union_wit wit1 wit2
) in
713 if List.mem
t rest
then rest
else t::rest
721 let triples_conj_AW trips trips'
=
722 let (trips,shared
,trips'
) =
723 if false && !pTRIPLES_CONJ_OPT
726 List.partition (function t -> List.mem
t trips'
) trips in
728 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
729 (trips,shared
,trips'
)
730 else (trips,[],trips'
) in
731 foldl (* returns a set - setify inlined *)
733 function (s1
,th1
,wit1
) ->
736 function (s2
,th2
,wit2
) ->
738 (match (conj_subst th1 th2
) with
740 let t = (s1
,th
,union_wit wit1 wit2
) in
741 if List.mem
t rest
then rest
else t::rest
748 (* *************************** *)
749 (* NEGATION (NegState style) *)
750 (* *************************** *)
752 (* Constructive negation at the state level *)
755 | NegState
of 'a list
758 let compatible_states = function
759 (PosState s1
, PosState s2
) ->
760 if s1
= s2
then Some
(PosState s1
) else None
761 | (PosState s1
, NegState s2
) ->
762 if List.mem s1 s2
then None
else Some
(PosState s1
)
763 | (NegState s1
, PosState s2
) ->
764 if List.mem s2 s1
then None
else Some
(PosState s2
)
765 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
768 (* Conjunction on triples with "special states" *)
769 let triples_state_conj trips trips'
=
770 let (trips,shared
,trips'
) =
771 if !pTRIPLES_CONJ_OPT
774 List.partition (function t -> List.mem
t trips'
) trips in
776 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
777 (trips,shared
,trips'
)
778 else (trips,[],trips'
) in
781 function (s1
,th1
,wit1
) ->
784 function (s2
,th2
,wit2
) ->
785 match compatible_states(s1
,s2
) with
787 (match (conj_subst th1 th2
) with
789 let t = (s
,th
,union_wit wit1 wit2
) in
790 if List.mem
t rest
then rest
else t::rest
797 let triple_negate (s
,th
,wits
) =
798 let negstates = (NegState
[s
],top_subst,top_wit) in
799 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
800 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
801 negstates :: (negths @ negwits) (* all different *)
803 (* FIX ME: it is not necessary to do full conjunction *)
804 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
805 if !pTRIPLES_COMPLEMENT_OPT
807 (let cleanup (s
,th
,wit
) =
809 PosState s'
-> [(s'
,th
,wit
)]
811 assert (th
=top_subst);
812 assert (wit
=top_wit);
813 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
814 let (simple
,complex
) =
815 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
817 let (simple
,complex
) =
818 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
820 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
821 top_subst,top_wit)] in
823 else ([(NegState
[],top_subst,top_wit)],trips) in
824 let rec compl trips =
827 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
828 let compld = (compl complex
) in
829 let compld = concatmap cleanup compld in
832 let negstates (st
,th
,wits
) =
833 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
834 let negths (st
,th
,wits
) =
835 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
836 let negwits (st
,th
,wits
) =
837 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
839 [] -> map (function st
-> (st
,top_subst,top_wit)) states
845 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
846 (negstates x @ negths x @ negwits x) xs
)
849 let triple_negate (s
,th
,wits
) =
850 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
851 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
852 ([s
], negths @ negwits) (* all different *)
854 let print_compl_state str (n
,p
) =
855 Printf.printf
"%s neg: " str;
857 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
862 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
864 then map (function st
-> (st
,top_subst,top_wit)) states
866 let cleanup (neg
,pos
) =
868 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
869 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
871 let trips = List.sort
state_compare trips in
872 let all_negated = List.map triple_negate trips in
873 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
874 let (pos1conj
,pos1keep
) =
875 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
876 let (pos2conj
,pos2keep
) =
877 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
878 (Common.union_set neg1 neg2
,
879 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
880 let rec inner_loop = function
881 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
883 let rec outer_loop = function
885 | l
-> outer_loop (inner_loop l
) in
886 cleanup (outer_loop all_negated)
888 (* ********************************** *)
889 (* END OF NEGATION (NegState style) *)
890 (* ********************************** *)
892 (* now this is always true, so we could get rid of it *)
893 let something_dropped = ref true
895 let triples_union trips trips'
=
896 (*unionBy compare eq_trip trips trips';;*)
897 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
899 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
900 Then, the following says that since the first is a more restrictive
901 environment and has fewer witnesses, then it should be dropped. But having
902 fewer witnesses is not necessarily less informative than having more,
903 because fewer witnesses can mean the absence of the witness-causing thing.
904 So the fewer witnesses have to be kept around.
905 subseteq changed to = to make it hopefully work
910 something_dropped := false;
912 then (something_dropped := true; trips)
914 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
917 (match conj_subst th1 th2
with
920 then if (*subseteq*) wit1
= wit2
then 1 else 0
923 then if (*subseteq*) wit2
= wit1
then (-1) else 0
927 let rec first_loop second
= function
929 | x::xs
-> first_loop (second_loop
x second
) xs
930 and second_loop
x = function
933 match subsumes x y
with
934 1 -> something_dropped := true; all
935 | (-1) -> second_loop
x ys
936 | _
-> y
::(second_loop
x ys
) in
937 first_loop trips trips'
939 else unionBy compare
eq_trip trips trips'
942 let triples_witness x unchecked not_keep
trips =
943 let anyneg = (* if any is neg, then all are *)
944 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
945 let anynegwit = (* if any is neg, then all are *)
946 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
947 let allnegwit = (* if any is neg, then all are *)
948 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
950 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
954 function (s
,th
,wit
) as t ->
955 let (th_x
,newth
) = split_subst th
x in
958 (* one consider whether if not not_keep is true, then we should
959 fail. but it could be that the variable is a used_after and
960 then it is the later rule that should fail and not this one *)
961 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
963 (SUB.print_mvar
x; Format.print_flush
();
964 print_state ": empty witness from" [t]);
966 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
967 (* see tests/nestseq for how neg bindings can come up even
968 without eg partial matches
969 (* negated substitution only allowed with negwits.
971 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
974 (print_generic_substitution l
; Format.print_newline
();
975 failwith
"unexpected negative binding with positive witnesses")*)
978 if unchecked
or not_keep
981 if anynegwit wit
&& allnegwit wit
982 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
983 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
986 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
992 (* ---------------------------------------------------------------------- *)
993 (* SAT - Model Checking Algorithm for CTL-FVex *)
995 (* TODO: Implement _all_ operators (directly) *)
996 (* ---------------------------------------------------------------------- *)
999 (* ************************************* *)
1000 (* The SAT algorithm and special helpers *)
1001 (* ************************************* *)
1003 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1005 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1006 let exp (s
,th
,wit
) =
1008 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1010 A.FORWARD
-> G.predecessors grp s
1011 | A.BACKWARD
-> G.successors grp s
) in
1012 setify (concatmap exp y
)
1017 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1020 None
-> true | Some reqst
-> List.mem s reqst
in
1023 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1026 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1029 (function p
-> (p
,succ grp p
))
1032 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1033 (* would a hash table be more efficient? *)
1034 let all = List.sort
state_compare all in
1035 let rec up_nodes child s
= function
1037 | (s1
,th
,wit
)::xs
->
1038 (match compare s1 child
with
1039 -1 -> up_nodes child s xs
1040 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1042 let neighbor_triples =
1045 function (s
,children
) ->
1049 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1053 match neighbor_triples with
1057 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1059 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1062 None
-> true | Some reqst
-> List.mem s reqst
in
1065 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1068 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1071 (function p
-> (p
,succ grp p
))
1074 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1075 (* would a hash table be more efficient? *)
1076 let all = List.sort
state_compare all in
1077 let rec up_nodes child s
= function
1079 | (s1
,th
,wit
)::xs
->
1080 (match compare s1 child
with
1081 -1 -> up_nodes child s xs
1082 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1084 let neighbor_triples =
1087 function (s
,children
) ->
1090 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1093 match neighbor_triples with
1095 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1097 (* drop_negwits will call setify *)
1098 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1100 let satAX dir m s reqst
= pre_forall dir m s s reqst
1103 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1104 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1105 (*Printf.printf "EU\n";
1106 let ctr = ref 0 in*)
1111 (*let ctr = ref 0 in*)
1114 let rec f y new_info
=
1120 print_graph y ctr;*)
1121 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1122 let res = triples_union first y
in
1123 let new_info = setdiff res y
in
1124 (*Printf.printf "iter %d res %d new_info %d\n"
1125 !ctr (List.length res) (List.length new_info);
1126 print_state "res" res;
1127 print_state "new_info" new_info;
1135 print_graph y ctr;*)
1136 let pre = pre_exist dir m y reqst
in
1137 triples_union s2
(triples_conj s1
pre) in
1141 (* EF phi == E[true U phi] *)
1142 let satEF dir m s2 reqst
=
1144 (*let ctr = ref 0 in*)
1147 let rec f y
new_info =
1153 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1154 let first = pre_exist dir m
new_info reqst
in
1155 let res = triples_union first y
in
1156 let new_info = setdiff res y
in
1157 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1158 (if dir = A.BACKWARD then "reachable" else "real ef")
1159 !ctr (List.length res) (List.length new_info);
1160 print_state "new info" new_info;
1167 let pre = pre_exist dir m y reqst
in
1168 triples_union s2
pre in
1172 type ('
pred,'anno
) auok
=
1173 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1175 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1176 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1182 (*let ctr = ref 0 in*)
1184 if !Flag_ctl.loop_in_src_code
1189 let rec f y newinfo
=
1195 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1199 try Some
(pre_forall dir m
new_info y reqst
)
1204 match triples_conj s1
pre with
1207 (*print_state "s1" s1;
1208 print_state "pre" pre;
1209 print_state "first" first;*)
1210 let res = triples_union first y
in
1212 if not
!something_dropped
1214 else setdiff res y
in
1216 "iter %d res %d new_info %d\n"
1217 !ctr (List.length res) (List.length new_info);
1222 if !Flag_ctl.loop_in_src_code
1226 fix (function s1 -> function s2 ->
1227 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1228 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1229 subseteq s1 s2) in for popl *)
1234 let pre = pre_forall dir m y y reqst
in
1235 triples_union s2 (triples_conj s1 pre) in
1240 (* reqst could be the states of s1 *)
1242 let lstates = mkstates states reqst in
1243 let initial_removed =
1244 triples_complement lstates (triples_union s1 s2) in
1245 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1246 let rec loop base removed =
1248 triples_conj base (pre_exist dir m removed reqst) in
1250 triples_conj base (triples_complement lstates new_removed) in
1251 if supseteq new_base base
1252 then triples_union base s2
1253 else loop new_base new_removed in
1254 loop initial_base initial_removed *)
1256 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1262 This works extremely badly when the region is small and the end of the
1263 region is very ambiguous, eg free(x) ... x
1267 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1268 let ostates = Common.union_set (get_states s1) (get_states s2) in
1271 A.FORWARD -> G.successors grp
1272 | A.BACKWARD -> G.predecessors grp) in
1274 List.fold_left Common.union_set ostates (List.map succ ostates) in
1275 let negphi = triples_complement states s1 in
1276 let negpsi = triples_complement states s2 in
1277 triples_complement ostates
1278 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1281 (*let ctr = ref 0 in*)
1285 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1288 let pre = pre_forall dir m y y reqst
in
1289 (*print_state "pre" pre;*)
1290 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1291 triples_union s2 conj in
1292 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1293 (* drop wits on s1 represents that we don't want any witnesses from
1294 the case that infinitely loops, only from the case that gets
1295 out of the loop. s1 is like a guard. To see the problem, consider
1296 an example where both s1 and s2 match some code after the loop.
1297 we only want the witness from s2. *)
1298 setgfix f (triples_union (nub(drop_wits s1)) s2)
1301 let satAF dir m s reqst
=
1305 let rec f y newinfo
=
1310 let first = pre_forall dir m
new_info y reqst
in
1311 let res = triples_union first y
in
1312 let new_info = setdiff res y
in
1318 let pre = pre_forall dir m y y reqst
in
1319 triples_union s
pre in
1322 let satAG dir
((_
,_
,states) as m
) s reqst
=
1326 let pre = pre_forall dir m y y reqst
in
1327 triples_conj y
pre in
1330 let satEG dir
((_
,_
,states) as m
) s reqst
=
1334 let pre = pre_exist dir m y reqst
in
1335 triples_conj y
pre in
1338 (* **************************************************************** *)
1339 (* Inner And - a way of dealing with multiple matches within a node *)
1340 (* **************************************************************** *)
1341 (* applied to the result of matching a node. collect witnesses when the
1342 states and environments are the same *)
1343 (* not a good idea, poses problem for unparsing, because don't realize that
1344 adjacent things come from different matches, leading to loss of newlines etc.
1345 exple struct I { ... - int x; + int y; ...} *)
1347 let inner_and trips = trips (*
1348 let rec loop = function
1350 | (s,th,w)::trips ->
1351 let (cur,acc) = loop trips in
1353 (s',_,_)::_ when s = s' ->
1354 let rec loop' = function
1356 | ((_,th',w') as t')::ts' ->
1357 (match conj_subst th th' with
1358 Some th'' -> (s,th'',union_wit w w')::ts'
1359 | None -> t'::(loop' ts')) in
1361 | _ -> ([(s,th,w)],cur@acc)) in
1363 loop (List.sort state_compare trips) (* is this sort needed? *) in
1366 (* *************** *)
1367 (* Partial matches *)
1368 (* *************** *)
1370 let filter_conj states unwanted partial_matches
=
1372 triples_conj (triples_complement states (unwitify unwanted
))
1374 triples_conj (unwitify x) (triples_complement states x)
1376 let strict_triples_conj strict
states trips trips'
=
1377 let res = triples_conj trips trips'
in
1378 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1380 let fail_left = filter_conj states trips trips'
in
1381 let fail_right = filter_conj states trips'
trips in
1382 let ors = triples_union fail_left fail_right in
1383 triples_union res ors
1386 let strict_triples_conj_none strict
states trips trips'
=
1387 let res = triples_conj_none trips trips'
in
1388 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1390 let fail_left = filter_conj states trips trips'
in
1391 let fail_right = filter_conj states trips'
trips in
1392 let ors = triples_union fail_left fail_right in
1393 triples_union res ors
1396 let left_strict_triples_conj strict
states trips trips'
=
1397 let res = triples_conj trips trips'
in
1398 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1400 let fail_left = filter_conj states trips trips'
in
1401 triples_union res fail_left
1404 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1405 let res = op dir m
trips required_states
in
1406 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1408 let states = mkstates states required_states
in
1409 let fail = filter_conj states res (failop dir m
trips required_states
) in
1410 triples_union res fail
1413 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1415 let res = op dir m
trips trips' required_states
in
1416 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1418 let states = mkstates states required_states
in
1419 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1420 triples_union res fail
1423 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1424 required_states
print_graph =
1425 match op dir m
trips trips' required_states
print_graph with
1427 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1429 let states = mkstates states required_states
in
1431 filter_conj states res (failop dir m
trips' required_states
) in
1432 AUok
(triples_union res fail)
1434 | AUfailed
res -> AUfailed
res
1436 (* ********************* *)
1437 (* Environment functions *)
1438 (* ********************* *)
1440 let drop_wits required_states s phi
=
1441 match required_states
with
1443 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1446 let print_required required
=
1449 Format.print_string
"{";
1452 print_generic_substitution reqd
; Format.print_newline
())
1454 Format.print_string
"}";
1455 Format.print_newline
())
1460 let extend_required trips required
=
1461 if !Flag_ctl.partial_match
1464 if !pREQUIRED_ENV_OPT
1470 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1472 let envs = if List.mem
[] envs then [] else envs in
1473 match (envs,required
) with
1477 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1482 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1489 match conj_subst t r
with
1490 None
-> rest
| Some th
-> add th rest
)
1494 with Too_long
-> envs :: required
)
1495 | (envs,_
) -> envs :: required
1498 let drop_required v required
=
1499 if !pREQUIRED_ENV_OPT
1506 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1508 (* check whether an entry has become useless *)
1509 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1512 (* no idea how to write this function ... *)
1514 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1516 let satLabel label required p
=
1518 if !pSATLABEL_MEMO_OPT
1521 let states_subs = Hashtbl.find
memo_label p
in
1522 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1525 let triples = setify(label p
) in
1526 Hashtbl.add memo_label p
1527 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1529 else setify(label p
) in
1530 (* normalize first; conj_subst relies on sorting *)
1531 let ntriples = normalize triples in
1532 if !pREQUIRED_ENV_OPT
1536 function ((s
,th
,_
) as t) ->
1538 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1545 let get_required_states l
=
1546 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1548 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1551 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1552 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1554 match required_states
with
1559 A.FORWARD
-> G.successors
1560 | A.BACKWARD
-> G.predecessors in
1561 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1564 let reachable_table =
1565 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1567 (* like satEF, but specialized for get_reachable *)
1568 let reachsatEF dir
(grp
,_
,_
) s2 =
1570 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1571 let union = unionBy compare
(=) in
1572 let rec f y
= function
1575 let (pre_collected
,new_info) =
1576 List.partition (function Common.Left
x -> true | _
-> false)
1579 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1580 with Not_found
-> Common.Right
x)
1585 function Common.Left
x -> union x rest
1586 | _
-> failwith
"not possible")
1590 (function Common.Right
x -> x | _
-> failwith
"not possible")
1592 let first = inner_setify (concatmap (dirop grp
) new_info) in
1593 let new_info = setdiff first y in
1594 let res = new_info @ y in
1596 List.rev
(f s2 s2) (* put root first *)
1598 let get_reachable dir m required_states
=
1599 match required_states
with
1606 if List.mem cur rest
1610 (try Hashtbl.find
reachable_table (cur
,dir
)
1613 let states = reachsatEF dir m
[cur
] in
1614 Hashtbl.add reachable_table (cur
,dir
) states;
1623 Printf.sprintf
"_c%d" c
1625 (* **************************** *)
1626 (* End of environment functions *)
1627 (* **************************** *)
1629 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1631 let rec satloop unchecked required required_states
1632 ((grp
,label,states) as m
) phi env
=
1633 let rec loop unchecked required required_states phi
=
1637 | A.True
-> triples_top states
1638 | A.Pred
(p
) -> satLabel label required p
1639 | A.Uncheck
(phi1
) ->
1640 let unchecked = if !pUNCHECK_OPT then true else false in
1641 loop unchecked required required_states phi1
1643 let phires = loop unchecked required required_states phi
in
1645 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1646 triples_complement (mkstates states required_states
)
1648 | A.Or
(phi1
,phi2
) ->
1650 (loop unchecked required required_states phi1
)
1651 (loop unchecked required required_states phi2
)
1652 | A.SeqOr
(phi1
,phi2
) ->
1653 let res1 = loop unchecked required required_states phi1
in
1654 let res2 = loop unchecked required required_states phi2
in
1655 let res1neg = unwitify res1 in
1656 let pm = !Flag_ctl.partial_match
in
1657 (match (pm,res1,res2) with
1658 (false,res1,[]) -> res1
1659 | (false,[],res2) -> res2
1663 (triples_complement (mkstates states required_states
) res1neg)
1665 | A.And
(strict
,phi1
,phi2
) ->
1666 (* phi1 is considered to be more likely to be [], because of the
1667 definition of asttoctl. Could use heuristics such as the size of
1669 let pm = !Flag_ctl.partial_match
in
1670 (match (pm,loop unchecked required required_states phi1
) with
1671 (false,[]) when !pLazyOpt -> []
1673 let new_required = extend_required phi1res required
in
1674 let new_required_states = get_required_states phi1res
in
1675 (match (pm,loop unchecked new_required new_required_states phi2
)
1677 (false,[]) when !pLazyOpt -> []
1679 strict_triples_conj strict
1680 (mkstates states required_states
)
1682 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1683 (* phi2 can appear anywhere that is reachable *)
1684 let pm = !Flag_ctl.partial_match
in
1685 (match (pm,loop unchecked required required_states phi1
) with
1688 let new_required = extend_required phi1res required
in
1689 let new_required_states = get_required_states phi1res
in
1690 let new_required_states =
1691 get_reachable dir m
new_required_states in
1692 (match (pm,loop unchecked new_required new_required_states phi2
)
1694 (false,[]) -> phi1res
1697 [] -> (* !Flag_ctl.partial_match must be true *)
1701 let s = mkstates states required_states
in
1703 (function a
-> function b
->
1704 strict_triples_conj strict
s a
[b
])
1705 [List.hd phi2res
] (List.tl phi2res
)
1708 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1709 let s = mkstates states required_states
in
1711 (function a
-> function b
->
1712 strict_triples_conj strict
s a b
)
1716 "only one result allowed for the left arg of AndAny")))
1717 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1718 (* phi2 can appear anywhere that is reachable *)
1719 let pm = !Flag_ctl.partial_match
in
1720 (match (pm,loop unchecked required required_states phi1
) with
1723 let new_required = extend_required phi1res required
in
1724 let new_required_states = get_required_states phi1res
in
1725 let new_required_states =
1726 get_reachable dir m
new_required_states in
1727 (match (pm,loop unchecked new_required new_required_states phi2
)
1729 (false,[]) -> phi1res
1731 (* if there is more than one state, something about the
1732 environment has to ensure that the right triples of
1733 phi2 get associated with the triples of phi1.
1734 the asttoctl2 has to ensure that that is the case.
1735 these should thus be structural properties.
1736 env of phi2 has to be a proper subset of env of phi1
1737 to ensure all end up being consistent. no new triples
1738 should be generated. strict_triples_conj_none takes
1741 let s = mkstates states required_states
in
1744 function (st
,th
,_
) as phi2_elem
->
1746 triples_complement [st
] [(st
,th
,[])] in
1747 strict_triples_conj_none strict
s acc
1748 (phi2_elem
::inverse))
1750 | A.InnerAnd
(phi
) ->
1751 inner_and(loop unchecked required required_states phi
)
1753 let new_required_states =
1754 get_children_required_states dir m required_states
in
1755 satEX dir m
(loop unchecked required
new_required_states phi
)
1757 | A.AX
(dir
,strict
,phi
) ->
1758 let new_required_states =
1759 get_children_required_states dir m required_states
in
1760 let res = loop unchecked required
new_required_states phi
in
1761 strict_A1 strict
satAX satEX dir m
res required_states
1763 let new_required_states = get_reachable dir m required_states
in
1764 satEF dir m
(loop unchecked required
new_required_states phi
)
1766 | A.AF
(dir
,strict
,phi
) ->
1767 if !Flag_ctl.loop_in_src_code
1769 loop unchecked required required_states
1770 (A.AU
(dir
,strict
,A.True
,phi
))
1772 let new_required_states = get_reachable dir m required_states
in
1773 let res = loop unchecked required
new_required_states phi
in
1774 strict_A1 strict
satAF satEF dir m
res new_required_states
1776 let new_required_states = get_reachable dir m required_states
in
1777 satEG dir m
(loop unchecked required
new_required_states phi
)
1779 | A.AG
(dir
,strict
,phi
) ->
1780 let new_required_states = get_reachable dir m required_states
in
1781 let res = loop unchecked required
new_required_states phi
in
1782 strict_A1 strict
satAG satEF dir m
res new_required_states
1783 | A.EU
(dir
,phi1
,phi2
) ->
1784 let new_required_states = get_reachable dir m required_states
in
1785 (match loop unchecked required
new_required_states phi2
with
1786 [] when !pLazyOpt -> []
1788 let new_required = extend_required s2 required
in
1789 let s1 = loop unchecked new_required new_required_states phi1
in
1790 satEU dir m
s1 s2 new_required_states
1791 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1792 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1793 let new_required_states = get_reachable dir m required_states
in
1794 (match loop unchecked required
new_required_states phi2
with
1795 [] when !pLazyOpt -> []
1797 let new_required = extend_required s2 required
in
1798 let s1 = loop unchecked new_required new_required_states phi1
in
1799 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1800 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1801 (*Printf.printf "using AU\n"; flush stdout;*)
1802 let new_required_states = get_reachable dir m required_states
in
1803 (match loop unchecked required
new_required_states phi2
with
1804 [] when !pLazyOpt -> []
1806 let new_required = extend_required s2 required
in
1807 let s1 = loop unchecked new_required new_required_states phi1
in
1809 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1811 print_graph_c grp
new_required_states y ctr phi
) in
1814 | AUfailed tmp_res
->
1815 (* found a loop, have to try AW *)
1817 A[E[phi1 U phi2] & phi1 W phi2]
1818 the and is nonstrict *)
1819 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1820 (*Printf.printf "using AW\n"; flush stdout;*)
1823 (satEU dir m
s1 tmp_res
new_required_states
1824 (* no graph, for the moment *)
1827 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1829 | A.Implies
(phi1
,phi2
) ->
1830 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1831 | A.Exists
(keep
,v
,phi
) ->
1832 let new_required = drop_required v required
in
1833 triples_witness v
unchecked (not keep
)
1834 (loop unchecked new_required required_states phi
)
1836 | A.Let
(v
,phi1
,phi2
) ->
1837 (* should only be used when the properties unchecked, required,
1838 and required_states are known to be the same or at least
1839 compatible between all the uses. this is not checked. *)
1840 let res = loop unchecked required required_states phi1
in
1841 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1842 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1843 (* should only be used when the properties unchecked, required,
1844 and required_states are known to be the same or at least
1845 compatible between all the uses. this is not checked. *)
1846 (* doesn't seem to be used any more *)
1847 let new_required_states = get_reachable dir m required_states
in
1848 let res = loop unchecked required
new_required_states phi1
in
1849 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1851 let res = List.assoc v env
in
1853 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1855 | A.XX
(phi
) -> failwith
"should have been removed" in
1856 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1857 let res = drop_wits required_states
res phi
(* ) *) in
1858 print_graph grp required_states
res "" phi
;
1861 loop unchecked required required_states phi
1865 (* SAT with tracking *)
1867 Printf.printf
"%s\n" str
1869 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1870 ((_
,label,states) as m
) phi env
=
1871 let anno res children
= (annot lvl phi
res children
,res) in
1872 let satv unchecked required required_states phi0 env
=
1873 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1875 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1876 anno (satloop unchecked required required_states m phi env
) []
1880 A.False
-> anno [] []
1881 | A.True
-> anno (triples_top states) []
1884 anno (satLabel label required p
) []
1885 | A.Uncheck
(phi1
) ->
1886 let unchecked = if !pUNCHECK_OPT then true else false in
1887 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1892 satv unchecked required required_states phi1 env
in
1894 anno (triples_complement (mkstates states required_states
) res) [child
]
1895 | A.Or
(phi1
,phi2
) ->
1897 satv unchecked required required_states phi1 env
in
1899 satv unchecked required required_states phi2 env
in
1901 anno (triples_union res1 res2) [child1
; child2
]
1902 | A.SeqOr
(phi1
,phi2
) ->
1904 satv unchecked required required_states phi1 env
in
1906 satv unchecked required required_states phi2 env
in
1908 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1910 let pm = !Flag_ctl.partial_match
in
1911 (match (pm,res1,res2) with
1912 (false,res1,[]) -> anno res1 [child1
; child2
]
1913 | (false,[],res2) -> anno res2 [child1
; child2
]
1915 anno (triples_union res1
1917 (triples_complement (mkstates states required_states
)
1921 | A.And
(strict
,phi1
,phi2
) ->
1922 let pm = !Flag_ctl.partial_match
in
1923 (match (pm,satv unchecked required required_states phi1 env
) with
1924 (false,(child1
,[])) ->
1925 output "and"; anno [] [child1
]
1926 | (_
,(child1
,res1)) ->
1927 let new_required = extend_required res1 required
in
1928 let new_required_states = get_required_states res1 in
1929 (match (pm,satv unchecked new_required new_required_states phi2
1931 (false,(child2
,[])) ->
1932 output "and"; anno [] [child1
;child2
]
1933 | (_
,(child2
,res2)) ->
1936 strict_triples_conj strict
1937 (mkstates states required_states
)
1939 anno res [child1
; child2
]))
1940 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1941 let pm = !Flag_ctl.partial_match
in
1942 (match (pm,satv unchecked required required_states phi1 env
) with
1943 (false,(child1
,[])) ->
1944 output "and"; anno [] [child1
]
1945 | (_
,(child1
,res1)) ->
1946 let new_required = extend_required res1 required
in
1947 let new_required_states = get_required_states res1 in
1948 let new_required_states =
1949 get_reachable dir m
new_required_states in
1950 (match (pm,satv unchecked new_required new_required_states phi2
1952 (false,(child2
,[])) ->
1954 anno res1 [child1
;child2
]
1955 | (_
,(child2
,res2)) ->
1957 [] -> (* !Flag_ctl.partial_match must be true *)
1959 then anno [] [child1
; child2
]
1962 let s = mkstates states required_states
in
1964 (function a
-> function b
->
1965 strict_triples_conj strict
s a
[b
])
1966 [List.hd
res2] (List.tl
res2) in
1967 anno res [child1
; child2
]
1970 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1973 let s = mkstates states required_states
in
1975 (function a
-> function b
->
1976 strict_triples_conj strict
s a b
)
1978 anno res [child1
; child2
]
1981 "only one result allowed for the left arg of AndAny")))
1982 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1983 let pm = !Flag_ctl.partial_match
in
1984 (match (pm,satv unchecked required required_states phi1 env
) with
1985 (false,(child1
,[])) ->
1986 output "and"; anno [] [child1
]
1987 | (_
,(child1
,res1)) ->
1988 let new_required = extend_required res1 required
in
1989 let new_required_states = get_required_states res1 in
1990 let new_required_states =
1991 get_reachable dir m
new_required_states in
1992 (match (pm,satv unchecked new_required new_required_states phi2
1994 (false,(child2
,[])) ->
1996 anno res1 [child1
;child2
]
1997 | (_
,(child2
,res2)) ->
1999 let s = mkstates states required_states
in
2002 function (st
,th
,_
) as phi2_elem
->
2004 triples_complement [st
] [(st
,th
,[])] in
2005 strict_triples_conj_none strict
s acc
2006 (phi2_elem
::inverse))
2008 anno res [child1
; child2
]))
2009 | A.InnerAnd
(phi1
) ->
2010 let (child1
,res1) = satv unchecked required required_states phi1 env
in
2012 anno (inner_and res1) [child1
]
2014 let new_required_states =
2015 get_children_required_states dir m required_states
in
2017 satv unchecked required
new_required_states phi1 env
in
2019 anno (satEX dir m
res required_states
) [child
]
2020 | A.AX
(dir
,strict
,phi1
) ->
2021 let new_required_states =
2022 get_children_required_states dir m required_states
in
2024 satv unchecked required
new_required_states phi1 env
in
2026 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2029 let new_required_states = get_reachable dir m required_states
in
2031 satv unchecked required
new_required_states phi1 env
in
2033 anno (satEF dir m
res new_required_states) [child
]
2034 | A.AF
(dir
,strict
,phi1
) ->
2035 if !Flag_ctl.loop_in_src_code
2037 satv unchecked required required_states
2038 (A.AU
(dir
,strict
,A.True
,phi1
))
2041 (let new_required_states = get_reachable dir m required_states
in
2043 satv unchecked required
new_required_states phi1 env
in
2046 strict_A1 strict
satAF satEF dir m
res new_required_states in
2049 let new_required_states = get_reachable dir m required_states
in
2051 satv unchecked required
new_required_states phi1 env
in
2053 anno (satEG dir m
res new_required_states) [child
]
2054 | A.AG
(dir
,strict
,phi1
) ->
2055 let new_required_states = get_reachable dir m required_states
in
2057 satv unchecked required
new_required_states phi1 env
in
2059 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2062 | A.EU
(dir
,phi1
,phi2
) ->
2063 let new_required_states = get_reachable dir m required_states
in
2064 (match satv unchecked required
new_required_states phi2 env
with
2069 let new_required = extend_required res2 required
in
2071 satv unchecked new_required new_required_states phi1 env
in
2073 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2075 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2076 failwith
"should not be used" (*
2077 let new_required_states = get_reachable dir m required_states in
2078 (match satv unchecked required new_required_states phi2 env with
2080 output (Printf.sprintf "AW %b" unchecked); anno [] [child2]
2082 let new_required = extend_required res2 required in
2084 satv unchecked new_required new_required_states phi1 env in
2085 output (Printf.sprintf "AW %b" unchecked);
2087 strict_A2 strict satAW satEF dir m res1 res2
2088 new_required_states in
2089 anno res [child1; child2]) *)
2090 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2091 let new_required_states = get_reachable dir m required_states
in
2092 (match satv unchecked required
new_required_states phi2 env
with
2094 output "AU"; anno [] [child2
]
2096 let new_required = extend_required s2 required
in
2098 satv unchecked new_required new_required_states phi1 env
in
2101 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2102 (fun y str -> ()) in
2105 anno res [child1
; child2
]
2106 | AUfailed tmp_res
->
2107 (* found a loop, have to try AW *)
2109 A[E[phi1 U phi2] & phi1 W phi2]
2110 the and is nonstrict *)
2111 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2115 (satEU dir m
s1 tmp_res
new_required_states
2116 (* no graph, for the moment *)
2120 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2121 anno res [child1
; child2
]))
2122 | A.Implies
(phi1
,phi2
) ->
2123 satv unchecked required required_states
2124 (A.Or
(A.Not phi1
,phi2
))
2126 | A.Exists
(keep
,v
,phi1
) ->
2127 let new_required = drop_required v required
in
2129 satv unchecked new_required required_states phi1 env
in
2131 anno (triples_witness v
unchecked (not keep
) res) [child
]
2132 | A.Let
(v
,phi1
,phi2
) ->
2134 satv unchecked required required_states phi1 env
in
2136 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2137 anno res2 [child1
;child2
]
2138 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2139 let new_required_states = get_reachable dir m required_states
in
2141 satv unchecked required
new_required_states phi1 env
in
2143 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2144 anno res2 [child1
;child2
]
2147 let res = List.assoc v env
in
2150 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2153 | A.XX
(phi
) -> failwith
"should have been removed" in
2154 let res1 = drop_wits required_states
res phi
in
2158 print_required_states required_states
;
2159 print_state "after drop_wits" res1 end;
2164 let sat_verbose annotate maxlvl lvl m phi
=
2165 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2167 (* Type for annotations collected in a tree *)
2168 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2170 let sat_annotree annotate m phi
=
2171 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2172 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2176 let sat m phi = satloop m phi []
2180 let simpleanno l phi
res =
2182 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2183 print_generic_algo
(List.sort compare
res);
2184 Format.print_string
"\n------------------------------\n\n" in
2185 let pp_dir = function
2187 | A.BACKWARD
-> pp "^" in
2189 | A.False
-> pp "False"
2190 | A.True
-> pp "True"
2191 | A.Pred
(p
) -> pp ("Pred" ^
(Common.dump p
))
2192 | A.Not
(phi
) -> pp "Not"
2193 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Common.dump
(v
)))
2194 | A.And
(_
,phi1
,phi2
) -> pp "And"
2195 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2196 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2197 | A.Or
(phi1
,phi2
) -> pp "Or"
2198 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2199 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2200 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2201 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2202 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2203 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2204 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2205 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2206 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2207 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2208 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2209 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2210 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2211 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2212 | A.Uncheck
(s) -> pp "Uncheck"
2213 | A.InnerAnd
(s) -> pp "InnerAnd"
2214 | A.XX
(phi1
) -> pp "XX"
2218 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2219 print a ctl formula more accurately if you want.
2220 Use the print_xxx provided in the different module to call
2221 Pretty_print_ctl.pp_ctl.
2224 let simpleanno2 l phi
res =
2226 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2227 Format.print_newline
();
2228 Format.print_string
"----------------------------------------------------";
2229 Format.print_newline
();
2230 print_generic_algo
(List.sort compare
res);
2231 Format.print_newline
();
2232 Format.print_string
"----------------------------------------------------";
2233 Format.print_newline
();
2234 Format.print_newline
();
2238 (* ---------------------------------------------------------------------- *)
2240 (* ---------------------------------------------------------------------- *)
2242 type optentry
= bool ref * string
2243 type options
= {label : optentry
; unch
: optentry
;
2244 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2246 reqenv
: optentry
; reqstates
: optentry
}
2249 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2250 unch
= (pUNCHECK_OPT,"uncheck_opt");
2251 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2252 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2253 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2254 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2255 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2256 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2260 ("label ",[options.label]);
2261 ("unch ",[options.unch
]);
2262 ("unch and label ",[options.label;options.unch
])]
2265 [("conj ", [options.conj]);
2266 ("compl1 ", [options.compl1
]);
2267 ("compl12 ", [options.compl1
;options.compl2
]);
2268 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2269 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2271 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2272 ("compl12 unch satl ",
2273 [options.compl1;options.compl2;options.unch;options.label]); *)
2274 ("conj/compl12 unch satl ",
2275 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2278 [("newinfo ", [options.newinfo
]);
2279 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2282 [("reqenv ", [options.reqenv
]);
2283 ("reqstates ", [options.reqstates
]);
2284 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2285 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2286 ("reqstates unch satl ",
2287 [options.reqstates;options.unch;options.label]);*)
2288 ("reqenv/states unch satl ",
2289 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2292 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2293 options.newinfo
;options.reqenv
;options.reqstates
]
2296 [("all ",all_options)]
2298 let all_options_but_path =
2299 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2300 options.reqenv
;options.reqstates
]
2302 let all_but_path = ("all but path ",all_options_but_path)
2305 [(satAW_calls, "satAW", ref 0);
2306 (satAU_calls, "satAU", ref 0);
2307 (satEF_calls, "satEF", ref 0);
2308 (satAF_calls, "satAF", ref 0);
2309 (satEG_calls, "satEG", ref 0);
2310 (satAG_calls, "satAG", ref 0);
2311 (satEU_calls, "satEU", ref 0)]
2315 (function (opt
,x) ->
2316 (opt
,x,ref 0.0,ref 0,
2317 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2318 [List.hd
all;all_but_path]
2319 (*(all@baseline@conjneg@path@required)*)
2323 let rec iter fn = function
2325 | n
-> let _ = fn() in
2326 (Hashtbl.clear
reachable_table;
2327 Hashtbl.clear
memo_label;
2331 let copy_to_stderr fl
=
2332 let i = open_in fl
in
2334 Printf.fprintf stderr
"%s\n" (input_line
i);
2336 try loop() with _ -> ();
2339 let bench_sat (_,_,states) fn =
2340 List.iter (function (opt
,_) -> opt
:= false) all_options;
2343 (function (name
,options,time
,trips,counter_info
) ->
2344 let iterct = !Flag_ctl.bench
in
2345 if !time
> float_of_int
timeout then time
:= -100.0;
2346 if not
(!time
= -100.0)
2349 Hashtbl.clear
reachable_table;
2350 Hashtbl.clear
memo_label;
2351 List.iter (function (opt
,_) -> opt
:= true) options;
2352 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2356 let bef = Sys.time
() in
2358 Common.timeout_function
timeout
2360 let bef = Sys.time
() in
2361 let res = iter fn iterct in
2362 let aft = Sys.time
() in
2363 time
:= !time
+. (aft -. bef);
2364 trips := !trips + !triples;
2366 (function (calls
,_,save_calls
) ->
2367 function (current_calls
,current_cfg
,current_max_cfg
) ->
2369 !current_calls
+ (!calls
- !save_calls
);
2370 if (!calls
- !save_calls
) > 0
2372 (let st = List.length
states in
2373 current_cfg
:= !current_cfg
+ st;
2374 if st > !current_max_cfg
2375 then current_max_cfg
:= st))
2376 counters counter_info
;
2381 let aft = Sys.time
() in
2383 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2387 List.iter (function (opt
,_) -> opt
:= false) options;
2392 Printf.fprintf stderr
"\n";
2396 (if not
(List.for_all
(function x -> x = res) rest
)
2398 (List.iter (print_state "a state") answers;
2399 Printf.printf
"something doesn't work\n");
2403 let iterct = !Flag_ctl.bench
in
2407 (function (name
,options,time
,trips,counter_info
) ->
2408 Printf.fprintf stderr
"%s Numbers: %f %d "
2409 name
(!time
/. (float_of_int
iterct)) !trips;
2411 (function (calls
,cfg
,max_cfg
) ->
2412 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2414 Printf.fprintf stderr
"\n")
2417 (* ---------------------------------------------------------------------- *)
2418 (* preprocessing: ignore irrelevant functions *)
2420 let preprocess (cfg
,_,_) label = function
2421 [] -> true (* no information, try everything *)
2423 let sz = G.size cfg
in
2424 let verbose_output pred = function
2426 Printf.printf
"did not find:\n";
2427 P.print_predicate
pred; Format.print_newline
()
2429 Printf.printf
"found:\n";
2430 P.print_predicate
pred; Format.print_newline
();
2431 Printf.printf
"but it was not enough\n" in
2432 let get_any verbose
x =
2434 try Hashtbl.find
memo_label x
2437 (let triples = label x in
2439 List.map (function (st,th
,_) -> (st,th
)) triples in
2440 Hashtbl.add memo_label x filtered;
2442 if verbose
then verbose_output x res;
2445 (* don't bother testing when there are more patterns than nodes *)
2446 if List.length l
> sz-2
2448 else List.for_all
(get_any false) l
in
2449 if List.exists
get_all l
2452 (if !Flag_ctl.verbose_match
2454 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2458 let filter_partial_matches trips =
2459 if !Flag_ctl.partial_match
2461 let anynegwit = (* if any is neg, then all are *)
2462 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2464 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2467 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2471 (* ---------------------------------------------------------------------- *)
2472 (* Main entry point for engine *)
2473 let sat m phi reqopt
=
2475 (match !Flag_ctl.steps
with
2476 None
-> step_count := 0
2477 | Some
x -> step_count := x);
2478 Hashtbl.clear
reachable_table;
2479 Hashtbl.clear
memo_label;
2480 let (x,label,states) = m
in
2481 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2483 ((* to drop when Yoann initialized this flag *)
2484 if List.exists
(G.extract_is_loop
x) states
2485 then Flag_ctl.loop_in_src_code
:= true;
2486 let m = (x,label,List.sort compare
states) in
2488 if(!Flag_ctl.verbose_ctl_engine
)
2490 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2491 if !Flag_ctl.bench
> 0
2495 let fn _ = satloop false [] None
m phi
[] in
2496 if !Flag_ctl.bench
> 0
2498 else Common.profile_code
"ctl" (fun _ -> fn()) in
2499 let res = filter_partial_matches res in
2501 Printf.printf "steps: start %d, stop %d\n"
2502 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2504 Printf.printf "triples: %d\n" !triples;
2505 print_state "final result" res;
2507 List.sort compare
res)
2509 (if !Flag_ctl.verbose_ctl_engine
2510 then Common.pr2
"missing something required";
2514 (* ********************************************************************** *)
2515 (* End of Module: CTL_ENGINE *)
2516 (* ********************************************************************** *)