cond and branches expanded

8 files changed, 691 insertions, 293 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index b3fb2350..4b27ee81 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -105,8 +105,8 @@ 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.
+(* TODO REMOVE Definition sltimm32 := opimm32 Psltw Psltiw.*)
+(* TODO REMOVE 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
@@ -132,8 +132,8 @@ 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.
+(* TODO REMOVE Definition sltimm64 := opimm64 Psltl Psltil.*)
+(* TODO REMOVE Definition sltuimm64 := opimm64 Psltul Psltiul.*)
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -145,7 +145,7 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   
 (** Translation of conditional branches. *)
 
-Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+(* TODO REMOVE Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
   match cmp with
   | Ceq => Pbeqw r1 r2 lbl
   | Cne => Pbnew r1 r2 lbl
@@ -203,12 +203,26 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
   | Cle => (Pfles rd fs1 fs2, true)
   | Cgt => (Pflts rd fs2 fs1, true)
   | Cge => (Pfles rd fs2 fs1, true)
+   end.*)
+ 
+Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) :=
+  match optR0 with
+  | None => sem r1 r2 lbl
+  | Some true => sem X0 r1 lbl
+  | Some false => sem r1 X0 lbl
+  end. 
+
+Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) :=
+  match optR0 with
+  | None => sem r1 r2
+  | Some true => sem X0 r1
+  | Some false => sem r1 X0
   end.
-  
+
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
+(* TODO REMOVE | 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 =>
@@ -259,7 +273,44 @@ Definition transl_cbranch
   | 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)
+   OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)*)
+
+  | CEbeqw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k)
+  | CEbnew optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k)
+  | CEbltw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k)
+  | CEbltuw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltuw r1 r2 lbl :: k)
+  | CEbgew optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgew r1 r2 lbl :: k)
+  | CEbgeuw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgeuw r1 r2 lbl :: k)
+  | CEbeql optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k)
+  | CEbnel optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k)
+  | CEbltl optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k)
+  | CEbltul optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltul r1 r2 lbl :: k)
+  | CEbgel optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgel r1 r2 lbl :: k)
+  | CEbgeul optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_cond_branch")
   end.
@@ -268,7 +319,7 @@ Definition transl_cbranch
   [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) :=
+(* TODO REMOVE 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
@@ -342,9 +393,9 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
   match cmp with
   | Clt => sltuimm64 rd r1 n k
   | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
-  end.
+   end. *)
 
-(* TODO Definition transl_cond_op
+(* TODO REMOVE Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
   | Ccomp c, a1 :: a2 :: nil =>
@@ -389,18 +440,11 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
   | _, _ =>
       Error(msg "Asmgen.transl_cond_op")
-              end.*)
+   end.*)
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
   
-Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) :=
-  match optR0 with
-  | None => sem r1 r2
-  | Some true => sem X0 r1
-  | Some false => sem r1 X0
-  end.
-  
 Definition transl_op
               (op: operation) (args: list mreg) (res: mreg) (k: code) :=
   match op, args with
@@ -711,11 +755,9 @@ Definition transl_op
   | Osingleoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
-
-      (* TODO | Ocmp cmp, _ =>
+  (* TODO REMOVE | Ocmp cmp, _ =>
       do rd <- ireg_of res;
-         transl_cond_op cmp rd args k*)
-      
+     transl_cond_op cmp rd args k *)
   | OEseqw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 6bacaa5c..52a3bf27 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -161,7 +161,7 @@ Proof.
 Qed.
 Hint Resolve addptrofs_label: labels.
 
