From 2867dee21f6fb696db554679d8535306c7a9d4ea Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 14 Feb 2022 18:15:17 +0100
Subject: long -> single precision float done with instructions

---
 kvx/FPExtra.v         | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++
 kvx/SelectLong.vp     |  5 ++++-
 kvx/SelectLongproof.v |  5 ++++-
 3 files changed, 65 insertions(+), 2 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPExtra.v b/kvx/FPExtra.v
index 05fd8842..9e3b55b6 100644
--- a/kvx/FPExtra.v
+++ b/kvx/FPExtra.v
@@ -15,9 +15,11 @@ 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_float_of_long a  := Eop Ofloatoflong (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 e_absl a := Eop (Oabsdifflimm Int64.zero) (a ::: Enil).
 
 Definition a_var := Eletvar 0%nat.
 
@@ -58,3 +60,58 @@ Proof.
   lia.
 Qed.
 
+Definition e_single_of_long a :=
+  Elet a (e_single_of_float (e_float_of_long
+    (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle (e_absl 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_long_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_long expr_a)
+            (Val.maketotal (Val.singleoflong va)).
+Proof.
+  intros.
+  unfold e_single_of_long.
+  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_long_double_2.
+    unfold long_absdiff, Z_abs_diff in LT.
+    change (Int64.signed Int64.zero) with 0%Z in LT.
+    rewrite Z.sub_0_r in LT.
+    rewrite Int64.unsigned_repr in LT.
+    lia.
+    pose proof (Int64.signed_range i).
+    change Int64.min_signed with (-9223372036854775808)%Z in *.
+    change Int64.max_signed with (9223372036854775807)%Z in *.
+    change Int64.max_unsigned with (18446744073709551615)%Z.
+    lia.
+  }
+  change (Int.eq Int.one Int.zero) with false. cbn.
+  f_equal.
+  symmetry.
+  apply Float32.of_long_double_1.
+  unfold long_absdiff, Z_abs_diff in GE.
+  change (Int64.signed Int64.zero) with 0%Z in GE.
+  rewrite Z.sub_0_r in GE.
+  rewrite Int64.unsigned_repr in GE.
+  lia.
+  pose proof (Int64.signed_range i).
+  change Int64.min_signed with (-9223372036854775808)%Z in *.
+  change Int64.max_signed with (9223372036854775807)%Z in *.
+  change Int64.max_unsigned with (18446744073709551615)%Z.
+  lia.
+Qed.
+
diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp
index 3598025a..9df3212b 100644
--- a/kvx/SelectLong.vp
+++ b/kvx/SelectLong.vp
@@ -452,7 +452,10 @@ 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 singleoflong (e: expr) :=
+  if use_inlined_fp_conversions
+  then FPExtra.e_single_of_long e
+  else SplitLong.singleoflong e.
 
 Definition singleoflongu (e: expr) :=
   if use_inlined_fp_conversions
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v
index b858158b..ca32d69a 100644
--- a/kvx/SelectLongproof.v
+++ b/kvx/SelectLongproof.v
@@ -933,7 +933,10 @@ Qed.
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
 Proof.
   unfold singleoflong; red; intros.
-  eapply SplitLongproof.eval_singleoflong; eauto.
+  destruct use_inlined_fp_conversions.
+  - econstructor. split. apply FPExtra.e_single_of_long_correct.
+    eassumption. rewrite H0. cbn. constructor.
+  - eapply SplitLongproof.eval_singleoflong; eauto.
 Qed.
 
 Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
-- 
cgit