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.
27 (* for MINUS and CONTEXT, pos is always None in this file *)
28 (*search for require*)
29 (* true = don't see all matched nodes, only modified ones *)
30 let onlyModif = ref true(*false*)
32 type ex
= Exists
| Forall
33 let exists = ref Forall
35 module Ast
= Ast_cocci
36 module V
= Visitor_ast
39 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
41 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
42 type formula
= Lib_engine.ctlcocci
43 type top_formula
= NONDECL
of Lib_engine.ctlcocci
| CODE
of Lib_engine.ctlcocci
45 let union = Common.union_set
46 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
47 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
49 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
51 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
53 let used_after = ref ([] : Ast.meta_name list
)
54 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
56 let saved = ref ([] : Ast.meta_name list
)
58 let string2var x
= ("",x
)
60 (* --------------------------------------------------------------------- *)
61 (* predicates matching various nodes in the graph *)
65 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
66 | (CTL.True
,a
) | (a
,CTL.True
) -> a
71 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
72 | (CTL.False
,a
) | (a
,CTL.False
) -> a
77 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
78 | (CTL.False
,a
) | (a
,CTL.False
) -> a
83 (* drop x or true case because x might have side effects *)
84 (CTL.True
,_
) (* | (_,CTL.True) *) -> CTL.True
85 | (CTL.False
,a
) | (a
,CTL.False
) -> a
88 let ctl_not = function
90 | CTL.False
-> CTL.True
93 let ctl_ax s
= function
95 | CTL.False
-> CTL.False
98 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
99 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
101 let ctl_ax_absolute s
= function
103 | CTL.False
-> CTL.False
104 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
106 let ctl_ex = function
108 | CTL.False
-> CTL.False
109 | x
-> CTL.EX
(CTL.FORWARD
,x
)
111 (* This stays being AX even for sgrep_mode, because it is used to identify
112 the structure of the term, not matching the pattern. *)
113 let ctl_back_ag = function
115 | CTL.False
-> CTL.False
116 | x
-> CTL.AG
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
118 let ctl_back_ax = function
120 | CTL.False
-> CTL.False
121 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
123 let ctl_back_ex = function
125 | CTL.False
-> CTL.False
126 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
128 let ctl_ef = function
130 | CTL.False
-> CTL.False
131 | x
-> CTL.EF
(CTL.FORWARD
,x
)
133 let ctl_ag s
= function
135 | CTL.False
-> CTL.False
136 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
139 match (x
,!exists) with
140 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
141 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
142 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
143 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
145 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
147 (match (x
,!exists) with
148 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
149 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
150 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
151 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
153 let ctl_uncheck = function
155 | CTL.False
-> CTL.False
158 let label_pred_maker = function
160 | Some
(label_var
,used
) ->
162 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
164 let bclabel_pred_maker = function
166 | Some
(label_var
,used
) ->
168 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
170 (* label used to be used here, but it is not used; label is only needed after
172 let predmaker guard pred label
= CTL.Pred pred
174 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
175 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
176 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
177 let unsbrpred = predmaker false (Lib_engine.UnsafeBrace
, CTL.Control
)
178 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
179 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
180 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
181 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
182 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
183 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
184 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
185 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
186 let loopfallpred = predmaker false (Lib_engine.LoopFallThrough
, CTL.Control
)
188 (*let aftret label_var =
189 ctl_or (aftpred label_var)
190 (ctl_or (loopfallpred label_var) (exitpred label_var))*)
196 Printf.sprintf
"r%d" cur
198 (* --------------------------------------------------------------------- *)
199 (* --------------------------------------------------------------------- *)
200 (* Eliminate OptStm *)
202 (* for optional thing with nothing after, should check that the optional thing
203 never occurs. otherwise the matching stops before it occurs *)
206 let donothing r k e
= k e
in
209 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
212 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
215 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
217 let inheritedlist l
=
218 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
221 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
224 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
226 let rec dots_list unwrapped wrapped
=
227 match (unwrapped
,wrapped
) with
230 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
232 | (Ast.Nest
(_
,_
,_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)
234 d0
::s
::d1
::rest
) -> (* why no case for nest as u? *)
235 let l = Ast.get_line stm
in
236 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
237 let new_rest2 = dots_list urest rest
in
238 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
239 varlists new_rest1 in
240 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
241 varlists new_rest2 in
245 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
247 Ast.free_vars
= fv_rest1
;
248 Ast.minus_free_vars
= mfv_rest1
;
249 Ast.fresh_vars
= fresh_rest1
;
250 Ast.inherited
= inherited_rest1
;
251 Ast.saved_witness
= s1
};
252 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
254 Ast.free_vars
= fv_rest2
;
255 Ast.minus_free_vars
= mfv_rest2
;
256 Ast.fresh_vars
= fresh_rest2
;
257 Ast.inherited
= inherited_rest2
;
258 Ast.saved_witness
= s2
}])) with
260 Ast.free_vars
= fv_rest1
;
261 Ast.minus_free_vars
= mfv_rest1
;
262 Ast.fresh_vars
= fresh_rest1
;
263 Ast.inherited
= inherited_rest1
;
264 Ast.saved_witness
= s1
}]
266 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
267 let l = Ast.get_line stm
in
268 let new_rest1 = dots_list urest rest
in
269 let new_rest2 = stm
::new_rest1 in
270 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
271 varlists new_rest1 in
272 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
273 varlists new_rest2 in
276 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
278 Ast.free_vars
= fv_rest2
;
279 Ast.minus_free_vars
= mfv_rest2
;
280 Ast.fresh_vars
= fresh_rest2
;
281 Ast.inherited
= inherited_rest2
;
282 Ast.saved_witness
= s2
};
283 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
285 Ast.free_vars
= fv_rest1
;
286 Ast.minus_free_vars
= mfv_rest1
;
287 Ast.fresh_vars
= fresh_rest1
;
288 Ast.inherited
= inherited_rest1
;
289 Ast.saved_witness
= s1
}])) with
291 Ast.free_vars
= fv_rest2
;
292 Ast.minus_free_vars
= mfv_rest2
;
293 Ast.fresh_vars
= fresh_rest2
;
294 Ast.inherited
= inherited_rest2
;
295 Ast.saved_witness
= s2
}]
297 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
298 let l = Ast.get_line stm
in
299 let fv_stm = Ast.get_fvs stm
in
300 let mfv_stm = Ast.get_mfvs stm
in
301 let fresh_stm = Ast.get_fresh stm
in
302 let inh_stm = Ast.get_inherited stm
in
303 let saved_stm = Ast.get_saved stm
in
304 let fv_d1 = Ast.get_fvs d1
in
305 let mfv_d1 = Ast.get_mfvs d1
in
306 let fresh_d1 = Ast.get_fresh d1
in
307 let inh_d1 = Ast.get_inherited d1
in
308 let saved_d1 = Ast.get_saved d1
in
309 let fv_both = Common.union_set
fv_stm fv_d1 in
310 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
311 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
312 let inh_both = Common.union_set
inh_stm inh_d1 in
313 let saved_both = Common.union_set
saved_stm saved_d1 in
317 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
319 Ast.free_vars
= fv_stm;
320 Ast.minus_free_vars
= mfv_stm;
321 Ast.fresh_vars
= fresh_stm;
322 Ast.inherited
= inh_stm;
323 Ast.saved_witness
= saved_stm};
324 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
326 Ast.free_vars
= fv_d1;
327 Ast.minus_free_vars
= mfv_d1;
328 Ast.fresh_vars
= fresh_d1;
329 Ast.inherited
= inh_d1;
330 Ast.saved_witness
= saved_d1}])) with
332 Ast.free_vars
= fv_both;
333 Ast.minus_free_vars
= mfv_both;
334 Ast.fresh_vars
= fresh_both;
335 Ast.inherited
= inh_both;
336 Ast.saved_witness
= saved_both}]
338 | ([Ast.Nest
(_
,_
,_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
339 let l = Ast.get_line stm
in
340 let rw = Ast.rewrap stm
in
341 let rwd = Ast.rewrap stm
in
342 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
344 [rwd(Ast.DOTS
([stm
]));
345 {(Ast.make_term
(Ast.DOTS
([rw dots])))
346 with Ast.node_line
= l}])]
348 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
349 | _
-> failwith
"not possible" in
351 let stmtdotsfn r k d
=
354 (match Ast.unwrap
d with
355 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
356 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
357 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
360 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
361 donothing donothing stmtdotsfn donothing donothing
362 donothing donothing donothing donothing donothing donothing donothing
363 donothing donothing donothing donothing donothing
365 (* --------------------------------------------------------------------- *)
366 (* after management *)
367 (* We need Guard for the following case:
376 Here the inner <... b ...> should not go past foo. But foo is not the
377 "after" of the body of the outer nest, because we don't want to search for
378 it in the case where the body of the outer nest ends in something other
379 than dots or a nest. *)
381 (* what is the difference between tail and end??? *)
383 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
385 type top
= Top
| NotTop
387 let a2n = function After x
-> Guard x
| a
-> a
390 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
391 let pp_meta (_
,x
) = Common.pp x
in
392 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
393 Format.print_newline
()
395 let print_after = function
396 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
397 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
398 | Tail
-> Printf.printf
"Tail\n"
399 | VeryEnd
-> Printf.printf
"Very End\n"
400 | End
-> Printf.printf
"End\n"
402 (* --------------------------------------------------------------------- *)
405 let fresh_var _
= string2var "_v"
406 let fresh_pos _
= string2var "_pos" (* must be a constant *)
408 let fresh_metavar _
= "_S"
410 (* fvinfo is going to end up being from the whole associated statement.
411 it would be better if it were just the free variables in d, but free_vars.ml
412 doesn't keep track of free variables on + code *)
413 let make_meta_rule_elem d fvinfo
=
414 let nm = fresh_metavar() in
415 Ast.make_meta_rule_elem nm d fvinfo
417 let get_unquantified quantified vars
=
418 List.filter
(function x
-> not
(List.mem x quantified
)) vars
420 let make_seq guard
l =
421 let s = guard_to_strict guard
in
422 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
424 let make_seq_after2 guard first rest
=
425 let s = guard_to_strict guard
in
427 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
430 let make_seq_after guard first rest
=
432 After rest
-> make_seq guard
[first
;rest
]
435 let opt_and guard first rest
=
436 let s = guard_to_strict guard
in
439 | Some first
-> ctl_and s first rest
441 let and_after guard first rest
=
442 let s = guard_to_strict guard
in
443 match rest
with After rest
-> ctl_and s first rest
| _
-> first
446 let bind x y
= x
or y
in
447 let option_default = false in
448 let mcode r
(_
,_
,kind
,metapos
) =
450 Ast.MINUS
(_
,_
,_
,_
) -> true
451 | Ast.PLUS _
-> failwith
"not possible"
452 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
453 let do_nothing r k e
= k e
in
454 let rule_elem r k re
=
456 match Ast.unwrap re
with
457 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
458 bind (mcode r
((),(),bef
,[])) res
459 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,[])) res
463 match Ast.unwrap i
with
464 Ast.StrInitList
(allminus
,_
,_
,_
,_
) -> allminus
or res
467 V.combiner
bind option_default
468 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
469 do_nothing do_nothing do_nothing do_nothing do_nothing
470 do_nothing do_nothing do_nothing do_nothing init do_nothing
471 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
472 recursor.V.combiner_rule_elem
475 let bind x y
= x
or y
in
476 let option_default = false in
477 let mcode r
(_
,_
,kind
,metapos
) = not
(metapos
= []) in
478 let do_nothing r k e
= k e
in
479 let rule_elem r k re
=
481 match Ast.unwrap re
with
482 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
483 bind (mcode r
((),(),bef
,[])) res
484 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,[])) res
487 V.combiner
bind option_default
488 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
489 do_nothing do_nothing do_nothing do_nothing do_nothing
490 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
491 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
492 recursor.V.combiner_rule_elem
494 (* code is not a DisjRuleElem *)
495 let make_match label guard code
=
496 let v = fresh_var() in
497 let matcher = Lib_engine.Match
(code
) in
498 if contains_modif code
&& not guard
499 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
501 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
502 (match (iso_info,!onlyModif,guard
,
503 intersect !used_after (Ast.get_fvs code
)) with
504 (false,true,_
,[]) | (_
,_
,true,_
) ->
505 predmaker guard
(matcher,CTL.Control
) label
506 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
508 let make_raw_match label guard code
=
509 match intersect !used_after (Ast.get_fvs code
) with
510 [] -> predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
512 let v = fresh_var() in
513 CTL.Exists
(true,v,predmaker guard
(Lib_engine.Match
(code
),CTL.UnModif
v)
516 let rec seq_fvs quantified
= function
519 let t1fvs = get_unquantified quantified fv1
in
521 List.fold_left
Common.union_set
[]
522 (List.map
(get_unquantified quantified
) fvs
) in
523 let bothfvs = Common.inter_set
t1fvs termfvs in
524 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
525 let new_quantified = Common.union_set
bothfvs quantified
in
526 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
531 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
533 let non_saved_quantify =
535 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
537 let intersectll lst nested_list
=
538 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
540 (* --------------------------------------------------------------------- *)
541 (* Count depth of braces. The translation of a closed brace appears deeply
542 nested within the translation of the sequence term, so the name of the
543 paren var has to take into account the names of the nested braces. On the
544 other hand the close brace does not escape, so we don't have to take into
545 account other paren variable names. *)
547 (* called repetitively, which is inefficient, but less trouble than adding a
548 new field to Seq and FunDecl *)
549 let count_nested_braces s =
550 let bind x y
= max x y
in
551 let option_default = 0 in
552 let stmt_count r k
s =
553 match Ast.unwrap
s with
554 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
556 let donothing r k e
= k e
in
558 let recursor = V.combiner
bind option_default
559 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
560 donothing donothing donothing donothing donothing
561 donothing donothing donothing donothing donothing donothing
562 donothing donothing stmt_count donothing donothing donothing in
563 let res = string_of_int
(recursor.V.combiner_statement
s) in
567 let get_label_ctr _
=
568 let cur = !labelctr in
570 string2var (Printf.sprintf
"l%d" cur)
572 (* --------------------------------------------------------------------- *)
573 (* annotate dots with before and after neighbors *)
575 let print_bef_aft = function
577 Printf.printf
"bef/aft\n";
578 Pretty_print_cocci.rule_elem "" re
;
579 Format.print_newline
()
581 Printf.printf
"bef/aft\n";
582 Pretty_print_cocci.statement
"" s;
583 Format.print_newline
()
584 | Ast.Other_dots
d ->
585 Printf.printf
"bef/aft\n";
586 Pretty_print_cocci.statement_dots
d;
587 Format.print_newline
()
589 (* [] can only occur if we are in a disj, where it comes from a ? In that
590 case, we want to use a, which accumulates all of the previous patterns in
592 let rec get_before_elem sl a
=
593 match Ast.unwrap sl
with
597 [] -> ([],Common.Right a
)
599 let (e
,ea
) = get_before_e e a
in
602 let (e
,ea
) = get_before_e e a
in
603 let (sl
,sla
) = loop sl ea
in
605 let (l,a
) = loop x a
in
606 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
607 | Ast.CIRCLES
(x
) -> failwith
"not supported"
608 | Ast.STARS
(x
) -> failwith
"not supported"
610 and get_before sl a
=
611 match get_before_elem sl a
with
612 (term
,Common.Left x
) -> (term
,x
)
613 | (term
,Common.Right x
) -> (term
,x
)
615 and get_before_whencode wc
=
618 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
619 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
620 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
621 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
622 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
625 and get_before_e
s a
=
626 match Ast.unwrap
s with
627 Ast.Dots
(d,w
,_
,aft
) ->
628 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
629 | Ast.Nest
(starter
,stmt_dots
,ender
,w
,multi
,_
,aft
) ->
630 let w = get_before_whencode
w in
631 let (sd
,_
) = get_before stmt_dots a
in
633 got rid of this, don't want to let nests overshoot
638 Unify_ast.unify_statement_dots
639 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
641 Unify_ast.MAYBE -> false
643 | Ast.Other_dots a ->
644 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
646 Unify_ast.MAYBE -> false
650 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,a,aft
)),
651 [Ast.Other_dots stmt_dots
])
652 | Ast.Disj
(stmt_dots_list
) ->
654 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
655 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
657 (match Ast.unwrap ast
with
658 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
659 | _
-> (s,[Ast.Other
s]))
660 | Ast.Seq
(lbrace
,body
,rbrace
) ->
661 let index = count_nested_braces s in
662 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
663 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
664 | Ast.Define
(header
,body
) ->
665 let (body
,_
) = get_before body
[] in
666 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
667 | Ast.AsStmt
(stmt
,asstmt
) ->
668 let (stmt
,_
) = get_before_e stmt
[] in
669 let (asstmt
,_
) = get_before_e asstmt
[] in
670 (Ast.rewrap
s (Ast.AsStmt
(stmt
,asstmt
)),[Ast.Other
s])
671 | Ast.IfThen
(ifheader
,branch
,aft
) ->
672 let (br
,_
) = get_before_e branch
[] in
673 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
674 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
675 let (br1
,_
) = get_before_e branch1
[] in
676 let (br2
,_
) = get_before_e branch2
[] in
677 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
678 | Ast.While
(header
,body
,aft
) ->
679 let (bd
,_
) = get_before_e body
[] in
680 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
681 | Ast.For
(header
,body
,aft
) ->
682 let (bd
,_
) = get_before_e body
[] in
683 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
684 | Ast.Do
(header
,body
,tail
) ->
685 let (bd
,_
) = get_before_e body
[] in
686 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
687 | Ast.Iterator
(header
,body
,aft
) ->
688 let (bd
,_
) = get_before_e body
[] in
689 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
690 | Ast.Switch
(header
,lb
,decls
,cases
,rb
) ->
691 let index = count_nested_braces s in
692 let (de
,dea
) = get_before decls
[Ast.WParen
(lb
,index)] in
695 (function case_line
->
696 match Ast.unwrap case_line
with
697 Ast.CaseLine
(header
,body
) ->
698 let (body
,_
) = get_before body
[] in
699 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
700 | Ast.OptCase
(case_line
) -> failwith
"not supported")
702 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),
703 [Ast.WParen
(rb
,index)])
704 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
705 let (bd
,_
) = get_before body
[] in
706 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
708 Pretty_print_cocci.statement
"" s; Format.print_newline
();
709 failwith
"get_before_e: not supported"
711 let rec get_after sl
a =
712 match Ast.unwrap sl
with
718 let (sl
,sla
) = loop sl
in
719 let (e
,ea
) = get_after_e e sla
in
721 let (l,a) = loop x
in
722 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
723 | Ast.CIRCLES
(x
) -> failwith
"not supported"
724 | Ast.STARS
(x
) -> failwith
"not supported"
726 and get_after_whencode
a wc
=
729 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
730 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
731 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
732 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
733 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
736 and get_after_e
s a =
737 match Ast.unwrap
s with
738 Ast.Dots
(d,w,bef
,_
) ->
739 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
740 | Ast.Nest
(starter
,stmt_dots
,ender
,w,multi
,bef
,_
) ->
741 let w = get_after_whencode
a w in
742 let (sd
,_
) = get_after stmt_dots
a in
744 got rid of this. don't want to let nests overshoot
749 Unify_ast.unify_statement_dots
750 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
752 Unify_ast.MAYBE -> false
754 | Ast.Other_dots a ->
755 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
757 Unify_ast.MAYBE -> false
761 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,bef
,a)),
762 [Ast.Other_dots stmt_dots
])
763 | Ast.Disj
(stmt_dots_list
) ->
765 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
766 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
768 (match Ast.unwrap ast
with
769 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
770 (* check "after" information for metavar optimization *)
771 (* if the error is not desired, could just return [], then
772 the optimization (check for EF) won't take place *)
776 (match Ast.unwrap x
with
777 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
779 "dots/nest not allowed before and after stmt metavar"
781 | Ast.Other_dots x
->
782 (match Ast.undots x
with
784 (match Ast.unwrap x
with
785 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
787 ("dots/nest not allowed before and after stmt "^
796 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
797 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
798 | _
-> (s,[Ast.Other
s]))
799 | Ast.Seq
(lbrace
,body
,rbrace
) ->
800 let index = count_nested_braces s in
801 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
802 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
803 [Ast.WParen
(lbrace
,index)])
804 | Ast.Define
(header
,body
) ->
805 let (body
,_
) = get_after body
a in
806 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
807 | Ast.AsStmt
(stmt
,asstmt
) ->
808 let (stmt
,_
) = get_after_e stmt
[] in
809 let (asstmt
,_
) = get_after_e asstmt
[] in
810 (Ast.rewrap
s (Ast.AsStmt
(stmt
,asstmt
)),[Ast.Other
s])
811 | Ast.IfThen
(ifheader
,branch
,aft
) ->
812 let (br
,_
) = get_after_e branch
a in
813 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
814 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
815 let (br1
,_
) = get_after_e branch1
a in
816 let (br2
,_
) = get_after_e branch2
a in
817 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
818 | Ast.While
(header
,body
,aft
) ->
819 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
820 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
821 | Ast.For
(header
,body
,aft
) ->
822 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
823 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
824 | Ast.Do
(header
,body
,tail
) ->
825 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
826 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
827 | Ast.Iterator
(header
,body
,aft
) ->
828 let (bd
,_
) = get_after_e body
((Ast.Other
s) :: a) in
829 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
830 | Ast.Switch
(header
,lb
,decls
,cases,rb
) ->
831 let index = count_nested_braces s in
834 (function case_line
->
835 match Ast.unwrap case_line
with
836 Ast.CaseLine
(header
,body
) ->
837 let (body
,_
) = get_after body
[Ast.WParen
(rb
,index)] in
838 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
839 | Ast.OptCase
(case_line
) -> failwith
"not supported")
841 let (de
,_
) = get_after decls
[] in
842 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),[Ast.WParen
(lb
,index)])
843 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
844 let (bd
,_
) = get_after body
[] in
845 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
846 | _
-> failwith
"get_after_e: not supported"
848 let preprocess_dots sl
=
849 let (sl
,_
) = get_before sl
[] in
850 let (sl
,_
) = get_after sl
[] in
853 let preprocess_dots_e sl
=
854 let (sl
,_
) = get_before_e sl
[] in
855 let (sl
,_
) = get_after_e sl
[] in
858 (* --------------------------------------------------------------------- *)
859 (* various return_related things *)
861 let rec ends_in_return stmt_list
=
862 match Ast.unwrap stmt_list
with
864 (match List.rev x
with
866 (match Ast.unwrap x
with
869 match Ast.unwrap x
with
870 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
871 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
874 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
877 | Ast.CIRCLES
(x
) -> failwith
"not supported"
878 | Ast.STARS
(x
) -> failwith
"not supported"
880 (* --------------------------------------------------------------------- *)
883 let exptymatch l make_match make_guard_match
=
884 let pos = fresh_pos() in
885 let matches_guard_matches =
888 let pos = Ast.make_mcode
pos in
889 (make_match (Ast.set_pos x
(Some
pos)),
890 make_guard_match
(Ast.set_pos x
(Some
pos))))
892 let (matches
,guard_matches
) = List.split
matches_guard_matches in
893 let rec suffixes = function
895 | x
::xs -> xs::(suffixes xs) in
897 (* normally, we check that an expression does not match something
898 earlier in the disjunction (calculated as prefixes). But for large
899 disjunctions, this can result in a very big CTL formula. So we
900 give the user the option to say he doesn't want this feature, if that is
902 if !Flag_matcher.no_safe_expressions
903 then List.map
(function _
-> []) matches
904 else List.rev
(suffixes (List.rev guard_matches
)) in
905 let info = (* not null *)
911 ctl_and CTL.NONSTRICT
matcher
913 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
915 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
917 (* code might be a DisjRuleElem, in which case we break it apart
918 code might contain an Exp or Ty
919 this one pushes the quantifier inwards *)
920 let do_re_matches label guard
res quantified minus_quantified
=
921 let make_guard_match x
=
922 let stmt_fvs = Ast.get_mfvs x
in
923 let fvs = get_unquantified minus_quantified
stmt_fvs in
924 non_saved_quantify fvs (make_match None
true x
) in
926 let stmt_fvs = Ast.get_fvs x
in
927 let fvs = get_unquantified quantified
stmt_fvs in
928 quantify guard
fvs (make_match None guard x
) in
929 (* label used to be used here, but it is not use; label is only needed after
931 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
932 (match List.map
Ast.unwrap
res with
933 [] -> failwith
"unexpected empty disj"
934 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
935 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
937 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
939 then failwith
"unexpected exp or ty";
940 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
942 (* code might be a DisjRuleElem, in which case we break it apart
943 code doesn't contain an Exp or Ty
944 this one is for use when it is not practical to push the quantifier inwards
946 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
947 match Ast.unwrap code
with
948 Ast.DisjRuleElem
(res) ->
949 let make_match = make_match None guard
in
950 let orop = if guard
then ctl_or else ctl_seqor in
951 (* label used to be used here, but it is not use; label is only needed after
953 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
954 (List.fold_left
orop CTL.False
(List.map
make_match res))
955 | _
-> make_match label guard code
957 (* --------------------------------------------------------------------- *)
958 (* control structures *)
960 let end_control_structure fvs header body after_pred
961 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
962 (* aft indicates what is added after the whole if, which has to be added
964 let (aft_needed
,after_branch
) =
966 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
967 (false,make_seq_after2 guard after_pred after
)
970 make_match label guard
971 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
973 make_seq_after guard after_pred
974 (After
(make_seq_after guard
match_endif after
))) in
975 let body = body after_branch
in
976 let s = guard_to_strict guard
in
981 (match (after
,aft_needed
) with
982 (After _
,_
) (* pattern doesn't end here *)
983 | (_
,true) (* + code added after *) -> after_checks
984 | _
-> no_after_checks
)
985 (ctl_ax_absolute s body)))
987 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
988 quantified minus_quantified label llabel slabel recurse
make_match guard
=
989 (* "if (test) thn" becomes:
990 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
992 "if (test) thn; after" becomes:
993 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
998 match seq_fvs quantified
999 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
1000 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1001 | _
-> failwith
"not possible" in
1002 let new_quantified = Common.union_set bfvs quantified
in
1004 match seq_fvs minus_quantified
1005 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
1006 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1007 | _
-> failwith
"not possible" in
1008 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1010 let if_header = quantify guard efvs
(make_match ifheader
) in
1011 (* then branch and after *)
1012 let lv = get_label_ctr() in
1013 let used = ref false in
1015 (* no point to put a label on truepred etc; it is local to this construct
1016 so it must have the same label *)
1018 [truepred None
; recurse branch NotTop Tail
new_quantified new_mquantified
1019 (Some
(lv,used)) llabel slabel guard
] in
1020 let after_pred = aftpred None
in
1021 let or_cases after_branch
=
1022 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
1023 let (if_header,wrapper
) =
1026 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1027 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1028 (function body -> quantify true [lv] body))
1029 else (if_header,function x
-> x
) in
1031 (end_control_structure bfvs
if_header or_cases after_pred
1032 (Some
(ctl_ex after_pred)) None aft after label guard
)
1034 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
1035 quantified minus_quantified label llabel slabel recurse
make_match guard
=
1036 (* "if (test) thn else els" becomes:
1037 if(test) & AX((TrueBranch & AX thn) v
1038 (FalseBranch & AX (else & AX els)) v After)
1041 "if (test) thn else els; after" becomes:
1042 if(test) & AX((TrueBranch & AX thn) v
1043 (FalseBranch & AX (else & AX els)) v
1044 (After & AXAX after))
1048 (* free variables *)
1049 let (e1fvs
,b1fvs
,s1fvs
) =
1050 match seq_fvs quantified
1051 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1052 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1053 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1054 | _
-> failwith
"not possible" in
1055 let (e2fvs
,b2fvs
,s2fvs
) =
1057 (* just combine with the else branch. no point to have separate
1058 quantifier, since there is only one possible control-flow path *)
1059 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1060 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1061 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1062 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1063 | _
-> failwith
"not possible" in
1064 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1065 let exponlyfvs = intersect e1fvs e2fvs
in
1066 let new_quantified = union bothfvs quantified
in
1067 (* minus free variables *)
1068 let (me1fvs
,mb1fvs
,ms1fvs
) =
1069 match seq_fvs minus_quantified
1070 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1071 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1072 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1073 | _
-> failwith
"not possible" in
1074 let (me2fvs
,mb2fvs
,ms2fvs
) =
1076 (* just combine with the else branch. no point to have separate
1077 quantifier, since there is only one possible control-flow path *)
1079 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1080 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1081 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1082 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1083 | _
-> failwith
"not possible" in
1084 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1085 let new_mquantified = union mbothfvs minus_quantified
in
1087 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1088 (* then and else branches *)
1089 let lv = get_label_ctr() in
1090 let used = ref false in
1093 [truepred None
; recurse branch1 NotTop Tail
new_quantified new_mquantified
1094 (Some
(lv,used)) llabel slabel guard
] in
1099 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1100 (header_match None guard els
);
1101 recurse branch2 NotTop Tail
new_quantified new_mquantified
1102 (Some
(lv,used)) llabel slabel guard
] in
1103 let after_pred = aftpred None
in
1104 let or_cases after_branch
=
1105 ctl_or true_branch (ctl_or false_branch after_branch
) in
1106 let s = guard_to_strict guard
in
1107 let (if_header,wrapper
) =
1110 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1111 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1112 (function body -> quantify true [lv] body))
1113 else (if_header,function x
-> x
) in
1115 (end_control_structure bothfvs if_header or_cases after_pred
1116 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1117 (Some
(ctl_ex (falsepred None
)))
1118 aft after label guard
)
1120 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1121 quantified minus_quantified label recurse
make_match guard
=
1123 (* the translation in this case is similar to that of an if with no else *)
1124 (* free variables *)
1126 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1127 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1128 | _
-> failwith
"not possible" in
1129 let new_quantified = Common.union_set bfvs quantified
in
1130 (* minus free variables *)
1132 match seq_fvs minus_quantified
1133 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1134 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1135 | _
-> failwith
"not possible" in
1136 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1138 let header = quantify guard efvs
(make_match header) in
1139 let lv = get_label_ctr() in
1140 let used = ref false in
1144 recurse
body NotTop Tail
new_quantified new_mquantified
1145 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1146 let after_pred = loopfallpred None
in
1147 let or_cases after_branch
= ctl_or body after_branch
in
1148 let (header,wrapper
) =
1151 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1152 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1153 (function body -> quantify true [lv] body))
1154 else (header,function x
-> x
) in
1156 (end_control_structure bfvs
header or_cases after_pred
1157 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1158 match (Ast.unwrap
body,aft
) with
1159 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1160 (match Ast.unwrap re
with
1161 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1162 Type_cocci.Unitary
,_
,false)
1163 when after
= Tail
or after
= End
or after
= VeryEnd
->
1165 match seq_fvs quantified
[Ast.get_fvs
header] with
1167 | _
-> failwith
"not possible" in
1168 quantify guard efvs
(make_match header)
1172 (* --------------------------------------------------------------------- *)
1173 (* statement metavariables *)
1175 (* issue: an S metavariable that is not an if branch/loop body
1176 should not match an if branch/loop body, so check that the labels
1177 of the nodes before the first node matched by the S are different
1178 from the label of the first node matched by the S *)
1179 let sequencibility body label_pred process_bef_aft
= function
1180 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1183 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1184 | Ast.SequencibleAfterDots
l ->
1185 (* S appears after some dots. l is the code that comes after the S.
1186 want to search for that first, because S can match anything, while
1187 the stuff after is probably more restricted *)
1188 let afts = List.map process_bef_aft
l in
1189 let ors = foldl1 ctl_or afts in
1190 ctl_and CTL.NONSTRICT
1191 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1194 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1195 | Ast.NotSequencible
-> body (function x
-> x
)
1197 let svar_context_with_add_after stmt
s label quantified
d ast
1198 seqible after process_bef_aft guard fvinfo
=
1199 let label_var = (*fresh_label_var*) string2var "_lab" in
1201 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1202 (*let prelabel_pred =
1203 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
1204 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1205 let full_metamatch = matcher d in
1206 let first_metamatch =
1209 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
,c
)) ->
1210 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
,c
))
1211 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1212 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1214 let middle_metamatch =
1217 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1218 | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
1220 let last_metamatch =
1223 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
,c
)) ->
1224 Ast.CONTEXT
(pos,Ast.AFTER
(aft
,c
))
1225 | Ast.CONTEXT
(_
,_
) -> d
1226 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1230 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1233 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1234 let left_or = (* the whole statement is one node *)
1235 make_seq_after guard
1236 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_ex to_end)) full_metamatch) after
in
1237 let right_or = (* the statement covers multiple nodes *)
1238 ctl_and CTL.NONSTRICT
1241 [to_end; make_seq_after guard
last_metamatch after
]))
1247 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1251 ctl_au CTL.NONSTRICT
1254 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1256 (ctl_not prelabel_pred) after])] in
1260 ctl_and CTL.NONSTRICT
label_pred
1261 (f
(ctl_and CTL.NONSTRICT
1262 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1263 let stmt_fvs = Ast.get_fvs stmt
in
1264 let fvs = get_unquantified quantified
stmt_fvs in
1265 quantify guard
(label_var::fvs)
1266 (sequencibility body label_pred process_bef_aft seqible
)
1268 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1269 seqible after process_bef_aft guard fvinfo
=
1270 let label_var = (*fresh_label_var*) string2var "_lab" in
1272 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1274 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1275 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1277 match (d,after
) with
1278 (Ast.PLUS _
, _
) -> failwith
"not possible"
1279 | (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1280 (* just match the root. don't care about label; always ok *)
1281 make_raw_match None
false ast
1282 | (Ast.CONTEXT
(pos,Ast.BEFORE
(_
,_
)),(Tail
|End
|VeryEnd
)) ->
1283 ctl_and CTL.NONSTRICT
1284 (make_raw_match None
false ast
) (* statement *)
1285 (matcher d) (* transformation *)
1286 | (Ast.CONTEXT
(pos,(Ast.NOTHING
|Ast.BEFORE
(_
,_
))),(After
a | Guard
a)) ->
1287 (* This case and the MINUS one couldprobably be merged, if
1288 HackForStmt were to notice when its arguments are trivial *)
1289 let first_metamatch = matcher d in
1290 (* try to follow after link *)
1291 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1293 ctl_ex(make_seq guard
[to_end; CTL.True
; a]) in
1295 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1296 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1297 (ctl_and CTL.NONSTRICT
1298 first_metamatch (ctl_or is_compound not_compound))
1299 | (Ast.CONTEXT
(pos,(Ast.AFTER _
|Ast.BEFOREAFTER _
)),_
) ->
1300 failwith
"not possible"
1301 | (Ast.MINUS
(pos,inst
,adj
,l),after
) ->
1302 let (first_metamatch,last_metamatch,rest_metamatch
) =
1304 Ast.NOREPLACEMENT
->
1305 (matcher(Ast.CONTEXT
(pos,Ast.NOTHING
)),CTL.True
,matcher d)
1307 matcher(Ast.MINUS
(pos,inst
,adj
,Ast.NOREPLACEMENT
)),
1308 ctl_and CTL.NONSTRICT
1309 (ctl_not (make_raw_match label
false ast
))
1310 (matcher(Ast.MINUS
(pos,inst
,adj
,Ast.NOREPLACEMENT
)))) in
1311 (* try to follow after link *)
1312 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1316 [to_end; make_seq_after guard
last_metamatch after
]) in
1318 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1319 ctl_and CTL.NONSTRICT
1320 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1321 (ctl_and CTL.NONSTRICT
1322 first_metamatch (ctl_or is_compound not_compound)))
1323 (* don't have to put anything before the beginning, so don't have to
1324 distinguish the first node. so don't have to bother about paths,
1325 just use the label. label ensures that found nodes match up with
1326 what they should because it is in the lhs of the andany. *)
1327 (CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1328 ctl_and CTL.NONSTRICT
label_pred
1329 (make_raw_match label
false ast
),
1330 ctl_and CTL.NONSTRICT
prelabel_pred rest_metamatch
))
1332 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1333 let stmt_fvs = Ast.get_fvs stmt
in
1334 let fvs = get_unquantified quantified
stmt_fvs in
1335 quantify guard
(label_var::fvs)
1336 (sequencibility body label_pred process_bef_aft seqible
)
1338 (* --------------------------------------------------------------------- *)
1339 (* dots and nests *)
1341 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1342 let matchgoto = gotopred None
in
1344 make_match None
false
1346 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1348 make_match None
false
1350 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1352 if quantifier
= Exists
1353 then Common.Left
(CTL.False
)
1355 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1357 then Common.Left
(aftpred label
)
1360 (function vx
-> function v ->
1361 (* vx is the contents of the nest, if any. we can only stop early
1362 if we find neither the ending code nor the nest contents in
1363 the if branch. not sure if this is a good idea. *)
1364 let lv = get_label_ctr() in
1365 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1366 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1368 (* Rather a special case. But if the code afterwards is just
1369 a } then there is no point checking after a goto that it does
1371 (* this optimization doesn't work. probably depends on whether
1372 the destination of the break/goto is local or more global than
1374 match seq_after
with
1376 let is_paren = function
1377 CTL.Pred
(Lib_engine.Paren _
,_
) -> true
1379 is_paren e1
or is_paren e2
1381 ctl_or (aftpred label
)
1382 (quantify false [lv]
1383 (ctl_and CTL.NONSTRICT
1384 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1385 (ctl_au CTL.NONSTRICT
1386 (ctl_and CTL.NONSTRICT
(ctl_not v)
1387 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1388 (ctl_and CTL.NONSTRICT
preflabelpred
1389 (if !Flag_matcher.only_return_is_error_exit
1391 (ctl_and CTL.NONSTRICT
1392 (retpred None
) (ctl_not seq_after
))
1395 (ctl_and CTL.NONSTRICT
1396 (ctl_or (retpred None
) matchcontinue)
1397 (ctl_not seq_after
))
1398 (ctl_and CTL.NONSTRICT
1399 (ctl_or matchgoto matchbreak)
1401 (* an optim that failed see defn is_paren
1402 and tests/makes_a_loop *)
1406 (ctl_not seq_after
))))))))))) in
1407 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1408 let v = get_let_ctr() in
1410 (match stop_early with
1411 Common.Left x1
-> ctl_or y x1
1412 | Common.Right
stop_early ->
1415 (ctl_and CTL.NONSTRICT
(label_pred_maker label
)
1416 (stop_early n
(CTL.Ref
v)))))
1418 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1419 process_bef_aft statement_list statement guard quantified wrapcode
=
1420 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1421 (* proces bef_aft *)
1423 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1424 let bef_aft = (* to be negated *)
1428 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1431 with Not_found
-> shortest (Common.union_set bef aft
) in
1434 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1436 let check_quantifier quant other
=
1438 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1442 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1444 then failwith
"inconsistent annotation on dots"
1448 if check_quantifier Ast.WhenExists
Ast.WhenForall
1451 if check_quantifier Ast.WhenForall
Ast.WhenExists
1454 (* the following is used when we find a goto, etc and consider accepting
1455 without finding the rest of the pattern *)
1456 let aft = shortest aft in
1457 (* process whencode *)
1458 let labelled = label_pred_maker label
in
1460 let (poswhen
,negwhen
) =
1462 (function (poswhen
,negwhen
) ->
1464 Ast.WhenNot
whencodes ->
1465 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1466 | Ast.WhenAlways stm
->
1467 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1468 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1469 | Ast.WhenNotTrue
(e
) ->
1471 ctl_or (whencond_true e label guard quantified
) negwhen
)
1472 | Ast.WhenNotFalse
(e
) ->
1474 ctl_or (whencond_false e label guard quantified
) negwhen
))
1475 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1476 (*bef_aft modifies arg so that inside of a nest can't cause the next
1477 to overshoot its boundaries, eg a() <...f()...> b() where f is
1478 a metavariable and the whole thing matches code in a loop;
1479 don't want f to match eg b(), allowing to go around the loop again*)
1480 let poswhen = ctl_and_ns arg
poswhen in
1484 (* add in After, because it's not part of the program *)
1485 ctl_or (aftpred label
) negwhen
1487 ctl_and_ns poswhen (ctl_not negwhen) in
1488 (* process dot code, if any *)
1490 match (dotcode,guard
) with
1491 (None
,_) | (_,true) -> CTL.True
1492 | (Some
dotcode,_) -> dotcode in
1493 (* process nest code, if any *)
1494 (* whencode goes in the negated part of the nest; if no nest, just goes
1495 on the "true" in between code *)
1496 let plus_var = if plus
then get_label_ctr() else string2var "" in
1497 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1498 let (ornest
,just_nest
) =
1499 (* just_nest is used when considering whether to stop early, to continue
1500 to collect nest information in the if branch *)
1501 match (nest
,guard
&& not plus
) with
1502 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1503 | (Some nest
,false) ->
1504 let v = get_let_ctr() in
1508 (* the idea is that BindGood is sort of a witness; a witness to
1509 having found the subterm in at least one place. If there is
1510 not a witness, then there is a risk that it will get thrown
1511 away, if it is merged with a node that has an empty
1512 environment. See tests/nestplus. But this all seems
1513 rather suspicious *)
1514 CTL.And
(CTL.NONSTRICT
,x
,
1515 CTL.Exists
(true,plus_var2,
1516 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1517 CTL.Modif
plus_var2)))
1521 CTL.Or
(is_plus (CTL.Ref
v),
1522 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1524 let plus_modifier x
=
1531 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1536 (* label within dots is taken care of elsewhere. the next two lines
1537 put the label on the code following dots *)
1538 After f
-> ctl_and (guard_to_strict guard
) f
labelled
1540 (* actually, label should be None based on the only use of Guard... *)
1541 assert (label
= None
);
1542 ctl_and CTL.NONSTRICT
(ctl_uncheck f
) labelled
1544 let exit = endpred label
in
1545 let errorexit = exitpred label
in
1546 ctl_or exit errorexit
1547 (* not at all sure what the next two mean... *)
1551 Some
(lv,used) -> used := true;
1552 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1553 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1554 | None
-> endpred label
)
1555 (* was the following, but not clear why sgrep should allow
1557 let exit = endpred label in
1558 let errorexit = exitpred label in
1560 then ctl_or exit errorexit (* end anywhere *)
1561 else exit (* end at the real end of the function *) *)
in
1563 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1564 label
(guard_to_strict guard
) wrapcode just_nest
1566 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1567 aft ender quantifier)
1569 and get_whencond_exps e
=
1570 match Ast.unwrap e
with
1572 | Ast.DisjRuleElem
(res) ->
1573 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1574 | _ -> failwith
"not possible"
1576 and make_whencond_headers e e1 label guard quantified
=
1577 let fvs = Ast.get_fvs e
in
1579 quantify guard
(get_unquantified quantified
fvs)
1580 (make_match label guard h
) in
1585 (Ast.make_mcode
"if",
1586 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1587 let while_header e1
=
1591 (Ast.make_mcode
"while",
1592 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1597 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1598 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1600 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1602 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1604 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1605 (if_headers, while_headers, for_headers)
1607 and whencond_true e label guard quantified
=
1608 let e1 = get_whencond_exps e
in
1609 let (if_headers, while_headers, for_headers) =
1610 make_whencond_headers e
e1 label guard quantified
in
1612 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1613 (ctl_and CTL.NONSTRICT
1614 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1616 and whencond_false e label guard quantified
=
1617 let e1 = get_whencond_exps e
in
1618 let (if_headers, while_headers, for_headers) =
1619 make_whencond_headers e
e1 label guard quantified
in
1621 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1622 (* if without else *)
1623 (ctl_or (ctl_and CTL.NONSTRICT
(fallpred label
) (ctl_back_ex if_headers))
1624 (* failure of loop test *)
1625 (ctl_and CTL.NONSTRICT
(loopfallpred label
)
1626 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1628 (* --------------------------------------------------------------------- *)
1629 (* the main translation loop *)
1631 let rec statement_list stmt_list top after quantified minus_quantified
1632 label llabel slabel dots_before guard
=
1634 (* include Disj to be on the safe side *)
1635 match Ast.unwrap x
with
1636 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1637 let compute_label l e db
= if db
or isdots e
then l else None
in
1638 match Ast.unwrap stmt_list
with
1640 let rec loop top quantified minus_quantified dots_before
1643 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1645 statement e top after quantified minus_quantified
1646 (compute_label label e dots_before
)
1648 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1649 let shared = intersectll fv
fvs in
1650 let unqshared = get_unquantified quantified
shared in
1651 let new_quantified = Common.union_set
unqshared quantified
in
1652 let minus_shared = intersectll mfv mfvs
in
1654 get_unquantified minus_quantified
minus_shared in
1655 let new_mquantified =
1656 Common.union_set
munqshared minus_quantified
in
1657 quantify guard
unqshared
1660 (let (label1
,llabel1
,slabel1
) =
1661 match Ast.unwrap e
with
1663 (match Ast.unwrap re
with
1664 Ast.Goto
_ -> (None
,None
,None
)
1665 | _ -> (label
,llabel
,slabel
))
1666 | _ -> (label
,llabel
,slabel
) in
1667 loop NotTop
new_quantified new_mquantified (isdots e
)
1668 label1 llabel1 slabel1
1670 new_quantified new_mquantified
1671 (compute_label label e dots_before
) llabel slabel guard
)
1672 | _ -> failwith
"not possible" in
1673 loop top quantified minus_quantified dots_before
1675 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1676 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1677 | Ast.STARS
(x
) -> failwith
"not supported"
1679 (* llabel is the label of the enclosing loop and slabel is the label of the
1681 and statement stmt top after quantified minus_quantified
1682 label llabel slabel guard
=
1683 let ctl_au = ctl_au CTL.NONSTRICT
in
1684 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1685 let ctl_and = ctl_and CTL.NONSTRICT
in
1686 let make_seq = make_seq guard
in
1687 let make_seq_after = make_seq_after guard
in
1688 let real_make_match = make_match in
1689 let make_match = header_match label guard
in
1691 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1694 match Ast.unwrap stmt
with
1696 (match Ast.unwrap ast
with
1697 (* the following optimisation is not a good idea, because when S
1698 is alone, we would like it not to match a declaration.
1699 this makes more matching for things like when (...) S, but perhaps
1700 that matching is not so costly anyway *)
1701 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1702 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_,_)) as d),_),
1704 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_,_)) as d),_),
1706 svar_context_with_add_after stmt
s label quantified
d ast seqible
1708 (process_bef_aft quantified minus_quantified
1709 label llabel slabel
true)
1711 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1713 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1714 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1716 (process_bef_aft quantified minus_quantified
1717 label llabel slabel
true)
1719 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1723 match Ast.unwrap ast
with
1724 Ast.DisjRuleElem
(res) ->
1725 do_re_matches label guard
res quantified minus_quantified
1726 | Ast.Exp
(_) | Ast.Ty
(_) ->
1727 let stmt_fvs = Ast.get_fvs stmt
in
1728 let fvs = get_unquantified quantified
stmt_fvs in
1729 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1731 let stmt_fvs = Ast.get_fvs stmt
in
1732 let fvs = get_unquantified quantified
stmt_fvs in
1733 quantify guard
fvs (make_match ast
) in
1734 match Ast.unwrap ast
with
1735 Ast.Break
(brk
,semi
) ->
1736 (match (llabel
,slabel
) with
1737 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1738 ctl_and term (bclabel_pred_maker slabel
)
1739 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1740 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1741 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1742 (* discard pattern that comes after return *)
1743 let normal_res = make_seq_after term after
in
1744 (* the following code tries to propagate the modifications on
1745 return; to a close brace, in the case where the final return
1748 match (retmc
,semmc
) with
1749 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1750 when !Flag.sgrep_mode2
->
1751 (* in sgrep mode, we can propagate the - *)
1754 (Ast.NOREPLACEMENT
,Ast.NOREPLACEMENT
) ->
1757 failwith
"no replacements allowed in sgrep mode" in
1758 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,new_info))
1759 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
)) ->
1762 (Ast.NOREPLACEMENT
,Ast.NOREPLACEMENT
) ->
1764 | (Ast.NOREPLACEMENT
,Ast.REPLACEMENT
(l,ct
))
1765 | (Ast.REPLACEMENT
(l,ct
),Ast.NOREPLACEMENT
) ->
1767 | (Ast.REPLACEMENT
(l1
,ct1
),Ast.REPLACEMENT
(l2
,ct2
)) ->
1768 Ast.BEFORE
(l1
@l2
,Ast.lub_count ct1 ct2
) in
1769 Some
(Ast.CONTEXT
(Ast.NoPos
,change))
1770 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
,c1
)),
1771 Ast.CONTEXT
(_,Ast.AFTER
(l2
,c2
))) ->
1773 (Ast.CONTEXT
(Ast.NoPos
,
1774 Ast.BEFORE
(l1
@l2
,Ast.lub_count c1 c2
)))
1775 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1776 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1778 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1779 Ast.CONTEXT
(_,Ast.AFTER
(l,c
))) ->
1780 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l,c
)))
1782 let ret = Ast.make_mcode
"return" in
1784 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1785 let semi = Ast.make_mcode
";" in
1787 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1789 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1792 let exit = endpred None
in
1794 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1795 let stripped_rbrace =
1796 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1798 (ctl_and (make_match mod_rbrace)
1801 (make_match stripped_rbrace)
1802 (* error exit not possible; it is in the middle
1803 of code, so a return is needed *)
1805 (* worry about perf, but seems correct, not ax *)
1809 (ctl_or simple_return return_expr))))))
1811 (* some change in the middle of the return, so have to
1812 find an actual return *)
1815 (* should try to deal with the dots_bef_aft problem elsewhere,
1816 but don't have the courage... *)
1821 do_between_dots stmt
term End
1822 quantified minus_quantified label llabel slabel guard
in
1824 make_seq_after term after
)
1825 | Ast.Seq
(lbrace
,body,rbrace
) ->
1826 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1829 [Ast.get_fvs lbrace
;Ast.get_fvs
body;Ast.get_fvs rbrace
]
1831 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] -> (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1832 | _ -> failwith
"not possible" in
1833 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1835 seq_fvs minus_quantified
1836 [Ast.get_mfvs lbrace
;Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1838 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1839 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1840 | _ -> failwith
"not possible" in
1841 let pv = count_nested_braces stmt
in
1842 let lv = get_label_ctr() in
1843 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1844 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1847 (quantify guard lbfvs
(make_match lbrace
))
1848 (ctl_and paren_pred label_pred) in
1850 match Ast.unwrap rbrace
with
1851 Ast.SeqEnd
((data
,info,_,pos)) ->
1852 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1853 | _ -> failwith
"unexpected close brace" in
1855 (* label is not needed; paren_pred is enough *)
1856 quantify guard rbfvs
1857 (ctl_au (make_match empty_rbrace)
1858 (ctl_and (real_make_match None guard rbrace
) paren_pred)) in
1859 let new_quantified2 =
1860 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1861 let new_mquantified2 =
1862 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1863 let pattern_as_given =
1864 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1865 quantify true [pv;lv]
1866 (quantify guard b1fvs
1870 (if !exists = Exists
then CTL.False
else (aftpred label
))
1871 (quantify guard b2fvs
1872 (statement_list body NotTop
1873 (After
(make_seq_after end_brace after
))
1874 new_quantified2 new_mquantified2
1875 (Some
(lv,ref true))
1876 llabel slabel
false guard
)))])) in
1878 match Ast.undots
body with
1880 (match Ast.unwrap
body with
1882 ((_,i
,Ast.CONTEXT
(_,Ast.NOTHING
),_),[],_,_) ->
1883 (match Ast.unwrap rbrace
with
1884 Ast.SeqEnd
((_,_,Ast.CONTEXT
(_,Ast.NOTHING
),_))
1885 when not
(contains_pos rbrace
) -> true
1889 if empty_body && List.mem after
[Tail
;End
;VeryEnd
]
1890 (* for just a match of an if branch of the form { ... }, just
1891 match the first brace *)
1892 then quantify guard lbfvs
(make_match lbrace
)
1893 else if ends_in_return body
1895 (* matching error handling code *)
1897 1. The pattern as given
1898 2. A goto, and then some close braces, and then the pattern as
1899 given, but without the braces (only possible if there are no
1900 decls, and open and close braces are unmodified)
1901 3. Part of the pattern as given, then a goto, and then the rest
1902 of the pattern. For this case, we just check that all paths have
1903 a goto within the current braces. checking for a goto at every
1904 point in the pattern seems expensive and not worthwhile. *)
1906 let body = preprocess_dots body in (* redo, to drop braces *)
1910 (make_match empty_rbrace)
1911 (ctl_ax (* skip the destination label *)
1912 (quantify guard b2fvs
1913 (statement_list body NotTop End
1914 new_quantified2 new_mquantified2 None llabel slabel
1917 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1918 quantify true [pv;lv]
1919 (quantify guard b1fvs
1923 (CTL.AU
(* want AF even for sgrep *)
1924 (CTL.FORWARD
,CTL.STRICT
,
1925 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1926 ctl_and (* brace must be eventually after goto *)
1927 (gotopred (Some
(lv,ref true)))
1928 (* want AF even for sgrep *)
1929 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1930 (quantify guard b2fvs
1931 (statement_list body NotTop Tail
1932 new_quantified2 new_mquantified2
1933 None
(*no label because past the goto*)
1934 llabel slabel
false guard
))])) in
1935 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1936 else pattern_as_given
1937 | Ast.IfThen
(ifheader
,branch
,aft) ->
1938 ifthen ifheader branch
aft after quantified minus_quantified
1939 label llabel slabel statement
make_match guard
1941 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1942 ifthenelse ifheader branch1 els branch2
aft after quantified
1943 minus_quantified label llabel slabel statement
make_match guard
1945 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1946 | Ast.Iterator
(header,body,aft) ->
1947 forwhile header body aft after quantified minus_quantified
1948 label statement
make_match guard
1950 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1951 (*ctl_and seems pointless, disjuncts see label too
1952 (label_pred_maker label)*)
1956 statement_list sl top after quantified minus_quantified label
1957 llabel slabel
true guard
)
1959 let safe_subformulas =
1961 Top
-> List.map2 protect_top_level stmt_dots_list
subformulas
1962 | NotTop
-> subformulas in
1963 List.fold_left
ctl_seqor CTL.False
safe_subformulas
1965 | Ast.Nest
(starter
,stmt_dots
,ender,whencode
,multi
,bef
,aft) ->
1966 (* label in recursive call is None because label check is already
1967 wrapped around the corresponding code. not good enough, want to stay
1968 in a specific region, dots and nests will keep going *)
1971 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1973 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1974 | _ -> failwith
"not possible" in
1976 (* no minus version because when code doesn't contain any minus code *)
1977 let new_quantified = Common.union_set
bfvs quantified
in
1980 match Ast.get_mcodekind starter
with (*ender must have the same mcode*)
1981 Ast.MINUS
(_,_,_,_) as d ->
1982 (* no need for the fresh metavar, but ... is a bit weird as a
1984 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1989 statement_list stmt_dots top
(a2n after
)
1990 new_quantified minus_quantified
1991 label
(*None*) llabel slabel
true guard
in
1992 dots_and_nests multi
1993 (Some
dots_pattern) whencode bef
aft dot_code after label
1994 (process_bef_aft
new_quantified minus_quantified
1995 label
(*None*) llabel slabel
true)
1996 (function x
-> (* for when code *)
1997 statement_list x NotTop Tail
1998 new_quantified minus_quantified label
(*None*)
1999 llabel slabel
true true)
2000 (function x
-> (* for when code *)
2001 statement x NotTop Tail
2002 new_quantified minus_quantified label
(*None*)
2005 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
2007 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
2010 Ast.MINUS
(_,_,_,_) ->
2011 (* no need for the fresh metavar, but ... is a bit weird as a
2013 Some
(make_match (make_meta_rule_elem d ([],[],[])))
2015 dots_and_nests false None
whencodes bef
aft dot_code after label
2016 (process_bef_aft quantified minus_quantified None llabel slabel
true)
2018 statement_list x NotTop Tail quantified minus_quantified
2019 None llabel slabel
true true)
2021 statement x NotTop Tail quantified minus_quantified
2022 None llabel slabel
true)
2024 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
2026 | Ast.Switch
(header,lb
,decls
,cases,rb
) ->
2027 let rec intersect_all = function
2030 | x
::xs -> intersect x
(intersect_all xs) in
2031 let rec intersect_all2 = function (* pairwise *)
2036 (function elem
-> List.exists (List.mem elem
) xs)
2038 Common.union_set
front (intersect_all2 xs) in
2039 let rec union_all l = List.fold_left
union [] l in
2040 (* start normal variables *)
2041 let header_fvs = Ast.get_fvs
header in
2042 let lb_fvs = Ast.get_fvs lb
in
2043 let decl_fvs = union_all (List.map
Ast.get_fvs
(Ast.undots decls
)) in
2044 let case_fvs = List.map
Ast.get_fvs
cases in
2045 let rb_fvs = Ast.get_fvs rb
in
2046 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2047 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2049 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2050 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2051 function case_fvs ->
2052 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
2053 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
2054 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
2055 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
2057 | _ -> failwith
"not possible")
2058 ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
2059 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2060 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2061 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
2062 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
2063 List.rev all_rbfvs
) in
2064 let exponlyfvs = intersect_all all_efvs
in
2065 let lbonlyfvs = intersect_all all_lbfvs
in
2066 (* don't do anything with right brace. Hope there is no + code on it *)
2067 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2068 let b1fvs = union_all all_b1fvs
in
2069 let new1_quantified = union b1fvs quantified
in
2071 union (union_all all_b2fvs
) (intersect_all2 all_casefvs
) in
2072 let new2_quantified = union b2fvs new1_quantified in
2073 (* let b3fvs = union_all all_b3fvs in*)
2074 (* ------------------- start minus free variables *)
2075 let header_mfvs = Ast.get_mfvs
header in
2076 let lb_mfvs = Ast.get_mfvs lb
in
2077 let decl_mfvs = union_all (List.map
Ast.get_mfvs
(Ast.undots decls
)) in
2078 let case_mfvs = List.map
Ast.get_mfvs
cases in
2079 let rb_mfvs = Ast.get_mfvs rb
in
2080 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2081 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2083 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2084 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2085 function case_mfvs ->
2088 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
2089 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
2090 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
2091 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
2093 | _ -> failwith
"not possible")
2094 ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
2095 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2096 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2097 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
2098 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
2099 List.rev all_mrbfvs
) in
2100 (* don't do anything with right brace. Hope there is no + code on it *)
2101 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2102 let mb1fvs = union_all all_mb1fvs
in
2103 let new1_mquantified = union mb1fvs quantified
in
2105 union (union_all all_mb2fvs
) (intersect_all2 all_mcasefvs
) in
2106 let new2_mquantified = union mb2fvs new1_mquantified in
2107 (* let b3fvs = union_all all_b3fvs in*)
2108 (* ------------------- end collection of free variables *)
2109 let switch_header = quantify guard
exponlyfvs (make_match header) in
2110 let lb = quantify guard
lbonlyfvs (make_match lb) in
2111 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
2114 (function case_line
->
2115 match Ast.unwrap case_line
with
2116 Ast.CaseLine
(header,body) ->
2118 match seq_fvs new2_quantified [Ast.get_fvs
header] with
2119 [(e1fvs,_)] -> e1fvs
2120 | _ -> failwith
"not possible" in
2121 quantify guard
e1fvs (real_make_match label
true header)
2122 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2124 let lv = get_label_ctr() in
2125 let used = ref false in
2126 let (decls_exists_code
,decls_all_code
) =
2127 (*don't really understand this*)
2128 if (Ast.undots decls
) = []
2129 then (CTL.True
,CTL.False
)
2132 statement_list decls NotTop Tail
2133 new2_quantified new2_mquantified (Some
(lv,used)) llabel None
2138 (List.fold_left
ctl_or_fl CTL.False
2139 (List.map
ctl_uncheck
2140 (decls_all_code
::case_headers))) in
2143 (function case_line
->
2144 match Ast.unwrap case_line
with
2145 Ast.CaseLine
(header,body) ->
2146 let (e1fvs,b1fvs,s1fvs
) =
2147 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
2148 match seq_fvs new2_quantified fvs with
2149 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2150 | _ -> failwith
"not possible" in
2151 let (me1fvs
,mb1fvs,ms1fvs
) =
2152 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
2153 match seq_fvs new2_mquantified fvs with
2154 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2155 | _ -> failwith
"not possible" in
2157 quantify guard
e1fvs (make_match header) in
2158 let new3_quantified = union b1fvs new2_quantified in
2159 let new3_mquantified = union mb1fvs new2_mquantified in
2161 statement_list body NotTop Tail
2162 new3_quantified new3_mquantified (Some
(lv,used)) llabel
2163 (Some
(lv,used)) false(*?*) guard
in
2164 quantify guard
b1fvs (make_seq [case_header; body])
2165 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2167 let default_required =
2170 match Ast.unwrap case
with
2171 Ast.CaseLine
(header,_) ->
2172 (match Ast.unwrap
header with
2173 Ast.Default
(_,_) -> true
2177 then function x
-> x
2178 else function x
-> ctl_or (fallpred label
) x
in
2179 let after_pred = aftpred label
in
2180 let body after_branch
=
2183 (quantify guard
b2fvs
2186 (List.fold_left
ctl_and CTL.True
2188 (decls_exists_code
:: case_headers)));
2189 List.fold_left
ctl_or_fl no_header
2190 (decls_all_code
:: case_code)])))
2193 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2194 match Ast.unwrap
rb with
2195 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2196 | _ -> failwith
"not possible") in
2197 let (switch_header,wrapper
) =
2200 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2201 (ctl_and switch_header label_pred,
2202 (function body -> quantify true [lv] body))
2203 else (switch_header,function x
-> x
) in
2205 (end_control_structure b1fvs switch_header body
2206 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2207 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2208 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2211 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2212 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2214 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2215 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2216 | _ -> failwith
"not possible" in
2217 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2220 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2221 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2223 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2224 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2225 | _ -> failwith
"not possible" in
2226 let function_header = quantify guard hfvs
(make_match header) in
2227 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2228 let stripped_rbrace =
2229 match Ast.unwrap rbrace
with
2230 Ast.SeqEnd
((data
,info,_,_)) ->
2231 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2232 | _ -> failwith
"unexpected close brace" in
2234 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2235 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2236 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2238 (quantify guard rbfvs
(make_match rbrace
))
2240 (* the following finds the beginning of the fake braces,
2241 if there are any, not completely sure how this works.
2242 sse the examples sw and return *)
2243 (ctl_back_ex (ctl_not fake_brace))
2244 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2245 let new_quantified3 =
2246 Common.union_set
b1fvs
2247 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2248 let new_mquantified3 =
2249 Common.union_set
mb1fvs
2250 (Common.union_set
mb2fvs
2251 (Common.union_set mb3fvs minus_quantified
)) in
2252 let not_minus = function Ast.MINUS
(_,_,_,_) -> false | _ -> true in
2254 match (Ast.undots
body,
2255 contains_modif rbrace
or contains_pos rbrace
) with
2257 (match Ast.unwrap
body with
2258 Ast.Nest
(starter
,stmt_dots
,ender,[],false,_,_)
2259 (* perhaps could optimize for minus case too... TODO *)
2260 when not_minus (Ast.get_mcodekind starter
)
2262 (* special case for function header + body - header is unambiguous
2263 and unique, so we can just look for the nested body anywhere
2267 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2268 statement_list stmt_dots NotTop
2269 (* discards match on right brace, but don't need it *)
2270 (Guard
(make_seq_after end_brace after
))
2271 new_quantified3 new_mquantified3
2272 None llabel slabel
true guard
))
2273 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2275 (* flow sensitive, so not optimizable *)
2276 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2278 | _ -> true) whencode
) ->
2279 (* try to be more efficient for the case where the body is just
2280 ... Perhaps this is too much of a special case, but useful
2281 for dropping a parameter and checking that it is never used. *)
2283 Ast.MINUS
(_,_,_,_) -> None
2286 (* no nested braces, because only dots *)
2287 string2var ("p1") in
2289 CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
2292 [ctl_and start_brace paren_pred;
2302 Ast.WhenAlways
(s) -> prev
2303 | Ast.WhenNot
(sl
) ->
2312 | Ast.WhenNotTrue
(_)
2313 | Ast.WhenNotFalse
(_) ->
2314 failwith
"unexpected"
2316 (Ast.WhenAny
) -> CTL.False
2317 | Ast.WhenModifier
(_) -> prev
)
2318 CTL.False whencode
))
2322 Ast.WhenAlways
(s) ->
2324 statement
s NotTop Tail
2327 label llabel slabel
true in
2329 | Ast.WhenNot
(sl
) -> prev
2330 | Ast.WhenNotTrue
(_)
2331 | Ast.WhenNotFalse
(_) ->
2332 failwith
"unexpected"
2333 | Ast.WhenModifier
(Ast.WhenAny
) ->
2335 | Ast.WhenModifier
(_) -> prev
)
2336 CTL.True whencode
) in
2339 (make_match stripped_rbrace)
2344 (* function body is all minus, no whencode *)
2345 match Ast.undots
body with
2347 (match Ast.unwrap
body with
2349 ((_,i
,(Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
) as d),_),[],_,_) ->
2350 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2351 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),_)),
2352 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),_)))
2353 when not
(contains_pos rbrace
) ->
2355 (* andany drops everything to the end, including close
2356 braces - not just function body, could check
2357 label to keep braces *)
2358 (ctl_and start_brace
2361 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2363 (make_meta_rule_elem d ([],[],[]))))))
2368 match (optim1,optim2) with
2374 quantify guard
b3fvs
2375 (statement_list body NotTop
2376 (After
(make_seq_after end_brace after
))
2377 new_quantified3 new_mquantified3 None llabel slabel
2379 quantify guard
b1fvs
2380 (make_seq [function_header; quantify guard
b2fvs body_code])
2381 | Ast.Define
(header,body) ->
2382 let (hfvs
,bfvs,bodyfvs
) =
2383 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2385 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2386 | _ -> failwith
"not possible" in
2387 let (mhfvs
,mbfvs
,mbodyfvs
) =
2388 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2390 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2391 | _ -> failwith
"not possible" in
2392 let define_header = quantify guard hfvs
(make_match header) in
2394 statement_list body NotTop after
2395 (Common.union_set
bfvs quantified
)
2396 (Common.union_set mbfvs minus_quantified
)
2397 None llabel slabel
true guard
in
2398 quantify guard
bfvs (make_seq [define_header; body_code])
2399 | Ast.AsStmt
(stmt
,asstmt
) ->
2401 (statement stmt top after quantified minus_quantified
2402 label llabel slabel guard
)
2403 (statement asstmt top after quantified minus_quantified
2404 label llabel slabel guard
)
2405 | Ast.OptStm
(stm
) ->
2406 failwith
"OptStm should have been compiled away\n"
2407 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2408 | _ -> failwith
"not supported" in
2409 if guard
or !dots_done
2412 do_between_dots stmt
term after quantified minus_quantified
2413 label llabel slabel guard
2415 (* term is the translation of stmt *)
2416 and do_between_dots stmt
term after quantified minus_quantified
2417 label llabel slabel guard
=
2418 match Ast.get_dots_bef_aft stmt
with
2419 Ast.AddingBetweenDots
(brace_term
,n
)
2420 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2422 statement brace_term NotTop after quantified minus_quantified
2423 label llabel slabel guard
in
2424 let v = Printf.sprintf
"_r_%d" n
in
2425 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2426 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2429 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2430 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2432 | Ast.NoDots
-> term
2434 (* un_process_bef_aft is because we don't want to do transformation in this
2435 code, and thus don't case about braces before or after it *)
2436 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2438 Ast.WParen
(re
,n
) ->
2439 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2440 let s = guard_to_strict guard
in
2441 quantify true (get_unquantified quantified
[n
])
2442 (ctl_and s (make_raw_match None guard re
) paren_pred)
2444 statement
s NotTop Tail quantified minus_quantified
2445 label llabel slabel guard
2446 | Ast.Other_dots
d ->
2447 statement_list d NotTop Tail quantified minus_quantified
2448 label llabel slabel
true guard
2450 and protect_top_level stmt_dots formula
=
2451 let starts_with_dots =
2452 match Ast.undots stmt_dots
with
2454 (match Ast.unwrap
d with
2455 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2456 | Ast.Stars
(_,_,_,_) -> true
2459 let starts_with_non_context_brace =
2461 Some false = OK except on function braces
2462 Some true = Never OK *)
2463 match Ast.undots stmt_dots
with
2465 (match Ast.unwrap
d with
2466 Ast.Seq
(before
,body,after
) ->
2468 match Ast.unwrap before
with
2469 Ast.SeqStart
(obr
) -> Ast.get_mcodekind obr
2470 | _ -> failwith
"bad seq" in
2472 match Ast.unwrap after
with
2473 Ast.SeqEnd
(cbr
) -> Ast.get_mcodekind cbr
2474 | _ -> failwith
"bad seq"in
2475 (match (beforemc,aftermc) with
2477 (Ast.CONTEXT
(_,(Ast.NOTHING
|Ast.AFTER
_)),
2478 Ast.CONTEXT
(_,(Ast.NOTHING
|Ast.BEFORE
_))) -> None
2479 | (Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
),
2480 Ast.MINUS
(_,_,_,Ast.NOREPLACEMENT
))
2481 when List.length
(Ast.undots
body) = 1 -> Some
false (*ok on if*)
2482 (* unsafe, can't be allowed to match fn top *)
2487 then (* EX because there is a loop on enter/top *)
2488 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex formula
)
2490 match starts_with_non_context_brace with
2493 ctl_and CTL.NONSTRICT
2494 (ctl_not(CTL.EX
(CTL.BACKWARD
,funpred None
)))
2497 ctl_and CTL.NONSTRICT
2498 (ctl_not(CTL.EX
(CTL.BACKWARD
,unsbrpred None
)))
2502 (* --------------------------------------------------------------------- *)
2503 (* cleanup: convert AX to EX for pdots.
2504 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2505 This is what we wanted in the first place, but it wasn't possible to make
2506 because the AX and its argument are not created in the same place.
2508 (* also cleanup XX, which is a marker for the case where the programmer
2509 specifies to change the quantifier on .... Assumed to only occur after one AX
2510 or EX, or at top level. *)
2513 let c = match c with CTL.XX
(c) -> c | _ -> c in
2515 CTL.False
-> CTL.False
2516 | CTL.True
-> CTL.True
2517 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2518 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2519 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2520 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2521 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2522 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2523 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2524 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2525 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2526 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2527 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2528 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2529 | CTL.AX
(CTL.FORWARD
,s,
2531 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2532 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2534 CTL.And
(CTL.NONSTRICT
,
2535 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2536 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2537 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2538 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2539 CTL.AX
(dir
,s,cleanup phi
)
2540 | CTL.XX
(phi
) -> failwith
"bad XX"
2541 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2542 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2543 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2544 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2545 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2546 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2547 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2548 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2549 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2550 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2551 | CTL.Ref
(s) -> CTL.Ref
(s)
2552 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2553 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2555 (* --------------------------------------------------------------------- *)
2556 (* Function declaration *)
2558 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2560 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2561 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2563 saved := Ast.get_saved t
;
2564 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2565 let (wrap
,formula
) =
2566 match Ast.unwrap t
with
2567 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2568 | Ast.NONDECL
(stmt
) ->
2569 let unopt = elim_opt.V.rebuilder_statement stmt
in
2570 let unopt = preprocess_dots_e unopt in
2573 (statement
unopt Top VeryEnd
quantified [] None None None
false) in
2574 ((function x -> NONDECL
x), formula)
2575 | Ast.CODE
(stmt_dots
) ->
2576 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2577 let unopt = preprocess_dots unopt in
2579 statement_list unopt Top VeryEnd
quantified [] None None None
2581 let clean_formula = cleanup (protect_top_level stmt_dots
formula) in
2582 ((function x -> CODE
x), clean_formula)
2583 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords" in
2584 wrap
(quantify false quantified formula)
2586 (* --------------------------------------------------------------------- *)
2589 let asttoctlz (name
,(_,_,exists_flag
),l)
2590 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2593 (match exists_flag
with
2594 Ast.Exists
-> exists := Exists
2595 | Ast.Forall
-> exists := Forall
2596 | Ast.Undetermined
->
2597 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2599 let (l,used_after) =
2603 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2604 (List.combine
l (List.combine
used_after positions
))) in
2606 List.map2
(top_level name
)
2607 (List.combine
used_after fresh_used_after
)
2608 (List.combine fresh_used_after_seeds
l) in
2612 let asttoctl r
used_after positions
=
2614 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2615 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2616 asttoctlz (a,b
,c) used_after positions
2617 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CODE
CTL.True
]
2619 let pp_cocci_predicate (pred
,modif
) =
2620 Pretty_print_engine.pp_predicate pred
2622 let cocci_predicate_to_string (pred
,modif
) =
2623 Pretty_print_engine.predicate_to_string pred