[MERGE] BTL into kvx-work (replacing RTLpath)

5 files changed, 2388 insertions, 1029 deletions

diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v
new file mode 100644
index 00000000..ab01f7ac
--- /dev/null
+++ b/riscV/BTL_SEsimplify.v
@@ -0,0 +1,1923 @@
+Require Import Coqlib Floats Values Memory.
+Require Import Integers.
+Require Import Op Registers.
+Require Import BTL_SEtheory.
+Require Import BTL_SEsimuref.
+Require Import Asmgen Asmgenproof1.
+
+(** Useful functions for conditions/branches expansion *)
+
+Definition is_inv_cmp_int (cmp: comparison) : bool :=
+  match cmp with | Cle | Cgt => true | _ => false end.
+
+Definition is_inv_cmp_float (cmp: comparison) : bool :=
+  match cmp with | Cge | Cgt => true | _ => false end.
+
+Definition make_optR (is_x0 is_inv: bool) : option oreg :=
+  if is_x0 then
+    (if is_inv then Some (X0_L)
+    else Some (X0_R))
+  else None.
+
+(** Functions to manage lists of "fake" values *)
+
+Definition make_lfsv_cmp (is_inv: bool) (fsv1 fsv2: sval) : list_sval :=
+  let (fsvfirst, fsvsec) := if is_inv then (fsv1, fsv2) else (fsv2, fsv1) in
+  let lfsv := fScons fsvfirst fSnil in
+  fScons fsvsec lfsv.
+
+Definition make_lfsv_single (fsv: sval) : list_sval :=
+  fScons fsv fSnil.
+
+(** * Expansion functions *)
+
+(** ** Immediate loads *)
+
+Definition load_hilo32 (hi lo: int) :=
+  if Int.eq lo Int.zero then
+    fSop (OEluiw hi) fSnil
+  else
+    let fsv := fSop (OEluiw hi) fSnil in
+    let lfsv := make_lfsv_single fsv in
+    fSop (OEaddiw None lo) lfsv.
+
+Definition load_hilo64 (hi lo: int64) :=
+  if Int64.eq lo Int64.zero then
+    fSop (OEluil hi) fSnil
+  else
+    let fsv := fSop (OEluil hi) fSnil in
+    let lfsv := make_lfsv_single fsv in
+    fSop (OEaddil None lo) lfsv.
+
+Definition loadimm32 (n: int) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      fSop (OEaddiw (Some X0_R) imm) fSnil
+  | Imm32_pair hi lo => load_hilo32 hi lo
+  end.
+
+Definition loadimm64 (n: int64) :=
+  match make_immed64 n with
+  | Imm64_single imm =>
+      fSop (OEaddil (Some X0_R) imm) fSnil
+  | Imm64_pair hi lo => load_hilo64 hi lo
+  | Imm64_large imm => fSop (OEloadli imm) fSnil
+  end.
+
+Definition opimm32 (fsv1: sval) (n: int) (op: operation) (opimm: int -> operation) :=
+  match make_immed32 n with
+  | Imm32_single imm =>
+      let lfsv := make_lfsv_single fsv1 in
+      fSop (opimm imm) lfsv
+  | Imm32_pair hi lo =>
+      let fsv := load_hilo32 hi lo in
+      let lfsv := make_lfsv_cmp false fsv1 fsv in
+      fSop op lfsv
+  end.
+
+Definition opimm64 (fsv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
+  match make_immed64 n with
+  | Imm64_single imm =>
+      let lfsv := make_lfsv_single fsv1 in
+      fSop (opimm imm) lfsv
+  | Imm64_pair hi lo =>
+      let fsv := load_hilo64 hi lo in
+      let lfsv := make_lfsv_cmp false fsv1 fsv in
+      fSop op lfsv
+  | Imm64_large imm =>
+      let fsv := fSop (OEloadli imm) fSnil in
+      let lfsv := make_lfsv_cmp false fsv1 fsv in
+      fSop op lfsv
+  end.
+
+Definition addimm32 (fsv1: sval) (n: int) (or: option oreg) := opimm32 fsv1 n Oadd (OEaddiw or).
+Definition andimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oand OEandiw.
+Definition orimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oor OEoriw.
+Definition xorimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oxor OExoriw.
+Definition sltimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltw None) OEsltiw.
+Definition sltuimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltuw None) OEsltiuw.
+Definition addimm64 (fsv1: sval) (n: int64) (or: option oreg) := opimm64 fsv1 n Oaddl (OEaddil or).
+Definition andimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oandl OEandil.
+Definition orimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oorl OEoril.
+Definition xorimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oxorl OExoril.
+Definition sltimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltl None) OEsltil.
+Definition sltuimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltul None) OEsltiul.
+(** ** Comparisons intructions *)
+
+Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEseqw optR) lsv
+  | Cne => fSop (OEsnew optR) lsv
+  | Clt | Cgt => fSop (OEsltw optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltw optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition cond_int32u (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEsequw optR) lsv
+  | Cne => fSop (OEsneuw optR) lsv
+  | Clt | Cgt => fSop (OEsltuw optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltuw optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition cond_int64s (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEseql optR) lsv
+  | Cne => fSop (OEsnel optR) lsv
+  | Clt | Cgt => fSop (OEsltl optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltl optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition cond_int64u (cmp: comparison) (lsv: list_sval) (optR: option oreg) :=
+  match cmp with
+  | Ceq => fSop (OEsequl optR) lsv
+  | Cne => fSop (OEsneul optR) lsv
+  | Clt | Cgt => fSop (OEsltul optR) lsv
+  | Cle | Cge =>
+      let fsv := (fSop (OEsltul optR) lsv) in
+      let lfsv := make_lfsv_single fsv in
+      fSop (OExoriw Int.one) lfsv
+  end.
+
+Definition expanse_condimm_int32s (cmp: comparison) (fsv1: sval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int32s cmp lfsv optR
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR := make_optR true is_inv in
+        let fsv := xorimm32 fsv1 n in
+        let lfsv := make_lfsv_cmp false fsv fsv in
+        cond_int32s cmp lfsv optR
+    | Clt => sltimm32 fsv1 n
+    | Cle =>
+        if Int.eq n (Int.repr Int.max_signed) then
+          let fsv := loadimm32 Int.one in
+          let lfsv := make_lfsv_cmp false fsv1 fsv in
+          fSop (OEmayundef MUint) lfsv
+        else sltimm32 fsv1 (Int.add n Int.one)
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int32s cmp lfsv optR
+    end.
+
+Definition expanse_condimm_int32u (cmp: comparison) (fsv1: sval) (n: int) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int.eq n Int.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int32u cmp lfsv optR
+  else
+    match cmp with
+    | Clt => sltuimm32 fsv1 n
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int32u cmp lfsv optR
+    end.
+
+Definition expanse_condimm_int64s (cmp: comparison) (fsv1: sval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int64s cmp lfsv optR
+  else
+    match cmp with
+    | Ceq | Cne =>
+        let optR := make_optR true is_inv in
+        let fsv := xorimm64 fsv1 n in
+        let lfsv := make_lfsv_cmp false fsv fsv in
+        cond_int64s cmp lfsv optR
+    | Clt => sltimm64 fsv1 n
+    | Cle =>
+        if Int64.eq n (Int64.repr Int64.max_signed) then
+          let fsv := loadimm32 Int.one in
+          let lfsv := make_lfsv_cmp false fsv1 fsv in
+          fSop (OEmayundef MUlong) lfsv
+        else sltimm64 fsv1 (Int64.add n Int64.one)
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int64s cmp lfsv optR
+    end.
+
+Definition expanse_condimm_int64u (cmp: comparison) (fsv1: sval) (n: int64) :=
+  let is_inv := is_inv_cmp_int cmp in
+  if Int64.eq n Int64.zero then
+    let optR := make_optR true is_inv in
+    let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+    cond_int64u cmp lfsv optR
+  else
+    match cmp with
+    | Clt => sltuimm64 fsv1 n
+    | _ =>
+        let optR := make_optR false is_inv in
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        cond_int64u cmp lfsv optR
+    end.
+
+Definition cond_float (cmp: comparison) (lsv: list_sval) :=
+  match cmp with
+  | Ceq | Cne => fSop OEfeqd lsv
+  | Clt | Cgt => fSop OEfltd lsv
+  | Cle | Cge => fSop OEfled lsv
+  end.
+
+Definition cond_single (cmp: comparison) (lsv: list_sval) :=
+  match cmp with
+  | Ceq | Cne => fSop OEfeqs lsv
+  | Clt | Cgt => fSop OEflts lsv
+  | Cle | Cge => fSop OEfles lsv
+  end.
+
+Definition is_normal_cmp cmp :=
+  match cmp with | Cne => false | _ => true end.
+
+Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  let fsv := fn_cond cmp lsv in
+  let lfsv := make_lfsv_single fsv in
+  if normal' then fsv else fSop (OExoriw Int.one) lfsv.
+
+(** ** Branches instructions *)
+
+Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbeqw optR
+  | Cne => CEbnew optR
+  | Clt => CEbltw optR
+  | Cle => CEbgew optR
+  | Cgt => CEbltw optR
+  | Cge => CEbgew optR
+  end.
+
+Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbequw optR
+  | Cne => CEbneuw optR
+  | Clt => CEbltuw optR
+  | Cle => CEbgeuw optR
+  | Cgt => CEbltuw optR
+  | Cge => CEbgeuw optR
+  end.
+
+Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbeql optR
+  | Cne => CEbnel optR
+  | Clt => CEbltl optR
+  | Cle => CEbgel optR
+  | Cgt => CEbltl optR
+  | Cge => CEbgel optR
+  end.
+
+Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbequl optR
+  | Cne => CEbneul optR
+  | Clt => CEbltul optR
+  | Cle => CEbgeul optR
+  | Cgt => CEbltul optR
+  | Cge => CEbgeul optR
+  end.
+
+Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lfsv: list_sval) : (condition * list_sval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  let fsv := fn_cond cmp lfsv in
+  let lfsv' := make_lfsv_cmp false fsv fsv in
+  if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), lfsv').
+
+(** Target op simplifications using "fake" values *)
+
+Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval :=
+  match op, lr with
+  | Ocmp (Ccomp c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int32s c lfsv optR)
+  | Ocmp (Ccompu c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int32u c lfsv optR)
+  | Ocmp (Ccompimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int32s c fsv1 imm)
+  | Ocmp (Ccompuimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int32u c fsv1 imm)
+  | Ocmp (Ccompl c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int64s c lfsv optR)
+  | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let fsv2 := ris_sreg_get hrs a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR := make_optR false is_inv in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond_int64u c lfsv optR)
+  | Ocmp (Ccomplimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int64s c fsv1 imm)
+  | Ocmp (Ccompluimm c imm), a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (expanse_condimm_int64u c fsv1 imm)
+  | Ocmp (Ccompf c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp false cond_float c lfsv)
+  | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp true cond_float c lfsv)
+  | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp false cond_single c lfsv)
+  | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
+      let fsv1 := ris_sreg_get hrs f1 in
+      let fsv2 := ris_sreg_get hrs f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cond_fp true cond_single c lfsv)
+  | Ofloatconst f, nil =>
+      let fsv := loadimm64 (Float.to_bits f) in
+      let lfsv := make_lfsv_single fsv in
+      Some (fSop (Ofloat_of_bits) lfsv)
+  | Osingleconst f, nil =>
+      let fsv := loadimm32 (Float32.to_bits f) in
+      let lfsv := make_lfsv_single fsv in
+      Some (fSop (Osingle_of_bits) lfsv)
+  | Ointconst n, nil =>
+      Some (loadimm32 n)
+  | Olongconst n, nil =>
+      Some (loadimm64 n)
+  | Oaddimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (addimm32 fsv1 n None)
+  | Oaddlimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (addimm64 fsv1 n None)
+  | Oandimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (andimm32 fsv1 n)
+  | Oandlimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (andimm64 fsv1 n)
+  | Oorimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (orimm32 fsv1 n)
+  | Oorlimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (orimm64 fsv1 n)
+  | Oxorimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (xorimm32 fsv1 n)
+  | Oxorlimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      Some (xorimm64 fsv1 n)
+  | Ocast8signed, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single fsv1 in
+      let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in
+      let hl' := make_lfsv_single fsv in
+      Some (fSop (Oshrimm (Int.repr 24)) hl')
+  | Ocast16signed, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single fsv1 in
+      let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in
+      let hl' := make_lfsv_single fsv in
+      Some (fSop (Oshrimm (Int.repr 16)) hl')
+  | Ocast32unsigned, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single fsv1 in
+      let cast32s_s := fSop Ocast32signed lfsv in
+      let cast32s_l := make_lfsv_single cast32s_s in
+      let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in
+      let sllil_l := make_lfsv_single sllil_s in
+      Some (fSop (Oshrluimm (Int.repr 32)) sllil_l)
+  | Oshrximm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single fsv1 in
+      if Int.eq n Int.zero then
+        let lhl := make_lfsv_cmp false fsv1 fsv1 in
+        Some (fSop (OEmayundef (MUshrx n)) lhl)
+      else
+        if Int.eq n Int.one then
+          let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in
+          let srliw_l := make_lfsv_cmp false fsv1 srliw_s in
+          let addw_s := fSop Oadd srliw_l in
+          let addw_l := make_lfsv_single addw_s in
+          let sraiw_s := fSop (Oshrimm Int.one) addw_l in
+          let sraiw_l := make_lfsv_cmp false sraiw_s sraiw_s in
+          Some (fSop (OEmayundef (MUshrx n)) sraiw_l)
+        else 
+          let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in
+          let sraiw_l := make_lfsv_single sraiw_s in
+          let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in
+          let srliw_l := make_lfsv_cmp false fsv1 srliw_s in
+          let addw_s := fSop Oadd srliw_l in
+          let addw_l := make_lfsv_single addw_s in
+          let sraiw_s' := fSop (Oshrimm n) addw_l in
+          let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in
+          Some (fSop (OEmayundef (MUshrx n)) sraiw_l')
+  | Oshrxlimm n, a1 :: nil =>
+      let fsv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single fsv1 in
+      if Int.eq n Int.zero then
+        let lhl := make_lfsv_cmp false fsv1 fsv1 in
+        Some (fSop (OEmayundef (MUshrxl n)) lhl)
+      else
+        if Int.eq n Int.one then
+          let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in
+          let srlil_l := make_lfsv_cmp false fsv1 srlil_s in
+          let addl_s := fSop Oaddl srlil_l in
+          let addl_l := make_lfsv_single addl_s in
+          let srail_s := fSop (Oshrlimm Int.one) addl_l in
+          let srail_l := make_lfsv_cmp false srail_s srail_s in
+          Some (fSop (OEmayundef (MUshrxl n)) srail_l)
+        else
+          let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in
+          let srail_l := make_lfsv_single srail_s in
+          let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in
+          let srlil_l := make_lfsv_cmp false fsv1 srlil_s in
+          let addl_s := fSop Oaddl srlil_l in
+          let addl_l := make_lfsv_single addl_s in
+          let srail_s' := fSop (Oshrlimm n) addl_l in
+          let srail_l' := make_lfsv_cmp false srail_s' srail_s' in
+          Some (fSop (OEmayundef (MUshrxl n)) srail_l')
+
+  | _, _ => None
+  end.
+
+Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
+  match cond, args with
+  | (Ccomp c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int32s c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccompu c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int32u c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccompimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int.eq n Int.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int32s c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int32s c (make_optR false is_inv) in
+        Some (cond, lfsv))
+  | (Ccompuimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int.eq n Int.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int32u c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int32u c (make_optR false is_inv) in
+         Some (cond, lfsv))
+  | (Ccompl c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int64s c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccomplu c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int64u c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccomplimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int64.eq n Int64.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int64s c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int64s c (make_optR false is_inv) in
+        Some (cond, lfsv))
+  | (Ccompluimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int64.eq n Int64.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int64u c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int64u c (make_optR false is_inv) in
+        Some (cond, lfsv))
+  | (Ccompf c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp false cond_float c lfsv)
+  | (Cnotcompf c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp true cond_float c lfsv)
+  | (Ccompfs c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp false cond_single c lfsv)
+  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp true cond_single c lfsv)
+  | _, _ => None
+   end.
+
+(** * Auxiliary lemmas on comparisons *)
+
+(** ** Signed ints *)
+
+Lemma xor_neg_ltle_cmp: forall v1 v2,
+  Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmp; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmp: core.
+
+(** ** Unsigned ints *)
+
+Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
+  Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  unfold Val.cmpu; simpl;
+  try rewrite Int.eq_sym;
+  try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl;
+  try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one;
+  auto.
+  1,2:
+    unfold Val.cmpu, Val.cmpu_bool;
+    destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _);
+    try destruct (eq_block _ _); auto.
+  unfold Val.cmpu, Val.cmpu_bool; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmpu: core.
+
+Remark ltu_12_wordsize:
+  Int.ltu (Int.repr 12) Int.iwordsize = true.
+Proof.
+  unfold Int.iwordsize, Int.zwordsize. simpl.
+  unfold Int.ltu. apply zlt_true.
+  rewrite !Int.unsigned_repr; try cbn; try lia.
+Qed.
+Local Hint Resolve ltu_12_wordsize: core.
+
+(** ** Signed longs *)
+
+Lemma xor_neg_ltle_cmpl: forall v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.lt _ _); auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmpl: core.
+
+Lemma xor_neg_ltge_cmpl: forall v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.lt _ _); auto.
+Qed.
+Local Hint Resolve xor_neg_ltge_cmpl: core.
+
+Lemma xorl_zero_eq_cmpl: forall c v1 v2,
+  c = Ceq \/ c = Cne ->
+  Some
+    (Val.maketotal
+     (option_map Val.of_bool
+       (Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) =
+  Some (Val.of_optbool (Val.cmpl_bool c v1 v2)).
+Proof.
+  intros. destruct c; inv H; try discriminate;
+  destruct v1, v2; simpl; auto;
+  destruct (Int64.eq i i0) eqn:EQ0.
+  1,3:
+    apply Int64.same_if_eq in EQ0; subst;
+    rewrite Int64.xor_idem;
+    rewrite Int64.eq_true; trivial.
+  1,2:
+    destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence;
+    rewrite Int64.xor_is_zero in EQ1; congruence.
+Qed.
+Local Hint Resolve xorl_zero_eq_cmpl: core.
+
+Lemma cmp_ltle_add_one: forall v n,
+  Int.eq n (Int.repr Int.max_signed) = false ->
+  Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
+Proof.
+  intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
+  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
+  destruct (zlt (Int.signed n) (Int.signed i)).
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  specialize (Int.eq_spec n (Int.repr Int.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); lia.
+Qed.
+Local Hint Resolve cmp_ltle_add_one: core.
+
+Lemma cmpl_ltle_add_one: forall v n,
+  Int64.eq n (Int64.repr Int64.max_signed) = false ->
+  Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) =
+  Some (Val.of_optbool (Val.cmpl_bool Cle v (Vlong n))).
+Proof.
+  intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto.
+  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
+  destruct (zlt (Int64.signed n) (Int64.signed i)).
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
+  specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int64.signed n <> Int64.max_signed).
+  { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
+  generalize (Int64.signed_range n); lia.
+Qed.
+Local Hint Resolve cmpl_ltle_add_one: core.
+
+Remark lt_maxsgn_false_int: forall i,
+  Int.lt (Int.repr Int.max_signed) i = false.
+Proof.
+  intros; unfold Int.lt.
+  specialize  Int.signed_range with i; intros.
+  rewrite zlt_false; auto. destruct H.
+  rewrite Int.signed_repr; try (cbn; lia).
+  apply Z.le_ge. trivial.
+Qed.
+Local Hint Resolve lt_maxsgn_false_int: core.
+
+Remark lt_maxsgn_false_long: forall i,
+  Int64.lt (Int64.repr Int64.max_signed) i = false.
+Proof.
+  intros; unfold Int64.lt.
+  specialize  Int64.signed_range with i; intros.
+  rewrite zlt_false; auto. destruct H.
+  rewrite Int64.signed_repr; try (cbn; lia).
+  apply Z.le_ge. trivial.
+Qed.
+Local Hint Resolve lt_maxsgn_false_long: core.
+
+(** ** Unsigned longs *)
+
+Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.ltu _ _); auto.
+  1,2: unfold Val.cmplu; simpl; auto;
+  destruct (Archi.ptr64); simpl;
+  try destruct (eq_block _ _); simpl;
+  try destruct (_ && _); simpl;
+  try destruct (Ptrofs.cmpu _ _);
+  try destruct cmp; simpl; auto.
+  unfold Val.cmplu; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_ltle_cmplu: core.
+
+Lemma xor_neg_ltge_cmplu: forall mptr v1 v2,
+  Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence.
+  destruct (Int64.ltu _ _); auto.
+  1,2: unfold Val.cmplu; simpl; auto;
+  destruct (Archi.ptr64); simpl;
+  try destruct (eq_block _ _); simpl;
+  try destruct (_ && _); simpl;
+  try destruct (Ptrofs.cmpu _ _);
+  try destruct cmp; simpl; auto.
+  unfold Val.cmplu; simpl;
+  destruct Archi.ptr64; try destruct (_ || _); simpl; auto;
+  destruct (eq_block b b0); destruct (eq_block b0 b);
+  try congruence;
+  try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _);
+  simpl; auto;
+  repeat destruct (_ && _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_ltge_cmplu: core.
+
+(** ** Floats *)
+
+Lemma xor_neg_eqne_cmpf: forall v1 v2,
+  Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence;
+  unfold Val.cmpf; simpl.
+  rewrite Float.cmp_ne_eq.
+  destruct (Float.cmp _ _ _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_eqne_cmpf: core.
+
+(** ** Singles *)
+
+Lemma xor_neg_eqne_cmpfs: forall v1 v2,
+  Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
+  Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)).
+Proof.
+  intros. eapply f_equal.
+  destruct v1, v2; simpl; try congruence;
+  unfold Val.cmpfs; simpl.
+  rewrite Float32.cmp_ne_eq.
+  destruct (Float32.cmp _ _ _); simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_eqne_cmpfs: core.
+
+(** ** More useful lemmas *)
+
+Lemma xor_neg_optb: forall v,
+  Some (Val.xor (Val.of_optbool (option_map negb v))
+    (Vint Int.one)) = Some (Val.of_optbool v).
+Proof.
+  intros.
+  destruct v; simpl; trivial.
+  destruct b; simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_optb: core.
+
+Lemma xor_neg_optb': forall v,
+  Some (Val.xor (Val.of_optbool v) (Vint Int.one)) =
+  Some (Val.of_optbool (option_map negb v)).
+Proof.
+  intros.
+  destruct v; simpl; trivial.
+  destruct b; simpl; auto.
+Qed.
+Local Hint Resolve xor_neg_optb': core.
+
+Lemma optbool_mktotal: forall v,
+  Val.maketotal (option_map Val.of_bool v) =
+  Val.of_optbool v.
+Proof.
+  intros.
+  destruct v; simpl; auto.
+Qed.
+Local Hint Resolve optbool_mktotal: core.
+
+(** * Intermediates lemmas on each expanded instruction *)
+
+Lemma simplify_ccomp_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int32s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmp_bool c v v0)).
+Proof.
+  intros.
+  unfold cond_int32s in *; destruct c; simpl;
+  erewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmp. eauto.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmp_bool; trivial.
+  - replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool; eauto.
+Qed.
+
+Lemma simplify_ccompu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int32u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)).
+Proof.
+  intros.
+  unfold cond_int32u in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpu.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpu_bool; trivial.
+  - replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmpu_bool; eauto.
+Qed.
+
+Lemma simplify_ccompimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int32s c (hrs r) n) =
+  Some (Val.of_optbool (Val.cmp_bool c v (Vint n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int32s, cond_int32s in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  try apply Int.same_if_eq in EQIMM; subst;
+  unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32;
+  try rewrite !REG_EQ, OKv1;
+  unfold Val.cmp, zero32.
+  all:
+    try apply xor_neg_ltle_cmp; 
+    try apply xor_neg_ltge_cmp; trivial.
+  4: 
+    try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst;
+    try apply Int.same_if_eq in EQMAX; subst; simpl.
+  4:
+    intros; try (specialize make_immed32_sound with (Int.one);
+    destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl.
+  6:
+    intros; try (specialize make_immed32_sound with (Int.add n Int.one);
+    destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl.
+  1,2,3,8,9:
+    intros; try (specialize make_immed32_sound with (n);
+    destruct (make_immed32 n) eqn:EQMKI); intros; simpl.
+  all: 
+    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
+    try apply Int.same_if_eq in EQLO32; subst;
+    try rewrite !REG_EQ, OKv1;
+    try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; simpl;
+    unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl;
+    destruct v; auto.
+  all:
+    try rewrite ltu_12_wordsize;
+    try rewrite <- H;
+    try (apply cmp_ltle_add_one; auto);
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    try (
+    simpl; trivial;
+    try rewrite Int.xor_is_zero;
+    try destruct (Int.lt _ _) eqn:EQLT; trivial;
+    try rewrite lt_maxsgn_false_int in EQLT;
+    simpl; trivial; try discriminate; fail).
+Qed.
+
+Lemma simplify_ccompuimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int32u c (hrs r) n) =
+  Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vint n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  try apply Int.same_if_eq in EQIMM; subst;
+  unfold loadimm32, sltuimm32, opimm32, load_hilo32;
+  try rewrite !REG_EQ, OKv1; trivial;
+  try rewrite xor_neg_ltle_cmpu;
+  unfold Val.cmpu, zero32.
+  all:
+    try (specialize make_immed32_sound with n;
+    destruct (make_immed32 n) eqn:EQMKI);
+    try destruct (Int.eq lo Int.zero) eqn:EQLO;
+    try apply Int.same_if_eq in EQLO; subst;
+    intros; subst; simpl;
+    try rewrite !REG_EQ, OKv1;
+    unfold eval_may_undef, Val.cmpu;
+    destruct v; simpl; auto;
+    try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl;
+    try rewrite ltu_12_wordsize; trivial;
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
+    try rewrite EQLTU; simpl; try rewrite EQIMM;
+    try rewrite EQARCH; trivial.
+Qed.
+
+Lemma simplify_ccompl_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int64s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmpl_bool c v v0)).
+Proof.
+  intros.
+  unfold cond_int64s in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpl.
+  1,2,3: rewrite optbool_mktotal; trivial.
+  replace (Clt) with (swap_comparison Cgt) by auto;
+  rewrite Val.swap_cmpl_bool; trivial.
+  rewrite optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccomplu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (cond_int64u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) =
+  Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)).
+Proof.
+  intros.
+  unfold cond_int64u in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmplu.
+  1,2,3: rewrite optbool_mktotal; trivial; eauto.
+  replace (Clt) with (swap_comparison Cgt) by auto;
+  rewrite Val.swap_cmplu_bool; trivial.
+  rewrite optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccomplimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int64s c (hrs r) n) =
+  Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int64s, cond_int64s in *; destruct c;
+  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
+  try apply Int64.same_if_eq in EQIMM; subst;
+  unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64;
+  try rewrite !REG_EQ, OKv1;
+  unfold Val.cmpl, zero64.
+  all:
+    try apply xor_neg_ltle_cmpl; 
+    try apply xor_neg_ltge_cmpl;
+    try rewrite optbool_mktotal; trivial.
+  4: 
+    try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst;
+    try apply Int64.same_if_eq in EQMAX; subst; simpl.
+  4:
+    intros; try (specialize make_immed32_sound with (Int.one);
+    destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl.
+  6:
+    intros; try (specialize make_immed64_sound with (Int64.add n Int64.one);
+    destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl.
+  1,2,3,9,10:
+    intros; try (specialize make_immed64_sound with (n);
+    destruct (make_immed64 n) eqn:EQMKI); intros; simpl.
+  all: 
+    try destruct (Int.eq lo Int.zero) eqn:EQLO32;
+    try apply Int.same_if_eq in EQLO32; subst;
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO64;
+    try apply Int64.same_if_eq in EQLO64; subst; simpl;
+    try rewrite !REG_EQ, OKv1;
+    try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst;
+    unfold Val.cmpl, Val.addl;
+    try rewrite optbool_mktotal; trivial;
+    destruct v; auto.
+  all:
+    try rewrite <- optbool_mktotal; trivial;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *;
+    try fold (Val.cmpl Clt (Vlong i) (Vlong imm));
+    try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12)))));
+    try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))).
+  all:
+    try rewrite <- cmpl_ltle_add_one; auto;
+    try rewrite ltu_12_wordsize;
+    try rewrite Int.add_commut, Int.add_zero_l in *;
+    simpl; try rewrite lt_maxsgn_false_long;
+    try (rewrite <- H; trivial; fail);
+    simpl; trivial.
+Qed.
+
+Lemma simplify_ccompluimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r v n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v),
+  eval_sval ctx (expanse_condimm_int64u c (hrs r) n) =
+  Some (Val.of_optbool
+     (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vlong n))).
+Proof.
+  intros.
+  unfold expanse_condimm_int64u, cond_int64u in *; destruct c;
+  intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl;
+  unfold loadimm64, sltuimm64, opimm64, load_hilo64;
+  try rewrite !REG_EQ, OKv1;
+  unfold Val.cmplu, zero64.
+  (* Simplify make immediate and decompose subcases *)
+  all:
+    try (specialize make_immed64_sound with n;
+    destruct (make_immed64 n) eqn:EQMKI);
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+    try rewrite !REG_EQ, OKv1.
+  (* Ceq, Cne, Clt = itself *)
+  all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial.
+  (* Cle = xor (Clt) *)
+  all: try apply xor_neg_ltle_cmplu; trivial.
+  (* Others subcases with swap/negation *)
+  all:
+    unfold Val.cmplu, eval_may_undef, zero64, Val.addl;
+    try apply Int64.same_if_eq in EQLO; subst;
+    try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
+    try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu;
+    trivial; fail);
+    try rewrite optbool_mktotal; trivial.
+  all:
+    try destruct v; simpl; auto;
+    try destruct (Archi.ptr64); simpl;
+    try rewrite EQIMM;
+    try destruct (Int64.ltu _ _);
+    try rewrite <- optbool_mktotal; trivial.
+Qed.
+
+Lemma simplify_ccompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (expanse_cond_fp false cond_float c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (Val.cmpf_bool c v v0)).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpf.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpf_bool; trivial.
+  - replace (Cle) with (swap_comparison Cge) by auto;
+    rewrite Val.swap_cmpf_bool; trivial.
+Qed.
+
+Lemma simplify_cnotcompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (expanse_cond_fp true cond_float c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpf.
+  1,3,4: apply xor_neg_optb'.
+  all: destruct v, v0; simpl; trivial.
+  rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial.
+  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl.
+  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl.
+  all: destruct (Float.cmp _ _ _); trivial.
+Qed.
+
+Lemma simplify_ccompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),  eval_sval ctx
+    (expanse_cond_fp false cond_single c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (Val.cmpfs_bool c v v0)).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpfs.
+  - replace (Clt) with (swap_comparison Cgt) by auto;
+    rewrite Val.swap_cmpfs_bool; trivial.
+  - replace (Cle) with (swap_comparison Cge) by auto;
+    rewrite Val.swap_cmpfs_bool; trivial.
+Qed.
+
+Lemma simplify_cnotcompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  c r r0 v v0: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (OKv1 : eval_sval ctx (st r) = Some v)
+  (OKv2 : eval_sval ctx (st r0) = Some v0),
+  eval_sval ctx
+    (expanse_cond_fp true cond_single c
+       (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) =
+  Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))).
+Proof.
+  intros.
+  unfold expanse_cond_fp in *; destruct c; simpl;
+  rewrite !REG_EQ, OKv1, OKv2; trivial;
+  unfold Val.cmpfs.
+  1,3,4: apply xor_neg_optb'.
+  all: destruct v, v0; simpl; trivial.
+  rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial.
+  1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl.
+  2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl.
+  all: destruct (Float32.cmp _ _ _); trivial.
+Qed.
+
+Lemma simplify_intconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil => Some (loadimm32 n)
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Ointconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm32, load_hilo32, make_lfsv_single; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  try apply Int.same_if_eq in EQLO; subst;
+  try rewrite Int.add_commut, Int.add_zero_l;
+  try rewrite ltu_12_wordsize; try rewrite H; trivial.
+Qed.
+
+Lemma simplify_longconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil => Some (loadimm64 n)
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Olongconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm64, load_hilo64, make_lfsv_single; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  try apply Int64.same_if_eq in EQLO; subst;
+  try rewrite Int64.add_commut, Int64.add_zero_l;
+  try rewrite Int64.add_commut;
+  try rewrite ltu_12_wordsize; try rewrite H; trivial.
+Qed.
+
+Lemma simplify_floatconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil =>
+           Some
+             (fSop Ofloat_of_bits
+                (make_lfsv_single (loadimm64 (Float.to_bits n))))
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Ofloatconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm64, load_hilo64; simpl;
+  specialize make_immed64_sound with (Float.to_bits n);
+  destruct (make_immed64 (Float.to_bits n)) eqn:EQMKI; intros;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
+  simpl.
+  - try rewrite Int64.add_commut, Int64.add_zero_l; inv H;
+    try rewrite Float.of_to_bits; trivial.
+  - apply Int64.same_if_eq in EQLO; subst.
+    try rewrite Int64.add_commut, Int64.add_zero_l in H.
+    rewrite <- H; try rewrite Float.of_to_bits; trivial.
+  - rewrite <- H; try rewrite Float.of_to_bits; trivial.
+  - rewrite <- H; try rewrite Float.of_to_bits; trivial.
+Qed.
+
+Lemma simplify_singleconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil =>
+           Some
+             (fSop Osingle_of_bits
+                (make_lfsv_single (loadimm32 (Float32.to_bits n))))
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Osingleconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm32, load_hilo32; simpl;
+  specialize make_immed32_sound with (Float32.to_bits n);
+  destruct (make_immed32 (Float32.to_bits n)) eqn:EQMKI; intros;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO;
+  simpl.
+  { try rewrite Int.add_commut, Int.add_zero_l; inv H;
+    try rewrite Float32.of_to_bits; trivial. }
+  all:
+    try apply Int.same_if_eq in EQLO; subst;
+    try rewrite Int.add_commut, Int.add_zero_l in H; simpl;
+    rewrite ltu_12_wordsize; simpl; try rewrite <- H;
+    try rewrite Float32.of_to_bits; trivial.
+Qed.
+
+Lemma simplify_cast8signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           Some
+             (fSop (Oshrimm (Int.repr 24))
+                (make_lfsv_single
+                   (fSop (Oshlimm (Int.repr 24)) (make_lfsv_single (hrs a1)))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) Ocast8signed args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  rewrite !REG_EQ.
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
+  unfold Val.shr, Val.shl, Val.sign_ext;
+  destruct v; simpl; auto.
+  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
+  rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia.
+Qed.
+
+Lemma simplify_cast16signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           Some
+             (fSop (Oshrimm (Int.repr 16))
+                (make_lfsv_single
+                   (fSop (Oshlimm (Int.repr 16)) (make_lfsv_single (hrs a1)))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) Ocast16signed args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  rewrite !REG_EQ.
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
+  unfold Val.shr, Val.shl, Val.sign_ext;
+  destruct v; simpl; auto.
+  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
+  rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia.
+Qed.
+
+Lemma simplify_addimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (addimm32 (hrs a1) n None)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oaddimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold addimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_andimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (andimm32 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oandimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold andimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_orimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (orimm32 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oorimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold orimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_xorimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (xorimm32 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oxorimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold xorimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_shrximm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           if Int.eq n Int.zero
+           then
+            Some
+              (fSop (OEmayundef (MUshrx n))
+                 (make_lfsv_cmp false (hrs a1) (hrs a1)))
+           else
+            if Int.eq n Int.one
+            then
+             Some
+               (fSop (OEmayundef (MUshrx n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.repr 31))
+                                    (make_lfsv_single (hrs a1)))))))
+                     (fSop (Oshrimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.repr 31))
+                                    (make_lfsv_single (hrs a1)))))))))
+            else
+             Some
+               (fSop (OEmayundef (MUshrx n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrimm n)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrimm (Int.repr 31))
+                                          (make_lfsv_single (hrs a1)))))))))
+                     (fSop (Oshrimm n)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrimm (Int.repr 31))
+                                          (make_lfsv_single (hrs a1)))))))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oshrximm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence).
+  assert (A: Int.ltu Int.zero (Int.repr 31) = true) by auto.
+  assert (B: Int.ltu (Int.repr 31) Int.iwordsize = true) by auto.
+  assert (C: Int.ltu Int.one Int.iwordsize = true) by auto.
+  destruct (Int.eq n Int.zero) eqn:EQ0;
+  destruct (Int.eq n Int.one) eqn:EQ1.
+  { apply Int.same_if_eq in EQ0.
+    apply Int.same_if_eq in EQ1; subst. discriminate. }
+  all:
+    simpl in OK1; inv H; simpl;
+    rewrite !REG_EQ;
+    destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1;
+    destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn;
+    unfold eval_may_undef.
+  2,4,6:
+    unfold Val.shrx in TOTAL;
+    destruct v; simpl in TOTAL; simpl; try congruence;
+    try rewrite B; simpl; try rewrite C; simpl;
+    try destruct (Val.shr _ _);
+    destruct (Int.ltu n (Int.repr 31)); try congruence.
+  - destruct v; simpl in TOTAL; try congruence;
+    apply Int.same_if_eq in EQ0; subst;
+    rewrite A, Int.shrx_zero in TOTAL;
+    [auto | cbn; lia].
+  - apply Int.same_if_eq in EQ1; subst;
+    unfold Val.shr, Val.shru, Val.shrx, Val.add; simpl;
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B, C.
+    rewrite Int.shrx1_shr in TOTAL; auto.
+  - exploit Val.shrx_shr_2; eauto. rewrite EQ0.
+    intros; subst.
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B in *.
+    destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate.
+    simpl in *.
+    destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate.
+    replace Int.iwordsize with (Int.repr 32) in * by auto.
+    rewrite !EQN1. simpl in *.
+    destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
+    rewrite !EQN2. rewrite EQN0.
+    reflexivity.
+Qed.
+
+Lemma simplify_cast32unsigned_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           Some
+             (fSop (Oshrluimm (Int.repr 32))
+                (make_lfsv_single
+                   (fSop (Oshllimm (Int.repr 32))
+                      (make_lfsv_single
+                         (fSop Ocast32signed (make_lfsv_single (hrs a1)))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) Ocast32unsigned args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
+  unfold Val.shrlu, Val.shll, Val.longofint, Val.longofintu.
+  destruct v; simpl; auto.
+  assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
+  rewrite A. rewrite Int64.shru'_shl'; auto.
+  replace (Int.ltu (Int.repr 32) (Int.repr 32)) with (false) by auto.
+  rewrite cast32unsigned_from_cast32signed.
+  replace Int64.zwordsize with 64 by auto.
+  rewrite Int.unsigned_repr; cbn; try lia.
+  replace (Int.sub (Int.repr 32) (Int.repr 32)) with (Int.zero) by auto.
+  rewrite Int64.shru'_zero. reflexivity.
+Qed.
+
+Lemma simplify_addlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (addimm64 (hrs a1) n None)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oaddlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold addimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int64.same_if_eq in EQLO; subst.
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_andlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (andimm64 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oandlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold andimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial.
+  apply Int64.same_if_eq in EQLO; subst;
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_orlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (orimm64 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oorlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold orimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial.
+  apply Int64.same_if_eq in EQLO; subst;
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_xorlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (xorimm64 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oxorlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold xorimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int64.same_if_eq in EQLO; subst;
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_shrxlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           if Int.eq n Int.zero
+           then
+            Some
+              (fSop (OEmayundef (MUshrxl n))
+                 (make_lfsv_cmp false (hrs a1) (hrs a1)))
+           else
+            if Int.eq n Int.one
+            then
+             Some
+               (fSop (OEmayundef (MUshrxl n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrlimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.repr 63))
+                                    (make_lfsv_single (hrs a1)))))))
+                     (fSop (Oshrlimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.repr 63))
+                                    (make_lfsv_single (hrs a1)))))))))
+            else
+             Some
+               (fSop (OEmayundef (MUshrxl n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrlimm n)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrlimm (Int.repr 63))
+                                          (make_lfsv_single (hrs a1)))))))))
+                     (fSop (Oshrlimm n)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrlimm (Int.repr 63))
+                                          (make_lfsv_single (hrs a1)))))))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oshrxlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence).
+  assert (A: Int.ltu Int.zero (Int.repr 63) = true) by auto.
+  assert (B: Int.ltu (Int.repr 63) Int64.iwordsize' = true) by auto.
+  assert (C: Int.ltu Int.one Int64.iwordsize' = true) by auto.
+  destruct (Int.eq n Int.zero) eqn:EQ0;
+  destruct (Int.eq n Int.one) eqn:EQ1.
+  { apply Int.same_if_eq in EQ0.
+    apply Int.same_if_eq in EQ1; subst. discriminate. }
+  all:
+    simpl in OK1; inv H; simpl;
+    rewrite !REG_EQ;
+    destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1;
+    destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn;
+    unfold eval_may_undef.
+  2,4,6:
+    unfold Val.shrxl in TOTAL;
+    destruct v; simpl in TOTAL; simpl; try congruence;
+    try rewrite B; simpl; try rewrite C; simpl;
+    try destruct (Val.shrl _ _);
+    destruct (Int.ltu n (Int.repr 63)); try congruence.
+  - destruct v; simpl in TOTAL; try congruence;
+    apply Int.same_if_eq in EQ0; subst;
+    rewrite A, Int64.shrx'_zero in *.
+    assumption.
+  - apply Int.same_if_eq in EQ1; subst;
+    unfold Val.shrl, Val.shrlu, Val.shrxl, Val.addl; simpl;
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B, C.
+    rewrite Int64.shrx'1_shr' in TOTAL; auto.
+  - exploit Val.shrxl_shrl_2; eauto. rewrite EQ0.
+    intros; subst.
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B in *.
+    destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate.
+    simpl in *.
+    destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate.
+    replace Int64.iwordsize' with (Int.repr 64) in * by auto.
+    rewrite !EQN1. simpl in *.
+    destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
+    rewrite !EQN2. rewrite EQN0.
+    reflexivity.
+Qed.
+
+(* Main proof of simplification *)
+
+Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall
+   (H: target_op_simplify op lr hrs = Some fsv)
+   (REF: ris_refines ctx hrs st)
+   (OK0: ris_ok ctx hrs)
+   (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args),
+   eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx).
+Proof.
+  unfold target_op_simplify; simpl.
+  intros H ? ? ?; inv REF.
+  destruct op; try congruence.
+  eapply simplify_intconst_correct; eauto.
+  eapply simplify_longconst_correct; eauto.
+  eapply simplify_floatconst_correct; eauto. 
+  eapply simplify_singleconst_correct; eauto. 
+  eapply simplify_cast8signed_correct; eauto.
+  eapply simplify_cast16signed_correct; eauto.
+  eapply simplify_addimm_correct; eauto.
+  eapply simplify_andimm_correct; eauto.
+  eapply simplify_orimm_correct; eauto.
+  eapply simplify_xorimm_correct; eauto.
+  eapply simplify_shrximm_correct; eauto.
+  eapply simplify_cast32unsigned_correct; eauto.
+  eapply simplify_addlimm_correct; eauto.
+  eapply simplify_andlimm_correct; eauto.
+  eapply simplify_orlimm_correct; eauto.
+  eapply simplify_xorlimm_correct; eauto.
+  eapply simplify_shrxlimm_correct; eauto.
+  (* Ocmp expansions *)
+  destruct cond; repeat (destruct lr; simpl; try congruence);
+  simpl in OK1;
+  try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+  try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+  inv H; inv OK1.
+  - eapply simplify_ccomp_correct; eauto.
+  - eapply simplify_ccompu_correct; eauto.
+  - eapply simplify_ccompimm_correct; eauto.
+  - eapply simplify_ccompuimm_correct; eauto.
+  - eapply simplify_ccompl_correct; eauto.
+  - eapply simplify_ccomplu_correct; eauto.
+  - eapply simplify_ccomplimm_correct; eauto.
+  - eapply simplify_ccompluimm_correct; eauto.
+  - eapply simplify_ccompf_correct; eauto.
+  - eapply simplify_cnotcompf_correct; eauto.
+  - eapply simplify_ccompfs_correct; eauto.
+  - eapply simplify_cnotcompfs_correct; eauto.
+Qed.
+
+Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall
+  (TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
+  (REF: ris_refines ctx hrs st)
+  (OK: ris_ok ctx hrs),
+  eval_scondition ctx c' l' =
+  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
+Proof.
+  unfold target_cbranch_expanse, eval_scondition; simpl.
+  intros H ? ?. inversion REF.
+  destruct c; try congruence;
+  repeat (destruct l; simpl in H; try congruence).
+  1,2,5,6:
+    destruct c; inv H; simpl;
+    rewrite !REG_EQ;
+    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+    try replace (Cle) with (swap_comparison Cge) by auto;
+    try replace (Clt) with (swap_comparison Cgt) by auto;
+    try rewrite Val.swap_cmp_bool; trivial;
+    try rewrite Val.swap_cmpu_bool; trivial;
+    try rewrite Val.swap_cmpl_bool; trivial;
+    try rewrite Val.swap_cmplu_bool; trivial.
+  1,2,3,4:
+    try destruct (Int.eq n Int.zero) eqn: EQIMM;
+    try apply Int.same_if_eq in EQIMM;
+    try destruct (Int64.eq n Int64.zero) eqn: EQIMM;
+    try apply Int64.same_if_eq in EQIMM;
+    destruct c; inv H; simpl;
+    rewrite !REG_EQ;
+    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+    unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32;
+    unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64;
+    intros; try (specialize make_immed32_sound with (n);
+    destruct (make_immed32 n) eqn:EQMKI); intros; simpl;
+    intros; try (specialize make_immed64_sound with (n);
+    destruct (make_immed64 n) eqn:EQMKI); intros; simpl;
+    try rewrite EQLO; simpl;
+    try destruct (Int.eq lo Int.zero) eqn:EQLO;
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
+    try apply Int.same_if_eq in EQLO; simpl; trivial;
+    try apply Int64.same_if_eq in EQLO; simpl; trivial;
+    unfold eval_may_undef; 
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try rewrite OKv1; simpl; trivial;
+    try destruct v; try rewrite H;
+    try rewrite ltu_12_wordsize; try rewrite EQLO;
+    try rewrite Int.add_commut, Int.add_zero_l;
+    try rewrite Int64.add_commut, Int64.add_zero_l;
+    try rewrite Int64.add_commut;
+    try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l;
+    auto; simpl;
+    try rewrite H in EQIMM;
+    try rewrite EQLO in EQIMM;
+    try rewrite Int.add_commut, Int.add_zero_l in EQIMM;
+    try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM;
+    try rewrite EQIMM; simpl;
+    try destruct (Archi.ptr64); trivial.
+
+    1,2,3,4:
+    destruct c; inv H; simpl;
+    rewrite !REG_EQ;
+    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+    unfold zero32, zero64, Val.cmpf, Val.cmpfs;
+    destruct v, v0; simpl; trivial;
+    try rewrite Float.cmp_ne_eq;
+    try rewrite Float32.cmp_ne_eq;
+    try rewrite <- Float.cmp_swap; simpl;
+    try rewrite <- Float32.cmp_swap; simpl;
+    try destruct (Float.cmp _ _); simpl;
+    try destruct (Float32.cmp _ _); simpl;
+    try rewrite Int.eq_true; simpl;
+    try rewrite Int.eq_false; try apply Int.one_not_zero;
+    simpl; trivial.
+Qed.
+Global Opaque target_op_simplify.
+Global Opaque target_cbranch_expanse.
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 68d4e4d2..49ca7e96 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -10,19 +10,29 @@
 (*                                                             *)
 (* *************************************************************)
 
-open RTLpathLivegenaux
-open RTLpathCommon
-open Datatypes
-open Maps
-open RTL
+open BTL
 open Op
-open Asmgen
-open RTLpath
 open! Integers
 open Camlcoq
-open Option
-open AST
 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 *)
@@ -31,22 +41,12 @@ open DebugPrint
 
 let reg = ref 1
 
-let node = ref 1
-
-let p2i r = P.to_int r
-
 let r2p () = P.of_int !reg
 
-let n2p () = P.of_int !node
-
 let r2pi () =
   reg := !reg + 1;
   r2p ()
 
-let n2pi () =
-  node := !node + 1;
-  n2p ()
-
 (** Below are the types for rhs and equations *)
 
 type rhs = Sop of operation * int list | Smove
@@ -54,18 +54,15 @@ type rhs = Sop of operation * int list | Smove
 type seq = Seq of int * rhs
 
 (** This is a mini abstraction to have a simpler representation during expansion
-    - Snop will be converted to Inop
     - (Sr r) is inserted if the value was found in register r
-    - (Sexp dest rhs args succ) represent an instruction
-      (succesor may not be defined at this point, hence the use of type option)
-    - (Sfinalcond cond args succ1 succ2 info) represents a condition (which must
-      always be the last instruction in expansion list *)
+    - (Sexp dest rhs args iinfo) represent an instruction
+    - (Scond cond args ib1 ib2 iinfo) represents a condition
+*)
 
 type expl =
-  | Snop of P.t
   | Sr of P.t
-  | Sexp of P.t * rhs * P.t list * node option
-  | Sfinalcond of condition * P.t list * node * node * bool option
+  | 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 *)
 
