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
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
)
96 let ctl_ax_absolute s
= function
98 | CTL.False
-> CTL.False
99 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
101 let ctl_ex = function
103 | CTL.False
-> CTL.False
104 | x
-> CTL.EX
(CTL.FORWARD
,x
)
106 (* This stays being AX even for sgrep_mode, because it is used to identify
107 the structure of the term, not matching the pattern. *)
108 let ctl_back_ax = function
110 | CTL.False
-> CTL.False
111 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
113 let ctl_back_ex = function
115 | CTL.False
-> CTL.False
116 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
118 let ctl_ef = function
120 | CTL.False
-> CTL.False
121 | x
-> CTL.EF
(CTL.FORWARD
,x
)
123 let ctl_ag s
= function
125 | CTL.False
-> CTL.False
126 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
129 match (x
,!exists) with
130 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
131 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
132 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
133 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
135 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
137 (match (x
,!exists) with
138 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
139 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
140 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
141 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
143 let ctl_uncheck = function
145 | CTL.False
-> CTL.False
148 let label_pred_maker = function
150 | Some
(label_var
,used
) ->
152 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
154 let bclabel_pred_maker = function
156 | Some
(label_var
,used
) ->
158 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
160 let predmaker guard pred label
=
161 ctl_and (guard_to_strict guard
) (CTL.Pred pred
) (label_pred_maker label
)
163 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
164 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
165 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
166 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
167 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
168 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
169 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
170 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
171 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
172 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
173 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
175 let aftret label_var f
= ctl_or (aftpred label_var
) (exitpred label_var
)
181 Printf.sprintf
"r%d" cur
183 (* --------------------------------------------------------------------- *)
184 (* --------------------------------------------------------------------- *)
185 (* Eliminate OptStm *)
187 (* for optional thing with nothing after, should check that the optional thing
188 never occurs. otherwise the matching stops before it occurs *)
191 let donothing r k e
= k e
in
194 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
197 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
200 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
202 let inheritedlist l
=
203 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
206 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
209 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
211 let rec dots_list unwrapped wrapped
=
212 match (unwrapped
,wrapped
) with
215 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
217 | (Ast.Nest
(_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
219 let l = Ast.get_line stm
in
220 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
221 let new_rest2 = dots_list urest rest
in
222 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
223 varlists new_rest1 in
224 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
225 varlists new_rest2 in
229 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
231 Ast.free_vars
= fv_rest1
;
232 Ast.minus_free_vars
= mfv_rest1
;
233 Ast.fresh_vars
= fresh_rest1
;
234 Ast.inherited
= inherited_rest1
;
235 Ast.saved_witness
= s1
};
236 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
238 Ast.free_vars
= fv_rest2
;
239 Ast.minus_free_vars
= mfv_rest2
;
240 Ast.fresh_vars
= fresh_rest2
;
241 Ast.inherited
= inherited_rest2
;
242 Ast.saved_witness
= s2
}])) with
244 Ast.free_vars
= fv_rest1
;
245 Ast.minus_free_vars
= mfv_rest1
;
246 Ast.fresh_vars
= fresh_rest1
;
247 Ast.inherited
= inherited_rest1
;
248 Ast.saved_witness
= s1
}]
250 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
251 let l = Ast.get_line stm
in
252 let new_rest1 = dots_list urest rest
in
253 let new_rest2 = stm
::new_rest1 in
254 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
255 varlists new_rest1 in
256 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
257 varlists new_rest2 in
260 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
262 Ast.free_vars
= fv_rest2
;
263 Ast.minus_free_vars
= mfv_rest2
;
264 Ast.fresh_vars
= fresh_rest2
;
265 Ast.inherited
= inherited_rest2
;
266 Ast.saved_witness
= s2
};
267 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
269 Ast.free_vars
= fv_rest1
;
270 Ast.minus_free_vars
= mfv_rest1
;
271 Ast.fresh_vars
= fresh_rest1
;
272 Ast.inherited
= inherited_rest1
;
273 Ast.saved_witness
= s1
}])) with
275 Ast.free_vars
= fv_rest2
;
276 Ast.minus_free_vars
= mfv_rest2
;
277 Ast.fresh_vars
= fresh_rest2
;
278 Ast.inherited
= inherited_rest2
;
279 Ast.saved_witness
= s2
}]
281 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
282 let l = Ast.get_line stm
in
283 let fv_stm = Ast.get_fvs stm
in
284 let mfv_stm = Ast.get_mfvs stm
in
285 let fresh_stm = Ast.get_fresh stm
in
286 let inh_stm = Ast.get_inherited stm
in
287 let saved_stm = Ast.get_saved stm
in
288 let fv_d1 = Ast.get_fvs d1
in
289 let mfv_d1 = Ast.get_mfvs d1
in
290 let fresh_d1 = Ast.get_fresh d1
in
291 let inh_d1 = Ast.get_inherited d1
in
292 let saved_d1 = Ast.get_saved d1
in
293 let fv_both = Common.union_set
fv_stm fv_d1 in
294 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
295 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
296 let inh_both = Common.union_set
inh_stm inh_d1 in
297 let saved_both = Common.union_set
saved_stm saved_d1 in
301 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
303 Ast.free_vars
= fv_stm;
304 Ast.minus_free_vars
= mfv_stm;
305 Ast.fresh_vars
= fresh_stm;
306 Ast.inherited
= inh_stm;
307 Ast.saved_witness
= saved_stm};
308 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
310 Ast.free_vars
= fv_d1;
311 Ast.minus_free_vars
= mfv_d1;
312 Ast.fresh_vars
= fresh_d1;
313 Ast.inherited
= inh_d1;
314 Ast.saved_witness
= saved_d1}])) with
316 Ast.free_vars
= fv_both;
317 Ast.minus_free_vars
= mfv_both;
318 Ast.fresh_vars
= fresh_both;
319 Ast.inherited
= inh_both;
320 Ast.saved_witness
= saved_both}]
322 | ([Ast.Nest
(_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
323 let l = Ast.get_line stm
in
324 let rw = Ast.rewrap stm
in
325 let rwd = Ast.rewrap stm
in
326 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
328 [rwd(Ast.DOTS
([stm
]));
329 {(Ast.make_term
(Ast.DOTS
([rw dots])))
330 with Ast.node_line
= l}])]
332 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
333 | _
-> failwith
"not possible" in
335 let stmtdotsfn r k d
=
338 (match Ast.unwrap
d with
339 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
340 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
341 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
344 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
345 donothing donothing stmtdotsfn donothing
346 donothing donothing donothing donothing donothing donothing donothing
347 donothing donothing donothing donothing donothing
349 (* --------------------------------------------------------------------- *)
350 (* after management *)
351 (* We need Guard for the following case:
360 Here the inner <... b ...> should not go past foo. But foo is not the
361 "after" of the body of the outer nest, because we don't want to search for
362 it in the case where the body of the outer nest ends in something other
363 than dots or a nest. *)
365 (* what is the difference between tail and end??? *)
367 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
369 let a2n = function After x
-> Guard x
| a
-> a
372 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
373 let pp_meta (_
,x
) = Common.pp x
in
374 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
375 Format.print_newline
()
377 let print_after = function
378 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
379 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
380 | Tail
-> Printf.printf
"Tail\n"
381 | VeryEnd
-> Printf.printf
"Very End\n"
382 | End
-> Printf.printf
"End\n"
384 (* --------------------------------------------------------------------- *)
387 let fresh_var _
= string2var "_v"
388 let fresh_pos _
= string2var "_pos" (* must be a constant *)
390 let fresh_metavar _
= "_S"
392 (* fvinfo is going to end up being from the whole associated statement.
393 it would be better if it were just the free variables in d, but free_vars.ml
394 doesn't keep track of free variables on + code *)
395 let make_meta_rule_elem d fvinfo
=
396 let nm = fresh_metavar() in
397 Ast.make_meta_rule_elem nm d fvinfo
399 let get_unquantified quantified vars
=
400 List.filter
(function x
-> not
(List.mem x quantified
)) vars
402 let make_seq guard
l =
403 let s = guard_to_strict guard
in
404 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
406 let make_seq_after2 guard first rest
=
407 let s = guard_to_strict guard
in
409 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
412 let make_seq_after guard first rest
=
414 After rest
-> make_seq guard
[first
;rest
]
417 let opt_and guard first rest
=
418 let s = guard_to_strict guard
in
421 | Some first
-> ctl_and s first rest
423 let and_after guard first rest
=
424 let s = guard_to_strict guard
in
425 match rest
with After rest
-> ctl_and s first rest
| _
-> first
428 let bind x y
= x
or y
in
429 let option_default = false in
430 let mcode r
(_
,_
,kind
,metapos
) =
432 Ast.MINUS
(_
,_
,_
,_
) -> true
433 | Ast.PLUS
-> failwith
"not possible"
434 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
435 let do_nothing r k e
= k e
in
436 let rule_elem r k re
=
438 match Ast.unwrap re
with
439 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
440 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
441 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
444 V.combiner
bind option_default
445 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
446 do_nothing do_nothing do_nothing do_nothing
447 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
448 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
449 recursor.V.combiner_rule_elem
452 let bind x y
= x
or y
in
453 let option_default = false in
454 let mcode r
(_
,_
,kind
,metapos
) =
456 Ast.MetaPos
(_
,_
,_
,_
,_
) -> true
457 | Ast.NoMetaPos
-> false in
458 let do_nothing r k e
= k e
in
459 let rule_elem r k re
=
461 match Ast.unwrap re
with
462 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
463 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
464 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
467 V.combiner
bind option_default
468 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
469 do_nothing do_nothing do_nothing do_nothing
470 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
471 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
472 recursor.V.combiner_rule_elem
474 (* code is not a DisjRuleElem *)
475 let make_match label guard code
=
476 let v = fresh_var() in
477 let matcher = Lib_engine.Match
(code
) in
478 if contains_modif code
&& not guard
479 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
481 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
482 (match (iso_info,!onlyModif,guard
,
483 intersect !used_after (Ast.get_fvs code
)) with
484 (false,true,_
,[]) | (_
,_
,true,_
) ->
485 predmaker guard
(matcher,CTL.Control
) label
486 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
488 let make_raw_match label guard code
=
489 predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
491 let rec seq_fvs quantified
= function
494 let t1fvs = get_unquantified quantified fv1
in
496 List.fold_left
Common.union_set
[]
497 (List.map
(get_unquantified quantified
) fvs
) in
498 let bothfvs = Common.inter_set
t1fvs termfvs in
499 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
500 let new_quantified = Common.union_set
bothfvs quantified
in
501 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
506 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
508 let non_saved_quantify =
510 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
512 let intersectll lst nested_list
=
513 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
515 (* --------------------------------------------------------------------- *)
516 (* Count depth of braces. The translation of a closed brace appears deeply
517 nested within the translation of the sequence term, so the name of the
518 paren var has to take into account the names of the nested braces. On the
519 other hand the close brace does not escape, so we don't have to take into
520 account other paren variable names. *)
522 (* called repetitively, which is inefficient, but less trouble than adding a
523 new field to Seq and FunDecl *)
524 let count_nested_braces s =
525 let bind x y
= max x y
in
526 let option_default = 0 in
527 let stmt_count r k
s =
528 match Ast.unwrap
s with
529 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
531 let donothing r k e
= k e
in
533 let recursor = V.combiner
bind option_default
534 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
535 donothing donothing donothing donothing
536 donothing donothing donothing donothing donothing donothing
537 donothing donothing stmt_count donothing donothing donothing in
538 let res = string_of_int
(recursor.V.combiner_statement
s) in
542 let get_label_ctr _
=
543 let cur = !labelctr in
545 string2var (Printf.sprintf
"l%d" cur)
547 (* --------------------------------------------------------------------- *)
548 (* annotate dots with before and after neighbors *)
550 let print_bef_aft = function
552 Printf.printf
"bef/aft\n";
553 Pretty_print_cocci.rule_elem "" re
;
554 Format.print_newline
()
556 Printf.printf
"bef/aft\n";
557 Pretty_print_cocci.statement
"" s;
558 Format.print_newline
()
559 | Ast.Other_dots
d ->
560 Printf.printf
"bef/aft\n";
561 Pretty_print_cocci.statement_dots
d;
562 Format.print_newline
()
564 (* [] can only occur if we are in a disj, where it comes from a ? In that
565 case, we want to use a, which accumulates all of the previous patterns in
567 let rec get_before_elem sl a
=
568 match Ast.unwrap sl
with
572 [] -> ([],Common.Right a
)
574 let (e
,ea
) = get_before_e e a
in
577 let (e
,ea
) = get_before_e e a
in
578 let (sl
,sla
) = loop sl ea
in
580 let (l,a
) = loop x a
in
581 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
582 | Ast.CIRCLES
(x
) -> failwith
"not supported"
583 | Ast.STARS
(x
) -> failwith
"not supported"
585 and get_before sl a
=
586 match get_before_elem sl a
with
587 (term
,Common.Left x
) -> (term
,x
)
588 | (term
,Common.Right x
) -> (term
,x
)
590 and get_before_whencode wc
=
593 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
594 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
595 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
596 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
597 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
600 and get_before_e
s a
=
601 match Ast.unwrap
s with
602 Ast.Dots
(d,w
,_
,aft
) ->
603 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
604 | Ast.Nest
(stmt_dots
,w
,multi
,_
,aft
) ->
605 let w = get_before_whencode
w in
606 let (sd
,_
) = get_before stmt_dots a
in
608 got rid of this, don't want to let nests overshoot
613 Unify_ast.unify_statement_dots
614 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
616 Unify_ast.MAYBE -> false
618 | Ast.Other_dots a ->
619 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
621 Unify_ast.MAYBE -> false
625 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,a,aft
)),[Ast.Other_dots stmt_dots
])
626 | Ast.Disj
(stmt_dots_list
) ->
628 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
629 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
631 (match Ast.unwrap ast
with
632 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
633 | _
-> (s,[Ast.Other
s]))
634 | Ast.Seq
(lbrace
,body
,rbrace
) ->
635 let index = count_nested_braces s in
636 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
637 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
638 | Ast.Define
(header
,body
) ->
639 let (body
,_
) = get_before body
[] in
640 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
641 | Ast.IfThen
(ifheader
,branch
,aft
) ->
642 let (br
,_
) = get_before_e branch
[] in
643 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
644 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
645 let (br1
,_
) = get_before_e branch1
[] in
646 let (br2
,_
) = get_before_e branch2
[] in
647 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
648 | Ast.While
(header
,body
,aft
) ->
649 let (bd
,_
) = get_before_e body
[] in
650 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
651 | Ast.For
(header
,body
,aft
) ->
652 let (bd
,_
) = get_before_e body
[] in
653 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
654 | Ast.Do
(header
,body
,tail
) ->
655 let (bd
,_
) = get_before_e body
[] in
656 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
657 | Ast.Iterator
(header
,body
,aft
) ->
658 let (bd
,_
) = get_before_e body
[] in
659 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
660 | Ast.Switch
(header
,lb
,cases
,rb
) ->
663 (function case_line
->
664 match Ast.unwrap case_line
with
665 Ast.CaseLine
(header
,body
) ->
666 let (body
,_
) = get_before body
[] in
667 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
668 | Ast.OptCase
(case_line
) -> failwith
"not supported")
670 (Ast.rewrap
s (Ast.Switch
(header
,lb
,cases,rb
)),[Ast.Other
s])
671 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
672 let (bd
,_
) = get_before body
[] in
673 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
675 Pretty_print_cocci.statement
"" s; Format.print_newline
();
676 failwith
"get_before_e: not supported"
678 let rec get_after sl
a =
679 match Ast.unwrap sl
with
685 let (sl
,sla
) = loop sl
in
686 let (e
,ea
) = get_after_e e sla
in
688 let (l,a) = loop x
in
689 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
690 | Ast.CIRCLES
(x
) -> failwith
"not supported"
691 | Ast.STARS
(x
) -> failwith
"not supported"
693 and get_after_whencode
a wc
=
696 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
697 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
698 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
699 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
700 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
703 and get_after_e
s a =
704 match Ast.unwrap
s with
705 Ast.Dots
(d,w,bef
,_
) ->
706 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
707 | Ast.Nest
(stmt_dots
,w,multi
,bef
,_
) ->
708 let w = get_after_whencode
a w in
709 let (sd
,_
) = get_after stmt_dots
a in
711 got rid of this. don't want to let nests overshoot
716 Unify_ast.unify_statement_dots
717 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
719 Unify_ast.MAYBE -> false
721 | Ast.Other_dots a ->
722 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
724 Unify_ast.MAYBE -> false
728 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,bef
,a)),[Ast.Other_dots stmt_dots
])
729 | Ast.Disj
(stmt_dots_list
) ->
731 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
732 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
734 (match Ast.unwrap ast
with
735 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
736 (* check "after" information for metavar optimization *)
737 (* if the error is not desired, could just return [], then
738 the optimization (check for EF) won't take place *)
742 (match Ast.unwrap x
with
743 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
745 "dots/nest not allowed before and after stmt metavar"
747 | Ast.Other_dots x
->
748 (match Ast.undots x
with
750 (match Ast.unwrap x
with
751 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
753 ("dots/nest not allowed before and after stmt "^
762 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
763 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
764 | _
-> (s,[Ast.Other
s]))
765 | Ast.Seq
(lbrace
,body
,rbrace
) ->
766 let index = count_nested_braces s in
767 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
768 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
769 [Ast.WParen
(lbrace
,index)])
770 | Ast.Define
(header
,body
) ->
771 let (body
,_
) = get_after body
a in
772 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
773 | Ast.IfThen
(ifheader
,branch
,aft
) ->
774 let (br
,_
) = get_after_e branch
a in
775 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
776 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
777 let (br1
,_
) = get_after_e branch1
a in
778 let (br2
,_
) = get_after_e branch2
a in
779 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
780 | Ast.While
(header
,body
,aft
) ->
781 let (bd
,_
) = get_after_e body
a in
782 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
783 | Ast.For
(header
,body
,aft
) ->
784 let (bd
,_
) = get_after_e body
a in
785 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
786 | Ast.Do
(header
,body
,tail
) ->
787 let (bd
,_
) = get_after_e body
a in
788 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
789 | Ast.Iterator
(header
,body
,aft
) ->
790 let (bd
,_
) = get_after_e body
a in
791 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
792 | Ast.Switch
(header
,lb
,cases,rb
) ->
795 (function case_line
->
796 match Ast.unwrap case_line
with
797 Ast.CaseLine
(header
,body
) ->
798 let (body
,_
) = get_after body
[] in
799 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
800 | Ast.OptCase
(case_line
) -> failwith
"not supported")
802 (Ast.rewrap
s (Ast.Switch
(header
,lb
,cases,rb
)),[Ast.Other
s])
803 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
804 let (bd
,_
) = get_after body
[] in
805 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
806 | _
-> failwith
"get_after_e: not supported"
808 let preprocess_dots sl
=
809 let (sl
,_
) = get_before sl
[] in
810 let (sl
,_
) = get_after sl
[] in
813 let preprocess_dots_e sl
=
814 let (sl
,_
) = get_before_e sl
[] in
815 let (sl
,_
) = get_after_e sl
[] in
818 (* --------------------------------------------------------------------- *)
819 (* various return_related things *)
821 let rec ends_in_return stmt_list
=
822 match Ast.unwrap stmt_list
with
824 (match List.rev x
with
826 (match Ast.unwrap x
with
829 match Ast.unwrap x
with
830 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
831 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
834 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
837 | Ast.CIRCLES
(x
) -> failwith
"not supported"
838 | Ast.STARS
(x
) -> failwith
"not supported"
840 (* --------------------------------------------------------------------- *)
843 let exptymatch l make_match make_guard_match
=
844 let pos = fresh_pos() in
845 let matches_guard_matches =
848 let pos = Ast.make_mcode
pos in
849 (make_match (Ast.set_pos x
(Some
pos)),
850 make_guard_match
(Ast.set_pos x
(Some
pos))))
852 let (matches
,guard_matches
) = List.split
matches_guard_matches in
853 let rec suffixes = function
855 | x
::xs -> xs::(suffixes xs) in
857 (* normally, we check that an expression does not match something
858 earlier in the disjunction (calculated as prefixes). But for large
859 disjunctions, this can result in a very big CTL formula. So we
860 give the user the option to say he doesn't want this feature, if that is
862 if !Flag_matcher.no_safe_expressions
863 then List.map
(function _
-> []) matches
864 else List.rev
(suffixes (List.rev guard_matches
)) in
865 let info = (* not null *)
871 ctl_and CTL.NONSTRICT
matcher
873 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
875 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
877 (* code might be a DisjRuleElem, in which case we break it apart
878 code might contain an Exp or Ty
879 this one pushes the quantifier inwards *)
880 let do_re_matches label guard
res quantified minus_quantified
=
881 let make_guard_match x
=
882 let stmt_fvs = Ast.get_mfvs x
in
883 let fvs = get_unquantified minus_quantified
stmt_fvs in
884 non_saved_quantify fvs (make_match None
true x
) in
886 let stmt_fvs = Ast.get_fvs x
in
887 let fvs = get_unquantified quantified
stmt_fvs in
888 quantify guard
fvs (make_match None guard x
) in
889 ctl_and CTL.NONSTRICT
(label_pred_maker label
)
890 (match List.map
Ast.unwrap
res with
891 [] -> failwith
"unexpected empty disj"
892 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
893 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
895 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
897 then failwith
"unexpected exp or ty";
898 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
900 (* code might be a DisjRuleElem, in which case we break it apart
901 code doesn't contain an Exp or Ty
902 this one is for use when it is not practical to push the quantifier inwards
904 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
905 match Ast.unwrap code
with
906 Ast.DisjRuleElem
(res) ->
907 let make_match = make_match None guard
in
908 let orop = if guard
then ctl_or else ctl_seqor in
909 ctl_and CTL.NONSTRICT
(label_pred_maker label
)
910 (List.fold_left
orop CTL.False
(List.map
make_match res))
911 | _
-> make_match label guard code
913 (* --------------------------------------------------------------------- *)
914 (* control structures *)
916 let end_control_structure fvs header body after_pred
917 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
918 (* aft indicates what is added after the whole if, which has to be added
920 let (aft_needed
,after_branch
) =
922 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
923 (false,make_seq_after2 guard after_pred after
)
926 make_match label guard
927 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
929 make_seq_after guard after_pred
930 (After
(make_seq_after guard
match_endif after
))) in
931 let body = body after_branch
in
932 let s = guard_to_strict guard
in
937 (match (after
,aft_needed
) with
938 (After _
,_
) (* pattern doesn't end here *)
939 | (_
,true) (* + code added after *) -> after_checks
940 | _
-> no_after_checks
)
941 (ctl_ax_absolute s body)))
943 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
944 quantified minus_quantified label llabel slabel recurse
make_match guard
=
945 (* "if (test) thn" becomes:
946 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
948 "if (test) thn; after" becomes:
949 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
954 match seq_fvs quantified
955 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
956 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
957 | _
-> failwith
"not possible" in
958 let new_quantified = Common.union_set bfvs quantified
in
960 match seq_fvs minus_quantified
961 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
962 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
963 | _
-> failwith
"not possible" in
964 let new_mquantified = Common.union_set mbfvs minus_quantified
in
966 let if_header = quantify guard efvs
(make_match ifheader
) in
967 (* then branch and after *)
968 let lv = get_label_ctr() in
969 let used = ref false in
971 (* no point to put a label on truepred etc; it is local to this construct
972 so it must have the same label *)
974 [truepred None
; recurse branch Tail
new_quantified new_mquantified
975 (Some
(lv,used)) llabel slabel guard
] in
976 let after_pred = aftpred None
in
977 let or_cases after_branch
=
978 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
979 let (if_header,wrapper
) =
982 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
983 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
984 (function body -> quantify true [lv] body))
985 else (if_header,function x
-> x
) in
987 (end_control_structure bfvs
if_header or_cases after_pred
988 (Some
(ctl_ex after_pred)) None aft after label guard
)
990 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
991 quantified minus_quantified label llabel slabel recurse
make_match guard
=
992 (* "if (test) thn else els" becomes:
993 if(test) & AX((TrueBranch & AX thn) v
994 (FalseBranch & AX (else & AX els)) v After)
997 "if (test) thn else els; after" becomes:
998 if(test) & AX((TrueBranch & AX thn) v
999 (FalseBranch & AX (else & AX els)) v
1000 (After & AXAX after))
1004 (* free variables *)
1005 let (e1fvs
,b1fvs
,s1fvs
) =
1006 match seq_fvs quantified
1007 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1008 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1009 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1010 | _
-> failwith
"not possible" in
1011 let (e2fvs
,b2fvs
,s2fvs
) =
1013 (* just combine with the else branch. no point to have separate
1014 quantifier, since there is only one possible control-flow path *)
1015 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1016 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1017 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1018 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1019 | _
-> failwith
"not possible" in
1020 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1021 let exponlyfvs = intersect e1fvs e2fvs
in
1022 let new_quantified = union bothfvs quantified
in
1023 (* minus free variables *)
1024 let (me1fvs
,mb1fvs
,ms1fvs
) =
1025 match seq_fvs minus_quantified
1026 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1027 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1028 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1029 | _
-> failwith
"not possible" in
1030 let (me2fvs
,mb2fvs
,ms2fvs
) =
1032 (* just combine with the else branch. no point to have separate
1033 quantifier, since there is only one possible control-flow path *)
1035 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1036 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1037 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1038 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1039 | _
-> failwith
"not possible" in
1040 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1041 let new_mquantified = union mbothfvs minus_quantified
in
1043 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1044 (* then and else branches *)
1045 let lv = get_label_ctr() in
1046 let used = ref false in
1049 [truepred None
; recurse branch1 Tail
new_quantified new_mquantified
1050 (Some
(lv,used)) llabel slabel guard
] in
1055 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1056 (header_match None guard els
);
1057 recurse branch2 Tail
new_quantified new_mquantified
1058 (Some
(lv,used)) llabel slabel guard
] in
1059 let after_pred = aftpred None
in
1060 let or_cases after_branch
=
1061 ctl_or true_branch (ctl_or false_branch after_branch
) in
1062 let s = guard_to_strict guard
in
1063 let (if_header,wrapper
) =
1066 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1067 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1068 (function body -> quantify true [lv] body))
1069 else (if_header,function x
-> x
) in
1071 (end_control_structure bothfvs if_header or_cases after_pred
1072 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1073 (Some
(ctl_ex (falsepred None
)))
1074 aft after label guard
)
1076 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1077 quantified minus_quantified label recurse
make_match guard
=
1079 (* the translation in this case is similar to that of an if with no else *)
1080 (* free variables *)
1082 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1083 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1084 | _
-> failwith
"not possible" in
1085 let new_quantified = Common.union_set bfvs quantified
in
1086 (* minus free variables *)
1088 match seq_fvs minus_quantified
1089 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1090 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1091 | _
-> failwith
"not possible" in
1092 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1094 let header = quantify guard efvs
(make_match header) in
1095 let lv = get_label_ctr() in
1096 let used = ref false in
1100 recurse
body Tail
new_quantified new_mquantified
1101 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1102 let after_pred = fallpred None
in
1103 let or_cases after_branch
= ctl_or body after_branch
in
1104 let (header,wrapper
) =
1107 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1108 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1109 (function body -> quantify true [lv] body))
1110 else (header,function x
-> x
) in
1112 (end_control_structure bfvs
header or_cases after_pred
1113 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1114 match (Ast.unwrap
body,aft
) with
1115 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1116 (match Ast.unwrap re
with
1117 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1118 Type_cocci.Unitary
,_
,false)
1119 when after
= Tail
or after
= End
or after
= VeryEnd
->
1121 match seq_fvs quantified
[Ast.get_fvs
header] with
1123 | _
-> failwith
"not possible" in
1124 quantify guard efvs
(make_match header)
1128 (* --------------------------------------------------------------------- *)
1129 (* statement metavariables *)
1131 (* issue: an S metavariable that is not an if branch/loop body
1132 should not match an if branch/loop body, so check that the labels
1133 of the nodes before the first node matched by the S are different
1134 from the label of the first node matched by the S *)
1135 let sequencibility body label_pred process_bef_aft
= function
1136 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1139 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1140 | Ast.SequencibleAfterDots
l ->
1141 (* S appears after some dots. l is the code that comes after the S.
1142 want to search for that first, because S can match anything, while
1143 the stuff after is probably more restricted *)
1144 let afts = List.map process_bef_aft
l in
1145 let ors = foldl1 ctl_or afts in
1146 ctl_and CTL.NONSTRICT
1147 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1150 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1151 | Ast.NotSequencible
-> body (function x
-> x
)
1153 let svar_context_with_add_after stmt
s label quantified
d ast
1154 seqible after process_bef_aft guard fvinfo
=
1155 let label_var = (*fresh_label_var*) string2var "_lab" in
1157 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1159 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1160 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1161 let full_metamatch = matcher d in
1162 let first_metamatch =
1165 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
)) ->
1166 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
))
1167 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1168 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1169 let middle_metamatch =
1172 Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1173 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1174 let last_metamatch =
1177 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
)) ->
1178 Ast.CONTEXT
(pos,Ast.AFTER
(aft
))
1179 | Ast.CONTEXT
(_
,_
) -> d
1180 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1183 ctl_and CTL.NONSTRICT
middle_metamatch prelabel_pred in
1184 let left_or = (* the whole statement is one node *)
1186 [full_metamatch; and_after guard
(ctl_not prelabel_pred) after
] in
1187 let right_or = (* the statement covers multiple nodes *)
1190 ctl_au CTL.NONSTRICT
1193 [ctl_and CTL.NONSTRICT
last_metamatch label_pred;
1195 (ctl_not prelabel_pred) after
])] in
1197 ctl_and CTL.NONSTRICT
label_pred
1198 (f
(ctl_and CTL.NONSTRICT
1199 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1200 let stmt_fvs = Ast.get_fvs stmt
in
1201 let fvs = get_unquantified quantified
stmt_fvs in
1202 quantify guard
(label_var::fvs)
1203 (sequencibility body label_pred process_bef_aft seqible
)
1205 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1206 seqible after process_bef_aft guard fvinfo
=
1207 let label_var = (*fresh_label_var*) string2var "_lab" in
1209 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1211 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1212 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1213 let stmt_fvs = Ast.get_fvs stmt
in
1214 let fvs = get_unquantified quantified
stmt_fvs in
1215 let (new_fvs
,body) =
1216 match (d,after
) with
1217 (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1218 (* just match the root. don't care about label; always ok *)
1219 (fvs,function f
-> f
(make_raw_match None
false ast
))
1220 | (Ast.MINUS
(pos,inst
,adj
,[]),(Tail
|End
|VeryEnd
)) ->
1221 (* don't have to put anything before the beginning, so don't have to
1222 distinguish the first node. so don't have to bother about paths,
1223 just use the label. label ensures that found nodes match up with
1224 what they should because it is in the lhs of the andany. *)
1226 CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1227 ctl_and CTL.NONSTRICT
label_pred
1228 (make_raw_match label
false ast
),
1229 ctl_and CTL.NONSTRICT
(matcher d) prelabel_pred) in
1231 function f
-> ctl_and CTL.NONSTRICT
label_pred (f
ender))
1233 (* more safe but less efficient *)
1234 let first_metamatch = matcher d in
1235 let rest_metamatch =
1238 Ast.MINUS
(pos,inst
,adj
,_
) -> Ast.MINUS
(pos,inst
,adj
,[])
1239 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1240 | Ast.PLUS
-> failwith
"not possible") in
1241 let rest_nodes = ctl_and CTL.NONSTRICT
rest_metamatch prelabel_pred in
1242 let last_node = and_after guard
(ctl_not prelabel_pred) after
in
1244 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1247 ctl_au CTL.NONSTRICT
rest_nodes last_node]) in
1249 function f
-> ctl_and CTL.NONSTRICT
label_pred (f
ender)) in
1250 quantify guard new_fvs
1251 (sequencibility body label_pred process_bef_aft seqible
)
1253 (* --------------------------------------------------------------------- *)
1254 (* dots and nests *)
1256 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1257 let matchgoto = gotopred None
in
1259 make_match None
false
1261 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1263 make_match None
false
1265 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1267 if quantifier
= Exists
1268 then Common.Left
(CTL.False
)
1270 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1272 then Common.Left
(aftpred label
)
1275 (function vx
-> function v ->
1276 (* vx is the contents of the nest, if any. we can only stop early
1277 if we find neither the ending code nor the nest contents in
1278 the if branch. not sure if this is a good idea. *)
1279 let lv = get_label_ctr() in
1280 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1281 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1282 ctl_or (aftpred label
)
1283 (quantify false [lv]
1284 (ctl_and CTL.NONSTRICT
1285 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1286 (ctl_au CTL.NONSTRICT
1287 (ctl_and CTL.NONSTRICT
(ctl_not v)
1288 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1289 (ctl_and CTL.NONSTRICT
preflabelpred
1290 (if !Flag_matcher.only_return_is_error_exit
1292 (ctl_and CTL.NONSTRICT
1293 (retpred None
) (ctl_not seq_after
))
1296 (ctl_and CTL.NONSTRICT
1297 (ctl_or (retpred None
) matchcontinue)
1298 (ctl_not seq_after
))
1299 (ctl_and CTL.NONSTRICT
1300 (ctl_or matchgoto matchbreak)
1301 (ctl_ag s (ctl_not seq_after
)))))))))) in
1302 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1303 let v = get_let_ctr() in
1305 (match stop_early with
1306 Common.Left x1
-> ctl_or y x1
1307 | Common.Right
stop_early ->
1310 (stop_early n
(CTL.Ref
v))))
1312 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1313 process_bef_aft statement_list statement guard quantified wrapcode
=
1314 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1315 (* proces bef_aft *)
1317 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1318 let bef_aft = (* to be negated *)
1322 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1325 with Not_found
-> shortest (Common.union_set bef aft
) in
1328 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1330 let check_quantifier quant other
=
1332 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1336 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1338 then failwith
"inconsistent annotation on dots"
1342 if check_quantifier Ast.WhenExists
Ast.WhenForall
1345 if check_quantifier Ast.WhenForall
Ast.WhenExists
1348 (* the following is used when we find a goto, etc and consider accepting
1349 without finding the rest of the pattern *)
1350 let aft = shortest aft in
1351 (* process whencode *)
1352 let labelled = label_pred_maker label
in
1354 let (poswhen
,negwhen
) =
1356 (function (poswhen
,negwhen
) ->
1358 Ast.WhenNot
whencodes ->
1359 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1360 | Ast.WhenAlways stm
->
1361 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1362 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1363 | Ast.WhenNotTrue
(e
) ->
1365 ctl_or (whencond_true e label guard quantified
) negwhen
)
1366 | Ast.WhenNotFalse
(e
) ->
1368 ctl_or (whencond_false e label guard quantified
) negwhen
))
1369 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1370 (*bef_aft modifies arg so that inside of a nest can't cause the next
1371 to overshoot its boundaries, eg a() <...f()...> b() where f is
1372 a metavariable and the whole thing matches code in a loop;
1373 don't want f to match eg b(), allowing to go around the loop again*)
1374 let poswhen = ctl_and_ns arg
poswhen in
1378 (* add in After, because it's not part of the program *)
1379 ctl_or (aftpred label
) negwhen
1381 ctl_and_ns poswhen (ctl_not negwhen) in
1382 (* process dot code, if any *)
1384 match (dotcode,guard
) with
1385 (None
,_) | (_,true) -> CTL.True
1386 | (Some
dotcode,_) -> dotcode in
1387 (* process nest code, if any *)
1388 (* whencode goes in the negated part of the nest; if no nest, just goes
1389 on the "true" in between code *)
1390 let plus_var = if plus
then get_label_ctr() else string2var "" in
1391 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1392 let (ornest
,just_nest
) =
1393 (* just_nest is used when considering whether to stop early, to continue
1394 to collect nest information in the if branch *)
1395 match (nest
,guard
&& not plus
) with
1396 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1397 | (Some nest
,false) ->
1398 let v = get_let_ctr() in
1402 (* the idea is that BindGood is sort of a witness; a witness to
1403 having found the subterm in at least one place. If there is
1404 not a witness, then there is a risk that it will get thrown
1405 away, if it is merged with a node that has an empty
1406 environment. See tests/nestplus. But this all seems
1407 rather suspicious *)
1408 CTL.And
(CTL.NONSTRICT
,x
,
1409 CTL.Exists
(true,plus_var2,
1410 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1411 CTL.Modif
plus_var2)))
1415 CTL.Or
(is_plus (CTL.Ref
v),
1416 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1418 let plus_modifier x
=
1425 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1431 | Guard f
-> ctl_uncheck f
1433 let exit = endpred label
in
1434 let errorexit = exitpred label
in
1435 ctl_or exit errorexit
1436 (* not at all sure what the next two mean... *)
1440 Some
(lv,used) -> used := true;
1441 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1442 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1443 | None
-> endpred label
)
1444 (* was the following, but not clear why sgrep should allow
1446 let exit = endpred label in
1447 let errorexit = exitpred label in
1449 then ctl_or exit errorexit (* end anywhere *)
1450 else exit (* end at the real end of the function *) *)
in
1452 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1453 label
(guard_to_strict guard
) wrapcode just_nest
1455 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1456 aft ender quantifier)
1458 and get_whencond_exps e
=
1459 match Ast.unwrap e
with
1461 | Ast.DisjRuleElem
(res) ->
1462 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1463 | _ -> failwith
"not possible"
1465 and make_whencond_headers e e1 label guard quantified
=
1466 let fvs = Ast.get_fvs e
in
1468 quantify guard
(get_unquantified quantified
fvs)
1469 (make_match label guard h
) in
1474 (Ast.make_mcode
"if",
1475 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1476 let while_header e1
=
1480 (Ast.make_mcode
"while",
1481 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1486 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1487 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1489 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1491 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1493 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1494 (if_headers, while_headers, for_headers)
1496 and whencond_true e label guard quantified
=
1497 let e1 = get_whencond_exps e
in
1498 let (if_headers, while_headers, for_headers) =
1499 make_whencond_headers e
e1 label guard quantified
in
1501 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1502 (ctl_and CTL.NONSTRICT
1503 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1505 and whencond_false e label guard quantified
=
1506 let e1 = get_whencond_exps e
in
1507 let (if_headers, while_headers, for_headers) =
1508 make_whencond_headers e
e1 label guard quantified
in
1509 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1510 (ctl_and CTL.NONSTRICT
(fallpred label
)
1511 (ctl_or (ctl_back_ex if_headers)
1512 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1514 (* --------------------------------------------------------------------- *)
1515 (* the main translation loop *)
1517 let rec statement_list stmt_list after quantified minus_quantified
1518 label llabel slabel dots_before guard
=
1520 (* include Disj to be on the safe side *)
1521 match Ast.unwrap x
with
1522 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1523 let compute_label l e db
= if db
or isdots e
then l else None
in
1524 match Ast.unwrap stmt_list
with
1526 let rec loop quantified minus_quantified dots_before label llabel slabel
1528 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1530 statement e after quantified minus_quantified
1531 (compute_label label e dots_before
)
1533 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1534 let shared = intersectll fv
fvs in
1535 let unqshared = get_unquantified quantified
shared in
1536 let new_quantified = Common.union_set
unqshared quantified
in
1537 let minus_shared = intersectll mfv mfvs
in
1539 get_unquantified minus_quantified
minus_shared in
1540 let new_mquantified =
1541 Common.union_set
munqshared minus_quantified
in
1542 quantify guard
unqshared
1545 (let (label1
,llabel1
,slabel1
) =
1546 match Ast.unwrap e
with
1548 (match Ast.unwrap re
with
1549 Ast.Goto
_ -> (None
,None
,None
)
1550 | _ -> (label
,llabel
,slabel
))
1551 | _ -> (label
,llabel
,slabel
) in
1552 loop new_quantified new_mquantified (isdots e
)
1553 label1 llabel1 slabel1
1555 new_quantified new_mquantified
1556 (compute_label label e dots_before
) llabel slabel guard
)
1557 | _ -> failwith
"not possible" in
1558 loop quantified minus_quantified dots_before
1560 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1561 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1562 | Ast.STARS
(x
) -> failwith
"not supported"
1564 (* llabel is the label of the enclosing loop and slabel is the label of the
1566 and statement stmt after quantified minus_quantified
1567 label llabel slabel guard
=
1568 let ctl_au = ctl_au CTL.NONSTRICT
in
1569 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1570 let ctl_and = ctl_and CTL.NONSTRICT
in
1571 let make_seq = make_seq guard
in
1572 let make_seq_after = make_seq_after guard
in
1573 let real_make_match = make_match in
1574 let make_match = header_match label guard
in
1576 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1579 match Ast.unwrap stmt
with
1581 (match Ast.unwrap ast
with
1582 (* the following optimisation is not a good idea, because when S
1583 is alone, we would like it not to match a declaration.
1584 this makes more matching for things like when (...) S, but perhaps
1585 that matching is not so costly anyway *)
1586 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1587 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_)) as d),_),
1589 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_)) as d),_),
1591 svar_context_with_add_after stmt
s label quantified
d ast seqible
1593 (process_bef_aft quantified minus_quantified
1594 label llabel slabel
true)
1596 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1598 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1599 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1601 (process_bef_aft quantified minus_quantified
1602 label llabel slabel
true)
1604 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1608 match Ast.unwrap ast
with
1609 Ast.DisjRuleElem
(res) ->
1610 do_re_matches label guard
res quantified minus_quantified
1611 | Ast.Exp
(_) | Ast.Ty
(_) ->
1612 let stmt_fvs = Ast.get_fvs stmt
in
1613 let fvs = get_unquantified quantified
stmt_fvs in
1614 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1616 let stmt_fvs = Ast.get_fvs stmt
in
1617 let fvs = get_unquantified quantified
stmt_fvs in
1618 quantify guard
fvs (make_match ast
) in
1619 match Ast.unwrap ast
with
1620 Ast.Break
(brk
,semi
) ->
1621 (match (llabel
,slabel
) with
1622 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1623 ctl_and term (bclabel_pred_maker slabel
)
1624 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1625 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1626 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1627 (* discard pattern that comes after return *)
1628 let normal_res = make_seq_after term after
in
1629 (* the following code tries to propagate the modifications on
1630 return; to a close brace, in the case where the final return
1633 match (retmc
,semmc
) with
1634 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1635 when !Flag.sgrep_mode2
->
1636 (* in sgrep mode, we can propagate the - *)
1637 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,l1
@l2
))
1638 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
))
1639 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
)),
1640 Ast.CONTEXT
(_,Ast.AFTER
(l2
))) ->
1641 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
)))
1642 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1643 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1645 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1646 Ast.CONTEXT
(_,Ast.AFTER
(l))) ->
1647 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l)))
1649 let ret = Ast.make_mcode
"return" in
1651 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1652 let semi = Ast.make_mcode
";" in
1654 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1656 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1659 let exit = endpred None
in
1661 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1662 let stripped_rbrace =
1663 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1665 (ctl_and (make_match mod_rbrace)
1670 (ctl_or simple_return return_expr))))
1672 (make_match stripped_rbrace)
1673 (* error exit not possible; it is in the middle
1674 of code, so a return is needed *)
1677 (* some change in the middle of the return, so have to
1678 find an actual return *)
1681 (* should try to deal with the dots_bef_aft problem elsewhere,
1682 but don't have the courage... *)
1687 do_between_dots stmt
term End
1688 quantified minus_quantified label llabel slabel guard
in
1690 make_seq_after term after
)
1691 | Ast.Seq
(lbrace
,body,rbrace
) ->
1692 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1695 [Ast.get_fvs lbrace
;
1696 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1698 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1699 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1700 | _ -> failwith
"not possible" in
1701 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1703 seq_fvs minus_quantified
1704 [Ast.get_mfvs lbrace
;
1705 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1707 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1708 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1709 | _ -> failwith
"not possible" in
1710 let pv = count_nested_braces stmt
in
1711 let lv = get_label_ctr() in
1712 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1713 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1716 (quantify guard lbfvs
(make_match lbrace
))
1717 (ctl_and paren_pred label_pred) in
1719 match Ast.unwrap rbrace
with
1720 Ast.SeqEnd
((data
,info,_,pos)) ->
1721 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1722 | _ -> failwith
"unexpected close brace" in
1724 (* label is not needed; paren_pred is enough *)
1725 quantify guard rbfvs
1726 (ctl_au (make_match empty_rbrace)
1728 (real_make_match None guard rbrace
)
1730 let new_quantified2 =
1731 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1732 let new_mquantified2 =
1733 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1734 let pattern_as_given =
1735 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1736 quantify true [pv;lv]
1737 (quantify guard b1fvs
1740 quantify guard b2fvs
1741 (statement_list body
1742 (After
(make_seq_after end_brace after
))
1743 new_quantified2 new_mquantified2
1744 (Some
(lv,ref true)) llabel slabel
false guard
)])) in
1745 if ends_in_return body
1747 (* matching error handling code *)
1749 1. The pattern as given
1750 2. A goto, and then some close braces, and then the pattern as
1751 given, but without the braces (only possible if there are no
1752 decls, and open and close braces are unmodified)
1753 3. Part of the pattern as given, then a goto, and then the rest
1754 of the pattern. For this case, we just check that all paths have
1755 a goto within the current braces. checking for a goto at every
1756 point in the pattern seems expensive and not worthwhile. *)
1758 let body = preprocess_dots body in (* redo, to drop braces *)
1762 (make_match empty_rbrace)
1763 (ctl_ax (* skip the destination label *)
1764 (quantify guard b2fvs
1765 (statement_list body End
1766 new_quantified2 new_mquantified2 None llabel slabel
1769 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1770 quantify true [pv;lv]
1771 (quantify guard b1fvs
1775 (CTL.AU
(* want AF even for sgrep *)
1776 (CTL.FORWARD
,CTL.STRICT
,
1777 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1778 ctl_and (* brace must be eventually after goto *)
1779 (gotopred (Some
(lv,ref true)))
1780 (* want AF even for sgrep *)
1781 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1782 (quantify guard b2fvs
1783 (statement_list body Tail
1784 new_quantified2 new_mquantified2
1785 None
(*no label because past the goto*)
1786 llabel slabel
false guard
))])) in
1787 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1788 else pattern_as_given
1789 | Ast.IfThen
(ifheader
,branch
,aft) ->
1790 ifthen ifheader branch
aft after quantified minus_quantified
1791 label llabel slabel statement
make_match guard
1793 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1794 ifthenelse ifheader branch1 els branch2
aft after quantified
1795 minus_quantified label llabel slabel statement
make_match guard
1797 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1798 | Ast.Iterator
(header,body,aft) ->
1799 forwhile header body aft after quantified minus_quantified
1800 label statement
make_match guard
1802 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1803 (*ctl_and seems pointless, disjuncts see label too
1804 (label_pred_maker label)*)
1805 (List.fold_left
ctl_seqor CTL.False
1808 statement_list sl after quantified minus_quantified label
1809 llabel slabel
true guard
)
1812 | Ast.Nest
(stmt_dots
,whencode
,multi
,bef
,aft) ->
1813 (* label in recursive call is None because label check is already
1814 wrapped around the corresponding code *)
1817 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1819 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1820 | _ -> failwith
"not possible" in
1822 (* no minus version because when code doesn't contain any minus code *)
1823 let new_quantified = Common.union_set
bfvs quantified
in
1827 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1828 None llabel slabel
true guard
in
1829 dots_and_nests multi
1830 (Some
dots_pattern) whencode bef
aft None after label
1831 (process_bef_aft
new_quantified minus_quantified
1832 None llabel slabel
true)
1834 statement_list x Tail
new_quantified minus_quantified None
1835 llabel slabel
true true)
1837 statement x Tail
new_quantified minus_quantified None
1840 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1842 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1845 Ast.MINUS
(_,_,_,_) ->
1846 (* no need for the fresh metavar, but ... is a bit weird as a
1848 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1850 dots_and_nests false None
whencodes bef
aft dot_code after label
1851 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1853 statement_list x Tail quantified minus_quantified
1854 None llabel slabel
true true)
1856 statement x Tail quantified minus_quantified None llabel slabel
true)
1858 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1860 | Ast.Switch
(header,lb
,cases,rb
) ->
1861 let rec intersect_all = function
1864 | x
::xs -> intersect x
(intersect_all xs) in
1865 let rec union_all l = List.fold_left
union [] l in
1866 (* start normal variables *)
1867 let header_fvs = Ast.get_fvs
header in
1868 let lb_fvs = Ast.get_fvs lb
in
1869 let case_fvs = List.map
Ast.get_fvs
cases in
1870 let rb_fvs = Ast.get_fvs rb
in
1871 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1872 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1874 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1875 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1876 function case_fvs ->
1877 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] 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_fvs in
1884 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1885 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1886 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
1887 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
1888 List.rev all_rbfvs
) in
1889 let exponlyfvs = intersect_all all_efvs
in
1890 let lbonlyfvs = intersect_all all_lbfvs
in
1891 (* don't do anything with right brace. Hope there is no + code on it *)
1892 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1893 let b1fvs = union_all all_b1fvs
in
1894 let new1_quantified = union b1fvs quantified
in
1895 let b2fvs = union (union_all all_b1fvs
) (intersect_all all_casefvs
) in
1896 let new2_quantified = union b2fvs new1_quantified in
1897 (* let b3fvs = union_all all_b3fvs in*)
1898 (* ------------------- start minus free variables *)
1899 let header_mfvs = Ast.get_mfvs
header in
1900 let lb_mfvs = Ast.get_mfvs lb
in
1901 let case_mfvs = List.map
Ast.get_mfvs
cases in
1902 let rb_mfvs = Ast.get_mfvs rb
in
1903 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1904 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1906 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1907 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1908 function case_mfvs ->
1911 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1912 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
1913 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
1914 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
1916 | _ -> failwith
"not possible")
1917 ([],[],[],[],[],[],[]) case_mfvs in
1918 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1919 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1920 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
1921 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
1922 List.rev all_mrbfvs
) in
1923 (* don't do anything with right brace. Hope there is no + code on it *)
1924 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1925 let mb1fvs = union_all all_mb1fvs
in
1926 let new1_mquantified = union mb1fvs quantified
in
1927 let mb2fvs = union (union_all all_mb1fvs
) (intersect_all all_mcasefvs
) in
1928 let new2_mquantified = union mb2fvs new1_mquantified in
1929 (* let b3fvs = union_all all_b3fvs in*)
1930 (* ------------------- end collection of free variables *)
1931 let switch_header = quantify guard
exponlyfvs (make_match header) in
1932 let lb = quantify guard
lbonlyfvs (make_match lb) in
1933 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
1936 (function case_line
->
1937 match Ast.unwrap case_line
with
1938 Ast.CaseLine
(header,body) ->
1940 match seq_fvs new2_quantified [Ast.get_fvs
header] with
1941 [(e1fvs,_)] -> e1fvs
1942 | _ -> failwith
"not possible" in
1943 quantify guard
e1fvs (real_make_match label
true header)
1944 | Ast.OptCase
(case_line
) -> failwith
"not supported")
1947 ctl_not (List.fold_left
ctl_or_fl CTL.False
case_headers) in
1948 let lv = get_label_ctr() in
1949 let used = ref false in
1952 (function case_line
->
1953 match Ast.unwrap case_line
with
1954 Ast.CaseLine
(header,body) ->
1955 let (e1fvs,b1fvs,s1fvs
) =
1956 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
1957 match seq_fvs new2_quantified fvs with
1958 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
1959 | _ -> failwith
"not possible" in
1960 let (me1fvs
,mb1fvs,ms1fvs
) =
1961 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
1962 match seq_fvs new2_mquantified fvs with
1963 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
1964 | _ -> failwith
"not possible" in
1966 quantify guard
e1fvs (make_match header) in
1967 let new3_quantified = union b1fvs new2_quantified in
1968 let new3_mquantified = union mb1fvs new2_mquantified in
1970 statement_list body Tail
1971 new3_quantified new3_mquantified label llabel
1972 (Some
(lv,used)) true(*?*) guard
in
1973 quantify guard
b1fvs (make_seq [case_header; body])
1974 | Ast.OptCase
(case_line
) -> failwith
"not supported")
1976 let default_required =
1979 match Ast.unwrap case
with
1980 Ast.CaseLine
(header,_) ->
1981 (match Ast.unwrap
header with
1982 Ast.Default
(_,_) -> true
1986 then function x
-> x
1987 else function x
-> ctl_or (fallpred label
) x
in
1988 let after_pred = aftpred label
in
1989 let body after_branch
=
1992 (quantify guard
b2fvs
1995 (List.fold_left
ctl_and CTL.True
1996 (List.map
ctl_ex case_headers));
1997 List.fold_left
ctl_or_fl no_header case_code])))
2000 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2001 match Ast.unwrap
rb with
2002 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2003 | _ -> failwith
"not possible") in
2004 let (switch_header,wrapper
) =
2007 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2008 (ctl_and switch_header label_pred,
2009 (function body -> quantify true [lv] body))
2010 else (switch_header,function x
-> x
) in
2012 (end_control_structure b1fvs switch_header body
2013 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2014 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2015 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2018 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2019 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2021 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2022 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2023 | _ -> failwith
"not possible" in
2024 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2027 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2028 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2030 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2031 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2032 | _ -> failwith
"not possible" in
2033 let function_header = quantify guard hfvs
(make_match header) in
2034 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2035 let stripped_rbrace =
2036 match Ast.unwrap rbrace
with
2037 Ast.SeqEnd
((data
,info,_,_)) ->
2038 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2039 | _ -> failwith
"unexpected close brace" in
2041 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2042 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2043 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2045 (quantify guard rbfvs
(make_match rbrace
))
2047 (* the following finds the beginning of the fake braces,
2048 if there are any, not completely sure how this works.
2049 sse the examples sw and return *)
2050 (ctl_back_ex (ctl_not fake_brace))
2051 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2052 let new_quantified3 =
2053 Common.union_set
b1fvs
2054 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2055 let new_mquantified3 =
2056 Common.union_set
mb1fvs
2057 (Common.union_set
mb2fvs
2058 (Common.union_set mb3fvs minus_quantified
)) in
2060 match (Ast.undots
body,
2061 contains_modif rbrace
or contains_pos rbrace
) with
2063 (match Ast.unwrap
body with
2064 Ast.Nest
(stmt_dots
,[],false,_,_) ->
2065 (* special case for function header + body - header is unambiguous
2066 and unique, so we can just look for the nested body anywhere
2070 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2071 statement_list stmt_dots
2072 (* discards match on right brace, but don't need it *)
2073 (Guard
(make_seq_after end_brace after
))
2074 new_quantified3 new_mquantified3
2075 None llabel slabel
true guard
))
2076 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2078 (* flow sensitive, so not optimizable *)
2079 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2081 | _ -> true) whencode
) ->
2082 (* try to be more efficient for the case where the body is just
2083 ... Perhaps this is too much of a special case, but useful
2084 for dropping a parameter and checking that it is never used. *)
2086 Ast.MINUS
(_,_,_,_) -> None
2100 Ast.WhenAlways
(s) -> prev
2101 | Ast.WhenNot
(sl
) ->
2103 statement_list sl Tail
2109 | Ast.WhenNotTrue
(_)
2110 | Ast.WhenNotFalse
(_) ->
2111 failwith
"unexpected"
2113 (Ast.WhenAny
) -> CTL.False
2114 | Ast.WhenModifier
(_) -> prev
)
2115 CTL.False whencode
))
2119 Ast.WhenAlways
(s) ->
2124 label llabel slabel
true in
2126 | Ast.WhenNot
(sl
) -> prev
2127 | Ast.WhenNotTrue
(_)
2128 | Ast.WhenNotFalse
(_) ->
2129 failwith
"unexpected"
2130 | Ast.WhenModifier
(Ast.WhenAny
) ->
2132 | Ast.WhenModifier
(_) -> prev
)
2133 CTL.True whencode
) in
2134 ctl_au leftarg (make_match stripped_rbrace)]))
2138 (* function body is all minus, no whencode *)
2139 match Ast.undots
body with
2141 (match Ast.unwrap
body with
2143 ((_,i
,(Ast.MINUS
(_,_,_,[]) as d),_),[],_,_) ->
2144 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2145 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,[]),_)),
2146 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,[]),_)))
2147 when not
(contains_pos rbrace
) ->
2149 (* andany drops everything to the end, including close
2150 braces - not just function body, could check
2151 label to keep braces *)
2152 (ctl_and start_brace
2155 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2157 (make_meta_rule_elem d ([],[],[]))))))
2162 match (optim1,optim2) with
2168 quantify guard
b3fvs
2169 (statement_list body
2170 (After
(make_seq_after end_brace after
))
2171 new_quantified3 new_mquantified3 None llabel slabel
2173 quantify guard
b1fvs
2174 (make_seq [function_header; quantify guard
b2fvs body_code])
2175 | Ast.Define
(header,body) ->
2176 let (hfvs
,bfvs,bodyfvs
) =
2177 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2179 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2180 | _ -> failwith
"not possible" in
2181 let (mhfvs
,mbfvs
,mbodyfvs
) =
2182 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2184 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2185 | _ -> failwith
"not possible" in
2186 let define_header = quantify guard hfvs
(make_match header) in
2188 statement_list body after
2189 (Common.union_set
bfvs quantified
)
2190 (Common.union_set mbfvs minus_quantified
)
2191 None llabel slabel
true guard
in
2192 quantify guard
bfvs (make_seq [define_header; body_code])
2193 | Ast.OptStm
(stm
) ->
2194 failwith
"OptStm should have been compiled away\n"
2195 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2196 | _ -> failwith
"not supported" in
2197 if guard
or !dots_done
2200 do_between_dots stmt
term after quantified minus_quantified
2201 label llabel slabel guard
2203 (* term is the translation of stmt *)
2204 and do_between_dots stmt
term after quantified minus_quantified
2205 label llabel slabel guard
=
2206 match Ast.get_dots_bef_aft stmt
with
2207 Ast.AddingBetweenDots
(brace_term
,n
)
2208 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2210 statement brace_term after quantified minus_quantified
2211 label llabel slabel guard
in
2212 let v = Printf.sprintf
"_r_%d" n
in
2213 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2214 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2217 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2218 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2220 | Ast.NoDots
-> term
2222 (* un_process_bef_aft is because we don't want to do transformation in this
2223 code, and thus don't case about braces before or after it *)
2224 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2226 Ast.WParen
(re
,n
) ->
2227 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2228 let s = guard_to_strict guard
in
2229 quantify true (get_unquantified quantified
[n
])
2230 (ctl_and s (make_raw_match None guard re
) paren_pred)
2232 statement
s Tail quantified minus_quantified label llabel slabel guard
2233 | Ast.Other_dots
d ->
2234 statement_list d Tail quantified minus_quantified
2235 label llabel slabel
true guard
2237 (* --------------------------------------------------------------------- *)
2238 (* cleanup: convert AX to EX for pdots.
2239 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2240 This is what we wanted in the first place, but it wasn't possible to make
2241 because the AX and its argument are not created in the same place.
2243 (* also cleanup XX, which is a marker for the case where the programmer
2244 specifies to change the quantifier on .... Assumed to only occur after one AX
2245 or EX, or at top level. *)
2248 let c = match c with CTL.XX
(c) -> c | _ -> c in
2250 CTL.False
-> CTL.False
2251 | CTL.True
-> CTL.True
2252 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2253 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2254 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2255 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2256 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2257 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2258 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2259 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2260 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2261 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2262 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2263 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2264 | CTL.AX
(CTL.FORWARD
,s,
2266 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2267 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2269 CTL.And
(CTL.NONSTRICT
,
2270 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2271 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2272 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2273 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2274 CTL.AX
(dir
,s,cleanup phi
)
2275 | CTL.XX
(phi
) -> failwith
"bad XX"
2276 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2277 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2278 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2279 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2280 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2281 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2282 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2283 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2284 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2285 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2286 | CTL.Ref
(s) -> CTL.Ref
(s)
2287 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2288 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2290 (* --------------------------------------------------------------------- *)
2291 (* Function declaration *)
2293 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2295 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2296 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2298 saved := Ast.get_saved t
;
2299 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2300 quantify false quantified
2301 (match Ast.unwrap t
with
2302 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2304 let unopt = elim_opt.V.rebuilder_statement stmt
in
2305 let unopt = preprocess_dots_e unopt in
2306 cleanup(statement
unopt VeryEnd
quantified [] None None None
false)
2307 | Ast.CODE
(stmt_dots
) ->
2308 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2309 let unopt = preprocess_dots unopt in
2310 let starts_with_dots =
2311 match Ast.undots stmt_dots
with
2313 (match Ast.unwrap
d with
2314 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2315 | Ast.Stars
(_,_,_,_) -> true
2318 let starts_with_brace =
2319 match Ast.undots stmt_dots
with
2321 (match Ast.unwrap
d with
2326 statement_list unopt VeryEnd
quantified [] None None None
2329 (if starts_with_dots
2331 (* EX because there is a loop on enter/top *)
2332 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2333 else if starts_with_brace
2335 ctl_and CTL.NONSTRICT
2336 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2338 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords")
2340 (* --------------------------------------------------------------------- *)
2343 let asttoctlz (name
,(_,_,exists_flag
),l)
2344 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2347 (match exists_flag
with
2348 Ast.Exists
-> exists := Exists
2349 | Ast.Forall
-> exists := Forall
2350 | Ast.Undetermined
->
2351 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2353 let (l,used_after) =
2357 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2358 (List.combine
l (List.combine
used_after positions
))) in
2360 List.map2
(top_level name
)
2361 (List.combine
used_after fresh_used_after
)
2362 (List.combine fresh_used_after_seeds
l) in
2366 let asttoctl r
used_after positions
=
2368 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2369 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2370 asttoctlz (a,b
,c) used_after positions
2371 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CTL.True
]
2373 let pp_cocci_predicate (pred
,modif
) =
2374 Pretty_print_engine.pp_predicate pred
2376 let cocci_predicate_to_string (pred
,modif
) =
2377 Pretty_print_engine.predicate_to_string pred