remove singleoflongu (does not exist)

5 files changed, 73 insertions, 32 deletions

diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v
index 163dcbd8..9a04815b 100644
--- a/kvx/Builtins1.v
+++ b/kvx/Builtins1.v
@@ -28,7 +28,8 @@ Inductive platform_builtin : Type :=
 | BI_fmaf
 | BI_lround_ne
 | BI_luround_ne
-| BI_fp_udiv32.
+| BI_fp_udiv32
+| BI_fp_udiv64.
 
 Local Open Scope string_scope.
 
@@ -42,6 +43,7 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
   :: ("__builtin_lround_ne", BI_lround_ne)
   :: ("__builtin_luround_ne", BI_luround_ne)
   :: ("__builtin_fp_udiv32", BI_fp_udiv32)
+  :: ("__builtin_fp_udiv64", BI_fp_udiv64)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
@@ -58,6 +60,8 @@ Definition platform_builtin_sig (b: platform_builtin) : signature :=
       mksignature (Tfloat :: nil) Tlong cc_default
   | BI_fp_udiv32 =>
       mksignature (Tint :: Tint :: nil) Tint cc_default
+  | BI_fp_udiv64 =>
+      mksignature (Tlong :: Tlong :: nil) Tlong cc_default
   end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
@@ -74,4 +78,8 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl
        (fun n1 n2 => if Int.eq n2 Int.zero
                      then None
                      else Some (Int.divu n1 n2))
+  | BI_fp_udiv64 => mkbuiltin_n2p Tlong Tlong Tlong
+       (fun n1 n2 => if Int64.eq n2 Int64.zero
+                     then None
+                     else Some (Int64.divu n1 n2))
   end.
diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml
index fad86d3c..49534867 100644
--- a/kvx/CBuiltins.ml
+++ b/kvx/CBuiltins.ml
@@ -139,6 +139,8 @@ let builtins = {
     (TInt(IULong, []), [TFloat(FDouble, [])], false);
     "__builtin_fp_udiv32",
     (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
+    "__builtin_fp_udiv64",
+    (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false);
 ]
 }
 
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index a4d609f0..bbd94321 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -50,7 +50,7 @@ Proof.
 Qed.
 
 Definition approx_inv_longu b :=
-  let invb_s := ExtValues.invfs (Val.maketotal (Val.singleoflongu b)) in
+  let invb_s := ExtValues.invfs (Val.singleoffloat (Val.maketotal (Val.floatoflongu b))) in
   let invb_d := Val.floatofsingle invb_s in
   let b_d := Val.maketotal (Val.floatoflongu b) in
   let one := Vfloat (ExtFloat.one) in
@@ -68,7 +68,8 @@ Qed.
 
 Definition approx_inv_thresh := (25/2251799813685248)%R.
 (* 1.11022302462516e-14 *)
-    
+
+(*
 Theorem approx_inv_longu_correct_abs :
   forall b,
     (0 < Int64.unsigned b)%Z ->
@@ -302,6 +303,7 @@ Proof.
   unfold approx_inv_thresh.
   gappa.
 Qed.
+ *)
 
 Local Notation "'rd'" := (round radix2 (FLT_exp (-1074) 53) ZnearestE).
 Local Notation "'rs'" := (round radix2 (FLT_exp (-149) 24) ZnearestE).
@@ -320,8 +322,8 @@ Proof.
   econstructor.
   split.
   reflexivity.
-  Local Transparent Float.neg Float.of_single Float32.of_longu Float32.div Float.of_longu Float32.of_int Float.of_int.
-  unfold Float.fma, Float.neg, Float.of_single, Float32.of_longu, ExtFloat32.inv, Float32.div, Float.of_longu, ExtFloat32.one, Float32.of_int, ExtFloat.one, Float.of_int.
+  Local Transparent Float.neg Float.of_single Float32.of_longu Float32.div Float.of_longu Float32.of_int Float.of_int Float.to_single.
+  unfold Float.fma, Float.neg, Float.of_single, Float32.of_longu, ExtFloat32.inv, Float32.div, Float.of_longu, ExtFloat32.one, Float32.of_int, ExtFloat.one, Float.of_int, Float.to_single.
   set (re := (@eq_refl Datatypes.comparison Lt)).
   change (Int.signed (Int.repr 1)) with 1%Z.
   set (b' := Int64.unsigned b) in *.
@@ -336,20 +338,34 @@ Proof.
   clear SILLY.
   set (one_s := (BofZ 24 128 re re 1)) in *.
   
-  pose proof (BofZ_correct 24 128 re re b') as C1.
-  cbn in C1.
+  pose proof (BofZ_correct 53 1024 re re b') as C5.
+  rewrite Rlt_bool_true in C5; cycle 1.
+  { clear C5.
+    eapply (Rabs_relax (bpow radix2 64)).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  cbn in C5.
+  destruct C5 as (C5R & C5F & C5S).
+  set (b_d :=  (BofZ 53 1024 re re b')) in *.
+
+  pose proof (Bconv_correct 53 1024 24 128 re re Float.to_single_nan mode_NE b_d C5F) as C1.
   rewrite Rlt_bool_true in C1; cycle 1.
   { clear C1.
-    eapply (Rabs_relax (IZR 18446744073709551616)).
-    lra.
-    set (b'' := IZR b') in *.
+    apply (Rabs_relax (bpow radix2 64)).
+    { apply bpow_lt. lia. }
+    rewrite C5R.
+    cbn.
     gappa.
   }
-  destruct C1 as (C1R & C1F & _).
-  set (b_s :=  (BofZ 24 128 re re b')) in *.
-
+  cbn in C1.
+  destruct C1 as (C1R & C1F & C1S).
+  set (b_s := (Bconv 53 1024 24 128 re re Float.to_single_nan mode_NE b_d)) in *.
   assert(1 <= B2R 24 128 b_s <= 18446744073709551616)%R as b_s_RANGE.
   { rewrite C1R.
+    rewrite C5R.
+    cbn.
     gappa.
   }
   assert(B2R 24 128 b_s <> 0)%R as b_s_NONZ by lra.
@@ -413,19 +429,7 @@ Proof.
     gappa.
   }
   destruct C4 as (C4R & C4F & _).
-  
-  pose proof (BofZ_correct 53 1024 re re b') as C5.
-  cbn in C5.
-  rewrite Rlt_bool_true in C5; cycle 1.
-  { clear C5.
-    eapply (Rabs_relax (IZR 18446744073709551616)).
-    lra.
-    set (b'' := IZR b') in *.
-    gappa.
-  }
-  destruct C5 as (C5R & C5F & _).
-  set (b_d :=  (BofZ 53 1024 re re b')) in *.
-  
+    
   assert(1 <= B2R 53 1024 b_d <= 18446744073709551616)%R as b_d_RANGE.
   { rewrite C5R.
     gappa.
@@ -477,15 +481,16 @@ Proof.
   rewrite C3R.
   rewrite C2R.
   rewrite C1R.
+  rewrite C5R.
   rewrite C0R.
   cbn.
   set(b1 := IZR b') in *.
 
   replace (rd 1) with 1%R by gappa.
-  replace (rd (rs (1 / rs b1))) with
-    ((((rd (rs (1 / rs b1)) - (/b1))/(/b1))+1)*(/ b1))%R ; cycle 1.
+  replace (rd (rs (1 / rs (rd b1)))) with
+    ((((rd (rs (1 / rs (rd b1))) - (/b1))/(/b1))+1)*(/ b1))%R ; cycle 1.
   { field. lra. }
-  set (er0 := ((rd (rs (1 / rs b1)) - (/b1))/(/b1))%R).
+  set (er0 := ((rd (rs (1 / rs (rd b1))) - (/b1))/(/b1))%R).
   replace (rd b1) with ((((rd b1) - b1)/b1 + 1) * b1)%R; cycle 1.
   { field. lra. }
   set (er1 := (((rd b1) - b1)/b1)%R).
@@ -2351,8 +2356,8 @@ Open Scope cminorsel_scope.
 Definition e_invfs a := Eop Oinvfs (a ::: 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_longu a := Eop Osingleoflongu (a ::: Enil).
 Definition e_float_of_single a := Eop Ofloatofsingle (a ::: Enil).
+Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil).
 Definition e_long_of_float_ne a := Eop Olongoffloat_ne (a ::: Enil).
 Definition e_longu_of_float_ne a := Eop Olonguoffloat_ne (a ::: Enil).
 Definition e_mulf a b := Eop Omulf (a ::: b ::: Enil).
@@ -2378,7 +2383,7 @@ Definition binv_d_var1 := Eletvar (0%nat).
 Definition e_setup1 a b rest :=
   Elet a (Elet (e_float_of_longu (Eletvar 0%nat))
     (Elet (lift (lift b)) (Elet (e_float_of_longu (Eletvar 0%nat))
-      (Elet (e_float_of_single (e_invfs (e_single_of_longu (Eletvar 1%nat))))
+      (Elet (e_float_of_single (e_invfs (e_single_of_float (Eletvar 0%nat))))
       rest)))).                  
 Definition e_step1 := e_longu_of_float_ne (e_mulf a_d_var1 binv_d_var1).
 
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 70941c48..72a6e4b3 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -742,7 +742,7 @@ Nondetfunction gen_fmaf args :=
   | _ => None
   end.
 
-Require FPDivision32.
+Require FPDivision32 FPDivision64.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
   match b with
@@ -758,6 +758,10 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
                      | a:::b:::Enil => Some (FPDivision32.fp_divu32 a b)
                      | _ => None
                      end)
+  | BI_fp_udiv64 => (match args with
+                     | a:::b:::Enil => Some (FPDivision64.fp_divu64 a b)
+                     | _ => None
+                     end)
   end.
 End SELECT.
 
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 658bf0b3..e6cce0fa 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1929,6 +1929,28 @@ Proof.
     }
     inv EVAL.
     constructor.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int64.eq in EVAL.
+    change (Int64.unsigned Int64.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vlong (Int64.divu i i0)). split.
+    {
+      apply FPDivision64.fp_divu64_correct; auto.
+      pose proof (Int64.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
 Qed.
 
 End CMCONSTR.