2 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
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.
24 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
25 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
26 * This file is part of Coccinelle.
28 * Coccinelle is free software: you can redistribute it and/or modify
29 * it under the terms of the GNU General Public License as published by
30 * the Free Software Foundation, according to version 2 of the License.
32 * Coccinelle is distributed in the hope that it will be useful,
33 * but WITHOUT ANY WARRANTY; without even the implied warranty of
34 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
35 * GNU General Public License for more details.
37 * You should have received a copy of the GNU General Public License
38 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
40 * The authors reserve the right to distribute this or future versions of
41 * Coccinelle under other licenses.
45 (* for MINUS and CONTEXT, pos is always None in this file *)
46 (*search for require*)
47 (* true = don't see all matched nodes, only modified ones *)
48 let onlyModif = ref true(*false*)
50 type ex
= Exists
| Forall
51 let exists = ref Forall
53 module Ast
= Ast_cocci
54 module V
= Visitor_ast
57 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
59 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
61 (cocci_predicate
,Ast.meta_name
, Wrapper_ctl.info
) Ast_ctl.generic_ctl
63 let union = Common.union_set
64 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
65 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
67 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
69 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
71 let used_after = ref ([] : Ast.meta_name list
)
72 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
74 let saved = ref ([] : Ast.meta_name list
)
76 let string2var x
= ("",x
)
78 (* --------------------------------------------------------------------- *)
79 (* predicates matching various nodes in the graph *)
83 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
84 | (CTL.True
,a
) | (a
,CTL.True
) -> a
89 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
90 | (CTL.False
,a
) | (a
,CTL.False
) -> a
95 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
96 | (CTL.False
,a
) | (a
,CTL.False
) -> a
101 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
102 | (CTL.False
,a
) | (a
,CTL.False
) -> a
103 | _
-> CTL.SeqOr
(x
,y
)
105 let ctl_not = function
106 CTL.True
-> CTL.False
107 | CTL.False
-> CTL.True
110 let ctl_ax s
= function
112 | CTL.False
-> CTL.False
115 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
116 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
118 let ctl_ax_absolute s
= function
120 | CTL.False
-> CTL.False
121 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
123 let ctl_ex = function
125 | CTL.False
-> CTL.False
126 | x
-> CTL.EX
(CTL.FORWARD
,x
)
128 (* This stays being AX even for sgrep_mode, because it is used to identify
129 the structure of the term, not matching the pattern. *)
130 let ctl_back_ax = function
132 | CTL.False
-> CTL.False
133 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
135 let ctl_back_ex = function
137 | CTL.False
-> CTL.False
138 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
140 let ctl_ef = function
142 | CTL.False
-> CTL.False
143 | x
-> CTL.EF
(CTL.FORWARD
,x
)
145 let ctl_ag s
= function
147 | CTL.False
-> CTL.False
148 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
151 match (x
,!exists) with
152 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
153 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
154 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
155 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
157 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
159 (match (x
,!exists) with
160 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
161 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
162 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
163 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
))
165 let ctl_uncheck = function
167 | CTL.False
-> CTL.False
170 let label_pred_maker = function
172 | Some
(label_var
,used
) ->
174 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
176 let bclabel_pred_maker = function
178 | Some
(label_var
,used
) ->
180 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
182 (* label used to be used here, but it is not used; label is only needed after
184 let predmaker guard pred label
= CTL.Pred pred
186 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
187 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
188 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
189 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
190 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
191 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
192 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
193 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
194 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
195 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
196 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
197 let loopfallpred = predmaker false (Lib_engine.LoopFallThrough
, CTL.Control
)
199 (*let aftret label_var =
200 ctl_or (aftpred label_var)
201 (ctl_or (loopfallpred label_var) (exitpred label_var))*)
207 Printf.sprintf
"r%d" cur
209 (* --------------------------------------------------------------------- *)
210 (* --------------------------------------------------------------------- *)
211 (* Eliminate OptStm *)
213 (* for optional thing with nothing after, should check that the optional thing
214 never occurs. otherwise the matching stops before it occurs *)
217 let donothing r k e
= k e
in
220 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
223 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
226 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
228 let inheritedlist l
=
229 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
232 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
235 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
237 let rec dots_list unwrapped wrapped
=
238 match (unwrapped
,wrapped
) with
241 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
243 | (Ast.Nest
(_
,_
,_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)
245 d0
::s
::d1
::rest
) -> (* why no case for nest as u? *)
246 let l = Ast.get_line stm
in
247 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
248 let new_rest2 = dots_list urest rest
in
249 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
250 varlists new_rest1 in
251 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
252 varlists new_rest2 in
256 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
258 Ast.free_vars
= fv_rest1
;
259 Ast.minus_free_vars
= mfv_rest1
;
260 Ast.fresh_vars
= fresh_rest1
;
261 Ast.inherited
= inherited_rest1
;
262 Ast.saved_witness
= s1
};
263 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
265 Ast.free_vars
= fv_rest2
;
266 Ast.minus_free_vars
= mfv_rest2
;
267 Ast.fresh_vars
= fresh_rest2
;
268 Ast.inherited
= inherited_rest2
;
269 Ast.saved_witness
= s2
}])) with
271 Ast.free_vars
= fv_rest1
;
272 Ast.minus_free_vars
= mfv_rest1
;
273 Ast.fresh_vars
= fresh_rest1
;
274 Ast.inherited
= inherited_rest1
;
275 Ast.saved_witness
= s1
}]
277 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
278 let l = Ast.get_line stm
in
279 let new_rest1 = dots_list urest rest
in
280 let new_rest2 = stm
::new_rest1 in
281 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
282 varlists new_rest1 in
283 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
284 varlists new_rest2 in
287 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
289 Ast.free_vars
= fv_rest2
;
290 Ast.minus_free_vars
= mfv_rest2
;
291 Ast.fresh_vars
= fresh_rest2
;
292 Ast.inherited
= inherited_rest2
;
293 Ast.saved_witness
= s2
};
294 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
296 Ast.free_vars
= fv_rest1
;
297 Ast.minus_free_vars
= mfv_rest1
;
298 Ast.fresh_vars
= fresh_rest1
;
299 Ast.inherited
= inherited_rest1
;
300 Ast.saved_witness
= s1
}])) with
302 Ast.free_vars
= fv_rest2
;
303 Ast.minus_free_vars
= mfv_rest2
;
304 Ast.fresh_vars
= fresh_rest2
;
305 Ast.inherited
= inherited_rest2
;
306 Ast.saved_witness
= s2
}]
308 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
309 let l = Ast.get_line stm
in
310 let fv_stm = Ast.get_fvs stm
in
311 let mfv_stm = Ast.get_mfvs stm
in
312 let fresh_stm = Ast.get_fresh stm
in
313 let inh_stm = Ast.get_inherited stm
in
314 let saved_stm = Ast.get_saved stm
in
315 let fv_d1 = Ast.get_fvs d1
in
316 let mfv_d1 = Ast.get_mfvs d1
in
317 let fresh_d1 = Ast.get_fresh d1
in
318 let inh_d1 = Ast.get_inherited d1
in
319 let saved_d1 = Ast.get_saved d1
in
320 let fv_both = Common.union_set
fv_stm fv_d1 in
321 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
322 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
323 let inh_both = Common.union_set
inh_stm inh_d1 in
324 let saved_both = Common.union_set
saved_stm saved_d1 in
328 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
330 Ast.free_vars
= fv_stm;
331 Ast.minus_free_vars
= mfv_stm;
332 Ast.fresh_vars
= fresh_stm;
333 Ast.inherited
= inh_stm;
334 Ast.saved_witness
= saved_stm};
335 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
337 Ast.free_vars
= fv_d1;
338 Ast.minus_free_vars
= mfv_d1;
339 Ast.fresh_vars
= fresh_d1;
340 Ast.inherited
= inh_d1;
341 Ast.saved_witness
= saved_d1}])) with
343 Ast.free_vars
= fv_both;
344 Ast.minus_free_vars
= mfv_both;
345 Ast.fresh_vars
= fresh_both;
346 Ast.inherited
= inh_both;
347 Ast.saved_witness
= saved_both}]
349 | ([Ast.Nest
(_
,_
,_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
350 let l = Ast.get_line stm
in
351 let rw = Ast.rewrap stm
in
352 let rwd = Ast.rewrap stm
in
353 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
355 [rwd(Ast.DOTS
([stm
]));
356 {(Ast.make_term
(Ast.DOTS
([rw dots])))
357 with Ast.node_line
= l}])]
359 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
360 | _
-> failwith
"not possible" in
362 let stmtdotsfn r k d
=
365 (match Ast.unwrap
d with
366 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
367 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
368 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
371 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
372 donothing donothing stmtdotsfn donothing
373 donothing donothing donothing donothing donothing donothing donothing
374 donothing donothing donothing donothing donothing
376 (* --------------------------------------------------------------------- *)
377 (* after management *)
378 (* We need Guard for the following case:
387 Here the inner <... b ...> should not go past foo. But foo is not the
388 "after" of the body of the outer nest, because we don't want to search for
389 it in the case where the body of the outer nest ends in something other
390 than dots or a nest. *)
392 (* what is the difference between tail and end??? *)
394 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
396 let a2n = function After x
-> Guard x
| a
-> a
399 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
400 let pp_meta (_
,x
) = Common.pp x
in
401 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
402 Format.print_newline
()
404 let print_after = function
405 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
406 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
407 | Tail
-> Printf.printf
"Tail\n"
408 | VeryEnd
-> Printf.printf
"Very End\n"
409 | End
-> Printf.printf
"End\n"
411 (* --------------------------------------------------------------------- *)
414 let fresh_var _
= string2var "_v"
415 let fresh_pos _
= string2var "_pos" (* must be a constant *)
417 let fresh_metavar _
= "_S"
419 (* fvinfo is going to end up being from the whole associated statement.
420 it would be better if it were just the free variables in d, but free_vars.ml
421 doesn't keep track of free variables on + code *)
422 let make_meta_rule_elem d fvinfo
=
423 let nm = fresh_metavar() in
424 Ast.make_meta_rule_elem nm d fvinfo
426 let get_unquantified quantified vars
=
427 List.filter
(function x
-> not
(List.mem x quantified
)) vars
429 let make_seq guard
l =
430 let s = guard_to_strict guard
in
431 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
433 let make_seq_after2 guard first rest
=
434 let s = guard_to_strict guard
in
436 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
439 let make_seq_after guard first rest
=
441 After rest
-> make_seq guard
[first
;rest
]
444 let opt_and guard first rest
=
445 let s = guard_to_strict guard
in
448 | Some first
-> ctl_and s first rest
450 let and_after guard first rest
=
451 let s = guard_to_strict guard
in
452 match rest
with After rest
-> ctl_and s first rest
| _
-> first
455 let bind x y
= x
or y
in
456 let option_default = false in
457 let mcode r
(_
,_
,kind
,metapos
) =
459 Ast.MINUS
(_
,_
,_
,_
) -> true
460 | Ast.PLUS _
-> failwith
"not possible"
461 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
462 let do_nothing r k e
= k e
in
463 let rule_elem r k re
=
465 match Ast.unwrap re
with
466 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
467 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
468 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
471 V.combiner
bind option_default
472 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
473 do_nothing do_nothing do_nothing do_nothing
474 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
475 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
476 recursor.V.combiner_rule_elem
479 let bind x y
= x
or y
in
480 let option_default = false in
481 let mcode r
(_
,_
,kind
,metapos
) =
483 Ast.MetaPos
(_
,_
,_
,_
,_
) -> true
484 | Ast.NoMetaPos
-> false in
485 let do_nothing r k e
= k e
in
486 let rule_elem r k re
=
488 match Ast.unwrap re
with
489 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
490 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
491 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
494 V.combiner
bind option_default
495 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
496 do_nothing do_nothing do_nothing do_nothing
497 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
498 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
499 recursor.V.combiner_rule_elem
501 (* code is not a DisjRuleElem *)
502 let make_match label guard code
=
503 let v = fresh_var() in
504 let matcher = Lib_engine.Match
(code
) in
505 if contains_modif code
&& not guard
506 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
508 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
509 (match (iso_info,!onlyModif,guard
,
510 intersect !used_after (Ast.get_fvs code
)) with
511 (false,true,_
,[]) | (_
,_
,true,_
) ->
512 predmaker guard
(matcher,CTL.Control
) label
513 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
515 let make_raw_match label guard code
=
516 predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
518 let rec seq_fvs quantified
= function
521 let t1fvs = get_unquantified quantified fv1
in
523 List.fold_left
Common.union_set
[]
524 (List.map
(get_unquantified quantified
) fvs
) in
525 let bothfvs = Common.inter_set
t1fvs termfvs in
526 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
527 let new_quantified = Common.union_set
bothfvs quantified
in
528 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
533 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
535 let non_saved_quantify =
537 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
539 let intersectll lst nested_list
=
540 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
542 (* --------------------------------------------------------------------- *)
543 (* Count depth of braces. The translation of a closed brace appears deeply
544 nested within the translation of the sequence term, so the name of the
545 paren var has to take into account the names of the nested braces. On the
546 other hand the close brace does not escape, so we don't have to take into
547 account other paren variable names. *)
549 (* called repetitively, which is inefficient, but less trouble than adding a
550 new field to Seq and FunDecl *)
551 let count_nested_braces s =
552 let bind x y
= max x y
in
553 let option_default = 0 in
554 let stmt_count r k
s =
555 match Ast.unwrap
s with
556 Ast.Seq
(_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
) -> (k
s) + 1
558 let donothing r k e
= k e
in
560 let recursor = V.combiner
bind option_default
561 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
562 donothing donothing donothing donothing
563 donothing donothing donothing donothing donothing donothing
564 donothing donothing stmt_count donothing donothing donothing in
565 let res = string_of_int
(recursor.V.combiner_statement
s) in
569 let get_label_ctr _
=
570 let cur = !labelctr in
572 string2var (Printf.sprintf
"l%d" cur)
574 (* --------------------------------------------------------------------- *)
575 (* annotate dots with before and after neighbors *)
577 let print_bef_aft = function
579 Printf.printf
"bef/aft\n";
580 Pretty_print_cocci.rule_elem "" re
;
581 Format.print_newline
()
583 Printf.printf
"bef/aft\n";
584 Pretty_print_cocci.statement
"" s;
585 Format.print_newline
()
586 | Ast.Other_dots
d ->
587 Printf.printf
"bef/aft\n";
588 Pretty_print_cocci.statement_dots
d;
589 Format.print_newline
()
591 (* [] can only occur if we are in a disj, where it comes from a ? In that
592 case, we want to use a, which accumulates all of the previous patterns in
594 let rec get_before_elem sl a
=
595 match Ast.unwrap sl
with
599 [] -> ([],Common.Right a
)
601 let (e
,ea
) = get_before_e e a
in
604 let (e
,ea
) = get_before_e e a
in
605 let (sl
,sla
) = loop sl ea
in
607 let (l,a
) = loop x a
in
608 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
609 | Ast.CIRCLES
(x
) -> failwith
"not supported"
610 | Ast.STARS
(x
) -> failwith
"not supported"
612 and get_before sl a
=
613 match get_before_elem sl a
with
614 (term
,Common.Left x
) -> (term
,x
)
615 | (term
,Common.Right x
) -> (term
,x
)
617 and get_before_whencode wc
=
620 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
621 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
622 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
623 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
624 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
627 and get_before_e
s a
=
628 match Ast.unwrap
s with
629 Ast.Dots
(d,w
,_
,aft
) ->
630 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
631 | Ast.Nest
(starter
,stmt_dots
,ender
,w
,multi
,_
,aft
) ->
632 let w = get_before_whencode
w in
633 let (sd
,_
) = get_before stmt_dots a
in
635 got rid of this, don't want to let nests overshoot
640 Unify_ast.unify_statement_dots
641 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
643 Unify_ast.MAYBE -> false
645 | Ast.Other_dots a ->
646 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
648 Unify_ast.MAYBE -> false
652 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,a,aft
)),
653 [Ast.Other_dots stmt_dots
])
654 | Ast.Disj
(stmt_dots_list
) ->
656 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
657 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
659 (match Ast.unwrap ast
with
660 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
661 | _
-> (s,[Ast.Other
s]))
662 | Ast.Seq
(lbrace
,body
,rbrace
) ->
663 let index = count_nested_braces s in
664 let (bd
,_
) = get_before body
[Ast.WParen
(lbrace
,index)] in
665 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),[Ast.WParen
(rbrace
,index)])
666 | Ast.Define
(header
,body
) ->
667 let (body
,_
) = get_before body
[] in
668 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
669 | Ast.IfThen
(ifheader
,branch
,aft
) ->
670 let (br
,_
) = get_before_e branch
[] in
671 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
672 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
673 let (br1
,_
) = get_before_e branch1
[] in
674 let (br2
,_
) = get_before_e branch2
[] in
675 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
676 | Ast.While
(header
,body
,aft
) ->
677 let (bd
,_
) = get_before_e body
[] in
678 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
679 | Ast.For
(header
,body
,aft
) ->
680 let (bd
,_
) = get_before_e body
[] in
681 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
682 | Ast.Do
(header
,body
,tail
) ->
683 let (bd
,_
) = get_before_e body
[] in
684 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
685 | Ast.Iterator
(header
,body
,aft
) ->
686 let (bd
,_
) = get_before_e body
[] in
687 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
688 | Ast.Switch
(header
,lb
,decls
,cases
,rb
) ->
689 let index = count_nested_braces s in
690 let (de
,dea
) = get_before decls
[Ast.WParen
(lb
,index)] in
693 (function case_line
->
694 match Ast.unwrap case_line
with
695 Ast.CaseLine
(header
,body
) ->
696 let (body
,_
) = get_before body
[] in
697 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
698 | Ast.OptCase
(case_line
) -> failwith
"not supported")
700 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),
701 [Ast.WParen
(rb
,index)])
702 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
703 let (bd
,_
) = get_before body
[] in
704 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
706 Pretty_print_cocci.statement
"" s; Format.print_newline
();
707 failwith
"get_before_e: not supported"
709 let rec get_after sl
a =
710 match Ast.unwrap sl
with
716 let (sl
,sla
) = loop sl
in
717 let (e
,ea
) = get_after_e e sla
in
719 let (l,a) = loop x
in
720 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
721 | Ast.CIRCLES
(x
) -> failwith
"not supported"
722 | Ast.STARS
(x
) -> failwith
"not supported"
724 and get_after_whencode
a wc
=
727 Ast.WhenNot
w -> let (w,_
) = get_after w a (*?*) in Ast.WhenNot
w
728 | Ast.WhenAlways
w -> let (w,_
) = get_after_e
w a in Ast.WhenAlways
w
729 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
730 | Ast.WhenNotTrue
w -> Ast.WhenNotTrue
w
731 | Ast.WhenNotFalse
w -> Ast.WhenNotFalse
w)
734 and get_after_e
s a =
735 match Ast.unwrap
s with
736 Ast.Dots
(d,w,bef
,_
) ->
737 (Ast.rewrap
s (Ast.Dots
(d,get_after_whencode
a w,bef
,a)),a)
738 | Ast.Nest
(starter
,stmt_dots
,ender
,w,multi
,bef
,_
) ->
739 let w = get_after_whencode
a w in
740 let (sd
,_
) = get_after stmt_dots
a in
742 got rid of this. don't want to let nests overshoot
747 Unify_ast.unify_statement_dots
748 (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
750 Unify_ast.MAYBE -> false
752 | Ast.Other_dots a ->
753 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
755 Unify_ast.MAYBE -> false
759 (Ast.rewrap
s (Ast.Nest
(starter
,sd
,ender
,w,multi
,bef
,a)),
760 [Ast.Other_dots stmt_dots
])
761 | Ast.Disj
(stmt_dots_list
) ->
763 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
764 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
766 (match Ast.unwrap ast
with
767 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
768 (* check "after" information for metavar optimization *)
769 (* if the error is not desired, could just return [], then
770 the optimization (check for EF) won't take place *)
774 (match Ast.unwrap x
with
775 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
777 "dots/nest not allowed before and after stmt metavar"
779 | Ast.Other_dots x
->
780 (match Ast.undots x
with
782 (match Ast.unwrap x
with
783 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
,_
,_
) ->
785 ("dots/nest not allowed before and after stmt "^
794 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
795 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
796 | _
-> (s,[Ast.Other
s]))
797 | Ast.Seq
(lbrace
,body
,rbrace
) ->
798 let index = count_nested_braces s in
799 let (bd
,_
) = get_after body
[Ast.WParen
(rbrace
,index)] in
800 (Ast.rewrap
s (Ast.Seq
(lbrace
,bd
,rbrace
)),
801 [Ast.WParen
(lbrace
,index)])
802 | Ast.Define
(header
,body
) ->
803 let (body
,_
) = get_after body
a in
804 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
805 | Ast.IfThen
(ifheader
,branch
,aft
) ->
806 let (br
,_
) = get_after_e branch
a in
807 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other
s])
808 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
809 let (br1
,_
) = get_after_e branch1
a in
810 let (br2
,_
) = get_after_e branch2
a in
811 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
812 | Ast.While
(header
,body
,aft
) ->
813 let (bd
,_
) = get_after_e body
a in
814 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
815 | Ast.For
(header
,body
,aft
) ->
816 let (bd
,_
) = get_after_e body
a in
817 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
818 | Ast.Do
(header
,body
,tail
) ->
819 let (bd
,_
) = get_after_e body
a in
820 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
821 | Ast.Iterator
(header
,body
,aft
) ->
822 let (bd
,_
) = get_after_e body
a in
823 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
824 | Ast.Switch
(header
,lb
,decls
,cases,rb
) ->
825 let index = count_nested_braces s in
828 (function case_line
->
829 match Ast.unwrap case_line
with
830 Ast.CaseLine
(header
,body
) ->
831 let (body
,_
) = get_after body
[Ast.WParen
(rb
,index)] in
832 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
833 | Ast.OptCase
(case_line
) -> failwith
"not supported")
835 let (de
,_
) = get_after decls
[] in
836 (Ast.rewrap
s (Ast.Switch
(header
,lb
,de
,cases,rb
)),[Ast.WParen
(lb
,index)])
837 | Ast.FunDecl
(header
,lbrace
,body
,rbrace
) ->
838 let (bd
,_
) = get_after body
[] in
839 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,bd
,rbrace
)),[])
840 | _
-> failwith
"get_after_e: not supported"
842 let preprocess_dots sl
=
843 let (sl
,_
) = get_before sl
[] in
844 let (sl
,_
) = get_after sl
[] in
847 let preprocess_dots_e sl
=
848 let (sl
,_
) = get_before_e sl
[] in
849 let (sl
,_
) = get_after_e sl
[] in
852 (* --------------------------------------------------------------------- *)
853 (* various return_related things *)
855 let rec ends_in_return stmt_list
=
856 match Ast.unwrap stmt_list
with
858 (match List.rev x
with
860 (match Ast.unwrap x
with
863 match Ast.unwrap x
with
864 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
865 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
868 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
871 | Ast.CIRCLES
(x
) -> failwith
"not supported"
872 | Ast.STARS
(x
) -> failwith
"not supported"
874 (* --------------------------------------------------------------------- *)
877 let exptymatch l make_match make_guard_match
=
878 let pos = fresh_pos() in
879 let matches_guard_matches =
882 let pos = Ast.make_mcode
pos in
883 (make_match (Ast.set_pos x
(Some
pos)),
884 make_guard_match
(Ast.set_pos x
(Some
pos))))
886 let (matches
,guard_matches
) = List.split
matches_guard_matches in
887 let rec suffixes = function
889 | x
::xs -> xs::(suffixes xs) in
891 (* normally, we check that an expression does not match something
892 earlier in the disjunction (calculated as prefixes). But for large
893 disjunctions, this can result in a very big CTL formula. So we
894 give the user the option to say he doesn't want this feature, if that is
896 if !Flag_matcher.no_safe_expressions
897 then List.map
(function _
-> []) matches
898 else List.rev
(suffixes (List.rev guard_matches
)) in
899 let info = (* not null *)
905 ctl_and CTL.NONSTRICT
matcher
907 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
909 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
911 (* code might be a DisjRuleElem, in which case we break it apart
912 code might contain an Exp or Ty
913 this one pushes the quantifier inwards *)
914 let do_re_matches label guard
res quantified minus_quantified
=
915 let make_guard_match x
=
916 let stmt_fvs = Ast.get_mfvs x
in
917 let fvs = get_unquantified minus_quantified
stmt_fvs in
918 non_saved_quantify fvs (make_match None
true x
) in
920 let stmt_fvs = Ast.get_fvs x
in
921 let fvs = get_unquantified quantified
stmt_fvs in
922 quantify guard
fvs (make_match None guard x
) in
923 (* label used to be used here, but it is not use; label is only needed after
925 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
926 (match List.map
Ast.unwrap
res with
927 [] -> failwith
"unexpected empty disj"
928 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
929 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
931 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
933 then failwith
"unexpected exp or ty";
934 List.fold_left
ctl_seqor CTL.False
(List.map
make_match res))
936 (* code might be a DisjRuleElem, in which case we break it apart
937 code doesn't contain an Exp or Ty
938 this one is for use when it is not practical to push the quantifier inwards
940 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
941 match Ast.unwrap code
with
942 Ast.DisjRuleElem
(res) ->
943 let make_match = make_match None guard
in
944 let orop = if guard
then ctl_or else ctl_seqor in
945 (* label used to be used here, but it is not use; label is only needed after
947 ctl_and CTL.NONSTRICT (label_pred_maker label) *)
948 (List.fold_left
orop CTL.False
(List.map
make_match res))
949 | _
-> make_match label guard code
951 (* --------------------------------------------------------------------- *)
952 (* control structures *)
954 let end_control_structure fvs header body after_pred
955 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
956 (* aft indicates what is added after the whole if, which has to be added
958 let (aft_needed
,after_branch
) =
960 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
961 (false,make_seq_after2 guard after_pred after
)
964 make_match label guard
965 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
967 make_seq_after guard after_pred
968 (After
(make_seq_after guard
match_endif after
))) in
969 let body = body after_branch
in
970 let s = guard_to_strict guard
in
975 (match (after
,aft_needed
) with
976 (After _
,_
) (* pattern doesn't end here *)
977 | (_
,true) (* + code added after *) -> after_checks
978 | _
-> no_after_checks
)
979 (ctl_ax_absolute s body)))
981 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
982 quantified minus_quantified label llabel slabel recurse
make_match guard
=
983 (* "if (test) thn" becomes:
984 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
986 "if (test) thn; after" becomes:
987 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
992 match seq_fvs quantified
993 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
994 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
995 | _
-> failwith
"not possible" in
996 let new_quantified = Common.union_set bfvs quantified
in
998 match seq_fvs minus_quantified
999 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
1000 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1001 | _
-> failwith
"not possible" in
1002 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1004 let if_header = quantify guard efvs
(make_match ifheader
) in
1005 (* then branch and after *)
1006 let lv = get_label_ctr() in
1007 let used = ref false in
1009 (* no point to put a label on truepred etc; it is local to this construct
1010 so it must have the same label *)
1012 [truepred None
; recurse branch Tail
new_quantified new_mquantified
1013 (Some
(lv,used)) llabel slabel guard
] in
1014 let after_pred = aftpred None
in
1015 let or_cases after_branch
=
1016 ctl_or true_branch (ctl_or (fallpred None
) after_branch
) in
1017 let (if_header,wrapper
) =
1020 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1021 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1022 (function body -> quantify true [lv] body))
1023 else (if_header,function x
-> x
) in
1025 (end_control_structure bfvs
if_header or_cases after_pred
1026 (Some
(ctl_ex after_pred)) None aft after label guard
)
1028 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
1029 quantified minus_quantified label llabel slabel recurse
make_match guard
=
1030 (* "if (test) thn else els" becomes:
1031 if(test) & AX((TrueBranch & AX thn) v
1032 (FalseBranch & AX (else & AX els)) v After)
1035 "if (test) thn else els; after" becomes:
1036 if(test) & AX((TrueBranch & AX thn) v
1037 (FalseBranch & AX (else & AX els)) v
1038 (After & AXAX after))
1042 (* free variables *)
1043 let (e1fvs
,b1fvs
,s1fvs
) =
1044 match seq_fvs quantified
1045 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
1046 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1047 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1048 | _
-> failwith
"not possible" in
1049 let (e2fvs
,b2fvs
,s2fvs
) =
1051 (* just combine with the else branch. no point to have separate
1052 quantifier, since there is only one possible control-flow path *)
1053 let else_fvs = Common.union_set
(Ast.get_fvs els
) (Ast.get_fvs branch2
) in
1054 match seq_fvs quantified
[Ast.get_fvs ifheader
;else_fvs;afvs
] with
1055 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1056 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1057 | _
-> failwith
"not possible" in
1058 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
1059 let exponlyfvs = intersect e1fvs e2fvs
in
1060 let new_quantified = union bothfvs quantified
in
1061 (* minus free variables *)
1062 let (me1fvs
,mb1fvs
,ms1fvs
) =
1063 match seq_fvs minus_quantified
1064 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1065 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1066 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1067 | _
-> failwith
"not possible" in
1068 let (me2fvs
,mb2fvs
,ms2fvs
) =
1070 (* just combine with the else branch. no point to have separate
1071 quantifier, since there is only one possible control-flow path *)
1073 Common.union_set
(Ast.get_mfvs els
) (Ast.get_mfvs branch2
) in
1074 match seq_fvs minus_quantified
[Ast.get_mfvs ifheader
;else_mfvs;[]] with
1075 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1076 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1077 | _
-> failwith
"not possible" in
1078 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1079 let new_mquantified = union mbothfvs minus_quantified
in
1081 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1082 (* then and else branches *)
1083 let lv = get_label_ctr() in
1084 let used = ref false in
1087 [truepred None
; recurse branch1 Tail
new_quantified new_mquantified
1088 (Some
(lv,used)) llabel slabel guard
] in
1093 (Common.minus_set
(Ast.get_fvs els
) new_quantified)
1094 (header_match None guard els
);
1095 recurse branch2 Tail
new_quantified new_mquantified
1096 (Some
(lv,used)) llabel slabel guard
] in
1097 let after_pred = aftpred None
in
1098 let or_cases after_branch
=
1099 ctl_or true_branch (ctl_or false_branch after_branch
) in
1100 let s = guard_to_strict guard
in
1101 let (if_header,wrapper
) =
1104 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1105 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1106 (function body -> quantify true [lv] body))
1107 else (if_header,function x
-> x
) in
1109 (end_control_structure bothfvs if_header or_cases after_pred
1110 (Some
(ctl_and s (ctl_ex (falsepred None
)) (ctl_ex after_pred)))
1111 (Some
(ctl_ex (falsepred None
)))
1112 aft after label guard
)
1114 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1115 quantified minus_quantified label recurse
make_match guard
=
1117 (* the translation in this case is similar to that of an if with no else *)
1118 (* free variables *)
1120 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1121 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1122 | _
-> failwith
"not possible" in
1123 let new_quantified = Common.union_set bfvs quantified
in
1124 (* minus free variables *)
1126 match seq_fvs minus_quantified
1127 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1128 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1129 | _
-> failwith
"not possible" in
1130 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1132 let header = quantify guard efvs
(make_match header) in
1133 let lv = get_label_ctr() in
1134 let used = ref false in
1138 recurse
body Tail
new_quantified new_mquantified
1139 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1140 let after_pred = loopfallpred None
in
1141 let or_cases after_branch
= ctl_or body after_branch
in
1142 let (header,wrapper
) =
1145 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1146 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1147 (function body -> quantify true [lv] body))
1148 else (header,function x
-> x
) in
1150 (end_control_structure bfvs
header or_cases after_pred
1151 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1152 match (Ast.unwrap
body,aft
) with
1153 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1154 (match Ast.unwrap re
with
1155 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1156 Type_cocci.Unitary
,_
,false)
1157 when after
= Tail
or after
= End
or after
= VeryEnd
->
1159 match seq_fvs quantified
[Ast.get_fvs
header] with
1161 | _
-> failwith
"not possible" in
1162 quantify guard efvs
(make_match header)
1166 (* --------------------------------------------------------------------- *)
1167 (* statement metavariables *)
1169 (* issue: an S metavariable that is not an if branch/loop body
1170 should not match an if branch/loop body, so check that the labels
1171 of the nodes before the first node matched by the S are different
1172 from the label of the first node matched by the S *)
1173 let sequencibility body label_pred process_bef_aft
= function
1174 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1177 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1178 | Ast.SequencibleAfterDots
l ->
1179 (* S appears after some dots. l is the code that comes after the S.
1180 want to search for that first, because S can match anything, while
1181 the stuff after is probably more restricted *)
1182 let afts = List.map process_bef_aft
l in
1183 let ors = foldl1 ctl_or afts in
1184 ctl_and CTL.NONSTRICT
1185 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1188 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1189 | Ast.NotSequencible
-> body (function x
-> x
)
1191 let svar_context_with_add_after stmt
s label quantified
d ast
1192 seqible after process_bef_aft guard fvinfo
=
1193 let label_var = (*fresh_label_var*) string2var "_lab" in
1195 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1196 (*let prelabel_pred =
1197 CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
1198 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1199 let full_metamatch = matcher d in
1200 let first_metamatch =
1203 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
,c
)) ->
1204 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
,c
))
1205 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1206 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1208 let middle_metamatch =
1211 Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
1212 | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
1214 let last_metamatch =
1217 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
,c
)) ->
1218 Ast.CONTEXT
(pos,Ast.AFTER
(aft
,c
))
1219 | Ast.CONTEXT
(_
,_
) -> d
1220 | Ast.MINUS
(_
,_
,_
,_
) | Ast.PLUS _
-> failwith
"not possible") in
1224 ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
1227 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1228 let left_or = (* the whole statement is one node *)
1229 make_seq_after guard
1230 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_ex to_end)) full_metamatch) after
in
1231 let right_or = (* the statement covers multiple nodes *)
1232 ctl_and CTL.NONSTRICT
1235 [to_end; make_seq_after guard
last_metamatch after
]))
1241 [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
1245 ctl_au CTL.NONSTRICT
1248 [ctl_and CTL.NONSTRICT last_metamatch label_pred;
1250 (ctl_not prelabel_pred) after])] in
1254 ctl_and CTL.NONSTRICT
label_pred
1255 (f
(ctl_and CTL.NONSTRICT
1256 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1257 let stmt_fvs = Ast.get_fvs stmt
in
1258 let fvs = get_unquantified quantified
stmt_fvs in
1259 quantify guard
(label_var::fvs)
1260 (sequencibility body label_pred process_bef_aft seqible
)
1262 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1263 seqible after process_bef_aft guard fvinfo
=
1264 let label_var = (*fresh_label_var*) string2var "_lab" in
1266 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1268 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1269 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1271 match (d,after
) with
1272 (Ast.PLUS _
, _
) -> failwith
"not possible"
1273 | (Ast.CONTEXT
(pos,Ast.NOTHING
),(Tail
|End
|VeryEnd
)) ->
1274 (* just match the root. don't care about label; always ok *)
1275 make_raw_match None
false ast
1276 | (Ast.CONTEXT
(pos,Ast.BEFORE
(_
,_
)),(Tail
|End
|VeryEnd
)) ->
1277 ctl_and CTL.NONSTRICT
1278 (make_raw_match None
false ast
) (* statement *)
1279 (matcher d) (* transformation *)
1280 | (Ast.CONTEXT
(pos,(Ast.NOTHING
|Ast.BEFORE
(_
,_
))),(After
a | Guard
a)) ->
1281 (* This case and the MINUS one couldprobably be merged, if
1282 HackForStmt were to notice when its arguments are trivial *)
1283 let first_metamatch = matcher d in
1284 (* try to follow after link *)
1285 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1287 ctl_ex(make_seq guard
[to_end; CTL.True
; a]) in
1289 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1290 ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1291 (ctl_and CTL.NONSTRICT
1292 first_metamatch (ctl_or is_compound not_compound))
1293 | (Ast.CONTEXT
(pos,(Ast.AFTER _
|Ast.BEFOREAFTER _
)),_
) ->
1294 failwith
"not possible"
1295 | (Ast.MINUS
(pos,inst
,adj
,l),after
) ->
1296 let (first_metamatch,last_metamatch,rest_metamatch
) =
1298 [] -> (matcher(Ast.CONTEXT
(pos,Ast.NOTHING
)),CTL.True
,matcher d)
1300 matcher(Ast.MINUS
(pos,inst
,adj
,[])),
1301 ctl_and CTL.NONSTRICT
1302 (ctl_not (make_raw_match label
false ast
))
1303 (matcher(Ast.MINUS
(pos,inst
,adj
,[])))) in
1304 (* try to follow after link *)
1305 let to_end = ctl_or (aftpred None
) (loopfallpred None
) in
1309 [to_end; make_seq_after guard
last_metamatch after
]) in
1311 make_seq_after guard
(ctl_not (ctl_ex to_end)) after
in
1312 ctl_and CTL.NONSTRICT
1313 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1314 (ctl_and CTL.NONSTRICT
1315 first_metamatch (ctl_or is_compound not_compound)))
1316 (* don't have to put anything before the beginning, so don't have to
1317 distinguish the first node. so don't have to bother about paths,
1318 just use the label. label ensures that found nodes match up with
1319 what they should because it is in the lhs of the andany. *)
1320 (CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1321 ctl_and CTL.NONSTRICT
label_pred
1322 (make_raw_match label
false ast
),
1323 ctl_and CTL.NONSTRICT rest_metamatch
prelabel_pred))
1325 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1326 let stmt_fvs = Ast.get_fvs stmt
in
1327 let fvs = get_unquantified quantified
stmt_fvs in
1328 quantify guard
(label_var::fvs)
1329 (sequencibility body label_pred process_bef_aft seqible
)
1331 (* --------------------------------------------------------------------- *)
1332 (* dots and nests *)
1334 let dots_au is_strict toend label
s wrapcode n x seq_after y quantifier
=
1335 let matchgoto = gotopred None
in
1337 make_match None
false
1339 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1341 make_match None
false
1343 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1345 if quantifier
= Exists
1346 then Common.Left
(CTL.False
)
1348 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1350 then Common.Left
(aftpred label
)
1353 (function vx
-> function v ->
1354 (* vx is the contents of the nest, if any. we can only stop early
1355 if we find neither the ending code nor the nest contents in
1356 the if branch. not sure if this is a good idea. *)
1357 let lv = get_label_ctr() in
1358 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1359 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1361 (* Rather a special case. But if the code afterwards is just
1362 a } then there is no point checking after a goto that it does
1364 (* this optimization doesn't work. probably depends on whether
1365 the destination of the break/goto is local or more global than
1367 match seq_after
with
1369 let is_paren = function
1370 CTL.Pred
(Lib_engine.Paren _
,_
) -> true
1372 is_paren e1
or is_paren e2
1374 ctl_or (aftpred label
)
1375 (quantify false [lv]
1376 (ctl_and CTL.NONSTRICT
1377 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1378 (ctl_au CTL.NONSTRICT
1379 (ctl_and CTL.NONSTRICT
(ctl_not v)
1380 (ctl_and CTL.NONSTRICT vx
preflabelpred))
1381 (ctl_and CTL.NONSTRICT
preflabelpred
1382 (if !Flag_matcher.only_return_is_error_exit
1384 (ctl_and CTL.NONSTRICT
1385 (retpred None
) (ctl_not seq_after
))
1388 (ctl_and CTL.NONSTRICT
1389 (ctl_or (retpred None
) matchcontinue)
1390 (ctl_not seq_after
))
1391 (ctl_and CTL.NONSTRICT
1392 (ctl_or matchgoto matchbreak)
1394 (* an optim that failed see defn is_paren
1395 and tests/makes_a_loop *)
1399 (ctl_not seq_after
))))))))))) in
1400 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1401 let v = get_let_ctr() in
1403 (match stop_early with
1404 Common.Left x1
-> ctl_or y x1
1405 | Common.Right
stop_early ->
1408 (ctl_and CTL.NONSTRICT
(label_pred_maker label
)
1409 (stop_early n
(CTL.Ref
v)))))
1411 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1412 process_bef_aft statement_list statement guard quantified wrapcode
=
1413 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1414 (* proces bef_aft *)
1416 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1417 let bef_aft = (* to be negated *)
1421 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1424 with Not_found
-> shortest (Common.union_set bef aft
) in
1427 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1429 let check_quantifier quant other
=
1431 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1435 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1437 then failwith
"inconsistent annotation on dots"
1441 if check_quantifier Ast.WhenExists
Ast.WhenForall
1444 if check_quantifier Ast.WhenForall
Ast.WhenExists
1447 (* the following is used when we find a goto, etc and consider accepting
1448 without finding the rest of the pattern *)
1449 let aft = shortest aft in
1450 (* process whencode *)
1451 let labelled = label_pred_maker label
in
1453 let (poswhen
,negwhen
) =
1455 (function (poswhen
,negwhen
) ->
1457 Ast.WhenNot
whencodes ->
1458 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1459 | Ast.WhenAlways stm
->
1460 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1461 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1462 | Ast.WhenNotTrue
(e
) ->
1464 ctl_or (whencond_true e label guard quantified
) negwhen
)
1465 | Ast.WhenNotFalse
(e
) ->
1467 ctl_or (whencond_false e label guard quantified
) negwhen
))
1468 (CTL.True
,CTL.False
(*bef_aft*)) (List.rev
whencodes) in
1469 (*bef_aft modifies arg so that inside of a nest can't cause the next
1470 to overshoot its boundaries, eg a() <...f()...> b() where f is
1471 a metavariable and the whole thing matches code in a loop;
1472 don't want f to match eg b(), allowing to go around the loop again*)
1473 let poswhen = ctl_and_ns arg
poswhen in
1477 (* add in After, because it's not part of the program *)
1478 ctl_or (aftpred label
) negwhen
1480 ctl_and_ns poswhen (ctl_not negwhen) in
1481 (* process dot code, if any *)
1483 match (dotcode,guard
) with
1484 (None
,_) | (_,true) -> CTL.True
1485 | (Some
dotcode,_) -> dotcode in
1486 (* process nest code, if any *)
1487 (* whencode goes in the negated part of the nest; if no nest, just goes
1488 on the "true" in between code *)
1489 let plus_var = if plus
then get_label_ctr() else string2var "" in
1490 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1491 let (ornest
,just_nest
) =
1492 (* just_nest is used when considering whether to stop early, to continue
1493 to collect nest information in the if branch *)
1494 match (nest
,guard
&& not plus
) with
1495 (None
,_) | (_,true) -> (whencodes CTL.True
,CTL.True
)
1496 | (Some nest
,false) ->
1497 let v = get_let_ctr() in
1501 (* the idea is that BindGood is sort of a witness; a witness to
1502 having found the subterm in at least one place. If there is
1503 not a witness, then there is a risk that it will get thrown
1504 away, if it is merged with a node that has an empty
1505 environment. See tests/nestplus. But this all seems
1506 rather suspicious *)
1507 CTL.And
(CTL.NONSTRICT
,x
,
1508 CTL.Exists
(true,plus_var2,
1509 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1510 CTL.Modif
plus_var2)))
1514 CTL.Or
(is_plus (CTL.Ref
v),
1515 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1517 let plus_modifier x
=
1524 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1529 (* label within dots is taken care of elsewhere. the next two lines
1530 put the label on the code following dots *)
1531 After f
-> ctl_and (guard_to_strict guard
) f
labelled
1533 (* actually, label should be None based on the only use of Guard... *)
1534 assert (label
= None
);
1535 ctl_and CTL.NONSTRICT
(ctl_uncheck f
) labelled
1537 let exit = endpred label
in
1538 let errorexit = exitpred label
in
1539 ctl_or exit errorexit
1540 (* not at all sure what the next two mean... *)
1544 Some
(lv,used) -> used := true;
1545 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1546 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1547 | None
-> endpred label
)
1548 (* was the following, but not clear why sgrep should allow
1550 let exit = endpred label in
1551 let errorexit = exitpred label in
1553 then ctl_or exit errorexit (* end anywhere *)
1554 else exit (* end at the real end of the function *) *)
in
1556 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1557 label
(guard_to_strict guard
) wrapcode just_nest
1559 (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest
) labelled))
1560 aft ender quantifier)
1562 and get_whencond_exps e
=
1563 match Ast.unwrap e
with
1565 | Ast.DisjRuleElem
(res) ->
1566 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1567 | _ -> failwith
"not possible"
1569 and make_whencond_headers e e1 label guard quantified
=
1570 let fvs = Ast.get_fvs e
in
1572 quantify guard
(get_unquantified quantified
fvs)
1573 (make_match label guard h
) in
1578 (Ast.make_mcode
"if",
1579 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1580 let while_header e1
=
1584 (Ast.make_mcode
"while",
1585 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1590 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1591 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1593 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1595 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1597 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1598 (if_headers, while_headers, for_headers)
1600 and whencond_true e label guard quantified
=
1601 let e1 = get_whencond_exps e
in
1602 let (if_headers, while_headers, for_headers) =
1603 make_whencond_headers e
e1 label guard quantified
in
1605 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1606 (ctl_and CTL.NONSTRICT
1607 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1609 and whencond_false e label guard quantified
=
1610 let e1 = get_whencond_exps e
in
1611 let (if_headers, while_headers, for_headers) =
1612 make_whencond_headers e
e1 label guard quantified
in
1613 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1614 (ctl_and CTL.NONSTRICT
(loopfallpred label
)
1615 (ctl_or (ctl_back_ex if_headers)
1616 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1618 (* --------------------------------------------------------------------- *)
1619 (* the main translation loop *)
1621 let rec statement_list stmt_list after quantified minus_quantified
1622 label llabel slabel dots_before guard
=
1624 (* include Disj to be on the safe side *)
1625 match Ast.unwrap x
with
1626 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1627 let compute_label l e db
= if db
or isdots e
then l else None
in
1628 match Ast.unwrap stmt_list
with
1630 let rec loop quantified minus_quantified dots_before label llabel slabel
1632 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1634 statement e after quantified minus_quantified
1635 (compute_label label e dots_before
)
1637 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1638 let shared = intersectll fv
fvs in
1639 let unqshared = get_unquantified quantified
shared in
1640 let new_quantified = Common.union_set
unqshared quantified
in
1641 let minus_shared = intersectll mfv mfvs
in
1643 get_unquantified minus_quantified
minus_shared in
1644 let new_mquantified =
1645 Common.union_set
munqshared minus_quantified
in
1646 quantify guard
unqshared
1649 (let (label1
,llabel1
,slabel1
) =
1650 match Ast.unwrap e
with
1652 (match Ast.unwrap re
with
1653 Ast.Goto
_ -> (None
,None
,None
)
1654 | _ -> (label
,llabel
,slabel
))
1655 | _ -> (label
,llabel
,slabel
) in
1656 loop new_quantified new_mquantified (isdots e
)
1657 label1 llabel1 slabel1
1659 new_quantified new_mquantified
1660 (compute_label label e dots_before
) llabel slabel guard
)
1661 | _ -> failwith
"not possible" in
1662 loop quantified minus_quantified dots_before
1664 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1665 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1666 | Ast.STARS
(x
) -> failwith
"not supported"
1668 (* llabel is the label of the enclosing loop and slabel is the label of the
1670 and statement stmt after quantified minus_quantified
1671 label llabel slabel guard
=
1672 let ctl_au = ctl_au CTL.NONSTRICT
in
1673 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1674 let ctl_and = ctl_and CTL.NONSTRICT
in
1675 let make_seq = make_seq guard
in
1676 let make_seq_after = make_seq_after guard
in
1677 let real_make_match = make_match in
1678 let make_match = header_match label guard
in
1680 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1683 match Ast.unwrap stmt
with
1685 (match Ast.unwrap ast
with
1686 (* the following optimisation is not a good idea, because when S
1687 is alone, we would like it not to match a declaration.
1688 this makes more matching for things like when (...) S, but perhaps
1689 that matching is not so costly anyway *)
1690 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1691 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_,_)) as d),_),
1693 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_,_)) as d),_),
1695 svar_context_with_add_after stmt
s label quantified
d ast seqible
1697 (process_bef_aft quantified minus_quantified
1698 label llabel slabel
true)
1700 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1702 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1703 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1705 (process_bef_aft quantified minus_quantified
1706 label llabel slabel
true)
1708 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1712 match Ast.unwrap ast
with
1713 Ast.DisjRuleElem
(res) ->
1714 do_re_matches label guard
res quantified minus_quantified
1715 | Ast.Exp
(_) | Ast.Ty
(_) ->
1716 let stmt_fvs = Ast.get_fvs stmt
in
1717 let fvs = get_unquantified quantified
stmt_fvs in
1718 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1720 let stmt_fvs = Ast.get_fvs stmt
in
1721 let fvs = get_unquantified quantified
stmt_fvs in
1722 quantify guard
fvs (make_match ast
) in
1723 match Ast.unwrap ast
with
1724 Ast.Break
(brk
,semi
) ->
1725 (match (llabel
,slabel
) with
1726 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1727 ctl_and term (bclabel_pred_maker slabel
)
1728 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1729 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1730 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1731 (* discard pattern that comes after return *)
1732 let normal_res = make_seq_after term after
in
1733 (* the following code tries to propagate the modifications on
1734 return; to a close brace, in the case where the final return
1737 match (retmc
,semmc
) with
1738 (Ast.MINUS
(_,inst1
,adj1
,l1
),Ast.MINUS
(_,_,_,l2
))
1739 when !Flag.sgrep_mode2
->
1740 (* in sgrep mode, we can propagate the - *)
1741 Some
(Ast.MINUS
(Ast.NoPos
,inst1
,adj1
,l1
@l2
))
1742 | (Ast.MINUS
(_,_,_,l1
),Ast.MINUS
(_,_,_,l2
)) ->
1743 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
,Ast.ONE
)))
1744 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
,c1
)),
1745 Ast.CONTEXT
(_,Ast.AFTER
(l2
,c2
))) ->
1746 (if not
(c1
= c2
) then failwith
"bad + code");
1747 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
,c1
)))
1748 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1749 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1751 | (Ast.CONTEXT
(_,Ast.NOTHING
),
1752 Ast.CONTEXT
(_,Ast.AFTER
(l,c
))) ->
1753 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l,c
)))
1755 let ret = Ast.make_mcode
"return" in
1757 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1758 let semi = Ast.make_mcode
";" in
1760 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1762 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1765 let exit = endpred None
in
1767 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1768 let stripped_rbrace =
1769 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1771 (ctl_and (make_match mod_rbrace)
1776 (ctl_or simple_return return_expr))))
1778 (make_match stripped_rbrace)
1779 (* error exit not possible; it is in the middle
1780 of code, so a return is needed *)
1783 (* some change in the middle of the return, so have to
1784 find an actual return *)
1787 (* should try to deal with the dots_bef_aft problem elsewhere,
1788 but don't have the courage... *)
1793 do_between_dots stmt
term End
1794 quantified minus_quantified label llabel slabel guard
in
1796 make_seq_after term after
)
1797 | Ast.Seq
(lbrace
,body,rbrace
) ->
1798 let (lbfvs
,b1fvs
,b2fvs
,rbfvs
) =
1801 [Ast.get_fvs lbrace
;
1802 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1804 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1805 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1806 | _ -> failwith
"not possible" in
1807 let (mlbfvs
,mb1fvs
,mb2fvs
,mrbfvs
) =
1809 seq_fvs minus_quantified
1810 [Ast.get_mfvs lbrace
;
1811 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1813 [(lbfvs
,b1fvs
);(_,b2fvs
);(rbfvs
,_)] ->
1814 (lbfvs
,b1fvs
,b2fvs
,rbfvs
)
1815 | _ -> failwith
"not possible" in
1816 let pv = count_nested_braces stmt
in
1817 let lv = get_label_ctr() in
1818 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1819 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1822 (quantify guard lbfvs
(make_match lbrace
))
1823 (ctl_and paren_pred label_pred) in
1825 match Ast.unwrap rbrace
with
1826 Ast.SeqEnd
((data
,info,_,pos)) ->
1827 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1828 | _ -> failwith
"unexpected close brace" in
1830 (* label is not needed; paren_pred is enough *)
1831 quantify guard rbfvs
1832 (ctl_au (make_match empty_rbrace)
1834 (real_make_match None guard rbrace
)
1836 let new_quantified2 =
1837 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1838 let new_mquantified2 =
1839 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1840 let pattern_as_given =
1841 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1842 quantify true [pv;lv]
1843 (quantify guard b1fvs
1847 (if !exists = Exists
then CTL.False
else (aftpred label
))
1848 (quantify guard b2fvs
1849 (statement_list body
1850 (After
(make_seq_after end_brace after
))
1851 new_quantified2 new_mquantified2
1852 (Some
(lv,ref true))
1853 llabel slabel
false guard
)))])) in
1854 if ends_in_return body
1856 (* matching error handling code *)
1858 1. The pattern as given
1859 2. A goto, and then some close braces, and then the pattern as
1860 given, but without the braces (only possible if there are no
1861 decls, and open and close braces are unmodified)
1862 3. Part of the pattern as given, then a goto, and then the rest
1863 of the pattern. For this case, we just check that all paths have
1864 a goto within the current braces. checking for a goto at every
1865 point in the pattern seems expensive and not worthwhile. *)
1867 let body = preprocess_dots body in (* redo, to drop braces *)
1871 (make_match empty_rbrace)
1872 (ctl_ax (* skip the destination label *)
1873 (quantify guard b2fvs
1874 (statement_list body End
1875 new_quantified2 new_mquantified2 None llabel slabel
1878 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1879 quantify true [pv;lv]
1880 (quantify guard b1fvs
1884 (CTL.AU
(* want AF even for sgrep *)
1885 (CTL.FORWARD
,CTL.STRICT
,
1886 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1887 ctl_and (* brace must be eventually after goto *)
1888 (gotopred (Some
(lv,ref true)))
1889 (* want AF even for sgrep *)
1890 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1891 (quantify guard b2fvs
1892 (statement_list body Tail
1893 new_quantified2 new_mquantified2
1894 None
(*no label because past the goto*)
1895 llabel slabel
false guard
))])) in
1896 ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1897 else pattern_as_given
1898 | Ast.IfThen
(ifheader
,branch
,aft) ->
1899 ifthen ifheader branch
aft after quantified minus_quantified
1900 label llabel slabel statement
make_match guard
1902 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1903 ifthenelse ifheader branch1 els branch2
aft after quantified
1904 minus_quantified label llabel slabel statement
make_match guard
1906 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1907 | Ast.Iterator
(header,body,aft) ->
1908 forwhile header body aft after quantified minus_quantified
1909 label statement
make_match guard
1911 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1912 (*ctl_and seems pointless, disjuncts see label too
1913 (label_pred_maker label)*)
1914 (List.fold_left
ctl_seqor CTL.False
1917 statement_list sl after quantified minus_quantified label
1918 llabel slabel
true guard
)
1921 | Ast.Nest
(starter
,stmt_dots
,ender,whencode
,multi
,bef
,aft) ->
1922 (* label in recursive call is None because label check is already
1923 wrapped around the corresponding code *)
1926 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1928 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1929 | _ -> failwith
"not possible" in
1931 (* no minus version because when code doesn't contain any minus code *)
1932 let new_quantified = Common.union_set
bfvs quantified
in
1935 match Ast.get_mcodekind starter
with (*ender must have the same mcode*)
1936 Ast.MINUS
(_,_,_,_) as d ->
1937 (* no need for the fresh metavar, but ... is a bit weird as a
1939 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1944 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1945 None llabel slabel
true guard
in
1946 dots_and_nests multi
1947 (Some
dots_pattern) whencode bef
aft dot_code after label
1948 (process_bef_aft
new_quantified minus_quantified
1949 None llabel slabel
true)
1951 statement_list x Tail
new_quantified minus_quantified None
1952 llabel slabel
true true)
1954 statement x Tail
new_quantified minus_quantified None
1957 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1959 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1962 Ast.MINUS
(_,_,_,_) ->
1963 (* no need for the fresh metavar, but ... is a bit weird as a
1965 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1967 dots_and_nests false None
whencodes bef
aft dot_code after label
1968 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1970 statement_list x Tail quantified minus_quantified
1971 None llabel slabel
true true)
1973 statement x Tail quantified minus_quantified None llabel slabel
true)
1975 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1977 | Ast.Switch
(header,lb
,decls
,cases,rb
) ->
1978 let rec intersect_all = function
1981 | x
::xs -> intersect x
(intersect_all xs) in
1982 let rec intersect_all2 = function (* pairwise *)
1987 (function elem
-> List.exists (List.mem elem
) xs)
1989 Common.union_set
front (intersect_all2 xs) in
1990 let rec union_all l = List.fold_left
union [] l in
1991 (* start normal variables *)
1992 let header_fvs = Ast.get_fvs
header in
1993 let lb_fvs = Ast.get_fvs lb
in
1994 let decl_fvs = union_all (List.map
Ast.get_fvs
(Ast.undots decls
)) in
1995 let case_fvs = List.map
Ast.get_fvs
cases in
1996 let rb_fvs = Ast.get_fvs rb
in
1997 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1998 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2000 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2001 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2002 function case_fvs ->
2003 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
2004 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
2005 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
2006 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
2008 | _ -> failwith
"not possible")
2009 ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
2010 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2011 all_casefvs
,all_b3fvs
,all_rbfvs
) =
2012 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
2013 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
2014 List.rev all_rbfvs
) in
2015 let exponlyfvs = intersect_all all_efvs
in
2016 let lbonlyfvs = intersect_all all_lbfvs
in
2017 (* don't do anything with right brace. Hope there is no + code on it *)
2018 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2019 let b1fvs = union_all all_b1fvs
in
2020 let new1_quantified = union b1fvs quantified
in
2022 union (union_all all_b2fvs
) (intersect_all2 all_casefvs
) in
2023 let new2_quantified = union b2fvs new1_quantified in
2024 (* let b3fvs = union_all all_b3fvs in*)
2025 (* ------------------- start minus free variables *)
2026 let header_mfvs = Ast.get_mfvs
header in
2027 let lb_mfvs = Ast.get_mfvs lb
in
2028 let decl_mfvs = union_all (List.map
Ast.get_mfvs
(Ast.undots decls
)) in
2029 let case_mfvs = List.map
Ast.get_mfvs
cases in
2030 let rb_mfvs = Ast.get_mfvs rb
in
2031 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2032 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2034 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
2035 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
2036 function case_mfvs ->
2039 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
2040 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
2041 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
2042 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
2044 | _ -> failwith
"not possible")
2045 ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
2046 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
2047 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
2048 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
2049 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
2050 List.rev all_mrbfvs
) in
2051 (* don't do anything with right brace. Hope there is no + code on it *)
2052 (* let rbonlyfvs = intersect_all all_rbfvs in*)
2053 let mb1fvs = union_all all_mb1fvs
in
2054 let new1_mquantified = union mb1fvs quantified
in
2056 union (union_all all_mb2fvs
) (intersect_all2 all_mcasefvs
) in
2057 let new2_mquantified = union mb2fvs new1_mquantified in
2058 (* let b3fvs = union_all all_b3fvs in*)
2059 (* ------------------- end collection of free variables *)
2060 let switch_header = quantify guard
exponlyfvs (make_match header) in
2061 let lb = quantify guard
lbonlyfvs (make_match lb) in
2062 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
2065 (function case_line
->
2066 match Ast.unwrap case_line
with
2067 Ast.CaseLine
(header,body) ->
2069 match seq_fvs new2_quantified [Ast.get_fvs
header] with
2070 [(e1fvs,_)] -> e1fvs
2071 | _ -> failwith
"not possible" in
2072 quantify guard
e1fvs (real_make_match label
true header)
2073 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2075 let lv = get_label_ctr() in
2076 let used = ref false in
2077 let (decls_exists_code
,decls_all_code
) =
2078 (*don't really understand this*)
2079 if (Ast.undots decls
) = []
2080 then (CTL.True
,CTL.False
)
2083 statement_list decls Tail
2084 new2_quantified new2_mquantified (Some
(lv,used)) llabel None
2089 (List.fold_left
ctl_or_fl CTL.False
2090 (List.map
ctl_uncheck
2091 (decls_all_code
::case_headers))) in
2094 (function case_line
->
2095 match Ast.unwrap case_line
with
2096 Ast.CaseLine
(header,body) ->
2097 let (e1fvs,b1fvs,s1fvs
) =
2098 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
2099 match seq_fvs new2_quantified fvs with
2100 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2101 | _ -> failwith
"not possible" in
2102 let (me1fvs
,mb1fvs,ms1fvs
) =
2103 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
2104 match seq_fvs new2_mquantified fvs with
2105 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
2106 | _ -> failwith
"not possible" in
2108 quantify guard
e1fvs (make_match header) in
2109 let new3_quantified = union b1fvs new2_quantified in
2110 let new3_mquantified = union mb1fvs new2_mquantified in
2112 statement_list body Tail
2113 new3_quantified new3_mquantified (Some
(lv,used)) llabel
2114 (Some
(lv,used)) false(*?*) guard
in
2115 quantify guard
b1fvs (make_seq [case_header; body])
2116 | Ast.OptCase
(case_line
) -> failwith
"not supported")
2118 let default_required =
2121 match Ast.unwrap case
with
2122 Ast.CaseLine
(header,_) ->
2123 (match Ast.unwrap
header with
2124 Ast.Default
(_,_) -> true
2128 then function x
-> x
2129 else function x
-> ctl_or (fallpred label
) x
in
2130 let after_pred = aftpred label
in
2131 let body after_branch
=
2134 (quantify guard
b2fvs
2137 (List.fold_left
ctl_and CTL.True
2139 (decls_exists_code
:: case_headers)));
2140 List.fold_left
ctl_or_fl no_header
2141 (decls_all_code
:: case_code)])))
2144 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
2145 match Ast.unwrap
rb with
2146 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
2147 | _ -> failwith
"not possible") in
2148 let (switch_header,wrapper
) =
2151 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
2152 (ctl_and switch_header label_pred,
2153 (function body -> quantify true [lv] body))
2154 else (switch_header,function x
-> x
) in
2156 (end_control_structure b1fvs switch_header body
2157 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
2158 | Ast.FunDecl
(header,lbrace
,body,rbrace
) ->
2159 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
) =
2162 [Ast.get_fvs
header;Ast.get_fvs lbrace
;
2163 Ast.get_fvs
body;Ast.get_fvs rbrace
]
2165 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2166 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2167 | _ -> failwith
"not possible" in
2168 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mrbfvs
) =
2171 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;
2172 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
2174 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(rbfvs
,_)] ->
2175 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,rbfvs
)
2176 | _ -> failwith
"not possible" in
2177 let function_header = quantify guard hfvs
(make_match header) in
2178 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2179 let stripped_rbrace =
2180 match Ast.unwrap rbrace
with
2181 Ast.SeqEnd
((data
,info,_,_)) ->
2182 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2183 | _ -> failwith
"unexpected close brace" in
2185 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2186 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2187 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2189 (quantify guard rbfvs
(make_match rbrace
))
2191 (* the following finds the beginning of the fake braces,
2192 if there are any, not completely sure how this works.
2193 sse the examples sw and return *)
2194 (ctl_back_ex (ctl_not fake_brace))
2195 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2196 let new_quantified3 =
2197 Common.union_set
b1fvs
2198 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2199 let new_mquantified3 =
2200 Common.union_set
mb1fvs
2201 (Common.union_set
mb2fvs
2202 (Common.union_set mb3fvs minus_quantified
)) in
2203 let not_minus = function Ast.MINUS
(_,_,_,_) -> false | _ -> true in
2205 match (Ast.undots
body,
2206 contains_modif rbrace
or contains_pos rbrace
) with
2208 (match Ast.unwrap
body with
2209 Ast.Nest
(starter
,stmt_dots
,ender,[],false,_,_)
2210 (* perhaps could optimize for minus case too... TODO *)
2211 when not_minus (Ast.get_mcodekind starter
)
2213 (* special case for function header + body - header is unambiguous
2214 and unique, so we can just look for the nested body anywhere
2218 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2219 statement_list stmt_dots
2220 (* discards match on right brace, but don't need it *)
2221 (Guard
(make_seq_after end_brace after
))
2222 new_quantified3 new_mquantified3
2223 None llabel slabel
true guard
))
2224 | Ast.Dots
((_,i
,d,_),whencode
,_,_) when
2226 (* flow sensitive, so not optimizable *)
2227 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2229 | _ -> true) whencode
) ->
2230 (* try to be more efficient for the case where the body is just
2231 ... Perhaps this is too much of a special case, but useful
2232 for dropping a parameter and checking that it is never used. *)
2234 Ast.MINUS
(_,_,_,_) -> None
2248 Ast.WhenAlways
(s) -> prev
2249 | Ast.WhenNot
(sl
) ->
2251 statement_list sl Tail
2257 | Ast.WhenNotTrue
(_)
2258 | Ast.WhenNotFalse
(_) ->
2259 failwith
"unexpected"
2261 (Ast.WhenAny
) -> CTL.False
2262 | Ast.WhenModifier
(_) -> prev
)
2263 CTL.False whencode
))
2267 Ast.WhenAlways
(s) ->
2272 label llabel slabel
true in
2274 | Ast.WhenNot
(sl
) -> prev
2275 | Ast.WhenNotTrue
(_)
2276 | Ast.WhenNotFalse
(_) ->
2277 failwith
"unexpected"
2278 | Ast.WhenModifier
(Ast.WhenAny
) ->
2280 | Ast.WhenModifier
(_) -> prev
)
2281 CTL.True whencode
) in
2282 ctl_au leftarg (make_match stripped_rbrace)]))
2286 (* function body is all minus, no whencode *)
2287 match Ast.undots
body with
2289 (match Ast.unwrap
body with
2291 ((_,i
,(Ast.MINUS
(_,_,_,[]) as d),_),[],_,_) ->
2292 (match (Ast.unwrap lbrace
,Ast.unwrap rbrace
) with
2293 (Ast.SeqStart
((_,_,Ast.MINUS
(_,_,_,[]),_)),
2294 Ast.SeqEnd
((_,_,Ast.MINUS
(_,_,_,[]),_)))
2295 when not
(contains_pos rbrace
) ->
2297 (* andany drops everything to the end, including close
2298 braces - not just function body, could check
2299 label to keep braces *)
2300 (ctl_and start_brace
2303 (CTL.FORWARD
,guard_to_strict guard
,CTL.True
,
2305 (make_meta_rule_elem d ([],[],[]))))))
2310 match (optim1,optim2) with
2316 quantify guard
b3fvs
2317 (statement_list body
2318 (After
(make_seq_after end_brace after
))
2319 new_quantified3 new_mquantified3 None llabel slabel
2321 quantify guard
b1fvs
2322 (make_seq [function_header; quantify guard
b2fvs body_code])
2323 | Ast.Define
(header,body) ->
2324 let (hfvs
,bfvs,bodyfvs
) =
2325 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2327 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2328 | _ -> failwith
"not possible" in
2329 let (mhfvs
,mbfvs
,mbodyfvs
) =
2330 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2332 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2333 | _ -> failwith
"not possible" in
2334 let define_header = quantify guard hfvs
(make_match header) in
2336 statement_list body after
2337 (Common.union_set
bfvs quantified
)
2338 (Common.union_set mbfvs minus_quantified
)
2339 None llabel slabel
true guard
in
2340 quantify guard
bfvs (make_seq [define_header; body_code])
2341 | Ast.OptStm
(stm
) ->
2342 failwith
"OptStm should have been compiled away\n"
2343 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2344 | _ -> failwith
"not supported" in
2345 if guard
or !dots_done
2348 do_between_dots stmt
term after quantified minus_quantified
2349 label llabel slabel guard
2351 (* term is the translation of stmt *)
2352 and do_between_dots stmt
term after quantified minus_quantified
2353 label llabel slabel guard
=
2354 match Ast.get_dots_bef_aft stmt
with
2355 Ast.AddingBetweenDots
(brace_term
,n
)
2356 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2358 statement brace_term after quantified minus_quantified
2359 label llabel slabel guard
in
2360 let v = Printf.sprintf
"_r_%d" n
in
2361 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2362 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2365 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2366 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2368 | Ast.NoDots
-> term
2370 (* un_process_bef_aft is because we don't want to do transformation in this
2371 code, and thus don't case about braces before or after it *)
2372 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2374 Ast.WParen
(re
,n
) ->
2375 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2376 let s = guard_to_strict guard
in
2377 quantify true (get_unquantified quantified
[n
])
2378 (ctl_and s (make_raw_match None guard re
) paren_pred)
2380 statement
s Tail quantified minus_quantified label llabel slabel guard
2381 | Ast.Other_dots
d ->
2382 statement_list d Tail quantified minus_quantified
2383 label llabel slabel
true guard
2385 (* --------------------------------------------------------------------- *)
2386 (* cleanup: convert AX to EX for pdots.
2387 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2388 This is what we wanted in the first place, but it wasn't possible to make
2389 because the AX and its argument are not created in the same place.
2391 (* also cleanup XX, which is a marker for the case where the programmer
2392 specifies to change the quantifier on .... Assumed to only occur after one AX
2393 or EX, or at top level. *)
2396 let c = match c with CTL.XX
(c) -> c | _ -> c in
2398 CTL.False
-> CTL.False
2399 | CTL.True
-> CTL.True
2400 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2401 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2402 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2403 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2404 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2405 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2406 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2407 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2408 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2409 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2410 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2411 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2412 | CTL.AX
(CTL.FORWARD
,s,
2414 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2415 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2417 CTL.And
(CTL.NONSTRICT
,
2418 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2419 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2420 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2421 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2422 CTL.AX
(dir
,s,cleanup phi
)
2423 | CTL.XX
(phi
) -> failwith
"bad XX"
2424 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2425 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2426 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2427 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2428 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2429 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2430 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2431 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2432 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2433 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2434 | CTL.Ref
(s) -> CTL.Ref
(s)
2435 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2436 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2438 (* --------------------------------------------------------------------- *)
2439 (* Function declaration *)
2441 (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2443 let top_level name
((ua
,pos),fua
) (fuas
,t
) =
2444 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2446 saved := Ast.get_saved t
;
2447 let quantified = Common.minus_set
(Common.union_set
ua fuas
) pos in
2448 quantify false quantified
2449 (match Ast.unwrap t
with
2450 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2452 let unopt = elim_opt.V.rebuilder_statement stmt
in
2453 let unopt = preprocess_dots_e unopt in
2454 cleanup(statement
unopt VeryEnd
quantified [] None None None
false)
2455 | Ast.CODE
(stmt_dots
) ->
2456 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2457 let unopt = preprocess_dots unopt in
2458 let starts_with_dots =
2459 match Ast.undots stmt_dots
with
2461 (match Ast.unwrap
d with
2462 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2463 | Ast.Stars
(_,_,_,_) -> true
2466 let starts_with_brace =
2467 match Ast.undots stmt_dots
with
2469 (match Ast.unwrap
d with
2474 statement_list unopt VeryEnd
quantified [] None None None
2477 (if starts_with_dots
2479 (* EX because there is a loop on enter/top *)
2480 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2481 else if starts_with_brace
2483 ctl_and CTL.NONSTRICT
2484 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2486 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords")
2488 (* --------------------------------------------------------------------- *)
2491 let asttoctlz (name
,(_,_,exists_flag
),l)
2492 (used_after,fresh_used_after
,fresh_used_after_seeds
) positions
=
2495 (match exists_flag
with
2496 Ast.Exists
-> exists := Exists
2497 | Ast.Forall
-> exists := Forall
2498 | Ast.Undetermined
->
2499 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2501 let (l,used_after) =
2505 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2506 (List.combine
l (List.combine
used_after positions
))) in
2508 List.map2
(top_level name
)
2509 (List.combine
used_after fresh_used_after
)
2510 (List.combine fresh_used_after_seeds
l) in
2514 let asttoctl r
used_after positions
=
2516 Ast.ScriptRule
_ | Ast.InitialScriptRule
_ | Ast.FinalScriptRule
_ -> []
2517 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Normal
) ->
2518 asttoctlz (a,b
,c) used_after positions
2519 | Ast.CocciRule
(a,b
,c,_,Ast_cocci.Generated
) -> [CTL.True
]
2521 let pp_cocci_predicate (pred
,modif
) =
2522 Pretty_print_engine.pp_predicate pred
2524 let cocci_predicate_to_string (pred
,modif
) =
2525 Pretty_print_engine.predicate_to_string pred