2 * Copyright 2012, INRIA
3 * Julia Lawall, Gilles Muller
4 * Copyright 2010-2011, INRIA, University of Copenhagen
5 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
6 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
7 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
8 * This file is part of Coccinelle.
10 * Coccinelle is free software: you can redistribute it and/or modify
11 * it under the terms of the GNU General Public License as published by
12 * the Free Software Foundation, according to version 2 of the License.
14 * Coccinelle is distributed in the hope that it will be useful,
15 * but WITHOUT ANY WARRANTY; without even the implied warranty of
16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 * GNU General Public License for more details.
19 * You should have received a copy of the GNU General Public License
20 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
22 * The authors reserve the right to distribute this or future versions of
23 * Coccinelle under other licenses.
28 (* for MINUS and CONTEXT, pos is always None in this file *)
29 (*search for require*)
30 (* true = don't see all matched nodes, only modified ones *)
31 let onlyModif = ref true(*false*)
33 type ex
= Exists
| Forall
34 let exists = ref Forall
36 module Ast
= Ast_cocci
37 module V
= Visitor_ast
40 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
42 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
43 type formula
= Lib_engine.ctlcocci
44 type top_formula
= NONDECL
of Lib_engine.ctlcocci
| CODE
of Lib_engine.ctlcocci
46 let union = Common.union_set
47 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
48 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
50 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
52 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
54 let used_after = ref ([] : Ast.meta_name list
)
55 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
57 let saved = ref ([] : Ast.meta_name list
)
59 let string2var x
= ("",x
)
61 (* --------------------------------------------------------------------- *)
62 (* predicates matching various nodes in the graph *)
66 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
67 | (CTL.True
,a
) | (a
,CTL.True
) -> a
72 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
73 | (CTL.False
,a
) | (a
,CTL.False
) -> a
78 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
79 | (CTL.False
,a
) | (a
,CTL.False
) -> a
84 (* drop x or true case because x might have side effects *)
85 (CTL.True
,_
) (* | (_,CTL.True) *) -> CTL.True
86 | (CTL.False
,a
) | (a
,CTL.False
) -> a
89 let ctl_not = function
91 | CTL.False
-> CTL.True
94 let ctl_ax s
= function
96 | CTL.False
-> CTL.False
99 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
100 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
102 let ctl_ax_absolute s
= function
104 | CTL.False
-> CTL.False
105 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
107 let ctl_ex = function
109 | CTL.False
-> CTL.False
110 | x
-> CTL.EX
(CTL.FORWARD
,x
)
112 (* This stays being AX even for sgrep_mode, because it is used to identify
113 the structure of the term, not matching the pattern. *)
114 let ctl_back_ag = function
116 | CTL.False
-> CTL.False
117 | x
-> CTL.AG
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
119 let ctl_back_ax = function
121 | CTL.False
-> CTL.False
122 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
124 let ctl_back_ex = function
126 | CTL.False
-> CTL.False
127 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
129 let ctl_ef = function
131 | CTL.False
-> CTL.False
132 | x
-> CTL.EF
(CTL.FORWARD
,x
)
134 let ctl_ag s
= function
136 | CTL.False
-> CTL.False
137 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
140 match (x
,!exists) with
141 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
142 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
143 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
144 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
146 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
148 (match (x
,!exists) with
149 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
150 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
151 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
152 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
154 let ctl_uncheck = function
156 | CTL.False
-> CTL.False
159 let label_pred_maker = function
161 | Some
(label_var
,used
) ->
163 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
165 let bclabel_pred_maker = function
167 | Some
(label_var
,used
) ->
169 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
171 (* label used to be used here, but it is not used; label is only needed after
173 let predmaker guard pred label
= CTL.Pred pred
175 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
176 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
177 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
178 let unsbrpred = predmaker false (Lib_engine.UnsafeBrace
, CTL.Control
)
179 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
180 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
181 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
182 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
183 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
184 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
185 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
186 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
187 let loopfallpred = predmaker false (Lib_engine.LoopFallThrough
, CTL.Control
)
189 (*let aftret label_var =
190 ctl_or (aftpred label_var)
191 (ctl_or (loopfallpred label_var) (exitpred label_var))*)
197 Printf.sprintf
"r%d" cur
199 (* --------------------------------------------------------------------- *)
200 (* --------------------------------------------------------------------- *)
201 (* Eliminate OptStm *)
203 (* for optional thing with nothing after, should check that the optional thing
204 never occurs. otherwise the matching stops before it occurs *)
207 let donothing r k e
= k e
in
210 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
213 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
216 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
218 let inheritedlist l
=
219 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
222 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
225 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
227 let rec dots_list unwrapped wrapped
=
228 match (unwrapped
,wrapped
) with
231 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
233 | (Ast.Nest
(_
,_
,_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)
235 d0
::s
::d1
::rest
) -> (* why no case for nest as u? *)
236 let l = Ast.get_line stm
in
237 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
238 let new_rest2 = dots_list urest rest
in
239 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
240 varlists new_rest1 in
241 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
242 varlists new_rest2 in
246 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
248 Ast.free_vars
= fv_rest1
;
249 Ast.minus_free_vars
= mfv_rest1
;
250 Ast.fresh_vars
= fresh_rest1
;
251 Ast.inherited
= inherited_rest1
;
252 Ast.saved_witness
= s1
};
253 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
255 Ast.free_vars
= fv_rest2
;
256 Ast.minus_free_vars
= mfv_rest2
;
257 Ast.fresh_vars
= fresh_rest2
;
258 Ast.inherited
= inherited_rest2
;
259 Ast.saved_witness
= s2
}])) with
261 Ast.free_vars
= fv_rest1
;
262 Ast.minus_free_vars
= mfv_rest1
;
263 Ast.fresh_vars
= fresh_rest1
;
264 Ast.inherited
= inherited_rest1
;
265 Ast.saved_witness
= s1
}]
267 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
268 let l = Ast.get_line stm
in
269 let new_rest1 = dots_list urest rest
in
270 let new_rest2 = stm
::new_rest1 in
271 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
272 varlists new_rest1 in
273 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
274 varlists new_rest2 in
277 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
279 Ast.free_vars
= fv_rest2
;
280 Ast.minus_free_vars
= mfv_rest2
;
281 Ast.fresh_vars
= fresh_rest2
;
282 Ast.inherited
= inherited_rest2
;
283 Ast.saved_witness
= s2
};
284 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
286 Ast.free_vars
= fv_rest1
;
287 Ast.minus_free_vars
= mfv_rest1
;
288 Ast.fresh_vars
= fresh_rest1
;
289 Ast.inherited
= inherited_rest1
;
290 Ast.saved_witness
= s1
}])) with
292 Ast.free_vars
= fv_rest2
;
293 Ast.minus_free_vars
= mfv_rest2
;
294 Ast.fresh_vars
= fresh_rest2
;
295 Ast.inherited
= inherited_rest2
;
296 Ast.saved_witness
= s2
}]
298 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
299 let l = Ast.get_line stm
in
300 let fv_stm = Ast.get_fvs stm
in
301 let mfv_stm = Ast.get_mfvs stm
in
302 let fresh_stm = Ast.get_fresh stm
in
303 let inh_stm = Ast.get_inherited stm
in
304 let saved_stm = Ast.get_saved stm
in
305 let fv_d1 = Ast.get_fvs d1
in
306 let mfv_d1 = Ast.get_mfvs d1
in
307 let fresh_d1 = Ast.get_fresh d1
in
308 let inh_d1 = Ast.get_inherited d1
in
309 let saved_d1 = Ast.get_saved d1
in
310 let fv_both = Common.union_set
fv_stm fv_d1 in
311 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
312 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
313 let inh_both = Common.union_set
inh_stm inh_d1 in
314 let saved_both = Common.union_set
saved_stm saved_d1 in
318 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
320 Ast.free_vars
= fv_stm;
321 Ast.minus_free_vars
= mfv_stm;
322 Ast.fresh_vars
= fresh_stm;
323 Ast.inherited
= inh_stm;
324 Ast.saved_witness
= saved_stm};
325 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
327 Ast.free_vars
= fv_d1;
328 Ast.minus_free_vars
= mfv_d1;
329 Ast.fresh_vars
= fresh_d1;
330 Ast.inherited
= inh_d1;
331 Ast.saved_witness
= saved_d1}])) with
333 Ast.free_vars
= fv_both;
334 Ast.minus_free_vars
= mfv_both;
335 Ast.fresh_vars
= fresh_both;
336 Ast.inherited
= inh_both;
337 Ast.saved_witness
= saved_both}]
339 | ([Ast.Nest
(_
,_
,_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
340 let l = Ast.get_line stm
in
341 let rw = Ast.rewrap stm
in
342 let rwd = Ast.rewrap stm
in
343 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
345 [rwd(Ast.DOTS
([stm
]));
346 {(Ast.make_term
(Ast.DOTS
([rw dots])))
347 with Ast.node_line
= l}])]
349 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
350 | _
-> failwith
"not possible" in
352 let stmtdotsfn r k d
=
355 (match Ast.unwrap
d with
356 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
357 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
358 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
361 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
362 donothing donothing stmtdotsfn donothing donothing
363 donothing donothing donothing donothing donothing donothing donothing
364 donothing donothing donothing donothing donothing
366 (* --------------------------------------------------------------------- *)
367 (* after management *)
368 (* We need Guard for the following case:
377 Here the inner <... b ...> should not go past foo. But foo is not the
378 "after" of the body of the outer nest, because we don't want to search for
379 it in the case where the body of the outer nest ends in something other
380 than dots or a nest. *)
382 (* what is the difference between tail and end??? *)
384 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
386 type top
= Top
| NotTop
388 let a2n = function After x
-> Guard x
| a
-> a
391 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
392 let pp_meta (_
,x
) = Common.pp x
in
393 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
394 Format.print_newline
()
396 let print_after = function
397 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
398 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
399 | Tail
-> Printf.printf
"Tail\n"
400 | VeryEnd
-> Printf.printf
"Very End\n"
401 | End
-> Printf.printf
"End\n"
403 (* --------------------------------------------------------------------- *)
406 let fresh_var _
= string2var "_v"
407 let fresh_pos _
= string2var "_pos" (* must be a constant *)
409 let fresh_metavar _
= "_S"
411 (* fvinfo is going to end up being from the whole associated statement.
412 it would be better if it were just the free variables in d, but free_vars.ml
413 doesn't keep track of free variables on + code *)
414 let make_meta_rule_elem d fvinfo
=
415 let nm = fresh_metavar() in
416 Ast.make_meta_rule_elem nm d fvinfo
418 let get_unquantified quantified vars
=
419 List.filter
(function x
-> not
(List.mem x quantified
)) vars
421 let make_seq guard
l =
422 let s = guard_to_strict guard
in
423 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
425 let make_seq_after2 guard first rest
=
426 let s = guard_to_strict guard
in
428 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
431 let make_seq_after guard first rest
=
433 After rest
-> make_seq guard
[first
;rest
]
436 let opt_and guard first rest
=
437 let s = guard_to_strict guard
in
440 | Some first
-> ctl_and s first rest
442 let and_after guard first rest
=
443 let s = guard_to_strict guard
in
444 match rest
with After rest
-> ctl_and s first rest
| _
-> first
447 let bind x y
= x
or y
in
448 let option_default = false in
449 let mcode r
(_
,_
,kind
,metapos
) =
451 Ast.MINUS
(_
,_
,_
,_
) -> true
452 | Ast.PLUS _
-> failwith
"not possible"
453 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
454 let do_nothing r k e
= k e
in
455 let rule_elem r k re
=
457 match Ast.unwrap re
with
458 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
459 bind (mcode r
((),(),bef
,[])) res
460 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,[])) res
464 match Ast.unwrap i
with
465 Ast.StrInitList
(allminus
,_
,_
,_
,_
) -> allminus
or res
468 V.combiner
bind option_default
469 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
470 do_nothing do_nothing do_nothing do_nothing do_nothing
471 do_nothing do_nothing do_nothing do_nothing init do_nothing
472 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
473 recursor.V.combiner_rule_elem
476 let bind x y
= x
or y
in
477 let option_default = false in
478 let mcode r
(_
,_
,kind
,metapos
) = not
(metapos
= []) in
479 let do_nothing r k e
= k e
in
480 let rule_elem r k re
=
482 match Ast.unwrap re
with
483 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
484 bind (mcode r
((),(),bef
,[])) res
485 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,[])) res
488 V.combiner
bind option_default
489 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
490 do_nothing do_nothing do_nothing do_nothing do_nothing
491 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
492 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
493 recursor.V.combiner_rule_elem
495 (* code is not a DisjRuleElem *)
496 let make_match label guard code
=
497 let v = fresh_var() in
498 let matcher = Lib_engine.Match
(code
) in
499 if contains_modif code
&& not guard
500 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
502 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
503 (match (iso_info,!onlyModif,guard
,
504 intersect !used_after (Ast.get_fvs code
)) with
505 (false,true,_
,[]) | (_
,_
,true,_
) ->
506 predmaker guard
(matcher,CTL.Control
) label
507 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
509 let make_raw_match label guard code
=
510 match intersect !used_after (Ast.get_fvs code
) with
511 [] -> predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
513 let v = fresh_var() in
514 CTL.Exists
(true,v,predmaker guard
(Lib_engine.Match
(code
),CTL.UnModif
v)
517 let rec seq_fvs quantified
= function
520 let t1fvs = get_unquantified quantified fv1
in
522 List.fold_left
Common.union_set
[]
523 (List.map
(get_unquantified quantified
) fvs
) in
524 let bothfvs = Common.inter_set
t1fvs termfvs in
525 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
526 let new_quantified = Common.union_set
bothfvs quantified
in
527 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
532 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
534 let non_saved_quantify =
536 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
538 let intersectll lst nested_list
=
539 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
541 (* --------------------------------------------------------------------- *)
542 (* Count depth of braces. The translation of a closed brace appears deeply
543 nested within the translation of the sequence term, so the name of the
544 paren var has to take into account the names of the nested braces. On the
545 other hand the close brace does not escape, so we don't have to take into
546 account other paren variable names. *)
548 (* called repetitively, which is inefficient, but less trouble than adding a
549 new field to Seq and FunDecl *)
550 let count_nested_braces s =
551 let bind x y
= max x y
in
552 let option_default = 0 in
553 let stmt_count r k
s =
554 match Ast.unwrap
s with
555 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
557 let donothing r k e
= k e
in
559 let recursor = V.combiner
bind option_default
560 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
561 donothing donothing donothing donothing donothing
562 donothing donothing donothing donothing donothing donothing
563 donothing donothing stmt_count donothing donothing donothing in
564 let res = string_of_int
(recursor.V.combiner_statement
s) in
568 let get_label_ctr _
=
569 let cur = !labelctr in
571 string2var (Printf.sprintf
"l%d" cur)
573 (* --------------------------------------------------------------------- *)
574 (* annotate dots with before and after neighbors *)
576 let print_bef_aft = function
578 Printf.printf
"bef/aft\n";
579 Pretty_print_cocci.rule_elem "" re
;
580 Format.print_newline
()
582 Printf.printf
"bef/aft\n";
583 Pretty_print_cocci.statement
"" s;
584 Format.print_newline
()
585 | Ast.Other_dots
d ->
586 Printf.printf
"bef/aft\n";
587 Pretty_print_cocci.statement_dots
d;
588 Format.print_newline
()
590 (* [] can only occur if we are in a disj, where it comes from a ? In that
591 case, we want to use a, which accumulates all of the previous patterns in
593 let rec get_before_elem sl a
=
594 match Ast.unwrap sl
with
598 [] -> ([],Common.Right a
)
600 let (e
,ea
) = get_before_e e a
in
603 let (e
,ea
) = get_before_e e a
in
604 let (sl
,sla
) = loop sl ea
in
606 let (l,a
) = loop x a
in
607 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
608 | Ast.CIRCLES
(x
) -> failwith
"not supported"
609 | Ast.STARS
(x
) -> failwith
"not supported"
611 and get_before sl a
=
612 match get_before_elem sl a
with
613 (term
,Common.Left x
) -> (term
,x
)
614 | (term
,Common.Right x
) -> (term
,x
)
616 and get_before_whencode wc
=
619 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
620 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
621 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
622 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
623 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
626 and get_before_e
s a
=
627 match Ast.unwrap
s with
628 Ast.Dots
(d,w
,_
,aft
) ->
629 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
630 | Ast.Nest
(starter
,stmt_dots
,ender
,w
,multi
,_
,aft
) ->
631 let w = get_before_whencode
w in
632 let (sd
,_
) = get_before stmt_dots a
in
634 got rid of this, don't want to let nests overshoot
639 Unify_ast.unify_statement_dots
640 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
642 Unify_ast.MAYBE -> false
644 | Ast.Other_dots a ->
645 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
647 Unify_ast.MAYBE -> false
651 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,a,aft
)),
652 [Ast.Other_dots stmt_dots
])
653 | Ast.Disj
(stmt_dots_list
) ->
655 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
656 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
658 (match Ast.unwrap ast
with
659 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
660 | _
-> (s,[Ast.Other
s]))
661 | Ast.Seq
(lbrace
,body
,rbrace
) ->
662 let index = count_nested_braces s in
663 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
664 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
665 | Ast.Define
(header
,body
) ->
666 let (body
,_
) = get_before body
[] in
667 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
668 | Ast.AsStmt
(stmt
,asstmt
) ->
669 let (stmt
,_
) = get_before_e stmt
[] in
670 let (asstmt
,_
) = get_before_e asstmt
[] in
671 (Ast.rewrap
s (Ast.AsStmt
(stmt
,asstmt
)),[Ast.Other
s])
672 | Ast.IfThen
(ifheader
,branch
,aft
) ->
673 let (br
,_
) = get_before_e branch
[] in
674 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
675 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
676 let (br1
,_
) = get_before_e branch1
[] in
677 let (br2
,_
) = get_before_e branch2
[] in
678 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
679 | Ast.While
(header
,body
,aft
) ->
680 let (bd
,_
) = get_before_e body
[] in
681 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
682 | Ast.For
(header
,body
,aft
) ->
683 let (bd
,_
) = get_before_e body
[] in
684 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
685 | Ast.Do
(header
,body
,tail
) ->
686 let (bd
,_
) = get_before_e body
[] in
687 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
688 | Ast.Iterator
(header
,body
,aft
) ->
689 let (bd
,_
) = get_before_e body
[] in
690 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
691 | Ast.Switch
(header
,lb
,decls
,cases
,rb
) ->
692 let index = count_nested_braces s in
693 let (de
,dea
) = get_before decls
[Ast.WParen
(lb
,index)] in
696 (function case_line
->
697 match Ast.unwrap case_line
with
698 Ast.CaseLine
(header
,body
) ->
699 let (body
,_
) = get_before body
[] in
700 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
701 | Ast.OptCase
(case_line
) -> failwith
"not supported")
703 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),
704 [Ast.WParen
(rb
,index)])
705 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
706 let (bd
,_
) = get_before body
[] in
707 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
709 Pretty_print_cocci.statement
"" s; Format.print_newline
();
710 failwith
"get_before_e: not supported"
712 let rec get_after sl
a =
713 match Ast.unwrap sl
with
719 let (sl
,sla
) = loop sl
in
720 let (e
,ea
) = get_after_e e sla
in
722 let (l,a) = loop x
in
723 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
724 | Ast.CIRCLES
(x
) -> failwith
"not supported"
725 | Ast.STARS
(x
) -> failwith
"not supported"
727 and get_after_whencode
a wc
=
730 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
731 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
732 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
733 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
734 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
737 and get_after_e
s a =
738 match Ast.unwrap
s with
739 Ast.Dots
(d,w,bef
,_
) ->
740 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
741 | Ast.Nest
(starter
,stmt_dots
,ender
,w,multi
,bef
,_
) ->
742 let w = get_after_whencode
a w in
743 let (sd
,_
) = get_after stmt_dots
a in
745 got rid of this. don't want to let nests overshoot
750 Unify_ast.unify_statement_dots
751 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
753 Unify_ast.MAYBE -> false
755 | Ast.Other_dots a ->
756 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
758 Unify_ast.MAYBE -> false
762 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,bef
,a)),
763 [Ast.Other_dots stmt_dots
])
764 | Ast.Disj
(stmt_dots_list
) ->
766 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
767 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
769 (match Ast.unwrap ast
with
770 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
771 (* check "after" information for metavar optimization *)
772 (* if the error is not desired, could just return [], then
773 the optimization (check for EF) won't take place *)
777 (match Ast.unwrap x
with
778 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
780 "dots/nest not allowed before and after stmt metavar"
782 | Ast.Other_dots x
->
783 (match Ast.undots x
with
785 (match Ast.unwrap x
with
786 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
788 ("dots/nest not allowed before and after stmt "^
797 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
798 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
799 | _
-> (s,[Ast.Other
s]))
800 | Ast.Seq
(lbrace
,body
,rbrace
) ->
801 let index = count_nested_braces s in
802 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
803 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
804 [Ast.WParen
(lbrace
,index)])
805 | Ast.Define
(header
,body
) ->
806 let (body
,_
) = get_after body
a in
807 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
808 | Ast.AsStmt
(stmt
,asstmt
) ->
809 let (stmt
,_
) = get_after_e stmt
[] in
810 let (asstmt
,_
) = get_after_e asstmt
[] in
811 (Ast.rewrap
s (Ast.AsStmt
(stmt
,asstmt
)),[Ast.Other
s])
812 | Ast.IfThen
(ifheader
,branch
,aft
) ->
813 let (br
,_
) = get_after_e branch
a in
814 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
815 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
816 let (br1
,_
) = get_after_e branch1
a in
817 let (br2
,_
) = get_after_e branch2
a in
818 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
819 | Ast.While
(header
,body
,aft
) ->
820 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
821 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
822 | Ast.For
(header
,body
,aft
) ->
823 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
824 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
825 | Ast.Do
(header
,body
,tail
) ->
826 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
827 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
828 | Ast.Iterator
(header
,body
,aft
) ->
829 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
830 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
831 | Ast.Switch
(header
,lb
,decls
,cases,rb
) ->
832 let index = count_nested_braces s in
835 (function case_line
->
836 match Ast.unwrap case_line
with
837 Ast.CaseLine
(header
,body
) ->
838 let (body
,_
) = get_after body
[Ast.WParen
(rb
,index)] in
839 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
840 | Ast.OptCase
(case_line
) -> failwith
"not supported")
842 let (de
,_
) = get_after decls
[] in
843 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),[Ast.WParen
(lb
,index)])
844 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
845 let (bd
,_
) = get_after body
[] in
846 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
847 | _
-> failwith
"get_after_e: not supported"
849 let preprocess_dots sl
=
850 let (sl
,_
) = get_before sl
[] in
851 let (sl
,_
) = get_after sl
[] in
854 let preprocess_dots_e sl
=
855 let (sl
,_
) = get_before_e sl
[] in
856 let (sl
,_
) = get_after_e sl
[] in
859 (* --------------------------------------------------------------------- *)
860 (* various return_related things *)
862 let rec ends_in_return stmt_list
=
863 match Ast.unwrap stmt_list
with
865 (match List.rev x
with
867 (match Ast.unwrap x
with
870 match Ast.unwrap x
with
871 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
872 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
875 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
878 | Ast.CIRCLES
(x
) -> failwith
"not supported"
879 | Ast.STARS
(x
) -> failwith
"not supported"
881 (* --------------------------------------------------------------------- *)
884 let exptymatch l make_match make_guard_match
=
885 let pos = fresh_pos() in
886 let matches_guard_matches =
889 let pos = Ast.make_mcode
pos in
890 (make_match (Ast.set_pos x
(Some
pos)),
891 make_guard_match
(Ast.set_pos x
(Some
pos))))
893 let (matches
,guard_matches
) = List.split
matches_guard_matches in
894 let rec suffixes = function
896 | x
::xs -> xs::(suffixes xs) in
898 (* normally, we check that an expression does not match something
899 earlier in the disjunction (calculated as prefixes). But for large
900 disjunctions, this can result in a very big CTL formula. So we
901 give the user the option to say he doesn't want this feature, if that is
903 if !Flag_matcher.no_safe_expressions
904 then List.map
(function _
-> []) matches
905 else List.rev
(suffixes (List.rev guard_matches
)) in
906 let info = (* not null *)
912 ctl_and CTL.NONSTRICT
matcher
914 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
916 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
918 (* code might be a DisjRuleElem, in which case we break it apart
919 code might contain an Exp or Ty
920 this one pushes the quantifier inwards *)
921 let do_re_matches label guard
res quantified minus_quantified
=
922 let make_guard_match x
=
923 let stmt_fvs = Ast.get_mfvs x
in
924 let fvs = get_unquantified minus_quantified
stmt_fvs in
925 non_saved_quantify fvs (make_match None
true x
) in
927 let stmt_fvs = Ast.get_fvs x
in
928 let fvs = get_unquantified quantified
stmt_fvs in
929 quantify guard
fvs (make_match None guard x
) in
930 (* label used to be used here, but it is not use; label is only needed after
932 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
933 (match List.map
Ast.unwrap
res with
934 [] -> failwith
"unexpected empty disj"
935 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
936 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
938 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
940 then failwith
"unexpected exp or ty";
941 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
943 (* code might be a DisjRuleElem, in which case we break it apart
944 code doesn't contain an Exp or Ty
945 this one is for use when it is not practical to push the quantifier inwards
947 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
948 match Ast.unwrap code
with
949 Ast.DisjRuleElem
(res) ->
950 let make_match = make_match None guard
in
951 let orop = if guard
then ctl_or else ctl_seqor in
952 (* label used to be used here, but it is not use; label is only needed after
954 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
955 (List.fold_left
orop CTL.False
(List.map
make_match res))
956 | _
-> make_match label guard code
958 (* --------------------------------------------------------------------- *)
959 (* control structures *)
961 let end_control_structure fvs header body after_pred
962 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
963 (* aft indicates what is added after the whole if, which has to be added
965 let (aft_needed
,after_branch
) =
967 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
968 (false,make_seq_after2 guard after_pred after
)
971 make_match label guard
972 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
974 make_seq_after guard after_pred
975 (After
(make_seq_after guard
match_endif after
))) in
976 let body = body after_branch
in
977 let s = guard_to_strict guard
in
982 (match (after
,aft_needed
) with
983 (After _
,_
) (* pattern doesn't end here *)
984 | (_
,true) (* + code added after *) -> after_checks
985 | _
-> no_after_checks
)
986 (ctl_ax_absolute s body)))
988 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
989 quantified minus_quantified label llabel slabel recurse
make_match guard
=
990 (* "if (test) thn" becomes:
991 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
993 "if (test) thn; after" becomes:
994 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
999 match seq_fvs quantified
1000 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
1001 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1002 | _
-> failwith
"not possible" in
1003 let new_quantified = Common.union_set bfvs quantified
in
1005 match seq_fvs minus_quantified
1006 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
1007 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1008 | _
-> failwith
"not possible" in
1009 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1011 let if_header = quantify guard efvs
(make_match ifheader
) in
1012 (* then branch and after *)
1013 let lv = get_label_ctr() in
1014 let used = ref false in
1016 (* no point to put a label on truepred etc; it is local to this construct
1017 so it must have the same label *)
1019 [truepred None
; recurse branch NotTop Tail
new_quantified new_mquantified
1020 (Some
(lv,used)) llabel slabel guard
] in
1021 let after_pred = aftpred None
in
1022 let or_cases after_branch
=
1023 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
1024 let (if_header,wrapper
) =
1027 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1028 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1029 (function body -> quantify true [lv] body))
1030 else (if_header,function x
-> x
) in
1032 (end_control_structure bfvs
if_header or_cases after_pred
1033 (Some
(ctl_ex after_pred)) None aft after label guard
)
1035 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
1036 quantified minus_quantified label llabel slabel recurse
make_match guard
=
1037 (* "if (test) thn else els" becomes:
1038 if(test) & AX((TrueBranch & AX thn) v
1039 (FalseBranch & AX (else & AX els)) v After)
1042 "if (test) thn else els; after" becomes:
1043 if(test) & AX((TrueBranch & AX thn) v
1044 (FalseBranch & AX (else & AX els)) v
1045 (After & AXAX after))
1049 (* free variables *)
1050 let (e1fvs
,b1fvs
,s1fvs
) =
1051 match seq_fvs quantified
1052 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1053 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1054 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1055 | _
-> failwith
"not possible" in
1056 let (e2fvs
,b2fvs
,s2fvs
) =
1058 (* just combine with the else branch. no point to have separate
1059 quantifier, since there is only one possible control-flow path *)
1060 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1061 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1062 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1063 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1064 | _
-> failwith
"not possible" in
1065 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1066 let exponlyfvs = intersect e1fvs e2fvs
in
1067 let new_quantified = union bothfvs quantified
in
1068 (* minus free variables *)
1069 let (me1fvs
,mb1fvs
,ms1fvs
) =
1070 match seq_fvs minus_quantified
1071 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1072 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1073 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1074 | _
-> failwith
"not possible" in
1075 let (me2fvs
,mb2fvs
,ms2fvs
) =
1077 (* just combine with the else branch. no point to have separate
1078 quantifier, since there is only one possible control-flow path *)
1080 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1081 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1082 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1083 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1084 | _
-> failwith
"not possible" in
1085 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1086 let new_mquantified = union mbothfvs minus_quantified
in
1088 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1089 (* then and else branches *)
1090 let lv = get_label_ctr() in
1091 let used = ref false in
1094 [truepred None
; recurse branch1 NotTop Tail
new_quantified new_mquantified
1095 (Some
(lv,used)) llabel slabel guard
] in
1100 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1101 (header_match None guard els
);
1102 recurse branch2 NotTop Tail
new_quantified new_mquantified
1103 (Some
(lv,used)) llabel slabel guard
] in
1104 let after_pred = aftpred None
in
1105 let or_cases after_branch
=
1106 ctl_or true_branch (ctl_or false_branch after_branch
) in
1107 let s = guard_to_strict guard
in
1108 let (if_header,wrapper
) =
1111 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1112 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1113 (function body -> quantify true [lv] body))
1114 else (if_header,function x
-> x
) in
1116 (end_control_structure bothfvs if_header or_cases after_pred
1117 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1118 (Some
(ctl_ex (falsepred None
)))
1119 aft after label guard
)
1121 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1122 quantified minus_quantified label recurse
make_match guard
=
1124 (* the translation in this case is similar to that of an if with no else *)
1125 (* free variables *)
1127 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1128 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1129 | _
-> failwith
"not possible" in
1130 let new_quantified = Common.union_set bfvs quantified
in
1131 (* minus free variables *)
1133 match seq_fvs minus_quantified
1134 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1135 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1136 | _
-> failwith
"not possible" in
1137 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1139 let header = quantify guard efvs
(make_match header) in
1140 let lv = get_label_ctr() in
1141 let used = ref false in
1145 recurse
body NotTop Tail
new_quantified new_mquantified
1146 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1147 let after_pred = loopfallpred None
in
1148 let or_cases after_branch
= ctl_or body after_branch
in
1149 let (header,wrapper
) =
1152 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1153 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1154 (function body -> quantify true [lv] body))
1155 else (header,function x
-> x
) in
1157 (end_control_structure bfvs
header or_cases after_pred
1158 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1159 match (Ast.unwrap
body,aft
) with
1160 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1161 (match Ast.unwrap re
with
1162 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1163 Type_cocci.Unitary
,_
,false)
1164 when after
= Tail
or after
= End
or after
= VeryEnd
->
1166 match seq_fvs quantified
[Ast.get_fvs
header] with
1168 | _
-> failwith
"not possible" in
1169 quantify guard efvs
(make_match header)
1173 (* --------------------------------------------------------------------- *)
1174 (* statement metavariables *)
1176 (* issue: an S metavariable that is not an if branch/loop body
1177 should not match an if branch/loop body, so check that the labels
1178 of the nodes before the first node matched by the S are different
1179 from the label of the first node matched by the S *)
1180 let sequencibility body label_pred process_bef_aft
= function
1181 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1184 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1185 | Ast.SequencibleAfterDots
l ->
1186 (* S appears after some dots. l is the code that comes after the S.
1187 want to search for that first, because S can match anything, while
1188 the stuff after is probably more restricted *)
1189 let afts = List.map process_bef_aft
l in
1190 let ors = foldl1 ctl_or afts in
1191 ctl_and CTL.NONSTRICT
1192 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1195 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1196 | Ast.NotSequencible
-> body (function x
-> x
)
1198 let svar_context_with_add_after stmt
s label quantified
d ast
1199 seqible after process_bef_aft guard fvinfo
=
1200 let label_var = (*fresh_label_var*) string2var "_lab" in
1202 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1203 (*let prelabel_pred =
1204 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
1205 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1206 let full_metamatch = matcher d in
1207 let first_metamatch =
1210 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
,c
)) ->
1211 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
,c
))
1212 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1213 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1215 let middle_metamatch =
1218 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1219 | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
1221 let last_metamatch =
1224 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
,c
)) ->
1225 Ast.CONTEXT
(pos,Ast.AFTER
(aft
,c
))
1226 | Ast.CONTEXT
(_
,_
) -> d
1227 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1231 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1234 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1235 let left_or = (* the whole statement is one node *)
1236 make_seq_after guard
1237 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_ex to_end)) full_metamatch) after
in
1238 let right_or = (* the statement covers multiple nodes *)
1239 ctl_and CTL.NONSTRICT
1242 [to_end; make_seq_after guard
last_metamatch after
]))
1248 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1252 ctl_au CTL.NONSTRICT
1255 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1257 (ctl_not prelabel_pred) after])] in
1261 ctl_and CTL.NONSTRICT
label_pred
1262 (f
(ctl_and CTL.NONSTRICT
1263 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1264 let stmt_fvs = Ast.get_fvs stmt
in
1265 let fvs = get_unquantified quantified
stmt_fvs in
1266 quantify guard
(label_var::fvs)
1267 (sequencibility body label_pred process_bef_aft seqible
)
1269 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1270 seqible after process_bef_aft guard fvinfo
=
1271 let label_var = (*fresh_label_var*) string2var "_lab" in
1273 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1275 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1276 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1278 match (d,after
) with
1279 (Ast.PLUS _
, _
) -> failwith
"not possible"
1280 | (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1281 (* just match the root. don't care about label; always ok *)
1282 make_raw_match None
false ast
1283 | (Ast.CONTEXT
(pos,Ast.BEFORE
(_
,_
)),(Tail
|End
|VeryEnd
)) ->
1284 ctl_and CTL.NONSTRICT
1285 (make_raw_match None
false ast
) (* statement *)
1286 (matcher d) (* transformation *)
1287 | (Ast.CONTEXT
(pos,(Ast.NOTHING
|Ast.BEFORE
(_
,_
))),(After
a | Guard
a)) ->
1288 (* This case and the MINUS one couldprobably be merged, if
1289 HackForStmt were to notice when its arguments are trivial *)
1290 let first_metamatch = matcher d in
1291 (* try to follow after link *)
1292 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1294 ctl_ex(make_seq guard
[to_end; CTL.True
; a]) in
1296 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1297 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1298 (ctl_and CTL.NONSTRICT
1299 first_metamatch (ctl_or is_compound not_compound))
1300 | (Ast.CONTEXT
(pos,(Ast.AFTER _
|Ast.BEFOREAFTER _
)),_
) ->
1301 failwith
"not possible"
1302 | (Ast.MINUS
(pos,inst
,adj
,l),after
) ->
1303 let (first_metamatch,last_metamatch,rest_metamatch
) =
1305 Ast.NOREPLACEMENT
->
1306 (matcher(Ast.CONTEXT
(pos,Ast.NOTHING
)),CTL.True
,matcher d)
1308 matcher(Ast.MINUS
(pos,inst
,adj
,Ast.NOREPLACEMENT
)),
1309 ctl_and CTL.NONSTRICT
1310 (ctl_not (make_raw_match label
false ast
))
1311 (matcher(Ast.MINUS
(pos,inst
,adj
,Ast.NOREPLACEMENT
)))) in
1312 (* try to follow after link *)
1313 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1317 [to_end; make_seq_after guard
last_metamatch after
]) in
1319 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1320 ctl_and CTL.NONSTRICT
1321 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1322 (ctl_and CTL.NONSTRICT
1323 first_metamatch (ctl_or is_compound not_compound)))
1324 (* don't have to put anything before the beginning, so don't have to
1325 distinguish the first node. so don't have to bother about paths,
1326 just use the label. label ensures that found nodes match up with
1327 what they should because it is in the lhs of the andany. *)
1328 (CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1329 ctl_and CTL.NONSTRICT
label_pred
1330 (make_raw_match label
false ast
),
1331 ctl_and CTL.NONSTRICT
prelabel_pred rest_metamatch
))
1333 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1334 let stmt_fvs = Ast.get_fvs stmt
in
1335 let fvs = get_unquantified quantified
stmt_fvs in
1336 quantify guard
(label_var::fvs)
1337 (sequencibility body label_pred process_bef_aft seqible
)
1339 (* --------------------------------------------------------------------- *)
1340 (* dots and nests *)
1342 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1343 let matchgoto = gotopred None
in
1345 make_match None
false
1347 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1349 make_match None
false
1351 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1352 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1354 if quantifier
= Exists
1355 then Common.Left
(CTL.False
)
1357 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1359 then Common.Left
(aftpred label
)
1362 (function vx
-> function v ->
1363 (* vx is the contents of the nest, if any. we can only stop early
1364 if we find neither the ending code nor the nest contents in
1365 the if branch. not sure if this is a good idea. *)
1366 let lv = get_label_ctr() in
1367 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1368 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1370 (* Rather a special case. But if the code afterwards is just
1371 a } then there is no point checking after a goto that it does
1373 (* this optimization doesn't work. probably depends on whether
1374 the destination of the break/goto is local or more global than
1376 match seq_after
with
1378 let is_paren = function
1379 CTL.Pred
(Lib_engine.Paren _
,_
) -> true
1381 is_paren e1
or is_paren e2
1383 ctl_or (aftpred label
)
1384 (quantify false [lv]
1385 (ctl_and CTL.NONSTRICT
1386 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1388 (ctl_and CTL.NONSTRICT
(ctl_not v)
1389 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1390 (ctl_and CTL.NONSTRICT
preflabelpred
1391 (if !Flag_matcher.only_return_is_error_exit
1393 (ctl_and CTL.NONSTRICT
1394 (retpred None
) (ctl_not seq_after
))
1397 (ctl_and CTL.NONSTRICT
1398 (ctl_or (retpred None
) matchcontinue)
1399 (ctl_not seq_after
))
1400 (ctl_and CTL.NONSTRICT
1401 (ctl_or matchgoto matchbreak)
1403 (* an optim that failed see defn is_paren
1404 and tests/makes_a_loop *)
1408 (ctl_not seq_after
))))))))))) in
1409 let v = get_let_ctr() in
1411 (match stop_early with
1412 Common.Left x1
-> ctl_or y x1
1413 | Common.Right
stop_early ->
1416 (ctl_and CTL.NONSTRICT
(label_pred_maker label
)
1417 (stop_early n
(CTL.Ref
v)))))
1419 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1420 process_bef_aft statement_list statement guard quantified wrapcode
=
1421 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1422 (* proces bef_aft *)
1424 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1425 let bef_aft = (* to be negated *)
1429 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1432 with Not_found
-> shortest (Common.union_set bef aft
) in
1435 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1437 let check_quantifier quant other
=
1439 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1443 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1445 then failwith
"inconsistent annotation on dots"
1449 if check_quantifier Ast.WhenExists
Ast.WhenForall
1452 if check_quantifier Ast.WhenForall
Ast.WhenExists
1455 (* the following is used when we find a goto, etc and consider accepting
1456 without finding the rest of the pattern *)
1457 let aft = shortest aft in
1458 (* process whencode *)
1459 let labelled = label_pred_maker label
in
1461 let (poswhen
,negwhen
) =
1463 (function (poswhen
,negwhen
) ->
1465 Ast.WhenNot
whencodes ->
1466 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1467 | Ast.WhenAlways stm
->
1468 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1469 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1470 | Ast.WhenNotTrue
(e
) ->
1472 ctl_or (whencond_true e label guard quantified
) negwhen
)
1473 | Ast.WhenNotFalse
(e
) ->
1475 ctl_or (whencond_false e label guard quantified
) negwhen
))
1476 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1477 (*bef_aft modifies arg so that inside of a nest can't cause the next
1478 to overshoot its boundaries, eg a() <...f()...> b() where f is
1479 a metavariable and the whole thing matches code in a loop;
1480 don't want f to match eg b(), allowing to go around the loop again*)
1481 let poswhen = ctl_and_ns arg
poswhen in
1485 (* add in After, because it's not part of the program *)
1486 ctl_or (aftpred label
) negwhen
1488 ctl_and_ns poswhen (ctl_not negwhen) in
1489 (* process dot code, if any *)
1491 match (dotcode,guard
) with
1492 (None
,_) | (_,true) -> CTL.True
1493 | (Some
dotcode,_) -> dotcode in
1494 (* process nest code, if any *)
1495 (* whencode goes in the negated part of the nest; if no nest, just goes
1496 on the "true" in between code *)
1497 let plus_var = if plus
then get_label_ctr() else string2var "" in
1498 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1499 let (ornest
,just_nest
) =
1500 (* just_nest is used when considering whether to stop early, to continue
1501 to collect nest information in the if branch *)
1502 match (nest
,guard
&& not plus
) with
1503 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1504 | (Some nest
,false) ->
1505 let v = get_let_ctr() in
1509 (* the idea is that BindGood is sort of a witness; a witness to
1510 having found the subterm in at least one place. If there is
1511 not a witness, then there is a risk that it will get thrown
1512 away, if it is merged with a node that has an empty
1513 environment. See tests/nestplus. But this all seems
1514 rather suspicious *)
1515 CTL.And
(CTL.NONSTRICT
,x
,
1516 CTL.Exists
(true,plus_var2,
1517 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1518 CTL.Modif
plus_var2)))
1522 CTL.Or
(is_plus (CTL.Ref
v),
1523 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1525 let plus_modifier x
=
1532 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1537 (* label within dots is taken care of elsewhere. the next two lines
1538 put the label on the code following dots *)
1539 After f
-> ctl_and (guard_to_strict guard
) f
labelled
1541 (* actually, label should be None based on the only use of Guard... *)
1542 assert (label
= None
);
1543 ctl_and CTL.NONSTRICT
(ctl_uncheck f
) labelled
1545 let exit = endpred label
in
1546 let errorexit = exitpred label
in
1547 ctl_or exit errorexit
1548 (* not at all sure what the next two mean... *)
1552 Some
(lv,used) -> used := true;
1553 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1554 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1555 | None
-> endpred label
)
1556 (* was the following, but not clear why sgrep should allow
1558 let exit = endpred label in
1559 let errorexit = exitpred label in
1561 then ctl_or exit errorexit (* end anywhere *)
1562 else exit (* end at the real end of the function *) *)
in
1564 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1565 label
(guard_to_strict guard
) wrapcode just_nest
1567 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1568 aft ender quantifier)
1570 and get_whencond_exps e
=
1571 match Ast.unwrap e
with
1573 | Ast.DisjRuleElem
(res) ->
1574 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1575 | _ -> failwith
"not possible"
1577 and make_whencond_headers e e1 label guard quantified
=
1578 let fvs = Ast.get_fvs e
in
1580 quantify guard
(get_unquantified quantified
fvs)
1581 (make_match label guard h
) in
1586 (Ast.make_mcode
"if",
1587 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1588 let while_header e1
=
1592 (Ast.make_mcode
"while",
1593 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1598 (Ast.make_mcode
"for",Ast.make_mcode
"(",
1599 Ast.ForExp
(None
,Ast.make_mcode
";"),
1600 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1602 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1604 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1606 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1607 (if_headers, while_headers, for_headers)
1609 and whencond_true e label guard quantified
=
1610 let e1 = get_whencond_exps e
in
1611 let (if_headers, while_headers, for_headers) =
1612 make_whencond_headers e
e1 label guard quantified
in
1614 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1615 (ctl_and CTL.NONSTRICT
1616 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1618 and whencond_false e label guard quantified
=
1619 let e1 = get_whencond_exps e
in
1620 let (if_headers, while_headers, for_headers) =
1621 make_whencond_headers e
e1 label guard quantified
in
1623 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1624 (* if without else *)
1625 (ctl_or (ctl_and CTL.NONSTRICT
(fallpred label
) (ctl_back_ex if_headers))
1626 (* failure of loop test *)
1627 (ctl_and CTL.NONSTRICT
(loopfallpred label
)
1628 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1630 (* --------------------------------------------------------------------- *)
1631 (* the main translation loop *)
1633 let rec statement_list stmt_list top after quantified minus_quantified
1634 label llabel slabel dots_before guard
=
1636 (* include Disj to be on the safe side *)
1637 match Ast.unwrap x
with
1638 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1639 let compute_label l e db
= if db
or isdots e
then l else None
in
1640 match Ast.unwrap stmt_list
with
1642 let rec loop top quantified minus_quantified dots_before
1645 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1647 statement e top after quantified minus_quantified
1648 (compute_label label e dots_before
)
1650 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1651 let shared = intersectll fv
fvs in
1652 let unqshared = get_unquantified quantified
shared in
1653 let new_quantified = Common.union_set
unqshared quantified
in
1654 let minus_shared = intersectll mfv mfvs
in
1656 get_unquantified minus_quantified
minus_shared in
1657 let new_mquantified =
1658 Common.union_set
munqshared minus_quantified
in
1659 quantify guard
unqshared
1662 (let (label1
,llabel1
,slabel1
) =
1663 match Ast.unwrap e
with
1665 (match Ast.unwrap re
with
1666 Ast.Goto
_ -> (None
,None
,None
)
1667 | _ -> (label
,llabel
,slabel
))
1668 | _ -> (label
,llabel
,slabel
) in
1669 loop NotTop
new_quantified new_mquantified (isdots e
)
1670 label1 llabel1 slabel1
1672 new_quantified new_mquantified
1673 (compute_label label e dots_before
) llabel slabel guard
)
1674 | _ -> failwith
"not possible" in
1675 loop top quantified minus_quantified dots_before
1677 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1678 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1679 | Ast.STARS
(x
) -> failwith
"not supported"
1681 (* llabel is the label of the enclosing loop and slabel is the label of the
1683 and statement stmt top after quantified minus_quantified
1684 label llabel slabel guard
=
1685 let ctl_au = ctl_au CTL.NONSTRICT
in
1686 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1687 let ctl_and = ctl_and CTL.NONSTRICT
in
1688 let make_seq = make_seq guard
in
1689 let make_seq_after = make_seq_after guard
in
1690 let real_make_match = make_match in
1691 let make_match = header_match label guard
in
1693 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1696 match Ast.unwrap stmt
with
1698 (match Ast.unwrap ast
with
1699 (* the following optimisation is not a good idea, because when S
1700 is alone, we would like it not to match a declaration.
1701 this makes more matching for things like when (...) S, but perhaps
1702 that matching is not so costly anyway *)
1703 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1704 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_,_)) as d),_),
1706 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_,_)) as d),_),
1708 svar_context_with_add_after stmt
s label quantified
d ast seqible
1710 (process_bef_aft quantified minus_quantified
1711 label llabel slabel
true)
1713 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1715 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1716 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1718 (process_bef_aft quantified minus_quantified
1719 label llabel slabel
true)
1721 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1725 match Ast.unwrap ast
with
1726 Ast.DisjRuleElem
(res) ->
1727 do_re_matches label guard
res quantified minus_quantified
1728 | Ast.Exp
(_) | Ast.Ty
(_) ->
1729 let stmt_fvs = Ast.get_fvs stmt
in
1730 let fvs = get_unquantified quantified
stmt_fvs in
1731 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1733 let stmt_fvs = Ast.get_fvs stmt
in
1734 let fvs = get_unquantified quantified
stmt_fvs in
1735 quantify guard
fvs (make_match ast
) in
1736 match Ast.unwrap ast
with
1737 Ast.Break
(brk
,semi
) ->
1738 (match (llabel
,slabel
) with
1739 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1740 ctl_and term (bclabel_pred_maker slabel
)
1741 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1742 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1743 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1744 (* discard pattern that comes after return *)
1745 let normal_res = make_seq_after term after
in
1746 (* the following code tries to propagate the modifications on
1747 return; to a close brace, in the case where the final return
1750 match (retmc
,semmc
) with
1751 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1752 when !Flag.sgrep_mode2
->
1753 (* in sgrep mode, we can propagate the - *)
1756 (Ast.NOREPLACEMENT
,Ast.NOREPLACEMENT
) ->
1759 failwith
"no replacements allowed in sgrep mode" in
1760 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,new_info))
1761 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
)) ->
1764 (Ast.NOREPLACEMENT
,Ast.NOREPLACEMENT
) ->
1766 | (Ast.NOREPLACEMENT
,Ast.REPLACEMENT
(l,ct
))
1767 | (Ast.REPLACEMENT
(l,ct
),Ast.NOREPLACEMENT
) ->
1769 | (Ast.REPLACEMENT
(l1
,ct1
),Ast.REPLACEMENT
(l2
,ct2
)) ->
1770 Ast.BEFORE
(l1
@l2
,Ast.lub_count ct1 ct2
) in
1771 Some
(Ast.CONTEXT
(Ast.NoPos
,change))
1772 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
,c1
)),
1773 Ast.CONTEXT
(_,Ast.AFTER
(l2
,c2
))) ->
1775 (Ast.CONTEXT
(Ast.NoPos
,
1776 Ast.BEFORE
(l1
@l2
,Ast.lub_count c1 c2
)))
1777 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1778 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1780 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1781 Ast.CONTEXT
(_,Ast.AFTER
(l,c
))) ->
1782 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l,c
)))
1784 let ret = Ast.make_mcode
"return" in
1786 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1787 let semi = Ast.make_mcode
";" in
1789 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1791 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1794 let exit = endpred None
in
1796 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1797 let stripped_rbrace =
1798 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1800 (ctl_and (make_match mod_rbrace)
1803 (make_match stripped_rbrace)
1804 (* error exit not possible; it is in the middle
1805 of code, so a return is needed *)
1807 (* worry about perf, but seems correct, not ax *)
1811 (ctl_or simple_return return_expr))))))
1813 (* some change in the middle of the return, so have to
1814 find an actual return *)
1817 (* should try to deal with the dots_bef_aft problem elsewhere,
1818 but don't have the courage... *)
1823 do_between_dots stmt
term End
1824 quantified minus_quantified label llabel slabel guard
in
1826 make_seq_after term after
)
1827 | Ast.Seq
(lbrace
,body,rbrace
) ->
1828 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1831 [Ast.get_fvs lbrace
;Ast.get_fvs
body;Ast.get_fvs rbrace
]
1833 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] -> (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1834 | _ -> failwith
"not possible" in
1835 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1837 seq_fvs minus_quantified
1838 [Ast.get_mfvs lbrace
;Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1840 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1841 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1842 | _ -> failwith
"not possible" in
1843 let pv = count_nested_braces stmt
in
1844 let lv = get_label_ctr() in
1845 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1846 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1849 (quantify guard lbfvs
(make_match lbrace
))
1850 (ctl_and paren_pred label_pred) in
1852 match Ast.unwrap rbrace
with
1853 Ast.SeqEnd
((data
,info,_,pos)) ->
1854 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1855 | _ -> failwith
"unexpected close brace" in
1857 (* label is not needed; paren_pred is enough *)
1858 quantify guard rbfvs
1859 (ctl_au (make_match empty_rbrace)
1860 (ctl_and (real_make_match None guard rbrace
) paren_pred)) in
1861 let new_quantified2 =
1862 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1863 let new_mquantified2 =
1864 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1865 let pattern_as_given =
1866 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1867 quantify true [pv;lv]
1868 (quantify guard b1fvs
1872 (if !exists = Exists
then CTL.False
else (aftpred label
))
1873 (quantify guard b2fvs
1874 (statement_list body NotTop
1875 (After
(make_seq_after end_brace after
))
1876 new_quantified2 new_mquantified2
1877 (Some
(lv,ref true))
1878 llabel slabel
false guard
)))])) in
1880 match Ast.undots
body with
1882 (match Ast.unwrap
body with
1884 ((_,i
,Ast.CONTEXT
(_,Ast.NOTHING
),_),[],_,_) ->
1885 (match Ast.unwrap rbrace
with
1886 Ast.SeqEnd
((_,_,Ast.CONTEXT
(_,Ast.NOTHING
),_))
1887 when not
(contains_pos rbrace
) -> true
1891 if empty_body && List.mem after
[Tail
;End
;VeryEnd
]
1892 (* for just a match of an if branch of the form { ... }, just
1893 match the first brace *)
1894 then quantify guard lbfvs
(make_match lbrace
)
1895 else if ends_in_return body
1897 (* matching error handling code *)
1899 1. The pattern as given
1900 2. A goto, and then some close braces, and then the pattern as
1901 given, but without the braces (only possible if there are no
1902 decls, and open and close braces are unmodified)
1903 3. Part of the pattern as given, then a goto, and then the rest
1904 of the pattern. For this case, we just check that all paths have
1905 a goto within the current braces. checking for a goto at every
1906 point in the pattern seems expensive and not worthwhile. *)
1908 let body = preprocess_dots body in (* redo, to drop braces *)
1912 (make_match empty_rbrace)
1913 (ctl_ax (* skip the destination label *)
1914 (quantify guard b2fvs
1915 (statement_list body NotTop End
1916 new_quantified2 new_mquantified2 None llabel slabel
1919 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1920 quantify true [pv;lv]
1921 (quantify guard b1fvs
1925 (CTL.AU
(* want AF even for sgrep *)
1926 (CTL.FORWARD
,CTL.STRICT
,
1927 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1928 ctl_and (* brace must be eventually after goto *)
1929 (gotopred (Some
(lv,ref true)))
1930 (* want AF even for sgrep *)
1931 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1932 (quantify guard b2fvs
1933 (statement_list body NotTop Tail
1934 new_quantified2 new_mquantified2
1935 None
(*no label because past the goto*)
1936 llabel slabel
false guard
))])) in
1937 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1938 else pattern_as_given
1939 | Ast.IfThen
(ifheader
,branch
,aft) ->
1940 ifthen ifheader branch
aft after quantified minus_quantified
1941 label llabel slabel statement
make_match guard
1943 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1944 ifthenelse ifheader branch1 els branch2
aft after quantified
1945 minus_quantified label llabel slabel statement
make_match guard
1947 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1948 | Ast.Iterator
(header,body,aft) ->
1949 forwhile header body aft after quantified minus_quantified
1950 label statement
make_match guard
1952 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1953 (*ctl_and seems pointless, disjuncts see label too
1954 (label_pred_maker label)*)
1958 statement_list sl top after quantified minus_quantified label
1959 llabel slabel
true guard
)
1961 let safe_subformulas =
1963 Top
-> List.map2 protect_top_level stmt_dots_list
subformulas
1964 | NotTop
-> subformulas in
1965 List.fold_left
ctl_seqor CTL.False
safe_subformulas
1967 | Ast.Nest
(starter
,stmt_dots
,ender,whencode
,multi
,bef
,aft) ->
1968 (* label in recursive call is None because label check is already
1969 wrapped around the corresponding code. not good enough, want to stay
1970 in a specific region, dots and nests will keep going *)
1973 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1975 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1976 | _ -> failwith
"not possible" in
1978 (* no minus version because when code doesn't contain any minus code *)
1979 let new_quantified = Common.union_set
bfvs quantified
in
1982 match Ast.get_mcodekind starter
with (*ender must have the same mcode*)
1983 Ast.MINUS
(_,_,_,_) as d ->
1984 (* no need for the fresh metavar, but ... is a bit weird as a
1986 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1991 statement_list stmt_dots top
(a2n after
)
1992 new_quantified minus_quantified
1993 label
(*None*) llabel slabel
true guard
in
1994 dots_and_nests multi
1995 (Some
dots_pattern) whencode bef
aft dot_code after label
1996 (process_bef_aft
new_quantified minus_quantified
1997 label
(*None*) llabel slabel
true)
1998 (function x
-> (* for when code *)
1999 statement_list x NotTop Tail
2000 new_quantified minus_quantified label
(*None*)
2001 llabel slabel
true true)
2002 (function x
-> (* for when code *)
2003 statement x NotTop Tail
2004 new_quantified minus_quantified label
(*None*)
2007 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
2009 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
2012 Ast.MINUS
(_,_,_,_) ->
2013 (* no need for the fresh metavar, but ... is a bit weird as a
2015 Some
(make_match (make_meta_rule_elem d ([],[],[])))
2017 dots_and_nests false None
whencodes bef
aft dot_code after label
2018 (process_bef_aft quantified minus_quantified None llabel slabel
true)
2020 statement_list x NotTop Tail quantified minus_quantified
2021 None llabel slabel
true true)
2023 statement x NotTop Tail quantified minus_quantified
2024 None llabel slabel
true)
2026 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
2028 | Ast.Switch
(header,lb
,decls
,cases,rb
) ->
2029 let rec intersect_all = function
2032 | x
::xs -> intersect x
(intersect_all xs) in
2033 let rec intersect_all2 = function (* pairwise *)
2038 (function elem
-> List.exists (List.mem elem
) xs)
2040 Common.union_set
front (intersect_all2 xs) in
2041 let rec union_all l = List.fold_left
union [] l in
2042 (* start normal variables *)
2043 let header_fvs = Ast.get_fvs
header in
2044 let lb_fvs = Ast.get_fvs lb
in
2045 let decl_fvs = union_all (List.map
Ast.get_fvs
(Ast.undots decls
)) in
2046 let case_fvs = List.map
Ast.get_fvs
cases in
2047 let rb_fvs = Ast.get_fvs rb
in
2048 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2049 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2051 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2052 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2053 function case_fvs ->
2054 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
2055 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
2056 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
2057 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
2059 | _ -> failwith
"not possible")
2060 ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
2061 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2062 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2063 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
2064 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
2065 List.rev all_rbfvs
) in
2066 let exponlyfvs = intersect_all all_efvs
in
2067 let lbonlyfvs = intersect_all all_lbfvs
in
2068 (* don't do anything with right brace. Hope there is no + code on it *)
2069 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2070 let b1fvs = union_all all_b1fvs
in
2071 let new1_quantified = union b1fvs quantified
in
2073 union (union_all all_b2fvs
) (intersect_all2 all_casefvs
) in
2074 let new2_quantified = union b2fvs new1_quantified in
2075 (* let b3fvs = union_all all_b3fvs in*)
2076 (* ------------------- start minus free variables *)
2077 let header_mfvs = Ast.get_mfvs
header in
2078 let lb_mfvs = Ast.get_mfvs lb
in
2079 let decl_mfvs = union_all (List.map
Ast.get_mfvs
(Ast.undots decls
)) in
2080 let case_mfvs = List.map
Ast.get_mfvs
cases in
2081 let rb_mfvs = Ast.get_mfvs rb
in
2082 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2083 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2085 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2086 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2087 function case_mfvs ->
2090 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
2091 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
2092 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
2093 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
2095 | _ -> failwith
"not possible")
2096 ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
2097 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2098 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2099 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
2100 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
2101 List.rev all_mrbfvs
) in
2102 (* don't do anything with right brace. Hope there is no + code on it *)
2103 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2104 let mb1fvs = union_all all_mb1fvs
in
2105 let new1_mquantified = union mb1fvs quantified
in
2107 union (union_all all_mb2fvs
) (intersect_all2 all_mcasefvs
) in
2108 let new2_mquantified = union mb2fvs new1_mquantified in
2109 (* let b3fvs = union_all all_b3fvs in*)
2110 (* ------------------- end collection of free variables *)
2111 let switch_header = quantify guard
exponlyfvs (make_match header) in
2112 let lb = quantify guard
lbonlyfvs (make_match lb) in
2113 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
2116 (function case_line
->
2117 match Ast.unwrap case_line
with
2118 Ast.CaseLine
(header,body) ->
2120 match seq_fvs new2_quantified [Ast.get_fvs
header] with
2121 [(e1fvs,_)] -> e1fvs
2122 | _ -> failwith
"not possible" in
2123 quantify guard
e1fvs (real_make_match label
true header)
2124 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2126 let lv = get_label_ctr() in
2127 let used = ref false in
2128 let (decls_exists_code
,decls_all_code
) =
2129 (*don't really understand this*)
2130 if (Ast.undots decls
) = []
2131 then (CTL.True
,CTL.False
)
2134 statement_list decls NotTop Tail
2135 new2_quantified new2_mquantified (Some
(lv,used)) llabel None
2140 (List.fold_left
ctl_or_fl CTL.False
2141 (List.map
ctl_uncheck
2142 (decls_all_code
::case_headers))) in
2145 (function case_line
->
2146 match Ast.unwrap case_line
with
2147 Ast.CaseLine
(header,body) ->
2148 let (e1fvs,b1fvs,s1fvs
) =
2149 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
2150 match seq_fvs new2_quantified fvs with
2151 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2152 | _ -> failwith
"not possible" in
2153 let (me1fvs
,mb1fvs,ms1fvs
) =
2154 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
2155 match seq_fvs new2_mquantified fvs with
2156 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2157 | _ -> failwith
"not possible" in
2159 quantify guard
e1fvs (make_match header) in
2160 let new3_quantified = union b1fvs new2_quantified in
2161 let new3_mquantified = union mb1fvs new2_mquantified in
2163 statement_list body NotTop Tail
2164 new3_quantified new3_mquantified (Some
(lv,used)) llabel
2165 (Some
(lv,used)) false(*?*) guard
in
2166 quantify guard
b1fvs (make_seq [case_header; body])
2167 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2169 let default_required =
2172 match Ast.unwrap case
with
2173 Ast.CaseLine
(header,_) ->
2174 (match Ast.unwrap
header with
2175 Ast.Default
(_,_) -> true
2179 then function x
-> x
2180 else function x
-> ctl_or (fallpred label
) x
in
2181 let after_pred = aftpred label
in
2182 let body after_branch
=
2185 (quantify guard
b2fvs
2188 (List.fold_left
ctl_and CTL.True
2190 (decls_exists_code
:: case_headers)));
2191 List.fold_left
ctl_or_fl no_header
2192 (decls_all_code
:: case_code)])))
2195 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2196 match Ast.unwrap
rb with
2197 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2198 | _ -> failwith
"not possible") in
2199 let (switch_header,wrapper
) =
2202 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2203 (ctl_and switch_header label_pred,
2204 (function body -> quantify true [lv] body))
2205 else (switch_header,function x
-> x
) in
2207 (end_control_structure b1fvs switch_header body
2208 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2209 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2210 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2213 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2214 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2216 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2217 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2218 | _ -> failwith
"not possible" in
2219 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2222 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2223 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2225 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2226 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2227 | _ -> failwith
"not possible" in
2228 let function_header = quantify guard hfvs
(make_match header) in
2229 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2230 let stripped_rbrace =
2231 match Ast.unwrap rbrace
with
2232 Ast.SeqEnd
((data
,info,_,_)) ->
2233 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2234 | _ -> failwith
"unexpected close brace" in
2236 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2237 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2238 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2240 (quantify guard rbfvs
(make_match rbrace
))
2242 (* the following finds the beginning of the fake braces,
2243 if there are any, not completely sure how this works.
2244 sse the examples sw and return *)
2245 (ctl_back_ex (ctl_not fake_brace))
2246 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2247 let new_quantified3 =
2248 Common.union_set
b1fvs
2249 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2250 let new_mquantified3 =
2251 Common.union_set
mb1fvs
2252 (Common.union_set
mb2fvs
2253 (Common.union_set mb3fvs minus_quantified
)) in
2254 let not_minus = function Ast.MINUS
(_,_,_,_) -> false | _ -> true in
2256 match (Ast.undots
body,
2257 contains_modif rbrace
or contains_pos rbrace
) with
2259 (match Ast.unwrap
body with
2260 Ast.Nest
(starter
,stmt_dots
,ender,[],false,_,_)
2261 (* perhaps could optimize for minus case too... TODO *)
2262 when not_minus (Ast.get_mcodekind starter
)
2264 (* special case for function header + body - header is unambiguous
2265 and unique, so we can just look for the nested body anywhere
2269 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2270 statement_list stmt_dots NotTop
2271 (* discards match on right brace, but don't need it *)
2272 (Guard
(make_seq_after end_brace after
))
2273 new_quantified3 new_mquantified3
2274 None llabel slabel
true guard
))
2275 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2277 (* flow sensitive, so not optimizable *)
2278 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2280 | _ -> true) whencode
) ->
2281 (* try to be more efficient for the case where the body is just
2282 ... Perhaps this is too much of a special case, but useful
2283 for dropping a parameter and checking that it is never used. *)
2285 Ast.MINUS
(_,_,_,_) -> None
2288 (* no nested braces, because only dots *)
2289 string2var ("p1") in
2291 CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
2294 [ctl_and start_brace paren_pred;
2304 Ast.WhenAlways
(s) -> prev
2305 | Ast.WhenNot
(sl
) ->
2314 | Ast.WhenNotTrue
(_)
2315 | Ast.WhenNotFalse
(_) ->
2316 failwith
"unexpected"
2318 (Ast.WhenAny
) -> CTL.False
2319 | Ast.WhenModifier
(_) -> prev
)
2320 CTL.False whencode
))
2324 Ast.WhenAlways
(s) ->
2326 statement
s NotTop Tail
2329 label llabel slabel
true in
2331 | Ast.WhenNot
(sl
) -> prev
2332 | Ast.WhenNotTrue
(_)
2333 | Ast.WhenNotFalse
(_) ->
2334 failwith
"unexpected"
2335 | Ast.WhenModifier
(Ast.WhenAny
) ->
2337 | Ast.WhenModifier
(_) -> prev
)
2338 CTL.True whencode
) in
2341 (make_match stripped_rbrace)
2346 (* function body is all minus, no whencode *)
2347 match Ast.undots
body with
2349 (match Ast.unwrap
body with
2351 ((_,i
,(Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
) as d),_),[],_,_) ->
2352 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2353 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),_)),
2354 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),_)))
2355 when not
(contains_pos rbrace
) ->
2357 (* andany drops everything to the end, including close
2358 braces - not just function body, could check
2359 label to keep braces *)
2360 (ctl_and start_brace
2363 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2365 (make_meta_rule_elem d ([],[],[]))))))
2370 match (optim1,optim2) with
2376 quantify guard
b3fvs
2377 (statement_list body NotTop
2378 (After
(make_seq_after end_brace after
))
2379 new_quantified3 new_mquantified3 None llabel slabel
2381 quantify guard
b1fvs
2382 (make_seq [function_header; quantify guard
b2fvs body_code])
2383 | Ast.Define
(header,body) ->
2384 let (hfvs
,bfvs,bodyfvs
) =
2385 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2387 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2388 | _ -> failwith
"not possible" in
2389 let (mhfvs
,mbfvs
,mbodyfvs
) =
2390 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2392 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2393 | _ -> failwith
"not possible" in
2394 let define_header = quantify guard hfvs
(make_match header) in
2396 statement_list body NotTop after
2397 (Common.union_set
bfvs quantified
)
2398 (Common.union_set mbfvs minus_quantified
)
2399 None llabel slabel
true guard
in
2400 quantify guard
bfvs (make_seq [define_header; body_code])
2401 | Ast.AsStmt
(stmt
,asstmt
) ->
2403 (statement stmt top after quantified minus_quantified
2404 label llabel slabel guard
)
2405 (statement asstmt top after quantified minus_quantified
2406 label llabel slabel guard
)
2407 | Ast.OptStm
(stm
) ->
2408 failwith
"OptStm should have been compiled away\n"
2409 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2410 | _ -> failwith
"not supported" in
2411 if guard
or !dots_done
2414 do_between_dots stmt
term after quantified minus_quantified
2415 label llabel slabel guard
2417 (* term is the translation of stmt *)
2418 and do_between_dots stmt
term after quantified minus_quantified
2419 label llabel slabel guard
=
2420 match Ast.get_dots_bef_aft stmt
with
2421 Ast.AddingBetweenDots
(brace_term
,n
)
2422 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2424 statement brace_term NotTop after quantified minus_quantified
2425 label llabel slabel guard
in
2426 let v = Printf.sprintf
"_r_%d" n
in
2427 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2428 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2431 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2432 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2434 | Ast.NoDots
-> term
2436 (* un_process_bef_aft is because we don't want to do transformation in this
2437 code, and thus don't case about braces before or after it *)
2438 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2440 Ast.WParen
(re
,n
) ->
2441 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2442 let s = guard_to_strict guard
in
2443 quantify true (get_unquantified quantified
[n
])
2444 (ctl_and s (make_raw_match None guard re
) paren_pred)
2446 statement
s NotTop Tail quantified minus_quantified
2447 label llabel slabel guard
2448 | Ast.Other_dots
d ->
2449 statement_list d NotTop Tail quantified minus_quantified
2450 label llabel slabel
true guard
2452 and protect_top_level stmt_dots formula
=
2453 let starts_with_dots =
2454 match Ast.undots stmt_dots
with
2456 (match Ast.unwrap
d with
2457 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2458 | Ast.Stars
(_,_,_,_) -> true
2461 let starts_with_non_context_brace =
2463 Some false = OK except on function braces
2464 Some true = Never OK *)
2465 match Ast.undots stmt_dots
with
2467 (match Ast.unwrap
d with
2468 Ast.Seq
(before
,body,after
) ->
2470 match Ast.unwrap before
with
2471 Ast.SeqStart
(obr
) -> Ast.get_mcodekind obr
2472 | _ -> failwith
"bad seq" in
2474 match Ast.unwrap after
with
2475 Ast.SeqEnd
(cbr
) -> Ast.get_mcodekind cbr
2476 | _ -> failwith
"bad seq"in
2477 (match (beforemc,aftermc) with
2479 (Ast.CONTEXT
(_,(Ast.NOTHING
|Ast.AFTER
_)),
2480 Ast.CONTEXT
(_,(Ast.NOTHING
|Ast.BEFORE
_))) -> None
2481 | (Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),
2482 Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
))
2483 when List.length
(Ast.undots
body) = 1 -> Some
false (*ok on if*)
2484 (* unsafe, can't be allowed to match fn top *)
2489 then (* EX because there is a loop on enter/top *)
2490 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex formula
)
2492 match starts_with_non_context_brace with
2495 ctl_and CTL.NONSTRICT
2496 (ctl_not(CTL.EX
(CTL.BACKWARD
,funpred None
)))
2499 ctl_and CTL.NONSTRICT
2500 (ctl_not(CTL.EX
(CTL.BACKWARD
,unsbrpred None
)))
2504 (* --------------------------------------------------------------------- *)
2505 (* cleanup: convert AX to EX for pdots.
2506 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2507 This is what we wanted in the first place, but it wasn't possible to make
2508 because the AX and its argument are not created in the same place.
2510 (* also cleanup XX, which is a marker for the case where the programmer
2511 specifies to change the quantifier on .... Assumed to only occur after one AX
2512 or EX, or at top level. *)
2515 let c = match c with CTL.XX
(c) -> c | _ -> c in
2517 CTL.False
-> CTL.False
2518 | CTL.True
-> CTL.True
2519 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2520 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2521 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2522 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2523 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2524 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2525 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2526 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2527 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2528 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2529 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2530 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2531 | CTL.AX
(CTL.FORWARD
,s,
2533 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2534 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2536 CTL.And
(CTL.NONSTRICT
,
2537 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2538 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2539 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2540 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2541 CTL.AX
(dir
,s,cleanup phi
)
2542 | CTL.XX
(phi
) -> failwith
"bad XX"
2543 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2544 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2545 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2546 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2547 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2548 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2549 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2550 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2551 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2552 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2553 | CTL.Ref
(s) -> CTL.Ref
(s)
2554 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2555 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2557 (* --------------------------------------------------------------------- *)
2558 (* Function declaration *)
2560 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2562 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2563 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2565 saved := Ast.get_saved t
;
2566 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2567 let (wrap
,formula
) =
2568 match Ast.unwrap t
with
2569 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2570 | Ast.NONDECL
(stmt
) ->
2571 let unopt = elim_opt.V.rebuilder_statement stmt
in
2572 let unopt = preprocess_dots_e unopt in
2575 (statement
unopt Top VeryEnd
quantified [] None None None
false) in
2576 ((function x -> NONDECL
x), formula)
2577 | Ast.CODE
(stmt_dots
) ->
2578 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2579 let unopt = preprocess_dots unopt in
2581 statement_list unopt Top VeryEnd
quantified [] None None None
2583 let clean_formula = cleanup (protect_top_level stmt_dots
formula) in
2584 ((function x -> CODE
x), clean_formula)
2585 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords" in
2586 wrap
(quantify false quantified formula)
2588 (* --------------------------------------------------------------------- *)
2591 let asttoctlz (name
,(_,_,exists_flag
),l)
2592 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2595 (match exists_flag
with
2596 Ast.Exists
-> exists := Exists
2597 | Ast.Forall
-> exists := Forall
2598 | Ast.Undetermined
->
2599 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2601 let (l,used_after) =
2605 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2606 (List.combine
l (List.combine
used_after positions
))) in
2608 List.map2
(top_level name
)
2609 (List.combine
used_after fresh_used_after
)
2610 (List.combine fresh_used_after_seeds
l) in
2614 let asttoctl r
used_after positions
=
2616 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2617 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2618 asttoctlz (a,b
,c) used_after positions
2619 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CODE
CTL.True
]
2621 let pp_cocci_predicate (pred
,modif
) =
2622 Pretty_print_engine.pp_predicate pred
2624 let cocci_predicate_to_string (pred
,modif
) =
2625 Pretty_print_engine.predicate_to_string pred