Adding both RV expansion methods in kvx-work

6 files changed, 1406 insertions, 48 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 3f9d3359..c5cd6817 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -23,7 +23,6 @@ open Asm
 open Asmexpandaux
 open AST
 open Camlcoq
-open Asmgen
 open! Integers
 
 exception Error of string
@@ -45,13 +44,11 @@ let align n a = (n + a - 1) land (-a)
 (* Emit instruction sequences that set or offset a register by a constant. *)
 
 let expand_loadimm32 dst n =
-  match make_immed32 n with
-  | Imm32_single imm -> emit (Paddiw (dst, X0, imm))
-  | Imm32_pair (hi, lo) -> List.iter emit (load_hilo32 dst hi lo [])
+  List.iter emit (Asmgen.loadimm32 dst n [])
 let expand_addptrofs dst src n =
-  List.iter emit (addptrofs dst src n [])
+  List.iter emit (Asmgen.addptrofs dst src n [])
 let expand_storeind_ptr src base ofs =
-  List.iter emit (storeind_ptr src base ofs [])
+  List.iter emit (Asmgen.storeind_ptr src base ofs [])
 
 (* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index da6c0101..3e84e950 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -86,6 +86,12 @@ Definition make_immed64 (val: int64) :=
 Definition load_hilo32 (r: ireg) (hi lo: int) k :=
   if Int.eq lo Int.zero then Pluiw r hi :: k
   else Pluiw r hi :: Paddiw r r lo :: k.
+  
+Definition loadimm32 (r: ireg) (n: int) (k: code) :=
+  match make_immed32 n with
+  | Imm32_single imm => Paddiw r X0 imm :: k
+  | Imm32_pair hi lo => load_hilo32 r hi lo k
+  end.
 
 Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
                    (opimm: ireg -> ireg0 -> int -> instruction)
@@ -96,11 +102,23 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction)
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
+Definition andimm32 := opimm32 Pandw Pandiw.
+Definition orimm32  := opimm32 Porw  Poriw.
+Definition xorimm32 := opimm32 Pxorw Pxoriw.
+Definition sltimm32 := opimm32 Psltw Psltiw.
+Definition sltuimm32 := opimm32 Psltuw Psltiuw.
   
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
   else Pluil r hi :: Paddil r r lo :: k.
 
+Definition loadimm64 (r: ireg) (n: int64) (k: code) :=
+  match make_immed64 n with
+  | Imm64_single imm => Paddil r X0 imm :: k
+  | Imm64_pair hi lo => load_hilo64 r hi lo k
+  | Imm64_large imm  => Ploadli r imm :: k
+  end.
+
 Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
                    (opimm: ireg -> ireg0 -> int64 -> instruction)
                    (rd rs: ireg) (n: int64) (k: code) :=
@@ -111,6 +129,11 @@ Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
   end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
+Definition andimm64 := opimm64 Pandl Pandil.
+Definition orimm64  := opimm64 Porl  Poril.
+Definition xorimm64 := opimm64 Pxorl  Pxoril.
+Definition sltimm64 := opimm64 Psltl Psltil.
+Definition sltuimm64 := opimm64 Psltul Psltiul.
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -120,6 +143,68 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
     then addimm64 rd rs (Ptrofs.to_int64 n) k
     else addimm32 rd rs (Ptrofs.to_int n) k.
   
