2 * Copyright 2005-2008, 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 (* for MINUS and CONTEXT, pos is always None in this file *)
24 (*search for require*)
25 (* true = don't see all matched nodes, only modified ones *)
26 let onlyModif = ref true(*false*)
28 type ex = Exists | Forall | ReverseForall
29 let exists = ref Forall
31 module Ast = Ast_cocci
32 module V = Visitor_ast
35 let warning s = Printf.fprintf stderr "warning: %s\n" s
37 type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
39 (cocci_predicate,Ast.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl
41 let union = Common.union_set
42 let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1
43 let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1
45 let foldl1 f xs = List.fold_left f (List.hd xs) (List.tl xs)
47 let xs = List.rev xs in List.fold_left f (List.hd xs) (List.tl xs)
49 let used_after = ref ([] : Ast.meta_name list)
50 let guard_to_strict guard = if guard then CTL.NONSTRICT else CTL.STRICT
52 let saved = ref ([] : Ast.meta_name list)
54 let string2var x = ("",x)
56 (* --------------------------------------------------------------------- *)
57 (* predicates matching various nodes in the graph *)
61 (CTL.False,_) | (_,CTL.False) -> CTL.False
62 | (CTL.True,a) | (a,CTL.True) -> a
67 (CTL.True,_) | (_,CTL.True) -> CTL.True
68 | (CTL.False,a) | (a,CTL.False) -> a
73 (CTL.True,_) | (_,CTL.True) -> CTL.True
74 | (CTL.False,a) | (a,CTL.False) -> a
79 (CTL.True,_) | (_,CTL.True) -> CTL.True
80 | (CTL.False,a) | (a,CTL.False) -> a
83 let ctl_not = function
85 | CTL.False -> CTL.True
88 let ctl_ax s = function
90 | CTL.False -> CTL.False
93 Exists -> CTL.EX(CTL.FORWARD,x)
94 | Forall -> CTL.AX(CTL.FORWARD,s,x)
95 | ReverseForall -> failwith "not supported"
97 let ctl_ax_absolute s = function
99 | CTL.False -> CTL.False
100 | x -> CTL.AX(CTL.FORWARD,s,x)
102 let ctl_ex = function
104 | CTL.False -> CTL.False
105 | x -> CTL.EX(CTL.FORWARD,x)
107 (* This stays being AX even for sgrep_mode, because it is used to identify
108 the structure of the term, not matching the pattern. *)
109 let ctl_back_ax = function
111 | CTL.False -> CTL.False
112 | x -> CTL.AX(CTL.BACKWARD,CTL.NONSTRICT,x)
114 let ctl_back_ex = function
116 | CTL.False -> CTL.False
117 | x -> CTL.EX(CTL.BACKWARD,x)
119 let ctl_ef = function
121 | CTL.False -> CTL.False
122 | x -> CTL.EF(CTL.FORWARD,x)
124 let ctl_ag s = function
126 | CTL.False -> CTL.False
127 | x -> CTL.AG(CTL.FORWARD,s,x)
130 match (x,!exists) with
131 (CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y)
132 | (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y)
133 | (CTL.True,ReverseForall) -> failwith "not supported"
134 | (_,Exists) -> CTL.EU(CTL.FORWARD,x,y)
135 | (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y)
136 | (_,ReverseForall) -> failwith "not supported"
138 let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *)
140 (match (x,!exists) with
141 (CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y)
142 | (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y)
143 | (CTL.True,ReverseForall) -> failwith "not supported"
144 | (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y)
145 | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y)
146 | (_,ReverseForall) -> failwith "not supported")
148 let ctl_uncheck = function
150 | CTL.False -> CTL.False
153 let label_pred_maker = function
155 | Some (label_var,used) ->
157 CTL.Pred(Lib_engine.PrefixLabel(label_var),CTL.Control)
159 let bclabel_pred_maker = function
161 | Some (label_var,used) ->
163 CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control)
165 let predmaker guard pred label =
166 ctl_and (guard_to_strict guard) (CTL.Pred pred) (label_pred_maker label)
168 let aftpred = predmaker false (Lib_engine.After, CTL.Control)
169 let retpred = predmaker false (Lib_engine.Return, CTL.Control)
170 let funpred = predmaker false (Lib_engine.FunHeader, CTL.Control)
171 let toppred = predmaker false (Lib_engine.Top, CTL.Control)
172 let exitpred = predmaker false (Lib_engine.ErrorExit, CTL.Control)
173 let endpred = predmaker false (Lib_engine.Exit, CTL.Control)
174 let gotopred = predmaker false (Lib_engine.Goto, CTL.Control)
175 let inlooppred = predmaker false (Lib_engine.InLoop, CTL.Control)
176 let truepred = predmaker false (Lib_engine.TrueBranch, CTL.Control)
177 let falsepred = predmaker false (Lib_engine.FalseBranch, CTL.Control)
178 let fallpred = predmaker false (Lib_engine.FallThrough, CTL.Control)
180 let aftret label_var f = ctl_or (aftpred label_var) (exitpred label_var)
186 Printf.sprintf "r%d" cur
188 (* --------------------------------------------------------------------- *)
189 (* --------------------------------------------------------------------- *)
190 (* Eliminate OptStm *)
192 (* for optional thing with nothing after, should check that the optional thing
193 never occurs. otherwise the matching stops before it occurs *)
196 let donothing r k e = k e in
199 List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in
202 List.fold_left Common.union_set [] (List.map Ast.get_mfvs l) in
205 List.fold_left Common.union_set [] (List.map Ast.get_fresh l) in
207 let inheritedlist l =
208 List.fold_left Common.union_set [] (List.map Ast.get_inherited l) in
211 List.fold_left Common.union_set [] (List.map Ast.get_saved l) in
214 (fvlist l, mfvlist l, freshlist l, inheritedlist l, savedlist l) in
216 let rec dots_list unwrapped wrapped =
217 match (unwrapped,wrapped) with
220 | (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
222 | (Ast.Nest(_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
224 let l = Ast.get_line stm in
225 let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
226 let new_rest2 = dots_list urest rest in
227 let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) =
228 varlists new_rest1 in
229 let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) =
230 varlists new_rest2 in
234 [{(Ast.make_term(Ast.DOTS(new_rest1))) with
236 Ast.free_vars = fv_rest1;
237 Ast.minus_free_vars = mfv_rest1;
238 Ast.fresh_vars = fresh_rest1;
239 Ast.inherited = inherited_rest1;
240 Ast.saved_witness = s1};
241 {(Ast.make_term(Ast.DOTS(new_rest2))) with
243 Ast.free_vars = fv_rest2;
244 Ast.minus_free_vars = mfv_rest2;
245 Ast.fresh_vars = fresh_rest2;
246 Ast.inherited = inherited_rest2;
247 Ast.saved_witness = s2}])) with
249 Ast.free_vars = fv_rest1;
250 Ast.minus_free_vars = mfv_rest1;
251 Ast.fresh_vars = fresh_rest1;
252 Ast.inherited = inherited_rest1;
253 Ast.saved_witness = s1}]
255 | (Ast.OptStm(stm)::urest,_::rest) ->
256 let l = Ast.get_line stm in
257 let new_rest1 = dots_list urest rest in
258 let new_rest2 = stm::new_rest1 in
259 let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) =
260 varlists new_rest1 in
261 let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) =
262 varlists new_rest2 in
265 [{(Ast.make_term(Ast.DOTS(new_rest2))) with
267 Ast.free_vars = fv_rest2;
268 Ast.minus_free_vars = mfv_rest2;
269 Ast.fresh_vars = fresh_rest2;
270 Ast.inherited = inherited_rest2;
271 Ast.saved_witness = s2};
272 {(Ast.make_term(Ast.DOTS(new_rest1))) with
274 Ast.free_vars = fv_rest1;
275 Ast.minus_free_vars = mfv_rest1;
276 Ast.fresh_vars = fresh_rest1;
277 Ast.inherited = inherited_rest1;
278 Ast.saved_witness = s1}])) with
280 Ast.free_vars = fv_rest2;
281 Ast.minus_free_vars = mfv_rest2;
282 Ast.fresh_vars = fresh_rest2;
283 Ast.inherited = inherited_rest2;
284 Ast.saved_witness = s2}]
286 | ([Ast.Dots(_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
287 let l = Ast.get_line stm in
288 let fv_stm = Ast.get_fvs stm in
289 let mfv_stm = Ast.get_mfvs stm in
290 let fresh_stm = Ast.get_fresh stm in
291 let inh_stm = Ast.get_inherited stm in
292 let saved_stm = Ast.get_saved stm in
293 let fv_d1 = Ast.get_fvs d1 in
294 let mfv_d1 = Ast.get_mfvs d1 in
295 let fresh_d1 = Ast.get_fresh d1 in
296 let inh_d1 = Ast.get_inherited d1 in
297 let saved_d1 = Ast.get_saved d1 in
298 let fv_both = Common.union_set fv_stm fv_d1 in
299 let mfv_both = Common.union_set mfv_stm mfv_d1 in
300 let fresh_both = Common.union_set fresh_stm fresh_d1 in
301 let inh_both = Common.union_set inh_stm inh_d1 in
302 let saved_both = Common.union_set saved_stm saved_d1 in
306 [{(Ast.make_term(Ast.DOTS([stm]))) with
308 Ast.free_vars = fv_stm;
309 Ast.minus_free_vars = mfv_stm;
310 Ast.fresh_vars = fresh_stm;
311 Ast.inherited = inh_stm;
312 Ast.saved_witness = saved_stm};
313 {(Ast.make_term(Ast.DOTS([d1]))) with
315 Ast.free_vars = fv_d1;
316 Ast.minus_free_vars = mfv_d1;
317 Ast.fresh_vars = fresh_d1;
318 Ast.inherited = inh_d1;
319 Ast.saved_witness = saved_d1}])) with
321 Ast.free_vars = fv_both;
322 Ast.minus_free_vars = mfv_both;
323 Ast.fresh_vars = fresh_both;
324 Ast.inherited = inh_both;
325 Ast.saved_witness = saved_both}]
327 | ([Ast.Nest(_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
328 let l = Ast.get_line stm in
329 let rw = Ast.rewrap stm in
330 let rwd = Ast.rewrap stm in
331 let dots = Ast.Dots(Ast.make_mcode "...",[],[],[]) in
333 [rwd(Ast.DOTS([stm]));
334 {(Ast.make_term(Ast.DOTS([rw dots])))
335 with Ast.node_line = l}])]
337 | (_::urest,stm::rest) -> stm :: (dots_list urest rest)
338 | _ -> failwith "not possible" in
340 let stmtdotsfn r k d =
343 (match Ast.unwrap d with
344 Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
345 | Ast.CIRCLES(l) -> failwith "elimopt: not supported"
346 | Ast.STARS(l) -> failwith "elimopt: not supported") in
349 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
351 donothing donothing stmtdotsfn donothing
352 donothing donothing donothing donothing donothing donothing donothing
353 donothing donothing donothing donothing donothing
355 (* --------------------------------------------------------------------- *)
356 (* after management *)
357 (* We need Guard for the following case:
366 Here the inner <... b ...> should not go past foo. But foo is not the
367 "after" of the body of the outer nest, because we don't want to search for
368 it in the case where the body of the outer nest ends in something other
369 than dots or a nest. *)
371 (* what is the difference between tail and end??? *)
373 type after = After of formula | Guard of formula | Tail | End | VeryEnd
375 let a2n = function After x -> Guard x | a -> a
378 let pp_pred (x,_) = Pretty_print_engine.pp_predicate x in
379 let pp_meta (_,x) = Common.pp x in
380 Pretty_print_ctl.pp_ctl (pp_pred,pp_meta) false x;
381 Format.print_newline()
383 let print_after = function
384 After ctl -> Printf.printf "After:\n"; print_ctl ctl
385 | Guard ctl -> Printf.printf "Guard:\n"; print_ctl ctl
386 | Tail -> Printf.printf "Tail\n"
387 | VeryEnd -> Printf.printf "Very End\n"
388 | End -> Printf.printf "End\n"
390 (* --------------------------------------------------------------------- *)
393 let fresh_var _ = string2var "_v"
394 let fresh_pos _ = string2var "_pos" (* must be a constant *)
396 let fresh_metavar _ = "_S"
398 (* fvinfo is going to end up being from the whole associated statement.
399 it would be better if it were just the free variables in d, but free_vars.ml
400 doesn't keep track of free variables on + code *)
401 let make_meta_rule_elem d fvinfo =
402 let nm = fresh_metavar() in
403 Ast.make_meta_rule_elem nm d fvinfo
405 let get_unquantified quantified vars =
406 List.filter (function x -> not (List.mem x quantified)) vars
408 let make_seq guard l =
409 let s = guard_to_strict guard in
410 foldr1 (function rest -> function cur -> ctl_and s cur (ctl_ax s rest)) l
412 let make_seq_after2 guard first rest =
413 let s = guard_to_strict guard in
415 After rest -> ctl_and s first (ctl_ax s (ctl_ax s rest))
418 let make_seq_after guard first rest =
420 After rest -> make_seq guard [first;rest]
423 let opt_and guard first rest =
424 let s = guard_to_strict guard in
427 | Some first -> ctl_and s first rest
429 let and_after guard first rest =
430 let s = guard_to_strict guard in
431 match rest with After rest -> ctl_and s first rest | _ -> first
434 let bind x y = x or y in
435 let option_default = false in
436 let mcode r (_,_,kind,metapos) =
439 Ast.MINUS(_,_) -> true
440 | Ast.PLUS -> failwith "not possible"
441 | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
444 Ast.MetaPos(_,_,_,_,_) -> true
445 | Ast.NoMetaPos -> false in
447 let do_nothing r k e = k e in
448 let rule_elem r k re =
450 match Ast.unwrap re with
451 Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
452 bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
453 | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
456 V.combiner bind option_default
457 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
459 do_nothing do_nothing do_nothing do_nothing
460 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
461 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
462 recursor.V.combiner_rule_elem
464 (* code is not a DisjRuleElem *)
465 let make_match label guard code =
466 let v = fresh_var() in
467 let matcher = Lib_engine.Match(code) in
468 if contains_modif code && not guard
469 then CTL.Exists(true,v,predmaker guard (matcher,CTL.Modif v) label)
471 let iso_info = !Flag.track_iso_usage && not (Ast.get_isos code = []) in
472 (match (iso_info,!onlyModif,guard,
473 intersect !used_after (Ast.get_fvs code)) with
474 (false,true,_,[]) | (_,_,true,_) ->
475 predmaker guard (matcher,CTL.Control) label
476 | _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))
478 let make_raw_match label guard code =
479 predmaker guard (Lib_engine.Match(code),CTL.Control) label
481 let rec seq_fvs quantified = function
484 let t1fvs = get_unquantified quantified fv1 in
486 List.fold_left Common.union_set []
487 (List.map (get_unquantified quantified) fvs) in
488 let bothfvs = Common.inter_set t1fvs termfvs in
489 let t1onlyfvs = Common.minus_set t1fvs bothfvs in
490 let new_quantified = Common.union_set bothfvs quantified in
491 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs)
496 function code -> CTL.Exists (not guard && List.mem cur !saved,cur,code))
498 let non_saved_quantify =
500 (function cur -> function code -> CTL.Exists (false,cur,code))
502 let intersectll lst nested_list =
503 List.filter (function x -> List.exists (List.mem x) nested_list) lst
505 (* --------------------------------------------------------------------- *)
506 (* Count depth of braces. The translation of a closed brace appears deeply
507 nested within the translation of the sequence term, so the name of the
508 paren var has to take into account the names of the nested braces. On the
509 other hand the close brace does not escape, so we don't have to take into
510 account other paren variable names. *)
512 (* called repetitively, which is inefficient, but less trouble than adding a
513 new field to Seq and FunDecl *)
514 let count_nested_braces s =
515 let bind x y = max x y in
516 let option_default = 0 in
517 let stmt_count r k s =
518 match Ast.unwrap s with
519 Ast.Seq(_,_,_,_) | Ast.FunDecl(_,_,_,_,_) -> (k s) + 1
521 let donothing r k e = k e in
523 let recursor = V.combiner bind option_default
524 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
526 donothing donothing donothing donothing
527 donothing donothing donothing donothing donothing donothing
528 donothing donothing stmt_count donothing donothing donothing in
529 let res = string_of_int (recursor.V.combiner_statement s) in
533 let get_label_ctr _ =
534 let cur = !labelctr in
536 string2var (Printf.sprintf "l%d" cur)
538 (* --------------------------------------------------------------------- *)
539 (* annotate dots with before and after neighbors *)
541 let print_bef_aft = function
543 Printf.printf "bef/aft\n";
544 Pretty_print_cocci.rule_elem "" re;
545 Format.print_newline()
547 Printf.printf "bef/aft\n";
548 Pretty_print_cocci.statement "" s;
549 Format.print_newline()
550 | Ast.Other_dots d ->
551 Printf.printf "bef/aft\n";
552 Pretty_print_cocci.statement_dots d;
553 Format.print_newline()
555 (* [] can only occur if we are in a disj, where it comes from a ? In that
556 case, we want to use a, which accumulates all of the previous patterns in
558 let rec get_before_elem sl a =
559 match Ast.unwrap sl with
563 [] -> ([],Common.Right a)
565 let (e,ea) = get_before_e e a in
568 let (e,ea) = get_before_e e a in
569 let (sl,sla) = loop sl ea in
571 let (l,a) = loop x a in
572 (Ast.rewrap sl (Ast.DOTS(l)),a)
573 | Ast.CIRCLES(x) -> failwith "not supported"
574 | Ast.STARS(x) -> failwith "not supported"
576 and get_before sl a =
577 match get_before_elem sl a with
578 (term,Common.Left x) -> (term,x)
579 | (term,Common.Right x) -> (term,x)
581 and get_before_whencode wc =
584 Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w
585 | Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w
586 | Ast.WhenModifier(x) -> Ast.WhenModifier(x)
587 | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
588 | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
591 and get_before_e s a =
592 match Ast.unwrap s with
593 Ast.Dots(d,w,_,aft) ->
594 (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)
595 | Ast.Nest(stmt_dots,w,multi,_,aft) ->
596 let w = get_before_whencode w in
597 let (sd,_) = get_before stmt_dots a in
603 Unify_ast.unify_statement_dots
604 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
606 Unify_ast.MAYBE -> false
608 | Ast.Other_dots a ->
609 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
611 Unify_ast.MAYBE -> false
615 (Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
616 | Ast.Disj(stmt_dots_list) ->
618 List.split (List.map (function e -> get_before e a) stmt_dots_list) in
619 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
621 (match Ast.unwrap ast with
622 Ast.MetaStmt(_,_,_,_) -> (s,[])
623 | _ -> (s,[Ast.Other s]))
624 | Ast.Seq(lbrace,decls,body,rbrace) ->
625 let index = count_nested_braces s in
626 let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
627 let (bd,_) = get_before body dea in
628 (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
629 [Ast.WParen(rbrace,index)])
630 | Ast.Define(header,body) ->
631 let (body,_) = get_before body [] in
632 (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
633 | Ast.IfThen(ifheader,branch,aft) ->
634 let (br,_) = get_before_e branch [] in
635 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s])
636 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
637 let (br1,_) = get_before_e branch1 [] in
638 let (br2,_) = get_before_e branch2 [] in
639 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
640 | Ast.While(header,body,aft) ->
641 let (bd,_) = get_before_e body [] in
642 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
643 | Ast.For(header,body,aft) ->
644 let (bd,_) = get_before_e body [] in
645 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
646 | Ast.Do(header,body,tail) ->
647 let (bd,_) = get_before_e body [] in
648 (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
649 | Ast.Iterator(header,body,aft) ->
650 let (bd,_) = get_before_e body [] in
651 (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
652 | Ast.Switch(header,lb,cases,rb) ->
655 (function case_line ->
656 match Ast.unwrap case_line with
657 Ast.CaseLine(header,body) ->
658 let (body,_) = get_before body [] in
659 Ast.rewrap case_line (Ast.CaseLine(header,body))
660 | Ast.OptCase(case_line) -> failwith "not supported")
662 (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
663 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
664 let (de,dea) = get_before decls [] in
665 let (bd,_) = get_before body dea in
666 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
668 Pretty_print_cocci.statement "" s; Format.print_newline();
669 failwith "get_before_e: not supported"
671 let rec get_after sl a =
672 match Ast.unwrap sl with
678 let (sl,sla) = loop sl in
679 let (e,ea) = get_after_e e sla in
681 let (l,a) = loop x in
682 (Ast.rewrap sl (Ast.DOTS(l)),a)
683 | Ast.CIRCLES(x) -> failwith "not supported"
684 | Ast.STARS(x) -> failwith "not supported"
686 and get_after_whencode a wc =
689 Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w
690 | Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w
691 | Ast.WhenModifier(x) -> Ast.WhenModifier(x)
692 | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
693 | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
696 and get_after_e s a =
697 match Ast.unwrap s with
698 Ast.Dots(d,w,bef,_) ->
699 (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)
700 | Ast.Nest(stmt_dots,w,multi,bef,_) ->
701 let w = get_after_whencode a w in
702 let (sd,_) = get_after stmt_dots a in
708 Unify_ast.unify_statement_dots
709 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
711 Unify_ast.MAYBE -> false
713 | Ast.Other_dots a ->
714 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
716 Unify_ast.MAYBE -> false
720 (Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
721 | Ast.Disj(stmt_dots_list) ->
723 List.split (List.map (function e -> get_after e a) stmt_dots_list) in
724 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
726 (match Ast.unwrap ast with
727 Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots _,i) ->
728 (* check "after" information for metavar optimization *)
729 (* if the error is not desired, could just return [], then
730 the optimization (check for EF) won't take place *)
734 (match Ast.unwrap x with
735 Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
737 "dots/nest not allowed before and after stmt metavar"
739 | Ast.Other_dots x ->
740 (match Ast.undots x with
742 (match Ast.unwrap x with
743 Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
745 ("dots/nest not allowed before and after stmt "^
754 (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
755 | Ast.MetaStmt(_,_,_,_) -> (s,[])
756 | _ -> (s,[Ast.Other s]))
757 | Ast.Seq(lbrace,decls,body,rbrace) ->
758 let index = count_nested_braces s in
759 let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
760 let (de,_) = get_after decls bda in
761 (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
762 [Ast.WParen(lbrace,index)])
763 | Ast.Define(header,body) ->
764 let (body,_) = get_after body a in
765 (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
766 | Ast.IfThen(ifheader,branch,aft) ->
767 let (br,_) = get_after_e branch a in
768 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s])
769 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
770 let (br1,_) = get_after_e branch1 a in
771 let (br2,_) = get_after_e branch2 a in
772 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
773 | Ast.While(header,body,aft) ->
774 let (bd,_) = get_after_e body a in
775 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
776 | Ast.For(header,body,aft) ->
777 let (bd,_) = get_after_e body a in
778 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
779 | Ast.Do(header,body,tail) ->
780 let (bd,_) = get_after_e body a in
781 (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
782 | Ast.Iterator(header,body,aft) ->
783 let (bd,_) = get_after_e body a in
784 (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
785 | Ast.Switch(header,lb,cases,rb) ->
788 (function case_line ->
789 match Ast.unwrap case_line with
790 Ast.CaseLine(header,body) ->
791 let (body,_) = get_after body [] in
792 Ast.rewrap case_line (Ast.CaseLine(header,body))
793 | Ast.OptCase(case_line) -> failwith "not supported")
795 (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
796 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
797 let (bd,bda) = get_after body [] in
798 let (de,_) = get_after decls bda in
799 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
800 | _ -> failwith "get_after_e: not supported"
802 let preprocess_dots sl =
803 let (sl,_) = get_before sl [] in
804 let (sl,_) = get_after sl [] in
807 let preprocess_dots_e sl =
808 let (sl,_) = get_before_e sl [] in
809 let (sl,_) = get_after_e sl [] in
812 (* --------------------------------------------------------------------- *)
813 (* various return_related things *)
815 let rec ends_in_return stmt_list =
816 match Ast.unwrap stmt_list with
818 (match List.rev x with
820 (match Ast.unwrap x with
823 match Ast.unwrap x with
824 Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true
825 | Ast.DisjRuleElem((_::_) as l) -> List.for_all loop l
828 | Ast.Disj(disjs) -> List.for_all ends_in_return disjs
831 | Ast.CIRCLES(x) -> failwith "not supported"
832 | Ast.STARS(x) -> failwith "not supported"
834 (* --------------------------------------------------------------------- *)
837 let exptymatch l make_match make_guard_match =
838 let pos = fresh_pos() in
839 let matches_guard_matches =
842 let pos = Ast.make_mcode pos in
843 (make_match (Ast.set_pos x (Some pos)),
844 make_guard_match (Ast.set_pos x (Some pos))))
846 let (matches,guard_matches) = List.split matches_guard_matches in
847 let rec suffixes = function
849 | x::xs -> xs::(suffixes xs) in
850 let prefixes = List.rev (suffixes (List.rev guard_matches)) in
851 let info = (* not null *)
857 ctl_and CTL.NONSTRICT matcher
859 (ctl_uncheck (List.fold_left ctl_or_fl CTL.False negates)))))
861 CTL.InnerAnd(List.fold_left ctl_or_fl CTL.False (List.rev info))
863 (* code might be a DisjRuleElem, in which case we break it apart
864 code might contain an Exp or Ty
865 this one pushes the quantifier inwards *)
866 let do_re_matches label guard res quantified minus_quantified =
867 let make_guard_match x =
868 let stmt_fvs = Ast.get_mfvs x in
869 let fvs = get_unquantified minus_quantified stmt_fvs in
870 non_saved_quantify fvs (make_match None true x) in
872 let stmt_fvs = Ast.get_fvs x in
873 let fvs = get_unquantified quantified stmt_fvs in
874 quantify guard fvs (make_match None guard x) in
875 ctl_and CTL.NONSTRICT (label_pred_maker label)
876 (match List.map Ast.unwrap res with
877 [] -> failwith "unexpected empty disj"
878 | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match
879 | Ast.Ty(t)::rest -> exptymatch res make_match make_guard_match
881 if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
883 then failwith "unexpected exp or ty";
884 List.fold_left ctl_seqor CTL.False
885 (List.rev (List.map make_match res)))
887 (* code might be a DisjRuleElem, in which case we break it apart
888 code doesn't contain an Exp or Ty
889 this one is for use when it is not practical to push the quantifier inwards
891 let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl =
892 match Ast.unwrap code with
893 Ast.DisjRuleElem(res) ->
894 let make_match = make_match None guard in
895 let orop = if guard then ctl_or else ctl_seqor in
896 ctl_and CTL.NONSTRICT (label_pred_maker label)
897 (List.fold_left orop CTL.False (List.map make_match res))
898 | _ -> make_match label guard code
900 (* --------------------------------------------------------------------- *)
901 (* control structures *)
903 let end_control_structure fvs header body after_pred
904 after_checks no_after_checks (afvs,afresh,ainh,aft) after label guard =
905 (* aft indicates what is added after the whole if, which has to be added
907 let (aft_needed,after_branch) =
909 Ast.CONTEXT(_,Ast.NOTHING) ->
910 (false,make_seq_after2 guard after_pred after)
913 make_match label guard
914 (make_meta_rule_elem aft (afvs,afresh,ainh)) in
916 make_seq_after guard after_pred
917 (After(make_seq_after guard match_endif after))) in
918 let body = body after_branch in
919 let s = guard_to_strict guard in
924 (match (after,aft_needed) with
925 (After _,_) (* pattern doesn't end here *)
926 | (_,true) (* + code added after *) -> after_checks
927 | _ -> no_after_checks)
928 (ctl_ax_absolute s body)))
930 let ifthen ifheader branch ((afvs,_,_,_) as aft) after
931 quantified minus_quantified label llabel slabel recurse make_match guard =
932 (* "if (test) thn" becomes:
933 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
935 "if (test) thn; after" becomes:
936 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
941 match seq_fvs quantified
942 [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with
943 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
944 | _ -> failwith "not possible" in
945 let new_quantified = Common.union_set bfvs quantified in
947 match seq_fvs minus_quantified
948 [Ast.get_mfvs ifheader;Ast.get_mfvs branch;[]] with
949 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
950 | _ -> failwith "not possible" in
951 let new_mquantified = Common.union_set mbfvs minus_quantified in
953 let if_header = quantify guard efvs (make_match ifheader) in
954 (* then branch and after *)
955 let lv = get_label_ctr() in
956 let used = ref false in
959 [truepred label; recurse branch Tail new_quantified new_mquantified
960 (Some (lv,used)) llabel slabel guard] in
961 let after_pred = aftpred label in
962 let or_cases after_branch =
963 ctl_or true_branch (ctl_or (fallpred label) after_branch) in
964 let (if_header,wrapper) =
967 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
968 (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
969 (function body -> quantify true [lv] body))
970 else (if_header,function x -> x) in
972 (end_control_structure bfvs if_header or_cases after_pred
973 (Some(ctl_ex after_pred)) None aft after label guard)
975 let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
976 quantified minus_quantified label llabel slabel recurse make_match guard =
977 (* "if (test) thn else els" becomes:
978 if(test) & AX((TrueBranch & AX thn) v
979 (FalseBranch & AX (else & AX els)) v After)
982 "if (test) thn else els; after" becomes:
983 if(test) & AX((TrueBranch & AX thn) v
984 (FalseBranch & AX (else & AX els)) v
985 (After & AXAX after))
990 let (e1fvs,b1fvs,s1fvs) =
991 match seq_fvs quantified
992 [Ast.get_fvs ifheader;Ast.get_fvs branch1;afvs] with
993 [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
994 (e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
995 | _ -> failwith "not possible" in
996 let (e2fvs,b2fvs,s2fvs) =
998 match seq_fvs quantified
999 [Ast.get_fvs ifheader;Ast.get_fvs branch2;afvs] with
1000 [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1001 (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1002 | _ -> failwith "not possible" in
1003 let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
1004 let exponlyfvs = intersect e1fvs e2fvs in
1005 let new_quantified = union bothfvs quantified in
1006 (* minus free variables *)
1007 let (me1fvs,mb1fvs,ms1fvs) =
1008 match seq_fvs minus_quantified
1009 [Ast.get_mfvs ifheader;Ast.get_mfvs branch1;[]] with
1010 [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
1011 (e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
1012 | _ -> failwith "not possible" in
1013 let (me2fvs,mb2fvs,ms2fvs) =
1015 match seq_fvs minus_quantified
1016 [Ast.get_mfvs ifheader;Ast.get_mfvs branch2;[]] with
1017 [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1018 (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1019 | _ -> failwith "not possible" in
1020 let mbothfvs = union (union mb1fvs mb2fvs) (intersect ms1fvs ms2fvs) in
1021 let new_mquantified = union mbothfvs minus_quantified in
1023 let if_header = quantify guard exponlyfvs (make_match ifheader) in
1024 (* then and else branches *)
1025 let lv = get_label_ctr() in
1026 let used = ref false in
1029 [truepred label; recurse branch1 Tail new_quantified new_mquantified
1030 (Some (lv,used)) llabel slabel guard] in
1033 [falsepred label; make_match els;
1034 recurse branch2 Tail new_quantified new_mquantified
1035 (Some (lv,used)) llabel slabel guard] in
1036 let after_pred = aftpred label in
1037 let or_cases after_branch =
1038 ctl_or true_branch (ctl_or false_branch after_branch) in
1039 let s = guard_to_strict guard in
1040 let (if_header,wrapper) =
1043 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1044 (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
1045 (function body -> quantify true [lv] body))
1046 else (if_header,function x -> x) in
1048 (end_control_structure bothfvs if_header or_cases after_pred
1049 (Some(ctl_and s (ctl_ex (falsepred label)) (ctl_ex after_pred)))
1050 (Some(ctl_ex (falsepred label)))
1051 aft after label guard)
1053 let forwhile header body ((afvs,_,_,_) as aft) after
1054 quantified minus_quantified label recurse make_match guard =
1056 (* the translation in this case is similar to that of an if with no else *)
1057 (* free variables *)
1059 match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
1060 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
1061 | _ -> failwith "not possible" in
1062 let new_quantified = Common.union_set bfvs quantified in
1063 (* minus free variables *)
1065 match seq_fvs minus_quantified
1066 [Ast.get_mfvs header;Ast.get_mfvs body;[]] with
1067 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
1068 | _ -> failwith "not possible" in
1069 let new_mquantified = Common.union_set mbfvs minus_quantified in
1071 let header = quantify guard efvs (make_match header) in
1072 let lv = get_label_ctr() in
1073 let used = ref false in
1077 recurse body Tail new_quantified new_mquantified
1078 (Some (lv,used)) (Some (lv,used)) None guard] in
1079 let after_pred = fallpred label in
1080 let or_cases after_branch = ctl_or body after_branch in
1081 let (header,wrapper) =
1084 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1085 (ctl_and CTL.NONSTRICT(*???*) header label_pred,
1086 (function body -> quantify true [lv] body))
1087 else (header,function x -> x) in
1089 (end_control_structure bfvs header or_cases after_pred
1090 (Some(ctl_ex after_pred)) None aft after label guard) in
1091 match (Ast.unwrap body,aft) with
1092 (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
1093 (match Ast.unwrap re with
1094 Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),
1095 Type_cocci.Unitary,_,false) ->
1097 match seq_fvs quantified [Ast.get_fvs header] with
1099 | _ -> failwith "not possible" in
1100 quantify guard efvs (make_match header)
1104 (* --------------------------------------------------------------------- *)
1105 (* statement metavariables *)
1107 (* issue: an S metavariable that is not an if branch/loop body
1108 should not match an if branch/loop body, so check that the labels
1109 of the nodes before the first node matched by the S are different
1110 from the label of the first node matched by the S *)
1111 let sequencibility body label_pred process_bef_aft = function
1112 Ast.Sequencible | Ast.SequencibleAfterDots [] ->
1115 (ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
1116 | Ast.SequencibleAfterDots l ->
1117 (* S appears after some dots. l is the code that comes after the S.
1118 want to search for that first, because S can match anything, while
1119 the stuff after is probably more restricted *)
1120 let afts = List.map process_bef_aft l in
1121 let ors = foldl1 ctl_or afts in
1122 ctl_and CTL.NONSTRICT
1123 (ctl_ef (ctl_and CTL.NONSTRICT ors (ctl_back_ax label_pred)))
1126 ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
1127 | Ast.NotSequencible -> body (function x -> x)
1129 let svar_context_with_add_after stmt s label quantified d ast
1130 seqible after process_bef_aft guard fvinfo =
1131 let label_var = (*fresh_label_var*) string2var "_lab" in
1133 CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
1135 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1136 let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1137 let full_metamatch = matcher d in
1138 let first_metamatch =
1141 Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_)) ->
1142 Ast.CONTEXT(pos,Ast.BEFORE(bef))
1143 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1144 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1145 let middle_metamatch =
1148 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1149 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1150 let last_metamatch =
1153 Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft)) ->
1154 Ast.CONTEXT(pos,Ast.AFTER(aft))
1155 | Ast.CONTEXT(_,_) -> d
1156 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1159 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1160 let left_or = (* the whole statement is one node *)
1162 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1163 let right_or = (* the statement covers multiple nodes *)
1166 ctl_au CTL.NONSTRICT
1169 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1171 (ctl_not prelabel_pred) after])] in
1173 ctl_and CTL.NONSTRICT label_pred
1174 (f (ctl_and CTL.NONSTRICT
1175 (make_raw_match label false ast) (ctl_or left_or right_or))) in
1176 let stmt_fvs = Ast.get_fvs stmt in
1177 let fvs = get_unquantified quantified stmt_fvs in
1178 quantify guard (label_var::fvs)
1179 (sequencibility body label_pred process_bef_aft seqible)
1181 let svar_minus_or_no_add_after stmt s label quantified d ast
1182 seqible after process_bef_aft guard fvinfo =
1183 let label_var = (*fresh_label_var*) string2var "_lab" in
1185 CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
1187 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1188 let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1190 (* don't have to put anything before the beginning, so don't have to
1191 distinguish the first node. so don't have to bother about paths,
1192 just use the label. label ensures that found nodes match up with
1193 what they should because it is in the lhs of the andany. *)
1195 Ast.MINUS(pos,[]) -> true
1196 | Ast.CONTEXT(pos,Ast.NOTHING) -> true
1199 match (pure_d,after) with
1200 (true,Tail) | (true,End) | (true,VeryEnd) ->
1201 (* the label sharing makes it safe to use AndAny *)
1202 CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
1203 ctl_and CTL.NONSTRICT label_pred
1204 (make_raw_match label false ast),
1205 ctl_and CTL.NONSTRICT (matcher d) prelabel_pred)
1207 (* more safe but less efficient *)
1208 let first_metamatch = matcher d in
1209 let rest_metamatch =
1212 Ast.MINUS(pos,_) -> Ast.MINUS(pos,[])
1213 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1214 | Ast.PLUS -> failwith "not possible") in
1215 let rest_nodes = ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred in
1216 let last_node = and_after guard (ctl_not prelabel_pred) after in
1217 (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
1220 ctl_au CTL.NONSTRICT rest_nodes last_node])) in
1221 let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
1222 let stmt_fvs = Ast.get_fvs stmt in
1223 let fvs = get_unquantified quantified stmt_fvs in
1224 quantify guard (label_var::fvs)
1225 (sequencibility body label_pred process_bef_aft seqible)
1227 (* --------------------------------------------------------------------- *)
1228 (* dots and nests *)
1230 let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
1231 let matchgoto = gotopred None in
1233 make_match None false
1235 (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in
1237 make_match None false
1239 (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in
1241 if quantifier = Exists
1242 then Common.Left(CTL.False)
1244 then Common.Left(CTL.Or(aftpred label,exitpred label))
1246 then Common.Left(aftpred label)
1250 let lv = get_label_ctr() in
1251 let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1252 let preflabelpred = label_pred_maker (Some (lv,ref true)) in
1253 ctl_or (aftpred label)
1254 (quantify false [lv]
1255 (ctl_and CTL.NONSTRICT
1256 (ctl_and CTL.NONSTRICT (truepred label) labelpred)
1257 (ctl_au CTL.NONSTRICT
1258 (ctl_and CTL.NONSTRICT (ctl_not v) preflabelpred)
1259 (ctl_and CTL.NONSTRICT preflabelpred
1260 (ctl_or (retpred None)
1261 (if !Flag_matcher.only_return_is_error_exit
1264 (ctl_or matchcontinue
1265 (ctl_and CTL.NONSTRICT
1266 (ctl_or matchgoto matchbreak)
1267 (ctl_ag s (ctl_not seq_after))))))))))) in
1268 let op = if quantifier = !exists then ctl_au else ctl_anti_au in
1269 let v = get_let_ctr() in
1271 (match stop_early with
1272 Common.Left x -> ctl_or y x
1273 | Common.Right stop_early ->
1274 CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
1276 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1277 process_bef_aft statement_list statement guard quantified wrapcode =
1278 let ctl_and_ns = ctl_and CTL.NONSTRICT in
1279 (* proces bef_aft *)
1281 List.fold_left ctl_or_fl CTL.False (List.map process_bef_aft l) in
1282 let bef_aft = (* to be negated *)
1286 (function Ast.WhenModifier(Ast.WhenAny) -> true | _ -> false)
1289 with Not_found -> shortest (Common.union_set bef aft) in
1292 (function Ast.WhenModifier(Ast.WhenStrict) -> true | _ -> false)
1294 let check_quantifier quant other =
1296 (function Ast.WhenModifier(x) -> x = quant | _ -> false)
1300 (function Ast.WhenModifier(x) -> x = other | _ -> false)
1302 then failwith "inconsistent annotation on dots"
1306 if check_quantifier Ast.WhenExists Ast.WhenForall
1309 if check_quantifier Ast.WhenForall Ast.WhenExists
1312 (* the following is used when we find a goto, etc and consider accepting
1313 without finding the rest of the pattern *)
1314 let aft = shortest aft in
1315 (* process whencode *)
1316 let labelled = label_pred_maker label in
1318 let (poswhen,negwhen) =
1320 (function (poswhen,negwhen) ->
1322 Ast.WhenNot whencodes ->
1323 (poswhen,ctl_or (statement_list whencodes) negwhen)
1324 | Ast.WhenAlways stm ->
1325 (ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen)
1326 | Ast.WhenModifier(_) -> (poswhen,negwhen)
1327 | Ast.WhenNotTrue(e) ->
1329 ctl_or (whencond_true e label guard quantified) negwhen)
1330 | Ast.WhenNotFalse(e) ->
1332 ctl_or (whencond_false e label guard quantified) negwhen))
1333 (CTL.True,bef_aft) (List.rev whencodes) in
1334 let poswhen = ctl_and_ns arg poswhen in
1338 (* add in After, because it's not part of the program *)
1339 ctl_or (aftpred label) negwhen
1341 ctl_and_ns poswhen (ctl_not negwhen) in
1342 (* process dot code, if any *)
1344 match (dotcode,guard) with
1345 (None,_) | (_,true) -> CTL.True
1346 | (Some dotcode,_) -> dotcode in
1347 (* process nest code, if any *)
1348 (* whencode goes in the negated part of the nest; if no nest, just goes
1349 on the "true" in between code *)
1350 let plus_var = if plus then get_label_ctr() else string2var "" in
1351 let plus_var2 = if plus then get_label_ctr() else string2var "" in
1353 match (nest,guard && not plus) with
1354 (None,_) | (_,true) -> whencodes CTL.True
1355 | (Some nest,false) ->
1356 let v = get_let_ctr() in
1360 (* the idea is that BindGood is sort of a witness; a witness to
1361 having found the subterm in at least one place. If there is
1362 not a witness, then there is a risk that it will get thrown
1363 away, if it is merged with a node that has an empty
1364 environment. See tests/nestplus. But this all seems
1365 rather suspicious *)
1366 CTL.And(CTL.NONSTRICT,x,
1367 CTL.Exists(true,plus_var2,
1368 CTL.Pred(Lib_engine.BindGood(plus_var),
1369 CTL.Modif plus_var2)))
1372 CTL.Or(is_plus (CTL.Ref v),
1373 whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
1374 let plus_modifier x =
1381 CTL.Not(CTL.Pred(Lib_engine.BindBad(plus_var),CTL.Control)))))
1387 | Guard f -> ctl_uncheck f
1389 let exit = endpred label in
1390 let errorexit = exitpred label in
1391 ctl_or exit errorexit
1392 (* not at all sure what the next two mean... *)
1396 Some (lv,used) -> used := true;
1397 ctl_or (CTL.Pred(Lib_engine.Label lv,CTL.Control))
1398 (ctl_back_ex (ctl_or (retpred label) (gotopred label)))
1399 | None -> endpred label)
1400 (* was the following, but not clear why sgrep should allow
1402 let exit = endpred label in
1403 let errorexit = exitpred label in
1405 then ctl_or exit errorexit (* end anywhere *)
1406 else exit (* end at the real end of the function *) *) in
1408 (dots_au is_strict ((after = Tail) or (after = VeryEnd))
1409 label (guard_to_strict guard) wrapcode
1410 (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
1411 aft ender quantifier)
1413 and get_whencond_exps e =
1414 match Ast.unwrap e with
1416 | Ast.DisjRuleElem(res) ->
1417 List.fold_left Common.union_set [] (List.map get_whencond_exps res)
1418 | _ -> failwith "not possible"
1420 and make_whencond_headers e e1 label guard quantified =
1421 let fvs = Ast.get_fvs e in
1423 quantify guard (get_unquantified quantified fvs)
1424 (make_match label guard h) in
1429 (Ast.make_mcode "if",
1430 Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
1431 let while_header e1 =
1435 (Ast.make_mcode "while",
1436 Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
1441 (Ast.make_mcode "for",Ast.make_mcode "(",None,Ast.make_mcode ";",
1442 Some e1,Ast.make_mcode ";",None,Ast.make_mcode ")"))) in
1444 List.fold_left ctl_or CTL.False (List.map if_header e1) in
1446 List.fold_left ctl_or CTL.False (List.map while_header e1) in
1448 List.fold_left ctl_or CTL.False (List.map for_header e1) in
1449 (if_headers, while_headers, for_headers)
1451 and whencond_true e label guard quantified =
1452 let e1 = get_whencond_exps e in
1453 let (if_headers, while_headers, for_headers) =
1454 make_whencond_headers e e1 label guard quantified in
1456 (ctl_and CTL.NONSTRICT (truepred label) (ctl_back_ex if_headers))
1457 (ctl_and CTL.NONSTRICT
1458 (inlooppred label) (ctl_back_ex (ctl_or while_headers for_headers)))
1460 and whencond_false e label guard quantified =
1461 let e1 = get_whencond_exps e in
1462 let (if_headers, while_headers, for_headers) =
1463 make_whencond_headers e e1 label guard quantified in
1464 ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
1465 (ctl_and CTL.NONSTRICT (fallpred label)
1466 (ctl_or (ctl_back_ex if_headers)
1467 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1469 (* --------------------------------------------------------------------- *)
1470 (* the main translation loop *)
1472 let rec statement_list stmt_list after quantified minus_quantified
1473 label llabel slabel dots_before guard =
1475 (* include Disj to be on the safe side *)
1476 match Ast.unwrap x with
1477 Ast.Dots _ | Ast.Nest _ | Ast.Disj _ -> true | _ -> false in
1478 let compute_label l e db = if db or isdots e then l else None in
1479 match Ast.unwrap stmt_list with
1481 let rec loop quantified minus_quantified dots_before label llabel slabel
1483 ([],_,_) -> (match after with After f -> f | _ -> CTL.True)
1485 statement e after quantified minus_quantified
1486 (compute_label label e dots_before)
1488 | (e::sl,fv::fvs,mfv::mfvs) ->
1489 let shared = intersectll fv fvs in
1490 let unqshared = get_unquantified quantified shared in
1491 let new_quantified = Common.union_set unqshared quantified in
1492 let minus_shared = intersectll mfv mfvs in
1494 get_unquantified minus_quantified minus_shared in
1495 let new_mquantified =
1496 Common.union_set munqshared minus_quantified in
1497 quantify guard unqshared
1500 (let (label1,llabel1,slabel1) =
1501 match Ast.unwrap e with
1503 (match Ast.unwrap re with
1504 Ast.Goto _ -> (None,None,None)
1505 | _ -> (label,llabel,slabel))
1506 | _ -> (label,llabel,slabel) in
1507 loop new_quantified new_mquantified (isdots e)
1508 label1 llabel1 slabel1
1510 new_quantified new_mquantified
1511 (compute_label label e dots_before) llabel slabel guard)
1512 | _ -> failwith "not possible" in
1513 loop quantified minus_quantified dots_before
1515 (x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x)
1516 | Ast.CIRCLES(x) -> failwith "not supported"
1517 | Ast.STARS(x) -> failwith "not supported"
1519 (* llabel is the label of the enclosing loop and slabel is the label of the
1521 and statement stmt after quantified minus_quantified
1522 label llabel slabel guard =
1523 let ctl_au = ctl_au CTL.NONSTRICT in
1524 let ctl_ax = ctl_ax CTL.NONSTRICT in
1525 let ctl_and = ctl_and CTL.NONSTRICT in
1526 let make_seq = make_seq guard in
1527 let make_seq_after = make_seq_after guard in
1528 let real_make_match = make_match in
1529 let make_match = header_match label guard in
1531 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1534 match Ast.unwrap stmt with
1536 (match Ast.unwrap ast with
1537 (* the following optimisation is not a good idea, because when S
1538 is alone, we would like it not to match a declaration.
1539 this makes more matching for things like when (...) S, but perhaps
1540 that matching is not so costly anyway *)
1541 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1542 | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_)) as d),_),
1544 | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_)) as d),_),
1546 svar_context_with_add_after stmt s label quantified d ast seqible
1548 (process_bef_aft quantified minus_quantified
1549 label llabel slabel true)
1551 (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)
1553 | Ast.MetaStmt((s,_,d,_),keep,seqible,_) ->
1554 svar_minus_or_no_add_after stmt s label quantified d ast seqible
1556 (process_bef_aft quantified minus_quantified
1557 label llabel slabel true)
1559 (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)
1563 match Ast.unwrap ast with
1564 Ast.DisjRuleElem(res) ->
1565 do_re_matches label guard res quantified minus_quantified
1566 | Ast.Exp(_) | Ast.Ty(_) ->
1567 let stmt_fvs = Ast.get_fvs stmt in
1568 let fvs = get_unquantified quantified stmt_fvs in
1569 CTL.InnerAnd(quantify guard fvs (make_match ast))
1571 let stmt_fvs = Ast.get_fvs stmt in
1572 let fvs = get_unquantified quantified stmt_fvs in
1573 quantify guard fvs (make_match ast) in
1574 match Ast.unwrap ast with
1575 Ast.Break(brk,semi) ->
1576 (match (llabel,slabel) with
1577 (_,Some(lv,used)) -> (* use switch label if there is one *)
1578 ctl_and term (bclabel_pred_maker slabel)
1579 | _ -> ctl_and term (bclabel_pred_maker llabel))
1580 | Ast.Continue(brk,semi) -> ctl_and term (bclabel_pred_maker llabel)
1581 | Ast.Return((_,info,retmc,pos),(_,_,semmc,_)) ->
1582 (* discard pattern that comes after return *)
1583 let normal_res = make_seq_after term after in
1584 (* the following code tries to propagate the modifications on
1585 return; to a close brace, in the case where the final return
1588 match (retmc,semmc) with
1589 (Ast.MINUS(_,l1),Ast.MINUS(_,l2)) when !Flag.sgrep_mode2 ->
1590 (* in sgrep mode, we can propagate the - *)
1591 Some (Ast.MINUS(Ast.NoPos,l1@l2))
1592 | (Ast.MINUS(_,l1),Ast.MINUS(_,l2))
1593 | (Ast.CONTEXT(_,Ast.BEFORE(l1)),
1594 Ast.CONTEXT(_,Ast.AFTER(l2))) ->
1595 Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2)))
1596 | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
1597 | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
1599 | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.AFTER(l))) ->
1600 Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l)))
1602 let ret = Ast.make_mcode "return" in
1604 Ast.rewrap ast (Ast.Edots(Ast.make_mcode "...",None)) in
1605 let semi = Ast.make_mcode ";" in
1607 make_match(Ast.rewrap ast (Ast.Return(ret,semi))) in
1609 make_match(Ast.rewrap ast (Ast.ReturnExpr(ret,edots,semi))) in
1612 let exit = endpred None in
1614 Ast.rewrap ast (Ast.SeqEnd (("}",info,new_mc,pos))) in
1615 let stripped_rbrace =
1616 Ast.rewrap ast (Ast.SeqEnd(Ast.make_mcode "}")) in
1618 (ctl_and (make_match mod_rbrace)
1623 (ctl_or simple_return return_expr))))
1625 (make_match stripped_rbrace)
1626 (* error exit not possible; it is in the middle
1627 of code, so a return is needed *)
1630 (* some change in the middle of the return, so have to
1631 find an actual return *)
1634 (* should try to deal with the dots_bef_aft problem elsewhere,
1635 but don't have the courage... *)
1640 do_between_dots stmt term End
1641 quantified minus_quantified label llabel slabel guard in
1643 make_seq_after term after)
1644 | Ast.Seq(lbrace,decls,body,rbrace) ->
1645 let (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs) =
1648 [Ast.get_fvs lbrace;Ast.get_fvs decls;
1649 Ast.get_fvs body;Ast.get_fvs rbrace]
1651 [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
1652 (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
1653 | _ -> failwith "not possible" in
1654 let (mlbfvs,mb1fvs,mb2fvs,mb3fvs,mrbfvs) =
1656 seq_fvs minus_quantified
1657 [Ast.get_mfvs lbrace;Ast.get_mfvs decls;
1658 Ast.get_mfvs body;Ast.get_mfvs rbrace]
1660 [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
1661 (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
1662 | _ -> failwith "not possible" in
1663 let pv = count_nested_braces stmt in
1664 let lv = get_label_ctr() in
1665 let paren_pred = CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
1666 let label_pred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1669 (quantify guard lbfvs (make_match lbrace))
1670 (ctl_and paren_pred label_pred) in
1672 match Ast.unwrap rbrace with
1673 Ast.SeqEnd((data,info,_,pos)) ->
1674 Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data))
1675 | _ -> failwith "unexpected close brace" in
1677 (* label is not needed; paren_pred is enough *)
1678 quantify guard rbfvs
1679 (ctl_au (make_match empty_rbrace)
1681 (real_make_match None guard rbrace)
1683 let new_quantified2 =
1684 Common.union_set b1fvs (Common.union_set b2fvs quantified) in
1685 let new_quantified3 = Common.union_set b3fvs new_quantified2 in
1686 let new_mquantified2 =
1687 Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in
1688 let new_mquantified3 = Common.union_set mb3fvs new_mquantified2 in
1689 let pattern_as_given =
1690 let new_quantified2 = Common.union_set [pv] new_quantified2 in
1691 let new_quantified3 = Common.union_set [pv] new_quantified3 in
1692 quantify true [pv;lv]
1693 (quantify guard b1fvs
1696 quantify guard b2fvs
1697 (statement_list decls
1699 (quantify guard b3fvs
1700 (statement_list body
1701 (After (make_seq_after end_brace after))
1702 new_quantified3 new_mquantified3
1703 (Some (lv,ref true)) (* label mostly useful *)
1704 llabel slabel true guard)))
1705 new_quantified2 new_mquantified2
1706 (Some (lv,ref true)) llabel slabel false guard)])) in
1707 if ends_in_return body
1709 (* matching error handling code *)
1711 1. The pattern as given
1712 2. A goto, and then some close braces, and then the pattern as
1713 given, but without the braces (only possible if there are no
1714 decls, and open and close braces are unmodified)
1715 3. Part of the pattern as given, then a goto, and then the rest
1716 of the pattern. For this case, we just check that all paths have
1717 a goto within the current braces. checking for a goto at every
1718 point in the pattern seems expensive and not worthwhile. *)
1720 let body = preprocess_dots body in (* redo, to drop braces *)
1724 (make_match empty_rbrace)
1725 (ctl_ax (* skip the destination label *)
1726 (quantify guard b3fvs
1727 (statement_list body End
1728 new_quantified3 new_mquantified3 None llabel slabel
1731 let new_quantified2 = Common.union_set [pv] new_quantified2 in
1732 let new_quantified3 = Common.union_set [pv] new_quantified3 in
1733 quantify true [pv;lv]
1734 (quantify guard b1fvs
1738 (CTL.AU (* want AF even for sgrep *)
1739 (CTL.FORWARD,CTL.STRICT,
1740 CTL.Pred(Lib_engine.PrefixLabel(lv),CTL.Control),
1741 ctl_and (* brace must be eventually after goto *)
1742 (gotopred (Some (lv,ref true)))
1743 (* want AF even for sgrep *)
1744 (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
1745 (quantify guard b2fvs
1746 (statement_list decls
1748 (quantify guard b3fvs
1749 (statement_list body Tail
1752 nopv_end_brace after)*)
1753 new_quantified3 new_mquantified3
1754 None llabel slabel true guard)))
1755 new_quantified2 new_mquantified2
1756 (Some (lv,ref true))
1757 llabel slabel false guard))])) in
1758 ctl_or pattern_as_given
1759 (match Ast.unwrap decls with
1760 Ast.DOTS([]) -> ctl_or pattern2 pattern3
1761 | Ast.DOTS(l) -> pattern3
1762 | _ -> failwith "circles and stars not supported")
1763 else pattern_as_given
1764 | Ast.IfThen(ifheader,branch,aft) ->
1765 ifthen ifheader branch aft after quantified minus_quantified
1766 label llabel slabel statement make_match guard
1768 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
1769 ifthenelse ifheader branch1 els branch2 aft after quantified
1770 minus_quantified label llabel slabel statement make_match guard
1772 | Ast.While(header,body,aft) | Ast.For(header,body,aft)
1773 | Ast.Iterator(header,body,aft) ->
1774 forwhile header body aft after quantified minus_quantified
1775 label statement make_match guard
1777 | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
1779 (label_pred_maker label)
1780 (List.fold_left ctl_seqor CTL.False
1783 statement_list sl after quantified minus_quantified label
1784 llabel slabel true guard)
1787 | Ast.Nest(stmt_dots,whencode,multi,bef,aft) ->
1788 (* label in recursive call is None because label check is already
1789 wrapped around the corresponding code *)
1792 match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
1794 [(wcfvs,bothfvs);(bdfvs,_)] -> bothfvs
1795 | _ -> failwith "not possible" in
1797 (* no minus version because when code doesn't contain any minus code *)
1798 let new_quantified = Common.union_set bfvs quantified in
1802 statement_list stmt_dots (a2n after) new_quantified minus_quantified
1803 None llabel slabel true guard in
1804 dots_and_nests multi
1805 (Some dots_pattern) whencode bef aft None after label
1806 (process_bef_aft new_quantified minus_quantified
1807 None llabel slabel true)
1809 statement_list x Tail new_quantified minus_quantified None
1810 llabel slabel true true)
1812 statement x Tail new_quantified minus_quantified None
1815 (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
1817 | Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
1821 (* no need for the fresh metavar, but ... is a bit wierd as a
1823 Some(make_match (make_meta_rule_elem d ([],[],[])))
1825 dots_and_nests false None whencodes bef aft dot_code after label
1826 (process_bef_aft quantified minus_quantified None llabel slabel true)
1828 statement_list x Tail quantified minus_quantified
1829 None llabel slabel true true)
1831 statement x Tail quantified minus_quantified None llabel slabel true)
1833 (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
1835 | Ast.Switch(header,lb,cases,rb) ->
1836 let rec intersect_all = function
1839 | x::xs -> intersect x (intersect_all xs) in
1840 let rec union_all l = List.fold_left union [] l in
1841 (* start normal variables *)
1842 let header_fvs = Ast.get_fvs header in
1843 let lb_fvs = Ast.get_fvs lb in
1844 let case_fvs = List.map Ast.get_fvs cases in
1845 let rb_fvs = Ast.get_fvs rb in
1846 let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1847 all_casefvs,all_b3fvs,all_rbfvs) =
1849 (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1850 all_casefvs,all_b3fvs,all_rbfvs) ->
1851 function case_fvs ->
1852 match seq_fvs quantified [header_fvs;lb_fvs;case_fvs;rb_fvs] with
1853 [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
1854 (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
1855 b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
1857 | _ -> failwith "not possible")
1858 ([],[],[],[],[],[],[]) case_fvs in
1859 let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1860 all_casefvs,all_b3fvs,all_rbfvs) =
1861 (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,
1862 List.rev all_b2fvs,List.rev all_casefvs,List.rev all_b3fvs,
1863 List.rev all_rbfvs) in
1864 let exponlyfvs = intersect_all all_efvs in
1865 let lbonlyfvs = intersect_all all_lbfvs in
1866 (* don't do anything with right brace. Hope there is no + code on it *)
1867 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1868 let b1fvs = union_all all_b1fvs in
1869 let new1_quantified = union b1fvs quantified in
1870 let b2fvs = union (union_all all_b1fvs) (intersect_all all_casefvs) in
1871 let new2_quantified = union b2fvs new1_quantified in
1872 (* let b3fvs = union_all all_b3fvs in*)
1873 (* ------------------- start minus free variables *)
1874 let header_mfvs = Ast.get_mfvs header in
1875 let lb_mfvs = Ast.get_mfvs lb in
1876 let case_mfvs = List.map Ast.get_mfvs cases in
1877 let rb_mfvs = Ast.get_mfvs rb in
1878 let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
1879 all_mcasefvs,all_mb3fvs,all_mrbfvs) =
1881 (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1882 all_casefvs,all_b3fvs,all_rbfvs) ->
1883 function case_mfvs ->
1886 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1887 [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
1888 (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
1889 b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
1891 | _ -> failwith "not possible")
1892 ([],[],[],[],[],[],[]) case_mfvs in
1893 let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
1894 all_mcasefvs,all_mb3fvs,all_mrbfvs) =
1895 (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,
1896 List.rev all_mb2fvs,List.rev all_mcasefvs,List.rev all_mb3fvs,
1897 List.rev all_mrbfvs) in
1898 (* don't do anything with right brace. Hope there is no + code on it *)
1899 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1900 let mb1fvs = union_all all_mb1fvs in
1901 let new1_mquantified = union mb1fvs quantified in
1902 let mb2fvs = union (union_all all_mb1fvs) (intersect_all all_mcasefvs) in
1903 let new2_mquantified = union mb2fvs new1_mquantified in
1904 (* let b3fvs = union_all all_b3fvs in*)
1905 (* ------------------- end collection of free variables *)
1906 let switch_header = quantify guard exponlyfvs (make_match header) in
1907 let lb = quantify guard lbonlyfvs (make_match lb) in
1908 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
1911 (function case_line ->
1912 match Ast.unwrap case_line with
1913 Ast.CaseLine(header,body) ->
1915 match seq_fvs new2_quantified [Ast.get_fvs header] with
1916 [(e1fvs,_)] -> e1fvs
1917 | _ -> failwith "not possible" in
1918 quantify guard e1fvs (real_make_match label true header)
1919 | Ast.OptCase(case_line) -> failwith "not supported")
1922 ctl_not (List.fold_left ctl_or_fl CTL.False case_headers) in
1923 let lv = get_label_ctr() in
1924 let used = ref false in
1927 (function case_line ->
1928 match Ast.unwrap case_line with
1929 Ast.CaseLine(header,body) ->
1930 let (e1fvs,b1fvs,s1fvs) =
1931 let fvs = [Ast.get_fvs header;Ast.get_fvs body] in
1932 match seq_fvs new2_quantified fvs with
1933 [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
1934 | _ -> failwith "not possible" in
1935 let (me1fvs,mb1fvs,ms1fvs) =
1936 let fvs = [Ast.get_mfvs header;Ast.get_mfvs body] in
1937 match seq_fvs new2_mquantified fvs with
1938 [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
1939 | _ -> failwith "not possible" in
1941 quantify guard e1fvs (make_match header) in
1942 let new3_quantified = union b1fvs new2_quantified in
1943 let new3_mquantified = union mb1fvs new2_mquantified in
1945 statement_list body Tail
1946 new3_quantified new3_mquantified label llabel
1947 (Some (lv,used)) true(*?*) guard in
1948 quantify guard b1fvs (make_seq [case_header; body])
1949 | Ast.OptCase(case_line) -> failwith "not supported")
1951 let default_required =
1954 match Ast.unwrap case with
1955 Ast.CaseLine(header,_) ->
1956 (match Ast.unwrap header with
1957 Ast.Default(_,_) -> true
1961 then function x -> x
1962 else function x -> ctl_or (fallpred label) x in
1963 let after_pred = aftpred label in
1964 let body after_branch =
1967 (quantify guard b2fvs
1970 (List.fold_left ctl_and CTL.True
1971 (List.map ctl_ex case_headers));
1972 List.fold_left ctl_or_fl no_header case_code])))
1975 (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,
1976 match Ast.unwrap rb with
1977 Ast.SeqEnd(rb) -> Ast.get_mcodekind rb
1978 | _ -> failwith "not possible") in
1979 let (switch_header,wrapper) =
1982 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1983 (ctl_and switch_header label_pred,
1984 (function body -> quantify true [lv] body))
1985 else (switch_header,function x -> x) in
1987 (end_control_structure b1fvs switch_header body
1988 after_pred (Some(ctl_ex after_pred)) None aft after label guard)
1989 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
1990 let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs) =
1993 [Ast.get_fvs header;Ast.get_fvs lbrace;Ast.get_fvs decls;
1994 Ast.get_fvs body;Ast.get_fvs rbrace]
1996 [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
1997 (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
1998 | _ -> failwith "not possible" in
1999 let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mb4fvs,mrbfvs) =
2002 [Ast.get_mfvs header;Ast.get_mfvs lbrace;Ast.get_mfvs decls;
2003 Ast.get_mfvs body;Ast.get_mfvs rbrace]
2005 [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
2006 (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
2007 | _ -> failwith "not possible" in
2008 let function_header = quantify guard hfvs (make_match header) in
2009 let start_brace = quantify guard lbfvs (make_match lbrace) in
2010 let stripped_rbrace =
2011 match Ast.unwrap rbrace with
2012 Ast.SeqEnd((data,info,_,_)) ->
2013 Ast.rewrap rbrace(Ast.SeqEnd (Ast.make_mcode data))
2014 | _ -> failwith "unexpected close brace" in
2016 let exit = CTL.Pred (Lib_engine.Exit,CTL.Control) in
2017 let errorexit = CTL.Pred (Lib_engine.ErrorExit,CTL.Control) in
2018 let fake_brace = CTL.Pred (Lib_engine.FakeBrace,CTL.Control) in
2020 (quantify guard rbfvs (make_match rbrace))
2022 (* the following finds the beginning of the fake braces,
2023 if there are any, not completely sure how this works.
2024 sse the examples sw and return *)
2025 (ctl_back_ex (ctl_not fake_brace))
2026 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2027 let new_quantified3 =
2028 Common.union_set b1fvs
2029 (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
2030 let new_quantified4 = Common.union_set b4fvs new_quantified3 in
2031 let new_mquantified3 =
2032 Common.union_set mb1fvs
2033 (Common.union_set mb2fvs
2034 (Common.union_set mb3fvs minus_quantified)) in
2035 let new_mquantified4 = Common.union_set mb4fvs new_mquantified3 in
2037 match (Ast.undots decls,Ast.undots body,contains_modif rbrace) with
2038 ([],[body],false) ->
2039 (match Ast.unwrap body with
2040 Ast.Nest(stmt_dots,[],multi,_,_) ->
2042 then None (* not sure how to optimize this case *)
2043 else Some (Common.Left stmt_dots)
2044 | Ast.Dots(_,whencode,_,_) when
2046 (* flow sensitive, so not optimizable *)
2047 (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2049 | _ -> true) whencode) ->
2050 Some (Common.Right whencode)
2055 Some (Common.Left stmt_dots) ->
2056 (* special case for function header + body - header is unambiguous
2057 and unique, so we can just look for the nested body anywhere
2060 (CTL.FORWARD,guard_to_strict guard,start_brace,
2061 statement_list stmt_dots
2062 (* discards match on right brace, but don't need it *)
2063 (Guard (make_seq_after end_brace after))
2064 new_quantified4 new_mquantified4
2065 None llabel slabel true guard)
2066 | Some (Common.Right whencode) ->
2067 (* try to be more efficient for the case where the body is just
2068 ... Perhaps this is too much of a special case, but useful
2069 for dropping a parameter and checking that it is never used. *)
2081 Ast.WhenAlways(s) -> prev
2082 | Ast.WhenNot(sl) ->
2084 statement_list sl Tail
2085 new_quantified4 new_mquantified4
2086 label llabel slabel true true in
2088 | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2089 failwith "unexpected"
2090 | Ast.WhenModifier(Ast.WhenAny) -> CTL.False
2091 | Ast.WhenModifier(_) -> prev)
2092 CTL.False whencode))
2096 Ast.WhenAlways(s) ->
2099 new_quantified4 new_mquantified4
2100 label llabel slabel true in
2102 | Ast.WhenNot(sl) -> prev
2103 | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2104 failwith "unexpected"
2105 | Ast.WhenModifier(Ast.WhenAny) -> CTL.True
2106 | Ast.WhenModifier(_) -> prev)
2107 CTL.True whencode) in
2108 ctl_au leftarg (make_match stripped_rbrace)]
2112 quantify guard b3fvs
2113 (statement_list decls
2115 (quantify guard b4fvs
2116 (statement_list body
2117 (After (make_seq_after end_brace after))
2118 new_quantified4 new_mquantified4
2119 None llabel slabel true guard)))
2120 new_quantified3 new_mquantified3 None llabel slabel
2122 quantify guard b1fvs
2123 (make_seq [function_header; quantify guard b2fvs body_code])
2124 | Ast.Define(header,body) ->
2125 let (hfvs,bfvs,bodyfvs) =
2126 match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body]
2128 [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
2129 | _ -> failwith "not possible" in
2130 let (mhfvs,mbfvs,mbodyfvs) =
2131 match seq_fvs minus_quantified [Ast.get_mfvs header;Ast.get_mfvs body]
2133 [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
2134 | _ -> failwith "not possible" in
2135 let define_header = quantify guard hfvs (make_match header) in
2137 statement_list body after
2138 (Common.union_set bfvs quantified)
2139 (Common.union_set mbfvs minus_quantified)
2140 None llabel slabel true guard in
2141 quantify guard bfvs (make_seq [define_header; body_code])
2142 | Ast.OptStm(stm) ->
2143 failwith "OptStm should have been compiled away\n"
2144 | Ast.UniqueStm(stm) -> failwith "arities not yet supported"
2145 | _ -> failwith "not supported" in
2146 if guard or !dots_done
2149 do_between_dots stmt term after quantified minus_quantified
2150 label llabel slabel guard
2152 (* term is the translation of stmt *)
2153 and do_between_dots stmt term after quantified minus_quantified
2154 label llabel slabel guard =
2155 match Ast.get_dots_bef_aft stmt with
2156 Ast.AddingBetweenDots (brace_term,n)
2157 | Ast.DroppingBetweenDots (brace_term,n) ->
2159 statement brace_term after quantified minus_quantified
2160 label llabel slabel guard in
2161 let v = Printf.sprintf "_r_%d" n in
2162 let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in
2163 let case2 = ctl_and CTL.NONSTRICT (ctl_not (CTL.Ref v)) term in
2166 (ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
2167 (ctl_back_ex (ctl_back_ex (falsepred label))),
2169 | Ast.NoDots -> term
2171 (* un_process_bef_aft is because we don't want to do transformation in this
2172 code, and thus don't case about braces before or after it *)
2173 and process_bef_aft quantified minus_quantified label llabel slabel guard =
2175 Ast.WParen (re,n) ->
2176 let paren_pred = CTL.Pred (Lib_engine.Paren n,CTL.Control) in
2177 let s = guard_to_strict guard in
2178 quantify true (get_unquantified quantified [n])
2179 (ctl_and s (make_raw_match None guard re) paren_pred)
2181 statement s Tail quantified minus_quantified label llabel slabel guard
2182 | Ast.Other_dots d ->
2183 statement_list d Tail quantified minus_quantified
2184 label llabel slabel true guard
2186 (* --------------------------------------------------------------------- *)
2187 (* cleanup: convert AX to EX for pdots.
2188 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2189 This is what we wanted in the first place, but it wasn't possible to make
2190 because the AX and its argument are not created in the same place.
2192 (* also cleanup XX, which is a marker for the case where the programmer
2193 specifies to change the quantifier on .... Assumed to only occur after one AX
2194 or EX, or at top level. *)
2197 let c = match c with CTL.XX(c) -> c | _ -> c in
2199 CTL.False -> CTL.False
2200 | CTL.True -> CTL.True
2201 | CTL.Pred(p) -> CTL.Pred(p)
2202 | CTL.Not(phi) -> CTL.Not(cleanup phi)
2203 | CTL.Exists(keep,v,phi) -> CTL.Exists(keep,v,cleanup phi)
2204 | CTL.AndAny(dir,s,phi1,phi2) ->
2205 CTL.AndAny(dir,s,cleanup phi1,cleanup phi2)
2206 | CTL.HackForStmt(dir,s,phi1,phi2) ->
2207 CTL.HackForStmt(dir,s,cleanup phi1,cleanup phi2)
2208 | CTL.And(s,phi1,phi2) -> CTL.And(s,cleanup phi1,cleanup phi2)
2209 | CTL.Or(phi1,phi2) -> CTL.Or(cleanup phi1,cleanup phi2)
2210 | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(cleanup phi1,cleanup phi2)
2211 | CTL.Implies(phi1,phi2) -> CTL.Implies(cleanup phi1,cleanup phi2)
2212 | CTL.AF(dir,s,phi1) -> CTL.AF(dir,s,cleanup phi1)
2213 | CTL.AX(CTL.FORWARD,s,
2215 CTL.And(CTL.NONSTRICT,CTL.AU(CTL.FORWARD,s2,e2,e3),
2216 CTL.EU(CTL.FORWARD,e4,e5)))) ->
2218 CTL.And(CTL.NONSTRICT,
2219 CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)),
2220 CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5))))
2221 | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,cleanup phi)
2222 | CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) ->
2223 CTL.AX(dir,s,cleanup phi)
2224 | CTL.XX(phi) -> failwith "bad XX"
2225 | CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1)
2226 | CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1)
2227 | CTL.EF(dir,phi1) -> CTL.EF(dir,cleanup phi1)
2228 | CTL.EX(dir,phi1) -> CTL.EX(dir,cleanup phi1)
2229 | CTL.EG(dir,phi1) -> CTL.EG(dir,cleanup phi1)
2230 | CTL.AW(dir,s,phi1,phi2) -> CTL.AW(dir,s,cleanup phi1,cleanup phi2)
2231 | CTL.AU(dir,s,phi1,phi2) -> CTL.AU(dir,s,cleanup phi1,cleanup phi2)
2232 | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,cleanup phi1,cleanup phi2)
2233 | CTL.Let (x,phi1,phi2) -> CTL.Let (x,cleanup phi1,cleanup phi2)
2234 | CTL.LetR (dir,x,phi1,phi2) -> CTL.LetR (dir,x,cleanup phi1,cleanup phi2)
2235 | CTL.Ref(s) -> CTL.Ref(s)
2236 | CTL.Uncheck(phi1) -> CTL.Uncheck(cleanup phi1)
2237 | CTL.InnerAnd(phi1) -> CTL.InnerAnd(cleanup phi1)
2239 (* --------------------------------------------------------------------- *)
2240 (* Function declaration *)
2242 let top_level name (ua,pos) t =
2243 let ua = List.filter (function (nm,_) -> nm = name) ua in
2245 saved := Ast.get_saved t;
2246 let quantified = Common.minus_set ua pos in
2247 quantify false quantified
2248 (match Ast.unwrap t with
2249 Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
2251 let unopt = elim_opt.V.rebuilder_statement stmt in
2252 let unopt = preprocess_dots_e unopt in
2253 cleanup(statement unopt VeryEnd quantified [] None None None false)
2254 | Ast.CODE(stmt_dots) ->
2255 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
2256 let unopt = preprocess_dots unopt in
2257 let starts_with_dots =
2258 match Ast.undots stmt_dots with
2260 (match Ast.unwrap d with
2261 Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_)
2262 | Ast.Stars(_,_,_,_) -> true
2265 let starts_with_brace =
2266 match Ast.undots stmt_dots with
2268 (match Ast.unwrap d with
2273 statement_list unopt VeryEnd quantified [] None None None
2276 (if starts_with_dots
2278 (* EX because there is a loop on enter/top *)
2279 ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res)
2280 else if starts_with_brace
2282 ctl_and CTL.NONSTRICT
2283 (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res
2285 | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords")
2287 (* --------------------------------------------------------------------- *)
2290 let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
2293 (match exists_flag with
2294 Ast.Exists -> exists := Exists
2295 | Ast.Forall -> exists := Forall
2296 | Ast.ReverseForall -> exists := ReverseForall
2297 | Ast.Undetermined ->
2298 exists := if !Flag.sgrep_mode2 then Exists else Forall);
2300 let (l,used_after) =
2304 match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
2305 (List.combine l (List.combine used_after positions))) in
2306 let res = List.map2 (top_level name) used_after l in
2310 let asttoctl r used_after positions =
2312 Ast.ScriptRule _ -> []
2313 | Ast.CocciRule (a,b,c,_) -> asttoctlz (a,b,c) used_after positions
2315 let pp_cocci_predicate (pred,modif) =
2316 Pretty_print_engine.pp_predicate pred
2318 let cocci_predicate_to_string (pred,modif) =
2319 Pretty_print_engine.predicate_to_string pred