Fix ldshiftexp

* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>

7 files changed, 20 insertions, 17 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index c21aeecb16..ca1308696c 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1711,7 +1711,8 @@ value coq_interprete
         print_instr("CHECKLDSHIFTEXP");
         CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2);
         Swap_accu_sp;
-        Int_of_uint63(accu);
+        Uint63_to_int_min(accu, Val_int(2 * FLOAT_EXP_SHIFT));
+        accu = Int_val(accu);
         Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT));
         Next;
       }
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index e09803ae2d..143a6d098c 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -169,5 +169,5 @@ DECLARE_UNOP(of_float)
 DECLARE_UNOP(of_int)
 #define Uint63_of_int(x) CALL_UNOP(of_int, x)
 
-DECLARE_UNOP(to_int_saturate)
-#define Int_of_uint63(x) CALL_PREDICATE(accu, to_int_saturate, x)
+DECLARE_BINOP(to_int_min)
+#define Uint63_to_int_min(n, m) CALL_BINOP(to_int_min, n, m)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 0ab374194e..5be7587091 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -155,10 +155,9 @@ value coq_uint63_to_float_byte(value x) {
 
 #define Uint63_of_int(x) (accu = (x))
 
-#define Int_of_uint63(x) do{ \
-  uint64_t int_of_uint63__ = uint63_of_value(x); \
-  if ((int_of_uint63__ & 0xFFFFFFFF80000000L) == 0) \
-    accu = (int)int_of_uint63__; \
+#define Uint63_to_int_min(n, m) do { \
+  if (uint63_lt((n),(m))) \
+    accu = (n); \
   else \
-    accu = 0x7FFFFFFF; \
+    accu = (m); \
   }while(0)
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 86b14c5cd2..07fb25734b 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -117,7 +117,7 @@ let frshiftexp f =
     m, Uint63.of_int (e + eshift)
 [@@ocaml.inline always]
 
-let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift)
+let ldshiftexp f e = ldexp f (Uint63.to_int_min e (2 * eshift) - eshift)
 [@@ocaml.inline always]
 
 external next_up : float -> float = "coq_next_up_byte" "coq_next_up"
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 7ed3d415e4..e0bf44da35 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -19,8 +19,10 @@ val to_int2 : t -> int * int (* msb, lsb *)
 val of_int64 : Int64.t -> t
 (*
 val of_uint : int -> t
-*)
-val to_int_saturate : t -> int (* maxuint31 in case of overflow *)
+ *)
+(** [int_min n m] returns the minimum of [n] and [m],
+    [m] must be in [0, 2^30-1]. *)
+val to_int_min : t -> int -> int
 
       (* conversion to float *)
 val of_float : float -> t
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index a5646e87c3..e38389ca13 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -27,9 +27,8 @@ let of_int i = Int64.of_int i
 let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i)
 let of_int64 i = i
 
-let to_int_saturate i =
-  let r = if Int64.(equal (logand i maxuint31) i) then i else maxuint31 in
-  Int64.to_int r
+let to_int_min n m =
+  if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m
 
 let of_float f = mask63 (Int64.of_float f)
 let to_float = Int64.to_float
@@ -225,4 +224,4 @@ let () =
   Callback.register "uint63 of_float" of_float;
   Callback.register "uint63 to_float" to_float;
   Callback.register "uint63 of_int" of_int;
-  Callback.register "uint63 to_int_saturate" to_int_saturate
+  Callback.register "uint63 to_int_min" to_int_min
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 1776f904d6..85b44528a7 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -27,8 +27,6 @@ let to_int2 i = (0,i)
 
 let of_int64 _i = assert false
 
-let to_int_saturate i = i
-
 let of_float = int_of_float
 
 external to_float : int -> (float [@unboxed])
@@ -104,6 +102,10 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
+let to_int_min n m =
+  if lt n m then n else m
+[@@ocaml.inline always]
+
     (* division of two numbers by one *)
 (* precondition: xh < y *)
 (* outputs: q, r s.t. x = q * y + r, r < y *)