Pselectd

3 files changed, 33 insertions, 0 deletions

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
@@ -962,6 +962,25 @@ Proof.
       * 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. }
       constructor. eassumption. constructor. eassumption. constructor.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.