(* *************************************************************)
(*                                                             *)
(*             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 = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul

let find_or_addnmove op args rd succ map_consts =
  let sop = Sop (op, args) in
  match Hashtbl.find_opt map_consts sop with
  | Some r -> Sr (P.of_int r)
  | None ->
      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 load_hilo32 dest hi lo succ map_consts =
  let op1 = OEluiw hi in
  if Int.eq lo Int.zero then
    let sv = find_or_addnmove op1 [] dest succ map_consts in
    build_head_tuple [] sv
  else
    let r = r2pi () in
    let op2 = Oaddimm lo in
    match find_or_addnmove op1 [] r (n2pi ()) map_consts with
    | Si i ->
        let sv = find_or_addnmove op2 [ r ] dest succ map_consts in
        build_head_tuple [ i ] sv
    | Sr r' ->
        let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in
        build_head_tuple [] sv

let load_hilo64 dest hi lo succ map_consts =
  let op1 = OEluil hi in
  if Int64.eq lo Int64.zero then
    let sv = find_or_addnmove op1 [] dest succ map_consts in
    build_head_tuple [] sv
  else
    let r = r2pi () in
    let op2 = Oaddlimm lo in
    match find_or_addnmove op1 [] r (n2pi ()) map_consts with
    | Si i ->
        let sv = find_or_addnmove op2 [ r ] dest succ map_consts in
        build_head_tuple [ i ] sv
    | Sr r' ->
        let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in
        build_head_tuple [] sv

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

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

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

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

let opimm32 a1 dest n succ k op opimm map_consts =
  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
      let ht = load_hilo32 r hi lo (n2pi ()) map_consts in
      let r' = unzip_head_tuple ht r in
      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k

let opimm64 a1 dest n succ k op opimm map_consts =
  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
      let ht = load_hilo64 r hi lo (n2pi ()) map_consts in
      let r' = unzip_head_tuple ht r in
      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
  | 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 in
      let ht = build_head_tuple [] sv in
      let r' = unzip_head_tuple ht r in
      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k

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 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 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, get tmp_reg)
      :: 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, get tmp_reg)
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

let cond_int32u is_x0 cmp a1 a2 dest tmp_reg 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, get tmp_reg)
      :: 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, get tmp_reg)
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

let cond_int64s is_x0 cmp a1 a2 dest tmp_reg 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, get tmp_reg)
      :: 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, get tmp_reg)
      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k

let cond_int64u is_x0 cmp a1 a2 dest tmp_reg 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, get tmp_reg)
      :: 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, get tmp_reg)
      :: 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 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 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 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 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 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 k 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 k
  else
    match cmp with
    | Ceq | Cne ->
        let r = r2pi () in
        xorimm32 a1 r n (n2pi ())
          (cond_int32s true cmp r r dest None succ k)
          map_consts
    | Clt -> sltimm32 a1 dest n succ k map_consts
    | Cle ->
        if Int.eq n (Int.repr Int.max_signed) then
          let ht = loadimm32 dest Int.one succ map_consts in
          fst ht @ k
        else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts
    | _ ->
        let r = r2pi () in
        let tmp_reg = get_tmp_reg cmp in
        let ht = loadimm32 r n (n2pi ()) map_consts in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ k

let expanse_condimm_int32u cmp a1 n dest succ k 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 k
  else
    match cmp with
    | Clt -> sltuimm32 a1 dest n succ k map_consts
    | _ ->
        let r = r2pi () in
        let ht = loadimm32 r n (n2pi ()) map_consts in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ k

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

let expanse_condimm_int64u cmp a1 n dest succ k 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 k
  else
    match cmp with
    | Clt -> sltuimm64 a1 dest n succ k map_consts
    | _ ->
        let r = r2pi () in
        let ht = loadimm64 r n (n2pi ()) map_consts in
        let r' = unzip_head_tuple ht r in
        fst ht @ cond_int64u false cmp a1 r' dest tmp_reg 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 initial current code' new_order =
  let target_node, next_node =
    if current = !node then (
      node := !node + 1;
      (P.to_int initial, current))
    else (current, current - 1)
  in
  match exp with
  | (Iop (_, _, _, succ) as inst) :: k ->
      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
  | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
      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
  | [] -> ()
  | _ -> 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
  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 [];
           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 [];
           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 [];
           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 [];
           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 [];
           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 [] 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 [];
           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
       | _ -> ());
      (if !Clflags.option_fexpanse_fpconst && 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
           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
       | _ -> ());
      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)
      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