Provide a default "select" operation for the RiscV port

No `Osel` operation for this port, so `SelectOp.select` always
returns None.

2 files changed, 20 insertions, 0 deletions

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index bb8af2ed..760f06af 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -420,6 +420,12 @@ Definition singleofintu (e: expr) := Eop Osingleofintu (e ::: Enil).
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
+(** ** Selection *)
+
+Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
+   : option expr
+   := None.
+ 
 (** ** Recognition of addressing modes for load and store operations *)
 
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index d12bd8af..d0e6979c 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -873,6 +873,20 @@ Proof.
   red; intros. unfold floatofsingle. TrivialExists.
 Qed.
 
+Theorem eval_select:
+  forall le ty cond al vl a1 v1 a2 v2 a b,
+  select ty cond al a1 a2 = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_condition cond vl m = Some b ->
+  exists v, 
+     eval_expr ge sp e m le a v
+  /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
+Proof.
+  unfold select; intros; discriminate.
+Qed.
+
 Theorem eval_addressing:
   forall le chunk a v b ofs,
   eval_expr ge sp e m le a v ->