1 (* ---------------------------------------------------------------- *)
2 (* code to check for ambiguities *)
4 (* Idea: for each node that is said to be modified in any witness tree, we
5 check that all backward paths end up at the root of some witness tree
6 that says that the node should be modified. We then give a warning, if
7 the node itself appears more than once in such a path, because then there
8 could be some instances that are modified and some that are not. An
11 f(); ... g(); ... - h();
13 with C code: f(); while(E) { h(); g(); } g(); h();
15 Then the h() in the while loop matches both the first ... and the - h();
17 Concretely, if a node 47 is in the witness tree rooted at 1 and the
18 witness tree rooted at 2, then we give an error if 47 is not in the set
19 of nodes satisfying AF[1v2] and give a warning if 47 is in the set of
20 nodes satisfying EXEF(47 & EXEF(1v2)). (Note that the root of a witness
21 tree here is the node causing the pattern to match; there might not be
22 any witnesses associated with this node.)
24 Another try on the exists formula:
25 !(1v2) & EXE[!(1v2) U 47]
26 The first !(1v2) is to discard immediately cases where the beginning and
27 end of the path are the same. Afterwards, it would only seem necessary to
28 serach up to the next occurrence of 47 (leaf), ensuring that there are not
29 1s or 2s (starting points) along the way. Then the second 47 would be in
30 the path, but possible not transformed.
33 module G
= Ograph_extended
36 (* Step 1: for each tree, make a mapping from the modified nodes to the root
39 let modified = (Hashtbl.create
(25) : (G.nodei
, G.nodei list
ref) Hashtbl.t
)
41 let build_modified (n
,_
,wits
) =
42 let rec loop = function
43 CTL.Wit
(st
,[CTL.Subst
(x
,Wrapper_ctl.PredVal
(CTL.Modif
(v
)))],anno
,wit
) ->
45 try Hashtbl.find
modified st
47 let cell = ref [] in Hashtbl.add
modified st
cell; cell in
50 | CTL.Wit
(st
,_
,anno
,wit
) -> List.iter
loop wit
51 | CTL.NegWit
(wit
) -> () in
54 (* Step 2: For each node in the hash table, create the error and warning
57 type 'a nodes
= Node
of 'a
| After
59 let create_formulas _
=
67 (Ast_ctl.BACKWARD,wrap(Ast_ctl.EF(Ast_ctl.BACKWARD,f)))) in*)
68 let match_node = Ast_ctl.Pred
(Node
(node
)) in
70 List.map
(function n
-> Ast_ctl.Pred
(Node
(n
)))
71 (List.sort compare
!roots
) in
74 (function prev
-> function cur
-> Ast_ctl.Or
(prev
,cur
))
75 (List.hd
match_roots) (List.tl
match_roots) in
76 (* no point to search if no path, and the presence of after
77 in the AF formula can make things slow *)
78 if List.mem node
!roots
82 Ast_ctl.AF
(Ast_ctl.BACKWARD
,Ast_ctl.NONSTRICT
,
83 Ast_ctl.Or
(or_roots,Ast_ctl.Pred
(After
))),
86 Ast_ctl.Not
(or_roots),
89 Ast_ctl.EU
(Ast_ctl.BACKWARD
,or_roots,match_node))))
91 (wrap(Ast_ctl.And(Ast_ctl.NONSTRICT,match_node,exef(roots))))*)
95 (* Step 3: check the formula on the control-flow graph *)
99 type t
= Ograph_extended.nodei nodes
100 let print_predicate = function
101 After
-> Format.print_string
"after"
102 | Node x
-> Format.print_string
(string_of_int x
)
109 let eq_mvar x x'
= failwith
"should not be invoked"
110 let eq_val v v'
= failwith
"should not be invoked"
111 let merge_val v v'
= failwith
"should not be invoked"
113 let print_mvar s
= failwith
"should not be invoked"
114 let print_value x
= failwith
"should not be invoked"
120 type node
= Ograph_extended.nodei
122 (Control_flow_c.node
, Control_flow_c.edge
)
123 Ograph_extended.ograph_mutable
124 let predecessors cfg n
= List.map fst
((cfg#
predecessors n
)#tolist
)
125 let successors cfg n
= List.map fst
((cfg#
successors n
)#tolist
)
126 let extract_is_loop cfg n
=
127 Control_flow_c.extract_is_loop (cfg#nodes#find n
)
128 let print_node i
= Format.print_string
(string_of_int i
)
129 let size cfg
= cfg#nodes#length
130 let print_graph cfg label border_nodes fill_nodes filename
= ()
133 module ENGINE
= Ctl_engine.CTL_ENGINE
(ENV
) (CFG
) (PRED
)
135 let test_formula state formula cfg
=
137 Node pred
-> [(pred
,[],[])]
141 (fun (nodei
, node
) ->
142 match Control_flow_c.unwrap node
with
143 Control_flow_c.AfterNode
-> [(nodei
,[],[])]
146 let verbose = !Flag_ctl.verbose_ctl_engine
in
147 let pm = !Flag_ctl.partial_match
in
148 (* let gt = !Flag_ctl.graphical_trace in *)
149 Flag_ctl.verbose_ctl_engine
:= false;
150 Flag_ctl.partial_match
:= false;
151 Flag_ctl.checking_reachability
:= true;
152 (* Flag_ctl.graphical_trace := ""; *)
154 ENGINE.sat
(cfg
,label,List.map fst cfg#nodes#tolist
)
155 (CTL.And
(CTL.NONSTRICT
,CTL.Pred
(Node
(state
)),formula
))
157 Flag_ctl.verbose_ctl_engine
:= verbose;
158 Flag_ctl.partial_match
:= pm;
159 Flag_ctl.checking_reachability
:= false;
160 (* Flag_ctl.graphical_trace := gt; *)
161 match res with [] -> false | _
-> true
163 (* ---------------------------------------------------------------- *)
166 (* The argument is a list of triples with a node name, an empty environment
167 and a witness tree *)
170 (Ograph_extended.nodei
, unit,
171 (Ograph_extended.nodei
, unit, unit) Ast_ctl.generic_ctl list
)
172 Ast_ctl.generic_witnesstree
174 type ('a
,'b
,'c
,'d
,'e
) triples
=
175 (Ograph_extended.nodei
* 'a
*
176 (Ograph_extended.nodei
,
177 ('b
, ('c
, 'd
) Wrapper_ctl.wrapped_binding
) CTL.generic_subst list
, 'e
)
178 CTL.generic_witnesstree list
) list
180 let check_reachability triples cfg
=
181 Hashtbl.clear
modified;
182 List.iter
build_modified triples
;
183 let formulas = create_formulas() in
185 (function (node
,af_formula
,ef_formula
) ->
186 if test_formula node af_formula cfg
188 if test_formula node ef_formula cfg
190 Printf.printf
"warning: node %d may be inconsistently modified\n"
196 "node %d reachable by inconsistent control-flow paths" node
))