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 (* 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
350 donothing donothing stmtdotsfn donothing
351 donothing donothing donothing donothing donothing donothing donothing
352 donothing donothing donothing donothing donothing
354 (* --------------------------------------------------------------------- *)
355 (* after management *)
356 (* We need Guard for the following case:
365 Here the inner <... b ...> should not go past foo. But foo is not the
366 "after" of the body of the outer nest, because we don't want to search for
367 it in the case where the body of the outer nest ends in something other
368 than dots or a nest. *)
370 (* what is the difference between tail and end??? *)
372 type after = After of formula | Guard of formula | Tail | End | VeryEnd
374 let a2n = function After x -> Guard x | a -> a
377 let pp_pred (x,_) = Pretty_print_engine.pp_predicate x in
378 let pp_meta (_,x) = Common.pp x in
379 Pretty_print_ctl.pp_ctl (pp_pred,pp_meta) false x;
380 Format.print_newline()
382 let print_after = function
383 After ctl -> Printf.printf "After:\n"; print_ctl ctl
384 | Guard ctl -> Printf.printf "Guard:\n"; print_ctl ctl
385 | Tail -> Printf.printf "Tail\n"
386 | VeryEnd -> Printf.printf "Very End\n"
387 | End -> Printf.printf "End\n"
389 (* --------------------------------------------------------------------- *)
392 let fresh_var _ = string2var "_v"
393 let fresh_pos _ = string2var "_pos" (* must be a constant *)
395 let fresh_metavar _ = "_S"
397 (* fvinfo is going to end up being from the whole associated statement.
398 it would be better if it were just the free variables in d, but free_vars.ml
399 doesn't keep track of free variables on + code *)
400 let make_meta_rule_elem d fvinfo =
401 let nm = fresh_metavar() in
402 Ast.make_meta_rule_elem nm d fvinfo
404 let get_unquantified quantified vars =
405 List.filter (function x -> not (List.mem x quantified)) vars
407 let make_seq guard l =
408 let s = guard_to_strict guard in
409 foldr1 (function rest -> function cur -> ctl_and s cur (ctl_ax s rest)) l
411 let make_seq_after2 guard first rest =
412 let s = guard_to_strict guard in
414 After rest -> ctl_and s first (ctl_ax s (ctl_ax s rest))
417 let make_seq_after guard first rest =
419 After rest -> make_seq guard [first;rest]
422 let opt_and guard first rest =
423 let s = guard_to_strict guard in
426 | Some first -> ctl_and s first rest
428 let and_after guard first rest =
429 let s = guard_to_strict guard in
430 match rest with After rest -> ctl_and s first rest | _ -> first
433 let bind x y = x or y in
434 let option_default = false in
435 let mcode r (_,_,kind,metapos) =
437 Ast.MINUS(_,_) -> true
438 | Ast.PLUS -> failwith "not possible"
439 | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
440 let do_nothing r k e = k e in
441 let rule_elem r k re =
443 match Ast.unwrap re with
444 Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
445 bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
446 | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
449 V.combiner bind option_default
450 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
451 do_nothing do_nothing do_nothing do_nothing
452 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
453 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
454 recursor.V.combiner_rule_elem
457 let bind x y = x or y in
458 let option_default = false in
459 let mcode r (_,_,kind,metapos) =
461 Ast.MetaPos(_,_,_,_,_) -> true
462 | Ast.NoMetaPos -> false in
463 let do_nothing r k e = k e in
464 let rule_elem r k re =
466 match Ast.unwrap re with
467 Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
468 bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
469 | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
472 V.combiner bind option_default
473 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
474 do_nothing do_nothing do_nothing do_nothing
475 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
476 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
477 recursor.V.combiner_rule_elem
479 (* code is not a DisjRuleElem *)
480 let make_match label guard code =
481 let v = fresh_var() in
482 let matcher = Lib_engine.Match(code) in
483 if contains_modif code && not guard
484 then CTL.Exists(true,v,predmaker guard (matcher,CTL.Modif v) label)
486 let iso_info = !Flag.track_iso_usage && not (Ast.get_isos code = []) in
487 (match (iso_info,!onlyModif,guard,
488 intersect !used_after (Ast.get_fvs code)) with
489 (false,true,_,[]) | (_,_,true,_) ->
490 predmaker guard (matcher,CTL.Control) label
491 | _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))
493 let make_raw_match label guard code =
494 predmaker guard (Lib_engine.Match(code),CTL.Control) label
496 let rec seq_fvs quantified = function
499 let t1fvs = get_unquantified quantified fv1 in
501 List.fold_left Common.union_set []
502 (List.map (get_unquantified quantified) fvs) in
503 let bothfvs = Common.inter_set t1fvs termfvs in
504 let t1onlyfvs = Common.minus_set t1fvs bothfvs in
505 let new_quantified = Common.union_set bothfvs quantified in
506 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs)
511 function code -> CTL.Exists (not guard && List.mem cur !saved,cur,code))
513 let non_saved_quantify =
515 (function cur -> function code -> CTL.Exists (false,cur,code))
517 let intersectll lst nested_list =
518 List.filter (function x -> List.exists (List.mem x) nested_list) lst
520 (* --------------------------------------------------------------------- *)
521 (* Count depth of braces. The translation of a closed brace appears deeply
522 nested within the translation of the sequence term, so the name of the
523 paren var has to take into account the names of the nested braces. On the
524 other hand the close brace does not escape, so we don't have to take into
525 account other paren variable names. *)
527 (* called repetitively, which is inefficient, but less trouble than adding a
528 new field to Seq and FunDecl *)
529 let count_nested_braces s =
530 let bind x y = max x y in
531 let option_default = 0 in
532 let stmt_count r k s =
533 match Ast.unwrap s with
534 Ast.Seq(_,_,_,_) | Ast.FunDecl(_,_,_,_,_) -> (k s) + 1
536 let donothing r k e = k e in
538 let recursor = V.combiner bind option_default
539 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
540 donothing donothing donothing donothing
541 donothing donothing donothing donothing donothing donothing
542 donothing donothing stmt_count donothing donothing donothing in
543 let res = string_of_int (recursor.V.combiner_statement s) in
547 let get_label_ctr _ =
548 let cur = !labelctr in
550 string2var (Printf.sprintf "l%d" cur)
552 (* --------------------------------------------------------------------- *)
553 (* annotate dots with before and after neighbors *)
555 let print_bef_aft = function
557 Printf.printf "bef/aft\n";
558 Pretty_print_cocci.rule_elem "" re;
559 Format.print_newline()
561 Printf.printf "bef/aft\n";
562 Pretty_print_cocci.statement "" s;
563 Format.print_newline()
564 | Ast.Other_dots d ->
565 Printf.printf "bef/aft\n";
566 Pretty_print_cocci.statement_dots d;
567 Format.print_newline()
569 (* [] can only occur if we are in a disj, where it comes from a ? In that
570 case, we want to use a, which accumulates all of the previous patterns in
572 let rec get_before_elem sl a =
573 match Ast.unwrap sl with
577 [] -> ([],Common.Right a)
579 let (e,ea) = get_before_e e a in
582 let (e,ea) = get_before_e e a in
583 let (sl,sla) = loop sl ea in
585 let (l,a) = loop x a in
586 (Ast.rewrap sl (Ast.DOTS(l)),a)
587 | Ast.CIRCLES(x) -> failwith "not supported"
588 | Ast.STARS(x) -> failwith "not supported"
590 and get_before sl a =
591 match get_before_elem sl a with
592 (term,Common.Left x) -> (term,x)
593 | (term,Common.Right x) -> (term,x)
595 and get_before_whencode wc =
598 Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w
599 | Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w
600 | Ast.WhenModifier(x) -> Ast.WhenModifier(x)
601 | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
602 | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
605 and get_before_e s a =
606 match Ast.unwrap s with
607 Ast.Dots(d,w,_,aft) ->
608 (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)
609 | Ast.Nest(stmt_dots,w,multi,_,aft) ->
610 let w = get_before_whencode w in
611 let (sd,_) = get_before stmt_dots a in
617 Unify_ast.unify_statement_dots
618 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
620 Unify_ast.MAYBE -> false
622 | Ast.Other_dots a ->
623 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
625 Unify_ast.MAYBE -> false
629 (Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
630 | Ast.Disj(stmt_dots_list) ->
632 List.split (List.map (function e -> get_before e a) stmt_dots_list) in
633 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
635 (match Ast.unwrap ast with
636 Ast.MetaStmt(_,_,_,_) -> (s,[])
637 | _ -> (s,[Ast.Other s]))
638 | Ast.Seq(lbrace,decls,body,rbrace) ->
639 let index = count_nested_braces s in
640 let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
641 let (bd,_) = get_before body dea in
642 (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
643 [Ast.WParen(rbrace,index)])
644 | Ast.Define(header,body) ->
645 let (body,_) = get_before body [] in
646 (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
647 | Ast.IfThen(ifheader,branch,aft) ->
648 let (br,_) = get_before_e branch [] in
649 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s])
650 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
651 let (br1,_) = get_before_e branch1 [] in
652 let (br2,_) = get_before_e branch2 [] in
653 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
654 | Ast.While(header,body,aft) ->
655 let (bd,_) = get_before_e body [] in
656 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
657 | Ast.For(header,body,aft) ->
658 let (bd,_) = get_before_e body [] in
659 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
660 | Ast.Do(header,body,tail) ->
661 let (bd,_) = get_before_e body [] in
662 (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
663 | Ast.Iterator(header,body,aft) ->
664 let (bd,_) = get_before_e body [] in
665 (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
666 | Ast.Switch(header,lb,cases,rb) ->
669 (function case_line ->
670 match Ast.unwrap case_line with
671 Ast.CaseLine(header,body) ->
672 let (body,_) = get_before body [] in
673 Ast.rewrap case_line (Ast.CaseLine(header,body))
674 | Ast.OptCase(case_line) -> failwith "not supported")
676 (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
677 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
678 let (de,dea) = get_before decls [] in
679 let (bd,_) = get_before body dea in
680 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
682 Pretty_print_cocci.statement "" s; Format.print_newline();
683 failwith "get_before_e: not supported"
685 let rec get_after sl a =
686 match Ast.unwrap sl with
692 let (sl,sla) = loop sl in
693 let (e,ea) = get_after_e e sla in
695 let (l,a) = loop x in
696 (Ast.rewrap sl (Ast.DOTS(l)),a)
697 | Ast.CIRCLES(x) -> failwith "not supported"
698 | Ast.STARS(x) -> failwith "not supported"
700 and get_after_whencode a wc =
703 Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w
704 | Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w
705 | Ast.WhenModifier(x) -> Ast.WhenModifier(x)
706 | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
707 | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
710 and get_after_e s a =
711 match Ast.unwrap s with
712 Ast.Dots(d,w,bef,_) ->
713 (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)
714 | Ast.Nest(stmt_dots,w,multi,bef,_) ->
715 let w = get_after_whencode a w in
716 let (sd,_) = get_after stmt_dots a in
722 Unify_ast.unify_statement_dots
723 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
725 Unify_ast.MAYBE -> false
727 | Ast.Other_dots a ->
728 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
730 Unify_ast.MAYBE -> false
734 (Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
735 | Ast.Disj(stmt_dots_list) ->
737 List.split (List.map (function e -> get_after e a) stmt_dots_list) in
738 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
740 (match Ast.unwrap ast with
741 Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots _,i) ->
742 (* check "after" information for metavar optimization *)
743 (* if the error is not desired, could just return [], then
744 the optimization (check for EF) won't take place *)
748 (match Ast.unwrap x with
749 Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
751 "dots/nest not allowed before and after stmt metavar"
753 | Ast.Other_dots x ->
754 (match Ast.undots x with
756 (match Ast.unwrap x with
757 Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
759 ("dots/nest not allowed before and after stmt "^
768 (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
769 | Ast.MetaStmt(_,_,_,_) -> (s,[])
770 | _ -> (s,[Ast.Other s]))
771 | Ast.Seq(lbrace,decls,body,rbrace) ->
772 let index = count_nested_braces s in
773 let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
774 let (de,_) = get_after decls bda in
775 (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
776 [Ast.WParen(lbrace,index)])
777 | Ast.Define(header,body) ->
778 let (body,_) = get_after body a in
779 (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
780 | Ast.IfThen(ifheader,branch,aft) ->
781 let (br,_) = get_after_e branch a in
782 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s])
783 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
784 let (br1,_) = get_after_e branch1 a in
785 let (br2,_) = get_after_e branch2 a in
786 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
787 | Ast.While(header,body,aft) ->
788 let (bd,_) = get_after_e body a in
789 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
790 | Ast.For(header,body,aft) ->
791 let (bd,_) = get_after_e body a in
792 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
793 | Ast.Do(header,body,tail) ->
794 let (bd,_) = get_after_e body a in
795 (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
796 | Ast.Iterator(header,body,aft) ->
797 let (bd,_) = get_after_e body a in
798 (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
799 | Ast.Switch(header,lb,cases,rb) ->
802 (function case_line ->
803 match Ast.unwrap case_line with
804 Ast.CaseLine(header,body) ->
805 let (body,_) = get_after body [] in
806 Ast.rewrap case_line (Ast.CaseLine(header,body))
807 | Ast.OptCase(case_line) -> failwith "not supported")
809 (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
810 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
811 let (bd,bda) = get_after body [] in
812 let (de,_) = get_after decls bda in
813 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
814 | _ -> failwith "get_after_e: not supported"
816 let preprocess_dots sl =
817 let (sl,_) = get_before sl [] in
818 let (sl,_) = get_after sl [] in
821 let preprocess_dots_e sl =
822 let (sl,_) = get_before_e sl [] in
823 let (sl,_) = get_after_e sl [] in
826 (* --------------------------------------------------------------------- *)
827 (* various return_related things *)
829 let rec ends_in_return stmt_list =
830 match Ast.unwrap stmt_list with
832 (match List.rev x with
834 (match Ast.unwrap x with
837 match Ast.unwrap x with
838 Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true
839 | Ast.DisjRuleElem((_::_) as l) -> List.for_all loop l
842 | Ast.Disj(disjs) -> List.for_all ends_in_return disjs
845 | Ast.CIRCLES(x) -> failwith "not supported"
846 | Ast.STARS(x) -> failwith "not supported"
848 (* --------------------------------------------------------------------- *)
851 let exptymatch l make_match make_guard_match =
852 let pos = fresh_pos() in
853 let matches_guard_matches =
856 let pos = Ast.make_mcode pos in
857 (make_match (Ast.set_pos x (Some pos)),
858 make_guard_match (Ast.set_pos x (Some pos))))
860 let (matches,guard_matches) = List.split matches_guard_matches in
861 let rec suffixes = function
863 | x::xs -> xs::(suffixes xs) in
864 let prefixes = List.rev (suffixes (List.rev guard_matches)) in
865 let info = (* not null *)
871 ctl_and CTL.NONSTRICT matcher
873 (ctl_uncheck (List.fold_left ctl_or_fl CTL.False negates)))))
875 CTL.InnerAnd(List.fold_left ctl_or_fl CTL.False (List.rev info))
877 (* code might be a DisjRuleElem, in which case we break it apart
878 code might contain an Exp or Ty
879 this one pushes the quantifier inwards *)
880 let do_re_matches label guard res quantified minus_quantified =
881 let make_guard_match x =
882 let stmt_fvs = Ast.get_mfvs x in
883 let fvs = get_unquantified minus_quantified stmt_fvs in
884 non_saved_quantify fvs (make_match None true x) in
886 let stmt_fvs = Ast.get_fvs x in
887 let fvs = get_unquantified quantified stmt_fvs in
888 quantify guard fvs (make_match None guard x) in
889 ctl_and CTL.NONSTRICT (label_pred_maker label)
890 (match List.map Ast.unwrap res with
891 [] -> failwith "unexpected empty disj"
892 | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match
893 | Ast.Ty(t)::rest -> exptymatch res make_match make_guard_match
895 if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
897 then failwith "unexpected exp or ty";
898 List.fold_left ctl_seqor CTL.False
899 (List.rev (List.map make_match res)))
901 (* code might be a DisjRuleElem, in which case we break it apart
902 code doesn't contain an Exp or Ty
903 this one is for use when it is not practical to push the quantifier inwards
905 let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl =
906 match Ast.unwrap code with
907 Ast.DisjRuleElem(res) ->
908 let make_match = make_match None guard in
909 let orop = if guard then ctl_or else ctl_seqor in
910 ctl_and CTL.NONSTRICT (label_pred_maker label)
911 (List.fold_left orop CTL.False (List.map make_match res))
912 | _ -> make_match label guard code
914 (* --------------------------------------------------------------------- *)
915 (* control structures *)
917 let end_control_structure fvs header body after_pred
918 after_checks no_after_checks (afvs,afresh,ainh,aft) after label guard =
919 (* aft indicates what is added after the whole if, which has to be added
921 let (aft_needed,after_branch) =
923 Ast.CONTEXT(_,Ast.NOTHING) ->
924 (false,make_seq_after2 guard after_pred after)
927 make_match label guard
928 (make_meta_rule_elem aft (afvs,afresh,ainh)) in
930 make_seq_after guard after_pred
931 (After(make_seq_after guard match_endif after))) in
932 let body = body after_branch in
933 let s = guard_to_strict guard in
938 (match (after,aft_needed) with
939 (After _,_) (* pattern doesn't end here *)
940 | (_,true) (* + code added after *) -> after_checks
941 | _ -> no_after_checks)
942 (ctl_ax_absolute s body)))
944 let ifthen ifheader branch ((afvs,_,_,_) as aft) after
945 quantified minus_quantified label llabel slabel recurse make_match guard =
946 (* "if (test) thn" becomes:
947 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
949 "if (test) thn; after" becomes:
950 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
955 match seq_fvs quantified
956 [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with
957 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
958 | _ -> failwith "not possible" in
959 let new_quantified = Common.union_set bfvs quantified in
961 match seq_fvs minus_quantified
962 [Ast.get_mfvs ifheader;Ast.get_mfvs branch;[]] with
963 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
964 | _ -> failwith "not possible" in
965 let new_mquantified = Common.union_set mbfvs minus_quantified in
967 let if_header = quantify guard efvs (make_match ifheader) in
968 (* then branch and after *)
969 let lv = get_label_ctr() in
970 let used = ref false in
973 [truepred label; recurse branch Tail new_quantified new_mquantified
974 (Some (lv,used)) llabel slabel guard] in
975 let after_pred = aftpred label in
976 let or_cases after_branch =
977 ctl_or true_branch (ctl_or (fallpred label) after_branch) in
978 let (if_header,wrapper) =
981 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
982 (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
983 (function body -> quantify true [lv] body))
984 else (if_header,function x -> x) in
986 (end_control_structure bfvs if_header or_cases after_pred
987 (Some(ctl_ex after_pred)) None aft after label guard)
989 let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
990 quantified minus_quantified label llabel slabel recurse make_match guard =
991 (* "if (test) thn else els" becomes:
992 if(test) & AX((TrueBranch & AX thn) v
993 (FalseBranch & AX (else & AX els)) v After)
996 "if (test) thn else els; after" becomes:
997 if(test) & AX((TrueBranch & AX thn) v
998 (FalseBranch & AX (else & AX els)) v
999 (After & AXAX after))
1003 (* free variables *)
1004 let (e1fvs,b1fvs,s1fvs) =
1005 match seq_fvs quantified
1006 [Ast.get_fvs ifheader;Ast.get_fvs branch1;afvs] with
1007 [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
1008 (e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
1009 | _ -> failwith "not possible" in
1010 let (e2fvs,b2fvs,s2fvs) =
1012 match seq_fvs quantified
1013 [Ast.get_fvs ifheader;Ast.get_fvs branch2;afvs] with
1014 [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1015 (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1016 | _ -> failwith "not possible" in
1017 let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
1018 let exponlyfvs = intersect e1fvs e2fvs in
1019 let new_quantified = union bothfvs quantified in
1020 (* minus free variables *)
1021 let (me1fvs,mb1fvs,ms1fvs) =
1022 match seq_fvs minus_quantified
1023 [Ast.get_mfvs ifheader;Ast.get_mfvs branch1;[]] with
1024 [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
1025 (e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
1026 | _ -> failwith "not possible" in
1027 let (me2fvs,mb2fvs,ms2fvs) =
1029 match seq_fvs minus_quantified
1030 [Ast.get_mfvs ifheader;Ast.get_mfvs branch2;[]] with
1031 [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1032 (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1033 | _ -> failwith "not possible" in
1034 let mbothfvs = union (union mb1fvs mb2fvs) (intersect ms1fvs ms2fvs) in
1035 let new_mquantified = union mbothfvs minus_quantified in
1037 let if_header = quantify guard exponlyfvs (make_match ifheader) in
1038 (* then and else branches *)
1039 let lv = get_label_ctr() in
1040 let used = ref false in
1043 [truepred label; recurse branch1 Tail new_quantified new_mquantified
1044 (Some (lv,used)) llabel slabel guard] in
1047 [falsepred label; make_match els;
1048 recurse branch2 Tail new_quantified new_mquantified
1049 (Some (lv,used)) llabel slabel guard] in
1050 let after_pred = aftpred label in
1051 let or_cases after_branch =
1052 ctl_or true_branch (ctl_or false_branch after_branch) in
1053 let s = guard_to_strict guard in
1054 let (if_header,wrapper) =
1057 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1058 (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
1059 (function body -> quantify true [lv] body))
1060 else (if_header,function x -> x) in
1062 (end_control_structure bothfvs if_header or_cases after_pred
1063 (Some(ctl_and s (ctl_ex (falsepred label)) (ctl_ex after_pred)))
1064 (Some(ctl_ex (falsepred label)))
1065 aft after label guard)
1067 let forwhile header body ((afvs,_,_,_) as aft) after
1068 quantified minus_quantified label recurse make_match guard =
1070 (* the translation in this case is similar to that of an if with no else *)
1071 (* free variables *)
1073 match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
1074 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
1075 | _ -> failwith "not possible" in
1076 let new_quantified = Common.union_set bfvs quantified in
1077 (* minus free variables *)
1079 match seq_fvs minus_quantified
1080 [Ast.get_mfvs header;Ast.get_mfvs body;[]] with
1081 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
1082 | _ -> failwith "not possible" in
1083 let new_mquantified = Common.union_set mbfvs minus_quantified in
1085 let header = quantify guard efvs (make_match header) in
1086 let lv = get_label_ctr() in
1087 let used = ref false in
1091 recurse body Tail new_quantified new_mquantified
1092 (Some (lv,used)) (Some (lv,used)) None guard] in
1093 let after_pred = fallpred label in
1094 let or_cases after_branch = ctl_or body after_branch in
1095 let (header,wrapper) =
1098 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1099 (ctl_and CTL.NONSTRICT(*???*) header label_pred,
1100 (function body -> quantify true [lv] body))
1101 else (header,function x -> x) in
1103 (end_control_structure bfvs header or_cases after_pred
1104 (Some(ctl_ex after_pred)) None aft after label guard) in
1105 match (Ast.unwrap body,aft) with
1106 (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
1107 (match Ast.unwrap re with
1108 Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),
1109 Type_cocci.Unitary,_,false) ->
1111 match seq_fvs quantified [Ast.get_fvs header] with
1113 | _ -> failwith "not possible" in
1114 quantify guard efvs (make_match header)
1118 (* --------------------------------------------------------------------- *)
1119 (* statement metavariables *)
1121 (* issue: an S metavariable that is not an if branch/loop body
1122 should not match an if branch/loop body, so check that the labels
1123 of the nodes before the first node matched by the S are different
1124 from the label of the first node matched by the S *)
1125 let sequencibility body label_pred process_bef_aft = function
1126 Ast.Sequencible | Ast.SequencibleAfterDots [] ->
1129 (ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
1130 | Ast.SequencibleAfterDots l ->
1131 (* S appears after some dots. l is the code that comes after the S.
1132 want to search for that first, because S can match anything, while
1133 the stuff after is probably more restricted *)
1134 let afts = List.map process_bef_aft l in
1135 let ors = foldl1 ctl_or afts in
1136 ctl_and CTL.NONSTRICT
1137 (ctl_ef (ctl_and CTL.NONSTRICT ors (ctl_back_ax label_pred)))
1140 ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
1141 | Ast.NotSequencible -> body (function x -> x)
1143 let svar_context_with_add_after stmt s label quantified d ast
1144 seqible after process_bef_aft guard fvinfo =
1145 let label_var = (*fresh_label_var*) string2var "_lab" in
1147 CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
1149 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1150 let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1151 let full_metamatch = matcher d in
1152 let first_metamatch =
1155 Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_)) ->
1156 Ast.CONTEXT(pos,Ast.BEFORE(bef))
1157 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1158 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1159 let middle_metamatch =
1162 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1163 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1164 let last_metamatch =
1167 Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft)) ->
1168 Ast.CONTEXT(pos,Ast.AFTER(aft))
1169 | Ast.CONTEXT(_,_) -> d
1170 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1173 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1174 let left_or = (* the whole statement is one node *)
1176 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1177 let right_or = (* the statement covers multiple nodes *)
1180 ctl_au CTL.NONSTRICT
1183 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1185 (ctl_not prelabel_pred) after])] in
1187 ctl_and CTL.NONSTRICT label_pred
1188 (f (ctl_and CTL.NONSTRICT
1189 (make_raw_match label false ast) (ctl_or left_or right_or))) in
1190 let stmt_fvs = Ast.get_fvs stmt in
1191 let fvs = get_unquantified quantified stmt_fvs in
1192 quantify guard (label_var::fvs)
1193 (sequencibility body label_pred process_bef_aft seqible)
1195 let svar_minus_or_no_add_after stmt s label quantified d ast
1196 seqible after process_bef_aft guard fvinfo =
1197 let label_var = (*fresh_label_var*) string2var "_lab" in
1199 CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
1201 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1202 let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1204 (* don't have to put anything before the beginning, so don't have to
1205 distinguish the first node. so don't have to bother about paths,
1206 just use the label. label ensures that found nodes match up with
1207 what they should because it is in the lhs of the andany. *)
1209 Ast.MINUS(pos,[]) -> true
1210 | Ast.CONTEXT(pos,Ast.NOTHING) -> true
1213 match (pure_d,after) with
1214 (true,Tail) | (true,End) | (true,VeryEnd) ->
1215 (* the label sharing makes it safe to use AndAny *)
1216 CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
1217 ctl_and CTL.NONSTRICT label_pred
1218 (make_raw_match label false ast),
1219 ctl_and CTL.NONSTRICT (matcher d) prelabel_pred)
1221 (* more safe but less efficient *)
1222 let first_metamatch = matcher d in
1223 let rest_metamatch =
1226 Ast.MINUS(pos,_) -> Ast.MINUS(pos,[])
1227 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1228 | Ast.PLUS -> failwith "not possible") in
1229 let rest_nodes = ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred in
1230 let last_node = and_after guard (ctl_not prelabel_pred) after in
1231 (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
1234 ctl_au CTL.NONSTRICT rest_nodes last_node])) in
1235 let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
1236 let stmt_fvs = Ast.get_fvs stmt in
1237 let fvs = get_unquantified quantified stmt_fvs in
1238 quantify guard (label_var::fvs)
1239 (sequencibility body label_pred process_bef_aft seqible)
1241 (* --------------------------------------------------------------------- *)
1242 (* dots and nests *)
1244 let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
1245 let matchgoto = gotopred None in
1247 make_match None false
1249 (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in
1251 make_match None false
1253 (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in
1255 if quantifier = Exists
1256 then Common.Left(CTL.False)
1258 then Common.Left(CTL.Or(aftpred label,exitpred label))
1260 then Common.Left(aftpred label)
1264 let lv = get_label_ctr() in
1265 let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1266 let preflabelpred = label_pred_maker (Some (lv,ref true)) in
1267 ctl_or (aftpred label)
1268 (quantify false [lv]
1269 (ctl_and CTL.NONSTRICT
1270 (ctl_and CTL.NONSTRICT (truepred label) labelpred)
1271 (ctl_au CTL.NONSTRICT
1272 (ctl_and CTL.NONSTRICT (ctl_not v) preflabelpred)
1273 (ctl_and CTL.NONSTRICT preflabelpred
1274 (if !Flag_matcher.only_return_is_error_exit
1276 (ctl_and CTL.NONSTRICT
1277 (retpred None) (ctl_not seq_after))
1280 (ctl_and CTL.NONSTRICT
1281 (ctl_or (retpred None) matchcontinue)
1282 (ctl_not seq_after))
1283 (ctl_and CTL.NONSTRICT
1284 (ctl_or matchgoto matchbreak)
1285 (ctl_ag s (ctl_not seq_after)))))))))) in
1286 let op = if quantifier = !exists then ctl_au else ctl_anti_au in
1287 let v = get_let_ctr() in
1289 (match stop_early with
1290 Common.Left x -> ctl_or y x
1291 | Common.Right stop_early ->
1292 CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
1294 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1295 process_bef_aft statement_list statement guard quantified wrapcode =
1296 let ctl_and_ns = ctl_and CTL.NONSTRICT in
1297 (* proces bef_aft *)
1299 List.fold_left ctl_or_fl CTL.False (List.map process_bef_aft l) in
1300 let bef_aft = (* to be negated *)
1304 (function Ast.WhenModifier(Ast.WhenAny) -> true | _ -> false)
1307 with Not_found -> shortest (Common.union_set bef aft) in
1310 (function Ast.WhenModifier(Ast.WhenStrict) -> true | _ -> false)
1312 let check_quantifier quant other =
1314 (function Ast.WhenModifier(x) -> x = quant | _ -> false)
1318 (function Ast.WhenModifier(x) -> x = other | _ -> false)
1320 then failwith "inconsistent annotation on dots"
1324 if check_quantifier Ast.WhenExists Ast.WhenForall
1327 if check_quantifier Ast.WhenForall Ast.WhenExists
1330 (* the following is used when we find a goto, etc and consider accepting
1331 without finding the rest of the pattern *)
1332 let aft = shortest aft in
1333 (* process whencode *)
1334 let labelled = label_pred_maker label in
1336 let (poswhen,negwhen) =
1338 (function (poswhen,negwhen) ->
1340 Ast.WhenNot whencodes ->
1341 (poswhen,ctl_or (statement_list whencodes) negwhen)
1342 | Ast.WhenAlways stm ->
1343 (ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen)
1344 | Ast.WhenModifier(_) -> (poswhen,negwhen)
1345 | Ast.WhenNotTrue(e) ->
1347 ctl_or (whencond_true e label guard quantified) negwhen)
1348 | Ast.WhenNotFalse(e) ->
1350 ctl_or (whencond_false e label guard quantified) negwhen))
1351 (CTL.True,bef_aft) (List.rev whencodes) in
1352 let poswhen = ctl_and_ns arg poswhen in
1356 (* add in After, because it's not part of the program *)
1357 ctl_or (aftpred label) negwhen
1359 ctl_and_ns poswhen (ctl_not negwhen) in
1360 (* process dot code, if any *)
1362 match (dotcode,guard) with
1363 (None,_) | (_,true) -> CTL.True
1364 | (Some dotcode,_) -> dotcode in
1365 (* process nest code, if any *)
1366 (* whencode goes in the negated part of the nest; if no nest, just goes
1367 on the "true" in between code *)
1368 let plus_var = if plus then get_label_ctr() else string2var "" in
1369 let plus_var2 = if plus then get_label_ctr() else string2var "" in
1371 match (nest,guard && not plus) with
1372 (None,_) | (_,true) -> whencodes CTL.True
1373 | (Some nest,false) ->
1374 let v = get_let_ctr() in
1378 (* the idea is that BindGood is sort of a witness; a witness to
1379 having found the subterm in at least one place. If there is
1380 not a witness, then there is a risk that it will get thrown
1381 away, if it is merged with a node that has an empty
1382 environment. See tests/nestplus. But this all seems
1383 rather suspicious *)
1384 CTL.And(CTL.NONSTRICT,x,
1385 CTL.Exists(true,plus_var2,
1386 CTL.Pred(Lib_engine.BindGood(plus_var),
1387 CTL.Modif plus_var2)))
1390 CTL.Or(is_plus (CTL.Ref v),
1391 whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
1392 let plus_modifier x =
1399 CTL.Not(CTL.Pred(Lib_engine.BindBad(plus_var),CTL.Control)))))
1405 | Guard f -> ctl_uncheck f
1407 let exit = endpred label in
1408 let errorexit = exitpred label in
1409 ctl_or exit errorexit
1410 (* not at all sure what the next two mean... *)
1414 Some (lv,used) -> used := true;
1415 ctl_or (CTL.Pred(Lib_engine.Label lv,CTL.Control))
1416 (ctl_back_ex (ctl_or (retpred label) (gotopred label)))
1417 | None -> endpred label)
1418 (* was the following, but not clear why sgrep should allow
1420 let exit = endpred label in
1421 let errorexit = exitpred label in
1423 then ctl_or exit errorexit (* end anywhere *)
1424 else exit (* end at the real end of the function *) *) in
1426 (dots_au is_strict ((after = Tail) or (after = VeryEnd))
1427 label (guard_to_strict guard) wrapcode
1428 (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
1429 aft ender quantifier)
1431 and get_whencond_exps e =
1432 match Ast.unwrap e with
1434 | Ast.DisjRuleElem(res) ->
1435 List.fold_left Common.union_set [] (List.map get_whencond_exps res)
1436 | _ -> failwith "not possible"
1438 and make_whencond_headers e e1 label guard quantified =
1439 let fvs = Ast.get_fvs e in
1441 quantify guard (get_unquantified quantified fvs)
1442 (make_match label guard h) in
1447 (Ast.make_mcode "if",
1448 Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
1449 let while_header e1 =
1453 (Ast.make_mcode "while",
1454 Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
1459 (Ast.make_mcode "for",Ast.make_mcode "(",None,Ast.make_mcode ";",
1460 Some e1,Ast.make_mcode ";",None,Ast.make_mcode ")"))) in
1462 List.fold_left ctl_or CTL.False (List.map if_header e1) in
1464 List.fold_left ctl_or CTL.False (List.map while_header e1) in
1466 List.fold_left ctl_or CTL.False (List.map for_header e1) in
1467 (if_headers, while_headers, for_headers)
1469 and whencond_true e label guard quantified =
1470 let e1 = get_whencond_exps e in
1471 let (if_headers, while_headers, for_headers) =
1472 make_whencond_headers e e1 label guard quantified in
1474 (ctl_and CTL.NONSTRICT (truepred label) (ctl_back_ex if_headers))
1475 (ctl_and CTL.NONSTRICT
1476 (inlooppred label) (ctl_back_ex (ctl_or while_headers for_headers)))
1478 and whencond_false e label guard quantified =
1479 let e1 = get_whencond_exps e in
1480 let (if_headers, while_headers, for_headers) =
1481 make_whencond_headers e e1 label guard quantified in
1482 ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
1483 (ctl_and CTL.NONSTRICT (fallpred label)
1484 (ctl_or (ctl_back_ex if_headers)
1485 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1487 (* --------------------------------------------------------------------- *)
1488 (* the main translation loop *)
1490 let rec statement_list stmt_list after quantified minus_quantified
1491 label llabel slabel dots_before guard =
1493 (* include Disj to be on the safe side *)
1494 match Ast.unwrap x with
1495 Ast.Dots _ | Ast.Nest _ | Ast.Disj _ -> true | _ -> false in
1496 let compute_label l e db = if db or isdots e then l else None in
1497 match Ast.unwrap stmt_list with
1499 let rec loop quantified minus_quantified dots_before label llabel slabel
1501 ([],_,_) -> (match after with After f -> f | _ -> CTL.True)
1503 statement e after quantified minus_quantified
1504 (compute_label label e dots_before)
1506 | (e::sl,fv::fvs,mfv::mfvs) ->
1507 let shared = intersectll fv fvs in
1508 let unqshared = get_unquantified quantified shared in
1509 let new_quantified = Common.union_set unqshared quantified in
1510 let minus_shared = intersectll mfv mfvs in
1512 get_unquantified minus_quantified minus_shared in
1513 let new_mquantified =
1514 Common.union_set munqshared minus_quantified in
1515 quantify guard unqshared
1518 (let (label1,llabel1,slabel1) =
1519 match Ast.unwrap e with
1521 (match Ast.unwrap re with
1522 Ast.Goto _ -> (None,None,None)
1523 | _ -> (label,llabel,slabel))
1524 | _ -> (label,llabel,slabel) in
1525 loop new_quantified new_mquantified (isdots e)
1526 label1 llabel1 slabel1
1528 new_quantified new_mquantified
1529 (compute_label label e dots_before) llabel slabel guard)
1530 | _ -> failwith "not possible" in
1531 loop quantified minus_quantified dots_before
1533 (x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x)
1534 | Ast.CIRCLES(x) -> failwith "not supported"
1535 | Ast.STARS(x) -> failwith "not supported"
1537 (* llabel is the label of the enclosing loop and slabel is the label of the
1539 and statement stmt after quantified minus_quantified
1540 label llabel slabel guard =
1541 let ctl_au = ctl_au CTL.NONSTRICT in
1542 let ctl_ax = ctl_ax CTL.NONSTRICT in
1543 let ctl_and = ctl_and CTL.NONSTRICT in
1544 let make_seq = make_seq guard in
1545 let make_seq_after = make_seq_after guard in
1546 let real_make_match = make_match in
1547 let make_match = header_match label guard in
1549 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1552 match Ast.unwrap stmt with
1554 (match Ast.unwrap ast with
1555 (* the following optimisation is not a good idea, because when S
1556 is alone, we would like it not to match a declaration.
1557 this makes more matching for things like when (...) S, but perhaps
1558 that matching is not so costly anyway *)
1559 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1560 | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_)) as d),_),
1562 | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_)) as d),_),
1564 svar_context_with_add_after stmt s label quantified d ast seqible
1566 (process_bef_aft quantified minus_quantified
1567 label llabel slabel true)
1569 (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)
1571 | Ast.MetaStmt((s,_,d,_),keep,seqible,_) ->
1572 svar_minus_or_no_add_after stmt s label quantified d ast seqible
1574 (process_bef_aft quantified minus_quantified
1575 label llabel slabel true)
1577 (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)
1581 match Ast.unwrap ast with
1582 Ast.DisjRuleElem(res) ->
1583 do_re_matches label guard res quantified minus_quantified
1584 | Ast.Exp(_) | Ast.Ty(_) ->
1585 let stmt_fvs = Ast.get_fvs stmt in
1586 let fvs = get_unquantified quantified stmt_fvs in
1587 CTL.InnerAnd(quantify guard fvs (make_match ast))
1589 let stmt_fvs = Ast.get_fvs stmt in
1590 let fvs = get_unquantified quantified stmt_fvs in
1591 quantify guard fvs (make_match ast) in
1592 match Ast.unwrap ast with
1593 Ast.Break(brk,semi) ->
1594 (match (llabel,slabel) with
1595 (_,Some(lv,used)) -> (* use switch label if there is one *)
1596 ctl_and term (bclabel_pred_maker slabel)
1597 | _ -> ctl_and term (bclabel_pred_maker llabel))
1598 | Ast.Continue(brk,semi) -> ctl_and term (bclabel_pred_maker llabel)
1599 | Ast.Return((_,info,retmc,pos),(_,_,semmc,_)) ->
1600 (* discard pattern that comes after return *)
1601 let normal_res = make_seq_after term after in
1602 (* the following code tries to propagate the modifications on
1603 return; to a close brace, in the case where the final return
1606 match (retmc,semmc) with
1607 (Ast.MINUS(_,l1),Ast.MINUS(_,l2)) when !Flag.sgrep_mode2 ->
1608 (* in sgrep mode, we can propagate the - *)
1609 Some (Ast.MINUS(Ast.NoPos,l1@l2))
1610 | (Ast.MINUS(_,l1),Ast.MINUS(_,l2))
1611 | (Ast.CONTEXT(_,Ast.BEFORE(l1)),
1612 Ast.CONTEXT(_,Ast.AFTER(l2))) ->
1613 Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2)))
1614 | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
1615 | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
1617 | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.AFTER(l))) ->
1618 Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l)))
1620 let ret = Ast.make_mcode "return" in
1622 Ast.rewrap ast (Ast.Edots(Ast.make_mcode "...",None)) in
1623 let semi = Ast.make_mcode ";" in
1625 make_match(Ast.rewrap ast (Ast.Return(ret,semi))) in
1627 make_match(Ast.rewrap ast (Ast.ReturnExpr(ret,edots,semi))) in
1630 let exit = endpred None in
1632 Ast.rewrap ast (Ast.SeqEnd (("}",info,new_mc,pos))) in
1633 let stripped_rbrace =
1634 Ast.rewrap ast (Ast.SeqEnd(Ast.make_mcode "}")) in
1636 (ctl_and (make_match mod_rbrace)
1641 (ctl_or simple_return return_expr))))
1643 (make_match stripped_rbrace)
1644 (* error exit not possible; it is in the middle
1645 of code, so a return is needed *)
1648 (* some change in the middle of the return, so have to
1649 find an actual return *)
1652 (* should try to deal with the dots_bef_aft problem elsewhere,
1653 but don't have the courage... *)
1658 do_between_dots stmt term End
1659 quantified minus_quantified label llabel slabel guard in
1661 make_seq_after term after)
1662 | Ast.Seq(lbrace,decls,body,rbrace) ->
1663 let (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs) =
1666 [Ast.get_fvs lbrace;Ast.get_fvs decls;
1667 Ast.get_fvs body;Ast.get_fvs rbrace]
1669 [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
1670 (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
1671 | _ -> failwith "not possible" in
1672 let (mlbfvs,mb1fvs,mb2fvs,mb3fvs,mrbfvs) =
1674 seq_fvs minus_quantified
1675 [Ast.get_mfvs lbrace;Ast.get_mfvs decls;
1676 Ast.get_mfvs body;Ast.get_mfvs rbrace]
1678 [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
1679 (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
1680 | _ -> failwith "not possible" in
1681 let pv = count_nested_braces stmt in
1682 let lv = get_label_ctr() in
1683 let paren_pred = CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
1684 let label_pred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1687 (quantify guard lbfvs (make_match lbrace))
1688 (ctl_and paren_pred label_pred) in
1690 match Ast.unwrap rbrace with
1691 Ast.SeqEnd((data,info,_,pos)) ->
1692 Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data))
1693 | _ -> failwith "unexpected close brace" in
1695 (* label is not needed; paren_pred is enough *)
1696 quantify guard rbfvs
1697 (ctl_au (make_match empty_rbrace)
1699 (real_make_match None guard rbrace)
1701 let new_quantified2 =
1702 Common.union_set b1fvs (Common.union_set b2fvs quantified) in
1703 let new_quantified3 = Common.union_set b3fvs new_quantified2 in
1704 let new_mquantified2 =
1705 Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in
1706 let new_mquantified3 = Common.union_set mb3fvs new_mquantified2 in
1707 let pattern_as_given =
1708 let new_quantified2 = Common.union_set [pv] new_quantified2 in
1709 let new_quantified3 = Common.union_set [pv] new_quantified3 in
1710 quantify true [pv;lv]
1711 (quantify guard b1fvs
1714 quantify guard b2fvs
1715 (statement_list decls
1717 (quantify guard b3fvs
1718 (statement_list body
1719 (After (make_seq_after end_brace after))
1720 new_quantified3 new_mquantified3
1721 (Some (lv,ref true)) (* label mostly useful *)
1722 llabel slabel true guard)))
1723 new_quantified2 new_mquantified2
1724 (Some (lv,ref true)) llabel slabel false guard)])) in
1725 if ends_in_return body
1727 (* matching error handling code *)
1729 1. The pattern as given
1730 2. A goto, and then some close braces, and then the pattern as
1731 given, but without the braces (only possible if there are no
1732 decls, and open and close braces are unmodified)
1733 3. Part of the pattern as given, then a goto, and then the rest
1734 of the pattern. For this case, we just check that all paths have
1735 a goto within the current braces. checking for a goto at every
1736 point in the pattern seems expensive and not worthwhile. *)
1738 let body = preprocess_dots body in (* redo, to drop braces *)
1742 (make_match empty_rbrace)
1743 (ctl_ax (* skip the destination label *)
1744 (quantify guard b3fvs
1745 (statement_list body End
1746 new_quantified3 new_mquantified3 None llabel slabel
1749 let new_quantified2 = Common.union_set [pv] new_quantified2 in
1750 let new_quantified3 = Common.union_set [pv] new_quantified3 in
1751 quantify true [pv;lv]
1752 (quantify guard b1fvs
1756 (CTL.AU (* want AF even for sgrep *)
1757 (CTL.FORWARD,CTL.STRICT,
1758 CTL.Pred(Lib_engine.PrefixLabel(lv),CTL.Control),
1759 ctl_and (* brace must be eventually after goto *)
1760 (gotopred (Some (lv,ref true)))
1761 (* want AF even for sgrep *)
1762 (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
1763 (quantify guard b2fvs
1764 (statement_list decls
1766 (quantify guard b3fvs
1767 (statement_list body Tail
1770 nopv_end_brace after)*)
1771 new_quantified3 new_mquantified3
1772 None llabel slabel true guard)))
1773 new_quantified2 new_mquantified2
1774 (Some (lv,ref true))
1775 llabel slabel false guard))])) in
1776 ctl_or pattern_as_given
1777 (match Ast.unwrap decls with
1778 Ast.DOTS([]) -> ctl_or pattern2 pattern3
1779 | Ast.DOTS(l) -> pattern3
1780 | _ -> failwith "circles and stars not supported")
1781 else pattern_as_given
1782 | Ast.IfThen(ifheader,branch,aft) ->
1783 ifthen ifheader branch aft after quantified minus_quantified
1784 label llabel slabel statement make_match guard
1786 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
1787 ifthenelse ifheader branch1 els branch2 aft after quantified
1788 minus_quantified label llabel slabel statement make_match guard
1790 | Ast.While(header,body,aft) | Ast.For(header,body,aft)
1791 | Ast.Iterator(header,body,aft) ->
1792 forwhile header body aft after quantified minus_quantified
1793 label statement make_match guard
1795 | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
1797 (label_pred_maker label)
1798 (List.fold_left ctl_seqor CTL.False
1801 statement_list sl after quantified minus_quantified label
1802 llabel slabel true guard)
1805 | Ast.Nest(stmt_dots,whencode,multi,bef,aft) ->
1806 (* label in recursive call is None because label check is already
1807 wrapped around the corresponding code *)
1810 match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
1812 [(wcfvs,bothfvs);(bdfvs,_)] -> bothfvs
1813 | _ -> failwith "not possible" in
1815 (* no minus version because when code doesn't contain any minus code *)
1816 let new_quantified = Common.union_set bfvs quantified in
1820 statement_list stmt_dots (a2n after) new_quantified minus_quantified
1821 None llabel slabel true guard in
1822 dots_and_nests multi
1823 (Some dots_pattern) whencode bef aft None after label
1824 (process_bef_aft new_quantified minus_quantified
1825 None llabel slabel true)
1827 statement_list x Tail new_quantified minus_quantified None
1828 llabel slabel true true)
1830 statement x Tail new_quantified minus_quantified None
1833 (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
1835 | Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
1839 (* no need for the fresh metavar, but ... is a bit wierd as a
1841 Some(make_match (make_meta_rule_elem d ([],[],[])))
1843 dots_and_nests false None whencodes bef aft dot_code after label
1844 (process_bef_aft quantified minus_quantified None llabel slabel true)
1846 statement_list x Tail quantified minus_quantified
1847 None llabel slabel true true)
1849 statement x Tail quantified minus_quantified None llabel slabel true)
1851 (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
1853 | Ast.Switch(header,lb,cases,rb) ->
1854 let rec intersect_all = function
1857 | x::xs -> intersect x (intersect_all xs) in
1858 let rec union_all l = List.fold_left union [] l in
1859 (* start normal variables *)
1860 let header_fvs = Ast.get_fvs header in
1861 let lb_fvs = Ast.get_fvs lb in
1862 let case_fvs = List.map Ast.get_fvs cases in
1863 let rb_fvs = Ast.get_fvs rb in
1864 let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1865 all_casefvs,all_b3fvs,all_rbfvs) =
1867 (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1868 all_casefvs,all_b3fvs,all_rbfvs) ->
1869 function case_fvs ->
1870 match seq_fvs quantified [header_fvs;lb_fvs;case_fvs;rb_fvs] with
1871 [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
1872 (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
1873 b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
1875 | _ -> failwith "not possible")
1876 ([],[],[],[],[],[],[]) case_fvs in
1877 let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1878 all_casefvs,all_b3fvs,all_rbfvs) =
1879 (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,
1880 List.rev all_b2fvs,List.rev all_casefvs,List.rev all_b3fvs,
1881 List.rev all_rbfvs) in
1882 let exponlyfvs = intersect_all all_efvs in
1883 let lbonlyfvs = intersect_all all_lbfvs in
1884 (* don't do anything with right brace. Hope there is no + code on it *)
1885 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1886 let b1fvs = union_all all_b1fvs in
1887 let new1_quantified = union b1fvs quantified in
1888 let b2fvs = union (union_all all_b1fvs) (intersect_all all_casefvs) in
1889 let new2_quantified = union b2fvs new1_quantified in
1890 (* let b3fvs = union_all all_b3fvs in*)
1891 (* ------------------- start minus free variables *)
1892 let header_mfvs = Ast.get_mfvs header in
1893 let lb_mfvs = Ast.get_mfvs lb in
1894 let case_mfvs = List.map Ast.get_mfvs cases in
1895 let rb_mfvs = Ast.get_mfvs rb in
1896 let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
1897 all_mcasefvs,all_mb3fvs,all_mrbfvs) =
1899 (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1900 all_casefvs,all_b3fvs,all_rbfvs) ->
1901 function case_mfvs ->
1904 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1905 [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
1906 (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
1907 b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
1909 | _ -> failwith "not possible")
1910 ([],[],[],[],[],[],[]) case_mfvs in
1911 let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
1912 all_mcasefvs,all_mb3fvs,all_mrbfvs) =
1913 (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,
1914 List.rev all_mb2fvs,List.rev all_mcasefvs,List.rev all_mb3fvs,
1915 List.rev all_mrbfvs) in
1916 (* don't do anything with right brace. Hope there is no + code on it *)
1917 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1918 let mb1fvs = union_all all_mb1fvs in
1919 let new1_mquantified = union mb1fvs quantified in
1920 let mb2fvs = union (union_all all_mb1fvs) (intersect_all all_mcasefvs) in
1921 let new2_mquantified = union mb2fvs new1_mquantified in
1922 (* let b3fvs = union_all all_b3fvs in*)
1923 (* ------------------- end collection of free variables *)
1924 let switch_header = quantify guard exponlyfvs (make_match header) in
1925 let lb = quantify guard lbonlyfvs (make_match lb) in
1926 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
1929 (function case_line ->
1930 match Ast.unwrap case_line with
1931 Ast.CaseLine(header,body) ->
1933 match seq_fvs new2_quantified [Ast.get_fvs header] with
1934 [(e1fvs,_)] -> e1fvs
1935 | _ -> failwith "not possible" in
1936 quantify guard e1fvs (real_make_match label true header)
1937 | Ast.OptCase(case_line) -> failwith "not supported")
1940 ctl_not (List.fold_left ctl_or_fl CTL.False case_headers) in
1941 let lv = get_label_ctr() in
1942 let used = ref false in
1945 (function case_line ->
1946 match Ast.unwrap case_line with
1947 Ast.CaseLine(header,body) ->
1948 let (e1fvs,b1fvs,s1fvs) =
1949 let fvs = [Ast.get_fvs header;Ast.get_fvs body] in
1950 match seq_fvs new2_quantified fvs with
1951 [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
1952 | _ -> failwith "not possible" in
1953 let (me1fvs,mb1fvs,ms1fvs) =
1954 let fvs = [Ast.get_mfvs header;Ast.get_mfvs body] in
1955 match seq_fvs new2_mquantified fvs with
1956 [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
1957 | _ -> failwith "not possible" in
1959 quantify guard e1fvs (make_match header) in
1960 let new3_quantified = union b1fvs new2_quantified in
1961 let new3_mquantified = union mb1fvs new2_mquantified in
1963 statement_list body Tail
1964 new3_quantified new3_mquantified label llabel
1965 (Some (lv,used)) true(*?*) guard in
1966 quantify guard b1fvs (make_seq [case_header; body])
1967 | Ast.OptCase(case_line) -> failwith "not supported")
1969 let default_required =
1972 match Ast.unwrap case with
1973 Ast.CaseLine(header,_) ->
1974 (match Ast.unwrap header with
1975 Ast.Default(_,_) -> true
1979 then function x -> x
1980 else function x -> ctl_or (fallpred label) x in
1981 let after_pred = aftpred label in
1982 let body after_branch =
1985 (quantify guard b2fvs
1988 (List.fold_left ctl_and CTL.True
1989 (List.map ctl_ex case_headers));
1990 List.fold_left ctl_or_fl no_header case_code])))
1993 (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,
1994 match Ast.unwrap rb with
1995 Ast.SeqEnd(rb) -> Ast.get_mcodekind rb
1996 | _ -> failwith "not possible") in
1997 let (switch_header,wrapper) =
2000 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
2001 (ctl_and switch_header label_pred,
2002 (function body -> quantify true [lv] body))
2003 else (switch_header,function x -> x) in
2005 (end_control_structure b1fvs switch_header body
2006 after_pred (Some(ctl_ex after_pred)) None aft after label guard)
2007 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
2008 let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs) =
2011 [Ast.get_fvs header;Ast.get_fvs lbrace;Ast.get_fvs decls;
2012 Ast.get_fvs body;Ast.get_fvs rbrace]
2014 [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
2015 (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
2016 | _ -> failwith "not possible" in
2017 let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mb4fvs,mrbfvs) =
2020 [Ast.get_mfvs header;Ast.get_mfvs lbrace;Ast.get_mfvs decls;
2021 Ast.get_mfvs body;Ast.get_mfvs rbrace]
2023 [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
2024 (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
2025 | _ -> failwith "not possible" in
2026 let function_header = quantify guard hfvs (make_match header) in
2027 let start_brace = quantify guard lbfvs (make_match lbrace) in
2028 let stripped_rbrace =
2029 match Ast.unwrap rbrace with
2030 Ast.SeqEnd((data,info,_,_)) ->
2031 Ast.rewrap rbrace(Ast.SeqEnd (Ast.make_mcode data))
2032 | _ -> failwith "unexpected close brace" in
2034 let exit = CTL.Pred (Lib_engine.Exit,CTL.Control) in
2035 let errorexit = CTL.Pred (Lib_engine.ErrorExit,CTL.Control) in
2036 let fake_brace = CTL.Pred (Lib_engine.FakeBrace,CTL.Control) in
2038 (quantify guard rbfvs (make_match rbrace))
2040 (* the following finds the beginning of the fake braces,
2041 if there are any, not completely sure how this works.
2042 sse the examples sw and return *)
2043 (ctl_back_ex (ctl_not fake_brace))
2044 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2045 let new_quantified3 =
2046 Common.union_set b1fvs
2047 (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
2048 let new_quantified4 = Common.union_set b4fvs new_quantified3 in
2049 let new_mquantified3 =
2050 Common.union_set mb1fvs
2051 (Common.union_set mb2fvs
2052 (Common.union_set mb3fvs minus_quantified)) in
2053 let new_mquantified4 = Common.union_set mb4fvs new_mquantified3 in
2055 match (Ast.undots decls,Ast.undots body,
2056 contains_modif rbrace or contains_pos rbrace) with
2057 ([],[body],false) ->
2058 (match Ast.unwrap body with
2059 Ast.Nest(stmt_dots,[],multi,_,_) ->
2061 then None (* not sure how to optimize this case *)
2062 else Some (Common.Left stmt_dots)
2063 | Ast.Dots(_,whencode,_,_) when
2065 (* flow sensitive, so not optimizable *)
2066 (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2068 | _ -> true) whencode) ->
2069 Some (Common.Right whencode)
2074 Some (Common.Left stmt_dots) ->
2075 (* special case for function header + body - header is unambiguous
2076 and unique, so we can just look for the nested body anywhere
2079 (CTL.FORWARD,guard_to_strict guard,start_brace,
2080 statement_list stmt_dots
2081 (* discards match on right brace, but don't need it *)
2082 (Guard (make_seq_after end_brace after))
2083 new_quantified4 new_mquantified4
2084 None llabel slabel true guard)
2085 | Some (Common.Right whencode) ->
2086 (* try to be more efficient for the case where the body is just
2087 ... Perhaps this is too much of a special case, but useful
2088 for dropping a parameter and checking that it is never used. *)
2100 Ast.WhenAlways(s) -> prev
2101 | Ast.WhenNot(sl) ->
2103 statement_list sl Tail
2104 new_quantified4 new_mquantified4
2105 label llabel slabel true true in
2107 | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2108 failwith "unexpected"
2109 | Ast.WhenModifier(Ast.WhenAny) -> CTL.False
2110 | Ast.WhenModifier(_) -> prev)
2111 CTL.False whencode))
2115 Ast.WhenAlways(s) ->
2118 new_quantified4 new_mquantified4
2119 label llabel slabel true in
2121 | Ast.WhenNot(sl) -> prev
2122 | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2123 failwith "unexpected"
2124 | Ast.WhenModifier(Ast.WhenAny) -> CTL.True
2125 | Ast.WhenModifier(_) -> prev)
2126 CTL.True whencode) in
2127 ctl_au leftarg (make_match stripped_rbrace)]
2131 quantify guard b3fvs
2132 (statement_list decls
2134 (quantify guard b4fvs
2135 (statement_list body
2136 (After (make_seq_after end_brace after))
2137 new_quantified4 new_mquantified4
2138 None llabel slabel true guard)))
2139 new_quantified3 new_mquantified3 None llabel slabel
2141 quantify guard b1fvs
2142 (make_seq [function_header; quantify guard b2fvs body_code])
2143 | Ast.Define(header,body) ->
2144 let (hfvs,bfvs,bodyfvs) =
2145 match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body]
2147 [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
2148 | _ -> failwith "not possible" in
2149 let (mhfvs,mbfvs,mbodyfvs) =
2150 match seq_fvs minus_quantified [Ast.get_mfvs header;Ast.get_mfvs body]
2152 [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
2153 | _ -> failwith "not possible" in
2154 let define_header = quantify guard hfvs (make_match header) in
2156 statement_list body after
2157 (Common.union_set bfvs quantified)
2158 (Common.union_set mbfvs minus_quantified)
2159 None llabel slabel true guard in
2160 quantify guard bfvs (make_seq [define_header; body_code])
2161 | Ast.OptStm(stm) ->
2162 failwith "OptStm should have been compiled away\n"
2163 | Ast.UniqueStm(stm) -> failwith "arities not yet supported"
2164 | _ -> failwith "not supported" in
2165 if guard or !dots_done
2168 do_between_dots stmt term after quantified minus_quantified
2169 label llabel slabel guard
2171 (* term is the translation of stmt *)
2172 and do_between_dots stmt term after quantified minus_quantified
2173 label llabel slabel guard =
2174 match Ast.get_dots_bef_aft stmt with
2175 Ast.AddingBetweenDots (brace_term,n)
2176 | Ast.DroppingBetweenDots (brace_term,n) ->
2178 statement brace_term after quantified minus_quantified
2179 label llabel slabel guard in
2180 let v = Printf.sprintf "_r_%d" n in
2181 let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in
2182 let case2 = ctl_and CTL.NONSTRICT (ctl_not (CTL.Ref v)) term in
2185 (ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
2186 (ctl_back_ex (ctl_back_ex (falsepred label))),
2188 | Ast.NoDots -> term
2190 (* un_process_bef_aft is because we don't want to do transformation in this
2191 code, and thus don't case about braces before or after it *)
2192 and process_bef_aft quantified minus_quantified label llabel slabel guard =
2194 Ast.WParen (re,n) ->
2195 let paren_pred = CTL.Pred (Lib_engine.Paren n,CTL.Control) in
2196 let s = guard_to_strict guard in
2197 quantify true (get_unquantified quantified [n])
2198 (ctl_and s (make_raw_match None guard re) paren_pred)
2200 statement s Tail quantified minus_quantified label llabel slabel guard
2201 | Ast.Other_dots d ->
2202 statement_list d Tail quantified minus_quantified
2203 label llabel slabel true guard
2205 (* --------------------------------------------------------------------- *)
2206 (* cleanup: convert AX to EX for pdots.
2207 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2208 This is what we wanted in the first place, but it wasn't possible to make
2209 because the AX and its argument are not created in the same place.
2211 (* also cleanup XX, which is a marker for the case where the programmer
2212 specifies to change the quantifier on .... Assumed to only occur after one AX
2213 or EX, or at top level. *)
2216 let c = match c with CTL.XX(c) -> c | _ -> c in
2218 CTL.False -> CTL.False
2219 | CTL.True -> CTL.True
2220 | CTL.Pred(p) -> CTL.Pred(p)
2221 | CTL.Not(phi) -> CTL.Not(cleanup phi)
2222 | CTL.Exists(keep,v,phi) -> CTL.Exists(keep,v,cleanup phi)
2223 | CTL.AndAny(dir,s,phi1,phi2) ->
2224 CTL.AndAny(dir,s,cleanup phi1,cleanup phi2)
2225 | CTL.HackForStmt(dir,s,phi1,phi2) ->
2226 CTL.HackForStmt(dir,s,cleanup phi1,cleanup phi2)
2227 | CTL.And(s,phi1,phi2) -> CTL.And(s,cleanup phi1,cleanup phi2)
2228 | CTL.Or(phi1,phi2) -> CTL.Or(cleanup phi1,cleanup phi2)
2229 | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(cleanup phi1,cleanup phi2)
2230 | CTL.Implies(phi1,phi2) -> CTL.Implies(cleanup phi1,cleanup phi2)
2231 | CTL.AF(dir,s,phi1) -> CTL.AF(dir,s,cleanup phi1)
2232 | CTL.AX(CTL.FORWARD,s,
2234 CTL.And(CTL.NONSTRICT,CTL.AU(CTL.FORWARD,s2,e2,e3),
2235 CTL.EU(CTL.FORWARD,e4,e5)))) ->
2237 CTL.And(CTL.NONSTRICT,
2238 CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)),
2239 CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5))))
2240 | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,cleanup phi)
2241 | CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) ->
2242 CTL.AX(dir,s,cleanup phi)
2243 | CTL.XX(phi) -> failwith "bad XX"
2244 | CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1)
2245 | CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1)
2246 | CTL.EF(dir,phi1) -> CTL.EF(dir,cleanup phi1)
2247 | CTL.EX(dir,phi1) -> CTL.EX(dir,cleanup phi1)
2248 | CTL.EG(dir,phi1) -> CTL.EG(dir,cleanup phi1)
2249 | CTL.AW(dir,s,phi1,phi2) -> CTL.AW(dir,s,cleanup phi1,cleanup phi2)
2250 | CTL.AU(dir,s,phi1,phi2) -> CTL.AU(dir,s,cleanup phi1,cleanup phi2)
2251 | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,cleanup phi1,cleanup phi2)
2252 | CTL.Let (x,phi1,phi2) -> CTL.Let (x,cleanup phi1,cleanup phi2)
2253 | CTL.LetR (dir,x,phi1,phi2) -> CTL.LetR (dir,x,cleanup phi1,cleanup phi2)
2254 | CTL.Ref(s) -> CTL.Ref(s)
2255 | CTL.Uncheck(phi1) -> CTL.Uncheck(cleanup phi1)
2256 | CTL.InnerAnd(phi1) -> CTL.InnerAnd(cleanup phi1)
2258 (* --------------------------------------------------------------------- *)
2259 (* Function declaration *)
2261 let top_level name (ua,pos) t =
2262 let ua = List.filter (function (nm,_) -> nm = name) ua in
2264 saved := Ast.get_saved t;
2265 let quantified = Common.minus_set ua pos in
2266 quantify false quantified
2267 (match Ast.unwrap t with
2268 Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
2270 let unopt = elim_opt.V.rebuilder_statement stmt in
2271 let unopt = preprocess_dots_e unopt in
2272 cleanup(statement unopt VeryEnd quantified [] None None None false)
2273 | Ast.CODE(stmt_dots) ->
2274 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
2275 let unopt = preprocess_dots unopt in
2276 let starts_with_dots =
2277 match Ast.undots stmt_dots with
2279 (match Ast.unwrap d with
2280 Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_)
2281 | Ast.Stars(_,_,_,_) -> true
2284 let starts_with_brace =
2285 match Ast.undots stmt_dots with
2287 (match Ast.unwrap d with
2292 statement_list unopt VeryEnd quantified [] None None None
2295 (if starts_with_dots
2297 (* EX because there is a loop on enter/top *)
2298 ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res)
2299 else if starts_with_brace
2301 ctl_and CTL.NONSTRICT
2302 (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res
2304 | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords")
2306 (* --------------------------------------------------------------------- *)
2309 let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
2312 (match exists_flag with
2313 Ast.Exists -> exists := Exists
2314 | Ast.Forall -> exists := Forall
2315 | Ast.ReverseForall -> exists := ReverseForall
2316 | Ast.Undetermined ->
2317 exists := if !Flag.sgrep_mode2 then Exists else Forall);
2319 let (l,used_after) =
2323 match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
2324 (List.combine l (List.combine used_after positions))) in
2325 let res = List.map2 (top_level name) used_after l in
2329 let asttoctl r used_after positions =
2331 Ast.ScriptRule _ -> []
2332 | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) ->
2333 asttoctlz (a,b,c) used_after positions
2334 | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CTL.True]
2336 let pp_cocci_predicate (pred,modif) =
2337 Pretty_print_engine.pp_predicate pred
2339 let cocci_predicate_to_string (pred,modif) =
2340 Pretty_print_engine.predicate_to_string pred