2 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
23 (* true = don't see all matched nodes, only modified ones *)
24 let onlyModif = ref true(*false*)
25 (* set to true for line numbers in the output of ctl_engine *)
26 let line_numbers = ref false
27 (* if true, only eg if header is included in not for ...s *)
28 let simple_get_end = ref false(*true*)
30 (* Question: where do we put the existential quantifier for or. At the
31 moment, let it float inwards. *)
33 (* nest shouldn't overlap with what comes after. not checked for. *)
35 module Ast = Ast_cocci
36 module V = Visitor_ast
40 let warning s = Printf.fprintf stderr "warning: %s\n" s
42 type cocci_predicate = Lib_engine.predicate * string Ast_ctl.modif
44 (cocci_predicate,string, Wrapper_ctl.info) Ast_ctl.generic_ctl
47 let aftpred = (Lib_engine.After,CTL.Control)
48 let retpred = (Lib_engine.Return,CTL.Control)
49 let exitpred = (Lib_engine.ErrorExit,CTL.Control)
51 let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1
52 let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1
54 (* --------------------------------------------------------------------- *)
58 (match CTL.unwrap f with
61 | CTL.Pred(p) as x -> x
62 | CTL.Not(phi) -> CTL.Not(drop_vs phi)
63 | CTL.Exists(v,phi) ->
64 (match CTL.unwrap phi with
65 CTL.Pred((x,CTL.Modif v1)) when v = v1 -> CTL.Pred((x,CTL.Control))
66 | _ -> CTL.Exists(v,drop_vs phi))
67 | CTL.And(phi1,phi2) -> CTL.And(drop_vs phi1,drop_vs phi2)
68 | CTL.Or(phi1,phi2) -> CTL.Or(drop_vs phi1,drop_vs phi2)
69 | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(drop_vs phi1,drop_vs phi2)
70 | CTL.Implies(phi1,phi2) -> CTL.Implies(drop_vs phi1,drop_vs phi2)
71 | CTL.AF(dir,phi1,phi2) -> CTL.AF(dir,drop_vs phi1,drop_vs phi2)
72 | CTL.AX(dir,phi) -> CTL.AX(dir,drop_vs phi)
73 | CTL.AG(dir,phi) -> CTL.AG(dir,drop_vs phi)
74 | CTL.AU(dir,phi1,phi2,phi3,phi4) ->
75 CTL.AU(dir,drop_vs phi1,drop_vs phi2,drop_vs phi3,drop_vs phi4)
76 | CTL.EF(dir,phi) -> CTL.EF(dir,drop_vs phi)
77 | CTL.EX(dir,phi) -> CTL.EX(dir,drop_vs phi)
78 | CTL.EG(dir,phi) -> CTL.EG(dir,drop_vs phi)
79 | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,drop_vs phi1,drop_vs phi2)
80 | CTL.Ref(v) as x -> x
81 | CTL.Let(v,term1,body) -> CTL.Let(v,drop_vs term1,drop_vs body))
83 (* --------------------------------------------------------------------- *)
85 let wrap n ctl = (ctl,n)
88 wrap 0 (CTL.Or(wrap 0 (CTL.Pred aftpred),wrap 0 (CTL.Pred exitpred)))
90 let wrapImplies n (x,y) = wrap n (CTL.Implies(x,y))
91 let wrapExists n (x,y) = wrap n (CTL.Exists(x,y))
92 let wrapAnd n (x,y) = wrap n (CTL.And(x,y))
93 let wrapOr n (x,y) = wrap n (CTL.Or(x,y))
94 let wrapSeqOr n (x,y) = wrap n (CTL.SeqOr(x,y))
95 let wrapAU n (x,y) = wrap n (CTL.AU(CTL.FORWARD,x,y,drop_vs x,drop_vs y))
96 let wrapEU n (x,y) = wrap n (CTL.EU(CTL.FORWARD,x,y))
97 let wrapAX n (x) = wrap n (CTL.AX(CTL.FORWARD,x))
98 let wrapBackAX n (x) = wrap n (CTL.AX(CTL.BACKWARD,x))
99 let wrapEX n (x) = wrap n (CTL.EX(CTL.FORWARD,x))
100 let wrapBackEX n (x) = wrap n (CTL.EX(CTL.BACKWARD,x))
101 let wrapAG n (x) = wrap n (CTL.AG(CTL.FORWARD,x))
102 let wrapEG n (x) = wrap n (CTL.EG(CTL.FORWARD,x))
103 let wrapAF n (x) = wrap n (CTL.AF(CTL.FORWARD,x,drop_vs x))
104 let wrapEF n (x) = wrap n (CTL.EF(CTL.FORWARD,x))
105 let wrapNot n (x) = wrap n (CTL.Not(x))
106 let wrapPred n (x) = wrap n (CTL.Pred(x))
107 let wrapLet n (x,y,z) = wrap n (CTL.Let(x,y,z))
108 let wrapRef n (x) = wrap n (CTL.Ref(x))
110 (* --------------------------------------------------------------------- *)
112 let get_option fn = function
114 | Some x -> Some (fn x)
116 let get_list_option fn = function
120 (* --------------------------------------------------------------------- *)
121 (* --------------------------------------------------------------------- *)
122 (* Eliminate OptStm *)
124 (* for optional thing with nothing after, should check that the optional thing
125 never occurs. otherwise the matching stops before it occurs *)
128 let donothing r k e = k e in
131 List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in
133 let rec dots_list unwrapped wrapped =
134 match (unwrapped,wrapped) with
137 | (Ast.Dots(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest,
139 | (Ast.Nest(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest,
141 let l = Ast.get_line stm in
142 let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
143 let new_rest2 = dots_list urest rest in
144 let fv_rest1 = fvlist new_rest1 in
145 let fv_rest2 = fvlist new_rest2 in
146 [d0;(Ast.Disj[(Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots);
147 (Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots)],
148 l,fv_rest1,Ast.NoDots)]
150 | (Ast.OptStm(stm)::urest,_::rest) ->
151 let l = Ast.get_line stm in
152 let new_rest1 = dots_list urest rest in
153 let new_rest2 = stm::new_rest1 in
154 let fv_rest1 = fvlist new_rest1 in
155 let fv_rest2 = fvlist new_rest2 in
156 [(Ast.Disj[(Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots);
157 (Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots)],
158 l,fv_rest2,Ast.NoDots)]
160 | ([Ast.Dots(_,_,_);Ast.OptStm(stm)],[d1;_]) ->
161 let l = Ast.get_line stm in
162 let fv_stm = Ast.get_fvs stm in
163 let fv_d1 = Ast.get_fvs d1 in
164 let fv_both = Common.union_set fv_stm fv_d1 in
165 [d1;(Ast.Disj[(Ast.DOTS([stm]),l,fv_stm,Ast.NoDots);
166 (Ast.DOTS([d1]),l,fv_d1,Ast.NoDots)],
167 l,fv_both,Ast.NoDots)]
169 | ([Ast.Nest(_,_,_);Ast.OptStm(stm)],[d1;_]) ->
170 let l = Ast.get_line stm in
171 let rw = Ast.rewrap stm in
172 let rwd = Ast.rewrap stm in
174 Ast.Dots(("...",{ Ast.line = 0; Ast.column = 0 },
175 Ast.CONTEXT(Ast.NOTHING)),
177 [d1;rw(Ast.Disj[rwd(Ast.DOTS([stm]));
178 (Ast.DOTS([rw dots]),l,[],Ast.NoDots)])]
180 | (_::urest,stm::rest) -> stm :: (dots_list urest rest)
181 | _ -> failwith "not possible" in
183 let stmtdotsfn r k d =
186 (match Ast.unwrap d with
187 Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
188 | Ast.CIRCLES(l) -> failwith "elimopt: not supported"
189 | Ast.STARS(l) -> failwith "elimopt: not supported") in
192 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
193 donothing donothing stmtdotsfn
194 donothing donothing donothing donothing donothing donothing donothing
195 donothing donothing donothing
197 (* --------------------------------------------------------------------- *)
198 (* Count depth of braces. The translation of a closed brace appears deeply
199 nested within the translation of the sequence term, so the name of the
200 paren var has to take into account the names of the nested braces. On the
201 other hand the close brace does not escape, so we don't have to take into
202 account other paren variable names. *)
204 (* called repetitively, which is inefficient, but less trouble than adding a
205 new field to Seq and FunDecl *)
206 let count_nested_braces s =
207 let bind x y = max x y in
208 let option_default = 0 in
209 let stmt_count r k s =
210 match Ast.unwrap s with
211 Ast.Seq(_,_,_,_,_) | Ast.FunDecl(_,_,_,_,_,_) -> (k s) + 1
213 let donothing r k e = k e in
215 let recursor = V.combiner bind option_default
216 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
217 donothing donothing donothing
218 donothing donothing donothing donothing donothing donothing
219 donothing stmt_count donothing donothing in
220 "p"^(string_of_int (recursor.V.combiner_statement s))
222 (* --------------------------------------------------------------------- *)
229 Printf.sprintf "v%d" c
232 let fresh_label_var s =
234 labctr := !labctr + 1;
235 Printf.sprintf "%s%d" s c
238 let fresh_let_var _ =
241 Printf.sprintf "l%d" c
244 let fresh_metavar _ =
246 (*sctr := !sctr + 1;*)
247 Printf.sprintf "_S%d" c
249 let get_unquantified quantified vars =
250 List.filter (function x -> not (List.mem x quantified)) vars
252 type after = After of formula | Guard of formula | Tail
255 let rec loop = function
256 [] -> failwith "not possible"
258 | x::xs -> wrapAnd n (x,wrapAX n (loop xs)) in
261 let make_seq_after2 n first = function
262 After rest -> wrapAnd n (first,wrapAX n (wrapAX n rest))
265 let make_seq_after n first = function
266 After rest -> make_seq n [first;rest]
269 let a2n = function After f -> Guard f | x -> x
271 let and_opt n first = function
272 After rest -> wrapAnd n (first,rest)
276 let bind x y = x or y in
277 let option_default = false in
278 let mcode r (_,_,kind) =
281 | Ast.PLUS -> failwith "not possible"
282 | Ast.CONTEXT(info) -> not (info = Ast.NOTHING) in
283 let do_nothing r k e = k e in
285 V.combiner bind option_default
286 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
287 do_nothing do_nothing do_nothing
288 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
289 do_nothing do_nothing do_nothing do_nothing in
290 recursor.V.combiner_rule_elem
292 let make_match n guard used_after code =
294 then wrapPred n (Lib_engine.Match(code),CTL.Control)
296 let v = fresh_var() in
297 if contains_modif code
298 then wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.Modif v))
301 List.exists (function x -> List.mem x used_after) (Ast.get_fvs code) in
302 if !onlyModif && not any_used_after
303 then wrapPred n (Lib_engine.Match(code),CTL.Control)
304 else wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.UnModif v))
306 let make_raw_match n code = wrapPred n (Lib_engine.Match(code),CTL.Control)
308 let rec seq_fvs quantified = function
311 let t1fvs = get_unquantified quantified fv1 in
313 List.fold_left Common.union_set []
314 (List.map (get_unquantified quantified) fvs) in
315 let bothfvs = Common.inter_set t1fvs termfvs in
316 let t1onlyfvs = Common.minus_set t1fvs bothfvs in
317 let new_quantified = Common.union_set bothfvs quantified in
318 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs)
320 let seq_fvs2 quantified fv1 fv2 =
321 match seq_fvs quantified [fv1;fv2] with
322 [(t1fvs,bfvs);(t2fvs,[])] -> (t1fvs,bfvs,t2fvs)
323 | _ -> failwith "impossible"
325 let seq_fvs3 quantified fv1 fv2 fv3 =
326 match seq_fvs quantified [fv1;fv2;fv3] with
327 [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,[])] ->
328 (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs)
329 | _ -> failwith "impossible"
331 let seq_fvs4 quantified fv1 fv2 fv3 fv4 =
332 match seq_fvs quantified [fv1;fv2;fv3;fv4] with
333 [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,[])] ->
334 (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs)
335 | _ -> failwith "impossible"
337 let seq_fvs5 quantified fv1 fv2 fv3 fv4 fv5 =
338 match seq_fvs quantified [fv1;fv2;fv3;fv4;fv5] with
339 [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,b45fvs);(t5fvs,[])] ->
340 (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs,b45fvs,t5fvs)
341 | _ -> failwith "impossible"
344 List.fold_right (function cur -> function code -> wrapExists n (cur,code))
346 let intersectll lst nested_list =
347 List.filter (function x -> List.exists (List.mem x) nested_list) lst
349 (* --------------------------------------------------------------------- *)
350 (* annotate dots with before and after neighbors *)
352 let rec get_before sl a =
353 match Ast.unwrap sl with
359 let (e,ea) = get_before_e e a in
360 let (sl,sla) = loop sl ea in
362 let (l,a) = loop x a in
363 (Ast.rewrap sl (Ast.DOTS(l)),a)
364 | Ast.CIRCLES(x) -> failwith "not supported"
365 | Ast.STARS(x) -> failwith "not supported"
367 and get_before_e s a =
368 match Ast.unwrap s with
369 Ast.Dots(d,Ast.NoWhen,t) ->
370 (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a)
371 | Ast.Dots(d,Ast.WhenNot w,t) ->
372 let (w,_) = get_before w [] in
373 (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a)
374 | Ast.Dots(d,Ast.WhenAlways w,t) ->
375 let (w,_) = get_before_e w [] in
376 (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a)
377 | Ast.Nest(stmt_dots,w,t) ->
378 let (w,_) = List.split (List.map (function s -> get_before s []) w) in
379 let (sd,_) = get_before stmt_dots a in
385 Unify_ast.unify_statement_dots
386 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
388 Unify_ast.MAYBE -> false
390 | Ast.Other_dots a ->
391 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
393 Unify_ast.MAYBE -> false
397 (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots])
398 | Ast.Disj(stmt_dots_list) ->
400 List.split (List.map (function e -> get_before e a) stmt_dots_list) in
401 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
403 (match Ast.unwrap ast with
404 Ast.MetaStmt(_,_,_) -> (s,[])
405 | _ -> (s,[Ast.Other s]))
406 | Ast.Seq(lbrace,decls,dots,body,rbrace) ->
407 let index = count_nested_braces s in
408 let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
409 let (bd,_) = get_before body dea in
410 (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)),
411 [Ast.WParen(rbrace,index)])
412 | Ast.IfThen(ifheader,branch,aft) ->
413 let (br,_) = get_before_e branch [] in
414 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s])
415 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
416 let (br1,_) = get_before_e branch1 [] in
417 let (br2,_) = get_before_e branch2 [] in
418 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
419 | Ast.While(header,body,aft) ->
420 let (bd,_) = get_before_e body [] in
421 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
422 | Ast.For(header,body,aft) ->
423 let (bd,_) = get_before_e body [] in
424 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
425 | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) ->
426 let index = count_nested_braces s in
427 let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
428 let (bd,_) = get_before body dea in
429 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[])
430 | _ -> failwith "not supported"
432 let rec get_after sl a =
433 match Ast.unwrap sl with
439 let (sl,sla) = loop sl in
440 let (e,ea) = get_after_e e sla in
442 let (l,a) = loop x in
443 (Ast.rewrap sl (Ast.DOTS(l)),a)
444 | Ast.CIRCLES(x) -> failwith "not supported"
445 | Ast.STARS(x) -> failwith "not supported"
447 and get_after_e s a =
448 match Ast.unwrap s with
449 Ast.Dots(d,Ast.NoWhen,t) ->
450 (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a)
451 | Ast.Dots(d,Ast.WhenNot w,t) ->
452 let (w,_) = get_after w [] in
453 (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a)
454 | Ast.Dots(d,Ast.WhenAlways w,t) ->
455 let (w,_) = get_after_e w [] in
456 (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a)
457 | Ast.Nest(stmt_dots,w,t) ->
458 let (w,_) = List.split (List.map (function s -> get_after s []) w) in
459 let (sd,_) = get_after stmt_dots a in
465 Unify_ast.unify_statement_dots
466 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
468 Unify_ast.MAYBE -> false
470 | Ast.Other_dots a ->
471 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
473 Unify_ast.MAYBE -> false
477 (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots])
478 | Ast.Disj(stmt_dots_list) ->
480 List.split (List.map (function e -> get_after e a) stmt_dots_list) in
481 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
483 (match Ast.unwrap ast with
484 Ast.MetaStmt(nm,Ast.SequencibleAfterDots _,i) ->
485 (* check after information for metavar optimization *)
486 (* if the error is not desired, could just return [], then
487 the optimization (check for EF) won't take place *)
491 (match Ast.unwrap x with
492 Ast.Dots(_,_,_) | Ast.Nest(_,_,_) ->
494 "dots/nest not allowed before and after stmt metavar"
496 | Ast.Other_dots x ->
497 (match Ast.undots x with
499 (match Ast.unwrap x with
500 Ast.Dots(_,_,_) | Ast.Nest(_,_,_) ->
502 ("dots/nest not allowed before and after stmt "^
511 (Ast.MetaStmt(nm,Ast.SequencibleAfterDots a,i)))),[])
512 | Ast.MetaStmt(_,_,_) -> (s,[])
513 | _ -> (s,[Ast.Other s]))
514 | Ast.Seq(lbrace,decls,dots,body,rbrace) ->
515 let index = count_nested_braces s in
516 let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
517 let (de,_) = get_after decls bda in
518 (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)),
519 [Ast.WParen(lbrace,index)])
520 | Ast.IfThen(ifheader,branch,aft) ->
521 let (br,_) = get_after_e branch a in
522 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s])
523 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
524 let (br1,_) = get_after_e branch1 a in
525 let (br2,_) = get_after_e branch2 a in
526 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
527 | Ast.While(header,body,aft) ->
528 let (bd,_) = get_after_e body a in
529 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
530 | Ast.For(header,body,aft) ->
531 let (bd,_) = get_after_e body a in
532 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
533 | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) ->
534 let index = count_nested_braces s in
535 let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
536 let (de,_) = get_after decls bda in
537 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[])
538 | _ -> failwith "not supported"
541 let preprocess_dots sl =
542 let (sl,_) = get_before sl [] in
543 let (sl,_) = get_after sl [] in
546 let preprocess_dots_e sl =
547 let (sl,_) = get_before_e sl [] in
548 let (sl,_) = get_after_e sl [] in
551 (* --------------------------------------------------------------------- *)
552 (* the main translation loop *)
554 let decl_to_not_decl n dots stmt make_match f =
559 let md = Ast.make_meta_decl "_d" (Ast.CONTEXT(Ast.NOTHING)) in
560 Ast.rewrap md (Ast.Decl md) in
561 wrapAU n (make_match de,
562 wrap n (CTL.And(wrap n (CTL.Not (make_match de)), f)))
564 let rec statement_list stmt_list used_after after quantified guard =
565 let n = if !line_numbers then Ast.get_line stmt_list else 0 in
566 match Ast.unwrap stmt_list with
568 let rec loop quantified = function
569 ([],_) -> (match after with After f -> f | _ -> wrap n CTL.True)
570 | ([e],_) -> statement e used_after after quantified guard
572 let shared = intersectll fv fvs in
573 let unqshared = get_unquantified quantified shared in
574 let new_quantified = Common.union_set unqshared quantified in
576 (statement e used_after (After(loop new_quantified (sl,fvs)))
577 new_quantified guard)
578 | _ -> failwith "not possible" in
579 loop quantified (x,List.map Ast.get_fvs x)
580 | Ast.CIRCLES(x) -> failwith "not supported"
581 | Ast.STARS(x) -> failwith "not supported"
583 and statement stmt used_after after quantified guard =
585 let n = if !line_numbers then Ast.get_line stmt else 0 in
586 let wrapExists = wrapExists n in
587 let wrapAnd = wrapAnd n in
588 let wrapOr = wrapOr n in
589 let wrapSeqOr = wrapSeqOr n in
590 let wrapAU = wrapAU n in
591 let wrapAX = wrapAX n in
592 let wrapBackAX = wrapBackAX n in
593 let wrapEX = wrapEX n in
594 let wrapBackEX = wrapBackEX n in
595 let wrapAG = wrapAG n in
596 let wrapAF = wrapAF n in
597 let wrapEF = wrapEF n in
598 let wrapNot = wrapNot n in
599 let wrapPred = wrapPred n in
600 let make_seq = make_seq n in
601 let make_seq_after2 = make_seq_after2 n in
602 let make_seq_after = make_seq_after n in
603 let and_opt = and_opt n in
604 let quantify = quantify n in
605 let make_match = make_match n guard used_after in
606 let make_raw_match = make_raw_match n in
608 let make_meta_rule_elem d =
609 let nm = fresh_metavar() in
610 Ast.make_meta_rule_elem nm d in
612 match Ast.unwrap stmt with
614 (match Ast.unwrap ast with
615 Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.BEFOREAFTER(_,_)) as d)),seqible,_)
616 | Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.AFTER(_)) as d)),seqible,_) ->
617 let label_var = (*fresh_label_var*) "_lab" in
618 let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in
620 wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in
621 let matcher d = make_match (make_meta_rule_elem d) in
622 let full_metamatch = matcher d in
623 let first_metamatch =
626 Ast.CONTEXT(Ast.BEFOREAFTER(bef,_)) ->
627 Ast.CONTEXT(Ast.BEFORE(bef))
628 | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING)
629 | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
630 let middle_metamatch =
633 Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING)
634 | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
638 Ast.CONTEXT(Ast.BEFOREAFTER(_,aft)) ->
639 Ast.CONTEXT(Ast.AFTER(aft))
640 | Ast.CONTEXT(_) -> d
641 | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
645 [full_metamatch; and_opt (wrapNot(prelabel_pred)) after] in
649 wrapAU(middle_metamatch,
651 [wrapAnd(last_metamatch,label_pred);
652 and_opt (wrapNot(prelabel_pred)) after])] in
655 f (wrapAnd(make_raw_match ast,
656 wrapOr(left_or,right_or)))) in
659 Ast.Sequencible | Ast.SequencibleAfterDots [] ->
660 quantify (label_var::get_unquantified quantified [s])
663 (wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
664 | Ast.SequencibleAfterDots l ->
666 List.map (process_bef_aft Tail quantified used_after n) l in
668 List.fold_left (function x -> function y -> wrapOr(x,y))
669 (List.hd afts) (List.tl afts) in
670 quantify (label_var::get_unquantified quantified [s])
671 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
674 wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
675 | Ast.NotSequencible ->
676 quantify (label_var::get_unquantified quantified [s]) (body id))
678 | Ast.MetaStmt((s,i,d),seqible,_) ->
679 let label_var = (*fresh_label_var*) "_lab" in
680 let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in
682 wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in
683 let matcher d = make_match (make_meta_rule_elem d) in
684 let first_metamatch = matcher d in
688 Ast.MINUS(_) -> Ast.MINUS([])
689 | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING)
690 | Ast.PLUS -> failwith "not possible") in
691 (* first_nodea and first_nodeb are separated here and above to
692 improve let sharing - only first_nodea is unique to this site *)
693 let first_nodeb = first_metamatch in
694 let rest_nodes = wrapAnd(rest_metamatch,prelabel_pred) in
695 let last_node = and_opt (wrapNot(prelabel_pred)) after in
702 [first_nodeb; wrapAU(rest_nodes,last_node)])))) in
704 Ast.Sequencible | Ast.SequencibleAfterDots [] ->
705 quantify (label_var::get_unquantified quantified [s])
707 (function x -> wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))
708 | Ast.SequencibleAfterDots l ->
710 List.map (process_bef_aft Tail quantified used_after n) l in
712 List.fold_left (function x -> function y -> wrapOr(x,y))
713 (List.hd afts) (List.tl afts) in
714 quantify (label_var::get_unquantified quantified [s])
715 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
718 wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
719 | Ast.NotSequencible ->
720 quantify (label_var::get_unquantified quantified [s])
721 (body (function x -> x)))
723 let stmt_fvs = Ast.get_fvs stmt in
724 let fvs = get_unquantified quantified stmt_fvs in
725 let between_dots = Ast.get_dots_bef_aft stmt in
726 let term = make_match ast in
728 match between_dots with
729 Ast.BetweenDots brace_term ->
730 (match Ast.unwrap brace_term with
731 Ast.Atomic(brace_ast) ->
736 (wrapPred(Lib_engine.TrueBranch,CTL.Control)),
738 (wrapBackEX(wrapPred(Lib_engine.FalseBranch,
740 make_match brace_ast) in
746 (wrapPred(Lib_engine.TrueBranch,CTL.Control)),
748 (wrapBackEX(wrapPred(Lib_engine.FalseBranch,
752 | _ -> failwith "not possible")
753 | Ast.NoDots -> term in
754 make_seq_after (quantify fvs term) after)
755 | Ast.Seq(lbrace,decls,dots,body,rbrace) ->
756 let (lbfvs,b1fvs,_,b2fvs,_,b3fvs,rbfvs) =
758 (Ast.get_fvs lbrace) (Ast.get_fvs decls)
759 (Ast.get_fvs body) (Ast.get_fvs rbrace) in
760 let v = count_nested_braces stmt in
761 let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in
763 wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in
765 wrapAnd(quantify rbfvs (make_match rbrace),paren_pred) in
766 let new_quantified2 =
767 Common.union_set b1fvs (Common.union_set b2fvs quantified) in
768 let new_quantified3 = Common.union_set b3fvs new_quantified2 in
774 (statement_list decls used_after
776 (decl_to_not_decl n dots stmt make_match
778 (statement_list body used_after
779 (After (make_seq_after end_brace after))
780 new_quantified3 guard))))
781 new_quantified2 guard)]))
782 | Ast.IfThen(ifheader,branch,aft) ->
784 (* "if (test) thn" becomes:
785 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
787 "if (test) thn; after" becomes:
788 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
794 seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch) in
795 let new_quantified = Common.union_set bfvs quantified in
797 let if_header = quantify efvs (make_match ifheader) in
798 (* then branch and after *)
801 [wrapPred(Lib_engine.TrueBranch,CTL.Control);
802 statement branch used_after (a2n after) new_quantified guard] in
803 let fall_branch = wrapPred(Lib_engine.FallThrough,CTL.Control) in
804 let after_pred = wrapPred(Lib_engine.After,CTL.Control) in
805 let (aft_needed,after_branch) =
807 Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after)
810 make_seq_after after_pred
812 (make_seq_after (make_match (make_meta_rule_elem aft))
814 let or_cases = wrapOr(true_branch,wrapOr(fall_branch,after_branch)) in
816 (match (after,aft_needed) with
817 (After _,_) (* pattern doesn't end here *)
818 | (_,true) (* + code added after *) ->
820 (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
821 | _ -> quantify bfvs (wrapAnd(if_header, wrapAX or_cases)))
823 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
825 (* "if (test) thn else els" becomes:
826 if(test) & AX((TrueBranch & AX thn) v
827 (FalseBranch & AX (else & AX els)) v After)
830 "if (test) thn else els; after" becomes:
831 if(test) & AX((TrueBranch & AX thn) v
832 (FalseBranch & AX (else & AX els)) v
833 (After & AXAX after))
838 Note that we rely on the well-formedness of C programs. For example, we
839 do not use EX to check that there is at least one then branch, because
840 there is always one. And we do not check that there is only one then or
841 else branch, because these again are always the case in a well-formed C
844 let (e1fvs,b1fvs,s1fvs) =
845 seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch1) in
846 let (e2fvs,b2fvs,s2fvs) =
847 seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch2) in
850 (Common.union_set b1fvs b2fvs)
851 (Common.inter_set s1fvs s2fvs) in
852 let exponlyfvs = Common.inter_set e1fvs e2fvs in
853 let new_quantified = Common.union_set bothfvs quantified in
855 let if_header = quantify exponlyfvs (make_match ifheader) in
856 (* then and else branches *)
859 [wrapPred(Lib_engine.TrueBranch,CTL.Control);
860 statement branch1 used_after (a2n after) new_quantified guard] in
861 let false_pred = wrapPred(Lib_engine.FalseBranch,CTL.Control) in
864 [false_pred; make_match els;
865 statement branch2 used_after (a2n after) new_quantified guard] in
866 let after_pred = wrapPred(Lib_engine.After,CTL.Control) in
867 let (aft_needed,after_branch) =
869 Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after)
872 make_seq_after after_pred
874 (make_seq_after (make_match (make_meta_rule_elem aft))
876 let or_cases = wrapOr(true_branch,wrapOr(false_branch,after_branch)) in
878 (match (after,aft_needed) with
879 (After _,_) (* pattern doesn't end here *)
880 | (_,true) (* + code added after *) ->
884 wrapAnd(wrapAX or_cases,
885 wrapAnd(wrapEX false_pred,wrapEX after_pred))))
888 (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX false_pred))))
890 | Ast.While(header,body,aft) | Ast.For(header,body,aft) ->
891 (* the translation in this case is similar to that of an if with no else *)
894 seq_fvs2 quantified (Ast.get_fvs header) (Ast.get_fvs body) in
895 let new_quantified = Common.union_set bfvs quantified in
897 let header = quantify efvs (make_match header) in
900 [wrapPred(Lib_engine.TrueBranch,CTL.Control);
901 statement body used_after (a2n after) new_quantified guard] in
902 let after_pred = wrapPred(Lib_engine.FallThrough,CTL.Control) in
903 let (aft_needed,after_branch) =
905 Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after)
908 make_seq_after after_pred
910 (make_seq_after (make_match (make_meta_rule_elem aft))
912 let or_cases = wrapOr(body,after_branch) in
914 (match (after,aft_needed) with
915 (After _,_) (* pattern doesn't end here *)
916 | (_,true) (* + code added after *) ->
918 (wrapAnd (header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
919 | _ -> quantify bfvs (wrapAnd(header, wrapAX or_cases)))
921 | Ast.Disj(stmt_dots_list) ->
924 (function x -> statement_list x used_after after quantified guard)
926 let rec loop = function
927 [] -> wrap n CTL.True
929 | x::xs -> wrapSeqOr(x,loop xs) in
933 statement_list e used_after (a2n after) quantified true in
936 (function rest -> function cur -> wrapAnd(wrapNot(do_one cur),rest))
938 let process_one nots cur =
939 match Ast.unwrap cur with
941 let on = List.map (function x -> Ast.OrOther_dots x) nots in
942 (match Ast.unwrap x with
946 Printf.printf "a not\n";
947 Pretty_print_cocci.statement_dots x)
951 (Ast.DOTS((Ast.rewrap x (Ast.Dots(d,w,on@t)))::xs)) in
952 statement_list cur used_after after quantified guard
953 | Ast.Nest(sd,w,t) ->
956 (Ast.DOTS((Ast.rewrap x (Ast.Nest(sd,w,on@t)))::xs)) in
957 statement_list cur used_after after quantified guard
960 (statement_list cur used_after after quantified guard))
963 (statement_list cur used_after after quantified guard)
964 | _ -> failwith "CIRCLES, STARS not supported" in
965 let rec loop after = function
966 [] -> failwith "disj shouldn't be empty" (*wrap n CTL.False*)
967 | [(nots,cur)] -> process_one nots cur
968 | (nots,cur)::rest -> wrapOr(process_one nots cur, loop after rest) in
969 loop after (preprocess_disj stmt_dots_list)
971 | Ast.Nest(stmt_dots,whencode,befaft) ->
973 statement_list stmt_dots used_after (a2n after) quantified guard in
978 statement_list sl used_after (a2n after) quantified true)
980 List.fold_left (function rest -> function cur -> wrapOr(cur,rest))
981 (statement_list stmt_dots used_after (a2n after) quantified true)
983 (match (after,guard&&(whencode=[])) with
986 List.map (process_bef_aft after quantified used_after n) befaft in
988 [] -> wrapAF(wrapOr(a,aftret))
993 (function rest -> function cur -> wrapOr(cur,rest))
995 wrapAU(left,wrapOr(a,aftret)))
997 let left = wrapOr(dots_pattern,wrapNot udots_pattern) in
999 List.map (process_bef_aft after quantified used_after n) befaft in
1007 (function rest -> function cur -> wrapOr(cur,rest))
1010 wrapAU(left,wrapOr(a,aftret))
1011 | (_,true) -> wrap n CTL.True
1012 | (_,false) -> wrapAG(wrapOr(dots_pattern,wrapNot udots_pattern)))
1013 | Ast.Dots((_,i,d),whencodes,t) ->
1017 (* no need for the fresh metavar, but ... is a bit wierd as a
1019 Some(make_match (make_meta_rule_elem d))
1022 (match whencodes with
1024 | Ast.WhenNot whencodes ->
1026 (statement_list whencodes used_after (a2n after) quantified
1028 | Ast.WhenAlways s ->
1029 [statement s used_after (a2n after) quantified true]) @
1031 (List.map (process_bef_aft after quantified used_after n) t)) in
1033 match whencodes with
1038 (function rest -> function cur -> wrapAnd(cur,rest))
1041 match (dot_code,phi2) with (* add - on dots, if any *)
1043 | (Some dotcode,None) -> Some dotcode
1044 | (None,Some whencode) -> Some whencode
1045 | (Some dotcode,Some whencode) -> Some(wrapAnd (dotcode,whencode)) in
1046 let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in
1047 (* add in the after code to make the result *)
1048 (match (after,phi3) with
1049 (Tail,Some whencode) -> wrapAU(whencode,wrapOr(exit,aftret))
1050 | (Tail,None) -> wrapAF(wrapOr(exit,aftret))
1051 | (After f,Some whencode) | (Guard f,Some whencode) ->
1052 wrapAU(whencode,wrapOr(f,aftret))
1053 | (After f,None) | (Guard f,None) -> wrapAF(wrapOr(f,aftret)))
1054 | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) ->
1055 let (hfvs,b1fvs,lbfvs,b2fvs,_,b3fvs,_,b4fvs,rbfvs) =
1056 seq_fvs5 quantified (Ast.get_fvs header) (Ast.get_fvs lbrace)
1057 (Ast.get_fvs decls) (Ast.get_fvs body) (Ast.get_fvs rbrace) in
1058 let function_header = quantify hfvs (make_match header) in
1059 let v = count_nested_braces stmt in
1060 let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in
1062 wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in
1064 let stripped_rbrace =
1065 match Ast.unwrap rbrace with
1066 Ast.SeqEnd((data,info,_)) ->
1068 (Ast.SeqEnd ((data,info,Ast.CONTEXT(Ast.NOTHING))))
1069 | _ -> failwith "unexpected close brace" in
1070 let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in
1071 let errorexit = wrap n (CTL.Pred (Lib_engine.ErrorExit,CTL.Control)) in
1072 wrapAnd(quantify rbfvs (make_match rbrace),
1073 wrapAU(make_match stripped_rbrace,
1074 wrapOr(exit,errorexit))) in
1075 let new_quantified3 =
1076 Common.union_set b1fvs
1077 (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
1078 let new_quantified4 = Common.union_set b4fvs new_quantified3 in
1088 (statement_list decls used_after
1090 (decl_to_not_decl n dots stmt
1093 (statement_list body used_after
1095 (make_seq_after end_brace after))
1096 new_quantified4 guard))))
1097 new_quantified3 guard)])))])
1098 | Ast.OptStm(stm) ->
1099 failwith "OptStm should have been compiled away\n";
1100 | Ast.UniqueStm(stm) ->
1101 failwith "arities not yet supported"
1102 | Ast.MultiStm(stm) ->
1103 failwith "arities not yet supported"
1104 | _ -> failwith "not supported"
1106 and process_bef_aft after quantified used_after ln = function
1107 Ast.WParen (re,n) ->
1108 let paren_pred = wrapPred ln (Lib_engine.Paren n,CTL.Control) in
1109 wrapAnd ln (make_raw_match ln re,paren_pred)
1110 | Ast.Other s -> statement s used_after (a2n after) quantified true
1111 | Ast.Other_dots d -> statement_list d used_after (a2n after) quantified true
1112 | Ast.OrOther_dots d -> statement_list d used_after Tail quantified true
1114 (* Returns a triple for each disj element. The first element of the triple is
1115 Some v if the triple element needs a name, and None otherwise. The second
1116 element is a list of names whose negations should be conjuncted with the
1117 term. The third element is the original term *)
1118 and (preprocess_disj :
1119 Ast.statement Ast.dots list ->
1120 (Ast.statement Ast.dots list * Ast.statement Ast.dots) list) =
1126 List.map (function r -> Unify_ast.unify_statement_dots cur r) rest in
1127 let processed = preprocess_disj rest in
1128 if List.exists (function Unify_ast.MAYBE -> true | _ -> false) template
1132 (function ((nots,r) as x) ->
1133 function Unify_ast.MAYBE -> (cur::nots,r) | Unify_ast.NO -> x)
1135 else ([], cur) :: processed
1137 (* --------------------------------------------------------------------- *)
1139 Phase 1: Use a hash table to identify formulas that appear more than once.
1140 Phase 2: Replace terms by variables.
1141 Phase 3: Drop lets to the point as close as possible to the uses of their
1145 (Hashtbl.create(50) :
1146 ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl,
1147 int ref (* count *) * string ref (* name *) * bool ref (* processed *))
1152 try Hashtbl.find formula_table phi
1154 let c = (ref 0,ref "",ref false) in
1155 Hashtbl.add formula_table phi c;
1159 let rec collect_duplicates f =
1161 match CTL.unwrap f with
1165 | CTL.Not(phi) -> collect_duplicates phi
1166 | CTL.Exists(v,phi) -> collect_duplicates phi
1167 | CTL.And(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1168 | CTL.Or(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1169 | CTL.SeqOr(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1170 | CTL.Implies(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1171 | CTL.AF(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1172 | CTL.AX(_,phi) -> collect_duplicates phi
1173 | CTL.AG(_,phi) -> collect_duplicates phi
1174 | CTL.AU(_,phi1,phi2,phi3,phi4) ->
1175 collect_duplicates phi1; collect_duplicates phi2;
1176 collect_duplicates phi3; collect_duplicates phi4
1177 | CTL.EF(_,phi) -> collect_duplicates phi
1178 | CTL.EX(_,phi) -> collect_duplicates phi
1179 | CTL.EG(_,phi) -> collect_duplicates phi
1180 | CTL.EU(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1181 | CTL.Uncheck(phi) -> collect_duplicates phi
1182 | _ -> failwith "not possible"
1184 let assign_variables _ =
1186 (function formula ->
1187 function (cell,str,_) -> if !cell > 1 then str := fresh_let_var())
1190 let rec replace_formulas dec f =
1191 let (ct,name,treated) = Hashtbl.find formula_table f in
1192 let real_ct = !ct - dec in
1199 let (acc,new_f) = replace_subformulas (dec + (real_ct - 1)) f in
1200 ((!name,new_f) :: acc, CTL.rewrap f (CTL.Ref !name))
1202 else ([],CTL.rewrap f (CTL.Ref !name))
1203 else replace_subformulas dec f
1205 and replace_subformulas dec f =
1206 match CTL.unwrap f with
1208 | CTL.True -> ([],f)
1209 | CTL.Pred(p) -> ([],f)
1211 let (acc,new_phi) = replace_formulas dec phi in
1212 (acc,CTL.rewrap f (CTL.Not(new_phi)))
1213 | CTL.Exists(v,phi) ->
1214 let (acc,new_phi) = replace_formulas dec phi in
1215 (acc,CTL.rewrap f (CTL.Exists(v,new_phi)))
1216 | CTL.And(phi1,phi2) ->
1217 let (acc1,new_phi1) = replace_formulas dec phi1 in
1218 let (acc2,new_phi2) = replace_formulas dec phi2 in
1219 (acc1@acc2,CTL.rewrap f (CTL.And(new_phi1,new_phi2)))
1220 | CTL.Or(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.Or(new_phi1,new_phi2)))
1224 | CTL.SeqOr(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.SeqOr(new_phi1,new_phi2)))
1228 | CTL.Implies(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.Implies(new_phi1,new_phi2)))
1232 | CTL.AF(dir,phi1,phi2) ->
1233 let (acc,new_phi1) = replace_formulas dec phi1 in
1234 let (acc,new_phi2) = replace_formulas dec phi2 in
1235 (acc,CTL.rewrap f (CTL.AF(dir,new_phi1,new_phi2)))
1236 | CTL.AX(dir,phi) ->
1237 let (acc,new_phi) = replace_formulas dec phi in
1238 (acc,CTL.rewrap f (CTL.AX(dir,new_phi)))
1239 | CTL.AG(dir,phi) ->
1240 let (acc,new_phi) = replace_formulas dec phi in
1241 (acc,CTL.rewrap f (CTL.AG(dir,new_phi)))
1242 | CTL.AU(dir,phi1,phi2,phi3,phi4) ->
1243 let (acc1,new_phi1) = replace_formulas dec phi1 in
1244 let (acc2,new_phi2) = replace_formulas dec phi2 in
1245 let (acc3,new_phi3) = replace_formulas dec phi3 in
1246 let (acc4,new_phi4) = replace_formulas dec phi4 in
1247 (acc1@acc2@acc3@acc4,
1248 CTL.rewrap f (CTL.AU(dir,new_phi1,new_phi2,new_phi3,new_phi4)))
1249 | CTL.EF(dir,phi) ->
1250 let (acc,new_phi) = replace_formulas dec phi in
1251 (acc,CTL.rewrap f (CTL.EF(dir,new_phi)))
1252 | CTL.EX(dir,phi) ->
1253 let (acc,new_phi) = replace_formulas dec phi in
1254 (acc,CTL.rewrap f (CTL.EX(dir,new_phi)))
1255 | CTL.EG(dir,phi) ->
1256 let (acc,new_phi) = replace_formulas dec phi in
1257 (acc,CTL.rewrap f (CTL.EG(dir,new_phi)))
1258 | CTL.EU(dir,phi1,phi2) ->
1259 let (acc1,new_phi1) = replace_formulas dec phi1 in
1260 let (acc2,new_phi2) = replace_formulas dec phi2 in
1261 (acc1@acc2,CTL.rewrap f (CTL.EU(dir,new_phi1,new_phi2)))
1262 | _ -> failwith "not possible"
1265 (Hashtbl.create(50) :
1266 ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl,
1267 string list (* fvs *) *
1268 string list (* intersection of fvs of subterms *))
1272 try let (fvs,_) = Hashtbl.find ctlfv_table f in fvs
1274 let ((fvs,_) as res) =
1275 match CTL.unwrap f with
1276 CTL.False | CTL.True | CTL.Pred(_) -> ([],[])
1277 | CTL.Not(phi) | CTL.Exists(_,phi)
1278 | CTL.AX(_,phi) | CTL.AG(_,phi)
1279 | CTL.EF(_,phi) | CTL.EX(_,phi) | CTL.EG(_,phi) -> (ctl_fvs phi,[])
1280 | CTL.AU(_,phi1,phi2,phi3,phi4) ->
1281 let phi1fvs = ctl_fvs phi1 in
1282 let phi2fvs = ctl_fvs phi2 in
1283 (* phi3 has the same fvs as phi1 and phi4 as phi2 *)
1284 (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1285 | CTL.And(phi1,phi2) | CTL.Or(phi1,phi2) | CTL.SeqOr(phi1,phi2)
1286 | CTL.Implies(phi1,phi2) | CTL.AF(_,phi1,phi2) | CTL.EU(_,phi1,phi2) ->
1287 let phi1fvs = ctl_fvs phi1 in
1288 let phi2fvs = ctl_fvs phi2 in
1289 (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1290 | CTL.Ref(v) -> ([v],[v])
1291 | CTL.Let(v,term,body) ->
1292 let phi1fvs = ctl_fvs term in
1293 let phi2fvs = Common.minus_set (ctl_fvs body) [v] in
1294 (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) in
1295 Hashtbl.add ctlfv_table f res;
1298 let rev_order_bindings b =
1301 (function (nm,term) ->
1302 let (fvs,_) = Hashtbl.find ctlfv_table term in (nm,fvs,term))
1304 let rec loop bound = function
1307 let (now_bound,still_unbound) =
1308 List.partition (function (_,fvs,_) -> subset fvs bound)
1310 let get_names = List.map (function (x,_,_) -> x) in
1311 now_bound @ (loop ((get_names now_bound) @ bound) still_unbound) in
1314 let drop_bindings b f = (* innermost bindings first in b *)
1315 let process_binary f ffvs inter nm term fail =
1316 if List.mem nm inter
1317 then CTL.rewrap f (CTL.Let(nm,term,f))
1318 else CTL.rewrap f (fail()) in
1320 let _ = ctl_fvs f in Hashtbl.find ctlfv_table f in
1321 let rec drop_one nm term f =
1322 match CTL.unwrap f with
1326 | CTL.Not(phi) -> CTL.rewrap f (CTL.Not(drop_one nm term phi))
1327 | CTL.Exists(v,phi) -> CTL.rewrap f (CTL.Exists(v,drop_one nm term phi))
1328 | CTL.And(phi1,phi2) ->
1329 let (ffvs,inter) = find_fvs f in
1330 process_binary f ffvs inter nm term
1331 (function _ -> CTL.And(drop_one nm term phi1,drop_one nm term phi2))
1332 | CTL.Or(phi1,phi2) ->
1333 let (ffvs,inter) = find_fvs f in
1334 process_binary f ffvs inter nm term
1335 (function _ -> CTL.Or(drop_one nm term phi1,drop_one nm term phi2))
1336 | CTL.SeqOr(phi1,phi2) ->
1337 let (ffvs,inter) = find_fvs f in
1338 process_binary f ffvs inter nm term
1340 CTL.SeqOr(drop_one nm term phi1,drop_one nm term phi2))
1341 | CTL.Implies(phi1,phi2) ->
1342 let (ffvs,inter) = find_fvs f in
1343 process_binary f ffvs inter nm term
1345 CTL.Implies(drop_one nm term phi1,drop_one nm term phi2))
1346 | CTL.AF(dir,phi1,phi2) ->
1347 let (ffvs,inter) = find_fvs f in
1348 process_binary f ffvs inter nm term
1350 CTL.AF(dir,drop_one nm term phi1,drop_one nm term phi2))
1351 | CTL.AX(dir,phi) ->
1352 CTL.rewrap f (CTL.AX(dir,drop_one nm term phi))
1353 | CTL.AG(dir,phi) -> CTL.rewrap f (CTL.AG(dir,drop_one nm term phi))
1354 | CTL.AU(dir,phi1,phi2,phi3,phi4) ->
1355 let (ffvs,inter) = find_fvs f in
1356 process_binary f ffvs inter nm term
1358 CTL.AU(dir,drop_one nm term phi1,drop_one nm term phi2,
1359 drop_one nm term phi3,drop_one nm term phi4))
1360 | CTL.EF(dir,phi) -> CTL.rewrap f (CTL.EF(dir,drop_one nm term phi))
1361 | CTL.EX(dir,phi) ->
1362 CTL.rewrap f (CTL.EX(dir,drop_one nm term phi))
1363 | CTL.EG(dir,phi) -> CTL.rewrap f (CTL.EG(dir,drop_one nm term phi))
1364 | CTL.EU(dir,phi1,phi2) ->
1365 let (ffvs,inter) = find_fvs f in
1366 process_binary f ffvs inter nm term
1368 CTL.EU(dir,drop_one nm term phi1,drop_one nm term phi2))
1369 | (CTL.Ref(v) as x) -> process_binary f [v] [v] nm term (function _ -> x)
1370 | CTL.Let(v,term1,body) ->
1371 let (ffvs,inter) = find_fvs f in
1372 process_binary f ffvs inter nm term
1374 CTL.Let(v,drop_one nm term term1,drop_one nm term body)) in
1376 (function processed -> function (nm,_,term) -> drop_one nm term processed)
1380 failwith "this code should not be used!!!"(*;
1381 Hashtbl.clear formula_table;
1382 Hashtbl.clear ctlfv_table;
1383 (* create a count of the number of occurrences of each subformula *)
1384 collect_duplicates f;
1385 (* give names to things that appear more than once *)
1387 (* replace duplicated formulas by their variables *)
1388 let (bindings,new_f) = replace_formulas 0 f in
1389 (* collect fvs of terms in bindings and new_f *)
1390 List.iter (function f -> let _ = ctl_fvs f in ())
1391 (new_f::(List.map (function (_,term) -> term) bindings));
1392 (* sort bindings with uses before defs *)
1393 let bindings = rev_order_bindings bindings in
1394 (* insert bindings as lets into the formula *)
1395 let res = drop_bindings bindings new_f in
1398 (* --------------------------------------------------------------------- *)
1399 (* Function declaration *)
1401 let top_level used_after t =
1402 match Ast.unwrap t with
1403 Ast.DECL(decl) -> failwith "not supported decl"
1404 | Ast.INCLUDE(inc,s) ->
1405 (* no indication of whether inc or s is modified *)
1406 wrap 0 (CTL.Pred((Lib_engine.Include(inc,s),CTL.Control)))
1407 | Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
1408 | Ast.FUNCTION(stmt) ->
1409 (*Printf.printf "orig\n";
1410 Pretty_print_cocci.statement "" stmt;
1411 Format.print_newline();*)
1412 let unopt = elim_opt.V.rebuilder_statement stmt in
1413 (*Printf.printf "unopt\n";
1414 Pretty_print_cocci.statement "" unopt;
1415 Format.print_newline();*)
1416 let unopt = preprocess_dots_e unopt in
1418 (statement unopt used_after Tail [] false)
1419 | Ast.CODE(stmt_dots) ->
1420 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
1421 let unopt = preprocess_dots unopt in
1423 (statement_list unopt used_after Tail [] false)
1424 | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords"
1426 (* --------------------------------------------------------------------- *)
1430 let bind x y = x or y in
1431 let option_default = false in
1432 let mcode r x = false in
1433 let statement r k s =
1434 match Ast.unwrap s with Ast.Dots(_,_,_) -> true | _ -> k s in
1435 let continue r k e = k e in
1436 let stop r k e = false in
1438 V.combiner bind option_default
1439 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
1440 continue continue continue
1441 stop stop stop stop stop stop stop statement continue continue in
1442 res.V.combiner_top_level
1444 (* --------------------------------------------------------------------- *)
1447 let asttoctl l used_after =
1454 match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
1456 List.map2 top_level used_after l
1458 let pp_cocci_predicate (pred,modif) =
1459 Pretty_print_engine.pp_predicate pred
1461 let cocci_predicate_to_string (pred,modif) =
1462 Pretty_print_engine.predicate_to_string pred