Auto merge of #2993 - Vanille-N:tb-protector, r=RalfJung

TB: Redefine trigger condition for protectors

The Coq formalization revealed that as currently implemented, read accesses did not always commute.
Indeed starting from a lazily initialized `Active` protected tag, applying a foreign read then a child read produces `Frozen`, but child read then foreign read triggers UB (because the child read initializes _before_ the `Active -> Frozen`).

This reformulation of when protectors trigger fixes that issue:
- instead of `Active + foreign read -> Frozen` and `Active -> Frozen` when protected is UB
- we do `Active + foreign read -> if protected { Disabled } else { Frozen }`

There is already precedent for transitions being dependent on the presence of a protector (`Reserved + foreign read -> if protected { Frozen } else { Reserved }`), and this has the nice side-effect of simplifying the protector trigger condition to just an equality check against `Disabled` since now there is protector UB iff a protected tag becomes `Disabled`.

In order not to introduce an extra `if`, it was decided that `Disabled -> Disabled` would be UB when protected, which was not the case previously. This is merely a theoretical for now because a protected `Disabled` is unreachable in the first place.

The extra test is not directly related to this modification, but also checks things related to protectors and lazy initialization.

17 files changed, 264 insertions, 151 deletions

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
index 3b2d6f9608e..7723f06f296 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
@@ -227,10 +227,10 @@ pub(super) enum TransitionError {
     ChildAccessForbidden(Permission),
     /// A protector was triggered due to an invalid transition that loses
     /// too much permissions.
-    /// For example, if a protected tag goes from `Active` to `Frozen` due
-    /// to a foreign write this will produce a `ProtectedTransition(PermTransition(Active, Frozen))`.
+    /// For example, if a protected tag goes from `Active` to `Disabled` due
+    /// to a foreign write this will produce a `ProtectedDisabled(Active)`.
     /// This kind of error can only occur on foreign accesses.
-    ProtectedTransition(PermTransition),
+    ProtectedDisabled(Permission),
     /// Cannot deallocate because some tag in the allocation is strongly protected.
     /// This kind of error can only occur on deallocations.
     ProtectedDealloc,
@@ -302,7 +302,7 @@ impl TbError<'_> {
                 ));
                 (title, details, conflicting_tag_name)
             }
-            ProtectedTransition(transition) => {
+            ProtectedDisabled(before_disabled) => {
                 let conflicting_tag_name = "protected";
                 let access = cause.print_as_access(/* is_foreign */ true);
                 let details = vec![
@@ -310,12 +310,9 @@ impl TbError<'_> {
                         "the accessed tag {accessed} is foreign to the {conflicting_tag_name} tag {conflicting} (i.e., it is not a child)"
                     ),
                     format!(
-                        "this {access} would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}"
-                    ),
-                    format!(
-                        "this transition would be {loss}, which is not allowed for protected tags",
-                        loss = transition.summary(),
+                        "this {access} would cause the {conflicting_tag_name} tag {conflicting} (currently {before_disabled}) to become Disabled"
                     ),
+                    format!("protected tags must never be Disabled"),
                 ];
                 (title, details, conflicting_tag_name)
             }
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
index 362070f1857..051b209da17 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
@@ -72,7 +72,12 @@ mod transition {
             // accesses, since the data is not being mutated. Hence the `{ .. }`
             res @ Reserved { .. } if !protected => res,
             Reserved { .. } => Frozen, // protected reserved
-            Active => Frozen,
+            Active =>
+                if protected {
+                    Disabled
+                } else {
+                    Frozen
+                },
             non_writeable @ (Frozen | Disabled) => non_writeable,
         })
     }
@@ -189,34 +194,9 @@ impl PermTransition {
         Permission { inner: self.from }
     }
 
