2 * Copyright 2010, INRIA, University of Copenhagen
3 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
4 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
5 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
6 * This file is part of Coccinelle.
8 * Coccinelle is free software: you can redistribute it and/or modify
9 * it under the terms of the GNU General Public License as published by
10 * the Free Software Foundation, according to version 2 of the License.
12 * Coccinelle is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
25 (* for MINUS and CONTEXT, pos is always None in this file *)
26 (*search for require*)
27 (* true = don't see all matched nodes, only modified ones *)
28 let onlyModif = ref true(*false*)
30 type ex
= Exists
| Forall
31 let exists = ref Forall
33 module Ast
= Ast_cocci
34 module V
= Visitor_ast
37 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
39 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
40 type formula
= Lib_engine.ctlcocci
41 type top_formula
= NONDECL
of Lib_engine.ctlcocci
| CODE
of Lib_engine.ctlcocci
43 let union = Common.union_set
44 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
45 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
47 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
49 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
51 let used_after = ref ([] : Ast.meta_name list
)
52 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
54 let saved = ref ([] : Ast.meta_name list
)
56 let string2var x
= ("",x
)
58 (* --------------------------------------------------------------------- *)
59 (* predicates matching various nodes in the graph *)
63 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
64 | (CTL.True
,a
) | (a
,CTL.True
) -> a
69 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
70 | (CTL.False
,a
) | (a
,CTL.False
) -> a
75 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
76 | (CTL.False
,a
) | (a
,CTL.False
) -> a
81 (* drop x or true case because x might have side effects *)
82 (CTL.True
,_
) (* | (_,CTL.True) *) -> CTL.True
83 | (CTL.False
,a
) | (a
,CTL.False
) -> a
86 let ctl_not = function
88 | CTL.False
-> CTL.True
91 let ctl_ax s
= function
93 | CTL.False
-> CTL.False
96 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
97 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
99 let ctl_ax_absolute s
= function
101 | CTL.False
-> CTL.False
102 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
104 let ctl_ex = function
106 | CTL.False
-> CTL.False
107 | x
-> CTL.EX
(CTL.FORWARD
,x
)
109 (* This stays being AX even for sgrep_mode, because it is used to identify
110 the structure of the term, not matching the pattern. *)
111 let ctl_back_ax = function
113 | CTL.False
-> CTL.False
114 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
116 let ctl_back_ex = function
118 | CTL.False
-> CTL.False
119 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
121 let ctl_ef = function
123 | CTL.False
-> CTL.False
124 | x
-> CTL.EF
(CTL.FORWARD
,x
)
126 let ctl_ag s
= function
128 | CTL.False
-> CTL.False
129 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
132 match (x
,!exists) with
133 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
134 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
135 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
136 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
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 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
144 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
146 let ctl_uncheck = function
148 | CTL.False
-> CTL.False
151 let label_pred_maker = function
153 | Some
(label_var
,used
) ->
155 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
157 let bclabel_pred_maker = function
159 | Some
(label_var
,used
) ->
161 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
163 (* label used to be used here, but it is not used; label is only needed after
165 let predmaker guard pred label
= CTL.Pred pred
167 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
168 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
169 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
170 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
171 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
172 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
173 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
174 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
175 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
176 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
177 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
178 let loopfallpred = predmaker false (Lib_engine.LoopFallThrough
, CTL.Control
)
180 (*let aftret label_var =
181 ctl_or (aftpred label_var)
182 (ctl_or (loopfallpred label_var) (exitpred label_var))*)
188 Printf.sprintf
"r%d" cur
190 (* --------------------------------------------------------------------- *)
191 (* --------------------------------------------------------------------- *)
192 (* Eliminate OptStm *)
194 (* for optional thing with nothing after, should check that the optional thing
195 never occurs. otherwise the matching stops before it occurs *)
198 let donothing r k e
= k e
in
201 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
204 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
207 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
209 let inheritedlist l
=
210 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
213 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
216 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
218 let rec dots_list unwrapped wrapped
=
219 match (unwrapped
,wrapped
) with
222 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
224 | (Ast.Nest
(_
,_
,_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)
226 d0
::s
::d1
::rest
) -> (* why no case for nest as u? *)
227 let l = Ast.get_line stm
in
228 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
229 let new_rest2 = dots_list urest rest
in
230 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
231 varlists new_rest1 in
232 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
233 varlists new_rest2 in
237 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
239 Ast.free_vars
= fv_rest1
;
240 Ast.minus_free_vars
= mfv_rest1
;
241 Ast.fresh_vars
= fresh_rest1
;
242 Ast.inherited
= inherited_rest1
;
243 Ast.saved_witness
= s1
};
244 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
246 Ast.free_vars
= fv_rest2
;
247 Ast.minus_free_vars
= mfv_rest2
;
248 Ast.fresh_vars
= fresh_rest2
;
249 Ast.inherited
= inherited_rest2
;
250 Ast.saved_witness
= s2
}])) with
252 Ast.free_vars
= fv_rest1
;
253 Ast.minus_free_vars
= mfv_rest1
;
254 Ast.fresh_vars
= fresh_rest1
;
255 Ast.inherited
= inherited_rest1
;
256 Ast.saved_witness
= s1
}]
258 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
259 let l = Ast.get_line stm
in
260 let new_rest1 = dots_list urest rest
in
261 let new_rest2 = stm
::new_rest1 in
262 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
263 varlists new_rest1 in
264 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
265 varlists new_rest2 in
268 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
270 Ast.free_vars
= fv_rest2
;
271 Ast.minus_free_vars
= mfv_rest2
;
272 Ast.fresh_vars
= fresh_rest2
;
273 Ast.inherited
= inherited_rest2
;
274 Ast.saved_witness
= s2
};
275 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
277 Ast.free_vars
= fv_rest1
;
278 Ast.minus_free_vars
= mfv_rest1
;
279 Ast.fresh_vars
= fresh_rest1
;
280 Ast.inherited
= inherited_rest1
;
281 Ast.saved_witness
= s1
}])) with
283 Ast.free_vars
= fv_rest2
;
284 Ast.minus_free_vars
= mfv_rest2
;
285 Ast.fresh_vars
= fresh_rest2
;
286 Ast.inherited
= inherited_rest2
;
287 Ast.saved_witness
= s2
}]
289 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
290 let l = Ast.get_line stm
in
291 let fv_stm = Ast.get_fvs stm
in
292 let mfv_stm = Ast.get_mfvs stm
in
293 let fresh_stm = Ast.get_fresh stm
in
294 let inh_stm = Ast.get_inherited stm
in
295 let saved_stm = Ast.get_saved stm
in
296 let fv_d1 = Ast.get_fvs d1
in
297 let mfv_d1 = Ast.get_mfvs d1
in
298 let fresh_d1 = Ast.get_fresh d1
in
299 let inh_d1 = Ast.get_inherited d1
in
300 let saved_d1 = Ast.get_saved d1
in
301 let fv_both = Common.union_set
fv_stm fv_d1 in
302 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
303 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
304 let inh_both = Common.union_set
inh_stm inh_d1 in
305 let saved_both = Common.union_set
saved_stm saved_d1 in
309 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
311 Ast.free_vars
= fv_stm;
312 Ast.minus_free_vars
= mfv_stm;
313 Ast.fresh_vars
= fresh_stm;
314 Ast.inherited
= inh_stm;
315 Ast.saved_witness
= saved_stm};
316 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
318 Ast.free_vars
= fv_d1;
319 Ast.minus_free_vars
= mfv_d1;
320 Ast.fresh_vars
= fresh_d1;
321 Ast.inherited
= inh_d1;
322 Ast.saved_witness
= saved_d1}])) with
324 Ast.free_vars
= fv_both;
325 Ast.minus_free_vars
= mfv_both;
326 Ast.fresh_vars
= fresh_both;
327 Ast.inherited
= inh_both;
328 Ast.saved_witness
= saved_both}]
330 | ([Ast.Nest
(_
,_
,_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
331 let l = Ast.get_line stm
in
332 let rw = Ast.rewrap stm
in
333 let rwd = Ast.rewrap stm
in
334 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
336 [rwd(Ast.DOTS
([stm
]));
337 {(Ast.make_term
(Ast.DOTS
([rw dots])))
338 with Ast.node_line
= l}])]
340 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
341 | _
-> failwith
"not possible" in
343 let stmtdotsfn r k d
=
346 (match Ast.unwrap
d with
347 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
348 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
349 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
352 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
353 donothing donothing stmtdotsfn donothing donothing
354 donothing donothing donothing donothing donothing donothing donothing
355 donothing donothing donothing donothing donothing
357 (* --------------------------------------------------------------------- *)
358 (* after management *)
359 (* We need Guard for the following case:
368 Here the inner <... b ...> should not go past foo. But foo is not the
369 "after" of the body of the outer nest, because we don't want to search for
370 it in the case where the body of the outer nest ends in something other
371 than dots or a nest. *)
373 (* what is the difference between tail and end??? *)
375 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
377 let a2n = function After x
-> Guard x
| a
-> a
380 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
381 let pp_meta (_
,x
) = Common.pp x
in
382 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
383 Format.print_newline
()
385 let print_after = function
386 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
387 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
388 | Tail
-> Printf.printf
"Tail\n"
389 | VeryEnd
-> Printf.printf
"Very End\n"
390 | End
-> Printf.printf
"End\n"
392 (* --------------------------------------------------------------------- *)
395 let fresh_var _
= string2var "_v"
396 let fresh_pos _
= string2var "_pos" (* must be a constant *)
398 let fresh_metavar _
= "_S"
400 (* fvinfo is going to end up being from the whole associated statement.
401 it would be better if it were just the free variables in d, but free_vars.ml
402 doesn't keep track of free variables on + code *)
403 let make_meta_rule_elem d fvinfo
=
404 let nm = fresh_metavar() in
405 Ast.make_meta_rule_elem nm d fvinfo
407 let get_unquantified quantified vars
=
408 List.filter
(function x
-> not
(List.mem x quantified
)) vars
410 let make_seq guard
l =
411 let s = guard_to_strict guard
in
412 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
414 let make_seq_after2 guard first rest
=
415 let s = guard_to_strict guard
in
417 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
420 let make_seq_after guard first rest
=
422 After rest
-> make_seq guard
[first
;rest
]
425 let opt_and guard first rest
=
426 let s = guard_to_strict guard
in
429 | Some first
-> ctl_and s first rest
431 let and_after guard first rest
=
432 let s = guard_to_strict guard
in
433 match rest
with After rest
-> ctl_and s first rest
| _
-> first
436 let bind x y
= x
or y
in
437 let option_default = false in
438 let mcode r
(_
,_
,kind
,metapos
) =
440 Ast.MINUS
(_
,_
,_
,_
) -> true
441 | Ast.PLUS _
-> failwith
"not possible"
442 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
443 let do_nothing r k e
= k e
in
444 let rule_elem r k re
=
446 match Ast.unwrap re
with
447 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
448 bind (mcode r
((),(),bef
,[])) res
449 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,[])) res
453 match Ast.unwrap i
with
454 Ast.StrInitList
(allminus
,_
,_
,_
,_
) -> allminus
or res
457 V.combiner
bind option_default
458 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
459 do_nothing do_nothing do_nothing do_nothing do_nothing
460 do_nothing do_nothing do_nothing do_nothing init do_nothing
461 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
462 recursor.V.combiner_rule_elem
465 let bind x y
= x
or y
in
466 let option_default = false in
467 let mcode r
(_
,_
,kind
,metapos
) = not
(metapos
= []) in
468 let do_nothing r k e
= k e
in
469 let rule_elem r k re
=
471 match Ast.unwrap re
with
472 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
473 bind (mcode r
((),(),bef
,[])) res
474 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,[])) res
477 V.combiner
bind option_default
478 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
479 do_nothing do_nothing do_nothing do_nothing do_nothing
480 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
481 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
482 recursor.V.combiner_rule_elem
484 (* code is not a DisjRuleElem *)
485 let make_match label guard code
=
486 let v = fresh_var() in
487 let matcher = Lib_engine.Match
(code
) in
488 if contains_modif code
&& not guard
489 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
491 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
492 (match (iso_info,!onlyModif,guard
,
493 intersect !used_after (Ast.get_fvs code
)) with
494 (false,true,_
,[]) | (_
,_
,true,_
) ->
495 predmaker guard
(matcher,CTL.Control
) label
496 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
498 let make_raw_match label guard code
=
499 match intersect !used_after (Ast.get_fvs code
) with
500 [] -> predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
502 let v = fresh_var() in
503 CTL.Exists
(true,v,predmaker guard
(Lib_engine.Match
(code
),CTL.UnModif
v)
506 let rec seq_fvs quantified
= function
509 let t1fvs = get_unquantified quantified fv1
in
511 List.fold_left
Common.union_set
[]
512 (List.map
(get_unquantified quantified
) fvs
) in
513 let bothfvs = Common.inter_set
t1fvs termfvs in
514 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
515 let new_quantified = Common.union_set
bothfvs quantified
in
516 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
521 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
523 let non_saved_quantify =
525 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
527 let intersectll lst nested_list
=
528 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
530 (* --------------------------------------------------------------------- *)
531 (* Count depth of braces. The translation of a closed brace appears deeply
532 nested within the translation of the sequence term, so the name of the
533 paren var has to take into account the names of the nested braces. On the
534 other hand the close brace does not escape, so we don't have to take into
535 account other paren variable names. *)
537 (* called repetitively, which is inefficient, but less trouble than adding a
538 new field to Seq and FunDecl *)
539 let count_nested_braces s =
540 let bind x y
= max x y
in
541 let option_default = 0 in
542 let stmt_count r k
s =
543 match Ast.unwrap
s with
544 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
546 let donothing r k e
= k e
in
548 let recursor = V.combiner
bind option_default
549 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
550 donothing donothing donothing donothing donothing
551 donothing donothing donothing donothing donothing donothing
552 donothing donothing stmt_count donothing donothing donothing in
553 let res = string_of_int
(recursor.V.combiner_statement
s) in
557 let get_label_ctr _
=
558 let cur = !labelctr in
560 string2var (Printf.sprintf
"l%d" cur)
562 (* --------------------------------------------------------------------- *)
563 (* annotate dots with before and after neighbors *)
565 let print_bef_aft = function
567 Printf.printf
"bef/aft\n";
568 Pretty_print_cocci.rule_elem "" re
;
569 Format.print_newline
()
571 Printf.printf
"bef/aft\n";
572 Pretty_print_cocci.statement
"" s;
573 Format.print_newline
()
574 | Ast.Other_dots
d ->
575 Printf.printf
"bef/aft\n";
576 Pretty_print_cocci.statement_dots
d;
577 Format.print_newline
()
579 (* [] can only occur if we are in a disj, where it comes from a ? In that
580 case, we want to use a, which accumulates all of the previous patterns in
582 let rec get_before_elem sl a
=
583 match Ast.unwrap sl
with
587 [] -> ([],Common.Right a
)
589 let (e
,ea
) = get_before_e e a
in
592 let (e
,ea
) = get_before_e e a
in
593 let (sl
,sla
) = loop sl ea
in
595 let (l,a
) = loop x a
in
596 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
597 | Ast.CIRCLES
(x
) -> failwith
"not supported"
598 | Ast.STARS
(x
) -> failwith
"not supported"
600 and get_before sl a
=
601 match get_before_elem sl a
with
602 (term
,Common.Left x
) -> (term
,x
)
603 | (term
,Common.Right x
) -> (term
,x
)
605 and get_before_whencode wc
=
608 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
609 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
610 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
611 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
612 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
615 and get_before_e
s a
=
616 match Ast.unwrap
s with
617 Ast.Dots
(d,w
,_
,aft
) ->
618 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
619 | Ast.Nest
(starter
,stmt_dots
,ender
,w
,multi
,_
,aft
) ->
620 let w = get_before_whencode
w in
621 let (sd
,_
) = get_before stmt_dots a
in
623 got rid of this, don't want to let nests overshoot
628 Unify_ast.unify_statement_dots
629 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
631 Unify_ast.MAYBE -> false
633 | Ast.Other_dots a ->
634 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
636 Unify_ast.MAYBE -> false
640 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,a,aft
)),
641 [Ast.Other_dots stmt_dots
])
642 | Ast.Disj
(stmt_dots_list
) ->
644 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
645 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
647 (match Ast.unwrap ast
with
648 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
649 | _
-> (s,[Ast.Other
s]))
650 | Ast.Seq
(lbrace
,body
,rbrace
) ->
651 let index = count_nested_braces s in
652 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
653 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
654 | Ast.Define
(header
,body
) ->
655 let (body
,_
) = get_before body
[] in
656 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
657 | Ast.IfThen
(ifheader
,branch
,aft
) ->
658 let (br
,_
) = get_before_e branch
[] in
659 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
660 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
661 let (br1
,_
) = get_before_e branch1
[] in
662 let (br2
,_
) = get_before_e branch2
[] in
663 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
664 | Ast.While
(header
,body
,aft
) ->
665 let (bd
,_
) = get_before_e body
[] in
666 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
667 | Ast.For
(header
,body
,aft
) ->
668 let (bd
,_
) = get_before_e body
[] in
669 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
670 | Ast.Do
(header
,body
,tail
) ->
671 let (bd
,_
) = get_before_e body
[] in
672 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
673 | Ast.Iterator
(header
,body
,aft
) ->
674 let (bd
,_
) = get_before_e body
[] in
675 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
676 | Ast.Switch
(header
,lb
,decls
,cases
,rb
) ->
677 let index = count_nested_braces s in
678 let (de
,dea
) = get_before decls
[Ast.WParen
(lb
,index)] in
681 (function case_line
->
682 match Ast.unwrap case_line
with
683 Ast.CaseLine
(header
,body
) ->
684 let (body
,_
) = get_before body
[] in
685 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
686 | Ast.OptCase
(case_line
) -> failwith
"not supported")
688 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),
689 [Ast.WParen
(rb
,index)])
690 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
691 let (bd
,_
) = get_before body
[] in
692 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
694 Pretty_print_cocci.statement
"" s; Format.print_newline
();
695 failwith
"get_before_e: not supported"
697 let rec get_after sl
a =
698 match Ast.unwrap sl
with
704 let (sl
,sla
) = loop sl
in
705 let (e
,ea
) = get_after_e e sla
in
707 let (l,a) = loop x
in
708 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
709 | Ast.CIRCLES
(x
) -> failwith
"not supported"
710 | Ast.STARS
(x
) -> failwith
"not supported"
712 and get_after_whencode
a wc
=
715 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
716 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
717 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
718 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
719 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
722 and get_after_e
s a =
723 match Ast.unwrap
s with
724 Ast.Dots
(d,w,bef
,_
) ->
725 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
726 | Ast.Nest
(starter
,stmt_dots
,ender
,w,multi
,bef
,_
) ->
727 let w = get_after_whencode
a w in
728 let (sd
,_
) = get_after stmt_dots
a in
730 got rid of this. don't want to let nests overshoot
735 Unify_ast.unify_statement_dots
736 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
738 Unify_ast.MAYBE -> false
740 | Ast.Other_dots a ->
741 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
743 Unify_ast.MAYBE -> false
747 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,bef
,a)),
748 [Ast.Other_dots stmt_dots
])
749 | Ast.Disj
(stmt_dots_list
) ->
751 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
752 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
754 (match Ast.unwrap ast
with
755 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
756 (* check "after" information for metavar optimization *)
757 (* if the error is not desired, could just return [], then
758 the optimization (check for EF) won't take place *)
762 (match Ast.unwrap x
with
763 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
765 "dots/nest not allowed before and after stmt metavar"
767 | Ast.Other_dots x
->
768 (match Ast.undots x
with
770 (match Ast.unwrap x
with
771 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
773 ("dots/nest not allowed before and after stmt "^
782 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
783 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
784 | _
-> (s,[Ast.Other
s]))
785 | Ast.Seq
(lbrace
,body
,rbrace
) ->
786 let index = count_nested_braces s in
787 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
788 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
789 [Ast.WParen
(lbrace
,index)])
790 | Ast.Define
(header
,body
) ->
791 let (body
,_
) = get_after body
a in
792 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
793 | Ast.IfThen
(ifheader
,branch
,aft
) ->
794 let (br
,_
) = get_after_e branch
a in
795 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
796 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
797 let (br1
,_
) = get_after_e branch1
a in
798 let (br2
,_
) = get_after_e branch2
a in
799 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
800 | Ast.While
(header
,body
,aft
) ->
801 let (bd
,_
) = get_after_e body
a in
802 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
803 | Ast.For
(header
,body
,aft
) ->
804 let (bd
,_
) = get_after_e body
a in
805 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
806 | Ast.Do
(header
,body
,tail
) ->
807 let (bd
,_
) = get_after_e body
a in
808 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
809 | Ast.Iterator
(header
,body
,aft
) ->
810 let (bd
,_
) = get_after_e body
a in
811 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
812 | Ast.Switch
(header
,lb
,decls
,cases,rb
) ->
813 let index = count_nested_braces s in
816 (function case_line
->
817 match Ast.unwrap case_line
with
818 Ast.CaseLine
(header
,body
) ->
819 let (body
,_
) = get_after body
[Ast.WParen
(rb
,index)] in
820 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
821 | Ast.OptCase
(case_line
) -> failwith
"not supported")
823 let (de
,_
) = get_after decls
[] in
824 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),[Ast.WParen
(lb
,index)])
825 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
826 let (bd
,_
) = get_after body
[] in
827 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
828 | _
-> failwith
"get_after_e: not supported"
830 let preprocess_dots sl
=
831 let (sl
,_
) = get_before sl
[] in
832 let (sl
,_
) = get_after sl
[] in
835 let preprocess_dots_e sl
=
836 let (sl
,_
) = get_before_e sl
[] in
837 let (sl
,_
) = get_after_e sl
[] in
840 (* --------------------------------------------------------------------- *)
841 (* various return_related things *)
843 let rec ends_in_return stmt_list
=
844 match Ast.unwrap stmt_list
with
846 (match List.rev x
with
848 (match Ast.unwrap x
with
851 match Ast.unwrap x
with
852 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
853 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
856 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
859 | Ast.CIRCLES
(x
) -> failwith
"not supported"
860 | Ast.STARS
(x
) -> failwith
"not supported"
862 (* --------------------------------------------------------------------- *)
865 let exptymatch l make_match make_guard_match
=
866 let pos = fresh_pos() in
867 let matches_guard_matches =
870 let pos = Ast.make_mcode
pos in
871 (make_match (Ast.set_pos x
(Some
pos)),
872 make_guard_match
(Ast.set_pos x
(Some
pos))))
874 let (matches
,guard_matches
) = List.split
matches_guard_matches in
875 let rec suffixes = function
877 | x
::xs -> xs::(suffixes xs) in
879 (* normally, we check that an expression does not match something
880 earlier in the disjunction (calculated as prefixes). But for large
881 disjunctions, this can result in a very big CTL formula. So we
882 give the user the option to say he doesn't want this feature, if that is
884 if !Flag_matcher.no_safe_expressions
885 then List.map
(function _
-> []) matches
886 else List.rev
(suffixes (List.rev guard_matches
)) in
887 let info = (* not null *)
893 ctl_and CTL.NONSTRICT
matcher
895 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
897 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
899 (* code might be a DisjRuleElem, in which case we break it apart
900 code might contain an Exp or Ty
901 this one pushes the quantifier inwards *)
902 let do_re_matches label guard
res quantified minus_quantified
=
903 let make_guard_match x
=
904 let stmt_fvs = Ast.get_mfvs x
in
905 let fvs = get_unquantified minus_quantified
stmt_fvs in
906 non_saved_quantify fvs (make_match None
true x
) in
908 let stmt_fvs = Ast.get_fvs x
in
909 let fvs = get_unquantified quantified
stmt_fvs in
910 quantify guard
fvs (make_match None guard x
) in
911 (* label used to be used here, but it is not use; label is only needed after
913 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
914 (match List.map
Ast.unwrap
res with
915 [] -> failwith
"unexpected empty disj"
916 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
917 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
919 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
921 then failwith
"unexpected exp or ty";
922 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
924 (* code might be a DisjRuleElem, in which case we break it apart
925 code doesn't contain an Exp or Ty
926 this one is for use when it is not practical to push the quantifier inwards
928 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
929 match Ast.unwrap code
with
930 Ast.DisjRuleElem
(res) ->
931 let make_match = make_match None guard
in
932 let orop = if guard
then ctl_or else ctl_seqor in
933 (* label used to be used here, but it is not use; label is only needed after
935 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
936 (List.fold_left
orop CTL.False
(List.map
make_match res))
937 | _
-> make_match label guard code
939 (* --------------------------------------------------------------------- *)
940 (* control structures *)
942 let end_control_structure fvs header body after_pred
943 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
944 (* aft indicates what is added after the whole if, which has to be added
946 let (aft_needed
,after_branch
) =
948 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
949 (false,make_seq_after2 guard after_pred after
)
952 make_match label guard
953 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
955 make_seq_after guard after_pred
956 (After
(make_seq_after guard
match_endif after
))) in
957 let body = body after_branch
in
958 let s = guard_to_strict guard
in
963 (match (after
,aft_needed
) with
964 (After _
,_
) (* pattern doesn't end here *)
965 | (_
,true) (* + code added after *) -> after_checks
966 | _
-> no_after_checks
)
967 (ctl_ax_absolute s body)))
969 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
970 quantified minus_quantified label llabel slabel recurse
make_match guard
=
971 (* "if (test) thn" becomes:
972 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
974 "if (test) thn; after" becomes:
975 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
980 match seq_fvs quantified
981 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
982 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
983 | _
-> failwith
"not possible" in
984 let new_quantified = Common.union_set bfvs quantified
in
986 match seq_fvs minus_quantified
987 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
988 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
989 | _
-> failwith
"not possible" in
990 let new_mquantified = Common.union_set mbfvs minus_quantified
in
992 let if_header = quantify guard efvs
(make_match ifheader
) in
993 (* then branch and after *)
994 let lv = get_label_ctr() in
995 let used = ref false in
997 (* no point to put a label on truepred etc; it is local to this construct
998 so it must have the same label *)
1000 [truepred None
; recurse branch Tail
new_quantified new_mquantified
1001 (Some
(lv,used)) llabel slabel guard
] in
1002 let after_pred = aftpred None
in
1003 let or_cases after_branch
=
1004 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
1005 let (if_header,wrapper
) =
1008 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1009 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1010 (function body -> quantify true [lv] body))
1011 else (if_header,function x
-> x
) in
1013 (end_control_structure bfvs
if_header or_cases after_pred
1014 (Some
(ctl_ex after_pred)) None aft after label guard
)
1016 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
1017 quantified minus_quantified label llabel slabel recurse
make_match guard
=
1018 (* "if (test) thn else els" becomes:
1019 if(test) & AX((TrueBranch & AX thn) v
1020 (FalseBranch & AX (else & AX els)) v After)
1023 "if (test) thn else els; after" becomes:
1024 if(test) & AX((TrueBranch & AX thn) v
1025 (FalseBranch & AX (else & AX els)) v
1026 (After & AXAX after))
1030 (* free variables *)
1031 let (e1fvs
,b1fvs
,s1fvs
) =
1032 match seq_fvs quantified
1033 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1034 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1035 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1036 | _
-> failwith
"not possible" in
1037 let (e2fvs
,b2fvs
,s2fvs
) =
1039 (* just combine with the else branch. no point to have separate
1040 quantifier, since there is only one possible control-flow path *)
1041 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1042 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1043 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1044 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1045 | _
-> failwith
"not possible" in
1046 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1047 let exponlyfvs = intersect e1fvs e2fvs
in
1048 let new_quantified = union bothfvs quantified
in
1049 (* minus free variables *)
1050 let (me1fvs
,mb1fvs
,ms1fvs
) =
1051 match seq_fvs minus_quantified
1052 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1053 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1054 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1055 | _
-> failwith
"not possible" in
1056 let (me2fvs
,mb2fvs
,ms2fvs
) =
1058 (* just combine with the else branch. no point to have separate
1059 quantifier, since there is only one possible control-flow path *)
1061 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1062 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1063 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1064 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1065 | _
-> failwith
"not possible" in
1066 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1067 let new_mquantified = union mbothfvs minus_quantified
in
1069 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1070 (* then and else branches *)
1071 let lv = get_label_ctr() in
1072 let used = ref false in
1075 [truepred None
; recurse branch1 Tail
new_quantified new_mquantified
1076 (Some
(lv,used)) llabel slabel guard
] in
1081 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1082 (header_match None guard els
);
1083 recurse branch2 Tail
new_quantified new_mquantified
1084 (Some
(lv,used)) llabel slabel guard
] in
1085 let after_pred = aftpred None
in
1086 let or_cases after_branch
=
1087 ctl_or true_branch (ctl_or false_branch after_branch
) in
1088 let s = guard_to_strict guard
in
1089 let (if_header,wrapper
) =
1092 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1093 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1094 (function body -> quantify true [lv] body))
1095 else (if_header,function x
-> x
) in
1097 (end_control_structure bothfvs if_header or_cases after_pred
1098 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1099 (Some
(ctl_ex (falsepred None
)))
1100 aft after label guard
)
1102 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1103 quantified minus_quantified label recurse
make_match guard
=
1105 (* the translation in this case is similar to that of an if with no else *)
1106 (* free variables *)
1108 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1109 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1110 | _
-> failwith
"not possible" in
1111 let new_quantified = Common.union_set bfvs quantified
in
1112 (* minus free variables *)
1114 match seq_fvs minus_quantified
1115 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1116 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1117 | _
-> failwith
"not possible" in
1118 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1120 let header = quantify guard efvs
(make_match header) in
1121 let lv = get_label_ctr() in
1122 let used = ref false in
1126 recurse
body Tail
new_quantified new_mquantified
1127 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1128 let after_pred = loopfallpred None
in
1129 let or_cases after_branch
= ctl_or body after_branch
in
1130 let (header,wrapper
) =
1133 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1134 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1135 (function body -> quantify true [lv] body))
1136 else (header,function x
-> x
) in
1138 (end_control_structure bfvs
header or_cases after_pred
1139 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1140 match (Ast.unwrap
body,aft
) with
1141 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1142 (match Ast.unwrap re
with
1143 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1144 Type_cocci.Unitary
,_
,false)
1145 when after
= Tail
or after
= End
or after
= VeryEnd
->
1147 match seq_fvs quantified
[Ast.get_fvs
header] with
1149 | _
-> failwith
"not possible" in
1150 quantify guard efvs
(make_match header)
1154 (* --------------------------------------------------------------------- *)
1155 (* statement metavariables *)
1157 (* issue: an S metavariable that is not an if branch/loop body
1158 should not match an if branch/loop body, so check that the labels
1159 of the nodes before the first node matched by the S are different
1160 from the label of the first node matched by the S *)
1161 let sequencibility body label_pred process_bef_aft
= function
1162 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1165 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1166 | Ast.SequencibleAfterDots
l ->
1167 (* S appears after some dots. l is the code that comes after the S.
1168 want to search for that first, because S can match anything, while
1169 the stuff after is probably more restricted *)
1170 let afts = List.map process_bef_aft
l in
1171 let ors = foldl1 ctl_or afts in
1172 ctl_and CTL.NONSTRICT
1173 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1176 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1177 | Ast.NotSequencible
-> body (function x
-> x
)
1179 let svar_context_with_add_after stmt
s label quantified
d ast
1180 seqible after process_bef_aft guard fvinfo
=
1181 let label_var = (*fresh_label_var*) string2var "_lab" in
1183 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1184 (*let prelabel_pred =
1185 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
1186 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1187 let full_metamatch = matcher d in
1188 let first_metamatch =
1191 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
,c
)) ->
1192 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
,c
))
1193 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1194 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1196 let middle_metamatch =
1199 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1200 | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
1202 let last_metamatch =
1205 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
,c
)) ->
1206 Ast.CONTEXT
(pos,Ast.AFTER
(aft
,c
))
1207 | Ast.CONTEXT
(_
,_
) -> d
1208 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1212 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1215 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1216 let left_or = (* the whole statement is one node *)
1217 make_seq_after guard
1218 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_ex to_end)) full_metamatch) after
in
1219 let right_or = (* the statement covers multiple nodes *)
1220 ctl_and CTL.NONSTRICT
1223 [to_end; make_seq_after guard
last_metamatch after
]))
1229 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1233 ctl_au CTL.NONSTRICT
1236 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1238 (ctl_not prelabel_pred) after])] in
1242 ctl_and CTL.NONSTRICT
label_pred
1243 (f
(ctl_and CTL.NONSTRICT
1244 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1245 let stmt_fvs = Ast.get_fvs stmt
in
1246 let fvs = get_unquantified quantified
stmt_fvs in
1247 quantify guard
(label_var::fvs)
1248 (sequencibility body label_pred process_bef_aft seqible
)
1250 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1251 seqible after process_bef_aft guard fvinfo
=
1252 let label_var = (*fresh_label_var*) string2var "_lab" in
1254 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1256 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1257 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1259 match (d,after
) with
1260 (Ast.PLUS _
, _
) -> failwith
"not possible"
1261 | (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1262 (* just match the root. don't care about label; always ok *)
1263 make_raw_match None
false ast
1264 | (Ast.CONTEXT
(pos,Ast.BEFORE
(_
,_
)),(Tail
|End
|VeryEnd
)) ->
1265 ctl_and CTL.NONSTRICT
1266 (make_raw_match None
false ast
) (* statement *)
1267 (matcher d) (* transformation *)
1268 | (Ast.CONTEXT
(pos,(Ast.NOTHING
|Ast.BEFORE
(_
,_
))),(After
a | Guard
a)) ->
1269 (* This case and the MINUS one couldprobably be merged, if
1270 HackForStmt were to notice when its arguments are trivial *)
1271 let first_metamatch = matcher d in
1272 (* try to follow after link *)
1273 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1275 ctl_ex(make_seq guard
[to_end; CTL.True
; a]) in
1277 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1278 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1279 (ctl_and CTL.NONSTRICT
1280 first_metamatch (ctl_or is_compound not_compound))
1281 | (Ast.CONTEXT
(pos,(Ast.AFTER _
|Ast.BEFOREAFTER _
)),_
) ->
1282 failwith
"not possible"
1283 | (Ast.MINUS
(pos,inst
,adj
,l),after
) ->
1284 let (first_metamatch,last_metamatch,rest_metamatch
) =
1286 Ast.NOREPLACEMENT
->
1287 (matcher(Ast.CONTEXT
(pos,Ast.NOTHING
)),CTL.True
,matcher d)
1289 matcher(Ast.MINUS
(pos,inst
,adj
,Ast.NOREPLACEMENT
)),
1290 ctl_and CTL.NONSTRICT
1291 (ctl_not (make_raw_match label
false ast
))
1292 (matcher(Ast.MINUS
(pos,inst
,adj
,Ast.NOREPLACEMENT
)))) in
1293 (* try to follow after link *)
1294 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1298 [to_end; make_seq_after guard
last_metamatch after
]) in
1300 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1301 ctl_and CTL.NONSTRICT
1302 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1303 (ctl_and CTL.NONSTRICT
1304 first_metamatch (ctl_or is_compound not_compound)))
1305 (* don't have to put anything before the beginning, so don't have to
1306 distinguish the first node. so don't have to bother about paths,
1307 just use the label. label ensures that found nodes match up with
1308 what they should because it is in the lhs of the andany. *)
1309 (CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1310 ctl_and CTL.NONSTRICT
label_pred
1311 (make_raw_match label
false ast
),
1312 ctl_and CTL.NONSTRICT rest_metamatch
prelabel_pred))
1314 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1315 let stmt_fvs = Ast.get_fvs stmt
in
1316 let fvs = get_unquantified quantified
stmt_fvs in
1317 quantify guard
(label_var::fvs)
1318 (sequencibility body label_pred process_bef_aft seqible
)
1320 (* --------------------------------------------------------------------- *)
1321 (* dots and nests *)
1323 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1324 let matchgoto = gotopred None
in
1326 make_match None
false
1328 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1330 make_match None
false
1332 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1334 if quantifier
= Exists
1335 then Common.Left
(CTL.False
)
1337 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1339 then Common.Left
(aftpred label
)
1342 (function vx
-> function v ->
1343 (* vx is the contents of the nest, if any. we can only stop early
1344 if we find neither the ending code nor the nest contents in
1345 the if branch. not sure if this is a good idea. *)
1346 let lv = get_label_ctr() in
1347 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1348 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1350 (* Rather a special case. But if the code afterwards is just
1351 a } then there is no point checking after a goto that it does
1353 (* this optimization doesn't work. probably depends on whether
1354 the destination of the break/goto is local or more global than
1356 match seq_after
with
1358 let is_paren = function
1359 CTL.Pred
(Lib_engine.Paren _
,_
) -> true
1361 is_paren e1
or is_paren e2
1363 ctl_or (aftpred label
)
1364 (quantify false [lv]
1365 (ctl_and CTL.NONSTRICT
1366 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1367 (ctl_au CTL.NONSTRICT
1368 (ctl_and CTL.NONSTRICT
(ctl_not v)
1369 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1370 (ctl_and CTL.NONSTRICT
preflabelpred
1371 (if !Flag_matcher.only_return_is_error_exit
1373 (ctl_and CTL.NONSTRICT
1374 (retpred None
) (ctl_not seq_after
))
1377 (ctl_and CTL.NONSTRICT
1378 (ctl_or (retpred None
) matchcontinue)
1379 (ctl_not seq_after
))
1380 (ctl_and CTL.NONSTRICT
1381 (ctl_or matchgoto matchbreak)
1383 (* an optim that failed see defn is_paren
1384 and tests/makes_a_loop *)
1388 (ctl_not seq_after
))))))))))) in
1389 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1390 let v = get_let_ctr() in
1392 (match stop_early with
1393 Common.Left x1
-> ctl_or y x1
1394 | Common.Right
stop_early ->
1397 (ctl_and CTL.NONSTRICT
(label_pred_maker label
)
1398 (stop_early n
(CTL.Ref
v)))))
1400 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1401 process_bef_aft statement_list statement guard quantified wrapcode
=
1402 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1403 (* proces bef_aft *)
1405 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1406 let bef_aft = (* to be negated *)
1410 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1413 with Not_found
-> shortest (Common.union_set bef aft
) in
1416 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1418 let check_quantifier quant other
=
1420 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1424 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1426 then failwith
"inconsistent annotation on dots"
1430 if check_quantifier Ast.WhenExists
Ast.WhenForall
1433 if check_quantifier Ast.WhenForall
Ast.WhenExists
1436 (* the following is used when we find a goto, etc and consider accepting
1437 without finding the rest of the pattern *)
1438 let aft = shortest aft in
1439 (* process whencode *)
1440 let labelled = label_pred_maker label
in
1442 let (poswhen
,negwhen
) =
1444 (function (poswhen
,negwhen
) ->
1446 Ast.WhenNot
whencodes ->
1447 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1448 | Ast.WhenAlways stm
->
1449 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1450 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1451 | Ast.WhenNotTrue
(e
) ->
1453 ctl_or (whencond_true e label guard quantified
) negwhen
)
1454 | Ast.WhenNotFalse
(e
) ->
1456 ctl_or (whencond_false e label guard quantified
) negwhen
))
1457 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1458 (*bef_aft modifies arg so that inside of a nest can't cause the next
1459 to overshoot its boundaries, eg a() <...f()...> b() where f is
1460 a metavariable and the whole thing matches code in a loop;
1461 don't want f to match eg b(), allowing to go around the loop again*)
1462 let poswhen = ctl_and_ns arg
poswhen in
1466 (* add in After, because it's not part of the program *)
1467 ctl_or (aftpred label
) negwhen
1469 ctl_and_ns poswhen (ctl_not negwhen) in
1470 (* process dot code, if any *)
1472 match (dotcode,guard
) with
1473 (None
,_) | (_,true) -> CTL.True
1474 | (Some
dotcode,_) -> dotcode in
1475 (* process nest code, if any *)
1476 (* whencode goes in the negated part of the nest; if no nest, just goes
1477 on the "true" in between code *)
1478 let plus_var = if plus
then get_label_ctr() else string2var "" in
1479 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1480 let (ornest
,just_nest
) =
1481 (* just_nest is used when considering whether to stop early, to continue
1482 to collect nest information in the if branch *)
1483 match (nest
,guard
&& not plus
) with
1484 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1485 | (Some nest
,false) ->
1486 let v = get_let_ctr() in
1490 (* the idea is that BindGood is sort of a witness; a witness to
1491 having found the subterm in at least one place. If there is
1492 not a witness, then there is a risk that it will get thrown
1493 away, if it is merged with a node that has an empty
1494 environment. See tests/nestplus. But this all seems
1495 rather suspicious *)
1496 CTL.And
(CTL.NONSTRICT
,x
,
1497 CTL.Exists
(true,plus_var2,
1498 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1499 CTL.Modif
plus_var2)))
1503 CTL.Or
(is_plus (CTL.Ref
v),
1504 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1506 let plus_modifier x
=
1513 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1518 (* label within dots is taken care of elsewhere. the next two lines
1519 put the label on the code following dots *)
1520 After f
-> ctl_and (guard_to_strict guard
) f
labelled
1522 (* actually, label should be None based on the only use of Guard... *)
1523 assert (label
= None
);
1524 ctl_and CTL.NONSTRICT
(ctl_uncheck f
) labelled
1526 let exit = endpred label
in
1527 let errorexit = exitpred label
in
1528 ctl_or exit errorexit
1529 (* not at all sure what the next two mean... *)
1533 Some
(lv,used) -> used := true;
1534 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1535 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1536 | None
-> endpred label
)
1537 (* was the following, but not clear why sgrep should allow
1539 let exit = endpred label in
1540 let errorexit = exitpred label in
1542 then ctl_or exit errorexit (* end anywhere *)
1543 else exit (* end at the real end of the function *) *)
in
1545 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1546 label
(guard_to_strict guard
) wrapcode just_nest
1548 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1549 aft ender quantifier)
1551 and get_whencond_exps e
=
1552 match Ast.unwrap e
with
1554 | Ast.DisjRuleElem
(res) ->
1555 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1556 | _ -> failwith
"not possible"
1558 and make_whencond_headers e e1 label guard quantified
=
1559 let fvs = Ast.get_fvs e
in
1561 quantify guard
(get_unquantified quantified
fvs)
1562 (make_match label guard h
) in
1567 (Ast.make_mcode
"if",
1568 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1569 let while_header e1
=
1573 (Ast.make_mcode
"while",
1574 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1579 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1580 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1582 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1584 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1586 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1587 (if_headers, while_headers, for_headers)
1589 and whencond_true e label guard quantified
=
1590 let e1 = get_whencond_exps e
in
1591 let (if_headers, while_headers, for_headers) =
1592 make_whencond_headers e
e1 label guard quantified
in
1594 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1595 (ctl_and CTL.NONSTRICT
1596 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1598 and whencond_false e label guard quantified
=
1599 let e1 = get_whencond_exps e
in
1600 let (if_headers, while_headers, for_headers) =
1601 make_whencond_headers e
e1 label guard quantified
in
1603 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1604 (* if without else *)
1605 (ctl_or (ctl_and CTL.NONSTRICT
(fallpred label
) (ctl_back_ex if_headers))
1606 (* failure of loop test *)
1607 (ctl_and CTL.NONSTRICT
(loopfallpred label
)
1608 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1610 (* --------------------------------------------------------------------- *)
1611 (* the main translation loop *)
1613 let rec statement_list stmt_list after quantified minus_quantified
1614 label llabel slabel dots_before guard
=
1616 (* include Disj to be on the safe side *)
1617 match Ast.unwrap x
with
1618 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1619 let compute_label l e db
= if db
or isdots e
then l else None
in
1620 match Ast.unwrap stmt_list
with
1622 let rec loop quantified minus_quantified dots_before label llabel slabel
1624 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1626 statement e after quantified minus_quantified
1627 (compute_label label e dots_before
)
1629 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1630 let shared = intersectll fv
fvs in
1631 let unqshared = get_unquantified quantified
shared in
1632 let new_quantified = Common.union_set
unqshared quantified
in
1633 let minus_shared = intersectll mfv mfvs
in
1635 get_unquantified minus_quantified
minus_shared in
1636 let new_mquantified =
1637 Common.union_set
munqshared minus_quantified
in
1638 quantify guard
unqshared
1641 (let (label1
,llabel1
,slabel1
) =
1642 match Ast.unwrap e
with
1644 (match Ast.unwrap re
with
1645 Ast.Goto
_ -> (None
,None
,None
)
1646 | _ -> (label
,llabel
,slabel
))
1647 | _ -> (label
,llabel
,slabel
) in
1648 loop new_quantified new_mquantified (isdots e
)
1649 label1 llabel1 slabel1
1651 new_quantified new_mquantified
1652 (compute_label label e dots_before
) llabel slabel guard
)
1653 | _ -> failwith
"not possible" in
1654 loop quantified minus_quantified dots_before
1656 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1657 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1658 | Ast.STARS
(x
) -> failwith
"not supported"
1660 (* llabel is the label of the enclosing loop and slabel is the label of the
1662 and statement stmt after quantified minus_quantified
1663 label llabel slabel guard
=
1664 let ctl_au = ctl_au CTL.NONSTRICT
in
1665 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1666 let ctl_and = ctl_and CTL.NONSTRICT
in
1667 let make_seq = make_seq guard
in
1668 let make_seq_after = make_seq_after guard
in
1669 let real_make_match = make_match in
1670 let make_match = header_match label guard
in
1672 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1675 match Ast.unwrap stmt
with
1677 (match Ast.unwrap ast
with
1678 (* the following optimisation is not a good idea, because when S
1679 is alone, we would like it not to match a declaration.
1680 this makes more matching for things like when (...) S, but perhaps
1681 that matching is not so costly anyway *)
1682 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1683 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_,_)) as d),_),
1685 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_,_)) as d),_),
1687 svar_context_with_add_after stmt
s label quantified
d ast seqible
1689 (process_bef_aft quantified minus_quantified
1690 label llabel slabel
true)
1692 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1694 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1695 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1697 (process_bef_aft quantified minus_quantified
1698 label llabel slabel
true)
1700 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1704 match Ast.unwrap ast
with
1705 Ast.DisjRuleElem
(res) ->
1706 do_re_matches label guard
res quantified minus_quantified
1707 | Ast.Exp
(_) | Ast.Ty
(_) ->
1708 let stmt_fvs = Ast.get_fvs stmt
in
1709 let fvs = get_unquantified quantified
stmt_fvs in
1710 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1712 let stmt_fvs = Ast.get_fvs stmt
in
1713 let fvs = get_unquantified quantified
stmt_fvs in
1714 quantify guard
fvs (make_match ast
) in
1715 match Ast.unwrap ast
with
1716 Ast.Break
(brk
,semi
) ->
1717 (match (llabel
,slabel
) with
1718 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1719 ctl_and term (bclabel_pred_maker slabel
)
1720 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1721 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1722 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1723 (* discard pattern that comes after return *)
1724 let normal_res = make_seq_after term after
in
1725 (* the following code tries to propagate the modifications on
1726 return; to a close brace, in the case where the final return
1729 match (retmc
,semmc
) with
1730 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1731 when !Flag.sgrep_mode2
->
1732 (* in sgrep mode, we can propagate the - *)
1735 (Ast.NOREPLACEMENT
,Ast.NOREPLACEMENT
) ->
1738 failwith
"no replacements allowed in sgrep mode" in
1739 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,new_info))
1740 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
)) ->
1743 (Ast.NOREPLACEMENT
,Ast.NOREPLACEMENT
) ->
1745 | (Ast.NOREPLACEMENT
,Ast.REPLACEMENT
(l,ct
))
1746 | (Ast.REPLACEMENT
(l,ct
),Ast.NOREPLACEMENT
) ->
1748 | (Ast.REPLACEMENT
(l1
,ct1
),Ast.REPLACEMENT
(l2
,ct2
)) ->
1749 Ast.BEFORE
(l1
@l2
,Ast.lub_count ct1 ct2
) in
1750 Some
(Ast.CONTEXT
(Ast.NoPos
,change))
1751 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
,c1
)),
1752 Ast.CONTEXT
(_,Ast.AFTER
(l2
,c2
))) ->
1754 (Ast.CONTEXT
(Ast.NoPos
,
1755 Ast.BEFORE
(l1
@l2
,Ast.lub_count c1 c2
)))
1756 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1757 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1759 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1760 Ast.CONTEXT
(_,Ast.AFTER
(l,c
))) ->
1761 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l,c
)))
1763 let ret = Ast.make_mcode
"return" in
1765 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1766 let semi = Ast.make_mcode
";" in
1768 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1770 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1773 let exit = endpred None
in
1775 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1776 let stripped_rbrace =
1777 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1779 (ctl_and (make_match mod_rbrace)
1784 (ctl_or simple_return return_expr))))
1786 (make_match stripped_rbrace)
1787 (* error exit not possible; it is in the middle
1788 of code, so a return is needed *)
1791 (* some change in the middle of the return, so have to
1792 find an actual return *)
1795 (* should try to deal with the dots_bef_aft problem elsewhere,
1796 but don't have the courage... *)
1801 do_between_dots stmt
term End
1802 quantified minus_quantified label llabel slabel guard
in
1804 make_seq_after term after
)
1805 | Ast.Seq
(lbrace
,body,rbrace
) ->
1806 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1809 [Ast.get_fvs lbrace
;Ast.get_fvs
body;Ast.get_fvs rbrace
]
1811 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] -> (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1812 | _ -> failwith
"not possible" in
1813 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1815 seq_fvs minus_quantified
1816 [Ast.get_mfvs lbrace
;Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1818 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1819 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1820 | _ -> failwith
"not possible" in
1821 let pv = count_nested_braces stmt
in
1822 let lv = get_label_ctr() in
1823 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1824 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1827 (quantify guard lbfvs
(make_match lbrace
))
1828 (ctl_and paren_pred label_pred) in
1830 match Ast.unwrap rbrace
with
1831 Ast.SeqEnd
((data
,info,_,pos)) ->
1832 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1833 | _ -> failwith
"unexpected close brace" in
1835 (* label is not needed; paren_pred is enough *)
1836 quantify guard rbfvs
1837 (ctl_au (make_match empty_rbrace)
1838 (ctl_and (real_make_match None guard rbrace
) paren_pred)) in
1839 let new_quantified2 =
1840 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1841 let new_mquantified2 =
1842 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1843 let pattern_as_given =
1844 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1845 quantify true [pv;lv]
1846 (quantify guard b1fvs
1850 (if !exists = Exists
then CTL.False
else (aftpred label
))
1851 (quantify guard b2fvs
1852 (statement_list body
1853 (After
(make_seq_after end_brace after
))
1854 new_quantified2 new_mquantified2
1855 (Some
(lv,ref true))
1856 llabel slabel
false guard
)))])) in
1858 match Ast.undots
body with
1860 (match Ast.unwrap
body with
1862 ((_,i
,Ast.CONTEXT
(_,Ast.NOTHING
),_),[],_,_) ->
1863 (match Ast.unwrap rbrace
with
1864 Ast.SeqEnd
((_,_,Ast.CONTEXT
(_,Ast.NOTHING
),_))
1865 when not
(contains_pos rbrace
) -> true
1869 if empty_body && after
= Tail
1870 (* for just a match of an if branch of the form { ... }, just
1871 match the first brace *)
1872 then quantify guard lbfvs
(make_match lbrace
)
1873 else if ends_in_return body
1875 (* matching error handling code *)
1877 1. The pattern as given
1878 2. A goto, and then some close braces, and then the pattern as
1879 given, but without the braces (only possible if there are no
1880 decls, and open and close braces are unmodified)
1881 3. Part of the pattern as given, then a goto, and then the rest
1882 of the pattern. For this case, we just check that all paths have
1883 a goto within the current braces. checking for a goto at every
1884 point in the pattern seems expensive and not worthwhile. *)
1886 let body = preprocess_dots body in (* redo, to drop braces *)
1890 (make_match empty_rbrace)
1891 (ctl_ax (* skip the destination label *)
1892 (quantify guard b2fvs
1893 (statement_list body End
1894 new_quantified2 new_mquantified2 None llabel slabel
1897 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1898 quantify true [pv;lv]
1899 (quantify guard b1fvs
1903 (CTL.AU
(* want AF even for sgrep *)
1904 (CTL.FORWARD
,CTL.STRICT
,
1905 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1906 ctl_and (* brace must be eventually after goto *)
1907 (gotopred (Some
(lv,ref true)))
1908 (* want AF even for sgrep *)
1909 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1910 (quantify guard b2fvs
1911 (statement_list body Tail
1912 new_quantified2 new_mquantified2
1913 None
(*no label because past the goto*)
1914 llabel slabel
false guard
))])) in
1915 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1916 else pattern_as_given
1917 | Ast.IfThen
(ifheader
,branch
,aft) ->
1918 ifthen ifheader branch
aft after quantified minus_quantified
1919 label llabel slabel statement
make_match guard
1921 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1922 ifthenelse ifheader branch1 els branch2
aft after quantified
1923 minus_quantified label llabel slabel statement
make_match guard
1925 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1926 | Ast.Iterator
(header,body,aft) ->
1927 forwhile header body aft after quantified minus_quantified
1928 label statement
make_match guard
1930 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1931 (*ctl_and seems pointless, disjuncts see label too
1932 (label_pred_maker label)*)
1933 (List.fold_left
ctl_seqor CTL.False
1936 statement_list sl after quantified minus_quantified label
1937 llabel slabel
true guard
)
1940 | Ast.Nest
(starter
,stmt_dots
,ender,whencode
,multi
,bef
,aft) ->
1941 (* label in recursive call is None because label check is already
1942 wrapped around the corresponding code. not good enough, want to stay
1943 in a specific region, dots and nests will keep going *)
1946 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1948 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1949 | _ -> failwith
"not possible" in
1951 (* no minus version because when code doesn't contain any minus code *)
1952 let new_quantified = Common.union_set
bfvs quantified
in
1955 match Ast.get_mcodekind starter
with (*ender must have the same mcode*)
1956 Ast.MINUS
(_,_,_,_) as d ->
1957 (* no need for the fresh metavar, but ... is a bit weird as a
1959 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1964 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1965 label
(*None*) llabel slabel
true guard
in
1966 dots_and_nests multi
1967 (Some
dots_pattern) whencode bef
aft dot_code after label
1968 (process_bef_aft
new_quantified minus_quantified
1969 label
(*None*) llabel slabel
true)
1971 statement_list x Tail
new_quantified minus_quantified label
(*None*)
1972 llabel slabel
true true)
1974 statement x Tail
new_quantified minus_quantified label
(*None*)
1977 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1979 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1982 Ast.MINUS
(_,_,_,_) ->
1983 (* no need for the fresh metavar, but ... is a bit weird as a
1985 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1987 dots_and_nests false None
whencodes bef
aft dot_code after label
1988 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1990 statement_list x Tail quantified minus_quantified
1991 None llabel slabel
true true)
1993 statement x Tail quantified minus_quantified None llabel slabel
true)
1995 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1997 | Ast.Switch
(header,lb
,decls
,cases,rb
) ->
1998 let rec intersect_all = function
2001 | x
::xs -> intersect x
(intersect_all xs) in
2002 let rec intersect_all2 = function (* pairwise *)
2007 (function elem
-> List.exists (List.mem elem
) xs)
2009 Common.union_set
front (intersect_all2 xs) in
2010 let rec union_all l = List.fold_left
union [] l in
2011 (* start normal variables *)
2012 let header_fvs = Ast.get_fvs
header in
2013 let lb_fvs = Ast.get_fvs lb
in
2014 let decl_fvs = union_all (List.map
Ast.get_fvs
(Ast.undots decls
)) in
2015 let case_fvs = List.map
Ast.get_fvs
cases in
2016 let rb_fvs = Ast.get_fvs rb
in
2017 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2018 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2020 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2021 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2022 function case_fvs ->
2023 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
2024 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
2025 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
2026 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
2028 | _ -> failwith
"not possible")
2029 ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
2030 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2031 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2032 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
2033 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
2034 List.rev all_rbfvs
) in
2035 let exponlyfvs = intersect_all all_efvs
in
2036 let lbonlyfvs = intersect_all all_lbfvs
in
2037 (* don't do anything with right brace. Hope there is no + code on it *)
2038 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2039 let b1fvs = union_all all_b1fvs
in
2040 let new1_quantified = union b1fvs quantified
in
2042 union (union_all all_b2fvs
) (intersect_all2 all_casefvs
) in
2043 let new2_quantified = union b2fvs new1_quantified in
2044 (* let b3fvs = union_all all_b3fvs in*)
2045 (* ------------------- start minus free variables *)
2046 let header_mfvs = Ast.get_mfvs
header in
2047 let lb_mfvs = Ast.get_mfvs lb
in
2048 let decl_mfvs = union_all (List.map
Ast.get_mfvs
(Ast.undots decls
)) in
2049 let case_mfvs = List.map
Ast.get_mfvs
cases in
2050 let rb_mfvs = Ast.get_mfvs rb
in
2051 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2052 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2054 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2055 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2056 function case_mfvs ->
2059 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
2060 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
2061 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
2062 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
2064 | _ -> failwith
"not possible")
2065 ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
2066 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2067 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2068 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
2069 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
2070 List.rev all_mrbfvs
) in
2071 (* don't do anything with right brace. Hope there is no + code on it *)
2072 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2073 let mb1fvs = union_all all_mb1fvs
in
2074 let new1_mquantified = union mb1fvs quantified
in
2076 union (union_all all_mb2fvs
) (intersect_all2 all_mcasefvs
) in
2077 let new2_mquantified = union mb2fvs new1_mquantified in
2078 (* let b3fvs = union_all all_b3fvs in*)
2079 (* ------------------- end collection of free variables *)
2080 let switch_header = quantify guard
exponlyfvs (make_match header) in
2081 let lb = quantify guard
lbonlyfvs (make_match lb) in
2082 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
2085 (function case_line
->
2086 match Ast.unwrap case_line
with
2087 Ast.CaseLine
(header,body) ->
2089 match seq_fvs new2_quantified [Ast.get_fvs
header] with
2090 [(e1fvs,_)] -> e1fvs
2091 | _ -> failwith
"not possible" in
2092 quantify guard
e1fvs (real_make_match label
true header)
2093 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2095 let lv = get_label_ctr() in
2096 let used = ref false in
2097 let (decls_exists_code
,decls_all_code
) =
2098 (*don't really understand this*)
2099 if (Ast.undots decls
) = []
2100 then (CTL.True
,CTL.False
)
2103 statement_list decls Tail
2104 new2_quantified new2_mquantified (Some
(lv,used)) llabel None
2109 (List.fold_left
ctl_or_fl CTL.False
2110 (List.map
ctl_uncheck
2111 (decls_all_code
::case_headers))) in
2114 (function case_line
->
2115 match Ast.unwrap case_line
with
2116 Ast.CaseLine
(header,body) ->
2117 let (e1fvs,b1fvs,s1fvs
) =
2118 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
2119 match seq_fvs new2_quantified fvs with
2120 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2121 | _ -> failwith
"not possible" in
2122 let (me1fvs
,mb1fvs,ms1fvs
) =
2123 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
2124 match seq_fvs new2_mquantified fvs with
2125 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2126 | _ -> failwith
"not possible" in
2128 quantify guard
e1fvs (make_match header) in
2129 let new3_quantified = union b1fvs new2_quantified in
2130 let new3_mquantified = union mb1fvs new2_mquantified in
2132 statement_list body Tail
2133 new3_quantified new3_mquantified (Some
(lv,used)) llabel
2134 (Some
(lv,used)) false(*?*) guard
in
2135 quantify guard
b1fvs (make_seq [case_header; body])
2136 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2138 let default_required =
2141 match Ast.unwrap case
with
2142 Ast.CaseLine
(header,_) ->
2143 (match Ast.unwrap
header with
2144 Ast.Default
(_,_) -> true
2148 then function x
-> x
2149 else function x
-> ctl_or (fallpred label
) x
in
2150 let after_pred = aftpred label
in
2151 let body after_branch
=
2154 (quantify guard
b2fvs
2157 (List.fold_left
ctl_and CTL.True
2159 (decls_exists_code
:: case_headers)));
2160 List.fold_left
ctl_or_fl no_header
2161 (decls_all_code
:: case_code)])))
2164 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2165 match Ast.unwrap
rb with
2166 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2167 | _ -> failwith
"not possible") in
2168 let (switch_header,wrapper
) =
2171 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2172 (ctl_and switch_header label_pred,
2173 (function body -> quantify true [lv] body))
2174 else (switch_header,function x
-> x
) in
2176 (end_control_structure b1fvs switch_header body
2177 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2178 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2179 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2182 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2183 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2185 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2186 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2187 | _ -> failwith
"not possible" in
2188 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2191 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2192 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2194 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2195 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2196 | _ -> failwith
"not possible" in
2197 let function_header = quantify guard hfvs
(make_match header) in
2198 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2199 let stripped_rbrace =
2200 match Ast.unwrap rbrace
with
2201 Ast.SeqEnd
((data
,info,_,_)) ->
2202 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2203 | _ -> failwith
"unexpected close brace" in
2205 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2206 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2207 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2209 (quantify guard rbfvs
(make_match rbrace
))
2211 (* the following finds the beginning of the fake braces,
2212 if there are any, not completely sure how this works.
2213 sse the examples sw and return *)
2214 (ctl_back_ex (ctl_not fake_brace))
2215 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2216 let new_quantified3 =
2217 Common.union_set
b1fvs
2218 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2219 let new_mquantified3 =
2220 Common.union_set
mb1fvs
2221 (Common.union_set
mb2fvs
2222 (Common.union_set mb3fvs minus_quantified
)) in
2223 let not_minus = function Ast.MINUS
(_,_,_,_) -> false | _ -> true in
2225 match (Ast.undots
body,
2226 contains_modif rbrace
or contains_pos rbrace
) with
2228 (match Ast.unwrap
body with
2229 Ast.Nest
(starter
,stmt_dots
,ender,[],false,_,_)
2230 (* perhaps could optimize for minus case too... TODO *)
2231 when not_minus (Ast.get_mcodekind starter
)
2233 (* special case for function header + body - header is unambiguous
2234 and unique, so we can just look for the nested body anywhere
2238 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2239 statement_list stmt_dots
2240 (* discards match on right brace, but don't need it *)
2241 (Guard
(make_seq_after end_brace after
))
2242 new_quantified3 new_mquantified3
2243 None llabel slabel
true guard
))
2244 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2246 (* flow sensitive, so not optimizable *)
2247 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2249 | _ -> true) whencode
) ->
2250 (* try to be more efficient for the case where the body is just
2251 ... Perhaps this is too much of a special case, but useful
2252 for dropping a parameter and checking that it is never used. *)
2254 Ast.MINUS
(_,_,_,_) -> None
2257 (* no nested braces, because only dots *)
2258 string2var ("p1") in
2260 CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
2263 [ctl_and start_brace paren_pred;
2273 Ast.WhenAlways
(s) -> prev
2274 | Ast.WhenNot
(sl
) ->
2276 statement_list sl Tail
2282 | Ast.WhenNotTrue
(_)
2283 | Ast.WhenNotFalse
(_) ->
2284 failwith
"unexpected"
2286 (Ast.WhenAny
) -> CTL.False
2287 | Ast.WhenModifier
(_) -> prev
)
2288 CTL.False whencode
))
2292 Ast.WhenAlways
(s) ->
2297 label llabel slabel
true in
2299 | Ast.WhenNot
(sl
) -> prev
2300 | Ast.WhenNotTrue
(_)
2301 | Ast.WhenNotFalse
(_) ->
2302 failwith
"unexpected"
2303 | Ast.WhenModifier
(Ast.WhenAny
) ->
2305 | Ast.WhenModifier
(_) -> prev
)
2306 CTL.True whencode
) in
2309 (make_match stripped_rbrace)
2314 (* function body is all minus, no whencode *)
2315 match Ast.undots
body with
2317 (match Ast.unwrap
body with
2319 ((_,i
,(Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
) as d),_),[],_,_) ->
2320 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2321 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),_)),
2322 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),_)))
2323 when not
(contains_pos rbrace
) ->
2325 (* andany drops everything to the end, including close
2326 braces - not just function body, could check
2327 label to keep braces *)
2328 (ctl_and start_brace
2331 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2333 (make_meta_rule_elem d ([],[],[]))))))
2338 match (optim1,optim2) with
2344 quantify guard
b3fvs
2345 (statement_list body
2346 (After
(make_seq_after end_brace after
))
2347 new_quantified3 new_mquantified3 None llabel slabel
2349 quantify guard
b1fvs
2350 (make_seq [function_header; quantify guard
b2fvs body_code])
2351 | Ast.Define
(header,body) ->
2352 let (hfvs
,bfvs,bodyfvs
) =
2353 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2355 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2356 | _ -> failwith
"not possible" in
2357 let (mhfvs
,mbfvs
,mbodyfvs
) =
2358 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2360 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2361 | _ -> failwith
"not possible" in
2362 let define_header = quantify guard hfvs
(make_match header) in
2364 statement_list body after
2365 (Common.union_set
bfvs quantified
)
2366 (Common.union_set mbfvs minus_quantified
)
2367 None llabel slabel
true guard
in
2368 quantify guard
bfvs (make_seq [define_header; body_code])
2369 | Ast.OptStm
(stm
) ->
2370 failwith
"OptStm should have been compiled away\n"
2371 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2372 | _ -> failwith
"not supported" in
2373 if guard
or !dots_done
2376 do_between_dots stmt
term after quantified minus_quantified
2377 label llabel slabel guard
2379 (* term is the translation of stmt *)
2380 and do_between_dots stmt
term after quantified minus_quantified
2381 label llabel slabel guard
=
2382 match Ast.get_dots_bef_aft stmt
with
2383 Ast.AddingBetweenDots
(brace_term
,n
)
2384 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2386 statement brace_term after quantified minus_quantified
2387 label llabel slabel guard
in
2388 let v = Printf.sprintf
"_r_%d" n
in
2389 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2390 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2393 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2394 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2396 | Ast.NoDots
-> term
2398 (* un_process_bef_aft is because we don't want to do transformation in this
2399 code, and thus don't case about braces before or after it *)
2400 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2402 Ast.WParen
(re
,n
) ->
2403 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2404 let s = guard_to_strict guard
in
2405 quantify true (get_unquantified quantified
[n
])
2406 (ctl_and s (make_raw_match None guard re
) paren_pred)
2408 statement
s Tail quantified minus_quantified label llabel slabel guard
2409 | Ast.Other_dots
d ->
2410 statement_list d Tail quantified minus_quantified
2411 label llabel slabel
true guard
2413 (* --------------------------------------------------------------------- *)
2414 (* cleanup: convert AX to EX for pdots.
2415 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2416 This is what we wanted in the first place, but it wasn't possible to make
2417 because the AX and its argument are not created in the same place.
2419 (* also cleanup XX, which is a marker for the case where the programmer
2420 specifies to change the quantifier on .... Assumed to only occur after one AX
2421 or EX, or at top level. *)
2424 let c = match c with CTL.XX
(c) -> c | _ -> c in
2426 CTL.False
-> CTL.False
2427 | CTL.True
-> CTL.True
2428 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2429 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2430 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2431 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2432 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2433 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2434 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2435 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2436 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2437 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2438 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2439 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2440 | CTL.AX
(CTL.FORWARD
,s,
2442 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2443 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2445 CTL.And
(CTL.NONSTRICT
,
2446 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2447 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2448 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2449 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2450 CTL.AX
(dir
,s,cleanup phi
)
2451 | CTL.XX
(phi
) -> failwith
"bad XX"
2452 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2453 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2454 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2455 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2456 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2457 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2458 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2459 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2460 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2461 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2462 | CTL.Ref
(s) -> CTL.Ref
(s)
2463 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2464 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2466 (* --------------------------------------------------------------------- *)
2467 (* Function declaration *)
2469 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2471 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2472 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2474 saved := Ast.get_saved t
;
2475 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2476 let (wrap
,formula
) =
2477 match Ast.unwrap t
with
2478 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2479 | Ast.NONDECL
(stmt
) ->
2480 let unopt = elim_opt.V.rebuilder_statement stmt
in
2481 let unopt = preprocess_dots_e unopt in
2483 cleanup(statement
unopt VeryEnd
quantified [] None None None
false) in
2484 ((function x -> NONDECL
x), formula)
2485 | Ast.CODE
(stmt_dots
) ->
2486 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2487 let unopt = preprocess_dots unopt in
2488 let starts_with_dots =
2489 match Ast.undots stmt_dots
with
2491 (match Ast.unwrap
d with
2492 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2493 | Ast.Stars
(_,_,_,_) -> true
2496 let starts_with_brace =
2497 match Ast.undots stmt_dots
with
2499 (match Ast.unwrap
d with
2504 statement_list unopt VeryEnd
quantified [] None None None
2508 (if starts_with_dots
2510 (* EX because there is a loop on enter/top *)
2511 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2512 else if starts_with_brace
2514 ctl_and CTL.NONSTRICT
2515 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2517 ((function x -> CODE
x), formula)
2518 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords" in
2519 wrap
(quantify false quantified formula)
2521 (* --------------------------------------------------------------------- *)
2524 let asttoctlz (name
,(_,_,exists_flag
),l)
2525 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2528 (match exists_flag
with
2529 Ast.Exists
-> exists := Exists
2530 | Ast.Forall
-> exists := Forall
2531 | Ast.Undetermined
->
2532 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2534 let (l,used_after) =
2538 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2539 (List.combine
l (List.combine
used_after positions
))) in
2541 List.map2
(top_level name
)
2542 (List.combine
used_after fresh_used_after
)
2543 (List.combine fresh_used_after_seeds
l) in
2547 let asttoctl r
used_after positions
=
2549 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2550 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2551 asttoctlz (a,b
,c) used_after positions
2552 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CODE
CTL.True
]
2554 let pp_cocci_predicate (pred
,modif
) =
2555 Pretty_print_engine.pp_predicate pred
2557 let cocci_predicate_to_string (pred
,modif
) =
2558 Pretty_print_engine.predicate_to_string pred