Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work

1 files changed, 42 insertions, 2 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index cd74080f..4c2390a1 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -32,6 +32,7 @@
 Require Import BoolEqual Coqlib.
 Require Import AST Integers Floats.
 Require Import Values Memory Globalenvs Events.
+Require ExtValues.
 
 Set Implicit Arguments.
 
@@ -200,6 +201,12 @@ Inductive operation : Type :=
   | OEfeqs                                       (**r compare equal *)
   | OEflts                                       (**r compare less-than *)
   | OEfles.                                      (**r compare less-than/equal *)
+  | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Obits_of_single
+  | Obits_of_float
+  | Osingle_of_bits
+  | Ofloat_of_bits
+  | Oselectl.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -411,6 +418,10 @@ Definition eval_operation
   | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
+  | Obits_of_single, v1::nil => Some (ExtValues.bits_of_single v1)
+  | Obits_of_float, v1::nil => Some (ExtValues.bits_of_float v1)
+  | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1)
+  | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits 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.cmp Ceq) v1 v2 zero32)
@@ -442,6 +453,7 @@ Definition eval_operation
   | 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)
+  | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
   | _, _ => None
   end.
 
@@ -472,9 +484,9 @@ Qed.
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
-      destruct x; simpl in H; FuncInv
+      destruct x; cbn in H; FuncInv
   | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ =>
-      destruct v; simpl in H; FuncInv
+      destruct v; cbn in H; FuncInv
   | H: (if Archi.ptr64 then _ else _) = Some _ |- _ =>
       destruct Archi.ptr64 eqn:?; FuncInv
   | H: (Some _ = Some _) |- _ =>
@@ -643,6 +655,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEfeqs => (Tsingle :: Tsingle :: nil, Tint)
   | OEflts => (Tsingle :: Tsingle :: nil, Tint)
   | OEfles => (Tsingle :: Tsingle :: nil, Tint)
+  | Obits_of_single => (Tsingle :: nil, Tint)
+  | Obits_of_float => (Tfloat :: nil, Tlong)
+  | Osingle_of_bits => (Tint :: nil, Tsingle)
+  | Ofloat_of_bits => (Tlong :: nil, Tfloat)
+  | Oselectl => (Tint :: Tlong :: Tlong :: nil, Tlong)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -929,6 +946,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OEfles *)
   - destruct v0; destruct v1; cbn; auto.
     destruct Float32.cmp; cbn; auto.
+  (* Bits_of_single, float *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
+  (* single, float of bits *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
+  (* selectl *)
+  - destruct v0; cbn; trivial.
+    destruct Int.eq; cbn.
+    apply Val.normalize_type.
+    destruct Int.eq; cbn; trivial.
+    apply Val.normalize_type.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1767,6 +1796,17 @@ Proof.
   (* OEfles *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* Bits_of_single, double *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
+  (* single, double of bits *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
+  (* selectl *)
+  - inv H4; trivial. cbn.
+    destruct (Int.eq i Int.one).
+    + auto using Val.normalize_inject.
+    + destruct (Int.eq i Int.zero); cbn; auto using Val.normalize_inject.
 Qed.
 
 Lemma eval_addressing_inj: