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.
28 (*external c_counter : unit -> int = "c_counter"*)
30 (* Optimize triples_conj by first extracting the intersection of the two sets,
31 which can certainly be in the intersection *)
32 let pTRIPLES_CONJ_OPT = ref true
33 (* For complement, make NegState for the negation of a single state *)
34 let pTRIPLES_COMPLEMENT_OPT = ref true
35 (* For complement, do something special for the case where the environment
36 and witnesses are empty *)
37 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref true
38 (* "Double negate" the arguments of the path operators *)
39 let pDOUBLE_NEGATE_OPT = ref true
40 (* Only do pre_forall/pre_exists on new elements in fixpoint iteration *)
41 let pNEW_INFO_OPT = ref true
42 (* Filter the result of the label function to drop entries that aren't
43 compatible with any of the available environments *)
44 let pREQUIRED_ENV_OPT = ref true
45 (* Memoize the raw result of the label function *)
46 let pSATLABEL_MEMO_OPT = ref true
47 (* Filter results according to the required states *)
48 let pREQUIRED_STATES_OPT = ref true
49 (* Drop negative witnesses at Uncheck *)
50 let pUNCHECK_OPT = ref true
51 let pANY_NEG_OPT = ref true
52 let pLazyOpt = ref true
54 (* Nico: This stack is use for graphical traces *)
55 let graph_stack = ref ([] : string list
)
56 let graph_hash = (Hashtbl.create
101)
59 let pTRIPLES_CONJ_OPT = ref false
60 let pTRIPLES_COMPLEMENT_OPT = ref false
61 let pTRIPLES_COMPLEMENT_SIMPLE_OPT = ref false
62 let pDOUBLE_NEGATE_OPT = ref false
63 let pNEW_INFO_OPT = ref false
64 let pREQUIRED_ENV_OPT = ref false
65 let pSATLABEL_MEMO_OPT = ref false
66 let pREQUIRED_STATES_OPT = ref false
67 let pUNCHECK_OPT = ref false
68 let pANY_NEG_OPT = ref false
69 let pLazyOpt = ref false
73 let step_count = ref 0
76 if not
(!step_count = 0)
79 step_count := !step_count - 1;
80 if !step_count = 0 then raise Steps
83 let inc cell
= cell
:= !cell
+ 1
85 let satEU_calls = ref 0
86 let satAW_calls = ref 0
87 let satAU_calls = ref 0
88 let satEF_calls = ref 0
89 let satAF_calls = ref 0
90 let satEG_calls = ref 0
91 let satAG_calls = ref 0
99 Printf.sprintf
"_fresh_r_%d" c
101 (* **********************************************************************
103 * Implementation of a Witness Tree model checking engine for CTL-FVex
106 * **********************************************************************)
108 (* ********************************************************************** *)
109 (* Module: SUBST (substitutions: meta. vars and values) *)
110 (* ********************************************************************** *)
116 val eq_mvar
: mvar
-> mvar
-> bool
117 val eq_val
: value -> value -> bool
118 val merge_val
: value -> value -> value
119 val print_mvar
: mvar
-> unit
120 val print_value
: value -> unit
124 (* ********************************************************************** *)
125 (* Module: GRAPH (control flow graphs / model) *)
126 (* ********************************************************************** *)
132 val predecessors
: cfg
-> node
-> node list
133 val successors
: cfg
-> node
-> node list
134 val extract_is_loop
: cfg
-> node
-> bool
135 val print_node
: node
-> unit
136 val size
: cfg
-> int
137 val print_graph
: cfg
-> string option ->
138 (node
* string) list
-> (node
* string) list
-> string -> unit
142 module OGRAPHEXT_GRAPH
=
145 type cfg
= (string,unit) Ograph_extended.ograph_mutable
;;
146 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
);;
147 let print_node i
= Format.print_string
(Common.i_to_s i
)
151 (* ********************************************************************** *)
152 (* Module: PREDICATE (predicates for CTL formulae) *)
153 (* ********************************************************************** *)
155 module type PREDICATE
=
158 val print_predicate
: t
-> unit
162 (* ********************************************************************** *)
164 (* ---------------------------------------------------------------------- *)
165 (* Misc. useful generic functions *)
166 (* ---------------------------------------------------------------------- *)
168 let get_graph_files () = !graph_stack
169 let get_graph_comp_files outfile
= Hashtbl.find_all
graph_hash outfile
179 let foldl = List.fold_left
;;
181 let foldl1 f xs
= foldl f
(head xs
) (tail xs
)
183 type 'a esc
= ESC
of 'a
| CONT
of 'a
185 let foldr = List.fold_right
;;
187 let concat = List.concat;;
191 let filter = List.filter;;
193 let partition = List.partition;;
195 let concatmap f l
= List.concat (List.map f l
);;
203 let some_map f opts
= map (maybe (fun x
-> Some
(f x
)) None
) opts
205 let some_tolist_alt opts
= concatmap (maybe (fun x
-> [x
]) []) opts
207 let rec some_tolist opts
=
210 | (Some x
)::rest
-> x
::(some_tolist rest
)
211 | _
::rest
-> some_tolist rest
214 let rec groupBy eq l
=
218 let (xs1
,xs2
) = partition (fun x'
-> eq x x'
) xs
in
219 (x
::xs1
)::(groupBy eq xs2
)
222 let group l
= groupBy (=) l
;;
224 let rec memBy eq x l
=
227 | (y
::ys
) -> if (eq x y
) then true else (memBy eq x ys
)
230 let rec nubBy eq ls
=
233 | (x
::xs
) when (memBy eq x xs
) -> nubBy eq xs
234 | (x
::xs
) -> x
::(nubBy eq xs
)
240 | (x
::xs
) when (List.mem x xs
) -> nub xs
241 | (x
::xs
) -> x
::(nub xs
)
244 let state_compare (s1
,_
,_
) (s2
,_
,_
) = compare s1 s2
246 let setifyBy eq xs
= nubBy eq xs
;;
248 let setify xs
= nub xs
;;
250 let inner_setify xs
= List.sort compare
(nub xs
);;
252 let unionBy compare eq xs
= function
255 let rec loop = function
257 | x
::xs
-> if memBy eq x ys
then loop xs
else x
::(loop xs
) in
258 List.sort compare
(loop xs
)
261 let union xs ys
= unionBy state_compare (=) xs ys
;;
263 let setdiff xs ys
= filter (fun x
-> not
(List.mem x ys
)) xs
;;
265 let subseteqBy eq xs ys
= List.for_all
(fun x
-> memBy eq x ys
) xs
;;
267 let subseteq xs ys
= List.for_all
(fun x
-> List.mem x ys
) xs
;;
268 let supseteq xs ys
= subseteq ys xs
270 let setequalBy eq xs ys
= (subseteqBy eq xs ys
) & (subseteqBy eq ys xs
);;
272 let setequal xs ys
= (subseteq xs ys
) & (subseteq ys xs
);;
274 (* Fix point calculation *)
276 let x'
= f
x in if (eq
x'
x) then x'
else fix eq f
x'
279 (* Fix point calculation on set-valued functions *)
280 let setfix f
x = (fix subseteq f
x) (*if new is a subset of old, stop*)
281 let setgfix f
x = (fix supseteq f
x) (*if new is a supset of old, stop*)
283 let get_states l
= nub (List.map (function (s
,_
,_
) -> s
) l
)
285 (* ********************************************************************** *)
286 (* Module: CTL_ENGINE *)
287 (* ********************************************************************** *)
290 functor (SUB
: SUBST
) ->
291 functor (G
: GRAPH
) ->
292 functor (P
: PREDICATE
) ->
297 type substitution
= (SUB.mvar
, SUB.value) Ast_ctl.generic_substitution
299 type ('pred
,'anno
) witness
=
300 (G.node
, substitution
,
301 ('pred
, SUB.mvar
, 'anno
) Ast_ctl.generic_ctl list
)
302 Ast_ctl.generic_witnesstree
304 type ('pred
,'anno
) triples =
305 (G.node
* substitution
* ('pred
,'anno
) witness list
) list
307 (* ---------------------------------------------------------------------- *)
308 (* Pretty printing functions *)
309 (* ---------------------------------------------------------------------- *)
311 let (print_generic_substitution
: substitution
-> unit) = fun substxs
->
312 let print_generic_subst = function
314 SUB.print_mvar mvar
; Format.print_string
" --> "; SUB.print_value v
315 | A.NegSubst
(mvar
, v
) ->
316 SUB.print_mvar mvar
; Format.print_string
" -/-> "; SUB.print_value v
in
317 Format.print_string
"[";
318 Common.print_between
(fun () -> Format.print_string
";" )
319 print_generic_subst substxs
;
320 Format.print_string
"]"
322 let rec (print_generic_witness
: ('pred
, 'anno
) witness
-> unit) =
324 | A.Wit
(state
, subst
, anno
, childrens
) ->
325 Format.print_string
"wit ";
327 print_generic_substitution subst
;
328 (match childrens
with
329 [] -> Format.print_string
"{}"
331 Format.force_newline
(); Format.print_string
" "; Format.open_box
0;
332 print_generic_witnesstree childrens
; Format.close_box
())
334 Format.print_string
"!";
335 print_generic_witness wit
337 and (print_generic_witnesstree
: ('pred
,'anno
) witness list
-> unit) =
340 Format.print_string
"{";
342 (fun () -> Format.print_string
";"; Format.force_newline
() )
343 print_generic_witness witnesstree
;
344 Format.print_string
"}";
347 and print_generic_triple
(node
,subst
,tree
) =
349 print_generic_substitution subst
;
350 print_generic_witnesstree tree
352 and (print_generic_algo
: ('pred
,'anno
) triples -> unit) = fun xs
->
353 Format.print_string
"<";
355 (fun () -> Format.print_string
";"; Format.force_newline
())
356 print_generic_triple xs
;
357 Format.print_string
">"
360 let print_state (str
: string) (l
: ('pred
,'anno
) triples) =
361 Printf.printf
"%s\n" str
;
362 List.iter
(function x ->
363 print_generic_triple
x; Format.print_newline
(); flush stdout
)
364 (List.sort compare l
);
367 let print_required_states = function
368 None
-> Printf.printf
"no required states\n"
370 Printf.printf
"required states: ";
373 G.print_node x; Format.print_string
" "; Format.print_flush
())
377 let mkstates states
= function
379 | Some states
-> states
381 let print_graph grp required_states res str
= function
382 A.Exists
(keep
,v
,phi
) -> ()
384 if !Flag_ctl.graphical_trace
&& not
!Flag_ctl.checking_reachability
387 | A.Exists
(keep
,v
,phi
) -> ()
390 Printf.sprintf
"%s%s"
392 (Common.format_to_string
394 Pretty_print_ctl.pp_ctl
395 (P.print_predicate
, SUB.print_mvar
)
398 let file = (match !Flag.currentfile
with
399 None
-> "graphical_trace"
402 (if not
(List.mem
file !graph_stack) then
403 graph_stack := file :: !graph_stack);
404 let filename = Filename.temp_file
(file^
":") ".dot" in
405 Hashtbl.add
graph_hash file filename;
407 (if !Flag_ctl.gt_without_label
then None
else (Some
label))
408 (match required_states
with
410 | Some required_states
->
411 (List.map (function s
-> (s
,"blue")) required_states
))
412 (List.map (function (s
,_
,_
) -> (s
,"\"#FF8080\"")) res
) filename
414 let print_graph_c grp required_states res
ctr phi
=
415 let str = "iter: "^
(string_of_int
!ctr) in
416 print_graph grp required_states res
str phi
418 (* ---------------------------------------------------------------------- *)
420 (* ---------------------------------------------------------------------- *)
423 (* ************************* *)
425 (* ************************* *)
430 | A.NegSubst
(x,_
) -> x
436 | A.NegSubst
(_
,x) -> x
439 let eq_subBy eqx eqv sub sub'
=
440 match (sub
,sub'
) with
441 | (A.Subst
(x,v
),A.Subst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
442 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) -> (eqx
x x'
) && (eqv v v'
)
447 let eq_sub sub sub'
= eq_subBy SUB.eq_mvar
SUB.eq_val sub sub'
449 let eq_subst th th'
= setequalBy eq_sub th th'
;;
451 let merge_subBy eqx
(===) (>+<) sub sub'
=
452 (* variable part is guaranteed to be the same *)
453 match (sub
,sub'
) with
454 (A.Subst
(x,v
),A.Subst
(x'
,v'
)) ->
456 then Some
[A.Subst
(x, v
>+< v'
)]
458 | (A.NegSubst
(x,v
),A.Subst
(x'
,v'
)) ->
460 then Some
[A.Subst
(x'
,v'
)]
462 | (A.Subst
(x,v
),A.NegSubst
(x'
,v'
)) ->
464 then Some
[A.Subst
(x,v
)]
466 | (A.NegSubst
(x,v
),A.NegSubst
(x'
,v'
)) ->
469 let merged = v
>+< v'
in
470 if merged = v
&& merged = v'
471 then Some
[A.NegSubst
(x,v
>+< v'
)]
473 (* positions are compatible, but not identical. keep apart. *)
474 Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
475 else Some
[A.NegSubst
(x,v
);A.NegSubst
(x'
,v'
)]
479 (* How could we accomadate subterm constraints here??? *)
480 let merge_sub sub sub'
=
481 merge_subBy SUB.eq_mvar
SUB.eq_val
SUB.merge_val sub sub'
483 let clean_substBy eq cmp theta
= List.sort cmp
(nubBy eq theta
);;
485 (* NOTE: we sort by using the generic "compare" on (meta-)variable
486 * names; we could also require a definition of compare for meta-variables
487 * or substitutions but that seems like overkill for sorting
489 let clean_subst theta
=
493 let res = compare
(dom_sub s
) (dom_sub s'
) in
497 (A.Subst
(_
,_
),A.NegSubst
(_
,_
)) -> -1
498 | (A.NegSubst
(_
,_
),A.Subst
(_
,_
)) -> 1
499 | _
-> compare
(ran_sub s
) (ran_sub s'
)
502 let rec loop = function
504 | (A.Subst
(x,v
)::A.NegSubst
(y
,v'
)::rest
) when SUB.eq_mvar
x y
->
505 loop (A.Subst
(x,v
)::rest
)
506 | x::xs
-> x::(loop xs
) in
509 let top_subst = [];; (* Always TRUE subst. *)
511 (* Split a theta in two parts: one with (only) "x" and one without *)
513 let split_subst theta
x =
514 partition (fun sub
-> SUB.eq_mvar
(dom_sub sub
) x) theta
;;
516 exception SUBST_MISMATCH
517 let conj_subst theta theta'
=
518 match (theta
,theta'
) with
519 | ([],_
) -> Some theta'
520 | (_
,[]) -> Some theta
522 let rec classify = function
524 | [x] -> [(dom_sub x,[x])]
526 (match classify xs
with
527 ((nm
,y
)::ys
) as res ->
530 else (dom_sub x,[x])::res
531 | _
-> failwith
"not possible") in
532 let merge_all theta theta'
=
539 match (merge_sub sub sub'
) with
540 Some subs
-> subs
@ rest
541 | _
-> raise SUBST_MISMATCH
)
544 let rec loop = function
546 List.concat (List.map (function (_
,ths
) -> ths
) ctheta'
)
548 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
549 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
550 (match compare
x y
with
551 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
552 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
553 | 1 -> ths'
@ loop (((x,ths
)::xs
),ys
)
554 | _
-> failwith
"not possible") in
555 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
556 with SUBST_MISMATCH
-> None
559 (* theta' must be a subset of theta *)
560 let conj_subst_none theta theta'
=
561 match (theta
,theta'
) with
562 | (_
,[]) -> Some theta
565 let rec classify = function
567 | [x] -> [(dom_sub x,[x])]
569 (match classify xs
with
570 ((nm
,y
)::ys
) as res ->
573 else (dom_sub x,[x])::res
574 | _
-> failwith
"not possible") in
575 let merge_all theta theta'
=
582 match (merge_sub sub sub'
) with
583 Some subs
-> subs
@ rest
584 | _
-> raise SUBST_MISMATCH
)
587 let rec loop = function
589 List.concat (List.map (function (_
,ths
) -> ths
) ctheta
)
590 | ([],ctheta'
) -> raise SUBST_MISMATCH
591 | ((x,ths
)::xs
,(y
,ths'
)::ys
) ->
592 (match compare
x y
with
593 0 -> (merge_all ths ths'
) @ loop (xs
,ys
)
594 | -1 -> ths
@ loop (xs
,((y
,ths'
)::ys
))
595 | 1 -> raise SUBST_MISMATCH
596 | _
-> failwith
"not possible") in
597 try Some
(clean_subst(loop (classify theta
, classify theta'
)))
598 with SUBST_MISMATCH
-> None
603 | A.Subst
(x,v
) -> A.NegSubst
(x,v
)
604 | A.NegSubst
(x,v
) -> A.Subst
(x,v
)
607 (* Turn a (big) theta into a list of (small) thetas *)
608 let negate_subst theta
= (map (fun sub
-> [negate_sub sub
]) theta
);;
611 (* ************************* *)
613 (* ************************* *)
615 (* Always TRUE witness *)
616 let top_wit = ([] : (('pred
, 'anno
) witness list
));;
618 let eq_wit wit wit'
= wit
= wit'
;;
620 let union_wit wit wit'
= (*List.sort compare (wit' @ wit) for popl*)
621 let res = unionBy compare
(=) wit wit'
in
622 let anynegwit = (* if any is neg, then all are *)
623 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
625 then List.filter (function A.NegWit _
-> true | A.Wit _
-> false) res
628 let negate_wit wit
= A.NegWit wit
(*
630 | A.Wit(s,th,anno,ws) -> A.NegWitWit(s,th,anno,ws)
631 | A.NegWitWit(s,th,anno,ws) -> A.Wit(s,th,anno,ws)*)
634 let negate_wits wits
=
635 List.sort compare
(map (fun wit
-> [negate_wit wit
]) wits
);;
638 let anynegwit = (* if any is neg, then all are *)
639 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
643 function (s
,th
,wit
) ->
644 if anynegwit wit
then prev
else (s
,th
,top_wit)::prev
)
647 (* ************************* *)
649 (* ************************* *)
651 (* Triples are equal when the constituents are equal *)
652 let eq_trip (s
,th
,wit
) (s'
,th'
,wit'
) =
653 (s
= s'
) && (eq_wit wit wit'
) && (eq_subst th th'
);;
655 let triples_top states
= map (fun s
-> (s
,top_subst,top_wit)) states
;;
657 let normalize trips
=
659 (function (st
,th
,wit
) -> (st
,List.sort compare th
,List.sort compare wit
))
663 (* conj opt doesn't work ((1,[],{{x=3}}) v (1,[],{{x=4}})) & (1,[],{{x=4}}) =
664 (1,[],{{x=3},{x=4}}), not (1,[],{{x=4}}) *)
665 let triples_conj trips trips'
=
666 let (trips
,shared
,trips'
) =
667 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
670 List.partition (function t
-> List.mem t trips'
) trips
in
672 List.filter (function t
-> not
(List.mem t shared
)) trips'
in
673 (trips,shared
,trips'
)
674 else (trips,[],trips'
) in
675 foldl (* returns a set - setify inlined *)
677 function (s1
,th1
,wit1
) ->
680 function (s2
,th2
,wit2
) ->
682 (match (conj_subst th1 th2
) with
684 let t = (s1
,th
,union_wit wit1 wit2
) in
685 if List.mem
t rest
then rest
else t::rest
692 (* ignore the state in the right argument. always pretend it is the same as
694 (* env on right has to be a subset of env on left *)
695 let triples_conj_none trips trips'
=
696 let (trips,shared
,trips'
) =
697 if false && !pTRIPLES_CONJ_OPT (* see comment above *)
700 List.partition (function t -> List.mem
t trips'
) trips in
702 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
703 (trips,shared
,trips'
)
704 else (trips,[],trips'
) in
705 foldl (* returns a set - setify inlined *)
707 function (s1
,th1
,wit1
) ->
710 function (s2
,th2
,wit2
) ->
711 match (conj_subst_none th1 th2
) with
713 let t = (s1
,th
,union_wit wit1 wit2
) in
714 if List.mem
t rest
then rest
else t::rest
722 let triples_conj_AW trips trips'
=
723 let (trips,shared
,trips'
) =
724 if false && !pTRIPLES_CONJ_OPT
727 List.partition (function t -> List.mem
t trips'
) trips in
729 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
730 (trips,shared
,trips'
)
731 else (trips,[],trips'
) in
732 foldl (* returns a set - setify inlined *)
734 function (s1
,th1
,wit1
) ->
737 function (s2
,th2
,wit2
) ->
739 (match (conj_subst th1 th2
) with
741 let t = (s1
,th
,union_wit wit1 wit2
) in
742 if List.mem
t rest
then rest
else t::rest
749 (* *************************** *)
750 (* NEGATION (NegState style) *)
751 (* *************************** *)
753 (* Constructive negation at the state level *)
756 | NegState
of 'a list
759 let compatible_states = function
760 (PosState s1
, PosState s2
) ->
761 if s1
= s2
then Some
(PosState s1
) else None
762 | (PosState s1
, NegState s2
) ->
763 if List.mem s1 s2
then None
else Some
(PosState s1
)
764 | (NegState s1
, PosState s2
) ->
765 if List.mem s2 s1
then None
else Some
(PosState s2
)
766 | (NegState s1
, NegState s2
) -> Some
(NegState
(s1
@ s2
))
769 (* Conjunction on triples with "special states" *)
770 let triples_state_conj trips trips'
=
771 let (trips,shared
,trips'
) =
772 if !pTRIPLES_CONJ_OPT
775 List.partition (function t -> List.mem
t trips'
) trips in
777 List.filter (function t -> not
(List.mem
t shared
)) trips'
in
778 (trips,shared
,trips'
)
779 else (trips,[],trips'
) in
782 function (s1
,th1
,wit1
) ->
785 function (s2
,th2
,wit2
) ->
786 match compatible_states(s1
,s2
) with
788 (match (conj_subst th1 th2
) with
790 let t = (s
,th
,union_wit wit1 wit2
) in
791 if List.mem
t rest
then rest
else t::rest
798 let triple_negate (s
,th
,wits
) =
799 let negstates = (NegState
[s
],top_subst,top_wit) in
800 let negths = map (fun th
-> (PosState s
,th
,top_wit)) (negate_subst th
) in
801 let negwits = map (fun nwit
-> (PosState s
,th
,nwit
)) (negate_wits wits
) in
802 negstates :: (negths @ negwits) (* all different *)
804 (* FIX ME: it is not necessary to do full conjunction *)
805 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
806 if !pTRIPLES_COMPLEMENT_OPT
808 (let cleanup (s
,th
,wit
) =
810 PosState s'
-> [(s'
,th
,wit
)]
812 assert (th
=top_subst);
813 assert (wit
=top_wit);
814 map (fun st
-> (st
,top_subst,top_wit)) (setdiff states ss
) in
815 let (simple
,complex
) =
816 if !pTRIPLES_COMPLEMENT_SIMPLE_OPT
818 let (simple
,complex
) =
819 List.partition (function (s
,[],[]) -> true | _
-> false) trips in
821 [(NegState
(List.map (function (s
,_
,_
) -> s
) simple),
822 top_subst,top_wit)] in
824 else ([(NegState
[],top_subst,top_wit)],trips) in
825 let rec compl trips =
828 | (t::ts
) -> triples_state_conj (triple_negate t) (compl ts
) in
829 let compld = (compl complex
) in
830 let compld = concatmap cleanup compld in
833 let negstates (st
,th
,wits
) =
834 map (function st
-> (st
,top_subst,top_wit)) (setdiff states
[st
]) in
835 let negths (st
,th
,wits
) =
836 map (function th
-> (st
,th
,top_wit)) (negate_subst th
) in
837 let negwits (st
,th
,wits
) =
838 map (function nwit
-> (st
,th
,nwit
)) (negate_wits wits
) in
840 [] -> map (function st
-> (st
,top_subst,top_wit)) states
846 triples_conj (negstates cur
@ negths cur
@ negwits cur
) prev
)
847 (negstates x @ negths x @ negwits x) xs
)
850 let triple_negate (s
,th
,wits
) =
851 let negths = map (fun th
-> (s
,th
,top_wit)) (negate_subst th
) in
852 let negwits = map (fun nwit
-> (s
,th
,nwit
)) (negate_wits wits
) in
853 ([s
], negths @ negwits) (* all different *)
855 let print_compl_state str (n
,p
) =
856 Printf.printf
"%s neg: " str;
858 (function x -> G.print_node x; Format.print_flush
(); Printf.printf
" ")
863 let triples_complement states
(trips : ('pred
, 'anno
) triples) =
865 then map (function st
-> (st
,top_subst,top_wit)) states
867 let cleanup (neg
,pos
) =
869 List.filter (function (s
,_
,_
) -> List.mem s neg
) pos
in
870 (map (fun st
-> (st
,top_subst,top_wit)) (setdiff states neg
)) @
872 let trips = List.sort
state_compare trips in
873 let all_negated = List.map triple_negate trips in
874 let merge_one (neg1
,pos1
) (neg2
,pos2
) =
875 let (pos1conj
,pos1keep
) =
876 List.partition (function (s
,_
,_
) -> List.mem s neg2
) pos1
in
877 let (pos2conj
,pos2keep
) =
878 List.partition (function (s
,_
,_
) -> List.mem s neg1
) pos2
in
879 (Common.union_set neg1 neg2
,
880 (triples_conj pos1conj pos2conj
) @ pos1keep
@ pos2keep
) in
881 let rec inner_loop = function
882 x1
::x2
::rest
-> (merge_one x1 x2
) :: (inner_loop rest
)
884 let rec outer_loop = function
886 | l
-> outer_loop (inner_loop l
) in
887 cleanup (outer_loop all_negated)
889 (* ********************************** *)
890 (* END OF NEGATION (NegState style) *)
891 (* ********************************** *)
893 (* now this is always true, so we could get rid of it *)
894 let something_dropped = ref true
896 let triples_union trips trips'
=
897 (*unionBy compare eq_trip trips trips';;*)
898 (* returns -1 is t1 > t2, 1 if t2 >= t1, and 0 otherwise *)
900 The following does not work. Suppose we have ([x->3],{A}) and ([],{A,B}).
901 Then, the following says that since the first is a more restrictive
902 environment and has fewer witnesses, then it should be dropped. But having
903 fewer witnesses is not necessarily less informative than having more,
904 because fewer witnesses can mean the absence of the witness-causing thing.
905 So the fewer witnesses have to be kept around.
906 subseteq changed to = to make it hopefully work
911 something_dropped := false;
913 then (something_dropped := true; trips)
915 let subsumes (s1
,th1
,wit1
) (s2
,th2
,wit2
) =
918 (match conj_subst th1 th2
with
921 then if (*subseteq*) wit1
= wit2
then 1 else 0
924 then if (*subseteq*) wit2
= wit1
then (-1) else 0
928 let rec first_loop second
= function
930 | x::xs
-> first_loop (second_loop
x second
) xs
931 and second_loop
x = function
934 match subsumes x y
with
935 1 -> something_dropped := true; all
936 | (-1) -> second_loop
x ys
937 | _
-> y
::(second_loop
x ys
) in
938 first_loop trips trips'
940 else unionBy compare
eq_trip trips trips'
943 let triples_witness x unchecked not_keep
trips =
944 let anyneg = (* if any is neg, then all are *)
945 List.exists
(function A.NegSubst _
-> true | A.Subst _
-> false) in
946 let anynegwit = (* if any is neg, then all are *)
947 List.exists
(function A.NegWit _
-> true | A.Wit _
-> false) in
948 let allnegwit = (* if any is neg, then all are *)
949 List.for_all
(function A.NegWit _
-> true | A.Wit _
-> false) in
951 List.map (function A.NegWit w
-> w
| A.Wit _
-> failwith
"bad wit")in
955 function (s
,th
,wit
) as t ->
956 let (th_x
,newth
) = split_subst th
x in
959 (* one consider whether if not not_keep is true, then we should
960 fail. but it could be that the variable is a used_after and
961 then it is the later rule that should fail and not this one *)
962 if not not_keep
&& !Flag_ctl.verbose_ctl_engine
964 (SUB.print_mvar
x; Format.print_flush
();
965 print_state ": empty witness from" [t]);
967 | l
when anyneg l
&& !pANY_NEG_OPT -> prev
968 (* see tests/nestseq for how neg bindings can come up even
969 without eg partial matches
970 (* negated substitution only allowed with negwits.
972 if anynegwit wit
&& allnegwit wit
(* nonempty negwit list *)
975 (print_generic_substitution l
; Format.print_newline
();
976 failwith
"unexpected negative binding with positive witnesses")*)
979 if unchecked
or not_keep
982 if anynegwit wit
&& allnegwit wit
983 then (s
,newth
,[A.NegWit
(A.Wit
(s
,th_x
,[],negtopos wit
))])
984 else (s
,newth
,[A.Wit
(s
,th_x
,[],wit
)]) in
987 if unchecked
|| !Flag_ctl.partial_match
(* the only way to have a NegWit *)
993 (* ---------------------------------------------------------------------- *)
994 (* SAT - Model Checking Algorithm for CTL-FVex *)
996 (* TODO: Implement _all_ operators (directly) *)
997 (* ---------------------------------------------------------------------- *)
1000 (* ************************************* *)
1001 (* The SAT algorithm and special helpers *)
1002 (* ************************************* *)
1004 let rec pre_exist dir
(grp
,_
,_
) y reqst
=
1006 match reqst
with None
-> true | Some reqst
-> List.mem s reqst
in
1007 let exp (s
,th
,wit
) =
1009 (fun s'
-> if check s'
then [(s'
,th
,wit
)] else [])
1011 A.FORWARD
-> G.predecessors grp s
1012 | A.BACKWARD
-> G.successors grp s
) in
1013 setify (concatmap exp y
)
1018 let pre_forall dir
(grp
,_
,states
) y all reqst
=
1021 None
-> true | Some reqst
-> List.mem s reqst
in
1024 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1027 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1030 (function p
-> (p
,succ grp p
))
1033 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1034 (* would a hash table be more efficient? *)
1035 let all = List.sort
state_compare all in
1036 let rec up_nodes child s
= function
1038 | (s1
,th
,wit
)::xs
->
1039 (match compare s1 child
with
1040 -1 -> up_nodes child s xs
1041 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1043 let neighbor_triples =
1046 function (s
,children
) ->
1050 match up_nodes child s
all with [] -> raise Empty
| l
-> l
)
1054 match neighbor_triples with
1058 (foldl1 (@) (List.map (foldl1 triples_conj) neighbor_triples))
1060 let pre_forall_AW dir
(grp
,_
,states
) y
all reqst
=
1063 None
-> true | Some reqst
-> List.mem s reqst
in
1066 A.FORWARD
-> G.predecessors | A.BACKWARD
-> G.successors
in
1069 A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1072 (function p
-> (p
,succ grp p
))
1075 (function (s
,_
,_
) -> List.filter check (pred grp s
)) y
)) in
1076 (* would a hash table be more efficient? *)
1077 let all = List.sort
state_compare all in
1078 let rec up_nodes child s
= function
1080 | (s1
,th
,wit
)::xs
->
1081 (match compare s1 child
with
1082 -1 -> up_nodes child s xs
1083 | 0 -> (s
,th
,wit
)::(up_nodes child s xs
)
1085 let neighbor_triples =
1088 function (s
,children
) ->
1091 match up_nodes child s
all with [] -> raise AW
| l
-> l
)
1094 match neighbor_triples with
1096 | _
-> foldl1 (@) (List.map (foldl1 triples_conj_AW) neighbor_triples)
1098 (* drop_negwits will call setify *)
1099 let satEX dir m s reqst
= pre_exist dir m s reqst
;;
1101 let satAX dir m s reqst
= pre_forall dir m s s reqst
1104 (* E[phi1 U phi2] == phi2 \/ (phi1 /\ EXE[phi1 U phi2]) *)
1105 let satEU dir
((_
,_
,states
) as m
) s1 s2 reqst
print_graph =
1106 (*Printf.printf "EU\n";
1107 let ctr = ref 0 in*)
1112 (*let ctr = ref 0 in*)
1115 let rec f y new_info
=
1121 print_graph y ctr;*)
1122 let first = triples_conj s1
(pre_exist dir m new_info reqst
) in
1123 let res = triples_union first y
in
1124 let new_info = setdiff res y
in
1125 (*Printf.printf "iter %d res %d new_info %d\n"
1126 !ctr (List.length res) (List.length new_info);
1127 print_state "res" res;
1128 print_state "new_info" new_info;
1136 print_graph y ctr;*)
1137 let pre = pre_exist dir m y reqst
in
1138 triples_union s2
(triples_conj s1
pre) in
1142 (* EF phi == E[true U phi] *)
1143 let satEF dir m s2 reqst
=
1145 (*let ctr = ref 0 in*)
1148 let rec f y
new_info =
1154 print_state (Printf.sprintf "iteration %d\n" !ctr) y;*)
1155 let first = pre_exist dir m
new_info reqst
in
1156 let res = triples_union first y
in
1157 let new_info = setdiff res y
in
1158 (*Printf.printf "EF %s iter %d res %d new_info %d\n"
1159 (if dir = A.BACKWARD then "reachable" else "real ef")
1160 !ctr (List.length res) (List.length new_info);
1161 print_state "new info" new_info;
1168 let pre = pre_exist dir m y reqst
in
1169 triples_union s2
pre in
1173 type ('
pred,'anno
) auok
=
1174 AUok
of ('
pred,'anno
) triples | AUfailed
of ('
pred,'anno
) triples
1176 (* A[phi1 U phi2] == phi2 \/ (phi1 /\ AXA[phi1 U phi2]) *)
1177 let satAU dir
((cfg
,_
,states
) as m
) s1 s2 reqst
print_graph =
1183 (*let ctr = ref 0 in*)
1185 if !Flag_ctl.loop_in_src_code
1190 let rec f y newinfo
=
1196 (*print_state (Printf.sprintf "iteration %d\n" !ctr) y;
1200 try Some
(pre_forall dir m
new_info y reqst
)
1205 match triples_conj s1
pre with
1208 (*print_state "s1" s1;
1209 print_state "pre" pre;
1210 print_state "first" first;*)
1211 let res = triples_union first y
in
1213 if not
!something_dropped
1215 else setdiff res y
in
1217 "iter %d res %d new_info %d\n"
1218 !ctr (List.length res) (List.length new_info);
1223 if !Flag_ctl.loop_in_src_code
1227 fix (function s1 -> function s2 ->
1228 let s1 = List.map (function (s,th,w) -> (s,th,nub w)) s1 in
1229 let s2 = List.map (function (s,th,w) -> (s,th,nub w)) s2 in
1230 subseteq s1 s2) in for popl *)
1235 let pre = pre_forall dir m y y reqst
in
1236 triples_union s2 (triples_conj s1 pre) in
1241 (* reqst could be the states of s1 *)
1243 let lstates = mkstates states reqst in
1244 let initial_removed =
1245 triples_complement lstates (triples_union s1 s2) in
1246 let initial_base = triples_conj s1 (triples_complement lstates s2) in
1247 let rec loop base removed =
1249 triples_conj base (pre_exist dir m removed reqst) in
1251 triples_conj base (triples_complement lstates new_removed) in
1252 if supseteq new_base base
1253 then triples_union base s2
1254 else loop new_base new_removed in
1255 loop initial_base initial_removed *)
1257 let satAW dir
((grp
,_
,states
) as m
) s1 s2 reqst
=
1263 This works extremely badly when the region is small and the end of the
1264 region is very ambiguous, eg free(x) ... x
1268 let get_states l = setify(List.map (function (s,_,_) -> s) l) in
1269 let ostates = Common.union_set (get_states s1) (get_states s2) in
1272 A.FORWARD -> G.successors grp
1273 | A.BACKWARD -> G.predecessors grp) in
1275 List.fold_left Common.union_set ostates (List.map succ ostates) in
1276 let negphi = triples_complement states s1 in
1277 let negpsi = triples_complement states s2 in
1278 triples_complement ostates
1279 (satEU dir m negpsi (triples_conj negphi negpsi) (Some ostates))
1282 (*let ctr = ref 0 in*)
1286 Printf.printf "iter %d y %d\n" !ctr (List.length y);
1289 let pre = pre_forall dir m y y reqst
in
1290 (*print_state "pre" pre;*)
1291 let conj = triples_conj s1 pre in (* or triples_conj_AW *)
1292 triples_union s2 conj in
1293 let drop_wits = List.map (function (s
,e
,_
) -> (s
,e
,[])) in
1294 (* drop wits on s1 represents that we don't want any witnesses from
1295 the case that infinitely loops, only from the case that gets
1296 out of the loop. s1 is like a guard. To see the problem, consider
1297 an example where both s1 and s2 match some code after the loop.
1298 we only want the witness from s2. *)
1299 setgfix f (triples_union (nub(drop_wits s1)) s2)
1302 let satAF dir m s reqst
=
1306 let rec f y newinfo
=
1311 let first = pre_forall dir m
new_info y reqst
in
1312 let res = triples_union first y
in
1313 let new_info = setdiff res y
in
1319 let pre = pre_forall dir m y y reqst
in
1320 triples_union s
pre in
1323 let satAG dir
((_
,_
,states) as m
) s reqst
=
1327 let pre = pre_forall dir m y y reqst
in
1328 triples_conj y
pre in
1331 let satEG dir
((_
,_
,states) as m
) s reqst
=
1335 let pre = pre_exist dir m y reqst
in
1336 triples_conj y
pre in
1339 (* **************************************************************** *)
1340 (* Inner And - a way of dealing with multiple matches within a node *)
1341 (* **************************************************************** *)
1342 (* applied to the result of matching a node. collect witnesses when the
1343 states and environments are the same *)
1344 (* not a good idea, poses problem for unparsing, because don't realize that
1345 adjacent things come from different matches, leading to loss of newlines etc.
1346 exple struct I { ... - int x; + int y; ...} *)
1348 let inner_and trips = trips (*
1349 let rec loop = function
1351 | (s,th,w)::trips ->
1352 let (cur,acc) = loop trips in
1354 (s',_,_)::_ when s = s' ->
1355 let rec loop' = function
1357 | ((_,th',w') as t')::ts' ->
1358 (match conj_subst th th' with
1359 Some th'' -> (s,th'',union_wit w w')::ts'
1360 | None -> t'::(loop' ts')) in
1362 | _ -> ([(s,th,w)],cur@acc)) in
1364 loop (List.sort state_compare trips) (* is this sort needed? *) in
1367 (* *************** *)
1368 (* Partial matches *)
1369 (* *************** *)
1371 let filter_conj states unwanted partial_matches
=
1373 triples_conj (triples_complement states (unwitify unwanted
))
1375 triples_conj (unwitify x) (triples_complement states x)
1377 let strict_triples_conj strict
states trips trips'
=
1378 let res = triples_conj trips trips'
in
1379 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1381 let fail_left = filter_conj states trips trips'
in
1382 let fail_right = filter_conj states trips'
trips in
1383 let ors = triples_union fail_left fail_right in
1384 triples_union res ors
1387 let strict_triples_conj_none strict
states trips trips'
=
1388 let res = triples_conj_none trips trips'
in
1389 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1391 let fail_left = filter_conj states trips trips'
in
1392 let fail_right = filter_conj states trips'
trips in
1393 let ors = triples_union fail_left fail_right in
1394 triples_union res ors
1397 let left_strict_triples_conj strict
states trips trips'
=
1398 let res = triples_conj trips trips'
in
1399 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1401 let fail_left = filter_conj states trips trips'
in
1402 triples_union res fail_left
1405 let strict_A1 strict op failop dir
((_
,_
,states) as m
) trips required_states
=
1406 let res = op dir m
trips required_states
in
1407 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1409 let states = mkstates states required_states
in
1410 let fail = filter_conj states res (failop dir m
trips required_states
) in
1411 triples_union res fail
1414 let strict_A2 strict op failop dir
((_
,_
,states) as m
) trips trips'
1416 let res = op dir m
trips trips' required_states
in
1417 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1419 let states = mkstates states required_states
in
1420 let fail = filter_conj states res (failop dir m
trips' required_states
) in
1421 triples_union res fail
1424 let strict_A2au strict op failop dir
((_
,_
,states) as m
) trips trips'
1425 required_states
print_graph =
1426 match op dir m
trips trips' required_states
print_graph with
1428 if !Flag_ctl.partial_match
&& strict
= A.STRICT
1430 let states = mkstates states required_states
in
1432 filter_conj states res (failop dir m
trips' required_states
) in
1433 AUok
(triples_union res fail)
1435 | AUfailed
res -> AUfailed
res
1437 (* ********************* *)
1438 (* Environment functions *)
1439 (* ********************* *)
1441 let drop_wits required_states s phi
=
1442 match required_states
with
1444 | Some
states -> List.filter (function (s
,_
,_
) -> List.mem s
states) s
1447 let print_required required
=
1450 Format.print_string
"{";
1453 print_generic_substitution reqd
; Format.print_newline
())
1455 Format.print_string
"}";
1456 Format.print_newline
())
1461 let extend_required trips required
=
1462 if !Flag_ctl.partial_match
1465 if !pREQUIRED_ENV_OPT
1471 function (_
,t,_
) -> if List.mem
t rest
then rest
else t::rest
)
1473 let envs = if List.mem
[] envs then [] else envs in
1474 match (envs,required
) with
1478 let hdln = List.length hd
+ 5 (* let it grow a little bit *) in
1483 else if ln
+ 1 > hdln then raise Too_long
else (ln
+1,x::y
) in
1490 match conj_subst t r
with
1491 None
-> rest
| Some th
-> add th rest
)
1495 with Too_long
-> envs :: required
)
1496 | (envs,_
) -> envs :: required
1499 let drop_required v required
=
1500 if !pREQUIRED_ENV_OPT
1507 (List.map (List.filter (function sub
-> not
(dom_sub sub
= v
))) l
))
1509 (* check whether an entry has become useless *)
1510 List.filter (function l
-> not
(List.exists
(function x -> x = []) l
)) res
1513 (* no idea how to write this function ... *)
1515 (Hashtbl.create
(50) : (P.t, (G.node
* substitution
) list
) Hashtbl.t)
1517 let satLabel label required p
=
1519 if !pSATLABEL_MEMO_OPT
1522 let states_subs = Hashtbl.find
memo_label p
in
1523 List.map (function (st
,th
) -> (st
,th
,[])) states_subs
1526 let triples = setify(label p
) in
1527 Hashtbl.add memo_label p
1528 (List.map (function (st
,th
,_
) -> (st
,th
)) triples);
1530 else setify(label p
) in
1531 (* normalize first; conj_subst relies on sorting *)
1532 let ntriples = normalize triples in
1533 if !pREQUIRED_ENV_OPT
1537 function ((s
,th
,_
) as t) ->
1539 (List.exists
(function th'
-> not
(conj_subst th th'
= None
)))
1546 let get_required_states l
=
1547 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1549 Some
(inner_setify (List.map (function (s
,_
,_
) -> s
) l
))
1552 let get_children_required_states dir
(grp
,_
,_
) required_states
=
1553 if !pREQUIRED_STATES_OPT && not
!Flag_ctl.partial_match
1555 match required_states
with
1560 A.FORWARD
-> G.successors
1561 | A.BACKWARD
-> G.predecessors in
1562 Some
(inner_setify (List.concat (List.map (fn grp
) states)))
1565 let reachable_table =
1566 (Hashtbl.create
(50) : (G.node
* A.direction
, G.node list
) Hashtbl.t)
1568 (* like satEF, but specialized for get_reachable *)
1569 let reachsatEF dir
(grp
,_
,_
) s2 =
1571 match dir
with A.FORWARD
-> G.successors
| A.BACKWARD
-> G.predecessors in
1572 let union = unionBy compare
(=) in
1573 let rec f y
= function
1576 let (pre_collected
,new_info) =
1577 List.partition (function Common.Left
x -> true | _
-> false)
1580 try Common.Left
(Hashtbl.find
reachable_table (x,dir
))
1581 with Not_found
-> Common.Right
x)
1586 function Common.Left
x -> union x rest
1587 | _
-> failwith
"not possible")
1591 (function Common.Right
x -> x | _
-> failwith
"not possible")
1593 let first = inner_setify (concatmap (dirop grp
) new_info) in
1594 let new_info = setdiff first y in
1595 let res = new_info @ y in
1597 List.rev
(f s2 s2) (* put root first *)
1599 let get_reachable dir m required_states
=
1600 match required_states
with
1607 if List.mem cur rest
1611 (try Hashtbl.find
reachable_table (cur
,dir
)
1614 let states = reachsatEF dir m
[cur
] in
1615 Hashtbl.add reachable_table (cur
,dir
) states;
1624 Printf.sprintf
"_c%d" c
1626 (* **************************** *)
1627 (* End of environment functions *)
1628 (* **************************** *)
1630 type ('code
,'
value) cell
= Frozen
of 'code
| Thawed
of '
value
1632 let rec satloop unchecked required required_states
1633 ((grp
,label,states) as m
) phi env
=
1634 let rec loop unchecked required required_states phi
=
1638 | A.True
-> triples_top states
1639 | A.Pred
(p
) -> satLabel label required p
1640 | A.Uncheck
(phi1
) ->
1641 let unchecked = if !pUNCHECK_OPT then true else false in
1642 loop unchecked required required_states phi1
1644 let phires = loop unchecked required required_states phi
in
1646 List.map (function (s,th,w) -> (s,th,[])) phires in*)
1647 triples_complement (mkstates states required_states
)
1649 | A.Or
(phi1
,phi2
) ->
1651 (loop unchecked required required_states phi1
)
1652 (loop unchecked required required_states phi2
)
1653 | A.SeqOr
(phi1
,phi2
) ->
1654 let res1 = loop unchecked required required_states phi1
in
1655 let res2 = loop unchecked required required_states phi2
in
1656 let res1neg = unwitify res1 in
1657 let pm = !Flag_ctl.partial_match
in
1658 (match (pm,res1,res2) with
1659 (false,res1,[]) -> res1
1660 | (false,[],res2) -> res2
1664 (triples_complement (mkstates states required_states
) res1neg)
1666 | A.And
(strict
,phi1
,phi2
) ->
1667 (* phi1 is considered to be more likely to be [], because of the
1668 definition of asttoctl. Could use heuristics such as the size of
1670 let pm = !Flag_ctl.partial_match
in
1671 (match (pm,loop unchecked required required_states phi1
) with
1672 (false,[]) when !pLazyOpt -> []
1674 let new_required = extend_required phi1res required
in
1675 let new_required_states = get_required_states phi1res
in
1676 (match (pm,loop unchecked new_required new_required_states phi2
)
1678 (false,[]) when !pLazyOpt -> []
1680 strict_triples_conj strict
1681 (mkstates states required_states
)
1683 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1684 (* phi2 can appear anywhere that is reachable *)
1685 let pm = !Flag_ctl.partial_match
in
1686 (match (pm,loop unchecked required required_states phi1
) with
1689 let new_required = extend_required phi1res required
in
1690 let new_required_states = get_required_states phi1res
in
1691 let new_required_states =
1692 get_reachable dir m
new_required_states in
1693 (match (pm,loop unchecked new_required new_required_states phi2
)
1695 (false,[]) -> phi1res
1698 [] -> (* !Flag_ctl.partial_match must be true *)
1702 let s = mkstates states required_states
in
1704 (function a
-> function b
->
1705 strict_triples_conj strict
s a
[b
])
1706 [List.hd phi2res
] (List.tl phi2res
)
1709 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) phi2res in
1710 let s = mkstates states required_states
in
1712 (function a
-> function b
->
1713 strict_triples_conj strict
s a b
)
1717 "only one result allowed for the left arg of AndAny")))
1718 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1719 (* phi2 can appear anywhere that is reachable *)
1720 let pm = !Flag_ctl.partial_match
in
1721 (match (pm,loop unchecked required required_states phi1
) with
1724 let new_required = extend_required phi1res required
in
1725 let new_required_states = get_required_states phi1res
in
1726 let new_required_states =
1727 get_reachable dir m
new_required_states in
1728 (match (pm,loop unchecked new_required new_required_states phi2
)
1730 (false,[]) -> phi1res
1732 (* if there is more than one state, something about the
1733 environment has to ensure that the right triples of
1734 phi2 get associated with the triples of phi1.
1735 the asttoctl2 has to ensure that that is the case.
1736 these should thus be structural properties.
1737 env of phi2 has to be a proper subset of env of phi1
1738 to ensure all end up being consistent. no new triples
1739 should be generated. strict_triples_conj_none takes
1742 let s = mkstates states required_states
in
1745 function (st
,th
,_
) as phi2_elem
->
1747 triples_complement [st
] [(st
,th
,[])] in
1748 strict_triples_conj_none strict
s acc
1749 (phi2_elem
::inverse))
1751 | A.InnerAnd
(phi
) ->
1752 inner_and(loop unchecked required required_states phi
)
1754 let new_required_states =
1755 get_children_required_states dir m required_states
in
1756 satEX dir m
(loop unchecked required
new_required_states phi
)
1758 | A.AX
(dir
,strict
,phi
) ->
1759 let new_required_states =
1760 get_children_required_states dir m required_states
in
1761 let res = loop unchecked required
new_required_states phi
in
1762 strict_A1 strict
satAX satEX dir m
res required_states
1764 let new_required_states = get_reachable dir m required_states
in
1765 satEF dir m
(loop unchecked required
new_required_states phi
)
1767 | A.AF
(dir
,strict
,phi
) ->
1768 if !Flag_ctl.loop_in_src_code
1770 loop unchecked required required_states
1771 (A.AU
(dir
,strict
,A.True
,phi
))
1773 let new_required_states = get_reachable dir m required_states
in
1774 let res = loop unchecked required
new_required_states phi
in
1775 strict_A1 strict
satAF satEF dir m
res new_required_states
1777 let new_required_states = get_reachable dir m required_states
in
1778 satEG dir m
(loop unchecked required
new_required_states phi
)
1780 | A.AG
(dir
,strict
,phi
) ->
1781 let new_required_states = get_reachable dir m required_states
in
1782 let res = loop unchecked required
new_required_states phi
in
1783 strict_A1 strict
satAG satEF dir m
res new_required_states
1784 | A.EU
(dir
,phi1
,phi2
) ->
1785 let new_required_states = get_reachable dir m required_states
in
1786 (match loop unchecked required
new_required_states phi2
with
1787 [] when !pLazyOpt -> []
1789 let new_required = extend_required s2 required
in
1790 let s1 = loop unchecked new_required new_required_states phi1
in
1791 satEU dir m
s1 s2 new_required_states
1792 (fun y ctr -> print_graph_c grp
new_required_states y ctr phi
))
1793 | A.AW
(dir
,strict
,phi1
,phi2
) ->
1794 let new_required_states = get_reachable dir m required_states
in
1795 (match loop unchecked required
new_required_states phi2
with
1796 [] when !pLazyOpt -> []
1798 let new_required = extend_required s2 required
in
1799 let s1 = loop unchecked new_required new_required_states phi1
in
1800 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states)
1801 | A.AU
(dir
,strict
,phi1
,phi2
) ->
1802 (*Printf.printf "using AU\n"; flush stdout;*)
1803 let new_required_states = get_reachable dir m required_states
in
1804 (match loop unchecked required
new_required_states phi2
with
1805 [] when !pLazyOpt -> []
1807 let new_required = extend_required s2 required
in
1808 let s1 = loop unchecked new_required new_required_states phi1
in
1810 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
1812 print_graph_c grp
new_required_states y ctr phi
) in
1815 | AUfailed tmp_res
->
1816 (* found a loop, have to try AW *)
1818 A[E[phi1 U phi2] & phi1 W phi2]
1819 the and is nonstrict *)
1820 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
1821 (*Printf.printf "using AW\n"; flush stdout;*)
1824 (satEU dir m
s1 tmp_res
new_required_states
1825 (* no graph, for the moment *)
1828 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states
1830 | A.Implies
(phi1
,phi2
) ->
1831 loop unchecked required required_states
(A.Or
(A.Not phi1
,phi2
))
1832 | A.Exists
(keep
,v
,phi
) ->
1833 let new_required = drop_required v required
in
1834 triples_witness v
unchecked (not keep
)
1835 (loop unchecked new_required required_states phi
)
1837 | A.Let
(v
,phi1
,phi2
) ->
1838 (* should only be used when the properties unchecked, required,
1839 and required_states are known to be the same or at least
1840 compatible between all the uses. this is not checked. *)
1841 let res = loop unchecked required required_states phi1
in
1842 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1843 | A.LetR
(dir
,v
,phi1
,phi2
) ->
1844 (* should only be used when the properties unchecked, required,
1845 and required_states are known to be the same or at least
1846 compatible between all the uses. this is not checked. *)
1847 (* doesn't seem to be used any more *)
1848 let new_required_states = get_reachable dir m required_states
in
1849 let res = loop unchecked required
new_required_states phi1
in
1850 satloop unchecked required required_states m phi2
((v
,res) :: env
)
1852 let res = List.assoc v env
in
1854 then List.map (function (s,th
,_
) -> (s,th
,[])) res
1856 | A.XX
(phi
) -> failwith
"should have been removed" in
1857 if !Flag_ctl.bench
> 0 then triples := !triples + (List.length
res);
1858 let res = drop_wits required_states
res phi
(* ) *) in
1859 print_graph grp required_states
res "" phi
;
1862 loop unchecked required required_states phi
1866 (* SAT with tracking *)
1868 Printf.printf
"%s\n" str
1870 let rec sat_verbose_loop unchecked required required_states annot maxlvl lvl
1871 ((_
,label,states) as m
) phi env
=
1872 let anno res children
= (annot lvl phi
res children
,res) in
1873 let satv unchecked required required_states phi0 env
=
1874 sat_verbose_loop unchecked required required_states annot maxlvl
(lvl
+1)
1876 if (lvl
> maxlvl
) && (maxlvl
> -1) then
1877 anno (satloop unchecked required required_states m phi env
) []
1881 A.False
-> anno [] []
1882 | A.True
-> anno (triples_top states) []
1885 anno (satLabel label required p
) []
1886 | A.Uncheck
(phi1
) ->
1887 let unchecked = if !pUNCHECK_OPT then true else false in
1888 let (child1
,res1) = satv unchecked required required_states phi1 env
in
1893 satv unchecked required required_states phi1 env
in
1895 anno (triples_complement (mkstates states required_states
) res) [child
]
1896 | A.Or
(phi1
,phi2
) ->
1898 satv unchecked required required_states phi1 env
in
1900 satv unchecked required required_states phi2 env
in
1902 anno (triples_union res1 res2) [child1
; child2
]
1903 | A.SeqOr
(phi1
,phi2
) ->
1905 satv unchecked required required_states phi1 env
in
1907 satv unchecked required required_states phi2 env
in
1909 List.map (function (s,th
,_
) -> (s,th
,[])) res1 in
1911 let pm = !Flag_ctl.partial_match
in
1912 (match (pm,res1,res2) with
1913 (false,res1,[]) -> anno res1 [child1
; child2
]
1914 | (false,[],res2) -> anno res2 [child1
; child2
]
1916 anno (triples_union res1
1918 (triples_complement (mkstates states required_states
)
1922 | A.And
(strict
,phi1
,phi2
) ->
1923 let pm = !Flag_ctl.partial_match
in
1924 (match (pm,satv unchecked required required_states phi1 env
) with
1925 (false,(child1
,[])) ->
1926 output "and"; anno [] [child1
]
1927 | (_
,(child1
,res1)) ->
1928 let new_required = extend_required res1 required
in
1929 let new_required_states = get_required_states res1 in
1930 (match (pm,satv unchecked new_required new_required_states phi2
1932 (false,(child2
,[])) ->
1933 output "and"; anno [] [child1
;child2
]
1934 | (_
,(child2
,res2)) ->
1937 strict_triples_conj strict
1938 (mkstates states required_states
)
1940 anno res [child1
; child2
]))
1941 | A.AndAny
(dir
,strict
,phi1
,phi2
) ->
1942 let pm = !Flag_ctl.partial_match
in
1943 (match (pm,satv unchecked required required_states phi1 env
) with
1944 (false,(child1
,[])) ->
1945 output "and"; anno [] [child1
]
1946 | (_
,(child1
,res1)) ->
1947 let new_required = extend_required res1 required
in
1948 let new_required_states = get_required_states res1 in
1949 let new_required_states =
1950 get_reachable dir m
new_required_states in
1951 (match (pm,satv unchecked new_required new_required_states phi2
1953 (false,(child2
,[])) ->
1955 anno res1 [child1
;child2
]
1956 | (_
,(child2
,res2)) ->
1958 [] -> (* !Flag_ctl.partial_match must be true *)
1960 then anno [] [child1
; child2
]
1963 let s = mkstates states required_states
in
1965 (function a
-> function b
->
1966 strict_triples_conj strict
s a
[b
])
1967 [List.hd
res2] (List.tl
res2) in
1968 anno res [child1
; child2
]
1971 List.map (function (s,e
,w
) -> [(state
,e
,w
)]) res2 in
1974 let s = mkstates states required_states
in
1976 (function a
-> function b
->
1977 strict_triples_conj strict
s a b
)
1979 anno res [child1
; child2
]
1982 "only one result allowed for the left arg of AndAny")))
1983 | A.HackForStmt
(dir
,strict
,phi1
,phi2
) ->
1984 let pm = !Flag_ctl.partial_match
in
1985 (match (pm,satv unchecked required required_states phi1 env
) with
1986 (false,(child1
,[])) ->
1987 output "and"; anno [] [child1
]
1988 | (_
,(child1
,res1)) ->
1989 let new_required = extend_required res1 required
in
1990 let new_required_states = get_required_states res1 in
1991 let new_required_states =
1992 get_reachable dir m
new_required_states in
1993 (match (pm,satv unchecked new_required new_required_states phi2
1995 (false,(child2
,[])) ->
1997 anno res1 [child1
;child2
]
1998 | (_
,(child2
,res2)) ->
2000 let s = mkstates states required_states
in
2003 function (st
,th
,_
) as phi2_elem
->
2005 triples_complement [st
] [(st
,th
,[])] in
2006 strict_triples_conj_none strict
s acc
2007 (phi2_elem
::inverse))
2009 anno res [child1
; child2
]))
2010 | A.InnerAnd
(phi1
) ->
2011 let (child1
,res1) = satv unchecked required required_states phi1 env
in
2013 anno (inner_and res1) [child1
]
2015 let new_required_states =
2016 get_children_required_states dir m required_states
in
2018 satv unchecked required
new_required_states phi1 env
in
2020 anno (satEX dir m
res required_states
) [child
]
2021 | A.AX
(dir
,strict
,phi1
) ->
2022 let new_required_states =
2023 get_children_required_states dir m required_states
in
2025 satv unchecked required
new_required_states phi1 env
in
2027 let res = strict_A1 strict
satAX satEX dir m
res required_states
in
2030 let new_required_states = get_reachable dir m required_states
in
2032 satv unchecked required
new_required_states phi1 env
in
2034 anno (satEF dir m
res new_required_states) [child
]
2035 | A.AF
(dir
,strict
,phi1
) ->
2036 if !Flag_ctl.loop_in_src_code
2038 satv unchecked required required_states
2039 (A.AU
(dir
,strict
,A.True
,phi1
))
2042 (let new_required_states = get_reachable dir m required_states
in
2044 satv unchecked required
new_required_states phi1 env
in
2047 strict_A1 strict
satAF satEF dir m
res new_required_states in
2050 let new_required_states = get_reachable dir m required_states
in
2052 satv unchecked required
new_required_states phi1 env
in
2054 anno (satEG dir m
res new_required_states) [child
]
2055 | A.AG
(dir
,strict
,phi1
) ->
2056 let new_required_states = get_reachable dir m required_states
in
2058 satv unchecked required
new_required_states phi1 env
in
2060 let res = strict_A1 strict
satAG satEF dir m
res new_required_states in
2063 | A.EU
(dir
,phi1
,phi2
) ->
2064 let new_required_states = get_reachable dir m required_states
in
2065 (match satv unchecked required
new_required_states phi2 env
with
2070 let new_required = extend_required res2 required
in
2072 satv unchecked new_required new_required_states phi1 env
in
2074 anno (satEU dir m
res1 res2 new_required_states (fun y str -> ()))
2076 | A.AW
(dir
,strict
,phi1
,phi2
) ->
2077 failwith
"should not be used" (*
2078 let new_required_states = get_reachable dir m required_states in
2079 (match satv unchecked required new_required_states phi2 env with
2081 output (Printf.sprintf "AW %b" unchecked); anno [] [child2]
2083 let new_required = extend_required res2 required in
2085 satv unchecked new_required new_required_states phi1 env in
2086 output (Printf.sprintf "AW %b" unchecked);
2088 strict_A2 strict satAW satEF dir m res1 res2
2089 new_required_states in
2090 anno res [child1; child2]) *)
2091 | A.AU
(dir
,strict
,phi1
,phi2
) ->
2092 let new_required_states = get_reachable dir m required_states
in
2093 (match satv unchecked required
new_required_states phi2 env
with
2095 output "AU"; anno [] [child2
]
2097 let new_required = extend_required s2 required
in
2099 satv unchecked new_required new_required_states phi1 env
in
2102 strict_A2au strict
satAU satEF dir m
s1 s2 new_required_states
2103 (fun y str -> ()) in
2106 anno res [child1
; child2
]
2107 | AUfailed tmp_res
->
2108 (* found a loop, have to try AW *)
2110 A[E[phi1 U phi2] & phi1 W phi2]
2111 the and is nonstrict *)
2112 (* tmp_res is bigger than s2, so perhaps closer to s1 *)
2116 (satEU dir m
s1 tmp_res
new_required_states
2117 (* no graph, for the moment *)
2121 strict_A2 strict
satAW satEF dir m
s1 s2 new_required_states in
2122 anno res [child1
; child2
]))
2123 | A.Implies
(phi1
,phi2
) ->
2124 satv unchecked required required_states
2125 (A.Or
(A.Not phi1
,phi2
))
2127 | A.Exists
(keep
,v
,phi1
) ->
2128 let new_required = drop_required v required
in
2130 satv unchecked new_required required_states phi1 env
in
2132 anno (triples_witness v
unchecked (not keep
) res) [child
]
2133 | A.Let
(v
,phi1
,phi2
) ->
2135 satv unchecked required required_states phi1 env
in
2137 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2138 anno res2 [child1
;child2
]
2139 | A.LetR
(dir
,v
,phi1
,phi2
) ->
2140 let new_required_states = get_reachable dir m required_states
in
2142 satv unchecked required
new_required_states phi1 env
in
2144 satv unchecked required required_states phi2
((v
,res1) :: env
) in
2145 anno res2 [child1
;child2
]
2148 let res = List.assoc v env
in
2151 then List.map (function (s,th
,_
) -> (s,th
,[])) res
2154 | A.XX
(phi
) -> failwith
"should have been removed" in
2155 let res1 = drop_wits required_states
res phi
in
2159 print_required_states required_states
;
2160 print_state "after drop_wits" res1 end;
2165 let sat_verbose annotate maxlvl lvl m phi
=
2166 sat_verbose_loop false [] None annotate maxlvl lvl m phi
[]
2168 (* Type for annotations collected in a tree *)
2169 type ('a
) witAnnoTree
= WitAnno
of ('a
* ('a witAnnoTree
) list
);;
2171 let sat_annotree annotate m phi
=
2172 let tree_anno l phi
res chld
= WitAnno
(annotate l phi
res,chld
) in
2173 sat_verbose_loop false [] None
tree_anno (-1) 0 m phi
[]
2177 let sat m phi = satloop m phi []
2181 let simpleanno l phi
res =
2183 Format.print_string
("\n" ^
s ^
"\n------------------------------\n");
2184 print_generic_algo
(List.sort compare
res);
2185 Format.print_string
"\n------------------------------\n\n" in
2186 let pp_dir = function
2188 | A.BACKWARD
-> pp "^" in
2190 | A.False
-> pp "False"
2191 | A.True
-> pp "True"
2192 | A.Pred
(p
) -> pp ("Pred" ^
(Dumper.dump p
))
2193 | A.Not
(phi
) -> pp "Not"
2194 | A.Exists
(_
,v
,phi
) -> pp ("Exists " ^
(Dumper.dump
(v
)))
2195 | A.And
(_
,phi1
,phi2
) -> pp "And"
2196 | A.AndAny
(dir
,_
,phi1
,phi2
) -> pp "AndAny"
2197 | A.HackForStmt
(dir
,_
,phi1
,phi2
) -> pp "HackForStmt"
2198 | A.Or
(phi1
,phi2
) -> pp "Or"
2199 | A.SeqOr
(phi1
,phi2
) -> pp "SeqOr"
2200 | A.Implies
(phi1
,phi2
) -> pp "Implies"
2201 | A.AF
(dir
,_
,phi1
) -> pp "AF"; pp_dir dir
2202 | A.AX
(dir
,_
,phi1
) -> pp "AX"; pp_dir dir
2203 | A.AG
(dir
,_
,phi1
) -> pp "AG"; pp_dir dir
2204 | A.AW
(dir
,_
,phi1
,phi2
)-> pp "AW"; pp_dir dir
2205 | A.AU
(dir
,_
,phi1
,phi2
)-> pp "AU"; pp_dir dir
2206 | A.EF
(dir
,phi1
) -> pp "EF"; pp_dir dir
2207 | A.EX
(dir
,phi1
) -> pp "EX"; pp_dir dir
2208 | A.EG
(dir
,phi1
) -> pp "EG"; pp_dir dir
2209 | A.EU
(dir
,phi1
,phi2
) -> pp "EU"; pp_dir dir
2210 | A.Let
(x,phi1
,phi2
) -> pp ("Let"^
" "^
x)
2211 | A.LetR
(dir
,x,phi1
,phi2
) -> pp ("LetR"^
" "^
x); pp_dir dir
2212 | A.Ref
(s) -> pp ("Ref("^
s^
")")
2213 | A.Uncheck
(s) -> pp "Uncheck"
2214 | A.InnerAnd
(s) -> pp "InnerAnd"
2215 | A.XX
(phi1
) -> pp "XX"
2219 (* pad: Rene, you can now use the module pretty_print_ctl.ml to
2220 print a ctl formula more accurately if you want.
2221 Use the print_xxx provided in the different module to call
2222 Pretty_print_ctl.pp_ctl.
2225 let simpleanno2 l phi
res =
2227 Pretty_print_ctl.pp_ctl
(P.print_predicate
, SUB.print_mvar
) false phi
;
2228 Format.print_newline
();
2229 Format.print_string
"----------------------------------------------------";
2230 Format.print_newline
();
2231 print_generic_algo
(List.sort compare
res);
2232 Format.print_newline
();
2233 Format.print_string
"----------------------------------------------------";
2234 Format.print_newline
();
2235 Format.print_newline
();
2239 (* ---------------------------------------------------------------------- *)
2241 (* ---------------------------------------------------------------------- *)
2243 type optentry
= bool ref * string
2244 type options
= {label : optentry
; unch
: optentry
;
2245 conj : optentry
; compl1
: optentry
; compl2
: optentry
;
2247 reqenv
: optentry
; reqstates
: optentry
}
2250 {label = (pSATLABEL_MEMO_OPT,"satlabel_memo_opt");
2251 unch
= (pUNCHECK_OPT,"uncheck_opt");
2252 conj = (pTRIPLES_CONJ_OPT,"triples_conj_opt");
2253 compl1
= (pTRIPLES_COMPLEMENT_OPT,"triples_complement_opt");
2254 compl2
= (pTRIPLES_COMPLEMENT_SIMPLE_OPT,"triples_complement_simple_opt");
2255 newinfo
= (pNEW_INFO_OPT,"new_info_opt");
2256 reqenv
= (pREQUIRED_ENV_OPT,"required_env_opt");
2257 reqstates
= (pREQUIRED_STATES_OPT,"required_states_opt")}
2261 ("label ",[options.label]);
2262 ("unch ",[options.unch
]);
2263 ("unch and label ",[options.label;options.unch
])]
2266 [("conj ", [options.conj]);
2267 ("compl1 ", [options.compl1
]);
2268 ("compl12 ", [options.compl1
;options.compl2
]);
2269 ("conj/compl12 ", [options.conj;options.compl1
;options.compl2
]);
2270 ("conj unch satl ", [options.conj;options.unch
;options.label]);
2272 ("compl1 unch satl ", [options.compl1;options.unch;options.label]);
2273 ("compl12 unch satl ",
2274 [options.compl1;options.compl2;options.unch;options.label]); *)
2275 ("conj/compl12 unch satl ",
2276 [options.conj;options.compl1
;options.compl2
;options.unch
;options.label])]
2279 [("newinfo ", [options.newinfo
]);
2280 ("newinfo unch satl ", [options.newinfo
;options.unch
;options.label])]
2283 [("reqenv ", [options.reqenv
]);
2284 ("reqstates ", [options.reqstates
]);
2285 ("reqenv/states ", [options.reqenv
;options.reqstates
]);
2286 (* ("reqenv unch satl ", [options.reqenv;options.unch;options.label]);
2287 ("reqstates unch satl ",
2288 [options.reqstates;options.unch;options.label]);*)
2289 ("reqenv/states unch satl ",
2290 [options.reqenv
;options.reqstates
;options.unch
;options.label])]
2293 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2294 options.newinfo
;options.reqenv
;options.reqstates
]
2297 [("all ",all_options)]
2299 let all_options_but_path =
2300 [options.label;options.unch
;options.conj;options.compl1
;options.compl2
;
2301 options.reqenv
;options.reqstates
]
2303 let all_but_path = ("all but path ",all_options_but_path)
2306 [(satAW_calls, "satAW", ref 0);
2307 (satAU_calls, "satAU", ref 0);
2308 (satEF_calls, "satEF", ref 0);
2309 (satAF_calls, "satAF", ref 0);
2310 (satEG_calls, "satEG", ref 0);
2311 (satAG_calls, "satAG", ref 0);
2312 (satEU_calls, "satEU", ref 0)]
2316 (function (opt
,x) ->
2317 (opt
,x,ref 0.0,ref 0,
2318 List.map (function _
-> (ref 0, ref 0, ref 0)) counters))
2319 [List.hd
all;all_but_path]
2320 (*(all@baseline@conjneg@path@required)*)
2324 let rec iter fn = function
2326 | n
-> let _ = fn() in
2327 (Hashtbl.clear
reachable_table;
2328 Hashtbl.clear
memo_label;
2332 let copy_to_stderr fl
=
2333 let i = open_in fl
in
2335 Printf.fprintf stderr
"%s\n" (input_line
i);
2337 try loop() with _ -> ();
2340 let bench_sat (_,_,states) fn =
2341 List.iter (function (opt
,_) -> opt
:= false) all_options;
2344 (function (name
,options,time
,trips,counter_info
) ->
2345 let iterct = !Flag_ctl.bench
in
2346 if !time
> float_of_int
timeout then time
:= -100.0;
2347 if not
(!time
= -100.0)
2350 Hashtbl.clear
reachable_table;
2351 Hashtbl.clear
memo_label;
2352 List.iter (function (opt
,_) -> opt
:= true) options;
2353 List.iter (function (calls
,_,save_calls
) -> save_calls
:= !calls
)
2357 let bef = Sys.time
() in
2359 Common.timeout_function
timeout
2361 let bef = Sys.time
() in
2362 let res = iter fn iterct in
2363 let aft = Sys.time
() in
2364 time
:= !time
+. (aft -. bef);
2365 trips := !trips + !triples;
2367 (function (calls
,_,save_calls
) ->
2368 function (current_calls
,current_cfg
,current_max_cfg
) ->
2370 !current_calls
+ (!calls
- !save_calls
);
2371 if (!calls
- !save_calls
) > 0
2373 (let st = List.length
states in
2374 current_cfg
:= !current_cfg
+ st;
2375 if st > !current_max_cfg
2376 then current_max_cfg
:= st))
2377 counters counter_info
;
2382 let aft = Sys.time
() in
2384 Printf.fprintf stderr
"Timeout at %f on: %s\n"
2388 List.iter (function (opt
,_) -> opt
:= false) options;
2393 Printf.fprintf stderr
"\n";
2397 (if not
(List.for_all
(function x -> x = res) rest
)
2399 (List.iter (print_state "a state") answers;
2400 Printf.printf
"something doesn't work\n");
2404 let iterct = !Flag_ctl.bench
in
2408 (function (name
,options,time
,trips,counter_info
) ->
2409 Printf.fprintf stderr
"%s Numbers: %f %d "
2410 name
(!time
/. (float_of_int
iterct)) !trips;
2412 (function (calls
,cfg
,max_cfg
) ->
2413 Printf.fprintf stderr
"%d %d %d " (!calls
/ iterct) !cfg
!max_cfg
)
2415 Printf.fprintf stderr
"\n")
2418 (* ---------------------------------------------------------------------- *)
2419 (* preprocessing: ignore irrelevant functions *)
2421 let preprocess (cfg
,_,_) label = function
2422 [] -> true (* no information, try everything *)
2424 let sz = G.size cfg
in
2425 let verbose_output pred = function
2427 Printf.printf
"did not find:\n";
2428 P.print_predicate
pred; Format.print_newline
()
2430 Printf.printf
"found:\n";
2431 P.print_predicate
pred; Format.print_newline
();
2432 Printf.printf
"but it was not enough\n" in
2433 let get_any verbose
x =
2435 try Hashtbl.find
memo_label x
2438 (let triples = label x in
2440 List.map (function (st,th
,_) -> (st,th
)) triples in
2441 Hashtbl.add memo_label x filtered;
2443 if verbose
then verbose_output x res;
2446 (* don't bother testing when there are more patterns than nodes *)
2447 if List.length l
> sz-2
2449 else List.for_all
(get_any false) l
in
2450 if List.exists
get_all l
2453 (if !Flag_ctl.verbose_match
2455 List.iter (List.iter (function x -> let _ = get_any true x in ()))
2459 let filter_partial_matches trips =
2460 if !Flag_ctl.partial_match
2462 let anynegwit = (* if any is neg, then all are *)
2463 List.exists
(function A.NegWit
_ -> true | A.Wit
_ -> false) in
2465 List.partition (function (s,th
,wit
) -> anynegwit wit
) trips in
2468 | _ -> print_state "partial matches" bad
; Format.print_newline
());
2472 (* ---------------------------------------------------------------------- *)
2473 (* Main entry point for engine *)
2474 let sat m phi reqopt
=
2476 (match !Flag_ctl.steps
with
2477 None
-> step_count := 0
2478 | Some
x -> step_count := x);
2479 Hashtbl.clear
reachable_table;
2480 Hashtbl.clear
memo_label;
2481 let (x,label,states) = m
in
2482 if (!Flag_ctl.bench
> 0) or (preprocess m
label reqopt
)
2484 ((* to drop when Yoann initialized this flag *)
2485 if List.exists
(G.extract_is_loop
x) states
2486 then Flag_ctl.loop_in_src_code
:= true;
2487 let m = (x,label,List.sort compare
states) in
2489 if(!Flag_ctl.verbose_ctl_engine
)
2491 let fn _ = snd
(sat_annotree simpleanno2 m phi
) in
2492 if !Flag_ctl.bench
> 0
2496 let fn _ = satloop false [] None
m phi
[] in
2497 if !Flag_ctl.bench
> 0
2499 else Common.profile_code
"ctl" (fun _ -> fn()) in
2500 let res = filter_partial_matches res in
2502 Printf.printf "steps: start %d, stop %d\n"
2503 (match !Flag_ctl.steps with Some x -> x | _ -> 0)
2505 Printf.printf "triples: %d\n" !triples;
2506 print_state "final result" res;
2508 List.sort compare
res)
2510 (if !Flag_ctl.verbose_ctl_engine
2511 then Common.pr2
"missing something required";
2515 (* ********************************************************************** *)
2516 (* End of Module: CTL_ENGINE *)
2517 (* ********************************************************************** *)