+(** Translation of conditional branches. *)
+
+Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeqw r1 r2 lbl
+  | Cne => Pbnew r1 r2 lbl
+  | Clt => Pbltw r1 r2 lbl
+  | Cle => Pbgew r2 r1 lbl
+  | Cgt => Pbltw r2 r1 lbl
+  | Cge => Pbgew r1 r2 lbl
+  end.
+
+Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeqw  r1 r2 lbl
+  | Cne => Pbnew  r1 r2 lbl
+  | Clt => Pbltuw r1 r2 lbl
+  | Cle => Pbgeuw r2 r1 lbl
+  | Cgt => Pbltuw r2 r1 lbl
+  | Cge => Pbgeuw r1 r2 lbl
+  end.
+
+Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeql r1 r2 lbl
+  | Cne => Pbnel r1 r2 lbl
+  | Clt => Pbltl r1 r2 lbl
+  | Cle => Pbgel r2 r1 lbl
+  | Cgt => Pbltl r2 r1 lbl
+  | Cge => Pbgel r1 r2 lbl
+  end.
+
+Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeql  r1 r2 lbl
+  | Cne => Pbnel  r1 r2 lbl
+  | Clt => Pbltul r1 r2 lbl
+  | Cle => Pbgeul r2 r1 lbl
+  | Cgt => Pbltul r2 r1 lbl
+  | Cge => Pbgeul r1 r2 lbl
+  end.
+
+Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
+  match cmp with
+  | Ceq => (Pfeqd rd fs1 fs2, true)
+  | Cne => (Pfeqd rd fs1 fs2, false)
+  | Clt => (Pfltd rd fs1 fs2, true)
+  | Cle => (Pfled rd fs1 fs2, true)
+  | Cgt => (Pfltd rd fs2 fs1, true)
+  | Cge => (Pfled rd fs2 fs1, true)
+  end.
+  
+Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
+  match cmp with
+  | Ceq => (Pfeqs rd fs1 fs2, true)
+  | Cne => (Pfeqs rd fs1 fs2, false)
+  | Clt => (Pflts rd fs1 fs2, true)
+  | Cle => (Pfles rd fs1 fs2, true)
+  | Cgt => (Pflts rd fs2 fs1, true)
+  | Cge => (Pfles rd fs2 fs1, true)
+   end.
+
 (** Functions to select a special register according to the op "oreg" argument from RTL *)
 
 Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
@@ -138,6 +223,59 @@ Definition get_oreg (optR: option oreg) (r: ireg0) :=
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
+  | Ccomp c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int32s c r1 r2 lbl :: k)
+  | Ccompu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int32u c r1 r2 lbl :: k)
+  | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int.eq n Int.zero then
+            transl_cbranch_int32s c r1 X0 lbl :: k
+          else
+            loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k))
+  | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int.eq n Int.zero then
+            transl_cbranch_int32u c r1 X0 lbl :: k
+          else
+            loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k))
+  | Ccompl c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int64s c r1 r2 lbl :: k)
+  | Ccomplu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int64u c r1 r2 lbl :: k)
+  | Ccomplimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int64.eq n Int64.zero then
+            transl_cbranch_int64s c r1 X0 lbl :: k
+          else
+            loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k))
+  | Ccompluimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int64.eq n Int64.zero then
+            transl_cbranch_int64u c r1 X0 lbl :: k
+          else
+            loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k))
+  | Ccompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c X31 r1 r2 in
+      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
+  | Cnotcompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c X31 r1 r2 in
+      OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
+  | Ccompfs c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_single c X31 r1 r2 in
+      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
+  | Cnotcompfs c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_single c X31 r1 r2 in
+   OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
+
   | CEbeqw optR, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in
@@ -206,6 +344,133 @@ Definition transl_cbranch
       Error(msg "Asmgen.transl_cond_branch")
   end.
 
