Commit | Line | Data |
---|---|---|
0708f913 C |
1 | (* |
2 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller | |
4 | * This file is part of Coccinelle. | |
5 | * | |
6 | * Coccinelle is free software: you can redistribute it and/or modify | |
7 | * it under the terms of the GNU General Public License as published by | |
8 | * the Free Software Foundation, according to version 2 of the License. | |
9 | * | |
10 | * Coccinelle is distributed in the hope that it will be useful, | |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
13 | * GNU General Public License for more details. | |
14 | * | |
15 | * You should have received a copy of the GNU General Public License | |
16 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
17 | * | |
18 | * The authors reserve the right to distribute this or future versions of | |
19 | * Coccinelle under other licenses. | |
20 | *) | |
21 | ||
22 | ||
23 | (* true = don't see all matched nodes, only modified ones *) | |
24 | let onlyModif = ref true(*false*) | |
25 | (* set to true for line numbers in the output of ctl_engine *) | |
26 | let line_numbers = ref false | |
27 | (* if true, only eg if header is included in not for ...s *) | |
28 | let simple_get_end = ref false(*true*) | |
29 | ||
30 | (* Question: where do we put the existential quantifier for or. At the | |
31 | moment, let it float inwards. *) | |
32 | ||
33 | (* nest shouldn't overlap with what comes after. not checked for. *) | |
34 | ||
35 | module Ast = Ast_cocci | |
36 | module V = Visitor_ast | |
37 | module CTL = Ast_ctl | |
38 | module FV = Free_vars | |
39 | ||
40 | let warning s = Printf.fprintf stderr "warning: %s\n" s | |
41 | ||
42 | type cocci_predicate = Lib_engine.predicate * string Ast_ctl.modif | |
43 | type formula = | |
44 | (cocci_predicate,string, Wrapper_ctl.info) Ast_ctl.generic_ctl | |
45 | ||
46 | ||
47 | let aftpred = (Lib_engine.After,CTL.Control) | |
48 | let retpred = (Lib_engine.Return,CTL.Control) | |
49 | let exitpred = (Lib_engine.ErrorExit,CTL.Control) | |
50 | ||
51 | let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1 | |
52 | let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1 | |
53 | ||
54 | (* --------------------------------------------------------------------- *) | |
55 | ||
56 | let rec drop_vs f = | |
57 | CTL.rewrap f | |
58 | (match CTL.unwrap f with | |
59 | CTL.False as x -> x | |
60 | | CTL.True as x -> x | |
61 | | CTL.Pred(p) as x -> x | |
62 | | CTL.Not(phi) -> CTL.Not(drop_vs phi) | |
63 | | CTL.Exists(v,phi) -> | |
64 | (match CTL.unwrap phi with | |
65 | CTL.Pred((x,CTL.Modif v1)) when v = v1 -> CTL.Pred((x,CTL.Control)) | |
66 | | _ -> CTL.Exists(v,drop_vs phi)) | |
67 | | CTL.And(phi1,phi2) -> CTL.And(drop_vs phi1,drop_vs phi2) | |
68 | | CTL.Or(phi1,phi2) -> CTL.Or(drop_vs phi1,drop_vs phi2) | |
69 | | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(drop_vs phi1,drop_vs phi2) | |
70 | | CTL.Implies(phi1,phi2) -> CTL.Implies(drop_vs phi1,drop_vs phi2) | |
71 | | CTL.AF(dir,phi1,phi2) -> CTL.AF(dir,drop_vs phi1,drop_vs phi2) | |
72 | | CTL.AX(dir,phi) -> CTL.AX(dir,drop_vs phi) | |
73 | | CTL.AG(dir,phi) -> CTL.AG(dir,drop_vs phi) | |
74 | | CTL.AU(dir,phi1,phi2,phi3,phi4) -> | |
75 | CTL.AU(dir,drop_vs phi1,drop_vs phi2,drop_vs phi3,drop_vs phi4) | |
76 | | CTL.EF(dir,phi) -> CTL.EF(dir,drop_vs phi) | |
77 | | CTL.EX(dir,phi) -> CTL.EX(dir,drop_vs phi) | |
78 | | CTL.EG(dir,phi) -> CTL.EG(dir,drop_vs phi) | |
79 | | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,drop_vs phi1,drop_vs phi2) | |
80 | | CTL.Ref(v) as x -> x | |
81 | | CTL.Let(v,term1,body) -> CTL.Let(v,drop_vs term1,drop_vs body)) | |
82 | ||
83 | (* --------------------------------------------------------------------- *) | |
84 | ||
85 | let wrap n ctl = (ctl,n) | |
86 | ||
87 | let aftret = | |
88 | wrap 0 (CTL.Or(wrap 0 (CTL.Pred aftpred),wrap 0 (CTL.Pred exitpred))) | |
89 | ||
90 | let wrapImplies n (x,y) = wrap n (CTL.Implies(x,y)) | |
91 | let wrapExists n (x,y) = wrap n (CTL.Exists(x,y)) | |
92 | let wrapAnd n (x,y) = wrap n (CTL.And(x,y)) | |
93 | let wrapOr n (x,y) = wrap n (CTL.Or(x,y)) | |
94 | let wrapSeqOr n (x,y) = wrap n (CTL.SeqOr(x,y)) | |
95 | let wrapAU n (x,y) = wrap n (CTL.AU(CTL.FORWARD,x,y,drop_vs x,drop_vs y)) | |
96 | let wrapEU n (x,y) = wrap n (CTL.EU(CTL.FORWARD,x,y)) | |
97 | let wrapAX n (x) = wrap n (CTL.AX(CTL.FORWARD,x)) | |
98 | let wrapBackAX n (x) = wrap n (CTL.AX(CTL.BACKWARD,x)) | |
99 | let wrapEX n (x) = wrap n (CTL.EX(CTL.FORWARD,x)) | |
100 | let wrapBackEX n (x) = wrap n (CTL.EX(CTL.BACKWARD,x)) | |
101 | let wrapAG n (x) = wrap n (CTL.AG(CTL.FORWARD,x)) | |
102 | let wrapEG n (x) = wrap n (CTL.EG(CTL.FORWARD,x)) | |
103 | let wrapAF n (x) = wrap n (CTL.AF(CTL.FORWARD,x,drop_vs x)) | |
104 | let wrapEF n (x) = wrap n (CTL.EF(CTL.FORWARD,x)) | |
105 | let wrapNot n (x) = wrap n (CTL.Not(x)) | |
106 | let wrapPred n (x) = wrap n (CTL.Pred(x)) | |
107 | let wrapLet n (x,y,z) = wrap n (CTL.Let(x,y,z)) | |
108 | let wrapRef n (x) = wrap n (CTL.Ref(x)) | |
109 | ||
110 | (* --------------------------------------------------------------------- *) | |
111 | ||
112 | let get_option fn = function | |
113 | None -> None | |
114 | | Some x -> Some (fn x) | |
115 | ||
116 | let get_list_option fn = function | |
117 | None -> [] | |
118 | | Some x -> fn x | |
119 | ||
120 | (* --------------------------------------------------------------------- *) | |
121 | (* --------------------------------------------------------------------- *) | |
122 | (* Eliminate OptStm *) | |
123 | ||
124 | (* for optional thing with nothing after, should check that the optional thing | |
125 | never occurs. otherwise the matching stops before it occurs *) | |
126 | let elim_opt = | |
127 | let mcode x = x in | |
128 | let donothing r k e = k e in | |
129 | ||
130 | let fvlist l = | |
131 | List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in | |
132 | ||
133 | let rec dots_list unwrapped wrapped = | |
134 | match (unwrapped,wrapped) with | |
135 | ([],_) -> [] | |
136 | ||
137 | | (Ast.Dots(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest, | |
138 | d0::_::d1::rest) | |
139 | | (Ast.Nest(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest, | |
140 | d0::_::d1::rest) -> | |
141 | let l = Ast.get_line stm in | |
142 | let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in | |
143 | let new_rest2 = dots_list urest rest in | |
144 | let fv_rest1 = fvlist new_rest1 in | |
145 | let fv_rest2 = fvlist new_rest2 in | |
146 | [d0;(Ast.Disj[(Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots); | |
147 | (Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots)], | |
148 | l,fv_rest1,Ast.NoDots)] | |
149 | ||
150 | | (Ast.OptStm(stm)::urest,_::rest) -> | |
151 | let l = Ast.get_line stm in | |
152 | let new_rest1 = dots_list urest rest in | |
153 | let new_rest2 = stm::new_rest1 in | |
154 | let fv_rest1 = fvlist new_rest1 in | |
155 | let fv_rest2 = fvlist new_rest2 in | |
156 | [(Ast.Disj[(Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots); | |
157 | (Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots)], | |
158 | l,fv_rest2,Ast.NoDots)] | |
159 | ||
160 | | ([Ast.Dots(_,_,_);Ast.OptStm(stm)],[d1;_]) -> | |
161 | let l = Ast.get_line stm in | |
162 | let fv_stm = Ast.get_fvs stm in | |
163 | let fv_d1 = Ast.get_fvs d1 in | |
164 | let fv_both = Common.union_set fv_stm fv_d1 in | |
165 | [d1;(Ast.Disj[(Ast.DOTS([stm]),l,fv_stm,Ast.NoDots); | |
166 | (Ast.DOTS([d1]),l,fv_d1,Ast.NoDots)], | |
167 | l,fv_both,Ast.NoDots)] | |
168 | ||
169 | | ([Ast.Nest(_,_,_);Ast.OptStm(stm)],[d1;_]) -> | |
170 | let l = Ast.get_line stm in | |
171 | let rw = Ast.rewrap stm in | |
172 | let rwd = Ast.rewrap stm in | |
173 | let dots = | |
174 | Ast.Dots(("...",{ Ast.line = 0; Ast.column = 0 }, | |
175 | Ast.CONTEXT(Ast.NOTHING)), | |
176 | Ast.NoWhen,[]) in | |
177 | [d1;rw(Ast.Disj[rwd(Ast.DOTS([stm])); | |
178 | (Ast.DOTS([rw dots]),l,[],Ast.NoDots)])] | |
179 | ||
180 | | (_::urest,stm::rest) -> stm :: (dots_list urest rest) | |
181 | | _ -> failwith "not possible" in | |
182 | ||
183 | let stmtdotsfn r k d = | |
184 | let d = k d in | |
185 | Ast.rewrap d | |
186 | (match Ast.unwrap d with | |
187 | Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l) | |
188 | | Ast.CIRCLES(l) -> failwith "elimopt: not supported" | |
189 | | Ast.STARS(l) -> failwith "elimopt: not supported") in | |
190 | ||
191 | V.rebuilder | |
192 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
193 | donothing donothing stmtdotsfn | |
194 | donothing donothing donothing donothing donothing donothing donothing | |
195 | donothing donothing donothing | |
196 | ||
197 | (* --------------------------------------------------------------------- *) | |
198 | (* Count depth of braces. The translation of a closed brace appears deeply | |
199 | nested within the translation of the sequence term, so the name of the | |
200 | paren var has to take into account the names of the nested braces. On the | |
201 | other hand the close brace does not escape, so we don't have to take into | |
202 | account other paren variable names. *) | |
203 | ||
204 | (* called repetitively, which is inefficient, but less trouble than adding a | |
205 | new field to Seq and FunDecl *) | |
206 | let count_nested_braces s = | |
207 | let bind x y = max x y in | |
208 | let option_default = 0 in | |
209 | let stmt_count r k s = | |
210 | match Ast.unwrap s with | |
211 | Ast.Seq(_,_,_,_,_) | Ast.FunDecl(_,_,_,_,_,_) -> (k s) + 1 | |
212 | | _ -> k s in | |
213 | let donothing r k e = k e in | |
214 | let mcode r x = 0 in | |
215 | let recursor = V.combiner bind option_default | |
216 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
217 | donothing donothing donothing | |
218 | donothing donothing donothing donothing donothing donothing | |
219 | donothing stmt_count donothing donothing in | |
220 | "p"^(string_of_int (recursor.V.combiner_statement s)) | |
221 | ||
222 | (* --------------------------------------------------------------------- *) | |
223 | (* Top-level code *) | |
224 | ||
225 | let ctr = ref 0 | |
226 | let fresh_var _ = | |
227 | let c = !ctr in | |
228 | (*ctr := !ctr + 1;*) | |
229 | Printf.sprintf "v%d" c | |
230 | ||
231 | let labctr = ref 0 | |
232 | let fresh_label_var s = | |
233 | let c = !labctr in | |
234 | labctr := !labctr + 1; | |
235 | Printf.sprintf "%s%d" s c | |
236 | ||
237 | let lctr = ref 0 | |
238 | let fresh_let_var _ = | |
239 | let c = !lctr in | |
240 | lctr := !lctr + 1; | |
241 | Printf.sprintf "l%d" c | |
242 | ||
243 | let sctr = ref 0 | |
244 | let fresh_metavar _ = | |
245 | let c = !sctr in | |
246 | (*sctr := !sctr + 1;*) | |
247 | Printf.sprintf "_S%d" c | |
248 | ||
249 | let get_unquantified quantified vars = | |
250 | List.filter (function x -> not (List.mem x quantified)) vars | |
251 | ||
252 | type after = After of formula | Guard of formula | Tail | |
253 | ||
254 | let make_seq n l = | |
255 | let rec loop = function | |
256 | [] -> failwith "not possible" | |
257 | | [x] -> x | |
258 | | x::xs -> wrapAnd n (x,wrapAX n (loop xs)) in | |
259 | loop l | |
260 | ||
261 | let make_seq_after2 n first = function | |
262 | After rest -> wrapAnd n (first,wrapAX n (wrapAX n rest)) | |
263 | | _ -> first | |
264 | ||
265 | let make_seq_after n first = function | |
266 | After rest -> make_seq n [first;rest] | |
267 | | _ -> first | |
268 | ||
269 | let a2n = function After f -> Guard f | x -> x | |
270 | ||
271 | let and_opt n first = function | |
272 | After rest -> wrapAnd n (first,rest) | |
273 | | _ -> first | |
274 | ||
275 | let contains_modif = | |
276 | let bind x y = x or y in | |
277 | let option_default = false in | |
278 | let mcode r (_,_,kind) = | |
279 | match kind with | |
280 | Ast.MINUS(_) -> true | |
281 | | Ast.PLUS -> failwith "not possible" | |
282 | | Ast.CONTEXT(info) -> not (info = Ast.NOTHING) in | |
283 | let do_nothing r k e = k e in | |
284 | let recursor = | |
285 | V.combiner bind option_default | |
286 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
287 | do_nothing do_nothing do_nothing | |
288 | do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing | |
289 | do_nothing do_nothing do_nothing do_nothing in | |
290 | recursor.V.combiner_rule_elem | |
291 | ||
292 | let make_match n guard used_after code = | |
293 | if guard | |
294 | then wrapPred n (Lib_engine.Match(code),CTL.Control) | |
295 | else | |
296 | let v = fresh_var() in | |
297 | if contains_modif code | |
298 | then wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.Modif v)) | |
299 | else | |
300 | let any_used_after = | |
301 | List.exists (function x -> List.mem x used_after) (Ast.get_fvs code) in | |
302 | if !onlyModif && not any_used_after | |
303 | then wrapPred n (Lib_engine.Match(code),CTL.Control) | |
304 | else wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.UnModif v)) | |
305 | ||
306 | let make_raw_match n code = wrapPred n (Lib_engine.Match(code),CTL.Control) | |
307 | ||
308 | let rec seq_fvs quantified = function | |
309 | [] -> [] | |
310 | | fv1::fvs -> | |
311 | let t1fvs = get_unquantified quantified fv1 in | |
312 | let termfvs = | |
313 | List.fold_left Common.union_set [] | |
314 | (List.map (get_unquantified quantified) fvs) in | |
315 | let bothfvs = Common.inter_set t1fvs termfvs in | |
316 | let t1onlyfvs = Common.minus_set t1fvs bothfvs in | |
317 | let new_quantified = Common.union_set bothfvs quantified in | |
318 | (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs) | |
319 | ||
320 | let seq_fvs2 quantified fv1 fv2 = | |
321 | match seq_fvs quantified [fv1;fv2] with | |
322 | [(t1fvs,bfvs);(t2fvs,[])] -> (t1fvs,bfvs,t2fvs) | |
323 | | _ -> failwith "impossible" | |
324 | ||
325 | let seq_fvs3 quantified fv1 fv2 fv3 = | |
326 | match seq_fvs quantified [fv1;fv2;fv3] with | |
327 | [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,[])] -> | |
328 | (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs) | |
329 | | _ -> failwith "impossible" | |
330 | ||
331 | let seq_fvs4 quantified fv1 fv2 fv3 fv4 = | |
332 | match seq_fvs quantified [fv1;fv2;fv3;fv4] with | |
333 | [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,[])] -> | |
334 | (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs) | |
335 | | _ -> failwith "impossible" | |
336 | ||
337 | let seq_fvs5 quantified fv1 fv2 fv3 fv4 fv5 = | |
338 | match seq_fvs quantified [fv1;fv2;fv3;fv4;fv5] with | |
339 | [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,b45fvs);(t5fvs,[])] -> | |
340 | (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs,b45fvs,t5fvs) | |
341 | | _ -> failwith "impossible" | |
342 | ||
343 | let quantify n = | |
344 | List.fold_right (function cur -> function code -> wrapExists n (cur,code)) | |
345 | ||
346 | let intersectll lst nested_list = | |
347 | List.filter (function x -> List.exists (List.mem x) nested_list) lst | |
348 | ||
349 | (* --------------------------------------------------------------------- *) | |
350 | (* annotate dots with before and after neighbors *) | |
351 | ||
352 | let rec get_before sl a = | |
353 | match Ast.unwrap sl with | |
354 | Ast.DOTS(x) -> | |
355 | let rec loop sl a = | |
356 | match sl with | |
357 | [] -> ([],a) | |
358 | | e::sl -> | |
359 | let (e,ea) = get_before_e e a in | |
360 | let (sl,sla) = loop sl ea in | |
361 | (e::sl,sla) in | |
362 | let (l,a) = loop x a in | |
363 | (Ast.rewrap sl (Ast.DOTS(l)),a) | |
364 | | Ast.CIRCLES(x) -> failwith "not supported" | |
365 | | Ast.STARS(x) -> failwith "not supported" | |
366 | ||
367 | and get_before_e s a = | |
368 | match Ast.unwrap s with | |
369 | Ast.Dots(d,Ast.NoWhen,t) -> | |
370 | (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a) | |
371 | | Ast.Dots(d,Ast.WhenNot w,t) -> | |
372 | let (w,_) = get_before w [] in | |
373 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a) | |
374 | | Ast.Dots(d,Ast.WhenAlways w,t) -> | |
375 | let (w,_) = get_before_e w [] in | |
376 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a) | |
377 | | Ast.Nest(stmt_dots,w,t) -> | |
378 | let (w,_) = List.split (List.map (function s -> get_before s []) w) in | |
379 | let (sd,_) = get_before stmt_dots a in | |
380 | let a = | |
381 | List.filter | |
382 | (function | |
383 | Ast.Other a -> | |
384 | let unifies = | |
385 | Unify_ast.unify_statement_dots | |
386 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in | |
387 | (match unifies with | |
388 | Unify_ast.MAYBE -> false | |
389 | | _ -> true) | |
390 | | Ast.Other_dots a -> | |
391 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in | |
392 | (match unifies with | |
393 | Unify_ast.MAYBE -> false | |
394 | | _ -> true) | |
395 | | _ -> true) | |
396 | a in | |
397 | (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots]) | |
398 | | Ast.Disj(stmt_dots_list) -> | |
399 | let (dsl,dsla) = | |
400 | List.split (List.map (function e -> get_before e a) stmt_dots_list) in | |
401 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) | |
402 | | Ast.Atomic(ast) -> | |
403 | (match Ast.unwrap ast with | |
404 | Ast.MetaStmt(_,_,_) -> (s,[]) | |
405 | | _ -> (s,[Ast.Other s])) | |
406 | | Ast.Seq(lbrace,decls,dots,body,rbrace) -> | |
407 | let index = count_nested_braces s in | |
408 | let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in | |
409 | let (bd,_) = get_before body dea in | |
410 | (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)), | |
411 | [Ast.WParen(rbrace,index)]) | |
412 | | Ast.IfThen(ifheader,branch,aft) -> | |
413 | let (br,_) = get_before_e branch [] in | |
414 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s]) | |
415 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
416 | let (br1,_) = get_before_e branch1 [] in | |
417 | let (br2,_) = get_before_e branch2 [] in | |
418 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) | |
419 | | Ast.While(header,body,aft) -> | |
420 | let (bd,_) = get_before_e body [] in | |
421 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) | |
422 | | Ast.For(header,body,aft) -> | |
423 | let (bd,_) = get_before_e body [] in | |
424 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) | |
425 | | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) -> | |
426 | let index = count_nested_braces s in | |
427 | let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in | |
428 | let (bd,_) = get_before body dea in | |
429 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[]) | |
430 | | _ -> failwith "not supported" | |
431 | ||
432 | let rec get_after sl a = | |
433 | match Ast.unwrap sl with | |
434 | Ast.DOTS(x) -> | |
435 | let rec loop sl = | |
436 | match sl with | |
437 | [] -> ([],a) | |
438 | | e::sl -> | |
439 | let (sl,sla) = loop sl in | |
440 | let (e,ea) = get_after_e e sla in | |
441 | (e::sl,ea) in | |
442 | let (l,a) = loop x in | |
443 | (Ast.rewrap sl (Ast.DOTS(l)),a) | |
444 | | Ast.CIRCLES(x) -> failwith "not supported" | |
445 | | Ast.STARS(x) -> failwith "not supported" | |
446 | ||
447 | and get_after_e s a = | |
448 | match Ast.unwrap s with | |
449 | Ast.Dots(d,Ast.NoWhen,t) -> | |
450 | (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a) | |
451 | | Ast.Dots(d,Ast.WhenNot w,t) -> | |
452 | let (w,_) = get_after w [] in | |
453 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a) | |
454 | | Ast.Dots(d,Ast.WhenAlways w,t) -> | |
455 | let (w,_) = get_after_e w [] in | |
456 | (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a) | |
457 | | Ast.Nest(stmt_dots,w,t) -> | |
458 | let (w,_) = List.split (List.map (function s -> get_after s []) w) in | |
459 | let (sd,_) = get_after stmt_dots a in | |
460 | let a = | |
461 | List.filter | |
462 | (function | |
463 | Ast.Other a -> | |
464 | let unifies = | |
465 | Unify_ast.unify_statement_dots | |
466 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in | |
467 | (match unifies with | |
468 | Unify_ast.MAYBE -> false | |
469 | | _ -> true) | |
470 | | Ast.Other_dots a -> | |
471 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in | |
472 | (match unifies with | |
473 | Unify_ast.MAYBE -> false | |
474 | | _ -> true) | |
475 | | _ -> true) | |
476 | a in | |
477 | (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots]) | |
478 | | Ast.Disj(stmt_dots_list) -> | |
479 | let (dsl,dsla) = | |
480 | List.split (List.map (function e -> get_after e a) stmt_dots_list) in | |
481 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) | |
482 | | Ast.Atomic(ast) -> | |
483 | (match Ast.unwrap ast with | |
484 | Ast.MetaStmt(nm,Ast.SequencibleAfterDots _,i) -> | |
485 | (* check after information for metavar optimization *) | |
486 | (* if the error is not desired, could just return [], then | |
487 | the optimization (check for EF) won't take place *) | |
488 | List.iter | |
489 | (function | |
490 | Ast.Other x -> | |
491 | (match Ast.unwrap x with | |
492 | Ast.Dots(_,_,_) | Ast.Nest(_,_,_) -> | |
493 | failwith | |
494 | "dots/nest not allowed before and after stmt metavar" | |
495 | | _ -> ()) | |
496 | | Ast.Other_dots x -> | |
497 | (match Ast.undots x with | |
498 | x::_ -> | |
499 | (match Ast.unwrap x with | |
500 | Ast.Dots(_,_,_) | Ast.Nest(_,_,_) -> | |
501 | failwith | |
502 | ("dots/nest not allowed before and after stmt "^ | |
503 | "metavar") | |
504 | | _ -> ()) | |
505 | | _ -> ()) | |
506 | | _ -> ()) | |
507 | a; | |
508 | (Ast.rewrap s | |
509 | (Ast.Atomic | |
510 | (Ast.rewrap s | |
511 | (Ast.MetaStmt(nm,Ast.SequencibleAfterDots a,i)))),[]) | |
512 | | Ast.MetaStmt(_,_,_) -> (s,[]) | |
513 | | _ -> (s,[Ast.Other s])) | |
514 | | Ast.Seq(lbrace,decls,dots,body,rbrace) -> | |
515 | let index = count_nested_braces s in | |
516 | let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in | |
517 | let (de,_) = get_after decls bda in | |
518 | (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)), | |
519 | [Ast.WParen(lbrace,index)]) | |
520 | | Ast.IfThen(ifheader,branch,aft) -> | |
521 | let (br,_) = get_after_e branch a in | |
522 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s]) | |
523 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
524 | let (br1,_) = get_after_e branch1 a in | |
525 | let (br2,_) = get_after_e branch2 a in | |
526 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) | |
527 | | Ast.While(header,body,aft) -> | |
528 | let (bd,_) = get_after_e body a in | |
529 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) | |
530 | | Ast.For(header,body,aft) -> | |
531 | let (bd,_) = get_after_e body a in | |
532 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) | |
533 | | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) -> | |
534 | let index = count_nested_braces s in | |
535 | let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in | |
536 | let (de,_) = get_after decls bda in | |
537 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[]) | |
538 | | _ -> failwith "not supported" | |
539 | ||
540 | ||
541 | let preprocess_dots sl = | |
542 | let (sl,_) = get_before sl [] in | |
543 | let (sl,_) = get_after sl [] in | |
544 | sl | |
545 | ||
546 | let preprocess_dots_e sl = | |
547 | let (sl,_) = get_before_e sl [] in | |
548 | let (sl,_) = get_after_e sl [] in | |
549 | sl | |
550 | ||
551 | (* --------------------------------------------------------------------- *) | |
552 | (* the main translation loop *) | |
553 | ||
554 | let decl_to_not_decl n dots stmt make_match f = | |
555 | if dots | |
556 | then f | |
557 | else | |
558 | let de = | |
559 | let md = Ast.make_meta_decl "_d" (Ast.CONTEXT(Ast.NOTHING)) in | |
560 | Ast.rewrap md (Ast.Decl md) in | |
561 | wrapAU n (make_match de, | |
562 | wrap n (CTL.And(wrap n (CTL.Not (make_match de)), f))) | |
563 | ||
564 | let rec statement_list stmt_list used_after after quantified guard = | |
565 | let n = if !line_numbers then Ast.get_line stmt_list else 0 in | |
566 | match Ast.unwrap stmt_list with | |
567 | Ast.DOTS(x) -> | |
568 | let rec loop quantified = function | |
569 | ([],_) -> (match after with After f -> f | _ -> wrap n CTL.True) | |
570 | | ([e],_) -> statement e used_after after quantified guard | |
571 | | (e::sl,fv::fvs) -> | |
572 | let shared = intersectll fv fvs in | |
573 | let unqshared = get_unquantified quantified shared in | |
574 | let new_quantified = Common.union_set unqshared quantified in | |
575 | quantify n unqshared | |
576 | (statement e used_after (After(loop new_quantified (sl,fvs))) | |
577 | new_quantified guard) | |
578 | | _ -> failwith "not possible" in | |
579 | loop quantified (x,List.map Ast.get_fvs x) | |
580 | | Ast.CIRCLES(x) -> failwith "not supported" | |
581 | | Ast.STARS(x) -> failwith "not supported" | |
582 | ||
583 | and statement stmt used_after after quantified guard = | |
584 | ||
585 | let n = if !line_numbers then Ast.get_line stmt else 0 in | |
586 | let wrapExists = wrapExists n in | |
587 | let wrapAnd = wrapAnd n in | |
588 | let wrapOr = wrapOr n in | |
589 | let wrapSeqOr = wrapSeqOr n in | |
590 | let wrapAU = wrapAU n in | |
591 | let wrapAX = wrapAX n in | |
592 | let wrapBackAX = wrapBackAX n in | |
593 | let wrapEX = wrapEX n in | |
594 | let wrapBackEX = wrapBackEX n in | |
595 | let wrapAG = wrapAG n in | |
596 | let wrapAF = wrapAF n in | |
597 | let wrapEF = wrapEF n in | |
598 | let wrapNot = wrapNot n in | |
599 | let wrapPred = wrapPred n in | |
600 | let make_seq = make_seq n in | |
601 | let make_seq_after2 = make_seq_after2 n in | |
602 | let make_seq_after = make_seq_after n in | |
603 | let and_opt = and_opt n in | |
604 | let quantify = quantify n in | |
605 | let make_match = make_match n guard used_after in | |
606 | let make_raw_match = make_raw_match n in | |
607 | ||
608 | let make_meta_rule_elem d = | |
609 | let nm = fresh_metavar() in | |
610 | Ast.make_meta_rule_elem nm d in | |
611 | ||
612 | match Ast.unwrap stmt with | |
613 | Ast.Atomic(ast) -> | |
614 | (match Ast.unwrap ast with | |
615 | Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.BEFOREAFTER(_,_)) as d)),seqible,_) | |
616 | | Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.AFTER(_)) as d)),seqible,_) -> | |
617 | let label_var = (*fresh_label_var*) "_lab" in | |
618 | let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in | |
619 | let prelabel_pred = | |
620 | wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in | |
621 | let matcher d = make_match (make_meta_rule_elem d) in | |
622 | let full_metamatch = matcher d in | |
623 | let first_metamatch = | |
624 | matcher | |
625 | (match d with | |
626 | Ast.CONTEXT(Ast.BEFOREAFTER(bef,_)) -> | |
627 | Ast.CONTEXT(Ast.BEFORE(bef)) | |
628 | | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING) | |
629 | | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in | |
630 | let middle_metamatch = | |
631 | matcher | |
632 | (match d with | |
633 | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING) | |
634 | | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in | |
635 | let last_metamatch = | |
636 | matcher | |
637 | (match d with | |
638 | Ast.CONTEXT(Ast.BEFOREAFTER(_,aft)) -> | |
639 | Ast.CONTEXT(Ast.AFTER(aft)) | |
640 | | Ast.CONTEXT(_) -> d | |
641 | | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in | |
642 | ||
643 | let left_or = | |
644 | make_seq | |
645 | [full_metamatch; and_opt (wrapNot(prelabel_pred)) after] in | |
646 | let right_or = | |
647 | make_seq | |
648 | [first_metamatch; | |
649 | wrapAU(middle_metamatch, | |
650 | make_seq | |
651 | [wrapAnd(last_metamatch,label_pred); | |
652 | and_opt (wrapNot(prelabel_pred)) after])] in | |
653 | let body f = | |
654 | wrapAnd(label_pred, | |
655 | f (wrapAnd(make_raw_match ast, | |
656 | wrapOr(left_or,right_or)))) in | |
657 | let id x = x in | |
658 | (match seqible with | |
659 | Ast.Sequencible | Ast.SequencibleAfterDots [] -> | |
660 | quantify (label_var::get_unquantified quantified [s]) | |
661 | (body | |
662 | (function x -> | |
663 | (wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))) | |
664 | | Ast.SequencibleAfterDots l -> | |
665 | let afts = | |
666 | List.map (process_bef_aft Tail quantified used_after n) l in | |
667 | let ors = | |
668 | List.fold_left (function x -> function y -> wrapOr(x,y)) | |
669 | (List.hd afts) (List.tl afts) in | |
670 | quantify (label_var::get_unquantified quantified [s]) | |
671 | (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))), | |
672 | body | |
673 | (function x -> | |
674 | wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))) | |
675 | | Ast.NotSequencible -> | |
676 | quantify (label_var::get_unquantified quantified [s]) (body id)) | |
677 | ||
678 | | Ast.MetaStmt((s,i,d),seqible,_) -> | |
679 | let label_var = (*fresh_label_var*) "_lab" in | |
680 | let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in | |
681 | let prelabel_pred = | |
682 | wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in | |
683 | let matcher d = make_match (make_meta_rule_elem d) in | |
684 | let first_metamatch = matcher d in | |
685 | let rest_metamatch = | |
686 | matcher | |
687 | (match d with | |
688 | Ast.MINUS(_) -> Ast.MINUS([]) | |
689 | | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING) | |
690 | | Ast.PLUS -> failwith "not possible") in | |
691 | (* first_nodea and first_nodeb are separated here and above to | |
692 | improve let sharing - only first_nodea is unique to this site *) | |
693 | let first_nodeb = first_metamatch in | |
694 | let rest_nodes = wrapAnd(rest_metamatch,prelabel_pred) in | |
695 | let last_node = and_opt (wrapNot(prelabel_pred)) after in | |
696 | let body f = | |
697 | wrapAnd | |
698 | (label_pred, | |
699 | f (wrapAnd | |
700 | (make_raw_match ast, | |
701 | (make_seq | |
702 | [first_nodeb; wrapAU(rest_nodes,last_node)])))) in | |
703 | (match seqible with | |
704 | Ast.Sequencible | Ast.SequencibleAfterDots [] -> | |
705 | quantify (label_var::get_unquantified quantified [s]) | |
706 | (body | |
707 | (function x -> wrapAnd(wrapNot(wrapBackAX(label_pred)),x))) | |
708 | | Ast.SequencibleAfterDots l -> | |
709 | let afts = | |
710 | List.map (process_bef_aft Tail quantified used_after n) l in | |
711 | let ors = | |
712 | List.fold_left (function x -> function y -> wrapOr(x,y)) | |
713 | (List.hd afts) (List.tl afts) in | |
714 | quantify (label_var::get_unquantified quantified [s]) | |
715 | (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))), | |
716 | body | |
717 | (function x -> | |
718 | wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))) | |
719 | | Ast.NotSequencible -> | |
720 | quantify (label_var::get_unquantified quantified [s]) | |
721 | (body (function x -> x))) | |
722 | | _ -> | |
723 | let stmt_fvs = Ast.get_fvs stmt in | |
724 | let fvs = get_unquantified quantified stmt_fvs in | |
725 | let between_dots = Ast.get_dots_bef_aft stmt in | |
726 | let term = make_match ast in | |
727 | let term = | |
728 | match between_dots with | |
729 | Ast.BetweenDots brace_term -> | |
730 | (match Ast.unwrap brace_term with | |
731 | Ast.Atomic(brace_ast) -> | |
732 | let case1 = | |
733 | wrapAnd | |
734 | (wrapOr | |
735 | (wrapBackEX | |
736 | (wrapPred(Lib_engine.TrueBranch,CTL.Control)), | |
737 | wrapBackEX | |
738 | (wrapBackEX(wrapPred(Lib_engine.FalseBranch, | |
739 | CTL.Control)))), | |
740 | make_match brace_ast) in | |
741 | let case2 = | |
742 | wrapAnd | |
743 | (wrapNot | |
744 | (wrapOr | |
745 | (wrapBackEX | |
746 | (wrapPred(Lib_engine.TrueBranch,CTL.Control)), | |
747 | wrapBackEX | |
748 | (wrapBackEX(wrapPred(Lib_engine.FalseBranch, | |
749 | CTL.Control))))), | |
750 | term) in | |
751 | wrapOr(case1,case2) | |
752 | | _ -> failwith "not possible") | |
753 | | Ast.NoDots -> term in | |
754 | make_seq_after (quantify fvs term) after) | |
755 | | Ast.Seq(lbrace,decls,dots,body,rbrace) -> | |
756 | let (lbfvs,b1fvs,_,b2fvs,_,b3fvs,rbfvs) = | |
757 | seq_fvs4 quantified | |
758 | (Ast.get_fvs lbrace) (Ast.get_fvs decls) | |
759 | (Ast.get_fvs body) (Ast.get_fvs rbrace) in | |
760 | let v = count_nested_braces stmt in | |
761 | let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in | |
762 | let start_brace = | |
763 | wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in | |
764 | let end_brace = | |
765 | wrapAnd(quantify rbfvs (make_match rbrace),paren_pred) in | |
766 | let new_quantified2 = | |
767 | Common.union_set b1fvs (Common.union_set b2fvs quantified) in | |
768 | let new_quantified3 = Common.union_set b3fvs new_quantified2 in | |
769 | wrapExists | |
770 | (v,quantify b1fvs | |
771 | (make_seq | |
772 | [start_brace; | |
773 | quantify b2fvs | |
774 | (statement_list decls used_after | |
775 | (After | |
776 | (decl_to_not_decl n dots stmt make_match | |
777 | (quantify b3fvs | |
778 | (statement_list body used_after | |
779 | (After (make_seq_after end_brace after)) | |
780 | new_quantified3 guard)))) | |
781 | new_quantified2 guard)])) | |
782 | | Ast.IfThen(ifheader,branch,aft) -> | |
783 | ||
784 | (* "if (test) thn" becomes: | |
785 | if(test) & AX((TrueBranch & AX thn) v FallThrough v After) | |
786 | ||
787 | "if (test) thn; after" becomes: | |
788 | if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after)) | |
789 | & EX After | |
790 | *) | |
791 | ||
792 | (* free variables *) | |
793 | let (efvs,bfvs,_) = | |
794 | seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch) in | |
795 | let new_quantified = Common.union_set bfvs quantified in | |
796 | (* if header *) | |
797 | let if_header = quantify efvs (make_match ifheader) in | |
798 | (* then branch and after *) | |
799 | let true_branch = | |
800 | make_seq | |
801 | [wrapPred(Lib_engine.TrueBranch,CTL.Control); | |
802 | statement branch used_after (a2n after) new_quantified guard] in | |
803 | let fall_branch = wrapPred(Lib_engine.FallThrough,CTL.Control) in | |
804 | let after_pred = wrapPred(Lib_engine.After,CTL.Control) in | |
805 | let (aft_needed,after_branch) = | |
806 | match aft with | |
807 | Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after) | |
808 | | _ -> | |
809 | (true, | |
810 | make_seq_after after_pred | |
811 | (After | |
812 | (make_seq_after (make_match (make_meta_rule_elem aft)) | |
813 | after))) in | |
814 | let or_cases = wrapOr(true_branch,wrapOr(fall_branch,after_branch)) in | |
815 | (* the code *) | |
816 | (match (after,aft_needed) with | |
817 | (After _,_) (* pattern doesn't end here *) | |
818 | | (_,true) (* + code added after *) -> | |
819 | quantify bfvs | |
820 | (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred))) | |
821 | | _ -> quantify bfvs (wrapAnd(if_header, wrapAX or_cases))) | |
822 | ||
823 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> | |
824 | ||
825 | (* "if (test) thn else els" becomes: | |
826 | if(test) & AX((TrueBranch & AX thn) v | |
827 | (FalseBranch & AX (else & AX els)) v After) | |
828 | & EX FalseBranch | |
829 | ||
830 | "if (test) thn else els; after" becomes: | |
831 | if(test) & AX((TrueBranch & AX thn) v | |
832 | (FalseBranch & AX (else & AX els)) v | |
833 | (After & AXAX after)) | |
834 | & EX FalseBranch | |
835 | & EX After | |
836 | ||
837 | ||
838 | Note that we rely on the well-formedness of C programs. For example, we | |
839 | do not use EX to check that there is at least one then branch, because | |
840 | there is always one. And we do not check that there is only one then or | |
841 | else branch, because these again are always the case in a well-formed C | |
842 | program. *) | |
843 | (* free variables *) | |
844 | let (e1fvs,b1fvs,s1fvs) = | |
845 | seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch1) in | |
846 | let (e2fvs,b2fvs,s2fvs) = | |
847 | seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch2) in | |
848 | let bothfvs = | |
849 | Common.union_set | |
850 | (Common.union_set b1fvs b2fvs) | |
851 | (Common.inter_set s1fvs s2fvs) in | |
852 | let exponlyfvs = Common.inter_set e1fvs e2fvs in | |
853 | let new_quantified = Common.union_set bothfvs quantified in | |
854 | (* if header *) | |
855 | let if_header = quantify exponlyfvs (make_match ifheader) in | |
856 | (* then and else branches *) | |
857 | let true_branch = | |
858 | make_seq | |
859 | [wrapPred(Lib_engine.TrueBranch,CTL.Control); | |
860 | statement branch1 used_after (a2n after) new_quantified guard] in | |
861 | let false_pred = wrapPred(Lib_engine.FalseBranch,CTL.Control) in | |
862 | let false_branch = | |
863 | make_seq | |
864 | [false_pred; make_match els; | |
865 | statement branch2 used_after (a2n after) new_quantified guard] in | |
866 | let after_pred = wrapPred(Lib_engine.After,CTL.Control) in | |
867 | let (aft_needed,after_branch) = | |
868 | match aft with | |
869 | Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after) | |
870 | | _ -> | |
871 | (true, | |
872 | make_seq_after after_pred | |
873 | (After | |
874 | (make_seq_after (make_match (make_meta_rule_elem aft)) | |
875 | after))) in | |
876 | let or_cases = wrapOr(true_branch,wrapOr(false_branch,after_branch)) in | |
877 | (* the code *) | |
878 | (match (after,aft_needed) with | |
879 | (After _,_) (* pattern doesn't end here *) | |
880 | | (_,true) (* + code added after *) -> | |
881 | quantify bothfvs | |
882 | (wrapAnd | |
883 | (if_header, | |
884 | wrapAnd(wrapAX or_cases, | |
885 | wrapAnd(wrapEX false_pred,wrapEX after_pred)))) | |
886 | | _ -> | |
887 | quantify bothfvs | |
888 | (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX false_pred)))) | |
889 | ||
890 | | Ast.While(header,body,aft) | Ast.For(header,body,aft) -> | |
891 | (* the translation in this case is similar to that of an if with no else *) | |
892 | (* free variables *) | |
893 | let (efvs,bfvs,_) = | |
894 | seq_fvs2 quantified (Ast.get_fvs header) (Ast.get_fvs body) in | |
895 | let new_quantified = Common.union_set bfvs quantified in | |
896 | (* if header *) | |
897 | let header = quantify efvs (make_match header) in | |
898 | let body = | |
899 | make_seq | |
900 | [wrapPred(Lib_engine.TrueBranch,CTL.Control); | |
901 | statement body used_after (a2n after) new_quantified guard] in | |
902 | let after_pred = wrapPred(Lib_engine.FallThrough,CTL.Control) in | |
903 | let (aft_needed,after_branch) = | |
904 | match aft with | |
905 | Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after) | |
906 | | _ -> | |
907 | (true, | |
908 | make_seq_after after_pred | |
909 | (After | |
910 | (make_seq_after (make_match (make_meta_rule_elem aft)) | |
911 | after))) in | |
912 | let or_cases = wrapOr(body,after_branch) in | |
913 | (* the code *) | |
914 | (match (after,aft_needed) with | |
915 | (After _,_) (* pattern doesn't end here *) | |
916 | | (_,true) (* + code added after *) -> | |
917 | quantify bfvs | |
918 | (wrapAnd (header, wrapAnd(wrapAX or_cases, wrapEX after_pred))) | |
919 | | _ -> quantify bfvs (wrapAnd(header, wrapAX or_cases))) | |
920 | ||
921 | | Ast.Disj(stmt_dots_list) -> | |
922 | let processed = | |
923 | List.map | |
924 | (function x -> statement_list x used_after after quantified guard) | |
925 | stmt_dots_list in | |
926 | let rec loop = function | |
927 | [] -> wrap n CTL.True | |
928 | | [x] -> x | |
929 | | x::xs -> wrapSeqOr(x,loop xs) in | |
930 | loop processed | |
931 | (* | |
932 | let do_one e = | |
933 | statement_list e used_after (a2n after) quantified true in | |
934 | let add_nots l e = | |
935 | List.fold_left | |
936 | (function rest -> function cur -> wrapAnd(wrapNot(do_one cur),rest)) | |
937 | e l in | |
938 | let process_one nots cur = | |
939 | match Ast.unwrap cur with | |
940 | Ast.DOTS(x::xs) -> | |
941 | let on = List.map (function x -> Ast.OrOther_dots x) nots in | |
942 | (match Ast.unwrap x with | |
943 | Ast.Dots(d,w,t) -> | |
944 | List.iter | |
945 | (function x -> | |
946 | Printf.printf "a not\n"; | |
947 | Pretty_print_cocci.statement_dots x) | |
948 | nots; | |
949 | let cur = | |
950 | Ast.rewrap cur | |
951 | (Ast.DOTS((Ast.rewrap x (Ast.Dots(d,w,on@t)))::xs)) in | |
952 | statement_list cur used_after after quantified guard | |
953 | | Ast.Nest(sd,w,t) -> | |
954 | let cur = | |
955 | Ast.rewrap cur | |
956 | (Ast.DOTS((Ast.rewrap x (Ast.Nest(sd,w,on@t)))::xs)) in | |
957 | statement_list cur used_after after quantified guard | |
958 | | _ -> | |
959 | add_nots nots | |
960 | (statement_list cur used_after after quantified guard)) | |
961 | | Ast.DOTS([]) -> | |
962 | add_nots nots | |
963 | (statement_list cur used_after after quantified guard) | |
964 | | _ -> failwith "CIRCLES, STARS not supported" in | |
965 | let rec loop after = function | |
966 | [] -> failwith "disj shouldn't be empty" (*wrap n CTL.False*) | |
967 | | [(nots,cur)] -> process_one nots cur | |
968 | | (nots,cur)::rest -> wrapOr(process_one nots cur, loop after rest) in | |
969 | loop after (preprocess_disj stmt_dots_list) | |
970 | *) | |
971 | | Ast.Nest(stmt_dots,whencode,befaft) -> | |
972 | let dots_pattern = | |
973 | statement_list stmt_dots used_after (a2n after) quantified guard in | |
974 | let udots_pattern = | |
975 | let whencodes = | |
976 | List.map | |
977 | (function sl -> | |
978 | statement_list sl used_after (a2n after) quantified true) | |
979 | whencode in | |
980 | List.fold_left (function rest -> function cur -> wrapOr(cur,rest)) | |
981 | (statement_list stmt_dots used_after (a2n after) quantified true) | |
982 | whencodes in | |
983 | (match (after,guard&&(whencode=[])) with | |
984 | (After a,true) -> | |
985 | let nots = | |
986 | List.map (process_bef_aft after quantified used_after n) befaft in | |
987 | (match nots with | |
988 | [] -> wrapAF(wrapOr(a,aftret)) | |
989 | | x::xs -> | |
990 | let left = | |
991 | wrapNot | |
992 | (List.fold_left | |
993 | (function rest -> function cur -> wrapOr(cur,rest)) | |
994 | x xs) in | |
995 | wrapAU(left,wrapOr(a,aftret))) | |
996 | | (After a,false) -> | |
997 | let left = wrapOr(dots_pattern,wrapNot udots_pattern) in | |
998 | let nots = | |
999 | List.map (process_bef_aft after quantified used_after n) befaft in | |
1000 | let left = | |
1001 | match nots with | |
1002 | [] -> left | |
1003 | | x::xs -> | |
1004 | wrapAnd | |
1005 | (wrapNot | |
1006 | (List.fold_left | |
1007 | (function rest -> function cur -> wrapOr(cur,rest)) | |
1008 | x xs), | |
1009 | left) in | |
1010 | wrapAU(left,wrapOr(a,aftret)) | |
1011 | | (_,true) -> wrap n CTL.True | |
1012 | | (_,false) -> wrapAG(wrapOr(dots_pattern,wrapNot udots_pattern))) | |
1013 | | Ast.Dots((_,i,d),whencodes,t) -> | |
1014 | let dot_code = | |
1015 | match d with | |
1016 | Ast.MINUS(_) -> | |
1017 | (* no need for the fresh metavar, but ... is a bit wierd as a | |
1018 | variable name *) | |
1019 | Some(make_match (make_meta_rule_elem d)) | |
1020 | | _ -> None in | |
1021 | let whencodes = | |
1022 | (match whencodes with | |
1023 | Ast.NoWhen -> [] | |
1024 | | Ast.WhenNot whencodes -> | |
1025 | [wrapNot | |
1026 | (statement_list whencodes used_after (a2n after) quantified | |
1027 | true)] | |
1028 | | Ast.WhenAlways s -> | |
1029 | [statement s used_after (a2n after) quantified true]) @ | |
1030 | (List.map wrapNot | |
1031 | (List.map (process_bef_aft after quantified used_after n) t)) in | |
1032 | let phi2 = | |
1033 | match whencodes with | |
1034 | [] -> None | |
1035 | | x::xs -> | |
1036 | Some | |
1037 | (List.fold_left | |
1038 | (function rest -> function cur -> wrapAnd(cur,rest)) | |
1039 | x xs) in | |
1040 | let phi3 = | |
1041 | match (dot_code,phi2) with (* add - on dots, if any *) | |
1042 | (None,None) -> None | |
1043 | | (Some dotcode,None) -> Some dotcode | |
1044 | | (None,Some whencode) -> Some whencode | |
1045 | | (Some dotcode,Some whencode) -> Some(wrapAnd (dotcode,whencode)) in | |
1046 | let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in | |
1047 | (* add in the after code to make the result *) | |
1048 | (match (after,phi3) with | |
1049 | (Tail,Some whencode) -> wrapAU(whencode,wrapOr(exit,aftret)) | |
1050 | | (Tail,None) -> wrapAF(wrapOr(exit,aftret)) | |
1051 | | (After f,Some whencode) | (Guard f,Some whencode) -> | |
1052 | wrapAU(whencode,wrapOr(f,aftret)) | |
1053 | | (After f,None) | (Guard f,None) -> wrapAF(wrapOr(f,aftret))) | |
1054 | | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) -> | |
1055 | let (hfvs,b1fvs,lbfvs,b2fvs,_,b3fvs,_,b4fvs,rbfvs) = | |
1056 | seq_fvs5 quantified (Ast.get_fvs header) (Ast.get_fvs lbrace) | |
1057 | (Ast.get_fvs decls) (Ast.get_fvs body) (Ast.get_fvs rbrace) in | |
1058 | let function_header = quantify hfvs (make_match header) in | |
1059 | let v = count_nested_braces stmt in | |
1060 | let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in | |
1061 | let start_brace = | |
1062 | wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in | |
1063 | let end_brace = | |
1064 | let stripped_rbrace = | |
1065 | match Ast.unwrap rbrace with | |
1066 | Ast.SeqEnd((data,info,_)) -> | |
1067 | Ast.rewrap rbrace | |
1068 | (Ast.SeqEnd ((data,info,Ast.CONTEXT(Ast.NOTHING)))) | |
1069 | | _ -> failwith "unexpected close brace" in | |
1070 | let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in | |
1071 | let errorexit = wrap n (CTL.Pred (Lib_engine.ErrorExit,CTL.Control)) in | |
1072 | wrapAnd(quantify rbfvs (make_match rbrace), | |
1073 | wrapAU(make_match stripped_rbrace, | |
1074 | wrapOr(exit,errorexit))) in | |
1075 | let new_quantified3 = | |
1076 | Common.union_set b1fvs | |
1077 | (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in | |
1078 | let new_quantified4 = Common.union_set b4fvs new_quantified3 in | |
1079 | quantify b1fvs | |
1080 | (make_seq | |
1081 | [function_header; | |
1082 | wrapExists | |
1083 | (v, | |
1084 | (quantify b2fvs | |
1085 | (make_seq | |
1086 | [start_brace; | |
1087 | quantify b3fvs | |
1088 | (statement_list decls used_after | |
1089 | (After | |
1090 | (decl_to_not_decl n dots stmt | |
1091 | make_match | |
1092 | (quantify b4fvs | |
1093 | (statement_list body used_after | |
1094 | (After | |
1095 | (make_seq_after end_brace after)) | |
1096 | new_quantified4 guard)))) | |
1097 | new_quantified3 guard)])))]) | |
1098 | | Ast.OptStm(stm) -> | |
1099 | failwith "OptStm should have been compiled away\n"; | |
1100 | | Ast.UniqueStm(stm) -> | |
1101 | failwith "arities not yet supported" | |
1102 | | Ast.MultiStm(stm) -> | |
1103 | failwith "arities not yet supported" | |
1104 | | _ -> failwith "not supported" | |
1105 | ||
1106 | and process_bef_aft after quantified used_after ln = function | |
1107 | Ast.WParen (re,n) -> | |
1108 | let paren_pred = wrapPred ln (Lib_engine.Paren n,CTL.Control) in | |
1109 | wrapAnd ln (make_raw_match ln re,paren_pred) | |
1110 | | Ast.Other s -> statement s used_after (a2n after) quantified true | |
1111 | | Ast.Other_dots d -> statement_list d used_after (a2n after) quantified true | |
1112 | | Ast.OrOther_dots d -> statement_list d used_after Tail quantified true | |
1113 | ||
1114 | (* Returns a triple for each disj element. The first element of the triple is | |
1115 | Some v if the triple element needs a name, and None otherwise. The second | |
1116 | element is a list of names whose negations should be conjuncted with the | |
1117 | term. The third element is the original term *) | |
1118 | and (preprocess_disj : | |
1119 | Ast.statement Ast.dots list -> | |
1120 | (Ast.statement Ast.dots list * Ast.statement Ast.dots) list) = | |
1121 | function | |
1122 | [] -> [] | |
1123 | | [s] -> [([],s)] | |
1124 | | cur::rest -> | |
1125 | let template = | |
1126 | List.map (function r -> Unify_ast.unify_statement_dots cur r) rest in | |
1127 | let processed = preprocess_disj rest in | |
1128 | if List.exists (function Unify_ast.MAYBE -> true | _ -> false) template | |
1129 | then | |
1130 | ([], cur) :: | |
1131 | (List.map2 | |
1132 | (function ((nots,r) as x) -> | |
1133 | function Unify_ast.MAYBE -> (cur::nots,r) | Unify_ast.NO -> x) | |
1134 | processed template) | |
1135 | else ([], cur) :: processed | |
1136 | ||
1137 | (* --------------------------------------------------------------------- *) | |
1138 | (* Letify: | |
1139 | Phase 1: Use a hash table to identify formulas that appear more than once. | |
1140 | Phase 2: Replace terms by variables. | |
1141 | Phase 3: Drop lets to the point as close as possible to the uses of their | |
1142 | variables *) | |
1143 | ||
1144 | let formula_table = | |
1145 | (Hashtbl.create(50) : | |
1146 | ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl, | |
1147 | int ref (* count *) * string ref (* name *) * bool ref (* processed *)) | |
1148 | Hashtbl.t) | |
1149 | ||
1150 | let add_hash phi = | |
1151 | let (cell,_,_) = | |
1152 | try Hashtbl.find formula_table phi | |
1153 | with Not_found -> | |
1154 | let c = (ref 0,ref "",ref false) in | |
1155 | Hashtbl.add formula_table phi c; | |
1156 | c in | |
1157 | cell := !cell + 1 | |
1158 | ||
1159 | let rec collect_duplicates f = | |
1160 | add_hash f; | |
1161 | match CTL.unwrap f with | |
1162 | CTL.False -> () | |
1163 | | CTL.True -> () | |
1164 | | CTL.Pred(p) -> () | |
1165 | | CTL.Not(phi) -> collect_duplicates phi | |
1166 | | CTL.Exists(v,phi) -> collect_duplicates phi | |
1167 | | CTL.And(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1168 | | CTL.Or(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1169 | | CTL.SeqOr(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1170 | | CTL.Implies(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1171 | | CTL.AF(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1172 | | CTL.AX(_,phi) -> collect_duplicates phi | |
1173 | | CTL.AG(_,phi) -> collect_duplicates phi | |
1174 | | CTL.AU(_,phi1,phi2,phi3,phi4) -> | |
1175 | collect_duplicates phi1; collect_duplicates phi2; | |
1176 | collect_duplicates phi3; collect_duplicates phi4 | |
1177 | | CTL.EF(_,phi) -> collect_duplicates phi | |
1178 | | CTL.EX(_,phi) -> collect_duplicates phi | |
1179 | | CTL.EG(_,phi) -> collect_duplicates phi | |
1180 | | CTL.EU(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2 | |
1181 | | CTL.Uncheck(phi) -> collect_duplicates phi | |
1182 | | _ -> failwith "not possible" | |
1183 | ||
1184 | let assign_variables _ = | |
1185 | Hashtbl.iter | |
1186 | (function formula -> | |
1187 | function (cell,str,_) -> if !cell > 1 then str := fresh_let_var()) | |
1188 | formula_table | |
1189 | ||
1190 | let rec replace_formulas dec f = | |
1191 | let (ct,name,treated) = Hashtbl.find formula_table f in | |
1192 | let real_ct = !ct - dec in | |
1193 | if real_ct > 1 | |
1194 | then | |
1195 | if not !treated | |
1196 | then | |
1197 | begin | |
1198 | treated := true; | |
1199 | let (acc,new_f) = replace_subformulas (dec + (real_ct - 1)) f in | |
1200 | ((!name,new_f) :: acc, CTL.rewrap f (CTL.Ref !name)) | |
1201 | end | |
1202 | else ([],CTL.rewrap f (CTL.Ref !name)) | |
1203 | else replace_subformulas dec f | |
1204 | ||
1205 | and replace_subformulas dec f = | |
1206 | match CTL.unwrap f with | |
1207 | CTL.False -> ([],f) | |
1208 | | CTL.True -> ([],f) | |
1209 | | CTL.Pred(p) -> ([],f) | |
1210 | | CTL.Not(phi) -> | |
1211 | let (acc,new_phi) = replace_formulas dec phi in | |
1212 | (acc,CTL.rewrap f (CTL.Not(new_phi))) | |
1213 | | CTL.Exists(v,phi) -> | |
1214 | let (acc,new_phi) = replace_formulas dec phi in | |
1215 | (acc,CTL.rewrap f (CTL.Exists(v,new_phi))) | |
1216 | | CTL.And(phi1,phi2) -> | |
1217 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1218 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1219 | (acc1@acc2,CTL.rewrap f (CTL.And(new_phi1,new_phi2))) | |
1220 | | CTL.Or(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.Or(new_phi1,new_phi2))) | |
1224 | | CTL.SeqOr(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.SeqOr(new_phi1,new_phi2))) | |
1228 | | CTL.Implies(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.Implies(new_phi1,new_phi2))) | |
1232 | | CTL.AF(dir,phi1,phi2) -> | |
1233 | let (acc,new_phi1) = replace_formulas dec phi1 in | |
1234 | let (acc,new_phi2) = replace_formulas dec phi2 in | |
1235 | (acc,CTL.rewrap f (CTL.AF(dir,new_phi1,new_phi2))) | |
1236 | | CTL.AX(dir,phi) -> | |
1237 | let (acc,new_phi) = replace_formulas dec phi in | |
1238 | (acc,CTL.rewrap f (CTL.AX(dir,new_phi))) | |
1239 | | CTL.AG(dir,phi) -> | |
1240 | let (acc,new_phi) = replace_formulas dec phi in | |
1241 | (acc,CTL.rewrap f (CTL.AG(dir,new_phi))) | |
1242 | | CTL.AU(dir,phi1,phi2,phi3,phi4) -> | |
1243 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1244 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1245 | let (acc3,new_phi3) = replace_formulas dec phi3 in | |
1246 | let (acc4,new_phi4) = replace_formulas dec phi4 in | |
1247 | (acc1@acc2@acc3@acc4, | |
1248 | CTL.rewrap f (CTL.AU(dir,new_phi1,new_phi2,new_phi3,new_phi4))) | |
1249 | | CTL.EF(dir,phi) -> | |
1250 | let (acc,new_phi) = replace_formulas dec phi in | |
1251 | (acc,CTL.rewrap f (CTL.EF(dir,new_phi))) | |
1252 | | CTL.EX(dir,phi) -> | |
1253 | let (acc,new_phi) = replace_formulas dec phi in | |
1254 | (acc,CTL.rewrap f (CTL.EX(dir,new_phi))) | |
1255 | | CTL.EG(dir,phi) -> | |
1256 | let (acc,new_phi) = replace_formulas dec phi in | |
1257 | (acc,CTL.rewrap f (CTL.EG(dir,new_phi))) | |
1258 | | CTL.EU(dir,phi1,phi2) -> | |
1259 | let (acc1,new_phi1) = replace_formulas dec phi1 in | |
1260 | let (acc2,new_phi2) = replace_formulas dec phi2 in | |
1261 | (acc1@acc2,CTL.rewrap f (CTL.EU(dir,new_phi1,new_phi2))) | |
1262 | | _ -> failwith "not possible" | |
1263 | ||
1264 | let ctlfv_table = | |
1265 | (Hashtbl.create(50) : | |
1266 | ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl, | |
1267 | string list (* fvs *) * | |
1268 | string list (* intersection of fvs of subterms *)) | |
1269 | Hashtbl.t) | |
1270 | ||
1271 | let rec ctl_fvs f = | |
1272 | try let (fvs,_) = Hashtbl.find ctlfv_table f in fvs | |
1273 | with Not_found -> | |
1274 | let ((fvs,_) as res) = | |
1275 | match CTL.unwrap f with | |
1276 | CTL.False | CTL.True | CTL.Pred(_) -> ([],[]) | |
1277 | | CTL.Not(phi) | CTL.Exists(_,phi) | |
1278 | | CTL.AX(_,phi) | CTL.AG(_,phi) | |
1279 | | CTL.EF(_,phi) | CTL.EX(_,phi) | CTL.EG(_,phi) -> (ctl_fvs phi,[]) | |
1280 | | CTL.AU(_,phi1,phi2,phi3,phi4) -> | |
1281 | let phi1fvs = ctl_fvs phi1 in | |
1282 | let phi2fvs = ctl_fvs phi2 in | |
1283 | (* phi3 has the same fvs as phi1 and phi4 as phi2 *) | |
1284 | (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) | |
1285 | | CTL.And(phi1,phi2) | CTL.Or(phi1,phi2) | CTL.SeqOr(phi1,phi2) | |
1286 | | CTL.Implies(phi1,phi2) | CTL.AF(_,phi1,phi2) | CTL.EU(_,phi1,phi2) -> | |
1287 | let phi1fvs = ctl_fvs phi1 in | |
1288 | let phi2fvs = ctl_fvs phi2 in | |
1289 | (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) | |
1290 | | CTL.Ref(v) -> ([v],[v]) | |
1291 | | CTL.Let(v,term,body) -> | |
1292 | let phi1fvs = ctl_fvs term in | |
1293 | let phi2fvs = Common.minus_set (ctl_fvs body) [v] in | |
1294 | (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) in | |
1295 | Hashtbl.add ctlfv_table f res; | |
1296 | fvs | |
1297 | ||
1298 | let rev_order_bindings b = | |
1299 | let b = | |
1300 | List.map | |
1301 | (function (nm,term) -> | |
1302 | let (fvs,_) = Hashtbl.find ctlfv_table term in (nm,fvs,term)) | |
1303 | b in | |
1304 | let rec loop bound = function | |
1305 | [] -> [] | |
1306 | | unbound -> | |
1307 | let (now_bound,still_unbound) = | |
1308 | List.partition (function (_,fvs,_) -> subset fvs bound) | |
1309 | unbound in | |
1310 | let get_names = List.map (function (x,_,_) -> x) in | |
1311 | now_bound @ (loop ((get_names now_bound) @ bound) still_unbound) in | |
1312 | List.rev(loop [] b) | |
1313 | ||
1314 | let drop_bindings b f = (* innermost bindings first in b *) | |
1315 | let process_binary f ffvs inter nm term fail = | |
1316 | if List.mem nm inter | |
1317 | then CTL.rewrap f (CTL.Let(nm,term,f)) | |
1318 | else CTL.rewrap f (fail()) in | |
1319 | let find_fvs f = | |
1320 | let _ = ctl_fvs f in Hashtbl.find ctlfv_table f in | |
1321 | let rec drop_one nm term f = | |
1322 | match CTL.unwrap f with | |
1323 | CTL.False -> f | |
1324 | | CTL.True -> f | |
1325 | | CTL.Pred(p) -> f | |
1326 | | CTL.Not(phi) -> CTL.rewrap f (CTL.Not(drop_one nm term phi)) | |
1327 | | CTL.Exists(v,phi) -> CTL.rewrap f (CTL.Exists(v,drop_one nm term phi)) | |
1328 | | CTL.And(phi1,phi2) -> | |
1329 | let (ffvs,inter) = find_fvs f in | |
1330 | process_binary f ffvs inter nm term | |
1331 | (function _ -> CTL.And(drop_one nm term phi1,drop_one nm term phi2)) | |
1332 | | CTL.Or(phi1,phi2) -> | |
1333 | let (ffvs,inter) = find_fvs f in | |
1334 | process_binary f ffvs inter nm term | |
1335 | (function _ -> CTL.Or(drop_one nm term phi1,drop_one nm term phi2)) | |
1336 | | CTL.SeqOr(phi1,phi2) -> | |
1337 | let (ffvs,inter) = find_fvs f in | |
1338 | process_binary f ffvs inter nm term | |
1339 | (function _ -> | |
1340 | CTL.SeqOr(drop_one nm term phi1,drop_one nm term phi2)) | |
1341 | | CTL.Implies(phi1,phi2) -> | |
1342 | let (ffvs,inter) = find_fvs f in | |
1343 | process_binary f ffvs inter nm term | |
1344 | (function _ -> | |
1345 | CTL.Implies(drop_one nm term phi1,drop_one nm term phi2)) | |
1346 | | CTL.AF(dir,phi1,phi2) -> | |
1347 | let (ffvs,inter) = find_fvs f in | |
1348 | process_binary f ffvs inter nm term | |
1349 | (function _ -> | |
1350 | CTL.AF(dir,drop_one nm term phi1,drop_one nm term phi2)) | |
1351 | | CTL.AX(dir,phi) -> | |
1352 | CTL.rewrap f (CTL.AX(dir,drop_one nm term phi)) | |
1353 | | CTL.AG(dir,phi) -> CTL.rewrap f (CTL.AG(dir,drop_one nm term phi)) | |
1354 | | CTL.AU(dir,phi1,phi2,phi3,phi4) -> | |
1355 | let (ffvs,inter) = find_fvs f in | |
1356 | process_binary f ffvs inter nm term | |
1357 | (function _ -> | |
1358 | CTL.AU(dir,drop_one nm term phi1,drop_one nm term phi2, | |
1359 | drop_one nm term phi3,drop_one nm term phi4)) | |
1360 | | CTL.EF(dir,phi) -> CTL.rewrap f (CTL.EF(dir,drop_one nm term phi)) | |
1361 | | CTL.EX(dir,phi) -> | |
1362 | CTL.rewrap f (CTL.EX(dir,drop_one nm term phi)) | |
1363 | | CTL.EG(dir,phi) -> CTL.rewrap f (CTL.EG(dir,drop_one nm term phi)) | |
1364 | | CTL.EU(dir,phi1,phi2) -> | |
1365 | let (ffvs,inter) = find_fvs f in | |
1366 | process_binary f ffvs inter nm term | |
1367 | (function _ -> | |
1368 | CTL.EU(dir,drop_one nm term phi1,drop_one nm term phi2)) | |
1369 | | (CTL.Ref(v) as x) -> process_binary f [v] [v] nm term (function _ -> x) | |
1370 | | CTL.Let(v,term1,body) -> | |
1371 | let (ffvs,inter) = find_fvs f in | |
1372 | process_binary f ffvs inter nm term | |
1373 | (function _ -> | |
1374 | CTL.Let(v,drop_one nm term term1,drop_one nm term body)) in | |
1375 | List.fold_left | |
1376 | (function processed -> function (nm,_,term) -> drop_one nm term processed) | |
1377 | f b | |
1378 | ||
1379 | let letify f = | |
1380 | failwith "this code should not be used!!!"(*; | |
1381 | Hashtbl.clear formula_table; | |
1382 | Hashtbl.clear ctlfv_table; | |
1383 | (* create a count of the number of occurrences of each subformula *) | |
1384 | collect_duplicates f; | |
1385 | (* give names to things that appear more than once *) | |
1386 | assign_variables(); | |
1387 | (* replace duplicated formulas by their variables *) | |
1388 | let (bindings,new_f) = replace_formulas 0 f in | |
1389 | (* collect fvs of terms in bindings and new_f *) | |
1390 | List.iter (function f -> let _ = ctl_fvs f in ()) | |
1391 | (new_f::(List.map (function (_,term) -> term) bindings)); | |
1392 | (* sort bindings with uses before defs *) | |
1393 | let bindings = rev_order_bindings bindings in | |
1394 | (* insert bindings as lets into the formula *) | |
1395 | let res = drop_bindings bindings new_f in | |
1396 | res*) | |
1397 | ||
1398 | (* --------------------------------------------------------------------- *) | |
1399 | (* Function declaration *) | |
1400 | ||
1401 | let top_level used_after t = | |
1402 | match Ast.unwrap t with | |
1403 | Ast.DECL(decl) -> failwith "not supported decl" | |
1404 | | Ast.INCLUDE(inc,s) -> | |
1405 | (* no indication of whether inc or s is modified *) | |
1406 | wrap 0 (CTL.Pred((Lib_engine.Include(inc,s),CTL.Control))) | |
1407 | | Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo" | |
1408 | | Ast.FUNCTION(stmt) -> | |
1409 | (*Printf.printf "orig\n"; | |
1410 | Pretty_print_cocci.statement "" stmt; | |
1411 | Format.print_newline();*) | |
1412 | let unopt = elim_opt.V.rebuilder_statement stmt in | |
1413 | (*Printf.printf "unopt\n"; | |
1414 | Pretty_print_cocci.statement "" unopt; | |
1415 | Format.print_newline();*) | |
1416 | let unopt = preprocess_dots_e unopt in | |
1417 | (*letify*) | |
1418 | (statement unopt used_after Tail [] false) | |
1419 | | Ast.CODE(stmt_dots) -> | |
1420 | let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in | |
1421 | let unopt = preprocess_dots unopt in | |
1422 | (*letify*) | |
1423 | (statement_list unopt used_after Tail [] false) | |
1424 | | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" | |
1425 | ||
1426 | (* --------------------------------------------------------------------- *) | |
1427 | (* Contains dots *) | |
1428 | ||
1429 | let contains_dots = | |
1430 | let bind x y = x or y in | |
1431 | let option_default = false in | |
1432 | let mcode r x = false in | |
1433 | let statement r k s = | |
1434 | match Ast.unwrap s with Ast.Dots(_,_,_) -> true | _ -> k s in | |
1435 | let continue r k e = k e in | |
1436 | let stop r k e = false in | |
1437 | let res = | |
1438 | V.combiner bind option_default | |
1439 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode | |
1440 | continue continue continue | |
1441 | stop stop stop stop stop stop stop statement continue continue in | |
1442 | res.V.combiner_top_level | |
1443 | ||
1444 | (* --------------------------------------------------------------------- *) | |
1445 | (* Entry points *) | |
1446 | ||
1447 | let asttoctl l used_after = | |
1448 | ctr := 0; | |
1449 | lctr := 0; | |
1450 | sctr := 0; | |
1451 | let l = | |
1452 | List.filter | |
1453 | (function t -> | |
1454 | match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true) | |
1455 | l in | |
1456 | List.map2 top_level used_after l | |
1457 | ||
1458 | let pp_cocci_predicate (pred,modif) = | |
1459 | Pretty_print_engine.pp_predicate pred | |
1460 | ||
1461 | let cocci_predicate_to_string (pred,modif) = | |
1462 | Pretty_print_engine.predicate_to_string pred |