HCoop / bpt / coccinelle.git / blob
? search:


b603e4c420ad0389cd2d5b195c3d86b16f6ae24e
[bpt/coccinelle.git] / engine / ctlcocci_integration.ml
1 (*
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.
7 *
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.
11 *
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.
16 *
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/>.
19 *
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
22 *)
23
24
25 open Common
26
27 open Ograph_extended
28
29 module F = Control_flow_c
30
31 (*****************************************************************************)
32 (* Debugging functions *)
33 (*****************************************************************************)
34 let show_or_not_predicate pred =
35 if !Flag_matcher.debug_engine then begin
36 indent_do (fun () ->
37 adjust_pp_with_indent_and_header "labeling: pred = " (fun () ->
38 Pretty_print_engine.pp_predicate pred;
39 );
40 )
41 end
42
43 let show_or_not_nodes nodes =
44 if !Flag_matcher.debug_engine then begin
45 indent_do (fun () ->
46 adjust_pp_with_indent_and_header "labeling: result = " (fun () ->
47 Common.pp_do_in_box (fun () ->
48 pp "{";
49 Common.print_between
50 (fun () -> pp ";"; Format.print_cut())
51 (fun (nodei, (_predTODO, subst)) ->
52 Format.print_int nodei;
53 Common.pp_do_in_box (fun () ->
54 Pretty_print_engine.pp_binding2_ctlsubst subst
55 )
56 ) nodes;
57 pp "}";
58 );
59 )
60 )
61 end
62
63 let show_isos rule_elem =
64 match Ast_cocci.get_isos rule_elem with
65 [] -> ()
66 | isos ->
67 let line = Ast_cocci.get_line rule_elem in
68 Printf.printf "rule elem: ";
69 Pretty_print_cocci.rule_elem "" rule_elem;
70 Format.print_newline();
71 List.iter
72 (function (nm,x) ->
73 Printf.printf " iso: %s(%d): " nm line;
74 Pretty_print_cocci.pp_print_anything x;
75 Format.print_newline())
76 isos
77
78 (*****************************************************************************)
79 (* Labeling function *)
80 (*****************************************************************************)
81 let (-->) x v = Ast_ctl.Subst (x,v);;
82
83 (* Take list of predicate and for each predicate returns where in the
84 * control flow it matches, and the set of subsitutions for this match.
85 *)
86 let (labels_for_ctl: string list (* dropped isos *) ->
87 (nodei * F.node) list -> Lib_engine.metavars_binding ->
88 Lib_engine.label_ctlcocci) =
89 fun dropped_isos nodes binding ->
90
91 (fun p ->
92 show_or_not_predicate p;
93
94 let nodes' = nodes +> List.map (fun (nodei, node) ->
95 (* todo? put part of this code in pattern ? *)
96 (match p, F.unwrap node with
97 | Lib_engine.Paren s, (F.SeqStart (_, bracelevel, _)) ->
98 let make_var x = ("",i_to_s x) in
99 [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))]
100 | Lib_engine.Paren s, (F.SeqEnd (bracelevel, _)) ->
101 let make_var x = ("",i_to_s x) in
102 [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))]
103 | Lib_engine.Paren _, _ -> []
104 | Lib_engine.Label s, _ ->
105 let labels = F.extract_labels node in
106 [(nodei,
107 (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))]
108 | Lib_engine.BCLabel s, _ ->
109 (match F.extract_bclabels node with
110 [] -> [] (* null for all nodes that are not break or continue *)
111 | labels ->
112 [(nodei,
113 (p,[(s -->
114 (Lib_engine.LabelVal (Lib_engine.Absolute labels)))]))])
115 | Lib_engine.PrefixLabel s, _ ->
116 let labels = F.extract_labels node in
117 [(nodei,
118 (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Prefix labels)))]))]
119
120 | Lib_engine.Match (re), _unwrapnode ->
121 let substs =
122 Pattern_c.match_re_node dropped_isos re node binding
123 +> List.map (fun (re', subst) ->
124 Lib_engine.Match (re'), subst
125 )
126 in
127 substs +> List.map (fun (p', subst) ->
128 (nodei,
129 (p',
130 subst +> List.map (fun (s, meta) ->
131 s --> Lib_engine.NormalMetaVal meta
132 ))))
133
134 | Lib_engine.InLoop, F.InLoopNode -> [nodei, (p,[])]
135 | Lib_engine.TrueBranch , F.TrueNode -> [nodei, (p,[])]
136 | Lib_engine.FalseBranch, F.FalseNode -> [nodei, (p,[])]
137 | Lib_engine.After, F.AfterNode -> [nodei, (p,[])]
138 | Lib_engine.FallThrough, F.FallThroughNode -> [nodei,(p,[])]
139 | Lib_engine.LoopFallThrough, F.LoopFallThroughNode -> [nodei,(p,[])]
140 | Lib_engine.FunHeader, F.FunHeader _ -> [nodei, (p,[])]
141 | Lib_engine.Top, F.TopNode -> [nodei, (p,[])]
142 | Lib_engine.Exit, F.Exit -> [nodei, (p,[])]
143 | Lib_engine.ErrorExit, F.ErrorExit -> [nodei, (p,[])]
144 | Lib_engine.Goto, F.Goto(_,_,_) -> [nodei, (p,[])]
145
146 | Lib_engine.InLoop , _ -> []
147 | Lib_engine.TrueBranch , _ -> []
148 | Lib_engine.FalseBranch, _ -> []
149 | Lib_engine.After, _ -> []
150 | Lib_engine.FallThrough, _ -> []
151 | Lib_engine.LoopFallThrough, _ -> []
152 | Lib_engine.FunHeader, _ -> []
153 | Lib_engine.Top, _ -> []
154 | Lib_engine.Exit, _ -> []
155 | Lib_engine.ErrorExit, _ -> []
156 | Lib_engine.Goto, _ -> []
157
158 | Lib_engine.BindGood s, _ -> [(nodei, (p,[(s --> Lib_engine.GoodVal)]))]
159 | Lib_engine.BindBad s, _ -> [(nodei, (p,[(s --> Lib_engine.BadVal)]))]
160 | Lib_engine.FakeBrace, _ ->
161 if F.extract_is_fake node then [nodei, (p,[])] else []
162
163 | Lib_engine.Return, node ->
164 (match node with
165 (* todo? should match the Exit code ?
166 * todo: one day try also to match the special function
167 * such as panic();
168 *)
169 | F.Return _ -> [nodei, (p,[])]
170 | F.ReturnExpr _ -> [nodei, (p,[])]
171 | _ -> []
172 )
173 )
174 ) +> List.concat
175 in
176
177 show_or_not_nodes nodes';
178 nodes'
179 )
180
181 (*****************************************************************************)
182 (* Some fix flow, for CTL, for unparse *)
183 (*****************************************************************************)
184 (* could erase info on nodes, and edge, because they are not used by rene *)
185 let (control_flow_for_ctl: F.cflow -> ('a, 'b) ograph_mutable) =
186 fun cflow -> cflow
187
188
189
190 (* Just make the final node of the control flow loop over itself.
191 * It seems that one hypothesis of the SAT algorithm is that each node as at
192 * least a successor.
193 *
194 * update: do same for errorexit node.
195 *
196 * update: also erase the fake nodes (and adjust the edges accordingly),
197 * so that AX in CTL can now work.
198 * Indeed, à la fin de la branche then (et else), on devrait aller directement
199 * au suivant du endif, sinon si ecrit if(1) { foo(); }; bar();
200 * sans '...' entre le if et bar(), alors ca matchera pas car le CTL
201 * generera un AX bar() qui il tombera d'abord sur le [endif] :(
202 * Mais chiant de changer l'algo de generation, marche pas tres bien avec
203 * ma facon de faire recursive et compositionnel.
204 * => faire une fonction qui applique des fixes autour de ce control flow,
205 * comme ca passe un bon flow a rene, mais garde un flow a moi pour pouvoir
206 * facilement generate back the ast.
207 * alt: faire un wrapper autourde mon graphe pour lui passer dans le module CFG
208 * une fonction qui passe a travers les Fake, mais bof.
209 *
210 * update: also make loop the deadcode nodes, the one that have
211 * no predecessor.
212 *)
213 let (fix_flow_ctl2: F.cflow -> F.cflow) = fun flow ->
214 let g = ref flow in
215
216 let topi = F.first_node !g in
217 !g#add_arc ((topi, topi), F.Direct);
218
219 (* for the #define CFG who have no Exit but have at least a EndNode *)
220 (try
221 let endi = F.find_node (fun x -> x =*= F.EndNode) !g in
222 !g#add_arc ((endi, endi), F.Direct);
223 with Not_found -> ()
224 );
225
226 (* for the regular functions *)
227 (try
228 let exitnodei = F.find_node (fun x -> x =*= F.Exit) !g in
229 let errornodei = F.find_node (fun x -> x =*= F.ErrorExit) !g in
230
231 !g#add_arc ((exitnodei, exitnodei), F.Direct);
232
233 if null ((!g#successors errornodei)#tolist) &&
234 null ((!g#predecessors errornodei)#tolist)
235 then !g#del_node errornodei
236 else !g#add_arc ((errornodei, errornodei), F.Direct);
237 with Not_found -> ()
238 );
239
240 let fake_nodes = !g#nodes#tolist +> List.filter (fun (nodei, node) ->
241 match F.unwrap node with
242 | F.CaseNode _
243 | F.Enter
244 (*| F.Fake*) (* [endif], [endswitch], ... *)
245 -> true
246 | _ -> false
247 ) in
248
249 fake_nodes +> List.iter (fun (nodei, node) -> F.remove_one_node nodei !g);
250
251 (* even when have deadcode, julia want loop over those nodes *)
252 !g#nodes#tolist +> List.iter (fun (nodei, node) ->
253 if (!g#predecessors nodei)#null
254 then begin
255 let fakei = !g#add_node (F.mk_node F.Fake [] [] "DEADCODELOOP") in
256 !g#add_arc ((fakei, nodei), F.Direct);
257 !g#add_arc ((fakei, fakei), F.Direct);
258 end
259 );
260
261 !g#nodes#tolist +> List.iter (fun (nodei, node) ->
262 assert (List.length ((!g#successors nodei)#tolist) >= 1);
263 (* no: && List.length ((!g#predecessors nodei)#tolist) >= 1
264 because the enter node at least have no predecessors *)
265 );
266
267 !g
268 let fix_flow_ctl a =
269 Common.profile_code "fix_flow" (fun () -> fix_flow_ctl2 a)
270
271
272
273
274
275 (*****************************************************************************)
276 (* subtil: the label must operate on newflow, not (old) cflow
277 * update: now I supposed that we give me a fixed_flow
278 *)
279 let model_for_ctl dropped_isos cflow binding =
280 let newflow = cflow (* old: fix_flow_ctl (control_flow_for_ctl cflow) *) in
281 let labels = labels_for_ctl dropped_isos (newflow#nodes#tolist) binding in
282 let states = List.map fst newflow#nodes#tolist in
283 newflow, labels, states
284
285
286 (*****************************************************************************)
287
288 module PRED =
289 struct
290 type t = Lib_engine.predicate
291 let print_predicate x =
292 Pretty_print_cocci.print_plus_flag := false;
293 Pretty_print_cocci.print_minus_flag := false;
294 Pretty_print_engine.pp_predicate x
295 end
296
297 (* prefix has to be nonempty *)
298 let prefix l1 l2 =
299 let rec loop = function
300 ([],_) -> true
301 | (_,[]) -> false
302 | (x::xs,y::ys) when x = y -> loop (xs,ys)
303 | _ -> false in
304 loop(l1,l2)
305
306 let compatible_labels l1 l2 =
307 match (l1,l2) with
308 (Lib_engine.Absolute(l1),Lib_engine.Absolute(l2)) -> l1 =*= l2
309 | (Lib_engine.Absolute(l1),Lib_engine.Prefix(l2)) -> prefix l1 l2
310 | (Lib_engine.Prefix(l1),Lib_engine.Absolute(l2)) -> prefix l2 l1
311 | (Lib_engine.Prefix(l1),Lib_engine.Prefix(l2)) ->
312 not (l1 = []) && not (l2 = []) &&
313 List.hd l1 =*= List.hd l2 (* labels are never empty *)
314
315 let merge_labels l1 l2 =
316 match (l1,l2) with
317 (* known to be compatible *)
318 (Lib_engine.Absolute(_),Lib_engine.Absolute(_)) -> l1
319 | (Lib_engine.Absolute(_),Lib_engine.Prefix(_)) -> l1
320 | (Lib_engine.Prefix(_),Lib_engine.Absolute(_)) -> l2
321 | (Lib_engine.Prefix(l1),Lib_engine.Prefix(l2)) ->
322 let rec max_prefix = function
323 (x::xs,y::ys) when x = y -> x::(max_prefix(xs,ys))
324 | (l1,l2) -> [] in
325 Lib_engine.Prefix(max_prefix(l1,l2))
326
327 module ENV =
328 struct
329 type value = Lib_engine.metavar_binding_kind2
330 type mvar = Ast_cocci.meta_name
331 let eq_mvar x x' = x =*= x'
332 let eq_val v v' =
333 (* v = v' *)
334 match (v,v') with
335 (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)),
336 Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) ->
337 ((min1 <= min2) && (max1 >= max2)) or
338 ((min2 <= min1) && (max2 >= max1))
339 | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
340 Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
341 C_vs_c.eq_type a b
342 | (Lib_engine.LabelVal(l1),Lib_engine.LabelVal(l2)) ->
343 compatible_labels l1 l2
344 | _ -> v =*= v'
345 let merge_val v v' = (* values guaranteed to be compatible *)
346 (* v *)
347 match (v,v') with
348 (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)),
349 Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) ->
350 if (min1 <= min2) && (max1 >= max2)
351 then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1))
352 else
353 if (min2 <= min1) && (max2 >= max1)
354 then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))
355 else failwith "incompatible positions give to merge"
356 | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
357 Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
358 Lib_engine.NormalMetaVal (Ast_c.MetaTypeVal (C_vs_c.merge_type a b))
359 | (Lib_engine.LabelVal(l1),Lib_engine.LabelVal(l2)) ->
360 Lib_engine.LabelVal(merge_labels l1 l2)
361
362 | _ -> v
363 let print_mvar (_,s) = Format.print_string s
364 let print_value x = Pretty_print_engine.pp_binding_kind2 x
365 end
366
367 module CFG =
368 struct
369 type node = Ograph_extended.nodei
370 type cfg = (F.node, F.edge) Ograph_extended.ograph_mutable
371 let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist)
372 let successors cfg n = List.map fst ((cfg#successors n)#tolist)
373 let extract_is_loop cfg n =
374 Control_flow_c.extract_is_loop (cfg#nodes#find n)
375 let print_node i = Format.print_string (i_to_s i)
376 let size cfg = cfg#nodes#length
377
378 (* In ctl_engine, we use 'node' for the node but in the Ograph_extended
379 * terminology, this 'node' is in fact an index to access the real
380 * node information (that ctl/ wants to abstract away to be more generic),
381 * the 'Ograph_extended.nodei'.
382 *)
383 let print_graph cfg label border_colors fill_colors filename =
384 Ograph_extended.print_ograph_mutable_generic cfg label
385 (fun (nodei, (node: F.node)) ->
386 (* the string julia wants to put ? *)
387 let bc = try Some(List.assoc nodei border_colors) with _ -> None in
388 let fc = try Some(List.assoc nodei fill_colors) with _ -> None in
389 (* the string yoann put as debug information in the cfg *)
390 let str = snd node in
391 (str,bc,fc)
392 )
393 ~output_file:filename
394 ~launch_gv:false
395 end
396
397
398 module WRAPPED_ENGINE = Wrapper_ctl.CTL_ENGINE_BIS (ENV) (CFG) (PRED)
399
400 let print_bench _ = WRAPPED_ENGINE.print_bench()
401
402 type pred = Lib_engine.predicate * Ast_cocci.meta_name Ast_ctl.modif
403
404 (*****************************************************************************)
405 let metavars_binding2_to_binding binding2 =
406 binding2 +> Common.map_filter (fun (s, kind2) ->
407 match kind2 with
408 | Lib_engine.NormalMetaVal kind -> Some (s, kind)
409 (* I thought it was Impossible to have this when called from
410 satbis_to_trans_info but it does not seems so *)
411 | Lib_engine.ParenVal _ -> None
412 | Lib_engine.LabelVal _ -> None
413 | Lib_engine.BadVal -> None (* should not occur *)
414 | Lib_engine.GoodVal -> None (* should not occur *)
415 )
416
417 let metavars_binding_to_binding2 binding =
418 binding +> List.map (fun (s, kind) -> s, Lib_engine.NormalMetaVal kind)
419
420
421 let (satbis_to_trans_info:
422 (int list *
423 (nodei * Lib_engine.metavars_binding2 * Lib_engine.predicate)) list ->
424 (int list *
425 (nodei * Lib_engine.metavars_binding * Ast_cocci.rule_elem)) list) =
426 fun xs ->
427 xs +> List.fold_left (fun prev (index,(nodei, binding2, pred)) ->
428 match pred with
429 | Lib_engine.Match (rule_elem) ->
430 if !Flag.track_iso_usage then show_isos rule_elem;
431 (index,
432 (nodei, metavars_binding2_to_binding binding2, rule_elem))
433 ::prev
434 (* see BindGood in asttotctl2 *)
435 | Lib_engine.BindGood (_) -> prev
436 | _ -> raise Impossible
437 ) []
438
439 (*****************************************************************************)
440
441 let rec coalesce_positions = function
442 [] -> []
443 | (x,Ast_c.MetaPosValList l)::rest ->
444 let (same,others) = List.partition (function (x1,_) -> x =*= x1) rest in
445 let ls =
446 List.concat
447 (List.map
448 (function
449 (_,Ast_c.MetaPosValList l) -> l
450 | _ -> failwith "unexpected non-position")
451 same) in
452 let new_ls = List.sort compare (l@ls) in
453 (x,Ast_c.MetaPosValList new_ls) :: coalesce_positions others
454 | x::rest -> x :: coalesce_positions rest
455
456 let strip env =
457 List.map
458 (function (v,vl) ->
459 let vl =
460 match vl with
461 Ast_c.MetaExprVal (a,c) ->
462 Ast_c.MetaExprVal(Lib_parsing_c.al_inh_expr a,c)
463 | Ast_c.MetaExprListVal a ->
464 Ast_c.MetaExprListVal(Lib_parsing_c.al_inh_arguments a)
465 | Ast_c.MetaStmtVal a ->
466 Ast_c.MetaStmtVal(Lib_parsing_c.al_inh_statement a)
467 | Ast_c.MetaInitVal a ->
468 Ast_c.MetaInitVal(Lib_parsing_c.al_inh_init a)
469 | x -> (*don't contain binding info*) x in
470 (v,vl))
471 env
472
473 let rec nub ls =
474 match ls with
475 [] -> []
476 | (x::xs) when (List.mem x xs) -> nub xs
477 | (x::xs) -> x::(nub xs)
478
479 (*****************************************************************************)
480 (* Call ctl engine *)
481 (*****************************************************************************)
482 let (mysat2:
483 Lib_engine.model ->
484 (Lib_engine.ctlcocci * (pred list list)) ->
485 (Lib_engine.mvar list*Lib_engine.metavars_binding) ->
486 (Lib_engine.numbered_transformation_info * bool *
487 Lib_engine.metavars_binding * Lib_engine.metavars_binding list)) =
488 fun (flow, label, states) ctl (used_after, binding) ->
489 let binding2 = metavars_binding_to_binding2 binding in
490 let (triples,(trans_info2, returned_any_states, used_after_envs)) =
491 WRAPPED_ENGINE.satbis (flow, label, states) ctl
492 (used_after, binding2)
493 in
494 if not (!Flag_parsing_cocci.sgrep_mode || !Flag.sgrep_mode2 ||
495 !Flag_matcher.allow_inconsistent_paths)
496 then Check_reachability.check_reachability triples flow;
497 let (trans_info2,used_after_fresh_envs) =
498 Postprocess_transinfo.process used_after binding2 trans_info2 in
499 let used_after_envs =
500 Common.uniq(List.map2 (@) used_after_fresh_envs used_after_envs) in
501 let trans_info = satbis_to_trans_info trans_info2 in
502 let newbindings = List.map metavars_binding2_to_binding used_after_envs in
503 let newbindings = List.map coalesce_positions newbindings in
504 let newbindings = List.map strip newbindings in
505 let newbindings = nub newbindings in
506 (trans_info, returned_any_states, binding, newbindings)
507
508 let mysat a b c =
509 Common.profile_code "mysat" (fun () -> mysat2 a b c)
Unnamed repository; edit this file 'description' to name the repository.