From ec337b6e5be76b69b4c82af682a08cfec2a8e12a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 22 Dec 2019 11:07:01 +0400 Subject: Do not hide constants from the compiler. --- kernel/uint63_31.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index e38389ca13..df8a354dcf 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -15,8 +15,8 @@ let _ = assert (Sys.word_size = 32) let uint_size = 63 -let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF" -let maxuint31 = Int64.of_string "0x7FFFFFFF" +let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL +let maxuint31 = 0x7FFF_FFFFL let zero = Int64.zero let one = Int64.one -- cgit v1.2.3 From 6e8c8068a8cbaf34dbb5e32a2eda61f190737f86 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 22 Dec 2019 11:09:54 +0400 Subject: Simplify equality of 63-bit integers. The sign bit is supposed to be zero, so no need to mask it out. If it was not zero, most of the algorithms in this file would fail horribly. --- kernel/uint63_31.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index df8a354dcf..3d7dd1792a 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -138,7 +138,7 @@ let mulc x y = then Int64.(sub !hr one, mask63 !lr) else (!hr, !lr) -let equal x y = mask63 x = mask63 y +let equal (x : t) y = x = y let compare x y = Int64.compare x y -- cgit v1.2.3 From 4e176a7ee4660d505321ca55c5ce70a6c3d50d3b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 22 Dec 2019 11:17:22 +0400 Subject: Use a more straightforward algorithm for mulc on 32-bit architectures. (Fixes #11321) It has the added advantage of performing 6 less 64-bit operations per long multiplication. --- kernel/uint63_31.ml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) (limited to 'kernel') diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 3d7dd1792a..ddb6ba656e 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -118,25 +118,27 @@ let div21 xh xl y = let div21 xh xl y = if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y - (* exact multiplication *) +(* exact multiplication *) let mulc x y = - let lx = ref (Int64.logand x maxuint31) in - let ly = ref (Int64.logand y maxuint31) in + let lx = Int64.logand x maxuint31 in + let ly = Int64.logand y maxuint31 in let hx = Int64.shift_right x 31 in let hy = Int64.shift_right y 31 in - let hr = ref (Int64.mul hx hy) in - let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in - hr := (Int64.shift_right_logical !hr 1); - lx := Int64.mul !lx hy; - ly := Int64.mul hx !ly; - hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32)); - lr := Int64.add !lr (Int64.shift_left !lx 31); - hr := Int64.add !hr (Int64.shift_right_logical !lr 63); - lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr); - hr := Int64.add !hr (Int64.shift_right_logical !lr 63); - if Int64.logand !lr Int64.min_int <> 0L - then Int64.(sub !hr one, mask63 !lr) - else (!hr, !lr) + (* compute the median products *) + let s = Int64.add (Int64.mul lx hy) (Int64.mul hx ly) in + (* s fits on 64 bits, split it into a 33-bit high part and a 31-bit low part *) + let lr = Int64.shift_left (Int64.logand s maxuint31) 31 in + let hr = Int64.shift_right_logical s 31 in + (* add the outer products *) + let lr = Int64.add (Int64.mul lx ly) lr in + let hr = Int64.add (Int64.mul hx hy) hr in + (* now x * y = hr * 2^62 + lr and lr < 2^63 *) + let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in + let hr = Int64.shift_right_logical hr 1 in + (* now x * y = hr * 2^63 + lr, but lr might be too large *) + if Int64.logand lr Int64.min_int <> 0L + then Int64.add hr 1L, mask63 lr + else hr, lr let equal (x : t) y = x = y -- cgit v1.2.3 From 00c0b652311b8c6b26c7e21b17db4ab12a35f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 27 Dec 2019 09:04:39 +0400 Subject: Add critical-bugs entry, tests-suite file, and code comment. --- kernel/uint63_31.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel') diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index ddb6ba656e..445166f6af 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -132,6 +132,7 @@ let mulc x y = (* add the outer products *) let lr = Int64.add (Int64.mul lx ly) lr in let hr = Int64.add (Int64.mul hx hy) hr in + (* hr fits on 64 bits, since the final result fits on 126 bits *) (* now x * y = hr * 2^62 + lr and lr < 2^63 *) let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in let hr = Int64.shift_right_logical hr 1 in -- cgit v1.2.3