Fix compile on ARM/x86 backends

1 files changed, 2 insertions, 1054 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index bbcc6807..0869007c 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -10,1058 +10,6 @@
 (*                                                             *)
 (* *************************************************************)
 
-open RTLpathLivegenaux
-open RTLpathCommon
-open Datatypes
-open Maps
-open RTL
-open Op
-open Asmgen
-open RTLpath
-open! Integers
-open Camlcoq
-open Option
-open AST
-open DebugPrint
-open RTLcommonaux
+let expanse n ibf btl = btl
 
-(** Mini CSE (a dynamic numbering is applied during expansion. 
-    The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)
-
-(** Managing virtual registers and node index *)
-
-let reg = ref 1
-
-let node = ref 1
-
-let r2p () = P.of_int !reg
-
-let n2p () = P.of_int !node
-
-let r2pi () =
-  reg := !reg + 1;
-  r2p ()
-
-let n2pi () =
-  node := !node + 1;
-  n2p ()
-
-(** Below are the types for rhs and equations *)
-
-type rhs = Sop of operation * int list | Smove
-
-type seq = Seq of int * rhs
-
-(** This is a mini abstraction to have a simpler representation during expansion
-    - Snop will be converted to Inop
-    - (Sr r) is inserted if the value was found in register r
-    - (Sexp dest rhs args succ) represent an instruction
-      (succesor may not be defined at this point, hence the use of type option)
-    - (Sfinalcond cond args succ1 succ2 info) represents a condition (which must
-      always be the last instruction in expansion list *)
-
-type expl =
-  | Snop of P.t
-  | Sr of P.t
-  | Sexp of P.t * rhs * P.t list * node option
-  | Sfinalcond of condition * P.t list * node * node * bool option
-
-(** Record used during the "dynamic" value numbering *)
-
-type numb = {
-  mutable nnext : int;  (** Next unusued value number *)
-  mutable seqs : seq list;  (** equations *)
-  mutable nreg : (P.t, int) Hashtbl.t;  (** mapping registers to values *)
-  mutable nval : (int, P.t list) Hashtbl.t;
-      (** reverse mapping values to registers containing it *)
-}
-
-let print_list_pos l =
-  debug "[";
-  List.iter (fun i -> debug "%d;" (p2i i)) l;
-  debug "]\n"
-
-let empty_numbering () =
-  { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 }
-
-let rec get_nvalues vn = function
-  | [] -> []
-  | r :: rs ->
-      let v =
-        match Hashtbl.find_opt !vn.nreg r with
-        | Some v ->
-            debug "getnval r=%d |-> v=%d\n" (p2i r) v;
-            v
-        | None ->
-            let n = !vn.nnext in
-            debug "getnval r=%d |-> v=%d\n" (p2i r) n;
-            !vn.nnext <- !vn.nnext + 1;
-            Hashtbl.replace !vn.nreg r n;
-            Hashtbl.replace !vn.nval n [ r ];
-            n
-      in
-      let vs = get_nvalues vn rs in
-      v :: vs
-
-let get_nval_ornil vn v =
-  match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l
-
-let forget_reg vn rd =
-  match Hashtbl.find_opt !vn.nreg rd with
-  | Some v ->
-      debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
-      let old_regs = get_nval_ornil vn v in
-      debug "forget_reg: old_regs are:\n";
-      print_list_pos old_regs;
-      Hashtbl.replace !vn.nval v
-        (List.filter (fun n -> not (P.eq n rd)) old_regs)
-  | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd)
-
-let update_reg vn rd v =
-  debug "update_reg: update v=%d with r=%d\n" v (p2i rd);
-  forget_reg vn rd;
-  let old_regs = get_nval_ornil vn v in
-  Hashtbl.replace !vn.nval v (rd :: old_regs)
-
-let rec find_valnum_rhs rh = function
-  | [] -> None
-  | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl
-
-let set_unknown vn rd =
-  debug "set_unknown: rd=%d\n" (p2i rd);
-  forget_reg vn rd;
-  Hashtbl.remove !vn.nreg rd
-
-let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> ()
-
-let addrhs vn rd rh =
-  match find_valnum_rhs rh !vn.seqs with
-  | Some vres ->
-      debug "addrhs: Some v=%d\n" vres;
-      Hashtbl.replace !vn.nreg rd vres;
-      update_reg vn rd vres
-  | None ->
-      let n = !vn.nnext in
-      debug "addrhs: None v=%d\n" n;
-      !vn.nnext <- !vn.nnext + 1;
-      !vn.seqs <- Seq (n, rh) :: !vn.seqs;
-      update_reg vn rd n;
-      Hashtbl.replace !vn.nreg rd n
-
-let addsop vn v op rd =
-  debug "addsop\n";
-  if op = Omove then (
-    update_reg vn rd (List.hd v);
-    Hashtbl.replace !vn.nreg rd (List.hd v))
-  else addrhs vn rd (Sop (op, v))
-
-let rec kill_mem_operations = function
-  | (Seq (v, Sop (op, vl)) as eq) :: tl ->
-      if op_depends_on_memory op then kill_mem_operations tl
-      else eq :: kill_mem_operations tl
-  | [] -> []
-  | eq :: tl -> eq :: kill_mem_operations tl
-
-let reg_valnum vn v =
-  debug "reg_valnum: trying to find a mapping for v=%d\n" v;
-  match Hashtbl.find !vn.nval v with
-  | [] -> None
-  | r :: rs ->
-      debug "reg_valnum: found a mapping r=%d\n" (p2i r);
-      Some r
-
-let rec reg_valnums vn = function
-  | [] -> Some []
-  | v :: vs -> (
-      match (reg_valnum vn v, reg_valnums vn vs) with
-      | Some r, Some rs -> Some (r :: rs)
-      | _, _ -> None)
-
-let find_rhs vn rh =
-  match find_valnum_rhs rh !vn.seqs with
-  | None -> None
-  | Some vres -> reg_valnum vn vres
-
-(** Functions to perform the dynamic reduction during CSE *)
-
-let extract_arg l =
-  if List.length l > 0 then
-    match List.hd l with
-    | Sr r -> (r, List.tl l)
-    | Sexp (rd, _, _, _) -> (rd, l)
-    | _ -> failwith "extract_arg: final instruction arg can not be extracted"
-  else failwith "extract_arg: trying to extract on an empty list"
-
-let extract_final vn fl fdest succ =
-  if List.length fl > 0 then
-    match List.hd fl with
-    | Sr r ->
-        if not (P.eq r fdest) then (
-          let v = get_nvalues vn [ r ] in
-          addsop vn v Omove fdest;
-          Sexp (fdest, Smove, [ r ], Some succ) :: List.tl fl)
-        else Snop succ :: List.tl fl
-    | Sexp (rd, rh, args, None) ->
-        assert (rd = fdest);
-        Sexp (fdest, rh, args, Some succ) :: List.tl fl
-    | _ -> fl
-  else failwith "extract_final: trying to extract on an empty list"
-
-let addinst vn op args rd =
-  let v = get_nvalues vn args in
-  let rh = Sop (op, v) in
-  match find_rhs vn rh with
-  | Some r ->
-      debug "addinst: rhs found with r=%d\n" (p2i r);
-      Sr r
-  | None ->
-      addsop vn v op rd;
-      Sexp (rd, rh, args, None)
-
-(** Expansion functions *)
-
-type immt =
-  | Addiw
-  | Addil
-  | Andiw
-  | Andil
-  | Oriw
-  | Oril
-  | Xoriw
-  | Xoril
-  | Sltiw
-  | Sltiuw
-  | Sltil
-  | Sltiul
-
-let load_hilo32 vn dest hi lo =
-  let op1 = OEluiw hi in
-  if Int.eq lo Int.zero then [ addinst vn op1 [] dest ]
-  else
-    let r = r2pi () in
-    let op2 = OEaddiw (None, lo) in
-    let i1 = addinst vn op1 [] r in
-    let r', l = extract_arg [ i1 ] in
-    let i2 = addinst vn op2 [ r' ] dest in
-    i2 :: l
-
-let load_hilo64 vn dest hi lo =
-  let op1 = OEluil hi in
-  if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ]
-  else
-    let r = r2pi () in
-    let op2 = OEaddil (None, lo) in
-    let i1 = addinst vn op1 [] r in
-    let r', l = extract_arg [ i1 ] in
-    let i2 = addinst vn op2 [ r' ] dest in
-    i2 :: l
-
-let loadimm32 vn dest n =
-  match make_immed32 n with
-  | Imm32_single imm ->
-      let op1 = OEaddiw (Some X0_R, imm) in
-      [ addinst vn op1 [] dest ]
-  | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo
-
-let loadimm64 vn dest n =
-  match make_immed64 n with
-  | Imm64_single imm ->
-      let op1 = OEaddil (Some X0_R, imm) in
-      [ addinst vn op1 [] dest ]
-  | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo
-  | Imm64_large imm ->
-      let op1 = OEloadli imm in
-      [ addinst vn op1 [] dest ]
-
-let get_opimm optR imm = function
-  | Addiw -> OEaddiw (optR, imm)
-  | Andiw -> OEandiw imm
-  | Oriw -> OEoriw imm
-  | Xoriw -> OExoriw imm
-  | Sltiw -> OEsltiw imm
-  | Sltiuw -> OEsltiuw imm
-  | Addil -> OEaddil (optR, imm)
-  | Andil -> OEandil imm
-  | Oril -> OEoril imm
-  | Xoril -> OExoril imm
-  | Sltil -> OEsltil imm
-  | Sltiul -> OEsltiul imm
-
-let opimm32 vn a1 dest n optR op opimm =
-  match make_immed32 n with
-  | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ]
-  | Imm32_pair (hi, lo) ->
-      let r = r2pi () in
-      let l = load_hilo32 vn r hi lo in
-      let r', l' = extract_arg l in
-      let i = addinst vn op [ a1; r' ] dest in
-      i :: l'
-
-let opimm64 vn a1 dest n optR op opimm =
-  match make_immed64 n with
-  | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ]
-  | Imm64_pair (hi, lo) ->
-      let r = r2pi () in
-      let l = load_hilo64 vn r hi lo in
-      let r', l' = extract_arg l in
-      let i = addinst vn op [ a1; r' ] dest in
-      i :: l'
-  | Imm64_large imm ->
-      let r = r2pi () in
-      let op1 = OEloadli imm in
-      let i1 = addinst vn op1 [] r in
-      let r', l' = extract_arg [ i1 ] in
-      let i2 = addinst vn op [ a1; r' ] dest in
-      i2 :: l'
-
-let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw
-
-let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw
-
-let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw
-
-let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw
-
-let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw
-
-let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw
-
-let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil
-
-let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil
-
-let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril
-
-let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril
-
-let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil
-
-let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul
-
-let is_inv_cmp = function Cle | Cgt -> true | _ -> false
-
-let make_optR is_x0 is_inv =
-  if is_x0 then if is_inv then Some X0_L else Some X0_R else None
-
-let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> Sfinalcond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> Sfinalcond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> Sfinalcond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> Sfinalcond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cond_int32s vn is_x0 cmp a1 a2 dest =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ]
-  | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ]
-  | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ]
-  | Cle ->
-      let r = r2pi () in
-      let op = OEsltw optR in
-      let i1 = addinst vn op [ a2; a1 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-  | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ]
-  | Cge ->
-      let r = r2pi () in
-      let op = OEsltw optR in
-      let i1 = addinst vn op [ a1; a2 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-
-let cond_int32u vn is_x0 cmp a1 a2 dest =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ]
-  | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ]
-  | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ]
-  | Cle ->
-      let r = r2pi () in
-      let op = OEsltuw optR in
-      let i1 = addinst vn op [ a2; a1 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-  | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ]
-  | Cge ->
-      let r = r2pi () in
-      let op = OEsltuw optR in
-      let i1 = addinst vn op [ a1; a2 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-
-let cond_int64s vn is_x0 cmp a1 a2 dest =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ]
-  | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ]
-  | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ]
-  | Cle ->
-      let r = r2pi () in
-      let op = OEsltl optR in
-      let i1 = addinst vn op [ a2; a1 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-  | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ]
-  | Cge ->
-      let r = r2pi () in
-      let op = OEsltl optR in
-      let i1 = addinst vn op [ a1; a2 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-
-let cond_int64u vn is_x0 cmp a1 a2 dest =
-  let optR = make_optR is_x0 (is_inv_cmp cmp) in
-  match cmp with
-  | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ]
-  | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ]
-  | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ]
-  | Cle ->
-      let r = r2pi () in
-      let op = OEsltul optR in
-      let i1 = addinst vn op [ a2; a1 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-  | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ]
-  | Cge ->
-      let r = r2pi () in
-      let op = OEsltul optR in
-      let i1 = addinst vn op [ a1; a2 ] r in
-      let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest :: l
-
-let is_normal_cmp = function Cne -> false | _ -> true
-
-let cond_float vn cmp f1 f2 dest =
-  match cmp with
-  | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ]
-  | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ]
-  | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ]
-  | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ]
-  | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ]
-  | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ]
-
-let cond_single vn cmp f1 f2 dest =
-  match cmp with
-  | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ]
-  | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ]
-  | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ]
-  | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ]
-  | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ]
-  | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ]
-
-let expanse_cbranchimm_int32s vn cmp a1 n info succ1 succ2 =
-  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 []
-  else
-    let r = r2pi () in
-    let l = loadimm32 vn r n in
-    let r', l' = extract_arg l in
-    cbranch_int32s false cmp a1 r' info succ1 succ2 l'
-
-let expanse_cbranchimm_int32u vn cmp a1 n info succ1 succ2 =
-  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 []
-  else
-    let r = r2pi () in
-    let l = loadimm32 vn r n in
-    let r', l' = extract_arg l in
-    cbranch_int32u false cmp a1 r' info succ1 succ2 l'
-
-let expanse_cbranchimm_int64s vn cmp a1 n info succ1 succ2 =
-  if Int64.eq n Int64.zero then
-    cbranch_int64s true cmp a1 a1 info succ1 succ2 []
-  else
-    let r = r2pi () in
-    let l = loadimm64 vn r n in
-    let r', l' = extract_arg l in
-    cbranch_int64s false cmp a1 r' info succ1 succ2 l'
-
-let expanse_cbranchimm_int64u vn cmp a1 n info succ1 succ2 =
-  if Int64.eq n Int64.zero then
-    cbranch_int64u true cmp a1 a1 info succ1 succ2 []
-  else
-    let r = r2pi () in
-    let l = loadimm64 vn r n in
-    let r', l' = extract_arg l in
-    cbranch_int64u false cmp a1 r' info succ1 succ2 l'
-
-let expanse_condimm_int32s vn cmp a1 n dest =
-  if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest
-  else
-    match cmp with
-    | Ceq | Cne ->
-        let r = r2pi () in
-        let l = xorimm32 vn a1 r n in
-        let r', l' = extract_arg l in
-        cond_int32s vn true cmp r' r' dest @ l'
-    | Clt -> sltimm32 vn a1 dest n
-    | Cle ->
-        if Int.eq n (Int.repr Int.max_signed) then
-          let l = loadimm32 vn dest Int.one in
-          let r, l' = extract_arg l in
-          addinst vn (OEmayundef MUint) [ a1; r ] dest :: l'
-        else sltimm32 vn a1 dest (Int.add n Int.one)
-    | _ ->
-        let r = r2pi () in
-        let l = loadimm32 vn r n in
-        let r', l' = extract_arg l in
-        cond_int32s vn false cmp a1 r' dest @ l'
-
-let expanse_condimm_int32u vn cmp a1 n dest =
-  if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest
-  else
-    match cmp with
-    | Clt -> sltuimm32 vn a1 dest n
-    | _ ->
-        let r = r2pi () in
-        let l = loadimm32 vn r n in
-        let r', l' = extract_arg l in
-        cond_int32u vn false cmp a1 r' dest @ l'
-
-let expanse_condimm_int64s vn cmp a1 n dest =
-  if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest
-  else
-    match cmp with
-    | Ceq | Cne ->
-        let r = r2pi () in
-        let l = xorimm64 vn a1 r n in
-        let r', l' = extract_arg l in
-        cond_int64s vn true cmp r' r' dest @ l'
-    | Clt -> sltimm64 vn a1 dest n
-    | Cle ->
-        if Int64.eq n (Int64.repr Int64.max_signed) then
-          let l = loadimm32 vn dest Int.one in
-          let r, l' = extract_arg l in
-          addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l'
-        else sltimm64 vn a1 dest (Int64.add n Int64.one)
-    | _ ->
-        let r = r2pi () in
-        let l = loadimm64 vn r n in
-        let r', l' = extract_arg l in
-        cond_int64s vn false cmp a1 r' dest @ l'
-
-let expanse_condimm_int64u vn cmp a1 n dest =
-  if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest
-  else
-    match cmp with
-    | Clt -> sltuimm64 vn a1 dest n
-    | _ ->
-        let r = r2pi () in
-        let l = loadimm64 vn r n in
-        let r', l' = extract_arg l in
-        cond_int64u vn false cmp a1 r' dest @ l'
-
-let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest =
-  let normal = is_normal_cmp cmp in
-  let normal' = if cnot then not normal else normal in
-  let insn = fn_cond vn cmp f1 f2 dest in
-  if normal' then insn
-  else
-    let r', l = extract_arg insn in
-    addinst vn (OExoriw Int.one) [ r' ] dest :: l
-
-let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 =
-  let r = r2pi () in
-  let normal = is_normal_cmp cmp in
-  let normal' = if cnot then not normal else normal in
-  let insn = fn_cond vn cmp f1 f2 r in
-  let r', l = extract_arg insn in
-  if normal' then
-    Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
-  else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
-
-(** Form a list containing both sources and destination regs of an instruction *)
-
-let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
-
-let get_regs_inst = function
-  | Inop _ -> []
-  | Iop (_, args, dest, _) -> dest :: args
-  | Iload (_, _, _, args, dest, _) -> dest :: args
-  | Istore (_, _, args, src, _) -> src :: args
-  | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args)
-  | Itailcall (_, t, args) -> get_regindent t @ args
-  | Ibuiltin (_, args, dest, _) ->
-      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
-  | Icond (_, args, _, _, _) -> args
-  | Ijumptable (arg, _) -> [ arg ]
-  | Ireturn (Some r) -> [ r ]
-  | _ -> []
-
-(** Modify pathmap according to the size of the expansion list *)
-
-let write_pathmap initial esize pm' =
-  debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize;
-  let path = get_some @@ PTree.get initial !pm' in
-  let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in
-  let path' =
-    {
-      psize = npsize;
-      input_regs = path.input_regs;
-      pre_output_regs = path.pre_output_regs;
-      output_regs = path.output_regs;
-    }
-  in
-  pm' := PTree.set initial path' !pm'
-
-(** Write a single instruction in the tree and update order *)
-
-let write_inst target_node inst code' new_order =
-  code' := PTree.set (P.of_int target_node) inst !code';
-  new_order := P.of_int target_node :: !new_order
-
-(** Return olds args if the CSE numbering is empty *)
-
-let get_arguments vn vals args =
-  match reg_valnums vn vals with Some args' -> args' | None -> args
-
-(** Update the code tree with the expansion list *)
-
-let rec write_tree vn exp initial current code' new_order fturn =
-  debug "wt: node is %d\n" !node;
-  let target_node, next_node =
-    if fturn then (P.to_int initial, current) else (current, current - 1)
-  in
-  match exp with
-  | Sr r :: _ ->
-      failwith "write_tree: there are still some symbolic values in the list"
-  | Sexp (rd, Sop (op, vals), args, None) :: k ->
-      let args = get_arguments vn vals args in
-      let inst = Iop (op, args, rd, P.of_int next_node) in
-      write_inst target_node inst code' new_order;
-      write_tree vn k initial next_node code' new_order false
-  | [ Snop succ ] ->
-      let inst = Inop succ in
-      write_inst target_node inst code' new_order
-  | [ Sexp (rd, Sop (op, vals), args, Some succ) ] ->
-      let args = get_arguments vn vals args in
-      let inst = Iop (op, args, rd, succ) in
-      write_inst target_node inst code' new_order
-  | [ Sexp (rd, Smove, args, Some succ) ] ->
-      let inst = Iop (Omove, args, rd, succ) in
-      write_inst target_node inst code' new_order
-  | [ Sfinalcond (cond, args, succ1, succ2, info) ] ->
-      let inst = Icond (cond, args, succ1, succ2, info) in
-      write_inst target_node inst code' new_order
-  | [] -> ()
-  | _ -> failwith "write_tree: invalid list"
-
-(** Main expansion function - TODO gourdinl to split? *)
-let expanse (sb : superblock) code pm =
-  debug "#### New superblock for expansion oracle\n";
-  let new_order = ref [] in
-  let liveins = ref sb.liveins in
-  let exp = ref [] in
-  let was_branch = ref false in
-  let was_exp = ref false in
-  let code' = ref code in
-  let pm' = ref pm in
-  let vn = ref (empty_numbering ()) in
-  Array.iter
-    (fun n ->
-      was_branch := false;
-      was_exp := false;
-      let inst = get_some @@ PTree.get n code in
-      (if !Clflags.option_fexpanse_rtlcond then
-       match inst with
-       (* Expansion of conditions - Ocmp *)
-       | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccomp\n";
-           exp := cond_int32s vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccompu\n";
-           exp := cond_int32u vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccompimm\n";
-           exp := expanse_condimm_int32s vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccompuimm\n";
-           exp := expanse_condimm_int32u vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccompl\n";
-           exp := cond_int64s vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccomplu\n";
-           exp := cond_int64u vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccomplimm\n";
-           exp := expanse_condimm_int64s vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccompluimm\n";
-           exp := expanse_condimm_int64u vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Ccompf\n";
-           exp := expanse_cond_fp vn false cond_float c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Cnotcompf\n";
-           exp := expanse_cond_fp vn true cond_float c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Ccompfs\n";
-           exp := expanse_cond_fp vn false cond_single c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Cnotcompfs\n";
-           exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       (* Expansion of branches - Ccomp *)
-       | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccomp\n";
-           exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompu\n";
-           exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompimm\n";
-           exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompuimm\n";
-           exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompl\n";
-           exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccomplu\n";
-           exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccomplimm\n";
-           exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompluimm\n";
-           exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompf\n";
-           exp :=
-             expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Cnotcompf\n";
-           exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompfs\n";
-           exp :=
-             expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Cnotcompfs\n";
-           exp :=
-             expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | _ -> ());
-      (if !Clflags.option_fexpanse_others && not !was_exp then
-       match inst with
-       | Iop (Ofloatconst f, nil, dest, succ) -> (
-           match make_immed64 (Floats.Float.to_bits f) with
-           | Imm64_single _ | Imm64_large _ -> ()
-           | Imm64_pair (hi, lo) ->
-               debug "Iop/Ofloatconst\n";
-               let r = r2pi () in
-               let l = load_hilo64 vn r hi lo in
-               let r', l' = extract_arg l in
-               exp := addinst vn Ofloat_of_bits [ r' ] dest :: l';
-               exp := extract_final vn !exp dest succ;
-               was_exp := true)
-       | Iop (Osingleconst f, nil, dest, succ) -> (
-           match make_immed32 (Floats.Float32.to_bits f) with
-           | Imm32_single imm -> ()
-           | Imm32_pair (hi, lo) ->
-               debug "Iop/Osingleconst\n";
-               let r = r2pi () in
-               let l = load_hilo32 vn r hi lo in
-               let r', l' = extract_arg l in
-               exp := addinst vn Osingle_of_bits [ r' ] dest :: l';
-               exp := extract_final vn !exp dest succ;
-               was_exp := true)
-       | Iop (Ointconst n, nil, dest, succ) ->
-           debug "Iop/Ointconst\n";
-           exp := loadimm32 vn dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Olongconst n, nil, dest, succ) ->
-           debug "Iop/Olongconst\n";
-           exp := loadimm64 vn dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oaddimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oaddimm\n";
-           exp := addimm32 vn a1 dest n None;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oaddlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oaddlimm\n";
-           exp := addimm64 vn a1 dest n None;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oandimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oandimm\n";
-           exp := andimm32 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oandlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oandlimm\n";
-           exp := andimm64 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oorimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oorimm\n";
-           exp := orimm32 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oorlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oorlimm\n";
-           exp := orimm64 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oxorimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oxorimm\n";
-           exp := xorimm32 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oxorlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oxorlimm\n";
-           exp := xorimm64 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocast8signed, a1 :: nil, dest, succ) ->
-           debug "Iop/cast8signed\n";
-           let op = Oshlimm (Int.repr (Z.of_sint 24)) in
-           let r = r2pi () in
-           let i1 = addinst vn op [ a1 ] r in
-           let r', l = extract_arg [ i1 ] in
-           exp :=
-             addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocast16signed, a1 :: nil, dest, succ) ->
-           debug "Iop/cast16signed\n";
-           let op = Oshlimm (Int.repr (Z.of_sint 16)) in
-           let r = r2pi () in
-           let i1 = addinst vn op [ a1 ] r in
-           let r', l = extract_arg [ i1 ] in
-           exp :=
-             addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocast32unsigned, a1 :: nil, dest, succ) ->
-           debug "Iop/Ocast32unsigned\n";
-           let r1 = r2pi () in
-           let r2 = r2pi () in
-           let op1 = Ocast32signed in
-           let i1 = addinst vn op1 [ a1 ] r1 in
-           let r1', l1 = extract_arg [ i1 ] in
-
-           let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in
-           let i2 = addinst vn op2 [ r1' ] r2 in
-           let r2', l2 = extract_arg (i2 :: l1) in
-
-           let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in
-           exp := addinst vn op3 [ r2' ] dest :: l2;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oshrximm n, a1 :: nil, dest, succ) ->
-           if Int.eq n Int.zero then (
-             debug "Iop/Oshrximm1\n";
-             exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
-           else if Int.eq n Int.one then (
-             debug "Iop/Oshrximm2\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
-
-             let op2 = Oadd in
-             let i2 = addinst vn op2 [ a1; r1' ] r2 in
-             let r2', l2 = extract_arg (i2 :: l1) in
-
-             let op3 = Oshrimm Int.one in
-             let i3 = addinst vn op3 [ r2' ] dest in
-             let r3, l3 = extract_arg (i3 :: l2) in
-             exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3)
-           else (
-             debug "Iop/Oshrximm3\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let r3 = r2pi () in
-             let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
-
-             let op2 = Oshruimm (Int.sub Int.iwordsize n) in
-             let i2 = addinst vn op2 [ r1' ] r2 in
-             let r2', l2 = extract_arg (i2 :: l1) in
-
-             let op3 = Oadd in
-             let i3 = addinst vn op3 [ a1; r2' ] r3 in
-             let r3', l3 = extract_arg (i3 :: l2) in
-
-             let op4 = Oshrimm n in
-             let i4 = addinst vn op4 [ r3' ] dest in
-             let r4, l4 = extract_arg (i4 :: l3) in
-             exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4);
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oshrxlimm n, a1 :: nil, dest, succ) ->
-           if Int.eq n Int.zero then (
-             debug "Iop/Oshrxlimm1\n";
-             exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
-           else if Int.eq n Int.one then (
-             debug "Iop/Oshrxlimm2\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
-
-             let op2 = Oaddl in
-             let i2 = addinst vn op2 [ a1; r1' ] r2 in
-             let r2', l2 = extract_arg (i2 :: l1) in
-
-             let op3 = Oshrlimm Int.one in
-             let i3 = addinst vn op3 [ r2' ] dest in
-             let r3, l3 = extract_arg (i3 :: l2) in
-             exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3)
-           else (
-             debug "Iop/Oshrxlimm3\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let r3 = r2pi () in
-             let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
-
-             let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in
-             let i2 = addinst vn op2 [ r1' ] r2 in
-             let r2', l2 = extract_arg (i2 :: l1) in
-
-             let op3 = Oaddl in
-             let i3 = addinst vn op3 [ a1; r2' ] r3 in
-             let r3', l3 = extract_arg (i3 :: l2) in
-
-             let op4 = Oshrlimm n in
-             let i4 = addinst vn op4 [ r3' ] dest in
-             let r4, l4 = extract_arg (i4 :: l3) in
-             exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4);
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | _ -> ());
-      (* Update the CSE numbering *)
-      (if not !was_exp then
-       match inst with
-       | Iop (op, args, dest, succ) ->
-           let v = get_nvalues vn args in
-           addsop vn v op dest
-       | Iload (_, _, _, _, dst, _) -> set_unknown vn dst
-       | Istore (chk, addr, args, src, s) ->
-           !vn.seqs <- kill_mem_operations !vn.seqs
-       | Icall (_, _, _, _, _) | Itailcall (_, _, _) | Ibuiltin (_, _, _, _) ->
-           vn := empty_numbering ()
-       | _ -> ());
-      (* Update code, liveins, pathmap, and order of the superblock for one expansion *)
-      if !was_exp then (
-        (if !was_branch && List.length !exp > 1 then
-         let lives = PTree.get n !liveins in
-         match lives with
-         | Some lives ->
-             let new_branch_pc = P.of_int (!node + 1) in
-             liveins := PTree.set new_branch_pc lives !liveins;
-             liveins := PTree.remove n !liveins
-         | _ -> ());
-        node := !node + List.length !exp - 1;
-        write_pathmap sb.instructions.(0) (List.length !exp - 1) pm';
-        write_tree vn (List.rev !exp) n !node code' new_order true)
-      else new_order := n :: !new_order)
-    sb.instructions;
-  sb.instructions <- Array.of_list (List.rev !new_order);
-  sb.liveins <- !liveins;
-  (!code', !pm')
-
-(** Compute the last used node and reg indexs *)
-
-let rec find_last_node_reg = function
-  | [] -> ()
-  | (pc, i) :: k ->
-      let rec traverse_list var = function
-        | [] -> ()
-        | e :: t ->
-            let e' = p2i e in
-            if e' > !var then var := e';
-            traverse_list var t
-      in
-      traverse_list node [ pc ];
-      traverse_list reg (get_regs_inst i);
-      find_last_node_reg k
+let find_last_node_reg c = ()