@@ -193,18 +190,15 @@ let extract_arg l =
     | _ -> failwith "extract_arg: final instruction arg can not be extracted"
   else failwith "extract_arg: trying to extract on an empty list"
 
-let extract_final vn fl fdest succ =
+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 ], Some succ) :: List.tl fl)
-        else Snop succ :: List.tl fl
-    | Sexp (rd, rh, args, None) ->
-        assert (rd = fdest);
-        Sexp (fdest, rh, args, Some succ) :: List.tl fl
+          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"
 
@@ -217,7 +211,7 @@ let addinst vn op args rd =
       Sr r
   | None ->
       addsop vn v op rd;
-      Sexp (rd, rh, args, None)
+      Sexp (rd, rh, args, def_iinfo ())
 
 (** Expansion functions *)
 
@@ -344,45 +338,45 @@ let is_inv_cmp = function Cle | Cgt -> true | _ -> false
 let make_optR is_x0 is_inv =
   if is_x0 then if is_inv then Some X0_L else Some X0_R else None
 
-let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
+let 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 -> Sfinalcond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
+  | 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 -> Sfinalcond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
+  | 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 -> Sfinalcond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
+  | 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 -> Sfinalcond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Sfinalcond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Sfinalcond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Sfinalcond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Sfinalcond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Sfinalcond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | 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
@@ -484,39 +478,39 @@ let cond_single vn cmp f1 f2 dest =
   | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ]
   | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ]
 