-    /// Determines whether a transition that occured is compatible with the presence
-    /// of a Protector. This is not included in the `transition` functions because
-    /// it would distract from the few places where the transition is modified
-    /// because of a protector, but not forbidden.
-    ///
-    /// Note: this is not in charge of checking that there *is* a protector,
-    /// it should be used as
-    /// ```
-    /// let no_protector_error = if is_protected(tag) {
-    ///     transition.is_allowed_by_protector()
-    /// };
-    /// ```
-    pub fn is_allowed_by_protector(&self) -> bool {
-        assert!(self.is_possible());
-        match (self.from, self.to) {
-            _ if self.from == self.to => true,
-            // It is always a protector violation to not be readable anymore
-            (_, Disabled) => false,
-            // In the case of a `Reserved` under a protector, both transitions
-            // `Reserved => Active` and `Reserved => Frozen` can legitimately occur.
-            // The first is standard (Child Write), the second is for Foreign Writes
-            // on protected Reserved where we must ensure that the pointer is not
-            // written to in the future.
-            (Reserved { .. }, Active) | (Reserved { .. }, Frozen) => true,
-            // This pointer should have stayed writeable for the whole function
-            (Active, Frozen) => false,
-            _ => unreachable!("Transition {} should never be possible", self),
-        }
+    /// Determines if this transition would disable the permission.
+    pub fn produces_disabled(self) -> bool {
+        self.to == Disabled
     }
 }
 
