diff options
| author | Pierre Roux | 2019-04-04 00:14:47 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:03 +0100 |
| commit | dca0135a263717b3a1a1d7c4f054f039dc08109e (patch) | |
| tree | 3f2ab5ea79e084a9c72e1376d5399ad4a62cb771 /kernel/uint63_31.ml | |
| parent | 3e0db1b645a8653c62b8b5a4978e6d8fbbe9a9cc (diff) | |
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.
Diffstat (limited to 'kernel/uint63_31.ml')
| -rw-r--r-- | kernel/uint63_31.ml | 10 |
1 files changed, 9 insertions, 1 deletions
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 |