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
   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, (p,[(s --> (Lib_engine.LabelVal labels))]))]
 105       | Lib_engine.BCLabel s, _ ->
 106           (match F.extract_bclabels node with
 107             [] -> [] (* null for all nodes that are not break or continue *)
 108           | labels ->
 109               [(nodei, (p,[(s --> (Lib_engine.LabelVal labels))]))])
 110       | Lib_engine.PrefixLabel s, _ ->
 111           let labels = F.extract_labels node in
 112           let prefixes = Common.inits labels +> Common.tail in
 113           prefixes +> List.map (fun prefixlabels ->
 114             (nodei, (p,[(s --> (Lib_engine.LabelVal prefixlabels))]))
 115           )
 116
 117       | Lib_engine.Match (re), _unwrapnode ->
 118           let substs =
 119             Pattern_c.match_re_node dropped_isos re node binding
 120             +> List.map (fun (re', subst) ->
 121               Lib_engine.Match (re'), subst
 122             )
 123           in
 124           substs +> List.map (fun (p', subst) ->
 125             (nodei,
 126               (p',
 127                 subst +> List.map (fun (s, meta) ->
 128                   s --> Lib_engine.NormalMetaVal meta
 129                 ))))
 130
 131       | Lib_engine.InLoop,      F.InLoopNode ->  [nodei, (p,[])]
 132       | Lib_engine.TrueBranch , F.TrueNode ->  [nodei, (p,[])]
 133       | Lib_engine.FalseBranch, F.FalseNode -> [nodei, (p,[])]
 134       | Lib_engine.After,       F.AfterNode -> [nodei, (p,[])]
 135       | Lib_engine.FallThrough, F.FallThroughNode -> [nodei,(p,[])]
 136       | Lib_engine.FunHeader,   F.FunHeader _ -> [nodei, (p,[])]
 137       | Lib_engine.Top,         F.TopNode ->   [nodei, (p,[])]
 138       | Lib_engine.Exit,        F.Exit ->      [nodei, (p,[])]
 139       | Lib_engine.ErrorExit,   F.ErrorExit -> [nodei, (p,[])]
 140       | Lib_engine.Goto,        F.Goto(_,_,_) -> [nodei, (p,[])]
 141
 142       | Lib_engine.InLoop , _ -> []
 143       | Lib_engine.TrueBranch , _ -> []
 144       | Lib_engine.FalseBranch, _ -> []
 145       | Lib_engine.After, _ -> []
 146       | Lib_engine.FallThrough, _ -> []
 147       | Lib_engine.FunHeader, _  -> []
 148       | Lib_engine.Top, _  -> []
 149       | Lib_engine.Exit, _  -> []
 150       | Lib_engine.ErrorExit, _  -> []
 151       | Lib_engine.Goto, _  -> []
 152
 153       | Lib_engine.BindGood s, _ -> [(nodei, (p,[(s --> Lib_engine.GoodVal)]))]
 154       | Lib_engine.BindBad s, _ ->  [(nodei, (p,[(s --> Lib_engine.BadVal)]))]
 155       | Lib_engine.FakeBrace, _ ->
 156           if F.extract_is_fake node then [nodei, (p,[])] else []
 157
 158       | Lib_engine.Return, node ->
 159           (match node with
 160             (* todo? should match the Exit code ?
 161              * todo: one day try also to match the special function
 162              * such as panic();
 163              *)
 164           | F.Return _ ->  [nodei, (p,[])]
 165           | F.ReturnExpr _ -> [nodei, (p,[])]
 166           | _ -> []
 167           )
 168       )
 169      ) +> List.concat
 170      in
 171
 172      show_or_not_nodes nodes';
 173      nodes'
 174    )
 175
 176 (*****************************************************************************)
 177 (* Some fix flow, for CTL, for unparse *)
 178 (*****************************************************************************)
 179 (* could erase info on nodes, and edge, because they are not used by rene *)
 180 let (control_flow_for_ctl: F.cflow -> ('a, 'b) ograph_mutable) =
 181  fun cflow -> cflow
 182
 183
 184
 185 (* Just make the final node of the control flow loop over itself.
 186  * It seems that one hypothesis of the SAT algorithm is that each node as at
 187  * least a successor.
 188  *
 189  * update: do same for errorexit node.
 190  *
 191  * update: also erase the fake nodes (and adjust the edges accordingly),
 192  * so that AX in CTL can now work.
 193  * Indeed, à la fin de la branche then (et else), on devrait aller directement
 194  * au suivant du endif, sinon si ecrit if(1) { foo(); }; bar();
 195  * sans '...' entre le if et bar(), alors ca matchera pas car le CTL
 196  * generera un AX bar()  qui il tombera d'abord sur le [endif] :(
 197  * Mais chiant de changer l'algo de generation, marche pas tres bien avec
 198  * ma facon de faire recursive et compositionnel.
 199  * => faire une fonction qui applique des fixes autour de ce control flow,
 200  * comme ca passe un bon flow a rene, mais garde un flow a moi pour pouvoir
 201  * facilement generate back the ast.
 202  * alt: faire un wrapper autourde mon graphe pour lui passer dans le module CFG
 203  * une fonction qui passe a travers les Fake, mais bof.
 204  *
 205  * update: also make loop the deadcode nodes, the one that have
 206  * no predecessor.
 207  *)
 208 let (fix_flow_ctl2: F.cflow -> F.cflow) = fun flow ->
 209   let g = ref flow in
 210
 211   let topi = F.first_node !g in
 212   !g#add_arc ((topi, topi), F.Direct);
 213
 214   (* for the #define CFG who have no Exit but have at least a EndNode *)
 215   (try
 216       let endi  = F.find_node (fun x -> x =*= F.EndNode) !g in
 217       !g#add_arc ((endi, endi), F.Direct);
 218     with Not_found -> ()
 219   );
 220
 221   (* for the regular functions *)
 222   (try
 223     let exitnodei  = F.find_node (fun x -> x =*= F.Exit) !g in
 224     let errornodei = F.find_node (fun x -> x =*= F.ErrorExit) !g in
 225
 226     !g#add_arc ((exitnodei, exitnodei), F.Direct);
 227
 228     if null ((!g#successors   errornodei)#tolist) &&
 229        null ((!g#predecessors errornodei)#tolist)
 230     then !g#del_node errornodei
 231     else !g#add_arc ((errornodei, errornodei), F.Direct);
 232    with Not_found -> ()
 233   );
 234
 235   let fake_nodes = !g#nodes#tolist +> List.filter (fun (nodei, node) ->
 236     match F.unwrap node with
 237     | F.CaseNode _
 238     | F.Enter
 239     (*| F.Fake*) (* [endif], [endswitch], ... *)
 240       -> true
 241     | _ -> false
 242     ) in
 243
 244   fake_nodes +> List.iter (fun (nodei, node) -> F.remove_one_node nodei !g);
 245
 246   (* even when have deadcode, julia want loop over those nodes *)
 247   !g#nodes#tolist +> List.iter (fun (nodei, node) ->
 248     if (!g#predecessors nodei)#null
 249     then begin
 250       let fakei = !g#add_node (F.mk_node F.Fake [] [] "DEADCODELOOP") in
 251       !g#add_arc ((fakei, nodei), F.Direct);
 252       !g#add_arc ((fakei, fakei), F.Direct);
 253     end
 254   );
 255
 256   !g#nodes#tolist +> List.iter (fun (nodei, node) ->
 257     assert (List.length ((!g#successors nodei)#tolist) >= 1);
 258     (* no:  && List.length ((!g#predecessors nodei)#tolist) >= 1
 259        because    the enter node at least have no predecessors *)
 260     );
 261
 262   !g
 263 let fix_flow_ctl a =
 264   Common.profile_code "fix_flow" (fun () -> fix_flow_ctl2 a)
 265
 266
 267
 268
 269
 270 (*****************************************************************************)
 271 (* subtil: the label must operate on newflow, not (old) cflow
 272  * update: now I supposed that we give me a fixed_flow
 273  *)
 274 let model_for_ctl dropped_isos cflow binding =
 275  let newflow = cflow (* old: fix_flow_ctl (control_flow_for_ctl cflow) *) in
 276  let labels = labels_for_ctl dropped_isos (newflow#nodes#tolist) binding  in
 277  let states = List.map fst  newflow#nodes#tolist  in
 278  newflow, labels, states
 279
 280
 281 (*****************************************************************************)
 282
 283 module PRED =
 284   struct
 285     type t = Lib_engine.predicate
 286     let print_predicate x =
 287       Pretty_print_cocci.print_plus_flag := false;
 288       Pretty_print_cocci.print_minus_flag := false;
 289       Pretty_print_engine.pp_predicate x
 290   end
 291
 292 module ENV =
 293   struct
 294     type value = Lib_engine.metavar_binding_kind2
 295     type mvar = Ast_cocci.meta_name
 296     let eq_mvar x x' = x =*= x'
 297     let eq_val v v' =
 298       (* v = v' *)
 299       match (v,v') with
 300         (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)),
 301          Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) ->
 302            ((min1 <= min2) && (max1 >= max2)) or
 303            ((min2 <= min1) && (max2 >= max1))
 304       | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
 305          Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
 306           C_vs_c.eq_type a b
 307       | _ -> v =*= v'
 308     let merge_val v v' = (* values guaranteed to be compatible *)
 309       (* v *)
 310       match (v,v') with
 311         (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)),
 312          Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) ->
 313            if (min1 <= min2) && (max1 >= max2)
 314            then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1))
 315            else
 316              if (min2 <= min1) && (max2 >= max1)
 317              then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))
 318              else failwith "incompatible positions give to merge"
 319       | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
 320          Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
 321           Lib_engine.NormalMetaVal (Ast_c.MetaTypeVal (C_vs_c.merge_type a b))
 322
 323       | _ -> v
 324     let print_mvar (_,s) = Format.print_string s
 325     let print_value x = Pretty_print_engine.pp_binding_kind2 x
 326   end
 327
 328 module CFG =
 329   struct
 330     type node = Ograph_extended.nodei
 331     type cfg = (F.node, F.edge) Ograph_extended.ograph_mutable
 332     let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist)
 333     let successors   cfg n = List.map fst ((cfg#successors n)#tolist)
 334     let extract_is_loop cfg n =
 335       Control_flow_c.extract_is_loop (cfg#nodes#find n)
 336     let print_node i = Format.print_string (i_to_s i)
 337     let size cfg = cfg#nodes#length
 338
 339     (* In ctl_engine, we use 'node' for the node but in the Ograph_extended
 340      * terminology, this 'node' is in fact an index to access the real
 341      * node information (that ctl/ wants to abstract away to be more generic),
 342      * the 'Ograph_extended.nodei'.
 343      *)
 344     let print_graph cfg label border_colors fill_colors filename =
 345       Ograph_extended.print_ograph_mutable_generic cfg label
 346         (fun (nodei, (node: F.node)) ->
 347           (* the string julia wants to put ? *)
 348           let bc = try Some(List.assoc nodei border_colors) with _ -> None in
 349           let fc = try Some(List.assoc nodei fill_colors) with _ -> None in
 350           (* the string yoann put as debug information in the cfg *)
 351           let str = snd node in
 352           (str,bc,fc)
 353         )
 354         ~output_file:filename
 355         ~launch_gv:false
 356   end
 357
 358
 359 module WRAPPED_ENGINE = Wrapper_ctl.CTL_ENGINE_BIS (ENV) (CFG) (PRED)
 360
 361 let print_bench _ = WRAPPED_ENGINE.print_bench()
 362
 363 type pred = Lib_engine.predicate * Ast_cocci.meta_name Ast_ctl.modif
 364
 365 (*****************************************************************************)
 366 let metavars_binding2_to_binding   binding2 =
 367   binding2 +> Common.map_filter (fun (s, kind2) ->
 368     match kind2 with
 369     | Lib_engine.NormalMetaVal kind -> Some (s, kind)
 370     (* I thought it was Impossible to have this when called from
 371        satbis_to_trans_info but it does not seems so *)
 372     | Lib_engine.ParenVal _ -> None
 373     | Lib_engine.LabelVal _ -> None
 374     | Lib_engine.BadVal     -> None (* should not occur *)
 375     | Lib_engine.GoodVal    -> None (* should not occur *)
 376    )
 377
 378 let metavars_binding_to_binding2 binding =
 379   binding +> List.map (fun (s, kind) -> s, Lib_engine.NormalMetaVal kind)
 380
 381
 382 let (satbis_to_trans_info:
 383   (int list *
 384      (nodei * Lib_engine.metavars_binding2 * Lib_engine.predicate)) list ->
 385   (int list *
 386      (nodei * Lib_engine.metavars_binding * Ast_cocci.rule_elem)) list) =
 387   fun xs ->
 388     xs +> List.fold_left (fun prev (index,(nodei, binding2, pred)) ->
 389       match pred with
 390       | Lib_engine.Match (rule_elem) ->
 391           if !Flag.track_iso_usage then show_isos rule_elem;
 392           (index,
 393            (nodei, metavars_binding2_to_binding binding2, rule_elem))
 394           ::prev
 395              (* see BindGood in asttotctl2 *)
 396       | Lib_engine.BindGood (_) -> prev
 397       | _ -> raise Impossible
 398     ) []
 399
 400 (*****************************************************************************)
 401
 402 let rec coalesce_positions = function
 403     [] -> []
 404   | (x,Ast_c.MetaPosValList l)::rest ->
 405       let (same,others) = List.partition (function (x1,_) -> x =*= x1) rest in
 406       let ls =
 407         List.concat
 408           (List.map
 409              (function
 410                  (_,Ast_c.MetaPosValList l) -> l
 411                | _ -> failwith "unexpected non-position")
 412              same) in
 413       let new_ls = List.sort compare (l@ls) in
 414       (x,Ast_c.MetaPosValList new_ls) :: coalesce_positions others
 415   | x::rest -> x :: coalesce_positions rest
 416
 417 (*****************************************************************************)
 418 (* Call ctl engine *)
 419 (*****************************************************************************)
 420 let (mysat2:
 421   Lib_engine.model ->
 422   (Lib_engine.ctlcocci * (pred list list)) ->
 423   (Lib_engine.mvar list*Lib_engine.metavars_binding) ->
 424   (Lib_engine.numbered_transformation_info * bool *
 425      Lib_engine.metavars_binding * Lib_engine.metavars_binding list)) =
 426   fun (flow, label, states) ctl (used_after, binding) ->
 427     let binding2 = metavars_binding_to_binding2 binding in
 428     let (triples,(trans_info2, returned_any_states, used_after_envs)) =
 429       WRAPPED_ENGINE.satbis (flow, label, states) ctl (used_after, binding2)
 430     in
 431     if not (!Flag_parsing_cocci.sgrep_mode || !Flag.sgrep_mode2 ||
 432             !Flag_matcher.allow_inconsistent_paths)
 433     then Check_reachability.check_reachability triples flow;
 434     let (trans_info2,used_after_fresh_envs) =
 435       Postprocess_transinfo.process used_after binding2 trans_info2 in
 436     let used_after_envs =
 437       Common.uniq(List.map2 (@) used_after_fresh_envs used_after_envs) in
 438     let trans_info = satbis_to_trans_info trans_info2 in
 439     let newbindings = List.map metavars_binding2_to_binding used_after_envs in
 440     let newbindings = List.map coalesce_positions newbindings in
 441     (trans_info, returned_any_states, binding, newbindings)
 442
 443 let mysat a b c =
 444   Common.profile_code "mysat" (fun () -> mysat2 a b c)