@@ -298,14 +278,15 @@ pub mod diagnostics {
         ///
         /// This function assumes that its arguments apply to the same location
         /// and that they were obtained during a normal execution. It will panic otherwise.
-        /// - `err` cannot be a `ProtectedTransition(_)` of a noop transition, as those
-        /// never trigger protectors;
         /// - all transitions involved in `self` and `err` should be increasing
         /// (Reserved < Active < Frozen < Disabled);
         /// - between `self` and `err` the permission should also be increasing,
         /// so all permissions inside `err` should be greater than `self.1`;
         /// - `Active` and `Reserved` cannot cause an error due to insufficient permissions,
         /// so `err` cannot be a `ChildAccessForbidden(_)` of either of them;
+        /// - `err` should not be `ProtectedDisabled(Disabled)`, because the protected
+        /// tag should not have been `Disabled` in the first place (if this occurs it means
+        /// we have unprotected tags that become protected)
         pub(in super::super) fn is_relevant(&self, err: TransitionError) -> bool {
             // NOTE: `super::super` is the visibility of `TransitionError`
             assert!(self.is_possible());
@@ -342,17 +323,16 @@ pub mod diagnostics {
                             unreachable!("permissions between self and err must be increasing"),
                     }
                 }
-                TransitionError::ProtectedTransition(forbidden) => {
-                    assert!(!forbidden.is_noop());
+                TransitionError::ProtectedDisabled(before_disabled) => {
                     // Show how we got to the starting point of the forbidden transition,
                     // but ignore what came before.
                     // This eliminates transitions like `Reserved -> Active`
                     // when the error is a `Frozen -> Disabled`.
-                    match (self.to, forbidden.from, forbidden.to) {
+                    match (self.to, before_disabled.inner) {
                         // We absolutely want to know where it was activated.
-                        (Active, Active, Frozen | Disabled) => true,
+                        (Active, Active) => true,
                         // And knowing where it became Frozen is also important.
-                        (Frozen, Frozen, Disabled) => true,
+                        (Frozen, Frozen) => true,
                         // If the error is a transition `Frozen -> Disabled`, then we don't really
                         // care whether before that was `Reserved -> Active -> Frozen` or
                         // `Reserved -> Frozen` or even `Frozen` directly.
@@ -360,27 +340,22 @@ pub mod diagnostics {
                         // - created as Frozen, then Frozen -> Disabled is forbidden
                         // - created as Reserved, later became Frozen, then Frozen -> Disabled is forbidden
                         // In both cases the `Reserved -> Active` part is inexistant or irrelevant.
-                        (Active, Frozen, Disabled) => false,
+                        (Active, Frozen) => false,
 
-                        // `Reserved -> Frozen` does not trigger protectors.
-                        (_, Reserved { .. }, Frozen) =>
-                            unreachable!("this transition cannot cause an error"),
+                        (_, Disabled) =>
+                            unreachable!(
+                                "permission that results in Disabled should not itself be Disabled in the first place"
+                            ),
                         // No transition has `Reserved` as its `.to` unless it's a noop.
-                        (Reserved { .. }, _, _) => unreachable!("self is a noop transition"),
-                        (_, Disabled, Disabled) | (_, Frozen, Frozen) | (_, Active, Active) =>
-                            unreachable!("err contains a noop transition"),
+                        (Reserved { .. }, _) => unreachable!("self is a noop transition"),
 
                         // Permissions only evolve in the order `Reserved -> Active -> Frozen -> Disabled`,
                         // so permissions found must be increasing in the order
                         // `self.from < self.to <= forbidden.from < forbidden.to`.
-                        (Disabled, Reserved { .. } | Active | Frozen, _)
-                        | (Frozen, Reserved { .. } | Active, _)
-                        | (Active, Reserved { .. }, _) =>
+                        (Disabled, Reserved { .. } | Active | Frozen)
+                        | (Frozen, Reserved { .. } | Active)
+                        | (Active, Reserved { .. }) =>
                             unreachable!("permissions between self and err must be increasing"),
-                        (_, Disabled, Reserved { .. } | Active | Frozen)
-                        | (_, Frozen, Reserved { .. } | Active)
-                        | (_, Active, Reserved { .. }) =>
-                            unreachable!("permissions within err must be increasing"),
                     }
                 }
                 // We don't care because protectors evolve independently from
@@ -406,7 +381,7 @@ mod propagation_optimization_checks {
         pub use super::*;
         impl PermissionPriv {
             /// Enumerate all states
-            pub fn all() -> impl Iterator<Item = PermissionPriv> {
+            pub fn all() -> impl Iterator<Item = Self> {
                 vec![
                     Active,
                     Reserved { ty_is_freeze: true },
@@ -418,9 +393,15 @@ mod propagation_optimization_checks {
             }
         }
 
+        impl Permission {
+            pub fn all() -> impl Iterator<Item = Self> {
+                PermissionPriv::all().map(|inner| Self { inner })
+            }
+        }
+
         impl AccessKind {
             /// Enumerate all AccessKind.
-            pub fn all() -> impl Iterator<Item = AccessKind> {
+            pub fn all() -> impl Iterator<Item = Self> {
                 use AccessKind::*;
                 [Read, Write].into_iter()
             }
@@ -428,7 +409,7 @@ mod propagation_optimization_checks {
 
         impl AccessRelatedness {
             /// Enumerate all relative positions
-            pub fn all() -> impl Iterator<Item = AccessRelatedness> {
+            pub fn all() -> impl Iterator<Item = Self> {
                 use AccessRelatedness::*;
                 [This, StrictChildAccess, AncestorAccess, DistantAccess].into_iter()
             }
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
index 9e8b1e11899..355356b743a 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
@@ -19,6 +19,7 @@ use rustc_target::abi::Size;
 
 use crate::borrow_tracker::tree_borrows::{
     diagnostics::{self, NodeDebugInfo, TbError, TransitionError},
+    perms::PermTransition,
     unimap::{UniEntry, UniIndex, UniKeyMap, UniValMap},
     Permission,
 };
@@ -28,17 +29,19 @@ use crate::*;
 /// Data for a single *location*.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(super) struct LocationState {
-    /// This pointer's current permission
-    permission: Permission,
-    /// A location is initialized when it is child accessed for the first time,
-    /// and it then stays initialized forever.
-    /// Before initialization we still apply some preemptive transitions on
-    /// `permission` to know what to do in case it ever gets initialized,
-    /// but these can never cause any immediate UB. There can however be UB
-    /// the moment we attempt to initialize (i.e. child-access) because some
-    /// foreign access done between the creation and the initialization is
-    /// incompatible with child accesses.
+    /// A location is initialized when it is child-accessed for the first time (and the initial
+    /// retag initializes the location for the range covered by the type), and it then stays
+    /// initialized forever.
+    /// For initialized locations, "permission" is the current permission. However, for
+    /// uninitialized locations, we still need to track the "future initial permission": this will
+    /// start out to be `default_initial_perm`, but foreign accesses need to be taken into account.
+    /// Crucially however, while transitions to `Disabled` would usually be UB if this location is
+    /// protected, that is *not* the case for uninitialized locations. Instead we just have a latent
+    /// "future initial permission" of `Disabled`, causing UB only if an access is ever actually
+    /// performed.
     initialized: bool,
+    /// This pointer's current permission / future initial permission.
+    permission: Permission,
     /// Strongest foreign access whose effects have already been applied to
     /// this node and all its children since the last child access.
     /// This is `None` if the most recent access is a child access,
@@ -69,6 +72,104 @@ impl LocationState {
     pub fn permission(&self) -> Permission {
         self.permission
     }
+
+    /// Apply the effect of an access to one location, including
+    /// - applying `Permission::perform_access` to the inner `Permission`,
+    /// - emitting protector UB if the location is initialized,
+    /// - updating the initialized status (child accesses produce initialized locations).
+    fn perform_access(
+        &mut self,
+        access_kind: AccessKind,
+        rel_pos: AccessRelatedness,
+        protected: bool,
+    ) -> Result<PermTransition, TransitionError> {
+        let old_perm = self.permission;
+        let transition = Permission::perform_access(access_kind, rel_pos, old_perm, protected)
+            .ok_or(TransitionError::ChildAccessForbidden(old_perm))?;
+        // Why do only initialized locations cause protector errors?
+        // Consider two mutable references `x`, `y` into disjoint parts of
+        // the same allocation. A priori, these may actually both be used to
+        // access the entire allocation, as long as only reads occur. However,
+        // a write to `y` needs to somehow record that `x` can no longer be used
+        // on that location at all. For these uninitialized locations (i.e., locations
+        // that haven't been accessed with `x` yet), we track the "future initial state":
+        // it defaults to whatever the initial state of the tag is,
+        // but the access to `y` moves that "future initial state" of `x` to `Disabled`.
+        // However, usually a `Reserved -> Disabled` transition would be UB due to the protector!
+        // So clearly protectors shouldn't fire for such "future initial state" transitions.
+        //
+        // See the test `two_mut_protected_same_alloc` in `tests/pass/tree_borrows/tree-borrows.rs`
+        // for an example of safe code that would be UB if we forgot to check `self.initialized`.
+        if protected && self.initialized && transition.produces_disabled() {
+            return Err(TransitionError::ProtectedDisabled(old_perm));
+        }
+        self.permission = transition.applied(old_perm).unwrap();
+        self.initialized |= !rel_pos.is_foreign();
+        Ok(transition)
+    }
+
+    // Helper to optimize the tree traversal.
+    // The optimization here consists of observing thanks to the tests
+    // `foreign_read_is_noop_after_write` and `all_transitions_idempotent`,
+    // that there are actually just three possible sequences of events that can occur
+    // in between two child accesses that produce different results.
+    //
+    // Indeed,
+    // - applying any number of foreign read accesses is the same as applying
+    //   exactly one foreign read,
+    // - applying any number of foreign read or write accesses is the same
+    //   as applying exactly one foreign write.
+    // therefore the three sequences of events that can produce different
+    // outcomes are
+    // - an empty sequence (`self.latest_foreign_access = None`)
+    // - a nonempty read-only sequence (`self.latest_foreign_access = Some(Read)`)
+    // - a nonempty sequence with at least one write (`self.latest_foreign_access = Some(Write)`)
+    //
+    // This function not only determines if skipping the propagation right now
+    // is possible, it also updates the internal state to keep track of whether
+    // the propagation can be skipped next time.
+    // It is a performance loss not to call this function when a foreign access occurs.
+    // It is unsound not to call this function when a child access occurs.
+    fn skip_if_known_noop(
+        &mut self,
+        access_kind: AccessKind,
+        rel_pos: AccessRelatedness,
+    ) -> ContinueTraversal {
+        if rel_pos.is_foreign() {
+            let new_access_noop = match (self.latest_foreign_access, access_kind) {
+                // Previously applied transition makes the new one a guaranteed
+                // noop in the two following cases:
+                // (1) justified by `foreign_read_is_noop_after_write`
+                (Some(AccessKind::Write), AccessKind::Read) => true,
+                // (2) justified by `all_transitions_idempotent`
+                (Some(old), new) if old == new => true,
+                // In all other cases there has been a recent enough
+                // child access that the effects of the new foreign access
+                // need to be applied to this subtree.
+                _ => false,
+            };
+            if new_access_noop {
+                // Abort traversal if the new transition is indeed guaranteed
+                // to be noop.
+                // No need to update `self.latest_foreign_access`,
+                // the type of the current streak among nonempty read-only
+                // or nonempty with at least one write has not changed.
+                ContinueTraversal::SkipChildren
+            } else {
+                // Otherwise propagate this time, and also record the
+                // access that just occurred so that we can skip the propagation
+                // next time.
+                self.latest_foreign_access = Some(access_kind);
+                ContinueTraversal::Recurse
+            }
+        } else {
+            // A child access occurred, this breaks the streak of foreign
+            // accesses in a row and the sequence since the previous child access
+            // is now empty.
+            self.latest_foreign_access = None;
+            ContinueTraversal::Recurse
+        }
+    }
 }
 
 /// Tree structure with both parents and children since we want to be
@@ -387,11 +488,15 @@ impl<'tcx> Tree {
         Ok(())
     }
 
-    /// Maps the following propagation procedure to each range:
-    /// - initialize if needed;
-    /// - compute new state after transition;
-    /// - check that there is no protector that would forbid this;
-    /// - record this specific location as accessed.
+    /// Map the per-node and per-location `LocationState::perform_access`
+    /// to each location of `access_range`, on every tag of the allocation.
+    ///
+    /// `LocationState::perform_access` will take care of raising transition
+    /// errors and updating the `initialized` status of each location,
+    /// this traversal adds to that:
+    /// - inserting into the map locations that do not exist yet,
+    /// - trimming the traversal,
+    /// - recording the history.
     pub fn perform_access(
         &mut self,
         access_kind: AccessKind,
@@ -411,55 +516,16 @@ impl<'tcx> Tree {
                         let old_state =
                             perm.or_insert_with(|| LocationState::new(node.default_initial_perm));
 
-                        // Optimize the tree traversal.
-                        // The optimization here consists of observing thanks to the tests
-                        // `foreign_read_is_noop_after_write` and `all_transitions_idempotent`
-                        // that if we apply twice in a row the effects of a foreign access
-                        // we can skip some branches.
-                        // "two foreign accesses in a row" occurs when `perm.latest_foreign_access` is `Some(_)`
-                        // AND the `rel_pos` of the current access corresponds to a foreign access.
-                        if rel_pos.is_foreign() {
-                            let new_access_noop =
-                                match (old_state.latest_foreign_access, access_kind) {
-                                    // Previously applied transition makes the new one a guaranteed
-                                    // noop in the two following cases:
-                                    // (1) justified by `foreign_read_is_noop_after_write`
-                                    (Some(AccessKind::Write), AccessKind::Read) => true,
-                                    // (2) justified by `all_transitions_idempotent`
-                                    (Some(old), new) if old == new => true,
-                                    // In all other cases there has been a recent enough
-                                    // child access that the effects of the new foreign access
-                                    // need to be applied to this subtree.
-                                    _ => false,
-                                };
-                            if new_access_noop {
-                                // Abort traversal if the new transition is indeed guaranteed
-                                // to be noop.
-                                return Ok(ContinueTraversal::SkipChildren);
-                            } else {
-                                // Otherwise propagate this time, and also record the
-                                // access that just occurred so that we can skip the propagation
-                                // next time.
-                                old_state.latest_foreign_access = Some(access_kind);
-                            }
-                        } else {
-                            // A child access occurred, this breaks the streak of "two foreign
-                            // accesses in a row" and we reset this field.
-                            old_state.latest_foreign_access = None;
+                        match old_state.skip_if_known_noop(access_kind, rel_pos) {
+                            ContinueTraversal::SkipChildren =>
+                                return Ok(ContinueTraversal::SkipChildren),
+                            _ => {}
                         }
 
-                        let old_perm = old_state.permission;
                         let protected = global.borrow().protected_tags.contains_key(&node.tag);
                         let transition =
-                            Permission::perform_access(access_kind, rel_pos, old_perm, protected)
-                                .ok_or(TransitionError::ChildAccessForbidden(old_perm))?;
-                        if protected
-                            // Can't trigger Protector on uninitialized locations
-                            && old_state.initialized
-                            && !transition.is_allowed_by_protector()
-                        {
-                            return Err(TransitionError::ProtectedTransition(transition));
-                        }
+                            old_state.perform_access(access_kind, rel_pos, protected)?;
+
                         // Record the event as part of the history
                         if !transition.is_noop() {
                             node.debug_info.history.push(diagnostics::Event {
@@ -470,10 +536,7 @@ impl<'tcx> Tree {
                                 transition_range: perms_range.clone(),
                                 span,
                             });
-                            old_state.permission =
-                                transition.applied(old_state.permission).unwrap();
                         }
-                        old_state.initialized |= !rel_pos.is_foreign();
                         Ok(ContinueTraversal::Recurse)
                     },
                     |args: ErrHandlerArgs<'_, TransitionError>| -> InterpError<'tcx> {
@@ -602,3 +665,57 @@ impl AccessRelatedness {
         }
     }
 }
+
+#[cfg(test)]
+mod commutation_tests {
+    use super::*;
+    impl LocationState {
+        pub fn all_without_access() -> impl Iterator<Item = Self> {
+            Permission::all().flat_map(|permission| {
+                [false, true].into_iter().map(move |initialized| {
+                    Self { permission, initialized, latest_foreign_access: None }
+                })
+            })
+        }
+    }
+
+    #[test]
+    #[rustfmt::skip]
+    // Exhaustive check that for any starting configuration loc,
+    // for any two read accesses r1 and r2, if `loc + r1 + r2` is not UB
+    // and results in `loc'`, then `loc + r2 + r1` is also not UB and results
+    // in the same final state `loc'`.
+    // This lets us justify arbitrary read-read reorderings.
+    fn all_read_accesses_commute() {
+        let kind = AccessKind::Read;
+        // Two of the four combinations of `AccessRelatedness` are trivial,
+        // but we might as well check them all.
+        for rel1 in AccessRelatedness::all() {
+            for rel2 in AccessRelatedness::all() {
+                // Any protector state works, but we can't move reads across function boundaries
+                // so the two read accesses occur under the same protector.
+                for &protected in &[true, false] {
+                    for loc in LocationState::all_without_access() {
+                        // Apply 1 then 2. Failure here means that there is UB in the source
+                        // and we skip the check in the target.
+                        let mut loc12 = loc;
+                        let Ok(_) = loc12.perform_access(kind, rel1, protected) else { continue; };
+                        let Ok(_) = loc12.perform_access(kind, rel2, protected) else { continue; };
+
+                        // If 1 followed by 2 succeeded, then 2 followed by 1 must also succeed...
+                        let mut loc21 = loc;
+                        loc21.perform_access(kind, rel2, protected).unwrap();
+                        loc21.perform_access(kind, rel1, protected).unwrap();
+
+                        // ... and produce the same final result.
+                        assert_eq!(
+                            loc12, loc21,
+                            "Read accesses {:?} followed by {:?} do not commute !",
+                            rel1, rel2
+                        );
+                    }
+                }
+            }
+        }
+    }
+}
diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr
index 4102c718af8..106e5c19bf2 100644
--- a/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr
@@ -6,8 +6,8 @@ LL |         ptr::write(dest, src);
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> to transition from Frozen to Disabled
-   = help: this transition would be a loss of read permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/aliasing_mut4.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr b/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr
index 1d1ed820324..1ecd6620806 100644
--- a/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr
@@ -6,8 +6,8 @@ LL |     *y
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign read access would cause the protected tag <TAG> to transition from Active to Frozen
-   = help: this transition would be a loss of write permissions, which is not allowed for protected tags
+   = help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/box_noalias_violation.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr b/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr
index 7308d045d19..64e08f545e3 100644
--- a/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { *y = 2 };
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> to transition from Active to Disabled
-   = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (currently Active) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/illegal_write6.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr
index ee64a66cc21..66f7f1788e4 100644
--- a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { *x = 0 };
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> to transition from Frozen to Disabled
-   = help: this transition would be a loss of read permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/invalidate_against_protector2.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr
index e217170afb9..ef807d7362e 100644
--- a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { *x = 0 };
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> to transition from Frozen to Disabled
-   = help: this transition would be a loss of read permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/invalidate_against_protector3.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr b/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr
index 00b2708a651..f26fc6cbaae 100644
--- a/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> to transition from Frozen to Disabled
-   = help: this transition would be a loss of read permissions, which is not allowed for protected tags
+   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/newtype_pair_retagging.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr b/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr
index aed2e7abebc..687c72d574d 100644
--- a/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> to transition from Frozen to Disabled
-   = help: this transition would be a loss of read permissions, which is not allowed for protected tags
+   = help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Frozen) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/newtype_retagging.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr b/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr
index 35c02cc2ebd..8393b80f25b 100644
--- a/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr
+++ b/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { ptr.write(S(0)) };
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> to transition from Active to Disabled
-   = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (currently Active) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/arg_inplace_mutate.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr b/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr
index cbd76c38f62..5af4856bbe3 100644
--- a/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr
+++ b/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { ptr.read() };
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign read access would cause the protected tag <TAG> to transition from Active to Frozen
-   = help: this transition would be a loss of write permissions, which is not allowed for protected tags
+   = help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/arg_inplace_observe_during.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr b/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr
index c2c9de3f4ee..c491a904a10 100644
--- a/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr
+++ b/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr
@@ -6,8 +6,8 @@ LL |     unsafe { ptr.read() };
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign read access would cause the protected tag <TAG> to transition from Active to Frozen
-   = help: this transition would be a loss of write permissions, which is not allowed for protected tags
+   = help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/return_pointer_aliasing.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr b/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr
index 0feafb1a71e..8b3bf8414db 100644
--- a/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr
@@ -6,8 +6,8 @@ LL |     *y.add(3) = 42;
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> to transition from Reserved to Disabled
-   = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (currently Reserved) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/outside-range.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr
index c77f1492a97..769769d957d 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr
@@ -16,8 +16,8 @@ LL |             *y = 1;
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled
-   = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/cell-protected-write.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr
index ac8788112e9..f7e9fb9e3c3 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr
@@ -16,8 +16,8 @@ LL |             *y = 0;
    |
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
    = help: the accessed tag <TAG> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
-   = help: this foreign write access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled
-   = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
+   = help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved) to become Disabled
+   = help: protected tags must never be Disabled
 help: the accessed tag <TAG> was created here
   --> $DIR/int-protected-write.rs:LL:CC
    |
diff --git a/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs b/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs
index 6bdad695965..0d50d54faf6 100644
--- a/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs
+++ b/src/tools/miri/tests/pass/tree_borrows/tree-borrows.rs
@@ -9,6 +9,7 @@ use std::ptr;
 fn main() {
     aliasing_read_only_mutable_refs();
     string_as_mut_ptr();
+    two_mut_protected_same_alloc();
 
     // Stacked Borrows tests
     read_does_not_invalidate1();
@@ -62,6 +63,23 @@ pub fn string_as_mut_ptr() {
     }
 }
 
+// This function checks that there is no issue with having two mutable references
+// from the same allocation both under a protector.
+// This is safe code, it must absolutely not be UB.
+// This test failing is a symptom of forgetting to check that only initialized
+// locations can cause protector UB.
+fn two_mut_protected_same_alloc() {
+    fn write_second(_x: &mut u8, y: &mut u8) {
+        // write through `y` will make some locations of `x` (protected)
+        // become Disabled. Those locations are outside of the range on which
+        // `x` is initialized, and the protector must not trigger.
+        *y = 1;
+    }
+
+    let mut data = (0u8, 1u8);
+    write_second(&mut data.0, &mut data.1);
+}
+
 // ----- The tests below were taken from Stacked Borrows ----
 
 // Make sure that reading from an `&mut` does, like reborrowing to `&`,