-let expanse_cbranchimm_int32s vn cmp a1 n info succ1 succ2 =
-  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 []
+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' info succ1 succ2 l'
+    cbranch_int32s false cmp a1 r' iinfo succ1 succ2 l'
 
-let expanse_cbranchimm_int32u vn cmp a1 n info succ1 succ2 =
-  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 []
+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' info succ1 succ2 l'
+    cbranch_int32u false cmp a1 r' iinfo succ1 succ2 l'
 
-let expanse_cbranchimm_int64s vn cmp a1 n info succ1 succ2 =
+let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 =
   if Int64.eq n Int64.zero then
-    cbranch_int64s true cmp a1 a1 info succ1 succ2 []
+    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' info succ1 succ2 l'
+    cbranch_int64s false cmp a1 r' iinfo succ1 succ2 l'
 
-let expanse_cbranchimm_int64u vn cmp a1 n info succ1 succ2 =
+let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 =
   if Int64.eq n Int64.zero then
-    cbranch_int64u true cmp a1 a1 info succ1 succ2 []
+    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' info succ1 succ2 l'
+    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
@@ -593,469 +587,427 @@ let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest =
     let r', l = extract_arg insn in
     addinst vn (OExoriw Int.one) [ r' ] dest :: l
 
-let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 =
+let 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
-    Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
-  else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
-
-(** Form a list containing both sources and destination regs of an instruction *)
-
-let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
-
-let get_regs_inst = function
-  | Inop _ -> []
-  | Iop (_, args, dest, _) -> dest :: args
-  | Iload (_, _, _, args, dest, _) -> dest :: args
-  | Istore (_, _, args, src, _) -> src :: args
-  | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args)
-  | Itailcall (_, t, args) -> get_regindent t @ args
-  | Ibuiltin (_, args, dest, _) ->
-      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
-  | Icond (_, args, _, _, _) -> args
-  | Ijumptable (arg, _) -> [ arg ]
-  | Ireturn (Some r) -> [ r ]
-  | _ -> []
-
-(** Modify pathmap according to the size of the expansion list *)
-
-let write_pathmap initial esize pm' =
-  debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize;
-  let path = get_some @@ PTree.get initial !pm' in
-  let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in
-  let path' =
-    {
-      psize = npsize;
-      input_regs = path.input_regs;
-      pre_output_regs = path.pre_output_regs;
-      output_regs = path.output_regs;
-    }
-  in
-  pm' := PTree.set initial path' !pm'
-
-(** Write a single instruction in the tree and update order *)
-
-let write_inst target_node inst code' new_order =
-  code' := PTree.set (P.of_int target_node) inst !code';
-  new_order := P.of_int target_node :: !new_order
+    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
 
