Merge PR #11323: Fix mulc on 32-bit architectures

Reviewed-by: MSoegtropIMC

3 files changed, 45 insertions, 20 deletions

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 67becb251a..2d187f7bae 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -255,6 +255,18 @@ Conversion machines
   GH issue number: #9925
   risk:
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: broken long multiplication primitive integer emulation layer on 32 bits
+  introduced: e43b176
+  impacted released versions: 8.10.0, 8.10.1, 8.10.2
+  impacted development branches: 8.11
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 4e176a7
+  found by: Soegtrop, Melquiond
+  exploit: test-suite/bugs/closed/bug_11321.v
+  GH issue number: #11321
+  risk: critical, as any BigN computation on 32-bit architectures is wrong
+
   component: "native" conversion machine (translation to OCaml which compiles to native code)
   summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
   introduced: V8.5
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index e38389ca13..445166f6af 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
@@ -118,27 +118,30 @@ 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)
-
-let equal x y = mask63 x = mask63 y
+  (* 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
+  (* 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
+  (* 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
 
 let compare x y = Int64.compare x y
 
diff --git a/test-suite/bugs/closed/bug_11321.v b/test-suite/bugs/closed/bug_11321.v
new file mode 100644
index 0000000000..ce95280fb1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11321.v
@@ -0,0 +1,10 @@
+Require Import Cyclic63.
+
+Goal False.
+Proof.
+assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H.
+  vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63).
+generalize (f_equal (zn2z_to_Z wB to_Z) H).
+now rewrite mulc_WW_spec.
+Fail Qed.
+Abort.