All Ocmp expanded in RTL

7 files changed, 417 insertions, 202 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index f702d11a..b3fb2350 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -344,10 +344,10 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
   | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
   end.
 
-Definition transl_cond_op
+(* TODO Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
-  (* TODO | Ccomp c, a1 :: a2 :: nil =>
+  | 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 =>
@@ -370,7 +370,7 @@ Definition transl_cond_op
       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)*)
+     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
@@ -386,10 +386,10 @@ Definition transl_cond_op
   | 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)
+     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]. *)
@@ -712,9 +712,9 @@ Definition transl_op
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
 
-  | Ocmp cmp, _ =>
+      (* TODO | 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;
@@ -795,6 +795,36 @@ Definition transl_op
   | OEloadli n, nil =>
       do rd <- ireg_of res;
       OK (Ploadli rd n :: k)
+  | OEfeqd, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfeqd rd r1 r2 :: k)
+  | OEfltd, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfltd rd r1 r2 :: k)
+  | OEfled, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfled rd r1 r2 :: k)
+  | OEfeqs, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfeqs rd r1 r2 :: k)
+  | OEflts, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pflts rd r1 r2 :: k)
+  | OEfles, f1 :: f2 :: nil =>
+      do rd <- ireg_of res;
+      do r1 <- freg_of f1;
+      do r2 <- freg_of f2;
+      OK (Pfles rd r1 r2 :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 63ceed0d..6bacaa5c 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -214,7 +214,7 @@ Proof.
   destruct normal; TailNoLabel.
 Qed.
 
-Remark transl_cond_op_label:
+(* TODO 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.
@@ -267,7 +267,7 @@ Proof.
 - 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.
+   Qed.*)
 
 Remark transl_op_label:
   forall op args r k c,
@@ -291,7 +291,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.
-- eapply transl_cond_op_label; eauto.
+(* TODO - 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 ee203da4..49635ebd 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -832,7 +832,7 @@ Proof.
 + apply DFL.
 Qed.
 
-Lemma transl_cond_op_correct:
+(* TODO Lemma transl_cond_op_correct:
   forall cond rd args k c rs m,
   transl_cond_op cond rd args k = OK c ->
   exists rs',
@@ -844,7 +844,7 @@ Proof.
   { destruct ob as [[]|]; reflexivity. }
   intros until m; intros TR.
   destruct cond; simpl in TR; ArgsInv.
-(* TODO + (* cmp *)
++ (* 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).
@@ -866,7 +866,7 @@ Proof.
 + (* 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.*)
+   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)).
@@ -923,7 +923,7 @@ Proof.
 * econstructor; split.
   apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
   split; intros; Simpl.
-Qed.
+   Qed.*)
 
 (** Some arithmetic properties. *)
 
@@ -1134,8 +1134,8 @@ Opaque Int.eq.
       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. }
