path: root/riscV/ExpansionOracle.ml

(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*                                                             *)
(*  Copyright VERIMAG. All rights reserved.                    *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

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 Printf

(** Mini CSE (a dynamic numbering is applied during expansion. 
    The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)

let exp_debug = false

(** Managing virtual registers and node index *)

let reg = ref 1

let node = ref 1

let p2i r = P.to_int r

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 =
  if exp_debug then eprintf "[";
  List.iter (fun i -> if exp_debug then eprintf "%d;" (p2i i)) l;
  if exp_debug then eprintf "]\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 ->
            if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) v;
            v
        | None ->
            let n = !vn.nnext in
            if exp_debug then eprintf "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 ->
      if exp_debug then eprintf "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
      let old_regs = get_nval_ornil vn v in
      if exp_debug then eprintf "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 ->
      if exp_debug then eprintf "forget_reg: no mapping for r=%d\n" (p2i rd)

let update_reg vn rd v =
  if exp_debug then eprintf "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 =
  if exp_debug then eprintf "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 ->
      if exp_debug then eprintf "addrhs: Some v=%d\n" vres;
      Hashtbl.replace !vn.nreg rd vres;
      update_reg vn rd vres
  | None ->
      let n = !vn.nnext in
      if exp_debug then eprintf "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 =
  if exp_debug then eprintf "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 =
  if exp_debug then eprintf "reg_valnum: trying to find a mapping for v=%d\n" v;
  match Hashtbl.find !vn.nval v with
  | [] -> None
  | r :: rs ->
      if exp_debug then eprintf "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 ->
      if exp_debug then eprintf "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

let addptrofs vn n dest =
  if Ptrofs.eq_dec n Ptrofs.zero then [ addinst vn OEmoveSP [] dest ]
  else if Archi.ptr64 then
    match make_immed64 (Ptrofs.to_int64 n) with
    | Imm64_single imm -> [ addinst vn (OEaddil (Some SP_S, imm)) [] 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
        addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: 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
        addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l
  else
    match make_immed32 (Ptrofs.to_int n) with
    | Imm32_single imm -> [ addinst vn (OEaddiw (Some SP_S, imm)) [] 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
        addinst vn (OEaddiw (Some SP_S, Int.zero)) [ r' ] dest :: 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' =
  if exp_debug then
    eprintf "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 =
  if exp_debug then eprintf "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 =
  if exp_debug then eprintf "#### 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 exp_debug then eprintf "We are checking node %d\n" (p2i n);
      (if !Clflags.option_fexpanse_rtlcond then
       match inst with
       (* Expansion of conditions - Ocmp *)
       | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "Iop/Ofloatconst\n";
           let r = r2pi () in
           let l = loadimm64 vn r (Floats.Float.to_bits f) 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) ->
           if exp_debug then eprintf "Iop/Osingleconst\n";
           let r = r2pi () in
           let l = loadimm32 vn r (Floats.Float32.to_bits f) 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) ->
           if exp_debug then eprintf "Iop/Ointconst\n";
           exp := loadimm32 vn dest n;
           exp := extract_final vn !exp dest succ;
           was_exp := true
       | Iop (Olongconst n, nil, dest, succ) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "Iop/Oorlimm\n";
           exp := orimm64 vn a1 dest n;
           exp := extract_final vn !exp dest succ;
           was_exp := true
       | Iop (Ocast8signed, a1 :: nil, dest, succ) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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) ->
           if exp_debug then eprintf "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 (
             if exp_debug then eprintf "Iop/Oshrximm1\n";
             exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
           else if Int.eq n Int.one then (
             if exp_debug then eprintf "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 (
             if exp_debug then eprintf "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 (
             if exp_debug then eprintf "Iop/Oshrxlimm1\n";
             exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
           else if Int.eq n Int.one then (
             if exp_debug then eprintf "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 (
             if exp_debug then eprintf "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
           (*| Iop (Oaddrstack n, nil, dest, succ) ->*)
           (*if exp_debug then eprintf "Iop/Oaddrstack\n";*)
           (*exp := addptrofs vn n dest;*)
           (*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 (
        node := !node + List.length !exp - 1;
        (if !was_branch && List.length !exp > 1 then
         let lives = PTree.get n !liveins in
         match lives with
         | Some lives ->
             let new_branch_pc = n2p () in
             liveins := PTree.set new_branch_pc lives !liveins;
             liveins := PTree.remove n !liveins
         | _ -> ());
        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