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