+(** Translation of a condition operator.  The generated code sets the
+  [rd] target register to 0 or 1 depending on the truth value of the
+  condition. *)
+
+Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseqw rd r1 r2 :: k
+  | Cne => Psnew rd r1 r2 :: k
+  | Clt => Psltw rd r1 r2 :: k
+  | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltw rd r2 r1 :: k
+  | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseqw rd r1 r2 :: k
+  | Cne => Psnew rd r1 r2 :: k
+  | Clt => Psltuw rd r1 r2 :: k
+  | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltuw rd r2 r1 :: k
+  | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseql rd r1 r2 :: k
+  | Cne => Psnel rd r1 r2 :: k
+  | Clt => Psltl rd r1 r2 :: k
+  | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltl rd r2 r1 :: k
+  | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseql rd r1 r2 :: k
+  | Cne => Psnel rd r1 r2 :: k
+  | Clt => Psltul rd r1 r2 :: k
+  | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltul rd r2 r1 :: k
+  | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
+  if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else
+  match cmp with
+  | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k)
+  | Clt => sltimm32 rd r1 n k
+  | Cle => if Int.eq n (Int.repr Int.max_signed)
+           then loadimm32 rd Int.one k
+           else sltimm32 rd r1 (Int.add n Int.one) k
+  | _   => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)
+  end.
+
+Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
+  if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else
+  match cmp with
+  | Clt => sltuimm32 rd r1 n k
+  | _   => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)
+  end.
+
+Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
+  if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else
+  match cmp with
+  | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k)
+  | Clt => sltimm64 rd r1 n k
+  | Cle => if Int64.eq n (Int64.repr Int64.max_signed)
+           then loadimm32 rd Int.one k
+           else sltimm64 rd r1 (Int64.add n Int64.one) k
+  | _   => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)
+  end.
+
+Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
+  if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else
+  match cmp with
+  | Clt => sltuimm64 rd r1 n k
+  | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
+   end.
+
+Definition transl_cond_op
+           (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
+  match cond, args with
+  | Ccomp c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int32s c rd r1 r2 k)
+  | Ccompu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int32u c rd r1 r2 k)
+  | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int32s c rd r1 n k)
+  | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int32u c rd r1 n k)
+  | Ccompl c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int64s c rd r1 r2 k)
+  | Ccomplu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+     OK (transl_cond_int64u c rd r1 r2 k)
+  | Ccomplimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int64s c rd r1 n k)
+  | Ccompluimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+     OK (transl_condimm_int64u c rd r1 n k)
+  | Ccompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c rd r1 r2 in
+      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
+  | Cnotcompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c rd r1 r2 in
+      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
+  | Ccompfs c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_single c rd r1 r2 in
+      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
+  | Cnotcompfs c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_single c rd r1 r2 in
+     OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
+  | _, _ =>
+      Error(msg "Asmgen.transl_cond_op")
+   end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
   
@@ -218,6 +483,22 @@ Definition transl_op
       | FR r, FR a => OK (Pfmv r a :: k)
       |  _  ,  _   => Error(msg "Asmgen.Omove")
       end
+  | Ointconst n, nil =>
+      do rd <- ireg_of res;
+      OK (loadimm32 rd n k)
+  | Olongconst n, nil =>
+      do rd <- ireg_of res;
+      OK (loadimm64 rd n k)
+  | Ofloatconst f, nil =>
+      do rd <- freg_of res;
+      OK (if Float.eq_dec f Float.zero
+          then Pfcvtdw rd X0 :: k
+          else Ploadfi rd f :: k)
+  | Osingleconst f, nil =>
+      do rd <- freg_of res;
+      OK (if Float32.eq_dec f Float32.zero
+          then Pfcvtsw rd X0 :: k
+          else Ploadsi rd f :: k)
   | Oaddrsymbol s ofs, nil =>
       do rd <- ireg_of res;
       OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
@@ -227,9 +508,18 @@ Definition transl_op
       do rd <- ireg_of res;
       OK (addptrofs rd SP n k)
 
+  | Ocast8signed, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k)
+  | Ocast16signed, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k)
   | Oadd, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Paddw rd rs1 rs2 :: k)
+  | Oaddimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (addimm32 rd rs n k)
   | Oneg, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Psubw rd X0 rs :: k)
@@ -260,12 +550,21 @@ Definition transl_op
   | Oand, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandw rd rs1 rs2 :: k)
+  | Oandimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (andimm32 rd rs n k)
   | Oor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porw rd rs1 rs2 :: k)
+  | Oorimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (orimm32 rd rs n k)
   | Oxor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pxorw rd rs1 rs2 :: k)
+  | Oxorimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (xorimm32 rd rs n k)
   | Oshl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psllw rd rs1 rs2 :: k)
@@ -284,6 +583,19 @@ Definition transl_op
   | Oshruimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrliw rd rs n :: k)
+  | Oshrximm n, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- ireg_of a1;
+        OK (if Int.eq n Int.zero
+            then Pmv rd rs :: k
+            else if Int.eq n Int.one
+                 then Psrliw X31 rs (Int.repr 31) ::
+                      Paddw X31 rs X31 ::
+                      Psraiw rd X31 Int.one :: k
+                 else Psraiw X31 rs (Int.repr 31) ::
+                      Psrliw X31 X31 (Int.sub Int.iwordsize n) ::
+                      Paddw X31 rs X31 ::
+                      Psraiw rd X31 n :: k)  
+
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
@@ -292,9 +604,16 @@ Definition transl_op
       do rd <- ireg_of res; do rs <- ireg_of a1;
       assertion (ireg_eq rd rs);
       OK (Pcvtw2l rd :: k)
