Commit | Line | Data |
---|---|---|
9bc82bae C |
1 | (* |
2 | * Copyright 2010, INRIA, University of Copenhagen | |
3 | * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix | |
4 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
5 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
6 | * This file is part of Coccinelle. | |
7 | * | |
8 | * Coccinelle is free software: you can redistribute it and/or modify | |
9 | * it under the terms of the GNU General Public License as published by | |
10 | * the Free Software Foundation, according to version 2 of the License. | |
11 | * | |
12 | * Coccinelle is distributed in the hope that it will be useful, | |
13 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
15 | * GNU General Public License for more details. | |
16 | * | |
17 | * You should have received a copy of the GNU General Public License | |
18 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
19 | * | |
20 | * The authors reserve the right to distribute this or future versions of | |
21 | * Coccinelle under other licenses. | |
22 | *) | |
23 | ||
24 | ||
c491d8ee C |
25 | (* |
26 | * Copyright 2010, INRIA, University of Copenhagen | |
27 | * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix | |
28 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
29 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
30 | * This file is part of Coccinelle. | |
31 | * | |
32 | * Coccinelle is free software: you can redistribute it and/or modify | |
33 | * it under the terms of the GNU General Public License as published by | |
34 | * the Free Software Foundation, according to version 2 of the License. | |
35 | * | |
36 | * Coccinelle is distributed in the hope that it will be useful, | |
37 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
38 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
39 | * GNU General Public License for more details. | |
40 | * | |
41 | * You should have received a copy of the GNU General Public License | |
42 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
43 | * | |
44 | * The authors reserve the right to distribute this or future versions of | |
45 | * Coccinelle under other licenses. | |
46 | *) | |
47 | ||
48 | ||
34e49164 C |
49 | (* ---------------------------------------------------------------- *) |
50 | (* code to check for ambiguities *) | |
51 | ||
52 | (* Idea: for each node that is said to be modified in any witness tree, we | |
53 | check that all backward paths end up at the root of some witness tree | |
54 | that says that the node should be modified. We then give a warning, if | |
55 | the node itself appears more than once in such a path, because then there | |
56 | could be some instances that are modified and some that are not. An | |
57 | example is as follows: | |
58 | ||
59 | f(); ... g(); ... - h(); | |
60 | ||
61 | with C code: f(); while(E) { h(); g(); } g(); h(); | |
62 | ||
63 | Then the h() in the while loop matches both the first ... and the - h(); | |
64 | ||
65 | Concretely, if a node 47 is in the witness tree rooted at 1 and the | |
66 | witness tree rooted at 2, then we give an error if 47 is not in the set | |
67 | of nodes satisfying AF[1v2] and give a warning if 47 is in the set of | |
68 | nodes satisfying EXEF(47 & EXEF(1v2)). (Note that the root of a witness | |
69 | tree here is the node causing the pattern to match; there might not be | |
70 | any witnesses associated with this node.) | |
71 | ||
72 | Another try on the exists formula: | |
73 | !(1v2) & EXE[!(1v2) U 47] | |
74 | The first !(1v2) is to discard immediately cases where the beginning and | |
75 | end of the path are the same. Afterwards, it would only seem necessary to | |
76 | serach up to the next occurrence of 47 (leaf), ensuring that there are not | |
77 | 1s or 2s (starting points) along the way. Then the second 47 would be in | |
78 | the path, but possible not transformed. | |
79 | *) | |
80 | ||
81 | module G = Ograph_extended | |
82 | module CTL = Ast_ctl | |
83 | ||
84 | (* Step 1: for each tree, make a mapping from the modified nodes to the root | |
85 | of the tree *) | |
86 | ||
87 | let modified = (Hashtbl.create(25) : (G.nodei, G.nodei list ref) Hashtbl.t) | |
88 | ||
89 | let build_modified (n,_,wits) = | |
90 | let rec loop = function | |
91 | CTL.Wit(st,[CTL.Subst(x,Wrapper_ctl.PredVal(CTL.Modif(v)))],anno,wit) -> | |
92 | let cell = | |
93 | try Hashtbl.find modified st | |
94 | with Not_found -> | |
95 | let cell = ref [] in Hashtbl.add modified st cell; cell in | |
96 | cell := n :: !cell; | |
97 | List.iter loop wit | |
98 | | CTL.Wit(st,_,anno,wit) -> List.iter loop wit | |
99 | | CTL.NegWit(wit) -> () in | |
100 | List.iter loop wits | |
ae4735db | 101 | |
34e49164 C |
102 | (* Step 2: For each node in the hash table, create the error and warning |
103 | formulas *) | |
104 | ||
105 | type 'a nodes = Node of 'a | After | |
ae4735db | 106 | |
34e49164 C |
107 | let create_formulas _ = |
108 | Hashtbl.fold | |
109 | (function node -> | |
110 | function roots -> | |
111 | function acc -> | |
112 | (*let exef f = | |
113 | wrap | |
114 | (Ast_ctl.EX | |
115 | (Ast_ctl.BACKWARD,wrap(Ast_ctl.EF(Ast_ctl.BACKWARD,f)))) in*) | |
116 | let match_node = Ast_ctl.Pred(Node(node)) in | |
117 | let match_roots = | |
118 | List.map (function n -> Ast_ctl.Pred(Node(n))) | |
119 | (List.sort compare !roots) in | |
5636bb2c | 120 | let or_roots = |
34e49164 C |
121 | List.fold_left |
122 | (function prev -> function cur -> Ast_ctl.Or(prev,cur)) | |
123 | (List.hd match_roots) (List.tl match_roots) in | |
5636bb2c C |
124 | (* no point to search if no path, and the presence of after |
125 | in the AF formula can make things slow *) | |
126 | if List.mem node !roots | |
127 | then acc | |
128 | else | |
129 | (node, | |
130 | Ast_ctl.AF(Ast_ctl.BACKWARD,Ast_ctl.NONSTRICT, | |
131 | Ast_ctl.Or(or_roots,Ast_ctl.Pred(After))), | |
132 | Ast_ctl.And | |
133 | (Ast_ctl.NONSTRICT, | |
134 | Ast_ctl.Not(or_roots), | |
135 | Ast_ctl.EX | |
136 | (Ast_ctl.BACKWARD, | |
137 | Ast_ctl.EU(Ast_ctl.BACKWARD,or_roots,match_node)))) | |
34e49164 C |
138 | (*exef |
139 | (wrap(Ast_ctl.And(Ast_ctl.NONSTRICT,match_node,exef(roots))))*) | |
140 | :: acc) | |
141 | modified [] | |
142 | ||
143 | (* Step 3: check the formula on the control-flow graph *) | |
144 | ||
ae4735db | 145 | module PRED = |
34e49164 C |
146 | struct |
147 | type t = Ograph_extended.nodei nodes | |
148 | let print_predicate = function | |
149 | After -> Format.print_string "after" | |
150 | | Node x -> Format.print_string (string_of_int x) | |
151 | end | |
152 | ||
153 | module ENV = | |
154 | struct | |
155 | type value = unit | |
156 | type mvar = unit | |
157 | let eq_mvar x x' = failwith "should not be invoked" | |
158 | let eq_val v v' = failwith "should not be invoked" | |
159 | let merge_val v v' = failwith "should not be invoked" | |
160 | ||
161 | let print_mvar s = failwith "should not be invoked" | |
162 | let print_value x = failwith "should not be invoked" | |
163 | end | |
164 | ||
165 | ||
ae4735db | 166 | module CFG = |
34e49164 C |
167 | struct |
168 | type node = Ograph_extended.nodei | |
ae4735db C |
169 | type cfg = |
170 | (Control_flow_c.node, Control_flow_c.edge) | |
34e49164 C |
171 | Ograph_extended.ograph_mutable |
172 | let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist) | |
173 | let successors cfg n = List.map fst ((cfg#successors n)#tolist) | |
174 | let extract_is_loop cfg n = | |
175 | Control_flow_c.extract_is_loop (cfg#nodes#find n) | |
176 | let print_node i = Format.print_string (string_of_int i) | |
177 | let size cfg = cfg#nodes#length | |
485bce71 | 178 | let print_graph cfg label border_nodes fill_nodes filename = () |
34e49164 C |
179 | end |
180 | ||
181 | module ENGINE = Ctl_engine.CTL_ENGINE (ENV) (CFG) (PRED) | |
182 | ||
183 | let test_formula state formula cfg = | |
184 | let label = function | |
185 | Node pred -> [(pred,[],[])] | |
186 | | After -> | |
187 | List.concat | |
188 | (List.map | |
189 | (fun (nodei, node) -> | |
190 | match Control_flow_c.unwrap node with | |
191 | Control_flow_c.AfterNode -> [(nodei,[],[])] | |
192 | | _ -> []) | |
193 | cfg#nodes#tolist) in | |
194 | let verbose = !Flag_ctl.verbose_ctl_engine in | |
195 | let pm = !Flag_ctl.partial_match in | |
485bce71 | 196 | (* let gt = !Flag_ctl.graphical_trace in *) |
34e49164 C |
197 | Flag_ctl.verbose_ctl_engine := false; |
198 | Flag_ctl.partial_match := false; | |
485bce71 C |
199 | Flag_ctl.checking_reachability := true; |
200 | (* Flag_ctl.graphical_trace := ""; *) | |
34e49164 C |
201 | let res = |
202 | ENGINE.sat (cfg,label,List.map fst cfg#nodes#tolist) | |
203 | (CTL.And(CTL.NONSTRICT,CTL.Pred(Node(state)),formula)) | |
204 | [[Node(state)]] in | |
205 | Flag_ctl.verbose_ctl_engine := verbose; | |
206 | Flag_ctl.partial_match := pm; | |
485bce71 C |
207 | Flag_ctl.checking_reachability := false; |
208 | (* Flag_ctl.graphical_trace := gt; *) | |
34e49164 C |
209 | match res with [] -> false | _ -> true |
210 | ||
211 | (* ---------------------------------------------------------------- *) | |
212 | (* Entry point *) | |
213 | ||
214 | (* The argument is a list of triples with a node name, an empty environment | |
215 | and a witness tree *) | |
216 | ||
217 | type witness = | |
218 | (Ograph_extended.nodei, unit, | |
219 | (Ograph_extended.nodei, unit, unit) Ast_ctl.generic_ctl list) | |
220 | Ast_ctl.generic_witnesstree | |
221 | ||
222 | type ('a,'b,'c,'d,'e) triples = | |
223 | (Ograph_extended.nodei * 'a * | |
224 | (Ograph_extended.nodei, | |
225 | ('b, ('c, 'd) Wrapper_ctl.wrapped_binding) CTL.generic_subst list, 'e) | |
226 | CTL.generic_witnesstree list) list | |
227 | ||
228 | let check_reachability triples cfg = | |
229 | Hashtbl.clear modified; | |
230 | List.iter build_modified triples; | |
231 | let formulas = create_formulas() in | |
232 | List.iter | |
233 | (function (node,af_formula,ef_formula) -> | |
234 | if test_formula node af_formula cfg | |
235 | then | |
236 | if test_formula node ef_formula cfg | |
237 | then | |
238 | Printf.printf "warning: node %d may be inconsistently modified\n" | |
239 | node | |
240 | else () | |
241 | else | |
242 | failwith | |
243 | (Printf.sprintf | |
244 | "node %d reachable by inconsistent control-flow paths" node)) | |
245 | formulas |