Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_division

3 files changed, 78 insertions, 18 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.
+
diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp
index b3638eca..3598025a 100644
--- a/kvx/SelectLong.vp
+++ b/kvx/SelectLong.vp
@@ -23,6 +23,7 @@ Require Import OpHelpers.
 Require Import SelectOp SplitLong.
 Require Import ExtValues.
 Require Import DecBoolOps.
+Require FPExtra.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -433,28 +434,30 @@ Definition cmpl (c: comparison) (e1 e2: expr) :=
 (** ** Floating-point conversions *)
 
 Definition longoffloat (e: expr) :=
-  if Archi.splitlong then SplitLong.longoffloat e else 
   Eop Olongoffloat (e:::Enil).
 
 Definition longuoffloat (e: expr) :=
-  if Archi.splitlong then SplitLong.longuoffloat e else 
   Eop Olonguoffloat (e:::Enil).
 
 Definition floatoflong (e: expr) := 
-  if Archi.splitlong then SplitLong.floatoflong e else 
   Eop Ofloatoflong (e:::Enil).
 
 Definition floatoflongu (e: expr) := 
-  if Archi.splitlong then SplitLong.floatoflongu e else 
   Eop Ofloatoflongu (e:::Enil).
 
 Definition longofsingle (e: expr) := longoffloat (floatofsingle e).
 
 Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).
 
+Definition use_inlined_fp_conversions := true.
+Opaque use_inlined_fp_conversions.
+
 Definition singleoflong (e: expr) := SplitLong.singleoflong e.
 
-Definition singleoflongu (e: expr) := SplitLong.singleoflongu e.
+Definition singleoflongu (e: expr) :=
+  if use_inlined_fp_conversions
+  then FPExtra.e_single_of_longu e
+  else SplitLong.singleoflongu e.
 
 End SELECT.
 
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v
index c3abdbc7..b858158b 100644
--- a/kvx/SelectLongproof.v
+++ b/kvx/SelectLongproof.v
@@ -884,32 +884,28 @@ Qed.
 
 Theorem eval_longoffloat: partial_unary_constructor_sound longoffloat Val.longoffloat.
 Proof.
-  unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_longoffloat; eauto.
+  unfold longoffloat; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
 Proof.
-  unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_longuoffloat; eauto.
+  unfold longuoffloat; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
 Proof.
-  unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_floatoflong; eauto.
+  unfold floatoflong; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
 Proof.
-  unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_floatoflongu; eauto.
+  unfold floatoflongu; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
@@ -936,16 +932,17 @@ Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
 Proof.
-  unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *)
+  unfold singleoflong; red; intros.
   eapply SplitLongproof.eval_singleoflong; eauto.
-(*   TrivialExists. *)
 Qed.
 
 Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
 Proof.
-  unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *)
-  eapply SplitLongproof.eval_singleoflongu; eauto.
-(*   TrivialExists. *)
+  unfold singleoflongu; red; intros.
+  destruct use_inlined_fp_conversions.
+  - econstructor. split. apply FPExtra.e_single_of_longu_correct.
+    eassumption. rewrite H0. cbn. constructor.
+  - eapply SplitLongproof.eval_singleoflongu; eauto.
 Qed.
 
 End CMCONSTR.