(* *************************************************************)
(*                                                             *)
(*             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 BTL
open Op
open! Integers
open Camlcoq
open DebugPrint
open RTLcommonaux
open BTLcommonaux
open AST
open Datatypes
open Maps
open Asmgen

(** Tools *)

let rec iblock_to_list ib =
  match ib with
  | Bseq (ib1, ib2) -> iblock_to_list ib1 @ iblock_to_list ib2
  | _ -> [ ib ]

let rec list_to_iblock lib =
  match lib with
  | i1 :: k -> if List.length lib > 1 then Bseq (i1, list_to_iblock k) else i1
  | [] -> failwith "list_to_iblock: called on empty list"

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

(** Managing virtual registers and node index *)

let reg = ref 1

let r2p () = P.of_int !reg

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

(** 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
    - (Sr r) is inserted if the value was found in register r
    - (Sexp dest rhs args iinfo) represent an instruction
    - (Scond cond args ib1 ib2 iinfo) represents a condition
*)

type expl =
  | Sr of P.t
  | Sexp of P.t * rhs * P.t list * inst_info
  | Scond of condition * P.t list * iblock * iblock * inst_info

(** Record used during the "dynamic" value numbering *)

type numb = {
  mutable nnext : int;  (** Next unusued value number *)
  mutable seqs : seq list;  (** equations *)
  mutable nreg : (P.t, int) Hashtbl.t;  (** mapping registers to values *)
  mutable nval : (int, P.t list) Hashtbl.t;
      (** reverse mapping values to registers containing it *)
}

let print_list_pos l =
  debug "[";
  List.iter (fun i -> debug "%d;" (p2i i)) l;
  debug "]\n"

let empty_numbering () =
  { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 }

let rec get_nvalues vn = function
  | [] -> []
  | r :: rs ->
      let v =
        match Hashtbl.find_opt !vn.nreg r with
        | Some v ->
            debug "getnval r=%d |-> v=%d\n" (p2i r) v;
            v
        | None ->
            let n = !vn.nnext in
            debug "getnval r=%d |-> v=%d\n" (p2i r) n;
            !vn.nnext <- !vn.nnext + 1;
            Hashtbl.replace !vn.nreg r n;
            Hashtbl.replace !vn.nval n [ r ];
            n
      in
      let vs = get_nvalues vn rs in
      v :: vs

let get_nval_ornil vn v =
  match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l

let forget_reg vn rd =
  match Hashtbl.find_opt !vn.nreg rd with
  | Some v ->
      debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
      let old_regs = get_nval_ornil vn v in
      debug "forget_reg: old_regs are:\n";
      print_list_pos old_regs;
      Hashtbl.replace !vn.nval v
        (List.filter (fun n -> not (P.eq n rd)) old_regs)
  | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd)

let update_reg vn rd v =
  debug "update_reg: update v=%d with r=%d\n" v (p2i rd);
  forget_reg vn rd;
  let old_regs = get_nval_ornil vn v in
  Hashtbl.replace !vn.nval v (rd :: old_regs)

let rec find_valnum_rhs rh = function
  | [] -> None
  | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl

let set_unknown vn rd =
  debug "set_unknown: rd=%d\n" (p2i rd);
  forget_reg vn rd;
  Hashtbl.remove !vn.nreg rd

let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> ()

let addrhs vn rd rh =
  match find_valnum_rhs rh !vn.seqs with
  | Some vres ->
      debug "addrhs: Some v=%d\n" vres;
      Hashtbl.replace !vn.nreg rd vres;
      update_reg vn rd vres
  | None ->
      let n = !vn.nnext in
      debug "addrhs: None v=%d\n" n;
      !vn.nnext <- !vn.nnext + 1;
      !vn.seqs <- Seq (n, rh) :: !vn.seqs;
      update_reg vn rd n;
      Hashtbl.replace !vn.nreg rd n

let addsop vn v op rd =
  debug "addsop\n";
  if op = Omove then (
    update_reg vn rd (List.hd v);
    Hashtbl.replace !vn.nreg rd (List.hd v))
  else addrhs vn rd (Sop (op, v))

let rec kill_mem_operations = function
  | (Seq (v, Sop (op, vl)) as eq) :: tl ->
      if op_depends_on_memory op then kill_mem_operations tl
      else eq :: kill_mem_operations tl
  | [] -> []
  | eq :: tl -> eq :: kill_mem_operations tl

let reg_valnum vn v =
  debug "reg_valnum: trying to find a mapping for v=%d\n" v;
  match Hashtbl.find !vn.nval v with
  | [] -> None
  | r :: rs ->
      debug "reg_valnum: found a mapping r=%d\n" (p2i r);
      Some r

