engine/ctlcocci_integration.ml

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