+  | Ocast32unsigned, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- ireg_of a1;
+      assertion (ireg_eq rd rs);
+      OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k)
   | Oaddl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Paddl rd rs1 rs2 :: k)
+  | Oaddlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (addimm64 rd rs n k)
   | Onegl, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Psubl rd X0 rs :: k)
@@ -325,12 +644,21 @@ Definition transl_op
   | Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandl rd rs1 rs2 :: k)
+  | Oandlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (andimm64 rd rs n k)
   | Oorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porl rd rs1 rs2 :: k)
+  | Oorlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (orimm64 rd rs n k)
   | Oxorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pxorl rd rs1 rs2 :: k)
+  | Oxorlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (xorimm64 rd rs n k)
   | Oshll, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pslll rd rs1 rs2 :: k)
@@ -349,6 +677,19 @@ Definition transl_op
   | Oshrluimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrlil rd rs n :: k)
+  | Oshrxlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- ireg_of a1;
+        OK (if Int.eq n Int.zero
+            then Pmv rd rs :: k
+            else if Int.eq n Int.one
+                 then Psrlil X31 rs (Int.repr 63) ::
+                      Paddl X31 rs X31 ::
+                      Psrail rd X31 Int.one :: k
+                 else Psrail X31 rs (Int.repr 63) ::
+                      Psrlil X31 X31 (Int.sub Int64.iwordsize' n) ::
+                      Paddl X31 rs X31 ::
+                      Psrail rd X31 n :: k)  
+
   | Onegf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfnegd rd rs :: k)
@@ -443,6 +784,9 @@ Definition transl_op
   | Osingleoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
+  | Ocmp cmp, _ =>
+      do rd <- ireg_of res;
+     transl_cond_op cmp rd args k
 
   (* Instructions expanded in RTL *)
   | OEseqw optR, a1 :: a2 :: nil =>
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 4af8352c..509eac94 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -115,6 +115,14 @@ Qed.
 
 Section TRANSL_LABEL.
 
+Remark loadimm32_label:
+  forall r n k, tail_nolabel k (loadimm32 r n k).
+Proof.
+  intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.
+  unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.
+Qed.
+Hint Resolve loadimm32_label: labels.
+
 Remark opimm32_label:
   forall op opimm r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
@@ -126,6 +134,14 @@ Proof.
 Qed.
 Hint Resolve opimm32_label: labels.
 
+Remark loadimm64_label:
+  forall r n k, tail_nolabel k (loadimm64 r n k).
+Proof.
+  intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.
+  unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.
+Qed.
+Hint Resolve loadimm64_label: labels.
+
 Remark opimm64_label:
   forall op opimm r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
@@ -145,25 +161,165 @@ Proof.
 Qed.
 Hint Resolve addptrofs_label: labels.
 
+Remark transl_cond_float_nolabel:
+  forall c r1 r2 r3 insn normal,
+  transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
+Proof.
+  unfold transl_cond_float; intros. destruct c; inv H; exact I.
+Qed.
+
+Remark transl_cond_single_nolabel:
+  forall c r1 r2 r3 insn normal,
+  transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
+Proof.
+  unfold transl_cond_single; intros. destruct c; inv H; exact I.
+   Qed.
+
 Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
-  all: destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
+- destruct (Int.eq n Int.zero).
+  destruct c0; simpl; TailNoLabel.
+  apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
+  auto with labels. destruct c0; simpl; TailNoLabel.
+- destruct (Int.eq n Int.zero).
+  destruct c0; simpl; TailNoLabel.
+  apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
+  auto with labels. destruct c0; simpl; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
+- destruct (Int64.eq n Int64.zero).
+  destruct c0; simpl; TailNoLabel.
+  apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
+  auto with labels. destruct c0; simpl; TailNoLabel.
+- destruct (Int64.eq n Int64.zero).
+  destruct c0; simpl; TailNoLabel.
+  apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
+  auto with labels. destruct c0; simpl; TailNoLabel.
+- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
+     destruct normal; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
 Qed.
 
