From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Fri, 13 Jul 2018 16:22:35 +0200 Subject: Add primitive float computation in Coq kernel Beware of 0. = -0. issue for primitive floats The IEEE 754 declares that 0. and -0. are treated equal but we cannot say that this is true with Leibniz equality. Therefore we must patch the equality and the total comparison inside the kernel to prevent inconsistency. --- kernel/uint63_31.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'kernel/uint63_31.ml') diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index b8eccd19fb..76d768e20a 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -26,6 +26,10 @@ let mask63 i = Int64.logand i maxuint63 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 of_float f = mask63 (Int64.of_float f) +let to_float = Int64.to_float + let hash i = let (h,l) = to_int2 i in (*Hashset.combine h l*) -- cgit v1.2.3 From dca0135a263717b3a1a1d7c4f054f039dc08109e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 4 Apr 2019 00:14:47 +0200 Subject: Make primitive float work on x86_32 Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings. --- kernel/uint63_31.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'kernel/uint63_31.ml') diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 76d768e20a..a5646e87c3 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -27,6 +27,10 @@ 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 of_float f = mask63 (Int64.of_float f) let to_float = Int64.to_float @@ -217,4 +221,8 @@ let () = Callback.register "uint63 one" one; Callback.register "uint63 sub" sub; Callback.register "uint63 subcarry" subcarry; - Callback.register "uint63 tail0" tail0 + Callback.register "uint63 tail0" tail0; + 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 -- cgit v1.2.3 From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 10 Oct 2019 20:11:02 +0200 Subject: 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 --- kernel/uint63_31.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel/uint63_31.ml') 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 -- cgit v1.2.3