-(** Update the code tree with the expansion list *)
-
-let rec write_tree vn exp initial current code' new_order fturn =
-  debug "wt: node is %d\n" !node;
-  let target_node, next_node =
-    if fturn then (P.to_int initial, current) else (current, current - 1)
-  in
+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, None) :: k ->
-      let args = get_arguments vn vals args in
-      let inst = Iop (op, args, rd, P.of_int next_node) in
-      write_inst target_node inst code' new_order;
-      write_tree vn k initial next_node code' new_order false
-  | [ Snop succ ] ->
-      let inst = Inop succ in
-      write_inst target_node inst code' new_order
-  | [ Sexp (rd, Sop (op, vals), args, Some succ) ] ->
+  | Sexp (rd, Sop (op, vals), args, iinfo) :: k ->
       let args = get_arguments vn vals args in
-      let inst = Iop (op, args, rd, succ) in
-      write_inst target_node inst code' new_order
-  | [ Sexp (rd, Smove, args, Some succ) ] ->
-      let inst = Iop (Omove, args, rd, succ) in
-      write_inst target_node inst code' new_order
-  | [ Sfinalcond (cond, args, succ1, succ2, info) ] ->
-      let inst = Icond (cond, args, succ1, succ2, info) in
-      write_inst target_node inst code' new_order
-  | [] -> ()
+      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"
 
-(** Main expansion function - TODO gourdinl to split? *)
-let expanse (sb : superblock) code pm =
-  debug "#### New superblock for expansion oracle\n";
-  let new_order = ref [] in
-  let liveins = ref sb.liveins in
+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 code' = ref code in
-  let pm' = ref pm in
   let vn = ref (empty_numbering ()) in
-  Array.iter
-    (fun n ->
-      was_branch := false;
-      was_exp := false;
-      let inst = get_some @@ PTree.get n code in
-      (if !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";
-           exp := cond_int32s vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccompu\n";
-           exp := cond_int32u vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccompimm\n";
-           exp := expanse_condimm_int32s vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccompuimm\n";
-           exp := expanse_condimm_int32u vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccompl\n";
-           exp := cond_int64s vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
-           debug "Iop/Ccomplu\n";
-           exp := cond_int64u vn false c a1 a2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccomplimm\n";
-           exp := expanse_condimm_int64s vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
-           debug "Iop/Ccompluimm\n";
-           exp := expanse_condimm_int64u vn c a1 imm dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Ccompf\n";
-           exp := expanse_cond_fp vn false cond_float c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Cnotcompf\n";
-           exp := expanse_cond_fp vn true cond_float c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Ccompfs\n";
-           exp := expanse_cond_fp vn false cond_single c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
-           debug "Iop/Cnotcompfs\n";
-           exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       (* Expansion of branches - Ccomp *)
-       | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           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 vn 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 vn 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 vn 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 vn 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 vn false cond_float c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Cnotcompf\n";
-           exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Ccompfs\n";
-           exp :=
-             expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           debug "Icond/Cnotcompfs\n";
-           exp :=
-             expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2;
-           was_branch := true;
-           was_exp := true
-       | _ -> ());
-      (if !Clflags.option_fexpanse_others && not !was_exp then
-       match inst with
-       | Iop (Ofloatconst f, nil, dest, succ) -> (
-           match make_immed64 (Floats.Float.to_bits f) with
-           | Imm64_single _ | Imm64_large _ -> ()
-           | Imm64_pair (hi, lo) ->
-               debug "Iop/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 succ;
-               was_exp := true)
-       | Iop (Osingleconst f, nil, dest, succ) -> (
-           match make_immed32 (Floats.Float32.to_bits f) with
-           | Imm32_single imm -> ()
-           | Imm32_pair (hi, lo) ->
-               debug "Iop/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 succ;
-               was_exp := true)
-       | Iop (Ointconst n, nil, dest, succ) ->
-           debug "Iop/Ointconst\n";
-           exp := loadimm32 vn dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Olongconst n, nil, dest, succ) ->
-           debug "Iop/Olongconst\n";
-           exp := loadimm64 vn dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oaddimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oaddimm\n";
-           exp := addimm32 vn a1 dest n None;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oaddlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oaddlimm\n";
-           exp := addimm64 vn a1 dest n None;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oandimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oandimm\n";
-           exp := andimm32 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oandlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oandlimm\n";
-           exp := andimm64 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oorimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oorimm\n";
-           exp := orimm32 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oorlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oorlimm\n";
-           exp := orimm64 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oxorimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oxorimm\n";
-           exp := xorimm32 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oxorlimm n, a1 :: nil, dest, succ) ->
-           debug "Iop/Oxorlimm\n";
-           exp := xorimm64 vn a1 dest n;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocast8signed, a1 :: nil, dest, succ) ->
-           debug "Iop/cast8signed\n";
-           let op = Oshlimm (Int.repr (Z.of_sint 24)) in
-           let r = r2pi () in
-           let i1 = addinst vn op [ a1 ] r in
-           let r', l = extract_arg [ i1 ] in
-           exp :=
-             addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocast16signed, a1 :: nil, dest, succ) ->
-           debug "Iop/cast16signed\n";
-           let op = Oshlimm (Int.repr (Z.of_sint 16)) in
-           let r = r2pi () in
-           let i1 = addinst vn op [ a1 ] r in
-           let r', l = extract_arg [ i1 ] in
-           exp :=
-             addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Ocast32unsigned, a1 :: nil, dest, succ) ->
-           debug "Iop/Ocast32unsigned\n";
-           let r1 = r2pi () in
-           let r2 = r2pi () in
-           let op1 = Ocast32signed in
-           let i1 = addinst vn op1 [ a1 ] r1 in
-           let r1', l1 = extract_arg [ i1 ] in
-
-           let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in
-           let i2 = addinst vn op2 [ r1' ] r2 in
-           let r2', l2 = extract_arg (i2 :: l1) in
-
-           let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in
-           exp := addinst vn op3 [ r2' ] dest :: l2;
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oshrximm n, a1 :: nil, dest, succ) ->
-           if Int.eq n Int.zero then (
-             debug "Iop/Oshrximm1\n";
-             exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
-           else if Int.eq n Int.one then (
-             debug "Iop/Oshrximm2\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
-
-             let op2 = Oadd in
-             let i2 = addinst vn op2 [ a1; r1' ] r2 in
-             let r2', l2 = extract_arg (i2 :: l1) in
-
-             let op3 = Oshrimm Int.one in
-             let i3 = addinst vn op3 [ r2' ] dest in
-             let r3, l3 = extract_arg (i3 :: l2) in
-             exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3)
-           else (
-             debug "Iop/Oshrximm3\n";
+  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 r3 = r2pi () in
-             let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in
+             let op1 = Ocast32signed 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 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 = Oadd in
-             let i3 = addinst vn op3 [ a1; r2' ] r3 in
-             let r3', l3 = extract_arg (i3 :: l2) in
-
-             let op4 = Oshrimm n in
-             let i4 = addinst vn op4 [ r3' ] dest in
-             let r4, l4 = extract_arg (i4 :: l3) in
-             exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4);
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | Iop (Oshrxlimm n, a1 :: nil, dest, succ) ->
-           if Int.eq n Int.zero then (
-             debug "Iop/Oshrxlimm1\n";
-             exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
-           else if Int.eq n Int.one then (
-             debug "Iop/Oshrxlimm2\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
+             let 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 op2 = Oaddl in
-             let i2 = addinst vn op2 [ a1; r1' ] r2 in
-             let r2', l2 = extract_arg (i2 :: l1) in
+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
 
-             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 "Iop/Oshrxlimm3\n";
-             let r1 = r2pi () in
-             let r2 = r2pi () in
-             let r3 = r2pi () in
-             let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in
-             let i1 = addinst vn op1 [ a1 ] r1 in
-             let r1', l1 = extract_arg [ i1 ] in
+(** Form a list containing both sources and destination regs of a block *)
+let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
 
-             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 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 op3 = Oaddl in
-             let i3 = addinst vn op3 [ a1; r2' ] r3 in
-             let r3', l3 = extract_arg (i3 :: l2) in
-
-             let op4 = Oshrlimm n in
-             let i4 = addinst vn op4 [ r3' ] dest in
-             let r4, l4 = extract_arg (i4 :: l3) in
-             exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4);
-           exp := extract_final vn !exp dest succ;
-           was_exp := true
-       | _ -> ());
-      (* Update the CSE numbering *)
-      (if not !was_exp then
-       match inst with
-       | Iop (op, args, dest, succ) ->
-           let v = get_nvalues vn args in
-           addsop vn v op dest
-       | Iload (_, _, _, _, dst, _) -> set_unknown vn dst
-       | Istore (chk, addr, args, src, s) ->
-           !vn.seqs <- kill_mem_operations !vn.seqs
-       | Icall (_, _, _, _, _) | Itailcall (_, _, _) | Ibuiltin (_, _, _, _) ->
-           vn := empty_numbering ()
-       | _ -> ());
-      (* Update code, liveins, pathmap, and order of the superblock for one expansion *)
-      if !was_exp then (
-        (if !was_branch && List.length !exp > 1 then
-         let lives = PTree.get n !liveins in
-         match lives with
-         | Some lives ->
-             let new_branch_pc = P.of_int (!node + 1) in
-             liveins := PTree.set new_branch_pc lives !liveins;
-             liveins := PTree.remove n !liveins
-         | _ -> ());
-        node := !node + List.length !exp - 1;
-        write_pathmap sb.instructions.(0) (List.length !exp - 1) pm';
-        write_tree vn (List.rev !exp) n !node code' new_order true)
-      else new_order := n :: !new_order)
-    sb.instructions;
-  sb.instructions <- Array.of_list (List.rev !new_order);
-  sb.liveins <- !liveins;
-  (!code', !pm')
-
-(** Compute the last used node and reg indexs *)
-
-let rec find_last_node_reg = function
+let rec find_last_reg = function
   | [] -> ()
-  | (pc, i) :: k ->
+  | (pc, ibf) :: k ->
       let rec traverse_list var = function
         | [] -> ()
         | e :: t ->
@@ -1063,6 +1015,5 @@ let rec find_last_node_reg = function
             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
+      traverse_list reg (get_regs_ib ibf.entry);
+      find_last_reg k
diff --git a/riscV/PrepassSchedulingOracle.ml b/riscV/PrepassSchedulingOracle.ml
index 53a81095..912e9ffa 100644..120000
--- a/riscV/PrepassSchedulingOracle.ml
+++ b/riscV/PrepassSchedulingOracle.ml
@@ -1,485 +1 @@
-open AST
-open RTL
-open Maps
-open InstructionScheduler
-open Registers
-open PrepassSchedulingOracleDeps
-   
-let use_alias_analysis () = false
-                          
-let length_of_chunk = function
-| Mint8signed
-| Mint8unsigned -> 1
-| Mint16signed
-| Mint16unsigned -> 2
-| Mint32
-| Mfloat32
-| Many32 -> 4
-| Mint64
-| Mfloat64 
-| Many64 -> 8;;
-
-let get_simple_dependencies (opweights : opweights) (seqa : (instruction*Regset.t) array) =
-  let last_reg_reads : int list PTree.t ref = ref PTree.empty
-  and last_reg_write : (int*int) PTree.t ref = ref PTree.empty
-  and last_mem_reads : int list ref = ref []
-  and last_mem_write : int option ref = ref None
-  and last_branch : int option ref = ref None
-  and last_non_pipelined_op : int array = Array.make
-                                        opweights.nr_non_pipelined_units ( -1 )
-  and latency_constraints : latency_constraint list ref = ref [] in
-  let add_constraint instr_from instr_to latency =
-    assert (instr_from <= instr_to);
-    assert (latency >= 0);
-    if instr_from = instr_to
-    then (if latency = 0
-          then ()
-          else failwith "PrepassSchedulingOracle.get_dependencies: negative self-loop")
-    else
-      latency_constraints :=
-        { instr_from = instr_from;
-          instr_to = instr_to;
-          latency = latency
-        }:: !latency_constraints
-  and get_last_reads reg =
-    match PTree.get reg !last_reg_reads
-     with Some l -> l
-        | None -> [] in
-  let add_input_mem i =
-    if not (use_alias_analysis ())
-    then
-      begin
-        begin
-          (* Read after write *)
-          match !last_mem_write with
-          | None -> ()
-          | Some j -> add_constraint j i 1
-        end;
-        last_mem_reads := i :: !last_mem_reads
-      end
-  and add_output_mem i =
-    if not (use_alias_analysis ())
-    then
-      begin
-        begin
-          (* Write after write *)
-          match !last_mem_write with
-          | None -> ()
-          | Some j -> add_constraint j i 1
-        end;
-        (* Write after read *)
-        List.iter (fun j -> add_constraint j i 0) !last_mem_reads;
-        last_mem_write := Some i;
-        last_mem_reads := []
-      end
-  and add_input_reg i reg =
-    begin
-      (* Read after write *)
-      match PTree.get reg !last_reg_write with
-      | None -> ()
-      | Some (j, latency) -> add_constraint j i latency
-    end;
-    last_reg_reads := PTree.set reg
-                       (i :: get_last_reads reg)
-                       !last_reg_reads
-  and add_output_reg i latency reg =
-    begin
-      (* Write after write *)
-      match PTree.get reg !last_reg_write with
-      | None -> ()
-      | Some (j, _) -> add_constraint j i 1
-    end;
-    begin
-      (* Write after read *)
-      List.iter (fun j -> add_constraint j i 0) (get_last_reads reg)
-    end;
-    last_reg_write := PTree.set reg (i, latency) !last_reg_write;
-    last_reg_reads := PTree.remove reg !last_reg_reads
-    in
-  let add_input_regs i regs = List.iter (add_input_reg i) regs in
-  let rec add_builtin_res i (res : reg builtin_res) =
-    match res with
-    | BR r -> add_output_reg i 10 r
-    | BR_none -> ()
-    | BR_splitlong (hi, lo) -> add_builtin_res i hi;
-                               add_builtin_res i lo in
-  let rec add_builtin_arg i (ba : reg builtin_arg) =
-    match ba with
-    | BA r -> add_input_reg i r
-    | BA_int _ | BA_long _ | BA_float _ | BA_single _ -> ()
-    | BA_loadstack(_,_) -> add_input_mem i
-    | BA_addrstack _ -> ()
-    | BA_loadglobal(_, _, _) -> add_input_mem i
-    | BA_addrglobal _ -> ()
-    | BA_splitlong(hi, lo) -> add_builtin_arg i hi;
-                              add_builtin_arg i lo
-    | BA_addptr(a1, a2) -> add_builtin_arg i a1;
-                           add_builtin_arg i a2 in
-  let irreversible_action i =
-    match !last_branch with
-    | None -> ()
-    | Some j -> add_constraint j i 1 in
-  let set_branch i =
-    irreversible_action i;
-    last_branch := Some i in
-  let add_non_pipelined_resources i resources =
-    Array.iter2
-      (fun latency last ->
-        if latency >= 0 && last >= 0 then add_constraint last i latency)
-      resources last_non_pipelined_op;
-    Array.iteri (fun rsc latency ->
-        if latency >= 0
-        then last_non_pipelined_op.(rsc) <- i) resources
-  in
-  Array.iteri
-    begin
-      fun i (insn, other_uses) ->
-      List.iter (fun use ->
-          add_input_reg i use)
-        (Regset.elements other_uses);
-      
-      match insn with
-      | Inop _ -> ()
-      | Iop(op, inputs, output, _) ->
-         add_non_pipelined_resources i
-           (opweights.non_pipelined_resources_of_op op (List.length inputs));
-         (if Op.is_trapping_op op then irreversible_action i);
-         add_input_regs i inputs;
-         add_output_reg i (opweights.latency_of_op op (List.length inputs)) output
-      | Iload(trap, chunk, addressing, addr_regs, output, _) ->
-         (if trap=TRAP then irreversible_action i);
-         add_input_mem i;
-         add_input_regs i addr_regs;
-         add_output_reg i (opweights.latency_of_load trap chunk addressing (List.length addr_regs)) output
-      | Istore(chunk, addressing, addr_regs, input, _) ->
-         irreversible_action i;
-         add_input_regs i addr_regs;
-         add_input_reg i input;
-         add_output_mem i
-      | Icall(signature, ef, inputs, output, _) ->
-         set_branch i;
-         (match ef with
-          | Datatypes.Coq_inl r -> add_input_reg i r
-          | Datatypes.Coq_inr symbol -> ()
-         );
-         add_input_mem i;
-         add_input_regs i inputs;
-         add_output_reg i (opweights.latency_of_call signature ef) output;
-         add_output_mem i;
-         failwith "Icall"
-      | Itailcall(signature, ef, inputs) ->
-         set_branch i;
-        (match ef with
-          | Datatypes.Coq_inl r -> add_input_reg i r
-          | Datatypes.Coq_inr symbol -> ()
-         );
-         add_input_mem i;
-         add_input_regs i inputs;
-         failwith "Itailcall"
-      | Ibuiltin(ef, builtin_inputs, builtin_output, _) ->
-         set_branch i;
-         add_input_mem i;
-         List.iter (add_builtin_arg i) builtin_inputs;
-         add_builtin_res i builtin_output;
-         add_output_mem i;
-         failwith "Ibuiltin"
-      | Icond(cond, inputs, _, _, _) ->
-         set_branch i;
-         add_input_mem i;
-         add_input_regs i inputs
-      | Ijumptable(input, _) ->
-         set_branch i;
-         add_input_reg i input;
-         failwith "Ijumptable"
-      | Ireturn(Some input) ->
-         set_branch i;
-         add_input_reg i input;
-         failwith "Ireturn"
-      | Ireturn(None) ->
-         set_branch i;
-         failwith "Ireturn none"
-    end seqa;
-  !latency_constraints;;
-
-let resources_of_instruction (opweights : opweights) = function
-  | Inop _ -> Array.map (fun _ -> 0) opweights.pipelined_resource_bounds
-  | Iop(op, inputs, output, _) ->
-     opweights.resources_of_op op (List.length inputs)
-  | Iload(trap, chunk, addressing, addr_regs, output, _) ->
-     opweights.resources_of_load trap chunk addressing (List.length addr_regs)
-  | Istore(chunk, addressing, addr_regs, input, _) ->
-     opweights.resources_of_store chunk addressing (List.length addr_regs)
-  | Icall(signature, ef, inputs, output, _) ->
-     opweights.resources_of_call signature ef
-  | Ibuiltin(ef, builtin_inputs, builtin_output, _) ->
-     opweights.resources_of_builtin ef
-  | Icond(cond, args, _, _ , _) ->
-     opweights.resources_of_cond cond (List.length args)
-  | Itailcall _ | Ijumptable _ | Ireturn _ -> opweights.pipelined_resource_bounds
-    
-let print_sequence pp (seqa : instruction array) =
-  Array.iteri (
-      fun i (insn : instruction) ->
-      PrintRTL.print_instruction pp (i, insn)) seqa;;
-
-type unique_id = int
-               
-type 'a symbolic_term_node =
-  | STop of Op.operation * 'a list
-  | STinitial_reg of int
-  | STother of int;;
-
-type symbolic_term = {
-    hash_id : unique_id;
-    hash_ct : symbolic_term symbolic_term_node
-  };;
-
-let rec print_term channel term =
-  match term.hash_ct with
-  | STop(op, args) ->
-     PrintOp.print_operation print_term channel (op, args)
-  | STinitial_reg n -> Printf.fprintf channel "x%d" n
-  | STother n -> Printf.fprintf channel "y%d" n;;
-
-type symbolic_term_table = {
-    st_table : (unique_id symbolic_term_node, symbolic_term) Hashtbl.t;
-    mutable st_next_id : unique_id };;
-
-let hash_init () = {
-    st_table = Hashtbl.create 20;
-    st_next_id = 0
-  };;
-
-let ground_to_id = function
-  | STop(op, l) -> STop(op, List.map (fun t -> t.hash_id) l)
-  | STinitial_reg r -> STinitial_reg r
-  | STother i -> STother i;;
-
-let hash_node (table : symbolic_term_table) (term : symbolic_term symbolic_term_node) : symbolic_term =
-  let grounded = ground_to_id term in
-  match Hashtbl.find_opt table.st_table grounded with
-  | Some x -> x
-  | None ->
-     let term' = { hash_id = table.st_next_id;
-                   hash_ct = term } in
-     (if table.st_next_id = max_int then failwith "hash: max_int");
-     table.st_next_id <- table.st_next_id + 1;
-     Hashtbl.add table.st_table grounded term';
-     term';;
-
-type access = {
-    base : symbolic_term;
-    offset : int64;
-    length : int
-  };;
-
-let term_equal a b = (a.hash_id = b.hash_id);;
-
-let access_of_addressing get_reg chunk addressing args =
-  match addressing, args with
-  | (Op.Aindexed ofs), [reg] -> Some
-     { base = get_reg reg;
-       offset = Camlcoq.camlint64_of_ptrofs ofs;
-       length = length_of_chunk chunk
-     }
-  | _, _ -> None ;;
-(* TODO: global *)
-
-let symbolic_execution (seqa : instruction array) =
-  let regs = ref PTree.empty
-  and table = hash_init() in
-  let assign reg term = regs := PTree.set reg term !regs
-  and hash term = hash_node table term in
-  let get_reg reg =
-    match PTree.get reg !regs with
-    | None -> hash (STinitial_reg (Camlcoq.P.to_int reg))
-    | Some x -> x in
-  let targets = Array.make (Array.length seqa) None in
-  Array.iteri
-    begin
-      fun i insn ->
-      match insn with
-      | Iop(Op.Omove, [input], output, _) ->
-         assign output (get_reg input)
-      | Iop(op, inputs, output, _) ->
-         assign output (hash (STop(op, List.map get_reg inputs)))
-
-      | Iload(trap, chunk, addressing, args, output, _) ->
-         let access = access_of_addressing get_reg chunk addressing args in
-         targets.(i) <- access;
-         assign output (hash (STother(i)))
-        
-      | Icall(_, _, _, output, _)
-      | Ibuiltin(_, _, BR output, _) -> 
-         assign output (hash (STother(i)))
-        
-      | Istore(chunk, addressing, args, va, _) ->
-         let access = access_of_addressing get_reg chunk addressing args in
-         targets.(i) <- access
-                                          
-      | Inop _ -> ()
-      | Ibuiltin(_, _, BR_none, _) -> ()
-      | Ibuiltin(_, _, BR_splitlong _, _) -> failwith "BR_splitlong"
-
-      | Itailcall (_, _, _)
-      |Icond (_, _, _, _, _)
-      |Ijumptable (_, _)
-      |Ireturn _ -> ()
-    end seqa;
-  targets;;
-
-let print_access channel = function
-  | None -> Printf.fprintf channel "any"
-  | Some x -> Printf.fprintf channel "%a + %Ld" print_term x.base x.offset;;
-
-let print_targets channel seqa =
-  let targets = symbolic_execution seqa in
-  Array.iteri
-    (fun i insn ->
-      match insn with
-      | Iload _ -> Printf.fprintf channel "%d: load %a\n"
-                      i print_access targets.(i) 
-      | Istore _ -> Printf.fprintf channel "%d: store %a\n"
-                       i print_access targets.(i)
-      | _ -> ()
-    ) seqa;;
-
-let may_overlap a0 b0 =
-  match a0, b0 with
-  | (None, _)  | (_ , None) -> true
-  | (Some a), (Some b) ->
-     if term_equal a.base b.base
-     then (max a.offset b.offset) <
-          (min (Int64.add (Int64.of_int a.length) a.offset)
-               (Int64.add (Int64.of_int b.length) b.offset))
-     else match a.base.hash_ct, b.base.hash_ct with
-          | STop(Op.Oaddrsymbol(ida, ofsa),[]),
-            STop(Op.Oaddrsymbol(idb, ofsb),[]) ->
-             (ida=idb) &&
-               let ao = Int64.add a.offset (Camlcoq.camlint64_of_ptrofs ofsa)
-               and bo = Int64.add b.offset (Camlcoq.camlint64_of_ptrofs ofsb) in
-               (max ao bo) <
-               (min (Int64.add (Int64.of_int a.length) ao)
-                  (Int64.add (Int64.of_int b.length) bo))
-          | STop(Op.Oaddrstack _, []),
-            STop(Op.Oaddrsymbol _, [])
-          | STop(Op.Oaddrsymbol _, []),
-            STop(Op.Oaddrstack _, []) -> false
-          | STop(Op.Oaddrstack(ofsa),[]),
-            STop(Op.Oaddrstack(ofsb),[]) ->
-               let ao = Int64.add a.offset (Camlcoq.camlint64_of_ptrofs ofsa)
-               and bo = Int64.add b.offset (Camlcoq.camlint64_of_ptrofs ofsb) in
-               (max ao bo) <
-               (min (Int64.add (Int64.of_int a.length) ao)
-                  (Int64.add (Int64.of_int b.length) bo))
-          | _ -> true;;
-
-(*
-(* TODO suboptimal quadratic algorithm *)
-let get_alias_dependencies seqa =
-  let targets = symbolic_execution seqa
-  and deps = ref [] in
-  let add_constraint instr_from instr_to latency =
-    deps := { instr_from = instr_from;
-              instr_to = instr_to;
-              latency = latency
-            }:: !deps in
-  for i=0 to (Array.length seqa)-1
-  do
-    for j=0 to i-1
-    do
-      match seqa.(j), seqa.(i) with
-      | (Istore _), ((Iload _) | (Istore _)) ->
-         if may_overlap targets.(j) targets.(i)
-         then add_constraint j i 1
-      | (Iload _), (Istore _) ->
-         if may_overlap targets.(j) targets.(i)
-         then add_constraint j i 0
-      | (Istore _ | Iload _), (Icall _ | Ibuiltin _)
-      | (Icall _ | Ibuiltin _), (Icall _ | Ibuiltin _ | Iload _ | Istore _) ->
-         add_constraint j i 1
-      | (Inop _ | Iop _), _
-      | _, (Inop _ | Iop _)
-      | (Iload _), (Iload _) -> ()
-    done
-  done;
-  !deps;;
- *)
-
-let define_problem (opweights : opweights) (live_entry_regs : Regset.t)
-      (typing : RTLtyping.regenv) reference_counting seqa =
-  let simple_deps = get_simple_dependencies opweights seqa in
-  { max_latency = -1;
-    resource_bounds = opweights.pipelined_resource_bounds;
-    live_regs_entry = live_entry_regs;
-    typing = typing;
-    reference_counting = Some reference_counting;
-      instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa);
-    latency_constraints =
-      (* if (use_alias_analysis ())
-      then (get_alias_dependencies seqa) @ simple_deps
-      else *) simple_deps };;
-
-let zigzag_scheduler problem early_ones =
-  let nr_instructions = get_nr_instructions problem in
-  assert(nr_instructions = (Array.length early_ones));
-  match list_scheduler problem with
-  | Some fwd_schedule ->
-     let fwd_makespan = fwd_schedule.((Array.length fwd_schedule) - 1) in
-     let constraints' = ref problem.latency_constraints in
-     Array.iteri (fun i is_early ->
-         if is_early then
-           constraints' :=  {
-             instr_from = i;
-             instr_to = nr_instructions ;
-             latency = fwd_makespan - fwd_schedule.(i) } ::!constraints' )
-       early_ones;
-     validated_scheduler reverse_list_scheduler
-       { problem with latency_constraints = !constraints' }
-  | None -> None;;
-  
-let prepass_scheduler_by_name name problem early_ones =
-  match name with
-  | "zigzag" -> zigzag_scheduler problem early_ones
-  | _ -> scheduler_by_name name problem
-  
-let schedule_sequence (seqa : (instruction*Regset.t) array)
-      (live_regs_entry : Registers.Regset.t)
-      (typing : RTLtyping.regenv)
-      reference =
-  let opweights = OpWeights.get_opweights () in
-  try
-    if (Array.length seqa) <= 1
-    then None
-    else
-      begin
-      let nr_instructions = Array.length seqa in
-      (if !Clflags.option_debug_compcert > 6
-       then Printf.printf "prepass scheduling length = %d\n" (Array.length seqa));
-      let problem = define_problem opweights live_regs_entry
-                      typing reference seqa in
-      (if !Clflags.option_debug_compcert > 7
-       then (print_sequence stdout (Array.map fst seqa);
-             print_problem stdout problem));
-      match prepass_scheduler_by_name
-              (!Clflags.option_fprepass_sched)
-              problem
-              (Array.map (fun (ins, _) ->
-                   match ins with
-                   | Icond _ -> true
-                   | _ -> false) seqa) with
-      | None -> Printf.printf "no solution in prepass scheduling\n";
-                None
-      | Some solution ->
-         let positions = Array.init nr_instructions (fun i -> i) in
-         Array.sort (fun i j ->
-             let si = solution.(i) and sj = solution.(j) in
-             if si < sj then -1
-             else if si > sj then 1
-             else i - j) positions;
-         Some positions
-    end
-  with (Failure s) ->
-    Printf.printf "failure in prepass scheduling: %s\n" s;
-    None;;
-                                                            
+../aarch64/PrepassSchedulingOracle.ml
\ No newline at end of file
diff --git a/riscV/PrepassSchedulingOracleDeps.ml b/riscV/PrepassSchedulingOracleDeps.ml
index 8d10d406..1e955b85 100644..120000
--- a/riscV/PrepassSchedulingOracleDeps.ml
+++ b/riscV/PrepassSchedulingOracleDeps.ml
@@ -1,17 +1 @@
-type called_function = (Registers.reg, AST.ident) Datatypes.sum
-  
-type opweights =
-  {
-    pipelined_resource_bounds : int array;
-    nr_non_pipelined_units : int;
-    latency_of_op : Op.operation -> int -> int;
-    resources_of_op : Op.operation -> int -> int array;
-    non_pipelined_resources_of_op : Op.operation -> int -> int array;
-    latency_of_load : AST.trapping_mode -> AST.memory_chunk -> Op.addressing -> int -> int;
-    resources_of_load : AST.trapping_mode -> AST.memory_chunk -> Op.addressing -> int -> int array;
-    resources_of_store : AST.memory_chunk -> Op.addressing -> int -> int array;
-    resources_of_cond : Op.condition -> int -> int array;
-    latency_of_call : AST.signature -> called_function -> int;
-    resources_of_call : AST.signature -> called_function -> int array;
-    resources_of_builtin : AST.external_function -> int array
-  };;
+../aarch64/PrepassSchedulingOracleDeps.ml
\ No newline at end of file
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 2739bc5d..2370ad66 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -838,21 +838,6 @@ Proof.
   destruct v; simpl; auto.
 Qed.
 
-(* TODO gourdinl move to common/Values ? *)
-Theorem swap_cmpf_bool:
-  forall c x y,
-  Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x.
-Proof.
-  destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto.
-Qed.
-
-Theorem swap_cmpfs_bool:
-  forall c x y,
-  Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x.
-Proof.
-  destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
-Qed.
-
 (** * Intermediates lemmas on each expanded instruction *)
 
 Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall
@@ -1239,9 +1224,9 @@ Proof.
   unfold Val.cmpf.
   - apply xor_neg_eqne_cmpf.
   - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite swap_cmpf_bool; trivial.
+    rewrite Val.swap_cmpf_bool; trivial.
   - replace (Cle) with (swap_comparison Cge) by auto;
-    rewrite swap_cmpf_bool; trivial.
+    rewrite Val.swap_cmpf_bool; trivial.
 Qed.
 
 Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall
@@ -1290,9 +1275,9 @@ Proof.
   unfold Val.cmpfs.
   - apply xor_neg_eqne_cmpfs.
   - replace (Clt) with (swap_comparison Cgt) by auto;
-    rewrite swap_cmpfs_bool; trivial.
+    rewrite Val.swap_cmpfs_bool; trivial.
   - replace (Cle) with (swap_comparison Cge) by auto;
-    rewrite swap_cmpfs_bool; trivial.
+    rewrite Val.swap_cmpfs_bool; trivial.
 Qed.
 
 Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall