begin implementing select

1 files changed, 15 insertions, 1 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 21de7787..64d5e4c9 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -157,7 +157,8 @@ Inductive operation : Type :=
   | Obits_of_single
   | Obits_of_float
   | Osingle_of_bits
-  | Ofloat_of_bits.
+  | Ofloat_of_bits
+  | Oselectl.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -327,6 +328,7 @@ Definition eval_operation
   | 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))
+  | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
   | _, _ => None
   end.
 
@@ -487,6 +489,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | 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 :=
@@ -699,6 +702,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* 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. *)
@@ -1271,6 +1280,11 @@ Proof.
   (* 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: