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