+Remark transl_cond_op_label:
+  forall cond args r k c,
+  transl_cond_op cond r args k = OK c -> tail_nolabel k c.
+Proof.
+  intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
+- destruct c0; simpl; TailNoLabel. 
+- unfold transl_condimm_int32s.
+  destruct (Int.eq n Int.zero).
++ destruct c0; simpl; TailNoLabel.
++ destruct c0; simpl.
+* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
+* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
+* apply opimm32_label; intros; exact I.
+* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I.
+* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
+* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
+- unfold transl_condimm_int32u.
+  destruct (Int.eq n Int.zero).
++ destruct c0; simpl; TailNoLabel.
++ destruct c0; simpl; 
+  try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]).
+  apply opimm32_label; intros; exact I.
+- destruct c0; simpl; TailNoLabel.
+     - destruct c0; simpl; TailNoLabel.
+- unfold transl_condimm_int64s.
+  destruct (Int64.eq n Int64.zero).
++ destruct c0; simpl; TailNoLabel.
++ destruct c0; simpl.
+* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
+* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
+* apply opimm64_label; intros; exact I.
+* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I.
+* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
+* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
+- unfold transl_condimm_int64u.
+  destruct (Int64.eq n Int64.zero).
++ destruct c0; simpl; TailNoLabel.
++ destruct c0; simpl; 
+  try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
+     apply opimm64_label; intros; exact I.
+- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
+  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
+  destruct normal; TailNoLabel.
+   Qed.
+
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
 Opaque Int.eq.
-  unfold transl_op; intros; destruct op; TailNoLabel;
-  try (destruct optR as [[]|]; simpl in *; TailNoLabel).
+  unfold transl_op; intros; destruct op; TailNoLabel.
 - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
+- destruct (Float.eq_dec n Float.zero); TailNoLabel.
+- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
 - destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
 + TailNoLabel. 
+- apply opimm32_label; intros; exact I.
+- apply opimm32_label; intros; exact I.
+- apply opimm32_label; intros; exact I.
+- apply opimm32_label; intros; exact I.
+- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
+- apply opimm64_label; intros; exact I.
+- apply opimm64_label; intros; exact I.
+- apply opimm64_label; intros; exact I.
+- apply opimm64_label; intros; exact I.
+- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
+- eapply transl_cond_op_label; eauto.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label:
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index faa066b0..2293e001 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -129,6 +129,22 @@ Proof.
   intros; Simpl.
 Qed.
 
+Lemma loadimm32_correct:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge fn (loadimm32 rd n k) rs m k rs' m
+  /\ rs'#rd = Vint n
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
+Proof.
+  unfold loadimm32; intros. generalize (make_immed32_sound n); intros E.
+  destruct (make_immed32 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. rewrite Int.add_zero_l; Simpl. 
+  intros; Simpl.
+- rewrite E. apply load_hilo32_correct.
+Qed.
+
 Lemma opimm32_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
          (opi: ireg -> ireg0 -> int -> instruction)
@@ -179,6 +195,27 @@ Proof.
   intros; Simpl.
 Qed.
 
+Lemma loadimm64_correct:
+  forall rd n k rs m,
+  exists rs',
+     exec_straight ge fn (loadimm64 rd n k) rs m k rs' m
+  /\ rs'#rd = Vlong n
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  unfold loadimm64; intros. generalize (make_immed64_sound n); intros E.
+  destruct (make_immed64 n). 
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. rewrite Int64.add_zero_l; Simpl. 
+  intros; Simpl.
+- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C).
+  rewrite E. exists rs'; eauto.
+- subst imm. econstructor; split. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. 
+  intros; Simpl.
+Qed.
+
 Lemma opimm64_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
          (opi: ireg -> ireg0 -> int64 -> instruction)
@@ -253,6 +290,102 @@ Proof.
   rewrite H0 in B. inv B. auto.
 Qed.
 
