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

let reg = ref 1

let node = ref 1

let r2p () = Camlcoq.P.of_int !reg

let n2p () = Camlcoq.P.of_int !node

let r2pi () =
  reg := !reg + 1;
  r2p ()

let n2pi () =
  node := !node + 1;
  n2p ()

type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul

let load_hilo32 a1 dest hi lo succ is_long k =
  if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k
  else
    let r = r2pi () in
    Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ())
    :: Iop (Oaddimm lo, [ r ], dest, succ) :: k

let load_hilo64 a1 dest hi lo succ k =
  if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k
  else
    let r = r2pi () in
    Iop (OEluil hi, [ a1 ], r, n2pi ())
    :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k

let loadimm32 a1 dest n succ is_long k =
  match make_immed32 n with
  | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k
  | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k

let loadimm64 a1 dest n succ k =
  match make_immed64 n with
  | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k
  | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k
  | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k

let get_opimm imm = function
  | Xoriw -> OExoriw imm
  | Sltiw -> OEsltiw imm
  | Sltiuw -> OEsltiuw imm
  | Xoril -> OExoril imm
  | Sltil -> OEsltil imm
  | Sltiul -> OEsltiul imm

let opimm32 a1 dest n succ is_long k op opimm =
  match make_immed32 n with
  | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
  | Imm32_pair (hi, lo) ->
      let r = r2pi () in
      load_hilo32 a1 r hi lo (n2pi ()) is_long
        (Iop (op, [ a1; r ], dest, succ) :: k)

let opimm64 a1 dest n succ k op opimm =
  match make_immed64 n with
  | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
  | Imm64_pair (hi, lo) ->
      let r = r2pi () in
      load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k)
  | Imm64_large imm ->
      let r = r2pi () in
      Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k

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

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

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

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 succ k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k
  | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k
  | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k
  | Cle ->
      let r = r2pi () in
      Iop (OEsltw optR0, [ a2; a1 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
  | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k
  | Cge ->
      let r = r2pi () in
      Iop (OEsltw optR0, [ a1; a2 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

let cond_int32u is_x0 cmp a1 a2 dest succ k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k
  | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k
  | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k
  | Cle ->
      let r = r2pi () in
      Iop (OEsltuw optR0, [ a2; a1 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
  | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k
  | Cge ->
      let r = r2pi () in
      Iop (OEsltuw optR0, [ a1; a2 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

let cond_int64s is_x0 cmp a1 a2 dest succ k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k
  | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k
  | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k
  | Cle ->
      let r = r2pi () in
      Iop (OEsltl optR0, [ a2; a1 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
  | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k
  | Cge ->
      let r = r2pi () in
      Iop (OEsltl optR0, [ a1; a2 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

let cond_int64u is_x0 cmp a1 a2 dest succ k =
  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k
  | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k
  | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k
  | Cle ->
      let r = r2pi () in
      Iop (OEsltul optR0, [ a2; a1 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
  | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k
  | Cge ->
      let r = r2pi () in
      Iop (OEsltul optR0, [ a1; a2 ], r, n2pi ())
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

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

let cond_float cmp f1 f2 dest succ =
  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 =
  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 =
  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
  else
    let r = r2pi () in
    loadimm32 a1 r n (n2pi ()) false
      (cbranch_int32s false cmp a1 r info succ1 succ2 k)

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

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

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

let expanse_condimm_int32s cmp a1 n dest succ k =
  if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
  else
    match cmp with
    | Ceq | Cne ->
        let r = r2pi () in
        xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k)
    | Clt -> sltimm32 a1 dest n succ false k
    | Cle ->
        if Int.eq n (Int.repr Int.max_signed) then
          loadimm32 a1 dest Int.one succ false k
        else sltimm32 a1 dest (Int.add n Int.one) succ false k
    | _ ->
        let r = r2pi () in
        loadimm32 a1 r n (n2pi ()) false
          (cond_int32s false cmp a1 r dest succ k)

let expanse_condimm_int32u cmp a1 n dest succ k =
  if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
  else
    match cmp with
    | Clt -> sltuimm32 a1 dest n succ false k
    | _ ->
        let r = r2pi () in
        loadimm32 a1 r n (n2pi ()) false
          (cond_int32u false cmp a1 r dest succ k)

let expanse_condimm_int64s cmp a1 n dest succ k =
  if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
  else
    match cmp with
    | Ceq | Cne ->
        let r = r2pi () in
        xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k)
    | Clt -> sltimm64 a1 dest n succ k
    | Cle ->
        if Int64.eq n (Int64.repr Int64.max_signed) then
          loadimm32 a1 dest Int.one succ true k
        else sltimm64 a1 dest (Int64.add n Int64.one) succ k
    | _ ->
        let r = r2pi () in
        loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k)

let expanse_condimm_int64u cmp a1 n dest succ k =
  if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
  else
    match cmp with
    | Clt -> sltuimm64 a1 dest n succ k
    | _ ->
        let r = r2pi () in
        loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k)

let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
  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' in
  insn
  :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)

let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
  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 cmp f1 f2 r (n2pi ()) in
  insn
  ::
  (if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info)
  else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info))
  :: k

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 current code' new_order =
  match exp with
  | (Iop (_, _, _, succ) as inst) :: k ->
      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
      new_order := Camlcoq.P.of_int current :: !new_order;
      write_tree k (current - 1) code' new_order
  | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
      new_order := Camlcoq.P.of_int current :: !new_order;
      write_tree k (current - 1) code' new_order
  | [] -> ()
  | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."

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
  Array.iter
    (fun n ->
      was_branch := false;
      was_exp := false;
      let inst = get_some @@ PTree.get n code in
      (match inst with
      (* Expansion of conditions - Ocmp *)
      | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
          debug "Iop/Ccomp\n";
          exp := cond_int32s false c a1 a2 dest succ [];
          was_exp := true
      | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
          debug "Iop/Ccompu\n";
          exp := cond_int32u false c a1 a2 dest succ [];
          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 [];
          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 [];
          was_exp := true
      | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
          debug "Iop/Ccompl\n";
          exp := cond_int64s false c a1 a2 dest succ [];
          was_exp := true
      | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
          debug "Iop/Ccomplu\n";
          exp := cond_int64u false c a1 a2 dest succ [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          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 [];
          was_branch := true;
          was_exp := true
      (* Expansion of fp constants *)
      | Iop (Ofloatconst f, nil, dest, succ) ->
          debug "Iop/Ofloatconst\n";
          let r = r2pi () in
          exp :=
            [
              Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ());
              Iop (Ofloat_of_bits, [ r ], dest, succ);
            ];
          was_exp := true
      | Iop (Osingleconst f, nil, dest, succ) ->
          debug "Iop/Osingleconst\n";
          let r = r2pi () in
          exp :=
            [
              Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ());
              Iop (Osingle_of_bits, [ r ], dest, succ);
            ];
          was_exp := true
      | _ -> new_order := n :: !new_order);
      if !was_exp then (
        node := !node + 1;
        (if !was_branch then
         let lives = PTree.get n !liveins in
         match lives with
         | Some lives ->
             let new_branch_pc =
               Camlcoq.P.of_int (!node - (List.length !exp - 1))
             in
             liveins := PTree.set new_branch_pc lives !liveins;
             liveins := PTree.remove n !liveins
         | _ -> ());
        write_pathmap sb.instructions.(0) (List.length !exp) pm';
        write_initial_node n code' new_order;
        write_tree !exp !node code' 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' = Camlcoq.P.to_int 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