diff options
Diffstat (limited to 'dev/doc/critical-bugs')
| -rw-r--r-- | dev/doc/critical-bugs | 262 |
1 files changed, 262 insertions, 0 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs new file mode 100644 index 00000000..8d78559c --- /dev/null +++ b/dev/doc/critical-bugs @@ -0,0 +1,262 @@ +Preliminary compilation of critical bugs in stable releases of Coq +================================================================== + WORK IN PROGRESS WITH SEVERAL OPEN QUESTIONS + + +To add: #7723 (vm_compute universe polymorphism), #7695 (modules and algebraic universes), #7615 (lost functor substitutions) + +Typing constructions + + component: "match" + summary: substitution missing in the body of a let + introduced: ? + impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk/v8.5 (e583a79b5, 22 Nov 2015, Herbelin), v8.4 (525056f1, 22 Nov 2015, Herbelin), v8.3 (4bed0289, 22 Nov 2015, Herbelin) + found by: Herbelin + exploit: test-suite/success/Case22.v + GH issue number: ? + risk: ? + + component: fixpoint, guard + summary: missing lift in checking guard + introduced: probably from V5.10 + impacted released versions: probably V5-V7, V8.0-V8.0pl4, V8.1-V8.1pl4 + impacted development branches: v8.0 ? + impacted coqchk versions: ? + fixed in: master/trunk/v8.2 (ff45afa8, r11646, 2 Dec 2008, Barras), v8.1 (f8e7f273, r11648, 2 Dec 2008, Barras) + found by: Barras + exploit: test-suite/failure/guard.v + GH issue number: none + risk: unprobable by chance + + component: cofixpoint, guard + summary: de Bruijn indice bug in checking guard of nested cofixpoints + introduced: after V6.3.1, before V7.0 + impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master (9f81e2c36, 10 Apr 2014, Dénès), v8.4 (f50ec9e7d, 11 Apr 2014, Dénès), v8.3 (40c0fe7f4, 11 Apr 2014, Dénès), v8.2 (06d66df8c, 11 Apr 2014, Dénès), v8.1 (977afae90, 11 Apr 2014, Dénès), v8.0 (f1d632992, 29 Nov 2015, Herbelin, backport) + found by: Dénès + exploit: ? + GH issue number: none ? + risk: ? + + component: inductive types, elimination principle + summary: de Bruijn indice bug in computing allowed elimination principle + introduced: 23 May 2006, 9c2d70b, r8845, Herbelin (part of universe polymorphism) + impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master (8a01c3685, 24 Jan 2014, Dénès), v8.4 (8a01c3685, 25 Feb 2014, Dénès), v8.3 (2b3cc4f85, 25 Feb 2014, Dénès), v8.2 (459888488, 25 Feb 2014, Dénès), v8.1 (79aa20872, 25 Feb 2014, Dénès) + found by: Dénès + exploit: see GH#3211 + GH issue number: #3211 + risk: ? + + component: universe subtyping + summary: bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop + introduced: V8.2 (bba897d5f, 12 May 2008, Herbelin) + impacted released versions: V8.2-V8.2pl2 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport) + found by: Georgi Guninski + exploit: test-suite/bugs/closed/4294.v + GH issue number: #4294 + risk: ? + +Module system + + component: modules, universes + summary: missing universe constraints in typing "with" clause of a module type + introduced: ? + impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl6; unclear for V8.2 and previous versions + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau) + found by: Dénès + exploit: test-suite/bugs/closed/4294.v + GH issue number: #4294 + risk: ? + +Module system + + component: modules, universes + summary: universe constraints for module subtyping not stored in vo files + introduced: presumably 8.2 (b3d3b56) + impacted released versions: 8.2, 8.3, 8.4 + impacted development branches: v8.5 + impacted coqchk versions: none + fixed in: v8.2 (c1d9889), v8.3 (8056d02), v8.4 (a07deb4), trunk (0cd0a3e) Mar 5, 2014, Tassi + found by: Tassi by running coqchk on the mathematical components library + exploit: requires multiple files, no test provided + GH issue number: #3243 + risk: could be exploited by mistake + +Universes + + component: template polymorphism + summary: issue with two parameters in the same universe level + introduced: 23 May 2006, 9c2d70b, r8845, Herbelin + impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), + found by: Barras + exploit: test-suite/failure/inductive4.v + GH issue number: none + risk: unlikely to be activated by chance + + component: universe polymorphism + summary: universe polymorphism can capture global universes + impacted released versions: V8.5 to V8.8 + impacted coqchk versions: V8.5 to current (NOT FIXED) + fixed in: 2385b5c1ef + found by: Gaëtan Gilbert + exploit: test-suite/misc/poly-capture-global-univs + GH issue number: #8341 + risk: unlikely to be activated by chance (requires a plugin) + +Primitive projections + + component: primitive projections, guard condition + summary: check of guardedness of extra arguments of primitive projections missing + introduced: 6 May 2014, a4043608f, Sozeau + impacted released versions: V8.5-V8.5pl2, + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.5 (ba00867d5, 25 Jul 2016, Sozeau) + found by: Sozeau, by analyzing bug report #4876 + exploit: to be done (?) + GH issue number: #4876 + risk: consequence of bug found by chance, unlikely to be exploited by chance (MS?) + + component: primitive projections, guard condition + summary: records based on primitive projections became possibly recursive without the guard condition being updated + introduced: 10 Sep 2014, 6624459e4, Sozeau (?) + impacted released versions: V8.5 + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès) + found by: Dénès exploiting bug #4588 + exploit: test-suite/bugs/closed/4588.v + GH issue number: #4588 + risk: ? + +Conversion machines + + component: "lazy machine" (lazy krivine abstract machine) + summary: the invariant justifying some optimization was wrong for some combination of sharing side effects + introduced: prior to V7.0 + impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl3 + impacted development branches: none + impacted coqchk versions: (eefe63d52, Barras, 20 May 2008), was in beta-development for 8.2 at this time + fixed in: master/trunk/8.2 (f13aaec57/a8b034513, 15 May 2008, Barras), v8.1 (e7611477a, 15 May 2008, Barras), v8.0 (6ed40a8bc, 29 Nov 2016, Herbelin, backport) + found by: Gonthier + exploit: by Gonthier + GH issue number: none + risk: unrealistic to be exploited by chance + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: collision between constructors when more than 256 constructors in a type + introduced: V8.1 + impacted released versions: V8.1-V8.5pl3, V8.2-V8.2pl2, V8.3-V8.3pl3, V8.4-V8.4pl5 + impacted development branches: none + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport) + found by: Dénès, Pédrot + exploit: test-suite/failure/vm-bug4157.v + GH issue number: #4157 + risk: + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: wrong universe constraints + introduced: possibly exploitable from V8.1; exploitable at least from V8.5 + impacted released versions: V8.1-V8.4pl5 unknown, V8.5-V8.5pl3, V8.6-V8.6.1, V8.7.0-V8.7.1 + impacted development branches: unknown for v8.1-v8.4, none from v8.5 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport) + found by: Dénès + exploit: test-suite/bugs/closed/6677.v + GH issue number: #6677 + risk: + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: missing pops in executing 31bit arithmetic + introduced: V8.5 + impacted released versions: V8.1-V8.4pl5 + impacted development branches: v8.1 (probably) + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (a5e04d9dd, 6 Sep 2015, Dénès), v8.4 (d5aa3bf6, 9 Sep 2015, Dénès), v8.3 (5da5d751, 9 Sep 2015, Dénès), v8.2 (369e82d2, 9 Sep 2015, Dénès), + found by: Catalin Hritcu + exploit: lost? + GH issue number: ? + risk: + + 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 + impacted released versions: V8.5-V8.5pl1 + impacted development branches: none + impacted coqchk versions: none (no native computation in coqchk) + fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), + found by: Letouzey, Dénès + exploit: lost? + GH issue number: ? + risk: + +Conflicts with axioms in library + + component: library of real numbers + summary: axiom of description and decidability of equality on real numbers in library Reals was inconsistent with impredicative Set + introduced: 67c75fa01, 20 Jun 2002 + impacted released versions: 7.3.1, 7.4 + impacted coqchk versions: + fixed by deciding to drop impredicativity of Set: bac707973, 28 Oct 2004 + found by: Herbelin & Werner + exploit: need to find the example again + GH issue number: no + risk: unlikely to be exploited by chance + + component: library of extensional sets, guard condition + summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets + introduced: not a bug per se but an incompatibility discovered late + impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it + impacted coqchk versions: ? + fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès) + found by: Schepler, Dénès, Azevedo de Amorim + exploit: ? + GH issue number: none + risk: unlikely to be exploited by chance (?) + + component: library for axiom of choice and excluded-middle + summary: incompatibility axiom of choice and excluded-middle with elimination of large singletons to Set + introduced: not a bug but a change of intended "model" + impacted released versions: strictly before 8.1 + impacted coqchk versions: ? + fixed by constraining singleton elimination: b19397ed8, r9633, 9 Feb 2007, Herbelin + found by: Benjamin Werner + exploit: + GH issue number: none + risk: + +There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1). + +There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical. + +Another non exploitable bug? + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: bug in 31bit arithmetic + introduced: V8.1 + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (0f8d1b92c, 6 Sep 2015, Dénès) + found by: Dénès, from a bug report by Tahina Ramananandro + exploit: ? + GH issue number: ? + risk: + |