2 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
23 (* for MINUS and CONTEXT, pos is always None in this file *)
24 (*search for require*)
25 (* true = don't see all matched nodes, only modified ones *)
26 let onlyModif = ref true(*false*)
28 type ex
= Exists
| Forall
| ReverseForall
29 let exists = ref Forall
31 module Ast
= Ast_cocci
32 module V
= Visitor_ast
35 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
37 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
39 (cocci_predicate
,Ast.meta_name
, Wrapper_ctl.info
) Ast_ctl.generic_ctl
41 let union = Common.union_set
42 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
43 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
45 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
47 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
49 let used_after = ref ([] : Ast.meta_name list
)
50 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
52 let saved = ref ([] : Ast.meta_name list
)
54 let string2var x
= ("",x
)
56 (* --------------------------------------------------------------------- *)
57 (* predicates matching various nodes in the graph *)
61 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
62 | (CTL.True
,a
) | (a
,CTL.True
) -> a
67 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
68 | (CTL.False
,a
) | (a
,CTL.False
) -> a
73 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
74 | (CTL.False
,a
) | (a
,CTL.False
) -> a
79 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
80 | (CTL.False
,a
) | (a
,CTL.False
) -> a
83 let ctl_not = function
85 | CTL.False
-> CTL.True
88 let ctl_ax s
= function
90 | CTL.False
-> CTL.False
93 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
94 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
95 | ReverseForall
-> failwith
"not supported"
97 let ctl_ax_absolute s
= function
99 | CTL.False
-> CTL.False
100 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
102 let ctl_ex = function
104 | CTL.False
-> CTL.False
105 | x
-> CTL.EX
(CTL.FORWARD
,x
)
107 (* This stays being AX even for sgrep_mode, because it is used to identify
108 the structure of the term, not matching the pattern. *)
109 let ctl_back_ax = function
111 | CTL.False
-> CTL.False
112 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
114 let ctl_back_ex = function
116 | CTL.False
-> CTL.False
117 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
119 let ctl_ef = function
121 | CTL.False
-> CTL.False
122 | x
-> CTL.EF
(CTL.FORWARD
,x
)
124 let ctl_ag s
= function
126 | CTL.False
-> CTL.False
127 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
130 match (x
,!exists) with
131 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
132 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
133 | (CTL.True
,ReverseForall
) -> failwith
"not supported"
134 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
135 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
136 | (_
,ReverseForall
) -> failwith
"not supported"
138 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
140 (match (x
,!exists) with
141 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
142 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
143 | (CTL.True
,ReverseForall
) -> failwith
"not supported"
144 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
145 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
146 | (_
,ReverseForall
) -> failwith
"not supported")
148 let ctl_uncheck = function
150 | CTL.False
-> CTL.False
153 let label_pred_maker = function
155 | Some
(label_var
,used
) ->
157 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
159 let bclabel_pred_maker = function
161 | Some
(label_var
,used
) ->
163 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
165 let predmaker guard pred label
=
166 ctl_and (guard_to_strict guard
) (CTL.Pred pred
) (label_pred_maker label
)
168 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
169 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
170 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
171 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
172 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
173 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
174 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
175 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
176 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
177 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
178 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
180 let aftret label_var f
= ctl_or (aftpred label_var
) (exitpred label_var
)
186 Printf.sprintf
"r%d" cur
188 (* --------------------------------------------------------------------- *)
189 (* --------------------------------------------------------------------- *)
190 (* Eliminate OptStm *)
192 (* for optional thing with nothing after, should check that the optional thing
193 never occurs. otherwise the matching stops before it occurs *)
196 let donothing r k e
= k e
in
199 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
202 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
205 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
207 let inheritedlist l
=
208 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
211 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
214 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
216 let rec dots_list unwrapped wrapped
=
217 match (unwrapped
,wrapped
) with
220 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
222 | (Ast.Nest
(_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
224 let l = Ast.get_line stm
in
225 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
226 let new_rest2 = dots_list urest rest
in
227 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
228 varlists new_rest1 in
229 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
230 varlists new_rest2 in
234 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
236 Ast.free_vars
= fv_rest1
;
237 Ast.minus_free_vars
= mfv_rest1
;
238 Ast.fresh_vars
= fresh_rest1
;
239 Ast.inherited
= inherited_rest1
;
240 Ast.saved_witness
= s1
};
241 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
243 Ast.free_vars
= fv_rest2
;
244 Ast.minus_free_vars
= mfv_rest2
;
245 Ast.fresh_vars
= fresh_rest2
;
246 Ast.inherited
= inherited_rest2
;
247 Ast.saved_witness
= s2
}])) with
249 Ast.free_vars
= fv_rest1
;
250 Ast.minus_free_vars
= mfv_rest1
;
251 Ast.fresh_vars
= fresh_rest1
;
252 Ast.inherited
= inherited_rest1
;
253 Ast.saved_witness
= s1
}]
255 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
256 let l = Ast.get_line stm
in
257 let new_rest1 = dots_list urest rest
in
258 let new_rest2 = stm
::new_rest1 in
259 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
260 varlists new_rest1 in
261 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
262 varlists new_rest2 in
265 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
267 Ast.free_vars
= fv_rest2
;
268 Ast.minus_free_vars
= mfv_rest2
;
269 Ast.fresh_vars
= fresh_rest2
;
270 Ast.inherited
= inherited_rest2
;
271 Ast.saved_witness
= s2
};
272 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
274 Ast.free_vars
= fv_rest1
;
275 Ast.minus_free_vars
= mfv_rest1
;
276 Ast.fresh_vars
= fresh_rest1
;
277 Ast.inherited
= inherited_rest1
;
278 Ast.saved_witness
= s1
}])) with
280 Ast.free_vars
= fv_rest2
;
281 Ast.minus_free_vars
= mfv_rest2
;
282 Ast.fresh_vars
= fresh_rest2
;
283 Ast.inherited
= inherited_rest2
;
284 Ast.saved_witness
= s2
}]
286 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
287 let l = Ast.get_line stm
in
288 let fv_stm = Ast.get_fvs stm
in
289 let mfv_stm = Ast.get_mfvs stm
in
290 let fresh_stm = Ast.get_fresh stm
in
291 let inh_stm = Ast.get_inherited stm
in
292 let saved_stm = Ast.get_saved stm
in
293 let fv_d1 = Ast.get_fvs d1
in
294 let mfv_d1 = Ast.get_mfvs d1
in
295 let fresh_d1 = Ast.get_fresh d1
in
296 let inh_d1 = Ast.get_inherited d1
in
297 let saved_d1 = Ast.get_saved d1
in
298 let fv_both = Common.union_set
fv_stm fv_d1 in
299 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
300 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
301 let inh_both = Common.union_set
inh_stm inh_d1 in
302 let saved_both = Common.union_set
saved_stm saved_d1 in
306 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
308 Ast.free_vars
= fv_stm;
309 Ast.minus_free_vars
= mfv_stm;
310 Ast.fresh_vars
= fresh_stm;
311 Ast.inherited
= inh_stm;
312 Ast.saved_witness
= saved_stm};
313 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
315 Ast.free_vars
= fv_d1;
316 Ast.minus_free_vars
= mfv_d1;
317 Ast.fresh_vars
= fresh_d1;
318 Ast.inherited
= inh_d1;
319 Ast.saved_witness
= saved_d1}])) with
321 Ast.free_vars
= fv_both;
322 Ast.minus_free_vars
= mfv_both;
323 Ast.fresh_vars
= fresh_both;
324 Ast.inherited
= inh_both;
325 Ast.saved_witness
= saved_both}]
327 | ([Ast.Nest
(_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
328 let l = Ast.get_line stm
in
329 let rw = Ast.rewrap stm
in
330 let rwd = Ast.rewrap stm
in
331 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
333 [rwd(Ast.DOTS
([stm
]));
334 {(Ast.make_term
(Ast.DOTS
([rw dots])))
335 with Ast.node_line
= l}])]
337 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
338 | _
-> failwith
"not possible" in
340 let stmtdotsfn r k d
=
343 (match Ast.unwrap
d with
344 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
345 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
346 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
349 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
350 donothing donothing stmtdotsfn donothing
351 donothing donothing donothing donothing donothing donothing donothing
352 donothing donothing donothing donothing donothing
354 (* --------------------------------------------------------------------- *)
355 (* after management *)
356 (* We need Guard for the following case:
365 Here the inner <... b ...> should not go past foo. But foo is not the
366 "after" of the body of the outer nest, because we don't want to search for
367 it in the case where the body of the outer nest ends in something other
368 than dots or a nest. *)
370 (* what is the difference between tail and end??? *)
372 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
374 let a2n = function After x
-> Guard x
| a
-> a
377 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
378 let pp_meta (_
,x
) = Common.pp x
in
379 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
380 Format.print_newline
()
382 let print_after = function
383 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
384 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
385 | Tail
-> Printf.printf
"Tail\n"
386 | VeryEnd
-> Printf.printf
"Very End\n"
387 | End
-> Printf.printf
"End\n"
389 (* --------------------------------------------------------------------- *)
392 let fresh_var _
= string2var "_v"
393 let fresh_pos _
= string2var "_pos" (* must be a constant *)
395 let fresh_metavar _
= "_S"
397 (* fvinfo is going to end up being from the whole associated statement.
398 it would be better if it were just the free variables in d, but free_vars.ml
399 doesn't keep track of free variables on + code *)
400 let make_meta_rule_elem d fvinfo
=
401 let nm = fresh_metavar() in
402 Ast.make_meta_rule_elem nm d fvinfo
404 let get_unquantified quantified vars
=
405 List.filter
(function x
-> not
(List.mem x quantified
)) vars
407 let make_seq guard
l =
408 let s = guard_to_strict guard
in
409 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
411 let make_seq_after2 guard first rest
=
412 let s = guard_to_strict guard
in
414 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
417 let make_seq_after guard first rest
=
419 After rest
-> make_seq guard
[first
;rest
]
422 let opt_and guard first rest
=
423 let s = guard_to_strict guard
in
426 | Some first
-> ctl_and s first rest
428 let and_after guard first rest
=
429 let s = guard_to_strict guard
in
430 match rest
with After rest
-> ctl_and s first rest
| _
-> first
433 let bind x y
= x
or y
in
434 let option_default = false in
435 let mcode r
(_
,_
,kind
,metapos
) =
437 Ast.MINUS
(_
,_
,_
,_
) -> true
438 | Ast.PLUS
-> failwith
"not possible"
439 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
440 let do_nothing r k e
= k e
in
441 let rule_elem r k re
=
443 match Ast.unwrap re
with
444 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
445 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
446 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
449 V.combiner
bind option_default
450 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
451 do_nothing do_nothing do_nothing do_nothing
452 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
453 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
454 recursor.V.combiner_rule_elem
457 let bind x y
= x
or y
in
458 let option_default = false in
459 let mcode r
(_
,_
,kind
,metapos
) =
461 Ast.MetaPos
(_
,_
,_
,_
,_
) -> true
462 | Ast.NoMetaPos
-> false in
463 let do_nothing r k e
= k e
in
464 let rule_elem r k re
=
466 match Ast.unwrap re
with
467 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
468 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
469 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
472 V.combiner
bind option_default
473 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
474 do_nothing do_nothing do_nothing do_nothing
475 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
476 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
477 recursor.V.combiner_rule_elem
479 (* code is not a DisjRuleElem *)
480 let make_match label guard code
=
481 let v = fresh_var() in
482 let matcher = Lib_engine.Match
(code
) in
483 if contains_modif code
&& not guard
484 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
486 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
487 (match (iso_info,!onlyModif,guard
,
488 intersect !used_after (Ast.get_fvs code
)) with
489 (false,true,_
,[]) | (_
,_
,true,_
) ->
490 predmaker guard
(matcher,CTL.Control
) label
491 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
493 let make_raw_match label guard code
=
494 predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
496 let rec seq_fvs quantified
= function
499 let t1fvs = get_unquantified quantified fv1
in
501 List.fold_left
Common.union_set
[]
502 (List.map
(get_unquantified quantified
) fvs
) in
503 let bothfvs = Common.inter_set
t1fvs termfvs in
504 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
505 let new_quantified = Common.union_set
bothfvs quantified
in
506 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
511 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
513 let non_saved_quantify =
515 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
517 let intersectll lst nested_list
=
518 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
520 (* --------------------------------------------------------------------- *)
521 (* Count depth of braces. The translation of a closed brace appears deeply
522 nested within the translation of the sequence term, so the name of the
523 paren var has to take into account the names of the nested braces. On the
524 other hand the close brace does not escape, so we don't have to take into
525 account other paren variable names. *)
527 (* called repetitively, which is inefficient, but less trouble than adding a
528 new field to Seq and FunDecl *)
529 let count_nested_braces s =
530 let bind x y
= max x y
in
531 let option_default = 0 in
532 let stmt_count r k
s =
533 match Ast.unwrap
s with
534 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
536 let donothing r k e
= k e
in
538 let recursor = V.combiner
bind option_default
539 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
540 donothing donothing donothing donothing
541 donothing donothing donothing donothing donothing donothing
542 donothing donothing stmt_count donothing donothing donothing in
543 let res = string_of_int
(recursor.V.combiner_statement
s) in
547 let get_label_ctr _
=
548 let cur = !labelctr in
550 string2var (Printf.sprintf
"l%d" cur)
552 (* --------------------------------------------------------------------- *)
553 (* annotate dots with before and after neighbors *)
555 let print_bef_aft = function
557 Printf.printf
"bef/aft\n";
558 Pretty_print_cocci.rule_elem "" re
;
559 Format.print_newline
()
561 Printf.printf
"bef/aft\n";
562 Pretty_print_cocci.statement
"" s;
563 Format.print_newline
()
564 | Ast.Other_dots
d ->
565 Printf.printf
"bef/aft\n";
566 Pretty_print_cocci.statement_dots
d;
567 Format.print_newline
()
569 (* [] can only occur if we are in a disj, where it comes from a ? In that
570 case, we want to use a, which accumulates all of the previous patterns in
572 let rec get_before_elem sl a
=
573 match Ast.unwrap sl
with
577 [] -> ([],Common.Right a
)
579 let (e
,ea
) = get_before_e e a
in
582 let (e
,ea
) = get_before_e e a
in
583 let (sl
,sla
) = loop sl ea
in
585 let (l,a
) = loop x a
in
586 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
587 | Ast.CIRCLES
(x
) -> failwith
"not supported"
588 | Ast.STARS
(x
) -> failwith
"not supported"
590 and get_before sl a
=
591 match get_before_elem sl a
with
592 (term
,Common.Left x
) -> (term
,x
)
593 | (term
,Common.Right x
) -> (term
,x
)
595 and get_before_whencode wc
=
598 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
599 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
600 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
601 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
602 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
605 and get_before_e
s a
=
606 match Ast.unwrap
s with
607 Ast.Dots
(d,w
,_
,aft
) ->
608 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
609 | Ast.Nest
(stmt_dots
,w
,multi
,_
,aft
) ->
610 let w = get_before_whencode
w in
611 let (sd
,_
) = get_before stmt_dots a
in
617 Unify_ast.unify_statement_dots
618 (Ast.rewrap
s (Ast.DOTS
([a]))) stmt_dots
in
620 Unify_ast.MAYBE
-> false
622 | Ast.Other_dots
a ->
623 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
625 Unify_ast.MAYBE
-> false
629 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,a,aft
)),[Ast.Other_dots stmt_dots
])
630 | Ast.Disj
(stmt_dots_list
) ->
632 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
633 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
635 (match Ast.unwrap ast
with
636 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
637 | _
-> (s,[Ast.Other
s]))
638 | Ast.Seq
(lbrace
,body
,rbrace
) ->
639 let index = count_nested_braces s in
640 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
641 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
642 | Ast.Define
(header
,body
) ->
643 let (body
,_
) = get_before body
[] in
644 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
645 | Ast.IfThen
(ifheader
,branch
,aft
) ->
646 let (br
,_
) = get_before_e branch
[] in
647 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
648 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
649 let (br1
,_
) = get_before_e branch1
[] in
650 let (br2
,_
) = get_before_e branch2
[] in
651 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
652 | Ast.While
(header
,body
,aft
) ->
653 let (bd
,_
) = get_before_e body
[] in
654 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
655 | Ast.For
(header
,body
,aft
) ->
656 let (bd
,_
) = get_before_e body
[] in
657 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
658 | Ast.Do
(header
,body
,tail
) ->
659 let (bd
,_
) = get_before_e body
[] in
660 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
661 | Ast.Iterator
(header
,body
,aft
) ->
662 let (bd
,_
) = get_before_e body
[] in
663 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
664 | Ast.Switch
(header
,lb
,cases
,rb
) ->
667 (function case_line
->
668 match Ast.unwrap case_line
with
669 Ast.CaseLine
(header
,body
) ->
670 let (body
,_
) = get_before body
[] in
671 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
672 | Ast.OptCase
(case_line
) -> failwith
"not supported")
674 (Ast.rewrap
s (Ast.Switch
(header
,lb
,cases,rb
)),[Ast.Other
s])
675 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
676 let (bd
,_
) = get_before body
[] in
677 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
679 Pretty_print_cocci.statement
"" s; Format.print_newline
();
680 failwith
"get_before_e: not supported"
682 let rec get_after sl
a =
683 match Ast.unwrap sl
with
689 let (sl
,sla
) = loop sl
in
690 let (e
,ea
) = get_after_e e sla
in
692 let (l,a) = loop x
in
693 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
694 | Ast.CIRCLES
(x
) -> failwith
"not supported"
695 | Ast.STARS
(x
) -> failwith
"not supported"
697 and get_after_whencode
a wc
=
700 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
701 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
702 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
703 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
704 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
707 and get_after_e
s a =
708 match Ast.unwrap
s with
709 Ast.Dots
(d,w,bef
,_
) ->
710 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
711 | Ast.Nest
(stmt_dots
,w,multi
,bef
,_
) ->
712 let w = get_after_whencode
a w in
713 let (sd
,_
) = get_after stmt_dots
a in
719 Unify_ast.unify_statement_dots
720 (Ast.rewrap
s (Ast.DOTS
([a]))) stmt_dots
in
722 Unify_ast.MAYBE
-> false
724 | Ast.Other_dots
a ->
725 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
727 Unify_ast.MAYBE
-> false
731 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,bef
,a)),[Ast.Other_dots stmt_dots
])
732 | Ast.Disj
(stmt_dots_list
) ->
734 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
735 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
737 (match Ast.unwrap ast
with
738 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
739 (* check "after" information for metavar optimization *)
740 (* if the error is not desired, could just return [], then
741 the optimization (check for EF) won't take place *)
745 (match Ast.unwrap x
with
746 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
748 "dots/nest not allowed before and after stmt metavar"
750 | Ast.Other_dots x
->
751 (match Ast.undots x
with
753 (match Ast.unwrap x
with
754 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
756 ("dots/nest not allowed before and after stmt "^
765 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
766 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
767 | _
-> (s,[Ast.Other
s]))
768 | Ast.Seq
(lbrace
,body
,rbrace
) ->
769 let index = count_nested_braces s in
770 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
771 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
772 [Ast.WParen
(lbrace
,index)])
773 | Ast.Define
(header
,body
) ->
774 let (body
,_
) = get_after body
a in
775 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
776 | Ast.IfThen
(ifheader
,branch
,aft
) ->
777 let (br
,_
) = get_after_e branch
a in
778 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
779 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
780 let (br1
,_
) = get_after_e branch1
a in
781 let (br2
,_
) = get_after_e branch2
a in
782 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
783 | Ast.While
(header
,body
,aft
) ->
784 let (bd
,_
) = get_after_e body
a in
785 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
786 | Ast.For
(header
,body
,aft
) ->
787 let (bd
,_
) = get_after_e body
a in
788 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
789 | Ast.Do
(header
,body
,tail
) ->
790 let (bd
,_
) = get_after_e body
a in
791 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
792 | Ast.Iterator
(header
,body
,aft
) ->
793 let (bd
,_
) = get_after_e body
a in
794 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
795 | Ast.Switch
(header
,lb
,cases,rb
) ->
798 (function case_line
->
799 match Ast.unwrap case_line
with
800 Ast.CaseLine
(header
,body
) ->
801 let (body
,_
) = get_after body
[] in
802 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
803 | Ast.OptCase
(case_line
) -> failwith
"not supported")
805 (Ast.rewrap
s (Ast.Switch
(header
,lb
,cases,rb
)),[Ast.Other
s])
806 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
807 let (bd
,_
) = get_after body
[] in
808 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
809 | _
-> failwith
"get_after_e: not supported"
811 let preprocess_dots sl
=
812 let (sl
,_
) = get_before sl
[] in
813 let (sl
,_
) = get_after sl
[] in
816 let preprocess_dots_e sl
=
817 let (sl
,_
) = get_before_e sl
[] in
818 let (sl
,_
) = get_after_e sl
[] in
821 (* --------------------------------------------------------------------- *)
822 (* various return_related things *)
824 let rec ends_in_return stmt_list
=
825 match Ast.unwrap stmt_list
with
827 (match List.rev x
with
829 (match Ast.unwrap x
with
832 match Ast.unwrap x
with
833 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
834 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
837 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
840 | Ast.CIRCLES
(x
) -> failwith
"not supported"
841 | Ast.STARS
(x
) -> failwith
"not supported"
843 (* --------------------------------------------------------------------- *)
846 let exptymatch l make_match make_guard_match
=
847 let pos = fresh_pos() in
848 let matches_guard_matches =
851 let pos = Ast.make_mcode
pos in
852 (make_match (Ast.set_pos x
(Some
pos)),
853 make_guard_match
(Ast.set_pos x
(Some
pos))))
855 let (matches
,guard_matches
) = List.split
matches_guard_matches in
856 let rec suffixes = function
858 | x
::xs -> xs::(suffixes xs) in
859 let prefixes = List.rev
(suffixes (List.rev guard_matches
)) in
860 let info = (* not null *)
866 ctl_and CTL.NONSTRICT
matcher
868 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
870 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
872 (* code might be a DisjRuleElem, in which case we break it apart
873 code might contain an Exp or Ty
874 this one pushes the quantifier inwards *)
875 let do_re_matches label guard
res quantified minus_quantified
=
876 let make_guard_match x
=
877 let stmt_fvs = Ast.get_mfvs x
in
878 let fvs = get_unquantified minus_quantified
stmt_fvs in
879 non_saved_quantify fvs (make_match None
true x
) in
881 let stmt_fvs = Ast.get_fvs x
in
882 let fvs = get_unquantified quantified
stmt_fvs in
883 quantify guard
fvs (make_match None guard x
) in
884 ctl_and CTL.NONSTRICT
(label_pred_maker label
)
885 (match List.map
Ast.unwrap
res with
886 [] -> failwith
"unexpected empty disj"
887 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
888 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
890 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
892 then failwith
"unexpected exp or ty";
893 List.fold_left
ctl_seqor CTL.False
894 (List.rev
(List.map
make_match res)))
896 (* code might be a DisjRuleElem, in which case we break it apart
897 code doesn't contain an Exp or Ty
898 this one is for use when it is not practical to push the quantifier inwards
900 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
901 match Ast.unwrap code
with
902 Ast.DisjRuleElem
(res) ->
903 let make_match = make_match None guard
in
904 let orop = if guard
then ctl_or else ctl_seqor in
905 ctl_and CTL.NONSTRICT
(label_pred_maker label
)
906 (List.fold_left
orop CTL.False
(List.map
make_match res))
907 | _
-> make_match label guard code
909 (* --------------------------------------------------------------------- *)
910 (* control structures *)
912 let end_control_structure fvs header body after_pred
913 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
914 (* aft indicates what is added after the whole if, which has to be added
916 let (aft_needed
,after_branch
) =
918 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
919 (false,make_seq_after2 guard after_pred after
)
922 make_match label guard
923 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
925 make_seq_after guard after_pred
926 (After
(make_seq_after guard
match_endif after
))) in
927 let body = body after_branch
in
928 let s = guard_to_strict guard
in
933 (match (after
,aft_needed
) with
934 (After _
,_
) (* pattern doesn't end here *)
935 | (_
,true) (* + code added after *) -> after_checks
936 | _
-> no_after_checks
)
937 (ctl_ax_absolute s body)))
939 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
940 quantified minus_quantified label llabel slabel recurse
make_match guard
=
941 (* "if (test) thn" becomes:
942 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
944 "if (test) thn; after" becomes:
945 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
950 match seq_fvs quantified
951 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
952 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
953 | _
-> failwith
"not possible" in
954 let new_quantified = Common.union_set bfvs quantified
in
956 match seq_fvs minus_quantified
957 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
958 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
959 | _
-> failwith
"not possible" in
960 let new_mquantified = Common.union_set mbfvs minus_quantified
in
962 let if_header = quantify guard efvs
(make_match ifheader
) in
963 (* then branch and after *)
964 let lv = get_label_ctr() in
965 let used = ref false in
968 [truepred label
; recurse branch Tail
new_quantified new_mquantified
969 (Some
(lv,used)) llabel slabel guard
] in
970 let after_pred = aftpred label
in
971 let or_cases after_branch
=
972 ctl_or true_branch (ctl_or (fallpred label
) after_branch
) in
973 let (if_header,wrapper
) =
976 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
977 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
978 (function body -> quantify true [lv] body))
979 else (if_header,function x
-> x
) in
981 (end_control_structure bfvs
if_header or_cases after_pred
982 (Some
(ctl_ex after_pred)) None aft after label guard
)
984 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
985 quantified minus_quantified label llabel slabel recurse
make_match guard
=
986 (* "if (test) thn else els" becomes:
987 if(test) & AX((TrueBranch & AX thn) v
988 (FalseBranch & AX (else & AX els)) v After)
991 "if (test) thn else els; after" becomes:
992 if(test) & AX((TrueBranch & AX thn) v
993 (FalseBranch & AX (else & AX els)) v
994 (After & AXAX after))
999 let (e1fvs
,b1fvs
,s1fvs
) =
1000 match seq_fvs quantified
1001 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1002 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1003 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1004 | _
-> failwith
"not possible" in
1005 let (e2fvs
,b2fvs
,s2fvs
) =
1007 match seq_fvs quantified
1008 [Ast.get_fvs ifheader
;Ast.get_fvs branch2
;afvs
] with
1009 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1010 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1011 | _
-> failwith
"not possible" in
1012 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1013 let exponlyfvs = intersect e1fvs e2fvs
in
1014 let new_quantified = union bothfvs quantified
in
1015 (* minus free variables *)
1016 let (me1fvs
,mb1fvs
,ms1fvs
) =
1017 match seq_fvs minus_quantified
1018 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1019 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1020 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1021 | _
-> failwith
"not possible" in
1022 let (me2fvs
,mb2fvs
,ms2fvs
) =
1024 match seq_fvs minus_quantified
1025 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch2
;[]] with
1026 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1027 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1028 | _
-> failwith
"not possible" in
1029 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1030 let new_mquantified = union mbothfvs minus_quantified
in
1032 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1033 (* then and else branches *)
1034 let lv = get_label_ctr() in
1035 let used = ref false in
1038 [truepred label
; recurse branch1 Tail
new_quantified new_mquantified
1039 (Some
(lv,used)) llabel slabel guard
] in
1042 [falsepred label
; make_match els
;
1043 recurse branch2 Tail
new_quantified new_mquantified
1044 (Some
(lv,used)) llabel slabel guard
] in
1045 let after_pred = aftpred label
in
1046 let or_cases after_branch
=
1047 ctl_or true_branch (ctl_or false_branch after_branch
) in
1048 let s = guard_to_strict guard
in
1049 let (if_header,wrapper
) =
1052 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1053 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1054 (function body -> quantify true [lv] body))
1055 else (if_header,function x
-> x
) in
1057 (end_control_structure bothfvs if_header or_cases after_pred
1058 (Some
(ctl_and s (ctl_ex (falsepred label
)) (ctl_ex after_pred)))
1059 (Some
(ctl_ex (falsepred label
)))
1060 aft after label guard
)
1062 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1063 quantified minus_quantified label recurse
make_match guard
=
1065 (* the translation in this case is similar to that of an if with no else *)
1066 (* free variables *)
1068 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1069 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1070 | _
-> failwith
"not possible" in
1071 let new_quantified = Common.union_set bfvs quantified
in
1072 (* minus free variables *)
1074 match seq_fvs minus_quantified
1075 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1076 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1077 | _
-> failwith
"not possible" in
1078 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1080 let header = quantify guard efvs
(make_match header) in
1081 let lv = get_label_ctr() in
1082 let used = ref false in
1086 recurse
body Tail
new_quantified new_mquantified
1087 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1088 let after_pred = fallpred label
in
1089 let or_cases after_branch
= ctl_or body after_branch
in
1090 let (header,wrapper
) =
1093 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1094 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1095 (function body -> quantify true [lv] body))
1096 else (header,function x
-> x
) in
1098 (end_control_structure bfvs
header or_cases after_pred
1099 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1100 match (Ast.unwrap
body,aft
) with
1101 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1102 (match Ast.unwrap re
with
1103 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1104 Type_cocci.Unitary
,_
,false)
1105 when after
= Tail
or after
= End
or after
= VeryEnd
->
1107 match seq_fvs quantified
[Ast.get_fvs
header] with
1109 | _
-> failwith
"not possible" in
1110 quantify guard efvs
(make_match header)
1114 (* --------------------------------------------------------------------- *)
1115 (* statement metavariables *)
1117 (* issue: an S metavariable that is not an if branch/loop body
1118 should not match an if branch/loop body, so check that the labels
1119 of the nodes before the first node matched by the S are different
1120 from the label of the first node matched by the S *)
1121 let sequencibility body label_pred process_bef_aft
= function
1122 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1125 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1126 | Ast.SequencibleAfterDots
l ->
1127 (* S appears after some dots. l is the code that comes after the S.
1128 want to search for that first, because S can match anything, while
1129 the stuff after is probably more restricted *)
1130 let afts = List.map process_bef_aft
l in
1131 let ors = foldl1 ctl_or afts in
1132 ctl_and CTL.NONSTRICT
1133 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1136 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1137 | Ast.NotSequencible
-> body (function x
-> x
)
1139 let svar_context_with_add_after stmt
s label quantified
d ast
1140 seqible after process_bef_aft guard fvinfo
=
1141 let label_var = (*fresh_label_var*) string2var "_lab" in
1143 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1145 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1146 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1147 let full_metamatch = matcher d in
1148 let first_metamatch =
1151 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
)) ->
1152 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
))
1153 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1154 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1155 let middle_metamatch =
1158 Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1159 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1160 let last_metamatch =
1163 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
)) ->
1164 Ast.CONTEXT
(pos,Ast.AFTER
(aft
))
1165 | Ast.CONTEXT
(_
,_
) -> d
1166 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1169 ctl_and CTL.NONSTRICT
middle_metamatch prelabel_pred in
1170 let left_or = (* the whole statement is one node *)
1172 [full_metamatch; and_after guard
(ctl_not prelabel_pred) after
] in
1173 let right_or = (* the statement covers multiple nodes *)
1176 ctl_au CTL.NONSTRICT
1179 [ctl_and CTL.NONSTRICT
last_metamatch label_pred;
1181 (ctl_not prelabel_pred) after
])] in
1183 ctl_and CTL.NONSTRICT
label_pred
1184 (f
(ctl_and CTL.NONSTRICT
1185 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1186 let stmt_fvs = Ast.get_fvs stmt
in
1187 let fvs = get_unquantified quantified
stmt_fvs in
1188 quantify guard
(label_var::fvs)
1189 (sequencibility body label_pred process_bef_aft seqible
)
1191 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1192 seqible after process_bef_aft guard fvinfo
=
1193 let label_var = (*fresh_label_var*) string2var "_lab" in
1195 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1197 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1198 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1200 match (d,after
) with
1201 (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1202 (* just match the root. don't care about label; always ok *)
1203 make_raw_match None
false ast
1204 | (Ast.MINUS
(pos,inst
,adj
,[]),(Tail
|End
|VeryEnd
)) ->
1205 (* don't have to put anything before the beginning, so don't have to
1206 distinguish the first node. so don't have to bother about paths,
1207 just use the label. label ensures that found nodes match up with
1208 what they should because it is in the lhs of the andany. *)
1209 CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1210 ctl_and CTL.NONSTRICT
label_pred
1211 (make_raw_match label
false ast
),
1212 ctl_and CTL.NONSTRICT
(matcher d) prelabel_pred)
1214 (* more safe but less efficient *)
1215 let first_metamatch = matcher d in
1216 let rest_metamatch =
1219 Ast.MINUS
(pos,inst
,adj
,_
) -> Ast.MINUS
(pos,inst
,adj
,[])
1220 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1221 | Ast.PLUS
-> failwith
"not possible") in
1222 let rest_nodes = ctl_and CTL.NONSTRICT
rest_metamatch prelabel_pred in
1223 let last_node = and_after guard
(ctl_not prelabel_pred) after
in
1224 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1227 ctl_au CTL.NONSTRICT
rest_nodes last_node])) in
1228 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1229 let stmt_fvs = Ast.get_fvs stmt
in
1230 let fvs = get_unquantified quantified
stmt_fvs in
1231 quantify guard
(label_var::fvs)
1232 (sequencibility body label_pred process_bef_aft seqible
)
1234 (* --------------------------------------------------------------------- *)
1235 (* dots and nests *)
1237 let dots_au is_strict toend label
s wrapcode x seq_after y quantifier
=
1238 let matchgoto = gotopred None
in
1240 make_match None
false
1242 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1244 make_match None
false
1246 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1248 if quantifier
= Exists
1249 then Common.Left
(CTL.False
)
1251 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1253 then Common.Left
(aftpred label
)
1257 let lv = get_label_ctr() in
1258 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1259 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1260 ctl_or (aftpred label
)
1261 (quantify false [lv]
1262 (ctl_and CTL.NONSTRICT
1263 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1264 (ctl_au CTL.NONSTRICT
1265 (ctl_and CTL.NONSTRICT
(ctl_not v) preflabelpred)
1266 (ctl_and CTL.NONSTRICT
preflabelpred
1267 (if !Flag_matcher.only_return_is_error_exit
1269 (ctl_and CTL.NONSTRICT
1270 (retpred None
) (ctl_not seq_after
))
1273 (ctl_and CTL.NONSTRICT
1274 (ctl_or (retpred None
) matchcontinue)
1275 (ctl_not seq_after
))
1276 (ctl_and CTL.NONSTRICT
1277 (ctl_or matchgoto matchbreak)
1278 (ctl_ag s (ctl_not seq_after
)))))))))) in
1279 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1280 let v = get_let_ctr() in
1282 (match stop_early with
1283 Common.Left x
-> ctl_or y x
1284 | Common.Right
stop_early ->
1285 CTL.Let
(v,y
,ctl_or (CTL.Ref
v) (stop_early (CTL.Ref
v))))
1287 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1288 process_bef_aft statement_list statement guard quantified wrapcode
=
1289 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1290 (* proces bef_aft *)
1292 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1293 let bef_aft = (* to be negated *)
1297 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1300 with Not_found
-> shortest (Common.union_set bef aft
) in
1303 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1305 let check_quantifier quant other
=
1307 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1311 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1313 then failwith
"inconsistent annotation on dots"
1317 if check_quantifier Ast.WhenExists
Ast.WhenForall
1320 if check_quantifier Ast.WhenForall
Ast.WhenExists
1323 (* the following is used when we find a goto, etc and consider accepting
1324 without finding the rest of the pattern *)
1325 let aft = shortest aft in
1326 (* process whencode *)
1327 let labelled = label_pred_maker label
in
1329 let (poswhen
,negwhen
) =
1331 (function (poswhen
,negwhen
) ->
1333 Ast.WhenNot
whencodes ->
1334 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1335 | Ast.WhenAlways stm
->
1336 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1337 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1338 | Ast.WhenNotTrue
(e
) ->
1340 ctl_or (whencond_true e label guard quantified
) negwhen
)
1341 | Ast.WhenNotFalse
(e
) ->
1343 ctl_or (whencond_false e label guard quantified
) negwhen
))
1344 (CTL.True
,bef_aft) (List.rev
whencodes) in
1345 let poswhen = ctl_and_ns arg
poswhen in
1349 (* add in After, because it's not part of the program *)
1350 ctl_or (aftpred label
) negwhen
1352 ctl_and_ns poswhen (ctl_not negwhen) in
1353 (* process dot code, if any *)
1355 match (dotcode,guard
) with
1356 (None
,_) | (_,true) -> CTL.True
1357 | (Some
dotcode,_) -> dotcode in
1358 (* process nest code, if any *)
1359 (* whencode goes in the negated part of the nest; if no nest, just goes
1360 on the "true" in between code *)
1361 let plus_var = if plus
then get_label_ctr() else string2var "" in
1362 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1364 match (nest
,guard
&& not plus
) with
1365 (None
,_) | (_,true) -> whencodes CTL.True
1366 | (Some nest
,false) ->
1367 let v = get_let_ctr() in
1371 (* the idea is that BindGood is sort of a witness; a witness to
1372 having found the subterm in at least one place. If there is
1373 not a witness, then there is a risk that it will get thrown
1374 away, if it is merged with a node that has an empty
1375 environment. See tests/nestplus. But this all seems
1376 rather suspicious *)
1377 CTL.And
(CTL.NONSTRICT
,x
,
1378 CTL.Exists
(true,plus_var2,
1379 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1380 CTL.Modif
plus_var2)))
1383 CTL.Or
(is_plus (CTL.Ref
v),
1384 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1385 let plus_modifier x
=
1392 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1398 | Guard f
-> ctl_uncheck f
1400 let exit = endpred label
in
1401 let errorexit = exitpred label
in
1402 ctl_or exit errorexit
1403 (* not at all sure what the next two mean... *)
1407 Some
(lv,used) -> used := true;
1408 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1409 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1410 | None
-> endpred label
)
1411 (* was the following, but not clear why sgrep should allow
1413 let exit = endpred label in
1414 let errorexit = exitpred label in
1416 then ctl_or exit errorexit (* end anywhere *)
1417 else exit (* end at the real end of the function *) *)
in
1419 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1420 label
(guard_to_strict guard
) wrapcode
1421 (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
1422 aft ender quantifier)
1424 and get_whencond_exps e
=
1425 match Ast.unwrap e
with
1427 | Ast.DisjRuleElem
(res) ->
1428 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1429 | _ -> failwith
"not possible"
1431 and make_whencond_headers e e1 label guard quantified
=
1432 let fvs = Ast.get_fvs e
in
1434 quantify guard
(get_unquantified quantified
fvs)
1435 (make_match label guard h
) in
1440 (Ast.make_mcode
"if",
1441 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1442 let while_header e1
=
1446 (Ast.make_mcode
"while",
1447 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1452 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1453 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1455 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1457 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1459 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1460 (if_headers, while_headers, for_headers)
1462 and whencond_true e label guard quantified
=
1463 let e1 = get_whencond_exps e
in
1464 let (if_headers, while_headers, for_headers) =
1465 make_whencond_headers e
e1 label guard quantified
in
1467 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1468 (ctl_and CTL.NONSTRICT
1469 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1471 and whencond_false e label guard quantified
=
1472 let e1 = get_whencond_exps e
in
1473 let (if_headers, while_headers, for_headers) =
1474 make_whencond_headers e
e1 label guard quantified
in
1475 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1476 (ctl_and CTL.NONSTRICT
(fallpred label
)
1477 (ctl_or (ctl_back_ex if_headers)
1478 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1480 (* --------------------------------------------------------------------- *)
1481 (* the main translation loop *)
1483 let rec statement_list stmt_list after quantified minus_quantified
1484 label llabel slabel dots_before guard
=
1486 (* include Disj to be on the safe side *)
1487 match Ast.unwrap x
with
1488 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1489 let compute_label l e db
= if db
or isdots e
then l else None
in
1490 match Ast.unwrap stmt_list
with
1492 let rec loop quantified minus_quantified dots_before label llabel slabel
1494 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1496 statement e after quantified minus_quantified
1497 (compute_label label e dots_before
)
1499 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1500 let shared = intersectll fv
fvs in
1501 let unqshared = get_unquantified quantified
shared in
1502 let new_quantified = Common.union_set
unqshared quantified
in
1503 let minus_shared = intersectll mfv mfvs
in
1505 get_unquantified minus_quantified
minus_shared in
1506 let new_mquantified =
1507 Common.union_set
munqshared minus_quantified
in
1508 quantify guard
unqshared
1511 (let (label1
,llabel1
,slabel1
) =
1512 match Ast.unwrap e
with
1514 (match Ast.unwrap re
with
1515 Ast.Goto
_ -> (None
,None
,None
)
1516 | _ -> (label
,llabel
,slabel
))
1517 | _ -> (label
,llabel
,slabel
) in
1518 loop new_quantified new_mquantified (isdots e
)
1519 label1 llabel1 slabel1
1521 new_quantified new_mquantified
1522 (compute_label label e dots_before
) llabel slabel guard
)
1523 | _ -> failwith
"not possible" in
1524 loop quantified minus_quantified dots_before
1526 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1527 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1528 | Ast.STARS
(x
) -> failwith
"not supported"
1530 (* llabel is the label of the enclosing loop and slabel is the label of the
1532 and statement stmt after quantified minus_quantified
1533 label llabel slabel guard
=
1534 let ctl_au = ctl_au CTL.NONSTRICT
in
1535 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1536 let ctl_and = ctl_and CTL.NONSTRICT
in
1537 let make_seq = make_seq guard
in
1538 let make_seq_after = make_seq_after guard
in
1539 let real_make_match = make_match in
1540 let make_match = header_match label guard
in
1542 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1545 match Ast.unwrap stmt
with
1547 (match Ast.unwrap ast
with
1548 (* the following optimisation is not a good idea, because when S
1549 is alone, we would like it not to match a declaration.
1550 this makes more matching for things like when (...) S, but perhaps
1551 that matching is not so costly anyway *)
1552 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1553 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_)) as d),_),
1555 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_)) as d),_),
1557 svar_context_with_add_after stmt
s label quantified
d ast seqible
1559 (process_bef_aft quantified minus_quantified
1560 label llabel slabel
true)
1562 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1564 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1565 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1567 (process_bef_aft quantified minus_quantified
1568 label llabel slabel
true)
1570 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1574 match Ast.unwrap ast
with
1575 Ast.DisjRuleElem
(res) ->
1576 do_re_matches label guard
res quantified minus_quantified
1577 | Ast.Exp
(_) | Ast.Ty
(_) ->
1578 let stmt_fvs = Ast.get_fvs stmt
in
1579 let fvs = get_unquantified quantified
stmt_fvs in
1580 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1582 let stmt_fvs = Ast.get_fvs stmt
in
1583 let fvs = get_unquantified quantified
stmt_fvs in
1584 quantify guard
fvs (make_match ast
) in
1585 match Ast.unwrap ast
with
1586 Ast.Break
(brk
,semi
) ->
1587 (match (llabel
,slabel
) with
1588 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1589 ctl_and term (bclabel_pred_maker slabel
)
1590 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1591 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1592 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1593 (* discard pattern that comes after return *)
1594 let normal_res = make_seq_after term after
in
1595 (* the following code tries to propagate the modifications on
1596 return; to a close brace, in the case where the final return
1599 match (retmc
,semmc
) with
1600 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1601 when !Flag.sgrep_mode2
->
1602 (* in sgrep mode, we can propagate the - *)
1603 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,l1
@l2
))
1604 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
))
1605 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
)),
1606 Ast.CONTEXT
(_,Ast.AFTER
(l2
))) ->
1607 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
)))
1608 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1609 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1611 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1612 Ast.CONTEXT
(_,Ast.AFTER
(l))) ->
1613 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l)))
1615 let ret = Ast.make_mcode
"return" in
1617 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1618 let semi = Ast.make_mcode
";" in
1620 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1622 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1625 let exit = endpred None
in
1627 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1628 let stripped_rbrace =
1629 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1631 (ctl_and (make_match mod_rbrace)
1636 (ctl_or simple_return return_expr))))
1638 (make_match stripped_rbrace)
1639 (* error exit not possible; it is in the middle
1640 of code, so a return is needed *)
1643 (* some change in the middle of the return, so have to
1644 find an actual return *)
1647 (* should try to deal with the dots_bef_aft problem elsewhere,
1648 but don't have the courage... *)
1653 do_between_dots stmt
term End
1654 quantified minus_quantified label llabel slabel guard
in
1656 make_seq_after term after
)
1657 | Ast.Seq
(lbrace
,body,rbrace
) ->
1658 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1661 [Ast.get_fvs lbrace
;
1662 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1664 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1665 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1666 | _ -> failwith
"not possible" in
1667 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1669 seq_fvs minus_quantified
1670 [Ast.get_mfvs lbrace
;
1671 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1673 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1674 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1675 | _ -> failwith
"not possible" in
1676 let pv = count_nested_braces stmt
in
1677 let lv = get_label_ctr() in
1678 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1679 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1682 (quantify guard lbfvs
(make_match lbrace
))
1683 (ctl_and paren_pred label_pred) in
1685 match Ast.unwrap rbrace
with
1686 Ast.SeqEnd
((data
,info,_,pos)) ->
1687 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1688 | _ -> failwith
"unexpected close brace" in
1690 (* label is not needed; paren_pred is enough *)
1691 quantify guard rbfvs
1692 (ctl_au (make_match empty_rbrace)
1694 (real_make_match None guard rbrace
)
1696 let new_quantified2 =
1697 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1698 let new_mquantified2 =
1699 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1700 let pattern_as_given =
1701 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1702 quantify true [pv;lv]
1703 (quantify guard b1fvs
1706 quantify guard b2fvs
1707 (statement_list body
1708 (After
(make_seq_after end_brace after
))
1709 new_quantified2 new_mquantified2
1710 (Some
(lv,ref true)) llabel slabel
false guard
)])) in
1711 if ends_in_return body
1713 (* matching error handling code *)
1715 1. The pattern as given
1716 2. A goto, and then some close braces, and then the pattern as
1717 given, but without the braces (only possible if there are no
1718 decls, and open and close braces are unmodified)
1719 3. Part of the pattern as given, then a goto, and then the rest
1720 of the pattern. For this case, we just check that all paths have
1721 a goto within the current braces. checking for a goto at every
1722 point in the pattern seems expensive and not worthwhile. *)
1724 let body = preprocess_dots body in (* redo, to drop braces *)
1728 (make_match empty_rbrace)
1729 (ctl_ax (* skip the destination label *)
1730 (quantify guard b2fvs
1731 (statement_list body End
1732 new_quantified2 new_mquantified2 None llabel slabel
1735 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1736 quantify true [pv;lv]
1737 (quantify guard b1fvs
1741 (CTL.AU
(* want AF even for sgrep *)
1742 (CTL.FORWARD
,CTL.STRICT
,
1743 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1744 ctl_and (* brace must be eventually after goto *)
1745 (gotopred (Some
(lv,ref true)))
1746 (* want AF even for sgrep *)
1747 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1748 (quantify guard b2fvs
1749 (statement_list body Tail
1750 new_quantified2 new_mquantified2
1751 (Some
(lv,ref true))
1752 llabel slabel
false guard
))])) in
1753 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1754 else pattern_as_given
1755 | Ast.IfThen
(ifheader
,branch
,aft) ->
1756 ifthen ifheader branch
aft after quantified minus_quantified
1757 label llabel slabel statement
make_match guard
1759 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1760 ifthenelse ifheader branch1 els branch2
aft after quantified
1761 minus_quantified label llabel slabel statement
make_match guard
1763 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1764 | Ast.Iterator
(header,body,aft) ->
1765 forwhile header body aft after quantified minus_quantified
1766 label statement
make_match guard
1768 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1770 (label_pred_maker label
)
1771 (List.fold_left
ctl_seqor CTL.False
1774 statement_list sl after quantified minus_quantified label
1775 llabel slabel
true guard
)
1778 | Ast.Nest
(stmt_dots
,whencode
,multi
,bef
,aft) ->
1779 (* label in recursive call is None because label check is already
1780 wrapped around the corresponding code *)
1783 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1785 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1786 | _ -> failwith
"not possible" in
1788 (* no minus version because when code doesn't contain any minus code *)
1789 let new_quantified = Common.union_set
bfvs quantified
in
1793 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1794 None llabel slabel
true guard
in
1795 dots_and_nests multi
1796 (Some
dots_pattern) whencode bef
aft None after label
1797 (process_bef_aft
new_quantified minus_quantified
1798 None llabel slabel
true)
1800 statement_list x Tail
new_quantified minus_quantified None
1801 llabel slabel
true true)
1803 statement x Tail
new_quantified minus_quantified None
1806 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1808 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1811 Ast.MINUS
(_,_,_,_) ->
1812 (* no need for the fresh metavar, but ... is a bit weird as a
1814 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1816 dots_and_nests false None
whencodes bef
aft dot_code after label
1817 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1819 statement_list x Tail quantified minus_quantified
1820 None llabel slabel
true true)
1822 statement x Tail quantified minus_quantified None llabel slabel
true)
1824 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1826 | Ast.Switch
(header,lb
,cases,rb
) ->
1827 let rec intersect_all = function
1830 | x
::xs -> intersect x
(intersect_all xs) in
1831 let rec union_all l = List.fold_left
union [] l in
1832 (* start normal variables *)
1833 let header_fvs = Ast.get_fvs
header in
1834 let lb_fvs = Ast.get_fvs lb
in
1835 let case_fvs = List.map
Ast.get_fvs
cases in
1836 let rb_fvs = Ast.get_fvs rb
in
1837 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1838 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1840 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1841 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1842 function case_fvs ->
1843 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
1844 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
1845 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
1846 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
1848 | _ -> failwith
"not possible")
1849 ([],[],[],[],[],[],[]) case_fvs in
1850 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1851 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1852 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
1853 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
1854 List.rev all_rbfvs
) in
1855 let exponlyfvs = intersect_all all_efvs
in
1856 let lbonlyfvs = intersect_all all_lbfvs
in
1857 (* don't do anything with right brace. Hope there is no + code on it *)
1858 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1859 let b1fvs = union_all all_b1fvs
in
1860 let new1_quantified = union b1fvs quantified
in
1861 let b2fvs = union (union_all all_b1fvs
) (intersect_all all_casefvs
) in
1862 let new2_quantified = union b2fvs new1_quantified in
1863 (* let b3fvs = union_all all_b3fvs in*)
1864 (* ------------------- start minus free variables *)
1865 let header_mfvs = Ast.get_mfvs
header in
1866 let lb_mfvs = Ast.get_mfvs lb
in
1867 let case_mfvs = List.map
Ast.get_mfvs
cases in
1868 let rb_mfvs = Ast.get_mfvs rb
in
1869 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1870 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1872 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1873 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1874 function case_mfvs ->
1877 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1878 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
1879 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
1880 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
1882 | _ -> failwith
"not possible")
1883 ([],[],[],[],[],[],[]) case_mfvs in
1884 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1885 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1886 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
1887 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
1888 List.rev all_mrbfvs
) in
1889 (* don't do anything with right brace. Hope there is no + code on it *)
1890 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1891 let mb1fvs = union_all all_mb1fvs
in
1892 let new1_mquantified = union mb1fvs quantified
in
1893 let mb2fvs = union (union_all all_mb1fvs
) (intersect_all all_mcasefvs
) in
1894 let new2_mquantified = union mb2fvs new1_mquantified in
1895 (* let b3fvs = union_all all_b3fvs in*)
1896 (* ------------------- end collection of free variables *)
1897 let switch_header = quantify guard
exponlyfvs (make_match header) in
1898 let lb = quantify guard
lbonlyfvs (make_match lb) in
1899 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
1902 (function case_line
->
1903 match Ast.unwrap case_line
with
1904 Ast.CaseLine
(header,body) ->
1906 match seq_fvs new2_quantified [Ast.get_fvs
header] with
1907 [(e1fvs,_)] -> e1fvs
1908 | _ -> failwith
"not possible" in
1909 quantify guard
e1fvs (real_make_match label
true header)
1910 | Ast.OptCase
(case_line
) -> failwith
"not supported")
1913 ctl_not (List.fold_left
ctl_or_fl CTL.False
case_headers) in
1914 let lv = get_label_ctr() in
1915 let used = ref false in
1918 (function case_line
->
1919 match Ast.unwrap case_line
with
1920 Ast.CaseLine
(header,body) ->
1921 let (e1fvs,b1fvs,s1fvs
) =
1922 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
1923 match seq_fvs new2_quantified fvs with
1924 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
1925 | _ -> failwith
"not possible" in
1926 let (me1fvs
,mb1fvs,ms1fvs
) =
1927 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
1928 match seq_fvs new2_mquantified fvs with
1929 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
1930 | _ -> failwith
"not possible" in
1932 quantify guard
e1fvs (make_match header) in
1933 let new3_quantified = union b1fvs new2_quantified in
1934 let new3_mquantified = union mb1fvs new2_mquantified in
1936 statement_list body Tail
1937 new3_quantified new3_mquantified label llabel
1938 (Some
(lv,used)) true(*?*) guard
in
1939 quantify guard
b1fvs (make_seq [case_header; body])
1940 | Ast.OptCase
(case_line
) -> failwith
"not supported")
1942 let default_required =
1945 match Ast.unwrap case
with
1946 Ast.CaseLine
(header,_) ->
1947 (match Ast.unwrap
header with
1948 Ast.Default
(_,_) -> true
1952 then function x
-> x
1953 else function x
-> ctl_or (fallpred label
) x
in
1954 let after_pred = aftpred label
in
1955 let body after_branch
=
1958 (quantify guard
b2fvs
1961 (List.fold_left
ctl_and CTL.True
1962 (List.map
ctl_ex case_headers));
1963 List.fold_left
ctl_or_fl no_header case_code])))
1966 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
1967 match Ast.unwrap
rb with
1968 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
1969 | _ -> failwith
"not possible") in
1970 let (switch_header,wrapper
) =
1973 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1974 (ctl_and switch_header label_pred,
1975 (function body -> quantify true [lv] body))
1976 else (switch_header,function x
-> x
) in
1978 (end_control_structure b1fvs switch_header body
1979 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
1980 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
1981 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
1984 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
1985 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1987 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
1988 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
1989 | _ -> failwith
"not possible" in
1990 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
1993 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
1994 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1996 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
1997 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
1998 | _ -> failwith
"not possible" in
1999 let function_header = quantify guard hfvs
(make_match header) in
2000 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2001 let stripped_rbrace =
2002 match Ast.unwrap rbrace
with
2003 Ast.SeqEnd
((data
,info,_,_)) ->
2004 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2005 | _ -> failwith
"unexpected close brace" in
2007 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2008 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2009 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2011 (quantify guard rbfvs
(make_match rbrace
))
2013 (* the following finds the beginning of the fake braces,
2014 if there are any, not completely sure how this works.
2015 sse the examples sw and return *)
2016 (ctl_back_ex (ctl_not fake_brace))
2017 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2018 let new_quantified3 =
2019 Common.union_set
b1fvs
2020 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2021 let new_mquantified3 =
2022 Common.union_set
mb1fvs
2023 (Common.union_set
mb2fvs
2024 (Common.union_set mb3fvs minus_quantified
)) in
2026 match (Ast.undots
body,
2027 contains_modif rbrace
or contains_pos rbrace
) with
2029 (match Ast.unwrap
body with
2030 Ast.Nest
(stmt_dots
,[],multi
,_,_) ->
2032 then None
(* not sure how to optimize this case *)
2033 else Some
(Common.Left stmt_dots
)
2034 | Ast.Dots
(_,whencode
,_,_) when
2036 (* flow sensitive, so not optimizable *)
2037 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2039 | _ -> true) whencode
) ->
2040 Some
(Common.Right whencode
)
2045 Some
(Common.Left stmt_dots
) ->
2046 (* special case for function header + body - header is unambiguous
2047 and unique, so we can just look for the nested body anywhere
2050 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2051 statement_list stmt_dots
2052 (* discards match on right brace, but don't need it *)
2053 (Guard
(make_seq_after end_brace after
))
2054 new_quantified3 new_mquantified3
2055 None llabel slabel
true guard
)
2056 | Some
(Common.Right whencode
) ->
2057 (* try to be more efficient for the case where the body is just
2058 ... Perhaps this is too much of a special case, but useful
2059 for dropping a parameter and checking that it is never used. *)
2071 Ast.WhenAlways
(s) -> prev
2072 | Ast.WhenNot
(sl
) ->
2074 statement_list sl Tail
2075 new_quantified3 new_mquantified3
2076 label llabel slabel
true true in
2078 | Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2079 failwith
"unexpected"
2080 | Ast.WhenModifier
(Ast.WhenAny
) -> CTL.False
2081 | Ast.WhenModifier
(_) -> prev
)
2082 CTL.False whencode
))
2086 Ast.WhenAlways
(s) ->
2089 new_quantified3 new_mquantified3
2090 label llabel slabel
true in
2092 | Ast.WhenNot
(sl
) -> prev
2093 | Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2094 failwith
"unexpected"
2095 | Ast.WhenModifier
(Ast.WhenAny
) -> CTL.True
2096 | Ast.WhenModifier
(_) -> prev
)
2097 CTL.True whencode
) in
2098 ctl_au leftarg (make_match stripped_rbrace)]
2102 quantify guard
b3fvs
2103 (statement_list body
2104 (After
(make_seq_after end_brace after
))
2105 new_quantified3 new_mquantified3 None llabel slabel
2107 quantify guard
b1fvs
2108 (make_seq [function_header; quantify guard
b2fvs body_code])
2109 | Ast.Define
(header,body) ->
2110 let (hfvs
,bfvs,bodyfvs
) =
2111 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2113 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2114 | _ -> failwith
"not possible" in
2115 let (mhfvs
,mbfvs
,mbodyfvs
) =
2116 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2118 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2119 | _ -> failwith
"not possible" in
2120 let define_header = quantify guard hfvs
(make_match header) in
2122 statement_list body after
2123 (Common.union_set
bfvs quantified
)
2124 (Common.union_set mbfvs minus_quantified
)
2125 None llabel slabel
true guard
in
2126 quantify guard
bfvs (make_seq [define_header; body_code])
2127 | Ast.OptStm
(stm
) ->
2128 failwith
"OptStm should have been compiled away\n"
2129 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2130 | _ -> failwith
"not supported" in
2131 if guard
or !dots_done
2134 do_between_dots stmt
term after quantified minus_quantified
2135 label llabel slabel guard
2137 (* term is the translation of stmt *)
2138 and do_between_dots stmt
term after quantified minus_quantified
2139 label llabel slabel guard
=
2140 match Ast.get_dots_bef_aft stmt
with
2141 Ast.AddingBetweenDots
(brace_term
,n
)
2142 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2144 statement brace_term after quantified minus_quantified
2145 label llabel slabel guard
in
2146 let v = Printf.sprintf
"_r_%d" n
in
2147 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2148 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2151 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2152 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2154 | Ast.NoDots
-> term
2156 (* un_process_bef_aft is because we don't want to do transformation in this
2157 code, and thus don't case about braces before or after it *)
2158 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2160 Ast.WParen
(re
,n
) ->
2161 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2162 let s = guard_to_strict guard
in
2163 quantify true (get_unquantified quantified
[n
])
2164 (ctl_and s (make_raw_match None guard re
) paren_pred)
2166 statement
s Tail quantified minus_quantified label llabel slabel guard
2167 | Ast.Other_dots
d ->
2168 statement_list d Tail quantified minus_quantified
2169 label llabel slabel
true guard
2171 (* --------------------------------------------------------------------- *)
2172 (* cleanup: convert AX to EX for pdots.
2173 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2174 This is what we wanted in the first place, but it wasn't possible to make
2175 because the AX and its argument are not created in the same place.
2177 (* also cleanup XX, which is a marker for the case where the programmer
2178 specifies to change the quantifier on .... Assumed to only occur after one AX
2179 or EX, or at top level. *)
2182 let c = match c with CTL.XX
(c) -> c | _ -> c in
2184 CTL.False
-> CTL.False
2185 | CTL.True
-> CTL.True
2186 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2187 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2188 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2189 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2190 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2191 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2192 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2193 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2194 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2195 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2196 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2197 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2198 | CTL.AX
(CTL.FORWARD
,s,
2200 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2201 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2203 CTL.And
(CTL.NONSTRICT
,
2204 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2205 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2206 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2207 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2208 CTL.AX
(dir
,s,cleanup phi
)
2209 | CTL.XX
(phi
) -> failwith
"bad XX"
2210 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2211 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2212 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2213 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2214 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2215 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2216 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2217 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2218 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2219 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2220 | CTL.Ref
(s) -> CTL.Ref
(s)
2221 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2222 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2224 (* --------------------------------------------------------------------- *)
2225 (* Function declaration *)
2227 let top_level name
(ua
,pos) t
=
2228 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2230 saved := Ast.get_saved t
;
2231 let quantified = Common.minus_set
ua pos in
2232 quantify false quantified
2233 (match Ast.unwrap t
with
2234 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2236 let unopt = elim_opt.V.rebuilder_statement stmt
in
2237 let unopt = preprocess_dots_e unopt in
2238 cleanup(statement
unopt VeryEnd
quantified [] None None None
false)
2239 | Ast.CODE
(stmt_dots
) ->
2240 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2241 let unopt = preprocess_dots unopt in
2242 let starts_with_dots =
2243 match Ast.undots stmt_dots
with
2245 (match Ast.unwrap
d with
2246 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2247 | Ast.Stars
(_,_,_,_) -> true
2250 let starts_with_brace =
2251 match Ast.undots stmt_dots
with
2253 (match Ast.unwrap
d with
2258 statement_list unopt VeryEnd
quantified [] None None None
2261 (if starts_with_dots
2263 (* EX because there is a loop on enter/top *)
2264 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2265 else if starts_with_brace
2267 ctl_and CTL.NONSTRICT
2268 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2270 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords")
2272 (* --------------------------------------------------------------------- *)
2275 let asttoctlz (name
,(_,_,exists_flag
),l) used_after positions
=
2278 (match exists_flag
with
2279 Ast.Exists
-> exists := Exists
2280 | Ast.Forall
-> exists := Forall
2281 | Ast.ReverseForall
-> exists := ReverseForall
2282 | Ast.Undetermined
->
2283 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2285 let (l,used_after) =
2289 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2290 (List.combine
l (List.combine
used_after positions
))) in
2291 let res = List.map2
(top_level name
) used_after l in
2295 let asttoctl r
used_after positions
=
2297 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2298 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2299 asttoctlz (a,b
,c) used_after positions
2300 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CTL.True
]
2302 let pp_cocci_predicate (pred
,modif
) =
2303 Pretty_print_engine.pp_predicate pred
2305 let cocci_predicate_to_string (pred
,modif
) =
2306 Pretty_print_engine.predicate_to_string pred