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 DebugPrint
open RTLpath
open! Integers
open Camlcoq
open Option

type sop = Sop of operation * P.t list

type sval = Si of RTL.instruction | Sr of P.t

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 ()

type immt =
  | Addiw
  | Addil
  | Andiw
  | Andil
  | Oriw
  | Oril
  | Xoriw
  | Xoril
  | Sltiw
  | Sltiuw
  | Sltil
  | Sltiul

let find_or_addnmove op args rd succ map_consts not_final =
  let sop = Sop (op, args) in
  match Hashtbl.find_opt map_consts sop with
  | Some r ->
      if not_final then node := !node - 1;
      Sr (P.of_int r)
  | None ->
      if not (List.exists (fun a -> a = rd) args) && not_final then
        Hashtbl.add map_consts sop (p2i rd);
      Si (Iop (op, args, rd, succ))

let build_head_tuple head sv =
  match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r)

let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r

let unzip_head_tuple_move ht r succ =
  match ht with
  | l, Some r' ->
      if r' != r then [ Iop (Omove, [ r' ], r, succ) ] else [ Inop succ ]
  | l, None -> l

let build_full_ilist op args dest succ hd k map_consts =
  let sv = find_or_addnmove op args dest succ map_consts false in
  let ht = build_head_tuple hd sv in
  unzip_head_tuple_move ht dest succ @ k

let load_hilo32 dest hi lo succ map_consts not_final =
  let op1 = OEluiw hi in
  if Int.eq lo Int.zero then
    let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
    build_head_tuple [] sv
  else
    let r = r2pi () in
    let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in
    let ht1 = build_head_tuple [] sv1 in
    let r' = unzip_head_tuple ht1 r in
    let op2 = OEaddiw lo in
    let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in
    build_head_tuple (fst ht1) sv2

let load_hilo64 dest hi lo succ map_consts not_final =
  let op1 = OEluil hi in
  if Int64.eq lo Int64.zero then
    let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
    build_head_tuple [] sv
  else
    let r = r2pi () in
    let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in
    let ht1 = build_head_tuple [] sv1 in
    let r' = unzip_head_tuple ht1 r in
    let op2 = OEaddil lo in
    let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in
    build_head_tuple (fst ht1) sv2

let loadimm32 dest n succ map_consts not_final =
  match make_immed32 n with
  | Imm32_single imm ->
      let op1 = OEaddiwr0 imm in
      let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
      build_head_tuple [] sv
  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final

let loadimm64 dest n succ map_consts not_final =
  match make_immed64 n with
  | Imm64_single imm ->
      let op1 = OEaddilr0 imm in
      let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
      build_head_tuple [] sv
  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final
  | Imm64_large imm ->
      let op1 = OEloadli imm in
      let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
      build_head_tuple [] sv

let get_opimm imm = function
  | Addiw -> OEaddiw imm
  | Andiw -> OEandiw imm
  | Oriw -> OEoriw imm
  | Xoriw -> OExoriw imm
  | Sltiw -> OEsltiw imm
  | Sltiuw -> OEsltiuw imm
  | Addil -> OEaddil imm
  | Andil -> OEandil imm
  | Oril -> OEoril imm
  | Xoril -> OExoril imm
  | Sltil -> OEsltil imm
  | Sltiul -> OEsltiul imm

let opimm32 a1 dest n succ k op opimm map_consts =
  match make_immed32 n with
  | Imm32_single imm ->
      build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts
  | Imm32_pair (hi, lo) ->
      let r = r2pi () in
      let ht = load_hilo32 r hi lo (n2pi ()) map_consts true in
      let r' = unzip_head_tuple ht r in
      build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts

let opimm64 a1 dest n succ k op opimm map_consts =
  match make_immed64 n with
  | Imm64_single imm ->
      build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts
  | Imm64_pair (hi, lo) ->
      let r = r2pi () in
      let ht = load_hilo64 r hi lo (n2pi ()) map_consts true in
      let r' = unzip_head_tuple ht r in
      build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts
  | Imm64_large imm ->
      let r = r2pi () in
      let op1 = OEloadli imm in
      let inode = n2pi () in
      let sv = find_or_addnmove op1 [] r inode map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts

let addimm32 a1 dest n succ k map_consts =
  opimm32 a1 dest n succ k Oadd Addiw map_consts

let andimm32 a1 dest n succ k map_consts =
  opimm32 a1 dest n succ k Oand Andiw map_consts

let orimm32 a1 dest n succ k map_consts =
  opimm32 a1 dest n succ k Oor Oriw map_consts

