2 * Copyright 2010, INRIA, University of Copenhagen
3 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
4 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
5 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
6 * This file is part of Coccinelle.
8 * Coccinelle is free software: you can redistribute it and/or modify
9 * it under the terms of the GNU General Public License as published by
10 * the Free Software Foundation, according to version 2 of the License.
12 * Coccinelle is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
25 (* true = don't see all matched nodes, only modified ones *)
26 let onlyModif = ref true(*false*)
27 (* set to true for line numbers in the output of ctl_engine *)
28 let line_numbers = ref false
29 (* if true, only eg if header is included in not for ...s *)
30 let simple_get_end = ref false(*true*)
32 (* Question: where do we put the existential quantifier for or. At the
33 moment, let it float inwards. *)
35 (* nest shouldn't overlap with what comes after. not checked for. *)
37 module Ast
= Ast_cocci
38 module V
= Visitor_ast
42 let warning s
= Printf.fprintf stderr
"warning: %s\n" s
44 type cocci_predicate
= Lib_engine.predicate
* string Ast_ctl.modif
46 (cocci_predicate
,string, Wrapper_ctl.info
) Ast_ctl.generic_ctl
49 let aftpred = (Lib_engine.After
,CTL.Control
)
50 let retpred = (Lib_engine.Return
,CTL.Control
)
51 let exitpred = (Lib_engine.ErrorExit
,CTL.Control
)
53 let intersect l1 l2
= List.filter
(function x
-> List.mem x l2
) l1
54 let subset l1 l2
= List.for_all
(function x
-> List.mem x l2
) l1
56 (* --------------------------------------------------------------------- *)
60 (match CTL.unwrap f
with
63 | CTL.Pred
(p
) as x
-> x
64 | CTL.Not
(phi
) -> CTL.Not
(drop_vs phi
)
65 | CTL.Exists
(v
,phi
) ->
66 (match CTL.unwrap phi
with
67 CTL.Pred
((x
,CTL.Modif v1
)) when v
= v1
-> CTL.Pred
((x
,CTL.Control
))
68 | _
-> CTL.Exists
(v
,drop_vs phi
))
69 | CTL.And
(phi1
,phi2
) -> CTL.And
(drop_vs phi1
,drop_vs phi2
)
70 | CTL.Or
(phi1
,phi2
) -> CTL.Or
(drop_vs phi1
,drop_vs phi2
)
71 | CTL.SeqOr
(phi1
,phi2
) -> CTL.SeqOr
(drop_vs phi1
,drop_vs phi2
)
72 | CTL.Implies
(phi1
,phi2
) -> CTL.Implies
(drop_vs phi1
,drop_vs phi2
)
73 | CTL.AF
(dir
,phi1
,phi2
) -> CTL.AF
(dir
,drop_vs phi1
,drop_vs phi2
)
74 | CTL.AX
(dir
,phi
) -> CTL.AX
(dir
,drop_vs phi
)
75 | CTL.AG
(dir
,phi
) -> CTL.AG
(dir
,drop_vs phi
)
76 | CTL.AU
(dir
,phi1
,phi2
,phi3
,phi4
) ->
77 CTL.AU
(dir
,drop_vs phi1
,drop_vs phi2
,drop_vs phi3
,drop_vs phi4
)
78 | CTL.EF
(dir
,phi
) -> CTL.EF
(dir
,drop_vs phi
)
79 | CTL.EX
(dir
,phi
) -> CTL.EX
(dir
,drop_vs phi
)
80 | CTL.EG
(dir
,phi
) -> CTL.EG
(dir
,drop_vs phi
)
81 | CTL.EU
(dir
,phi1
,phi2
) -> CTL.EU
(dir
,drop_vs phi1
,drop_vs phi2
)
82 | CTL.Ref
(v
) as x
-> x
83 | CTL.Let
(v
,term1
,body
) -> CTL.Let
(v
,drop_vs term1
,drop_vs body
))
85 (* --------------------------------------------------------------------- *)
87 let wrap n ctl
= (ctl
,n
)
90 wrap 0 (CTL.Or
(wrap 0 (CTL.Pred
aftpred),wrap 0 (CTL.Pred
exitpred)))
92 let wrapImplies n
(x
,y
) = wrap n
(CTL.Implies
(x
,y
))
93 let wrapExists n
(x
,y
) = wrap n
(CTL.Exists
(x
,y
))
94 let wrapAnd n
(x
,y
) = wrap n
(CTL.And
(x
,y
))
95 let wrapOr n
(x
,y
) = wrap n
(CTL.Or
(x
,y
))
96 let wrapSeqOr n
(x
,y
) = wrap n
(CTL.SeqOr
(x
,y
))
97 let wrapAU n
(x
,y
) = wrap n
(CTL.AU
(CTL.FORWARD
,x
,y
,drop_vs x
,drop_vs y
))
98 let wrapEU n
(x
,y
) = wrap n
(CTL.EU
(CTL.FORWARD
,x
,y
))
99 let wrapAX n
(x
) = wrap n
(CTL.AX
(CTL.FORWARD
,x
))
100 let wrapBackAX n
(x
) = wrap n
(CTL.AX
(CTL.BACKWARD
,x
))
101 let wrapEX n
(x
) = wrap n
(CTL.EX
(CTL.FORWARD
,x
))
102 let wrapBackEX n
(x
) = wrap n
(CTL.EX
(CTL.BACKWARD
,x
))
103 let wrapAG n
(x
) = wrap n
(CTL.AG
(CTL.FORWARD
,x
))
104 let wrapEG n
(x
) = wrap n
(CTL.EG
(CTL.FORWARD
,x
))
105 let wrapAF n
(x
) = wrap n
(CTL.AF
(CTL.FORWARD
,x
,drop_vs x
))
106 let wrapEF n
(x
) = wrap n
(CTL.EF
(CTL.FORWARD
,x
))
107 let wrapNot n
(x
) = wrap n
(CTL.Not
(x
))
108 let wrapPred n
(x
) = wrap n
(CTL.Pred
(x
))
109 let wrapLet n
(x
,y
,z
) = wrap n
(CTL.Let
(x
,y
,z
))
110 let wrapRef n
(x
) = wrap n
(CTL.Ref
(x
))
112 (* --------------------------------------------------------------------- *)
114 let get_option fn
= function
116 | Some x
-> Some
(fn x
)
118 let get_list_option fn
= function
122 (* --------------------------------------------------------------------- *)
123 (* --------------------------------------------------------------------- *)
124 (* Eliminate OptStm *)
126 (* for optional thing with nothing after, should check that the optional thing
127 never occurs. otherwise the matching stops before it occurs *)
130 let donothing r k e
= k e
in
133 List.fold_left
Common.union_set
[] (List.map
Ast.get_fvs l
) in
135 let rec dots_list unwrapped wrapped
=
136 match (unwrapped
,wrapped
) with
139 | (Ast.Dots
(_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
) as u
)::urest
,
141 | (Ast.Nest
(_
,_
,_
)::Ast.OptStm
(stm
)::(Ast.Dots
(_
,_
,_
) as u
)::urest
,
143 let l = Ast.get_line stm
in
144 let new_rest1 = stm
:: (dots_list (u
::urest
) (d1
::rest
)) in
145 let new_rest2 = dots_list urest rest
in
146 let fv_rest1 = fvlist new_rest1 in
147 let fv_rest2 = fvlist new_rest2 in
148 [d0
;(Ast.Disj
[(Ast.DOTS
(new_rest1),l,fv_rest1,Ast.NoDots
);
149 (Ast.DOTS
(new_rest2),l,fv_rest2,Ast.NoDots
)],
150 l,fv_rest1,Ast.NoDots
)]
152 | (Ast.OptStm
(stm
)::urest
,_
::rest
) ->
153 let l = Ast.get_line stm
in
154 let new_rest1 = dots_list urest rest
in
155 let new_rest2 = stm
::new_rest1 in
156 let fv_rest1 = fvlist new_rest1 in
157 let fv_rest2 = fvlist new_rest2 in
158 [(Ast.Disj
[(Ast.DOTS
(new_rest2),l,fv_rest2,Ast.NoDots
);
159 (Ast.DOTS
(new_rest1),l,fv_rest1,Ast.NoDots
)],
160 l,fv_rest2,Ast.NoDots
)]
162 | ([Ast.Dots
(_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
163 let l = Ast.get_line stm
in
164 let fv_stm = Ast.get_fvs stm
in
165 let fv_d1 = Ast.get_fvs d1
in
166 let fv_both = Common.union_set
fv_stm fv_d1 in
167 [d1
;(Ast.Disj
[(Ast.DOTS
([stm
]),l,fv_stm,Ast.NoDots
);
168 (Ast.DOTS
([d1
]),l,fv_d1,Ast.NoDots
)],
169 l,fv_both,Ast.NoDots
)]
171 | ([Ast.Nest
(_
,_
,_
);Ast.OptStm
(stm
)],[d1
;_
]) ->
172 let l = Ast.get_line stm
in
173 let rw = Ast.rewrap stm
in
174 let rwd = Ast.rewrap stm
in
176 Ast.Dots
(("...",{ Ast.line
= 0; Ast.column
= 0 },
177 Ast.CONTEXT
(Ast.NOTHING
)),
179 [d1
;rw(Ast.Disj
[rwd(Ast.DOTS
([stm
]));
180 (Ast.DOTS
([rw dots]),l,[],Ast.NoDots
)])]
182 | (_
::urest
,stm
::rest
) -> stm
:: (dots_list urest rest
)
183 | _
-> failwith
"not possible" in
185 let stmtdotsfn r k d
=
188 (match Ast.unwrap
d with
189 Ast.DOTS
(l) -> Ast.DOTS
(dots_list (List.map
Ast.unwrap
l) l)
190 | Ast.CIRCLES
(l) -> failwith
"elimopt: not supported"
191 | Ast.STARS
(l) -> failwith
"elimopt: not supported") in
194 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
195 donothing donothing stmtdotsfn
196 donothing donothing donothing donothing donothing donothing donothing
197 donothing donothing donothing
199 (* --------------------------------------------------------------------- *)
200 (* Count depth of braces. The translation of a closed brace appears deeply
201 nested within the translation of the sequence term, so the name of the
202 paren var has to take into account the names of the nested braces. On the
203 other hand the close brace does not escape, so we don't have to take into
204 account other paren variable names. *)
206 (* called repetitively, which is inefficient, but less trouble than adding a
207 new field to Seq and FunDecl *)
208 let count_nested_braces s
=
209 let bind x y
= max x y
in
210 let option_default = 0 in
211 let stmt_count r k s
=
212 match Ast.unwrap s
with
213 Ast.Seq
(_
,_
,_
,_
,_
) | Ast.FunDecl
(_
,_
,_
,_
,_
,_
) -> (k s
) + 1
215 let donothing r k e
= k e
in
217 let recursor = V.combiner
bind option_default
218 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
219 donothing donothing donothing
220 donothing donothing donothing donothing donothing donothing
221 donothing stmt_count donothing donothing in
222 "p"^
(string_of_int
(recursor.V.combiner_statement s
))
224 (* --------------------------------------------------------------------- *)
231 Printf.sprintf
"v%d" c
234 let fresh_label_var s
=
236 labctr := !labctr + 1;
237 Printf.sprintf
"%s%d" s
c
240 let fresh_let_var _
=
243 Printf.sprintf
"l%d" c
246 let fresh_metavar _
=
248 (*sctr := !sctr + 1;*)
249 Printf.sprintf
"_S%d" c
251 let get_unquantified quantified vars
=
252 List.filter
(function x
-> not
(List.mem x quantified
)) vars
254 type after
= After
of formula
| Guard
of formula
| Tail
257 let rec loop = function
258 [] -> failwith
"not possible"
260 | x
::xs
-> wrapAnd n
(x
,wrapAX n
(loop xs
)) in
263 let make_seq_after2 n first
= function
264 After rest
-> wrapAnd n
(first
,wrapAX n
(wrapAX n rest
))
267 let make_seq_after n first
= function
268 After rest
-> make_seq n
[first
;rest
]
271 let a2n = function After f
-> Guard f
| x
-> x
273 let and_opt n first
= function
274 After rest
-> wrapAnd n
(first
,rest
)
278 let bind x y
= x
or y
in
279 let option_default = false in
280 let mcode r
(_
,_
,kind
) =
283 | Ast.PLUS
-> failwith
"not possible"
284 | Ast.CONTEXT
(info
) -> not
(info
= Ast.NOTHING
) in
285 let do_nothing r k e
= k e
in
287 V.combiner
bind option_default
288 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
289 do_nothing do_nothing do_nothing
290 do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
291 do_nothing do_nothing do_nothing do_nothing in
292 recursor.V.combiner_rule_elem
294 let make_match n guard used_after code
=
296 then wrapPred n
(Lib_engine.Match
(code
),CTL.Control
)
298 let v = fresh_var() in
299 if contains_modif code
300 then wrapExists n
(v,wrapPred n
(Lib_engine.Match
(code
),CTL.Modif
v))
303 List.exists
(function x
-> List.mem x used_after
) (Ast.get_fvs code
) in
304 if !onlyModif && not
any_used_after
305 then wrapPred n
(Lib_engine.Match
(code
),CTL.Control
)
306 else wrapExists n
(v,wrapPred n
(Lib_engine.Match
(code
),CTL.UnModif
v))
308 let make_raw_match n code
= wrapPred n
(Lib_engine.Match
(code
),CTL.Control
)
310 let rec seq_fvs quantified
= function
313 let t1fvs = get_unquantified quantified fv1
in
315 List.fold_left
Common.union_set
[]
316 (List.map
(get_unquantified quantified
) fvs
) in
317 let bothfvs = Common.inter_set
t1fvs termfvs in
318 let t1onlyfvs = Common.minus_set
t1fvs bothfvs in
319 let new_quantified = Common.union_set
bothfvs quantified
in
320 (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs
)
322 let seq_fvs2 quantified fv1 fv2
=
323 match seq_fvs quantified
[fv1
;fv2
] with
324 [(t1fvs,bfvs
);(t2fvs
,[])] -> (t1fvs,bfvs
,t2fvs
)
325 | _
-> failwith
"impossible"
327 let seq_fvs3 quantified fv1 fv2 fv3
=
328 match seq_fvs quantified
[fv1
;fv2
;fv3
] with
329 [(t1fvs,b12fvs
);(t2fvs
,b23fvs
);(t3fvs
,[])] ->
330 (t1fvs,b12fvs
,t2fvs
,b23fvs
,t3fvs
)
331 | _
-> failwith
"impossible"
333 let seq_fvs4 quantified fv1 fv2 fv3 fv4
=
334 match seq_fvs quantified
[fv1
;fv2
;fv3
;fv4
] with
335 [(t1fvs,b12fvs
);(t2fvs
,b23fvs
);(t3fvs
,b34fvs
);(t4fvs
,[])] ->
336 (t1fvs,b12fvs
,t2fvs
,b23fvs
,t3fvs
,b34fvs
,t4fvs
)
337 | _
-> failwith
"impossible"
339 let seq_fvs5 quantified fv1 fv2 fv3 fv4 fv5
=
340 match seq_fvs quantified
[fv1
;fv2
;fv3
;fv4
;fv5
] with
341 [(t1fvs,b12fvs
);(t2fvs
,b23fvs
);(t3fvs
,b34fvs
);(t4fvs
,b45fvs
);(t5fvs
,[])] ->
342 (t1fvs,b12fvs
,t2fvs
,b23fvs
,t3fvs
,b34fvs
,t4fvs
,b45fvs
,t5fvs
)
343 | _
-> failwith
"impossible"
346 List.fold_right
(function cur
-> function code
-> wrapExists n
(cur
,code
))
348 let intersectll lst nested_list
=
349 List.filter
(function x
-> List.exists
(List.mem x
) nested_list
) lst
351 (* --------------------------------------------------------------------- *)
352 (* annotate dots with before and after neighbors *)
354 let rec get_before sl a
=
355 match Ast.unwrap sl
with
361 let (e
,ea
) = get_before_e e a
in
362 let (sl
,sla
) = loop sl ea
in
364 let (l,a
) = loop x a
in
365 (Ast.rewrap sl
(Ast.DOTS
(l)),a
)
366 | Ast.CIRCLES
(x
) -> failwith
"not supported"
367 | Ast.STARS
(x
) -> failwith
"not supported"
369 and get_before_e s a
=
370 match Ast.unwrap s
with
371 Ast.Dots
(d,Ast.NoWhen
,t
) ->
372 (Ast.rewrap s
(Ast.Dots
(d,Ast.NoWhen
,a
@t
)),a
)
373 | Ast.Dots
(d,Ast.WhenNot w
,t
) ->
374 let (w
,_
) = get_before w
[] in
375 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenNot w
,a
@t
)),a
)
376 | Ast.Dots
(d,Ast.WhenAlways w
,t
) ->
377 let (w
,_
) = get_before_e w
[] in
378 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenAlways w
,a
@t
)),a
)
379 | Ast.Nest
(stmt_dots
,w
,t
) ->
380 let (w
,_
) = List.split
(List.map
(function s
-> get_before s
[]) w
) in
381 let (sd
,_
) = get_before stmt_dots a
in
387 Unify_ast.unify_statement_dots
388 (Ast.rewrap s
(Ast.DOTS
([a]))) stmt_dots
in
390 Unify_ast.MAYBE
-> false
392 | Ast.Other_dots
a ->
393 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
395 Unify_ast.MAYBE
-> false
399 (Ast.rewrap s
(Ast.Nest
(sd
,w
,a@t
)),[Ast.Other_dots stmt_dots
])
400 | Ast.Disj
(stmt_dots_list
) ->
402 List.split
(List.map
(function e
-> get_before e
a) stmt_dots_list
) in
403 (Ast.rewrap s
(Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
405 (match Ast.unwrap ast
with
406 Ast.MetaStmt
(_
,_
,_
) -> (s
,[])
407 | _
-> (s
,[Ast.Other s
]))
408 | Ast.Seq
(lbrace
,decls
,dots,body
,rbrace
) ->
409 let index = count_nested_braces s
in
410 let (de
,dea
) = get_before decls
[Ast.WParen
(lbrace
,index)] in
411 let (bd
,_
) = get_before body dea
in
412 (Ast.rewrap s
(Ast.Seq
(lbrace
,de
,dots,bd
,rbrace
)),
413 [Ast.WParen
(rbrace
,index)])
414 | Ast.IfThen
(ifheader
,branch
,aft
) ->
415 let (br
,_
) = get_before_e branch
[] in
416 (Ast.rewrap s
(Ast.IfThen
(ifheader
,br
,aft
)), [Ast.Other s
])
417 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
418 let (br1
,_
) = get_before_e branch1
[] in
419 let (br2
,_
) = get_before_e branch2
[] in
420 (Ast.rewrap s
(Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other s
])
421 | Ast.While
(header
,body
,aft
) ->
422 let (bd
,_
) = get_before_e body
[] in
423 (Ast.rewrap s
(Ast.While
(header
,bd
,aft
)),[Ast.Other s
])
424 | Ast.For
(header
,body
,aft
) ->
425 let (bd
,_
) = get_before_e body
[] in
426 (Ast.rewrap s
(Ast.For
(header
,bd
,aft
)),[Ast.Other s
])
427 | Ast.FunDecl
(header
,lbrace
,decls
,dots,body
,rbrace
) ->
428 let index = count_nested_braces s
in
429 let (de
,dea
) = get_before decls
[Ast.WParen
(lbrace
,index)] in
430 let (bd
,_
) = get_before body dea
in
431 (Ast.rewrap s
(Ast.FunDecl
(header
,lbrace
,de
,dots,bd
,rbrace
)),[])
432 | _
-> failwith
"not supported"
434 let rec get_after sl
a =
435 match Ast.unwrap sl
with
441 let (sl
,sla
) = loop sl
in
442 let (e
,ea
) = get_after_e e sla
in
444 let (l,a) = loop x
in
445 (Ast.rewrap sl
(Ast.DOTS
(l)),a)
446 | Ast.CIRCLES
(x
) -> failwith
"not supported"
447 | Ast.STARS
(x
) -> failwith
"not supported"
449 and get_after_e s
a =
450 match Ast.unwrap s
with
451 Ast.Dots
(d,Ast.NoWhen
,t
) ->
452 (Ast.rewrap s
(Ast.Dots
(d,Ast.NoWhen
,a@t
)),a)
453 | Ast.Dots
(d,Ast.WhenNot w
,t
) ->
454 let (w
,_
) = get_after w
[] in
455 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenNot w
,a@t
)),a)
456 | Ast.Dots
(d,Ast.WhenAlways w
,t
) ->
457 let (w
,_
) = get_after_e w
[] in
458 (Ast.rewrap s
(Ast.Dots
(d,Ast.WhenAlways w
,a@t
)),a)
459 | Ast.Nest
(stmt_dots
,w
,t
) ->
460 let (w
,_
) = List.split
(List.map
(function s
-> get_after s
[]) w
) in
461 let (sd
,_
) = get_after stmt_dots
a in
467 Unify_ast.unify_statement_dots
468 (Ast.rewrap s
(Ast.DOTS
([a]))) stmt_dots
in
470 Unify_ast.MAYBE
-> false
472 | Ast.Other_dots
a ->
473 let unifies = Unify_ast.unify_statement_dots
a stmt_dots
in
475 Unify_ast.MAYBE
-> false
479 (Ast.rewrap s
(Ast.Nest
(sd
,w
,a@t
)),[Ast.Other_dots stmt_dots
])
480 | Ast.Disj
(stmt_dots_list
) ->
482 List.split
(List.map
(function e
-> get_after e
a) stmt_dots_list
) in
483 (Ast.rewrap s
(Ast.Disj
(dsl
)),List.fold_left
Common.union_set
[] dsla
)
485 (match Ast.unwrap ast
with
486 Ast.MetaStmt
(nm
,Ast.SequencibleAfterDots _
,i
) ->
487 (* check after information for metavar optimization *)
488 (* if the error is not desired, could just return [], then
489 the optimization (check for EF) won't take place *)
493 (match Ast.unwrap x
with
494 Ast.Dots
(_
,_
,_
) | Ast.Nest
(_
,_
,_
) ->
496 "dots/nest not allowed before and after stmt metavar"
498 | Ast.Other_dots x
->
499 (match Ast.undots x
with
501 (match Ast.unwrap x
with
502 Ast.Dots
(_
,_
,_
) | Ast.Nest
(_
,_
,_
) ->
504 ("dots/nest not allowed before and after stmt "^
513 (Ast.MetaStmt
(nm
,Ast.SequencibleAfterDots
a,i
)))),[])
514 | Ast.MetaStmt
(_
,_
,_
) -> (s
,[])
515 | _
-> (s
,[Ast.Other s
]))
516 | Ast.Seq
(lbrace
,decls
,dots,body
,rbrace
) ->
517 let index = count_nested_braces s
in
518 let (bd
,bda
) = get_after body
[Ast.WParen
(rbrace
,index)] in
519 let (de
,_
) = get_after decls bda
in
520 (Ast.rewrap s
(Ast.Seq
(lbrace
,de
,dots,bd
,rbrace
)),
521 [Ast.WParen
(lbrace
,index)])
522 | Ast.IfThen
(ifheader
,branch
,aft
) ->
523 let (br
,_
) = get_after_e branch
a in
524 (Ast.rewrap s
(Ast.IfThen
(ifheader
,br
,aft
)),[Ast.Other s
])
525 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
526 let (br1
,_
) = get_after_e branch1
a in
527 let (br2
,_
) = get_after_e branch2
a in
528 (Ast.rewrap s
(Ast.IfThenElse
(ifheader
,br1
,els
,br2
,aft
)),[Ast.Other s
])
529 | Ast.While
(header
,body
,aft
) ->
530 let (bd
,_
) = get_after_e body
a in
531 (Ast.rewrap s
(Ast.While
(header
,bd
,aft
)),[Ast.Other s
])
532 | Ast.For
(header
,body
,aft
) ->
533 let (bd
,_
) = get_after_e body
a in
534 (Ast.rewrap s
(Ast.For
(header
,bd
,aft
)),[Ast.Other s
])
535 | Ast.FunDecl
(header
,lbrace
,decls
,dots,body
,rbrace
) ->
536 let index = count_nested_braces s
in
537 let (bd
,bda
) = get_after body
[Ast.WParen
(rbrace
,index)] in
538 let (de
,_
) = get_after decls bda
in
539 (Ast.rewrap s
(Ast.FunDecl
(header
,lbrace
,de
,dots,bd
,rbrace
)),[])
540 | _
-> failwith
"not supported"
543 let preprocess_dots sl
=
544 let (sl
,_
) = get_before sl
[] in
545 let (sl
,_
) = get_after sl
[] in
548 let preprocess_dots_e sl
=
549 let (sl
,_
) = get_before_e sl
[] in
550 let (sl
,_
) = get_after_e sl
[] in
553 (* --------------------------------------------------------------------- *)
554 (* the main translation loop *)
556 let decl_to_not_decl n
dots stmt
make_match f
=
561 let md = Ast.make_meta_decl
"_d" (Ast.CONTEXT
(Ast.NOTHING
)) in
562 Ast.rewrap
md (Ast.Decl
md) in
563 wrapAU n
(make_match de,
564 wrap n
(CTL.And
(wrap n
(CTL.Not
(make_match de)), f
)))
566 let rec statement_list stmt_list used_after after quantified guard
=
567 let n = if !line_numbers then Ast.get_line stmt_list
else 0 in
568 match Ast.unwrap stmt_list
with
570 let rec loop quantified
= function
571 ([],_
) -> (match after
with After f
-> f
| _
-> wrap n CTL.True
)
572 | ([e
],_
) -> statement e used_after after quantified guard
574 let shared = intersectll fv fvs
in
575 let unqshared = get_unquantified quantified
shared in
576 let new_quantified = Common.union_set
unqshared quantified
in
578 (statement e used_after
(After
(loop new_quantified (sl
,fvs
)))
579 new_quantified guard
)
580 | _
-> failwith
"not possible" in
581 loop quantified
(x
,List.map
Ast.get_fvs x
)
582 | Ast.CIRCLES
(x
) -> failwith
"not supported"
583 | Ast.STARS
(x
) -> failwith
"not supported"
585 and statement stmt used_after after quantified guard
=
587 let n = if !line_numbers then Ast.get_line stmt
else 0 in
588 let wrapExists = wrapExists n in
589 let wrapAnd = wrapAnd n in
590 let wrapOr = wrapOr n in
591 let wrapSeqOr = wrapSeqOr n in
592 let wrapAU = wrapAU n in
593 let wrapAX = wrapAX n in
594 let wrapBackAX = wrapBackAX n in
595 let wrapEX = wrapEX n in
596 let wrapBackEX = wrapBackEX n in
597 let wrapAG = wrapAG n in
598 let wrapAF = wrapAF n in
599 let wrapEF = wrapEF n in
600 let wrapNot = wrapNot n in
601 let wrapPred = wrapPred n in
602 let make_seq = make_seq n in
603 let make_seq_after2 = make_seq_after2 n in
604 let make_seq_after = make_seq_after n in
605 let and_opt = and_opt n in
606 let quantify = quantify n in
607 let make_match = make_match n guard used_after
in
608 let make_raw_match = make_raw_match n in
610 let make_meta_rule_elem d =
611 let nm = fresh_metavar() in
612 Ast.make_meta_rule_elem nm d in
614 match Ast.unwrap stmt
with
616 (match Ast.unwrap ast
with
617 Ast.MetaStmt
((s
,i
,(Ast.CONTEXT
(Ast.BEFOREAFTER
(_
,_
)) as d)),seqible
,_
)
618 | Ast.MetaStmt
((s
,i
,(Ast.CONTEXT
(Ast.AFTER
(_
)) as d)),seqible
,_
) ->
619 let label_var = (*fresh_label_var*) "_lab" in
620 let label_pred = wrapPred(Lib_engine.Label
(label_var),CTL.Control
) in
622 wrapPred(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
623 let matcher d = make_match (make_meta_rule_elem d) in
624 let full_metamatch = matcher d in
625 let first_metamatch =
628 Ast.CONTEXT
(Ast.BEFOREAFTER
(bef
,_
)) ->
629 Ast.CONTEXT
(Ast.BEFORE
(bef
))
630 | Ast.CONTEXT
(_
) -> Ast.CONTEXT
(Ast.NOTHING
)
631 | Ast.MINUS
(_
) | Ast.PLUS
-> failwith
"not possible") in
632 let middle_metamatch =
635 Ast.CONTEXT
(_
) -> Ast.CONTEXT
(Ast.NOTHING
)
636 | Ast.MINUS
(_
) | Ast.PLUS
-> failwith
"not possible") in
640 Ast.CONTEXT
(Ast.BEFOREAFTER
(_
,aft
)) ->
641 Ast.CONTEXT
(Ast.AFTER
(aft
))
642 | Ast.CONTEXT
(_
) -> d
643 | Ast.MINUS
(_
) | Ast.PLUS
-> failwith
"not possible") in
647 [full_metamatch; and_opt (wrapNot(prelabel_pred)) after
] in
651 wrapAU(middle_metamatch,
653 [wrapAnd(last_metamatch,label_pred);
654 and_opt (wrapNot(prelabel_pred)) after
])] in
657 f
(wrapAnd(make_raw_match ast
,
658 wrapOr(left_or,right_or)))) in
661 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
662 quantify (label_var::get_unquantified quantified
[s
])
665 (wrapAnd(wrapNot(wrapBackAX(label_pred)),x
))))
666 | Ast.SequencibleAfterDots
l ->
668 List.map
(process_bef_aft Tail quantified used_after
n) l in
670 List.fold_left
(function x
-> function y
-> wrapOr(x
,y
))
671 (List.hd
afts) (List.tl
afts) in
672 quantify (label_var::get_unquantified quantified
[s
])
673 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
676 wrapAnd(wrapNot(wrapBackAX(label_pred)),x
))))
677 | Ast.NotSequencible
->
678 quantify (label_var::get_unquantified quantified
[s
]) (body id))
680 | Ast.MetaStmt
((s
,i
,d),seqible
,_
) ->
681 let label_var = (*fresh_label_var*) "_lab" in
682 let label_pred = wrapPred(Lib_engine.Label
(label_var),CTL.Control
) in
684 wrapPred(Lib_engine.PrefixLabel
(label_var),CTL.Control
) in
685 let matcher d = make_match (make_meta_rule_elem d) in
686 let first_metamatch = matcher d in
690 Ast.MINUS
(_
) -> Ast.MINUS
([])
691 | Ast.CONTEXT
(_
) -> Ast.CONTEXT
(Ast.NOTHING
)
692 | Ast.PLUS
-> failwith
"not possible") in
693 (* first_nodea and first_nodeb are separated here and above to
694 improve let sharing - only first_nodea is unique to this site *)
695 let first_nodeb = first_metamatch in
696 let rest_nodes = wrapAnd(rest_metamatch,prelabel_pred) in
697 let last_node = and_opt (wrapNot(prelabel_pred)) after
in
704 [first_nodeb; wrapAU(rest_nodes,last_node)])))) in
706 Ast.Sequencible
| Ast.SequencibleAfterDots
[] ->
707 quantify (label_var::get_unquantified quantified
[s
])
709 (function x
-> wrapAnd(wrapNot(wrapBackAX(label_pred)),x
)))
710 | Ast.SequencibleAfterDots
l ->
712 List.map
(process_bef_aft Tail quantified used_after
n) l in
714 List.fold_left
(function x
-> function y
-> wrapOr(x
,y
))
715 (List.hd
afts) (List.tl
afts) in
716 quantify (label_var::get_unquantified quantified
[s
])
717 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
720 wrapAnd(wrapNot(wrapBackAX(label_pred)),x
))))
721 | Ast.NotSequencible
->
722 quantify (label_var::get_unquantified quantified
[s
])
723 (body (function x
-> x
)))
725 let stmt_fvs = Ast.get_fvs stmt
in
726 let fvs = get_unquantified quantified
stmt_fvs in
727 let between_dots = Ast.get_dots_bef_aft stmt
in
728 let term = make_match ast
in
730 match between_dots with
731 Ast.BetweenDots brace_term
->
732 (match Ast.unwrap brace_term
with
733 Ast.Atomic
(brace_ast
) ->
738 (wrapPred(Lib_engine.TrueBranch
,CTL.Control
)),
740 (wrapBackEX(wrapPred(Lib_engine.FalseBranch
,
742 make_match brace_ast
) in
748 (wrapPred(Lib_engine.TrueBranch
,CTL.Control
)),
750 (wrapBackEX(wrapPred(Lib_engine.FalseBranch
,
754 | _
-> failwith
"not possible")
755 | Ast.NoDots
-> term in
756 make_seq_after (quantify fvs term) after
)
757 | Ast.Seq
(lbrace
,decls
,dots,body,rbrace
) ->
758 let (lbfvs
,b1fvs
,_
,b2fvs
,_
,b3fvs
,rbfvs
) =
760 (Ast.get_fvs lbrace
) (Ast.get_fvs decls
)
761 (Ast.get_fvs
body) (Ast.get_fvs rbrace
) in
762 let v = count_nested_braces stmt
in
763 let paren_pred = wrapPred(Lib_engine.Paren
v,CTL.Control
) in
765 wrapAnd(quantify lbfvs
(make_match lbrace
),paren_pred) in
767 wrapAnd(quantify rbfvs
(make_match rbrace
),paren_pred) in
768 let new_quantified2 =
769 Common.union_set b1fvs
(Common.union_set b2fvs quantified
) in
770 let new_quantified3 = Common.union_set b3fvs
new_quantified2 in
776 (statement_list decls used_after
778 (decl_to_not_decl n dots stmt
make_match
780 (statement_list body used_after
781 (After
(make_seq_after end_brace after
))
782 new_quantified3 guard
))))
783 new_quantified2 guard
)]))
784 | Ast.IfThen
(ifheader
,branch
,aft
) ->
786 (* "if (test) thn" becomes:
787 if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
789 "if (test) thn; after" becomes:
790 if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
796 seq_fvs2 quantified
(Ast.get_fvs ifheader
) (Ast.get_fvs branch
) in
797 let new_quantified = Common.union_set bfvs quantified
in
799 let if_header = quantify efvs
(make_match ifheader
) in
800 (* then branch and after *)
803 [wrapPred(Lib_engine.TrueBranch
,CTL.Control
);
804 statement branch used_after
(a2n after
) new_quantified guard
] in
805 let fall_branch = wrapPred(Lib_engine.FallThrough
,CTL.Control
) in
806 let after_pred = wrapPred(Lib_engine.After
,CTL.Control
) in
807 let (aft_needed
,after_branch
) =
809 Ast.CONTEXT
(Ast.NOTHING
) -> (false,make_seq_after2 after_pred after
)
812 make_seq_after after_pred
814 (make_seq_after (make_match (make_meta_rule_elem aft
))
816 let or_cases = wrapOr(true_branch,wrapOr(fall_branch,after_branch
)) in
818 (match (after
,aft_needed
) with
819 (After _
,_
) (* pattern doesn't end here *)
820 | (_
,true) (* + code added after *) ->
822 (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
823 | _
-> quantify bfvs
(wrapAnd(if_header, wrapAX or_cases)))
825 | Ast.IfThenElse
(ifheader
,branch1
,els
,branch2
,aft
) ->
827 (* "if (test) thn else els" becomes:
828 if(test) & AX((TrueBranch & AX thn) v
829 (FalseBranch & AX (else & AX els)) v After)
832 "if (test) thn else els; after" becomes:
833 if(test) & AX((TrueBranch & AX thn) v
834 (FalseBranch & AX (else & AX els)) v
835 (After & AXAX after))
840 Note that we rely on the well-formedness of C programs. For example, we
841 do not use EX to check that there is at least one then branch, because
842 there is always one. And we do not check that there is only one then or
843 else branch, because these again are always the case in a well-formed C
846 let (e1fvs
,b1fvs
,s1fvs
) =
847 seq_fvs2 quantified
(Ast.get_fvs ifheader
) (Ast.get_fvs branch1
) in
848 let (e2fvs
,b2fvs
,s2fvs
) =
849 seq_fvs2 quantified
(Ast.get_fvs ifheader
) (Ast.get_fvs branch2
) in
852 (Common.union_set b1fvs b2fvs
)
853 (Common.inter_set s1fvs s2fvs
) in
854 let exponlyfvs = Common.inter_set e1fvs e2fvs
in
855 let new_quantified = Common.union_set
bothfvs quantified
in
857 let if_header = quantify exponlyfvs (make_match ifheader
) in
858 (* then and else branches *)
861 [wrapPred(Lib_engine.TrueBranch
,CTL.Control
);
862 statement branch1 used_after
(a2n after
) new_quantified guard
] in
863 let false_pred = wrapPred(Lib_engine.FalseBranch
,CTL.Control
) in
866 [false_pred; make_match els
;
867 statement branch2 used_after
(a2n after
) new_quantified guard
] in
868 let after_pred = wrapPred(Lib_engine.After
,CTL.Control
) in
869 let (aft_needed
,after_branch
) =
871 Ast.CONTEXT
(Ast.NOTHING
) -> (false,make_seq_after2 after_pred after
)
874 make_seq_after after_pred
876 (make_seq_after (make_match (make_meta_rule_elem aft
))
878 let or_cases = wrapOr(true_branch,wrapOr(false_branch,after_branch
)) in
880 (match (after
,aft_needed
) with
881 (After _
,_
) (* pattern doesn't end here *)
882 | (_
,true) (* + code added after *) ->
886 wrapAnd(wrapAX or_cases,
887 wrapAnd(wrapEX false_pred,wrapEX after_pred))))
890 (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX false_pred))))
892 | Ast.While
(header
,body,aft
) | Ast.For
(header
,body,aft
) ->
893 (* the translation in this case is similar to that of an if with no else *)
896 seq_fvs2 quantified
(Ast.get_fvs header
) (Ast.get_fvs
body) in
897 let new_quantified = Common.union_set bfvs quantified
in
899 let header = quantify efvs
(make_match header) in
902 [wrapPred(Lib_engine.TrueBranch
,CTL.Control
);
903 statement
body used_after
(a2n after
) new_quantified guard
] in
904 let after_pred = wrapPred(Lib_engine.FallThrough
,CTL.Control
) in
905 let (aft_needed
,after_branch
) =
907 Ast.CONTEXT
(Ast.NOTHING
) -> (false,make_seq_after2 after_pred after
)
910 make_seq_after after_pred
912 (make_seq_after (make_match (make_meta_rule_elem aft
))
914 let or_cases = wrapOr(body,after_branch
) in
916 (match (after
,aft_needed
) with
917 (After _
,_
) (* pattern doesn't end here *)
918 | (_
,true) (* + code added after *) ->
920 (wrapAnd (header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
921 | _
-> quantify bfvs
(wrapAnd(header, wrapAX or_cases)))
923 | Ast.Disj
(stmt_dots_list
) ->
926 (function x
-> statement_list x used_after after quantified guard
)
928 let rec loop = function
929 [] -> wrap n CTL.True
931 | x
::xs
-> wrapSeqOr(x
,loop xs
) in
935 statement_list e used_after (a2n after) quantified true in
938 (function rest -> function cur -> wrapAnd(wrapNot(do_one cur),rest))
940 let process_one nots cur =
941 match Ast.unwrap cur with
943 let on = List.map (function x -> Ast.OrOther_dots x) nots in
944 (match Ast.unwrap x with
948 Printf.printf "a not\n";
949 Pretty_print_cocci.statement_dots x)
953 (Ast.DOTS((Ast.rewrap x (Ast.Dots(d,w,on@t)))::xs)) in
954 statement_list cur used_after after quantified guard
955 | Ast.Nest(sd,w,t) ->
958 (Ast.DOTS((Ast.rewrap x (Ast.Nest(sd,w,on@t)))::xs)) in
959 statement_list cur used_after after quantified guard
962 (statement_list cur used_after after quantified guard))
965 (statement_list cur used_after after quantified guard)
966 | _ -> failwith "CIRCLES, STARS not supported" in
967 let rec loop after = function
968 [] -> failwith "disj shouldn't be empty" (*wrap n CTL.False*)
969 | [(nots
,cur)] -> process_one nots
cur
970 | (nots
,cur)::rest
-> wrapOr(process_one nots
cur, loop after rest
) in
971 loop after
(preprocess_disj stmt_dots_list
)
973 | Ast.Nest
(stmt_dots
,whencode
,befaft
) ->
975 statement_list stmt_dots used_after
(a2n after
) quantified guard
in
980 statement_list sl used_after
(a2n after
) quantified
true)
982 List.fold_left
(function rest
-> function cur -> wrapOr(cur,rest
))
983 (statement_list stmt_dots used_after
(a2n after
) quantified
true)
985 (match (after
,guard
&&(whencode
=[])) with
988 List.map
(process_bef_aft after quantified used_after
n) befaft
in
990 [] -> wrapAF(wrapOr(a,aftret))
995 (function rest
-> function cur -> wrapOr(cur,rest
))
997 wrapAU(left,wrapOr(a,aftret)))
999 let left = wrapOr(dots_pattern,wrapNot udots_pattern) in
1001 List.map
(process_bef_aft after quantified used_after
n) befaft
in
1009 (function rest
-> function cur -> wrapOr(cur,rest
))
1012 wrapAU(left,wrapOr(a,aftret))
1013 | (_
,true) -> wrap n CTL.True
1014 | (_
,false) -> wrapAG(wrapOr(dots_pattern,wrapNot udots_pattern)))
1015 | Ast.Dots
((_
,i
,d),whencodes,t
) ->
1019 (* no need for the fresh metavar, but ... is a bit weird as a
1021 Some
(make_match (make_meta_rule_elem d))
1024 (match whencodes with
1026 | Ast.WhenNot
whencodes ->
1028 (statement_list whencodes used_after
(a2n after
) quantified
1030 | Ast.WhenAlways s
->
1031 [statement s used_after
(a2n after
) quantified
true]) @
1033 (List.map
(process_bef_aft after quantified used_after
n) t
)) in
1035 match whencodes with
1040 (function rest
-> function cur -> wrapAnd(cur,rest
))
1043 match (dot_code,phi2) with (* add - on dots, if any *)
1045 | (Some dotcode
,None
) -> Some dotcode
1046 | (None
,Some whencode
) -> Some whencode
1047 | (Some dotcode
,Some whencode
) -> Some
(wrapAnd (dotcode
,whencode
)) in
1048 let exit = wrap n (CTL.Pred
(Lib_engine.Exit
,CTL.Control
)) in
1049 (* add in the after code to make the result *)
1050 (match (after
,phi3) with
1051 (Tail
,Some whencode
) -> wrapAU(whencode
,wrapOr(exit,aftret))
1052 | (Tail
,None
) -> wrapAF(wrapOr(exit,aftret))
1053 | (After f
,Some whencode
) | (Guard f
,Some whencode
) ->
1054 wrapAU(whencode
,wrapOr(f
,aftret))
1055 | (After f
,None
) | (Guard f
,None
) -> wrapAF(wrapOr(f
,aftret)))
1056 | Ast.FunDecl
(header,lbrace
,decls
,dots,body,rbrace
) ->
1057 let (hfvs
,b1fvs
,lbfvs
,b2fvs
,_
,b3fvs
,_
,b4fvs
,rbfvs
) =
1058 seq_fvs5 quantified
(Ast.get_fvs
header) (Ast.get_fvs lbrace
)
1059 (Ast.get_fvs decls
) (Ast.get_fvs
body) (Ast.get_fvs rbrace
) in
1060 let function_header = quantify hfvs
(make_match header) in
1061 let v = count_nested_braces stmt
in
1062 let paren_pred = wrapPred(Lib_engine.Paren
v,CTL.Control
) in
1064 wrapAnd(quantify lbfvs
(make_match lbrace
),paren_pred) in
1066 let stripped_rbrace =
1067 match Ast.unwrap rbrace
with
1068 Ast.SeqEnd
((data
,info
,_
)) ->
1070 (Ast.SeqEnd
((data
,info
,Ast.CONTEXT
(Ast.NOTHING
))))
1071 | _
-> failwith
"unexpected close brace" in
1072 let exit = wrap n (CTL.Pred
(Lib_engine.Exit
,CTL.Control
)) in
1073 let errorexit = wrap n (CTL.Pred
(Lib_engine.ErrorExit
,CTL.Control
)) in
1074 wrapAnd(quantify rbfvs
(make_match rbrace
),
1075 wrapAU(make_match stripped_rbrace,
1076 wrapOr(exit,errorexit))) in
1077 let new_quantified3 =
1078 Common.union_set b1fvs
1079 (Common.union_set b2fvs
(Common.union_set b3fvs quantified
)) in
1080 let new_quantified4 = Common.union_set b4fvs
new_quantified3 in
1090 (statement_list decls used_after
1092 (decl_to_not_decl n dots stmt
1095 (statement_list body used_after
1097 (make_seq_after end_brace after
))
1098 new_quantified4 guard
))))
1099 new_quantified3 guard
)])))])
1100 | Ast.OptStm
(stm
) ->
1101 failwith
"OptStm should have been compiled away\n";
1102 | Ast.UniqueStm
(stm
) ->
1103 failwith
"arities not yet supported"
1104 | Ast.MultiStm
(stm
) ->
1105 failwith
"arities not yet supported"
1106 | _
-> failwith
"not supported"
1108 and process_bef_aft after quantified used_after ln
= function
1109 Ast.WParen
(re
,n) ->
1110 let paren_pred = wrapPred ln
(Lib_engine.Paren
n,CTL.Control
) in
1111 wrapAnd ln
(make_raw_match ln re
,paren_pred)
1112 | Ast.Other s
-> statement s used_after
(a2n after
) quantified
true
1113 | Ast.Other_dots
d -> statement_list d used_after
(a2n after
) quantified
true
1114 | Ast.OrOther_dots
d -> statement_list d used_after Tail quantified
true
1116 (* Returns a triple for each disj element. The first element of the triple is
1117 Some v if the triple element needs a name, and None otherwise. The second
1118 element is a list of names whose negations should be conjuncted with the
1119 term. The third element is the original term *)
1120 and (preprocess_disj
:
1121 Ast.statement
Ast.dots list
->
1122 (Ast.statement
Ast.dots list
* Ast.statement
Ast.dots) list
) =
1128 List.map
(function r
-> Unify_ast.unify_statement_dots
cur r
) rest
in
1129 let processed = preprocess_disj rest
in
1130 if List.exists
(function Unify_ast.MAYBE
-> true | _
-> false) template
1134 (function ((nots,r
) as x
) ->
1135 function Unify_ast.MAYBE
-> (cur::nots,r
) | Unify_ast.NO
-> x
)
1137 else ([], cur) :: processed
1139 (* --------------------------------------------------------------------- *)
1141 Phase 1: Use a hash table to identify formulas that appear more than once.
1142 Phase 2: Replace terms by variables.
1143 Phase 3: Drop lets to the point as close as possible to the uses of their
1147 (Hashtbl.create
(50) :
1148 ((cocci_predicate
,string,Wrapper_ctl.info
) CTL.generic_ctl
,
1149 int ref (* count *) * string ref (* name *) * bool ref (* processed *))
1154 try Hashtbl.find
formula_table phi
1156 let c = (ref 0,ref "",ref false) in
1157 Hashtbl.add
formula_table phi
c;
1161 let rec collect_duplicates f
=
1163 match CTL.unwrap f
with
1167 | CTL.Not
(phi
) -> collect_duplicates phi
1168 | CTL.Exists
(v,phi
) -> collect_duplicates phi
1169 | CTL.And
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1170 | CTL.Or
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1171 | CTL.SeqOr
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1172 | CTL.Implies
(phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1173 | CTL.AF
(_
,phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1174 | CTL.AX
(_
,phi
) -> collect_duplicates phi
1175 | CTL.AG
(_
,phi
) -> collect_duplicates phi
1176 | CTL.AU
(_
,phi1
,phi2,phi3,phi4
) ->
1177 collect_duplicates phi1
; collect_duplicates phi2;
1178 collect_duplicates phi3; collect_duplicates phi4
1179 | CTL.EF
(_
,phi
) -> collect_duplicates phi
1180 | CTL.EX
(_
,phi
) -> collect_duplicates phi
1181 | CTL.EG
(_
,phi
) -> collect_duplicates phi
1182 | CTL.EU
(_
,phi1
,phi2) -> collect_duplicates phi1
; collect_duplicates phi2
1183 | CTL.Uncheck
(phi
) -> collect_duplicates phi
1184 | _
-> failwith
"not possible"
1186 let assign_variables _
=
1188 (function formula
->
1189 function (cell
,str
,_
) -> if !cell
> 1 then str
:= fresh_let_var())
1192 let rec replace_formulas dec f
=
1193 let (ct
,name
,treated
) = Hashtbl.find
formula_table f
in
1194 let real_ct = !ct
- dec
in
1201 let (acc
,new_f
) = replace_subformulas
(dec
+ (real_ct - 1)) f
in
1202 ((!name
,new_f
) :: acc
, CTL.rewrap f
(CTL.Ref
!name
))
1204 else ([],CTL.rewrap f
(CTL.Ref
!name
))
1205 else replace_subformulas dec f
1207 and replace_subformulas dec f
=
1208 match CTL.unwrap f
with
1210 | CTL.True
-> ([],f
)
1211 | CTL.Pred
(p
) -> ([],f
)
1213 let (acc
,new_phi
) = replace_formulas dec phi
in
1214 (acc
,CTL.rewrap f
(CTL.Not
(new_phi
)))
1215 | CTL.Exists
(v,phi
) ->
1216 let (acc
,new_phi
) = replace_formulas dec phi
in
1217 (acc
,CTL.rewrap f
(CTL.Exists
(v,new_phi
)))
1218 | CTL.And
(phi1
,phi2) ->
1219 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1220 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1221 (acc1
@acc2
,CTL.rewrap f
(CTL.And
(new_phi1
,new_phi2
)))
1222 | CTL.Or
(phi1
,phi2) ->
1223 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1224 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1225 (acc1
@acc2
,CTL.rewrap f
(CTL.Or
(new_phi1
,new_phi2
)))
1226 | CTL.SeqOr
(phi1
,phi2) ->
1227 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1228 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1229 (acc1
@acc2
,CTL.rewrap f
(CTL.SeqOr
(new_phi1
,new_phi2
)))
1230 | CTL.Implies
(phi1
,phi2) ->
1231 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1232 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1233 (acc1
@acc2
,CTL.rewrap f
(CTL.Implies
(new_phi1
,new_phi2
)))
1234 | CTL.AF
(dir
,phi1
,phi2) ->
1235 let (acc
,new_phi1
) = replace_formulas dec phi1
in
1236 let (acc
,new_phi2
) = replace_formulas dec
phi2 in
1237 (acc
,CTL.rewrap f
(CTL.AF
(dir
,new_phi1
,new_phi2
)))
1238 | CTL.AX
(dir
,phi
) ->
1239 let (acc
,new_phi
) = replace_formulas dec phi
in
1240 (acc
,CTL.rewrap f
(CTL.AX
(dir
,new_phi
)))
1241 | CTL.AG
(dir
,phi
) ->
1242 let (acc
,new_phi
) = replace_formulas dec phi
in
1243 (acc
,CTL.rewrap f
(CTL.AG
(dir
,new_phi
)))
1244 | CTL.AU
(dir
,phi1
,phi2,phi3,phi4
) ->
1245 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1246 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1247 let (acc3
,new_phi3
) = replace_formulas dec
phi3 in
1248 let (acc4
,new_phi4
) = replace_formulas dec phi4
in
1249 (acc1
@acc2
@acc3
@acc4
,
1250 CTL.rewrap f
(CTL.AU
(dir
,new_phi1
,new_phi2
,new_phi3
,new_phi4
)))
1251 | CTL.EF
(dir
,phi
) ->
1252 let (acc
,new_phi
) = replace_formulas dec phi
in
1253 (acc
,CTL.rewrap f
(CTL.EF
(dir
,new_phi
)))
1254 | CTL.EX
(dir
,phi
) ->
1255 let (acc
,new_phi
) = replace_formulas dec phi
in
1256 (acc
,CTL.rewrap f
(CTL.EX
(dir
,new_phi
)))
1257 | CTL.EG
(dir
,phi
) ->
1258 let (acc
,new_phi
) = replace_formulas dec phi
in
1259 (acc
,CTL.rewrap f
(CTL.EG
(dir
,new_phi
)))
1260 | CTL.EU
(dir
,phi1
,phi2) ->
1261 let (acc1
,new_phi1
) = replace_formulas dec phi1
in
1262 let (acc2
,new_phi2
) = replace_formulas dec
phi2 in
1263 (acc1
@acc2
,CTL.rewrap f
(CTL.EU
(dir
,new_phi1
,new_phi2
)))
1264 | _
-> failwith
"not possible"
1267 (Hashtbl.create
(50) :
1268 ((cocci_predicate
,string,Wrapper_ctl.info
) CTL.generic_ctl
,
1269 string list
(* fvs *) *
1270 string list
(* intersection of fvs of subterms *))
1274 try let (fvs,_
) = Hashtbl.find
ctlfv_table f
in fvs
1276 let ((fvs,_
) as res
) =
1277 match CTL.unwrap f
with
1278 CTL.False
| CTL.True
| CTL.Pred
(_
) -> ([],[])
1279 | CTL.Not
(phi
) | CTL.Exists
(_
,phi
)
1280 | CTL.AX
(_
,phi
) | CTL.AG
(_
,phi
)
1281 | CTL.EF
(_
,phi
) | CTL.EX
(_
,phi
) | CTL.EG
(_
,phi
) -> (ctl_fvs phi
,[])
1282 | CTL.AU
(_
,phi1
,phi2,phi3,phi4
) ->
1283 let phi1fvs = ctl_fvs phi1
in
1284 let phi2fvs = ctl_fvs phi2 in
1285 (* phi3 has the same fvs as phi1 and phi4 as phi2 *)
1286 (Common.union_set
phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1287 | CTL.And
(phi1
,phi2) | CTL.Or
(phi1
,phi2) | CTL.SeqOr
(phi1
,phi2)
1288 | CTL.Implies
(phi1
,phi2) | CTL.AF
(_
,phi1
,phi2) | CTL.EU
(_
,phi1
,phi2) ->
1289 let phi1fvs = ctl_fvs phi1
in
1290 let phi2fvs = ctl_fvs phi2 in
1291 (Common.union_set
phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1292 | CTL.Ref
(v) -> ([v],[v])
1293 | CTL.Let
(v,term,body) ->
1294 let phi1fvs = ctl_fvs term in
1295 let phi2fvs = Common.minus_set
(ctl_fvs body) [v] in
1296 (Common.union_set
phi1fvs phi2fvs,intersect phi1fvs phi2fvs) in
1297 Hashtbl.add
ctlfv_table f res
;
1300 let rev_order_bindings b
=
1303 (function (nm,term) ->
1304 let (fvs,_
) = Hashtbl.find
ctlfv_table term in (nm,fvs,term))
1306 let rec loop bound
= function
1309 let (now_bound
,still_unbound
) =
1310 List.partition
(function (_
,fvs,_
) -> subset fvs bound
)
1312 let get_names = List.map
(function (x
,_
,_
) -> x
) in
1313 now_bound
@ (loop ((get_names now_bound
) @ bound
) still_unbound
) in
1316 let drop_bindings b f
= (* innermost bindings first in b *)
1317 let process_binary f ffvs inter
nm term fail
=
1318 if List.mem
nm inter
1319 then CTL.rewrap f
(CTL.Let
(nm,term,f
))
1320 else CTL.rewrap f
(fail
()) in
1322 let _ = ctl_fvs f
in Hashtbl.find
ctlfv_table f
in
1323 let rec drop_one nm term f
=
1324 match CTL.unwrap f
with
1328 | CTL.Not
(phi
) -> CTL.rewrap f
(CTL.Not
(drop_one nm term phi
))
1329 | CTL.Exists
(v,phi
) -> CTL.rewrap f
(CTL.Exists
(v,drop_one nm term phi
))
1330 | CTL.And
(phi1
,phi2) ->
1331 let (ffvs
,inter
) = find_fvs f
in
1332 process_binary f ffvs inter
nm term
1333 (function _ -> CTL.And
(drop_one nm term phi1
,drop_one nm term phi2))
1334 | CTL.Or
(phi1
,phi2) ->
1335 let (ffvs
,inter
) = find_fvs f
in
1336 process_binary f ffvs inter
nm term
1337 (function _ -> CTL.Or
(drop_one nm term phi1
,drop_one nm term phi2))
1338 | CTL.SeqOr
(phi1
,phi2) ->
1339 let (ffvs
,inter
) = find_fvs f
in
1340 process_binary f ffvs inter
nm term
1342 CTL.SeqOr
(drop_one nm term phi1
,drop_one nm term phi2))
1343 | CTL.Implies
(phi1
,phi2) ->
1344 let (ffvs
,inter
) = find_fvs f
in
1345 process_binary f ffvs inter
nm term
1347 CTL.Implies
(drop_one nm term phi1
,drop_one nm term phi2))
1348 | CTL.AF
(dir
,phi1
,phi2) ->
1349 let (ffvs
,inter
) = find_fvs f
in
1350 process_binary f ffvs inter
nm term
1352 CTL.AF
(dir
,drop_one nm term phi1
,drop_one nm term phi2))
1353 | CTL.AX
(dir
,phi
) ->
1354 CTL.rewrap f
(CTL.AX
(dir
,drop_one nm term phi
))
1355 | CTL.AG
(dir
,phi
) -> CTL.rewrap f
(CTL.AG
(dir
,drop_one nm term phi
))
1356 | CTL.AU
(dir
,phi1
,phi2,phi3,phi4
) ->
1357 let (ffvs
,inter
) = find_fvs f
in
1358 process_binary f ffvs inter
nm term
1360 CTL.AU
(dir
,drop_one nm term phi1
,drop_one nm term phi2,
1361 drop_one nm term phi3,drop_one nm term phi4
))
1362 | CTL.EF
(dir
,phi
) -> CTL.rewrap f
(CTL.EF
(dir
,drop_one nm term phi
))
1363 | CTL.EX
(dir
,phi
) ->
1364 CTL.rewrap f
(CTL.EX
(dir
,drop_one nm term phi
))
1365 | CTL.EG
(dir
,phi
) -> CTL.rewrap f
(CTL.EG
(dir
,drop_one nm term phi
))
1366 | CTL.EU
(dir
,phi1
,phi2) ->
1367 let (ffvs
,inter
) = find_fvs f
in
1368 process_binary f ffvs inter
nm term
1370 CTL.EU
(dir
,drop_one nm term phi1
,drop_one nm term phi2))
1371 | (CTL.Ref
(v) as x
) -> process_binary f
[v] [v] nm term (function _ -> x
)
1372 | CTL.Let
(v,term1
,body) ->
1373 let (ffvs
,inter
) = find_fvs f
in
1374 process_binary f ffvs inter
nm term
1376 CTL.Let
(v,drop_one nm term term1
,drop_one nm term body)) in
1378 (function processed -> function (nm,_,term) -> drop_one nm term processed)
1382 failwith
"this code should not be used!!!"(*;
1383 Hashtbl.clear formula_table;
1384 Hashtbl.clear ctlfv_table;
1385 (* create a count of the number of occurrences of each subformula *)
1386 collect_duplicates f
;
1387 (* give names to things that appear more than once *)
1389 (* replace duplicated formulas by their variables *)
1390 let (bindings
,new_f
) = replace_formulas 0 f
in
1391 (* collect fvs of terms in bindings and new_f *)
1392 List.iter
(function f
-> let _ = ctl_fvs f
in ())
1393 (new_f
::(List.map
(function (_,term) -> term) bindings
));
1394 (* sort bindings with uses before defs *)
1395 let bindings = rev_order_bindings bindings in
1396 (* insert bindings as lets into the formula *)
1397 let res = drop_bindings bindings new_f
in
1400 (* --------------------------------------------------------------------- *)
1401 (* Function declaration *)
1403 let top_level used_after t
=
1404 match Ast.unwrap t
with
1405 Ast.DECL
(decl
) -> failwith
"not supported decl"
1406 | Ast.INCLUDE
(inc
,s
) ->
1407 (* no indication of whether inc or s is modified *)
1408 wrap 0 (CTL.Pred
((Lib_engine.Include
(inc
,s
),CTL.Control
)))
1409 | Ast.FILEINFO
(old_file
,new_file
) -> failwith
"not supported fileinfo"
1410 | Ast.FUNCTION
(stmt
) ->
1411 (*Printf.printf "orig\n";
1412 Pretty_print_cocci.statement "" stmt;
1413 Format.print_newline();*)
1414 let unopt = elim_opt.V.rebuilder_statement stmt
in
1415 (*Printf.printf "unopt\n";
1416 Pretty_print_cocci.statement "" unopt;
1417 Format.print_newline();*)
1418 let unopt = preprocess_dots_e unopt in
1420 (statement
unopt used_after Tail
[] false)
1421 | Ast.CODE
(stmt_dots
) ->
1422 let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots
in
1423 let unopt = preprocess_dots unopt in
1425 (statement_list unopt used_after Tail
[] false)
1426 | Ast.ERRORWORDS
(exps
) -> failwith
"not supported errorwords"
1428 (* --------------------------------------------------------------------- *)
1432 let bind x y
= x
or y
in
1433 let option_default = false in
1434 let mcode r x
= false in
1435 let statement r k s
=
1436 match Ast.unwrap s
with Ast.Dots
(_,_,_) -> true | _ -> k s
in
1437 let continue r k e
= k e
in
1438 let stop r k e
= false in
1440 V.combiner
bind option_default
1441 mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
1442 continue continue continue
1443 stop stop stop stop stop stop stop statement continue continue in
1444 res.V.combiner_top_level
1446 (* --------------------------------------------------------------------- *)
1449 let asttoctl l used_after
=
1456 match Ast.unwrap t
with Ast.ERRORWORDS
(exps
) -> false | _ -> true)
1458 List.map2
top_level used_after
l
1460 let pp_cocci_predicate (pred
,modif
) =
1461 Pretty_print_engine.pp_predicate pred
1463 let cocci_predicate_to_string (pred
,modif
) =
1464 Pretty_print_engine.predicate_to_string pred