2 * Copyright 2005-2008, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
23 (* for MINUS and CONTEXT, pos is always None in this file *)
24 (*search for require*)
25 (* true = don't see all matched nodes, only modified ones *)
26 let onlyModif = ref true(*false*)
28 type ex
= Exists
| Forall
| ReverseForall
29 let exists = ref Forall
31 module Ast
= Ast_cocci
32 module V
= Visitor_ast
35 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
37 type cocci_predicate
= Lib_engine.predicate
* Ast.meta_name
Ast_ctl.modif
39 (cocci_predicate
,Ast.meta_name
, Wrapper_ctl.info
) Ast_ctl.generic_ctl
41 let union = Common.union_set
42 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
43 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
45 let foldl1 f xs
= List.fold_left f
(List.hd xs
) (List.tl xs
)
47 let xs = List.rev
xs in List.fold_left f
(List.hd
xs) (List.tl
xs)
49 let used_after = ref ([] : Ast.meta_name list
)
50 let guard_to_strict guard
= if guard
then CTL.NONSTRICT
else CTL.STRICT
52 let saved = ref ([] : Ast.meta_name list
)
54 let string2var x
= ("",x
)
56 (* --------------------------------------------------------------------- *)
57 (* predicates matching various nodes in the graph *)
61 (CTL.False
,_
) | (_
,CTL.False
) -> CTL.False
62 | (CTL.True
,a
) | (a
,CTL.True
) -> a
67 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
68 | (CTL.False
,a
) | (a
,CTL.False
) -> a
73 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
74 | (CTL.False
,a
) | (a
,CTL.False
) -> a
79 (CTL.True
,_
) | (_
,CTL.True
) -> CTL.True
80 | (CTL.False
,a
) | (a
,CTL.False
) -> a
83 let ctl_not = function
85 | CTL.False
-> CTL.True
88 let ctl_ax s
= function
90 | CTL.False
-> CTL.False
93 Exists
-> CTL.EX
(CTL.FORWARD
,x
)
94 | Forall
-> CTL.AX
(CTL.FORWARD
,s
,x
)
95 | ReverseForall
-> failwith
"not supported"
97 let ctl_ax_absolute s
= function
99 | CTL.False
-> CTL.False
100 | x
-> CTL.AX
(CTL.FORWARD
,s
,x
)
102 let ctl_ex = function
104 | CTL.False
-> CTL.False
105 | x
-> CTL.EX
(CTL.FORWARD
,x
)
107 (* This stays being AX even for sgrep_mode, because it is used to identify
108 the structure of the term, not matching the pattern. *)
109 let ctl_back_ax = function
111 | CTL.False
-> CTL.False
112 | x
-> CTL.AX
(CTL.BACKWARD
,CTL.NONSTRICT
,x
)
114 let ctl_back_ex = function
116 | CTL.False
-> CTL.False
117 | x
-> CTL.EX
(CTL.BACKWARD
,x
)
119 let ctl_ef = function
121 | CTL.False
-> CTL.False
122 | x
-> CTL.EF
(CTL.FORWARD
,x
)
124 let ctl_ag s
= function
126 | CTL.False
-> CTL.False
127 | x
-> CTL.AG
(CTL.FORWARD
,s
,x
)
130 match (x
,!exists) with
131 (CTL.True
,Exists
) -> CTL.EF
(CTL.FORWARD
,y
)
132 | (CTL.True
,Forall
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
133 | (CTL.True
,ReverseForall
) -> failwith
"not supported"
134 | (_
,Exists
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
135 | (_
,Forall
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
136 | (_
,ReverseForall
) -> failwith
"not supported"
138 let ctl_anti_au s x y
= (* only for ..., where the quantifier is changed *)
140 (match (x
,!exists) with
141 (CTL.True
,Exists
) -> CTL.AF
(CTL.FORWARD
,s
,y
)
142 | (CTL.True
,Forall
) -> CTL.EF
(CTL.FORWARD
,y
)
143 | (CTL.True
,ReverseForall
) -> failwith
"not supported"
144 | (_
,Exists
) -> CTL.AU
(CTL.FORWARD
,s
,x
,y
)
145 | (_
,Forall
) -> CTL.EU
(CTL.FORWARD
,x
,y
)
146 | (_
,ReverseForall
) -> failwith
"not supported")
148 let ctl_uncheck = function
150 | CTL.False
-> CTL.False
153 let label_pred_maker = function
155 | Some
(label_var
,used
) ->
157 CTL.Pred
(Lib_engine.PrefixLabel
(label_var
),CTL.Control
)
159 let bclabel_pred_maker = function
161 | Some
(label_var
,used
) ->
163 CTL.Pred
(Lib_engine.BCLabel
(label_var
),CTL.Control
)
165 let predmaker guard pred label
=
166 ctl_and (guard_to_strict guard
) (CTL.Pred pred
) (label_pred_maker label
)
168 let aftpred = predmaker false (Lib_engine.After
, CTL.Control
)
169 let retpred = predmaker false (Lib_engine.Return
, CTL.Control
)
170 let funpred = predmaker false (Lib_engine.FunHeader
, CTL.Control
)
171 let toppred = predmaker false (Lib_engine.Top
, CTL.Control
)
172 let exitpred = predmaker false (Lib_engine.ErrorExit
, CTL.Control
)
173 let endpred = predmaker false (Lib_engine.Exit
, CTL.Control
)
174 let gotopred = predmaker false (Lib_engine.Goto
, CTL.Control
)
175 let inlooppred = predmaker false (Lib_engine.InLoop
, CTL.Control
)
176 let truepred = predmaker false (Lib_engine.TrueBranch
, CTL.Control
)
177 let falsepred = predmaker false (Lib_engine.FalseBranch
, CTL.Control
)
178 let fallpred = predmaker false (Lib_engine.FallThrough
, CTL.Control
)
180 let aftret label_var f
= ctl_or (aftpred label_var
) (exitpred label_var
)
186 Printf.sprintf
"r%d" cur
188 (* --------------------------------------------------------------------- *)
189 (* --------------------------------------------------------------------- *)
190 (* Eliminate OptStm *)
192 (* for optional thing with nothing after, should check that the optional thing
193 never occurs. otherwise the matching stops before it occurs *)
196 let donothing r k e
= k e
in
199 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
202 List.fold_left
Common.union_set
[] (List.map
Ast.get_mfvs l
) in
205 List.fold_left
Common.union_set
[] (List.map
Ast.get_fresh l
) in
207 let inheritedlist l
=
208 List.fold_left
Common.union_set
[] (List.map
Ast.get_inherited l
) in
211 List.fold_left
Common.union_set
[] (List.map
Ast.get_saved l
) in
214 (fvlist l
, mfvlist l
, freshlist l
, inheritedlist l
, savedlist l
) in
216 let rec dots_list unwrapped wrapped
=
217 match (unwrapped
,wrapped
) with
220 | (Ast.Dots
(_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
222 | (Ast.Nest
(_
,_
,_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
,_
) as u
)::urest
,
224 let l = Ast.get_line stm
in
225 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
226 let new_rest2 = dots_list urest rest
in
227 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
228 varlists new_rest1 in
229 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
230 varlists new_rest2 in
234 [{(Ast.make_term
(Ast.DOTS
(new_rest1))) with
236 Ast.free_vars
= fv_rest1
;
237 Ast.minus_free_vars
= mfv_rest1
;
238 Ast.fresh_vars
= fresh_rest1
;
239 Ast.inherited
= inherited_rest1
;
240 Ast.saved_witness
= s1
};
241 {(Ast.make_term
(Ast.DOTS
(new_rest2))) with
243 Ast.free_vars
= fv_rest2
;
244 Ast.minus_free_vars
= mfv_rest2
;
245 Ast.fresh_vars
= fresh_rest2
;
246 Ast.inherited
= inherited_rest2
;
247 Ast.saved_witness
= s2
}])) with
249 Ast.free_vars
= fv_rest1
;
250 Ast.minus_free_vars
= mfv_rest1
;
251 Ast.fresh_vars
= fresh_rest1
;
252 Ast.inherited
= inherited_rest1
;
253 Ast.saved_witness
= s1
}]
255 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
256 let l = Ast.get_line stm
in
257 let new_rest1 = dots_list urest rest
in
258 let new_rest2 = stm
::new_rest1 in
259 let (fv_rest1
,mfv_rest1
,fresh_rest1
,inherited_rest1
,s1
) =
260 varlists new_rest1 in
261 let (fv_rest2
,mfv_rest2
,fresh_rest2
,inherited_rest2
,s2
) =
262 varlists new_rest2 in
265 [{(Ast.make_term
(Ast.DOTS
(new_rest2))) with
267 Ast.free_vars
= fv_rest2
;
268 Ast.minus_free_vars
= mfv_rest2
;
269 Ast.fresh_vars
= fresh_rest2
;
270 Ast.inherited
= inherited_rest2
;
271 Ast.saved_witness
= s2
};
272 {(Ast.make_term
(Ast.DOTS
(new_rest1))) with
274 Ast.free_vars
= fv_rest1
;
275 Ast.minus_free_vars
= mfv_rest1
;
276 Ast.fresh_vars
= fresh_rest1
;
277 Ast.inherited
= inherited_rest1
;
278 Ast.saved_witness
= s1
}])) with
280 Ast.free_vars
= fv_rest2
;
281 Ast.minus_free_vars
= mfv_rest2
;
282 Ast.fresh_vars
= fresh_rest2
;
283 Ast.inherited
= inherited_rest2
;
284 Ast.saved_witness
= s2
}]
286 | ([Ast.Dots
(_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
287 let l = Ast.get_line stm
in
288 let fv_stm = Ast.get_fvs stm
in
289 let mfv_stm = Ast.get_mfvs stm
in
290 let fresh_stm = Ast.get_fresh stm
in
291 let inh_stm = Ast.get_inherited stm
in
292 let saved_stm = Ast.get_saved stm
in
293 let fv_d1 = Ast.get_fvs d1
in
294 let mfv_d1 = Ast.get_mfvs d1
in
295 let fresh_d1 = Ast.get_fresh d1
in
296 let inh_d1 = Ast.get_inherited d1
in
297 let saved_d1 = Ast.get_saved d1
in
298 let fv_both = Common.union_set
fv_stm fv_d1 in
299 let mfv_both = Common.union_set
mfv_stm mfv_d1 in
300 let fresh_both = Common.union_set
fresh_stm fresh_d1 in
301 let inh_both = Common.union_set
inh_stm inh_d1 in
302 let saved_both = Common.union_set
saved_stm saved_d1 in
306 [{(Ast.make_term
(Ast.DOTS
([stm
]))) with
308 Ast.free_vars
= fv_stm;
309 Ast.minus_free_vars
= mfv_stm;
310 Ast.fresh_vars
= fresh_stm;
311 Ast.inherited
= inh_stm;
312 Ast.saved_witness
= saved_stm};
313 {(Ast.make_term
(Ast.DOTS
([d1
]))) with
315 Ast.free_vars
= fv_d1;
316 Ast.minus_free_vars
= mfv_d1;
317 Ast.fresh_vars
= fresh_d1;
318 Ast.inherited
= inh_d1;
319 Ast.saved_witness
= saved_d1}])) with
321 Ast.free_vars
= fv_both;
322 Ast.minus_free_vars
= mfv_both;
323 Ast.fresh_vars
= fresh_both;
324 Ast.inherited
= inh_both;
325 Ast.saved_witness
= saved_both}]
327 | ([Ast.Nest
(_
,_
,_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
328 let l = Ast.get_line stm
in
329 let rw = Ast.rewrap stm
in
330 let rwd = Ast.rewrap stm
in
331 let dots = Ast.Dots
(Ast.make_mcode
"...",[],[],[]) in
333 [rwd(Ast.DOTS
([stm
]));
334 {(Ast.make_term
(Ast.DOTS
([rw dots])))
335 with Ast.node_line
= l}])]
337 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
338 | _
-> failwith
"not possible" in
340 let stmtdotsfn r k d
=
343 (match Ast.unwrap
d with
344 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
345 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
346 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
349 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
351 donothing donothing stmtdotsfn donothing
352 donothing donothing donothing donothing donothing donothing donothing
353 donothing donothing donothing donothing donothing
355 (* --------------------------------------------------------------------- *)
356 (* after management *)
357 (* We need Guard for the following case:
366 Here the inner <... b ...> should not go past foo. But foo is not the
367 "after" of the body of the outer nest, because we don't want to search for
368 it in the case where the body of the outer nest ends in something other
369 than dots or a nest. *)
371 (* what is the difference between tail and end??? *)
373 type after
= After
of formula
| Guard
of formula
| Tail
| End
| VeryEnd
375 let a2n = function After x
-> Guard x
| a
-> a
378 let pp_pred (x
,_
) = Pretty_print_engine.pp_predicate x
in
379 let pp_meta (_
,x
) = Common.pp x
in
380 Pretty_print_ctl.pp_ctl
(pp_pred,pp_meta) false x
;
381 Format.print_newline
()
383 let print_after = function
384 After ctl
-> Printf.printf
"After:\n"; print_ctl ctl
385 | Guard ctl
-> Printf.printf
"Guard:\n"; print_ctl ctl
386 | Tail
-> Printf.printf
"Tail\n"
387 | VeryEnd
-> Printf.printf
"Very End\n"
388 | End
-> Printf.printf
"End\n"
390 (* --------------------------------------------------------------------- *)
393 let fresh_var _
= string2var "_v"
394 let fresh_pos _
= string2var "_pos" (* must be a constant *)
396 let fresh_metavar _
= "_S"
398 (* fvinfo is going to end up being from the whole associated statement.
399 it would be better if it were just the free variables in d, but free_vars.ml
400 doesn't keep track of free variables on + code *)
401 let make_meta_rule_elem d fvinfo
=
402 let nm = fresh_metavar() in
403 Ast.make_meta_rule_elem nm d fvinfo
405 let get_unquantified quantified vars
=
406 List.filter
(function x
-> not
(List.mem x quantified
)) vars
408 let make_seq guard
l =
409 let s = guard_to_strict guard
in
410 foldr1 (function rest
-> function cur -> ctl_and s cur (ctl_ax s rest
)) l
412 let make_seq_after2 guard first rest
=
413 let s = guard_to_strict guard
in
415 After rest
-> ctl_and s first
(ctl_ax s (ctl_ax s rest
))
418 let make_seq_after guard first rest
=
420 After rest
-> make_seq guard
[first
;rest
]
423 let opt_and guard first rest
=
424 let s = guard_to_strict guard
in
427 | Some first
-> ctl_and s first rest
429 let and_after guard first rest
=
430 let s = guard_to_strict guard
in
431 match rest
with After rest
-> ctl_and s first rest
| _
-> first
434 let bind x y
= x
or y
in
435 let option_default = false in
436 let mcode r
(_
,_
,kind
,_
) =
438 Ast.MINUS
(_
,_
) -> true
439 | Ast.PLUS
-> failwith
"not possible"
440 | Ast.CONTEXT
(_
,info
) -> not
(info
= Ast.NOTHING
) in
441 let do_nothing r k e
= k e
in
442 let rule_elem r k re
=
444 match Ast.unwrap re
with
445 Ast.FunHeader
(bef
,_
,fninfo
,name
,lp
,params
,rp
) ->
446 bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
447 | Ast.Decl
(bef
,_
,decl
) -> bind (mcode r
((),(),bef
,Ast.NoMetaPos
)) res
450 V.combiner
bind option_default
451 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
453 do_nothing do_nothing do_nothing do_nothing
454 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
455 do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
456 recursor.V.combiner_rule_elem
458 (* code is not a DisjRuleElem *)
459 let make_match label guard code
=
460 let v = fresh_var() in
461 let matcher = Lib_engine.Match
(code
) in
462 if contains_modif code
&& not guard
463 then CTL.Exists
(true,v,predmaker guard
(matcher,CTL.Modif
v) label
)
465 let iso_info = !Flag.track_iso_usage
&& not
(Ast.get_isos code
= []) in
466 (match (iso_info,!onlyModif,guard
,
467 intersect !used_after (Ast.get_fvs code
)) with
468 (false,true,_
,[]) | (_
,_
,true,_
) ->
469 predmaker guard
(matcher,CTL.Control
) label
470 | _
-> CTL.Exists
(true,v,predmaker guard
(matcher,CTL.UnModif
v) label
))
472 let make_raw_match label guard code
=
473 predmaker guard
(Lib_engine.Match
(code
),CTL.Control
) label
475 let rec seq_fvs quantified
= function
478 let t1fvs = get_unquantified quantified fv1
in
480 List.fold_left
Common.union_set
[]
481 (List.map
(get_unquantified quantified
) fvs
) in
482 let bothfvs = Common.inter_set
t1fvs termfvs in
483 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
484 let new_quantified = Common.union_set
bothfvs quantified
in
485 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
490 function code
-> CTL.Exists
(not guard
&& List.mem
cur !saved,cur,code
))
492 let non_saved_quantify =
494 (function cur -> function code
-> CTL.Exists
(false,cur,code
))
496 let intersectll lst nested_list
=
497 List.filter
(function x
-> List.exists (List.mem x
) nested_list
) lst
499 (* --------------------------------------------------------------------- *)
500 (* Count depth of braces. The translation of a closed brace appears deeply
501 nested within the translation of the sequence term, so the name of the
502 paren var has to take into account the names of the nested braces. On the
503 other hand the close brace does not escape, so we don't have to take into
504 account other paren variable names. *)
506 (* called repetitively, which is inefficient, but less trouble than adding a
507 new field to Seq and FunDecl *)
508 let count_nested_braces s =
509 let bind x y
= max x y
in
510 let option_default = 0 in
511 let stmt_count r k
s =
512 match Ast.unwrap
s with
513 Ast.Seq
(_
,_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
,_
) -> (k
s) + 1
515 let donothing r k e
= k e
in
517 let recursor = V.combiner
bind option_default
518 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
520 donothing donothing donothing donothing
521 donothing donothing donothing donothing donothing donothing
522 donothing donothing stmt_count donothing donothing donothing in
523 let res = string_of_int
(recursor.V.combiner_statement
s) in
527 let get_label_ctr _
=
528 let cur = !labelctr in
530 string2var (Printf.sprintf
"l%d" cur)
532 (* --------------------------------------------------------------------- *)
533 (* annotate dots with before and after neighbors *)
535 let print_bef_aft = function
537 Printf.printf
"bef/aft\n";
538 Pretty_print_cocci.rule_elem "" re
;
539 Format.print_newline
()
541 Printf.printf
"bef/aft\n";
542 Pretty_print_cocci.statement
"" s;
543 Format.print_newline
()
544 | Ast.Other_dots
d ->
545 Printf.printf
"bef/aft\n";
546 Pretty_print_cocci.statement_dots
d;
547 Format.print_newline
()
549 (* [] can only occur if we are in a disj, where it comes from a ? In that
550 case, we want to use a, which accumulates all of the previous patterns in
552 let rec get_before_elem sl a
=
553 match Ast.unwrap sl
with
557 [] -> ([],Common.Right a
)
559 let (e
,ea
) = get_before_e e a
in
562 let (e
,ea
) = get_before_e e a
in
563 let (sl
,sla
) = loop sl ea
in
565 let (l,a
) = loop x a
in
566 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
567 | Ast.CIRCLES
(x
) -> failwith
"not supported"
568 | Ast.STARS
(x
) -> failwith
"not supported"
570 and get_before sl a
=
571 match get_before_elem sl a
with
572 (term
,Common.Left x
) -> (term
,x
)
573 | (term
,Common.Right x
) -> (term
,x
)
575 and get_before_whencode wc
=
578 Ast.WhenNot w
-> let (w
,_
) = get_before w
[] in Ast.WhenNot w
579 | Ast.WhenAlways w
-> let (w
,_
) = get_before_e w
[] in Ast.WhenAlways w
580 | Ast.WhenModifier
(x
) -> Ast.WhenModifier
(x
)
581 | Ast.WhenNotTrue w
-> Ast.WhenNotTrue w
582 | Ast.WhenNotFalse w
-> Ast.WhenNotFalse w
)
585 and get_before_e
s a
=
586 match Ast.unwrap
s with
587 Ast.Dots
(d,w
,_
,aft
) ->
588 (Ast.rewrap
s (Ast.Dots
(d,get_before_whencode w
,a
,aft
)),a
)
589 | Ast.Nest
(stmt_dots
,w
,multi
,_
,aft
) ->
590 let w = get_before_whencode
w in
591 let (sd
,_
) = get_before stmt_dots a
in
597 Unify_ast.unify_statement_dots
598 (Ast.rewrap
s (Ast.DOTS
([a]))) stmt_dots
in
600 Unify_ast.MAYBE
-> false
602 | Ast.Other_dots
a ->
603 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
605 Unify_ast.MAYBE
-> false
609 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,a,aft
)),[Ast.Other_dots stmt_dots
])
610 | Ast.Disj
(stmt_dots_list
) ->
612 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
613 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
615 (match Ast.unwrap ast
with
616 Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
617 | _
-> (s,[Ast.Other
s]))
618 | Ast.Seq
(lbrace
,decls
,body
,rbrace
) ->
619 let index = count_nested_braces s in
620 let (de
,dea
) = get_before decls
[Ast.WParen
(lbrace
,index)] in
621 let (bd
,_
) = get_before body dea
in
622 (Ast.rewrap
s (Ast.Seq
(lbrace
,de
,bd
,rbrace
)),
623 [Ast.WParen
(rbrace
,index)])
624 | Ast.Define
(header
,body
) ->
625 let (body
,_
) = get_before body
[] in
626 (Ast.rewrap
s (Ast.Define
(header
,body
)), [Ast.Other
s])
627 | Ast.IfThen
(ifheader
,branch
,aft
) ->
628 let (br
,_
) = get_before_e branch
[] in
629 (Ast.rewrap
s (Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other
s])
630 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
631 let (br1
,_
) = get_before_e branch1
[] in
632 let (br2
,_
) = get_before_e branch2
[] in
633 (Ast.rewrap
s (Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other
s])
634 | Ast.While
(header
,body
,aft
) ->
635 let (bd
,_
) = get_before_e body
[] in
636 (Ast.rewrap
s (Ast.While
(header
,bd
,aft
)),[Ast.Other
s])
637 | Ast.For
(header
,body
,aft
) ->
638 let (bd
,_
) = get_before_e body
[] in
639 (Ast.rewrap
s (Ast.For
(header
,bd
,aft
)),[Ast.Other
s])
640 | Ast.Do
(header
,body
,tail
) ->
641 let (bd
,_
) = get_before_e body
[] in
642 (Ast.rewrap
s (Ast.Do
(header
,bd
,tail
)),[Ast.Other
s])
643 | Ast.Iterator
(header
,body
,aft
) ->
644 let (bd
,_
) = get_before_e body
[] in
645 (Ast.rewrap
s (Ast.Iterator
(header
,bd
,aft
)),[Ast.Other
s])
646 | Ast.Switch
(header
,lb
,cases
,rb
) ->
649 (function case_line
->
650 match Ast.unwrap case_line
with
651 Ast.CaseLine
(header
,body
) ->
652 let (body
,_
) = get_before body
[] in
653 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
654 | Ast.OptCase
(case_line
) -> failwith
"not supported")
656 (Ast.rewrap
s (Ast.Switch
(header
,lb
,cases,rb
)),[Ast.Other
s])
657 | Ast.FunDecl
(header
,lbrace
,decls
,body
,rbrace
) ->
658 let (de
,dea
) = get_before decls
[] in
659 let (bd
,_
) = get_before body dea
in
660 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,de
,bd
,rbrace
)),[])
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
700 Unify_ast.unify_statement_dots
701 (Ast.rewrap
s (Ast.DOTS
([a]))) stmt_dots
in
703 Unify_ast.MAYBE
-> false
705 | Ast.Other_dots
a ->
706 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
708 Unify_ast.MAYBE
-> false
712 (Ast.rewrap
s (Ast.Nest
(sd
,w,multi
,bef
,a)),[Ast.Other_dots stmt_dots
])
713 | Ast.Disj
(stmt_dots_list
) ->
715 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
716 (Ast.rewrap
s (Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
718 (match Ast.unwrap ast
with
719 Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots _
,i
) ->
720 (* check "after" information for metavar optimization *)
721 (* if the error is not desired, could just return [], then
722 the optimization (check for EF) won't take place *)
726 (match Ast.unwrap x
with
727 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
729 "dots/nest not allowed before and after stmt metavar"
731 | Ast.Other_dots x
->
732 (match Ast.undots x
with
734 (match Ast.unwrap x
with
735 Ast.Dots
(_
,_
,_
,_
) | Ast.Nest
(_
,_
,_
,_
,_
) ->
737 ("dots/nest not allowed before and after stmt "^
746 (Ast.MetaStmt
(nm,keep
,Ast.SequencibleAfterDots
a,i
)))),[])
747 | Ast.MetaStmt
(_
,_
,_
,_
) -> (s,[])
748 | _
-> (s,[Ast.Other
s]))
749 | Ast.Seq
(lbrace
,decls
,body
,rbrace
) ->
750 let index = count_nested_braces s in
751 let (bd
,bda
) = get_after body
[Ast.WParen
(rbrace
,index)] in
752 let (de
,_
) = get_after decls bda
in
753 (Ast.rewrap
s (Ast.Seq
(lbrace
,de
,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
,cases,rb
) ->
780 (function case_line
->
781 match Ast.unwrap case_line
with
782 Ast.CaseLine
(header
,body
) ->
783 let (body
,_
) = get_after body
[] in
784 Ast.rewrap case_line
(Ast.CaseLine
(header
,body
))
785 | Ast.OptCase
(case_line
) -> failwith
"not supported")
787 (Ast.rewrap
s (Ast.Switch
(header
,lb
,cases,rb
)),[Ast.Other
s])
788 | Ast.FunDecl
(header
,lbrace
,decls
,body
,rbrace
) ->
789 let (bd
,bda
) = get_after body
[] in
790 let (de
,_
) = get_after decls bda
in
791 (Ast.rewrap
s (Ast.FunDecl
(header
,lbrace
,de
,bd
,rbrace
)),[])
792 | _
-> failwith
"get_after_e: not supported"
794 let preprocess_dots sl
=
795 let (sl
,_
) = get_before sl
[] in
796 let (sl
,_
) = get_after sl
[] in
799 let preprocess_dots_e sl
=
800 let (sl
,_
) = get_before_e sl
[] in
801 let (sl
,_
) = get_after_e sl
[] in
804 (* --------------------------------------------------------------------- *)
805 (* various return_related things *)
807 let rec ends_in_return stmt_list
=
808 match Ast.unwrap stmt_list
with
810 (match List.rev x
with
812 (match Ast.unwrap x
with
815 match Ast.unwrap x
with
816 Ast.Return
(_
,_
) | Ast.ReturnExpr
(_
,_
,_
) -> true
817 | Ast.DisjRuleElem
((_
::_
) as l) -> List.for_all
loop l
820 | Ast.Disj
(disjs
) -> List.for_all
ends_in_return disjs
823 | Ast.CIRCLES
(x
) -> failwith
"not supported"
824 | Ast.STARS
(x
) -> failwith
"not supported"
826 (* --------------------------------------------------------------------- *)
829 let exptymatch l make_match make_guard_match
=
830 let pos = fresh_pos() in
831 let matches_guard_matches =
834 let pos = Ast.make_mcode
pos in
835 (make_match (Ast.set_pos x
(Some
pos)),
836 make_guard_match
(Ast.set_pos x
(Some
pos))))
838 let (matches
,guard_matches
) = List.split
matches_guard_matches in
839 let rec suffixes = function
841 | x
::xs -> xs::(suffixes xs) in
842 let prefixes = List.rev
(suffixes (List.rev guard_matches
)) in
843 let info = (* not null *)
849 ctl_and CTL.NONSTRICT
matcher
851 (ctl_uncheck (List.fold_left
ctl_or_fl CTL.False negates
)))))
853 CTL.InnerAnd
(List.fold_left
ctl_or_fl CTL.False
(List.rev
info))
855 (* code might be a DisjRuleElem, in which case we break it apart
856 code might contain an Exp or Ty
857 this one pushes the quantifier inwards *)
858 let do_re_matches label guard
res quantified minus_quantified
=
859 let make_guard_match x
=
860 let stmt_fvs = Ast.get_mfvs x
in
861 let fvs = get_unquantified minus_quantified
stmt_fvs in
862 non_saved_quantify fvs (make_match None
true x
) in
864 let stmt_fvs = Ast.get_fvs x
in
865 let fvs = get_unquantified quantified
stmt_fvs in
866 quantify guard
fvs (make_match None guard x
) in
867 ctl_and CTL.NONSTRICT
(label_pred_maker label
)
868 (match List.map
Ast.unwrap
res with
869 [] -> failwith
"unexpected empty disj"
870 | Ast.Exp
(e
)::rest
-> exptymatch res make_match make_guard_match
871 | Ast.Ty
(t
)::rest
-> exptymatch res make_match make_guard_match
873 if List.exists (function Ast.Exp
(_
) | Ast.Ty
(_
) -> true | _
-> false)
875 then failwith
"unexpected exp or ty";
876 List.fold_left
ctl_seqor CTL.False
877 (List.rev
(List.map
make_match res)))
879 (* code might be a DisjRuleElem, in which case we break it apart
880 code doesn't contain an Exp or Ty
881 this one is for use when it is not practical to push the quantifier inwards
883 let header_match label guard code
: ('
a, Ast.meta_name
, 'b
) CTL.generic_ctl
=
884 match Ast.unwrap code
with
885 Ast.DisjRuleElem
(res) ->
886 let make_match = make_match None guard
in
887 let orop = if guard
then ctl_or else ctl_seqor in
888 ctl_and CTL.NONSTRICT
(label_pred_maker label
)
889 (List.fold_left
orop CTL.False
(List.map
make_match res))
890 | _
-> make_match label guard code
892 (* --------------------------------------------------------------------- *)
893 (* control structures *)
895 let end_control_structure fvs header body after_pred
896 after_checks no_after_checks
(afvs
,afresh
,ainh
,aft
) after label guard
=
897 (* aft indicates what is added after the whole if, which has to be added
899 let (aft_needed
,after_branch
) =
901 Ast.CONTEXT
(_
,Ast.NOTHING
) ->
902 (false,make_seq_after2 guard after_pred after
)
905 make_match label guard
906 (make_meta_rule_elem aft
(afvs
,afresh
,ainh
)) in
908 make_seq_after guard after_pred
909 (After
(make_seq_after guard
match_endif after
))) in
910 let body = body after_branch
in
911 let s = guard_to_strict guard
in
916 (match (after
,aft_needed
) with
917 (After _
,_
) (* pattern doesn't end here *)
918 | (_
,true) (* + code added after *) -> after_checks
919 | _
-> no_after_checks
)
920 (ctl_ax_absolute s body)))
922 let ifthen ifheader branch
((afvs
,_
,_
,_
) as aft
) after
923 quantified minus_quantified label llabel slabel recurse
make_match guard
=
924 (* "if (test) thn" becomes:
925 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
927 "if (test) thn; after" becomes:
928 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
933 match seq_fvs quantified
934 [Ast.get_fvs ifheader
;Ast.get_fvs branch
;afvs
] with
935 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
936 | _
-> failwith
"not possible" in
937 let new_quantified = Common.union_set bfvs quantified
in
939 match seq_fvs minus_quantified
940 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch
;[]] with
941 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
942 | _
-> failwith
"not possible" in
943 let new_mquantified = Common.union_set mbfvs minus_quantified
in
945 let if_header = quantify guard efvs
(make_match ifheader
) in
946 (* then branch and after *)
947 let lv = get_label_ctr() in
948 let used = ref false in
951 [truepred label
; recurse branch Tail
new_quantified new_mquantified
952 (Some
(lv,used)) llabel slabel guard
] in
953 let after_pred = aftpred label
in
954 let or_cases after_branch
=
955 ctl_or true_branch (ctl_or (fallpred label
) after_branch
) in
956 let (if_header,wrapper
) =
959 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
960 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
961 (function body -> quantify true [lv] body))
962 else (if_header,function x
-> x
) in
964 (end_control_structure bfvs
if_header or_cases after_pred
965 (Some
(ctl_ex after_pred)) None aft after label guard
)
967 let ifthenelse ifheader branch1 els branch2
((afvs
,_
,_
,_
) as aft
) after
968 quantified minus_quantified label llabel slabel recurse
make_match guard
=
969 (* "if (test) thn else els" becomes:
970 if(test) & AX((TrueBranch & AX thn) v
971 (FalseBranch & AX (else & AX els)) v After)
974 "if (test) thn else els; after" becomes:
975 if(test) & AX((TrueBranch & AX thn) v
976 (FalseBranch & AX (else & AX els)) v
977 (After & AXAX after))
982 let (e1fvs
,b1fvs
,s1fvs
) =
983 match seq_fvs quantified
984 [Ast.get_fvs ifheader
;Ast.get_fvs branch1
;afvs
] with
985 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
986 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
987 | _
-> failwith
"not possible" in
988 let (e2fvs
,b2fvs
,s2fvs
) =
990 match seq_fvs quantified
991 [Ast.get_fvs ifheader
;Ast.get_fvs branch2
;afvs
] with
992 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
993 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
994 | _
-> failwith
"not possible" in
995 let bothfvs = union (union b1fvs b2fvs
) (intersect s1fvs s2fvs
) in
996 let exponlyfvs = intersect e1fvs e2fvs
in
997 let new_quantified = union bothfvs quantified
in
998 (* minus free variables *)
999 let (me1fvs
,mb1fvs
,ms1fvs
) =
1000 match seq_fvs minus_quantified
1001 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch1
;[]] with
1002 [(e1fvs
,b1fvs
);(s1fvs
,b1afvs
);_
] ->
1003 (e1fvs
,Common.union_set b1fvs b1afvs
,s1fvs
)
1004 | _
-> failwith
"not possible" in
1005 let (me2fvs
,mb2fvs
,ms2fvs
) =
1007 match seq_fvs minus_quantified
1008 [Ast.get_mfvs ifheader
;Ast.get_mfvs branch2
;[]] with
1009 [(e2fvs
,b2fvs
);(s2fvs
,b2afvs
);_
] ->
1010 (e2fvs
,Common.union_set b2fvs b2afvs
,s2fvs
)
1011 | _
-> failwith
"not possible" in
1012 let mbothfvs = union (union mb1fvs mb2fvs
) (intersect ms1fvs ms2fvs
) in
1013 let new_mquantified = union mbothfvs minus_quantified
in
1015 let if_header = quantify guard
exponlyfvs (make_match ifheader
) in
1016 (* then and else branches *)
1017 let lv = get_label_ctr() in
1018 let used = ref false in
1021 [truepred label
; recurse branch1 Tail
new_quantified new_mquantified
1022 (Some
(lv,used)) llabel slabel guard
] in
1025 [falsepred label
; make_match els
;
1026 recurse branch2 Tail
new_quantified new_mquantified
1027 (Some
(lv,used)) llabel slabel guard
] in
1028 let after_pred = aftpred label
in
1029 let or_cases after_branch
=
1030 ctl_or true_branch (ctl_or false_branch after_branch
) in
1031 let s = guard_to_strict guard
in
1032 let (if_header,wrapper
) =
1035 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1036 (ctl_and CTL.NONSTRICT
(*???*) if_header label_pred,
1037 (function body -> quantify true [lv] body))
1038 else (if_header,function x
-> x
) in
1040 (end_control_structure bothfvs if_header or_cases after_pred
1041 (Some
(ctl_and s (ctl_ex (falsepred label
)) (ctl_ex after_pred)))
1042 (Some
(ctl_ex (falsepred label
)))
1043 aft after label guard
)
1045 let forwhile header
body ((afvs
,_
,_
,_
) as aft
) after
1046 quantified minus_quantified label recurse
make_match guard
=
1048 (* the translation in this case is similar to that of an if with no else *)
1049 (* free variables *)
1051 match seq_fvs quantified
[Ast.get_fvs header
;Ast.get_fvs
body;afvs
] with
1052 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1053 | _
-> failwith
"not possible" in
1054 let new_quantified = Common.union_set bfvs quantified
in
1055 (* minus free variables *)
1057 match seq_fvs minus_quantified
1058 [Ast.get_mfvs header
;Ast.get_mfvs
body;[]] with
1059 [(efvs
,b1fvs
);(_
,b2fvs
);_
] -> (efvs
,Common.union_set b1fvs b2fvs
)
1060 | _
-> failwith
"not possible" in
1061 let new_mquantified = Common.union_set mbfvs minus_quantified
in
1063 let header = quantify guard efvs
(make_match header) in
1064 let lv = get_label_ctr() in
1065 let used = ref false in
1069 recurse
body Tail
new_quantified new_mquantified
1070 (Some
(lv,used)) (Some
(lv,used)) None guard
] in
1071 let after_pred = fallpred label
in
1072 let or_cases after_branch
= ctl_or body after_branch
in
1073 let (header,wrapper
) =
1076 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1077 (ctl_and CTL.NONSTRICT
(*???*) header label_pred,
1078 (function body -> quantify true [lv] body))
1079 else (header,function x
-> x
) in
1081 (end_control_structure bfvs
header or_cases after_pred
1082 (Some
(ctl_ex after_pred)) None aft after label guard
) in
1083 match (Ast.unwrap
body,aft
) with
1084 (Ast.Atomic
(re
),(_
,_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
))) ->
1085 (match Ast.unwrap re
with
1086 Ast.MetaStmt
((_
,_
,Ast.CONTEXT
(_
,Ast.NOTHING
),_
),
1087 Type_cocci.Unitary
,_
,false) ->
1089 match seq_fvs quantified
[Ast.get_fvs
header] with
1091 | _
-> failwith
"not possible" in
1092 quantify guard efvs
(make_match header)
1096 (* --------------------------------------------------------------------- *)
1097 (* statement metavariables *)
1099 (* issue: an S metavariable that is not an if branch/loop body
1100 should not match an if branch/loop body, so check that the labels
1101 of the nodes before the first node matched by the S are different
1102 from the label of the first node matched by the S *)
1103 let sequencibility body label_pred process_bef_aft
= function
1104 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
1107 (ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1108 | Ast.SequencibleAfterDots
l ->
1109 (* S appears after some dots. l is the code that comes after the S.
1110 want to search for that first, because S can match anything, while
1111 the stuff after is probably more restricted *)
1112 let afts = List.map process_bef_aft
l in
1113 let ors = foldl1 ctl_or afts in
1114 ctl_and CTL.NONSTRICT
1115 (ctl_ef (ctl_and CTL.NONSTRICT
ors (ctl_back_ax label_pred)))
1118 ctl_and CTL.NONSTRICT
(ctl_not (ctl_back_ax label_pred)) x
))
1119 | Ast.NotSequencible
-> body (function x
-> x
)
1121 let svar_context_with_add_after stmt
s label quantified
d ast
1122 seqible after process_bef_aft guard fvinfo
=
1123 let label_var = (*fresh_label_var*) string2var "_lab" in
1125 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1127 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1128 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1129 let full_metamatch = matcher d in
1130 let first_metamatch =
1133 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(bef
,_
)) ->
1134 Ast.CONTEXT
(pos,Ast.BEFORE
(bef
))
1135 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1136 | Ast.MINUS
(_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1137 let middle_metamatch =
1140 Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1141 | Ast.MINUS
(_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1142 let last_metamatch =
1145 Ast.CONTEXT
(pos,Ast.BEFOREAFTER
(_
,aft
)) ->
1146 Ast.CONTEXT
(pos,Ast.AFTER
(aft
))
1147 | Ast.CONTEXT
(_
,_
) -> d
1148 | Ast.MINUS
(_
,_
) | Ast.PLUS
-> failwith
"not possible") in
1151 ctl_and CTL.NONSTRICT
middle_metamatch prelabel_pred in
1152 let left_or = (* the whole statement is one node *)
1154 [full_metamatch; and_after guard
(ctl_not prelabel_pred) after
] in
1155 let right_or = (* the statement covers multiple nodes *)
1158 ctl_au CTL.NONSTRICT
1161 [ctl_and CTL.NONSTRICT
last_metamatch label_pred;
1163 (ctl_not prelabel_pred) after
])] in
1165 ctl_and CTL.NONSTRICT
label_pred
1166 (f
(ctl_and CTL.NONSTRICT
1167 (make_raw_match label
false ast
) (ctl_or left_or right_or))) in
1168 let stmt_fvs = Ast.get_fvs stmt
in
1169 let fvs = get_unquantified quantified
stmt_fvs in
1170 quantify guard
(label_var::fvs)
1171 (sequencibility body label_pred process_bef_aft seqible
)
1173 let svar_minus_or_no_add_after stmt
s label quantified
d ast
1174 seqible after process_bef_aft guard fvinfo
=
1175 let label_var = (*fresh_label_var*) string2var "_lab" in
1177 CTL.Pred
(Lib_engine.Label
(label_var),CTL.Control
) in
1179 CTL.Pred
(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
1180 let matcher d = make_match None guard
(make_meta_rule_elem d fvinfo
) in
1182 (* don't have to put anything before the beginning, so don't have to
1183 distinguish the first node. so don't have to bother about paths,
1184 just use the label. label ensures that found nodes match up with
1185 what they should because it is in the lhs of the andany. *)
1187 Ast.MINUS
(pos,[]) -> true
1188 | Ast.CONTEXT
(pos,Ast.NOTHING
) -> true
1191 match (pure_d,after
) with
1192 (true,Tail
) | (true,End
) | (true,VeryEnd
) ->
1193 (* the label sharing makes it safe to use AndAny *)
1194 CTL.HackForStmt
(CTL.FORWARD
,CTL.NONSTRICT
,
1195 ctl_and CTL.NONSTRICT
label_pred
1196 (make_raw_match label
false ast
),
1197 ctl_and CTL.NONSTRICT
(matcher d) prelabel_pred)
1199 (* more safe but less efficient *)
1200 let first_metamatch = matcher d in
1201 let rest_metamatch =
1204 Ast.MINUS
(pos,_
) -> Ast.MINUS
(pos,[])
1205 | Ast.CONTEXT
(pos,_
) -> Ast.CONTEXT
(pos,Ast.NOTHING
)
1206 | Ast.PLUS
-> failwith
"not possible") in
1207 let rest_nodes = ctl_and CTL.NONSTRICT
rest_metamatch prelabel_pred in
1208 let last_node = and_after guard
(ctl_not prelabel_pred) after
in
1209 (ctl_and CTL.NONSTRICT
(make_raw_match label
false ast
)
1212 ctl_au CTL.NONSTRICT
rest_nodes last_node])) in
1213 let body f
= ctl_and CTL.NONSTRICT
label_pred (f
ender) in
1214 let stmt_fvs = Ast.get_fvs stmt
in
1215 let fvs = get_unquantified quantified
stmt_fvs in
1216 quantify guard
(label_var::fvs)
1217 (sequencibility body label_pred process_bef_aft seqible
)
1219 (* --------------------------------------------------------------------- *)
1220 (* dots and nests *)
1222 let dots_au is_strict toend label
s wrapcode x seq_after y quantifier
=
1223 let matchgoto = gotopred None
in
1225 make_match None
false
1227 (Ast.Break
(Ast.make_mcode
"break",Ast.make_mcode
";"))) in
1229 make_match None
false
1231 (Ast.Continue
(Ast.make_mcode
"continue",Ast.make_mcode
";"))) in
1233 if quantifier
= Exists
1234 then Common.Left
(CTL.False
)
1236 then Common.Left
(CTL.Or
(aftpred label
,exitpred label
))
1238 then Common.Left
(aftpred label
)
1242 let lv = get_label_ctr() in
1243 let labelpred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1244 let preflabelpred = label_pred_maker (Some
(lv,ref true)) in
1245 ctl_or (aftpred label
)
1246 (quantify false [lv]
1247 (ctl_and CTL.NONSTRICT
1248 (ctl_and CTL.NONSTRICT
(truepred label
) labelpred)
1249 (ctl_au CTL.NONSTRICT
1250 (ctl_and CTL.NONSTRICT
(ctl_not v) preflabelpred)
1251 (ctl_and CTL.NONSTRICT
preflabelpred
1252 (ctl_or (retpred None
)
1253 (if !Flag_matcher.only_return_is_error_exit
1256 (ctl_or matchcontinue
1257 (ctl_and CTL.NONSTRICT
1258 (ctl_or matchgoto matchbreak)
1259 (ctl_ag s (ctl_not seq_after
))))))))))) in
1260 let op = if quantifier
= !exists then ctl_au else ctl_anti_au in
1261 let v = get_let_ctr() in
1263 (match stop_early with
1264 Common.Left x
-> ctl_or y x
1265 | Common.Right
stop_early ->
1266 CTL.Let
(v,y
,ctl_or (CTL.Ref
v) (stop_early (CTL.Ref
v))))
1268 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1269 process_bef_aft statement_list statement guard quantified wrapcode
=
1270 let ctl_and_ns = ctl_and CTL.NONSTRICT
in
1271 (* proces bef_aft *)
1273 List.fold_left
ctl_or_fl CTL.False
(List.map process_bef_aft
l) in
1274 let bef_aft = (* to be negated *)
1278 (function Ast.WhenModifier
(Ast.WhenAny
) -> true | _ -> false)
1281 with Not_found
-> shortest (Common.union_set bef aft
) in
1284 (function Ast.WhenModifier
(Ast.WhenStrict
) -> true | _ -> false)
1286 let check_quantifier quant other
=
1288 (function Ast.WhenModifier
(x
) -> x
= quant
| _ -> false)
1292 (function Ast.WhenModifier
(x
) -> x
= other
| _ -> false)
1294 then failwith
"inconsistent annotation on dots"
1298 if check_quantifier Ast.WhenExists
Ast.WhenForall
1301 if check_quantifier Ast.WhenForall
Ast.WhenExists
1304 (* the following is used when we find a goto, etc and consider accepting
1305 without finding the rest of the pattern *)
1306 let aft = shortest aft in
1307 (* process whencode *)
1308 let labelled = label_pred_maker label
in
1310 let (poswhen
,negwhen
) =
1312 (function (poswhen
,negwhen
) ->
1314 Ast.WhenNot
whencodes ->
1315 (poswhen
,ctl_or (statement_list
whencodes) negwhen
)
1316 | Ast.WhenAlways stm
->
1317 (ctl_and CTL.NONSTRICT
(statement stm
) poswhen
,negwhen
)
1318 | Ast.WhenModifier
(_) -> (poswhen
,negwhen
)
1319 | Ast.WhenNotTrue
(e
) ->
1321 ctl_or (whencond_true e label guard quantified
) negwhen
)
1322 | Ast.WhenNotFalse
(e
) ->
1324 ctl_or (whencond_false e label guard quantified
) negwhen
))
1325 (CTL.True
,bef_aft) (List.rev
whencodes) in
1326 let poswhen = ctl_and_ns arg
poswhen in
1330 (* add in After, because it's not part of the program *)
1331 ctl_or (aftpred label
) negwhen
1333 ctl_and_ns poswhen (ctl_not negwhen) in
1334 (* process dot code, if any *)
1336 match (dotcode,guard
) with
1337 (None
,_) | (_,true) -> CTL.True
1338 | (Some
dotcode,_) -> dotcode in
1339 (* process nest code, if any *)
1340 (* whencode goes in the negated part of the nest; if no nest, just goes
1341 on the "true" in between code *)
1342 let plus_var = if plus
then get_label_ctr() else string2var "" in
1343 let plus_var2 = if plus
then get_label_ctr() else string2var "" in
1345 match (nest
,guard
&& not plus
) with
1346 (None
,_) | (_,true) -> whencodes CTL.True
1347 | (Some nest
,false) ->
1348 let v = get_let_ctr() in
1352 (* the idea is that BindGood is sort of a witness; a witness to
1353 having found the subterm in at least one place. If there is
1354 not a witness, then there is a risk that it will get thrown
1355 away, if it is merged with a node that has an empty
1356 environment. See tests/nestplus. But this all seems
1357 rather suspicious *)
1358 CTL.And
(CTL.NONSTRICT
,x
,
1359 CTL.Exists
(true,plus_var2,
1360 CTL.Pred
(Lib_engine.BindGood
(plus_var),
1361 CTL.Modif
plus_var2)))
1364 CTL.Or
(is_plus (CTL.Ref
v),
1365 whencodes (CTL.Not
(ctl_uncheck (CTL.Ref
v))))) in
1366 let plus_modifier x
=
1373 CTL.Not
(CTL.Pred
(Lib_engine.BindBad
(plus_var),CTL.Control
)))))
1379 | Guard f
-> ctl_uncheck f
1381 let exit = endpred label
in
1382 let errorexit = exitpred label
in
1383 ctl_or exit errorexit
1384 (* not at all sure what the next two mean... *)
1388 Some
(lv,used) -> used := true;
1389 ctl_or (CTL.Pred
(Lib_engine.Label
lv,CTL.Control
))
1390 (ctl_back_ex (ctl_or (retpred label
) (gotopred label
)))
1391 | None
-> endpred label
)
1392 (* was the following, but not clear why sgrep should allow
1394 let exit = endpred label in
1395 let errorexit = exitpred label in
1397 then ctl_or exit errorexit (* end anywhere *)
1398 else exit (* end at the real end of the function *) *)
in
1400 (dots_au is_strict ((after
= Tail
) or (after
= VeryEnd
))
1401 label
(guard_to_strict guard
) wrapcode
1402 (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
1403 aft ender quantifier)
1405 and get_whencond_exps e
=
1406 match Ast.unwrap e
with
1408 | Ast.DisjRuleElem
(res) ->
1409 List.fold_left
Common.union_set
[] (List.map get_whencond_exps
res)
1410 | _ -> failwith
"not possible"
1412 and make_whencond_headers e e1 label guard quantified
=
1413 let fvs = Ast.get_fvs e
in
1415 quantify guard
(get_unquantified quantified
fvs)
1416 (make_match label guard h
) in
1421 (Ast.make_mcode
"if",
1422 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1423 let while_header e1
=
1427 (Ast.make_mcode
"while",
1428 Ast.make_mcode
"(",e1
,Ast.make_mcode
")"))) in
1433 (Ast.make_mcode
"for",Ast.make_mcode
"(",None
,Ast.make_mcode
";",
1434 Some e1
,Ast.make_mcode
";",None
,Ast.make_mcode
")"))) in
1436 List.fold_left
ctl_or CTL.False
(List.map
if_header e1
) in
1438 List.fold_left
ctl_or CTL.False
(List.map
while_header e1
) in
1440 List.fold_left
ctl_or CTL.False
(List.map
for_header e1
) in
1441 (if_headers, while_headers, for_headers)
1443 and whencond_true e label guard quantified
=
1444 let e1 = get_whencond_exps e
in
1445 let (if_headers, while_headers, for_headers) =
1446 make_whencond_headers e
e1 label guard quantified
in
1448 (ctl_and CTL.NONSTRICT
(truepred label
) (ctl_back_ex if_headers))
1449 (ctl_and CTL.NONSTRICT
1450 (inlooppred label
) (ctl_back_ex (ctl_or while_headers for_headers)))
1452 and whencond_false e label guard quantified
=
1453 let e1 = get_whencond_exps e
in
1454 let (if_headers, while_headers, for_headers) =
1455 make_whencond_headers e
e1 label guard quantified
in
1456 ctl_or (ctl_and CTL.NONSTRICT
(falsepred label
) (ctl_back_ex if_headers))
1457 (ctl_and CTL.NONSTRICT
(fallpred label
)
1458 (ctl_or (ctl_back_ex if_headers)
1459 (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
1461 (* --------------------------------------------------------------------- *)
1462 (* the main translation loop *)
1464 let rec statement_list stmt_list after quantified minus_quantified
1465 label llabel slabel dots_before guard
=
1467 (* include Disj to be on the safe side *)
1468 match Ast.unwrap x
with
1469 Ast.Dots
_ | Ast.Nest
_ | Ast.Disj
_ -> true | _ -> false in
1470 let compute_label l e db
= if db
or isdots e
then l else None
in
1471 match Ast.unwrap stmt_list
with
1473 let rec loop quantified minus_quantified dots_before label llabel slabel
1475 ([],_,_) -> (match after
with After f
-> f
| _ -> CTL.True
)
1477 statement e after quantified minus_quantified
1478 (compute_label label e dots_before
)
1480 | (e
::sl
,fv
::fvs,mfv
::mfvs
) ->
1481 let shared = intersectll fv
fvs in
1482 let unqshared = get_unquantified quantified
shared in
1483 let new_quantified = Common.union_set
unqshared quantified
in
1484 let minus_shared = intersectll mfv mfvs
in
1486 get_unquantified minus_quantified
minus_shared in
1487 let new_mquantified =
1488 Common.union_set
munqshared minus_quantified
in
1489 quantify guard
unqshared
1492 (let (label1
,llabel1
,slabel1
) =
1493 match Ast.unwrap e
with
1495 (match Ast.unwrap re
with
1496 Ast.Goto
_ -> (None
,None
,None
)
1497 | _ -> (label
,llabel
,slabel
))
1498 | _ -> (label
,llabel
,slabel
) in
1499 loop new_quantified new_mquantified (isdots e
)
1500 label1 llabel1 slabel1
1502 new_quantified new_mquantified
1503 (compute_label label e dots_before
) llabel slabel guard
)
1504 | _ -> failwith
"not possible" in
1505 loop quantified minus_quantified dots_before
1507 (x
,List.map
Ast.get_fvs x
,List.map
Ast.get_mfvs x
)
1508 | Ast.CIRCLES
(x
) -> failwith
"not supported"
1509 | Ast.STARS
(x
) -> failwith
"not supported"
1511 (* llabel is the label of the enclosing loop and slabel is the label of the
1513 and statement stmt after quantified minus_quantified
1514 label llabel slabel guard
=
1515 let ctl_au = ctl_au CTL.NONSTRICT
in
1516 let ctl_ax = ctl_ax CTL.NONSTRICT
in
1517 let ctl_and = ctl_and CTL.NONSTRICT
in
1518 let make_seq = make_seq guard
in
1519 let make_seq_after = make_seq_after guard
in
1520 let real_make_match = make_match in
1521 let make_match = header_match label guard
in
1523 let dots_done = ref false in (* hack for dots cases we can easily handle *)
1526 match Ast.unwrap stmt
with
1528 (match Ast.unwrap ast
with
1529 (* the following optimisation is not a good idea, because when S
1530 is alone, we would like it not to match a declaration.
1531 this makes more matching for things like when (...) S, but perhaps
1532 that matching is not so costly anyway *)
1533 (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
1534 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.BEFOREAFTER
(_,_)) as d),_),
1536 | Ast.MetaStmt
((s,_,(Ast.CONTEXT
(_,Ast.AFTER
(_)) as d),_),
1538 svar_context_with_add_after stmt
s label quantified
d ast seqible
1540 (process_bef_aft quantified minus_quantified
1541 label llabel slabel
true)
1543 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1545 | Ast.MetaStmt
((s,_,d,_),keep
,seqible
,_) ->
1546 svar_minus_or_no_add_after stmt
s label quantified
d ast seqible
1548 (process_bef_aft quantified minus_quantified
1549 label llabel slabel
true)
1551 (Ast.get_fvs stmt
, Ast.get_fresh stmt
, Ast.get_inherited stmt
)
1555 match Ast.unwrap ast
with
1556 Ast.DisjRuleElem
(res) ->
1557 do_re_matches label guard
res quantified minus_quantified
1558 | Ast.Exp
(_) | Ast.Ty
(_) ->
1559 let stmt_fvs = Ast.get_fvs stmt
in
1560 let fvs = get_unquantified quantified
stmt_fvs in
1561 CTL.InnerAnd
(quantify guard
fvs (make_match ast
))
1563 let stmt_fvs = Ast.get_fvs stmt
in
1564 let fvs = get_unquantified quantified
stmt_fvs in
1565 quantify guard
fvs (make_match ast
) in
1566 match Ast.unwrap ast
with
1567 Ast.Break
(brk
,semi
) ->
1568 (match (llabel
,slabel
) with
1569 (_,Some
(lv,used)) -> (* use switch label if there is one *)
1570 ctl_and term (bclabel_pred_maker slabel
)
1571 | _ -> ctl_and term (bclabel_pred_maker llabel
))
1572 | Ast.Continue
(brk
,semi
) -> ctl_and term (bclabel_pred_maker llabel
)
1573 | Ast.Return
((_,info,retmc
,pos),(_,_,semmc
,_)) ->
1574 (* discard pattern that comes after return *)
1575 let normal_res = make_seq_after term after
in
1576 (* the following code tries to propagate the modifications on
1577 return; to a close brace, in the case where the final return
1580 match (retmc
,semmc
) with
1581 (Ast.MINUS
(_,l1
),Ast.MINUS
(_,l2
)) when !Flag.sgrep_mode2
->
1582 (* in sgrep mode, we can propagate the - *)
1583 Some
(Ast.MINUS
(Ast.NoPos
,l1
@l2
))
1584 | (Ast.MINUS
(_,l1
),Ast.MINUS
(_,l2
))
1585 | (Ast.CONTEXT
(_,Ast.BEFORE
(l1
)),
1586 Ast.CONTEXT
(_,Ast.AFTER
(l2
))) ->
1587 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l1
@l2
)))
1588 | (Ast.CONTEXT
(_,Ast.BEFORE
(_)),Ast.CONTEXT
(_,Ast.NOTHING
))
1589 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.NOTHING
)) ->
1591 | (Ast.CONTEXT
(_,Ast.NOTHING
),Ast.CONTEXT
(_,Ast.AFTER
(l))) ->
1592 Some
(Ast.CONTEXT
(Ast.NoPos
,Ast.BEFORE
(l)))
1594 let ret = Ast.make_mcode
"return" in
1596 Ast.rewrap ast
(Ast.Edots
(Ast.make_mcode
"...",None
)) in
1597 let semi = Ast.make_mcode
";" in
1599 make_match(Ast.rewrap ast
(Ast.Return
(ret,semi))) in
1601 make_match(Ast.rewrap ast
(Ast.ReturnExpr
(ret,edots,semi))) in
1604 let exit = endpred None
in
1606 Ast.rewrap ast
(Ast.SeqEnd
(("}",info,new_mc,pos))) in
1607 let stripped_rbrace =
1608 Ast.rewrap ast
(Ast.SeqEnd
(Ast.make_mcode
"}")) in
1610 (ctl_and (make_match mod_rbrace)
1615 (ctl_or simple_return return_expr))))
1617 (make_match stripped_rbrace)
1618 (* error exit not possible; it is in the middle
1619 of code, so a return is needed *)
1622 (* some change in the middle of the return, so have to
1623 find an actual return *)
1626 (* should try to deal with the dots_bef_aft problem elsewhere,
1627 but don't have the courage... *)
1632 do_between_dots stmt
term End
1633 quantified minus_quantified label llabel slabel guard
in
1635 make_seq_after term after
)
1636 | Ast.Seq
(lbrace
,decls
,body,rbrace
) ->
1637 let (lbfvs
,b1fvs
,b2fvs
,b3fvs
,rbfvs
) =
1640 [Ast.get_fvs lbrace
;Ast.get_fvs decls
;
1641 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1643 [(lbfvs
,b1fvs
);(_,b2fvs
);(_,b3fvs
);(rbfvs
,_)] ->
1644 (lbfvs
,b1fvs
,b2fvs
,b3fvs
,rbfvs
)
1645 | _ -> failwith
"not possible" in
1646 let (mlbfvs
,mb1fvs
,mb2fvs
,mb3fvs
,mrbfvs
) =
1648 seq_fvs minus_quantified
1649 [Ast.get_mfvs lbrace
;Ast.get_mfvs decls
;
1650 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1652 [(lbfvs
,b1fvs
);(_,b2fvs
);(_,b3fvs
);(rbfvs
,_)] ->
1653 (lbfvs
,b1fvs
,b2fvs
,b3fvs
,rbfvs
)
1654 | _ -> failwith
"not possible" in
1655 let pv = count_nested_braces stmt
in
1656 let lv = get_label_ctr() in
1657 let paren_pred = CTL.Pred
(Lib_engine.Paren
pv,CTL.Control
) in
1658 let label_pred = CTL.Pred
(Lib_engine.Label
lv,CTL.Control
) in
1661 (quantify guard lbfvs
(make_match lbrace
))
1662 (ctl_and paren_pred label_pred) in
1664 match Ast.unwrap rbrace
with
1665 Ast.SeqEnd
((data
,info,_,pos)) ->
1666 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
1667 | _ -> failwith
"unexpected close brace" in
1669 (* label is not needed; paren_pred is enough *)
1670 quantify guard rbfvs
1671 (ctl_au (make_match empty_rbrace)
1673 (real_make_match None guard rbrace
)
1675 let new_quantified2 =
1676 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
1677 let new_quantified3 = Common.union_set b3fvs
new_quantified2 in
1678 let new_mquantified2 =
1679 Common.union_set mb1fvs
(Common.union_set mb2fvs minus_quantified
) in
1680 let new_mquantified3 = Common.union_set mb3fvs
new_mquantified2 in
1681 let pattern_as_given =
1682 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1683 let new_quantified3 = Common.union_set
[pv] new_quantified3 in
1684 quantify true [pv;lv]
1685 (quantify guard b1fvs
1688 quantify guard b2fvs
1689 (statement_list decls
1691 (quantify guard b3fvs
1692 (statement_list body
1693 (After
(make_seq_after end_brace after
))
1694 new_quantified3 new_mquantified3
1695 (Some
(lv,ref true)) (* label mostly useful *)
1696 llabel slabel
true guard
)))
1697 new_quantified2 new_mquantified2
1698 (Some
(lv,ref true)) llabel slabel
false guard
)])) in
1699 if ends_in_return body
1701 (* matching error handling code *)
1703 1. The pattern as given
1704 2. A goto, and then some close braces, and then the pattern as
1705 given, but without the braces (only possible if there are no
1706 decls, and open and close braces are unmodified)
1707 3. Part of the pattern as given, then a goto, and then the rest
1708 of the pattern. For this case, we just check that all paths have
1709 a goto within the current braces. checking for a goto at every
1710 point in the pattern seems expensive and not worthwhile. *)
1712 let body = preprocess_dots body in (* redo, to drop braces *)
1716 (make_match empty_rbrace)
1717 (ctl_ax (* skip the destination label *)
1718 (quantify guard b3fvs
1719 (statement_list body End
1720 new_quantified3 new_mquantified3 None llabel slabel
1723 let new_quantified2 = Common.union_set
[pv] new_quantified2 in
1724 let new_quantified3 = Common.union_set
[pv] new_quantified3 in
1725 quantify true [pv;lv]
1726 (quantify guard b1fvs
1730 (CTL.AU
(* want AF even for sgrep *)
1731 (CTL.FORWARD
,CTL.STRICT
,
1732 CTL.Pred
(Lib_engine.PrefixLabel
(lv),CTL.Control
),
1733 ctl_and (* brace must be eventually after goto *)
1734 (gotopred (Some
(lv,ref true)))
1735 (* want AF even for sgrep *)
1736 (CTL.AF
(CTL.FORWARD
,CTL.STRICT
,end_brace))))
1737 (quantify guard b2fvs
1738 (statement_list decls
1740 (quantify guard b3fvs
1741 (statement_list body Tail
1744 nopv_end_brace after)*)
1745 new_quantified3 new_mquantified3
1746 None llabel slabel
true guard
)))
1747 new_quantified2 new_mquantified2
1748 (Some
(lv,ref true))
1749 llabel slabel
false guard
))])) in
1750 ctl_or pattern_as_given
1751 (match Ast.unwrap decls
with
1752 Ast.DOTS
([]) -> ctl_or pattern2 pattern3
1753 | Ast.DOTS
(l) -> pattern3
1754 | _ -> failwith
"circles and stars not supported")
1755 else pattern_as_given
1756 | Ast.IfThen
(ifheader
,branch
,aft) ->
1757 ifthen ifheader branch
aft after quantified minus_quantified
1758 label llabel slabel statement
make_match guard
1760 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft) ->
1761 ifthenelse ifheader branch1 els branch2
aft after quantified
1762 minus_quantified label llabel slabel statement
make_match guard
1764 | Ast.While
(header,body,aft) | Ast.For
(header,body,aft)
1765 | Ast.Iterator
(header,body,aft) ->
1766 forwhile header body aft after quantified minus_quantified
1767 label statement
make_match guard
1769 | Ast.Disj
(stmt_dots_list
) -> (* list shouldn't be empty *)
1771 (label_pred_maker label
)
1772 (List.fold_left
ctl_seqor CTL.False
1775 statement_list sl after quantified minus_quantified label
1776 llabel slabel
true guard
)
1779 | Ast.Nest
(stmt_dots
,whencode
,multi
,bef
,aft) ->
1780 (* label in recursive call is None because label check is already
1781 wrapped around the corresponding code *)
1784 match seq_fvs quantified
[Ast.get_wcfvs whencode
;Ast.get_fvs stmt_dots
]
1786 [(wcfvs
,bothfvs);(bdfvs
,_)] -> bothfvs
1787 | _ -> failwith
"not possible" in
1789 (* no minus version because when code doesn't contain any minus code *)
1790 let new_quantified = Common.union_set
bfvs quantified
in
1794 statement_list stmt_dots
(a2n after
) new_quantified minus_quantified
1795 None llabel slabel
true guard
in
1796 dots_and_nests multi
1797 (Some
dots_pattern) whencode bef
aft None after label
1798 (process_bef_aft
new_quantified minus_quantified
1799 None llabel slabel
true)
1801 statement_list x Tail
new_quantified minus_quantified None
1802 llabel slabel
true true)
1804 statement x Tail
new_quantified minus_quantified None
1807 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
)))
1809 | Ast.Dots
((_,i
,d,_),whencodes,bef
,aft) ->
1813 (* no need for the fresh metavar, but ... is a bit wierd as a
1815 Some
(make_match (make_meta_rule_elem d ([],[],[])))
1817 dots_and_nests false None
whencodes bef
aft dot_code after label
1818 (process_bef_aft quantified minus_quantified None llabel slabel
true)
1820 statement_list x Tail quantified minus_quantified
1821 None llabel slabel
true true)
1823 statement x Tail quantified minus_quantified None llabel slabel
true)
1825 (function x
-> Ast.set_fvs
[] (Ast.rewrap stmt x
))
1827 | Ast.Switch
(header,lb
,cases,rb
) ->
1828 let rec intersect_all = function
1831 | x
::xs -> intersect x
(intersect_all xs) in
1832 let rec union_all l = List.fold_left
union [] l in
1833 (* start normal variables *)
1834 let header_fvs = Ast.get_fvs
header in
1835 let lb_fvs = Ast.get_fvs lb
in
1836 let case_fvs = List.map
Ast.get_fvs
cases in
1837 let rb_fvs = Ast.get_fvs rb
in
1838 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1839 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1841 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1842 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1843 function case_fvs ->
1844 match seq_fvs quantified
[header_fvs;lb_fvs;case_fvs;rb_fvs] with
1845 [(efvs
,b1fvs
);(lbfvs
,b2fvs
);(casefvs
,b3fvs
);(rbfvs
,_)] ->
1846 (efvs
::all_efvs
,b1fvs
::all_b1fvs
,lbfvs
::all_lbfvs
,
1847 b2fvs
::all_b2fvs
,casefvs
::all_casefvs
,b3fvs
::all_b3fvs
,
1849 | _ -> failwith
"not possible")
1850 ([],[],[],[],[],[],[]) case_fvs in
1851 let (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1852 all_casefvs
,all_b3fvs
,all_rbfvs
) =
1853 (List.rev all_efvs
,List.rev all_b1fvs
,List.rev all_lbfvs
,
1854 List.rev all_b2fvs
,List.rev all_casefvs
,List.rev all_b3fvs
,
1855 List.rev all_rbfvs
) in
1856 let exponlyfvs = intersect_all all_efvs
in
1857 let lbonlyfvs = intersect_all all_lbfvs
in
1858 (* don't do anything with right brace. Hope there is no + code on it *)
1859 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1860 let b1fvs = union_all all_b1fvs
in
1861 let new1_quantified = union b1fvs quantified
in
1862 let b2fvs = union (union_all all_b1fvs
) (intersect_all all_casefvs
) in
1863 let new2_quantified = union b2fvs new1_quantified in
1864 (* let b3fvs = union_all all_b3fvs in*)
1865 (* ------------------- start minus free variables *)
1866 let header_mfvs = Ast.get_mfvs
header in
1867 let lb_mfvs = Ast.get_mfvs lb
in
1868 let case_mfvs = List.map
Ast.get_mfvs
cases in
1869 let rb_mfvs = Ast.get_mfvs rb
in
1870 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1871 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1873 (function (all_efvs
,all_b1fvs
,all_lbfvs
,all_b2fvs
,
1874 all_casefvs
,all_b3fvs
,all_rbfvs
) ->
1875 function case_mfvs ->
1878 [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with
1879 [(efvs
,b1fvs);(lbfvs
,b2fvs);(casefvs
,b3fvs);(rbfvs
,_)] ->
1880 (efvs
::all_efvs
,b1fvs::all_b1fvs
,lbfvs
::all_lbfvs
,
1881 b2fvs::all_b2fvs
,casefvs
::all_casefvs
,b3fvs::all_b3fvs
,
1883 | _ -> failwith
"not possible")
1884 ([],[],[],[],[],[],[]) case_mfvs in
1885 let (all_mefvs
,all_mb1fvs
,all_mlbfvs
,all_mb2fvs
,
1886 all_mcasefvs
,all_mb3fvs
,all_mrbfvs
) =
1887 (List.rev all_mefvs
,List.rev all_mb1fvs
,List.rev all_mlbfvs
,
1888 List.rev all_mb2fvs
,List.rev all_mcasefvs
,List.rev all_mb3fvs
,
1889 List.rev all_mrbfvs
) in
1890 (* don't do anything with right brace. Hope there is no + code on it *)
1891 (* let rbonlyfvs = intersect_all all_rbfvs in*)
1892 let mb1fvs = union_all all_mb1fvs
in
1893 let new1_mquantified = union mb1fvs quantified
in
1894 let mb2fvs = union (union_all all_mb1fvs
) (intersect_all all_mcasefvs
) in
1895 let new2_mquantified = union mb2fvs new1_mquantified in
1896 (* let b3fvs = union_all all_b3fvs in*)
1897 (* ------------------- end collection of free variables *)
1898 let switch_header = quantify guard
exponlyfvs (make_match header) in
1899 let lb = quantify guard
lbonlyfvs (make_match lb) in
1900 (* let rb = quantify guard rbonlyfvs (make_match rb) in*)
1903 (function case_line
->
1904 match Ast.unwrap case_line
with
1905 Ast.CaseLine
(header,body) ->
1907 match seq_fvs new2_quantified [Ast.get_fvs
header] with
1908 [(e1fvs,_)] -> e1fvs
1909 | _ -> failwith
"not possible" in
1910 quantify guard
e1fvs (real_make_match label
true header)
1911 | Ast.OptCase
(case_line
) -> failwith
"not supported")
1914 ctl_not (List.fold_left
ctl_or_fl CTL.False
case_headers) in
1915 let lv = get_label_ctr() in
1916 let used = ref false in
1919 (function case_line
->
1920 match Ast.unwrap case_line
with
1921 Ast.CaseLine
(header,body) ->
1922 let (e1fvs,b1fvs,s1fvs
) =
1923 let fvs = [Ast.get_fvs
header;Ast.get_fvs
body] in
1924 match seq_fvs new2_quantified fvs with
1925 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
1926 | _ -> failwith
"not possible" in
1927 let (me1fvs
,mb1fvs,ms1fvs
) =
1928 let fvs = [Ast.get_mfvs
header;Ast.get_mfvs
body] in
1929 match seq_fvs new2_mquantified fvs with
1930 [(e1fvs,b1fvs);(s1fvs
,_)] -> (e1fvs,b1fvs,s1fvs
)
1931 | _ -> failwith
"not possible" in
1933 quantify guard
e1fvs (make_match header) in
1934 let new3_quantified = union b1fvs new2_quantified in
1935 let new3_mquantified = union mb1fvs new2_mquantified in
1937 statement_list body Tail
1938 new3_quantified new3_mquantified label llabel
1939 (Some
(lv,used)) true(*?*) guard
in
1940 quantify guard
b1fvs (make_seq [case_header; body])
1941 | Ast.OptCase
(case_line
) -> failwith
"not supported")
1943 let default_required =
1946 match Ast.unwrap case
with
1947 Ast.CaseLine
(header,_) ->
1948 (match Ast.unwrap
header with
1949 Ast.Default
(_,_) -> true
1953 then function x
-> x
1954 else function x
-> ctl_or (fallpred label
) x
in
1955 let after_pred = aftpred label
in
1956 let body after_branch
=
1959 (quantify guard
b2fvs
1962 (List.fold_left
ctl_and CTL.True
1963 (List.map
ctl_ex case_headers));
1964 List.fold_left
ctl_or_fl no_header case_code])))
1967 (rb_fvs,Ast.get_fresh
rb,Ast.get_inherited
rb,
1968 match Ast.unwrap
rb with
1969 Ast.SeqEnd
(rb) -> Ast.get_mcodekind
rb
1970 | _ -> failwith
"not possible") in
1971 let (switch_header,wrapper
) =
1974 let label_pred = CTL.Pred
(Lib_engine.Label
(lv),CTL.Control
) in
1975 (ctl_and switch_header label_pred,
1976 (function body -> quantify true [lv] body))
1977 else (switch_header,function x
-> x
) in
1979 (end_control_structure b1fvs switch_header body
1980 after_pred (Some
(ctl_ex after_pred)) None
aft after label guard
)
1981 | Ast.FunDecl
(header,lbrace
,decls
,body,rbrace
) ->
1982 let (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,b4fvs
,rbfvs
) =
1985 [Ast.get_fvs
header;Ast.get_fvs lbrace
;Ast.get_fvs decls
;
1986 Ast.get_fvs
body;Ast.get_fvs rbrace
]
1988 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(_,b4fvs
);(rbfvs
,_)] ->
1989 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,b4fvs
,rbfvs
)
1990 | _ -> failwith
"not possible" in
1991 let (mhfvs
,mb1fvs,mlbfvs
,mb2fvs,mb3fvs
,mb4fvs
,mrbfvs
) =
1994 [Ast.get_mfvs
header;Ast.get_mfvs lbrace
;Ast.get_mfvs decls
;
1995 Ast.get_mfvs
body;Ast.get_mfvs rbrace
]
1997 [(hfvs
,b1fvs);(lbfvs
,b2fvs);(_,b3fvs);(_,b4fvs
);(rbfvs
,_)] ->
1998 (hfvs
,b1fvs,lbfvs
,b2fvs,b3fvs,b4fvs
,rbfvs
)
1999 | _ -> failwith
"not possible" in
2000 let function_header = quantify guard hfvs
(make_match header) in
2001 let start_brace = quantify guard lbfvs
(make_match lbrace
) in
2002 let stripped_rbrace =
2003 match Ast.unwrap rbrace
with
2004 Ast.SeqEnd
((data
,info,_,_)) ->
2005 Ast.rewrap rbrace
(Ast.SeqEnd
(Ast.make_mcode data
))
2006 | _ -> failwith
"unexpected close brace" in
2008 let exit = CTL.Pred
(Lib_engine.Exit
,CTL.Control
) in
2009 let errorexit = CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
) in
2010 let fake_brace = CTL.Pred
(Lib_engine.FakeBrace
,CTL.Control
) in
2012 (quantify guard rbfvs
(make_match rbrace
))
2014 (* the following finds the beginning of the fake braces,
2015 if there are any, not completely sure how this works.
2016 sse the examples sw and return *)
2017 (ctl_back_ex (ctl_not fake_brace))
2018 (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in
2019 let new_quantified3 =
2020 Common.union_set
b1fvs
2021 (Common.union_set
b2fvs (Common.union_set
b3fvs quantified
)) in
2022 let new_quantified4 = Common.union_set b4fvs
new_quantified3 in
2023 let new_mquantified3 =
2024 Common.union_set
mb1fvs
2025 (Common.union_set
mb2fvs
2026 (Common.union_set mb3fvs minus_quantified
)) in
2027 let new_mquantified4 = Common.union_set mb4fvs
new_mquantified3 in
2029 match (Ast.undots decls
,Ast.undots
body,contains_modif rbrace
) with
2030 ([],[body],false) ->
2031 (match Ast.unwrap
body with
2032 Ast.Nest
(stmt_dots
,[],multi
,_,_) ->
2034 then None
(* not sure how to optimize this case *)
2035 else Some
(Common.Left stmt_dots
)
2036 | Ast.Dots
(_,whencode
,_,_) when
2038 (* flow sensitive, so not optimizable *)
2039 (function Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2041 | _ -> true) whencode
) ->
2042 Some
(Common.Right whencode
)
2047 Some
(Common.Left stmt_dots
) ->
2048 (* special case for function header + body - header is unambiguous
2049 and unique, so we can just look for the nested body anywhere
2052 (CTL.FORWARD
,guard_to_strict guard
,start_brace,
2053 statement_list stmt_dots
2054 (* discards match on right brace, but don't need it *)
2055 (Guard
(make_seq_after end_brace after
))
2056 new_quantified4 new_mquantified4
2057 None llabel slabel
true guard
)
2058 | Some
(Common.Right whencode
) ->
2059 (* try to be more efficient for the case where the body is just
2060 ... Perhaps this is too much of a special case, but useful
2061 for dropping a parameter and checking that it is never used. *)
2073 Ast.WhenAlways
(s) -> prev
2074 | Ast.WhenNot
(sl
) ->
2076 statement_list sl Tail
2077 new_quantified4 new_mquantified4
2078 label llabel slabel
true true in
2080 | Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2081 failwith
"unexpected"
2082 | Ast.WhenModifier
(Ast.WhenAny
) -> CTL.False
2083 | Ast.WhenModifier
(_) -> prev
)
2084 CTL.False whencode
))
2088 Ast.WhenAlways
(s) ->
2091 new_quantified4 new_mquantified4
2092 label llabel slabel
true in
2094 | Ast.WhenNot
(sl
) -> prev
2095 | Ast.WhenNotTrue
(_) | Ast.WhenNotFalse
(_) ->
2096 failwith
"unexpected"
2097 | Ast.WhenModifier
(Ast.WhenAny
) -> CTL.True
2098 | Ast.WhenModifier
(_) -> prev
)
2099 CTL.True whencode
) in
2100 ctl_au leftarg (make_match stripped_rbrace)]
2104 quantify guard
b3fvs
2105 (statement_list decls
2107 (quantify guard b4fvs
2108 (statement_list body
2109 (After
(make_seq_after end_brace after
))
2110 new_quantified4 new_mquantified4
2111 None llabel slabel
true guard
)))
2112 new_quantified3 new_mquantified3 None llabel slabel
2114 quantify guard
b1fvs
2115 (make_seq [function_header; quantify guard
b2fvs body_code])
2116 | Ast.Define
(header,body) ->
2117 let (hfvs
,bfvs,bodyfvs
) =
2118 match seq_fvs quantified
[Ast.get_fvs
header;Ast.get_fvs
body]
2120 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2121 | _ -> failwith
"not possible" in
2122 let (mhfvs
,mbfvs
,mbodyfvs
) =
2123 match seq_fvs minus_quantified
[Ast.get_mfvs
header;Ast.get_mfvs
body]
2125 [(hfvs
,b1fvs);(bodyfvs
,_)] -> (hfvs
,b1fvs,bodyfvs
)
2126 | _ -> failwith
"not possible" in
2127 let define_header = quantify guard hfvs
(make_match header) in
2129 statement_list body after
2130 (Common.union_set
bfvs quantified
)
2131 (Common.union_set mbfvs minus_quantified
)
2132 None llabel slabel
true guard
in
2133 quantify guard
bfvs (make_seq [define_header; body_code])
2134 | Ast.OptStm
(stm
) ->
2135 failwith
"OptStm should have been compiled away\n"
2136 | Ast.UniqueStm
(stm
) -> failwith
"arities not yet supported"
2137 | _ -> failwith
"not supported" in
2138 if guard
or !dots_done
2141 do_between_dots stmt
term after quantified minus_quantified
2142 label llabel slabel guard
2144 (* term is the translation of stmt *)
2145 and do_between_dots stmt
term after quantified minus_quantified
2146 label llabel slabel guard
=
2147 match Ast.get_dots_bef_aft stmt
with
2148 Ast.AddingBetweenDots
(brace_term
,n
)
2149 | Ast.DroppingBetweenDots
(brace_term
,n
) ->
2151 statement brace_term after quantified minus_quantified
2152 label llabel slabel guard
in
2153 let v = Printf.sprintf
"_r_%d" n
in
2154 let case1 = ctl_and CTL.NONSTRICT
(CTL.Ref
v) match_brace in
2155 let case2 = ctl_and CTL.NONSTRICT
(ctl_not (CTL.Ref
v)) term in
2158 (ctl_back_ex (ctl_or (truepred label
) (inlooppred label
)))
2159 (ctl_back_ex (ctl_back_ex (falsepred label
))),
2161 | Ast.NoDots
-> term
2163 (* un_process_bef_aft is because we don't want to do transformation in this
2164 code, and thus don't case about braces before or after it *)
2165 and process_bef_aft quantified minus_quantified label llabel slabel guard
=
2167 Ast.WParen
(re
,n
) ->
2168 let paren_pred = CTL.Pred
(Lib_engine.Paren n
,CTL.Control
) in
2169 let s = guard_to_strict guard
in
2170 quantify true (get_unquantified quantified
[n
])
2171 (ctl_and s (make_raw_match None guard re
) paren_pred)
2173 statement
s Tail quantified minus_quantified label llabel slabel guard
2174 | Ast.Other_dots
d ->
2175 statement_list d Tail quantified minus_quantified
2176 label llabel slabel
true guard
2178 (* --------------------------------------------------------------------- *)
2179 (* cleanup: convert AX to EX for pdots.
2180 Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])
2181 This is what we wanted in the first place, but it wasn't possible to make
2182 because the AX and its argument are not created in the same place.
2184 (* also cleanup XX, which is a marker for the case where the programmer
2185 specifies to change the quantifier on .... Assumed to only occur after one AX
2186 or EX, or at top level. *)
2189 let c = match c with CTL.XX
(c) -> c | _ -> c in
2191 CTL.False
-> CTL.False
2192 | CTL.True
-> CTL.True
2193 | CTL.Pred
(p
) -> CTL.Pred
(p
)
2194 | CTL.Not
(phi
) -> CTL.Not
(cleanup phi
)
2195 | CTL.Exists
(keep
,v,phi
) -> CTL.Exists
(keep
,v,cleanup phi
)
2196 | CTL.AndAny
(dir
,s,phi1
,phi2
) ->
2197 CTL.AndAny
(dir
,s,cleanup phi1
,cleanup phi2
)
2198 | CTL.HackForStmt
(dir
,s,phi1
,phi2
) ->
2199 CTL.HackForStmt
(dir
,s,cleanup phi1
,cleanup phi2
)
2200 | CTL.And
(s,phi1
,phi2
) -> CTL.And
(s,cleanup phi1
,cleanup phi2
)
2201 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(cleanup phi1
,cleanup phi2
)
2202 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(cleanup phi1
,cleanup phi2
)
2203 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(cleanup phi1
,cleanup phi2
)
2204 | CTL.AF
(dir
,s,phi1
) -> CTL.AF
(dir
,s,cleanup phi1
)
2205 | CTL.AX
(CTL.FORWARD
,s,
2207 CTL.And
(CTL.NONSTRICT
,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
),
2208 CTL.EU
(CTL.FORWARD
,e4
,e5
)))) ->
2210 CTL.And
(CTL.NONSTRICT
,
2211 CTL.AX
(CTL.FORWARD
,s,CTL.AU
(CTL.FORWARD
,s2
,e2
,e3
)),
2212 CTL.EX
(CTL.FORWARD
,CTL.EU
(CTL.FORWARD
,e4
,e5
))))
2213 | CTL.AX
(dir
,s,CTL.XX
(phi
)) -> CTL.EX
(dir
,cleanup phi
)
2214 | CTL.EX
(dir
,CTL.XX
((CTL.AU
(_,s,_,_)) as phi
)) ->
2215 CTL.AX
(dir
,s,cleanup phi
)
2216 | CTL.XX
(phi
) -> failwith
"bad XX"
2217 | CTL.AX
(dir
,s,phi1
) -> CTL.AX
(dir
,s,cleanup phi1
)
2218 | CTL.AG
(dir
,s,phi1
) -> CTL.AG
(dir
,s,cleanup phi1
)
2219 | CTL.EF
(dir
,phi1
) -> CTL.EF
(dir
,cleanup phi1
)
2220 | CTL.EX
(dir
,phi1
) -> CTL.EX
(dir
,cleanup phi1
)
2221 | CTL.EG
(dir
,phi1
) -> CTL.EG
(dir
,cleanup phi1
)
2222 | CTL.AW
(dir
,s,phi1
,phi2
) -> CTL.AW
(dir
,s,cleanup phi1
,cleanup phi2
)
2223 | CTL.AU
(dir
,s,phi1
,phi2
) -> CTL.AU
(dir
,s,cleanup phi1
,cleanup phi2
)
2224 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,cleanup phi1
,cleanup phi2
)
2225 | CTL.Let
(x,phi1
,phi2
) -> CTL.Let
(x,cleanup phi1
,cleanup phi2
)
2226 | CTL.LetR
(dir
,x,phi1
,phi2
) -> CTL.LetR
(dir
,x,cleanup phi1
,cleanup phi2
)
2227 | CTL.Ref
(s) -> CTL.Ref
(s)
2228 | CTL.Uncheck
(phi1
) -> CTL.Uncheck
(cleanup phi1
)
2229 | CTL.InnerAnd
(phi1
) -> CTL.InnerAnd
(cleanup phi1
)
2231 (* --------------------------------------------------------------------- *)
2232 (* Function declaration *)
2234 let top_level name
(ua
,pos) t
=
2235 let ua = List.filter
(function (nm,_) -> nm = name
) ua in
2237 saved := Ast.get_saved t
;
2238 let quantified = Common.minus_set
ua pos in
2239 quantify false quantified
2240 (match Ast.unwrap t
with
2241 Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
2243 let unopt = elim_opt.V.rebuilder_statement stmt
in
2244 let unopt = preprocess_dots_e unopt in
2245 cleanup(statement
unopt VeryEnd
quantified [] None None None
false)
2246 | Ast.CODE
(stmt_dots
) ->
2247 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
2248 let unopt = preprocess_dots unopt in
2249 let starts_with_dots =
2250 match Ast.undots stmt_dots
with
2252 (match Ast.unwrap
d with
2253 Ast.Dots
(_,_,_,_) | Ast.Circles
(_,_,_,_)
2254 | Ast.Stars
(_,_,_,_) -> true
2257 let starts_with_brace =
2258 match Ast.undots stmt_dots
with
2260 (match Ast.unwrap
d with
2265 statement_list unopt VeryEnd
quantified [] None None None
2268 (if starts_with_dots
2270 (* EX because there is a loop on enter/top *)
2271 ctl_and CTL.NONSTRICT
(toppred None
) (ctl_ex res)
2272 else if starts_with_brace
2274 ctl_and CTL.NONSTRICT
2275 (ctl_not(CTL.EX
(CTL.BACKWARD
,(funpred None
)))) res
2277 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords")
2279 (* --------------------------------------------------------------------- *)
2282 let asttoctlz (name
,(_,_,exists_flag
),l) used_after positions
=
2285 (match exists_flag
with
2286 Ast.Exists
-> exists := Exists
2287 | Ast.Forall
-> exists := Forall
2288 | Ast.ReverseForall
-> exists := ReverseForall
2289 | Ast.Undetermined
->
2290 exists := if !Flag.sgrep_mode2
then Exists
else Forall
);
2292 let (l,used_after) =
2296 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
2297 (List.combine
l (List.combine
used_after positions
))) in
2298 let res = List.map2
(top_level name
) used_after l in
2302 let asttoctl r
used_after positions
=
2304 Ast.ScriptRule
_ -> []
2305 | Ast.CocciRule
(a,b
,c,_) -> asttoctlz (a,b
,c) used_after positions
2307 let pp_cocci_predicate (pred
,modif
) =
2308 Pretty_print_engine.pp_predicate pred
2310 let cocci_predicate_to_string (pred
,modif
) =
2311 Pretty_print_engine.predicate_to_string pred