1 (* for MINUS and CONTEXT, pos is always None in this file *)
3 (* true = don't see all matched nodes, only modified ones *)
4 let onlyModif = ref true(*false*)
6 type ex
= Exists
| Forall
7 let exists = ref Forall
10 module V
= Visitor_ast
13 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
15 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
17 (cocci_predicate
,Ast.meta_name
, Wrapper_ctl.info
) Ast_ctl.generic_ctl
19 let union = Common.union_set
20 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
21 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
23 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
25 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
27 let used_after = ref ([] : Ast.meta_name list
)
28 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
30 let saved = ref ([] : Ast.meta_name list
)
32 let string2var x
= ("",x
)
34 (* --------------------------------------------------------------------- *)
35 (* predicates matching various nodes in the graph *)
39 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
40 | (CTL.True
,a
) | (a
,CTL.True
) -> a
45 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
46 | (CTL.False
,a
) | (a
,CTL.False
) -> a
51 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
52 | (CTL.False
,a
) | (a
,CTL.False
) -> a
57 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
58 | (CTL.False
,a
) | (a
,CTL.False
) -> a
61 let ctl_not = function
63 | CTL.False
-> CTL.True
66 let ctl_ax s
= function
68 | CTL.False
-> CTL.False
71 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
72 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
74 let ctl_ax_absolute s
= function
76 | CTL.False
-> CTL.False
77 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
81 | CTL.False
-> CTL.False
82 | x
-> CTL.EX
(CTL.FORWARD
,x
)
84 (* This stays being AX even for sgrep_mode, because it is used to identify
85 the structure of the term, not matching the pattern. *)
86 let ctl_back_ax = function
88 | CTL.False
-> CTL.False
89 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
91 let ctl_back_ex = function
93 | CTL.False
-> CTL.False
94 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
98 | CTL.False
-> CTL.False
99 | x
-> CTL.EF
(CTL.FORWARD
,x
)
101 let ctl_ag s
= function
103 | CTL.False
-> CTL.False
104 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
107 match (x
,!exists) with
108 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
109 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
110 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
111 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
113 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
115 (match (x
,!exists) with
116 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
117 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
118 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
119 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
121 let ctl_uncheck = function
123 | CTL.False
-> CTL.False
126 let label_pred_maker = function
128 | Some
(label_var
,used
) ->
130 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
132 let bclabel_pred_maker = function
134 | Some
(label_var
,used
) ->
136 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
138 (* label used to be used here, but it is not used; label is only needed after
140 let predmaker guard pred label
= CTL.Pred pred
142 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
143 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
144 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
145 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
146 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
147 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
148 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
149 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
150 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
151 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
152 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
153 let loopfallpred = predmaker false (Lib_engine.LoopFallThrough
, CTL.Control
)
155 (*let aftret label_var =
156 ctl_or (aftpred label_var)
157 (ctl_or (loopfallpred label_var) (exitpred label_var))*)
163 Printf.sprintf
"r%d" cur
165 (* --------------------------------------------------------------------- *)
166 (* --------------------------------------------------------------------- *)
167 (* Eliminate OptStm *)
169 (* for optional thing with nothing after, should check that the optional thing
170 never occurs. otherwise the matching stops before it occurs *)
173 let donothing r k e
= k e
in
176 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
179 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
182 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
184 let inheritedlist l
=
185 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
188 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
191 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
193 let rec dots_list unwrapped wrapped
=
194 match (unwrapped
,wrapped
) with
197 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
199 | (Ast.Nest
(_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
200 d0
::s
::d1
::rest
) -> (* why no case for nest as u? *)
201 let l = Ast.get_line stm
in
202 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
203 let new_rest2 = dots_list urest rest
in
204 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
205 varlists new_rest1 in
206 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
207 varlists new_rest2 in
211 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
213 Ast.free_vars
= fv_rest1
;
214 Ast.minus_free_vars
= mfv_rest1
;
215 Ast.fresh_vars
= fresh_rest1
;
216 Ast.inherited
= inherited_rest1
;
217 Ast.saved_witness
= s1
};
218 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
220 Ast.free_vars
= fv_rest2
;
221 Ast.minus_free_vars
= mfv_rest2
;
222 Ast.fresh_vars
= fresh_rest2
;
223 Ast.inherited
= inherited_rest2
;
224 Ast.saved_witness
= s2
}])) with
226 Ast.free_vars
= fv_rest1
;
227 Ast.minus_free_vars
= mfv_rest1
;
228 Ast.fresh_vars
= fresh_rest1
;
229 Ast.inherited
= inherited_rest1
;
230 Ast.saved_witness
= s1
}]
232 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
233 let l = Ast.get_line stm
in
234 let new_rest1 = dots_list urest rest
in
235 let new_rest2 = stm
::new_rest1 in
236 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
237 varlists new_rest1 in
238 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
239 varlists new_rest2 in
242 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
244 Ast.free_vars
= fv_rest2
;
245 Ast.minus_free_vars
= mfv_rest2
;
246 Ast.fresh_vars
= fresh_rest2
;
247 Ast.inherited
= inherited_rest2
;
248 Ast.saved_witness
= s2
};
249 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
251 Ast.free_vars
= fv_rest1
;
252 Ast.minus_free_vars
= mfv_rest1
;
253 Ast.fresh_vars
= fresh_rest1
;
254 Ast.inherited
= inherited_rest1
;
255 Ast.saved_witness
= s1
}])) with
257 Ast.free_vars
= fv_rest2
;
258 Ast.minus_free_vars
= mfv_rest2
;
259 Ast.fresh_vars
= fresh_rest2
;
260 Ast.inherited
= inherited_rest2
;
261 Ast.saved_witness
= s2
}]
263 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
264 let l = Ast.get_line stm
in
265 let fv_stm = Ast.get_fvs stm
in
266 let mfv_stm = Ast.get_mfvs stm
in
267 let fresh_stm = Ast.get_fresh stm
in
268 let inh_stm = Ast.get_inherited stm
in
269 let saved_stm = Ast.get_saved stm
in
270 let fv_d1 = Ast.get_fvs d1
in
271 let mfv_d1 = Ast.get_mfvs d1
in
272 let fresh_d1 = Ast.get_fresh d1
in
273 let inh_d1 = Ast.get_inherited d1
in
274 let saved_d1 = Ast.get_saved d1
in
275 let fv_both = Common.union_set
fv_stm fv_d1 in
276 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
277 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
278 let inh_both = Common.union_set
inh_stm inh_d1 in
279 let saved_both = Common.union_set
saved_stm saved_d1 in
283 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
285 Ast.free_vars
= fv_stm;
286 Ast.minus_free_vars
= mfv_stm;
287 Ast.fresh_vars
= fresh_stm;
288 Ast.inherited
= inh_stm;
289 Ast.saved_witness
= saved_stm};
290 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
292 Ast.free_vars
= fv_d1;
293 Ast.minus_free_vars
= mfv_d1;
294 Ast.fresh_vars
= fresh_d1;
295 Ast.inherited
= inh_d1;
296 Ast.saved_witness
= saved_d1}])) with
298 Ast.free_vars
= fv_both;
299 Ast.minus_free_vars
= mfv_both;
300 Ast.fresh_vars
= fresh_both;
301 Ast.inherited
= inh_both;
302 Ast.saved_witness
= saved_both}]
304 | ([Ast.Nest
(_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
305 let l = Ast.get_line stm
in
306 let rw = Ast.rewrap stm
in
307 let rwd = Ast.rewrap stm
in
308 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
310 [rwd(Ast.DOTS
([stm
]));
311 {(Ast.make_term
(Ast.DOTS
([rw dots])))
312 with Ast.node_line
= l}])]
314 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
315 | _
-> failwith
"not possible" in
317 let stmtdotsfn r k d
=
320 (match Ast.unwrap
d with
321 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
322 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
323 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
326 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
327 donothing donothing stmtdotsfn donothing
328 donothing donothing donothing donothing donothing donothing donothing
329 donothing donothing donothing donothing donothing
331 (* --------------------------------------------------------------------- *)
332 (* after management *)
333 (* We need Guard for the following case:
342 Here the inner <... b ...> should not go past foo. But foo is not the
343 "after" of the body of the outer nest, because we don't want to search for
344 it in the case where the body of the outer nest ends in something other
345 than dots or a nest. *)
347 (* what is the difference between tail and end??? *)
349 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
351 let a2n = function After x
-> Guard x
| a
-> a
354 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
355 let pp_meta (_
,x
) = Common.pp x
in
356 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
357 Format.print_newline
()
359 let print_after = function
360 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
361 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
362 | Tail
-> Printf.printf
"Tail\n"
363 | VeryEnd
-> Printf.printf
"Very End\n"
364 | End
-> Printf.printf
"End\n"
366 (* --------------------------------------------------------------------- *)
369 let fresh_var _
= string2var "_v"
370 let fresh_pos _
= string2var "_pos" (* must be a constant *)
372 let fresh_metavar _
= "_S"
374 (* fvinfo is going to end up being from the whole associated statement.
375 it would be better if it were just the free variables in d, but free_vars.ml
376 doesn't keep track of free variables on + code *)
377 let make_meta_rule_elem d fvinfo
=
378 let nm = fresh_metavar() in
379 Ast.make_meta_rule_elem nm d fvinfo
381 let get_unquantified quantified vars
=
382 List.filter
(function x
-> not
(List.mem x quantified
)) vars
384 let make_seq guard
l =
385 let s = guard_to_strict guard
in
386 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
388 let make_seq_after2 guard first rest
=
389 let s = guard_to_strict guard
in
391 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
394 let make_seq_after guard first rest
=
396 After rest
-> make_seq guard
[first
;rest
]
399 let opt_and guard first rest
=
400 let s = guard_to_strict guard
in
403 | Some first
-> ctl_and s first rest
405 let and_after guard first rest
=
406 let s = guard_to_strict guard
in
407 match rest
with After rest
-> ctl_and s first rest
| _
-> first
410 let bind x y
= x
or y
in
411 let option_default = false in
412 let mcode r
(_
,_
,kind
,metapos
) =
414 Ast.MINUS
(_
,_
,_
,_
) -> true
415 | Ast.PLUS _
-> failwith
"not possible"
416 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
417 let do_nothing r k e
= k e
in
418 let rule_elem r k re
=
420 match Ast.unwrap re
with
421 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
422 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
423 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
426 V.combiner
bind option_default
427 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
428 do_nothing do_nothing do_nothing do_nothing
429 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
430 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
431 recursor.V.combiner_rule_elem
434 let bind x y
= x
or y
in
435 let option_default = false in
436 let mcode r
(_
,_
,kind
,metapos
) =
438 Ast.MetaPos
(_
,_
,_
,_
,_
) -> true
439 | Ast.NoMetaPos
-> false 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
456 (* code is not a DisjRuleElem *)
457 let make_match label guard code
=
458 let v = fresh_var() in
459 let matcher = Lib_engine.Match
(code
) in
460 if contains_modif code
&& not guard
461 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
463 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
464 (match (iso_info,!onlyModif,guard
,
465 intersect !used_after (Ast.get_fvs code
)) with
466 (false,true,_
,[]) | (_
,_
,true,_
) ->
467 predmaker guard
(matcher,CTL.Control
) label
468 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
470 let make_raw_match label guard code
=
471 predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
473 let rec seq_fvs quantified
= function
476 let t1fvs = get_unquantified quantified fv1
in
478 List.fold_left
Common.union_set
[]
479 (List.map
(get_unquantified quantified
) fvs
) in
480 let bothfvs = Common.inter_set
t1fvs termfvs in
481 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
482 let new_quantified = Common.union_set
bothfvs quantified
in
483 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
488 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
490 let non_saved_quantify =
492 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
494 let intersectll lst nested_list
=
495 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
497 (* --------------------------------------------------------------------- *)
498 (* Count depth of braces. The translation of a closed brace appears deeply
499 nested within the translation of the sequence term, so the name of the
500 paren var has to take into account the names of the nested braces. On the
501 other hand the close brace does not escape, so we don't have to take into
502 account other paren variable names. *)
504 (* called repetitively, which is inefficient, but less trouble than adding a
505 new field to Seq and FunDecl *)
506 let count_nested_braces s =
507 let bind x y
= max x y
in
508 let option_default = 0 in
509 let stmt_count r k
s =
510 match Ast.unwrap
s with
511 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
513 let donothing r k e
= k e
in
515 let recursor = V.combiner
bind option_default
516 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
517 donothing donothing donothing donothing
518 donothing donothing donothing donothing donothing donothing
519 donothing donothing stmt_count donothing donothing donothing in
520 let res = string_of_int
(recursor.V.combiner_statement
s) in
524 let get_label_ctr _
=
525 let cur = !labelctr in
527 string2var (Printf.sprintf
"l%d" cur)
529 (* --------------------------------------------------------------------- *)
530 (* annotate dots with before and after neighbors *)
532 let print_bef_aft = function
534 Printf.printf
"bef/aft\n";
535 Pretty_print_cocci.rule_elem "" re
;
536 Format.print_newline
()
538 Printf.printf
"bef/aft\n";
539 Pretty_print_cocci.statement
"" s;
540 Format.print_newline
()
541 | Ast.Other_dots
d ->
542 Printf.printf
"bef/aft\n";
543 Pretty_print_cocci.statement_dots
d;
544 Format.print_newline
()
546 (* [] can only occur if we are in a disj, where it comes from a ? In that
547 case, we want to use a, which accumulates all of the previous patterns in
549 let rec get_before_elem sl a
=
550 match Ast.unwrap sl
with
554 [] -> ([],Common.Right a
)
556 let (e
,ea
) = get_before_e e a
in
559 let (e
,ea
) = get_before_e e a
in
560 let (sl
,sla
) = loop sl ea
in
562 let (l,a
) = loop x a
in
563 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
564 | Ast.CIRCLES
(x
) -> failwith
"not supported"
565 | Ast.STARS
(x
) -> failwith
"not supported"
567 and get_before sl a
=
568 match get_before_elem sl a
with
569 (term
,Common.Left x
) -> (term
,x
)
570 | (term
,Common.Right x
) -> (term
,x
)
572 and get_before_whencode wc
=
575 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
576 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
577 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
578 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
579 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
582 and get_before_e
s a
=
583 match Ast.unwrap
s with
584 Ast.Dots
(d,w
,_
,aft
) ->
585 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
586 | Ast.Nest
(stmt_dots
,w
,multi
,_
,aft
) ->
587 let w = get_before_whencode
w in
588 let (sd
,_
) = get_before stmt_dots a
in
590 got rid of this, don't want to let nests overshoot
595 Unify_ast.unify_statement_dots
596 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
598 Unify_ast.MAYBE -> false
600 | Ast.Other_dots a ->
601 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
603 Unify_ast.MAYBE -> false
607 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,a,aft
)),[Ast.Other_dots stmt_dots
])
608 | Ast.Disj
(stmt_dots_list
) ->
610 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
611 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
613 (match Ast.unwrap ast
with
614 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
615 | _
-> (s,[Ast.Other
s]))
616 | Ast.Seq
(lbrace
,body
,rbrace
) ->
617 let index = count_nested_braces s in
618 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
619 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
620 | Ast.Define
(header
,body
) ->
621 let (body
,_
) = get_before body
[] in
622 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
623 | Ast.IfThen
(ifheader
,branch
,aft
) ->
624 let (br
,_
) = get_before_e branch
[] in
625 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
626 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
627 let (br1
,_
) = get_before_e branch1
[] in
628 let (br2
,_
) = get_before_e branch2
[] in
629 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
630 | Ast.While
(header
,body
,aft
) ->
631 let (bd
,_
) = get_before_e body
[] in
632 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
633 | Ast.For
(header
,body
,aft
) ->
634 let (bd
,_
) = get_before_e body
[] in
635 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
636 | Ast.Do
(header
,body
,tail
) ->
637 let (bd
,_
) = get_before_e body
[] in
638 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
639 | Ast.Iterator
(header
,body
,aft
) ->
640 let (bd
,_
) = get_before_e body
[] in
641 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
642 | Ast.Switch
(header
,lb
,decls
,cases
,rb
) ->
643 let index = count_nested_braces s in
644 let (de
,dea
) = get_before decls
[Ast.WParen
(lb
,index)] in
647 (function case_line
->
648 match Ast.unwrap case_line
with
649 Ast.CaseLine
(header
,body
) ->
650 let (body
,_
) = get_before body
[] in
651 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
652 | Ast.OptCase
(case_line
) -> failwith
"not supported")
654 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),
655 [Ast.WParen
(rb
,index)])
656 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
657 let (bd
,_
) = get_before body
[] in
658 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
660 Pretty_print_cocci.statement
"" s; Format.print_newline
();
661 failwith
"get_before_e: not supported"
663 let rec get_after sl
a =
664 match Ast.unwrap sl
with
670 let (sl
,sla
) = loop sl
in
671 let (e
,ea
) = get_after_e e sla
in
673 let (l,a) = loop x
in
674 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
675 | Ast.CIRCLES
(x
) -> failwith
"not supported"
676 | Ast.STARS
(x
) -> failwith
"not supported"
678 and get_after_whencode
a wc
=
681 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
682 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
683 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
684 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
685 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
688 and get_after_e
s a =
689 match Ast.unwrap
s with
690 Ast.Dots
(d,w,bef
,_
) ->
691 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
692 | Ast.Nest
(stmt_dots
,w,multi
,bef
,_
) ->
693 let w = get_after_whencode
a w in
694 let (sd
,_
) = get_after stmt_dots
a in
696 got rid of this. don't want to let nests overshoot
701 Unify_ast.unify_statement_dots
702 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
704 Unify_ast.MAYBE -> false
706 | Ast.Other_dots a ->
707 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
709 Unify_ast.MAYBE -> false
713 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,bef
,a)),[Ast.Other_dots stmt_dots
])
714 | Ast.Disj
(stmt_dots_list
) ->
716 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
717 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
719 (match Ast.unwrap ast
with
720 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
721 (* check "after" information for metavar optimization *)
722 (* if the error is not desired, could just return [], then
723 the optimization (check for EF) won't take place *)
727 (match Ast.unwrap x
with
728 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
730 "dots/nest not allowed before and after stmt metavar"
732 | Ast.Other_dots x
->
733 (match Ast.undots x
with
735 (match Ast.unwrap x
with
736 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
738 ("dots/nest not allowed before and after stmt "^
747 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
748 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
749 | _
-> (s,[Ast.Other
s]))
750 | Ast.Seq
(lbrace
,body
,rbrace
) ->
751 let index = count_nested_braces s in
752 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
753 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
754 [Ast.WParen
(lbrace
,index)])
755 | Ast.Define
(header
,body
) ->
756 let (body
,_
) = get_after body
a in
757 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
758 | Ast.IfThen
(ifheader
,branch
,aft
) ->
759 let (br
,_
) = get_after_e branch
a in
760 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
761 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
762 let (br1
,_
) = get_after_e branch1
a in
763 let (br2
,_
) = get_after_e branch2
a in
764 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
765 | Ast.While
(header
,body
,aft
) ->
766 let (bd
,_
) = get_after_e body
a in
767 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
768 | Ast.For
(header
,body
,aft
) ->
769 let (bd
,_
) = get_after_e body
a in
770 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
771 | Ast.Do
(header
,body
,tail
) ->
772 let (bd
,_
) = get_after_e body
a in
773 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
774 | Ast.Iterator
(header
,body
,aft
) ->
775 let (bd
,_
) = get_after_e body
a in
776 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
777 | Ast.Switch
(header
,lb
,decls
,cases,rb
) ->
778 let index = count_nested_braces s in
781 (function case_line
->
782 match Ast.unwrap case_line
with
783 Ast.CaseLine
(header
,body
) ->
784 let (body
,_
) = get_after body
[Ast.WParen
(rb
,index)] in
785 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
786 | Ast.OptCase
(case_line
) -> failwith
"not supported")
788 let (de
,_
) = get_after decls
[] in
789 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),[Ast.WParen
(lb
,index)])
790 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
791 let (bd
,_
) = get_after body
[] in
792 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
793 | _
-> failwith
"get_after_e: not supported"
795 let preprocess_dots sl
=
796 let (sl
,_
) = get_before sl
[] in
797 let (sl
,_
) = get_after sl
[] in
800 let preprocess_dots_e sl
=
801 let (sl
,_
) = get_before_e sl
[] in
802 let (sl
,_
) = get_after_e sl
[] in
805 (* --------------------------------------------------------------------- *)
806 (* various return_related things *)
808 let rec ends_in_return stmt_list
=
809 match Ast.unwrap stmt_list
with
811 (match List.rev x
with
813 (match Ast.unwrap x
with
816 match Ast.unwrap x
with
817 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
818 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
821 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
824 | Ast.CIRCLES
(x
) -> failwith
"not supported"
825 | Ast.STARS
(x
) -> failwith
"not supported"
827 (* --------------------------------------------------------------------- *)
830 let exptymatch l make_match make_guard_match
=
831 let pos = fresh_pos() in
832 let matches_guard_matches =
835 let pos = Ast.make_mcode
pos in
836 (make_match (Ast.set_pos x
(Some
pos)),
837 make_guard_match
(Ast.set_pos x
(Some
pos))))
839 let (matches
,guard_matches
) = List.split
matches_guard_matches in
840 let rec suffixes = function
842 | x
::xs -> xs::(suffixes xs) in
844 (* normally, we check that an expression does not match something
845 earlier in the disjunction (calculated as prefixes). But for large
846 disjunctions, this can result in a very big CTL formula. So we
847 give the user the option to say he doesn't want this feature, if that is
849 if !Flag_matcher.no_safe_expressions
850 then List.map
(function _
-> []) matches
851 else List.rev
(suffixes (List.rev guard_matches
)) in
852 let info = (* not null *)
858 ctl_and CTL.NONSTRICT
matcher
860 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
862 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
864 (* code might be a DisjRuleElem, in which case we break it apart
865 code might contain an Exp or Ty
866 this one pushes the quantifier inwards *)
867 let do_re_matches label guard
res quantified minus_quantified
=
868 let make_guard_match x
=
869 let stmt_fvs = Ast.get_mfvs x
in
870 let fvs = get_unquantified minus_quantified
stmt_fvs in
871 non_saved_quantify fvs (make_match None
true x
) in
873 let stmt_fvs = Ast.get_fvs x
in
874 let fvs = get_unquantified quantified
stmt_fvs in
875 quantify guard
fvs (make_match None guard x
) in
876 (* label used to be used here, but it is not use; label is only needed after
878 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
879 (match List.map
Ast.unwrap
res with
880 [] -> failwith
"unexpected empty disj"
881 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
882 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
884 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
886 then failwith
"unexpected exp or ty";
887 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
889 (* code might be a DisjRuleElem, in which case we break it apart
890 code doesn't contain an Exp or Ty
891 this one is for use when it is not practical to push the quantifier inwards
893 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
894 match Ast.unwrap code
with
895 Ast.DisjRuleElem
(res) ->
896 let make_match = make_match None guard
in
897 let orop = if guard
then ctl_or else ctl_seqor in
898 (* label used to be used here, but it is not use; label is only needed after
900 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
901 (List.fold_left
orop CTL.False
(List.map
make_match res))
902 | _
-> make_match label guard code
904 (* --------------------------------------------------------------------- *)
905 (* control structures *)
907 let end_control_structure fvs header body after_pred
908 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
909 (* aft indicates what is added after the whole if, which has to be added
911 let (aft_needed
,after_branch
) =
913 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
914 (false,make_seq_after2 guard after_pred after
)
917 make_match label guard
918 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
920 make_seq_after guard after_pred
921 (After
(make_seq_after guard
match_endif after
))) in
922 let body = body after_branch
in
923 let s = guard_to_strict guard
in
928 (match (after
,aft_needed
) with
929 (After _
,_
) (* pattern doesn't end here *)
930 | (_
,true) (* + code added after *) -> after_checks
931 | _
-> no_after_checks
)
932 (ctl_ax_absolute s body)))
934 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
935 quantified minus_quantified label llabel slabel recurse
make_match guard
=
936 (* "if (test) thn" becomes:
937 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
939 "if (test) thn; after" becomes:
940 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
945 match seq_fvs quantified
946 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
947 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
948 | _
-> failwith
"not possible" in
949 let new_quantified = Common.union_set bfvs quantified
in
951 match seq_fvs minus_quantified
952 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
953 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
954 | _
-> failwith
"not possible" in
955 let new_mquantified = Common.union_set mbfvs minus_quantified
in
957 let if_header = quantify guard efvs
(make_match ifheader
) in
958 (* then branch and after *)
959 let lv = get_label_ctr() in
960 let used = ref false in
962 (* no point to put a label on truepred etc; it is local to this construct
963 so it must have the same label *)
965 [truepred None
; recurse branch Tail
new_quantified new_mquantified
966 (Some
(lv,used)) llabel slabel guard
] in
967 let after_pred = aftpred None
in
968 let or_cases after_branch
=
969 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
970 let (if_header,wrapper
) =
973 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
974 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
975 (function body -> quantify true [lv] body))
976 else (if_header,function x
-> x
) in
978 (end_control_structure bfvs
if_header or_cases after_pred
979 (Some
(ctl_ex after_pred)) None aft after label guard
)
981 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
982 quantified minus_quantified label llabel slabel recurse
make_match guard
=
983 (* "if (test) thn else els" becomes:
984 if(test) & AX((TrueBranch & AX thn) v
985 (FalseBranch & AX (else & AX els)) v After)
988 "if (test) thn else els; after" becomes:
989 if(test) & AX((TrueBranch & AX thn) v
990 (FalseBranch & AX (else & AX els)) v
991 (After & AXAX after))
996 let (e1fvs
,b1fvs
,s1fvs
) =
997 match seq_fvs quantified
998 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
999 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1000 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1001 | _
-> failwith
"not possible" in
1002 let (e2fvs
,b2fvs
,s2fvs
) =
1004 (* just combine with the else branch. no point to have separate
1005 quantifier, since there is only one possible control-flow path *)
1006 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1007 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1008 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1009 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1010 | _
-> failwith
"not possible" in
1011 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1012 let exponlyfvs = intersect e1fvs e2fvs
in
1013 let new_quantified = union bothfvs quantified
in
1014 (* minus free variables *)
1015 let (me1fvs
,mb1fvs
,ms1fvs
) =
1016 match seq_fvs minus_quantified
1017 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1018 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1019 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1020 | _
-> failwith
"not possible" in
1021 let (me2fvs
,mb2fvs
,ms2fvs
) =
1023 (* just combine with the else branch. no point to have separate
1024 quantifier, since there is only one possible control-flow path *)
1026 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1027 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1028 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1029 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1030 | _
-> failwith
"not possible" in
1031 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1032 let new_mquantified = union mbothfvs minus_quantified
in
1034 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1035 (* then and else branches *)
1036 let lv = get_label_ctr() in
1037 let used = ref false in
1040 [truepred None
; recurse branch1 Tail
new_quantified new_mquantified
1041 (Some
(lv,used)) llabel slabel guard
] in
1046 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1047 (header_match None guard els
);
1048 recurse branch2 Tail
new_quantified new_mquantified
1049 (Some
(lv,used)) llabel slabel guard
] in
1050 let after_pred = aftpred None
in
1051 let or_cases after_branch
=
1052 ctl_or true_branch (ctl_or false_branch after_branch
) in
1053 let s = guard_to_strict guard
in
1054 let (if_header,wrapper
) =
1057 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1058 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1059 (function body -> quantify true [lv] body))
1060 else (if_header,function x
-> x
) in
1062 (end_control_structure bothfvs if_header or_cases after_pred
1063 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1064 (Some
(ctl_ex (falsepred None
)))
1065 aft after label guard
)
1067 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1068 quantified minus_quantified label recurse
make_match guard
=
1070 (* the translation in this case is similar to that of an if with no else *)
1071 (* free variables *)
1073 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1074 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1075 | _
-> failwith
"not possible" in
1076 let new_quantified = Common.union_set bfvs quantified
in
1077 (* minus free variables *)
1079 match seq_fvs minus_quantified
1080 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1081 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1082 | _
-> failwith
"not possible" in
1083 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1085 let header = quantify guard efvs
(make_match header) in
1086 let lv = get_label_ctr() in
1087 let used = ref false in
1091 recurse
body Tail
new_quantified new_mquantified
1092 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1093 let after_pred = loopfallpred None
in
1094 let or_cases after_branch
= ctl_or body after_branch
in
1095 let (header,wrapper
) =
1098 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1099 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1100 (function body -> quantify true [lv] body))
1101 else (header,function x
-> x
) in
1103 (end_control_structure bfvs
header or_cases after_pred
1104 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1105 match (Ast.unwrap
body,aft
) with
1106 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1107 (match Ast.unwrap re
with
1108 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1109 Type_cocci.Unitary
,_
,false)
1110 when after
= Tail
or after
= End
or after
= VeryEnd
->
1112 match seq_fvs quantified
[Ast.get_fvs
header] with
1114 | _
-> failwith
"not possible" in
1115 quantify guard efvs
(make_match header)
1119 (* --------------------------------------------------------------------- *)
1120 (* statement metavariables *)
1122 (* issue: an S metavariable that is not an if branch/loop body
1123 should not match an if branch/loop body, so check that the labels
1124 of the nodes before the first node matched by the S are different
1125 from the label of the first node matched by the S *)
1126 let sequencibility body label_pred process_bef_aft
= function
1127 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1130 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1131 | Ast.SequencibleAfterDots
l ->
1132 (* S appears after some dots. l is the code that comes after the S.
1133 want to search for that first, because S can match anything, while
1134 the stuff after is probably more restricted *)
1135 let afts = List.map process_bef_aft
l in
1136 let ors = foldl1 ctl_or afts in
1137 ctl_and CTL.NONSTRICT
1138 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1141 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1142 | Ast.NotSequencible
-> body (function x
-> x
)
1144 let svar_context_with_add_after stmt
s label quantified
d ast
1145 seqible after process_bef_aft guard fvinfo
=
1146 let label_var = (*fresh_label_var*) string2var "_lab" in
1148 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1149 (*let prelabel_pred =
1150 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
1151 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1152 let full_metamatch = matcher d in
1153 let first_metamatch =
1156 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
,c
)) ->
1157 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
,c
))
1158 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1159 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1161 let middle_metamatch =
1164 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1165 | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
1167 let last_metamatch =
1170 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
,c
)) ->
1171 Ast.CONTEXT
(pos,Ast.AFTER
(aft
,c
))
1172 | Ast.CONTEXT
(_
,_
) -> d
1173 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1177 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1180 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1181 let left_or = (* the whole statement is one node *)
1182 make_seq_after guard
1183 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_ex to_end)) full_metamatch) after
in
1184 let right_or = (* the statement covers multiple nodes *)
1185 ctl_and CTL.NONSTRICT
1188 [to_end; make_seq_after guard
last_metamatch after
]))
1194 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1198 ctl_au CTL.NONSTRICT
1201 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1203 (ctl_not prelabel_pred) after])] in
1207 ctl_and CTL.NONSTRICT
label_pred
1208 (f
(ctl_and CTL.NONSTRICT
1209 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1210 let stmt_fvs = Ast.get_fvs stmt
in
1211 let fvs = get_unquantified quantified
stmt_fvs in
1212 quantify guard
(label_var::fvs)
1213 (sequencibility body label_pred process_bef_aft seqible
)
1215 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1216 seqible after process_bef_aft guard fvinfo
=
1217 let label_var = (*fresh_label_var*) string2var "_lab" in
1219 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1221 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1222 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1224 match (d,after
) with
1225 (Ast.PLUS _
, _
) -> failwith
"not possible"
1226 | (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1227 (* just match the root. don't care about label; always ok *)
1228 make_raw_match None
false ast
1229 | (Ast.CONTEXT
(pos,Ast.BEFORE
(_
,_
)),(Tail
|End
|VeryEnd
)) ->
1230 ctl_and CTL.NONSTRICT
1231 (make_raw_match None
false ast
) (* statement *)
1232 (matcher d) (* transformation *)
1233 | (Ast.CONTEXT
(pos,(Ast.NOTHING
|Ast.BEFORE
(_
,_
))),(After
a | Guard
a)) ->
1234 (* This case and the MINUS one couldprobably be merged, if
1235 HackForStmt were to notice when its arguments are trivial *)
1236 let first_metamatch = matcher d in
1237 (* try to follow after link *)
1238 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1240 ctl_ex(make_seq guard
[to_end; CTL.True
; a]) in
1242 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1243 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1244 (ctl_and CTL.NONSTRICT
1245 first_metamatch (ctl_or is_compound not_compound))
1246 | (Ast.CONTEXT
(pos,(Ast.AFTER _
|Ast.BEFOREAFTER _
)),_
) ->
1247 failwith
"not possible"
1248 | (Ast.MINUS
(pos,inst
,adj
,l),after
) ->
1249 let (first_metamatch,last_metamatch,rest_metamatch
) =
1251 [] -> (matcher(Ast.CONTEXT
(pos,Ast.NOTHING
)),CTL.True
,matcher d)
1253 matcher(Ast.MINUS
(pos,inst
,adj
,[])),
1254 ctl_and CTL.NONSTRICT
1255 (ctl_not (make_raw_match label
false ast
))
1256 (matcher(Ast.MINUS
(pos,inst
,adj
,[])))) in
1257 (* try to follow after link *)
1258 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1262 [to_end; make_seq_after guard
last_metamatch after
]) in
1264 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1265 ctl_and CTL.NONSTRICT
1266 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1267 (ctl_and CTL.NONSTRICT
1268 first_metamatch (ctl_or is_compound not_compound)))
1269 (* don't have to put anything before the beginning, so don't have to
1270 distinguish the first node. so don't have to bother about paths,
1271 just use the label. label ensures that found nodes match up with
1272 what they should because it is in the lhs of the andany. *)
1273 (CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1274 ctl_and CTL.NONSTRICT
label_pred
1275 (make_raw_match label
false ast
),
1276 ctl_and CTL.NONSTRICT rest_metamatch
prelabel_pred))
1278 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1279 let stmt_fvs = Ast.get_fvs stmt
in
1280 let fvs = get_unquantified quantified
stmt_fvs in
1281 quantify guard
(label_var::fvs)
1282 (sequencibility body label_pred process_bef_aft seqible
)
1284 (* --------------------------------------------------------------------- *)
1285 (* dots and nests *)
1287 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1288 let matchgoto = gotopred None
in
1290 make_match None
false
1292 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1294 make_match None
false
1296 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1298 if quantifier
= Exists
1299 then Common.Left
(CTL.False
)
1301 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1303 then Common.Left
(aftpred label
)
1306 (function vx
-> function v ->
1307 (* vx is the contents of the nest, if any. we can only stop early
1308 if we find neither the ending code nor the nest contents in
1309 the if branch. not sure if this is a good idea. *)
1310 let lv = get_label_ctr() in
1311 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1312 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1314 (* Rather a special case. But if the code afterwards is just
1315 a } then there is no point checking after a goto that it does
1317 (* this optimization doesn't work. probably depends on whether
1318 the destination of the break/goto is local or more global than
1320 match seq_after
with
1322 let is_paren = function
1323 CTL.Pred
(Lib_engine.Paren _
,_
) -> true
1325 is_paren e1
or is_paren e2
1327 ctl_or (aftpred label
)
1328 (quantify false [lv]
1329 (ctl_and CTL.NONSTRICT
1330 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1331 (ctl_au CTL.NONSTRICT
1332 (ctl_and CTL.NONSTRICT
(ctl_not v)
1333 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1334 (ctl_and CTL.NONSTRICT
preflabelpred
1335 (if !Flag_matcher.only_return_is_error_exit
1337 (ctl_and CTL.NONSTRICT
1338 (retpred None
) (ctl_not seq_after
))
1341 (ctl_and CTL.NONSTRICT
1342 (ctl_or (retpred None
) matchcontinue)
1343 (ctl_not seq_after
))
1344 (ctl_and CTL.NONSTRICT
1345 (ctl_or matchgoto matchbreak)
1347 (* an optim that failed see defn is_paren
1348 and tests/makes_a_loop *)
1352 (ctl_not seq_after
))))))))))) in
1353 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1354 let v = get_let_ctr() in
1356 (match stop_early with
1357 Common.Left x1
-> ctl_or y x1
1358 | Common.Right
stop_early ->
1361 (ctl_and CTL.NONSTRICT
(label_pred_maker label
)
1362 (stop_early n
(CTL.Ref
v)))))
1364 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1365 process_bef_aft statement_list statement guard quantified wrapcode
=
1366 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1367 (* proces bef_aft *)
1369 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1370 let bef_aft = (* to be negated *)
1374 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1377 with Not_found
-> shortest (Common.union_set bef aft
) in
1380 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1382 let check_quantifier quant other
=
1384 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1388 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1390 then failwith
"inconsistent annotation on dots"
1394 if check_quantifier Ast.WhenExists
Ast.WhenForall
1397 if check_quantifier Ast.WhenForall
Ast.WhenExists
1400 (* the following is used when we find a goto, etc and consider accepting
1401 without finding the rest of the pattern *)
1402 let aft = shortest aft in
1403 (* process whencode *)
1404 let labelled = label_pred_maker label
in
1406 let (poswhen
,negwhen
) =
1408 (function (poswhen
,negwhen
) ->
1410 Ast.WhenNot
whencodes ->
1411 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1412 | Ast.WhenAlways stm
->
1413 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1414 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1415 | Ast.WhenNotTrue
(e
) ->
1417 ctl_or (whencond_true e label guard quantified
) negwhen
)
1418 | Ast.WhenNotFalse
(e
) ->
1420 ctl_or (whencond_false e label guard quantified
) negwhen
))
1421 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1422 (*bef_aft modifies arg so that inside of a nest can't cause the next
1423 to overshoot its boundaries, eg a() <...f()...> b() where f is
1424 a metavariable and the whole thing matches code in a loop;
1425 don't want f to match eg b(), allowing to go around the loop again*)
1426 let poswhen = ctl_and_ns arg
poswhen in
1430 (* add in After, because it's not part of the program *)
1431 ctl_or (aftpred label
) negwhen
1433 ctl_and_ns poswhen (ctl_not negwhen) in
1434 (* process dot code, if any *)
1436 match (dotcode,guard
) with
1437 (None
,_) | (_,true) -> CTL.True
1438 | (Some
dotcode,_) -> dotcode in
1439 (* process nest code, if any *)
1440 (* whencode goes in the negated part of the nest; if no nest, just goes
1441 on the "true" in between code *)
1442 let plus_var = if plus
then get_label_ctr() else string2var "" in
1443 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1444 let (ornest
,just_nest
) =
1445 (* just_nest is used when considering whether to stop early, to continue
1446 to collect nest information in the if branch *)
1447 match (nest
,guard
&& not plus
) with
1448 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1449 | (Some nest
,false) ->
1450 let v = get_let_ctr() in
1454 (* the idea is that BindGood is sort of a witness; a witness to
1455 having found the subterm in at least one place. If there is
1456 not a witness, then there is a risk that it will get thrown
1457 away, if it is merged with a node that has an empty
1458 environment. See tests/nestplus. But this all seems
1459 rather suspicious *)
1460 CTL.And
(CTL.NONSTRICT
,x
,
1461 CTL.Exists
(true,plus_var2,
1462 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1463 CTL.Modif
plus_var2)))
1467 CTL.Or
(is_plus (CTL.Ref
v),
1468 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1470 let plus_modifier x
=
1477 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1482 (* label within dots is taken care of elsewhere. the next two lines
1483 put the label on the code following dots *)
1484 After f
-> ctl_and (guard_to_strict guard
) f
labelled
1486 (* actually, label should be None based on the only use of Guard... *)
1487 assert (label
= None
);
1488 ctl_and CTL.NONSTRICT
(ctl_uncheck f
) labelled
1490 let exit = endpred label
in
1491 let errorexit = exitpred label
in
1492 ctl_or exit errorexit
1493 (* not at all sure what the next two mean... *)
1497 Some
(lv,used) -> used := true;
1498 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1499 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1500 | None
-> endpred label
)
1501 (* was the following, but not clear why sgrep should allow
1503 let exit = endpred label in
1504 let errorexit = exitpred label in
1506 then ctl_or exit errorexit (* end anywhere *)
1507 else exit (* end at the real end of the function *) *)
in
1509 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1510 label
(guard_to_strict guard
) wrapcode just_nest
1512 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1513 aft ender quantifier)
1515 and get_whencond_exps e
=
1516 match Ast.unwrap e
with
1518 | Ast.DisjRuleElem
(res) ->
1519 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1520 | _ -> failwith
"not possible"
1522 and make_whencond_headers e e1 label guard quantified
=
1523 let fvs = Ast.get_fvs e
in
1525 quantify guard
(get_unquantified quantified
fvs)
1526 (make_match label guard h
) in
1531 (Ast.make_mcode
"if",
1532 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1533 let while_header e1
=
1537 (Ast.make_mcode
"while",
1538 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1543 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1544 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1546 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1548 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1550 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1551 (if_headers, while_headers, for_headers)
1553 and whencond_true e label guard quantified
=
1554 let e1 = get_whencond_exps e
in
1555 let (if_headers, while_headers, for_headers) =
1556 make_whencond_headers e
e1 label guard quantified
in
1558 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1559 (ctl_and CTL.NONSTRICT
1560 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1562 and whencond_false e label guard quantified
=
1563 let e1 = get_whencond_exps e
in
1564 let (if_headers, while_headers, for_headers) =
1565 make_whencond_headers e
e1 label guard quantified
in
1566 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1567 (ctl_and CTL.NONSTRICT
(loopfallpred label
)
1568 (ctl_or (ctl_back_ex if_headers)
1569 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1571 (* --------------------------------------------------------------------- *)
1572 (* the main translation loop *)
1574 let rec statement_list stmt_list after quantified minus_quantified
1575 label llabel slabel dots_before guard
=
1577 (* include Disj to be on the safe side *)
1578 match Ast.unwrap x
with
1579 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1580 let compute_label l e db
= if db
or isdots e
then l else None
in
1581 match Ast.unwrap stmt_list
with
1583 let rec loop quantified minus_quantified dots_before label llabel slabel
1585 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1587 statement e after quantified minus_quantified
1588 (compute_label label e dots_before
)
1590 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1591 let shared = intersectll fv
fvs in
1592 let unqshared = get_unquantified quantified
shared in
1593 let new_quantified = Common.union_set
unqshared quantified
in
1594 let minus_shared = intersectll mfv mfvs
in
1596 get_unquantified minus_quantified
minus_shared in
1597 let new_mquantified =
1598 Common.union_set
munqshared minus_quantified
in
1599 quantify guard
unqshared
1602 (let (label1
,llabel1
,slabel1
) =
1603 match Ast.unwrap e
with
1605 (match Ast.unwrap re
with
1606 Ast.Goto
_ -> (None
,None
,None
)
1607 | _ -> (label
,llabel
,slabel
))
1608 | _ -> (label
,llabel
,slabel
) in
1609 loop new_quantified new_mquantified (isdots e
)
1610 label1 llabel1 slabel1
1612 new_quantified new_mquantified
1613 (compute_label label e dots_before
) llabel slabel guard
)
1614 | _ -> failwith
"not possible" in
1615 loop quantified minus_quantified dots_before
1617 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1618 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1619 | Ast.STARS
(x
) -> failwith
"not supported"
1621 (* llabel is the label of the enclosing loop and slabel is the label of the
1623 and statement stmt after quantified minus_quantified
1624 label llabel slabel guard
=
1625 let ctl_au = ctl_au CTL.NONSTRICT
in
1626 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1627 let ctl_and = ctl_and CTL.NONSTRICT
in
1628 let make_seq = make_seq guard
in
1629 let make_seq_after = make_seq_after guard
in
1630 let real_make_match = make_match in
1631 let make_match = header_match label guard
in
1633 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1636 match Ast.unwrap stmt
with
1638 (match Ast.unwrap ast
with
1639 (* the following optimisation is not a good idea, because when S
1640 is alone, we would like it not to match a declaration.
1641 this makes more matching for things like when (...) S, but perhaps
1642 that matching is not so costly anyway *)
1643 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1644 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_,_)) as d),_),
1646 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_,_)) as d),_),
1648 svar_context_with_add_after stmt
s label quantified
d ast seqible
1650 (process_bef_aft quantified minus_quantified
1651 label llabel slabel
true)
1653 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1655 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1656 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1658 (process_bef_aft quantified minus_quantified
1659 label llabel slabel
true)
1661 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1665 match Ast.unwrap ast
with
1666 Ast.DisjRuleElem
(res) ->
1667 do_re_matches label guard
res quantified minus_quantified
1668 | Ast.Exp
(_) | Ast.Ty
(_) ->
1669 let stmt_fvs = Ast.get_fvs stmt
in
1670 let fvs = get_unquantified quantified
stmt_fvs in
1671 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1673 let stmt_fvs = Ast.get_fvs stmt
in
1674 let fvs = get_unquantified quantified
stmt_fvs in
1675 quantify guard
fvs (make_match ast
) in
1676 match Ast.unwrap ast
with
1677 Ast.Break
(brk
,semi
) ->
1678 (match (llabel
,slabel
) with
1679 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1680 ctl_and term (bclabel_pred_maker slabel
)
1681 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1682 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1683 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1684 (* discard pattern that comes after return *)
1685 let normal_res = make_seq_after term after
in
1686 (* the following code tries to propagate the modifications on
1687 return; to a close brace, in the case where the final return
1690 match (retmc
,semmc
) with
1691 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1692 when !Flag.sgrep_mode2
->
1693 (* in sgrep mode, we can propagate the - *)
1694 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,l1
@l2
))
1695 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
)) ->
1696 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
,Ast.ONE
)))
1697 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
,c1
)),
1698 Ast.CONTEXT
(_,Ast.AFTER
(l2
,c2
))) ->
1699 (if not
(c1
= c2
) then failwith
"bad + code");
1700 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
,c1
)))
1701 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1702 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1704 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1705 Ast.CONTEXT
(_,Ast.AFTER
(l,c
))) ->
1706 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l,c
)))
1708 let ret = Ast.make_mcode
"return" in
1710 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1711 let semi = Ast.make_mcode
";" in
1713 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1715 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1718 let exit = endpred None
in
1720 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1721 let stripped_rbrace =
1722 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1724 (ctl_and (make_match mod_rbrace)
1729 (ctl_or simple_return return_expr))))
1731 (make_match stripped_rbrace)
1732 (* error exit not possible; it is in the middle
1733 of code, so a return is needed *)
1736 (* some change in the middle of the return, so have to
1737 find an actual return *)
1740 (* should try to deal with the dots_bef_aft problem elsewhere,
1741 but don't have the courage... *)
1746 do_between_dots stmt
term End
1747 quantified minus_quantified label llabel slabel guard
in
1749 make_seq_after term after
)
1750 | Ast.Seq
(lbrace
,body,rbrace
) ->
1751 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1754 [Ast.get_fvs lbrace
;
1755 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1757 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1758 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1759 | _ -> failwith
"not possible" in
1760 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1762 seq_fvs minus_quantified
1763 [Ast.get_mfvs lbrace
;
1764 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1766 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1767 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1768 | _ -> failwith
"not possible" in
1769 let pv = count_nested_braces stmt
in
1770 let lv = get_label_ctr() in
1771 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1772 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1775 (quantify guard lbfvs
(make_match lbrace
))
1776 (ctl_and paren_pred label_pred) in
1778 match Ast.unwrap rbrace
with
1779 Ast.SeqEnd
((data
,info,_,pos)) ->
1780 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1781 | _ -> failwith
"unexpected close brace" in
1783 (* label is not needed; paren_pred is enough *)
1784 quantify guard rbfvs
1785 (ctl_au (make_match empty_rbrace)
1787 (real_make_match None guard rbrace
)
1789 let new_quantified2 =
1790 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1791 let new_mquantified2 =
1792 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1793 let pattern_as_given =
1794 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1795 quantify true [pv;lv]
1796 (quantify guard b1fvs
1800 (if !exists = Exists
then CTL.False
else (aftpred label
))
1801 (quantify guard b2fvs
1802 (statement_list body
1803 (After
(make_seq_after end_brace after
))
1804 new_quantified2 new_mquantified2
1805 (Some
(lv,ref true))
1806 llabel slabel
false guard
)))])) in
1807 if ends_in_return body
1809 (* matching error handling code *)
1811 1. The pattern as given
1812 2. A goto, and then some close braces, and then the pattern as
1813 given, but without the braces (only possible if there are no
1814 decls, and open and close braces are unmodified)
1815 3. Part of the pattern as given, then a goto, and then the rest
1816 of the pattern. For this case, we just check that all paths have
1817 a goto within the current braces. checking for a goto at every
1818 point in the pattern seems expensive and not worthwhile. *)
1820 let body = preprocess_dots body in (* redo, to drop braces *)
1824 (make_match empty_rbrace)
1825 (ctl_ax (* skip the destination label *)
1826 (quantify guard b2fvs
1827 (statement_list body End
1828 new_quantified2 new_mquantified2 None llabel slabel
1831 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1832 quantify true [pv;lv]
1833 (quantify guard b1fvs
1837 (CTL.AU
(* want AF even for sgrep *)
1838 (CTL.FORWARD
,CTL.STRICT
,
1839 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1840 ctl_and (* brace must be eventually after goto *)
1841 (gotopred (Some
(lv,ref true)))
1842 (* want AF even for sgrep *)
1843 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1844 (quantify guard b2fvs
1845 (statement_list body Tail
1846 new_quantified2 new_mquantified2
1847 None
(*no label because past the goto*)
1848 llabel slabel
false guard
))])) in
1849 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1850 else pattern_as_given
1851 | Ast.IfThen
(ifheader
,branch
,aft) ->
1852 ifthen ifheader branch
aft after quantified minus_quantified
1853 label llabel slabel statement
make_match guard
1855 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1856 ifthenelse ifheader branch1 els branch2
aft after quantified
1857 minus_quantified label llabel slabel statement
make_match guard
1859 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1860 | Ast.Iterator
(header,body,aft) ->
1861 forwhile header body aft after quantified minus_quantified
1862 label statement
make_match guard
1864 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1865 (*ctl_and seems pointless, disjuncts see label too
1866 (label_pred_maker label)*)
1867 (List.fold_left
ctl_seqor CTL.False
1870 statement_list sl after quantified minus_quantified label
1871 llabel slabel
true guard
)
1874 | Ast.Nest
(stmt_dots
,whencode
,multi
,bef
,aft) ->
1875 (* label in recursive call is None because label check is already
1876 wrapped around the corresponding code *)
1879 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1881 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1882 | _ -> failwith
"not possible" in
1884 (* no minus version because when code doesn't contain any minus code *)
1885 let new_quantified = Common.union_set
bfvs quantified
in
1889 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1890 None llabel slabel
true guard
in
1891 dots_and_nests multi
1892 (Some
dots_pattern) whencode bef
aft None after label
1893 (process_bef_aft
new_quantified minus_quantified
1894 None llabel slabel
true)
1896 statement_list x Tail
new_quantified minus_quantified None
1897 llabel slabel
true true)
1899 statement x Tail
new_quantified minus_quantified None
1902 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1904 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1907 Ast.MINUS
(_,_,_,_) ->
1908 (* no need for the fresh metavar, but ... is a bit weird as a
1910 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1912 dots_and_nests false None
whencodes bef
aft dot_code after label
1913 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1915 statement_list x Tail quantified minus_quantified
1916 None llabel slabel
true true)
1918 statement x Tail quantified minus_quantified None llabel slabel
true)
1920 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1922 | Ast.Switch
(header,lb
,decls
,cases,rb
) ->
1923 let rec intersect_all = function
1926 | x
::xs -> intersect x
(intersect_all xs) in
1927 let rec intersect_all2 = function (* pairwise *)
1932 (function elem
-> List.exists (List.mem elem
) xs)
1934 Common.union_set
front (intersect_all2 xs) in
1935 let rec union_all l = List.fold_left
union [] l in
1936 (* start normal variables *)
1937 let header_fvs = Ast.get_fvs
header in
1938 let lb_fvs = Ast.get_fvs lb
in
1939 let decl_fvs = union_all (List.map
Ast.get_fvs
(Ast.undots decls
)) in
1940 let case_fvs = List.map
Ast.get_fvs
cases in
1941 let rb_fvs = Ast.get_fvs rb
in
1942 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1943 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1945 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1946 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1947 function case_fvs ->
1948 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
1949 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
1950 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
1951 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
1953 | _ -> failwith
"not possible")
1954 ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
1955 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1956 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1957 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
1958 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
1959 List.rev all_rbfvs
) in
1960 let exponlyfvs = intersect_all all_efvs
in
1961 let lbonlyfvs = intersect_all all_lbfvs
in
1962 (* don't do anything with right brace. Hope there is no + code on it *)
1963 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1964 let b1fvs = union_all all_b1fvs
in
1965 let new1_quantified = union b1fvs quantified
in
1967 union (union_all all_b2fvs
) (intersect_all2 all_casefvs
) in
1968 let new2_quantified = union b2fvs new1_quantified in
1969 (* let b3fvs = union_all all_b3fvs in*)
1970 (* ------------------- start minus free variables *)
1971 let header_mfvs = Ast.get_mfvs
header in
1972 let lb_mfvs = Ast.get_mfvs lb
in
1973 let decl_mfvs = union_all (List.map
Ast.get_mfvs
(Ast.undots decls
)) in
1974 let case_mfvs = List.map
Ast.get_mfvs
cases in
1975 let rb_mfvs = Ast.get_mfvs rb
in
1976 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1977 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1979 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1980 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1981 function case_mfvs ->
1984 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1985 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
1986 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
1987 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
1989 | _ -> failwith
"not possible")
1990 ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
1991 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1992 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1993 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
1994 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
1995 List.rev all_mrbfvs
) in
1996 (* don't do anything with right brace. Hope there is no + code on it *)
1997 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1998 let mb1fvs = union_all all_mb1fvs
in
1999 let new1_mquantified = union mb1fvs quantified
in
2001 union (union_all all_mb2fvs
) (intersect_all2 all_mcasefvs
) in
2002 let new2_mquantified = union mb2fvs new1_mquantified in
2003 (* let b3fvs = union_all all_b3fvs in*)
2004 (* ------------------- end collection of free variables *)
2005 let switch_header = quantify guard
exponlyfvs (make_match header) in
2006 let lb = quantify guard
lbonlyfvs (make_match lb) in
2007 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
2010 (function case_line
->
2011 match Ast.unwrap case_line
with
2012 Ast.CaseLine
(header,body) ->
2014 match seq_fvs new2_quantified [Ast.get_fvs
header] with
2015 [(e1fvs,_)] -> e1fvs
2016 | _ -> failwith
"not possible" in
2017 quantify guard
e1fvs (real_make_match label
true header)
2018 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2020 let lv = get_label_ctr() in
2021 let used = ref false in
2022 let (decls_exists_code
,decls_all_code
) =
2023 (*don't really understand this*)
2024 if (Ast.undots decls
) = []
2025 then (CTL.True
,CTL.False
)
2028 statement_list decls Tail
2029 new2_quantified new2_mquantified (Some
(lv,used)) llabel None
2034 (List.fold_left
ctl_or_fl CTL.False
2035 (List.map
ctl_uncheck
2036 (decls_all_code
::case_headers))) in
2039 (function case_line
->
2040 match Ast.unwrap case_line
with
2041 Ast.CaseLine
(header,body) ->
2042 let (e1fvs,b1fvs,s1fvs
) =
2043 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
2044 match seq_fvs new2_quantified fvs with
2045 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2046 | _ -> failwith
"not possible" in
2047 let (me1fvs
,mb1fvs,ms1fvs
) =
2048 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
2049 match seq_fvs new2_mquantified fvs with
2050 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2051 | _ -> failwith
"not possible" in
2053 quantify guard
e1fvs (make_match header) in
2054 let new3_quantified = union b1fvs new2_quantified in
2055 let new3_mquantified = union mb1fvs new2_mquantified in
2057 statement_list body Tail
2058 new3_quantified new3_mquantified (Some
(lv,used)) llabel
2059 (Some
(lv,used)) false(*?*) guard
in
2060 quantify guard
b1fvs (make_seq [case_header; body])
2061 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2063 let default_required =
2066 match Ast.unwrap case
with
2067 Ast.CaseLine
(header,_) ->
2068 (match Ast.unwrap
header with
2069 Ast.Default
(_,_) -> true
2073 then function x
-> x
2074 else function x
-> ctl_or (fallpred label
) x
in
2075 let after_pred = aftpred label
in
2076 let body after_branch
=
2079 (quantify guard
b2fvs
2082 (List.fold_left
ctl_and CTL.True
2084 (decls_exists_code
:: case_headers)));
2085 List.fold_left
ctl_or_fl no_header
2086 (decls_all_code
:: case_code)])))
2089 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2090 match Ast.unwrap
rb with
2091 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2092 | _ -> failwith
"not possible") in
2093 let (switch_header,wrapper
) =
2096 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2097 (ctl_and switch_header label_pred,
2098 (function body -> quantify true [lv] body))
2099 else (switch_header,function x
-> x
) in
2101 (end_control_structure b1fvs switch_header body
2102 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2103 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2104 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2107 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2108 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2110 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2111 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2112 | _ -> failwith
"not possible" in
2113 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2116 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2117 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2119 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2120 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2121 | _ -> failwith
"not possible" in
2122 let function_header = quantify guard hfvs
(make_match header) in
2123 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2124 let stripped_rbrace =
2125 match Ast.unwrap rbrace
with
2126 Ast.SeqEnd
((data
,info,_,_)) ->
2127 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2128 | _ -> failwith
"unexpected close brace" in
2130 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2131 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2132 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2134 (quantify guard rbfvs
(make_match rbrace
))
2136 (* the following finds the beginning of the fake braces,
2137 if there are any, not completely sure how this works.
2138 sse the examples sw and return *)
2139 (ctl_back_ex (ctl_not fake_brace))
2140 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2141 let new_quantified3 =
2142 Common.union_set
b1fvs
2143 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2144 let new_mquantified3 =
2145 Common.union_set
mb1fvs
2146 (Common.union_set
mb2fvs
2147 (Common.union_set mb3fvs minus_quantified
)) in
2149 match (Ast.undots
body,
2150 contains_modif rbrace
or contains_pos rbrace
) with
2152 (match Ast.unwrap
body with
2153 Ast.Nest
(stmt_dots
,[],false,_,_) ->
2154 (* special case for function header + body - header is unambiguous
2155 and unique, so we can just look for the nested body anywhere
2159 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2160 statement_list stmt_dots
2161 (* discards match on right brace, but don't need it *)
2162 (Guard
(make_seq_after end_brace after
))
2163 new_quantified3 new_mquantified3
2164 None llabel slabel
true guard
))
2165 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2167 (* flow sensitive, so not optimizable *)
2168 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2170 | _ -> true) whencode
) ->
2171 (* try to be more efficient for the case where the body is just
2172 ... Perhaps this is too much of a special case, but useful
2173 for dropping a parameter and checking that it is never used. *)
2175 Ast.MINUS
(_,_,_,_) -> None
2189 Ast.WhenAlways
(s) -> prev
2190 | Ast.WhenNot
(sl
) ->
2192 statement_list sl Tail
2198 | Ast.WhenNotTrue
(_)
2199 | Ast.WhenNotFalse
(_) ->
2200 failwith
"unexpected"
2202 (Ast.WhenAny
) -> CTL.False
2203 | Ast.WhenModifier
(_) -> prev
)
2204 CTL.False whencode
))
2208 Ast.WhenAlways
(s) ->
2213 label llabel slabel
true in
2215 | Ast.WhenNot
(sl
) -> prev
2216 | Ast.WhenNotTrue
(_)
2217 | Ast.WhenNotFalse
(_) ->
2218 failwith
"unexpected"
2219 | Ast.WhenModifier
(Ast.WhenAny
) ->
2221 | Ast.WhenModifier
(_) -> prev
)
2222 CTL.True whencode
) in
2223 ctl_au leftarg (make_match stripped_rbrace)]))
2227 (* function body is all minus, no whencode *)
2228 match Ast.undots
body with
2230 (match Ast.unwrap
body with
2232 ((_,i
,(Ast.MINUS
(_,_,_,[]) as d),_),[],_,_) ->
2233 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2234 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,[]),_)),
2235 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,[]),_)))
2236 when not
(contains_pos rbrace
) ->
2238 (* andany drops everything to the end, including close
2239 braces - not just function body, could check
2240 label to keep braces *)
2241 (ctl_and start_brace
2244 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2246 (make_meta_rule_elem d ([],[],[]))))))
2251 match (optim1,optim2) with
2257 quantify guard
b3fvs
2258 (statement_list body
2259 (After
(make_seq_after end_brace after
))
2260 new_quantified3 new_mquantified3 None llabel slabel
2262 quantify guard
b1fvs
2263 (make_seq [function_header; quantify guard
b2fvs body_code])
2264 | Ast.Define
(header,body) ->
2265 let (hfvs
,bfvs,bodyfvs
) =
2266 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2268 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2269 | _ -> failwith
"not possible" in
2270 let (mhfvs
,mbfvs
,mbodyfvs
) =
2271 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2273 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2274 | _ -> failwith
"not possible" in
2275 let define_header = quantify guard hfvs
(make_match header) in
2277 statement_list body after
2278 (Common.union_set
bfvs quantified
)
2279 (Common.union_set mbfvs minus_quantified
)
2280 None llabel slabel
true guard
in
2281 quantify guard
bfvs (make_seq [define_header; body_code])
2282 | Ast.OptStm
(stm
) ->
2283 failwith
"OptStm should have been compiled away\n"
2284 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2285 | _ -> failwith
"not supported" in
2286 if guard
or !dots_done
2289 do_between_dots stmt
term after quantified minus_quantified
2290 label llabel slabel guard
2292 (* term is the translation of stmt *)
2293 and do_between_dots stmt
term after quantified minus_quantified
2294 label llabel slabel guard
=
2295 match Ast.get_dots_bef_aft stmt
with
2296 Ast.AddingBetweenDots
(brace_term
,n
)
2297 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2299 statement brace_term after quantified minus_quantified
2300 label llabel slabel guard
in
2301 let v = Printf.sprintf
"_r_%d" n
in
2302 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2303 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2306 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2307 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2309 | Ast.NoDots
-> term
2311 (* un_process_bef_aft is because we don't want to do transformation in this
2312 code, and thus don't case about braces before or after it *)
2313 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2315 Ast.WParen
(re
,n
) ->
2316 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2317 let s = guard_to_strict guard
in
2318 quantify true (get_unquantified quantified
[n
])
2319 (ctl_and s (make_raw_match None guard re
) paren_pred)
2321 statement
s Tail quantified minus_quantified label llabel slabel guard
2322 | Ast.Other_dots
d ->
2323 statement_list d Tail quantified minus_quantified
2324 label llabel slabel
true guard
2326 (* --------------------------------------------------------------------- *)
2327 (* cleanup: convert AX to EX for pdots.
2328 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2329 This is what we wanted in the first place, but it wasn't possible to make
2330 because the AX and its argument are not created in the same place.
2332 (* also cleanup XX, which is a marker for the case where the programmer
2333 specifies to change the quantifier on .... Assumed to only occur after one AX
2334 or EX, or at top level. *)
2337 let c = match c with CTL.XX
(c) -> c | _ -> c in
2339 CTL.False
-> CTL.False
2340 | CTL.True
-> CTL.True
2341 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2342 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2343 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2344 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2345 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2346 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2347 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2348 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2349 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2350 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2351 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2352 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2353 | CTL.AX
(CTL.FORWARD
,s,
2355 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2356 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2358 CTL.And
(CTL.NONSTRICT
,
2359 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2360 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2361 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2362 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2363 CTL.AX
(dir
,s,cleanup phi
)
2364 | CTL.XX
(phi
) -> failwith
"bad XX"
2365 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2366 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2367 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2368 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2369 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2370 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2371 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2372 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2373 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2374 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2375 | CTL.Ref
(s) -> CTL.Ref
(s)
2376 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2377 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2379 (* --------------------------------------------------------------------- *)
2380 (* Function declaration *)
2382 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2384 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2385 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2387 saved := Ast.get_saved t
;
2388 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2389 quantify false quantified
2390 (match Ast.unwrap t
with
2391 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2393 let unopt = elim_opt.V.rebuilder_statement stmt
in
2394 let unopt = preprocess_dots_e unopt in
2395 cleanup(statement
unopt VeryEnd
quantified [] None None None
false)
2396 | Ast.CODE
(stmt_dots
) ->
2397 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2398 let unopt = preprocess_dots unopt in
2399 let starts_with_dots =
2400 match Ast.undots stmt_dots
with
2402 (match Ast.unwrap
d with
2403 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2404 | Ast.Stars
(_,_,_,_) -> true
2407 let starts_with_brace =
2408 match Ast.undots stmt_dots
with
2410 (match Ast.unwrap
d with
2415 statement_list unopt VeryEnd
quantified [] None None None
2418 (if starts_with_dots
2420 (* EX because there is a loop on enter/top *)
2421 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2422 else if starts_with_brace
2424 ctl_and CTL.NONSTRICT
2425 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2427 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords")
2429 (* --------------------------------------------------------------------- *)
2432 let asttoctlz (name
,(_,_,exists_flag
),l)
2433 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2436 (match exists_flag
with
2437 Ast.Exists
-> exists := Exists
2438 | Ast.Forall
-> exists := Forall
2439 | Ast.Undetermined
->
2440 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2442 let (l,used_after) =
2446 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2447 (List.combine
l (List.combine
used_after positions
))) in
2449 List.map2
(top_level name
)
2450 (List.combine
used_after fresh_used_after
)
2451 (List.combine fresh_used_after_seeds
l) in
2455 let asttoctl r
used_after positions
=
2457 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2458 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2459 asttoctlz (a,b
,c) used_after positions
2460 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CTL.True
]
2462 let pp_cocci_predicate (pred
,modif
) =
2463 Pretty_print_engine.pp_predicate pred
2465 let cocci_predicate_to_string (pred
,modif
) =
2466 Pretty_print_engine.predicate_to_string pred