diff options
| author | Guillaume Melquiond | 2019-12-27 09:04:39 +0400 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-12-27 18:53:38 +0400 |
| commit | 00c0b652311b8c6b26c7e21b17db4ab12a35f286 (patch) | |
| tree | f0f8effc012a2d43d8ffe6b723b8de7b6e11201d | |
| parent | 4e176a7ee4660d505321ca55c5ce70a6c3d50d3b (diff) | |
Add critical-bugs entry, tests-suite file, and code comment.
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | kernel/uint63_31.ml | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_11321.v | 10 |
3 files changed, 23 insertions, 0 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 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 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. |