Commit | Line | Data |
---|---|---|
9f8e26f4 | 1 | (* |
ae4735db | 2 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen |
9f8e26f4 C |
3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix |
4 | * This file is part of Coccinelle. | |
5 | * | |
6 | * Coccinelle is free software: you can redistribute it and/or modify | |
7 | * it under the terms of the GNU General Public License as published by | |
8 | * the Free Software Foundation, according to version 2 of the License. | |
9 | * | |
10 | * Coccinelle is distributed in the hope that it will be useful, | |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
13 | * GNU General Public License for more details. | |
14 | * | |
15 | * You should have received a copy of the GNU General Public License | |
16 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
17 | * | |
18 | * The authors reserve the right to distribute this or future versions of | |
19 | * Coccinelle under other licenses. | |
20 | *) | |
5636bb2c C |
21 | |
22 | ||
23 | (* | |
24 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen | |
25 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
26 | * This file is part of Coccinelle. | |
27 | * | |
28 | * Coccinelle is free software: you can redistribute it and/or modify | |
29 | * it under the terms of the GNU General Public License as published by | |
30 | * the Free Software Foundation, according to version 2 of the License. | |
31 | * | |
32 | * Coccinelle is distributed in the hope that it will be useful, | |
33 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
34 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
35 | * GNU General Public License for more details. | |
36 | * | |
37 | * You should have received a copy of the GNU General Public License | |
38 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
39 | * | |
40 | * The authors reserve the right to distribute this or future versions of | |
41 | * Coccinelle under other licenses. | |
42 | *) | |
9f8e26f4 C |
43 | |
44 | ||
34e49164 C |
45 | (* true = don't see all matched nodes, only modified ones *) |
46 | let onlyModif = ref true(*false*) | |
47 | (* set to true for line numbers in the output of ctl_engine *) | |
48 | let line_numbers = ref false | |
49 | (* if true, only eg if header is included in not for ...s *) | |
50 | let simple_get_end = ref false(*true*) | |
51 | ||
52 | (* Question: where do we put the existential quantifier for or. At the | |
53 | moment, let it float inwards. *) | |
54 | ||
55 | (* nest shouldn't overlap with what comes after. not checked for. *) | |
56 | ||
57 | module Ast = Ast_cocci | |
58 | module V = Visitor_ast | |
59 | module CTL = Ast_ctl | |
60 | module FV = Free_vars | |
61 | ||
62 | let warning s = Printf.fprintf stderr "warning: %s\n" s | |
63 | ||
64 | type cocci_predicate = Lib_engine.predicate * string Ast_ctl.modif | |
65 | type formula = | |
66 | (cocci_predicate,string, Wrapper_ctl.info) Ast_ctl.generic_ctl | |
67 | ||
68 | ||
69 | let aftpred = (Lib_engine.After,CTL.Control) | |
70 | let retpred = (Lib_engine.Return,CTL.Control) | |
71 | let exitpred = (Lib_engine.ErrorExit,CTL.Control) | |
72 | ||
73 | let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1 | |
74 | let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1 | |
75 | ||
76 | (* --------------------------------------------------------------------- *) | |
77 | ||
78 | let rec drop_vs f = | |
79 | CTL.rewrap f | |
80 | (match CTL.unwrap f with | |
81 | CTL.False as x -> x | |
82 | | CTL.True as x -> x | |
83 | | CTL.Pred(p) as x -> x | |
84 | | CTL.Not(phi) -> CTL.Not(drop_vs phi) | |
85 | | CTL.Exists(v,phi) -> | |
86 | (match CTL.unwrap phi with | |
87 | CTL.Pred((x,CTL.Modif v1)) when v = v1 -> CTL.Pred((x,CTL.Control)) | |
88 | | _ -> CTL.Exists(v,drop_vs phi)) | |
89 | | CTL.And(phi1,phi2) -> CTL.And(drop_vs phi1,drop_vs phi2) | |
90 | | CTL.Or(phi1,phi2) -> CTL.Or(drop_vs phi1,drop_vs phi2) | |
91 | | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(drop_vs phi1,drop_vs phi2) | |
92 | | CTL.Implies(phi1,phi2) -> CTL.Implies(drop_vs phi1,drop_vs phi2) | |
93 | | CTL.AF(dir,phi1,phi2) -> CTL.AF(dir,drop_vs phi1,drop_vs phi2) | |
94 | | CTL.AX(dir,phi) -> CTL.AX(dir,drop_vs phi) | |
95 | | CTL.AG(dir,phi) -> CTL.AG(dir,drop_vs phi) | |
96 | | CTL.AU(dir,phi1,phi2,phi3,phi4) -> | |
97 | CTL.AU(dir,drop_vs phi1,drop_vs phi2,drop_vs phi3,drop_vs phi4) | |
98 | | CTL.EF(dir,phi) -> CTL.EF(dir,drop_vs phi) | |
99 | | CTL.EX(dir,phi) -> CTL.EX(dir,drop_vs phi) | |
100 | | CTL.EG(dir,phi) -> CTL.EG(dir,drop_vs phi) | |
101 | | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,drop_vs phi1,drop_vs phi2) | |
102 | | CTL.Ref(v) as x -> x | |
103 | | CTL.Let(v,term1,body) -> CTL.Let(v,drop_vs term1,drop_vs body)) | |
104 | ||
105 | (* --------------------------------------------------------------------- *) | |
106 | ||
107 | let wrap n ctl = (ctl,n) | |
108 | ||
109 | let aftret = | |
110 | wrap 0 (CTL.Or(wrap 0 (CTL.Pred aftpred),wrap 0 (CTL.Pred exitpred))) | |
111 | ||
112 | let wrapImplies n (x,y) = wrap n (CTL.Implies(x,y)) | |
113 | let wrapExists n (x,y) = wrap n (CTL.Exists(x,y)) | |
114 | let wrapAnd n (x,y) = wrap n (CTL.And(x,y)) | |
115 | let wrapOr n (x,y) = wrap n (CTL.Or(x,y)) | |
116 | let wrapSeqOr n (x,y) = wrap n (CTL.SeqOr(x,y)) | |
117 | let wrapAU n (x,y) = wrap n (CTL.AU(CTL.FORWARD,x,y,drop_vs x,drop_vs y)) | |
118 | let wrapEU n (x,y) = wrap n (CTL.EU(CTL.FORWARD,x,y)) | |
119 | let wrapAX n (x) = wrap n (CTL.AX(CTL.FORWARD,x)) | |
120 | let wrapBackAX n (x) = wrap n (CTL.AX(CTL.BACKWARD,x)) | |
121 | let wrapEX n (x) = wrap n (CTL.EX(CTL.FORWARD,x)) | |
122 | let wrapBackEX n (x) = wrap n (CTL.EX(CTL.BACKWARD,x)) | |
123 | let wrapAG n (x) = wrap n (CTL.AG(CTL.FORWARD,x)) | |
124 | let wrapEG n (x) = wrap n (CTL.EG(CTL.FORWARD,x)) | |
125 | let wrapAF n (x) = wrap n (CTL.AF(CTL.FORWARD,x,drop_vs x)) | |
126 | let wrapEF n (x) = wrap n (CTL.EF(CTL.FORWARD,x)) | |
127 | let wrapNot n (x) = wrap n (CTL.Not(x)) | |
128 | let wrapPred n (x) = wrap n (CTL.Pred(x)) | |
129 | let wrapLet n (x,y,z) = wrap n (CTL.Let(x,y,z)) | |
130 | let wrapRef n (x) = wrap n (CTL.Ref(x)) | |
131 | ||
132 | (* --------------------------------------------------------------------- *) | |
133 | ||
134 | let get_option fn = function | |
135 | None -> None | |
136 | | Some x -> Some (fn x) | |
137 | ||
138 | let get_list_option fn = function | |
139 | None -> [] | |
140 | | Some x -> fn x | |
141 | ||
142 | (* --------------------------------------------------------------------- *) | |
143 | (* --------------------------------------------------------------------- *) | |
144 | (* Eliminate OptStm *) | |
145 | ||
146 | (* for optional thing with nothing after, should check that the optional thing | |
147 | never occurs. otherwise the matching stops before it occurs *) | |
148 | let elim_opt = | |
149 | let mcode x = x in | |
150 | let donothing r k e = k e in | |
151 | ||
152 | let fvlist l = | |
153 | List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in | |
154 | ||
155 | let rec dots_list unwrapped wrapped = | |
156 | match (unwrapped,wrapped) with | |
157 | ([],_) -> [] | |
158 | ||
159 | | (Ast.Dots(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest, | |
160 | d0::_::d1::rest) | |
161 | | (Ast.Nest(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest, | |
162 | d0::_::d1::rest) -> | |
163 | let l = Ast.get_line stm in | |
164 | let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in | |
165 | let new_rest2 = dots_list urest rest in | |
166 | let fv_rest1 = fvlist new_rest1 in | |
167 | let fv_rest2 = fvlist new_rest2 in | |
168 | [d0;(Ast.Disj[(Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots); | |
169 | (Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots)], | |
170 | l,fv_rest1,Ast.NoDots)] | |
171 | ||
172 | | (Ast.OptStm(stm)::urest,_::rest) -> | |
173 | let l = Ast.get_line stm in | |
174 | let new_rest1 = dots_list urest rest in | |
175 | let new_rest2 = stm::new_rest1 in | |
176 | let fv_rest1 = fvlist new_rest1 in | |
177 | let fv_rest2 = fvlist new_rest2 in | |
178 | [(Ast.Disj[(Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots); | |
179 | (Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots)], | |
180 | l,fv_rest2,Ast.NoDots)] | |
181 | ||
182 | | ([Ast.Dots(_,_,_);Ast.OptStm(stm)],[d1;_]) -> | |
183 | let l = Ast.get_line stm in | |
184 | let fv_stm = Ast.get_fvs stm in | |
185 | let fv_d1 = Ast.get_fvs d1 in | |
186 | let fv_both = Common.union_set fv_stm fv_d1 in | |
187 | [d1;(Ast.Disj[(Ast.DOTS([stm]),l,fv_stm,Ast.NoDots); | |
188 | (Ast.DOTS([d1]),l,fv_d1,Ast.NoDots)], | |
189 | l,fv_both,Ast.NoDots)] | |
190 | ||
191 | | ([Ast.Nest(_,_,_);Ast.OptStm(stm)],[d1;_]) -> | |
192 | let l = Ast.get_line stm in | |
193 | let rw = Ast.rewrap stm in | |
194 | let rwd = Ast.rewrap stm in | |
195 | let dots = | |
196 | Ast.Dots(("...",{ Ast.line = 0; Ast.column = 0 }, | |
197 | Ast.CONTEXT(Ast.NOTHING)), | |
198 | Ast.NoWhen,[]) in | |
199 | [d1;rw(Ast.Disj[rwd(Ast.DOTS([stm])); | |
200 | (Ast.DOTS([rw dots]),l,[],Ast.NoDots)])] | |
201 | ||
202 | | (_::urest,stm::rest) -> stm :: (dots_list urest rest) | |
203 | | _ -> failwith "not possible" in | |
204 | ||
205 | let stmtdotsfn r k d = | |
206 | let d = k d in | |
207 | Ast.rewrap d | |
208 | (match Ast.unwrap d with | |
209 | Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l) | |
210 | | Ast.CIRCLES(l) -> failwith "elimopt: not supported" | |
211 | | Ast.STARS(l) -> failwith "elimopt: not supported") in | |
ae4735db | 212 | |
34e49164 C |
213 | V.rebuilder |
214 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
215 | donothing donothing stmtdotsfn | |
216 | donothing donothing donothing donothing donothing donothing donothing | |
217 | donothing donothing donothing | |
218 | ||
219 | (* --------------------------------------------------------------------- *) | |
220 | (* Count depth of braces. The translation of a closed brace appears deeply | |
221 | nested within the translation of the sequence term, so the name of the | |
222 | paren var has to take into account the names of the nested braces. On the | |
223 | other hand the close brace does not escape, so we don't have to take into | |
224 | account other paren variable names. *) | |
225 | ||
226 | (* called repetitively, which is inefficient, but less trouble than adding a | |
227 | new field to Seq and FunDecl *) | |
228 | let count_nested_braces s = | |
229 | let bind x y = max x y in | |
230 | let option_default = 0 in | |
231 | let stmt_count r k s = | |
232 | match Ast.unwrap s with | |
233 | Ast.Seq(_,_,_,_,_) | Ast.FunDecl(_,_,_,_,_,_) -> (k s) + 1 | |
234 | | _ -> k s in | |
235 | let donothing r k e = k e in | |
236 | let mcode r x = 0 in | |
237 | let recursor = V.combiner bind option_default | |
238 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
239 | donothing donothing donothing | |
240 | donothing donothing donothing donothing donothing donothing | |
241 | donothing stmt_count donothing donothing in | |
242 | "p"^(string_of_int (recursor.V.combiner_statement s)) | |
243 | ||
244 | (* --------------------------------------------------------------------- *) | |
245 | (* Top-level code *) | |
246 | ||
247 | let ctr = ref 0 | |
248 | let fresh_var _ = | |
249 | let c = !ctr in | |
250 | (*ctr := !ctr + 1;*) | |
251 | Printf.sprintf "v%d" c | |
252 | ||
253 | let labctr = ref 0 | |
254 | let fresh_label_var s = | |
255 | let c = !labctr in | |
256 | labctr := !labctr + 1; | |
257 | Printf.sprintf "%s%d" s c | |
258 | ||
259 | let lctr = ref 0 | |
260 | let fresh_let_var _ = | |
261 | let c = !lctr in | |
262 | lctr := !lctr + 1; | |
263 | Printf.sprintf "l%d" c | |
264 | ||
265 | let sctr = ref 0 | |
266 | let fresh_metavar _ = | |
267 | let c = !sctr in | |
268 | (*sctr := !sctr + 1;*) | |
269 | Printf.sprintf "_S%d" c | |
270 | ||
271 | let get_unquantified quantified vars = | |
272 | List.filter (function x -> not (List.mem x quantified)) vars | |
273 | ||
274 | type after = After of formula | Guard of formula | Tail | |
275 | ||
276 | let make_seq n l = | |
277 | let rec loop = function | |
278 | [] -> failwith "not possible" | |
279 | | [x] -> x | |
280 | | x::xs -> wrapAnd n (x,wrapAX n (loop xs)) in | |
281 | loop l | |
282 | ||
283 | let make_seq_after2 n first = function | |
284 | After rest -> wrapAnd n (first,wrapAX n (wrapAX n rest)) | |
285 | | _ -> first | |
286 | ||
287 | let make_seq_after n first = function | |
288 | After rest -> make_seq n [first;rest] | |
289 | | _ -> first | |
290 | ||
291 | let a2n = function After f -> Guard f | x -> x | |
292 | ||
293 | let and_opt n first = function | |
294 | After rest -> wrapAnd n (first,rest) | |
295 | | _ -> first | |
296 | ||
297 | let contains_modif = | |
298 | let bind x y = x or y in | |
299 | let option_default = false in | |
300 | let mcode r (_,_,kind) = | |
301 | match kind with | |
302 | Ast.MINUS(_) -> true | |
303 | | Ast.PLUS -> failwith "not possible" | |
304 | | Ast.CONTEXT(info) -> not (info = Ast.NOTHING) in | |
305 | let do_nothing r k e = k e in | |
306 | let recursor = | |
307 | V.combiner bind option_default | |
308 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
309 | do_nothing do_nothing do_nothing | |
310 | do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing | |
311 | do_nothing do_nothing do_nothing do_nothing in | |
312 | recursor.V.combiner_rule_elem | |
313 | ||
314 | let make_match n guard used_after code = | |
315 | if guard | |
316 | then wrapPred n (Lib_engine.Match(code),CTL.Control) | |
317 | else | |
318 | let v = fresh_var() in | |
319 | if contains_modif code | |
320 | then wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.Modif v)) | |
321 | else | |
322 | let any_used_after = | |
323 | List.exists (function x -> List.mem x used_after) (Ast.get_fvs code) in | |
324 | if !onlyModif && not any_used_after | |
325 | then wrapPred n (Lib_engine.Match(code),CTL.Control) | |
326 | else wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.UnModif v)) | |
327 | ||
328 | let make_raw_match n code = wrapPred n (Lib_engine.Match(code),CTL.Control) | |
329 | ||
330 | let rec seq_fvs quantified = function | |
331 | [] -> [] | |
332 | | fv1::fvs -> | |
333 | let t1fvs = get_unquantified quantified fv1 in | |
334 | let termfvs = | |
335 | List.fold_left Common.union_set [] | |
336 | (List.map (get_unquantified quantified) fvs) in | |
337 | let bothfvs = Common.inter_set t1fvs termfvs in | |
338 | let t1onlyfvs = Common.minus_set t1fvs bothfvs in | |
339 | let new_quantified = Common.union_set bothfvs quantified in | |
340 | (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs) | |
341 | ||
342 | let seq_fvs2 quantified fv1 fv2 = | |
343 | match seq_fvs quantified [fv1;fv2] with | |
344 | [(t1fvs,bfvs);(t2fvs,[])] -> (t1fvs,bfvs,t2fvs) | |
345 | | _ -> failwith "impossible" | |
346 | ||
347 | let seq_fvs3 quantified fv1 fv2 fv3 = | |
348 | match seq_fvs quantified [fv1;fv2;fv3] with | |
349 | [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,[])] -> | |
350 | (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs) | |
351 | | _ -> failwith "impossible" | |
352 | ||
353 | let seq_fvs4 quantified fv1 fv2 fv3 fv4 = | |
354 | match seq_fvs quantified [fv1;fv2;fv3;fv4] with | |
355 | [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,[])] -> | |
356 | (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs) | |
357 | | _ -> failwith "impossible" | |
358 | ||
359 | let seq_fvs5 quantified fv1 fv2 fv3 fv4 fv5 = | |
360 | match seq_fvs quantified [fv1;fv2;fv3;fv4;fv5] with | |
361 | [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,b45fvs);(t5fvs,[])] -> | |
362 | (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs,b45fvs,t5fvs) | |
363 | | _ -> failwith "impossible" | |
364 | ||
365 | let quantify n = | |
366 | List.fold_right (function cur -> function code -> wrapExists n (cur,code)) | |
367 | ||
368 | let intersectll lst nested_list = | |
369 | List.filter (function x -> List.exists (List.mem x) nested_list) lst | |
370 | ||
371 | (* --------------------------------------------------------------------- *) | |
372 | (* annotate dots with before and after neighbors *) | |
373 | ||
374 | let rec get_before sl a = | |
375 | match Ast.unwrap sl with | |
376 | Ast.DOTS(x) -> | |
377 | let rec loop sl a = | |
378 | match sl with | |
379 | [] -> ([],a) | |
380 | | e::sl -> | |
381 | let (e,ea) = get_before_e e a in | |
382 | let (sl,sla) = loop sl ea in | |
383 | (e::sl,sla) in | |
384 | let (l,a) = loop x a in | |
385 | (Ast.rewrap sl (Ast.DOTS(l)),a) | |
386 | | Ast.CIRCLES(x) -> failwith "not supported" | |
387 | | Ast.STARS(x) -> failwith "not supported" | |
388 | ||
389 | and get_before_e s a = | |
390 | match Ast.unwrap s with | |
391 | Ast.Dots(d,Ast.NoWhen,t) -> | |
392 | (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a) | |
393 | | Ast.Dots(d,Ast.WhenNot w,t) -> | |
394 | let (w,_) = get_before w [] in | |
395 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a) | |
396 | | Ast.Dots(d,Ast.WhenAlways w,t) -> | |
397 | let (w,_) = get_before_e w [] in | |
398 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a) | |
399 | | Ast.Nest(stmt_dots,w,t) -> | |
400 | let (w,_) = List.split (List.map (function s -> get_before s []) w) in | |
401 | let (sd,_) = get_before stmt_dots a in | |
402 | let a = | |
403 | List.filter | |
404 | (function | |
405 | Ast.Other a -> | |
406 | let unifies = | |
407 | Unify_ast.unify_statement_dots | |
408 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in | |
409 | (match unifies with | |
410 | Unify_ast.MAYBE -> false | |
411 | | _ -> true) | |
412 | | Ast.Other_dots a -> | |
413 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in | |
414 | (match unifies with | |
415 | Unify_ast.MAYBE -> false | |
416 | | _ -> true) | |
417 | | _ -> true) | |
418 | a in | |
419 | (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots]) | |
420 | | Ast.Disj(stmt_dots_list) -> | |
421 | let (dsl,dsla) = | |
422 | List.split (List.map (function e -> get_before e a) stmt_dots_list) in | |
423 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) | |
424 | | Ast.Atomic(ast) -> | |
425 | (match Ast.unwrap ast with | |
426 | Ast.MetaStmt(_,_,_) -> (s,[]) | |
427 | | _ -> (s,[Ast.Other s])) | |
428 | | Ast.Seq(lbrace,decls,dots,body,rbrace) -> | |
429 | let index = count_nested_braces s in | |
430 | let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in | |
431 | let (bd,_) = get_before body dea in | |
432 | (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)), | |
433 | [Ast.WParen(rbrace,index)]) | |
434 | | Ast.IfThen(ifheader,branch,aft) -> | |
435 | let (br,_) = get_before_e branch [] in | |
436 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s]) | |
437 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
438 | let (br1,_) = get_before_e branch1 [] in | |
439 | let (br2,_) = get_before_e branch2 [] in | |
440 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) | |
441 | | Ast.While(header,body,aft) -> | |
442 | let (bd,_) = get_before_e body [] in | |
443 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) | |
444 | | Ast.For(header,body,aft) -> | |
445 | let (bd,_) = get_before_e body [] in | |
446 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) | |
447 | | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) -> | |
448 | let index = count_nested_braces s in | |
449 | let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in | |
450 | let (bd,_) = get_before body dea in | |
451 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[]) | |
452 | | _ -> failwith "not supported" | |
453 | ||
454 | let rec get_after sl a = | |
455 | match Ast.unwrap sl with | |
456 | Ast.DOTS(x) -> | |
457 | let rec loop sl = | |
458 | match sl with | |
459 | [] -> ([],a) | |
460 | | e::sl -> | |
461 | let (sl,sla) = loop sl in | |
462 | let (e,ea) = get_after_e e sla in | |
463 | (e::sl,ea) in | |
464 | let (l,a) = loop x in | |
465 | (Ast.rewrap sl (Ast.DOTS(l)),a) | |
466 | | Ast.CIRCLES(x) -> failwith "not supported" | |
467 | | Ast.STARS(x) -> failwith "not supported" | |
468 | ||
469 | and get_after_e s a = | |
470 | match Ast.unwrap s with | |
471 | Ast.Dots(d,Ast.NoWhen,t) -> | |
472 | (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a) | |
473 | | Ast.Dots(d,Ast.WhenNot w,t) -> | |
474 | let (w,_) = get_after w [] in | |
475 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a) | |
476 | | Ast.Dots(d,Ast.WhenAlways w,t) -> | |
477 | let (w,_) = get_after_e w [] in | |
478 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a) | |
479 | | Ast.Nest(stmt_dots,w,t) -> | |
480 | let (w,_) = List.split (List.map (function s -> get_after s []) w) in | |
481 | let (sd,_) = get_after stmt_dots a in | |
482 | let a = | |
483 | List.filter | |
484 | (function | |
485 | Ast.Other a -> | |
486 | let unifies = | |
487 | Unify_ast.unify_statement_dots | |
488 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in | |
489 | (match unifies with | |
490 | Unify_ast.MAYBE -> false | |
491 | | _ -> true) | |
492 | | Ast.Other_dots a -> | |
493 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in | |
494 | (match unifies with | |
495 | Unify_ast.MAYBE -> false | |
496 | | _ -> true) | |
497 | | _ -> true) | |
498 | a in | |
499 | (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots]) | |
500 | | Ast.Disj(stmt_dots_list) -> | |
501 | let (dsl,dsla) = | |
502 | List.split (List.map (function e -> get_after e a) stmt_dots_list) in | |
503 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) | |
504 | | Ast.Atomic(ast) -> | |
505 | (match Ast.unwrap ast with | |
506 | Ast.MetaStmt(nm,Ast.SequencibleAfterDots _,i) -> | |
507 | (* check after information for metavar optimization *) | |
508 | (* if the error is not desired, could just return [], then | |
509 | the optimization (check for EF) won't take place *) | |
510 | List.iter | |
511 | (function | |
512 | Ast.Other x -> | |
513 | (match Ast.unwrap x with | |
514 | Ast.Dots(_,_,_) | Ast.Nest(_,_,_) -> | |
515 | failwith | |
516 | "dots/nest not allowed before and after stmt metavar" | |
517 | | _ -> ()) | |
518 | | Ast.Other_dots x -> | |
519 | (match Ast.undots x with | |
520 | x::_ -> | |
521 | (match Ast.unwrap x with | |
522 | Ast.Dots(_,_,_) | Ast.Nest(_,_,_) -> | |
523 | failwith | |
524 | ("dots/nest not allowed before and after stmt "^ | |
525 | "metavar") | |
526 | | _ -> ()) | |
527 | | _ -> ()) | |
528 | | _ -> ()) | |
529 | a; | |
530 | (Ast.rewrap s | |
531 | (Ast.Atomic | |
532 | (Ast.rewrap s | |
533 | (Ast.MetaStmt(nm,Ast.SequencibleAfterDots a,i)))),[]) | |
534 | | Ast.MetaStmt(_,_,_) -> (s,[]) | |
535 | | _ -> (s,[Ast.Other s])) | |
536 | | Ast.Seq(lbrace,decls,dots,body,rbrace) -> | |
537 | let index = count_nested_braces s in | |
538 | let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in | |
539 | let (de,_) = get_after decls bda in | |
540 | (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)), | |
541 | [Ast.WParen(lbrace,index)]) | |
542 | | Ast.IfThen(ifheader,branch,aft) -> | |
543 | let (br,_) = get_after_e branch a in | |
544 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s]) | |
545 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
546 | let (br1,_) = get_after_e branch1 a in | |
547 | let (br2,_) = get_after_e branch2 a in | |
548 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) | |
549 | | Ast.While(header,body,aft) -> | |
550 | let (bd,_) = get_after_e body a in | |
551 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) | |
552 | | Ast.For(header,body,aft) -> | |
553 | let (bd,_) = get_after_e body a in | |
554 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) | |
555 | | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) -> | |
556 | let index = count_nested_braces s in | |
557 | let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in | |
558 | let (de,_) = get_after decls bda in | |
559 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[]) | |
560 | | _ -> failwith "not supported" | |
561 | ||
562 | ||
563 | let preprocess_dots sl = | |
564 | let (sl,_) = get_before sl [] in | |
565 | let (sl,_) = get_after sl [] in | |
566 | sl | |
567 | ||
568 | let preprocess_dots_e sl = | |
569 | let (sl,_) = get_before_e sl [] in | |
570 | let (sl,_) = get_after_e sl [] in | |
571 | sl | |
572 | ||
573 | (* --------------------------------------------------------------------- *) | |
574 | (* the main translation loop *) | |
575 | ||
576 | let decl_to_not_decl n dots stmt make_match f = | |
577 | if dots | |
578 | then f | |
579 | else | |
580 | let de = | |
581 | let md = Ast.make_meta_decl "_d" (Ast.CONTEXT(Ast.NOTHING)) in | |
582 | Ast.rewrap md (Ast.Decl md) in | |
583 | wrapAU n (make_match de, | |
584 | wrap n (CTL.And(wrap n (CTL.Not (make_match de)), f))) | |
585 | ||
586 | let rec statement_list stmt_list used_after after quantified guard = | |
587 | let n = if !line_numbers then Ast.get_line stmt_list else 0 in | |
588 | match Ast.unwrap stmt_list with | |
589 | Ast.DOTS(x) -> | |
590 | let rec loop quantified = function | |
591 | ([],_) -> (match after with After f -> f | _ -> wrap n CTL.True) | |
592 | | ([e],_) -> statement e used_after after quantified guard | |
593 | | (e::sl,fv::fvs) -> | |
594 | let shared = intersectll fv fvs in | |
595 | let unqshared = get_unquantified quantified shared in | |
596 | let new_quantified = Common.union_set unqshared quantified in | |
597 | quantify n unqshared | |
598 | (statement e used_after (After(loop new_quantified (sl,fvs))) | |
599 | new_quantified guard) | |
600 | | _ -> failwith "not possible" in | |
601 | loop quantified (x,List.map Ast.get_fvs x) | |
602 | | Ast.CIRCLES(x) -> failwith "not supported" | |
603 | | Ast.STARS(x) -> failwith "not supported" | |
604 | ||
605 | and statement stmt used_after after quantified guard = | |
606 | ||
607 | let n = if !line_numbers then Ast.get_line stmt else 0 in | |
608 | let wrapExists = wrapExists n in | |
609 | let wrapAnd = wrapAnd n in | |
610 | let wrapOr = wrapOr n in | |
611 | let wrapSeqOr = wrapSeqOr n in | |
612 | let wrapAU = wrapAU n in | |
613 | let wrapAX = wrapAX n in | |
614 | let wrapBackAX = wrapBackAX n in | |
615 | let wrapEX = wrapEX n in | |
616 | let wrapBackEX = wrapBackEX n in | |
617 | let wrapAG = wrapAG n in | |
618 | let wrapAF = wrapAF n in | |
619 | let wrapEF = wrapEF n in | |
620 | let wrapNot = wrapNot n in | |
621 | let wrapPred = wrapPred n in | |
622 | let make_seq = make_seq n in | |
623 | let make_seq_after2 = make_seq_after2 n in | |
624 | let make_seq_after = make_seq_after n in | |
625 | let and_opt = and_opt n in | |
626 | let quantify = quantify n in | |
627 | let make_match = make_match n guard used_after in | |
628 | let make_raw_match = make_raw_match n in | |
629 | ||
630 | let make_meta_rule_elem d = | |
631 | let nm = fresh_metavar() in | |
632 | Ast.make_meta_rule_elem nm d in | |
633 | ||
634 | match Ast.unwrap stmt with | |
635 | Ast.Atomic(ast) -> | |
636 | (match Ast.unwrap ast with | |
637 | Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.BEFOREAFTER(_,_)) as d)),seqible,_) | |
638 | | Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.AFTER(_)) as d)),seqible,_) -> | |
639 | let label_var = (*fresh_label_var*) "_lab" in | |
640 | let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in | |
641 | let prelabel_pred = | |
642 | wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in | |
643 | let matcher d = make_match (make_meta_rule_elem d) in | |
644 | let full_metamatch = matcher d in | |
645 | let first_metamatch = | |
646 | matcher | |
647 | (match d with | |
648 | Ast.CONTEXT(Ast.BEFOREAFTER(bef,_)) -> | |
649 | Ast.CONTEXT(Ast.BEFORE(bef)) | |
650 | | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING) | |
651 | | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in | |
652 | let middle_metamatch = | |
653 | matcher | |
654 | (match d with | |
655 | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING) | |
656 | | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in | |
657 | let last_metamatch = | |
658 | matcher | |
659 | (match d with | |
660 | Ast.CONTEXT(Ast.BEFOREAFTER(_,aft)) -> | |
661 | Ast.CONTEXT(Ast.AFTER(aft)) | |
662 | | Ast.CONTEXT(_) -> d | |
663 | | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in | |
ae4735db | 664 | |
34e49164 C |
665 | let left_or = |
666 | make_seq | |
667 | [full_metamatch; and_opt (wrapNot(prelabel_pred)) after] in | |
668 | let right_or = | |
669 | make_seq | |
670 | [first_metamatch; | |
671 | wrapAU(middle_metamatch, | |
672 | make_seq | |
673 | [wrapAnd(last_metamatch,label_pred); | |
674 | and_opt (wrapNot(prelabel_pred)) after])] in | |
675 | let body f = | |
676 | wrapAnd(label_pred, | |
677 | f (wrapAnd(make_raw_match ast, | |
678 | wrapOr(left_or,right_or)))) in | |
679 | let id x = x in | |
680 | (match seqible with | |
681 | Ast.Sequencible | Ast.SequencibleAfterDots [] -> | |
682 | quantify (label_var::get_unquantified quantified [s]) | |
683 | (body | |
684 | (function x -> | |
685 | (wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))) | |
686 | | Ast.SequencibleAfterDots l -> | |
687 | let afts = | |
688 | List.map (process_bef_aft Tail quantified used_after n) l in | |
689 | let ors = | |
690 | List.fold_left (function x -> function y -> wrapOr(x,y)) | |
691 | (List.hd afts) (List.tl afts) in | |
692 | quantify (label_var::get_unquantified quantified [s]) | |
693 | (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))), | |
694 | body | |
695 | (function x -> | |
696 | wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))) | |
697 | | Ast.NotSequencible -> | |
698 | quantify (label_var::get_unquantified quantified [s]) (body id)) | |
ae4735db | 699 | |
34e49164 C |
700 | | Ast.MetaStmt((s,i,d),seqible,_) -> |
701 | let label_var = (*fresh_label_var*) "_lab" in | |
702 | let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in | |
703 | let prelabel_pred = | |
704 | wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in | |
705 | let matcher d = make_match (make_meta_rule_elem d) in | |
706 | let first_metamatch = matcher d in | |
707 | let rest_metamatch = | |
708 | matcher | |
709 | (match d with | |
710 | Ast.MINUS(_) -> Ast.MINUS([]) | |
711 | | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING) | |
712 | | Ast.PLUS -> failwith "not possible") in | |
713 | (* first_nodea and first_nodeb are separated here and above to | |
714 | improve let sharing - only first_nodea is unique to this site *) | |
715 | let first_nodeb = first_metamatch in | |
716 | let rest_nodes = wrapAnd(rest_metamatch,prelabel_pred) in | |
717 | let last_node = and_opt (wrapNot(prelabel_pred)) after in | |
718 | let body f = | |
719 | wrapAnd | |
720 | (label_pred, | |
721 | f (wrapAnd | |
722 | (make_raw_match ast, | |
723 | (make_seq | |
724 | [first_nodeb; wrapAU(rest_nodes,last_node)])))) in | |
725 | (match seqible with | |
726 | Ast.Sequencible | Ast.SequencibleAfterDots [] -> | |
727 | quantify (label_var::get_unquantified quantified [s]) | |
728 | (body | |
729 | (function x -> wrapAnd(wrapNot(wrapBackAX(label_pred)),x))) | |
730 | | Ast.SequencibleAfterDots l -> | |
731 | let afts = | |
732 | List.map (process_bef_aft Tail quantified used_after n) l in | |
733 | let ors = | |
734 | List.fold_left (function x -> function y -> wrapOr(x,y)) | |
735 | (List.hd afts) (List.tl afts) in | |
736 | quantify (label_var::get_unquantified quantified [s]) | |
737 | (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))), | |
738 | body | |
739 | (function x -> | |
740 | wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))) | |
741 | | Ast.NotSequencible -> | |
742 | quantify (label_var::get_unquantified quantified [s]) | |
743 | (body (function x -> x))) | |
744 | | _ -> | |
745 | let stmt_fvs = Ast.get_fvs stmt in | |
746 | let fvs = get_unquantified quantified stmt_fvs in | |
747 | let between_dots = Ast.get_dots_bef_aft stmt in | |
748 | let term = make_match ast in | |
749 | let term = | |
750 | match between_dots with | |
751 | Ast.BetweenDots brace_term -> | |
752 | (match Ast.unwrap brace_term with | |
753 | Ast.Atomic(brace_ast) -> | |
754 | let case1 = | |
755 | wrapAnd | |
756 | (wrapOr | |
757 | (wrapBackEX | |
758 | (wrapPred(Lib_engine.TrueBranch,CTL.Control)), | |
759 | wrapBackEX | |
760 | (wrapBackEX(wrapPred(Lib_engine.FalseBranch, | |
761 | CTL.Control)))), | |
762 | make_match brace_ast) in | |
763 | let case2 = | |
764 | wrapAnd | |
765 | (wrapNot | |
766 | (wrapOr | |
767 | (wrapBackEX | |
768 | (wrapPred(Lib_engine.TrueBranch,CTL.Control)), | |
769 | wrapBackEX | |
770 | (wrapBackEX(wrapPred(Lib_engine.FalseBranch, | |
771 | CTL.Control))))), | |
772 | term) in | |
773 | wrapOr(case1,case2) | |
774 | | _ -> failwith "not possible") | |
775 | | Ast.NoDots -> term in | |
776 | make_seq_after (quantify fvs term) after) | |
777 | | Ast.Seq(lbrace,decls,dots,body,rbrace) -> | |
778 | let (lbfvs,b1fvs,_,b2fvs,_,b3fvs,rbfvs) = | |
779 | seq_fvs4 quantified | |
780 | (Ast.get_fvs lbrace) (Ast.get_fvs decls) | |
781 | (Ast.get_fvs body) (Ast.get_fvs rbrace) in | |
782 | let v = count_nested_braces stmt in | |
783 | let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in | |
784 | let start_brace = | |
785 | wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in | |
786 | let end_brace = | |
787 | wrapAnd(quantify rbfvs (make_match rbrace),paren_pred) in | |
788 | let new_quantified2 = | |
789 | Common.union_set b1fvs (Common.union_set b2fvs quantified) in | |
790 | let new_quantified3 = Common.union_set b3fvs new_quantified2 in | |
791 | wrapExists | |
792 | (v,quantify b1fvs | |
793 | (make_seq | |
794 | [start_brace; | |
795 | quantify b2fvs | |
796 | (statement_list decls used_after | |
797 | (After | |
798 | (decl_to_not_decl n dots stmt make_match | |
799 | (quantify b3fvs | |
800 | (statement_list body used_after | |
801 | (After (make_seq_after end_brace after)) | |
802 | new_quantified3 guard)))) | |
803 | new_quantified2 guard)])) | |
804 | | Ast.IfThen(ifheader,branch,aft) -> | |
805 | ||
806 | (* "if (test) thn" becomes: | |
807 | if(test) & AX((TrueBranch & AX thn) v FallThrough v After) | |
808 | ||
809 | "if (test) thn; after" becomes: | |
810 | if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after)) | |
811 | & EX After | |
812 | *) | |
813 | ||
ae4735db | 814 | (* free variables *) |
34e49164 C |
815 | let (efvs,bfvs,_) = |
816 | seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch) in | |
817 | let new_quantified = Common.union_set bfvs quantified in | |
818 | (* if header *) | |
819 | let if_header = quantify efvs (make_match ifheader) in | |
820 | (* then branch and after *) | |
821 | let true_branch = | |
822 | make_seq | |
823 | [wrapPred(Lib_engine.TrueBranch,CTL.Control); | |
824 | statement branch used_after (a2n after) new_quantified guard] in | |
825 | let fall_branch = wrapPred(Lib_engine.FallThrough,CTL.Control) in | |
826 | let after_pred = wrapPred(Lib_engine.After,CTL.Control) in | |
827 | let (aft_needed,after_branch) = | |
828 | match aft with | |
829 | Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after) | |
830 | | _ -> | |
831 | (true, | |
832 | make_seq_after after_pred | |
833 | (After | |
834 | (make_seq_after (make_match (make_meta_rule_elem aft)) | |
835 | after))) in | |
836 | let or_cases = wrapOr(true_branch,wrapOr(fall_branch,after_branch)) in | |
837 | (* the code *) | |
838 | (match (after,aft_needed) with | |
839 | (After _,_) (* pattern doesn't end here *) | |
840 | | (_,true) (* + code added after *) -> | |
841 | quantify bfvs | |
842 | (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred))) | |
843 | | _ -> quantify bfvs (wrapAnd(if_header, wrapAX or_cases))) | |
ae4735db | 844 | |
34e49164 C |
845 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> |
846 | ||
847 | (* "if (test) thn else els" becomes: | |
848 | if(test) & AX((TrueBranch & AX thn) v | |
849 | (FalseBranch & AX (else & AX els)) v After) | |
850 | & EX FalseBranch | |
851 | ||
852 | "if (test) thn else els; after" becomes: | |
853 | if(test) & AX((TrueBranch & AX thn) v | |
854 | (FalseBranch & AX (else & AX els)) v | |
855 | (After & AXAX after)) | |
856 | & EX FalseBranch | |
857 | & EX After | |
858 | ||
859 | ||
860 | Note that we rely on the well-formedness of C programs. For example, we | |
861 | do not use EX to check that there is at least one then branch, because | |
862 | there is always one. And we do not check that there is only one then or | |
863 | else branch, because these again are always the case in a well-formed C | |
864 | program. *) | |
865 | (* free variables *) | |
866 | let (e1fvs,b1fvs,s1fvs) = | |
867 | seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch1) in | |
868 | let (e2fvs,b2fvs,s2fvs) = | |
869 | seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch2) in | |
870 | let bothfvs = | |
871 | Common.union_set | |
872 | (Common.union_set b1fvs b2fvs) | |
873 | (Common.inter_set s1fvs s2fvs) in | |
874 | let exponlyfvs = Common.inter_set e1fvs e2fvs in | |
875 | let new_quantified = Common.union_set bothfvs quantified in | |
876 | (* if header *) | |
877 | let if_header = quantify exponlyfvs (make_match ifheader) in | |
878 | (* then and else branches *) | |
879 | let true_branch = | |
880 | make_seq | |
881 | [wrapPred(Lib_engine.TrueBranch,CTL.Control); | |
882 | statement branch1 used_after (a2n after) new_quantified guard] in | |
883 | let false_pred = wrapPred(Lib_engine.FalseBranch,CTL.Control) in | |
884 | let false_branch = | |
885 | make_seq | |
886 | [false_pred; make_match els; | |
887 | statement branch2 used_after (a2n after) new_quantified guard] in | |
888 | let after_pred = wrapPred(Lib_engine.After,CTL.Control) in | |
889 | let (aft_needed,after_branch) = | |
890 | match aft with | |
891 | Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after) | |
892 | | _ -> | |
893 | (true, | |
894 | make_seq_after after_pred | |
895 | (After | |
896 | (make_seq_after (make_match (make_meta_rule_elem aft)) | |
897 | after))) in | |
898 | let or_cases = wrapOr(true_branch,wrapOr(false_branch,after_branch)) in | |
899 | (* the code *) | |
900 | (match (after,aft_needed) with | |
901 | (After _,_) (* pattern doesn't end here *) | |
902 | | (_,true) (* + code added after *) -> | |
903 | quantify bothfvs | |
904 | (wrapAnd | |
905 | (if_header, | |
906 | wrapAnd(wrapAX or_cases, | |
907 | wrapAnd(wrapEX false_pred,wrapEX after_pred)))) | |
908 | | _ -> | |
909 | quantify bothfvs | |
910 | (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX false_pred)))) | |
911 | ||
912 | | Ast.While(header,body,aft) | Ast.For(header,body,aft) -> | |
913 | (* the translation in this case is similar to that of an if with no else *) | |
ae4735db | 914 | (* free variables *) |
34e49164 C |
915 | let (efvs,bfvs,_) = |
916 | seq_fvs2 quantified (Ast.get_fvs header) (Ast.get_fvs body) in | |
917 | let new_quantified = Common.union_set bfvs quantified in | |
918 | (* if header *) | |
919 | let header = quantify efvs (make_match header) in | |
920 | let body = | |
921 | make_seq | |
922 | [wrapPred(Lib_engine.TrueBranch,CTL.Control); | |
923 | statement body used_after (a2n after) new_quantified guard] in | |
924 | let after_pred = wrapPred(Lib_engine.FallThrough,CTL.Control) in | |
925 | let (aft_needed,after_branch) = | |
926 | match aft with | |
927 | Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after) | |
928 | | _ -> | |
929 | (true, | |
930 | make_seq_after after_pred | |
931 | (After | |
932 | (make_seq_after (make_match (make_meta_rule_elem aft)) | |
933 | after))) in | |
934 | let or_cases = wrapOr(body,after_branch) in | |
935 | (* the code *) | |
936 | (match (after,aft_needed) with | |
937 | (After _,_) (* pattern doesn't end here *) | |
938 | | (_,true) (* + code added after *) -> | |
939 | quantify bfvs | |
940 | (wrapAnd (header, wrapAnd(wrapAX or_cases, wrapEX after_pred))) | |
941 | | _ -> quantify bfvs (wrapAnd(header, wrapAX or_cases))) | |
942 | ||
943 | | Ast.Disj(stmt_dots_list) -> | |
944 | let processed = | |
945 | List.map | |
946 | (function x -> statement_list x used_after after quantified guard) | |
947 | stmt_dots_list in | |
948 | let rec loop = function | |
949 | [] -> wrap n CTL.True | |
950 | | [x] -> x | |
951 | | x::xs -> wrapSeqOr(x,loop xs) in | |
952 | loop processed | |
953 | (* | |
954 | let do_one e = | |
955 | statement_list e used_after (a2n after) quantified true in | |
956 | let add_nots l e = | |
957 | List.fold_left | |
958 | (function rest -> function cur -> wrapAnd(wrapNot(do_one cur),rest)) | |
959 | e l in | |
960 | let process_one nots cur = | |
961 | match Ast.unwrap cur with | |
962 | Ast.DOTS(x::xs) -> | |
963 | let on = List.map (function x -> Ast.OrOther_dots x) nots in | |
964 | (match Ast.unwrap x with | |
965 | Ast.Dots(d,w,t) -> | |
966 | List.iter | |
967 | (function x -> | |
968 | Printf.printf "a not\n"; | |
969 | Pretty_print_cocci.statement_dots x) | |
970 | nots; | |
971 | let cur = | |
972 | Ast.rewrap cur | |
973 | (Ast.DOTS((Ast.rewrap x (Ast.Dots(d,w,on@t)))::xs)) in | |
974 | statement_list cur used_after after quantified guard | |
975 | | Ast.Nest(sd,w,t) -> | |
976 | let cur = | |
977 | Ast.rewrap cur | |
978 | (Ast.DOTS((Ast.rewrap x (Ast.Nest(sd,w,on@t)))::xs)) in | |
979 | statement_list cur used_after after quantified guard | |
980 | | _ -> | |
981 | add_nots nots | |
982 | (statement_list cur used_after after quantified guard)) | |
983 | | Ast.DOTS([]) -> | |
984 | add_nots nots | |
985 | (statement_list cur used_after after quantified guard) | |
986 | | _ -> failwith "CIRCLES, STARS not supported" in | |
987 | let rec loop after = function | |
988 | [] -> failwith "disj shouldn't be empty" (*wrap n CTL.False*) | |
989 | | [(nots,cur)] -> process_one nots cur | |
990 | | (nots,cur)::rest -> wrapOr(process_one nots cur, loop after rest) in | |
991 | loop after (preprocess_disj stmt_dots_list) | |
992 | *) | |
993 | | Ast.Nest(stmt_dots,whencode,befaft) -> | |
994 | let dots_pattern = | |
995 | statement_list stmt_dots used_after (a2n after) quantified guard in | |
996 | let udots_pattern = | |
997 | let whencodes = | |
998 | List.map | |
999 | (function sl -> | |
1000 | statement_list sl used_after (a2n after) quantified true) | |
1001 | whencode in | |
1002 | List.fold_left (function rest -> function cur -> wrapOr(cur,rest)) | |
1003 | (statement_list stmt_dots used_after (a2n after) quantified true) | |
1004 | whencodes in | |
1005 | (match (after,guard&&(whencode=[])) with | |
1006 | (After a,true) -> | |
1007 | let nots = | |
1008 | List.map (process_bef_aft after quantified used_after n) befaft in | |
1009 | (match nots with | |
1010 | [] -> wrapAF(wrapOr(a,aftret)) | |
1011 | | x::xs -> | |
1012 | let left = | |
1013 | wrapNot | |
1014 | (List.fold_left | |
1015 | (function rest -> function cur -> wrapOr(cur,rest)) | |
1016 | x xs) in | |
1017 | wrapAU(left,wrapOr(a,aftret))) | |
1018 | | (After a,false) -> | |
1019 | let left = wrapOr(dots_pattern,wrapNot udots_pattern) in | |
1020 | let nots = | |
1021 | List.map (process_bef_aft after quantified used_after n) befaft in | |
1022 | let left = | |
1023 | match nots with | |
1024 | [] -> left | |
1025 | | x::xs -> | |
1026 | wrapAnd | |
1027 | (wrapNot | |
1028 | (List.fold_left | |
1029 | (function rest -> function cur -> wrapOr(cur,rest)) | |
1030 | x xs), | |
1031 | left) in | |
1032 | wrapAU(left,wrapOr(a,aftret)) | |
1033 | | (_,true) -> wrap n CTL.True | |
1034 | | (_,false) -> wrapAG(wrapOr(dots_pattern,wrapNot udots_pattern))) | |
1035 | | Ast.Dots((_,i,d),whencodes,t) -> | |
1036 | let dot_code = | |
1037 | match d with | |
1038 | Ast.MINUS(_) -> | |
0708f913 | 1039 | (* no need for the fresh metavar, but ... is a bit weird as a |
34e49164 C |
1040 | variable name *) |
1041 | Some(make_match (make_meta_rule_elem d)) | |
1042 | | _ -> None in | |
1043 | let whencodes = | |
1044 | (match whencodes with | |
1045 | Ast.NoWhen -> [] | |
1046 | | Ast.WhenNot whencodes -> | |
1047 | [wrapNot | |
1048 | (statement_list whencodes used_after (a2n after) quantified | |
1049 | true)] | |
1050 | | Ast.WhenAlways s -> | |
1051 | [statement s used_after (a2n after) quantified true]) @ | |
1052 | (List.map wrapNot | |
1053 | (List.map (process_bef_aft after quantified used_after n) t)) in | |
1054 | let phi2 = | |
1055 | match whencodes with | |
1056 | [] -> None | |
1057 | | x::xs -> | |
1058 | Some | |
1059 | (List.fold_left | |
1060 | (function rest -> function cur -> wrapAnd(cur,rest)) | |
1061 | x xs) in | |
1062 | let phi3 = | |
1063 | match (dot_code,phi2) with (* add - on dots, if any *) | |
1064 | (None,None) -> None | |
1065 | | (Some dotcode,None) -> Some dotcode | |
1066 | | (None,Some whencode) -> Some whencode | |
1067 | | (Some dotcode,Some whencode) -> Some(wrapAnd (dotcode,whencode)) in | |
1068 | let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in | |
1069 | (* add in the after code to make the result *) | |
1070 | (match (after,phi3) with | |
1071 | (Tail,Some whencode) -> wrapAU(whencode,wrapOr(exit,aftret)) | |
1072 | | (Tail,None) -> wrapAF(wrapOr(exit,aftret)) | |
1073 | | (After f,Some whencode) | (Guard f,Some whencode) -> | |
1074 | wrapAU(whencode,wrapOr(f,aftret)) | |
1075 | | (After f,None) | (Guard f,None) -> wrapAF(wrapOr(f,aftret))) | |
1076 | | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) -> | |
1077 | let (hfvs,b1fvs,lbfvs,b2fvs,_,b3fvs,_,b4fvs,rbfvs) = | |
1078 | seq_fvs5 quantified (Ast.get_fvs header) (Ast.get_fvs lbrace) | |
1079 | (Ast.get_fvs decls) (Ast.get_fvs body) (Ast.get_fvs rbrace) in | |
1080 | let function_header = quantify hfvs (make_match header) in | |
1081 | let v = count_nested_braces stmt in | |
1082 | let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in | |
1083 | let start_brace = | |
1084 | wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in | |
1085 | let end_brace = | |
1086 | let stripped_rbrace = | |
1087 | match Ast.unwrap rbrace with | |
1088 | Ast.SeqEnd((data,info,_)) -> | |
1089 | Ast.rewrap rbrace | |
1090 | (Ast.SeqEnd ((data,info,Ast.CONTEXT(Ast.NOTHING)))) | |
1091 | | _ -> failwith "unexpected close brace" in | |
1092 | let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in | |
1093 | let errorexit = wrap n (CTL.Pred (Lib_engine.ErrorExit,CTL.Control)) in | |
1094 | wrapAnd(quantify rbfvs (make_match rbrace), | |
1095 | wrapAU(make_match stripped_rbrace, | |
1096 | wrapOr(exit,errorexit))) in | |
1097 | let new_quantified3 = | |
1098 | Common.union_set b1fvs | |
1099 | (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in | |
1100 | let new_quantified4 = Common.union_set b4fvs new_quantified3 in | |
1101 | quantify b1fvs | |
1102 | (make_seq | |
1103 | [function_header; | |
1104 | wrapExists | |
1105 | (v, | |
1106 | (quantify b2fvs | |
1107 | (make_seq | |
1108 | [start_brace; | |
1109 | quantify b3fvs | |
1110 | (statement_list decls used_after | |
1111 | (After | |
1112 | (decl_to_not_decl n dots stmt | |
1113 | make_match | |
1114 | (quantify b4fvs | |
1115 | (statement_list body used_after | |
1116 | (After | |
1117 | (make_seq_after end_brace after)) | |
1118 | new_quantified4 guard)))) | |
1119 | new_quantified3 guard)])))]) | |
1120 | | Ast.OptStm(stm) -> | |
1121 | failwith "OptStm should have been compiled away\n"; | |
1122 | | Ast.UniqueStm(stm) -> | |
1123 | failwith "arities not yet supported" | |
1124 | | Ast.MultiStm(stm) -> | |
1125 | failwith "arities not yet supported" | |
1126 | | _ -> failwith "not supported" | |
1127 | ||
1128 | and process_bef_aft after quantified used_after ln = function | |
1129 | Ast.WParen (re,n) -> | |
1130 | let paren_pred = wrapPred ln (Lib_engine.Paren n,CTL.Control) in | |
1131 | wrapAnd ln (make_raw_match ln re,paren_pred) | |
1132 | | Ast.Other s -> statement s used_after (a2n after) quantified true | |
1133 | | Ast.Other_dots d -> statement_list d used_after (a2n after) quantified true | |
1134 | | Ast.OrOther_dots d -> statement_list d used_after Tail quantified true | |
1135 | ||
1136 | (* Returns a triple for each disj element. The first element of the triple is | |
1137 | Some v if the triple element needs a name, and None otherwise. The second | |
1138 | element is a list of names whose negations should be conjuncted with the | |
1139 | term. The third element is the original term *) | |
1140 | and (preprocess_disj : | |
1141 | Ast.statement Ast.dots list -> | |
1142 | (Ast.statement Ast.dots list * Ast.statement Ast.dots) list) = | |
1143 | function | |
1144 | [] -> [] | |
1145 | | [s] -> [([],s)] | |
1146 | | cur::rest -> | |
1147 | let template = | |
1148 | List.map (function r -> Unify_ast.unify_statement_dots cur r) rest in | |
1149 | let processed = preprocess_disj rest in | |
1150 | if List.exists (function Unify_ast.MAYBE -> true | _ -> false) template | |
1151 | then | |
1152 | ([], cur) :: | |
1153 | (List.map2 | |
1154 | (function ((nots,r) as x) -> | |
1155 | function Unify_ast.MAYBE -> (cur::nots,r) | Unify_ast.NO -> x) | |
1156 | processed template) | |
1157 | else ([], cur) :: processed | |
1158 | ||
1159 | (* --------------------------------------------------------------------- *) | |
1160 | (* Letify: | |
1161 | Phase 1: Use a hash table to identify formulas that appear more than once. | |
1162 | Phase 2: Replace terms by variables. | |
1163 | Phase 3: Drop lets to the point as close as possible to the uses of their | |
1164 | variables *) | |
1165 | ||
1166 | let formula_table = | |
1167 | (Hashtbl.create(50) : | |
1168 | ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl, | |
1169 | int ref (* count *) * string ref (* name *) * bool ref (* processed *)) | |
1170 | Hashtbl.t) | |
1171 | ||
1172 | let add_hash phi = | |
1173 | let (cell,_,_) = | |
1174 | try Hashtbl.find formula_table phi | |
1175 | with Not_found -> | |
1176 | let c = (ref 0,ref "",ref false) in | |
1177 | Hashtbl.add formula_table phi c; | |
1178 | c in | |
1179 | cell := !cell + 1 | |
1180 | ||
1181 | let rec collect_duplicates f = | |
1182 | add_hash f; | |
1183 | match CTL.unwrap f with | |
1184 | CTL.False -> () | |
1185 | | CTL.True -> () | |
1186 | | CTL.Pred(p) -> () | |
1187 | | CTL.Not(phi) -> collect_duplicates phi | |
1188 | | CTL.Exists(v,phi) -> collect_duplicates phi | |
1189 | | CTL.And(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1190 | | CTL.Or(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1191 | | CTL.SeqOr(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1192 | | CTL.Implies(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1193 | | CTL.AF(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1194 | | CTL.AX(_,phi) -> collect_duplicates phi | |
1195 | | CTL.AG(_,phi) -> collect_duplicates phi | |
1196 | | CTL.AU(_,phi1,phi2,phi3,phi4) -> | |
1197 | collect_duplicates phi1; collect_duplicates phi2; | |
1198 | collect_duplicates phi3; collect_duplicates phi4 | |
1199 | | CTL.EF(_,phi) -> collect_duplicates phi | |
1200 | | CTL.EX(_,phi) -> collect_duplicates phi | |
1201 | | CTL.EG(_,phi) -> collect_duplicates phi | |
1202 | | CTL.EU(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1203 | | CTL.Uncheck(phi) -> collect_duplicates phi | |
1204 | | _ -> failwith "not possible" | |
1205 | ||
1206 | let assign_variables _ = | |
1207 | Hashtbl.iter | |
1208 | (function formula -> | |
1209 | function (cell,str,_) -> if !cell > 1 then str := fresh_let_var()) | |
1210 | formula_table | |
1211 | ||
1212 | let rec replace_formulas dec f = | |
1213 | let (ct,name,treated) = Hashtbl.find formula_table f in | |
1214 | let real_ct = !ct - dec in | |
1215 | if real_ct > 1 | |
1216 | then | |
1217 | if not !treated | |
1218 | then | |
1219 | begin | |
1220 | treated := true; | |
1221 | let (acc,new_f) = replace_subformulas (dec + (real_ct - 1)) f in | |
1222 | ((!name,new_f) :: acc, CTL.rewrap f (CTL.Ref !name)) | |
1223 | end | |
1224 | else ([],CTL.rewrap f (CTL.Ref !name)) | |
1225 | else replace_subformulas dec f | |
1226 | ||
1227 | and replace_subformulas dec f = | |
1228 | match CTL.unwrap f with | |
1229 | CTL.False -> ([],f) | |
1230 | | CTL.True -> ([],f) | |
1231 | | CTL.Pred(p) -> ([],f) | |
1232 | | CTL.Not(phi) -> | |
1233 | let (acc,new_phi) = replace_formulas dec phi in | |
1234 | (acc,CTL.rewrap f (CTL.Not(new_phi))) | |
ae4735db | 1235 | | CTL.Exists(v,phi) -> |
34e49164 C |
1236 | let (acc,new_phi) = replace_formulas dec phi in |
1237 | (acc,CTL.rewrap f (CTL.Exists(v,new_phi))) | |
1238 | | CTL.And(phi1,phi2) -> | |
1239 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1240 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1241 | (acc1@acc2,CTL.rewrap f (CTL.And(new_phi1,new_phi2))) | |
1242 | | CTL.Or(phi1,phi2) -> | |
1243 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1244 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1245 | (acc1@acc2,CTL.rewrap f (CTL.Or(new_phi1,new_phi2))) | |
1246 | | CTL.SeqOr(phi1,phi2) -> | |
1247 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1248 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1249 | (acc1@acc2,CTL.rewrap f (CTL.SeqOr(new_phi1,new_phi2))) | |
ae4735db | 1250 | | CTL.Implies(phi1,phi2) -> |
34e49164 C |
1251 | let (acc1,new_phi1) = replace_formulas dec phi1 in |
1252 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1253 | (acc1@acc2,CTL.rewrap f (CTL.Implies(new_phi1,new_phi2))) | |
1254 | | CTL.AF(dir,phi1,phi2) -> | |
1255 | let (acc,new_phi1) = replace_formulas dec phi1 in | |
1256 | let (acc,new_phi2) = replace_formulas dec phi2 in | |
1257 | (acc,CTL.rewrap f (CTL.AF(dir,new_phi1,new_phi2))) | |
1258 | | CTL.AX(dir,phi) -> | |
1259 | let (acc,new_phi) = replace_formulas dec phi in | |
1260 | (acc,CTL.rewrap f (CTL.AX(dir,new_phi))) | |
1261 | | CTL.AG(dir,phi) -> | |
1262 | let (acc,new_phi) = replace_formulas dec phi in | |
1263 | (acc,CTL.rewrap f (CTL.AG(dir,new_phi))) | |
1264 | | CTL.AU(dir,phi1,phi2,phi3,phi4) -> | |
1265 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1266 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1267 | let (acc3,new_phi3) = replace_formulas dec phi3 in | |
1268 | let (acc4,new_phi4) = replace_formulas dec phi4 in | |
1269 | (acc1@acc2@acc3@acc4, | |
1270 | CTL.rewrap f (CTL.AU(dir,new_phi1,new_phi2,new_phi3,new_phi4))) | |
1271 | | CTL.EF(dir,phi) -> | |
1272 | let (acc,new_phi) = replace_formulas dec phi in | |
1273 | (acc,CTL.rewrap f (CTL.EF(dir,new_phi))) | |
1274 | | CTL.EX(dir,phi) -> | |
1275 | let (acc,new_phi) = replace_formulas dec phi in | |
1276 | (acc,CTL.rewrap f (CTL.EX(dir,new_phi))) | |
ae4735db | 1277 | | CTL.EG(dir,phi) -> |
34e49164 C |
1278 | let (acc,new_phi) = replace_formulas dec phi in |
1279 | (acc,CTL.rewrap f (CTL.EG(dir,new_phi))) | |
1280 | | CTL.EU(dir,phi1,phi2) -> | |
1281 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1282 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1283 | (acc1@acc2,CTL.rewrap f (CTL.EU(dir,new_phi1,new_phi2))) | |
1284 | | _ -> failwith "not possible" | |
1285 | ||
1286 | let ctlfv_table = | |
1287 | (Hashtbl.create(50) : | |
1288 | ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl, | |
1289 | string list (* fvs *) * | |
1290 | string list (* intersection of fvs of subterms *)) | |
1291 | Hashtbl.t) | |
1292 | ||
1293 | let rec ctl_fvs f = | |
1294 | try let (fvs,_) = Hashtbl.find ctlfv_table f in fvs | |
1295 | with Not_found -> | |
1296 | let ((fvs,_) as res) = | |
1297 | match CTL.unwrap f with | |
1298 | CTL.False | CTL.True | CTL.Pred(_) -> ([],[]) | |
1299 | | CTL.Not(phi) | CTL.Exists(_,phi) | |
1300 | | CTL.AX(_,phi) | CTL.AG(_,phi) | |
1301 | | CTL.EF(_,phi) | CTL.EX(_,phi) | CTL.EG(_,phi) -> (ctl_fvs phi,[]) | |
1302 | | CTL.AU(_,phi1,phi2,phi3,phi4) -> | |
1303 | let phi1fvs = ctl_fvs phi1 in | |
1304 | let phi2fvs = ctl_fvs phi2 in | |
1305 | (* phi3 has the same fvs as phi1 and phi4 as phi2 *) | |
1306 | (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) | |
1307 | | CTL.And(phi1,phi2) | CTL.Or(phi1,phi2) | CTL.SeqOr(phi1,phi2) | |
1308 | | CTL.Implies(phi1,phi2) | CTL.AF(_,phi1,phi2) | CTL.EU(_,phi1,phi2) -> | |
1309 | let phi1fvs = ctl_fvs phi1 in | |
1310 | let phi2fvs = ctl_fvs phi2 in | |
1311 | (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) | |
1312 | | CTL.Ref(v) -> ([v],[v]) | |
1313 | | CTL.Let(v,term,body) -> | |
1314 | let phi1fvs = ctl_fvs term in | |
1315 | let phi2fvs = Common.minus_set (ctl_fvs body) [v] in | |
1316 | (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) in | |
1317 | Hashtbl.add ctlfv_table f res; | |
1318 | fvs | |
1319 | ||
1320 | let rev_order_bindings b = | |
1321 | let b = | |
1322 | List.map | |
1323 | (function (nm,term) -> | |
1324 | let (fvs,_) = Hashtbl.find ctlfv_table term in (nm,fvs,term)) | |
1325 | b in | |
1326 | let rec loop bound = function | |
1327 | [] -> [] | |
1328 | | unbound -> | |
1329 | let (now_bound,still_unbound) = | |
1330 | List.partition (function (_,fvs,_) -> subset fvs bound) | |
1331 | unbound in | |
1332 | let get_names = List.map (function (x,_,_) -> x) in | |
1333 | now_bound @ (loop ((get_names now_bound) @ bound) still_unbound) in | |
1334 | List.rev(loop [] b) | |
1335 | ||
1336 | let drop_bindings b f = (* innermost bindings first in b *) | |
1337 | let process_binary f ffvs inter nm term fail = | |
1338 | if List.mem nm inter | |
1339 | then CTL.rewrap f (CTL.Let(nm,term,f)) | |
1340 | else CTL.rewrap f (fail()) in | |
1341 | let find_fvs f = | |
1342 | let _ = ctl_fvs f in Hashtbl.find ctlfv_table f in | |
1343 | let rec drop_one nm term f = | |
1344 | match CTL.unwrap f with | |
1345 | CTL.False -> f | |
1346 | | CTL.True -> f | |
1347 | | CTL.Pred(p) -> f | |
1348 | | CTL.Not(phi) -> CTL.rewrap f (CTL.Not(drop_one nm term phi)) | |
1349 | | CTL.Exists(v,phi) -> CTL.rewrap f (CTL.Exists(v,drop_one nm term phi)) | |
1350 | | CTL.And(phi1,phi2) -> | |
1351 | let (ffvs,inter) = find_fvs f in | |
1352 | process_binary f ffvs inter nm term | |
1353 | (function _ -> CTL.And(drop_one nm term phi1,drop_one nm term phi2)) | |
1354 | | CTL.Or(phi1,phi2) -> | |
1355 | let (ffvs,inter) = find_fvs f in | |
1356 | process_binary f ffvs inter nm term | |
1357 | (function _ -> CTL.Or(drop_one nm term phi1,drop_one nm term phi2)) | |
1358 | | CTL.SeqOr(phi1,phi2) -> | |
1359 | let (ffvs,inter) = find_fvs f in | |
1360 | process_binary f ffvs inter nm term | |
1361 | (function _ -> | |
1362 | CTL.SeqOr(drop_one nm term phi1,drop_one nm term phi2)) | |
1363 | | CTL.Implies(phi1,phi2) -> | |
1364 | let (ffvs,inter) = find_fvs f in | |
1365 | process_binary f ffvs inter nm term | |
1366 | (function _ -> | |
1367 | CTL.Implies(drop_one nm term phi1,drop_one nm term phi2)) | |
1368 | | CTL.AF(dir,phi1,phi2) -> | |
1369 | let (ffvs,inter) = find_fvs f in | |
1370 | process_binary f ffvs inter nm term | |
1371 | (function _ -> | |
1372 | CTL.AF(dir,drop_one nm term phi1,drop_one nm term phi2)) | |
1373 | | CTL.AX(dir,phi) -> | |
1374 | CTL.rewrap f (CTL.AX(dir,drop_one nm term phi)) | |
1375 | | CTL.AG(dir,phi) -> CTL.rewrap f (CTL.AG(dir,drop_one nm term phi)) | |
1376 | | CTL.AU(dir,phi1,phi2,phi3,phi4) -> | |
1377 | let (ffvs,inter) = find_fvs f in | |
1378 | process_binary f ffvs inter nm term | |
1379 | (function _ -> | |
1380 | CTL.AU(dir,drop_one nm term phi1,drop_one nm term phi2, | |
1381 | drop_one nm term phi3,drop_one nm term phi4)) | |
1382 | | CTL.EF(dir,phi) -> CTL.rewrap f (CTL.EF(dir,drop_one nm term phi)) | |
1383 | | CTL.EX(dir,phi) -> | |
1384 | CTL.rewrap f (CTL.EX(dir,drop_one nm term phi)) | |
1385 | | CTL.EG(dir,phi) -> CTL.rewrap f (CTL.EG(dir,drop_one nm term phi)) | |
1386 | | CTL.EU(dir,phi1,phi2) -> | |
1387 | let (ffvs,inter) = find_fvs f in | |
1388 | process_binary f ffvs inter nm term | |
1389 | (function _ -> | |
1390 | CTL.EU(dir,drop_one nm term phi1,drop_one nm term phi2)) | |
1391 | | (CTL.Ref(v) as x) -> process_binary f [v] [v] nm term (function _ -> x) | |
1392 | | CTL.Let(v,term1,body) -> | |
1393 | let (ffvs,inter) = find_fvs f in | |
1394 | process_binary f ffvs inter nm term | |
1395 | (function _ -> | |
1396 | CTL.Let(v,drop_one nm term term1,drop_one nm term body)) in | |
1397 | List.fold_left | |
1398 | (function processed -> function (nm,_,term) -> drop_one nm term processed) | |
1399 | f b | |
1400 | ||
1401 | let letify f = | |
1402 | failwith "this code should not be used!!!"(*; | |
1403 | Hashtbl.clear formula_table; | |
1404 | Hashtbl.clear ctlfv_table; | |
1405 | (* create a count of the number of occurrences of each subformula *) | |
1406 | collect_duplicates f; | |
1407 | (* give names to things that appear more than once *) | |
1408 | assign_variables(); | |
1409 | (* replace duplicated formulas by their variables *) | |
1410 | let (bindings,new_f) = replace_formulas 0 f in | |
1411 | (* collect fvs of terms in bindings and new_f *) | |
1412 | List.iter (function f -> let _ = ctl_fvs f in ()) | |
1413 | (new_f::(List.map (function (_,term) -> term) bindings)); | |
1414 | (* sort bindings with uses before defs *) | |
1415 | let bindings = rev_order_bindings bindings in | |
1416 | (* insert bindings as lets into the formula *) | |
1417 | let res = drop_bindings bindings new_f in | |
1418 | res*) | |
1419 | ||
1420 | (* --------------------------------------------------------------------- *) | |
1421 | (* Function declaration *) | |
1422 | ||
1423 | let top_level used_after t = | |
1424 | match Ast.unwrap t with | |
1425 | Ast.DECL(decl) -> failwith "not supported decl" | |
1426 | | Ast.INCLUDE(inc,s) -> | |
1427 | (* no indication of whether inc or s is modified *) | |
1428 | wrap 0 (CTL.Pred((Lib_engine.Include(inc,s),CTL.Control))) | |
1429 | | Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo" | |
1430 | | Ast.FUNCTION(stmt) -> | |
1431 | (*Printf.printf "orig\n"; | |
1432 | Pretty_print_cocci.statement "" stmt; | |
1433 | Format.print_newline();*) | |
1434 | let unopt = elim_opt.V.rebuilder_statement stmt in | |
1435 | (*Printf.printf "unopt\n"; | |
1436 | Pretty_print_cocci.statement "" unopt; | |
1437 | Format.print_newline();*) | |
1438 | let unopt = preprocess_dots_e unopt in | |
1439 | (*letify*) | |
1440 | (statement unopt used_after Tail [] false) | |
1441 | | Ast.CODE(stmt_dots) -> | |
1442 | let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in | |
1443 | let unopt = preprocess_dots unopt in | |
1444 | (*letify*) | |
1445 | (statement_list unopt used_after Tail [] false) | |
1446 | | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" | |
1447 | ||
1448 | (* --------------------------------------------------------------------- *) | |
1449 | (* Contains dots *) | |
1450 | ||
1451 | let contains_dots = | |
1452 | let bind x y = x or y in | |
1453 | let option_default = false in | |
1454 | let mcode r x = false in | |
1455 | let statement r k s = | |
1456 | match Ast.unwrap s with Ast.Dots(_,_,_) -> true | _ -> k s in | |
1457 | let continue r k e = k e in | |
1458 | let stop r k e = false in | |
1459 | let res = | |
1460 | V.combiner bind option_default | |
1461 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
1462 | continue continue continue | |
1463 | stop stop stop stop stop stop stop statement continue continue in | |
1464 | res.V.combiner_top_level | |
1465 | ||
1466 | (* --------------------------------------------------------------------- *) | |
1467 | (* Entry points *) | |
1468 | ||
1469 | let asttoctl l used_after = | |
1470 | ctr := 0; | |
1471 | lctr := 0; | |
1472 | sctr := 0; | |
1473 | let l = | |
1474 | List.filter | |
1475 | (function t -> | |
1476 | match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true) | |
1477 | l in | |
1478 | List.map2 top_level used_after l | |
1479 | ||
1480 | let pp_cocci_predicate (pred,modif) = | |
1481 | Pretty_print_engine.pp_predicate pred | |
1482 | ||
1483 | let cocci_predicate_to_string (pred,modif) = | |
1484 | Pretty_print_engine.predicate_to_string pred |