From a47d709fd9251f58032444fde27a3ad7e947c26d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:33:43 +0100
Subject: Pselectd

---
 riscV/ExtValues.v     | 10 ++++++++++
 riscV/SelectOp.vp     |  4 ++++
 riscV/SelectOpproof.v | 19 +++++++++++++++++++
 3 files changed, 33 insertions(+)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 3f283cdc..aebbe5c5 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -101,3 +101,13 @@ Proof.
   rewrite Int.eq_false. reflexivity.
   cbv. discriminate.
 Qed.
+
+Lemma float_bits_normalize:
+  forall v1,
+  ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) =
+  Val.normalize v1 AST.Tfloat.
+Proof.
+  destruct v1; cbn; trivial.
+  f_equal.
+  apply Float.of_to_bits.
+Qed.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 0e82f8ba..b6720e40 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -429,6 +429,10 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
                        ((Eop (Ocmp cond) args) :::
 		         (Eop Ocast32signed (e1 ::: Enil)) :::
 			 (Eop Ocast32signed (e2 ::: Enil)) ::: Enil)) ::: Enil))
+      | Tfloat => Some (Eop Ofloat_of_bits ((Eop Oselectl
+                       ((Eop (Ocmp cond) args) :::
+		         (Eop Obits_of_float (e1 ::: Enil)) :::
+			 (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil))
       | _ => None
       end
       else None.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 7f7474b6..c313fbaf 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -960,6 +960,25 @@ Proof.
       destruct b.
       * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
       * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
+  - inv H. TrivialExists.
+    + cbn. constructor.
+      { econstructor.
+        { constructor.
+          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
+          constructor. econstructor. constructor. eassumption.
+          constructor. cbn. reflexivity.
+          constructor. econstructor. constructor. eassumption. constructor.
+          cbn. reflexivity. constructor.
+        }
+        constructor.
+      }
+      constructor.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      destruct b.
+      * rewrite ExtValues.select01_long_true.
+        apply ExtValues.float_bits_normalize.
+      * rewrite ExtValues.select01_long_false.
+        apply ExtValues.float_bits_normalize.
   - inv H. TrivialExists.
     + cbn. constructor.
       { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
-- 
cgit