let rec reg_valnums vn = function
  | [] -> Some []
  | v :: vs -> (
      match (reg_valnum vn v, reg_valnums vn vs) with
      | Some r, Some rs -> Some (r :: rs)
      | _, _ -> None)

let find_rhs vn rh =
  match find_valnum_rhs rh !vn.seqs with
  | None -> None
  | Some vres -> reg_valnum vn vres

(** Functions to perform the dynamic reduction during CSE *)

let extract_arg l =
  if List.length l > 0 then
    match List.hd l with
    | Sr r -> (r, List.tl l)
    | Sexp (rd, _, _, _) -> (rd, l)
    | _ -> failwith "extract_arg: final instruction arg can not be extracted"
  else failwith "extract_arg: trying to extract on an empty list"

let extract_final vn fl fdest =
  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 ], def_iinfo ()) :: List.tl fl)
        else List.tl fl
    | _ -> fl
  else failwith "extract_final: trying to extract on an empty list"

let addinst vn op args rd =
  let v = get_nvalues vn args in
  let rh = Sop (op, v) in
  match find_rhs vn rh with
  | Some r ->
      debug "addinst: rhs found with r=%d\n" (p2i r);
      Sr r
  | None ->
      addsop vn v op rd;
      Sexp (rd, rh, args, def_iinfo ())

(** 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 iinfo succ1 succ2 k =
  let optR = make_optR is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Scond (CEbeqw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
  | Cne -> Scond (CEbnew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
  | Clt -> Scond (CEbltw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
  | Cle -> Scond (CEbgew optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
  | Cgt -> Scond (CEbltw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
  | Cge -> Scond (CEbgew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k

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

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

let cbranch_int64u is_x0 cmp a1 a2 iinfo succ1 succ2 k =
  let optR = make_optR is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> Scond (CEbequl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
  | Cne -> Scond (CEbneul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
  | Clt -> Scond (CEbltul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
  | Cle -> Scond (CEbgeul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
  | Cgt -> Scond (CEbltul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
  | Cge -> Scond (CEbgeul optR, [ a1; a2 ], succ1, succ2, iinfo) :: 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 iinfo succ1 succ2 =
  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 iinfo 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' iinfo succ1 succ2 l'

let expanse_cbranchimm_int32u vn cmp a1 n iinfo succ1 succ2 =
  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 iinfo 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' iinfo succ1 succ2 l'

let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 =
  if Int64.eq n Int64.zero then
    cbranch_int64s true cmp a1 a1 iinfo 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' iinfo succ1 succ2 l'

let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 =
  if Int64.eq n Int64.zero then
    cbranch_int64u true cmp a1 a1 iinfo 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' iinfo 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 iinfo 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
    Scond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l
  else Scond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l

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

let rec gen_btl_list vn exp =
  match exp with
  | Sr r :: _ ->
      failwith "write_tree: there are still some symbolic values in the list"
  | Sexp (rd, Sop (op, vals), args, iinfo) :: k ->
      let args = get_arguments vn vals args in
      let inst = Bop (op, args, rd, iinfo) in
      inst :: gen_btl_list vn k
  | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ]
  | [ Scond (cond, args, succ1, succ2, iinfo) ] ->
      let ib = Bcond (cond, args, succ1, succ2, iinfo) in
      [ ib ]
  | [] -> []
  | _ -> failwith "write_tree: invalid list"

let expanse_list li =
  debug "#### New block for expansion oracle\n";
  let exp = ref [] in
  let was_branch = ref false in
  let was_exp = ref false in
  let vn = ref (empty_numbering ()) in
  let rec expanse_list_rec li =
    match li with
    | [] -> li
    | i :: li' ->
        was_branch := false;
        was_exp := false;
        (if !Clflags.option_fexpanse_rtlcond then
         match i with
         (* Expansion of conditions - Ocmp *)
         | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) ->
             debug "Bop/Ccomp\n";
             exp := cond_int32s vn false c a1 a2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, iinfo) ->
             debug "Bop/Ccompu\n";
             exp := cond_int32u vn false c a1 a2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, iinfo) ->
             debug "Bop/Ccompimm\n";
             exp := expanse_condimm_int32s vn c a1 imm dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, iinfo) ->
             debug "Bop/Ccompuimm\n";
             exp := expanse_condimm_int32u vn c a1 imm dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, iinfo) ->
             debug "Bop/Ccompl\n";
             exp := cond_int64s vn false c a1 a2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, iinfo) ->
             debug "Bop/Ccomplu\n";
             exp := cond_int64u vn false c a1 a2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, iinfo) ->
             debug "Bop/Ccomplimm\n";
             exp := expanse_condimm_int64s vn c a1 imm dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, iinfo) ->
             debug "Bop/Ccompluimm\n";
             exp := expanse_condimm_int64u vn c a1 imm dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, iinfo) ->
             debug "Bop/Ccompf\n";
             exp := expanse_cond_fp vn false cond_float c f1 f2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, iinfo) ->
             debug "Bop/Cnotcompf\n";
             exp := expanse_cond_fp vn true cond_float c f1 f2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, iinfo) ->
             debug "Bop/Ccompfs\n";
             exp := expanse_cond_fp vn false cond_single c f1 f2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, iinfo) ->
             debug "Bop/Cnotcompfs\n";
             exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
             exp := extract_final vn !exp dest;
             was_exp := true
         (* Expansion of branches - Ccomp *)
         | Bcond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccomp\n";
             exp := cbranch_int32s false c a1 a2 iinfo succ1 succ2 [];
             was_branch := true;
             was_exp := true
         | Bcond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompu\n";
             exp := cbranch_int32u false c a1 a2 iinfo succ1 succ2 [];
             was_branch := true;
             was_exp := true
         | Bcond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompimm\n";
             exp := expanse_cbranchimm_int32s vn c a1 imm iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompuimm\n";
             exp := expanse_cbranchimm_int32u vn c a1 imm iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompl\n";
             exp := cbranch_int64s false c a1 a2 iinfo succ1 succ2 [];
             was_branch := true;
             was_exp := true
         | Bcond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccomplu\n";
             exp := cbranch_int64u false c a1 a2 iinfo succ1 succ2 [];
             was_branch := true;
             was_exp := true
         | Bcond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccomplimm\n";
             exp := expanse_cbranchimm_int64s vn c a1 imm iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompluimm\n";
             exp := expanse_cbranchimm_int64u vn c a1 imm iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompf\n";
             exp :=
               expanse_cbranch_fp vn false cond_float c f1 f2 iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Cnotcompf\n";
             exp :=
               expanse_cbranch_fp vn true cond_float c f1 f2 iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Ccompfs\n";
             exp :=
               expanse_cbranch_fp vn false cond_single c f1 f2 iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | Bcond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
             debug "Bcond/Cnotcompfs\n";
             exp :=
               expanse_cbranch_fp vn true cond_single c f1 f2 iinfo succ1 succ2;
             was_branch := true;
             was_exp := true
         | _ -> ());
        (if !Clflags.option_fexpanse_others && not !was_exp then
         match i with
         (* Others expansions *)
         | Bop (Ofloatconst f, nil, dest, iinfo) -> (
             match make_immed64 (Floats.Float.to_bits f) with
             | Imm64_single _ | Imm64_large _ -> ()
             | Imm64_pair (hi, lo) ->
                 debug "Bop/Ofloatconst\n";
                 let r = r2pi () in
                 let l = load_hilo64 vn r hi lo in
                 let r', l' = extract_arg l in
                 exp := addinst vn Ofloat_of_bits [ r' ] dest :: l';
                 exp := extract_final vn !exp dest;
                 was_exp := true)
         | Bop (Osingleconst f, nil, dest, iinfo) -> (
             match make_immed32 (Floats.Float32.to_bits f) with
             | Imm32_single imm -> ()
             | Imm32_pair (hi, lo) ->
                 debug "Bop/Osingleconst\n";
                 let r = r2pi () in
                 let l = load_hilo32 vn r hi lo in
                 let r', l' = extract_arg l in
                 exp := addinst vn Osingle_of_bits [ r' ] dest :: l';
                 exp := extract_final vn !exp dest;
                 was_exp := true)
         | Bop (Ointconst n, nil, dest, iinfo) ->
             debug "Bop/Ointconst\n";
             exp := loadimm32 vn dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Olongconst n, nil, dest, iinfo) ->
             debug "Bop/Olongconst\n";
             exp := loadimm64 vn dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oaddimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oaddimm\n";
             exp := addimm32 vn a1 dest n None;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oaddlimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oaddlimm\n";
             exp := addimm64 vn a1 dest n None;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oandimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oandimm\n";
             exp := andimm32 vn a1 dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oandlimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oandlimm\n";
             exp := andimm64 vn a1 dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oorimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oorimm\n";
             exp := orimm32 vn a1 dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oorlimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oorlimm\n";
             exp := orimm64 vn a1 dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oxorimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oxorimm\n";
             exp := xorimm32 vn a1 dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Oxorlimm n, a1 :: nil, dest, iinfo) ->
             debug "Bop/Oxorlimm\n";
             exp := xorimm64 vn a1 dest n;
             exp := extract_final vn !exp dest;
             was_exp := true
         | Bop (Ocast8signed, a1 :: nil, dest, iinfo) ->
             debug "Bop/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;
             was_exp := true
         | Bop (Ocast16signed, a1 :: nil, dest, iinfo) ->
             debug "Bop/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;
             was_exp := true
         | Bop (Ocast32unsigned, a1 :: nil, dest, iinfo) ->
             debug "Bop/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;
             was_exp := true
         | Bop (Oshrximm n, a1 :: nil, dest, iinfo) ->
             if Int.eq n Int.zero then (
               debug "Bop/Oshrximm1\n";
               exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
             else if Int.eq n Int.one then (
               debug "Bop/Oshrximm2\n";
               let r1 = r2pi () in
               let r2 = r2pi () in
               let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
               let i1 = addinst vn op1 [ a1 ] r1 in
               let r1', l1 = extract_arg [ i1 ] in

               let op2 = Oadd in
               let i2 = addinst vn op2 [ a1; r1' ] r2 in
               let r2', l2 = extract_arg (i2 :: l1) in

               let op3 = Oshrimm Int.one in
               let i3 = addinst vn op3 [ r2' ] dest in
               let r3, l3 = extract_arg (i3 :: l2) in
               exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3)
             else (
               debug "Bop/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;
             was_exp := true
         | Bop (Oshrxlimm n, a1 :: nil, dest, iinfo) ->
             if Int.eq n Int.zero then (
               debug "Bop/Oshrxlimm1\n";
               exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
             else if Int.eq n Int.one then (
               debug "Bop/Oshrxlimm2\n";
               let r1 = r2pi () in
               let r2 = r2pi () in
               let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
               let i1 = addinst vn op1 [ a1 ] r1 in
               let r1', l1 = extract_arg [ i1 ] in

               let op2 = Oaddl in
               let i2 = addinst vn op2 [ a1; r1' ] r2 in
               let r2', l2 = extract_arg (i2 :: l1) in

               let op3 = Oshrlimm Int.one in
               let i3 = addinst vn op3 [ r2' ] dest in
               let r3, l3 = extract_arg (i3 :: l2) in
               exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3)
             else (
               debug "Bop/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;
             was_exp := true
         | _ -> ());
        if not !was_exp then (
          (match i with
          | Bop (op, args, dest, iinfo) ->
              let v = get_nvalues vn args in
              addsop vn v op dest
          | Bload (_, _, _, _, dst, _) -> set_unknown vn dst
          | Bstore (_, _, _, _, _) ->
              !vn.seqs <- kill_mem_operations !vn.seqs
              (* TODO gourdinl empty numb BF? vn := empty_numbering ()*)
          | _ -> ());
          i :: expanse_list_rec li')
        else
          let hd = gen_btl_list vn (List.rev !exp) in
          hd @ expanse_list_rec li'
  in
  expanse_list_rec li

let expanse n ibf btl =
  (*debug_flag := true;*)
  let lib = iblock_to_list ibf.entry in
  let new_lib = expanse_list lib in
  let ibf' =
    {
      entry = list_to_iblock new_lib;
      input_regs = ibf.input_regs;
      binfo = ibf.binfo;
    }
  in
  (*debug_flag := false;*)
  PTree.set n ibf' btl

(** Form a list containing both sources and destination regs of a block *)
let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]

let rec get_regs_ib = function
  | Bnop _ -> []
  | Bop (_, args, dest, _) -> dest :: args
  | Bload (_, _, _, args, dest, _) -> dest :: args
  | Bstore (_, _, args, src, _) -> src :: args
  | Bcond (_, args, ib1, ib2, _) -> get_regs_ib ib1 @ get_regs_ib ib2 @ args
  | Bseq (ib1, ib2) -> get_regs_ib ib1 @ get_regs_ib ib2
  | BF (Breturn (Some r), _) -> [ r ]
  | BF (Bcall (_, t, args, dest, _), _) -> dest :: (get_regindent t @ args)
  | BF (Btailcall (_, t, args), _) -> get_regindent t @ args
  | BF (Bbuiltin (_, args, dest, _), _) ->
      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
  | BF (Bjumptable (arg, _), _) -> [ arg ]
  | _ -> []

let rec find_last_reg = function
  | [] -> ()
  | (pc, ibf) :: 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 reg (get_regs_ib ibf.entry);
      find_last_reg k