-Remark transl_cond_float_nolabel:
+(* TODO REMOVE Remark transl_cond_float_nolabel:
   forall c r1 r2 r3 insn normal,
   transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
 Proof.
@@ -173,14 +173,14 @@ Remark transl_cond_single_nolabel:
   transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
 Proof.
   unfold transl_cond_single; intros. destruct c; inv H; exact I.
-Qed.
+   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.
-- destruct c0; simpl; TailNoLabel.
+  (* TODO REMOVE - destruct c0; simpl; TailNoLabel.
 - destruct c0; simpl; TailNoLabel.
 - destruct (Int.eq n Int.zero).
   destruct c0; simpl; TailNoLabel.
@@ -211,15 +211,27 @@ Proof.
   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 normal; TailNoLabel.*)
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
+- destruct optR0 as [[]|]; TailNoLabel.
 Qed.
 
-(* TODO Remark transl_cond_op_label:
+(* TODO REMOVE 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.
-  (* TODO - destruct c0; simpl; TailNoLabel.
+- destruct c0; simpl; TailNoLabel.
 - destruct c0; simpl; TailNoLabel. 
 - unfold transl_condimm_int32s.
   destruct (Int.eq n Int.zero).
@@ -254,7 +266,7 @@ Proof.
 + destruct c0; simpl; TailNoLabel.
 + destruct c0; simpl; 
   try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
-     apply opimm64_label; intros; exact I.*)
+     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.
@@ -291,7 +303,7 @@ Opaque Int.eq.
 - 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.
-(* TODO - eapply transl_cond_op_label; eauto.*)
+(* TODO REMOVE - eapply transl_cond_op_label; eauto.*)
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 49635ebd..429c5fec 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -292,7 +292,7 @@ Qed.
 
 (** Translation of conditional branches *)
 
-Lemma transl_cbranch_int32s_correct:
+(* TODO REMOVE 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 =
@@ -375,16 +375,16 @@ Proof.
   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.
+   Qed.*)
 
-Remark branch_on_X31:
+(* TODO 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.
+   Qed.*)
 
 Ltac ArgsInv :=
   repeat (match goal with
@@ -417,7 +417,7 @@ 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.
-- exists rs, (transl_cbranch_int32s c0 x x0 lbl).
+  (* TODO REMOVE - 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.
@@ -492,7 +492,68 @@ Proof.
   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.
+     intros; Simpl.*)
+
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
@@ -528,7 +589,7 @@ Qed.
 
 (** Translation of condition operators *)
 
-Lemma transl_cond_int32s_correct:
+(* TODO REMOVE 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
@@ -830,9 +891,9 @@ Proof.
 + apply DFL.
 + apply DFL.
 + apply DFL.
-Qed.
+   Qed.
 
-(* TODO Lemma transl_cond_op_correct:
+Lemma transl_cond_op_correct:
   forall cond rd args k c rs m,
   transl_cond_op cond rd args k = OK c ->
   exists rs',
@@ -1134,7 +1195,7 @@ Opaque Int.eq.
       apply exec_straight_one. simpl; reflexivity. auto. 
       split; intros; Simpl. }
   (* cond *)
-  (* TODO { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+  (* TODO REMOVE { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
      exists rs'; split. eexact A. eauto with asmgen. }*)
   (* Expanded instructions from RTL *)
   5: econstructor; split; try apply exec_straight_one; simpl; eauto;
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 9e494d0a..af14811d 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,8 +18,6 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
-
-(*open PrintRTL*)
 open! Integers
 
 let reg = ref 1
@@ -102,150 +100,169 @@ let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil
 
 let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
 
-let cond_int32s_x0 cmp a1 dest succ k =
-  match cmp with
-  | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k
-  | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k
-  | Clt -> Iop (OEsltw (Some false), [ a1; a1 ], dest, succ) :: k
-  | Cle ->
-      Iop (OEsltw (Some true), [ a1; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
-  | Cgt -> Iop (OEsltw (Some true), [ a1; a1 ], dest, succ) :: k
-  | Cge ->
-      Iop (OEsltw (Some false), [ a1; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+let is_inv_cmp = function Cle | Cgt -> true | _ -> false
 
-let cond_int32s_reg cmp a1 a2 dest succ k =
-  match cmp with
-  | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k
-  | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k
-  | Clt -> Iop (OEsltw None, [ a1; a2 ], dest, succ) :: k
-  | Cle ->
-      Iop (OEsltw None, [ a2; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
-  | Cgt -> Iop (OEsltw None, [ a2; a1 ], dest, succ) :: k
-  | Cge ->
-      Iop (OEsltw None, [ a1; a2 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None
 
-let cond_int32u_x0 cmp a1 dest succ k =
+let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k
-  | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k
-  | Clt -> Iop (OEsltuw (Some false), [ a1; a1 ], dest, succ) :: k
-  | Cle ->
-      Iop (OEsltuw (Some true), [ a1; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
-  | Cgt -> Iop (OEsltuw (Some true), [ a1; a1 ], dest, succ) :: k
-  | Cge ->
-      Iop (OEsltuw (Some false), [ a1; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
-
-let cond_int32u_reg cmp a1 a2 dest succ k =
+  | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k
-  | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k
-  | Clt -> Iop (OEsltuw None, [ a1; a2 ], dest, succ) :: k
-  | Cle ->
-      Iop (OEsltuw None, [ a2; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
-  | Cgt -> Iop (OEsltuw None, [ a2; a1 ], dest, succ) :: k
-  | Cge ->
-      Iop (OEsltuw None, [ a1; a2 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
-
-let cond_int64s_x0 cmp a1 dest succ k =
+  | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cond_int32s is_x0 cmp a1 a2 dest succ k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Iop (OEseql (Some false), [ a1; a1 ], dest, succ) :: k
-  | Cne -> Iop (OEsnel (Some false), [ a1; a1 ], dest, succ) :: k
-  | Clt -> Iop (OEsltl (Some false), [ a1; a1 ], dest, succ) :: k
+  | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltl (Some true), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltl (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltl (Some false), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
-let cond_int64s_reg cmp a1 a2 dest succ k =
+let cond_int32u is_x0 cmp a1 a2 dest succ k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Iop (OEseql None, [ a1; a2 ], dest, succ) :: k
-  | Cne -> Iop (OEsnel None, [ a1; a2 ], dest, succ) :: k
-  | Clt -> Iop (OEsltl None, [ a1; a2 ], dest, succ) :: k
+  | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltl None, [ a2; a1 ], dest, n2pi ())
+      Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltl None, [ a2; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltl None, [ a1; a2 ], dest, n2pi ())
+      Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
-let cond_int64u_x0 cmp a1 dest succ k =
+let cond_int64s is_x0 cmp a1 a2 dest succ k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Iop (OEseql (Some false), [ a1; a1 ], dest, succ) :: k
-  | Cne -> Iop (OEsnel (Some false), [ a1; a1 ], dest, succ) :: k
-  | Clt -> Iop (OEsltul (Some false), [ a1; a1 ], dest, succ) :: k
+  | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltul (Some true), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltul (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltul (Some false), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
-let cond_int64u_reg cmp a1 a2 dest succ k =
+let cond_int64u is_x0 cmp a1 a2 dest succ k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Iop (OEseql None, [ a1; a2 ], dest, succ) :: k
-  | Cne -> Iop (OEsnel None, [ a1; a2 ], dest, succ) :: k
-  | Clt -> Iop (OEsltul None, [ a1; a2 ], dest, succ) :: k
+  | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltul None, [ a2; a1 ], dest, n2pi ())
+      Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltul None, [ a2; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltul None, [ a1; a2 ], dest, n2pi ())
+      Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
+let is_normal_cmp = function Cne -> false | _ -> true
+
 let cond_float cmp f1 f2 dest succ =
   match cmp with
-  | Ceq -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), true)
-  | Cne -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), false)
-  | Clt -> (Iop (OEfltd, [ f1; f2 ], dest, succ), true)
-  | Cle -> (Iop (OEfled, [ f1; f2 ], dest, succ), true)
-  | Cgt -> (Iop (OEfltd, [ f2; f1 ], dest, succ), true)
-  | Cge -> (Iop (OEfled, [ f2; f1 ], dest, succ), true)
+  | Ceq -> Iop (OEfeqd, [ f1; f2 ], dest, succ)
+  | Cne -> Iop (OEfeqd, [ f1; f2 ], dest, succ)
+  | Clt -> Iop (OEfltd, [ f1; f2 ], dest, succ)
+  | Cle -> Iop (OEfled, [ f1; f2 ], dest, succ)
+  | Cgt -> Iop (OEfltd, [ f2; f1 ], dest, succ)
+  | Cge -> Iop (OEfled, [ f2; f1 ], dest, succ)
 
 let cond_single cmp f1 f2 dest succ =
   match cmp with
-  | Ceq -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), true)
-  | Cne -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), false)
-  | Clt -> (Iop (OEflts, [ f1; f2 ], dest, succ), true)
-  | Cle -> (Iop (OEfles, [ f1; f2 ], dest, succ), true)
-  | Cgt -> (Iop (OEflts, [ f2; f1 ], dest, succ), true)
-  | Cge -> (Iop (OEfles, [ f2; f1 ], dest, succ), true)
+  | Ceq -> Iop (OEfeqs, [ f1; f2 ], dest, succ)
+  | Cne -> Iop (OEfeqs, [ f1; f2 ], dest, succ)
+  | Clt -> Iop (OEflts, [ f1; f2 ], dest, succ)
+  | Cle -> Iop (OEfles, [ f1; f2 ], dest, succ)
+  | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ)
+  | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ)
+
+let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
+  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
+  else (
+    reg := !reg + 1;
+    loadimm32 (r2p ()) n (n2pi ())
+      (cbranch_int32s false cmp a1 (r2p ()) info succ1 succ2 k))
+
+let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
+  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
+  else (
+    reg := !reg + 1;
+    loadimm32 (r2p ()) n (n2pi ())
+      (cbranch_int32u false cmp a1 (r2p ()) info succ1 succ2 k))
+
+let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
+  if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
+  else (
+    reg := !reg + 1;
+    loadimm64 (r2p ()) n (n2pi ())
+      (cbranch_int64s false cmp a1 (r2p ()) info succ1 succ2 k))
+
+let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
+  if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
+  else (
+    reg := !reg + 1;
+    loadimm64 (r2p ()) n (n2pi ())
+      (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_condimm_int32s cmp a1 n dest succ k =
-  if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k
+  if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
-        xorimm32 a1 dest n (n2pi ()) (cond_int32s_x0 cmp dest dest succ k)
+        xorimm32 a1 dest n (n2pi ())
+          (cond_int32s true cmp dest dest dest succ k)
     | Clt -> sltimm32 a1 dest n succ k
     | Cle ->
         if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k
@@ -253,26 +270,26 @@ let expanse_condimm_int32s cmp a1 n dest succ k =
     | _ ->
         reg := !reg + 1;
         loadimm32 (r2p ()) n (n2pi ())
-          (cond_int32s_reg cmp a1 (r2p ()) dest succ k)
+          (cond_int32s false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int32u cmp a1 n dest succ k =
-  if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k
+  if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
   else
     match cmp with
     | Clt -> sltuimm32 a1 dest n succ k
     | _ ->
         reg := !reg + 1;
         loadimm32 (r2p ()) n (n2pi ())
-          (cond_int32u_reg cmp a1 (r2p ()) dest succ k)
+          (cond_int32u false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64s cmp a1 n dest succ k =
-  if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k
+  if Int.eq n Int.zero then cond_int64s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
         reg := !reg + 1;
         xorimm64 a1 (r2p ()) n (n2pi ())
-          (cond_int64s_x0 cmp (r2p ()) dest succ k)
+          (cond_int64s true cmp (r2p ()) (r2p ()) dest succ k)
     | Clt -> sltimm64 a1 dest n succ k
     | Cle ->
         if Int64.eq n (Int64.repr Int64.max_signed) then
@@ -281,47 +298,36 @@ let expanse_condimm_int64s cmp a1 n dest succ k =
     | _ ->
         reg := !reg + 1;
         loadimm64 (r2p ()) n (n2pi ())
-          (cond_int64s_reg cmp a1 (r2p ()) dest succ k)
+          (cond_int64s false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64u cmp a1 n dest succ k =
-  if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k
+  if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
   else
     match cmp with
     | Clt -> sltuimm64 a1 dest n succ k
     | _ ->
         reg := !reg + 1;
         loadimm64 (r2p ()) n (n2pi ())
-          (cond_int64u_reg cmp a1 (r2p ()) dest succ k)
-
-let expanse_cond_float cmp f1 f2 dest succ k =
-  let insn, normal = cond_float cmp f1 f2 dest succ in
-  insn
-  :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
+          (cond_int64u false cmp a1 (r2p ()) dest succ k)
 
-let expanse_cond_not_float cmp f1 f2 dest succ k =
-  let insn, normal = cond_float cmp f1 f2 dest succ in
+let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
+  let normal = is_normal_cmp cmp in
+  let normal' = if cnot then not normal else normal in
+  let succ' = if normal' then succ else n2pi () in
+  let insn = fn_cond cmp f1 f2 dest succ' in
   insn
-  :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k)
+  :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
 
-let expanse_cond_single cmp f1 f2 dest succ k =
-  let insn, normal = cond_single cmp f1 f2 dest succ in
+let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
+  reg := !reg + 1;
+  let normal = is_normal_cmp cmp in
+  let normal' = if cnot then not normal else normal in
+  let insn = fn_cond cmp f1 f2 (r2p ()) (n2pi ()) in
   insn
-  :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
-
-let expanse_cond_not_single cmp f1 f2 dest succ k =
-  let insn, normal = cond_single cmp f1 f2 dest succ in
-  insn
-  :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k)
-
-let rec write_tree exp n code' =
-  match exp with
-  | (Iop (_, _, _, succ) as inst) :: k ->
-      (*print_instruction stderr (0,inst);*)
-      (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*)
-      code' := PTree.set n inst !code';
-      (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*)
-      write_tree k (Camlcoq.P.of_int (Camlcoq.P.to_int n + 1)) code'
-  | _ -> !code'
+  :: (if normal' then
+      Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
+     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info))
+  :: k
 
 let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
 
@@ -339,94 +345,158 @@ let get_regs_inst = function
   | Ireturn (Some r) -> [ r ]
   | _ -> []
 
-let generate_head_order n start_node new_order =
-  Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n)
-    (Camlcoq.P.to_int start_node)
-    !node;
-  for i = !node downto Camlcoq.P.to_int start_node do
-    new_order := !new_order @ [ Camlcoq.P.of_int i ]
-  done;
-  new_order := n :: !new_order
+let rec write_tree' exp current initial code' new_order =
+  if current = !node then (
+    code' := PTree.set initial (Inop (n2p ())) !code';
+    new_order := initial :: !new_order);
+  match exp with
+  | (Iop (_, _, _, succ) as inst) :: k ->
+      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
+      new_order := Camlcoq.P.of_int current :: !new_order;
+      write_tree' k (current - 1) initial code' new_order
+  | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
+      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
+      new_order := Camlcoq.P.of_int current :: !new_order;
+      write_tree' k (current - 1) initial code' new_order
+  | [] -> ()
+  | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
 let expanse (sb : superblock) code =
-  debug_flag := true;
   let new_order = ref [] in
+  let liveins = ref sb.liveins in
   let exp = ref [] in
+  let was_branch = ref false in
   let was_exp = ref false in
   let code' = ref code in
   Array.iter
     (fun n ->
+      was_branch := false;
       was_exp := false;
       let inst = get_some @@ PTree.get n code in
-      let start_node = Camlcoq.P.of_int (!node + 1) in
       (match inst with
       | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
-          Printf.eprintf "Ccomp\n";
-          exp := cond_int32s_reg c a1 a2 dest succ [];
+          debug "Iop/Ccomp\n";
+          exp := cond_int32s false c a1 a2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompu\n";
-          exp := cond_int32u_reg c a1 a2 dest succ [];
+          debug "Iop/Ccompu\n";
+          exp := cond_int32u false c a1 a2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompimm\n";
+          debug "Iop/Ccompimm\n";
           exp := expanse_condimm_int32s c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompuimm\n";
+          debug "Iop/Ccompuimm\n";
           exp := expanse_condimm_int32u c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompl\n";
-          exp := cond_int64s_reg c a1 a2 dest succ [];
+          debug "Iop/Ccompl\n";
+          exp := cond_int64s false c a1 a2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
-          Printf.eprintf "Ccomplu\n";
-          exp := cond_int64u_reg c a1 a2 dest succ [];
+          debug "Iop/Ccomplu\n";
+          exp := cond_int64u false c a1 a2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
-          (*Printf.eprintf "Ccomplimm\n";*)
-          (*Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;*)
-          (*Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;*)
-          (*Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);*)
-          (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*)
-          (*debug "[EXPANSION] Replace this:\n";*)
-          (*print_instruction stderr (0,inst);*)
-          (*debug "[EXPANSION] With:\n";*)
-          (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
-          (*entry := n2p()*)
+          debug "Iop/Ccomplimm\n";
           exp := expanse_condimm_int64s c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompluimm\n";
+          debug "Iop/Ccompluimm\n";
           exp := expanse_condimm_int64u c a1 imm dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompf\n";
-          exp := expanse_cond_float c f1 f2 dest succ [];
+          debug "Iop/Ccompf\n";
+          exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
-          Printf.eprintf "Cnotcompf\n";
-          exp := expanse_cond_not_float c f1 f2 dest succ [];
+          debug "Iop/Cnotcompf\n";
+          exp := expanse_cond_fp true cond_float c f1 f2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompfs\n";
-          exp := expanse_cond_single c f1 f2 dest succ [];
+          debug "Iop/Ccompfs\n";
+          exp := expanse_cond_fp false cond_single c f1 f2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
-          Printf.eprintf "Cnotcompfs\n";
-          exp := expanse_cond_not_single c f1 f2 dest succ [];
+          debug "Iop/Cnotcompfs\n";
+          exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
+          was_exp := true
+      | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccomp\n";
+          exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompu\n";
+          exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompimm\n";
+          exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompuimm\n";
+          exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompl\n";
+          exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccomplu\n";
+          exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccomplimm\n";
+          exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompluimm\n";
+          exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompf\n";
+          exp := expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Cnotcompf\n";
+          exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompfs\n";
+          exp :=
+            expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Cnotcompfs\n";
+          exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
+          was_branch := true;
           was_exp := true
-      | _ -> new_order := !new_order @ [ n ]);
+      | _ -> new_order := n :: !new_order);
       if !was_exp then (
-        code' := write_tree (List.rev !exp) start_node code';
-        let first = Inop (n2pi ()) in
-        code' := PTree.set n first !code';
-        generate_head_order n start_node new_order))
+        node := !node + 1;
+        (if !was_branch then
+         let lives = PTree.get n !liveins in
+         match lives with
+         | Some lives ->
+             liveins := PTree.set (n2p ()) lives !liveins;
+             liveins := PTree.remove n !liveins
+         | _ -> ());
+        write_tree' !exp !node n code' new_order))
     sb.instructions;
-  sb.instructions <- Array.of_list !new_order;
-  (*print_arrayp sb.instructions;*)
-  debug_flag := false;
+  sb.instructions <- Array.of_list (List.rev !new_order);
+  sb.liveins <- !liveins;
   !code'
 
 let rec find_last_node_reg = function
diff --git a/riscV/Op.v b/riscV/Op.v
index 1ca6f2e9..c99c3b43 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -49,7 +49,20 @@ Inductive condition : Type :=
   | Ccompf (c: comparison)      (**r 64-bit floating-point comparison *)
   | Cnotcompf (c: comparison)   (**r negation of a floating-point comparison *)
   | Ccompfs (c: comparison)     (**r 32-bit floating-point comparison *)
-  | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *)
+  | Cnotcompfs (c: comparison)  (**r negation of a floating-point comparison *)
+  (* Expansed branches *)
+  | CEbeqw (optR0: option bool)                      (**r branch-if-equal *)
+  | CEbnew (optR0: option bool)                      (**r branch-if-not-equal signed *)
+  | CEbltw (optR0: option bool)                      (**r branch-if-less signed *)
+  | CEbltuw (optR0: option bool)                     (**r branch-if-less unsigned *)
+  | CEbgew (optR0: option bool)                      (**r branch-if-greater-or-equal signed *)
+  | CEbgeuw (optR0: option bool)                     (**r branch-if-greater-or-equal unsigned *)
+  | CEbeql (optR0: option bool)                      (**r branch-if-equal *)
+  | CEbnel (optR0: option bool)                      (**r branch-if-not-equal signed *)
+  | CEbltl (optR0: option bool)                      (**r branch-if-less signed *)
+  | CEbltul (optR0: option bool)                     (**r branch-if-less unsigned *)
+  | CEbgel (optR0: option bool)                      (**r branch-if-greater-or-equal signed *)
+  | CEbgeul (optR0: option bool).                    (**r branch-if-greater-or-equal unsigned *)
 
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
@@ -153,6 +166,7 @@ Inductive operation : Type :=
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  (* Expansed conditions *)
   | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
   | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
   | OEsltw (optR0: option bool)                  (**r set-less-than *)
@@ -191,9 +205,10 @@ Inductive addressing: Type :=
 
 Definition eq_condition (x y: condition) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec; intro.
+  generalize Int.eq_dec Int64.eq_dec bool_dec; intros.
   assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
   decide equality.
+  all: destruct optR0, optR1; decide equality.
 Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
@@ -254,6 +269,19 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
   | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
   | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
+  (* Expansed branches *)
+  | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32
+  | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32
+  | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32
+  | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32
+  | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32
+  | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32
+  | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64
+  | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64
+  | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64
+  | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64
+  | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64
+  | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64
   | _, _ => None
   end.
 
@@ -354,6 +382,7 @@ Definition eval_operation
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
+  (* Expansed conditions *)
   | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
   | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
   | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32)
@@ -438,6 +467,18 @@ Definition type_of_condition (c: condition) : list typ :=
   | Cnotcompf _ => Tfloat :: Tfloat :: nil
   | Ccompfs _ => Tsingle :: Tsingle :: nil
   | Cnotcompfs _ => Tsingle :: Tsingle :: nil
+  | CEbeqw _ => Tint :: Tint :: nil
+  | CEbnew _ => Tint :: Tint :: nil
+  | CEbltw _ => Tint :: Tint :: nil
+  | CEbltuw _ => Tint :: Tint :: nil
+  | CEbgew _ => Tint :: Tint :: nil
+  | CEbgeuw _ => Tint :: Tint :: nil
+  | CEbeql _ => Tlong :: Tlong :: nil
+  | CEbnel _ => Tlong :: Tlong :: nil
+  | CEbltl _ => Tlong :: Tlong :: nil
+  | CEbltul _ => Tlong :: Tlong :: nil
+  | CEbgel _ => Tlong :: Tlong :: nil
+  | CEbgeul _ => Tlong :: Tlong :: nil
   end.
 
 Definition type_of_operation (op: operation) : list typ * typ :=
@@ -766,48 +807,72 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
-  
-- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
-  destruct Val.cmpu_bool... all: destruct b...
-- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
-  destruct Val.cmpu_bool... all: destruct b...
-- destruct optR0 as [[]|]; simpl; unfold Val.cmp;
-  destruct Val.cmp_bool... all: destruct b...
-- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
-  destruct Val.cmpu_bool... all: destruct b...
-- unfold Val.cmp; destruct Val.cmp_bool...
-  all: destruct b...
-- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
-- destruct v0...
-- trivial.
-- trivial.
-- destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
-  destruct Val.cmplu_bool... all: destruct b...
-- destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
-  destruct Val.cmplu_bool... all: destruct b...
-- destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
-  destruct Val.cmpl_bool... all: destruct b...
-- destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
-  destruct Val.cmplu_bool... all: destruct b...
-- unfold Val.cmpl; destruct Val.cmpl_bool...
-  all: destruct b...
-- unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
-- destruct v0...
-- trivial.
-- trivial.
-- trivial.
-- destruct v0; destruct v1; cbn; auto.
-  destruct Float.cmp; cbn; auto.
-- destruct v0; destruct v1; cbn; auto.
-  destruct Float.cmp; cbn; auto.
-- destruct v0; destruct v1; cbn; auto.
-  destruct Float.cmp; cbn; auto.
-- destruct v0; destruct v1; cbn; auto.
-  destruct Float32.cmp; cbn; auto.
-- destruct v0; destruct v1; cbn; auto.
-  destruct Float32.cmp; cbn; auto.
-- destruct v0; destruct v1; cbn; auto.
-  destruct Float32.cmp; cbn; auto.
+  (* OEseqw *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+    destruct Val.cmpu_bool... all: destruct b...
+  (* OEsnew *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+    destruct Val.cmpu_bool... all: destruct b...
+  (* OEsltw *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmp;
+    destruct Val.cmp_bool... all: destruct b...
+  (* OEsltuw *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+    destruct Val.cmpu_bool... all: destruct b...
+  (* OEsltiw *)
+  - unfold Val.cmp; destruct Val.cmp_bool...
+    all: destruct b...
+  (* OEsltiuw *)
+  - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
+  (* OExoriw *)
+  - destruct v0...
+  (* OEluiw *)
+  - trivial.
+  (* OEaddiwr0 *)
+  - trivial.
+  (* OEseql *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
+    destruct Val.cmplu_bool... all: destruct b...
+  (* OEsnel *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
+    destruct Val.cmplu_bool... all: destruct b...
+  (* OEsltl *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
+    destruct Val.cmpl_bool... all: destruct b...
+  (* OEsltul *)
+  - destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
+    destruct Val.cmplu_bool... all: destruct b...
+  (* OEsltil *)
+  - unfold Val.cmpl; destruct Val.cmpl_bool...
+    all: destruct b...
+  (* OEsltiul *)
+  - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
+  (* OExoril *)
+  - destruct v0...
+  (* OEluil *)
+  - trivial.
+  (* OEaddilr0 *)
+  - trivial.
+  (* OEloadli *)
+  - trivial.
+  (* OEfeqd *)
+  - destruct v0; destruct v1; cbn; auto.
+    destruct Float.cmp; cbn; auto.
+  (* OEfltd *)
+  - destruct v0; destruct v1; cbn; auto.
+    destruct Float.cmp; cbn; auto.
+  (* OEfled *)
+  - destruct v0; destruct v1; cbn; auto.
+    destruct Float.cmp; cbn; auto.
+  (* OEfeqs *)
+  - destruct v0; destruct v1; cbn; auto.
+    destruct Float32.cmp; cbn; auto.
+  (* OEflts *)
+  - destruct v0; destruct v1; cbn; auto.
+    destruct Float32.cmp; cbn; auto.
+  (* OEfles *)
+  - destruct v0; destruct v1; cbn; auto.
+    destruct Float32.cmp; cbn; auto.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -877,6 +942,18 @@ Definition negate_condition (cond: condition): condition :=
   | Cnotcompf c => Ccompf c
   | Ccompfs c => Cnotcompfs c
   | Cnotcompfs c => Ccompfs c
+  | CEbeqw optR0 => CEbnew optR0
+  | CEbnew optR0 => CEbeqw optR0
+  | CEbltw optR0 => CEbgew optR0
+  | CEbltuw optR0 => CEbgeuw optR0
+  | CEbgew optR0 => CEbltw optR0
+  | CEbgeuw optR0 => CEbltuw optR0
+  | CEbeql optR0 => CEbnel optR0
+  | CEbnel optR0 => CEbeql optR0
+  | CEbltl optR0 => CEbgel optR0
+  | CEbltul optR0 => CEbgeul optR0
+  | CEbgel optR0 => CEbltl optR0
+  | CEbgeul optR0 => CEbltul optR0
   end.
 
 Lemma eval_negate_condition:
@@ -896,6 +973,31 @@ Proof.
   repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto.
   repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto.
+
+  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmp_bool.
+  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmplu_bool.
+  repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmplu_bool.
+  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmplu_bool.
+  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|];
+  apply Val.negate_cmplu_bool.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
@@ -992,6 +1094,14 @@ Definition cond_depends_on_memory (cond : condition) : bool :=
   | Ccompuimm _ _ => negb Archi.ptr64
   | Ccomplu _ => Archi.ptr64
   | Ccompluimm _ _ => Archi.ptr64
+  | CEbeqw _ => negb Archi.ptr64
+  | CEbnew _ => negb Archi.ptr64
+  | CEbltuw _ => negb Archi.ptr64
+  | CEbgeuw _ => negb Archi.ptr64
+  | CEbeql _ => Archi.ptr64
+  | CEbnel _ => Archi.ptr64
+  | CEbltul _ => Archi.ptr64
+  | CEbgeul _ => Archi.ptr64
   | _ => false
   end.
 
@@ -1043,7 +1153,9 @@ Lemma cond_valid_pointer_eq:
 Proof.
   intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
   all: repeat (destruct args; simpl; try congruence);
-    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+       try destruct optR0 as [[]|]; simpl;
+       try destruct v, v0; try rewrite !MEM; auto;
+       try erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.
  
 Lemma op_valid_pointer_eq:
@@ -1052,8 +1164,7 @@ Lemma op_valid_pointer_eq:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence.
-  intros MEM; destruct cond; repeat (destruct args; simpl; try congruence);
-    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+  intro MEM; erewrite cond_valid_pointer_eq; eauto.
   all: intros MEM; repeat (destruct args; simpl; try congruence);
        try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto;
        unfold Val.cmpu, Val.cmplu;
@@ -1164,27 +1275,6 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Lemma eval_condition_inj:
-  forall cond vl1 vl2 b,
-  Val.inject_list f vl1 vl2 ->
-  eval_condition cond vl1 m1 = Some b ->
-  eval_condition cond vl2 m2 = Some b.
-Proof.
-  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; simpl in H0; inv H0; auto.
-- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; simpl in H0; inv H0; auto.
-- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-Qed.
-
 Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0',
   Val.inject f v v' ->
   Val.inject f v0 v0' ->
@@ -1267,6 +1357,54 @@ Proof.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
 Qed.
 
+Lemma eval_condition_inj:
+  forall cond vl1 vl2 b,
+  Val.inject_list f vl1 vl2 ->
+  eval_condition cond vl1 m1 = Some b ->
+  eval_condition cond vl2 m2 = Some b.
+Proof.
+  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
+  all: assert (HVI32: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int;
+       assert (HVI64: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long;
+       try unfold zero32, zero64.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmpu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmpu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; simpl;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmpu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; simpl;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmpu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmplu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmplu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; simpl;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmplu_bool_inj'; eauto.
+- destruct optR0 as [[]|]; simpl;
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+- destruct optR0 as [[]|]; unfold apply_bin_r0 in *;
+  eapply eval_cmplu_bool_inj'; eauto.
+Qed.
+
 Ltac TrivialExists :=
   match goal with
   | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
@@ -1473,35 +1611,54 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
-
+  (* OEseqw *)
   - apply eval_cmpu_bool_inj_opt; auto.
+  (* OEsnew *)
   - apply eval_cmpu_bool_inj_opt; auto.
+  (* OEsltw *)
   - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
     inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto;
     try apply Val.inject_int.
+  (* OEsltuw *)
   - apply eval_cmpu_bool_inj_opt; auto.
+  (* OEsltiw *)
   - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
+  (* OEsltiuw *)
   - apply eval_cmpu_bool_inj; auto.
+  (* OExoriw *)
   - inv H4; simpl; auto.
+  (* OEseql *)
   - apply eval_cmplu_bool_inj_opt; auto.
+  (* OEsnel *)
   - apply eval_cmplu_bool_inj_opt; auto.
+  (* OEsltl *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
     inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto;
     try apply Val.inject_int.
+  (* OEsltul *)
   - apply eval_cmplu_bool_inj_opt; auto.
+  (* OEsltil *)
   - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int.
+  (* OEsltiul *)
   - apply eval_cmplu_bool_inj; auto.
+  (* OExoril *)
   - inv H4; simpl; auto.
+  (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* OEfltd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* OEfled *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* OEfeqs *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* OEflts *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* OEfles *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
 Qed.
diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 75a913c6..09760db9 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -56,7 +56,19 @@ module Rocket =
             | Ccompl _
             | Ccomplu _
             | Ccomplimm _
-            | Ccompluimm _ -> 1
+            | Ccompluimm _
+            | CEbeqw _
+            | CEbnew _
+            | CEbltw _
+            | CEbltuw _
+            | CEbgew _
+            | CEbgeuw _ 
+            | CEbeql _
+            | CEbnel _
+            | CEbltl _
+            | CEbltul _
+            | CEbgel _
+            | CEbgeul _ -> 1
           | Ccompf _
             | Cnotcompf _ -> 6
           | Ccompfs _
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index c222f777..2b5ae1f5 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -60,6 +60,30 @@ let print_condition reg pp = function
       fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2
   | (Cnotcompfs c, [r1;r2]) ->
       fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2
+  | (CEbeqw optR0, [r1;r2]) ->
+      fprintf pp "CEbeqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
+  | (CEbnew optR0, [r1;r2]) ->
+      fprintf pp "CEbnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
+  | (CEbltw optR0, [r1;r2]) ->
+      fprintf pp "CEbltw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbltuw optR0, [r1;r2]) ->
+      fprintf pp "CEbltuw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbgew optR0, [r1;r2]) ->
+      fprintf pp "CEbgew"; (get_optR0_s Cge reg pp r1 r2 optR0)
+  | (CEbgeuw optR0, [r1;r2]) ->
+      fprintf pp "CEbgeuw"; (get_optR0_s Cge reg pp r1 r2 optR0)
+  | (CEbeql optR0, [r1;r2]) ->
+      fprintf pp "CEbeql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
+  | (CEbnel optR0, [r1;r2]) ->
+      fprintf pp "CEbnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
+  | (CEbltl optR0, [r1;r2]) ->
+      fprintf pp "CEbltl"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbltul optR0, [r1;r2]) ->
+      fprintf pp "CEbltul"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbgel optR0, [r1;r2]) ->
+      fprintf pp "CEbgel"; (get_optR0_s Cge reg pp r1 r2 optR0)
+  | (CEbgeul optR0, [r1;r2]) ->
+      fprintf pp "CEbgeul"; (get_optR0_s Cge reg pp r1 r2 optR0)
   | _ ->
       fprintf pp "<bad condition>"
 
@@ -180,6 +204,12 @@ let print_operation reg pp = function
   | OEluil n, [] -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
   | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n)
   | OEloadli n, [] -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
+  | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
+  | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
+  | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
+  | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
+  | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
+  | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 4880a929..ece28eff 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -41,6 +41,18 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
   | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
   | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
   | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
+  | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32
+  | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32
+  | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32
+  | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32
+  | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32
+  | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32
+  | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64
+  | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64
+  | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64
+  | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64
+  | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64
+  | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cge) v1 v2 zero64
   | _, _ => Bnone
   end.
 
@@ -194,7 +206,9 @@ Proof.
   destruct cond; simpl; eauto with va.
   inv H2.
   destruct cond; simpl; eauto with va.
-  destruct cond; auto with va.
+  13: destruct cond; simpl; eauto with va.
+  all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0;
+       unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va.
 Qed.
 
 Lemma symbol_address_sound: