2 * Copyright 2012, INRIA
3 * Julia Lawall, Gilles Muller
4 * Copyright 2010-2011, INRIA, University of Copenhagen
5 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
6 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
7 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
8 * This file is part of Coccinelle.
10 * Coccinelle is free software: you can redistribute it and/or modify
11 * it under the terms of the GNU General Public License as published by
12 * the Free Software Foundation, according to version 2 of the License.
14 * Coccinelle is distributed in the hope that it will be useful,
15 * but WITHOUT ANY WARRANTY; without even the implied warranty of
16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 * GNU General Public License for more details.
19 * You should have received a copy of the GNU General Public License
20 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
22 * The authors reserve the right to distribute this or future versions of
23 * Coccinelle under other licenses.
27 (* true = don't see all matched nodes, only modified ones *)
28 let onlyModif = ref true(*false*)
29 (* set to true for line numbers in the output of ctl_engine *)
30 let line_numbers = ref false
31 (* if true, only eg if header is included in not for ...s *)
32 let simple_get_end = ref false(*true*)
34 (* Question: where do we put the existential quantifier for or. At the
35 moment, let it float inwards. *)
37 (* nest shouldn't overlap with what comes after. not checked for. *)
39 module Ast
= Ast_cocci
40 module V
= Visitor_ast
44 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
46 type cocci_predicate
= Lib_engine.predicate
* string Ast_ctl.modif
48 (cocci_predicate
,string, Wrapper_ctl.info
) Ast_ctl.generic_ctl
51 let aftpred = (Lib_engine.After
,CTL.Control
)
52 let retpred = (Lib_engine.Return
,CTL.Control
)
53 let exitpred = (Lib_engine.ErrorExit
,CTL.Control
)
55 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
56 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
58 (* --------------------------------------------------------------------- *)
62 (match CTL.unwrap f
with
65 | CTL.Pred
(p
) as x
-> x
66 | CTL.Not
(phi
) -> CTL.Not
(drop_vs phi
)
67 | CTL.Exists
(v
,phi
) ->
68 (match CTL.unwrap phi
with
69 CTL.Pred
((x
,CTL.Modif v1
)) when v
= v1
-> CTL.Pred
((x
,CTL.Control
))
70 | _
-> CTL.Exists
(v
,drop_vs phi
))
71 | CTL.And
(phi1
,phi2
) -> CTL.And
(drop_vs phi1
,drop_vs phi2
)
72 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(drop_vs phi1
,drop_vs phi2
)
73 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(drop_vs phi1
,drop_vs phi2
)
74 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(drop_vs phi1
,drop_vs phi2
)
75 | CTL.AF
(dir
,phi1
,phi2
) -> CTL.AF
(dir
,drop_vs phi1
,drop_vs phi2
)
76 | CTL.AX
(dir
,phi
) -> CTL.AX
(dir
,drop_vs phi
)
77 | CTL.AG
(dir
,phi
) -> CTL.AG
(dir
,drop_vs phi
)
78 | CTL.AU
(dir
,phi1
,phi2
,phi3
,phi4
) ->
79 CTL.AU
(dir
,drop_vs phi1
,drop_vs phi2
,drop_vs phi3
,drop_vs phi4
)
80 | CTL.EF
(dir
,phi
) -> CTL.EF
(dir
,drop_vs phi
)
81 | CTL.EX
(dir
,phi
) -> CTL.EX
(dir
,drop_vs phi
)
82 | CTL.EG
(dir
,phi
) -> CTL.EG
(dir
,drop_vs phi
)
83 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,drop_vs phi1
,drop_vs phi2
)
84 | CTL.Ref
(v
) as x
-> x
85 | CTL.Let
(v
,term1
,body
) -> CTL.Let
(v
,drop_vs term1
,drop_vs body
))
87 (* --------------------------------------------------------------------- *)
89 let wrap n ctl
= (ctl
,n
)
92 wrap 0 (CTL.Or
(wrap 0 (CTL.Pred
aftpred),wrap 0 (CTL.Pred
exitpred)))
94 let wrapImplies n
(x
,y
) = wrap n
(CTL.Implies
(x
,y
))
95 let wrapExists n
(x
,y
) = wrap n
(CTL.Exists
(x
,y
))
96 let wrapAnd n
(x
,y
) = wrap n
(CTL.And
(x
,y
))
97 let wrapOr n
(x
,y
) = wrap n
(CTL.Or
(x
,y
))
98 let wrapSeqOr n
(x
,y
) = wrap n
(CTL.SeqOr
(x
,y
))
99 let wrapAU n
(x
,y
) = wrap n
(CTL.AU
(CTL.FORWARD
,x
,y
,drop_vs x
,drop_vs y
))
100 let wrapEU n
(x
,y
) = wrap n
(CTL.EU
(CTL.FORWARD
,x
,y
))
101 let wrapAX n
(x
) = wrap n
(CTL.AX
(CTL.FORWARD
,x
))
102 let wrapBackAX n
(x
) = wrap n
(CTL.AX
(CTL.BACKWARD
,x
))
103 let wrapEX n
(x
) = wrap n
(CTL.EX
(CTL.FORWARD
,x
))
104 let wrapBackEX n
(x
) = wrap n
(CTL.EX
(CTL.BACKWARD
,x
))
105 let wrapAG n
(x
) = wrap n
(CTL.AG
(CTL.FORWARD
,x
))
106 let wrapEG n
(x
) = wrap n
(CTL.EG
(CTL.FORWARD
,x
))
107 let wrapAF n
(x
) = wrap n
(CTL.AF
(CTL.FORWARD
,x
,drop_vs x
))
108 let wrapEF n
(x
) = wrap n
(CTL.EF
(CTL.FORWARD
,x
))
109 let wrapNot n
(x
) = wrap n
(CTL.Not
(x
))
110 let wrapPred n
(x
) = wrap n
(CTL.Pred
(x
))
111 let wrapLet n
(x
,y
,z
) = wrap n
(CTL.Let
(x
,y
,z
))
112 let wrapRef n
(x
) = wrap n
(CTL.Ref
(x
))
114 (* --------------------------------------------------------------------- *)
116 let get_option fn
= function
118 | Some x
-> Some
(fn x
)
120 let get_list_option fn
= function
124 (* --------------------------------------------------------------------- *)
125 (* --------------------------------------------------------------------- *)
126 (* Eliminate OptStm *)
128 (* for optional thing with nothing after, should check that the optional thing
129 never occurs. otherwise the matching stops before it occurs *)
132 let donothing r k e
= k e
in
135 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
137 let rec dots_list unwrapped wrapped
=
138 match (unwrapped
,wrapped
) with
141 | (Ast.Dots
(_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
) as u
)::urest
,
143 | (Ast.Nest
(_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
) as u
)::urest
,
145 let l = Ast.get_line stm
in
146 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
147 let new_rest2 = dots_list urest rest
in
148 let fv_rest1 = fvlist new_rest1 in
149 let fv_rest2 = fvlist new_rest2 in
150 [d0
;(Ast.Disj
[(Ast.DOTS
(new_rest1),l,fv_rest1,Ast.NoDots
);
151 (Ast.DOTS
(new_rest2),l,fv_rest2,Ast.NoDots
)],
152 l,fv_rest1,Ast.NoDots
)]
154 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
155 let l = Ast.get_line stm
in
156 let new_rest1 = dots_list urest rest
in
157 let new_rest2 = stm
::new_rest1 in
158 let fv_rest1 = fvlist new_rest1 in
159 let fv_rest2 = fvlist new_rest2 in
160 [(Ast.Disj
[(Ast.DOTS
(new_rest2),l,fv_rest2,Ast.NoDots
);
161 (Ast.DOTS
(new_rest1),l,fv_rest1,Ast.NoDots
)],
162 l,fv_rest2,Ast.NoDots
)]
164 | ([Ast.Dots
(_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
165 let l = Ast.get_line stm
in
166 let fv_stm = Ast.get_fvs stm
in
167 let fv_d1 = Ast.get_fvs d1
in
168 let fv_both = Common.union_set
fv_stm fv_d1 in
169 [d1
;(Ast.Disj
[(Ast.DOTS
([stm
]),l,fv_stm,Ast.NoDots
);
170 (Ast.DOTS
([d1
]),l,fv_d1,Ast.NoDots
)],
171 l,fv_both,Ast.NoDots
)]
173 | ([Ast.Nest
(_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
174 let l = Ast.get_line stm
in
175 let rw = Ast.rewrap stm
in
176 let rwd = Ast.rewrap stm
in
178 Ast.Dots
(("...",{ Ast.line
= 0; Ast.column
= 0 },
179 Ast.CONTEXT
(Ast.NOTHING
)),
181 [d1
;rw(Ast.Disj
[rwd(Ast.DOTS
([stm
]));
182 (Ast.DOTS
([rw dots]),l,[],Ast.NoDots
)])]
184 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
185 | _
-> failwith
"not possible" in
187 let stmtdotsfn r k d
=
190 (match Ast.unwrap
d with
191 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
192 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
193 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
196 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
197 donothing donothing stmtdotsfn
198 donothing donothing donothing donothing donothing donothing donothing
199 donothing donothing donothing
201 (* --------------------------------------------------------------------- *)
202 (* Count depth of braces. The translation of a closed brace appears deeply
203 nested within the translation of the sequence term, so the name of the
204 paren var has to take into account the names of the nested braces. On the
205 other hand the close brace does not escape, so we don't have to take into
206 account other paren variable names. *)
208 (* called repetitively, which is inefficient, but less trouble than adding a
209 new field to Seq and FunDecl *)
210 let count_nested_braces s
=
211 let bind x y
= max x y
in
212 let option_default = 0 in
213 let stmt_count r k s
=
214 match Ast.unwrap s
with
215 Ast.Seq
(_
,_
,_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
,_
,_
) -> (k s
) + 1
217 let donothing r k e
= k e
in
219 let recursor = V.combiner
bind option_default
220 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
221 donothing donothing donothing
222 donothing donothing donothing donothing donothing donothing
223 donothing stmt_count donothing donothing in
224 "p"^
(string_of_int
(recursor.V.combiner_statement s
))
226 (* --------------------------------------------------------------------- *)
233 Printf.sprintf
"v%d" c
236 let fresh_label_var s
=
238 labctr := !labctr + 1;
239 Printf.sprintf
"%s%d" s
c
242 let fresh_let_var _
=
245 Printf.sprintf
"l%d" c
248 let fresh_metavar _
=
250 (*sctr := !sctr + 1;*)
251 Printf.sprintf
"_S%d" c
253 let get_unquantified quantified vars
=
254 List.filter
(function x
-> not
(List.mem x quantified
)) vars
256 type after
= After
of formula
| Guard
of formula
| Tail
259 let rec loop = function
260 [] -> failwith
"not possible"
262 | x
::xs
-> wrapAnd n
(x
,wrapAX n
(loop xs
)) in
265 let make_seq_after2 n first
= function
266 After rest
-> wrapAnd n
(first
,wrapAX n
(wrapAX n rest
))
269 let make_seq_after n first
= function
270 After rest
-> make_seq n
[first
;rest
]
273 let a2n = function After f
-> Guard f
| x
-> x
275 let and_opt n first
= function
276 After rest
-> wrapAnd n
(first
,rest
)
280 let bind x y
= x
or y
in
281 let option_default = false in
282 let mcode r
(_
,_
,kind
) =
285 | Ast.PLUS
-> failwith
"not possible"
286 | Ast.CONTEXT
(info
) -> not
(info
= Ast.NOTHING
) in
287 let do_nothing r k e
= k e
in
289 V.combiner
bind option_default
290 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
291 do_nothing do_nothing do_nothing
292 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
293 do_nothing do_nothing do_nothing do_nothing in
294 recursor.V.combiner_rule_elem
296 let make_match n guard used_after code
=
298 then wrapPred n
(Lib_engine.Match
(code
),CTL.Control
)
300 let v = fresh_var() in
301 if contains_modif code
302 then wrapExists n
(v,wrapPred n
(Lib_engine.Match
(code
),CTL.Modif
v))
305 List.exists
(function x
-> List.mem x used_after
) (Ast.get_fvs code
) in
306 if !onlyModif && not
any_used_after
307 then wrapPred n
(Lib_engine.Match
(code
),CTL.Control
)
308 else wrapExists n
(v,wrapPred n
(Lib_engine.Match
(code
),CTL.UnModif
v))
310 let make_raw_match n code
= wrapPred n
(Lib_engine.Match
(code
),CTL.Control
)
312 let rec seq_fvs quantified
= function
315 let t1fvs = get_unquantified quantified fv1
in
317 List.fold_left
Common.union_set
[]
318 (List.map
(get_unquantified quantified
) fvs
) in
319 let bothfvs = Common.inter_set
t1fvs termfvs in
320 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
321 let new_quantified = Common.union_set
bothfvs quantified
in
322 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
324 let seq_fvs2 quantified fv1 fv2
=
325 match seq_fvs quantified
[fv1
;fv2
] with
326 [(t1fvs,bfvs
);(t2fvs
,[])] -> (t1fvs,bfvs
,t2fvs
)
327 | _
-> failwith
"impossible"
329 let seq_fvs3 quantified fv1 fv2 fv3
=
330 match seq_fvs quantified
[fv1
;fv2
;fv3
] with
331 [(t1fvs,b12fvs
);(t2fvs
,b23fvs
);(t3fvs
,[])] ->
332 (t1fvs,b12fvs
,t2fvs
,b23fvs
,t3fvs
)
333 | _
-> failwith
"impossible"
335 let seq_fvs4 quantified fv1 fv2 fv3 fv4
=
336 match seq_fvs quantified
[fv1
;fv2
;fv3
;fv4
] with
337 [(t1fvs,b12fvs
);(t2fvs
,b23fvs
);(t3fvs
,b34fvs
);(t4fvs
,[])] ->
338 (t1fvs,b12fvs
,t2fvs
,b23fvs
,t3fvs
,b34fvs
,t4fvs
)
339 | _
-> failwith
"impossible"
341 let seq_fvs5 quantified fv1 fv2 fv3 fv4 fv5
=
342 match seq_fvs quantified
[fv1
;fv2
;fv3
;fv4
;fv5
] with
343 [(t1fvs,b12fvs
);(t2fvs
,b23fvs
);(t3fvs
,b34fvs
);(t4fvs
,b45fvs
);(t5fvs
,[])] ->
344 (t1fvs,b12fvs
,t2fvs
,b23fvs
,t3fvs
,b34fvs
,t4fvs
,b45fvs
,t5fvs
)
345 | _
-> failwith
"impossible"
348 List.fold_right
(function cur
-> function code
-> wrapExists n
(cur
,code
))
350 let intersectll lst nested_list
=
351 List.filter
(function x
-> List.exists
(List.mem x
) nested_list
) lst
353 (* --------------------------------------------------------------------- *)
354 (* annotate dots with before and after neighbors *)
356 let rec get_before sl a
=
357 match Ast.unwrap sl
with
363 let (e
,ea
) = get_before_e e a
in
364 let (sl
,sla
) = loop sl ea
in
366 let (l,a
) = loop x a
in
367 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
368 | Ast.CIRCLES
(x
) -> failwith
"not supported"
369 | Ast.STARS
(x
) -> failwith
"not supported"
371 and get_before_e s a
=
372 match Ast.unwrap s
with
373 Ast.Dots
(d,Ast.NoWhen
,t
) ->
374 (Ast.rewrap s
(Ast.Dots
(d,Ast.NoWhen
,a
@t
)),a
)
375 | Ast.Dots
(d,Ast.WhenNot w
,t
) ->
376 let (w
,_
) = get_before w
[] in
377 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenNot w
,a
@t
)),a
)
378 | Ast.Dots
(d,Ast.WhenAlways w
,t
) ->
379 let (w
,_
) = get_before_e w
[] in
380 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenAlways w
,a
@t
)),a
)
381 | Ast.Nest
(stmt_dots
,w
,t
) ->
382 let (w
,_
) = List.split
(List.map
(function s
-> get_before s
[]) w
) in
383 let (sd
,_
) = get_before stmt_dots a
in
389 Unify_ast.unify_statement_dots
390 (Ast.rewrap s
(Ast.DOTS
([a]))) stmt_dots
in
392 Unify_ast.MAYBE
-> false
394 | Ast.Other_dots
a ->
395 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
397 Unify_ast.MAYBE
-> false
401 (Ast.rewrap s
(Ast.Nest
(sd
,w
,a@t
)),[Ast.Other_dots stmt_dots
])
402 | Ast.Disj
(stmt_dots_list
) ->
404 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
405 (Ast.rewrap s
(Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
407 (match Ast.unwrap ast
with
408 Ast.MetaStmt
(_
,_
,_
) -> (s
,[])
409 | _
-> (s
,[Ast.Other s
]))
410 | Ast.Seq
(lbrace
,decls
,dots,body
,rbrace
) ->
411 let index = count_nested_braces s
in
412 let (de
,dea
) = get_before decls
[Ast.WParen
(lbrace
,index)] in
413 let (bd
,_
) = get_before body dea
in
414 (Ast.rewrap s
(Ast.Seq
(lbrace
,de
,dots,bd
,rbrace
)),
415 [Ast.WParen
(rbrace
,index)])
416 | Ast.IfThen
(ifheader
,branch
,aft
) ->
417 let (br
,_
) = get_before_e branch
[] in
418 (Ast.rewrap s
(Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other s
])
419 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
420 let (br1
,_
) = get_before_e branch1
[] in
421 let (br2
,_
) = get_before_e branch2
[] in
422 (Ast.rewrap s
(Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other s
])
423 | Ast.While
(header
,body
,aft
) ->
424 let (bd
,_
) = get_before_e body
[] in
425 (Ast.rewrap s
(Ast.While
(header
,bd
,aft
)),[Ast.Other s
])
426 | Ast.For
(header
,body
,aft
) ->
427 let (bd
,_
) = get_before_e body
[] in
428 (Ast.rewrap s
(Ast.For
(header
,bd
,aft
)),[Ast.Other s
])
429 | Ast.FunDecl
(header
,lbrace
,decls
,dots,body
,rbrace
) ->
430 let index = count_nested_braces s
in
431 let (de
,dea
) = get_before decls
[Ast.WParen
(lbrace
,index)] in
432 let (bd
,_
) = get_before body dea
in
433 (Ast.rewrap s
(Ast.FunDecl
(header
,lbrace
,de
,dots,bd
,rbrace
)),[])
434 | _
-> failwith
"not supported"
436 let rec get_after sl
a =
437 match Ast.unwrap sl
with
443 let (sl
,sla
) = loop sl
in
444 let (e
,ea
) = get_after_e e sla
in
446 let (l,a) = loop x
in
447 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
448 | Ast.CIRCLES
(x
) -> failwith
"not supported"
449 | Ast.STARS
(x
) -> failwith
"not supported"
451 and get_after_e s
a =
452 match Ast.unwrap s
with
453 Ast.Dots
(d,Ast.NoWhen
,t
) ->
454 (Ast.rewrap s
(Ast.Dots
(d,Ast.NoWhen
,a@t
)),a)
455 | Ast.Dots
(d,Ast.WhenNot w
,t
) ->
456 let (w
,_
) = get_after w
[] in
457 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenNot w
,a@t
)),a)
458 | Ast.Dots
(d,Ast.WhenAlways w
,t
) ->
459 let (w
,_
) = get_after_e w
[] in
460 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenAlways w
,a@t
)),a)
461 | Ast.Nest
(stmt_dots
,w
,t
) ->
462 let (w
,_
) = List.split
(List.map
(function s
-> get_after s
[]) w
) in
463 let (sd
,_
) = get_after stmt_dots
a in
469 Unify_ast.unify_statement_dots
470 (Ast.rewrap s
(Ast.DOTS
([a]))) stmt_dots
in
472 Unify_ast.MAYBE
-> false
474 | Ast.Other_dots
a ->
475 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
477 Unify_ast.MAYBE
-> false
481 (Ast.rewrap s
(Ast.Nest
(sd
,w
,a@t
)),[Ast.Other_dots stmt_dots
])
482 | Ast.Disj
(stmt_dots_list
) ->
484 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
485 (Ast.rewrap s
(Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
487 (match Ast.unwrap ast
with
488 Ast.MetaStmt
(nm
,Ast.SequencibleAfterDots _
,i
) ->
489 (* check after information for metavar optimization *)
490 (* if the error is not desired, could just return [], then
491 the optimization (check for EF) won't take place *)
495 (match Ast.unwrap x
with
496 Ast.Dots
(_
,_
,_
) | Ast.Nest
(_
,_
,_
) ->
498 "dots/nest not allowed before and after stmt metavar"
500 | Ast.Other_dots x
->
501 (match Ast.undots x
with
503 (match Ast.unwrap x
with
504 Ast.Dots
(_
,_
,_
) | Ast.Nest
(_
,_
,_
) ->
506 ("dots/nest not allowed before and after stmt "^
515 (Ast.MetaStmt
(nm
,Ast.SequencibleAfterDots
a,i
)))),[])
516 | Ast.MetaStmt
(_
,_
,_
) -> (s
,[])
517 | _
-> (s
,[Ast.Other s
]))
518 | Ast.Seq
(lbrace
,decls
,dots,body
,rbrace
) ->
519 let index = count_nested_braces s
in
520 let (bd
,bda
) = get_after body
[Ast.WParen
(rbrace
,index)] in
521 let (de
,_
) = get_after decls bda
in
522 (Ast.rewrap s
(Ast.Seq
(lbrace
,de
,dots,bd
,rbrace
)),
523 [Ast.WParen
(lbrace
,index)])
524 | Ast.IfThen
(ifheader
,branch
,aft
) ->
525 let (br
,_
) = get_after_e branch
a in
526 (Ast.rewrap s
(Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other s
])
527 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
528 let (br1
,_
) = get_after_e branch1
a in
529 let (br2
,_
) = get_after_e branch2
a in
530 (Ast.rewrap s
(Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other s
])
531 | Ast.While
(header
,body
,aft
) ->
532 let (bd
,_
) = get_after_e body
a in
533 (Ast.rewrap s
(Ast.While
(header
,bd
,aft
)),[Ast.Other s
])
534 | Ast.For
(header
,body
,aft
) ->
535 let (bd
,_
) = get_after_e body
a in
536 (Ast.rewrap s
(Ast.For
(header
,bd
,aft
)),[Ast.Other s
])
537 | Ast.FunDecl
(header
,lbrace
,decls
,dots,body
,rbrace
) ->
538 let index = count_nested_braces s
in
539 let (bd
,bda
) = get_after body
[Ast.WParen
(rbrace
,index)] in
540 let (de
,_
) = get_after decls bda
in
541 (Ast.rewrap s
(Ast.FunDecl
(header
,lbrace
,de
,dots,bd
,rbrace
)),[])
542 | _
-> failwith
"not supported"
545 let preprocess_dots sl
=
546 let (sl
,_
) = get_before sl
[] in
547 let (sl
,_
) = get_after sl
[] in
550 let preprocess_dots_e sl
=
551 let (sl
,_
) = get_before_e sl
[] in
552 let (sl
,_
) = get_after_e sl
[] in
555 (* --------------------------------------------------------------------- *)
556 (* the main translation loop *)
558 let decl_to_not_decl n
dots stmt
make_match f
=
563 let md = Ast.make_meta_decl
"_d" (Ast.CONTEXT
(Ast.NOTHING
)) in
564 Ast.rewrap
md (Ast.Decl
md) in
565 wrapAU n
(make_match de,
566 wrap n
(CTL.And
(wrap n
(CTL.Not
(make_match de)), f
)))
568 let rec statement_list stmt_list used_after after quantified guard
=
569 let n = if !line_numbers then Ast.get_line stmt_list
else 0 in
570 match Ast.unwrap stmt_list
with
572 let rec loop quantified
= function
573 ([],_
) -> (match after
with After f
-> f
| _
-> wrap n CTL.True
)
574 | ([e
],_
) -> statement e used_after after quantified guard
576 let shared = intersectll fv fvs
in
577 let unqshared = get_unquantified quantified
shared in
578 let new_quantified = Common.union_set
unqshared quantified
in
580 (statement e used_after
(After
(loop new_quantified (sl
,fvs
)))
581 new_quantified guard
)
582 | _
-> failwith
"not possible" in
583 loop quantified
(x
,List.map
Ast.get_fvs x
)
584 | Ast.CIRCLES
(x
) -> failwith
"not supported"
585 | Ast.STARS
(x
) -> failwith
"not supported"
587 and statement stmt used_after after quantified guard
=
589 let n = if !line_numbers then Ast.get_line stmt
else 0 in
590 let wrapExists = wrapExists n in
591 let wrapAnd = wrapAnd n in
592 let wrapOr = wrapOr n in
593 let wrapSeqOr = wrapSeqOr n in
594 let wrapAU = wrapAU n in
595 let wrapAX = wrapAX n in
596 let wrapBackAX = wrapBackAX n in
597 let wrapEX = wrapEX n in
598 let wrapBackEX = wrapBackEX n in
599 let wrapAG = wrapAG n in
600 let wrapAF = wrapAF n in
601 let wrapEF = wrapEF n in
602 let wrapNot = wrapNot n in
603 let wrapPred = wrapPred n in
604 let make_seq = make_seq n in
605 let make_seq_after2 = make_seq_after2 n in
606 let make_seq_after = make_seq_after n in
607 let and_opt = and_opt n in
608 let quantify = quantify n in
609 let make_match = make_match n guard used_after
in
610 let make_raw_match = make_raw_match n in
612 let make_meta_rule_elem d =
613 let nm = fresh_metavar() in
614 Ast.make_meta_rule_elem nm d in
616 match Ast.unwrap stmt
with
618 (match Ast.unwrap ast
with
619 Ast.MetaStmt
((s
,i
,(Ast.CONTEXT
(Ast.BEFOREAFTER
(_
,_
)) as d)),seqible
,_
)
620 | Ast.MetaStmt
((s
,i
,(Ast.CONTEXT
(Ast.AFTER
(_
)) as d)),seqible
,_
) ->
621 let label_var = (*fresh_label_var*) "_lab" in
622 let label_pred = wrapPred(Lib_engine.Label
(label_var),CTL.Control
) in
624 wrapPred(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
625 let matcher d = make_match (make_meta_rule_elem d) in
626 let full_metamatch = matcher d in
627 let first_metamatch =
630 Ast.CONTEXT
(Ast.BEFOREAFTER
(bef
,_
)) ->
631 Ast.CONTEXT
(Ast.BEFORE
(bef
))
632 | Ast.CONTEXT
(_
) -> Ast.CONTEXT
(Ast.NOTHING
)
633 | Ast.MINUS
(_
) | Ast.PLUS
-> failwith
"not possible") in
634 let middle_metamatch =
637 Ast.CONTEXT
(_
) -> Ast.CONTEXT
(Ast.NOTHING
)
638 | Ast.MINUS
(_
) | Ast.PLUS
-> failwith
"not possible") in
642 Ast.CONTEXT
(Ast.BEFOREAFTER
(_
,aft
)) ->
643 Ast.CONTEXT
(Ast.AFTER
(aft
))
644 | Ast.CONTEXT
(_
) -> d
645 | Ast.MINUS
(_
) | Ast.PLUS
-> failwith
"not possible") in
649 [full_metamatch; and_opt (wrapNot(prelabel_pred)) after
] in
653 wrapAU(middle_metamatch,
655 [wrapAnd(last_metamatch,label_pred);
656 and_opt (wrapNot(prelabel_pred)) after
])] in
659 f
(wrapAnd(make_raw_match ast
,
660 wrapOr(left_or,right_or)))) in
663 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
664 quantify (label_var::get_unquantified quantified
[s
])
667 (wrapAnd(wrapNot(wrapBackAX(label_pred)),x
))))
668 | Ast.SequencibleAfterDots
l ->
670 List.map
(process_bef_aft Tail quantified used_after
n) l in
672 List.fold_left
(function x
-> function y
-> wrapOr(x
,y
))
673 (List.hd
afts) (List.tl
afts) in
674 quantify (label_var::get_unquantified quantified
[s
])
675 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
678 wrapAnd(wrapNot(wrapBackAX(label_pred)),x
))))
679 | Ast.NotSequencible
->
680 quantify (label_var::get_unquantified quantified
[s
]) (body id))
682 | Ast.MetaStmt
((s
,i
,d),seqible
,_
) ->
683 let label_var = (*fresh_label_var*) "_lab" in
684 let label_pred = wrapPred(Lib_engine.Label
(label_var),CTL.Control
) in
686 wrapPred(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
687 let matcher d = make_match (make_meta_rule_elem d) in
688 let first_metamatch = matcher d in
692 Ast.MINUS
(_
) -> Ast.MINUS
([])
693 | Ast.CONTEXT
(_
) -> Ast.CONTEXT
(Ast.NOTHING
)
694 | Ast.PLUS
-> failwith
"not possible") in
695 (* first_nodea and first_nodeb are separated here and above to
696 improve let sharing - only first_nodea is unique to this site *)
697 let first_nodeb = first_metamatch in
698 let rest_nodes = wrapAnd(rest_metamatch,prelabel_pred) in
699 let last_node = and_opt (wrapNot(prelabel_pred)) after
in
706 [first_nodeb; wrapAU(rest_nodes,last_node)])))) in
708 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
709 quantify (label_var::get_unquantified quantified
[s
])
711 (function x
-> wrapAnd(wrapNot(wrapBackAX(label_pred)),x
)))
712 | Ast.SequencibleAfterDots
l ->
714 List.map
(process_bef_aft Tail quantified used_after
n) l in
716 List.fold_left
(function x
-> function y
-> wrapOr(x
,y
))
717 (List.hd
afts) (List.tl
afts) in
718 quantify (label_var::get_unquantified quantified
[s
])
719 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
722 wrapAnd(wrapNot(wrapBackAX(label_pred)),x
))))
723 | Ast.NotSequencible
->
724 quantify (label_var::get_unquantified quantified
[s
])
725 (body (function x
-> x
)))
727 let stmt_fvs = Ast.get_fvs stmt
in
728 let fvs = get_unquantified quantified
stmt_fvs in
729 let between_dots = Ast.get_dots_bef_aft stmt
in
730 let term = make_match ast
in
732 match between_dots with
733 Ast.BetweenDots brace_term
->
734 (match Ast.unwrap brace_term
with
735 Ast.Atomic
(brace_ast
) ->
740 (wrapPred(Lib_engine.TrueBranch
,CTL.Control
)),
742 (wrapBackEX(wrapPred(Lib_engine.FalseBranch
,
744 make_match brace_ast
) in
750 (wrapPred(Lib_engine.TrueBranch
,CTL.Control
)),
752 (wrapBackEX(wrapPred(Lib_engine.FalseBranch
,
756 | _
-> failwith
"not possible")
757 | Ast.NoDots
-> term in
758 make_seq_after (quantify fvs term) after
)
759 | Ast.Seq
(lbrace
,decls
,dots,body,rbrace
) ->
760 let (lbfvs
,b1fvs
,_
,b2fvs
,_
,b3fvs
,rbfvs
) =
762 (Ast.get_fvs lbrace
) (Ast.get_fvs decls
)
763 (Ast.get_fvs
body) (Ast.get_fvs rbrace
) in
764 let v = count_nested_braces stmt
in
765 let paren_pred = wrapPred(Lib_engine.Paren
v,CTL.Control
) in
767 wrapAnd(quantify lbfvs
(make_match lbrace
),paren_pred) in
769 wrapAnd(quantify rbfvs
(make_match rbrace
),paren_pred) in
770 let new_quantified2 =
771 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
772 let new_quantified3 = Common.union_set b3fvs
new_quantified2 in
778 (statement_list decls used_after
780 (decl_to_not_decl n dots stmt
make_match
782 (statement_list body used_after
783 (After
(make_seq_after end_brace after
))
784 new_quantified3 guard
))))
785 new_quantified2 guard
)]))
786 | Ast.IfThen
(ifheader
,branch
,aft
) ->
788 (* "if (test) thn" becomes:
789 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
791 "if (test) thn; after" becomes:
792 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
798 seq_fvs2 quantified
(Ast.get_fvs ifheader
) (Ast.get_fvs branch
) in
799 let new_quantified = Common.union_set bfvs quantified
in
801 let if_header = quantify efvs
(make_match ifheader
) in
802 (* then branch and after *)
805 [wrapPred(Lib_engine.TrueBranch
,CTL.Control
);
806 statement branch used_after
(a2n after
) new_quantified guard
] in
807 let fall_branch = wrapPred(Lib_engine.FallThrough
,CTL.Control
) in
808 let after_pred = wrapPred(Lib_engine.After
,CTL.Control
) in
809 let (aft_needed
,after_branch
) =
811 Ast.CONTEXT
(Ast.NOTHING
) -> (false,make_seq_after2 after_pred after
)
814 make_seq_after after_pred
816 (make_seq_after (make_match (make_meta_rule_elem aft
))
818 let or_cases = wrapOr(true_branch,wrapOr(fall_branch,after_branch
)) in
820 (match (after
,aft_needed
) with
821 (After _
,_
) (* pattern doesn't end here *)
822 | (_
,true) (* + code added after *) ->
824 (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
825 | _
-> quantify bfvs
(wrapAnd(if_header, wrapAX or_cases)))
827 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
829 (* "if (test) thn else els" becomes:
830 if(test) & AX((TrueBranch & AX thn) v
831 (FalseBranch & AX (else & AX els)) v After)
834 "if (test) thn else els; after" becomes:
835 if(test) & AX((TrueBranch & AX thn) v
836 (FalseBranch & AX (else & AX els)) v
837 (After & AXAX after))
842 Note that we rely on the well-formedness of C programs. For example, we
843 do not use EX to check that there is at least one then branch, because
844 there is always one. And we do not check that there is only one then or
845 else branch, because these again are always the case in a well-formed C
848 let (e1fvs
,b1fvs
,s1fvs
) =
849 seq_fvs2 quantified
(Ast.get_fvs ifheader
) (Ast.get_fvs branch1
) in
850 let (e2fvs
,b2fvs
,s2fvs
) =
851 seq_fvs2 quantified
(Ast.get_fvs ifheader
) (Ast.get_fvs branch2
) in
854 (Common.union_set b1fvs b2fvs
)
855 (Common.inter_set s1fvs s2fvs
) in
856 let exponlyfvs = Common.inter_set e1fvs e2fvs
in
857 let new_quantified = Common.union_set
bothfvs quantified
in
859 let if_header = quantify exponlyfvs (make_match ifheader
) in
860 (* then and else branches *)
863 [wrapPred(Lib_engine.TrueBranch
,CTL.Control
);
864 statement branch1 used_after
(a2n after
) new_quantified guard
] in
865 let false_pred = wrapPred(Lib_engine.FalseBranch
,CTL.Control
) in
868 [false_pred; make_match els
;
869 statement branch2 used_after
(a2n after
) new_quantified guard
] in
870 let after_pred = wrapPred(Lib_engine.After
,CTL.Control
) in
871 let (aft_needed
,after_branch
) =
873 Ast.CONTEXT
(Ast.NOTHING
) -> (false,make_seq_after2 after_pred after
)
876 make_seq_after after_pred
878 (make_seq_after (make_match (make_meta_rule_elem aft
))
880 let or_cases = wrapOr(true_branch,wrapOr(false_branch,after_branch
)) in
882 (match (after
,aft_needed
) with
883 (After _
,_
) (* pattern doesn't end here *)
884 | (_
,true) (* + code added after *) ->
888 wrapAnd(wrapAX or_cases,
889 wrapAnd(wrapEX false_pred,wrapEX after_pred))))
892 (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX false_pred))))
894 | Ast.While
(header
,body,aft
) | Ast.For
(header
,body,aft
) ->
895 (* the translation in this case is similar to that of an if with no else *)
898 seq_fvs2 quantified
(Ast.get_fvs header
) (Ast.get_fvs
body) in
899 let new_quantified = Common.union_set bfvs quantified
in
901 let header = quantify efvs
(make_match header) in
904 [wrapPred(Lib_engine.TrueBranch
,CTL.Control
);
905 statement
body used_after
(a2n after
) new_quantified guard
] in
906 let after_pred = wrapPred(Lib_engine.FallThrough
,CTL.Control
) in
907 let (aft_needed
,after_branch
) =
909 Ast.CONTEXT
(Ast.NOTHING
) -> (false,make_seq_after2 after_pred after
)
912 make_seq_after after_pred
914 (make_seq_after (make_match (make_meta_rule_elem aft
))
916 let or_cases = wrapOr(body,after_branch
) in
918 (match (after
,aft_needed
) with
919 (After _
,_
) (* pattern doesn't end here *)
920 | (_
,true) (* + code added after *) ->
922 (wrapAnd (header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
923 | _
-> quantify bfvs
(wrapAnd(header, wrapAX or_cases)))
925 | Ast.Disj
(stmt_dots_list
) ->
928 (function x
-> statement_list x used_after after quantified guard
)
930 let rec loop = function
931 [] -> wrap n CTL.True
933 | x
::xs
-> wrapSeqOr(x
,loop xs
) in
937 statement_list e used_after (a2n after) quantified true in
940 (function rest -> function cur -> wrapAnd(wrapNot(do_one cur),rest))
942 let process_one nots cur =
943 match Ast.unwrap cur with
945 let on = List.map (function x -> Ast.OrOther_dots x) nots in
946 (match Ast.unwrap x with
950 Printf.printf "a not\n";
951 Pretty_print_cocci.statement_dots x)
955 (Ast.DOTS((Ast.rewrap x (Ast.Dots(d,w,on@t)))::xs)) in
956 statement_list cur used_after after quantified guard
957 | Ast.Nest(sd,w,t) ->
960 (Ast.DOTS((Ast.rewrap x (Ast.Nest(sd,w,on@t)))::xs)) in
961 statement_list cur used_after after quantified guard
964 (statement_list cur used_after after quantified guard))
967 (statement_list cur used_after after quantified guard)
968 | _ -> failwith "CIRCLES, STARS not supported" in
969 let rec loop after = function
970 [] -> failwith "disj shouldn't be empty" (*wrap n CTL.False*)
971 | [(nots
,cur)] -> process_one nots
cur
972 | (nots
,cur)::rest
-> wrapOr(process_one nots
cur, loop after rest
) in
973 loop after
(preprocess_disj stmt_dots_list
)
975 | Ast.Nest
(stmt_dots
,whencode
,befaft
) ->
977 statement_list stmt_dots used_after
(a2n after
) quantified guard
in
982 statement_list sl used_after
(a2n after
) quantified
true)
984 List.fold_left
(function rest
-> function cur -> wrapOr(cur,rest
))
985 (statement_list stmt_dots used_after
(a2n after
) quantified
true)
987 (match (after
,guard
&&(whencode
=[])) with
990 List.map
(process_bef_aft after quantified used_after
n) befaft
in
992 [] -> wrapAF(wrapOr(a,aftret))
997 (function rest
-> function cur -> wrapOr(cur,rest
))
999 wrapAU(left,wrapOr(a,aftret)))
1000 | (After
a,false) ->
1001 let left = wrapOr(dots_pattern,wrapNot udots_pattern) in
1003 List.map
(process_bef_aft after quantified used_after
n) befaft
in
1011 (function rest
-> function cur -> wrapOr(cur,rest
))
1014 wrapAU(left,wrapOr(a,aftret))
1015 | (_
,true) -> wrap n CTL.True
1016 | (_
,false) -> wrapAG(wrapOr(dots_pattern,wrapNot udots_pattern)))
1017 | Ast.Dots
((_
,i
,d),whencodes,t
) ->
1021 (* no need for the fresh metavar, but ... is a bit weird as a
1023 Some
(make_match (make_meta_rule_elem d))
1026 (match whencodes with
1028 | Ast.WhenNot
whencodes ->
1030 (statement_list whencodes used_after
(a2n after
) quantified
1032 | Ast.WhenAlways s
->
1033 [statement s used_after
(a2n after
) quantified
true]) @
1035 (List.map
(process_bef_aft after quantified used_after
n) t
)) in
1037 match whencodes with
1042 (function rest
-> function cur -> wrapAnd(cur,rest
))
1045 match (dot_code,phi2) with (* add - on dots, if any *)
1047 | (Some dotcode
,None
) -> Some dotcode
1048 | (None
,Some whencode
) -> Some whencode
1049 | (Some dotcode
,Some whencode
) -> Some
(wrapAnd (dotcode
,whencode
)) in
1050 let exit = wrap n (CTL.Pred
(Lib_engine.Exit
,CTL.Control
)) in
1051 (* add in the after code to make the result *)
1052 (match (after
,phi3) with
1053 (Tail
,Some whencode
) -> wrapAU(whencode
,wrapOr(exit,aftret))
1054 | (Tail
,None
) -> wrapAF(wrapOr(exit,aftret))
1055 | (After f
,Some whencode
) | (Guard f
,Some whencode
) ->
1056 wrapAU(whencode
,wrapOr(f
,aftret))
1057 | (After f
,None
) | (Guard f
,None
) -> wrapAF(wrapOr(f
,aftret)))
1058 | Ast.FunDecl
(header,lbrace
,decls
,dots,body,rbrace
) ->
1059 let (hfvs
,b1fvs
,lbfvs
,b2fvs
,_
,b3fvs
,_
,b4fvs
,rbfvs
) =
1060 seq_fvs5 quantified
(Ast.get_fvs
header) (Ast.get_fvs lbrace
)
1061 (Ast.get_fvs decls
) (Ast.get_fvs
body) (Ast.get_fvs rbrace
) in
1062 let function_header = quantify hfvs
(make_match header) in
1063 let v = count_nested_braces stmt
in
1064 let paren_pred = wrapPred(Lib_engine.Paren
v,CTL.Control
) in
1066 wrapAnd(quantify lbfvs
(make_match lbrace
),paren_pred) in
1068 let stripped_rbrace =
1069 match Ast.unwrap rbrace
with
1070 Ast.SeqEnd
((data
,info
,_
)) ->
1072 (Ast.SeqEnd
((data
,info
,Ast.CONTEXT
(Ast.NOTHING
))))
1073 | _
-> failwith
"unexpected close brace" in
1074 let exit = wrap n (CTL.Pred
(Lib_engine.Exit
,CTL.Control
)) in
1075 let errorexit = wrap n (CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
)) in
1076 wrapAnd(quantify rbfvs
(make_match rbrace
),
1077 wrapAU(make_match stripped_rbrace,
1078 wrapOr(exit,errorexit))) in
1079 let new_quantified3 =
1080 Common.union_set b1fvs
1081 (Common.union_set b2fvs
(Common.union_set b3fvs quantified
)) in
1082 let new_quantified4 = Common.union_set b4fvs
new_quantified3 in
1092 (statement_list decls used_after
1094 (decl_to_not_decl n dots stmt
1097 (statement_list body used_after
1099 (make_seq_after end_brace after
))
1100 new_quantified4 guard
))))
1101 new_quantified3 guard
)])))])
1102 | Ast.OptStm
(stm
) ->
1103 failwith
"OptStm should have been compiled away\n";
1104 | Ast.UniqueStm
(stm
) ->
1105 failwith
"arities not yet supported"
1106 | Ast.MultiStm
(stm
) ->
1107 failwith
"arities not yet supported"
1108 | _
-> failwith
"not supported"
1110 and process_bef_aft after quantified used_after ln
= function
1111 Ast.WParen
(re
,n) ->
1112 let paren_pred = wrapPred ln
(Lib_engine.Paren
n,CTL.Control
) in
1113 wrapAnd ln
(make_raw_match ln re
,paren_pred)
1114 | Ast.Other s
-> statement s used_after
(a2n after
) quantified
true
1115 | Ast.Other_dots
d -> statement_list d used_after
(a2n after
) quantified
true
1116 | Ast.OrOther_dots
d -> statement_list d used_after Tail quantified
true
1118 (* Returns a triple for each disj element. The first element of the triple is
1119 Some v if the triple element needs a name, and None otherwise. The second
1120 element is a list of names whose negations should be conjuncted with the
1121 term. The third element is the original term *)
1122 and (preprocess_disj
:
1123 Ast.statement
Ast.dots list
->
1124 (Ast.statement
Ast.dots list
* Ast.statement
Ast.dots) list
) =
1130 List.map
(function r
-> Unify_ast.unify_statement_dots
cur r
) rest
in
1131 let processed = preprocess_disj rest
in
1132 if List.exists
(function Unify_ast.MAYBE
-> true | _
-> false) template
1136 (function ((nots,r
) as x
) ->
1137 function Unify_ast.MAYBE
-> (cur::nots,r
) | Unify_ast.NO
-> x
)
1139 else ([], cur) :: processed
1141 (* --------------------------------------------------------------------- *)
1143 Phase 1: Use a hash table to identify formulas that appear more than once.
1144 Phase 2: Replace terms by variables.
1145 Phase 3: Drop lets to the point as close as possible to the uses of their
1149 (Hashtbl.create
(50) :
1150 ((cocci_predicate
,string,Wrapper_ctl.info
) CTL.generic_ctl
,
1151 int ref (* count *) * string ref (* name *) * bool ref (* processed *))
1156 try Hashtbl.find
formula_table phi
1158 let c = (ref 0,ref "",ref false) in
1159 Hashtbl.add
formula_table phi
c;
1163 let rec collect_duplicates f
=
1165 match CTL.unwrap f
with
1169 | CTL.Not
(phi
) -> collect_duplicates phi
1170 | CTL.Exists
(v,phi
) -> collect_duplicates phi
1171 | CTL.And
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1172 | CTL.Or
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1173 | CTL.SeqOr
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1174 | CTL.Implies
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1175 | CTL.AF
(_
,phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1176 | CTL.AX
(_
,phi
) -> collect_duplicates phi
1177 | CTL.AG
(_
,phi
) -> collect_duplicates phi
1178 | CTL.AU
(_
,phi1
,phi2,phi3,phi4
) ->
1179 collect_duplicates phi1
; collect_duplicates phi2;
1180 collect_duplicates phi3; collect_duplicates phi4
1181 | CTL.EF
(_
,phi
) -> collect_duplicates phi
1182 | CTL.EX
(_
,phi
) -> collect_duplicates phi
1183 | CTL.EG
(_
,phi
) -> collect_duplicates phi
1184 | CTL.EU
(_
,phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1185 | CTL.Uncheck
(phi
) -> collect_duplicates phi
1186 | _
-> failwith
"not possible"
1188 let assign_variables _
=
1190 (function formula
->
1191 function (cell
,str
,_
) -> if !cell
> 1 then str
:= fresh_let_var())
1194 let rec replace_formulas dec f
=
1195 let (ct
,name
,treated
) = Hashtbl.find
formula_table f
in
1196 let real_ct = !ct
- dec
in
1203 let (acc
,new_f
) = replace_subformulas
(dec
+ (real_ct - 1)) f
in
1204 ((!name
,new_f
) :: acc
, CTL.rewrap f
(CTL.Ref
!name
))
1206 else ([],CTL.rewrap f
(CTL.Ref
!name
))
1207 else replace_subformulas dec f
1209 and replace_subformulas dec f
=
1210 match CTL.unwrap f
with
1212 | CTL.True
-> ([],f
)
1213 | CTL.Pred
(p
) -> ([],f
)
1215 let (acc
,new_phi
) = replace_formulas dec phi
in
1216 (acc
,CTL.rewrap f
(CTL.Not
(new_phi
)))
1217 | CTL.Exists
(v,phi
) ->
1218 let (acc
,new_phi
) = replace_formulas dec phi
in
1219 (acc
,CTL.rewrap f
(CTL.Exists
(v,new_phi
)))
1220 | CTL.And
(phi1
,phi2) ->
1221 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1222 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1223 (acc1
@acc2
,CTL.rewrap f
(CTL.And
(new_phi1
,new_phi2
)))
1224 | CTL.Or
(phi1
,phi2) ->
1225 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1226 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1227 (acc1
@acc2
,CTL.rewrap f
(CTL.Or
(new_phi1
,new_phi2
)))
1228 | CTL.SeqOr
(phi1
,phi2) ->
1229 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1230 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1231 (acc1
@acc2
,CTL.rewrap f
(CTL.SeqOr
(new_phi1
,new_phi2
)))
1232 | CTL.Implies
(phi1
,phi2) ->
1233 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1234 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1235 (acc1
@acc2
,CTL.rewrap f
(CTL.Implies
(new_phi1
,new_phi2
)))
1236 | CTL.AF
(dir
,phi1
,phi2) ->
1237 let (acc
,new_phi1
) = replace_formulas dec phi1
in
1238 let (acc
,new_phi2
) = replace_formulas dec
phi2 in
1239 (acc
,CTL.rewrap f
(CTL.AF
(dir
,new_phi1
,new_phi2
)))
1240 | CTL.AX
(dir
,phi
) ->
1241 let (acc
,new_phi
) = replace_formulas dec phi
in
1242 (acc
,CTL.rewrap f
(CTL.AX
(dir
,new_phi
)))
1243 | CTL.AG
(dir
,phi
) ->
1244 let (acc
,new_phi
) = replace_formulas dec phi
in
1245 (acc
,CTL.rewrap f
(CTL.AG
(dir
,new_phi
)))
1246 | CTL.AU
(dir
,phi1
,phi2,phi3,phi4
) ->
1247 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1248 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1249 let (acc3
,new_phi3
) = replace_formulas dec
phi3 in
1250 let (acc4
,new_phi4
) = replace_formulas dec phi4
in
1251 (acc1
@acc2
@acc3
@acc4
,
1252 CTL.rewrap f
(CTL.AU
(dir
,new_phi1
,new_phi2
,new_phi3
,new_phi4
)))
1253 | CTL.EF
(dir
,phi
) ->
1254 let (acc
,new_phi
) = replace_formulas dec phi
in
1255 (acc
,CTL.rewrap f
(CTL.EF
(dir
,new_phi
)))
1256 | CTL.EX
(dir
,phi
) ->
1257 let (acc
,new_phi
) = replace_formulas dec phi
in
1258 (acc
,CTL.rewrap f
(CTL.EX
(dir
,new_phi
)))
1259 | CTL.EG
(dir
,phi
) ->
1260 let (acc
,new_phi
) = replace_formulas dec phi
in
1261 (acc
,CTL.rewrap f
(CTL.EG
(dir
,new_phi
)))
1262 | CTL.EU
(dir
,phi1
,phi2) ->
1263 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1264 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1265 (acc1
@acc2
,CTL.rewrap f
(CTL.EU
(dir
,new_phi1
,new_phi2
)))
1266 | _
-> failwith
"not possible"
1269 (Hashtbl.create
(50) :
1270 ((cocci_predicate
,string,Wrapper_ctl.info
) CTL.generic_ctl
,
1271 string list
(* fvs *) *
1272 string list
(* intersection of fvs of subterms *))
1276 try let (fvs,_
) = Hashtbl.find
ctlfv_table f
in fvs
1278 let ((fvs,_
) as res
) =
1279 match CTL.unwrap f
with
1280 CTL.False
| CTL.True
| CTL.Pred
(_
) -> ([],[])
1281 | CTL.Not
(phi
) | CTL.Exists
(_
,phi
)
1282 | CTL.AX
(_
,phi
) | CTL.AG
(_
,phi
)
1283 | CTL.EF
(_
,phi
) | CTL.EX
(_
,phi
) | CTL.EG
(_
,phi
) -> (ctl_fvs phi
,[])
1284 | CTL.AU
(_
,phi1
,phi2,phi3,phi4
) ->
1285 let phi1fvs = ctl_fvs phi1
in
1286 let phi2fvs = ctl_fvs phi2 in
1287 (* phi3 has the same fvs as phi1 and phi4 as phi2 *)
1288 (Common.union_set
phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1289 | CTL.And
(phi1
,phi2) | CTL.Or
(phi1
,phi2) | CTL.SeqOr
(phi1
,phi2)
1290 | CTL.Implies
(phi1
,phi2) | CTL.AF
(_
,phi1
,phi2) | CTL.EU
(_
,phi1
,phi2) ->
1291 let phi1fvs = ctl_fvs phi1
in
1292 let phi2fvs = ctl_fvs phi2 in
1293 (Common.union_set
phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1294 | CTL.Ref
(v) -> ([v],[v])
1295 | CTL.Let
(v,term,body) ->
1296 let phi1fvs = ctl_fvs term in
1297 let phi2fvs = Common.minus_set
(ctl_fvs body) [v] in
1298 (Common.union_set
phi1fvs phi2fvs,intersect phi1fvs phi2fvs) in
1299 Hashtbl.add
ctlfv_table f res
;
1302 let rev_order_bindings b
=
1305 (function (nm,term) ->
1306 let (fvs,_
) = Hashtbl.find
ctlfv_table term in (nm,fvs,term))
1308 let rec loop bound
= function
1311 let (now_bound
,still_unbound
) =
1312 List.partition
(function (_
,fvs,_
) -> subset fvs bound
)
1314 let get_names = List.map
(function (x
,_
,_
) -> x
) in
1315 now_bound
@ (loop ((get_names now_bound
) @ bound
) still_unbound
) in
1318 let drop_bindings b f
= (* innermost bindings first in b *)
1319 let process_binary f ffvs inter
nm term fail
=
1320 if List.mem
nm inter
1321 then CTL.rewrap f
(CTL.Let
(nm,term,f
))
1322 else CTL.rewrap f
(fail
()) in
1324 let _ = ctl_fvs f
in Hashtbl.find
ctlfv_table f
in
1325 let rec drop_one nm term f
=
1326 match CTL.unwrap f
with
1330 | CTL.Not
(phi
) -> CTL.rewrap f
(CTL.Not
(drop_one nm term phi
))
1331 | CTL.Exists
(v,phi
) -> CTL.rewrap f
(CTL.Exists
(v,drop_one nm term phi
))
1332 | CTL.And
(phi1
,phi2) ->
1333 let (ffvs
,inter
) = find_fvs f
in
1334 process_binary f ffvs inter
nm term
1335 (function _ -> CTL.And
(drop_one nm term phi1
,drop_one nm term phi2))
1336 | CTL.Or
(phi1
,phi2) ->
1337 let (ffvs
,inter
) = find_fvs f
in
1338 process_binary f ffvs inter
nm term
1339 (function _ -> CTL.Or
(drop_one nm term phi1
,drop_one nm term phi2))
1340 | CTL.SeqOr
(phi1
,phi2) ->
1341 let (ffvs
,inter
) = find_fvs f
in
1342 process_binary f ffvs inter
nm term
1344 CTL.SeqOr
(drop_one nm term phi1
,drop_one nm term phi2))
1345 | CTL.Implies
(phi1
,phi2) ->
1346 let (ffvs
,inter
) = find_fvs f
in
1347 process_binary f ffvs inter
nm term
1349 CTL.Implies
(drop_one nm term phi1
,drop_one nm term phi2))
1350 | CTL.AF
(dir
,phi1
,phi2) ->
1351 let (ffvs
,inter
) = find_fvs f
in
1352 process_binary f ffvs inter
nm term
1354 CTL.AF
(dir
,drop_one nm term phi1
,drop_one nm term phi2))
1355 | CTL.AX
(dir
,phi
) ->
1356 CTL.rewrap f
(CTL.AX
(dir
,drop_one nm term phi
))
1357 | CTL.AG
(dir
,phi
) -> CTL.rewrap f
(CTL.AG
(dir
,drop_one nm term phi
))
1358 | CTL.AU
(dir
,phi1
,phi2,phi3,phi4
) ->
1359 let (ffvs
,inter
) = find_fvs f
in
1360 process_binary f ffvs inter
nm term
1362 CTL.AU
(dir
,drop_one nm term phi1
,drop_one nm term phi2,
1363 drop_one nm term phi3,drop_one nm term phi4
))
1364 | CTL.EF
(dir
,phi
) -> CTL.rewrap f
(CTL.EF
(dir
,drop_one nm term phi
))
1365 | CTL.EX
(dir
,phi
) ->
1366 CTL.rewrap f
(CTL.EX
(dir
,drop_one nm term phi
))
1367 | CTL.EG
(dir
,phi
) -> CTL.rewrap f
(CTL.EG
(dir
,drop_one nm term phi
))
1368 | CTL.EU
(dir
,phi1
,phi2) ->
1369 let (ffvs
,inter
) = find_fvs f
in
1370 process_binary f ffvs inter
nm term
1372 CTL.EU
(dir
,drop_one nm term phi1
,drop_one nm term phi2))
1373 | (CTL.Ref
(v) as x
) -> process_binary f
[v] [v] nm term (function _ -> x
)
1374 | CTL.Let
(v,term1
,body) ->
1375 let (ffvs
,inter
) = find_fvs f
in
1376 process_binary f ffvs inter
nm term
1378 CTL.Let
(v,drop_one nm term term1
,drop_one nm term body)) in
1380 (function processed -> function (nm,_,term) -> drop_one nm term processed)
1384 failwith
"this code should not be used!!!"(*;
1385 Hashtbl.clear formula_table;
1386 Hashtbl.clear ctlfv_table;
1387 (* create a count of the number of occurrences of each subformula *)
1388 collect_duplicates f
;
1389 (* give names to things that appear more than once *)
1391 (* replace duplicated formulas by their variables *)
1392 let (bindings
,new_f
) = replace_formulas 0 f
in
1393 (* collect fvs of terms in bindings and new_f *)
1394 List.iter
(function f
-> let _ = ctl_fvs f
in ())
1395 (new_f
::(List.map
(function (_,term) -> term) bindings
));
1396 (* sort bindings with uses before defs *)
1397 let bindings = rev_order_bindings bindings in
1398 (* insert bindings as lets into the formula *)
1399 let res = drop_bindings bindings new_f
in
1402 (* --------------------------------------------------------------------- *)
1403 (* Function declaration *)
1405 let top_level used_after t
=
1406 match Ast.unwrap t
with
1407 Ast.DECL
(decl
) -> failwith
"not supported decl"
1408 | Ast.INCLUDE
(inc
,s
) ->
1409 (* no indication of whether inc or s is modified *)
1410 wrap 0 (CTL.Pred
((Lib_engine.Include
(inc
,s
),CTL.Control
)))
1411 | Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
1412 | Ast.FUNCTION
(stmt
) ->
1413 (*Printf.printf "orig\n";
1414 Pretty_print_cocci.statement "" stmt;
1415 Format.print_newline();*)
1416 let unopt = elim_opt.V.rebuilder_statement stmt
in
1417 (*Printf.printf "unopt\n";
1418 Pretty_print_cocci.statement "" unopt;
1419 Format.print_newline();*)
1420 let unopt = preprocess_dots_e unopt in
1422 (statement
unopt used_after Tail
[] false)
1423 | Ast.CODE
(stmt_dots
) ->
1424 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
1425 let unopt = preprocess_dots unopt in
1427 (statement_list unopt used_after Tail
[] false)
1428 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords"
1430 (* --------------------------------------------------------------------- *)
1434 let bind x y
= x
or y
in
1435 let option_default = false in
1436 let mcode r x
= false in
1437 let statement r k s
=
1438 match Ast.unwrap s
with Ast.Dots
(_,_,_) -> true | _ -> k s
in
1439 let continue r k e
= k e
in
1440 let stop r k e
= false in
1442 V.combiner
bind option_default
1443 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
1444 continue continue continue
1445 stop stop stop stop stop stop stop statement continue continue in
1446 res.V.combiner_top_level
1448 (* --------------------------------------------------------------------- *)
1451 let asttoctl l used_after
=
1458 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
1460 List.map2
top_level used_after
l
1462 let pp_cocci_predicate (pred
,modif
) =
1463 Pretty_print_engine.pp_predicate pred
1465 let cocci_predicate_to_string (pred
,modif
) =
1466 Pretty_print_engine.predicate_to_string pred