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,_) =
438 Ast.MINUS(_,_) -> true
439 | Ast.PLUS -> failwith "not possible"
440 | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
441 let do_nothing r k e = k e in
442 let rule_elem r k re =
444 match Ast.unwrap re with
445 Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
446 bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
447 | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
450 V.combiner bind option_default
451 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
453 do_nothing do_nothing do_nothing do_nothing
454 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
455 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
456 recursor.V.combiner_rule_elem
458 (* code is not a DisjRuleElem *)
459 let make_match label guard code =
460 let v = fresh_var() in
461 let matcher = Lib_engine.Match(code) in
462 if contains_modif code && not guard
463 then CTL.Exists(true,v,predmaker guard (matcher,CTL.Modif v) label)
465 let iso_info = !Flag.track_iso_usage && not (Ast.get_isos code = []) in
466 (match (iso_info,!onlyModif,guard,
467 intersect !used_after (Ast.get_fvs code)) with
468 (false,true,_,[]) | (_,_,true,_) ->
469 predmaker guard (matcher,CTL.Control) label
470 | _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))
472 let make_raw_match label guard code =
473 predmaker guard (Lib_engine.Match(code),CTL.Control) label
475 let rec seq_fvs quantified = function
478 let t1fvs = get_unquantified quantified fv1 in
480 List.fold_left Common.union_set []
481 (List.map (get_unquantified quantified) fvs) in
482 let bothfvs = Common.inter_set t1fvs termfvs in
483 let t1onlyfvs = Common.minus_set t1fvs bothfvs in
484 let new_quantified = Common.union_set bothfvs quantified in
485 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs)
490 function code -> CTL.Exists (not guard && List.mem cur !saved,cur,code))
492 let non_saved_quantify =
494 (function cur -> function code -> CTL.Exists (false,cur,code))
496 let intersectll lst nested_list =
497 List.filter (function x -> List.exists (List.mem x) nested_list) lst
499 (* --------------------------------------------------------------------- *)
500 (* Count depth of braces. The translation of a closed brace appears deeply
501 nested within the translation of the sequence term, so the name of the
502 paren var has to take into account the names of the nested braces. On the
503 other hand the close brace does not escape, so we don't have to take into
504 account other paren variable names. *)
506 (* called repetitively, which is inefficient, but less trouble than adding a
507 new field to Seq and FunDecl *)
508 let count_nested_braces s =
509 let bind x y = max x y in
510 let option_default = 0 in
511 let stmt_count r k s =
512 match Ast.unwrap s with
513 Ast.Seq(_,_,_,_) | Ast.FunDecl(_,_,_,_,_) -> (k s) + 1
515 let donothing r k e = k e in
517 let recursor = V.combiner bind option_default
518 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
520 donothing donothing donothing donothing
521 donothing donothing donothing donothing donothing donothing
522 donothing donothing stmt_count donothing donothing donothing in
523 let res = string_of_int (recursor.V.combiner_statement s) in
527 let get_label_ctr _ =
528 let cur = !labelctr in
530 string2var (Printf.sprintf "l%d" cur)
532 (* --------------------------------------------------------------------- *)
533 (* annotate dots with before and after neighbors *)
535 let print_bef_aft = function
537 Printf.printf "bef/aft\n";
538 Pretty_print_cocci.rule_elem "" re;
539 Format.print_newline()
541 Printf.printf "bef/aft\n";
542 Pretty_print_cocci.statement "" s;
543 Format.print_newline()
544 | Ast.Other_dots d ->
545 Printf.printf "bef/aft\n";
546 Pretty_print_cocci.statement_dots d;
547 Format.print_newline()
549 (* [] can only occur if we are in a disj, where it comes from a ? In that
550 case, we want to use a, which accumulates all of the previous patterns in
552 let rec get_before_elem sl a =
553 match Ast.unwrap sl with
557 [] -> ([],Common.Right a)
559 let (e,ea) = get_before_e e a in
562 let (e,ea) = get_before_e e a in
563 let (sl,sla) = loop sl ea in
565 let (l,a) = loop x a in
566 (Ast.rewrap sl (Ast.DOTS(l)),a)
567 | Ast.CIRCLES(x) -> failwith "not supported"
568 | Ast.STARS(x) -> failwith "not supported"
570 and get_before sl a =
571 match get_before_elem sl a with
572 (term,Common.Left x) -> (term,x)
573 | (term,Common.Right x) -> (term,x)
575 and get_before_whencode wc =
578 Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w
579 | Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w
580 | Ast.WhenModifier(x) -> Ast.WhenModifier(x))
583 and get_before_e s a =
584 match Ast.unwrap s with
585 Ast.Dots(d,w,_,aft) ->
586 (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)
587 | Ast.Nest(stmt_dots,w,multi,_,aft) ->
588 let w = get_before_whencode w in
589 let (sd,_) = get_before stmt_dots a in
595 Unify_ast.unify_statement_dots
596 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
598 Unify_ast.MAYBE -> false
600 | Ast.Other_dots a ->
601 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
603 Unify_ast.MAYBE -> false
607 (Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
608 | Ast.Disj(stmt_dots_list) ->
610 List.split (List.map (function e -> get_before e a) stmt_dots_list) in
611 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
613 (match Ast.unwrap ast with
614 Ast.MetaStmt(_,_,_,_) -> (s,[])
615 | _ -> (s,[Ast.Other s]))
616 | Ast.Seq(lbrace,decls,body,rbrace) ->
617 let index = count_nested_braces s in
618 let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
619 let (bd,_) = get_before body dea in
620 (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
621 [Ast.WParen(rbrace,index)])
622 | Ast.Define(header,body) ->
623 let (body,_) = get_before body [] in
624 (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
625 | Ast.IfThen(ifheader,branch,aft) ->
626 let (br,_) = get_before_e branch [] in
627 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s])
628 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
629 let (br1,_) = get_before_e branch1 [] in
630 let (br2,_) = get_before_e branch2 [] in
631 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
632 | Ast.While(header,body,aft) ->
633 let (bd,_) = get_before_e body [] in
634 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
635 | Ast.For(header,body,aft) ->
636 let (bd,_) = get_before_e body [] in
637 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
638 | Ast.Do(header,body,tail) ->
639 let (bd,_) = get_before_e body [] in
640 (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
641 | Ast.Iterator(header,body,aft) ->
642 let (bd,_) = get_before_e body [] in
643 (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
644 | Ast.Switch(header,lb,cases,rb) ->
647 (function case_line ->
648 match Ast.unwrap case_line with
649 Ast.CaseLine(header,body) ->
650 let (body,_) = get_before body [] in
651 Ast.rewrap case_line (Ast.CaseLine(header,body))
652 | Ast.OptCase(case_line) -> failwith "not supported")
654 (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
655 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
656 let (de,dea) = get_before decls [] in
657 let (bd,_) = get_before body dea in
658 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
659 | _ -> failwith "get_before_e: not supported"
661 let rec get_after sl a =
662 match Ast.unwrap sl with
668 let (sl,sla) = loop sl in
669 let (e,ea) = get_after_e e sla in
671 let (l,a) = loop x in
672 (Ast.rewrap sl (Ast.DOTS(l)),a)
673 | Ast.CIRCLES(x) -> failwith "not supported"
674 | Ast.STARS(x) -> failwith "not supported"
676 and get_after_whencode a wc =
679 Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w
680 | Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w
681 | Ast.WhenModifier(x) -> Ast.WhenModifier(x))
684 and get_after_e s a =
685 match Ast.unwrap s with
686 Ast.Dots(d,w,bef,_) ->
687 (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)
688 | Ast.Nest(stmt_dots,w,multi,bef,_) ->
689 let w = get_after_whencode a w in
690 let (sd,_) = get_after stmt_dots a in
696 Unify_ast.unify_statement_dots
697 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
699 Unify_ast.MAYBE -> false
701 | Ast.Other_dots a ->
702 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
704 Unify_ast.MAYBE -> false
708 (Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
709 | Ast.Disj(stmt_dots_list) ->
711 List.split (List.map (function e -> get_after e a) stmt_dots_list) in
712 (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
714 (match Ast.unwrap ast with
715 Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots _,i) ->
716 (* check "after" information for metavar optimization *)
717 (* if the error is not desired, could just return [], then
718 the optimization (check for EF) won't take place *)
722 (match Ast.unwrap x with
723 Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
725 "dots/nest not allowed before and after stmt metavar"
727 | Ast.Other_dots x ->
728 (match Ast.undots x with
730 (match Ast.unwrap x with
731 Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
733 ("dots/nest not allowed before and after stmt "^
742 (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
743 | Ast.MetaStmt(_,_,_,_) -> (s,[])
744 | _ -> (s,[Ast.Other s]))
745 | Ast.Seq(lbrace,decls,body,rbrace) ->
746 let index = count_nested_braces s in
747 let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
748 let (de,_) = get_after decls bda in
749 (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
750 [Ast.WParen(lbrace,index)])
751 | Ast.Define(header,body) ->
752 let (body,_) = get_after body a in
753 (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
754 | Ast.IfThen(ifheader,branch,aft) ->
755 let (br,_) = get_after_e branch a in
756 (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s])
757 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
758 let (br1,_) = get_after_e branch1 a in
759 let (br2,_) = get_after_e branch2 a in
760 (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
761 | Ast.While(header,body,aft) ->
762 let (bd,_) = get_after_e body a in
763 (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
764 | Ast.For(header,body,aft) ->
765 let (bd,_) = get_after_e body a in
766 (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
767 | Ast.Do(header,body,tail) ->
768 let (bd,_) = get_after_e body a in
769 (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])
770 | Ast.Iterator(header,body,aft) ->
771 let (bd,_) = get_after_e body a in
772 (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
773 | Ast.Switch(header,lb,cases,rb) ->
776 (function case_line ->
777 match Ast.unwrap case_line with
778 Ast.CaseLine(header,body) ->
779 let (body,_) = get_after body [] in
780 Ast.rewrap case_line (Ast.CaseLine(header,body))
781 | Ast.OptCase(case_line) -> failwith "not supported")
783 (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
784 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
785 let (bd,bda) = get_after body [] in
786 let (de,_) = get_after decls bda in
787 (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
788 | _ -> failwith "get_after_e: not supported"
790 let preprocess_dots sl =
791 let (sl,_) = get_before sl [] in
792 let (sl,_) = get_after sl [] in
795 let preprocess_dots_e sl =
796 let (sl,_) = get_before_e sl [] in
797 let (sl,_) = get_after_e sl [] in
800 (* --------------------------------------------------------------------- *)
801 (* various return_related things *)
803 let rec ends_in_return stmt_list =
804 match Ast.unwrap stmt_list with
806 (match List.rev x with
808 (match Ast.unwrap x with
810 (match Ast.unwrap x with
811 Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true
813 | Ast.Disj(disjs) -> List.for_all ends_in_return disjs
816 | Ast.CIRCLES(x) -> failwith "not supported"
817 | Ast.STARS(x) -> failwith "not supported"
819 (* --------------------------------------------------------------------- *)
822 let exptymatch l make_match make_guard_match =
823 let pos = fresh_pos() in
824 let matches_guard_matches =
827 let pos = Ast.make_mcode pos in
828 (make_match (Ast.set_pos x (Some pos)),
829 make_guard_match (Ast.set_pos x (Some pos))))
831 let (matches,guard_matches) = List.split matches_guard_matches in
832 let rec suffixes = function
834 | x::xs -> xs::(suffixes xs) in
835 let prefixes = List.rev (suffixes (List.rev guard_matches)) in
836 let info = (* not null *)
842 ctl_and CTL.NONSTRICT matcher
844 (ctl_uncheck (List.fold_left ctl_or_fl CTL.False negates)))))
846 CTL.InnerAnd(List.fold_left ctl_or_fl CTL.False (List.rev info))
848 (* code might be a DisjRuleElem, in which case we break it apart
849 code might contain an Exp or Ty
850 this one pushes the quantifier inwards *)
851 let do_re_matches label guard res quantified minus_quantified =
852 let make_guard_match x =
853 let stmt_fvs = Ast.get_mfvs x in
854 let fvs = get_unquantified minus_quantified stmt_fvs in
855 non_saved_quantify fvs (make_match None true x) in
857 let stmt_fvs = Ast.get_fvs x in
858 let fvs = get_unquantified quantified stmt_fvs in
859 quantify guard fvs (make_match None guard x) in
860 ctl_and CTL.NONSTRICT (label_pred_maker label)
861 (match List.map Ast.unwrap res with
862 [] -> failwith "unexpected empty disj"
863 | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match
864 | Ast.Ty(t)::rest -> exptymatch res make_match make_guard_match
866 if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
868 then failwith "unexpected exp or ty";
869 List.fold_left ctl_seqor CTL.False
870 (List.rev (List.map make_match res)))
872 (* code might be a DisjRuleElem, in which case we break it apart
873 code doesn't contain an Exp or Ty
874 this one is for use when it is not practical to push the quantifier inwards
876 let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl =
877 match Ast.unwrap code with
878 Ast.DisjRuleElem(res) ->
879 let make_match = make_match None guard in
880 let orop = if guard then ctl_or else ctl_seqor in
881 ctl_and CTL.NONSTRICT (label_pred_maker label)
882 (List.fold_left orop CTL.False (List.map make_match res))
883 | _ -> make_match label guard code
885 (* --------------------------------------------------------------------- *)
886 (* control structures *)
888 let end_control_structure fvs header body after_pred
889 after_checks no_after_checks (afvs,afresh,ainh,aft) after label guard =
890 (* aft indicates what is added after the whole if, which has to be added
892 let (aft_needed,after_branch) =
894 Ast.CONTEXT(_,Ast.NOTHING) ->
895 (false,make_seq_after2 guard after_pred after)
898 make_match label guard
899 (make_meta_rule_elem aft (afvs,afresh,ainh)) in
901 make_seq_after guard after_pred
902 (After(make_seq_after guard match_endif after))) in
903 let body = body after_branch in
904 let s = guard_to_strict guard in
909 (match (after,aft_needed) with
910 (After _,_) (* pattern doesn't end here *)
911 | (_,true) (* + code added after *) -> after_checks
912 | _ -> no_after_checks)
913 (ctl_ax_absolute s body)))
915 let ifthen ifheader branch ((afvs,_,_,_) as aft) after
916 quantified minus_quantified label llabel slabel recurse make_match guard =
917 (* "if (test) thn" becomes:
918 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
920 "if (test) thn; after" becomes:
921 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
926 match seq_fvs quantified
927 [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with
928 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
929 | _ -> failwith "not possible" in
930 let new_quantified = Common.union_set bfvs quantified in
932 match seq_fvs minus_quantified
933 [Ast.get_mfvs ifheader;Ast.get_mfvs branch;[]] with
934 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
935 | _ -> failwith "not possible" in
936 let new_mquantified = Common.union_set mbfvs minus_quantified in
938 let if_header = quantify guard efvs (make_match ifheader) in
939 (* then branch and after *)
940 let lv = get_label_ctr() in
941 let used = ref false in
944 [truepred label; recurse branch Tail new_quantified new_mquantified
945 (Some (lv,used)) llabel slabel guard] in
946 let after_pred = aftpred label in
947 let or_cases after_branch =
948 ctl_or true_branch (ctl_or (fallpred label) after_branch) in
949 let (if_header,wrapper) =
952 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
953 (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
954 (function body -> quantify true [lv] body))
955 else (if_header,function x -> x) in
957 (end_control_structure bfvs if_header or_cases after_pred
958 (Some(ctl_ex after_pred)) None aft after label guard)
960 let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
961 quantified minus_quantified label llabel slabel recurse make_match guard =
962 (* "if (test) thn else els" becomes:
963 if(test) & AX((TrueBranch & AX thn) v
964 (FalseBranch & AX (else & AX els)) v After)
967 "if (test) thn else els; after" becomes:
968 if(test) & AX((TrueBranch & AX thn) v
969 (FalseBranch & AX (else & AX els)) v
970 (After & AXAX after))
975 let (e1fvs,b1fvs,s1fvs) =
976 match seq_fvs quantified
977 [Ast.get_fvs ifheader;Ast.get_fvs branch1;afvs] with
978 [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
979 (e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
980 | _ -> failwith "not possible" in
981 let (e2fvs,b2fvs,s2fvs) =
983 match seq_fvs quantified
984 [Ast.get_fvs ifheader;Ast.get_fvs branch2;afvs] with
985 [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
986 (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
987 | _ -> failwith "not possible" in
988 let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
989 let exponlyfvs = intersect e1fvs e2fvs in
990 let new_quantified = union bothfvs quantified in
991 (* minus free variables *)
992 let (me1fvs,mb1fvs,ms1fvs) =
993 match seq_fvs minus_quantified
994 [Ast.get_mfvs ifheader;Ast.get_mfvs branch1;[]] with
995 [(e1fvs,b1fvs);(s1fvs,b1afvs);_] ->
996 (e1fvs,Common.union_set b1fvs b1afvs,s1fvs)
997 | _ -> failwith "not possible" in
998 let (me2fvs,mb2fvs,ms2fvs) =
1000 match seq_fvs minus_quantified
1001 [Ast.get_mfvs ifheader;Ast.get_mfvs branch2;[]] with
1002 [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1003 (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1004 | _ -> failwith "not possible" in
1005 let mbothfvs = union (union mb1fvs mb2fvs) (intersect ms1fvs ms2fvs) in
1006 let new_mquantified = union mbothfvs minus_quantified in
1008 let if_header = quantify guard exponlyfvs (make_match ifheader) in
1009 (* then and else branches *)
1010 let lv = get_label_ctr() in
1011 let used = ref false in
1014 [truepred label; recurse branch1 Tail new_quantified new_mquantified
1015 (Some (lv,used)) llabel slabel guard] in
1018 [falsepred label; make_match els;
1019 recurse branch2 Tail new_quantified new_mquantified
1020 (Some (lv,used)) llabel slabel guard] in
1021 let after_pred = aftpred label in
1022 let or_cases after_branch =
1023 ctl_or true_branch (ctl_or false_branch after_branch) in
1024 let s = guard_to_strict guard in
1025 let (if_header,wrapper) =
1028 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1029 (ctl_and CTL.NONSTRICT(*???*) if_header label_pred,
1030 (function body -> quantify true [lv] body))
1031 else (if_header,function x -> x) in
1033 (end_control_structure bothfvs if_header or_cases after_pred
1034 (Some(ctl_and s (ctl_ex (falsepred label)) (ctl_ex after_pred)))
1035 (Some(ctl_ex (falsepred label)))
1036 aft after label guard)
1038 let forwhile header body ((afvs,_,_,_) as aft) after
1039 quantified minus_quantified label recurse make_match guard =
1041 (* the translation in this case is similar to that of an if with no else *)
1042 (* free variables *)
1044 match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
1045 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
1046 | _ -> failwith "not possible" in
1047 let new_quantified = Common.union_set bfvs quantified in
1048 (* minus free variables *)
1050 match seq_fvs minus_quantified
1051 [Ast.get_mfvs header;Ast.get_mfvs body;[]] with
1052 [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
1053 | _ -> failwith "not possible" in
1054 let new_mquantified = Common.union_set mbfvs minus_quantified in
1056 let header = quantify guard efvs (make_match header) in
1057 let lv = get_label_ctr() in
1058 let used = ref false in
1062 recurse body Tail new_quantified new_mquantified
1063 (Some (lv,used)) (Some (lv,used)) None guard] in
1064 let after_pred = fallpred label in
1065 let or_cases after_branch = ctl_or body after_branch in
1066 let (header,wrapper) =
1069 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1070 (ctl_and CTL.NONSTRICT(*???*) header label_pred,
1071 (function body -> quantify true [lv] body))
1072 else (header,function x -> x) in
1074 (end_control_structure bfvs header or_cases after_pred
1075 (Some(ctl_ex after_pred)) None aft after label guard) in
1076 match (Ast.unwrap body,aft) with
1077 (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
1078 (match Ast.unwrap re with
1079 Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),
1080 Type_cocci.Unitary,_,false) ->
1082 match seq_fvs quantified [Ast.get_fvs header] with
1084 | _ -> failwith "not possible" in
1085 quantify guard efvs (make_match header)
1089 (* --------------------------------------------------------------------- *)
1090 (* statement metavariables *)
1092 (* issue: an S metavariable that is not an if branch/loop body
1093 should not match an if branch/loop body, so check that the labels
1094 of the nodes before the first node matched by the S are different
1095 from the label of the first node matched by the S *)
1096 let sequencibility body label_pred process_bef_aft = function
1097 Ast.Sequencible | Ast.SequencibleAfterDots [] ->
1100 (ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
1101 | Ast.SequencibleAfterDots l ->
1102 (* S appears after some dots. l is the code that comes after the S.
1103 want to search for that first, because S can match anything, while
1104 the stuff after is probably more restricted *)
1105 let afts = List.map process_bef_aft l in
1106 let ors = foldl1 ctl_or afts in
1107 ctl_and CTL.NONSTRICT
1108 (ctl_ef (ctl_and CTL.NONSTRICT ors (ctl_back_ax label_pred)))
1111 ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x))
1112 | Ast.NotSequencible -> body (function x -> x)
1114 let svar_context_with_add_after stmt s label quantified d ast
1115 seqible after process_bef_aft guard fvinfo =
1116 let label_var = (*fresh_label_var*) string2var "_lab" in
1118 CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
1120 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1121 let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1122 let full_metamatch = matcher d in
1123 let first_metamatch =
1126 Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_)) ->
1127 Ast.CONTEXT(pos,Ast.BEFORE(bef))
1128 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1129 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1130 let middle_metamatch =
1133 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1134 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1135 let last_metamatch =
1138 Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft)) ->
1139 Ast.CONTEXT(pos,Ast.AFTER(aft))
1140 | Ast.CONTEXT(_,_) -> d
1141 | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
1144 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1145 let left_or = (* the whole statement is one node *)
1147 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1148 let right_or = (* the statement covers multiple nodes *)
1151 ctl_au CTL.NONSTRICT
1154 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1156 (ctl_not prelabel_pred) after])] in
1158 ctl_and CTL.NONSTRICT label_pred
1159 (f (ctl_and CTL.NONSTRICT
1160 (make_raw_match label false ast) (ctl_or left_or right_or))) in
1161 let stmt_fvs = Ast.get_fvs stmt in
1162 let fvs = get_unquantified quantified stmt_fvs in
1163 quantify guard (label_var::fvs)
1164 (sequencibility body label_pred process_bef_aft seqible)
1166 let svar_minus_or_no_add_after stmt s label quantified d ast
1167 seqible after process_bef_aft guard fvinfo =
1168 let label_var = (*fresh_label_var*) string2var "_lab" in
1170 CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
1172 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1173 let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1175 (* don't have to put anything before the beginning, so don't have to
1176 distinguish the first node. so don't have to bother about paths,
1177 just use the label. label ensures that found nodes match up with
1178 what they should because it is in the lhs of the andany. *)
1180 Ast.MINUS(pos,[]) -> true
1181 | Ast.CONTEXT(pos,Ast.NOTHING) -> true
1184 match (pure_d,after) with
1185 (true,Tail) | (true,End) | (true,VeryEnd) ->
1186 (* the label sharing makes it safe to use AndAny *)
1187 CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
1188 ctl_and CTL.NONSTRICT label_pred
1189 (make_raw_match label false ast),
1190 ctl_and CTL.NONSTRICT (matcher d) prelabel_pred)
1192 (* more safe but less efficient *)
1193 let first_metamatch = matcher d in
1194 let rest_metamatch =
1197 Ast.MINUS(pos,_) -> Ast.MINUS(pos,[])
1198 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1199 | Ast.PLUS -> failwith "not possible") in
1200 let rest_nodes = ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred in
1201 let last_node = and_after guard (ctl_not prelabel_pred) after in
1202 (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
1205 ctl_au CTL.NONSTRICT rest_nodes last_node])) in
1206 let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
1207 let stmt_fvs = Ast.get_fvs stmt in
1208 let fvs = get_unquantified quantified stmt_fvs in
1209 quantify guard (label_var::fvs)
1210 (sequencibility body label_pred process_bef_aft seqible)
1212 (* --------------------------------------------------------------------- *)
1213 (* dots and nests *)
1215 let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
1216 let matchgoto = gotopred None in
1218 make_match None false
1220 (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in
1222 make_match None false
1224 (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in
1229 then CTL.Or(aftpred label,exitpred label)
1233 let lv = get_label_ctr() in
1234 let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1235 let preflabelpred = label_pred_maker (Some (lv,ref true)) in
1236 ctl_or (aftpred label)
1237 (quantify false [lv]
1238 (ctl_and CTL.NONSTRICT
1239 (ctl_and CTL.NONSTRICT (truepred label) labelpred)
1240 (ctl_au CTL.NONSTRICT
1241 (ctl_and CTL.NONSTRICT (ctl_not v) preflabelpred)
1242 (ctl_and CTL.NONSTRICT preflabelpred
1243 (ctl_or (retpred None)
1244 (if !Flag_engine.only_return_is_error_exit
1247 (ctl_or matchcontinue
1248 (ctl_and CTL.NONSTRICT
1249 (ctl_or matchgoto matchbreak)
1250 (ctl_ag s (ctl_not seq_after)))))))))) in
1251 let v = get_let_ctr() in
1252 let op = if quantifier = !exists then ctl_au else ctl_anti_au in
1253 op s x (CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
1255 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1256 process_bef_aft statement_list statement guard wrapcode =
1257 let ctl_and_ns = ctl_and CTL.NONSTRICT in
1258 (* proces bef_aft *)
1260 List.fold_left ctl_or_fl CTL.False (List.map process_bef_aft l) in
1261 let bef_aft = (* to be negated *)
1265 (function Ast.WhenModifier(Ast.WhenAny) -> true | _ -> false)
1268 with Not_found -> shortest (Common.union_set bef aft) in
1271 (function Ast.WhenModifier(Ast.WhenStrict) -> true | _ -> false)
1273 let check_quantifier quant other =
1275 (function Ast.WhenModifier(x) -> x = quant | _ -> false)
1279 (function Ast.WhenModifier(x) -> x = other | _ -> false)
1281 then failwith "inconsistent annotation on dots"
1285 if check_quantifier Ast.WhenExists Ast.WhenForall
1288 if check_quantifier Ast.WhenExists Ast.WhenForall
1291 (* the following is used when we find a goto, etc and consider accepting
1292 without finding the rest of the pattern *)
1293 let aft = shortest aft in
1294 (* process whencode *)
1295 let labelled = label_pred_maker label in
1297 let (poswhen,negwhen) =
1299 (function (poswhen,negwhen) ->
1301 Ast.WhenNot whencodes ->
1302 (poswhen,ctl_or (statement_list whencodes) negwhen)
1303 | Ast.WhenAlways stm ->
1304 (ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen)
1305 | Ast.WhenModifier(_) -> (poswhen,negwhen))
1306 (CTL.True,bef_aft) (List.rev whencodes) in
1307 let poswhen = ctl_and_ns arg poswhen in
1311 (* add in After, because it's not part of the program *)
1312 ctl_or (aftpred label) negwhen
1314 ctl_and_ns poswhen (ctl_not negwhen) in
1315 (* process dot code, if any *)
1317 match (dotcode,guard) with
1318 (None,_) | (_,true) -> CTL.True
1319 | (Some dotcode,_) -> dotcode in
1320 (* process nest code, if any *)
1321 (* whencode goes in the negated part of the nest; if no nest, just goes
1322 on the "true" in between code *)
1323 let plus_var = if plus then get_label_ctr() else string2var "" in
1324 let plus_var2 = if plus then get_label_ctr() else string2var "" in
1326 match (nest,guard && not plus) with
1327 (None,_) | (_,true) -> whencodes CTL.True
1328 | (Some nest,false) ->
1329 let v = get_let_ctr() in
1333 (* the idea is that BindGood is sort of a witness; a witness to
1334 having found the subterm in at least one place. If there is
1335 not a witness, then there is a risk that it will get thrown
1336 away, if it is merged with a node that has an empty
1337 environment. See tests/nestplus. But this all seems
1338 rather suspicious *)
1339 CTL.And(CTL.NONSTRICT,x,
1340 CTL.Exists(true,plus_var2,
1341 CTL.Pred(Lib_engine.BindGood(plus_var),
1342 CTL.Modif plus_var2)))
1345 CTL.Or(is_plus (CTL.Ref v),
1346 whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
1347 let plus_modifier x =
1354 CTL.Not(CTL.Pred(Lib_engine.BindBad(plus_var),CTL.Control)))))
1360 | Guard f -> ctl_uncheck f
1362 let exit = endpred label in
1363 let errorexit = exitpred label in
1364 ctl_or exit errorexit
1365 (* not at all sure what the next two mean... *)
1369 Some (lv,used) -> used := true;
1370 ctl_or (CTL.Pred(Lib_engine.Label lv,CTL.Control))
1371 (ctl_back_ex (ctl_or (retpred label) (gotopred label)))
1372 | None -> endpred label)
1373 (* was the following, but not clear why sgrep should allow
1375 let exit = endpred label in
1376 let errorexit = exitpred label in
1378 then ctl_or exit errorexit (* end anywhere *)
1379 else exit (* end at the real end of the function *) *) in
1381 (dots_au is_strict ((after = Tail) or (after = VeryEnd))
1382 label (guard_to_strict guard) wrapcode
1383 (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
1384 aft ender quantifier)
1386 (* --------------------------------------------------------------------- *)
1387 (* the main translation loop *)
1389 let rec statement_list stmt_list after quantified minus_quantified
1390 label llabel slabel dots_before guard =
1392 (* include Disj to be on the safe side *)
1393 match Ast.unwrap x with
1394 Ast.Dots _ | Ast.Nest _ | Ast.Disj _ -> true | _ -> false in
1395 let compute_label l e db = if db or isdots e then l else None in
1396 match Ast.unwrap stmt_list with
1398 let rec loop quantified minus_quantified dots_before label llabel slabel
1400 ([],_,_) -> (match after with After f -> f | _ -> CTL.True)
1402 statement e after quantified minus_quantified
1403 (compute_label label e dots_before)
1405 | (e::sl,fv::fvs,mfv::mfvs) ->
1406 let shared = intersectll fv fvs in
1407 let unqshared = get_unquantified quantified shared in
1408 let new_quantified = Common.union_set unqshared quantified in
1409 let minus_shared = intersectll mfv mfvs in
1411 get_unquantified minus_quantified minus_shared in
1412 let new_mquantified =
1413 Common.union_set munqshared minus_quantified in
1414 quantify guard unqshared
1417 (let (label1,llabel1,slabel1) =
1418 match Ast.unwrap e with
1420 (match Ast.unwrap re with
1421 Ast.Goto _ -> (None,None,None)
1422 | _ -> (label,llabel,slabel))
1423 | _ -> (label,llabel,slabel) in
1424 loop new_quantified new_mquantified (isdots e)
1425 label1 llabel1 slabel1
1427 new_quantified new_mquantified
1428 (compute_label label e dots_before) llabel slabel guard)
1429 | _ -> failwith "not possible" in
1430 loop quantified minus_quantified dots_before
1432 (x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x)
1433 | Ast.CIRCLES(x) -> failwith "not supported"
1434 | Ast.STARS(x) -> failwith "not supported"
1436 (* llabel is the label of the enclosing loop and slabel is the label of the
1438 and statement stmt after quantified minus_quantified
1439 label llabel slabel guard =
1440 let ctl_au = ctl_au CTL.NONSTRICT in
1441 let ctl_ax = ctl_ax CTL.NONSTRICT in
1442 let ctl_and = ctl_and CTL.NONSTRICT in
1443 let make_seq = make_seq guard in
1444 let make_seq_after = make_seq_after guard in
1445 let real_make_match = make_match in
1446 let make_match = header_match label guard in
1448 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1451 match Ast.unwrap stmt with
1453 (match Ast.unwrap ast with
1454 (* the following optimisation is not a good idea, because when S
1455 is alone, we would like it not to match a declaration.
1456 this makes more matching for things like when (...) S, but perhaps
1457 that matching is not so costly anyway *)
1458 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1459 | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_)) as d),_),
1461 | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_)) as d),_),
1463 svar_context_with_add_after stmt s label quantified d ast seqible
1465 (process_bef_aft quantified minus_quantified
1466 label llabel slabel true)
1468 (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)
1470 | Ast.MetaStmt((s,_,d,_),keep,seqible,_) ->
1471 svar_minus_or_no_add_after stmt s label quantified d ast seqible
1473 (process_bef_aft quantified minus_quantified
1474 label llabel slabel true)
1476 (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt)
1480 match Ast.unwrap ast with
1481 Ast.DisjRuleElem(res) ->
1482 do_re_matches label guard res quantified minus_quantified
1483 | Ast.Exp(_) | Ast.Ty(_) ->
1484 let stmt_fvs = Ast.get_fvs stmt in
1485 let fvs = get_unquantified quantified stmt_fvs in
1486 CTL.InnerAnd(quantify guard fvs (make_match ast))
1488 let stmt_fvs = Ast.get_fvs stmt in
1489 let fvs = get_unquantified quantified stmt_fvs in
1490 quantify guard fvs (make_match ast) in
1491 match Ast.unwrap ast with
1492 Ast.Break(brk,semi) ->
1493 (match (llabel,slabel) with
1494 (_,Some(lv,used)) -> (* use switch label if there is one *)
1495 ctl_and term (bclabel_pred_maker slabel)
1496 | _ -> ctl_and term (bclabel_pred_maker llabel))
1497 | Ast.Continue(brk,semi) -> ctl_and term (bclabel_pred_maker llabel)
1498 | Ast.Return((_,info,retmc,pos),(_,_,semmc,_)) ->
1499 (* discard pattern that comes after return *)
1500 let normal_res = make_seq_after term after in
1501 (* the following code tries to propagate the modifications on
1502 return; to a close brace, in the case where the final return
1505 match (retmc,semmc) with
1506 (Ast.MINUS(_,l1),Ast.MINUS(_,l2)) when !Flag.sgrep_mode2 ->
1507 (* in sgrep mode, we can propagate the - *)
1508 Some (Ast.MINUS(Ast.NoPos,l1@l2))
1509 | (Ast.MINUS(_,l1),Ast.MINUS(_,l2))
1510 | (Ast.CONTEXT(_,Ast.BEFORE(l1)),
1511 Ast.CONTEXT(_,Ast.AFTER(l2))) ->
1512 Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2)))
1513 | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
1514 | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
1516 | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.AFTER(l))) ->
1517 Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l)))
1519 let ret = Ast.make_mcode "return" in
1521 Ast.rewrap ast (Ast.Edots(Ast.make_mcode "...",None)) in
1522 let semi = Ast.make_mcode ";" in
1524 make_match(Ast.rewrap ast (Ast.Return(ret,semi))) in
1526 make_match(Ast.rewrap ast (Ast.ReturnExpr(ret,edots,semi))) in
1529 let exit = endpred None in
1531 Ast.rewrap ast (Ast.SeqEnd (("}",info,new_mc,pos))) in
1532 let stripped_rbrace =
1533 Ast.rewrap ast (Ast.SeqEnd(Ast.make_mcode "}")) in
1535 (ctl_and (make_match mod_rbrace)
1540 (ctl_or simple_return return_expr))))
1542 (make_match stripped_rbrace)
1543 (* error exit not possible; it is in the middle
1544 of code, so a return is needed *)
1547 (* some change in the middle of the return, so have to
1548 find an actual return *)
1551 (* should try to deal with the dots_bef_aft problem elsewhere,
1552 but don't have the courage... *)
1557 do_between_dots stmt term End
1558 quantified minus_quantified label llabel slabel guard in
1560 make_seq_after term after)
1561 | Ast.Seq(lbrace,decls,body,rbrace) ->
1562 let (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs) =
1565 [Ast.get_fvs lbrace;Ast.get_fvs decls;
1566 Ast.get_fvs body;Ast.get_fvs rbrace]
1568 [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
1569 (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
1570 | _ -> failwith "not possible" in
1571 let (mlbfvs,mb1fvs,mb2fvs,mb3fvs,mrbfvs) =
1573 seq_fvs minus_quantified
1574 [Ast.get_mfvs lbrace;Ast.get_mfvs decls;
1575 Ast.get_mfvs body;Ast.get_mfvs rbrace]
1577 [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
1578 (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
1579 | _ -> failwith "not possible" in
1580 let pv = count_nested_braces stmt in
1581 let lv = get_label_ctr() in
1582 let paren_pred = CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
1583 let label_pred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1586 (quantify guard lbfvs (make_match lbrace))
1587 (ctl_and paren_pred label_pred) in
1589 (* label is not needed; paren_pred is enough *)
1591 (quantify guard rbfvs (real_make_match None guard rbrace))
1593 let new_quantified2 =
1594 Common.union_set b1fvs (Common.union_set b2fvs quantified) in
1595 let new_quantified3 = Common.union_set b3fvs new_quantified2 in
1596 let new_mquantified2 =
1597 Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in
1598 let new_mquantified3 = Common.union_set mb3fvs new_mquantified2 in
1599 let pattern_as_given =
1600 let new_quantified2 = Common.union_set [pv] new_quantified2 in
1601 let new_quantified3 = Common.union_set [pv] new_quantified3 in
1602 quantify true [pv;lv]
1603 (quantify guard b1fvs
1606 quantify guard b2fvs
1607 (statement_list decls
1609 (quantify guard b3fvs
1610 (statement_list body
1611 (After (make_seq_after end_brace after))
1612 new_quantified3 new_mquantified3
1613 (Some (lv,ref true)) (* label mostly useful *)
1614 llabel slabel true guard)))
1615 new_quantified2 new_mquantified2
1616 (Some (lv,ref true)) llabel slabel false guard)])) in
1617 if ends_in_return body
1619 (* matching error handling code *)
1621 1. The pattern as given
1622 2. A goto, and then some close braces, and then the pattern as
1623 given, but without the braces (only possible if there are no
1624 decls, and open and close braces are unmodified)
1625 3. Part of the pattern as given, then a goto, and then the rest
1626 of the pattern. For this case, we just check that all paths have
1627 a goto within the current braces. checking for a goto at every
1628 point in the pattern seems expensive and not worthwhile. *)
1631 match Ast.unwrap rbrace with
1632 Ast.SeqEnd((data,info,_,pos)) ->
1633 Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data))
1634 | _ -> failwith "unexpected close brace" in
1635 let body = preprocess_dots body in (* redo, to drop braces *)
1639 (make_match empty_rbrace)
1640 (ctl_ax (* skip the destination label *)
1641 (quantify guard b3fvs
1642 (statement_list body End
1643 new_quantified3 new_mquantified3 None llabel slabel
1646 let new_quantified2 = Common.union_set [pv] new_quantified2 in
1647 let new_quantified3 = Common.union_set [pv] new_quantified3 in
1648 quantify true [pv;lv]
1649 (quantify guard b1fvs
1653 (CTL.AU (* want AF even for sgrep *)
1654 (CTL.FORWARD,CTL.STRICT,
1655 CTL.Pred(Lib_engine.PrefixLabel(lv),CTL.Control),
1656 ctl_and (* brace must be eventually after goto *)
1657 (gotopred (Some (lv,ref true)))
1658 (* want AF even for sgrep *)
1659 (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
1660 (quantify guard b2fvs
1661 (statement_list decls
1663 (quantify guard b3fvs
1664 (statement_list body Tail
1667 nopv_end_brace after)*)
1668 new_quantified3 new_mquantified3
1669 None llabel slabel true guard)))
1670 new_quantified2 new_mquantified2
1671 (Some (lv,ref true))
1672 llabel slabel false guard))])) in
1673 ctl_or pattern_as_given
1674 (match Ast.unwrap decls with
1675 Ast.DOTS([]) -> ctl_or pattern2 pattern3
1676 | Ast.DOTS(l) -> pattern3
1677 | _ -> failwith "circles and stars not supported")
1678 else pattern_as_given
1679 | Ast.IfThen(ifheader,branch,aft) ->
1680 ifthen ifheader branch aft after quantified minus_quantified
1681 label llabel slabel statement make_match guard
1683 | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
1684 ifthenelse ifheader branch1 els branch2 aft after quantified
1685 minus_quantified label llabel slabel statement make_match guard
1687 | Ast.While(header,body,aft) | Ast.For(header,body,aft)
1688 | Ast.Iterator(header,body,aft) ->
1689 forwhile header body aft after quantified minus_quantified
1690 label statement make_match guard
1692 | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
1694 (label_pred_maker label)
1695 (List.fold_left ctl_seqor CTL.False
1698 statement_list sl after quantified minus_quantified label
1699 llabel slabel true guard)
1702 | Ast.Nest(stmt_dots,whencode,multi,bef,aft) ->
1703 (* label in recursive call is None because label check is already
1704 wrapped around the corresponding code *)
1707 match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
1709 [(wcfvs,bothfvs);(bdfvs,_)] -> bothfvs
1710 | _ -> failwith "not possible" in
1712 (* no minus version because when code doesn't contain any minus code *)
1713 let new_quantified = Common.union_set bfvs quantified in
1717 statement_list stmt_dots (a2n after) new_quantified minus_quantified
1718 None llabel slabel true guard in
1719 dots_and_nests multi
1720 (Some dots_pattern) whencode bef aft None after label
1721 (process_bef_aft new_quantified minus_quantified
1722 None llabel slabel true)
1724 statement_list x Tail new_quantified minus_quantified None
1725 llabel slabel true true)
1727 statement x Tail new_quantified minus_quantified None
1729 guard (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
1731 | Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
1735 (* no need for the fresh metavar, but ... is a bit wierd as a
1737 Some(make_match (make_meta_rule_elem d ([],[],[])))
1739 dots_and_nests false None whencodes bef aft dot_code after label
1740 (process_bef_aft quantified minus_quantified None llabel slabel true)
1742 statement_list x Tail quantified minus_quantified
1743 None llabel slabel true true)
1745 statement x Tail quantified minus_quantified None llabel slabel true)
1746 guard (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
1748 | Ast.Switch(header,lb,cases,rb) ->
1749 let rec intersect_all = function
1752 | x::xs -> intersect x (intersect_all xs) in
1753 let rec union_all l = List.fold_left union [] l in
1754 (* start normal variables *)
1755 let header_fvs = Ast.get_fvs header in
1756 let lb_fvs = Ast.get_fvs lb in
1757 let case_fvs = List.map Ast.get_fvs cases in
1758 let rb_fvs = Ast.get_fvs rb in
1759 let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1760 all_casefvs,all_b3fvs,all_rbfvs) =
1762 (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1763 all_casefvs,all_b3fvs,all_rbfvs) ->
1764 function case_fvs ->
1765 match seq_fvs quantified [header_fvs;lb_fvs;case_fvs;rb_fvs] with
1766 [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
1767 (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
1768 b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
1770 | _ -> failwith "not possible")
1771 ([],[],[],[],[],[],[]) case_fvs in
1772 let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1773 all_casefvs,all_b3fvs,all_rbfvs) =
1774 (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,
1775 List.rev all_b2fvs,List.rev all_casefvs,List.rev all_b3fvs,
1776 List.rev all_rbfvs) in
1777 let exponlyfvs = intersect_all all_efvs in
1778 let lbonlyfvs = intersect_all all_lbfvs in
1779 (* don't do anything with right brace. Hope there is no + code on it *)
1780 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1781 let b1fvs = union_all all_b1fvs in
1782 let new1_quantified = union b1fvs quantified in
1783 let b2fvs = union (union_all all_b1fvs) (intersect_all all_casefvs) in
1784 let new2_quantified = union b2fvs new1_quantified in
1785 (* let b3fvs = union_all all_b3fvs in*)
1786 (* ------------------- start minus free variables *)
1787 let header_mfvs = Ast.get_mfvs header in
1788 let lb_mfvs = Ast.get_mfvs lb in
1789 let case_mfvs = List.map Ast.get_mfvs cases in
1790 let rb_mfvs = Ast.get_mfvs rb in
1791 let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
1792 all_mcasefvs,all_mb3fvs,all_mrbfvs) =
1794 (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
1795 all_casefvs,all_b3fvs,all_rbfvs) ->
1796 function case_mfvs ->
1799 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1800 [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] ->
1801 (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs,
1802 b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
1804 | _ -> failwith "not possible")
1805 ([],[],[],[],[],[],[]) case_mfvs in
1806 let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
1807 all_mcasefvs,all_mb3fvs,all_mrbfvs) =
1808 (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,
1809 List.rev all_mb2fvs,List.rev all_mcasefvs,List.rev all_mb3fvs,
1810 List.rev all_mrbfvs) in
1811 (* don't do anything with right brace. Hope there is no + code on it *)
1812 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1813 let mb1fvs = union_all all_mb1fvs in
1814 let new1_mquantified = union mb1fvs quantified in
1815 let mb2fvs = union (union_all all_mb1fvs) (intersect_all all_mcasefvs) in
1816 let new2_mquantified = union mb2fvs new1_mquantified in
1817 (* let b3fvs = union_all all_b3fvs in*)
1818 (* ------------------- end collection of free variables *)
1819 let switch_header = quantify guard exponlyfvs (make_match header) in
1820 let lb = quantify guard lbonlyfvs (make_match lb) in
1821 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
1824 (function case_line ->
1825 match Ast.unwrap case_line with
1826 Ast.CaseLine(header,body) ->
1828 match seq_fvs new2_quantified [Ast.get_fvs header] with
1829 [(e1fvs,_)] -> e1fvs
1830 | _ -> failwith "not possible" in
1831 quantify guard e1fvs (real_make_match label true header)
1832 | Ast.OptCase(case_line) -> failwith "not supported")
1835 ctl_not (List.fold_left ctl_or_fl CTL.False case_headers) in
1836 let lv = get_label_ctr() in
1837 let used = ref false in
1840 (function case_line ->
1841 match Ast.unwrap case_line with
1842 Ast.CaseLine(header,body) ->
1843 let (e1fvs,b1fvs,s1fvs) =
1844 let fvs = [Ast.get_fvs header;Ast.get_fvs body] in
1845 match seq_fvs new2_quantified fvs with
1846 [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
1847 | _ -> failwith "not possible" in
1848 let (me1fvs,mb1fvs,ms1fvs) =
1849 let fvs = [Ast.get_mfvs header;Ast.get_mfvs body] in
1850 match seq_fvs new2_mquantified fvs with
1851 [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs)
1852 | _ -> failwith "not possible" in
1854 quantify guard e1fvs (make_match header) in
1855 let new3_quantified = union b1fvs new2_quantified in
1856 let new3_mquantified = union mb1fvs new2_mquantified in
1858 statement_list body Tail
1859 new3_quantified new3_mquantified label llabel
1860 (Some (lv,used)) true(*?*) guard in
1861 quantify guard b1fvs (make_seq [case_header; body])
1862 | Ast.OptCase(case_line) -> failwith "not supported")
1864 let default_required =
1867 match Ast.unwrap case with
1868 Ast.CaseLine(header,_) ->
1869 (match Ast.unwrap header with
1870 Ast.Default(_,_) -> true
1874 then function x -> x
1875 else function x -> ctl_or (fallpred label) x in
1876 let after_pred = aftpred label in
1877 let body after_branch =
1880 (quantify guard b2fvs
1883 (List.fold_left ctl_and CTL.True
1884 (List.map ctl_ex case_headers));
1885 List.fold_left ctl_or_fl no_header case_code])))
1888 (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,
1889 match Ast.unwrap rb with
1890 Ast.SeqEnd(rb) -> Ast.get_mcodekind rb
1891 | _ -> failwith "not possible") in
1892 let (switch_header,wrapper) =
1895 let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in
1896 (ctl_and switch_header label_pred,
1897 (function body -> quantify true [lv] body))
1898 else (switch_header,function x -> x) in
1900 (end_control_structure b1fvs switch_header body
1901 after_pred (Some(ctl_ex after_pred)) None aft after label guard)
1902 | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
1903 let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs) =
1906 [Ast.get_fvs header;Ast.get_fvs lbrace;Ast.get_fvs decls;
1907 Ast.get_fvs body;Ast.get_fvs rbrace]
1909 [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
1910 (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
1911 | _ -> failwith "not possible" in
1912 let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mb4fvs,mrbfvs) =
1915 [Ast.get_mfvs header;Ast.get_mfvs lbrace;Ast.get_mfvs decls;
1916 Ast.get_mfvs body;Ast.get_mfvs rbrace]
1918 [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
1919 (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
1920 | _ -> failwith "not possible" in
1921 let function_header = quantify guard hfvs (make_match header) in
1922 let start_brace = quantify guard lbfvs (make_match lbrace) in
1923 let stripped_rbrace =
1924 match Ast.unwrap rbrace with
1925 Ast.SeqEnd((data,info,_,_)) ->
1926 Ast.rewrap rbrace(Ast.SeqEnd (Ast.make_mcode data))
1927 | _ -> failwith "unexpected close brace" in
1929 let exit = CTL.Pred (Lib_engine.Exit,CTL.Control) in
1930 let errorexit = CTL.Pred (Lib_engine.ErrorExit,CTL.Control) in
1931 let fake_brace = CTL.Pred (Lib_engine.FakeBrace,CTL.Control) in
1933 (quantify guard rbfvs (make_match rbrace))
1935 (* the following finds the beginning of the fake braces,
1936 if there are any, not completely sure how this works.
1937 sse the examples sw and return *)
1938 (ctl_back_ex (ctl_not fake_brace))
1939 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
1940 let new_quantified3 =
1941 Common.union_set b1fvs
1942 (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
1943 let new_quantified4 = Common.union_set b4fvs new_quantified3 in
1944 let new_mquantified3 =
1945 Common.union_set mb1fvs
1946 (Common.union_set mb2fvs
1947 (Common.union_set mb3fvs minus_quantified)) in
1948 let new_mquantified4 = Common.union_set mb4fvs new_mquantified3 in
1950 match (Ast.undots decls,Ast.undots body,contains_modif rbrace) with
1951 ([],[body],false) ->
1952 (match Ast.unwrap body with
1953 Ast.Nest(stmt_dots,[],multi,_,_) ->
1955 then None (* not sure how to optimize this case *)
1956 else Some (Common.Left stmt_dots)
1957 | Ast.Dots(_,whencode,_,_) -> Some (Common.Right whencode)
1962 Some (Common.Left stmt_dots) ->
1963 (* special case for function header + body - header is unambiguous
1964 and unique, so we can just look for the nested body anywhere
1967 (CTL.FORWARD,guard_to_strict guard,start_brace,
1968 statement_list stmt_dots
1969 (* discards match on right brace, but don't need it *)
1970 (Guard (make_seq_after end_brace after))
1971 new_quantified4 new_mquantified4
1972 None llabel slabel true guard)
1973 | Some (Common.Right whencode) ->
1974 (* try to be more efficient for the case where the body is just
1975 ... Perhaps this is too much of a special case, but useful
1976 for dropping a parameter and checking that it is never used. *)
1988 Ast.WhenAlways(s) -> prev
1989 | Ast.WhenNot(sl) ->
1991 statement_list sl Tail
1992 new_quantified4 new_mquantified4
1993 label llabel slabel true true in
1995 | Ast.WhenModifier(Ast.WhenAny) -> CTL.False
1996 | Ast.WhenModifier(_) -> prev)
1997 CTL.False whencode))
2001 Ast.WhenAlways(s) ->
2004 new_quantified4 new_mquantified4
2005 label llabel slabel true in
2007 | Ast.WhenNot(sl) -> prev
2008 | Ast.WhenModifier(Ast.WhenAny) -> CTL.True
2009 | Ast.WhenModifier(_) -> prev)
2010 CTL.True whencode) in
2011 ctl_au leftarg (make_match stripped_rbrace)]
2015 quantify guard b3fvs
2016 (statement_list decls
2018 (quantify guard b4fvs
2019 (statement_list body
2020 (After (make_seq_after end_brace after))
2021 new_quantified4 new_mquantified4
2022 None llabel slabel true guard)))
2023 new_quantified3 new_mquantified3 None llabel slabel
2025 quantify guard b1fvs
2026 (make_seq [function_header; quantify guard b2fvs body_code])
2027 | Ast.Define(header,body) ->
2028 let (hfvs,bfvs,bodyfvs) =
2029 match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body]
2031 [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
2032 | _ -> failwith "not possible" in
2033 let (mhfvs,mbfvs,mbodyfvs) =
2034 match seq_fvs minus_quantified [Ast.get_mfvs header;Ast.get_mfvs body]
2036 [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs)
2037 | _ -> failwith "not possible" in
2038 let define_header = quantify guard hfvs (make_match header) in
2040 statement_list body after
2041 (Common.union_set bfvs quantified)
2042 (Common.union_set mbfvs minus_quantified)
2043 None llabel slabel true guard in
2044 quantify guard bfvs (make_seq [define_header; body_code])
2045 | Ast.OptStm(stm) ->
2046 failwith "OptStm should have been compiled away\n"
2047 | Ast.UniqueStm(stm) -> failwith "arities not yet supported"
2048 | _ -> failwith "not supported" in
2049 if guard or !dots_done
2052 do_between_dots stmt term after quantified minus_quantified
2053 label llabel slabel guard
2055 (* term is the translation of stmt *)
2056 and do_between_dots stmt term after quantified minus_quantified
2057 label llabel slabel guard =
2058 match Ast.get_dots_bef_aft stmt with
2059 Ast.AddingBetweenDots (brace_term,n)
2060 | Ast.DroppingBetweenDots (brace_term,n) ->
2062 statement brace_term after quantified minus_quantified
2063 label llabel slabel guard in
2064 let v = Printf.sprintf "_r_%d" n in
2065 let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in
2066 let case2 = ctl_and CTL.NONSTRICT (ctl_not (CTL.Ref v)) term in
2069 (ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
2070 (ctl_back_ex (ctl_back_ex (falsepred label))),
2072 | Ast.NoDots -> term
2074 (* un_process_bef_aft is because we don't want to do transformation in this
2075 code, and thus don't case about braces before or after it *)
2076 and process_bef_aft quantified minus_quantified label llabel slabel guard =
2078 Ast.WParen (re,n) ->
2079 let paren_pred = CTL.Pred (Lib_engine.Paren n,CTL.Control) in
2080 let s = guard_to_strict guard in
2081 quantify true (get_unquantified quantified [n])
2082 (ctl_and s (make_raw_match None guard re) paren_pred)
2084 statement s Tail quantified minus_quantified label llabel slabel guard
2085 | Ast.Other_dots d ->
2086 statement_list d Tail quantified minus_quantified
2087 label llabel slabel true guard
2089 (* --------------------------------------------------------------------- *)
2090 (* cleanup: convert AX to EX for pdots.
2091 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2092 This is what we wanted in the first place, but it wasn't possible to make
2093 because the AX and its argument are not created in the same place.
2095 (* also cleanup XX, which is a marker for the case where the programmer
2096 specifies to change the quantifier on .... Assumed to only occur after one AX
2097 or EX, or at top level. *)
2100 let c = match c with CTL.XX(c) -> c | _ -> c in
2102 CTL.False -> CTL.False
2103 | CTL.True -> CTL.True
2104 | CTL.Pred(p) -> CTL.Pred(p)
2105 | CTL.Not(phi) -> CTL.Not(cleanup phi)
2106 | CTL.Exists(keep,v,phi) -> CTL.Exists(keep,v,cleanup phi)
2107 | CTL.AndAny(dir,s,phi1,phi2) ->
2108 CTL.AndAny(dir,s,cleanup phi1,cleanup phi2)
2109 | CTL.HackForStmt(dir,s,phi1,phi2) ->
2110 CTL.HackForStmt(dir,s,cleanup phi1,cleanup phi2)
2111 | CTL.And(s,phi1,phi2) -> CTL.And(s,cleanup phi1,cleanup phi2)
2112 | CTL.Or(phi1,phi2) -> CTL.Or(cleanup phi1,cleanup phi2)
2113 | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(cleanup phi1,cleanup phi2)
2114 | CTL.Implies(phi1,phi2) -> CTL.Implies(cleanup phi1,cleanup phi2)
2115 | CTL.AF(dir,s,phi1) -> CTL.AF(dir,s,cleanup phi1)
2116 | CTL.AX(CTL.FORWARD,s,
2118 CTL.And(CTL.NONSTRICT,CTL.AU(CTL.FORWARD,s2,e2,e3),
2119 CTL.EU(CTL.FORWARD,e4,e5)))) ->
2121 CTL.And(CTL.NONSTRICT,
2122 CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)),
2123 CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5))))
2124 | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,CTL.XX(cleanup phi))
2125 | CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) ->
2126 CTL.AX(dir,s,CTL.XX(cleanup phi))
2127 | CTL.XX(phi) -> failwith "bad XX"
2128 | CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1)
2129 | CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1)
2130 | CTL.EF(dir,phi1) -> CTL.EF(dir,cleanup phi1)
2131 | CTL.EX(dir,phi1) -> CTL.EX(dir,cleanup phi1)
2132 | CTL.EG(dir,phi1) -> CTL.EG(dir,cleanup phi1)
2133 | CTL.AW(dir,s,phi1,phi2) -> CTL.AW(dir,s,cleanup phi1,cleanup phi2)
2134 | CTL.AU(dir,s,phi1,phi2) -> CTL.AU(dir,s,cleanup phi1,cleanup phi2)
2135 | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,cleanup phi1,cleanup phi2)
2136 | CTL.Let (x,phi1,phi2) -> CTL.Let (x,cleanup phi1,cleanup phi2)
2137 | CTL.LetR (dir,x,phi1,phi2) -> CTL.LetR (dir,x,cleanup phi1,cleanup phi2)
2138 | CTL.Ref(s) -> CTL.Ref(s)
2139 | CTL.Uncheck(phi1) -> CTL.Uncheck(cleanup phi1)
2140 | CTL.InnerAnd(phi1) -> CTL.InnerAnd(cleanup phi1)
2142 (* --------------------------------------------------------------------- *)
2143 (* Function declaration *)
2145 let top_level name (ua,pos) t =
2146 let ua = List.filter (function (nm,_) -> nm = name) ua in
2148 saved := Ast.get_saved t;
2149 let quantified = Common.minus_set ua pos in
2150 quantify false quantified
2151 (match Ast.unwrap t with
2152 Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
2154 let unopt = elim_opt.V.rebuilder_statement stmt in
2155 let unopt = preprocess_dots_e unopt in
2156 cleanup(statement unopt VeryEnd quantified [] None None None false)
2157 | Ast.CODE(stmt_dots) ->
2158 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
2159 let unopt = preprocess_dots unopt in
2160 let starts_with_dots =
2161 match Ast.undots stmt_dots with
2163 (match Ast.unwrap d with
2164 Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_)
2165 | Ast.Stars(_,_,_,_) -> true
2168 let starts_with_brace =
2169 match Ast.undots stmt_dots with
2171 (match Ast.unwrap d with
2176 statement_list unopt VeryEnd quantified [] None None None
2179 (if starts_with_dots
2181 (* EX because there is a loop on enter/top *)
2182 ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res)
2183 else if starts_with_brace
2185 ctl_and CTL.NONSTRICT
2186 (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res
2188 | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords")
2190 (* --------------------------------------------------------------------- *)
2193 let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
2196 (match exists_flag with
2197 Ast.Exists -> exists := Exists
2198 | Ast.Forall -> exists := Forall
2199 | Ast.ReverseForall -> exists := ReverseForall
2200 | Ast.Undetermined ->
2201 exists := if !Flag.sgrep_mode2 then Exists else Forall);
2203 let (l,used_after) =
2207 match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
2208 (List.combine l (List.combine used_after positions))) in
2209 let res = List.map2 (top_level name) used_after l in
2213 let asttoctl r used_after positions =
2215 Ast.ScriptRule _ -> []
2216 | Ast.CocciRule (a,b,c,_) -> asttoctlz (a,b,c) used_after positions
2218 let pp_cocci_predicate (pred,modif) =
2219 Pretty_print_engine.pp_predicate pred
2221 let cocci_predicate_to_string (pred,modif) =
2222 Pretty_print_engine.predicate_to_string pred