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