From 5afebe369cea7f2746dec7c64514822562e9100e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 11:22:59 +0100
Subject: begin synthesizing select

---
 riscV/ExtValues.v     | 18 ++++++++++++++++++
 riscV/SelectOp.vp     |  6 +++++-
 riscV/SelectOpproof.v | 12 +++++++++++-
 3 files changed, 34 insertions(+), 2 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 81688ca6..3f283cdc 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -83,3 +83,21 @@ Proof.
   destruct (Int.eq i Int.one); trivial.
   destruct (Int.eq i Int.zero); trivial.
 Qed.
+
+Lemma select01_long_true:
+  forall vt vf,
+    select01_long Vtrue vt vf = vt.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true. reflexivity.
+Qed.
+
+Lemma select01_long_false:
+  forall vt vf,
+    select01_long Vfalse vt vf = vf.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true.
+  rewrite Int.eq_false. reflexivity.
+  cbv. discriminate.
+Qed.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 7714f12d..0596ebf6 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -421,7 +421,11 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
    : option expr
-   := None.
+   := match ty with
+      | Tlong => Some (Eop Oselectl
+                       ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
+      | _ => None
+      end.
  
 (** ** Recognition of addressing modes for load and store operations *)
 
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1d713010..9dfe9b6e 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -886,7 +886,17 @@ Theorem eval_select:
      eval_expr ge sp e m le a v
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
-  unfold select; intros; discriminate.
+  unfold select; intros.
+  destruct ty; cbn in *; try discriminate.
+  inv H.
+  TrivialExists.
+  - cbn. constructor.
+    { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
+    constructor. eassumption. constructor. eassumption. constructor.
+  - cbn. f_equal. rewrite ExtValues.normalize_select01.
+    destruct b.
+    + rewrite ExtValues.select01_long_true. reflexivity.
+    + rewrite ExtValues.select01_long_false. reflexivity.
 Qed.
 
 Theorem eval_addressing:
-- 
cgit