extra FP code

1 files changed, 60 insertions, 0 deletions

diff --git a/kvx/FPExtra.v b/kvx/FPExtra.v
new file mode 100644
index 00000000..05fd8842
--- /dev/null
+++ b/kvx/FPExtra.v
@@ -0,0 +1,60 @@
+Require Import Coqlib.
+Require Import Compopts.
+Require Import AST Integers Floats.
+Require Import Op CminorSel.
+Require Import OpHelpers.
+Require Import SelectOp SplitLong.
+Require Import Values ExtValues.
+Require Import DecBoolOps.
+
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
+Definition e_andl a b := Eop Oandl (a ::: b ::: Enil).
+Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil).
+Definition e_orl  a b := Eop Oorl  (a ::: b ::: Enil).
+Definition e_constl n := Eop (Olongconst (Int64.repr n)) Enil.
+Definition e_float_of_longu a  := Eop Ofloatoflongu (a ::: Enil).
+Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil).
+Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil).
+Definition e_cmpluimm c v n := Eop (Ocmp (Ccompluimm c n)) (v ::: Enil).
+
+Definition a_var := Eletvar 0%nat.
+
+Definition e_single_of_longu a :=
+  Elet a (e_single_of_float (e_float_of_longu
+    (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle a_var (Int64.repr (2^53))) a_var
+           (e_andl (e_orl a_var (e_addl (e_andl a_var (e_constl 2047))
+                                        (e_constl 2047)))
+                   (e_constl (-2048))))))%Z.
+
+Theorem e_single_of_longu_correct :
+  forall (ge : genv)  (sp: val) cmenv memenv
+         (le : letenv) (expr_a : expr) (va : val)
+         (EVAL_a : eval_expr ge sp cmenv memenv le expr_a va),
+  eval_expr ge sp cmenv memenv le (e_single_of_longu expr_a)
+            (Val.maketotal (Val.singleoflongu va)).
+Proof.
+  intros.
+  unfold e_single_of_longu.
+  repeat econstructor. eassumption.
+  cbn.
+  destruct va; cbn.
+  all: try reflexivity.
+  f_equal.
+  unfold Int64.ltu.
+  change (Int64.unsigned (Int64.repr 9007199254740992))%Z with 9007199254740992%Z.
+  destruct zlt as [LT | GE]; cbn.
+  { change (Int.eq Int.zero Int.zero) with true. cbn.
+    f_equal.
+    symmetry.
+    apply Float32.of_longu_double_2.
+    lia.
+  }
+  change (Int.eq Int.one Int.zero) with false. cbn.
+  f_equal.
+  symmetry.
+  apply Float32.of_longu_double_1.
+  lia.
+Qed.
+