engine/ctlcocci_integration.ml

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