Commit | Line | Data |
---|---|---|
f537ebc4 | 1 | (* |
17ba0788 C |
2 | * Copyright 2012, INRIA |
3 | * Julia Lawall, Gilles Muller | |
4 | * Copyright 2010-2011, INRIA, University of Copenhagen | |
f537ebc4 C |
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. | |
9 | * | |
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. | |
13 | * | |
14 | * Coccinelle is distributed in the hope that it will be useful, | |
d6ce1786 C |
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. | |
18 | * | |
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/>. | |
21 | * | |
22 | * The authors reserve the right to distribute this or future versions of | |
23 | * Coccinelle under other licenses. | |
24 | *) | |
25 | ||
26 | ||
feec80c3 | 27 | # 0 "./asttoctl2.ml" |
34e49164 C |
28 | (* for MINUS and CONTEXT, pos is always None in this file *) |
29 | (*search for require*) | |
30 | (* true = don't see all matched nodes, only modified ones *) | |
31 | let onlyModif = ref true(*false*) | |
32 | ||
978fd7e5 | 33 | type ex = Exists | Forall |
34e49164 C |
34 | let exists = ref Forall |
35 | ||
36 | module Ast = Ast_cocci | |
37 | module V = Visitor_ast | |
38 | module CTL = Ast_ctl | |
39 | ||
40 | let warning s = Printf.fprintf stderr "warning: %s\n" s | |
41 | ||
42 | type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif | |
65038c61 C |
43 | type formula = Lib_engine.ctlcocci |
44 | type top_formula = NONDECL of Lib_engine.ctlcocci | CODE of Lib_engine.ctlcocci | |
34e49164 C |
45 | |
46 | let union = Common.union_set | |
47 | let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1 | |
48 | let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1 | |
49 | ||
50 | let foldl1 f xs = List.fold_left f (List.hd xs) (List.tl xs) | |
51 | let foldr1 f xs = | |
52 | let xs = List.rev xs in List.fold_left f (List.hd xs) (List.tl xs) | |
53 | ||
54 | let used_after = ref ([] : Ast.meta_name list) | |
55 | let guard_to_strict guard = if guard then CTL.NONSTRICT else CTL.STRICT | |
56 | ||
57 | let saved = ref ([] : Ast.meta_name list) | |
58 | ||
59 | let string2var x = ("",x) | |
60 | ||
61 | (* --------------------------------------------------------------------- *) | |
62 | (* predicates matching various nodes in the graph *) | |
63 | ||
64 | let ctl_and s x y = | |
65 | match (x,y) with | |
66 | (CTL.False,_) | (_,CTL.False) -> CTL.False | |
67 | | (CTL.True,a) | (a,CTL.True) -> a | |
68 | | _ -> CTL.And(s,x,y) | |
69 | ||
70 | let ctl_or x y = | |
71 | match (x,y) with | |
72 | (CTL.True,_) | (_,CTL.True) -> CTL.True | |
73 | | (CTL.False,a) | (a,CTL.False) -> a | |
74 | | _ -> CTL.Or(x,y) | |
75 | ||
76 | let ctl_or_fl x y = | |
77 | match (x,y) with | |
78 | (CTL.True,_) | (_,CTL.True) -> CTL.True | |
79 | | (CTL.False,a) | (a,CTL.False) -> a | |
80 | | _ -> CTL.Or(y,x) | |
81 | ||
82 | let ctl_seqor x y = | |
83 | match (x,y) with | |
190f1acf C |
84 | (* drop x or true case because x might have side effects *) |
85 | (CTL.True,_) (* | (_,CTL.True) *) -> CTL.True | |
34e49164 C |
86 | | (CTL.False,a) | (a,CTL.False) -> a |
87 | | _ -> CTL.SeqOr(x,y) | |
88 | ||
89 | let ctl_not = function | |
90 | CTL.True -> CTL.False | |
91 | | CTL.False -> CTL.True | |
92 | | x -> CTL.Not(x) | |
93 | ||
94 | let ctl_ax s = function | |
95 | CTL.True -> CTL.True | |
96 | | CTL.False -> CTL.False | |
97 | | x -> | |
98 | match !exists with | |
99 | Exists -> CTL.EX(CTL.FORWARD,x) | |
100 | | Forall -> CTL.AX(CTL.FORWARD,s,x) | |
34e49164 C |
101 | |
102 | let ctl_ax_absolute s = function | |
103 | CTL.True -> CTL.True | |
104 | | CTL.False -> CTL.False | |
105 | | x -> CTL.AX(CTL.FORWARD,s,x) | |
106 | ||
107 | let ctl_ex = function | |
108 | CTL.True -> CTL.True | |
109 | | CTL.False -> CTL.False | |
110 | | x -> CTL.EX(CTL.FORWARD,x) | |
111 | ||
112 | (* This stays being AX even for sgrep_mode, because it is used to identify | |
113 | the structure of the term, not matching the pattern. *) | |
993936c0 C |
114 | let ctl_back_ag = function |
115 | CTL.True -> CTL.True | |
116 | | CTL.False -> CTL.False | |
117 | | x -> CTL.AG(CTL.BACKWARD,CTL.NONSTRICT,x) | |
118 | ||
34e49164 C |
119 | let ctl_back_ax = function |
120 | CTL.True -> CTL.True | |
121 | | CTL.False -> CTL.False | |
122 | | x -> CTL.AX(CTL.BACKWARD,CTL.NONSTRICT,x) | |
123 | ||
124 | let ctl_back_ex = function | |
125 | CTL.True -> CTL.True | |
126 | | CTL.False -> CTL.False | |
127 | | x -> CTL.EX(CTL.BACKWARD,x) | |
128 | ||
129 | let ctl_ef = function | |
130 | CTL.True -> CTL.True | |
131 | | CTL.False -> CTL.False | |
132 | | x -> CTL.EF(CTL.FORWARD,x) | |
133 | ||
134 | let ctl_ag s = function | |
135 | CTL.True -> CTL.True | |
136 | | CTL.False -> CTL.False | |
137 | | x -> CTL.AG(CTL.FORWARD,s,x) | |
138 | ||
139 | let ctl_au s x y = | |
140 | match (x,!exists) with | |
141 | (CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y) | |
142 | | (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y) | |
34e49164 C |
143 | | (_,Exists) -> CTL.EU(CTL.FORWARD,x,y) |
144 | | (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y) | |
34e49164 C |
145 | |
146 | let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *) | |
147 | CTL.XX | |
148 | (match (x,!exists) with | |
149 | (CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y) | |
150 | | (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y) | |
34e49164 | 151 | | (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y) |
978fd7e5 | 152 | | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y)) |
34e49164 C |
153 | |
154 | let ctl_uncheck = function | |
155 | CTL.True -> CTL.True | |
156 | | CTL.False -> CTL.False | |
157 | | x -> CTL.Uncheck x | |
158 | ||
159 | let label_pred_maker = function | |
160 | None -> CTL.True | |
161 | | Some (label_var,used) -> | |
162 | used := true; | |
163 | CTL.Pred(Lib_engine.PrefixLabel(label_var),CTL.Control) | |
164 | ||
165 | let bclabel_pred_maker = function | |
166 | None -> CTL.True | |
167 | | Some (label_var,used) -> | |
168 | used := true; | |
169 | CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control) | |
170 | ||
fc1ad971 C |
171 | (* label used to be used here, but it is not used; label is only needed after |
172 | and within dots *) | |
173 | let predmaker guard pred label = CTL.Pred pred | |
34e49164 C |
174 | |
175 | let aftpred = predmaker false (Lib_engine.After, CTL.Control) | |
176 | let retpred = predmaker false (Lib_engine.Return, CTL.Control) | |
177 | let funpred = predmaker false (Lib_engine.FunHeader, CTL.Control) | |
5427db06 | 178 | let unsbrpred = predmaker false (Lib_engine.UnsafeBrace, CTL.Control) |
34e49164 C |
179 | let toppred = predmaker false (Lib_engine.Top, CTL.Control) |
180 | let exitpred = predmaker false (Lib_engine.ErrorExit, CTL.Control) | |
181 | let endpred = predmaker false (Lib_engine.Exit, CTL.Control) | |
182 | let gotopred = predmaker false (Lib_engine.Goto, CTL.Control) | |
183 | let inlooppred = predmaker false (Lib_engine.InLoop, CTL.Control) | |
184 | let truepred = predmaker false (Lib_engine.TrueBranch, CTL.Control) | |
185 | let falsepred = predmaker false (Lib_engine.FalseBranch, CTL.Control) | |
186 | let fallpred = predmaker false (Lib_engine.FallThrough, CTL.Control) | |
951c7801 | 187 | let loopfallpred = predmaker false (Lib_engine.LoopFallThrough, CTL.Control) |
34e49164 | 188 | |
951c7801 C |
189 | (*let aftret label_var = |
190 | ctl_or (aftpred label_var) | |
191 | (ctl_or (loopfallpred label_var) (exitpred label_var))*) | |
34e49164 C |
192 | |
193 | let letctr = ref 0 | |
194 | let get_let_ctr _ = | |
195 | let cur = !letctr in | |
196 | letctr := cur + 1; | |
197 | Printf.sprintf "r%d" cur | |
198 | ||
199 | (* --------------------------------------------------------------------- *) | |
200 | (* --------------------------------------------------------------------- *) | |
201 | (* Eliminate OptStm *) | |
202 | ||
203 | (* for optional thing with nothing after, should check that the optional thing | |
204 | never occurs. otherwise the matching stops before it occurs *) | |
205 | let elim_opt = | |
206 | let mcode x = x in | |
207 | let donothing r k e = k e in | |
208 | ||
209 | let fvlist l = | |
210 | List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in | |
211 | ||
212 | let mfvlist l = | |
213 | List.fold_left Common.union_set [] (List.map Ast.get_mfvs l) in | |
214 | ||
215 | let freshlist l = | |
216 | List.fold_left Common.union_set [] (List.map Ast.get_fresh l) in | |
217 | ||
218 | let inheritedlist l = | |
219 | List.fold_left Common.union_set [] (List.map Ast.get_inherited l) in | |
220 | ||
221 | let savedlist l = | |
222 | List.fold_left Common.union_set [] (List.map Ast.get_saved l) in | |
223 | ||
224 | let varlists l = | |
225 | (fvlist l, mfvlist l, freshlist l, inheritedlist l, savedlist l) in | |
226 | ||
227 | let rec dots_list unwrapped wrapped = | |
228 | match (unwrapped,wrapped) with | |
229 | ([],_) -> [] | |
230 | ||
231 | | (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest, | |
232 | d0::s::d1::rest) | |
5636bb2c C |
233 | | (Ast.Nest(_,_,_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u) |
234 | ::urest, | |
951c7801 | 235 | d0::s::d1::rest) -> (* why no case for nest as u? *) |
34e49164 C |
236 | let l = Ast.get_line stm in |
237 | let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in | |
238 | let new_rest2 = dots_list urest rest in | |
239 | let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) = | |
240 | varlists new_rest1 in | |
241 | let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) = | |
242 | varlists new_rest2 in | |
243 | [d0; | |
244 | {(Ast.make_term | |
245 | (Ast.Disj | |
246 | [{(Ast.make_term(Ast.DOTS(new_rest1))) with | |
247 | Ast.node_line = l; | |
248 | Ast.free_vars = fv_rest1; | |
249 | Ast.minus_free_vars = mfv_rest1; | |
250 | Ast.fresh_vars = fresh_rest1; | |
251 | Ast.inherited = inherited_rest1; | |
252 | Ast.saved_witness = s1}; | |
253 | {(Ast.make_term(Ast.DOTS(new_rest2))) with | |
254 | Ast.node_line = l; | |
255 | Ast.free_vars = fv_rest2; | |
256 | Ast.minus_free_vars = mfv_rest2; | |
257 | Ast.fresh_vars = fresh_rest2; | |
258 | Ast.inherited = inherited_rest2; | |
259 | Ast.saved_witness = s2}])) with | |
260 | Ast.node_line = l; | |
261 | Ast.free_vars = fv_rest1; | |
262 | Ast.minus_free_vars = mfv_rest1; | |
263 | Ast.fresh_vars = fresh_rest1; | |
264 | Ast.inherited = inherited_rest1; | |
265 | Ast.saved_witness = s1}] | |
266 | ||
267 | | (Ast.OptStm(stm)::urest,_::rest) -> | |
268 | let l = Ast.get_line stm in | |
269 | let new_rest1 = dots_list urest rest in | |
270 | let new_rest2 = stm::new_rest1 in | |
271 | let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) = | |
272 | varlists new_rest1 in | |
273 | let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) = | |
274 | varlists new_rest2 in | |
275 | [{(Ast.make_term | |
276 | (Ast.Disj | |
277 | [{(Ast.make_term(Ast.DOTS(new_rest2))) with | |
278 | Ast.node_line = l; | |
279 | Ast.free_vars = fv_rest2; | |
280 | Ast.minus_free_vars = mfv_rest2; | |
281 | Ast.fresh_vars = fresh_rest2; | |
282 | Ast.inherited = inherited_rest2; | |
283 | Ast.saved_witness = s2}; | |
284 | {(Ast.make_term(Ast.DOTS(new_rest1))) with | |
285 | Ast.node_line = l; | |
286 | Ast.free_vars = fv_rest1; | |
287 | Ast.minus_free_vars = mfv_rest1; | |
288 | Ast.fresh_vars = fresh_rest1; | |
289 | Ast.inherited = inherited_rest1; | |
290 | Ast.saved_witness = s1}])) with | |
291 | Ast.node_line = l; | |
292 | Ast.free_vars = fv_rest2; | |
293 | Ast.minus_free_vars = mfv_rest2; | |
294 | Ast.fresh_vars = fresh_rest2; | |
295 | Ast.inherited = inherited_rest2; | |
296 | Ast.saved_witness = s2}] | |
297 | ||
298 | | ([Ast.Dots(_,_,_,_);Ast.OptStm(stm)],[d1;_]) -> | |
299 | let l = Ast.get_line stm in | |
300 | let fv_stm = Ast.get_fvs stm in | |
301 | let mfv_stm = Ast.get_mfvs stm in | |
302 | let fresh_stm = Ast.get_fresh stm in | |
303 | let inh_stm = Ast.get_inherited stm in | |
304 | let saved_stm = Ast.get_saved stm in | |
305 | let fv_d1 = Ast.get_fvs d1 in | |
306 | let mfv_d1 = Ast.get_mfvs d1 in | |
307 | let fresh_d1 = Ast.get_fresh d1 in | |
308 | let inh_d1 = Ast.get_inherited d1 in | |
309 | let saved_d1 = Ast.get_saved d1 in | |
310 | let fv_both = Common.union_set fv_stm fv_d1 in | |
311 | let mfv_both = Common.union_set mfv_stm mfv_d1 in | |
312 | let fresh_both = Common.union_set fresh_stm fresh_d1 in | |
313 | let inh_both = Common.union_set inh_stm inh_d1 in | |
314 | let saved_both = Common.union_set saved_stm saved_d1 in | |
315 | [d1; | |
316 | {(Ast.make_term | |
317 | (Ast.Disj | |
318 | [{(Ast.make_term(Ast.DOTS([stm]))) with | |
319 | Ast.node_line = l; | |
320 | Ast.free_vars = fv_stm; | |
321 | Ast.minus_free_vars = mfv_stm; | |
322 | Ast.fresh_vars = fresh_stm; | |
323 | Ast.inherited = inh_stm; | |
324 | Ast.saved_witness = saved_stm}; | |
325 | {(Ast.make_term(Ast.DOTS([d1]))) with | |
326 | Ast.node_line = l; | |
327 | Ast.free_vars = fv_d1; | |
328 | Ast.minus_free_vars = mfv_d1; | |
329 | Ast.fresh_vars = fresh_d1; | |
330 | Ast.inherited = inh_d1; | |
331 | Ast.saved_witness = saved_d1}])) with | |
332 | Ast.node_line = l; | |
333 | Ast.free_vars = fv_both; | |
334 | Ast.minus_free_vars = mfv_both; | |
335 | Ast.fresh_vars = fresh_both; | |
336 | Ast.inherited = inh_both; | |
337 | Ast.saved_witness = saved_both}] | |
338 | ||
5636bb2c | 339 | | ([Ast.Nest(_,_,_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) -> |
34e49164 C |
340 | let l = Ast.get_line stm in |
341 | let rw = Ast.rewrap stm in | |
342 | let rwd = Ast.rewrap stm in | |
343 | let dots = Ast.Dots(Ast.make_mcode "...",[],[],[]) in | |
344 | [d1;rw(Ast.Disj | |
345 | [rwd(Ast.DOTS([stm])); | |
346 | {(Ast.make_term(Ast.DOTS([rw dots]))) | |
347 | with Ast.node_line = l}])] | |
348 | ||
349 | | (_::urest,stm::rest) -> stm :: (dots_list urest rest) | |
350 | | _ -> failwith "not possible" in | |
351 | ||
352 | let stmtdotsfn r k d = | |
353 | let d = k d in | |
354 | Ast.rewrap d | |
355 | (match Ast.unwrap d with | |
356 | Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l) | |
357 | | Ast.CIRCLES(l) -> failwith "elimopt: not supported" | |
358 | | Ast.STARS(l) -> failwith "elimopt: not supported") in | |
ae4735db | 359 | |
34e49164 C |
360 | V.rebuilder |
361 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
c491d8ee | 362 | donothing donothing stmtdotsfn donothing donothing |
34e49164 C |
363 | donothing donothing donothing donothing donothing donothing donothing |
364 | donothing donothing donothing donothing donothing | |
365 | ||
366 | (* --------------------------------------------------------------------- *) | |
367 | (* after management *) | |
368 | (* We need Guard for the following case: | |
369 | <... | |
370 | a | |
371 | <... | |
372 | b | |
373 | ...> | |
374 | ...> | |
375 | foo(); | |
376 | ||
377 | Here the inner <... b ...> should not go past foo. But foo is not the | |
378 | "after" of the body of the outer nest, because we don't want to search for | |
379 | it in the case where the body of the outer nest ends in something other | |
380 | than dots or a nest. *) | |
381 | ||
382 | (* what is the difference between tail and end??? *) | |
383 | ||
384 | type after = After of formula | Guard of formula | Tail | End | VeryEnd | |
385 | ||
5427db06 C |
386 | type top = Top | NotTop |
387 | ||
34e49164 C |
388 | let a2n = function After x -> Guard x | a -> a |
389 | ||
390 | let print_ctl x = | |
391 | let pp_pred (x,_) = Pretty_print_engine.pp_predicate x in | |
392 | let pp_meta (_,x) = Common.pp x in | |
393 | Pretty_print_ctl.pp_ctl (pp_pred,pp_meta) false x; | |
394 | Format.print_newline() | |
395 | ||
396 | let print_after = function | |
397 | After ctl -> Printf.printf "After:\n"; print_ctl ctl | |
398 | | Guard ctl -> Printf.printf "Guard:\n"; print_ctl ctl | |
399 | | Tail -> Printf.printf "Tail\n" | |
400 | | VeryEnd -> Printf.printf "Very End\n" | |
401 | | End -> Printf.printf "End\n" | |
402 | ||
403 | (* --------------------------------------------------------------------- *) | |
404 | (* Top-level code *) | |
405 | ||
406 | let fresh_var _ = string2var "_v" | |
407 | let fresh_pos _ = string2var "_pos" (* must be a constant *) | |
408 | ||
409 | let fresh_metavar _ = "_S" | |
410 | ||
411 | (* fvinfo is going to end up being from the whole associated statement. | |
412 | it would be better if it were just the free variables in d, but free_vars.ml | |
413 | doesn't keep track of free variables on + code *) | |
414 | let make_meta_rule_elem d fvinfo = | |
415 | let nm = fresh_metavar() in | |
416 | Ast.make_meta_rule_elem nm d fvinfo | |
417 | ||
418 | let get_unquantified quantified vars = | |
419 | List.filter (function x -> not (List.mem x quantified)) vars | |
420 | ||
421 | let make_seq guard l = | |
422 | let s = guard_to_strict guard in | |
423 | foldr1 (function rest -> function cur -> ctl_and s cur (ctl_ax s rest)) l | |
424 | ||
425 | let make_seq_after2 guard first rest = | |
426 | let s = guard_to_strict guard in | |
427 | match rest with | |
428 | After rest -> ctl_and s first (ctl_ax s (ctl_ax s rest)) | |
429 | | _ -> first | |
430 | ||
431 | let make_seq_after guard first rest = | |
432 | match rest with | |
433 | After rest -> make_seq guard [first;rest] | |
434 | | _ -> first | |
435 | ||
436 | let opt_and guard first rest = | |
437 | let s = guard_to_strict guard in | |
438 | match first with | |
439 | None -> rest | |
440 | | Some first -> ctl_and s first rest | |
441 | ||
442 | let and_after guard first rest = | |
443 | let s = guard_to_strict guard in | |
444 | match rest with After rest -> ctl_and s first rest | _ -> first | |
445 | ||
446 | let contains_modif = | |
447 | let bind x y = x or y in | |
448 | let option_default = false in | |
91eba41f | 449 | let mcode r (_,_,kind,metapos) = |
34e49164 | 450 | match kind with |
708f4980 | 451 | Ast.MINUS(_,_,_,_) -> true |
951c7801 | 452 | | Ast.PLUS _ -> failwith "not possible" |
34e49164 C |
453 | | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in |
454 | let do_nothing r k e = k e in | |
455 | let rule_elem r k re = | |
456 | let res = k re in | |
457 | match Ast.unwrap re with | |
458 | Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) -> | |
8f657093 C |
459 | bind (mcode r ((),(),bef,[])) res |
460 | | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res | |
34e49164 | 461 | | _ -> res in |
90aeb998 C |
462 | let init r k i = |
463 | let res = k i in | |
464 | match Ast.unwrap i with | |
c491d8ee | 465 | Ast.StrInitList(allminus,_,_,_,_) -> allminus or res |
90aeb998 | 466 | | _ -> res in |
34e49164 C |
467 | let recursor = |
468 | V.combiner bind option_default | |
469 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
c491d8ee | 470 | do_nothing do_nothing do_nothing do_nothing do_nothing |
90aeb998 | 471 | do_nothing do_nothing do_nothing do_nothing init do_nothing |
34e49164 C |
472 | do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in |
473 | recursor.V.combiner_rule_elem | |
474 | ||
91eba41f C |
475 | let contains_pos = |
476 | let bind x y = x or y in | |
477 | let option_default = false in | |
8f657093 | 478 | let mcode r (_,_,kind,metapos) = not (metapos = []) in |
91eba41f C |
479 | let do_nothing r k e = k e in |
480 | let rule_elem r k re = | |
481 | let res = k re in | |
482 | match Ast.unwrap re with | |
483 | Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) -> | |
8f657093 C |
484 | bind (mcode r ((),(),bef,[])) res |
485 | | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res | |
91eba41f C |
486 | | _ -> res in |
487 | let recursor = | |
488 | V.combiner bind option_default | |
489 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
c491d8ee | 490 | do_nothing do_nothing do_nothing do_nothing do_nothing |
91eba41f C |
491 | do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing |
492 | do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in | |
493 | recursor.V.combiner_rule_elem | |
494 | ||
34e49164 C |
495 | (* code is not a DisjRuleElem *) |
496 | let make_match label guard code = | |
497 | let v = fresh_var() in | |
498 | let matcher = Lib_engine.Match(code) in | |
499 | if contains_modif code && not guard | |
500 | then CTL.Exists(true,v,predmaker guard (matcher,CTL.Modif v) label) | |
501 | else | |
502 | let iso_info = !Flag.track_iso_usage && not (Ast.get_isos code = []) in | |
503 | (match (iso_info,!onlyModif,guard, | |
504 | intersect !used_after (Ast.get_fvs code)) with | |
505 | (false,true,_,[]) | (_,_,true,_) -> | |
506 | predmaker guard (matcher,CTL.Control) label | |
507 | | _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label)) | |
508 | ||
509 | let make_raw_match label guard code = | |
413ffc02 C |
510 | match intersect !used_after (Ast.get_fvs code) with |
511 | [] -> predmaker guard (Lib_engine.Match(code),CTL.Control) label | |
512 | | _ -> | |
513 | let v = fresh_var() in | |
514 | CTL.Exists(true,v,predmaker guard (Lib_engine.Match(code),CTL.UnModif v) | |
515 | label) | |
ae4735db | 516 | |
34e49164 C |
517 | let rec seq_fvs quantified = function |
518 | [] -> [] | |
519 | | fv1::fvs -> | |
520 | let t1fvs = get_unquantified quantified fv1 in | |
521 | let termfvs = | |
522 | List.fold_left Common.union_set [] | |
523 | (List.map (get_unquantified quantified) fvs) in | |
524 | let bothfvs = Common.inter_set t1fvs termfvs in | |
525 | let t1onlyfvs = Common.minus_set t1fvs bothfvs in | |
526 | let new_quantified = Common.union_set bothfvs quantified in | |
527 | (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs) | |
528 | ||
529 | let quantify guard = | |
530 | List.fold_right | |
531 | (function cur -> | |
532 | function code -> CTL.Exists (not guard && List.mem cur !saved,cur,code)) | |
533 | ||
534 | let non_saved_quantify = | |
535 | List.fold_right | |
536 | (function cur -> function code -> CTL.Exists (false,cur,code)) | |
537 | ||
538 | let intersectll lst nested_list = | |
539 | List.filter (function x -> List.exists (List.mem x) nested_list) lst | |
540 | ||
541 | (* --------------------------------------------------------------------- *) | |
542 | (* Count depth of braces. The translation of a closed brace appears deeply | |
543 | nested within the translation of the sequence term, so the name of the | |
544 | paren var has to take into account the names of the nested braces. On the | |
545 | other hand the close brace does not escape, so we don't have to take into | |
546 | account other paren variable names. *) | |
547 | ||
548 | (* called repetitively, which is inefficient, but less trouble than adding a | |
549 | new field to Seq and FunDecl *) | |
550 | let count_nested_braces s = | |
551 | let bind x y = max x y in | |
552 | let option_default = 0 in | |
553 | let stmt_count r k s = | |
554 | match Ast.unwrap s with | |
708f4980 | 555 | Ast.Seq(_,_,_) | Ast.FunDecl(_,_,_,_) -> (k s) + 1 |
34e49164 C |
556 | | _ -> k s in |
557 | let donothing r k e = k e in | |
558 | let mcode r x = 0 in | |
559 | let recursor = V.combiner bind option_default | |
560 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
c491d8ee | 561 | donothing donothing donothing donothing donothing |
34e49164 C |
562 | donothing donothing donothing donothing donothing donothing |
563 | donothing donothing stmt_count donothing donothing donothing in | |
564 | let res = string_of_int (recursor.V.combiner_statement s) in | |
565 | string2var ("p"^res) | |
566 | ||
567 | let labelctr = ref 0 | |
568 | let get_label_ctr _ = | |
569 | let cur = !labelctr in | |
570 | labelctr := cur + 1; | |
571 | string2var (Printf.sprintf "l%d" cur) | |
572 | ||
573 | (* --------------------------------------------------------------------- *) | |
574 | (* annotate dots with before and after neighbors *) | |
575 | ||
576 | let print_bef_aft = function | |
577 | Ast.WParen (re,n) -> | |
578 | Printf.printf "bef/aft\n"; | |
579 | Pretty_print_cocci.rule_elem "" re; | |
580 | Format.print_newline() | |
581 | | Ast.Other s -> | |
582 | Printf.printf "bef/aft\n"; | |
583 | Pretty_print_cocci.statement "" s; | |
584 | Format.print_newline() | |
585 | | Ast.Other_dots d -> | |
586 | Printf.printf "bef/aft\n"; | |
587 | Pretty_print_cocci.statement_dots d; | |
588 | Format.print_newline() | |
589 | ||
590 | (* [] can only occur if we are in a disj, where it comes from a ? In that | |
591 | case, we want to use a, which accumulates all of the previous patterns in | |
592 | their entirety. *) | |
593 | let rec get_before_elem sl a = | |
594 | match Ast.unwrap sl with | |
595 | Ast.DOTS(x) -> | |
596 | let rec loop sl a = | |
597 | match sl with | |
598 | [] -> ([],Common.Right a) | |
599 | | [e] -> | |
600 | let (e,ea) = get_before_e e a in | |
601 | ([e],Common.Left ea) | |
602 | | e::sl -> | |
603 | let (e,ea) = get_before_e e a in | |
604 | let (sl,sla) = loop sl ea in | |
605 | (e::sl,sla) in | |
606 | let (l,a) = loop x a in | |
607 | (Ast.rewrap sl (Ast.DOTS(l)),a) | |
608 | | Ast.CIRCLES(x) -> failwith "not supported" | |
609 | | Ast.STARS(x) -> failwith "not supported" | |
610 | ||
611 | and get_before sl a = | |
612 | match get_before_elem sl a with | |
613 | (term,Common.Left x) -> (term,x) | |
614 | | (term,Common.Right x) -> (term,x) | |
615 | ||
616 | and get_before_whencode wc = | |
617 | List.map | |
618 | (function | |
619 | Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w | |
620 | | Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w | |
1be43e12 C |
621 | | Ast.WhenModifier(x) -> Ast.WhenModifier(x) |
622 | | Ast.WhenNotTrue w -> Ast.WhenNotTrue w | |
623 | | Ast.WhenNotFalse w -> Ast.WhenNotFalse w) | |
34e49164 C |
624 | wc |
625 | ||
626 | and get_before_e s a = | |
627 | match Ast.unwrap s with | |
628 | Ast.Dots(d,w,_,aft) -> | |
629 | (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a) | |
5636bb2c | 630 | | Ast.Nest(starter,stmt_dots,ender,w,multi,_,aft) -> |
34e49164 C |
631 | let w = get_before_whencode w in |
632 | let (sd,_) = get_before stmt_dots a in | |
978fd7e5 C |
633 | (*let a = |
634 | got rid of this, don't want to let nests overshoot | |
34e49164 C |
635 | List.filter |
636 | (function | |
637 | Ast.Other a -> | |
638 | let unifies = | |
639 | Unify_ast.unify_statement_dots | |
640 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in | |
641 | (match unifies with | |
642 | Unify_ast.MAYBE -> false | |
643 | | _ -> true) | |
644 | | Ast.Other_dots a -> | |
645 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in | |
646 | (match unifies with | |
647 | Unify_ast.MAYBE -> false | |
648 | | _ -> true) | |
649 | | _ -> true) | |
978fd7e5 | 650 | a in*) |
5636bb2c C |
651 | (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,a,aft)), |
652 | [Ast.Other_dots stmt_dots]) | |
34e49164 C |
653 | | Ast.Disj(stmt_dots_list) -> |
654 | let (dsl,dsla) = | |
655 | List.split (List.map (function e -> get_before e a) stmt_dots_list) in | |
656 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) | |
657 | | Ast.Atomic(ast) -> | |
658 | (match Ast.unwrap ast with | |
659 | Ast.MetaStmt(_,_,_,_) -> (s,[]) | |
660 | | _ -> (s,[Ast.Other s])) | |
708f4980 | 661 | | Ast.Seq(lbrace,body,rbrace) -> |
34e49164 | 662 | let index = count_nested_braces s in |
708f4980 C |
663 | let (bd,_) = get_before body [Ast.WParen(lbrace,index)] in |
664 | (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),[Ast.WParen(rbrace,index)]) | |
34e49164 C |
665 | | Ast.Define(header,body) -> |
666 | let (body,_) = get_before body [] in | |
667 | (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s]) | |
17ba0788 C |
668 | | Ast.AsStmt(stmt,asstmt) -> |
669 | let (stmt,_) = get_before_e stmt [] in | |
670 | let (asstmt,_) = get_before_e asstmt [] in | |
671 | (Ast.rewrap s (Ast.AsStmt(stmt,asstmt)),[Ast.Other s]) | |
34e49164 C |
672 | | Ast.IfThen(ifheader,branch,aft) -> |
673 | let (br,_) = get_before_e branch [] in | |
674 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s]) | |
675 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
676 | let (br1,_) = get_before_e branch1 [] in | |
677 | let (br2,_) = get_before_e branch2 [] in | |
678 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) | |
679 | | Ast.While(header,body,aft) -> | |
680 | let (bd,_) = get_before_e body [] in | |
681 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) | |
682 | | Ast.For(header,body,aft) -> | |
683 | let (bd,_) = get_before_e body [] in | |
684 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) | |
685 | | Ast.Do(header,body,tail) -> | |
686 | let (bd,_) = get_before_e body [] in | |
687 | (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s]) | |
688 | | Ast.Iterator(header,body,aft) -> | |
689 | let (bd,_) = get_before_e body [] in | |
690 | (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s]) | |
fc1ad971 C |
691 | | Ast.Switch(header,lb,decls,cases,rb) -> |
692 | let index = count_nested_braces s in | |
693 | let (de,dea) = get_before decls [Ast.WParen(lb,index)] in | |
34e49164 C |
694 | let cases = |
695 | List.map | |
696 | (function case_line -> | |
697 | match Ast.unwrap case_line with | |
698 | Ast.CaseLine(header,body) -> | |
699 | let (body,_) = get_before body [] in | |
700 | Ast.rewrap case_line (Ast.CaseLine(header,body)) | |
701 | | Ast.OptCase(case_line) -> failwith "not supported") | |
702 | cases in | |
fc1ad971 C |
703 | (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)), |
704 | [Ast.WParen(rb,index)]) | |
708f4980 C |
705 | | Ast.FunDecl(header,lbrace,body,rbrace) -> |
706 | let (bd,_) = get_before body [] in | |
707 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[]) | |
91eba41f C |
708 | | _ -> |
709 | Pretty_print_cocci.statement "" s; Format.print_newline(); | |
710 | failwith "get_before_e: not supported" | |
34e49164 C |
711 | |
712 | let rec get_after sl a = | |
713 | match Ast.unwrap sl with | |
714 | Ast.DOTS(x) -> | |
715 | let rec loop sl = | |
716 | match sl with | |
717 | [] -> ([],a) | |
718 | | e::sl -> | |
719 | let (sl,sla) = loop sl in | |
720 | let (e,ea) = get_after_e e sla in | |
721 | (e::sl,ea) in | |
722 | let (l,a) = loop x in | |
723 | (Ast.rewrap sl (Ast.DOTS(l)),a) | |
724 | | Ast.CIRCLES(x) -> failwith "not supported" | |
725 | | Ast.STARS(x) -> failwith "not supported" | |
726 | ||
727 | and get_after_whencode a wc = | |
728 | List.map | |
729 | (function | |
730 | Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w | |
731 | | Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w | |
1be43e12 C |
732 | | Ast.WhenModifier(x) -> Ast.WhenModifier(x) |
733 | | Ast.WhenNotTrue w -> Ast.WhenNotTrue w | |
734 | | Ast.WhenNotFalse w -> Ast.WhenNotFalse w) | |
34e49164 C |
735 | wc |
736 | ||
737 | and get_after_e s a = | |
738 | match Ast.unwrap s with | |
739 | Ast.Dots(d,w,bef,_) -> | |
740 | (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a) | |
5636bb2c | 741 | | Ast.Nest(starter,stmt_dots,ender,w,multi,bef,_) -> |
34e49164 C |
742 | let w = get_after_whencode a w in |
743 | let (sd,_) = get_after stmt_dots a in | |
978fd7e5 C |
744 | (*let a = |
745 | got rid of this. don't want to let nests overshoot | |
34e49164 C |
746 | List.filter |
747 | (function | |
748 | Ast.Other a -> | |
749 | let unifies = | |
750 | Unify_ast.unify_statement_dots | |
751 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in | |
752 | (match unifies with | |
753 | Unify_ast.MAYBE -> false | |
754 | | _ -> true) | |
755 | | Ast.Other_dots a -> | |
756 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in | |
757 | (match unifies with | |
758 | Unify_ast.MAYBE -> false | |
759 | | _ -> true) | |
760 | | _ -> true) | |
978fd7e5 | 761 | a in*) |
5636bb2c C |
762 | (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,bef,a)), |
763 | [Ast.Other_dots stmt_dots]) | |
34e49164 C |
764 | | Ast.Disj(stmt_dots_list) -> |
765 | let (dsl,dsla) = | |
766 | List.split (List.map (function e -> get_after e a) stmt_dots_list) in | |
767 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) | |
768 | | Ast.Atomic(ast) -> | |
769 | (match Ast.unwrap ast with | |
770 | Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots _,i) -> | |
771 | (* check "after" information for metavar optimization *) | |
772 | (* if the error is not desired, could just return [], then | |
773 | the optimization (check for EF) won't take place *) | |
774 | List.iter | |
775 | (function | |
776 | Ast.Other x -> | |
777 | (match Ast.unwrap x with | |
5636bb2c | 778 | Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) -> |
34e49164 C |
779 | failwith |
780 | "dots/nest not allowed before and after stmt metavar" | |
781 | | _ -> ()) | |
782 | | Ast.Other_dots x -> | |
783 | (match Ast.undots x with | |
784 | x::_ -> | |
785 | (match Ast.unwrap x with | |
5636bb2c | 786 | Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) -> |
34e49164 C |
787 | failwith |
788 | ("dots/nest not allowed before and after stmt "^ | |
789 | "metavar") | |
790 | | _ -> ()) | |
791 | | _ -> ()) | |
792 | | _ -> ()) | |
793 | a; | |
794 | (Ast.rewrap s | |
795 | (Ast.Atomic | |
796 | (Ast.rewrap s | |
797 | (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[]) | |
798 | | Ast.MetaStmt(_,_,_,_) -> (s,[]) | |
799 | | _ -> (s,[Ast.Other s])) | |
708f4980 | 800 | | Ast.Seq(lbrace,body,rbrace) -> |
34e49164 | 801 | let index = count_nested_braces s in |
708f4980 C |
802 | let (bd,_) = get_after body [Ast.WParen(rbrace,index)] in |
803 | (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)), | |
34e49164 C |
804 | [Ast.WParen(lbrace,index)]) |
805 | | Ast.Define(header,body) -> | |
806 | let (body,_) = get_after body a in | |
807 | (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s]) | |
17ba0788 C |
808 | | Ast.AsStmt(stmt,asstmt) -> |
809 | let (stmt,_) = get_after_e stmt [] in | |
810 | let (asstmt,_) = get_after_e asstmt [] in | |
811 | (Ast.rewrap s (Ast.AsStmt(stmt,asstmt)),[Ast.Other s]) | |
34e49164 C |
812 | | Ast.IfThen(ifheader,branch,aft) -> |
813 | let (br,_) = get_after_e branch a in | |
814 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s]) | |
815 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
816 | let (br1,_) = get_after_e branch1 a in | |
817 | let (br2,_) = get_after_e branch2 a in | |
818 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) | |
819 | | Ast.While(header,body,aft) -> | |
993936c0 | 820 | let (bd,_) = get_after_e body ((Ast.Other s) :: a) in |
34e49164 C |
821 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) |
822 | | Ast.For(header,body,aft) -> | |
993936c0 | 823 | let (bd,_) = get_after_e body ((Ast.Other s) :: a) in |
34e49164 C |
824 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) |
825 | | Ast.Do(header,body,tail) -> | |
993936c0 | 826 | let (bd,_) = get_after_e body ((Ast.Other s) :: a) in |
34e49164 C |
827 | (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s]) |
828 | | Ast.Iterator(header,body,aft) -> | |
993936c0 | 829 | let (bd,_) = get_after_e body ((Ast.Other s) :: a) in |
34e49164 | 830 | (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s]) |
fc1ad971 C |
831 | | Ast.Switch(header,lb,decls,cases,rb) -> |
832 | let index = count_nested_braces s in | |
34e49164 C |
833 | let cases = |
834 | List.map | |
835 | (function case_line -> | |
836 | match Ast.unwrap case_line with | |
837 | Ast.CaseLine(header,body) -> | |
fc1ad971 | 838 | let (body,_) = get_after body [Ast.WParen(rb,index)] in |
34e49164 C |
839 | Ast.rewrap case_line (Ast.CaseLine(header,body)) |
840 | | Ast.OptCase(case_line) -> failwith "not supported") | |
841 | cases in | |
fc1ad971 C |
842 | let (de,_) = get_after decls [] in |
843 | (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),[Ast.WParen(lb,index)]) | |
708f4980 C |
844 | | Ast.FunDecl(header,lbrace,body,rbrace) -> |
845 | let (bd,_) = get_after body [] in | |
846 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[]) | |
34e49164 C |
847 | | _ -> failwith "get_after_e: not supported" |
848 | ||
849 | let preprocess_dots sl = | |
850 | let (sl,_) = get_before sl [] in | |
851 | let (sl,_) = get_after sl [] in | |
852 | sl | |
853 | ||
854 | let preprocess_dots_e sl = | |
855 | let (sl,_) = get_before_e sl [] in | |
856 | let (sl,_) = get_after_e sl [] in | |
857 | sl | |
858 | ||
859 | (* --------------------------------------------------------------------- *) | |
860 | (* various return_related things *) | |
861 | ||
862 | let rec ends_in_return stmt_list = | |
863 | match Ast.unwrap stmt_list with | |
864 | Ast.DOTS(x) -> | |
865 | (match List.rev x with | |
866 | x::_ -> | |
867 | (match Ast.unwrap x with | |
868 | Ast.Atomic(x) -> | |
1be43e12 C |
869 | let rec loop x = |
870 | match Ast.unwrap x with | |
871 | Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true | |
872 | | Ast.DisjRuleElem((_::_) as l) -> List.for_all loop l | |
873 | | _ -> false in | |
874 | loop x | |
34e49164 C |
875 | | Ast.Disj(disjs) -> List.for_all ends_in_return disjs |
876 | | _ -> false) | |
877 | | _ -> false) | |
878 | | Ast.CIRCLES(x) -> failwith "not supported" | |
879 | | Ast.STARS(x) -> failwith "not supported" | |
880 | ||
881 | (* --------------------------------------------------------------------- *) | |
882 | (* expressions *) | |
883 | ||
884 | let exptymatch l make_match make_guard_match = | |
885 | let pos = fresh_pos() in | |
886 | let matches_guard_matches = | |
887 | List.map | |
888 | (function x -> | |
889 | let pos = Ast.make_mcode pos in | |
890 | (make_match (Ast.set_pos x (Some pos)), | |
891 | make_guard_match (Ast.set_pos x (Some pos)))) | |
892 | l in | |
893 | let (matches,guard_matches) = List.split matches_guard_matches in | |
894 | let rec suffixes = function | |
895 | [] -> [] | |
896 | | x::xs -> xs::(suffixes xs) in | |
978fd7e5 C |
897 | let prefixes = |
898 | (* normally, we check that an expression does not match something | |
899 | earlier in the disjunction (calculated as prefixes). But for large | |
900 | disjunctions, this can result in a very big CTL formula. So we | |
901 | give the user the option to say he doesn't want this feature, if that is | |
902 | the case. *) | |
903 | if !Flag_matcher.no_safe_expressions | |
904 | then List.map (function _ -> []) matches | |
905 | else List.rev (suffixes (List.rev guard_matches)) in | |
34e49164 C |
906 | let info = (* not null *) |
907 | List.map2 | |
908 | (function matcher -> | |
909 | function negates -> | |
910 | CTL.Exists | |
911 | (false,pos, | |
912 | ctl_and CTL.NONSTRICT matcher | |
913 | (ctl_not | |
914 | (ctl_uncheck (List.fold_left ctl_or_fl CTL.False negates))))) | |
915 | matches prefixes in | |
916 | CTL.InnerAnd(List.fold_left ctl_or_fl CTL.False (List.rev info)) | |
917 | ||
918 | (* code might be a DisjRuleElem, in which case we break it apart | |
919 | code might contain an Exp or Ty | |
920 | this one pushes the quantifier inwards *) | |
921 | let do_re_matches label guard res quantified minus_quantified = | |
922 | let make_guard_match x = | |
923 | let stmt_fvs = Ast.get_mfvs x in | |
924 | let fvs = get_unquantified minus_quantified stmt_fvs in | |
925 | non_saved_quantify fvs (make_match None true x) in | |
926 | let make_match x = | |
927 | let stmt_fvs = Ast.get_fvs x in | |
928 | let fvs = get_unquantified quantified stmt_fvs in | |
929 | quantify guard fvs (make_match None guard x) in | |
fc1ad971 | 930 | (* label used to be used here, but it is not use; label is only needed after |
ae4735db | 931 | and within dots |
fc1ad971 | 932 | ctl_and CTL.NONSTRICT (label_pred_maker label) *) |
34e49164 C |
933 | (match List.map Ast.unwrap res with |
934 | [] -> failwith "unexpected empty disj" | |
935 | | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match | |
936 | | Ast.Ty(t)::rest -> exptymatch res make_match make_guard_match | |
937 | | all -> | |
938 | if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false) | |
939 | all | |
940 | then failwith "unexpected exp or ty"; | |
978fd7e5 | 941 | List.fold_left ctl_seqor CTL.False (List.map make_match res)) |
34e49164 C |
942 | |
943 | (* code might be a DisjRuleElem, in which case we break it apart | |
944 | code doesn't contain an Exp or Ty | |
945 | this one is for use when it is not practical to push the quantifier inwards | |
946 | *) | |
947 | let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl = | |
948 | match Ast.unwrap code with | |
949 | Ast.DisjRuleElem(res) -> | |
950 | let make_match = make_match None guard in | |
951 | let orop = if guard then ctl_or else ctl_seqor in | |
fc1ad971 C |
952 | (* label used to be used here, but it is not use; label is only needed after |
953 | and within dots | |
954 | ctl_and CTL.NONSTRICT (label_pred_maker label) *) | |
34e49164 C |
955 | (List.fold_left orop CTL.False (List.map make_match res)) |
956 | | _ -> make_match label guard code | |
957 | ||
958 | (* --------------------------------------------------------------------- *) | |
959 | (* control structures *) | |
960 | ||
961 | let end_control_structure fvs header body after_pred | |
962 | after_checks no_after_checks (afvs,afresh,ainh,aft) after label guard = | |
963 | (* aft indicates what is added after the whole if, which has to be added | |
964 | to the endif node *) | |
965 | let (aft_needed,after_branch) = | |
966 | match aft with | |
967 | Ast.CONTEXT(_,Ast.NOTHING) -> | |
968 | (false,make_seq_after2 guard after_pred after) | |
969 | | _ -> | |
970 | let match_endif = | |
971 | make_match label guard | |
972 | (make_meta_rule_elem aft (afvs,afresh,ainh)) in | |
973 | (true, | |
974 | make_seq_after guard after_pred | |
975 | (After(make_seq_after guard match_endif after))) in | |
976 | let body = body after_branch in | |
977 | let s = guard_to_strict guard in | |
978 | (* the code *) | |
979 | quantify guard fvs | |
980 | (ctl_and s header | |
981 | (opt_and guard | |
982 | (match (after,aft_needed) with | |
983 | (After _,_) (* pattern doesn't end here *) | |
984 | | (_,true) (* + code added after *) -> after_checks | |
985 | | _ -> no_after_checks) | |
986 | (ctl_ax_absolute s body))) | |
987 | ||
988 | let ifthen ifheader branch ((afvs,_,_,_) as aft) after | |
989 | quantified minus_quantified label llabel slabel recurse make_match guard = | |
990 | (* "if (test) thn" becomes: | |
991 | if(test) & AX((TrueBranch & AX thn) v FallThrough v After) | |
992 | ||
993 | "if (test) thn; after" becomes: | |
994 | if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after)) | |
995 | & EX After | |
996 | *) | |
ae4735db | 997 | (* free variables *) |
34e49164 C |
998 | let (efvs,bfvs) = |
999 | match seq_fvs quantified | |
1000 | [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with | |
1001 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) | |
1002 | | _ -> failwith "not possible" in | |
1003 | let new_quantified = Common.union_set bfvs quantified in | |
1004 | let (mefvs,mbfvs) = | |
1005 | match seq_fvs minus_quantified | |
1006 | [Ast.get_mfvs ifheader;Ast.get_mfvs branch;[]] with | |
1007 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) | |
1008 | | _ -> failwith "not possible" in | |
1009 | let new_mquantified = Common.union_set mbfvs minus_quantified in | |
1010 | (* if header *) | |
1011 | let if_header = quantify guard efvs (make_match ifheader) in | |
1012 | (* then branch and after *) | |
1013 | let lv = get_label_ctr() in | |
1014 | let used = ref false in | |
1015 | let true_branch = | |
002099fc C |
1016 | (* no point to put a label on truepred etc; it is local to this construct |
1017 | so it must have the same label *) | |
34e49164 | 1018 | make_seq guard |
5427db06 | 1019 | [truepred None; recurse branch NotTop Tail new_quantified new_mquantified |
34e49164 | 1020 | (Some (lv,used)) llabel slabel guard] in |
002099fc | 1021 | let after_pred = aftpred None in |
34e49164 | 1022 | let or_cases after_branch = |
002099fc | 1023 | ctl_or true_branch (ctl_or (fallpred None) after_branch) in |
34e49164 C |
1024 | let (if_header,wrapper) = |
1025 | if !used | |
1026 | then | |
1027 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in | |
1028 | (ctl_and CTL.NONSTRICT(*???*) if_header label_pred, | |
1029 | (function body -> quantify true [lv] body)) | |
1030 | else (if_header,function x -> x) in | |
1031 | wrapper | |
1032 | (end_control_structure bfvs if_header or_cases after_pred | |
1033 | (Some(ctl_ex after_pred)) None aft after label guard) | |
1034 | ||
1035 | let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after | |
1036 | quantified minus_quantified label llabel slabel recurse make_match guard = | |
1037 | (* "if (test) thn else els" becomes: | |
1038 | if(test) & AX((TrueBranch & AX thn) v | |
1039 | (FalseBranch & AX (else & AX els)) v After) | |
1040 | & EX FalseBranch | |
1041 | ||
1042 | "if (test) thn else els; after" becomes: | |
1043 | if(test) & AX((TrueBranch & AX thn) v | |
1044 | (FalseBranch & AX (else & AX els)) v | |
1045 | (After & AXAX after)) | |
1046 | & EX FalseBranch | |
1047 | & EX After | |
1048 | *) | |
1049 | (* free variables *) | |
1050 | let (e1fvs,b1fvs,s1fvs) = | |
1051 | match seq_fvs quantified | |
1052 | [Ast.get_fvs ifheader;Ast.get_fvs branch1;afvs] with | |
1053 | [(e1fvs,b1fvs);(s1fvs,b1afvs);_] -> | |
1054 | (e1fvs,Common.union_set b1fvs b1afvs,s1fvs) | |
1055 | | _ -> failwith "not possible" in | |
1056 | let (e2fvs,b2fvs,s2fvs) = | |
1057 | (* fvs on else? *) | |
978fd7e5 C |
1058 | (* just combine with the else branch. no point to have separate |
1059 | quantifier, since there is only one possible control-flow path *) | |
1060 | let else_fvs = Common.union_set (Ast.get_fvs els) (Ast.get_fvs branch2) in | |
1061 | match seq_fvs quantified [Ast.get_fvs ifheader;else_fvs;afvs] with | |
34e49164 | 1062 | [(e2fvs,b2fvs);(s2fvs,b2afvs);_] -> |
978fd7e5 | 1063 | (e2fvs,Common.union_set b2fvs b2afvs,s2fvs) |
34e49164 C |
1064 | | _ -> failwith "not possible" in |
1065 | let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in | |
1066 | let exponlyfvs = intersect e1fvs e2fvs in | |
1067 | let new_quantified = union bothfvs quantified in | |
1068 | (* minus free variables *) | |
1069 | let (me1fvs,mb1fvs,ms1fvs) = | |
1070 | match seq_fvs minus_quantified | |
1071 | [Ast.get_mfvs ifheader;Ast.get_mfvs branch1;[]] with | |
1072 | [(e1fvs,b1fvs);(s1fvs,b1afvs);_] -> | |
1073 | (e1fvs,Common.union_set b1fvs b1afvs,s1fvs) | |
1074 | | _ -> failwith "not possible" in | |
1075 | let (me2fvs,mb2fvs,ms2fvs) = | |
1076 | (* fvs on else? *) | |
978fd7e5 C |
1077 | (* just combine with the else branch. no point to have separate |
1078 | quantifier, since there is only one possible control-flow path *) | |
1079 | let else_mfvs = | |
1080 | Common.union_set (Ast.get_mfvs els) (Ast.get_mfvs branch2) in | |
1081 | match seq_fvs minus_quantified [Ast.get_mfvs ifheader;else_mfvs;[]] with | |
34e49164 C |
1082 | [(e2fvs,b2fvs);(s2fvs,b2afvs);_] -> |
1083 | (e2fvs,Common.union_set b2fvs b2afvs,s2fvs) | |
1084 | | _ -> failwith "not possible" in | |
1085 | let mbothfvs = union (union mb1fvs mb2fvs) (intersect ms1fvs ms2fvs) in | |
1086 | let new_mquantified = union mbothfvs minus_quantified in | |
1087 | (* if header *) | |
1088 | let if_header = quantify guard exponlyfvs (make_match ifheader) in | |
1089 | (* then and else branches *) | |
1090 | let lv = get_label_ctr() in | |
1091 | let used = ref false in | |
1092 | let true_branch = | |
1093 | make_seq guard | |
5427db06 | 1094 | [truepred None; recurse branch1 NotTop Tail new_quantified new_mquantified |
34e49164 C |
1095 | (Some (lv,used)) llabel slabel guard] in |
1096 | let false_branch = | |
1097 | make_seq guard | |
002099fc | 1098 | [falsepred None; |
978fd7e5 C |
1099 | quantify guard |
1100 | (Common.minus_set (Ast.get_fvs els) new_quantified) | |
002099fc | 1101 | (header_match None guard els); |
5427db06 | 1102 | recurse branch2 NotTop Tail new_quantified new_mquantified |
34e49164 | 1103 | (Some (lv,used)) llabel slabel guard] in |
002099fc | 1104 | let after_pred = aftpred None in |
34e49164 C |
1105 | let or_cases after_branch = |
1106 | ctl_or true_branch (ctl_or false_branch after_branch) in | |
1107 | let s = guard_to_strict guard in | |
1108 | let (if_header,wrapper) = | |
1109 | if !used | |
1110 | then | |
1111 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in | |
1112 | (ctl_and CTL.NONSTRICT(*???*) if_header label_pred, | |
1113 | (function body -> quantify true [lv] body)) | |
1114 | else (if_header,function x -> x) in | |
1115 | wrapper | |
1116 | (end_control_structure bothfvs if_header or_cases after_pred | |
002099fc C |
1117 | (Some(ctl_and s (ctl_ex (falsepred None)) (ctl_ex after_pred))) |
1118 | (Some(ctl_ex (falsepred None))) | |
34e49164 C |
1119 | aft after label guard) |
1120 | ||
1121 | let forwhile header body ((afvs,_,_,_) as aft) after | |
1122 | quantified minus_quantified label recurse make_match guard = | |
1123 | let process _ = | |
1124 | (* the translation in this case is similar to that of an if with no else *) | |
ae4735db | 1125 | (* free variables *) |
34e49164 C |
1126 | let (efvs,bfvs) = |
1127 | match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with | |
1128 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) | |
1129 | | _ -> failwith "not possible" in | |
1130 | let new_quantified = Common.union_set bfvs quantified in | |
ae4735db | 1131 | (* minus free variables *) |
34e49164 C |
1132 | let (mefvs,mbfvs) = |
1133 | match seq_fvs minus_quantified | |
1134 | [Ast.get_mfvs header;Ast.get_mfvs body;[]] with | |
1135 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) | |
1136 | | _ -> failwith "not possible" in | |
1137 | let new_mquantified = Common.union_set mbfvs minus_quantified in | |
1138 | (* loop header *) | |
1139 | let header = quantify guard efvs (make_match header) in | |
1140 | let lv = get_label_ctr() in | |
1141 | let used = ref false in | |
1142 | let body = | |
1143 | make_seq guard | |
002099fc | 1144 | [inlooppred None; |
5427db06 | 1145 | recurse body NotTop Tail new_quantified new_mquantified |
34e49164 | 1146 | (Some (lv,used)) (Some (lv,used)) None guard] in |
951c7801 | 1147 | let after_pred = loopfallpred None in |
34e49164 C |
1148 | let or_cases after_branch = ctl_or body after_branch in |
1149 | let (header,wrapper) = | |
1150 | if !used | |
1151 | then | |
1152 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in | |
1153 | (ctl_and CTL.NONSTRICT(*???*) header label_pred, | |
1154 | (function body -> quantify true [lv] body)) | |
1155 | else (header,function x -> x) in | |
1156 | wrapper | |
1157 | (end_control_structure bfvs header or_cases after_pred | |
1158 | (Some(ctl_ex after_pred)) None aft after label guard) in | |
1159 | match (Ast.unwrap body,aft) with | |
1160 | (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) -> | |
1161 | (match Ast.unwrap re with | |
1162 | Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_), | |
b1b2de81 C |
1163 | Type_cocci.Unitary,_,false) |
1164 | when after = Tail or after = End or after = VeryEnd -> | |
34e49164 C |
1165 | let (efvs) = |
1166 | match seq_fvs quantified [Ast.get_fvs header] with | |
1167 | [(efvs,_)] -> efvs | |
1168 | | _ -> failwith "not possible" in | |
1169 | quantify guard efvs (make_match header) | |
1170 | | _ -> process()) | |
1171 | | _ -> process() | |
ae4735db | 1172 | |
34e49164 C |
1173 | (* --------------------------------------------------------------------- *) |
1174 | (* statement metavariables *) | |
1175 | ||
1176 | (* issue: an S metavariable that is not an if branch/loop body | |
1177 | should not match an if branch/loop body, so check that the labels | |
1178 | of the nodes before the first node matched by the S are different | |
1179 | from the label of the first node matched by the S *) | |
1180 | let sequencibility body label_pred process_bef_aft = function | |
1181 | Ast.Sequencible | Ast.SequencibleAfterDots [] -> | |
1182 | body | |
1183 | (function x -> | |
1184 | (ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x)) | |
1185 | | Ast.SequencibleAfterDots l -> | |
1186 | (* S appears after some dots. l is the code that comes after the S. | |
1187 | want to search for that first, because S can match anything, while | |
1188 | the stuff after is probably more restricted *) | |
1189 | let afts = List.map process_bef_aft l in | |
1190 | let ors = foldl1 ctl_or afts in | |
1191 | ctl_and CTL.NONSTRICT | |
1192 | (ctl_ef (ctl_and CTL.NONSTRICT ors (ctl_back_ax label_pred))) | |
1193 | (body | |
1194 | (function x -> | |
1195 | ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x)) | |
1196 | | Ast.NotSequencible -> body (function x -> x) | |
1197 | ||
1198 | let svar_context_with_add_after stmt s label quantified d ast | |
1199 | seqible after process_bef_aft guard fvinfo = | |
1200 | let label_var = (*fresh_label_var*) string2var "_lab" in | |
1201 | let label_pred = | |
1202 | CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in | |
951c7801 C |
1203 | (*let prelabel_pred = |
1204 | CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*) | |
34e49164 C |
1205 | let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in |
1206 | let full_metamatch = matcher d in | |
1207 | let first_metamatch = | |
1208 | matcher | |
1209 | (match d with | |
951c7801 C |
1210 | Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_,c)) -> |
1211 | Ast.CONTEXT(pos,Ast.BEFORE(bef,c)) | |
34e49164 | 1212 | | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING) |
951c7801 C |
1213 | | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in |
1214 | (* | |
34e49164 C |
1215 | let middle_metamatch = |
1216 | matcher | |
1217 | (match d with | |
1218 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING) | |
951c7801 C |
1219 | | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in |
1220 | *) | |
34e49164 C |
1221 | let last_metamatch = |
1222 | matcher | |
1223 | (match d with | |
951c7801 C |
1224 | Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft,c)) -> |
1225 | Ast.CONTEXT(pos,Ast.AFTER(aft,c)) | |
34e49164 | 1226 | | Ast.CONTEXT(_,_) -> d |
951c7801 | 1227 | | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in |
34e49164 | 1228 | |
951c7801 | 1229 | (* |
34e49164 | 1230 | let rest_nodes = |
951c7801 C |
1231 | ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in |
1232 | *) | |
1233 | ||
1234 | let to_end = ctl_or (aftpred None) (loopfallpred None) in | |
34e49164 | 1235 | let left_or = (* the whole statement is one node *) |
951c7801 C |
1236 | make_seq_after guard |
1237 | (ctl_and CTL.NONSTRICT (ctl_not (ctl_ex to_end)) full_metamatch) after in | |
1238 | let right_or = (* the statement covers multiple nodes *) | |
ae4735db | 1239 | ctl_and CTL.NONSTRICT |
951c7801 C |
1240 | (ctl_ex |
1241 | (make_seq guard | |
1242 | [to_end; make_seq_after guard last_metamatch after])) | |
1243 | first_metamatch in | |
1244 | ||
1245 | (* | |
1246 | let left_or = | |
34e49164 C |
1247 | make_seq guard |
1248 | [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in | |
951c7801 | 1249 | let right_or = |
34e49164 C |
1250 | make_seq guard |
1251 | [first_metamatch; | |
1252 | ctl_au CTL.NONSTRICT | |
1253 | rest_nodes | |
1254 | (make_seq guard | |
1255 | [ctl_and CTL.NONSTRICT last_metamatch label_pred; | |
1256 | and_after guard | |
1257 | (ctl_not prelabel_pred) after])] in | |
951c7801 C |
1258 | *) |
1259 | ||
34e49164 C |
1260 | let body f = |
1261 | ctl_and CTL.NONSTRICT label_pred | |
1262 | (f (ctl_and CTL.NONSTRICT | |
1263 | (make_raw_match label false ast) (ctl_or left_or right_or))) in | |
1264 | let stmt_fvs = Ast.get_fvs stmt in | |
1265 | let fvs = get_unquantified quantified stmt_fvs in | |
1266 | quantify guard (label_var::fvs) | |
1267 | (sequencibility body label_pred process_bef_aft seqible) | |
1268 | ||
1269 | let svar_minus_or_no_add_after stmt s label quantified d ast | |
1270 | seqible after process_bef_aft guard fvinfo = | |
1271 | let label_var = (*fresh_label_var*) string2var "_lab" in | |
1272 | let label_pred = | |
1273 | CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in | |
1274 | let prelabel_pred = | |
1275 | CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in | |
1276 | let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in | |
fc1ad971 | 1277 | let ender = |
708f4980 | 1278 | match (d,after) with |
951c7801 C |
1279 | (Ast.PLUS _, _) -> failwith "not possible" |
1280 | | (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) -> | |
708f4980 | 1281 | (* just match the root. don't care about label; always ok *) |
951c7801 C |
1282 | make_raw_match None false ast |
1283 | | (Ast.CONTEXT(pos,Ast.BEFORE(_,_)),(Tail|End|VeryEnd)) -> | |
1284 | ctl_and CTL.NONSTRICT | |
1285 | (make_raw_match None false ast) (* statement *) | |
1286 | (matcher d) (* transformation *) | |
1287 | | (Ast.CONTEXT(pos,(Ast.NOTHING|Ast.BEFORE(_,_))),(After a | Guard a)) -> | |
1288 | (* This case and the MINUS one couldprobably be merged, if | |
1289 | HackForStmt were to notice when its arguments are trivial *) | |
34e49164 | 1290 | let first_metamatch = matcher d in |
951c7801 C |
1291 | (* try to follow after link *) |
1292 | let to_end = ctl_or (aftpred None) (loopfallpred None) in | |
1293 | let is_compound = | |
1294 | ctl_ex(make_seq guard [to_end; CTL.True; a]) in | |
1295 | let not_compound = | |
1296 | make_seq_after guard (ctl_not (ctl_ex to_end)) after in | |
fc1ad971 | 1297 | ctl_and CTL.NONSTRICT (make_raw_match label false ast) |
951c7801 C |
1298 | (ctl_and CTL.NONSTRICT |
1299 | first_metamatch (ctl_or is_compound not_compound)) | |
1300 | | (Ast.CONTEXT(pos,(Ast.AFTER _|Ast.BEFOREAFTER _)),_) -> | |
1301 | failwith "not possible" | |
1302 | | (Ast.MINUS(pos,inst,adj,l),after) -> | |
1303 | let (first_metamatch,last_metamatch,rest_metamatch) = | |
1304 | match l with | |
8babbc8f C |
1305 | Ast.NOREPLACEMENT -> |
1306 | (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d) | |
951c7801 | 1307 | | _ -> (matcher d, |
8babbc8f | 1308 | matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)), |
951c7801 C |
1309 | ctl_and CTL.NONSTRICT |
1310 | (ctl_not (make_raw_match label false ast)) | |
8babbc8f | 1311 | (matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)))) in |
951c7801 C |
1312 | (* try to follow after link *) |
1313 | let to_end = ctl_or (aftpred None) (loopfallpred None) in | |
1314 | let is_compound = | |
1315 | ctl_ex | |
1316 | (make_seq guard | |
1317 | [to_end; make_seq_after guard last_metamatch after]) in | |
1318 | let not_compound = | |
1319 | make_seq_after guard (ctl_not (ctl_ex to_end)) after in | |
1320 | ctl_and CTL.NONSTRICT | |
1321 | (ctl_and CTL.NONSTRICT (make_raw_match label false ast) | |
1322 | (ctl_and CTL.NONSTRICT | |
1323 | first_metamatch (ctl_or is_compound not_compound))) | |
1324 | (* don't have to put anything before the beginning, so don't have to | |
1325 | distinguish the first node. so don't have to bother about paths, | |
1326 | just use the label. label ensures that found nodes match up with | |
1327 | what they should because it is in the lhs of the andany. *) | |
1328 | (CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT, | |
1329 | ctl_and CTL.NONSTRICT label_pred | |
1330 | (make_raw_match label false ast), | |
993936c0 | 1331 | ctl_and CTL.NONSTRICT prelabel_pred rest_metamatch)) |
951c7801 | 1332 | in |
fc1ad971 C |
1333 | let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in |
1334 | let stmt_fvs = Ast.get_fvs stmt in | |
1335 | let fvs = get_unquantified quantified stmt_fvs in | |
1336 | quantify guard (label_var::fvs) | |
34e49164 C |
1337 | (sequencibility body label_pred process_bef_aft seqible) |
1338 | ||
1339 | (* --------------------------------------------------------------------- *) | |
1340 | (* dots and nests *) | |
1341 | ||
978fd7e5 | 1342 | let dots_au is_strict toend label s wrapcode n x seq_after y quantifier = |
34e49164 C |
1343 | let matchgoto = gotopred None in |
1344 | let matchbreak = | |
1345 | make_match None false | |
1346 | (wrapcode | |
1347 | (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in | |
1348 | let matchcontinue = | |
1349 | make_match None false | |
1350 | (wrapcode | |
1351 | (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in | |
7f339edd | 1352 | let op = if quantifier = !exists then ctl_au else ctl_anti_au in |
485bce71 | 1353 | let stop_early = |
1be43e12 | 1354 | if quantifier = Exists |
485bce71 | 1355 | then Common.Left(CTL.False) |
34e49164 | 1356 | else if toend |
485bce71 | 1357 | then Common.Left(CTL.Or(aftpred label,exitpred label)) |
34e49164 | 1358 | else if is_strict |
485bce71 | 1359 | then Common.Left(aftpred label) |
34e49164 | 1360 | else |
485bce71 | 1361 | Common.Right |
978fd7e5 C |
1362 | (function vx -> function v -> |
1363 | (* vx is the contents of the nest, if any. we can only stop early | |
1364 | if we find neither the ending code nor the nest contents in | |
1365 | the if branch. not sure if this is a good idea. *) | |
485bce71 C |
1366 | let lv = get_label_ctr() in |
1367 | let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in | |
1368 | let preflabelpred = label_pred_maker (Some (lv,ref true)) in | |
951c7801 | 1369 | (*let is_paren = |
fc1ad971 C |
1370 | (* Rather a special case. But if the code afterwards is just |
1371 | a } then there is no point checking after a goto that it does | |
1372 | not appear. *) | |
1373 | (* this optimization doesn't work. probably depends on whether | |
1374 | the destination of the break/goto is local or more global than | |
1375 | the dots *) | |
1376 | match seq_after with | |
1377 | CTL.And(_,e1,e2) -> | |
1378 | let is_paren = function | |
1379 | CTL.Pred(Lib_engine.Paren _,_) -> true | |
1380 | | _ -> false in | |
1381 | is_paren e1 or is_paren e2 | |
951c7801 | 1382 | | _ -> false in *) |
485bce71 C |
1383 | ctl_or (aftpred label) |
1384 | (quantify false [lv] | |
1385 | (ctl_and CTL.NONSTRICT | |
1386 | (ctl_and CTL.NONSTRICT (truepred label) labelpred) | |
7f339edd | 1387 | (op CTL.NONSTRICT |
978fd7e5 C |
1388 | (ctl_and CTL.NONSTRICT (ctl_not v) |
1389 | (ctl_and CTL.NONSTRICT vx preflabelpred)) | |
485bce71 | 1390 | (ctl_and CTL.NONSTRICT preflabelpred |
faf9a90c C |
1391 | (if !Flag_matcher.only_return_is_error_exit |
1392 | then | |
1393 | (ctl_and CTL.NONSTRICT | |
1394 | (retpred None) (ctl_not seq_after)) | |
1395 | else | |
1396 | (ctl_or | |
1397 | (ctl_and CTL.NONSTRICT | |
1398 | (ctl_or (retpred None) matchcontinue) | |
1399 | (ctl_not seq_after)) | |
1400 | (ctl_and CTL.NONSTRICT | |
1401 | (ctl_or matchgoto matchbreak) | |
fc1ad971 C |
1402 | ((*if is_paren |
1403 | (* an optim that failed see defn is_paren | |
1404 | and tests/makes_a_loop *) | |
1405 | then CTL.True | |
1406 | else*) | |
1407 | (ctl_ag s | |
1408 | (ctl_not seq_after))))))))))) in | |
485bce71 C |
1409 | let v = get_let_ctr() in |
1410 | op s x | |
1411 | (match stop_early with | |
755320b0 C |
1412 | Common.Left x1 -> ctl_or y x1 |
1413 | | Common.Right stop_early -> | |
978fd7e5 C |
1414 | CTL.Let(v,y, |
1415 | ctl_or (CTL.Ref v) | |
fc1ad971 C |
1416 | (ctl_and CTL.NONSTRICT (label_pred_maker label) |
1417 | (stop_early n (CTL.Ref v))))) | |
34e49164 C |
1418 | |
1419 | let rec dots_and_nests plus nest whencodes bef aft dotcode after label | |
1be43e12 | 1420 | process_bef_aft statement_list statement guard quantified wrapcode = |
34e49164 C |
1421 | let ctl_and_ns = ctl_and CTL.NONSTRICT in |
1422 | (* proces bef_aft *) | |
1423 | let shortest l = | |
1424 | List.fold_left ctl_or_fl CTL.False (List.map process_bef_aft l) in | |
1425 | let bef_aft = (* to be negated *) | |
1426 | try | |
1427 | let _ = | |
1428 | List.find | |
1429 | (function Ast.WhenModifier(Ast.WhenAny) -> true | _ -> false) | |
1430 | whencodes in | |
1431 | CTL.False | |
1432 | with Not_found -> shortest (Common.union_set bef aft) in | |
1433 | let is_strict = | |
1434 | List.exists | |
1435 | (function Ast.WhenModifier(Ast.WhenStrict) -> true | _ -> false) | |
1436 | whencodes in | |
1437 | let check_quantifier quant other = | |
1438 | if List.exists | |
1439 | (function Ast.WhenModifier(x) -> x = quant | _ -> false) | |
1440 | whencodes | |
1441 | then | |
1442 | if List.exists | |
1443 | (function Ast.WhenModifier(x) -> x = other | _ -> false) | |
1444 | whencodes | |
1445 | then failwith "inconsistent annotation on dots" | |
1446 | else true | |
1447 | else false in | |
1448 | let quantifier = | |
1449 | if check_quantifier Ast.WhenExists Ast.WhenForall | |
1450 | then Exists | |
1451 | else | |
1be43e12 | 1452 | if check_quantifier Ast.WhenForall Ast.WhenExists |
34e49164 C |
1453 | then Forall |
1454 | else !exists in | |
1455 | (* the following is used when we find a goto, etc and consider accepting | |
1456 | without finding the rest of the pattern *) | |
1457 | let aft = shortest aft in | |
1458 | (* process whencode *) | |
1459 | let labelled = label_pred_maker label in | |
1460 | let whencodes arg = | |
1461 | let (poswhen,negwhen) = | |
1462 | List.fold_left | |
1463 | (function (poswhen,negwhen) -> | |
1464 | function | |
1465 | Ast.WhenNot whencodes -> | |
1466 | (poswhen,ctl_or (statement_list whencodes) negwhen) | |
1467 | | Ast.WhenAlways stm -> | |
1468 | (ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen) | |
1be43e12 C |
1469 | | Ast.WhenModifier(_) -> (poswhen,negwhen) |
1470 | | Ast.WhenNotTrue(e) -> | |
1471 | (poswhen, | |
1472 | ctl_or (whencond_true e label guard quantified) negwhen) | |
1473 | | Ast.WhenNotFalse(e) -> | |
1474 | (poswhen, | |
1475 | ctl_or (whencond_false e label guard quantified) negwhen)) | |
978fd7e5 C |
1476 | (CTL.True,CTL.False(*bef_aft*)) (List.rev whencodes) in |
1477 | (*bef_aft modifies arg so that inside of a nest can't cause the next | |
1478 | to overshoot its boundaries, eg a() <...f()...> b() where f is | |
1479 | a metavariable and the whole thing matches code in a loop; | |
1480 | don't want f to match eg b(), allowing to go around the loop again*) | |
34e49164 C |
1481 | let poswhen = ctl_and_ns arg poswhen in |
1482 | let negwhen = | |
1483 | (* if !exists | |
1484 | then*) | |
1485 | (* add in After, because it's not part of the program *) | |
1486 | ctl_or (aftpred label) negwhen | |
1487 | (*else negwhen*) in | |
1488 | ctl_and_ns poswhen (ctl_not negwhen) in | |
1489 | (* process dot code, if any *) | |
1490 | let dotcode = | |
1491 | match (dotcode,guard) with | |
1492 | (None,_) | (_,true) -> CTL.True | |
1493 | | (Some dotcode,_) -> dotcode in | |
1494 | (* process nest code, if any *) | |
1495 | (* whencode goes in the negated part of the nest; if no nest, just goes | |
1496 | on the "true" in between code *) | |
1497 | let plus_var = if plus then get_label_ctr() else string2var "" in | |
1498 | let plus_var2 = if plus then get_label_ctr() else string2var "" in | |
978fd7e5 C |
1499 | let (ornest,just_nest) = |
1500 | (* just_nest is used when considering whether to stop early, to continue | |
1501 | to collect nest information in the if branch *) | |
34e49164 | 1502 | match (nest,guard && not plus) with |
978fd7e5 | 1503 | (None,_) | (_,true) -> (whencodes CTL.True,CTL.True) |
34e49164 C |
1504 | | (Some nest,false) -> |
1505 | let v = get_let_ctr() in | |
1506 | let is_plus x = | |
1507 | if plus | |
1508 | then | |
1509 | (* the idea is that BindGood is sort of a witness; a witness to | |
1510 | having found the subterm in at least one place. If there is | |
1511 | not a witness, then there is a risk that it will get thrown | |
1512 | away, if it is merged with a node that has an empty | |
1513 | environment. See tests/nestplus. But this all seems | |
1514 | rather suspicious *) | |
1515 | CTL.And(CTL.NONSTRICT,x, | |
1516 | CTL.Exists(true,plus_var2, | |
1517 | CTL.Pred(Lib_engine.BindGood(plus_var), | |
1518 | CTL.Modif plus_var2))) | |
1519 | else x in | |
ae4735db | 1520 | let body = |
978fd7e5 C |
1521 | CTL.Let(v,nest, |
1522 | CTL.Or(is_plus (CTL.Ref v), | |
1523 | whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in | |
1524 | (body,body) in | |
34e49164 C |
1525 | let plus_modifier x = |
1526 | if plus | |
1527 | then | |
1528 | CTL.Exists | |
1529 | (false,plus_var, | |
1530 | (CTL.And | |
1531 | (CTL.NONSTRICT,x, | |
1532 | CTL.Not(CTL.Pred(Lib_engine.BindBad(plus_var),CTL.Control))))) | |
1533 | else x in | |
1534 | ||
1535 | let ender = | |
1536 | match after with | |
fc1ad971 C |
1537 | (* label within dots is taken care of elsewhere. the next two lines |
1538 | put the label on the code following dots *) | |
1539 | After f -> ctl_and (guard_to_strict guard) f labelled | |
1540 | | Guard f -> | |
1541 | (* actually, label should be None based on the only use of Guard... *) | |
1542 | assert (label = None); | |
1543 | ctl_and CTL.NONSTRICT (ctl_uncheck f) labelled | |
34e49164 C |
1544 | | VeryEnd -> |
1545 | let exit = endpred label in | |
1546 | let errorexit = exitpred label in | |
1547 | ctl_or exit errorexit | |
1548 | (* not at all sure what the next two mean... *) | |
1549 | | End -> CTL.True | |
1550 | | Tail -> | |
1551 | (match label with | |
1552 | Some (lv,used) -> used := true; | |
1553 | ctl_or (CTL.Pred(Lib_engine.Label lv,CTL.Control)) | |
1554 | (ctl_back_ex (ctl_or (retpred label) (gotopred label))) | |
1555 | | None -> endpred label) | |
1556 | (* was the following, but not clear why sgrep should allow | |
1557 | incomplete patterns | |
1558 | let exit = endpred label in | |
1559 | let errorexit = exitpred label in | |
1560 | if !exists | |
1561 | then ctl_or exit errorexit (* end anywhere *) | |
1562 | else exit (* end at the real end of the function *) *) in | |
1563 | plus_modifier | |
1564 | (dots_au is_strict ((after = Tail) or (after = VeryEnd)) | |
978fd7e5 | 1565 | label (guard_to_strict guard) wrapcode just_nest |
5636bb2c C |
1566 | (ctl_and_ns dotcode |
1567 | (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest) labelled)) | |
1568 | aft ender quantifier) | |
34e49164 | 1569 | |
1be43e12 C |
1570 | and get_whencond_exps e = |
1571 | match Ast.unwrap e with | |
1572 | Ast.Exp e -> [e] | |
1573 | | Ast.DisjRuleElem(res) -> | |
1574 | List.fold_left Common.union_set [] (List.map get_whencond_exps res) | |
1575 | | _ -> failwith "not possible" | |
1576 | ||
1577 | and make_whencond_headers e e1 label guard quantified = | |
1578 | let fvs = Ast.get_fvs e in | |
1579 | let header_pred h = | |
1580 | quantify guard (get_unquantified quantified fvs) | |
1581 | (make_match label guard h) in | |
1582 | let if_header e1 = | |
1583 | header_pred | |
1584 | (Ast.rewrap e | |
1585 | (Ast.IfHeader | |
1586 | (Ast.make_mcode "if", | |
1587 | Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in | |
1588 | let while_header e1 = | |
1589 | header_pred | |
1590 | (Ast.rewrap e | |
1591 | (Ast.WhileHeader | |
1592 | (Ast.make_mcode "while", | |
1593 | Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in | |
1594 | let for_header e1 = | |
1595 | header_pred | |
1596 | (Ast.rewrap e | |
1597 | (Ast.ForHeader | |
755320b0 C |
1598 | (Ast.make_mcode "for",Ast.make_mcode "(", |
1599 | Ast.ForExp(None,Ast.make_mcode ";"), | |
1be43e12 C |
1600 | Some e1,Ast.make_mcode ";",None,Ast.make_mcode ")"))) in |
1601 | let if_headers = | |
1602 | List.fold_left ctl_or CTL.False (List.map if_header e1) in | |
1603 | let while_headers = | |
1604 | List.fold_left ctl_or CTL.False (List.map while_header e1) in | |
1605 | let for_headers = | |
1606 | List.fold_left ctl_or CTL.False (List.map for_header e1) in | |
1607 | (if_headers, while_headers, for_headers) | |
1608 | ||
1609 | and whencond_true e label guard quantified = | |
1610 | let e1 = get_whencond_exps e in | |
1611 | let (if_headers, while_headers, for_headers) = | |
1612 | make_whencond_headers e e1 label guard quantified in | |
1613 | ctl_or | |
1614 | (ctl_and CTL.NONSTRICT (truepred label) (ctl_back_ex if_headers)) | |
1615 | (ctl_and CTL.NONSTRICT | |
1616 | (inlooppred label) (ctl_back_ex (ctl_or while_headers for_headers))) | |
1617 | ||
1618 | and whencond_false e label guard quantified = | |
1619 | let e1 = get_whencond_exps e in | |
1620 | let (if_headers, while_headers, for_headers) = | |
1621 | make_whencond_headers e e1 label guard quantified in | |
88e71198 | 1622 | (* if with else *) |
1be43e12 | 1623 | ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers)) |
88e71198 C |
1624 | (* if without else *) |
1625 | (ctl_or (ctl_and CTL.NONSTRICT (fallpred label) (ctl_back_ex if_headers)) | |
1626 | (* failure of loop test *) | |
1627 | (ctl_and CTL.NONSTRICT (loopfallpred label) | |
1be43e12 C |
1628 | (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers)))) |
1629 | ||
34e49164 C |
1630 | (* --------------------------------------------------------------------- *) |
1631 | (* the main translation loop *) | |
ae4735db | 1632 | |
5427db06 | 1633 | let rec statement_list stmt_list top after quantified minus_quantified |
34e49164 C |
1634 | label llabel slabel dots_before guard = |
1635 | let isdots x = | |
1636 | (* include Disj to be on the safe side *) | |
1637 | match Ast.unwrap x with | |
1638 | Ast.Dots _ | Ast.Nest _ | Ast.Disj _ -> true | _ -> false in | |
1639 | let compute_label l e db = if db or isdots e then l else None in | |
1640 | match Ast.unwrap stmt_list with | |
1641 | Ast.DOTS(x) -> | |
5427db06 C |
1642 | let rec loop top quantified minus_quantified dots_before |
1643 | label llabel slabel | |
34e49164 C |
1644 | = function |
1645 | ([],_,_) -> (match after with After f -> f | _ -> CTL.True) | |
1646 | | ([e],_,_) -> | |
5427db06 | 1647 | statement e top after quantified minus_quantified |
34e49164 C |
1648 | (compute_label label e dots_before) |
1649 | llabel slabel guard | |
1650 | | (e::sl,fv::fvs,mfv::mfvs) -> | |
1651 | let shared = intersectll fv fvs in | |
1652 | let unqshared = get_unquantified quantified shared in | |
1653 | let new_quantified = Common.union_set unqshared quantified in | |
1654 | let minus_shared = intersectll mfv mfvs in | |
1655 | let munqshared = | |
1656 | get_unquantified minus_quantified minus_shared in | |
1657 | let new_mquantified = | |
1658 | Common.union_set munqshared minus_quantified in | |
1659 | quantify guard unqshared | |
5427db06 | 1660 | (statement e top |
34e49164 C |
1661 | (After |
1662 | (let (label1,llabel1,slabel1) = | |
1663 | match Ast.unwrap e with | |
1664 | Ast.Atomic(re) -> | |
1665 | (match Ast.unwrap re with | |
1666 | Ast.Goto _ -> (None,None,None) | |
1667 | | _ -> (label,llabel,slabel)) | |
1668 | | _ -> (label,llabel,slabel) in | |
5427db06 | 1669 | loop NotTop new_quantified new_mquantified (isdots e) |
34e49164 C |
1670 | label1 llabel1 slabel1 |
1671 | (sl,fvs,mfvs))) | |
1672 | new_quantified new_mquantified | |
1673 | (compute_label label e dots_before) llabel slabel guard) | |
1674 | | _ -> failwith "not possible" in | |
5427db06 | 1675 | loop top quantified minus_quantified dots_before |
34e49164 C |
1676 | label llabel slabel |
1677 | (x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x) | |
1678 | | Ast.CIRCLES(x) -> failwith "not supported" | |
1679 | | Ast.STARS(x) -> failwith "not supported" | |
1680 | ||
1681 | (* llabel is the label of the enclosing loop and slabel is the label of the | |
1682 | enclosing switch *) | |
5427db06 | 1683 | and statement stmt top after quantified minus_quantified |
34e49164 C |
1684 | label llabel slabel guard = |
1685 | let ctl_au = ctl_au CTL.NONSTRICT in | |
1686 | let ctl_ax = ctl_ax CTL.NONSTRICT in | |
1687 | let ctl_and = ctl_and CTL.NONSTRICT in | |
1688 | let make_seq = make_seq guard in | |
1689 | let make_seq_after = make_seq_after guard in | |
1690 | let real_make_match = make_match in | |
1691 | let make_match = header_match label guard in | |
1692 | ||
1693 | let dots_done = ref false in (* hack for dots cases we can easily handle *) | |
1694 | ||
1695 | let term = | |
1696 | match Ast.unwrap stmt with | |
1697 | Ast.Atomic(ast) -> | |
1698 | (match Ast.unwrap ast with | |
1699 | (* the following optimisation is not a good idea, because when S | |
1700 | is alone, we would like it not to match a declaration. | |
1701 | this makes more matching for things like when (...) S, but perhaps | |
1702 | that matching is not so costly anyway *) | |
1703 | (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*) | |
951c7801 | 1704 | | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_,_)) as d),_), |
34e49164 | 1705 | keep,seqible,_) |
951c7801 | 1706 | | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_,_)) as d),_), |
34e49164 C |
1707 | keep,seqible,_)-> |
1708 | svar_context_with_add_after stmt s label quantified d ast seqible | |
1709 | after | |
1710 | (process_bef_aft quantified minus_quantified | |
1711 | label llabel slabel true) | |
1712 | guard | |
1713 | (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt) | |
1714 | ||
1715 | | Ast.MetaStmt((s,_,d,_),keep,seqible,_) -> | |
1716 | svar_minus_or_no_add_after stmt s label quantified d ast seqible | |
1717 | after | |
1718 | (process_bef_aft quantified minus_quantified | |
1719 | label llabel slabel true) | |
1720 | guard | |
1721 | (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt) | |
1722 | ||
1723 | | _ -> | |
1724 | let term = | |
1725 | match Ast.unwrap ast with | |
1726 | Ast.DisjRuleElem(res) -> | |
1727 | do_re_matches label guard res quantified minus_quantified | |
1728 | | Ast.Exp(_) | Ast.Ty(_) -> | |
1729 | let stmt_fvs = Ast.get_fvs stmt in | |
1730 | let fvs = get_unquantified quantified stmt_fvs in | |
1731 | CTL.InnerAnd(quantify guard fvs (make_match ast)) | |
1732 | | _ -> | |
1733 | let stmt_fvs = Ast.get_fvs stmt in | |
1734 | let fvs = get_unquantified quantified stmt_fvs in | |
1735 | quantify guard fvs (make_match ast) in | |
1736 | match Ast.unwrap ast with | |
1737 | Ast.Break(brk,semi) -> | |
1738 | (match (llabel,slabel) with | |
1739 | (_,Some(lv,used)) -> (* use switch label if there is one *) | |
1740 | ctl_and term (bclabel_pred_maker slabel) | |
1741 | | _ -> ctl_and term (bclabel_pred_maker llabel)) | |
1742 | | Ast.Continue(brk,semi) -> ctl_and term (bclabel_pred_maker llabel) | |
1743 | | Ast.Return((_,info,retmc,pos),(_,_,semmc,_)) -> | |
1744 | (* discard pattern that comes after return *) | |
1745 | let normal_res = make_seq_after term after in | |
1746 | (* the following code tries to propagate the modifications on | |
1747 | return; to a close brace, in the case where the final return | |
1748 | is absent *) | |
1749 | let new_mc = | |
1750 | match (retmc,semmc) with | |
708f4980 C |
1751 | (Ast.MINUS(_,inst1,adj1,l1),Ast.MINUS(_,_,_,l2)) |
1752 | when !Flag.sgrep_mode2 -> | |
34e49164 | 1753 | (* in sgrep mode, we can propagate the - *) |
8babbc8f C |
1754 | let new_info = |
1755 | match (l1,l2) with | |
1756 | (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) -> | |
1757 | Ast.NOREPLACEMENT | |
1758 | | _ -> | |
1759 | failwith "no replacements allowed in sgrep mode" in | |
1760 | Some (Ast.MINUS(Ast.NoPos,inst1,adj1,new_info)) | |
951c7801 | 1761 | | (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) -> |
8babbc8f C |
1762 | let change = |
1763 | match (l1,l2) with | |
1764 | (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) -> | |
1765 | Ast.NOTHING | |
1766 | | (Ast.NOREPLACEMENT,Ast.REPLACEMENT(l,ct)) | |
1767 | | (Ast.REPLACEMENT(l,ct),Ast.NOREPLACEMENT) -> | |
1768 | Ast.BEFORE(l,ct) | |
1769 | | (Ast.REPLACEMENT(l1,ct1),Ast.REPLACEMENT(l2,ct2)) -> | |
1770 | Ast.BEFORE(l1@l2,Ast.lub_count ct1 ct2) in | |
1771 | Some (Ast.CONTEXT(Ast.NoPos,change)) | |
951c7801 C |
1772 | | (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)), |
1773 | Ast.CONTEXT(_,Ast.AFTER(l2,c2))) -> | |
8babbc8f C |
1774 | Some |
1775 | (Ast.CONTEXT(Ast.NoPos, | |
1776 | Ast.BEFORE(l1@l2,Ast.lub_count c1 c2))) | |
34e49164 C |
1777 | | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING)) |
1778 | | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) -> | |
1779 | Some retmc | |
708f4980 | 1780 | | (Ast.CONTEXT(_,Ast.NOTHING), |
951c7801 C |
1781 | Ast.CONTEXT(_,Ast.AFTER(l,c))) -> |
1782 | Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l,c))) | |
34e49164 C |
1783 | | _ -> None in |
1784 | let ret = Ast.make_mcode "return" in | |
1785 | let edots = | |
1786 | Ast.rewrap ast (Ast.Edots(Ast.make_mcode "...",None)) in | |
1787 | let semi = Ast.make_mcode ";" in | |
1788 | let simple_return = | |
1789 | make_match(Ast.rewrap ast (Ast.Return(ret,semi))) in | |
1790 | let return_expr = | |
1791 | make_match(Ast.rewrap ast (Ast.ReturnExpr(ret,edots,semi))) in | |
1792 | (match new_mc with | |
1793 | Some new_mc -> | |
1794 | let exit = endpred None in | |
1795 | let mod_rbrace = | |
1796 | Ast.rewrap ast (Ast.SeqEnd (("}",info,new_mc,pos))) in | |
1797 | let stripped_rbrace = | |
1798 | Ast.rewrap ast (Ast.SeqEnd(Ast.make_mcode "}")) in | |
1799 | ctl_or normal_res | |
1800 | (ctl_and (make_match mod_rbrace) | |
1801 | (ctl_and | |
34e49164 C |
1802 | (ctl_au |
1803 | (make_match stripped_rbrace) | |
1804 | (* error exit not possible; it is in the middle | |
1805 | of code, so a return is needed *) | |
993936c0 C |
1806 | exit) |
1807 | (* worry about perf, but seems correct, not ax *) | |
1808 | (ctl_back_ag | |
1809 | (ctl_not | |
1810 | (ctl_uncheck | |
1811 | (ctl_or simple_return return_expr)))))) | |
34e49164 C |
1812 | | _ -> |
1813 | (* some change in the middle of the return, so have to | |
1814 | find an actual return *) | |
1815 | normal_res) | |
1816 | | _ -> | |
1817 | (* should try to deal with the dots_bef_aft problem elsewhere, | |
1818 | but don't have the courage... *) | |
1819 | let term = | |
1820 | if guard | |
1821 | then term | |
1822 | else | |
1823 | do_between_dots stmt term End | |
1824 | quantified minus_quantified label llabel slabel guard in | |
1825 | dots_done := true; | |
1826 | make_seq_after term after) | |
708f4980 C |
1827 | | Ast.Seq(lbrace,body,rbrace) -> |
1828 | let (lbfvs,b1fvs,b2fvs,rbfvs) = | |
34e49164 C |
1829 | match |
1830 | seq_fvs quantified | |
d3f655c6 | 1831 | [Ast.get_fvs lbrace;Ast.get_fvs body;Ast.get_fvs rbrace] |
34e49164 | 1832 | with |
d3f655c6 | 1833 | [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> (lbfvs,b1fvs,b2fvs,rbfvs) |
34e49164 | 1834 | | _ -> failwith "not possible" in |
708f4980 | 1835 | let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) = |
34e49164 C |
1836 | match |
1837 | seq_fvs minus_quantified | |
d3f655c6 | 1838 | [Ast.get_mfvs lbrace;Ast.get_mfvs body;Ast.get_mfvs rbrace] |
34e49164 | 1839 | with |
708f4980 C |
1840 | [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> |
1841 | (lbfvs,b1fvs,b2fvs,rbfvs) | |
34e49164 C |
1842 | | _ -> failwith "not possible" in |
1843 | let pv = count_nested_braces stmt in | |
1844 | let lv = get_label_ctr() in | |
1845 | let paren_pred = CTL.Pred(Lib_engine.Paren pv,CTL.Control) in | |
1846 | let label_pred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in | |
1847 | let start_brace = | |
1848 | ctl_and | |
1849 | (quantify guard lbfvs (make_match lbrace)) | |
1850 | (ctl_and paren_pred label_pred) in | |
1be43e12 C |
1851 | let empty_rbrace = |
1852 | match Ast.unwrap rbrace with | |
1853 | Ast.SeqEnd((data,info,_,pos)) -> | |
1854 | Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data)) | |
1855 | | _ -> failwith "unexpected close brace" in | |
34e49164 C |
1856 | let end_brace = |
1857 | (* label is not needed; paren_pred is enough *) | |
1be43e12 C |
1858 | quantify guard rbfvs |
1859 | (ctl_au (make_match empty_rbrace) | |
d3f655c6 | 1860 | (ctl_and (real_make_match None guard rbrace) paren_pred)) in |
34e49164 C |
1861 | let new_quantified2 = |
1862 | Common.union_set b1fvs (Common.union_set b2fvs quantified) in | |
34e49164 C |
1863 | let new_mquantified2 = |
1864 | Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in | |
34e49164 C |
1865 | let pattern_as_given = |
1866 | let new_quantified2 = Common.union_set [pv] new_quantified2 in | |
34e49164 C |
1867 | quantify true [pv;lv] |
1868 | (quantify guard b1fvs | |
1869 | (make_seq | |
1870 | [start_brace; | |
951c7801 C |
1871 | (ctl_or |
1872 | (if !exists = Exists then CTL.False else (aftpred label)) | |
1873 | (quantify guard b2fvs | |
5427db06 | 1874 | (statement_list body NotTop |
951c7801 C |
1875 | (After (make_seq_after end_brace after)) |
1876 | new_quantified2 new_mquantified2 | |
1877 | (Some (lv,ref true)) | |
1878 | llabel slabel false guard)))])) in | |
d3f655c6 C |
1879 | let empty_body = |
1880 | match Ast.undots body with | |
1881 | [body] -> | |
1882 | (match Ast.unwrap body with | |
1883 | Ast.Dots | |
1884 | ((_,i,Ast.CONTEXT(_,Ast.NOTHING),_),[],_,_) -> | |
1885 | (match Ast.unwrap rbrace with | |
1886 | Ast.SeqEnd((_,_,Ast.CONTEXT(_,Ast.NOTHING),_)) | |
1887 | when not (contains_pos rbrace) -> true | |
1888 | | _ -> false) | |
1889 | | _ -> false) | |
1890 | | _ -> false in | |
993936c0 | 1891 | if empty_body && List.mem after [Tail;End;VeryEnd] |
d3f655c6 C |
1892 | (* for just a match of an if branch of the form { ... }, just |
1893 | match the first brace *) | |
1894 | then quantify guard lbfvs (make_match lbrace) | |
1895 | else if ends_in_return body | |
34e49164 C |
1896 | then |
1897 | (* matching error handling code *) | |
1898 | (* Cases: | |
1899 | 1. The pattern as given | |
1900 | 2. A goto, and then some close braces, and then the pattern as | |
1901 | given, but without the braces (only possible if there are no | |
1902 | decls, and open and close braces are unmodified) | |
1903 | 3. Part of the pattern as given, then a goto, and then the rest | |
1904 | of the pattern. For this case, we just check that all paths have | |
1905 | a goto within the current braces. checking for a goto at every | |
1906 | point in the pattern seems expensive and not worthwhile. *) | |
1907 | let pattern2 = | |
34e49164 C |
1908 | let body = preprocess_dots body in (* redo, to drop braces *) |
1909 | make_seq | |
1910 | [gotopred label; | |
1911 | ctl_au | |
1912 | (make_match empty_rbrace) | |
1913 | (ctl_ax (* skip the destination label *) | |
708f4980 | 1914 | (quantify guard b2fvs |
5427db06 | 1915 | (statement_list body NotTop End |
708f4980 | 1916 | new_quantified2 new_mquantified2 None llabel slabel |
34e49164 C |
1917 | true guard)))] in |
1918 | let pattern3 = | |
1919 | let new_quantified2 = Common.union_set [pv] new_quantified2 in | |
34e49164 C |
1920 | quantify true [pv;lv] |
1921 | (quantify guard b1fvs | |
1922 | (make_seq | |
1923 | [start_brace; | |
1924 | ctl_and | |
1925 | (CTL.AU (* want AF even for sgrep *) | |
1926 | (CTL.FORWARD,CTL.STRICT, | |
1927 | CTL.Pred(Lib_engine.PrefixLabel(lv),CTL.Control), | |
1928 | ctl_and (* brace must be eventually after goto *) | |
1929 | (gotopred (Some (lv,ref true))) | |
1930 | (* want AF even for sgrep *) | |
1931 | (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace)))) | |
1932 | (quantify guard b2fvs | |
5427db06 | 1933 | (statement_list body NotTop Tail |
34e49164 | 1934 | new_quantified2 new_mquantified2 |
978fd7e5 | 1935 | None(*no label because past the goto*) |
34e49164 | 1936 | llabel slabel false guard))])) in |
708f4980 | 1937 | ctl_or pattern_as_given (ctl_or pattern2 pattern3) |
34e49164 C |
1938 | else pattern_as_given |
1939 | | Ast.IfThen(ifheader,branch,aft) -> | |
1940 | ifthen ifheader branch aft after quantified minus_quantified | |
1941 | label llabel slabel statement make_match guard | |
ae4735db | 1942 | |
34e49164 C |
1943 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> |
1944 | ifthenelse ifheader branch1 els branch2 aft after quantified | |
1945 | minus_quantified label llabel slabel statement make_match guard | |
1946 | ||
1947 | | Ast.While(header,body,aft) | Ast.For(header,body,aft) | |
1948 | | Ast.Iterator(header,body,aft) -> | |
1949 | forwhile header body aft after quantified minus_quantified | |
1950 | label statement make_match guard | |
1951 | ||
1952 | | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *) | |
002099fc C |
1953 | (*ctl_and seems pointless, disjuncts see label too |
1954 | (label_pred_maker label)*) | |
5427db06 C |
1955 | let subformulas = |
1956 | List.map | |
1957 | (function sl -> | |
1958 | statement_list sl top after quantified minus_quantified label | |
1959 | llabel slabel true guard) | |
1960 | stmt_dots_list in | |
1961 | let safe_subformulas = | |
1962 | match top with | |
1963 | Top -> List.map2 protect_top_level stmt_dots_list subformulas | |
1964 | | NotTop -> subformulas in | |
1965 | List.fold_left ctl_seqor CTL.False safe_subformulas | |
34e49164 | 1966 | |
5636bb2c | 1967 | | Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) -> |
34e49164 | 1968 | (* label in recursive call is None because label check is already |
c491d8ee C |
1969 | wrapped around the corresponding code. not good enough, want to stay |
1970 | in a specific region, dots and nests will keep going *) | |
34e49164 C |
1971 | |
1972 | let bfvs = | |
1973 | match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots] | |
1974 | with | |
1975 | [(wcfvs,bothfvs);(bdfvs,_)] -> bothfvs | |
1976 | | _ -> failwith "not possible" in | |
1977 | ||
1978 | (* no minus version because when code doesn't contain any minus code *) | |
1979 | let new_quantified = Common.union_set bfvs quantified in | |
1980 | ||
5636bb2c C |
1981 | let dot_code = |
1982 | match Ast.get_mcodekind starter with (*ender must have the same mcode*) | |
1983 | Ast.MINUS(_,_,_,_) as d -> | |
1984 | (* no need for the fresh metavar, but ... is a bit weird as a | |
1985 | variable name *) | |
1986 | Some(make_match (make_meta_rule_elem d ([],[],[]))) | |
1987 | | _ -> None in | |
1988 | ||
34e49164 C |
1989 | quantify guard bfvs |
1990 | (let dots_pattern = | |
5427db06 C |
1991 | statement_list stmt_dots top (a2n after) |
1992 | new_quantified minus_quantified | |
c491d8ee | 1993 | label(*None*) llabel slabel true guard in |
34e49164 | 1994 | dots_and_nests multi |
5636bb2c | 1995 | (Some dots_pattern) whencode bef aft dot_code after label |
34e49164 | 1996 | (process_bef_aft new_quantified minus_quantified |
c491d8ee | 1997 | label(*None*) llabel slabel true) |
5427db06 C |
1998 | (function x -> (* for when code *) |
1999 | statement_list x NotTop Tail | |
2000 | new_quantified minus_quantified label(*None*) | |
34e49164 | 2001 | llabel slabel true true) |
5427db06 C |
2002 | (function x -> (* for when code *) |
2003 | statement x NotTop Tail | |
2004 | new_quantified minus_quantified label(*None*) | |
34e49164 | 2005 | llabel slabel true) |
1be43e12 C |
2006 | guard quantified |
2007 | (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))) | |
34e49164 C |
2008 | |
2009 | | Ast.Dots((_,i,d,_),whencodes,bef,aft) -> | |
2010 | let dot_code = | |
2011 | match d with | |
708f4980 | 2012 | Ast.MINUS(_,_,_,_) -> |
0708f913 | 2013 | (* no need for the fresh metavar, but ... is a bit weird as a |
34e49164 C |
2014 | variable name *) |
2015 | Some(make_match (make_meta_rule_elem d ([],[],[]))) | |
2016 | | _ -> None in | |
2017 | dots_and_nests false None whencodes bef aft dot_code after label | |
2018 | (process_bef_aft quantified minus_quantified None llabel slabel true) | |
2019 | (function x -> | |
5427db06 | 2020 | statement_list x NotTop Tail quantified minus_quantified |
34e49164 C |
2021 | None llabel slabel true true) |
2022 | (function x -> | |
5427db06 C |
2023 | statement x NotTop Tail quantified minus_quantified |
2024 | None llabel slabel true) | |
1be43e12 C |
2025 | guard quantified |
2026 | (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)) | |
34e49164 | 2027 | |
fc1ad971 | 2028 | | Ast.Switch(header,lb,decls,cases,rb) -> |
34e49164 C |
2029 | let rec intersect_all = function |
2030 | [] -> [] | |
2031 | | [x] -> x | |
2032 | | x::xs -> intersect x (intersect_all xs) in | |
fc1ad971 C |
2033 | let rec intersect_all2 = function (* pairwise *) |
2034 | [] -> [] | |
2035 | | x::xs -> | |
2036 | let front = | |
2037 | List.filter | |
2038 | (function elem -> List.exists (List.mem elem) xs) | |
2039 | x in | |
2040 | Common.union_set front (intersect_all2 xs) in | |
34e49164 C |
2041 | let rec union_all l = List.fold_left union [] l in |
2042 | (* start normal variables *) | |
2043 | let header_fvs = Ast.get_fvs header in | |
2044 | let lb_fvs = Ast.get_fvs lb in | |
fc1ad971 | 2045 | let decl_fvs = union_all (List.map Ast.get_fvs (Ast.undots decls)) in |
34e49164 C |
2046 | let case_fvs = List.map Ast.get_fvs cases in |
2047 | let rb_fvs = Ast.get_fvs rb in | |
2048 | let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, | |
2049 | all_casefvs,all_b3fvs,all_rbfvs) = | |
2050 | List.fold_left | |
2051 | (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, | |
2052 | all_casefvs,all_b3fvs,all_rbfvs) -> | |
2053 | function case_fvs -> | |
2054 | match seq_fvs quantified [header_fvs;lb_fvs;case_fvs;rb_fvs] with | |
2055 | [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] -> | |
2056 | (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs, | |
2057 | b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs, | |
2058 | rbfvs::all_rbfvs) | |
2059 | | _ -> failwith "not possible") | |
fc1ad971 | 2060 | ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in |
34e49164 C |
2061 | let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, |
2062 | all_casefvs,all_b3fvs,all_rbfvs) = | |
2063 | (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs, | |
2064 | List.rev all_b2fvs,List.rev all_casefvs,List.rev all_b3fvs, | |
2065 | List.rev all_rbfvs) in | |
2066 | let exponlyfvs = intersect_all all_efvs in | |
2067 | let lbonlyfvs = intersect_all all_lbfvs in | |
2068 | (* don't do anything with right brace. Hope there is no + code on it *) | |
2069 | (* let rbonlyfvs = intersect_all all_rbfvs in*) | |
2070 | let b1fvs = union_all all_b1fvs in | |
2071 | let new1_quantified = union b1fvs quantified in | |
fc1ad971 C |
2072 | let b2fvs = |
2073 | union (union_all all_b2fvs) (intersect_all2 all_casefvs) in | |
34e49164 C |
2074 | let new2_quantified = union b2fvs new1_quantified in |
2075 | (* let b3fvs = union_all all_b3fvs in*) | |
2076 | (* ------------------- start minus free variables *) | |
2077 | let header_mfvs = Ast.get_mfvs header in | |
2078 | let lb_mfvs = Ast.get_mfvs lb in | |
fc1ad971 | 2079 | let decl_mfvs = union_all (List.map Ast.get_mfvs (Ast.undots decls)) in |
34e49164 C |
2080 | let case_mfvs = List.map Ast.get_mfvs cases in |
2081 | let rb_mfvs = Ast.get_mfvs rb in | |
2082 | let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs, | |
2083 | all_mcasefvs,all_mb3fvs,all_mrbfvs) = | |
2084 | List.fold_left | |
2085 | (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, | |
2086 | all_casefvs,all_b3fvs,all_rbfvs) -> | |
2087 | function case_mfvs -> | |
2088 | match | |
2089 | seq_fvs quantified | |
2090 | [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with | |
2091 | [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] -> | |
2092 | (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs, | |
2093 | b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs, | |
2094 | rbfvs::all_rbfvs) | |
2095 | | _ -> failwith "not possible") | |
fc1ad971 | 2096 | ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in |
34e49164 C |
2097 | let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs, |
2098 | all_mcasefvs,all_mb3fvs,all_mrbfvs) = | |
2099 | (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs, | |
2100 | List.rev all_mb2fvs,List.rev all_mcasefvs,List.rev all_mb3fvs, | |
2101 | List.rev all_mrbfvs) in | |
2102 | (* don't do anything with right brace. Hope there is no + code on it *) | |
2103 | (* let rbonlyfvs = intersect_all all_rbfvs in*) | |
2104 | let mb1fvs = union_all all_mb1fvs in | |
2105 | let new1_mquantified = union mb1fvs quantified in | |
fc1ad971 C |
2106 | let mb2fvs = |
2107 | union (union_all all_mb2fvs) (intersect_all2 all_mcasefvs) in | |
34e49164 C |
2108 | let new2_mquantified = union mb2fvs new1_mquantified in |
2109 | (* let b3fvs = union_all all_b3fvs in*) | |
2110 | (* ------------------- end collection of free variables *) | |
2111 | let switch_header = quantify guard exponlyfvs (make_match header) in | |
2112 | let lb = quantify guard lbonlyfvs (make_match lb) in | |
2113 | (* let rb = quantify guard rbonlyfvs (make_match rb) in*) | |
2114 | let case_headers = | |
2115 | List.map | |
2116 | (function case_line -> | |
2117 | match Ast.unwrap case_line with | |
2118 | Ast.CaseLine(header,body) -> | |
2119 | let e1fvs = | |
2120 | match seq_fvs new2_quantified [Ast.get_fvs header] with | |
2121 | [(e1fvs,_)] -> e1fvs | |
2122 | | _ -> failwith "not possible" in | |
2123 | quantify guard e1fvs (real_make_match label true header) | |
2124 | | Ast.OptCase(case_line) -> failwith "not supported") | |
2125 | cases in | |
34e49164 C |
2126 | let lv = get_label_ctr() in |
2127 | let used = ref false in | |
fc1ad971 C |
2128 | let (decls_exists_code,decls_all_code) = |
2129 | (*don't really understand this*) | |
2130 | if (Ast.undots decls) = [] | |
2131 | then (CTL.True,CTL.False) | |
2132 | else | |
2133 | let res = | |
5427db06 | 2134 | statement_list decls NotTop Tail |
fc1ad971 C |
2135 | new2_quantified new2_mquantified (Some (lv,used)) llabel None |
2136 | false(*?*) guard in | |
2137 | (res,res) in | |
2138 | let no_header = | |
2139 | ctl_not | |
2140 | (List.fold_left ctl_or_fl CTL.False | |
951c7801 C |
2141 | (List.map ctl_uncheck |
2142 | (decls_all_code::case_headers))) in | |
34e49164 C |
2143 | let case_code = |
2144 | List.map | |
2145 | (function case_line -> | |
2146 | match Ast.unwrap case_line with | |
2147 | Ast.CaseLine(header,body) -> | |
2148 | let (e1fvs,b1fvs,s1fvs) = | |
2149 | let fvs = [Ast.get_fvs header;Ast.get_fvs body] in | |
2150 | match seq_fvs new2_quantified fvs with | |
2151 | [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs) | |
2152 | | _ -> failwith "not possible" in | |
2153 | let (me1fvs,mb1fvs,ms1fvs) = | |
2154 | let fvs = [Ast.get_mfvs header;Ast.get_mfvs body] in | |
2155 | match seq_fvs new2_mquantified fvs with | |
2156 | [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs) | |
2157 | | _ -> failwith "not possible" in | |
2158 | let case_header = | |
2159 | quantify guard e1fvs (make_match header) in | |
2160 | let new3_quantified = union b1fvs new2_quantified in | |
2161 | let new3_mquantified = union mb1fvs new2_mquantified in | |
2162 | let body = | |
5427db06 | 2163 | statement_list body NotTop Tail |
fc1ad971 C |
2164 | new3_quantified new3_mquantified (Some (lv,used)) llabel |
2165 | (Some (lv,used)) false(*?*) guard in | |
34e49164 C |
2166 | quantify guard b1fvs (make_seq [case_header; body]) |
2167 | | Ast.OptCase(case_line) -> failwith "not supported") | |
2168 | cases in | |
2169 | let default_required = | |
2170 | if List.exists | |
2171 | (function case -> | |
2172 | match Ast.unwrap case with | |
2173 | Ast.CaseLine(header,_) -> | |
2174 | (match Ast.unwrap header with | |
2175 | Ast.Default(_,_) -> true | |
2176 | | _ -> false) | |
2177 | | _ -> false) | |
2178 | cases | |
2179 | then function x -> x | |
2180 | else function x -> ctl_or (fallpred label) x in | |
2181 | let after_pred = aftpred label in | |
2182 | let body after_branch = | |
2183 | ctl_or | |
2184 | (default_required | |
2185 | (quantify guard b2fvs | |
2186 | (make_seq | |
2187 | [ctl_and lb | |
2188 | (List.fold_left ctl_and CTL.True | |
fc1ad971 C |
2189 | (List.map ctl_ex |
2190 | (decls_exists_code :: case_headers))); | |
2191 | List.fold_left ctl_or_fl no_header | |
2192 | (decls_all_code :: case_code)]))) | |
34e49164 C |
2193 | after_branch in |
2194 | let aft = | |
2195 | (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb, | |
2196 | match Ast.unwrap rb with | |
2197 | Ast.SeqEnd(rb) -> Ast.get_mcodekind rb | |
2198 | | _ -> failwith "not possible") in | |
2199 | let (switch_header,wrapper) = | |
2200 | if !used | |
2201 | then | |
2202 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in | |
2203 | (ctl_and switch_header label_pred, | |
2204 | (function body -> quantify true [lv] body)) | |
2205 | else (switch_header,function x -> x) in | |
2206 | wrapper | |
2207 | (end_control_structure b1fvs switch_header body | |
2208 | after_pred (Some(ctl_ex after_pred)) None aft after label guard) | |
708f4980 C |
2209 | | Ast.FunDecl(header,lbrace,body,rbrace) -> |
2210 | let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) = | |
34e49164 C |
2211 | match |
2212 | seq_fvs quantified | |
708f4980 | 2213 | [Ast.get_fvs header;Ast.get_fvs lbrace; |
34e49164 C |
2214 | Ast.get_fvs body;Ast.get_fvs rbrace] |
2215 | with | |
708f4980 C |
2216 | [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] -> |
2217 | (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) | |
34e49164 | 2218 | | _ -> failwith "not possible" in |
708f4980 | 2219 | let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mrbfvs) = |
34e49164 C |
2220 | match |
2221 | seq_fvs quantified | |
708f4980 | 2222 | [Ast.get_mfvs header;Ast.get_mfvs lbrace; |
34e49164 C |
2223 | Ast.get_mfvs body;Ast.get_mfvs rbrace] |
2224 | with | |
708f4980 C |
2225 | [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] -> |
2226 | (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) | |
34e49164 C |
2227 | | _ -> failwith "not possible" in |
2228 | let function_header = quantify guard hfvs (make_match header) in | |
2229 | let start_brace = quantify guard lbfvs (make_match lbrace) in | |
2230 | let stripped_rbrace = | |
2231 | match Ast.unwrap rbrace with | |
2232 | Ast.SeqEnd((data,info,_,_)) -> | |
2233 | Ast.rewrap rbrace(Ast.SeqEnd (Ast.make_mcode data)) | |
2234 | | _ -> failwith "unexpected close brace" in | |
2235 | let end_brace = | |
2236 | let exit = CTL.Pred (Lib_engine.Exit,CTL.Control) in | |
2237 | let errorexit = CTL.Pred (Lib_engine.ErrorExit,CTL.Control) in | |
2238 | let fake_brace = CTL.Pred (Lib_engine.FakeBrace,CTL.Control) in | |
2239 | ctl_and | |
2240 | (quantify guard rbfvs (make_match rbrace)) | |
2241 | (ctl_and | |
2242 | (* the following finds the beginning of the fake braces, | |
2243 | if there are any, not completely sure how this works. | |
2244 | sse the examples sw and return *) | |
2245 | (ctl_back_ex (ctl_not fake_brace)) | |
2246 | (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in | |
2247 | let new_quantified3 = | |
2248 | Common.union_set b1fvs | |
2249 | (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in | |
34e49164 C |
2250 | let new_mquantified3 = |
2251 | Common.union_set mb1fvs | |
2252 | (Common.union_set mb2fvs | |
2253 | (Common.union_set mb3fvs minus_quantified)) in | |
5636bb2c | 2254 | let not_minus = function Ast.MINUS(_,_,_,_) -> false | _ -> true in |
978fd7e5 | 2255 | let optim1 = |
708f4980 | 2256 | match (Ast.undots body, |
91eba41f | 2257 | contains_modif rbrace or contains_pos rbrace) with |
708f4980 | 2258 | ([body],false) -> |
34e49164 | 2259 | (match Ast.unwrap body with |
5636bb2c C |
2260 | Ast.Nest(starter,stmt_dots,ender,[],false,_,_) |
2261 | (* perhaps could optimize for minus case too... TODO *) | |
2262 | when not_minus (Ast.get_mcodekind starter) | |
2263 | -> | |
978fd7e5 C |
2264 | (* special case for function header + body - header is unambiguous |
2265 | and unique, so we can just look for the nested body anywhere | |
2266 | else in the CFG *) | |
2267 | Some | |
2268 | (CTL.AndAny | |
2269 | (CTL.FORWARD,guard_to_strict guard,start_brace, | |
5427db06 | 2270 | statement_list stmt_dots NotTop |
978fd7e5 C |
2271 | (* discards match on right brace, but don't need it *) |
2272 | (Guard (make_seq_after end_brace after)) | |
2273 | new_quantified3 new_mquantified3 | |
2274 | None llabel slabel true guard)) | |
2275 | | Ast.Dots((_,i,d,_),whencode,_,_) when | |
1be43e12 C |
2276 | (List.for_all |
2277 | (* flow sensitive, so not optimizable *) | |
2278 | (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) -> | |
2279 | false | |
2280 | | _ -> true) whencode) -> | |
978fd7e5 C |
2281 | (* try to be more efficient for the case where the body is just |
2282 | ... Perhaps this is too much of a special case, but useful | |
2283 | for dropping a parameter and checking that it is never used. *) | |
2284 | (match d with | |
2285 | Ast.MINUS(_,_,_,_) -> None | |
2286 | | _ -> | |
18b1275a C |
2287 | let pv = |
2288 | (* no nested braces, because only dots *) | |
2289 | string2var ("p1") in | |
2290 | let paren_pred = | |
2291 | CTL.Pred(Lib_engine.Paren pv,CTL.Control) in | |
978fd7e5 C |
2292 | Some ( |
2293 | make_seq | |
18b1275a | 2294 | [ctl_and start_brace paren_pred; |
978fd7e5 C |
2295 | match whencode with |
2296 | [] -> CTL.True | |
2297 | | _ -> | |
2298 | let leftarg = | |
2299 | ctl_and | |
2300 | (ctl_not | |
2301 | (List.fold_left | |
2302 | (function prev -> | |
2303 | function | |
2304 | Ast.WhenAlways(s) -> prev | |
2305 | | Ast.WhenNot(sl) -> | |
2306 | let x = | |
5427db06 C |
2307 | statement_list sl |
2308 | NotTop Tail | |
978fd7e5 C |
2309 | new_quantified3 |
2310 | new_mquantified3 | |
2311 | label llabel slabel | |
2312 | true true in | |
2313 | ctl_or prev x | |
2314 | | Ast.WhenNotTrue(_) | |
2315 | | Ast.WhenNotFalse(_) -> | |
2316 | failwith "unexpected" | |
2317 | | Ast.WhenModifier | |
2318 | (Ast.WhenAny) -> CTL.False | |
2319 | | Ast.WhenModifier(_) -> prev) | |
2320 | CTL.False whencode)) | |
2321 | (List.fold_left | |
2322 | (function prev -> | |
2323 | function | |
2324 | Ast.WhenAlways(s) -> | |
2325 | let x = | |
5427db06 | 2326 | statement s NotTop Tail |
978fd7e5 C |
2327 | new_quantified3 |
2328 | new_mquantified3 | |
2329 | label llabel slabel true in | |
2330 | ctl_and prev x | |
2331 | | Ast.WhenNot(sl) -> prev | |
2332 | | Ast.WhenNotTrue(_) | |
2333 | | Ast.WhenNotFalse(_) -> | |
2334 | failwith "unexpected" | |
2335 | | Ast.WhenModifier(Ast.WhenAny) -> | |
2336 | CTL.True | |
2337 | | Ast.WhenModifier(_) -> prev) | |
2338 | CTL.True whencode) in | |
18b1275a C |
2339 | ctl_au leftarg |
2340 | (ctl_and | |
2341 | (make_match stripped_rbrace) | |
2342 | paren_pred)])) | |
978fd7e5 C |
2343 | | _ -> None) |
2344 | | _ -> None in | |
2345 | let optim2 = | |
2346 | (* function body is all minus, no whencode *) | |
2347 | match Ast.undots body with | |
2348 | [body] -> | |
ae4735db | 2349 | (match Ast.unwrap body with |
978fd7e5 | 2350 | Ast.Dots |
8babbc8f | 2351 | ((_,i,(Ast.MINUS(_,_,_,Ast.NOREPLACEMENT) as d),_),[],_,_) -> |
978fd7e5 | 2352 | (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with |
8babbc8f C |
2353 | (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)), |
2354 | Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_))) | |
978fd7e5 C |
2355 | when not (contains_pos rbrace) -> |
2356 | Some | |
2357 | (* andany drops everything to the end, including close | |
2358 | braces - not just function body, could check | |
2359 | label to keep braces *) | |
2360 | (ctl_and start_brace | |
2361 | (ctl_ax | |
2362 | (CTL.AndAny | |
2363 | (CTL.FORWARD,guard_to_strict guard,CTL.True, | |
2364 | make_match | |
2365 | (make_meta_rule_elem d ([],[],[])))))) | |
2366 | | _ -> None) | |
34e49164 C |
2367 | | _ -> None) |
2368 | | _ -> None in | |
2369 | let body_code = | |
978fd7e5 C |
2370 | match (optim1,optim2) with |
2371 | (Some o1,_) -> o1 | |
2372 | | (_,Some o2) -> o2 | |
2373 | | _ -> | |
34e49164 C |
2374 | make_seq |
2375 | [start_brace; | |
2376 | quantify guard b3fvs | |
5427db06 | 2377 | (statement_list body NotTop |
708f4980 | 2378 | (After (make_seq_after end_brace after)) |
34e49164 C |
2379 | new_quantified3 new_mquantified3 None llabel slabel |
2380 | false guard)] in | |
2381 | quantify guard b1fvs | |
2382 | (make_seq [function_header; quantify guard b2fvs body_code]) | |
2383 | | Ast.Define(header,body) -> | |
2384 | let (hfvs,bfvs,bodyfvs) = | |
2385 | match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body] | |
2386 | with | |
2387 | [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs) | |
2388 | | _ -> failwith "not possible" in | |
2389 | let (mhfvs,mbfvs,mbodyfvs) = | |
2390 | match seq_fvs minus_quantified [Ast.get_mfvs header;Ast.get_mfvs body] | |
2391 | with | |
2392 | [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs) | |
2393 | | _ -> failwith "not possible" in | |
2394 | let define_header = quantify guard hfvs (make_match header) in | |
2395 | let body_code = | |
5427db06 | 2396 | statement_list body NotTop after |
34e49164 C |
2397 | (Common.union_set bfvs quantified) |
2398 | (Common.union_set mbfvs minus_quantified) | |
2399 | None llabel slabel true guard in | |
2400 | quantify guard bfvs (make_seq [define_header; body_code]) | |
17ba0788 C |
2401 | | Ast.AsStmt(stmt,asstmt) -> |
2402 | ctl_and | |
2403 | (statement stmt top after quantified minus_quantified | |
2404 | label llabel slabel guard) | |
2405 | (statement asstmt top after quantified minus_quantified | |
2406 | label llabel slabel guard) | |
34e49164 C |
2407 | | Ast.OptStm(stm) -> |
2408 | failwith "OptStm should have been compiled away\n" | |
2409 | | Ast.UniqueStm(stm) -> failwith "arities not yet supported" | |
2410 | | _ -> failwith "not supported" in | |
2411 | if guard or !dots_done | |
2412 | then term | |
2413 | else | |
2414 | do_between_dots stmt term after quantified minus_quantified | |
2415 | label llabel slabel guard | |
2416 | ||
2417 | (* term is the translation of stmt *) | |
2418 | and do_between_dots stmt term after quantified minus_quantified | |
2419 | label llabel slabel guard = | |
2420 | match Ast.get_dots_bef_aft stmt with | |
2421 | Ast.AddingBetweenDots (brace_term,n) | |
2422 | | Ast.DroppingBetweenDots (brace_term,n) -> | |
2423 | let match_brace = | |
5427db06 | 2424 | statement brace_term NotTop after quantified minus_quantified |
34e49164 C |
2425 | label llabel slabel guard in |
2426 | let v = Printf.sprintf "_r_%d" n in | |
2427 | let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in | |
2428 | let case2 = ctl_and CTL.NONSTRICT (ctl_not (CTL.Ref v)) term in | |
2429 | CTL.Let | |
2430 | (v,ctl_or | |
2431 | (ctl_back_ex (ctl_or (truepred label) (inlooppred label))) | |
2432 | (ctl_back_ex (ctl_back_ex (falsepred label))), | |
ae4735db | 2433 | ctl_or case1 case2) |
34e49164 C |
2434 | | Ast.NoDots -> term |
2435 | ||
2436 | (* un_process_bef_aft is because we don't want to do transformation in this | |
2437 | code, and thus don't case about braces before or after it *) | |
2438 | and process_bef_aft quantified minus_quantified label llabel slabel guard = | |
2439 | function | |
2440 | Ast.WParen (re,n) -> | |
2441 | let paren_pred = CTL.Pred (Lib_engine.Paren n,CTL.Control) in | |
2442 | let s = guard_to_strict guard in | |
2443 | quantify true (get_unquantified quantified [n]) | |
2444 | (ctl_and s (make_raw_match None guard re) paren_pred) | |
2445 | | Ast.Other s -> | |
5427db06 C |
2446 | statement s NotTop Tail quantified minus_quantified |
2447 | label llabel slabel guard | |
34e49164 | 2448 | | Ast.Other_dots d -> |
5427db06 | 2449 | statement_list d NotTop Tail quantified minus_quantified |
34e49164 C |
2450 | label llabel slabel true guard |
2451 | ||
5427db06 C |
2452 | and protect_top_level stmt_dots formula = |
2453 | let starts_with_dots = | |
2454 | match Ast.undots stmt_dots with | |
2455 | d::ds -> | |
2456 | (match Ast.unwrap d with | |
2457 | Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_) | |
2458 | | Ast.Stars(_,_,_,_) -> true | |
2459 | | _ -> false) | |
2460 | | _ -> false in | |
2461 | let starts_with_non_context_brace = | |
2462 | (* None = No danger | |
2463 | Some false = OK except on function braces | |
2464 | Some true = Never OK *) | |
2465 | match Ast.undots stmt_dots with | |
2466 | d::ds -> | |
2467 | (match Ast.unwrap d with | |
2468 | Ast.Seq(before,body,after) -> | |
2469 | let beforemc = | |
2470 | match Ast.unwrap before with | |
2471 | Ast.SeqStart(obr) -> Ast.get_mcodekind obr | |
2472 | | _ -> failwith "bad seq" in | |
2473 | let aftermc = | |
2474 | match Ast.unwrap after with | |
2475 | Ast.SeqEnd(cbr) -> Ast.get_mcodekind cbr | |
2476 | | _ -> failwith "bad seq"in | |
2477 | (match (beforemc,aftermc) with | |
2478 | (* safe cases *) | |
2479 | (Ast.CONTEXT(_,(Ast.NOTHING|Ast.AFTER _)), | |
2480 | Ast.CONTEXT(_,(Ast.NOTHING|Ast.BEFORE _))) -> None | |
2481 | | (Ast.MINUS(_,_,_,Ast.NOREPLACEMENT), | |
2482 | Ast.MINUS(_,_,_,Ast.NOREPLACEMENT)) | |
2483 | when List.length (Ast.undots body) = 1 -> Some false (*ok on if*) | |
2484 | (* unsafe, can't be allowed to match fn top *) | |
2485 | | _ -> Some true) | |
2486 | | _ -> None) | |
2487 | | _ -> None in | |
2488 | if starts_with_dots | |
2489 | then (* EX because there is a loop on enter/top *) | |
2490 | ctl_and CTL.NONSTRICT (toppred None) (ctl_ex formula) | |
2491 | else | |
2492 | match starts_with_non_context_brace with | |
2493 | None -> formula | |
2494 | | Some false -> | |
2495 | ctl_and CTL.NONSTRICT | |
2496 | (ctl_not(CTL.EX(CTL.BACKWARD,funpred None))) | |
2497 | formula | |
2498 | | Some true -> | |
2499 | ctl_and CTL.NONSTRICT | |
2500 | (ctl_not(CTL.EX(CTL.BACKWARD,unsbrpred None))) | |
2501 | formula | |
2502 | ||
2503 | ||
34e49164 C |
2504 | (* --------------------------------------------------------------------- *) |
2505 | (* cleanup: convert AX to EX for pdots. | |
2506 | Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...]) | |
2507 | This is what we wanted in the first place, but it wasn't possible to make | |
2508 | because the AX and its argument are not created in the same place. | |
2509 | Rather clunky... *) | |
2510 | (* also cleanup XX, which is a marker for the case where the programmer | |
2511 | specifies to change the quantifier on .... Assumed to only occur after one AX | |
2512 | or EX, or at top level. *) | |
2513 | ||
2514 | let rec cleanup c = | |
2515 | let c = match c with CTL.XX(c) -> c | _ -> c in | |
2516 | match c with | |
2517 | CTL.False -> CTL.False | |
2518 | | CTL.True -> CTL.True | |
2519 | | CTL.Pred(p) -> CTL.Pred(p) | |
2520 | | CTL.Not(phi) -> CTL.Not(cleanup phi) | |
2521 | | CTL.Exists(keep,v,phi) -> CTL.Exists(keep,v,cleanup phi) | |
2522 | | CTL.AndAny(dir,s,phi1,phi2) -> | |
2523 | CTL.AndAny(dir,s,cleanup phi1,cleanup phi2) | |
2524 | | CTL.HackForStmt(dir,s,phi1,phi2) -> | |
2525 | CTL.HackForStmt(dir,s,cleanup phi1,cleanup phi2) | |
2526 | | CTL.And(s,phi1,phi2) -> CTL.And(s,cleanup phi1,cleanup phi2) | |
2527 | | CTL.Or(phi1,phi2) -> CTL.Or(cleanup phi1,cleanup phi2) | |
2528 | | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(cleanup phi1,cleanup phi2) | |
2529 | | CTL.Implies(phi1,phi2) -> CTL.Implies(cleanup phi1,cleanup phi2) | |
2530 | | CTL.AF(dir,s,phi1) -> CTL.AF(dir,s,cleanup phi1) | |
2531 | | CTL.AX(CTL.FORWARD,s, | |
2532 | CTL.Let(v1,e1, | |
2533 | CTL.And(CTL.NONSTRICT,CTL.AU(CTL.FORWARD,s2,e2,e3), | |
2534 | CTL.EU(CTL.FORWARD,e4,e5)))) -> | |
2535 | CTL.Let(v1,e1, | |
2536 | CTL.And(CTL.NONSTRICT, | |
2537 | CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)), | |
2538 | CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5)))) | |
1be43e12 | 2539 | | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,cleanup phi) |
34e49164 | 2540 | | CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) -> |
1be43e12 | 2541 | CTL.AX(dir,s,cleanup phi) |
34e49164 C |
2542 | | CTL.XX(phi) -> failwith "bad XX" |
2543 | | CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1) | |
2544 | | CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1) | |
2545 | | CTL.EF(dir,phi1) -> CTL.EF(dir,cleanup phi1) | |
2546 | | CTL.EX(dir,phi1) -> CTL.EX(dir,cleanup phi1) | |
2547 | | CTL.EG(dir,phi1) -> CTL.EG(dir,cleanup phi1) | |
2548 | | CTL.AW(dir,s,phi1,phi2) -> CTL.AW(dir,s,cleanup phi1,cleanup phi2) | |
2549 | | CTL.AU(dir,s,phi1,phi2) -> CTL.AU(dir,s,cleanup phi1,cleanup phi2) | |
2550 | | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,cleanup phi1,cleanup phi2) | |
2551 | | CTL.Let (x,phi1,phi2) -> CTL.Let (x,cleanup phi1,cleanup phi2) | |
2552 | | CTL.LetR (dir,x,phi1,phi2) -> CTL.LetR (dir,x,cleanup phi1,cleanup phi2) | |
2553 | | CTL.Ref(s) -> CTL.Ref(s) | |
2554 | | CTL.Uncheck(phi1) -> CTL.Uncheck(cleanup phi1) | |
2555 | | CTL.InnerAnd(phi1) -> CTL.InnerAnd(cleanup phi1) | |
2556 | ||
2557 | (* --------------------------------------------------------------------- *) | |
2558 | (* Function declaration *) | |
2559 | ||
978fd7e5 C |
2560 | (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *) |
2561 | ||
2562 | let top_level name ((ua,pos),fua) (fuas,t) = | |
34e49164 C |
2563 | let ua = List.filter (function (nm,_) -> nm = name) ua in |
2564 | used_after := ua; | |
2565 | saved := Ast.get_saved t; | |
978fd7e5 | 2566 | let quantified = Common.minus_set (Common.union_set ua fuas) pos in |
65038c61 C |
2567 | let (wrap,formula) = |
2568 | match Ast.unwrap t with | |
34e49164 | 2569 | Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo" |
65038c61 | 2570 | | Ast.NONDECL(stmt) -> |
34e49164 C |
2571 | let unopt = elim_opt.V.rebuilder_statement stmt in |
2572 | let unopt = preprocess_dots_e unopt in | |
65038c61 | 2573 | let formula = |
5427db06 C |
2574 | cleanup |
2575 | (statement unopt Top VeryEnd quantified [] None None None false) in | |
65038c61 | 2576 | ((function x -> NONDECL x), formula) |
34e49164 C |
2577 | | Ast.CODE(stmt_dots) -> |
2578 | let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in | |
2579 | let unopt = preprocess_dots unopt in | |
65038c61 | 2580 | let formula = |
5427db06 C |
2581 | statement_list unopt Top VeryEnd quantified [] None None None |
2582 | false false in | |
2583 | let clean_formula = cleanup (protect_top_level stmt_dots formula) in | |
2584 | ((function x -> CODE x), clean_formula) | |
65038c61 C |
2585 | | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" in |
2586 | wrap (quantify false quantified formula) | |
34e49164 C |
2587 | |
2588 | (* --------------------------------------------------------------------- *) | |
2589 | (* Entry points *) | |
2590 | ||
978fd7e5 C |
2591 | let asttoctlz (name,(_,_,exists_flag),l) |
2592 | (used_after,fresh_used_after,fresh_used_after_seeds) positions = | |
34e49164 C |
2593 | letctr := 0; |
2594 | labelctr := 0; | |
2595 | (match exists_flag with | |
2596 | Ast.Exists -> exists := Exists | |
2597 | | Ast.Forall -> exists := Forall | |
34e49164 C |
2598 | | Ast.Undetermined -> |
2599 | exists := if !Flag.sgrep_mode2 then Exists else Forall); | |
2600 | ||
2601 | let (l,used_after) = | |
2602 | List.split | |
2603 | (List.filter | |
2604 | (function (t,_) -> | |
2605 | match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true) | |
2606 | (List.combine l (List.combine used_after positions))) in | |
978fd7e5 C |
2607 | let res = |
2608 | List.map2 (top_level name) | |
2609 | (List.combine used_after fresh_used_after) | |
2610 | (List.combine fresh_used_after_seeds l) in | |
34e49164 C |
2611 | exists := Forall; |
2612 | res | |
2613 | ||
2614 | let asttoctl r used_after positions = | |
2615 | match r with | |
b1b2de81 | 2616 | Ast.ScriptRule _ | Ast.InitialScriptRule _ | Ast.FinalScriptRule _ -> [] |
faf9a90c C |
2617 | | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) -> |
2618 | asttoctlz (a,b,c) used_after positions | |
65038c61 | 2619 | | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CODE CTL.True] |
34e49164 C |
2620 | |
2621 | let pp_cocci_predicate (pred,modif) = | |
2622 | Pretty_print_engine.pp_predicate pred | |
2623 | ||
2624 | let cocci_predicate_to_string (pred,modif) = | |
2625 | Pretty_print_engine.predicate_to_string pred |