+(** Translation of conditional branches *)
+
+Lemma transl_cbranch_int32s_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
+Proof.
+  intros. destruct cmp; simpl; rewrite ? H.
+- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
+  simpl; auto.
+- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
+  simpl; auto.
+- auto.
+- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
+- auto.
+Qed.
+
+Lemma transl_cbranch_int32u_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
+Proof.
+  intros. destruct cmp; simpl; rewrite ? H; auto.
+- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
+Qed.
+
+Lemma transl_cbranch_int64s_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
+Proof.
+  intros. destruct cmp; simpl; rewrite ? H.
+- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
+  simpl; auto.
+- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
+  simpl; auto.
+- auto.
+- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
+- auto.
+Qed.
+
+Lemma transl_cbranch_int64u_correct:
+  forall cmp r1 r2 lbl (rs: regset) m b,
+  Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
+  exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
+Proof.
+  intros. destruct cmp; simpl; rewrite ? H; auto.
+- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
+- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
+Qed.
+
+Lemma transl_cond_float_correct:
+  forall (rs: regset) m cmp rd r1 r2 insn normal v,
+  transl_cond_float cmp rd r1 r2 = (insn, normal) ->
+  v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) ->
+  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
+Proof.
+  intros. destruct cmp; simpl in H; inv H; auto. 
+- rewrite Val.negate_cmpf_eq. auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
+  rewrite <- Float.cmp_swap. auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
+  rewrite <- Float.cmp_swap. auto.
+Qed.
+
+Lemma transl_cond_single_correct:
+  forall (rs: regset) m cmp rd r1 r2 insn normal v,
+  transl_cond_single cmp rd r1 r2 = (insn, normal) ->
+  v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) ->
+  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
+Proof.
+  intros. destruct cmp; simpl in H; inv H; auto. 
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
+  rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
+  rewrite <- Float32.cmp_swap. auto.
+- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
+  rewrite <- Float32.cmp_swap. auto.
+   Qed.
+
+(* TODO gourdinl UNUSUED ? Remark branch_on_X31:
+  forall normal lbl (rs: regset) m b,
+  rs#X31 = Val.of_bool (eqb normal b) -> 
+  exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
+  eval_branch fn lbl rs m (Some b).
+Proof.
+  intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
+   Qed.*)
+
 Ltac ArgsInv :=
   repeat (match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -284,46 +417,219 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
-  all:
-    destruct optR as [[]|];
-    unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
-    unfold zero32, Op.zero32 in *;
-    unfold zero64, Op.zero64 in *; inv EQ2;
-    try (destruct (rs x); simpl in EVAL'; discriminate; fail);
-    try (eexists; eexists; eauto; split; constructor;
-    simpl in *; try rewrite EVAL'; auto; fail).
-  all:
-    destruct (rs x) eqn:EQRS; simpl in *; try congruence;
-    eexists; eexists; eauto; split; constructor; auto;
-    simpl in *; rewrite EQRS.
-  - assert (HB: (Int.eq Int.zero i) = b) by congruence;
+  - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
+- exists rs, (transl_cbranch_int32u c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
+- predSpec Int.eq Int.eq_spec n Int.zero.
++ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
++ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int32s c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int32s_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- predSpec Int.eq Int.eq_spec n Int.zero.
++ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
++ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int32u c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int32u_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- exists rs, (transl_cbranch_int64s c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
+- exists rs, (transl_cbranch_int64u c0 x x0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
+- predSpec Int64.eq Int64.eq_spec n Int64.zero.
++ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
++ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int64s c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int64s_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- predSpec Int64.eq Int64.eq_spec n Int64.zero.
++ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl).
+  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
++ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
+  exists rs', (transl_cbranch_int64u c0 x X31 lbl).
+  split. constructor; eexact A. split; auto.
+  apply transl_cbranch_int64u_correct; auto.
+  simpl; rewrite B, C; eauto with asmgen.
+- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (eqb normal b)).
+  { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+  intros; Simpl.
+- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)).
+  { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
+  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (xorb normal b)).
+  { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+  intros; Simpl.
+- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (eqb normal b)).
+  { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+  intros; Simpl.
+- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
+  assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)).
+  { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
+  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
+  assert (V: v = Val.of_bool (xorb normal b)).
+  { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. }
+  econstructor; econstructor.
+  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split. rewrite V; destruct normal, b; reflexivity.
+     intros; Simpl.
+
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
+  simpl in *.
+  + rewrite EQRS;
+    assert (HB: (Int.eq Int.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  - assert (HB: (Int.eq i Int.zero) = b) by congruence.
+  + rewrite EQRS;
+    assert (HB: (Int.eq i Int.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - destruct (rs x0); try congruence.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
     assert (HB: (Int.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
+  simpl in *.
+  + rewrite EQRS;
+    assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  - assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
+  + rewrite EQRS;
+    assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - destruct (rs x0); try congruence.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
     assert (HB: negb (Int.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; auto.
+  + rewrite EQRS;
+    assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  - assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
+  + rewrite EQRS;
+    assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - destruct (rs x0); try congruence.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
     assert (HB: (Int64.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; auto.
+  + rewrite EQRS;
+    assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
+  + rewrite EQRS;
+    assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
-  - destruct (rs x0); try congruence.
+  + rewrite EQRS;
+    destruct (rs x0); try congruence.
     assert (HB: negb (Int64.eq i i0) = b) by congruence.
     rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+  try (destruct (rs x); simpl in EVAL'; discriminate; fail);
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
@@ -357,6 +663,417 @@ Proof.
   intros; Simpl. 
 Qed.
 
+(** Translation of condition operators *)
+
+Lemma transl_cond_int32s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
+  /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
+  simpl. rewrite (Val.negate_cmp_bool Clt). 
+  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
+  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_cond_int32u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
+  /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
+  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_cond_int64s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
+  simpl. rewrite (Val.negate_cmpl_bool Clt). 
+  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
+  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_cond_int64u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
+  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
+  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_condimm_int32s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int32s.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
+  exists rs'; eauto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ unfold xorimm32. 
+  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ unfold xorimm32. 
+  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
+* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
+  unfold Int.lt. rewrite zlt_false. auto. 
+  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
+  generalize (Int.signed_range i); omega.
+* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); 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 omega. auto.
+  rewrite zlt_true by omega. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); omega.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_condimm_int32u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int32u.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto. rewrite B; auto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ apply DFL.
++ apply DFL.
++ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
+  intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ apply DFL.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_condimm_int64s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int64s.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
+  exists rs'; eauto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ unfold xorimm64. 
+  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ unfold xorimm64. 
+  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
+* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
+  unfold Int64.lt. rewrite zlt_false. auto. 
+  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
+  generalize (Int64.signed_range i); omega.
+* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); 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 omega. auto.
+  rewrite zlt_true by omega. auto.
+  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
+  assert (Int64.signed n <> Int64.max_signed).
+  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
+  generalize (Int64.signed_range n); omega.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_condimm_int64u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int64u.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto. rewrite B; auto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ apply DFL.
++ apply DFL.
++ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
+  intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ apply DFL.
++ apply DFL.
++ apply DFL.
+   Qed.
+
+Lemma transl_cond_op_correct:
+  forall cond rd args k c rs m,
+  transl_cond_op cond rd args k = OK c ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m
+  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
+  { destruct ob as [[]|]; reflexivity. }
+  intros until m; intros TR.
+  destruct cond; simpl in TR; ArgsInv.
++ (* cmp *)
+  exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpu *)
+  exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite B; auto.
++ (* cmpimm *)
+  apply transl_condimm_int32s_correct; eauto with asmgen.
++ (* cmpuimm *)
+  apply transl_condimm_int32u_correct; eauto with asmgen.
++ (* cmpl *)
+  exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmplu *)
+  exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
+   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
++ (* cmplimm *)
+  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
+  intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpluimm *)
+  exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
+  intros (rs' & A & B & C).
+   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpf *)
+  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
+  fold (Val.cmpf c0 (rs x) (rs x0)).
+  set (v := Val.cmpf c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split; intros; Simpl.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
++ (* notcmpf *)
+  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
+  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
+  set (v := Val.cmpf c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_float_correct with (v := v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
+  split; intros; Simpl.
++ (* cmpfs *)
+  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
+  fold (Val.cmpfs c0 (rs x) (rs x0)).
+  set (v := Val.cmpfs c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split; intros; Simpl.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
++ (* notcmpfs *)
+  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
+  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
+  set (v := Val.cmpfs c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_single_correct with (v := v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
+  split; intros; Simpl.
+   Qed.
+
+(** Some arithmetic properties. *)
+
+Remark cast32unsigned_from_cast32signed:
+  forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
+Proof.
+  intros. apply Int64.same_bits_eq; intros. 
+  rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto.
+  rewrite Int.bits_signed by tauto. fold (Int.testbit i i0).
+  change Int.zwordsize with 32.
+  destruct (zlt i0 32). auto. apply Int.bits_above. auto.
+Qed.
+
 (* Translation of arithmetic operations *)
 
 Ltac SimplEval H :=
@@ -386,6 +1103,28 @@ Opaque Int.eq.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
   (* move *)
   { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. }
+  (* intconst *)
+  { exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* longconst *)
+  { exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* floatconst *)
+  { destruct (Float.eq_dec n Float.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* singleconst *)
+  { destruct (Float32.eq_dec n Float32.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
   (* addrsymbol *)
   { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
     + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
@@ -402,6 +1141,138 @@ Opaque Int.eq.
   (* stackoffset *)
   { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
   exists rs'; split; eauto. auto with asmgen. }
+  (* cast8signed *)
+  { econstructor; split.
+  eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
+  split; intros; Simpl.
+  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
+  destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* cast16signed *)
+  { econstructor; split.
+  eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
+  split; intros; Simpl.
+  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
+  destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* addimm *)
+  { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
+  exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen.
+  { intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrximm *)
+  { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
+    {
+    exploit Val.shrx_shr_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* longofintu *)
+  { econstructor; split.
+  eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
+  split; intros; Simpl. destruct (rs x0); auto. simpl. 
+  assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
+  rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
+  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. }
+  (* addlimm *)
+  { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
+  { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
+  intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrxlimm *)
+  { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
+    {
+     exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* cond *)
+  { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+     exists rs'; split. eexact A. eauto with asmgen. }
   (* Expanded instructions from RTL *)
   9,10,19,20:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 5d739375..1384b9b3 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -116,8 +116,7 @@ let forget_reg vn rd =
       print_list_pos old_regs;
       Hashtbl.replace !vn.nval v
         (List.filter (fun n -> not (P.eq n rd)) old_regs)
-  | None ->
-      debug "forget_reg: no mapping for r=%d\n" (p2i rd)
+  | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd)
 
 let update_reg vn rd v =
   debug "update_reg: update v=%d with r=%d\n" v (p2i rd);
@@ -696,8 +695,9 @@ let expanse (sb : superblock) code pm =
       was_branch := false;
       was_exp := false;
       let inst = get_some @@ PTree.get n code in
-      debug "We are checking node %d\n" (p2i n);
-      (match inst with
+      (if !Clflags.option_fexpanse_rtlcond then
+         debug "We are checking node %d\n" (p2i n);
+       match inst with
        (* Expansion of conditions - Ocmp *)
        | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
            debug "Iop/Ccomp\n";
@@ -824,7 +824,7 @@ let expanse (sb : superblock) code pm =
            was_branch := true;
            was_exp := true
        | _ -> ());
-      (if not !was_exp then
+      (if !Clflags.option_fexpanse_others && not !was_exp then
        match inst with
        | Iop (Ofloatconst f, nil, dest, succ) ->
            debug "Iop/Ofloatconst\n";
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 7aca1772..ca049962 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -853,16 +853,6 @@ Proof.
   destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
 Qed.
 
-Remark cast32unsigned_from_cast32signed:
-  forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)).
-Proof.
-  intros. apply Int64.same_bits_eq; intros. 
-  rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto.
-  rewrite Int.bits_signed by tauto. fold (Int.testbit i i0).
-  change Int.zwordsize with 32.
-  destruct (zlt i0 32). auto. apply Int.bits_above. auto.
-Qed.
-
 (** * Intermediates lemmas on each expanded instruction *)
 
 Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall