diff options
| author | Pierre Roux | 2019-10-10 20:11:02 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:35 +0100 |
| commit | d39fab9a7c39d8da868c4481b96cf1086c21b1a4 (patch) | |
| tree | 4d544f1407d0a082c5c60740a6f456aa250fd593 /kernel/byterun | |
| parent | 40df8d4c451a09e82a5da29a2c3309dedebc64de (diff) | |
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>
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 3 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_emul.h | 4 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_native.h | 9 |
3 files changed, 8 insertions, 8 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) |