engine/ctlcocci_integration.ml

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