From 4c10de23bc14e419db49631f77f37062ca4a4b6f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 26 May 2021 17:15:34 +0200
Subject: [PATCH] Forbid changing typing flags inside sections

Fix #14317
---
 dev/doc/critical-bugs                          | 12 ++++++++++++
 kernel/environ.mli                             |  2 ++
 kernel/safe_typing.ml                          |  9 +++++++++
 test-suite/{output => bugs/closed}/bug_14317.v |  6 +++---
 test-suite/output/bug_14317.out                |  2 --
 5 files changed, 26 insertions(+), 5 deletions(-)
 rename test-suite/{output => bugs/closed}/bug_14317.v (64%)
 delete mode 100644 test-suite/output/bug_14317.out

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 5c8b8944a73fd..efd466b324268 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -366,6 +366,18 @@ Side-effects
   GH issue number: #13330
   risk: unlikely to be exploited by mistake, requires the use of unsafe tactics
 
+Forgetting unsafe flags
+
+  component: sections
+  summary: unsafe typing flags used inside a section would not be reported by Print Assumptions
+           after closing the section
+  introduced: abab878b8d8b5ca85a4da688abed68518f0b17bd (#10291, 8.11)
+              technically available earlier through plugins
+  impacted coqchk versions: none (coqchk rejects affected files)
+  found by: Anton Trunov
+  GH issue number: #14317
+  risk: low as it needs the use of explicit unsafe flags 
+
 Conflicts with axioms in library
 
   component: library of real numbers
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 414ef2b4d70dc..1e1a3f5b03dad 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -356,6 +356,8 @@ val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
+val same_flags : typing_flags -> typing_flags -> bool
+
 (** [update_typing_flags ?typing_flags] may update env with optional typing flags *)
 val update_typing_flags : ?typing_flags:typing_flags -> env -> env
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5f83e78eb059c..3fa5c5e9221df 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -218,6 +218,15 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_typing_flags flags senv =
+  (* NB: we allow changing the conv_oracle inside sections because it
+     doesn't matter for consistency. *)
+  if Option.has_some senv.sections
+  && not (Environ.same_flags flags
+            {(Environ.typing_flags senv.env) with conv_oracle = flags.conv_oracle})
+  then CErrors.user_err Pp.(str "Changing typing flags inside sections is not allowed.");
+  set_typing_flags flags senv
+
 let set_check_guarded b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with check_guarded = b } senv
diff --git a/test-suite/output/bug_14317.v b/test-suite/bugs/closed/bug_14317.v
similarity index 64%
rename from test-suite/output/bug_14317.v
rename to test-suite/bugs/closed/bug_14317.v
index b579a53e9dbf9..29601072ffef0 100644
--- a/test-suite/output/bug_14317.v
+++ b/test-suite/bugs/closed/bug_14317.v
@@ -1,15 +1,15 @@
 Section FooSect.
 
-  Unset Guard Checking.
+  Fail Unset Guard Checking.
 
   (* Let bad := fix bad (n:nat) : False := bad n. *)
 
-  Fixpoint loop (n : nat) : nat := loop n.
+  (* Fixpoint loop (n : nat) : nat := loop n. *)
 
   (* Set Guard Checking. *)
   (* Definition really_bad := bad 0. *)
 
 End FooSect.
 
-Print Assumptions loop.
+(* Print Assumptions loop. *)
 (* Print Assumptions really_bad. TODO *)
diff --git a/test-suite/output/bug_14317.out b/test-suite/output/bug_14317.out
deleted file mode 100644
index dd3a9c728c3e8..0000000000000
--- a/test-suite/output/bug_14317.out
+++ /dev/null
@@ -1,2 +0,0 @@
-Axioms:
-loop is assumed to be guarded.