+  (* TODO { 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;
   split; intros; Simpl; rewrite Int.add_commut; auto.
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index c3f2cb3f..9e494d0a 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,40 +18,46 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
+
 (*open PrintRTL*)
 open! Integers
 
 let reg = ref 1
+
 let node = ref 1
 
 let r2p () = Camlcoq.P.of_int !reg
+
 let n2p () = Camlcoq.P.of_int !node
-let n2pi () = node := !node + 1; n2p()
+
+let n2pi () =
+  node := !node + 1;
+  n2p ()
 
 type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
 let load_hilo32 dest hi lo succ k =
-  if Int.eq lo Int.zero then
-    Iop (OEluiw hi, [], dest, succ) :: k
-  else (
-      Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)
+  if Int.eq lo Int.zero then Iop (OEluiw hi, [], dest, succ) :: k
+  else
+    Iop (OEluiw hi, [], dest, n2pi ())
+    :: Iop (Oaddimm lo, [ dest ], dest, succ)
+    :: k
 
 let load_hilo64 dest hi lo succ k =
-  if Int64.eq lo Int64.zero then
-    Iop (OEluil hi, [], dest, succ) :: k
-  else (
-      Iop (OEluil hi, [], dest, n2pi()) :: (Iop (Oaddlimm lo, [dest], dest, succ)) :: k)
+  if Int64.eq lo Int64.zero then Iop (OEluil hi, [], dest, succ) :: k
+  else
+    Iop (OEluil hi, [], dest, n2pi ())
+    :: Iop (Oaddlimm lo, [ dest ], dest, succ)
+    :: k
 
 let loadimm32 dest n succ k =
   match make_immed32 n with
-  | Imm32_single imm ->
-      Iop (OEaddiwr0 imm, [], dest, succ) :: k
+  | Imm32_single imm -> Iop (OEaddiwr0 imm, [], dest, succ) :: k
   | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k
 
 let loadimm64 dest n succ k =
   match make_immed64 n with
-  | Imm64_single imm ->
-      Iop (OEaddilr0 imm, [], dest, succ) :: k
+  | Imm64_single imm -> Iop (OEaddilr0 imm, [], dest, succ) :: k
   | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k
   | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
 
@@ -65,236 +71,359 @@ let get_opimm imm = function
 
 let opimm32 a1 dest n succ k op opimm =
   match make_immed32 n with
-  | Imm32_single imm ->
-      Iop (get_opimm imm opimm, [a1], dest, succ) :: k
+  | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
+      load_hilo32 (r2p ()) hi lo (n2pi ())
+        (Iop (op, [ a1; r2p () ], dest, succ) :: k)
 
 let opimm64 a1 dest n succ k op opimm =
   match make_immed64 n with
-  | Imm64_single imm ->
-      Iop (get_opimm imm opimm, [a1], dest, succ) :: k
+  | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm64_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo64 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
-  | Imm64_large imm  ->
+      load_hilo64 (r2p ()) hi lo (n2pi ())
+        (Iop (op, [ a1; r2p () ], dest, succ) :: k)
+  | Imm64_large imm ->
       reg := !reg + 1;
-      Iop (OEloadli imm, [], r2p(), n2pi()) :: Iop (op, [a1;r2p()], dest, succ) :: k
+      Iop (OEloadli imm, [], r2p (), n2pi ())
+      :: Iop (op, [ a1; r2p () ], dest, succ)
+      :: k
 
 let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw
+
 let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw
+
 let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw
+
 let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
+
 let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil
+
 let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
 
 let 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
+  | 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 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
+  | 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 cond_int32u_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 (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
+  | 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 =
   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
+  | 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 =
   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
-  | Cle -> Iop (OEsltl (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
-  | Cgt -> Iop (OEsltl (Some true), [a1;a1], dest, succ) :: k
-  | Cge -> Iop (OEsltl (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | 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
+  | Cle ->
+      Iop (OEsltl (Some true), [ a1; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
+  | Cgt -> Iop (OEsltl (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cge ->
+      Iop (OEsltl (Some false), [ a1; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
 
 let cond_int64s_reg cmp a1 a2 dest succ k =
   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
-  | Cle -> Iop (OEsltl None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
-  | Cgt -> Iop (OEsltl None, [a2;a1], dest, succ) :: k
-  | Cge -> Iop (OEsltl None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | 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
+  | Cle ->
+      Iop (OEsltl None, [ a2; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
+  | Cgt -> Iop (OEsltl None, [ a2; a1 ], dest, succ) :: k
+  | Cge ->
+      Iop (OEsltl None, [ a1; a2 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
 
 let cond_int64u_x0 cmp a1 dest succ k =
   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
-  | Cle -> Iop (OEsltul (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
-  | Cgt -> Iop (OEsltul (Some true), [a1;a1], dest, succ) :: k
-  | Cge -> Iop (OEsltul (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | 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
+  | Cle ->
+      Iop (OEsltul (Some true), [ a1; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
+  | Cgt -> Iop (OEsltul (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cge ->
+      Iop (OEsltul (Some false), [ a1; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
 
 let cond_int64u_reg cmp a1 a2 dest succ k =
   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
-  | Cle -> Iop (OEsltul None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
-  | Cgt -> Iop (OEsltul None, [a2;a1], dest, succ) :: k
-  | Cge -> Iop (OEsltul None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | 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
+  | Cle ->
+      Iop (OEsltul None, [ a2; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
+  | Cgt -> Iop (OEsltul None, [ a2; a1 ], dest, succ) :: k
+  | Cge ->
+      Iop (OEsltul None, [ a1; a2 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: 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 else
+let cond_float cmp f1 f2 dest succ =
   match cmp with
-  | Ceq | Cne ->
-      xorimm32 a1 dest n (n2pi()) (cond_int32s_x0 cmp 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
-            else sltimm32 a1 dest (Int.add n Int.one) succ k
-  | _   -> reg := !reg + 1;
-           loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k)
+  | 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)
 
-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 else
+let cond_single cmp f1 f2 dest succ =
   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)
+  | 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)
+
+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
+  else
+    match cmp with
+    | Ceq | Cne ->
+        xorimm32 a1 dest n (n2pi ()) (cond_int32s_x0 cmp 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
+        else sltimm32 a1 dest (Int.add n Int.one) succ k
+    | _ ->
+        reg := !reg + 1;
+        loadimm32 (r2p ()) n (n2pi ())
+          (cond_int32s_reg 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
+  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)
 
 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 else
-  match cmp with
-  | Ceq | Cne ->
-      reg := !reg + 1;
-      xorimm64 a1 (r2p()) n (n2pi()) (cond_int64s_x0 cmp (r2p()) dest succ k)
-  | Clt -> sltimm64 a1 dest n succ k
-  | Cle -> if Int64.eq n (Int64.repr Int64.max_signed)
-           then loadimm32 dest Int.one succ k
-            else sltimm64 a1 dest (Int64.add n Int64.one) succ k
-  | _   -> reg := !reg + 1;
-           loadimm64 (r2p()) n (n2pi()) (cond_int64s_reg cmp a1 (r2p()) dest succ k)
- 
+  if Int.eq n Int.zero then cond_int64s_x0 cmp 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)
+    | Clt -> sltimm64 a1 dest n succ k
+    | Cle ->
+        if Int64.eq n (Int64.repr Int64.max_signed) then
+          loadimm32 dest Int.one succ k
+        else sltimm64 a1 dest (Int64.add n Int64.one) succ k
+    | _ ->
+        reg := !reg + 1;
+        loadimm64 (r2p ()) n (n2pi ())
+          (cond_int64s_reg 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 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)
+  if Int64.eq n Int64.zero then cond_int64u_x0 cmp 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)
+
+let expanse_cond_not_float cmp f1 f2 dest succ k =
+  let insn, normal = cond_float cmp f1 f2 dest succ in
+  insn
+  :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k)
+
+let expanse_cond_single cmp f1 f2 dest succ k =
+  let insn, normal = cond_single cmp f1 f2 dest succ 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 ->
+  | (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'
+      write_tree k (Camlcoq.P.of_int (Camlcoq.P.to_int n + 1)) code'
   | _ -> !code'
 
-let get_regindent = function
-  | Coq_inr _ -> []
-  | Coq_inl r -> [r]
-  
+let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
+
 let get_regs_inst = function
-  | Inop (_) -> []
-  | Iop (_,args,dest,_) -> dest :: args
-  | Iload (_,_,_,args,dest,_) -> dest :: args
-  | Istore (_,_,args,src,_) -> src :: args
-  | Icall (_,t,args,dest,_) -> dest :: ((get_regindent t) @ args)
-  | Itailcall (_,t,args) -> (get_regindent t) @ args
-  | Ibuiltin (_,args,dest,_) ->
-      (AST.params_of_builtin_res dest) @
-      AST.params_of_builtin_args args
-  | Icond (_,args,_,_,_) -> args
-  | Ijumptable (arg,_) -> [arg]
-  | Ireturn (Some r) -> [r]
+  | Inop _ -> []
+  | Iop (_, args, dest, _) -> dest :: args
+  | Iload (_, _, _, args, dest, _) -> dest :: args
+  | Istore (_, _, args, src, _) -> src :: args
+  | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args)
+  | Itailcall (_, t, args) -> get_regindent t @ args
+  | Ibuiltin (_, args, dest, _) ->
+      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
+  | Icond (_, args, _, _, _) -> args
+  | Ijumptable (arg, _) -> [ arg ]
+  | Ireturn (Some r) -> [ r ]
   | _ -> []
 
 let 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];
+  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 expanse (sb: superblock) code =
+let expanse (sb : superblock) code =
   debug_flag := true;
   let new_order = ref [] in
   let exp = ref [] in
   let was_exp = ref false in
   let code' = ref code in
-  Array.iter (fun n ->
-    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 [];
-      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 [];
-      was_exp := true)
-    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
-      Printf.eprintf "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";
-      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 [];
-      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 [];
-      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()*)
-      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";
-      exp := expanse_condimm_int64u c a1 imm dest succ [];
-      was_exp := true)
-    | _ -> new_order := !new_order @ [n]);
-    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)
-  ) sb.instructions;
+  Array.iter
+    (fun n ->
+      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 [];
+          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 [];
+          was_exp := true
+      | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
+          Printf.eprintf "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";
+          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 [];
+          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 [];
+          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()*)
+          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";
+          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 [];
+          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 [];
+          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 [];
+          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 [];
+          was_exp := true
+      | _ -> new_order := !new_order @ [ n ]);
+      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))
+    sb.instructions;
   sb.instructions <- Array.of_list !new_order;
   (*print_arrayp sb.instructions;*)
   debug_flag := false;
@@ -303,12 +432,13 @@ let expanse (sb: superblock) code =
 let rec find_last_node_reg = function
   | [] -> ()
   | (pc, i) :: k ->
-    let rec traverse_list var = function
-    | [] -> ()
-    | e :: t ->
-        (let e' = Camlcoq.P.to_int e in
-        if e' > !var then var := e';
-        traverse_list var t) in
-    traverse_list node [pc];
-    traverse_list reg (get_regs_inst i);
-    find_last_node_reg k
+      let rec traverse_list var = function
+        | [] -> ()
+        | e :: t ->
+            let e' = Camlcoq.P.to_int e in
+            if e' > !var then var := e';
+            traverse_list var t
+      in
+      traverse_list node [ pc ];
+      traverse_list reg (get_regs_inst i);
+      find_last_node_reg k
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 67940c47..db8b68ef 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -106,6 +106,12 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEluil n => op1 (default nv)
   | OEaddilr0 n => op1 (modarith nv)
   | OEloadli n => op1 (default nv)
+  | OEfeqd => op2 (default nv)
+  | OEfltd => op2 (default nv)
+  | OEfled => op2 (default nv)
+  | OEfeqs => op2 (default nv)
+  | OEflts => op2 (default nv)
+  | OEfles => op2 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
diff --git a/riscV/Op.v b/riscV/Op.v
index ae38f361..1ca6f2e9 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -171,7 +171,13 @@ Inductive operation : Type :=
   | OExoril (n: int64)                           (**r xor immediate *)
   | OEluil (n: int64)                            (**r load upper-immediate *)
   | OEaddilr0 (n: int64)                         (**r add immediate *)
-  | OEloadli (n: int64).                         (**r load an immediate int64 *)
+  | OEloadli (n: int64)                          (**r load an immediate int64 *)
+  | OEfeqd                                       (**r compare equal *)
+  | OEfltd                                       (**r compare less-than *)
+  | OEfled                                       (**r compare less-than/equal *)
+  | OEfeqs                                       (**r compare equal *)
+  | OEflts                                       (**r compare less-than *)
+  | OEfles.                                      (**r compare less-than/equal *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -367,6 +373,12 @@ Definition eval_operation
   | OEluil n, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
   | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
   | OEloadli n, nil => Some (Vlong n)
+  | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
+  | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
+  | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2)
+  | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2)
+  | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2)
+  | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2)
   | _, _ => None
   end.
 
@@ -542,6 +554,12 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEluil _ => (nil, Tlong)
   | OEaddilr0 _ => (nil, Tlong)
   | OEloadli _ => (nil, Tlong)
+  | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
+  | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
+  | OEfled => (Tfloat :: Tfloat :: nil, Tint)
+  | OEfeqs => (Tsingle :: Tsingle :: nil, Tint)
+  | OEflts => (Tsingle :: Tsingle :: nil, Tint)
+  | OEfles => (Tsingle :: Tsingle :: nil, Tint)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -778,6 +796,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
 - 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.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1462,6 +1492,18 @@ Proof.
   - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int.
   - apply eval_cmplu_bool_inj; auto.
   - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; simpl; auto.
+    destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  - inv H4; inv H2; cbn; simpl; auto.
+    destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  - inv H4; inv H2; cbn; simpl; auto.
+    destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  - inv H4; inv H2; cbn; simpl; auto.
+    destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  - inv H4; inv H2; cbn; simpl; auto.
+    destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  - inv H4; inv H2; cbn; simpl; auto.
+    destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 9218d80d..4880a929 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -166,6 +166,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEluil n, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
   | OEaddilr0 n, nil => addl (L n) zero64
   | OEloadli n, nil => L (n)
+  | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
+  | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
+  | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2)
+  | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2)
+  | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2)
+  | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2)
   | _, _ => Vbot
   end.
 
@@ -317,6 +323,7 @@ Proof.
   unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va.
   unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va.
   unfold zero64; simpl. eauto with va.
+  all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
 Qed.
 
 End SOUNDNESS.