let xorimm32 a1 dest n succ k map_consts =
  opimm32 a1 dest n succ k Oxor Xoriw map_consts

let sltimm32 a1 dest n succ k map_consts =
  opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts

let sltuimm32 a1 dest n succ k map_consts =
  opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts

let addimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oaddl Addil

let andimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oandl Andil

let orimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oorl Oril

let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril

let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil

let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul

let is_inv_cmp = function Cle | Cgt -> true | _ -> false

let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None

let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k

let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Icond (CEbequw optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cne -> Icond (CEbneuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k

let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k

let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Icond (CEbequl optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cne -> Icond (CEbneul optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k
  | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k
  | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k

let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> [ Iop (OEseqw optR0, [ a1; a2 ], dest, succ) ]
  | Cne -> [ Iop (OEsnew optR0, [ a1; a2 ], dest, succ) ]
  | Clt -> [ Iop (OEsltw optR0, [ a1; a2 ], dest, succ) ]
  | Cle ->
      let r = r2pi () in
      let op = OEsltw optR0 in
      let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
  | Cgt -> [ Iop (OEsltw optR0, [ a2; a1 ], dest, succ) ]
  | Cge ->
      let r = r2pi () in
      let op = OEsltw optR0 in
      let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]

let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> [ Iop (OEsequw optR0, [ a1; a2 ], dest, succ) ]
  | Cne -> [ Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) ]
  | Clt -> [ Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) ]
  | Cle ->
      let r = r2pi () in
      let op = OEsltuw optR0 in
      let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
  | Cgt -> [ Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) ]
  | Cge ->
      let r = r2pi () in
      let op = OEsltuw optR0 in
      let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]

let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> [ Iop (OEseql optR0, [ a1; a2 ], dest, succ) ]
  | Cne -> [ Iop (OEsnel optR0, [ a1; a2 ], dest, succ) ]
  | Clt -> [ Iop (OEsltl optR0, [ a1; a2 ], dest, succ) ]
  | Cle ->
      let r = r2pi () in
      let op = OEsltl optR0 in
      let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
  | Cgt -> [ Iop (OEsltl optR0, [ a2; a1 ], dest, succ) ]
  | Cge ->
      let r = r2pi () in
      let op = OEsltl optR0 in
      let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]

let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> [ Iop (OEsequl optR0, [ a1; a2 ], dest, succ) ]
  | Cne -> [ Iop (OEsneul optR0, [ a1; a2 ], dest, succ) ]
  | Clt -> [ Iop (OEsltul optR0, [ a1; a2 ], dest, succ) ]
  | Cle ->
      let r = r2pi () in
      let op = OEsltul optR0 in
      let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
  | Cgt -> [ Iop (OEsltul optR0, [ a2; a1 ], dest, succ) ]
  | Cge ->
      let r = r2pi () in
      let op = OEsltul optR0 in
      let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]

let is_normal_cmp = function Cne -> false | _ -> true

let cond_float cmp f1 f2 dest succ map_consts =
  match cmp with
  | Ceq -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ]
  | Cne -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ]
  | Clt -> [ Iop (OEfltd, [ f1; f2 ], dest, succ) ]
  | Cle -> [ Iop (OEfled, [ f1; f2 ], dest, succ) ]
  | Cgt -> [ Iop (OEfltd, [ f2; f1 ], dest, succ) ]
  | Cge -> [ Iop (OEfled, [ f2; f1 ], dest, succ) ]

let cond_single cmp f1 f2 dest succ map_consts =
  match cmp with
  | Ceq -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ]
  | Cne -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ]
  | Clt -> [ Iop (OEflts, [ f1; f2 ], dest, succ) ]
  | Cle -> [ Iop (OEfles, [ f1; f2 ], dest, succ) ]
  | Cgt -> [ Iop (OEflts, [ f2; f1 ], dest, succ) ]
  | Cge -> [ Iop (OEfles, [ f2; f1 ], dest, succ) ]

let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts =
  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
  else
    let r = r2pi () in
    let ht = loadimm32 r n (n2pi ()) map_consts true in
    let r' = unzip_head_tuple ht r in
    fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k

let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts =
  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
  else
    let r = r2pi () in
    let ht = loadimm32 r n (n2pi ()) map_consts true in
    let r' = unzip_head_tuple ht r in
    fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k

let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts =
  if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
  else
    let r = r2pi () in
    let ht = loadimm64 r n (n2pi ()) map_consts true in
    let r' = unzip_head_tuple ht r in
    fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k

let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts =
  if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
  else
    let r = r2pi () in
    let ht = loadimm64 r n (n2pi ()) map_consts true in
    let r' = unzip_head_tuple ht r in
    fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k

let get_tmp_reg = function Cle | Cge -> Some (n2pi ()) | _ -> None

let expanse_condimm_int32s cmp a1 n dest succ map_consts =
  if Int.eq n Int.zero then
    let tmp_reg = get_tmp_reg cmp in
    cond_int32s true cmp a1 a1 dest tmp_reg succ map_consts
  else
    match cmp with
    | Ceq | Cne ->
        let r = r2pi () in
        xorimm32 a1 r n (n2pi ())
          (cond_int32s true cmp r r dest None succ map_consts)
          map_consts
    | Clt -> sltimm32 a1 dest n succ [] map_consts
    | Cle ->
        if Int.eq n (Int.repr Int.max_signed) then
          let ht = loadimm32 dest Int.one succ map_consts false in
          fst ht
        else sltimm32 a1 dest (Int.add n Int.one) succ [] map_consts
    | _ ->
        let r = r2pi () in
        let tmp_reg = get_tmp_reg cmp in
        let ht = loadimm32 r n (n2pi ()) map_consts true in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ map_consts

let expanse_condimm_int32u cmp a1 n dest succ map_consts =
  let tmp_reg = get_tmp_reg cmp in
  if Int.eq n Int.zero then
    cond_int32u true cmp a1 a1 dest tmp_reg succ map_consts
  else
    match cmp with
    | Clt -> sltuimm32 a1 dest n succ [] map_consts
    | _ ->
        let r = r2pi () in
        let ht = loadimm32 r n (n2pi ()) map_consts true in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ map_consts

let expanse_condimm_int64s cmp a1 n dest succ map_consts =
  if Int64.eq n Int64.zero then
    let tmp_reg = get_tmp_reg cmp in
    cond_int64s true cmp a1 a1 dest tmp_reg succ map_consts
  else
    match cmp with
    | Ceq | Cne ->
        let r = r2pi () in
        xorimm64 a1 r n (n2pi ())
          (cond_int64s true cmp r r dest None succ map_consts)
          map_consts
    | Clt -> sltimm64 a1 dest n succ [] map_consts
    | Cle ->
        if Int64.eq n (Int64.repr Int64.max_signed) then
          let ht = loadimm32 dest Int.one succ map_consts false in
          fst ht
        else sltimm64 a1 dest (Int64.add n Int64.one) succ [] map_consts
    | _ ->
        let r = r2pi () in
        let tmp_reg = get_tmp_reg cmp in
        let ht = loadimm64 r n (n2pi ()) map_consts true in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ map_consts

let expanse_condimm_int64u cmp a1 n dest succ map_consts =
  let tmp_reg = get_tmp_reg cmp in
  if Int64.eq n Int64.zero then
    cond_int64u true cmp a1 a1 dest tmp_reg succ map_consts
  else
    match cmp with
    | Clt -> sltuimm64 a1 dest n succ [] map_consts
    | _ ->
        let r = r2pi () in
        let ht = loadimm64 r n (n2pi ()) map_consts true in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ map_consts

let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ map_consts =
  let normal = is_normal_cmp cmp in
  let normal' = if cnot then not normal else normal in
  let succ' = if normal' then succ else n2pi () in
  let insn = fn_cond cmp f1 f2 dest succ' map_consts in
  if normal' then insn
  else build_full_ilist (OExoriw Int.one) [ dest ] dest succ insn [] map_consts

let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts =
  let r = r2pi () in
  let normal = is_normal_cmp cmp in
  let normal' = if cnot then not normal else normal in
  let insn = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in
  insn
  ::
  (if normal' then [ Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) ]
  else [ Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info) ])

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 ]
  | _ -> []

let write_initial_node initial code' new_order =
  code' := PTree.set initial (Inop (n2p ())) !code';
  new_order := initial :: !new_order

let write_pathmap initial esize pm' =
  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'

let rec write_tree exp initial current code' new_order fturn =
  (*Printf.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
  | inst :: k ->
      (*let open PrintRTL in*)
      (*print_instruction stderr (target_node, inst);*)
      code' := PTree.set (P.of_int target_node) inst !code';
      new_order := P.of_int target_node :: !new_order;
      write_tree k initial next_node code' new_order false
  | [] -> ()

let expanse (sb : superblock) code pm =
  (*debug_flag := true;*)
  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 map_consts = Hashtbl.create 100 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";
           let tmp_reg = get_tmp_reg c in
           exp := cond_int32s false c a1 a2 dest tmp_reg succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
           debug "Iop/Ccompu\n";
           let tmp_reg = get_tmp_reg c in
           exp := cond_int32u false c a1 a2 dest tmp_reg succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompimm\n";
           exp := expanse_condimm_int32s c a1 imm dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompuimm\n";
           exp := expanse_condimm_int32u c a1 imm dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
           debug "Iop/Ccompl\n";
           let tmp_reg = get_tmp_reg c in
           exp := cond_int64s false c a1 a2 dest tmp_reg succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
           debug "Iop/Ccomplu\n";
           let tmp_reg = get_tmp_reg c in
           exp := cond_int64u false c a1 a2 dest tmp_reg succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccomplimm\n";
           exp := expanse_condimm_int64s c a1 imm dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
           debug "Iop/Ccompluimm\n";
           exp := expanse_condimm_int64u c a1 imm dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
           debug "Iop/Ccompf\n";
           exp := expanse_cond_fp false cond_float c f1 f2 dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
           debug "Iop/Cnotcompf\n";
           exp := expanse_cond_fp true cond_float c f1 f2 dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
           debug "Iop/Ccompfs\n";
           exp := expanse_cond_fp false cond_single c f1 f2 dest succ map_consts;
           was_exp := true
       | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
           debug "Iop/Cnotcompfs\n";
           exp := expanse_cond_fp true cond_single c f1 f2 dest succ map_consts;
           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 c a1 imm info succ1 succ2 [] map_consts;
           was_branch := true;
           was_exp := true
       | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompuimm\n";
           exp :=
             expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [] map_consts;
           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 c a1 imm info succ1 succ2 [] map_consts;
           was_branch := true;
           was_exp := true
       | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompluimm\n";
           exp :=
             expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [] map_consts;
           was_branch := true;
           was_exp := true
       | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompf\n";
           exp :=
             expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2
               map_consts;
           was_branch := true;
           was_exp := true
       | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
           debug "Icond/Cnotcompf\n";
           exp :=
             expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2
               map_consts;
           was_branch := true;
           was_exp := true
       | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompfs\n";
           exp :=
             expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2
               map_consts;
           was_branch := true;
           was_exp := true
       | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
           debug "Icond/Cnotcompfs\n";
           exp :=
             expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2
               map_consts;
           was_branch := true;
           was_exp := true
       | _ -> ());
      (if !Clflags.option_fexpanse_others && not !was_exp then
       match inst with
       (* Expansion of fp constants *)
       | Iop (Ofloatconst f, nil, dest, succ) ->
           debug "Iop/Ofloatconst\n";
           let r = r2pi () in
           let ht =
             loadimm64 r (Floats.Float.to_bits f) (n2pi ()) map_consts true
           in
           let r' = unzip_head_tuple ht r in
           exp :=
             build_full_ilist Ofloat_of_bits [ r' ] dest succ (fst ht) []
               map_consts;
           was_exp := true
       | Iop (Osingleconst f, nil, dest, succ) ->
           debug "Iop/Osingleconst\n";
           let r = r2pi () in
           let ht =
             loadimm32 r (Floats.Float32.to_bits f) (n2pi ()) map_consts true
           in
           let r' = unzip_head_tuple ht r in
           exp :=
             build_full_ilist Osingle_of_bits [ r' ] dest succ (fst ht) []
               map_consts;
           was_exp := true
       | Iop (Ointconst n, nil, dest, succ) ->
           debug "Iop/Ointconst\n";
           let ht = loadimm32 dest n succ map_consts false in
           exp := unzip_head_tuple_move ht dest succ;
           was_exp := true
       | Iop (Olongconst n, nil, dest, succ) ->
           debug "Iop/Olongconst\n";
           let ht = loadimm64 dest n succ map_consts false in
           exp := unzip_head_tuple_move ht dest succ;
           was_exp := true
       | Iop (Oaddimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oaddimm\n";
           exp := addimm32 a1 dest n succ [] map_consts;
           was_exp := true
       | Iop (Oaddlimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oaddlimm\n";
           exp := addimm64 a1 dest n succ [] map_consts;
           was_exp := true
       | Iop (Oandimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oandimm\n";
           exp := andimm32 a1 dest n succ [] map_consts;
           was_exp := true
       | Iop (Oandlimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oandlimm\n";
           exp := andimm64 a1 dest n succ [] map_consts;
           was_exp := true
       | Iop (Oorimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oorimm\n";
           exp := orimm32 a1 dest n succ [] map_consts;
           was_exp := true
       | Iop (Oorlimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oorlimm\n";
           exp := orimm64 a1 dest n succ [] map_consts;
           was_exp := true
       | Iop (Ocast8signed, a1 :: nil, dest, succ) ->
           debug "Iop/cast8signed";
           let op = Oshlimm (Int.repr (Z.of_sint 24)) in
           let r = r2pi () in
           let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in
           let ht = build_head_tuple [] sv in
           let r' = unzip_head_tuple ht r in
           exp :=
             build_full_ilist
               (Oshrimm (Int.repr (Z.of_sint 24)))
               [ r' ] dest succ (fst ht) [] map_consts;
           was_exp := true
       | Iop (Ocast16signed, a1 :: nil, dest, succ) ->
           debug "Iop/cast8signed";
           let op = Oshlimm (Int.repr (Z.of_sint 16)) in
           let r = r2pi () in
           let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in
           let ht = build_head_tuple [] sv in
           let r' = unzip_head_tuple ht r in
           exp :=
             build_full_ilist
               (Oshrimm (Int.repr (Z.of_sint 16)))
               [ r' ] dest succ (fst ht) [] map_consts;
           was_exp := true
       | Iop (Ocast32unsigned, a1 :: nil, dest, succ) ->
           debug "Iop/Ocast32unsigned";
           let n2 = n2pi () in
           let n1 = n2pi () in
           let r1 = r2pi () in
           let r2 = r2pi () in
           let op1 = Ocast32signed in
           let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
           let ht1 = build_head_tuple [] sv1 in
           let r1' = unzip_head_tuple ht1 r1 in

           let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in
           let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in
           let ht2 = build_head_tuple (fst ht1) sv2 in
           let r2' = unzip_head_tuple ht2 r2 in

           let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in
           exp := build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts
       | Iop (Oshrximm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oshrximm";
           if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ]
           else if Int.eq n Int.one then
             let n2 = n2pi () in
             let n1 = n2pi () in
             let r1 = r2pi () in
             let r2 = r2pi () in
             let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
             let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
             let ht1 = build_head_tuple [] sv1 in
             let r1' = unzip_head_tuple ht1 r1 in

             let op2 = Oadd in
             let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in
             let ht2 = build_head_tuple (fst ht1) sv2 in
             let r2' = unzip_head_tuple ht2 r2 in

             let op3 = Oshrimm Int.one in
             exp :=
               build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts
           else
             let n3 = n2pi () in
             let n2 = n2pi () in
             let n1 = n2pi () in
             let r1 = r2pi () in
             let r2 = r2pi () in
             let r3 = r2pi () in
             let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in
             let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
             let ht1 = build_head_tuple [] sv1 in
             let r1' = unzip_head_tuple ht1 r1 in

             let op2 = Oshruimm (Int.sub Int.iwordsize n) in
             let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in
             let ht2 = build_head_tuple (fst ht1) sv2 in
             let r2' = unzip_head_tuple ht2 r2 in

             let op3 = Oadd in
             let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in
             let ht3 = build_head_tuple (fst ht2) sv3 in
             let r3' = unzip_head_tuple ht3 r3 in

             let op4 = Oshrimm n in
             exp :=
               build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts
       | Iop (Oshrxlimm n, a1 :: nil, dest, succ) ->
           debug "Iop/Oshrxlimm";
           if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ]
           else if Int.eq n Int.one then
             let n2 = n2pi () in
             let n1 = n2pi () in
             let r1 = r2pi () in
             let r2 = r2pi () in
             let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
             let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
             let ht1 = build_head_tuple [] sv1 in
             let r1' = unzip_head_tuple ht1 r1 in

             let op2 = Oaddl in
             let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in
             let ht2 = build_head_tuple (fst ht1) sv2 in
             let r2' = unzip_head_tuple ht2 r2 in

             let op3 = Oshrlimm Int.one in
             exp :=
               build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts
           else
             let n3 = n2pi () in
             let n2 = n2pi () in
             let n1 = n2pi () in
             let r1 = r2pi () in
             let r2 = r2pi () in
             let r3 = r2pi () in
             let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in
             let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
             let ht1 = build_head_tuple [] sv1 in
             let r1' = unzip_head_tuple ht1 r1 in

             let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in
             let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in
             let ht2 = build_head_tuple (fst ht1) sv2 in
             let r2' = unzip_head_tuple ht2 r2 in

             let op3 = Oaddl in
             let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in
             let ht3 = build_head_tuple (fst ht2) sv3 in
             let r3' = unzip_head_tuple ht3 r3 in

             let op4 = Oshrlimm n in
             exp :=
               build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts
       | _ -> ());
      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 = 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 !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;
  (*debug_flag := false;*)
  (!code', !pm')

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