All Ocmp expanded in RTL

1 files changed, 43 insertions, 1 deletions

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: