2 * Copyright 2010, INRIA, University of Copenhagen
3 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
4 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
5 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
6 * This file is part of Coccinelle.
8 * Coccinelle is free software: you can redistribute it and/or modify
9 * it under the terms of the GNU General Public License as published by
10 * the Free Software Foundation, according to version 2 of the License.
12 * Coccinelle is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
25 (* for MINUS and CONTEXT, pos is always None in this file *)
26 (*search for require*)
27 (* true = don't see all matched nodes, only modified ones *)
28 let onlyModif = ref true(*false*)
30 type ex
= Exists
| Forall
31 let exists = ref Forall
33 module Ast
= Ast_cocci
34 module V
= Visitor_ast
37 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
39 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
41 (cocci_predicate
,Ast.meta_name
, Wrapper_ctl.info
) Ast_ctl.generic_ctl
43 let union = Common.union_set
44 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
45 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
47 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
49 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
51 let used_after = ref ([] : Ast.meta_name list
)
52 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
54 let saved = ref ([] : Ast.meta_name list
)
56 let string2var x
= ("",x
)
58 (* --------------------------------------------------------------------- *)
59 (* predicates matching various nodes in the graph *)
63 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
64 | (CTL.True
,a
) | (a
,CTL.True
) -> a
69 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
70 | (CTL.False
,a
) | (a
,CTL.False
) -> a
75 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
76 | (CTL.False
,a
) | (a
,CTL.False
) -> a
81 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
82 | (CTL.False
,a
) | (a
,CTL.False
) -> a
85 let ctl_not = function
87 | CTL.False
-> CTL.True
90 let ctl_ax s
= function
92 | CTL.False
-> CTL.False
95 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
96 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
98 let ctl_ax_absolute s
= function
100 | CTL.False
-> CTL.False
101 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
103 let ctl_ex = function
105 | CTL.False
-> CTL.False
106 | x
-> CTL.EX
(CTL.FORWARD
,x
)
108 (* This stays being AX even for sgrep_mode, because it is used to identify
109 the structure of the term, not matching the pattern. *)
110 let ctl_back_ax = function
112 | CTL.False
-> CTL.False
113 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
115 let ctl_back_ex = function
117 | CTL.False
-> CTL.False
118 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
120 let ctl_ef = function
122 | CTL.False
-> CTL.False
123 | x
-> CTL.EF
(CTL.FORWARD
,x
)
125 let ctl_ag s
= function
127 | CTL.False
-> CTL.False
128 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
131 match (x
,!exists) with
132 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
133 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
134 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
135 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
137 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
139 (match (x
,!exists) with
140 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
141 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
142 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
143 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
145 let ctl_uncheck = function
147 | CTL.False
-> CTL.False
150 let label_pred_maker = function
152 | Some
(label_var
,used
) ->
154 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
156 let bclabel_pred_maker = function
158 | Some
(label_var
,used
) ->
160 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
162 (* label used to be used here, but it is not used; label is only needed after
164 let predmaker guard pred label
= CTL.Pred pred
166 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
167 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
168 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
169 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
170 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
171 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
172 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
173 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
174 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
175 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
176 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
177 let loopfallpred = predmaker false (Lib_engine.LoopFallThrough
, CTL.Control
)
179 (*let aftret label_var =
180 ctl_or (aftpred label_var)
181 (ctl_or (loopfallpred label_var) (exitpred label_var))*)
187 Printf.sprintf
"r%d" cur
189 (* --------------------------------------------------------------------- *)
190 (* --------------------------------------------------------------------- *)
191 (* Eliminate OptStm *)
193 (* for optional thing with nothing after, should check that the optional thing
194 never occurs. otherwise the matching stops before it occurs *)
197 let donothing r k e
= k e
in
200 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
203 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
206 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
208 let inheritedlist l
=
209 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
212 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
215 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
217 let rec dots_list unwrapped wrapped
=
218 match (unwrapped
,wrapped
) with
221 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
223 | (Ast.Nest
(_
,_
,_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)
225 d0
::s
::d1
::rest
) -> (* why no case for nest as u? *)
226 let l = Ast.get_line stm
in
227 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
228 let new_rest2 = dots_list urest rest
in
229 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
230 varlists new_rest1 in
231 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
232 varlists new_rest2 in
236 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
238 Ast.free_vars
= fv_rest1
;
239 Ast.minus_free_vars
= mfv_rest1
;
240 Ast.fresh_vars
= fresh_rest1
;
241 Ast.inherited
= inherited_rest1
;
242 Ast.saved_witness
= s1
};
243 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
245 Ast.free_vars
= fv_rest2
;
246 Ast.minus_free_vars
= mfv_rest2
;
247 Ast.fresh_vars
= fresh_rest2
;
248 Ast.inherited
= inherited_rest2
;
249 Ast.saved_witness
= s2
}])) with
251 Ast.free_vars
= fv_rest1
;
252 Ast.minus_free_vars
= mfv_rest1
;
253 Ast.fresh_vars
= fresh_rest1
;
254 Ast.inherited
= inherited_rest1
;
255 Ast.saved_witness
= s1
}]
257 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
258 let l = Ast.get_line stm
in
259 let new_rest1 = dots_list urest rest
in
260 let new_rest2 = stm
::new_rest1 in
261 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
262 varlists new_rest1 in
263 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
264 varlists new_rest2 in
267 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
269 Ast.free_vars
= fv_rest2
;
270 Ast.minus_free_vars
= mfv_rest2
;
271 Ast.fresh_vars
= fresh_rest2
;
272 Ast.inherited
= inherited_rest2
;
273 Ast.saved_witness
= s2
};
274 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
276 Ast.free_vars
= fv_rest1
;
277 Ast.minus_free_vars
= mfv_rest1
;
278 Ast.fresh_vars
= fresh_rest1
;
279 Ast.inherited
= inherited_rest1
;
280 Ast.saved_witness
= s1
}])) with
282 Ast.free_vars
= fv_rest2
;
283 Ast.minus_free_vars
= mfv_rest2
;
284 Ast.fresh_vars
= fresh_rest2
;
285 Ast.inherited
= inherited_rest2
;
286 Ast.saved_witness
= s2
}]
288 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
289 let l = Ast.get_line stm
in
290 let fv_stm = Ast.get_fvs stm
in
291 let mfv_stm = Ast.get_mfvs stm
in
292 let fresh_stm = Ast.get_fresh stm
in
293 let inh_stm = Ast.get_inherited stm
in
294 let saved_stm = Ast.get_saved stm
in
295 let fv_d1 = Ast.get_fvs d1
in
296 let mfv_d1 = Ast.get_mfvs d1
in
297 let fresh_d1 = Ast.get_fresh d1
in
298 let inh_d1 = Ast.get_inherited d1
in
299 let saved_d1 = Ast.get_saved d1
in
300 let fv_both = Common.union_set
fv_stm fv_d1 in
301 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
302 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
303 let inh_both = Common.union_set
inh_stm inh_d1 in
304 let saved_both = Common.union_set
saved_stm saved_d1 in
308 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
310 Ast.free_vars
= fv_stm;
311 Ast.minus_free_vars
= mfv_stm;
312 Ast.fresh_vars
= fresh_stm;
313 Ast.inherited
= inh_stm;
314 Ast.saved_witness
= saved_stm};
315 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
317 Ast.free_vars
= fv_d1;
318 Ast.minus_free_vars
= mfv_d1;
319 Ast.fresh_vars
= fresh_d1;
320 Ast.inherited
= inh_d1;
321 Ast.saved_witness
= saved_d1}])) with
323 Ast.free_vars
= fv_both;
324 Ast.minus_free_vars
= mfv_both;
325 Ast.fresh_vars
= fresh_both;
326 Ast.inherited
= inh_both;
327 Ast.saved_witness
= saved_both}]
329 | ([Ast.Nest
(_
,_
,_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
330 let l = Ast.get_line stm
in
331 let rw = Ast.rewrap stm
in
332 let rwd = Ast.rewrap stm
in
333 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
335 [rwd(Ast.DOTS
([stm
]));
336 {(Ast.make_term
(Ast.DOTS
([rw dots])))
337 with Ast.node_line
= l}])]
339 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
340 | _
-> failwith
"not possible" in
342 let stmtdotsfn r k d
=
345 (match Ast.unwrap
d with
346 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
347 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
348 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
351 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
352 donothing donothing stmtdotsfn donothing donothing
353 donothing donothing donothing donothing donothing donothing donothing
354 donothing donothing donothing donothing donothing
356 (* --------------------------------------------------------------------- *)
357 (* after management *)
358 (* We need Guard for the following case:
367 Here the inner <... b ...> should not go past foo. But foo is not the
368 "after" of the body of the outer nest, because we don't want to search for
369 it in the case where the body of the outer nest ends in something other
370 than dots or a nest. *)
372 (* what is the difference between tail and end??? *)
374 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
376 let a2n = function After x
-> Guard x
| a
-> a
379 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
380 let pp_meta (_
,x
) = Common.pp x
in
381 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
382 Format.print_newline
()
384 let print_after = function
385 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
386 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
387 | Tail
-> Printf.printf
"Tail\n"
388 | VeryEnd
-> Printf.printf
"Very End\n"
389 | End
-> Printf.printf
"End\n"
391 (* --------------------------------------------------------------------- *)
394 let fresh_var _
= string2var "_v"
395 let fresh_pos _
= string2var "_pos" (* must be a constant *)
397 let fresh_metavar _
= "_S"
399 (* fvinfo is going to end up being from the whole associated statement.
400 it would be better if it were just the free variables in d, but free_vars.ml
401 doesn't keep track of free variables on + code *)
402 let make_meta_rule_elem d fvinfo
=
403 let nm = fresh_metavar() in
404 Ast.make_meta_rule_elem nm d fvinfo
406 let get_unquantified quantified vars
=
407 List.filter
(function x
-> not
(List.mem x quantified
)) vars
409 let make_seq guard
l =
410 let s = guard_to_strict guard
in
411 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
413 let make_seq_after2 guard first rest
=
414 let s = guard_to_strict guard
in
416 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
419 let make_seq_after guard first rest
=
421 After rest
-> make_seq guard
[first
;rest
]
424 let opt_and guard first rest
=
425 let s = guard_to_strict guard
in
428 | Some first
-> ctl_and s first rest
430 let and_after guard first rest
=
431 let s = guard_to_strict guard
in
432 match rest
with After rest
-> ctl_and s first rest
| _
-> first
435 let bind x y
= x
or y
in
436 let option_default = false in
437 let mcode r
(_
,_
,kind
,metapos
) =
439 Ast.MINUS
(_
,_
,_
,_
) -> true
440 | Ast.PLUS _
-> failwith
"not possible"
441 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
442 let do_nothing r k e
= k e
in
443 let rule_elem r k re
=
445 match Ast.unwrap re
with
446 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
447 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
448 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
452 match Ast.unwrap i
with
453 Ast.StrInitList
(allminus
,_
,_
,_
,_
) -> allminus
or res
456 V.combiner
bind option_default
457 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
458 do_nothing do_nothing do_nothing do_nothing do_nothing
459 do_nothing do_nothing do_nothing do_nothing init do_nothing
460 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
461 recursor.V.combiner_rule_elem
464 let bind x y
= x
or y
in
465 let option_default = false in
466 let mcode r
(_
,_
,kind
,metapos
) =
468 Ast.MetaPos
(_
,_
,_
,_
,_
) -> true
469 | Ast.NoMetaPos
-> false in
470 let do_nothing r k e
= k e
in
471 let rule_elem r k re
=
473 match Ast.unwrap re
with
474 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
475 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
476 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
479 V.combiner
bind option_default
480 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
481 do_nothing do_nothing do_nothing do_nothing do_nothing
482 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
483 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
484 recursor.V.combiner_rule_elem
486 (* code is not a DisjRuleElem *)
487 let make_match label guard code
=
488 let v = fresh_var() in
489 let matcher = Lib_engine.Match
(code
) in
490 if contains_modif code
&& not guard
491 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
493 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
494 (match (iso_info,!onlyModif,guard
,
495 intersect !used_after (Ast.get_fvs code
)) with
496 (false,true,_
,[]) | (_
,_
,true,_
) ->
497 predmaker guard
(matcher,CTL.Control
) label
498 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
500 let make_raw_match label guard code
=
501 match intersect !used_after (Ast.get_fvs code
) with
502 [] -> predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
504 let v = fresh_var() in
505 CTL.Exists
(true,v,predmaker guard
(Lib_engine.Match
(code
),CTL.UnModif
v)
508 let rec seq_fvs quantified
= function
511 let t1fvs = get_unquantified quantified fv1
in
513 List.fold_left
Common.union_set
[]
514 (List.map
(get_unquantified quantified
) fvs
) in
515 let bothfvs = Common.inter_set
t1fvs termfvs in
516 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
517 let new_quantified = Common.union_set
bothfvs quantified
in
518 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
523 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
525 let non_saved_quantify =
527 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
529 let intersectll lst nested_list
=
530 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
532 (* --------------------------------------------------------------------- *)
533 (* Count depth of braces. The translation of a closed brace appears deeply
534 nested within the translation of the sequence term, so the name of the
535 paren var has to take into account the names of the nested braces. On the
536 other hand the close brace does not escape, so we don't have to take into
537 account other paren variable names. *)
539 (* called repetitively, which is inefficient, but less trouble than adding a
540 new field to Seq and FunDecl *)
541 let count_nested_braces s =
542 let bind x y
= max x y
in
543 let option_default = 0 in
544 let stmt_count r k
s =
545 match Ast.unwrap
s with
546 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
548 let donothing r k e
= k e
in
550 let recursor = V.combiner
bind option_default
551 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
552 donothing donothing donothing donothing donothing
553 donothing donothing donothing donothing donothing donothing
554 donothing donothing stmt_count donothing donothing donothing in
555 let res = string_of_int
(recursor.V.combiner_statement
s) in
559 let get_label_ctr _
=
560 let cur = !labelctr in
562 string2var (Printf.sprintf
"l%d" cur)
564 (* --------------------------------------------------------------------- *)
565 (* annotate dots with before and after neighbors *)
567 let print_bef_aft = function
569 Printf.printf
"bef/aft\n";
570 Pretty_print_cocci.rule_elem "" re
;
571 Format.print_newline
()
573 Printf.printf
"bef/aft\n";
574 Pretty_print_cocci.statement
"" s;
575 Format.print_newline
()
576 | Ast.Other_dots
d ->
577 Printf.printf
"bef/aft\n";
578 Pretty_print_cocci.statement_dots
d;
579 Format.print_newline
()
581 (* [] can only occur if we are in a disj, where it comes from a ? In that
582 case, we want to use a, which accumulates all of the previous patterns in
584 let rec get_before_elem sl a
=
585 match Ast.unwrap sl
with
589 [] -> ([],Common.Right a
)
591 let (e
,ea
) = get_before_e e a
in
594 let (e
,ea
) = get_before_e e a
in
595 let (sl
,sla
) = loop sl ea
in
597 let (l,a
) = loop x a
in
598 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
599 | Ast.CIRCLES
(x
) -> failwith
"not supported"
600 | Ast.STARS
(x
) -> failwith
"not supported"
602 and get_before sl a
=
603 match get_before_elem sl a
with
604 (term
,Common.Left x
) -> (term
,x
)
605 | (term
,Common.Right x
) -> (term
,x
)
607 and get_before_whencode wc
=
610 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
611 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
612 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
613 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
614 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
617 and get_before_e
s a
=
618 match Ast.unwrap
s with
619 Ast.Dots
(d,w
,_
,aft
) ->
620 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
621 | Ast.Nest
(starter
,stmt_dots
,ender
,w
,multi
,_
,aft
) ->
622 let w = get_before_whencode
w in
623 let (sd
,_
) = get_before stmt_dots a
in
625 got rid of this, don't want to let nests overshoot
630 Unify_ast.unify_statement_dots
631 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
633 Unify_ast.MAYBE -> false
635 | Ast.Other_dots a ->
636 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
638 Unify_ast.MAYBE -> false
642 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,a,aft
)),
643 [Ast.Other_dots stmt_dots
])
644 | Ast.Disj
(stmt_dots_list
) ->
646 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
647 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
649 (match Ast.unwrap ast
with
650 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
651 | _
-> (s,[Ast.Other
s]))
652 | Ast.Seq
(lbrace
,body
,rbrace
) ->
653 let index = count_nested_braces s in
654 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
655 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
656 | Ast.Define
(header
,body
) ->
657 let (body
,_
) = get_before body
[] in
658 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
659 | Ast.IfThen
(ifheader
,branch
,aft
) ->
660 let (br
,_
) = get_before_e branch
[] in
661 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
662 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
663 let (br1
,_
) = get_before_e branch1
[] in
664 let (br2
,_
) = get_before_e branch2
[] in
665 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
666 | Ast.While
(header
,body
,aft
) ->
667 let (bd
,_
) = get_before_e body
[] in
668 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
669 | Ast.For
(header
,body
,aft
) ->
670 let (bd
,_
) = get_before_e body
[] in
671 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
672 | Ast.Do
(header
,body
,tail
) ->
673 let (bd
,_
) = get_before_e body
[] in
674 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
675 | Ast.Iterator
(header
,body
,aft
) ->
676 let (bd
,_
) = get_before_e body
[] in
677 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
678 | Ast.Switch
(header
,lb
,decls
,cases
,rb
) ->
679 let index = count_nested_braces s in
680 let (de
,dea
) = get_before decls
[Ast.WParen
(lb
,index)] in
683 (function case_line
->
684 match Ast.unwrap case_line
with
685 Ast.CaseLine
(header
,body
) ->
686 let (body
,_
) = get_before body
[] in
687 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
688 | Ast.OptCase
(case_line
) -> failwith
"not supported")
690 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),
691 [Ast.WParen
(rb
,index)])
692 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
693 let (bd
,_
) = get_before body
[] in
694 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
696 Pretty_print_cocci.statement
"" s; Format.print_newline
();
697 failwith
"get_before_e: not supported"
699 let rec get_after sl
a =
700 match Ast.unwrap sl
with
706 let (sl
,sla
) = loop sl
in
707 let (e
,ea
) = get_after_e e sla
in
709 let (l,a) = loop x
in
710 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
711 | Ast.CIRCLES
(x
) -> failwith
"not supported"
712 | Ast.STARS
(x
) -> failwith
"not supported"
714 and get_after_whencode
a wc
=
717 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
718 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
719 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
720 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
721 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
724 and get_after_e
s a =
725 match Ast.unwrap
s with
726 Ast.Dots
(d,w,bef
,_
) ->
727 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
728 | Ast.Nest
(starter
,stmt_dots
,ender
,w,multi
,bef
,_
) ->
729 let w = get_after_whencode
a w in
730 let (sd
,_
) = get_after stmt_dots
a in
732 got rid of this. don't want to let nests overshoot
737 Unify_ast.unify_statement_dots
738 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
740 Unify_ast.MAYBE -> false
742 | Ast.Other_dots a ->
743 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
745 Unify_ast.MAYBE -> false
749 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,bef
,a)),
750 [Ast.Other_dots stmt_dots
])
751 | Ast.Disj
(stmt_dots_list
) ->
753 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
754 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
756 (match Ast.unwrap ast
with
757 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
758 (* check "after" information for metavar optimization *)
759 (* if the error is not desired, could just return [], then
760 the optimization (check for EF) won't take place *)
764 (match Ast.unwrap x
with
765 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
767 "dots/nest not allowed before and after stmt metavar"
769 | Ast.Other_dots x
->
770 (match Ast.undots x
with
772 (match Ast.unwrap x
with
773 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
775 ("dots/nest not allowed before and after stmt "^
784 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
785 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
786 | _
-> (s,[Ast.Other
s]))
787 | Ast.Seq
(lbrace
,body
,rbrace
) ->
788 let index = count_nested_braces s in
789 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
790 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
791 [Ast.WParen
(lbrace
,index)])
792 | Ast.Define
(header
,body
) ->
793 let (body
,_
) = get_after body
a in
794 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
795 | Ast.IfThen
(ifheader
,branch
,aft
) ->
796 let (br
,_
) = get_after_e branch
a in
797 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
798 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
799 let (br1
,_
) = get_after_e branch1
a in
800 let (br2
,_
) = get_after_e branch2
a in
801 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
802 | Ast.While
(header
,body
,aft
) ->
803 let (bd
,_
) = get_after_e body
a in
804 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
805 | Ast.For
(header
,body
,aft
) ->
806 let (bd
,_
) = get_after_e body
a in
807 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
808 | Ast.Do
(header
,body
,tail
) ->
809 let (bd
,_
) = get_after_e body
a in
810 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
811 | Ast.Iterator
(header
,body
,aft
) ->
812 let (bd
,_
) = get_after_e body
a in
813 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
814 | Ast.Switch
(header
,lb
,decls
,cases,rb
) ->
815 let index = count_nested_braces s in
818 (function case_line
->
819 match Ast.unwrap case_line
with
820 Ast.CaseLine
(header
,body
) ->
821 let (body
,_
) = get_after body
[Ast.WParen
(rb
,index)] in
822 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
823 | Ast.OptCase
(case_line
) -> failwith
"not supported")
825 let (de
,_
) = get_after decls
[] in
826 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),[Ast.WParen
(lb
,index)])
827 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
828 let (bd
,_
) = get_after body
[] in
829 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
830 | _
-> failwith
"get_after_e: not supported"
832 let preprocess_dots sl
=
833 let (sl
,_
) = get_before sl
[] in
834 let (sl
,_
) = get_after sl
[] in
837 let preprocess_dots_e sl
=
838 let (sl
,_
) = get_before_e sl
[] in
839 let (sl
,_
) = get_after_e sl
[] in
842 (* --------------------------------------------------------------------- *)
843 (* various return_related things *)
845 let rec ends_in_return stmt_list
=
846 match Ast.unwrap stmt_list
with
848 (match List.rev x
with
850 (match Ast.unwrap x
with
853 match Ast.unwrap x
with
854 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
855 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
858 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
861 | Ast.CIRCLES
(x
) -> failwith
"not supported"
862 | Ast.STARS
(x
) -> failwith
"not supported"
864 (* --------------------------------------------------------------------- *)
867 let exptymatch l make_match make_guard_match
=
868 let pos = fresh_pos() in
869 let matches_guard_matches =
872 let pos = Ast.make_mcode
pos in
873 (make_match (Ast.set_pos x
(Some
pos)),
874 make_guard_match
(Ast.set_pos x
(Some
pos))))
876 let (matches
,guard_matches
) = List.split
matches_guard_matches in
877 let rec suffixes = function
879 | x
::xs -> xs::(suffixes xs) in
881 (* normally, we check that an expression does not match something
882 earlier in the disjunction (calculated as prefixes). But for large
883 disjunctions, this can result in a very big CTL formula. So we
884 give the user the option to say he doesn't want this feature, if that is
886 if !Flag_matcher.no_safe_expressions
887 then List.map
(function _
-> []) matches
888 else List.rev
(suffixes (List.rev guard_matches
)) in
889 let info = (* not null *)
895 ctl_and CTL.NONSTRICT
matcher
897 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
899 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
901 (* code might be a DisjRuleElem, in which case we break it apart
902 code might contain an Exp or Ty
903 this one pushes the quantifier inwards *)
904 let do_re_matches label guard
res quantified minus_quantified
=
905 let make_guard_match x
=
906 let stmt_fvs = Ast.get_mfvs x
in
907 let fvs = get_unquantified minus_quantified
stmt_fvs in
908 non_saved_quantify fvs (make_match None
true x
) in
910 let stmt_fvs = Ast.get_fvs x
in
911 let fvs = get_unquantified quantified
stmt_fvs in
912 quantify guard
fvs (make_match None guard x
) in
913 (* label used to be used here, but it is not use; label is only needed after
915 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
916 (match List.map
Ast.unwrap
res with
917 [] -> failwith
"unexpected empty disj"
918 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
919 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
921 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
923 then failwith
"unexpected exp or ty";
924 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
926 (* code might be a DisjRuleElem, in which case we break it apart
927 code doesn't contain an Exp or Ty
928 this one is for use when it is not practical to push the quantifier inwards
930 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
931 match Ast.unwrap code
with
932 Ast.DisjRuleElem
(res) ->
933 let make_match = make_match None guard
in
934 let orop = if guard
then ctl_or else ctl_seqor in
935 (* label used to be used here, but it is not use; label is only needed after
937 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
938 (List.fold_left
orop CTL.False
(List.map
make_match res))
939 | _
-> make_match label guard code
941 (* --------------------------------------------------------------------- *)
942 (* control structures *)
944 let end_control_structure fvs header body after_pred
945 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
946 (* aft indicates what is added after the whole if, which has to be added
948 let (aft_needed
,after_branch
) =
950 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
951 (false,make_seq_after2 guard after_pred after
)
954 make_match label guard
955 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
957 make_seq_after guard after_pred
958 (After
(make_seq_after guard
match_endif after
))) in
959 let body = body after_branch
in
960 let s = guard_to_strict guard
in
965 (match (after
,aft_needed
) with
966 (After _
,_
) (* pattern doesn't end here *)
967 | (_
,true) (* + code added after *) -> after_checks
968 | _
-> no_after_checks
)
969 (ctl_ax_absolute s body)))
971 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
972 quantified minus_quantified label llabel slabel recurse
make_match guard
=
973 (* "if (test) thn" becomes:
974 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
976 "if (test) thn; after" becomes:
977 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
982 match seq_fvs quantified
983 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
984 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
985 | _
-> failwith
"not possible" in
986 let new_quantified = Common.union_set bfvs quantified
in
988 match seq_fvs minus_quantified
989 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
990 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
991 | _
-> failwith
"not possible" in
992 let new_mquantified = Common.union_set mbfvs minus_quantified
in
994 let if_header = quantify guard efvs
(make_match ifheader
) in
995 (* then branch and after *)
996 let lv = get_label_ctr() in
997 let used = ref false in
999 (* no point to put a label on truepred etc; it is local to this construct
1000 so it must have the same label *)
1002 [truepred None
; recurse branch Tail
new_quantified new_mquantified
1003 (Some
(lv,used)) llabel slabel guard
] in
1004 let after_pred = aftpred None
in
1005 let or_cases after_branch
=
1006 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
1007 let (if_header,wrapper
) =
1010 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1011 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1012 (function body -> quantify true [lv] body))
1013 else (if_header,function x
-> x
) in
1015 (end_control_structure bfvs
if_header or_cases after_pred
1016 (Some
(ctl_ex after_pred)) None aft after label guard
)
1018 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
1019 quantified minus_quantified label llabel slabel recurse
make_match guard
=
1020 (* "if (test) thn else els" becomes:
1021 if(test) & AX((TrueBranch & AX thn) v
1022 (FalseBranch & AX (else & AX els)) v After)
1025 "if (test) thn else els; after" becomes:
1026 if(test) & AX((TrueBranch & AX thn) v
1027 (FalseBranch & AX (else & AX els)) v
1028 (After & AXAX after))
1032 (* free variables *)
1033 let (e1fvs
,b1fvs
,s1fvs
) =
1034 match seq_fvs quantified
1035 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1036 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1037 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1038 | _
-> failwith
"not possible" in
1039 let (e2fvs
,b2fvs
,s2fvs
) =
1041 (* just combine with the else branch. no point to have separate
1042 quantifier, since there is only one possible control-flow path *)
1043 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1044 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1045 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1046 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1047 | _
-> failwith
"not possible" in
1048 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1049 let exponlyfvs = intersect e1fvs e2fvs
in
1050 let new_quantified = union bothfvs quantified
in
1051 (* minus free variables *)
1052 let (me1fvs
,mb1fvs
,ms1fvs
) =
1053 match seq_fvs minus_quantified
1054 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1055 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1056 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1057 | _
-> failwith
"not possible" in
1058 let (me2fvs
,mb2fvs
,ms2fvs
) =
1060 (* just combine with the else branch. no point to have separate
1061 quantifier, since there is only one possible control-flow path *)
1063 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1064 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1065 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1066 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1067 | _
-> failwith
"not possible" in
1068 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1069 let new_mquantified = union mbothfvs minus_quantified
in
1071 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1072 (* then and else branches *)
1073 let lv = get_label_ctr() in
1074 let used = ref false in
1077 [truepred None
; recurse branch1 Tail
new_quantified new_mquantified
1078 (Some
(lv,used)) llabel slabel guard
] in
1083 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1084 (header_match None guard els
);
1085 recurse branch2 Tail
new_quantified new_mquantified
1086 (Some
(lv,used)) llabel slabel guard
] in
1087 let after_pred = aftpred None
in
1088 let or_cases after_branch
=
1089 ctl_or true_branch (ctl_or false_branch after_branch
) in
1090 let s = guard_to_strict guard
in
1091 let (if_header,wrapper
) =
1094 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1095 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1096 (function body -> quantify true [lv] body))
1097 else (if_header,function x
-> x
) in
1099 (end_control_structure bothfvs if_header or_cases after_pred
1100 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1101 (Some
(ctl_ex (falsepred None
)))
1102 aft after label guard
)
1104 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1105 quantified minus_quantified label recurse
make_match guard
=
1107 (* the translation in this case is similar to that of an if with no else *)
1108 (* free variables *)
1110 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1111 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1112 | _
-> failwith
"not possible" in
1113 let new_quantified = Common.union_set bfvs quantified
in
1114 (* minus free variables *)
1116 match seq_fvs minus_quantified
1117 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1118 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1119 | _
-> failwith
"not possible" in
1120 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1122 let header = quantify guard efvs
(make_match header) in
1123 let lv = get_label_ctr() in
1124 let used = ref false in
1128 recurse
body Tail
new_quantified new_mquantified
1129 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1130 let after_pred = loopfallpred None
in
1131 let or_cases after_branch
= ctl_or body after_branch
in
1132 let (header,wrapper
) =
1135 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1136 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1137 (function body -> quantify true [lv] body))
1138 else (header,function x
-> x
) in
1140 (end_control_structure bfvs
header or_cases after_pred
1141 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1142 match (Ast.unwrap
body,aft
) with
1143 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1144 (match Ast.unwrap re
with
1145 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1146 Type_cocci.Unitary
,_
,false)
1147 when after
= Tail
or after
= End
or after
= VeryEnd
->
1149 match seq_fvs quantified
[Ast.get_fvs
header] with
1151 | _
-> failwith
"not possible" in
1152 quantify guard efvs
(make_match header)
1156 (* --------------------------------------------------------------------- *)
1157 (* statement metavariables *)
1159 (* issue: an S metavariable that is not an if branch/loop body
1160 should not match an if branch/loop body, so check that the labels
1161 of the nodes before the first node matched by the S are different
1162 from the label of the first node matched by the S *)
1163 let sequencibility body label_pred process_bef_aft
= function
1164 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1167 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1168 | Ast.SequencibleAfterDots
l ->
1169 (* S appears after some dots. l is the code that comes after the S.
1170 want to search for that first, because S can match anything, while
1171 the stuff after is probably more restricted *)
1172 let afts = List.map process_bef_aft
l in
1173 let ors = foldl1 ctl_or afts in
1174 ctl_and CTL.NONSTRICT
1175 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1178 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1179 | Ast.NotSequencible
-> body (function x
-> x
)
1181 let svar_context_with_add_after stmt
s label quantified
d ast
1182 seqible after process_bef_aft guard fvinfo
=
1183 let label_var = (*fresh_label_var*) string2var "_lab" in
1185 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1186 (*let prelabel_pred =
1187 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
1188 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1189 let full_metamatch = matcher d in
1190 let first_metamatch =
1193 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
,c
)) ->
1194 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
,c
))
1195 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1196 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1198 let middle_metamatch =
1201 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1202 | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
1204 let last_metamatch =
1207 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
,c
)) ->
1208 Ast.CONTEXT
(pos,Ast.AFTER
(aft
,c
))
1209 | Ast.CONTEXT
(_
,_
) -> d
1210 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1214 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1217 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1218 let left_or = (* the whole statement is one node *)
1219 make_seq_after guard
1220 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_ex to_end)) full_metamatch) after
in
1221 let right_or = (* the statement covers multiple nodes *)
1222 ctl_and CTL.NONSTRICT
1225 [to_end; make_seq_after guard
last_metamatch after
]))
1231 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1235 ctl_au CTL.NONSTRICT
1238 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1240 (ctl_not prelabel_pred) after])] in
1244 ctl_and CTL.NONSTRICT
label_pred
1245 (f
(ctl_and CTL.NONSTRICT
1246 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1247 let stmt_fvs = Ast.get_fvs stmt
in
1248 let fvs = get_unquantified quantified
stmt_fvs in
1249 quantify guard
(label_var::fvs)
1250 (sequencibility body label_pred process_bef_aft seqible
)
1252 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1253 seqible after process_bef_aft guard fvinfo
=
1254 let label_var = (*fresh_label_var*) string2var "_lab" in
1256 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1258 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1259 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1261 match (d,after
) with
1262 (Ast.PLUS _
, _
) -> failwith
"not possible"
1263 | (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1264 (* just match the root. don't care about label; always ok *)
1265 make_raw_match None
false ast
1266 | (Ast.CONTEXT
(pos,Ast.BEFORE
(_
,_
)),(Tail
|End
|VeryEnd
)) ->
1267 ctl_and CTL.NONSTRICT
1268 (make_raw_match None
false ast
) (* statement *)
1269 (matcher d) (* transformation *)
1270 | (Ast.CONTEXT
(pos,(Ast.NOTHING
|Ast.BEFORE
(_
,_
))),(After
a | Guard
a)) ->
1271 (* This case and the MINUS one couldprobably be merged, if
1272 HackForStmt were to notice when its arguments are trivial *)
1273 let first_metamatch = matcher d in
1274 (* try to follow after link *)
1275 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1277 ctl_ex(make_seq guard
[to_end; CTL.True
; a]) in
1279 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1280 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1281 (ctl_and CTL.NONSTRICT
1282 first_metamatch (ctl_or is_compound not_compound))
1283 | (Ast.CONTEXT
(pos,(Ast.AFTER _
|Ast.BEFOREAFTER _
)),_
) ->
1284 failwith
"not possible"
1285 | (Ast.MINUS
(pos,inst
,adj
,l),after
) ->
1286 let (first_metamatch,last_metamatch,rest_metamatch
) =
1288 [] -> (matcher(Ast.CONTEXT
(pos,Ast.NOTHING
)),CTL.True
,matcher d)
1290 matcher(Ast.MINUS
(pos,inst
,adj
,[])),
1291 ctl_and CTL.NONSTRICT
1292 (ctl_not (make_raw_match label
false ast
))
1293 (matcher(Ast.MINUS
(pos,inst
,adj
,[])))) in
1294 (* try to follow after link *)
1295 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1299 [to_end; make_seq_after guard
last_metamatch after
]) in
1301 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1302 ctl_and CTL.NONSTRICT
1303 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1304 (ctl_and CTL.NONSTRICT
1305 first_metamatch (ctl_or is_compound not_compound)))
1306 (* don't have to put anything before the beginning, so don't have to
1307 distinguish the first node. so don't have to bother about paths,
1308 just use the label. label ensures that found nodes match up with
1309 what they should because it is in the lhs of the andany. *)
1310 (CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1311 ctl_and CTL.NONSTRICT
label_pred
1312 (make_raw_match label
false ast
),
1313 ctl_and CTL.NONSTRICT rest_metamatch
prelabel_pred))
1315 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1316 let stmt_fvs = Ast.get_fvs stmt
in
1317 let fvs = get_unquantified quantified
stmt_fvs in
1318 quantify guard
(label_var::fvs)
1319 (sequencibility body label_pred process_bef_aft seqible
)
1321 (* --------------------------------------------------------------------- *)
1322 (* dots and nests *)
1324 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1325 let matchgoto = gotopred None
in
1327 make_match None
false
1329 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1331 make_match None
false
1333 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1335 if quantifier
= Exists
1336 then Common.Left
(CTL.False
)
1338 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1340 then Common.Left
(aftpred label
)
1343 (function vx
-> function v ->
1344 (* vx is the contents of the nest, if any. we can only stop early
1345 if we find neither the ending code nor the nest contents in
1346 the if branch. not sure if this is a good idea. *)
1347 let lv = get_label_ctr() in
1348 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1349 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1351 (* Rather a special case. But if the code afterwards is just
1352 a } then there is no point checking after a goto that it does
1354 (* this optimization doesn't work. probably depends on whether
1355 the destination of the break/goto is local or more global than
1357 match seq_after
with
1359 let is_paren = function
1360 CTL.Pred
(Lib_engine.Paren _
,_
) -> true
1362 is_paren e1
or is_paren e2
1364 ctl_or (aftpred label
)
1365 (quantify false [lv]
1366 (ctl_and CTL.NONSTRICT
1367 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1368 (ctl_au CTL.NONSTRICT
1369 (ctl_and CTL.NONSTRICT
(ctl_not v)
1370 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1371 (ctl_and CTL.NONSTRICT
preflabelpred
1372 (if !Flag_matcher.only_return_is_error_exit
1374 (ctl_and CTL.NONSTRICT
1375 (retpred None
) (ctl_not seq_after
))
1378 (ctl_and CTL.NONSTRICT
1379 (ctl_or (retpred None
) matchcontinue)
1380 (ctl_not seq_after
))
1381 (ctl_and CTL.NONSTRICT
1382 (ctl_or matchgoto matchbreak)
1384 (* an optim that failed see defn is_paren
1385 and tests/makes_a_loop *)
1389 (ctl_not seq_after
))))))))))) in
1390 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1391 let v = get_let_ctr() in
1393 (match stop_early with
1394 Common.Left x1
-> ctl_or y x1
1395 | Common.Right
stop_early ->
1398 (ctl_and CTL.NONSTRICT
(label_pred_maker label
)
1399 (stop_early n
(CTL.Ref
v)))))
1401 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1402 process_bef_aft statement_list statement guard quantified wrapcode
=
1403 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1404 (* proces bef_aft *)
1406 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1407 let bef_aft = (* to be negated *)
1411 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1414 with Not_found
-> shortest (Common.union_set bef aft
) in
1417 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1419 let check_quantifier quant other
=
1421 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1425 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1427 then failwith
"inconsistent annotation on dots"
1431 if check_quantifier Ast.WhenExists
Ast.WhenForall
1434 if check_quantifier Ast.WhenForall
Ast.WhenExists
1437 (* the following is used when we find a goto, etc and consider accepting
1438 without finding the rest of the pattern *)
1439 let aft = shortest aft in
1440 (* process whencode *)
1441 let labelled = label_pred_maker label
in
1443 let (poswhen
,negwhen
) =
1445 (function (poswhen
,negwhen
) ->
1447 Ast.WhenNot
whencodes ->
1448 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1449 | Ast.WhenAlways stm
->
1450 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1451 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1452 | Ast.WhenNotTrue
(e
) ->
1454 ctl_or (whencond_true e label guard quantified
) negwhen
)
1455 | Ast.WhenNotFalse
(e
) ->
1457 ctl_or (whencond_false e label guard quantified
) negwhen
))
1458 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1459 (*bef_aft modifies arg so that inside of a nest can't cause the next
1460 to overshoot its boundaries, eg a() <...f()...> b() where f is
1461 a metavariable and the whole thing matches code in a loop;
1462 don't want f to match eg b(), allowing to go around the loop again*)
1463 let poswhen = ctl_and_ns arg
poswhen in
1467 (* add in After, because it's not part of the program *)
1468 ctl_or (aftpred label
) negwhen
1470 ctl_and_ns poswhen (ctl_not negwhen) in
1471 (* process dot code, if any *)
1473 match (dotcode,guard
) with
1474 (None
,_) | (_,true) -> CTL.True
1475 | (Some
dotcode,_) -> dotcode in
1476 (* process nest code, if any *)
1477 (* whencode goes in the negated part of the nest; if no nest, just goes
1478 on the "true" in between code *)
1479 let plus_var = if plus
then get_label_ctr() else string2var "" in
1480 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1481 let (ornest
,just_nest
) =
1482 (* just_nest is used when considering whether to stop early, to continue
1483 to collect nest information in the if branch *)
1484 match (nest
,guard
&& not plus
) with
1485 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1486 | (Some nest
,false) ->
1487 let v = get_let_ctr() in
1491 (* the idea is that BindGood is sort of a witness; a witness to
1492 having found the subterm in at least one place. If there is
1493 not a witness, then there is a risk that it will get thrown
1494 away, if it is merged with a node that has an empty
1495 environment. See tests/nestplus. But this all seems
1496 rather suspicious *)
1497 CTL.And
(CTL.NONSTRICT
,x
,
1498 CTL.Exists
(true,plus_var2,
1499 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1500 CTL.Modif
plus_var2)))
1504 CTL.Or
(is_plus (CTL.Ref
v),
1505 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1507 let plus_modifier x
=
1514 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1519 (* label within dots is taken care of elsewhere. the next two lines
1520 put the label on the code following dots *)
1521 After f
-> ctl_and (guard_to_strict guard
) f
labelled
1523 (* actually, label should be None based on the only use of Guard... *)
1524 assert (label
= None
);
1525 ctl_and CTL.NONSTRICT
(ctl_uncheck f
) labelled
1527 let exit = endpred label
in
1528 let errorexit = exitpred label
in
1529 ctl_or exit errorexit
1530 (* not at all sure what the next two mean... *)
1534 Some
(lv,used) -> used := true;
1535 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1536 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1537 | None
-> endpred label
)
1538 (* was the following, but not clear why sgrep should allow
1540 let exit = endpred label in
1541 let errorexit = exitpred label in
1543 then ctl_or exit errorexit (* end anywhere *)
1544 else exit (* end at the real end of the function *) *)
in
1546 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1547 label
(guard_to_strict guard
) wrapcode just_nest
1549 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1550 aft ender quantifier)
1552 and get_whencond_exps e
=
1553 match Ast.unwrap e
with
1555 | Ast.DisjRuleElem
(res) ->
1556 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1557 | _ -> failwith
"not possible"
1559 and make_whencond_headers e e1 label guard quantified
=
1560 let fvs = Ast.get_fvs e
in
1562 quantify guard
(get_unquantified quantified
fvs)
1563 (make_match label guard h
) in
1568 (Ast.make_mcode
"if",
1569 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1570 let while_header e1
=
1574 (Ast.make_mcode
"while",
1575 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1580 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1581 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1583 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1585 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1587 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1588 (if_headers, while_headers, for_headers)
1590 and whencond_true e label guard quantified
=
1591 let e1 = get_whencond_exps e
in
1592 let (if_headers, while_headers, for_headers) =
1593 make_whencond_headers e
e1 label guard quantified
in
1595 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1596 (ctl_and CTL.NONSTRICT
1597 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1599 and whencond_false e label guard quantified
=
1600 let e1 = get_whencond_exps e
in
1601 let (if_headers, while_headers, for_headers) =
1602 make_whencond_headers e
e1 label guard quantified
in
1604 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1605 (* if without else *)
1606 (ctl_or (ctl_and CTL.NONSTRICT
(fallpred label
) (ctl_back_ex if_headers))
1607 (* failure of loop test *)
1608 (ctl_and CTL.NONSTRICT
(loopfallpred label
)
1609 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1611 (* --------------------------------------------------------------------- *)
1612 (* the main translation loop *)
1614 let rec statement_list stmt_list after quantified minus_quantified
1615 label llabel slabel dots_before guard
=
1617 (* include Disj to be on the safe side *)
1618 match Ast.unwrap x
with
1619 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1620 let compute_label l e db
= if db
or isdots e
then l else None
in
1621 match Ast.unwrap stmt_list
with
1623 let rec loop quantified minus_quantified dots_before label llabel slabel
1625 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1627 statement e after quantified minus_quantified
1628 (compute_label label e dots_before
)
1630 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1631 let shared = intersectll fv
fvs in
1632 let unqshared = get_unquantified quantified
shared in
1633 let new_quantified = Common.union_set
unqshared quantified
in
1634 let minus_shared = intersectll mfv mfvs
in
1636 get_unquantified minus_quantified
minus_shared in
1637 let new_mquantified =
1638 Common.union_set
munqshared minus_quantified
in
1639 quantify guard
unqshared
1642 (let (label1
,llabel1
,slabel1
) =
1643 match Ast.unwrap e
with
1645 (match Ast.unwrap re
with
1646 Ast.Goto
_ -> (None
,None
,None
)
1647 | _ -> (label
,llabel
,slabel
))
1648 | _ -> (label
,llabel
,slabel
) in
1649 loop new_quantified new_mquantified (isdots e
)
1650 label1 llabel1 slabel1
1652 new_quantified new_mquantified
1653 (compute_label label e dots_before
) llabel slabel guard
)
1654 | _ -> failwith
"not possible" in
1655 loop quantified minus_quantified dots_before
1657 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1658 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1659 | Ast.STARS
(x
) -> failwith
"not supported"
1661 (* llabel is the label of the enclosing loop and slabel is the label of the
1663 and statement stmt after quantified minus_quantified
1664 label llabel slabel guard
=
1665 let ctl_au = ctl_au CTL.NONSTRICT
in
1666 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1667 let ctl_and = ctl_and CTL.NONSTRICT
in
1668 let make_seq = make_seq guard
in
1669 let make_seq_after = make_seq_after guard
in
1670 let real_make_match = make_match in
1671 let make_match = header_match label guard
in
1673 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1676 match Ast.unwrap stmt
with
1678 (match Ast.unwrap ast
with
1679 (* the following optimisation is not a good idea, because when S
1680 is alone, we would like it not to match a declaration.
1681 this makes more matching for things like when (...) S, but perhaps
1682 that matching is not so costly anyway *)
1683 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1684 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_,_)) as d),_),
1686 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_,_)) as d),_),
1688 svar_context_with_add_after stmt
s label quantified
d ast seqible
1690 (process_bef_aft quantified minus_quantified
1691 label llabel slabel
true)
1693 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1695 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1696 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1698 (process_bef_aft quantified minus_quantified
1699 label llabel slabel
true)
1701 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1705 match Ast.unwrap ast
with
1706 Ast.DisjRuleElem
(res) ->
1707 do_re_matches label guard
res quantified minus_quantified
1708 | Ast.Exp
(_) | Ast.Ty
(_) ->
1709 let stmt_fvs = Ast.get_fvs stmt
in
1710 let fvs = get_unquantified quantified
stmt_fvs in
1711 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1713 let stmt_fvs = Ast.get_fvs stmt
in
1714 let fvs = get_unquantified quantified
stmt_fvs in
1715 quantify guard
fvs (make_match ast
) in
1716 match Ast.unwrap ast
with
1717 Ast.Break
(brk
,semi
) ->
1718 (match (llabel
,slabel
) with
1719 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1720 ctl_and term (bclabel_pred_maker slabel
)
1721 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1722 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1723 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1724 (* discard pattern that comes after return *)
1725 let normal_res = make_seq_after term after
in
1726 (* the following code tries to propagate the modifications on
1727 return; to a close brace, in the case where the final return
1730 match (retmc
,semmc
) with
1731 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1732 when !Flag.sgrep_mode2
->
1733 (* in sgrep mode, we can propagate the - *)
1734 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,l1
@l2
))
1735 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
)) ->
1736 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
,Ast.ONE
)))
1737 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
,c1
)),
1738 Ast.CONTEXT
(_,Ast.AFTER
(l2
,c2
))) ->
1739 (if not
(c1
= c2
) then failwith
"bad + code");
1740 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
,c1
)))
1741 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1742 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1744 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1745 Ast.CONTEXT
(_,Ast.AFTER
(l,c
))) ->
1746 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l,c
)))
1748 let ret = Ast.make_mcode
"return" in
1750 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1751 let semi = Ast.make_mcode
";" in
1753 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1755 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1758 let exit = endpred None
in
1760 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1761 let stripped_rbrace =
1762 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1764 (ctl_and (make_match mod_rbrace)
1769 (ctl_or simple_return return_expr))))
1771 (make_match stripped_rbrace)
1772 (* error exit not possible; it is in the middle
1773 of code, so a return is needed *)
1776 (* some change in the middle of the return, so have to
1777 find an actual return *)
1780 (* should try to deal with the dots_bef_aft problem elsewhere,
1781 but don't have the courage... *)
1786 do_between_dots stmt
term End
1787 quantified minus_quantified label llabel slabel guard
in
1789 make_seq_after term after
)
1790 | Ast.Seq
(lbrace
,body,rbrace
) ->
1791 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1794 [Ast.get_fvs lbrace
;
1795 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1797 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1798 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1799 | _ -> failwith
"not possible" in
1800 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1802 seq_fvs minus_quantified
1803 [Ast.get_mfvs lbrace
;
1804 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1806 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1807 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1808 | _ -> failwith
"not possible" in
1809 let pv = count_nested_braces stmt
in
1810 let lv = get_label_ctr() in
1811 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1812 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1815 (quantify guard lbfvs
(make_match lbrace
))
1816 (ctl_and paren_pred label_pred) in
1818 match Ast.unwrap rbrace
with
1819 Ast.SeqEnd
((data
,info,_,pos)) ->
1820 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1821 | _ -> failwith
"unexpected close brace" in
1823 (* label is not needed; paren_pred is enough *)
1824 quantify guard rbfvs
1825 (ctl_au (make_match empty_rbrace)
1827 (real_make_match None guard rbrace
)
1829 let new_quantified2 =
1830 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1831 let new_mquantified2 =
1832 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1833 let pattern_as_given =
1834 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1835 quantify true [pv;lv]
1836 (quantify guard b1fvs
1840 (if !exists = Exists
then CTL.False
else (aftpred label
))
1841 (quantify guard b2fvs
1842 (statement_list body
1843 (After
(make_seq_after end_brace after
))
1844 new_quantified2 new_mquantified2
1845 (Some
(lv,ref true))
1846 llabel slabel
false guard
)))])) in
1847 if ends_in_return body
1849 (* matching error handling code *)
1851 1. The pattern as given
1852 2. A goto, and then some close braces, and then the pattern as
1853 given, but without the braces (only possible if there are no
1854 decls, and open and close braces are unmodified)
1855 3. Part of the pattern as given, then a goto, and then the rest
1856 of the pattern. For this case, we just check that all paths have
1857 a goto within the current braces. checking for a goto at every
1858 point in the pattern seems expensive and not worthwhile. *)
1860 let body = preprocess_dots body in (* redo, to drop braces *)
1864 (make_match empty_rbrace)
1865 (ctl_ax (* skip the destination label *)
1866 (quantify guard b2fvs
1867 (statement_list body End
1868 new_quantified2 new_mquantified2 None llabel slabel
1871 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1872 quantify true [pv;lv]
1873 (quantify guard b1fvs
1877 (CTL.AU
(* want AF even for sgrep *)
1878 (CTL.FORWARD
,CTL.STRICT
,
1879 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1880 ctl_and (* brace must be eventually after goto *)
1881 (gotopred (Some
(lv,ref true)))
1882 (* want AF even for sgrep *)
1883 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1884 (quantify guard b2fvs
1885 (statement_list body Tail
1886 new_quantified2 new_mquantified2
1887 None
(*no label because past the goto*)
1888 llabel slabel
false guard
))])) in
1889 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1890 else pattern_as_given
1891 | Ast.IfThen
(ifheader
,branch
,aft) ->
1892 ifthen ifheader branch
aft after quantified minus_quantified
1893 label llabel slabel statement
make_match guard
1895 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1896 ifthenelse ifheader branch1 els branch2
aft after quantified
1897 minus_quantified label llabel slabel statement
make_match guard
1899 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1900 | Ast.Iterator
(header,body,aft) ->
1901 forwhile header body aft after quantified minus_quantified
1902 label statement
make_match guard
1904 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1905 (*ctl_and seems pointless, disjuncts see label too
1906 (label_pred_maker label)*)
1907 (List.fold_left
ctl_seqor CTL.False
1910 statement_list sl after quantified minus_quantified label
1911 llabel slabel
true guard
)
1914 | Ast.Nest
(starter
,stmt_dots
,ender,whencode
,multi
,bef
,aft) ->
1915 (* label in recursive call is None because label check is already
1916 wrapped around the corresponding code. not good enough, want to stay
1917 in a specific region, dots and nests will keep going *)
1920 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1922 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1923 | _ -> failwith
"not possible" in
1925 (* no minus version because when code doesn't contain any minus code *)
1926 let new_quantified = Common.union_set
bfvs quantified
in
1929 match Ast.get_mcodekind starter
with (*ender must have the same mcode*)
1930 Ast.MINUS
(_,_,_,_) as d ->
1931 (* no need for the fresh metavar, but ... is a bit weird as a
1933 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1938 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1939 label
(*None*) llabel slabel
true guard
in
1940 dots_and_nests multi
1941 (Some
dots_pattern) whencode bef
aft dot_code after label
1942 (process_bef_aft
new_quantified minus_quantified
1943 label
(*None*) llabel slabel
true)
1945 statement_list x Tail
new_quantified minus_quantified label
(*None*)
1946 llabel slabel
true true)
1948 statement x Tail
new_quantified minus_quantified label
(*None*)
1951 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1953 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1956 Ast.MINUS
(_,_,_,_) ->
1957 (* no need for the fresh metavar, but ... is a bit weird as a
1959 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1961 dots_and_nests false None
whencodes bef
aft dot_code after label
1962 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1964 statement_list x Tail quantified minus_quantified
1965 None llabel slabel
true true)
1967 statement x Tail quantified minus_quantified None llabel slabel
true)
1969 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1971 | Ast.Switch
(header,lb
,decls
,cases,rb
) ->
1972 let rec intersect_all = function
1975 | x
::xs -> intersect x
(intersect_all xs) in
1976 let rec intersect_all2 = function (* pairwise *)
1981 (function elem
-> List.exists (List.mem elem
) xs)
1983 Common.union_set
front (intersect_all2 xs) in
1984 let rec union_all l = List.fold_left
union [] l in
1985 (* start normal variables *)
1986 let header_fvs = Ast.get_fvs
header in
1987 let lb_fvs = Ast.get_fvs lb
in
1988 let decl_fvs = union_all (List.map
Ast.get_fvs
(Ast.undots decls
)) in
1989 let case_fvs = List.map
Ast.get_fvs
cases in
1990 let rb_fvs = Ast.get_fvs rb
in
1991 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1992 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1994 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1995 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1996 function case_fvs ->
1997 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
1998 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
1999 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
2000 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
2002 | _ -> failwith
"not possible")
2003 ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
2004 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2005 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2006 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
2007 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
2008 List.rev all_rbfvs
) in
2009 let exponlyfvs = intersect_all all_efvs
in
2010 let lbonlyfvs = intersect_all all_lbfvs
in
2011 (* don't do anything with right brace. Hope there is no + code on it *)
2012 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2013 let b1fvs = union_all all_b1fvs
in
2014 let new1_quantified = union b1fvs quantified
in
2016 union (union_all all_b2fvs
) (intersect_all2 all_casefvs
) in
2017 let new2_quantified = union b2fvs new1_quantified in
2018 (* let b3fvs = union_all all_b3fvs in*)
2019 (* ------------------- start minus free variables *)
2020 let header_mfvs = Ast.get_mfvs
header in
2021 let lb_mfvs = Ast.get_mfvs lb
in
2022 let decl_mfvs = union_all (List.map
Ast.get_mfvs
(Ast.undots decls
)) in
2023 let case_mfvs = List.map
Ast.get_mfvs
cases in
2024 let rb_mfvs = Ast.get_mfvs rb
in
2025 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2026 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2028 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2029 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2030 function case_mfvs ->
2033 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
2034 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
2035 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
2036 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
2038 | _ -> failwith
"not possible")
2039 ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
2040 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2041 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2042 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
2043 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
2044 List.rev all_mrbfvs
) in
2045 (* don't do anything with right brace. Hope there is no + code on it *)
2046 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2047 let mb1fvs = union_all all_mb1fvs
in
2048 let new1_mquantified = union mb1fvs quantified
in
2050 union (union_all all_mb2fvs
) (intersect_all2 all_mcasefvs
) in
2051 let new2_mquantified = union mb2fvs new1_mquantified in
2052 (* let b3fvs = union_all all_b3fvs in*)
2053 (* ------------------- end collection of free variables *)
2054 let switch_header = quantify guard
exponlyfvs (make_match header) in
2055 let lb = quantify guard
lbonlyfvs (make_match lb) in
2056 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
2059 (function case_line
->
2060 match Ast.unwrap case_line
with
2061 Ast.CaseLine
(header,body) ->
2063 match seq_fvs new2_quantified [Ast.get_fvs
header] with
2064 [(e1fvs,_)] -> e1fvs
2065 | _ -> failwith
"not possible" in
2066 quantify guard
e1fvs (real_make_match label
true header)
2067 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2069 let lv = get_label_ctr() in
2070 let used = ref false in
2071 let (decls_exists_code
,decls_all_code
) =
2072 (*don't really understand this*)
2073 if (Ast.undots decls
) = []
2074 then (CTL.True
,CTL.False
)
2077 statement_list decls Tail
2078 new2_quantified new2_mquantified (Some
(lv,used)) llabel None
2083 (List.fold_left
ctl_or_fl CTL.False
2084 (List.map
ctl_uncheck
2085 (decls_all_code
::case_headers))) in
2088 (function case_line
->
2089 match Ast.unwrap case_line
with
2090 Ast.CaseLine
(header,body) ->
2091 let (e1fvs,b1fvs,s1fvs
) =
2092 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
2093 match seq_fvs new2_quantified fvs with
2094 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2095 | _ -> failwith
"not possible" in
2096 let (me1fvs
,mb1fvs,ms1fvs
) =
2097 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
2098 match seq_fvs new2_mquantified fvs with
2099 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2100 | _ -> failwith
"not possible" in
2102 quantify guard
e1fvs (make_match header) in
2103 let new3_quantified = union b1fvs new2_quantified in
2104 let new3_mquantified = union mb1fvs new2_mquantified in
2106 statement_list body Tail
2107 new3_quantified new3_mquantified (Some
(lv,used)) llabel
2108 (Some
(lv,used)) false(*?*) guard
in
2109 quantify guard
b1fvs (make_seq [case_header; body])
2110 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2112 let default_required =
2115 match Ast.unwrap case
with
2116 Ast.CaseLine
(header,_) ->
2117 (match Ast.unwrap
header with
2118 Ast.Default
(_,_) -> true
2122 then function x
-> x
2123 else function x
-> ctl_or (fallpred label
) x
in
2124 let after_pred = aftpred label
in
2125 let body after_branch
=
2128 (quantify guard
b2fvs
2131 (List.fold_left
ctl_and CTL.True
2133 (decls_exists_code
:: case_headers)));
2134 List.fold_left
ctl_or_fl no_header
2135 (decls_all_code
:: case_code)])))
2138 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2139 match Ast.unwrap
rb with
2140 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2141 | _ -> failwith
"not possible") in
2142 let (switch_header,wrapper
) =
2145 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2146 (ctl_and switch_header label_pred,
2147 (function body -> quantify true [lv] body))
2148 else (switch_header,function x
-> x
) in
2150 (end_control_structure b1fvs switch_header body
2151 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2152 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2153 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2156 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2157 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2159 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2160 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2161 | _ -> failwith
"not possible" in
2162 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2165 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2166 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2168 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2169 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2170 | _ -> failwith
"not possible" in
2171 let function_header = quantify guard hfvs
(make_match header) in
2172 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2173 let stripped_rbrace =
2174 match Ast.unwrap rbrace
with
2175 Ast.SeqEnd
((data
,info,_,_)) ->
2176 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2177 | _ -> failwith
"unexpected close brace" in
2179 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2180 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2181 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2183 (quantify guard rbfvs
(make_match rbrace
))
2185 (* the following finds the beginning of the fake braces,
2186 if there are any, not completely sure how this works.
2187 sse the examples sw and return *)
2188 (ctl_back_ex (ctl_not fake_brace))
2189 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2190 let new_quantified3 =
2191 Common.union_set
b1fvs
2192 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2193 let new_mquantified3 =
2194 Common.union_set
mb1fvs
2195 (Common.union_set
mb2fvs
2196 (Common.union_set mb3fvs minus_quantified
)) in
2197 let not_minus = function Ast.MINUS
(_,_,_,_) -> false | _ -> true in
2199 match (Ast.undots
body,
2200 contains_modif rbrace
or contains_pos rbrace
) with
2202 (match Ast.unwrap
body with
2203 Ast.Nest
(starter
,stmt_dots
,ender,[],false,_,_)
2204 (* perhaps could optimize for minus case too... TODO *)
2205 when not_minus (Ast.get_mcodekind starter
)
2207 (* special case for function header + body - header is unambiguous
2208 and unique, so we can just look for the nested body anywhere
2212 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2213 statement_list stmt_dots
2214 (* discards match on right brace, but don't need it *)
2215 (Guard
(make_seq_after end_brace after
))
2216 new_quantified3 new_mquantified3
2217 None llabel slabel
true guard
))
2218 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2220 (* flow sensitive, so not optimizable *)
2221 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2223 | _ -> true) whencode
) ->
2224 (* try to be more efficient for the case where the body is just
2225 ... Perhaps this is too much of a special case, but useful
2226 for dropping a parameter and checking that it is never used. *)
2228 Ast.MINUS
(_,_,_,_) -> None
2231 (* no nested braces, because only dots *)
2232 string2var ("p1") in
2234 CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
2237 [ctl_and start_brace paren_pred;
2247 Ast.WhenAlways
(s) -> prev
2248 | Ast.WhenNot
(sl
) ->
2250 statement_list sl Tail
2256 | Ast.WhenNotTrue
(_)
2257 | Ast.WhenNotFalse
(_) ->
2258 failwith
"unexpected"
2260 (Ast.WhenAny
) -> CTL.False
2261 | Ast.WhenModifier
(_) -> prev
)
2262 CTL.False whencode
))
2266 Ast.WhenAlways
(s) ->
2271 label llabel slabel
true in
2273 | Ast.WhenNot
(sl
) -> prev
2274 | Ast.WhenNotTrue
(_)
2275 | Ast.WhenNotFalse
(_) ->
2276 failwith
"unexpected"
2277 | Ast.WhenModifier
(Ast.WhenAny
) ->
2279 | Ast.WhenModifier
(_) -> prev
)
2280 CTL.True whencode
) in
2283 (make_match stripped_rbrace)
2288 (* function body is all minus, no whencode *)
2289 match Ast.undots
body with
2291 (match Ast.unwrap
body with
2293 ((_,i
,(Ast.MINUS
(_,_,_,[]) as d),_),[],_,_) ->
2294 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2295 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,[]),_)),
2296 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,[]),_)))
2297 when not
(contains_pos rbrace
) ->
2299 (* andany drops everything to the end, including close
2300 braces - not just function body, could check
2301 label to keep braces *)
2302 (ctl_and start_brace
2305 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2307 (make_meta_rule_elem d ([],[],[]))))))
2312 match (optim1,optim2) with
2318 quantify guard
b3fvs
2319 (statement_list body
2320 (After
(make_seq_after end_brace after
))
2321 new_quantified3 new_mquantified3 None llabel slabel
2323 quantify guard
b1fvs
2324 (make_seq [function_header; quantify guard
b2fvs body_code])
2325 | Ast.Define
(header,body) ->
2326 let (hfvs
,bfvs,bodyfvs
) =
2327 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2329 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2330 | _ -> failwith
"not possible" in
2331 let (mhfvs
,mbfvs
,mbodyfvs
) =
2332 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2334 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2335 | _ -> failwith
"not possible" in
2336 let define_header = quantify guard hfvs
(make_match header) in
2338 statement_list body after
2339 (Common.union_set
bfvs quantified
)
2340 (Common.union_set mbfvs minus_quantified
)
2341 None llabel slabel
true guard
in
2342 quantify guard
bfvs (make_seq [define_header; body_code])
2343 | Ast.OptStm
(stm
) ->
2344 failwith
"OptStm should have been compiled away\n"
2345 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2346 | _ -> failwith
"not supported" in
2347 if guard
or !dots_done
2350 do_between_dots stmt
term after quantified minus_quantified
2351 label llabel slabel guard
2353 (* term is the translation of stmt *)
2354 and do_between_dots stmt
term after quantified minus_quantified
2355 label llabel slabel guard
=
2356 match Ast.get_dots_bef_aft stmt
with
2357 Ast.AddingBetweenDots
(brace_term
,n
)
2358 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2360 statement brace_term after quantified minus_quantified
2361 label llabel slabel guard
in
2362 let v = Printf.sprintf
"_r_%d" n
in
2363 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2364 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2367 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2368 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2370 | Ast.NoDots
-> term
2372 (* un_process_bef_aft is because we don't want to do transformation in this
2373 code, and thus don't case about braces before or after it *)
2374 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2376 Ast.WParen
(re
,n
) ->
2377 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2378 let s = guard_to_strict guard
in
2379 quantify true (get_unquantified quantified
[n
])
2380 (ctl_and s (make_raw_match None guard re
) paren_pred)
2382 statement
s Tail quantified minus_quantified label llabel slabel guard
2383 | Ast.Other_dots
d ->
2384 statement_list d Tail quantified minus_quantified
2385 label llabel slabel
true guard
2387 (* --------------------------------------------------------------------- *)
2388 (* cleanup: convert AX to EX for pdots.
2389 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2390 This is what we wanted in the first place, but it wasn't possible to make
2391 because the AX and its argument are not created in the same place.
2393 (* also cleanup XX, which is a marker for the case where the programmer
2394 specifies to change the quantifier on .... Assumed to only occur after one AX
2395 or EX, or at top level. *)
2398 let c = match c with CTL.XX
(c) -> c | _ -> c in
2400 CTL.False
-> CTL.False
2401 | CTL.True
-> CTL.True
2402 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2403 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2404 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2405 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2406 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2407 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2408 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2409 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2410 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2411 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2412 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2413 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2414 | CTL.AX
(CTL.FORWARD
,s,
2416 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2417 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2419 CTL.And
(CTL.NONSTRICT
,
2420 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2421 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2422 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2423 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2424 CTL.AX
(dir
,s,cleanup phi
)
2425 | CTL.XX
(phi
) -> failwith
"bad XX"
2426 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2427 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2428 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2429 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2430 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2431 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2432 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2433 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2434 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2435 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2436 | CTL.Ref
(s) -> CTL.Ref
(s)
2437 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2438 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2440 (* --------------------------------------------------------------------- *)
2441 (* Function declaration *)
2443 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2445 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2446 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2448 saved := Ast.get_saved t
;
2449 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2450 quantify false quantified
2451 (match Ast.unwrap t
with
2452 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2454 let unopt = elim_opt.V.rebuilder_statement stmt
in
2455 let unopt = preprocess_dots_e unopt in
2456 cleanup(statement
unopt VeryEnd
quantified [] None None None
false)
2457 | Ast.CODE
(stmt_dots
) ->
2458 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2459 let unopt = preprocess_dots unopt in
2460 let starts_with_dots =
2461 match Ast.undots stmt_dots
with
2463 (match Ast.unwrap
d with
2464 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2465 | Ast.Stars
(_,_,_,_) -> true
2468 let starts_with_brace =
2469 match Ast.undots stmt_dots
with
2471 (match Ast.unwrap
d with
2476 statement_list unopt VeryEnd
quantified [] None None None
2479 (if starts_with_dots
2481 (* EX because there is a loop on enter/top *)
2482 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2483 else if starts_with_brace
2485 ctl_and CTL.NONSTRICT
2486 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2488 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords")
2490 (* --------------------------------------------------------------------- *)
2493 let asttoctlz (name
,(_,_,exists_flag
),l)
2494 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2497 (match exists_flag
with
2498 Ast.Exists
-> exists := Exists
2499 | Ast.Forall
-> exists := Forall
2500 | Ast.Undetermined
->
2501 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2503 let (l,used_after) =
2507 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2508 (List.combine
l (List.combine
used_after positions
))) in
2510 List.map2
(top_level name
)
2511 (List.combine
used_after fresh_used_after
)
2512 (List.combine fresh_used_after_seeds
l) in
2516 let asttoctl r
used_after positions
=
2518 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2519 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2520 asttoctlz (a,b
,c) used_after positions
2521 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CTL.True
]
2523 let pp_cocci_predicate (pred
,modif
) =
2524 Pretty_print_engine.pp_predicate pred
2526 let cocci_predicate_to_string (pred
,modif
) =
2527 Pretty_print_engine.predicate_to_string pred