diff options
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 7 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13330.v | 17 | ||||
| -rwxr-xr-x | test-suite/misc/13330.sh | 10 | ||||
| -rw-r--r-- | test-suite/misc/13330/bug_13330.v | 16 |
6 files changed, 67 insertions, 5 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 066facd5db..37619833ac 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -312,6 +312,18 @@ Conversion machines risk: none without using -allow-sprop (off by default in 8.10.0), otherwise could be exploited by mistake +Side-effects + + component: side-effects + summary: polymorphic side-effects inside monomorphic definitions incorrectly handled as not inlined + introduced: ? + impacted released versions: at least from 8.6 to 8.12.0 + impacted coqchk versions: none (no side-effects in the checker) + found by: ppedrot + exploit: test-suite/bugs/closed/bug_13330.v + GH issue number: #13330 + risk: unlikely to be exploited by mistake, requires the use of unsafe tactics + Conflicts with axioms in library component: library of real numbers diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 8da5014125..f1bcd2fb44 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1224,6 +1224,13 @@ Changes in 8.12.1 <https://github.com/coq/coq/pull/12738>`_, fixes `#7015 <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert). +- **Fixed:** + Polymorphic side-effects inside monomorphic definitions were incorrectly + handled as not inlined. This allowed deriving an inconsistency + (`#13331 <https://github.com/coq/coq/pull/13331>`_, + fixes `#13330 <https://github.com/coq/coq/issues/13330>`_, + by Pierre-Marie Pédrot). + **Notations** - **Fixed:** diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bf02ceb2c2..6abd283f6c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -671,7 +671,7 @@ let inline_side_effects env body side_eff = let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in let side_eff = List.rev side_eff in (** Most recent side-effects first in side_eff *) - if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) + if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs, 0) else (** Second step: compute the lifts and substitutions to apply *) let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in @@ -725,10 +725,10 @@ let inline_side_effects env body side_eff = else mkLetIn (na, b, ty, accu) in let body = List.fold_right fold_arg args body in - (body, ctx, sigs) + (body, ctx, sigs, len - 1) let inline_private_constants env ((body, ctx), side_eff) = - let body, ctx',_ = inline_side_effects env body side_eff in + let body, ctx', _, _ = inline_side_effects env body side_eff in let ctx' = Univ.ContextSet.union ctx ctx' in (body, ctx') @@ -880,11 +880,11 @@ let add_constant l decl senv = match decl with | OpaqueEntry ce -> let handle env body eff = - let body, uctx, signatures = inline_side_effects env body eff in + let body, uctx, signatures, skip = inline_side_effects env body eff in let trusted = check_signatures senv signatures in let trusted, uctx = match trusted with | None -> 0, uctx - | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx + | Some univs -> skip, Univ.ContextSet.union univs uctx in body, uctx, trusted in diff --git a/test-suite/bugs/closed/bug_13330.v b/test-suite/bugs/closed/bug_13330.v new file mode 100644 index 0000000000..d13de2e58d --- /dev/null +++ b/test-suite/bugs/closed/bug_13330.v @@ -0,0 +1,17 @@ +Polymorphic Inductive path {A : Type} (x : A) : A -> Type := + refl : path x x. + +Goal False. +Proof. +simple refine (let H : False := _ in _). ++ exact_no_check I. ++ assert (path true false -> path false true). + (** Create a dummy polymorphic side-effect *) + { + intro IHn. + rewrite IHn. + reflexivity. + } + exact H. +Fail Qed. +Abort. diff --git a/test-suite/misc/13330.sh b/test-suite/misc/13330.sh new file mode 100755 index 0000000000..7340559432 --- /dev/null +++ b/test-suite/misc/13330.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +$coqc misc/13330/bug_13330.v +R=$? + +if [ $R == 0 ]; then + exit 1 +else + exit 0 +fi diff --git a/test-suite/misc/13330/bug_13330.v b/test-suite/misc/13330/bug_13330.v new file mode 100644 index 0000000000..acf6e80c48 --- /dev/null +++ b/test-suite/misc/13330/bug_13330.v @@ -0,0 +1,16 @@ +Polymorphic Inductive path {A : Type} (x : A) : A -> Type := + refl : path x x. + +Goal False. +Proof. +simple refine (let H : False := _ in _). ++ exact_no_check I. ++ assert (path true false -> path false true). + (** Create a dummy polymorphic side-effect *) + { + intro IHn. + rewrite IHn. + reflexivity. + } + exact H. +Qed. |