Transpose the C code of uint63_div21 to the OCaml implementations.

2 files changed, 31 insertions, 84 deletions

diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml
index 20b2f58496..1bb633d413 100644
--- a/kernel/uint63_amd64_63.ml
+++ b/kernel/uint63_amd64_63.ml
@@ -94,53 +94,28 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
-(* A few helper functions on 128 bits *)
-let lt128 xh xl yh yl =
-  lt xh yh || (xh = yh && lt xl yl)
-
-let le128 xh xl yh yl =
-  lt xh yh || (xh = yh && le xl yl)
-
     (* division of two numbers by one *)
 (* precondition: y <> 0 *)
 (* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
 let div21 xh xl y =
-  let maskh = ref 0 in
-  let maskl = ref 1 in
-  let dh = ref 0 in
-  let dl = ref y in
-  let cmp = ref true in
-  (* n = ref 0 *)
-  (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
-  while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *)
-    (* We don't use addmuldiv below to avoid checks on 1 *)
-    dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1));
-    dl := !dl lsl 1;
-    maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1));
-    maskl := !maskl lsl 1;
-    (* incr n *)
-    cmp := lt128 !dh !dl xh xl;
-  done; (* mask = 2^n, d = 2^n * y, 2 * d > x *)
-  let remh = ref xh in
-  let reml = ref xl in
-  (* quotienth = ref 0 *)
-  let quotientl = ref 0 in
-  (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
-     mask = floor(2^n), d = mask * y, n >= -1 *)
-  while !maskh lor !maskl <> 0 do
-    if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
-      (* quotienth := !quotienth lor !maskh *)
-      quotientl := !quotientl lor !maskl;
-      remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh;
-      reml := !reml - !dl;
-    end;
-    maskl := (!maskl lsr 1) lor (!maskh lsl (uint_size - 1));
-    maskh := !maskh lsr 1;
-    dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1));
-    dh := !dh lsr 1;
-    (* decr n *)
+  let y = to_uint64 y in
+  (* nh might temporarily grow as large as 2*y - 1 in the loop body,
+     so we store it as a 64-bit unsigned integer *)
+  let nh = ref (Int64.rem (to_uint64 xh) y) in
+  let nl = ref xl in
+  let q = ref 0 in
+  for _i = 0 to 62 do
+    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^63,
+       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
+    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.of_int (!nl lsr 62));
+    nl := !nl lsl 1;
+    q := !q lsl 1;
+    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
+       once OCaml 4.08 becomes the minimal required version *)
+    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
+      begin q := !q lor 1; nh := Int64.sub !nh y; end
   done;
-  !quotientl, !reml
+  !q, Int64.to_int !nh
 
 let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y
 
diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml
index c3279779e1..91a1e397a8 100644
--- a/kernel/uint63_i386_31.ml
+++ b/kernel/uint63_i386_31.ml
@@ -86,53 +86,25 @@ let rem x y =
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))
 
-(* A few helper functions on 128 bits *)
-let lt128 xh xl yh yl =
-  lt xh yh || (xh = yh && lt xl yl)
-
-let le128 xh xl yh yl =
-  lt xh yh || (xh = yh && le xl yl)
-
     (* division of two numbers by one *)
 (* precondition: y <> 0 *)
 (* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
 let div21 xh xl y =
-  let maskh = ref zero in
-  let maskl = ref one in
-  let dh = ref zero in
-  let dl = ref y in
-  let cmp = ref true in
-  (* n = ref 0 *)
-  (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
-  while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do
-    (* We don't use addmuldiv below to avoid checks on 1 *)
-    dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1)));
-    dl := l_sl !dl one;
-    maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1)));
-    maskl := l_sl !maskl one;
-    (* incr n *)
-    cmp := lt128 !dh !dl xh xl;
-  done; (* mask = 2^n, d = 2^n * d, 2 * d > x *)
-  let remh = ref xh in
-  let reml = ref xl in
-  (* quotienth = ref 0 *)
-  let quotientl = ref zero in
-  (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
-     mask = floor(2^n), d = mask * y, n >= -1 *)
-  while not (Int64.equal (l_or !maskh !maskl) zero) do
-    if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
-      (* quotienth := !quotienth lor !maskh *)
-      quotientl := l_or !quotientl !maskl;
-      remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh;
-      reml := sub !reml !dl
-    end;
-    maskl := l_or (l_sr !maskl one) (l_sl !maskh (of_int (uint_size - 1)));
-    maskh := l_sr !maskh one;
-    dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1)));
-    dh := l_sr !dh one
-    (* decr n *)
+  let nh = ref (Int64.rem xh y) in
+  let nl = ref xl in
+  let q = ref 0L in
+  for _i = 0 to 62 do
+    (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
+       (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
+    nl := Int64.shift_left !nl 1;
+    nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63);
+    q := Int64.shift_left !q 1;
+    (* TODO: use "Int64.unsigned_compare !nh y >= 0",
+       once OCaml 4.08 becomes the minimal required version *)
+    if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
+      begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end
   done;
-  !quotientl, !reml
+  !q, !nh
 
 let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y