Auto merge of #3754 - Vanille-N:master, r=RalfJung

Make unused states of Reserved unrepresentable

In the [previous TB update](https://github.com/rust-lang/miri/pull/3742) we discovered that the existence of `Reserved + !ty_is_freeze + protected` is undesirable.

This has the side effect of making `Reserved { conflicted: true, ty_is_freeze: false }` unreachable.
As such it is desirable that this state would also be unrepresentable.

This PR eliminates the unused configuration by changing
```rs
enum PermissionPriv {
    Reserved { ty_is_freeze: bool, conflicted: bool },
    ...
}
```
into
```rs
enum PermissionPriv {
    ReservedFrz { conflicted: bool },
    ReservedIM,
    ...
}
```
but this is not the only solution and `Reserved(Activable | Conflicted | InteriorMut)` could be discussed.
In addition to making the unreachable state not representable anymore, this change has the nice side effect of enabling `foreign_read` to no longer depend explicitly on the `protected` flag.

Currently waiting for
- `@JoJoDeveloping` to confirm that this is the same representation of `Reserved` as what is being implemented in simuliris,
- `@RalfJung` to approve that this does not introduce too much overhead in the trusted codebase.

13 files changed, 200 insertions, 134 deletions

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
index 44f42d5fb9c..722cb79c66b 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
@@ -1,10 +1,6 @@
 use rustc_middle::{
     mir::{Mutability, RetagKind},
-    ty::{
-        self,
-        layout::{HasParamEnv, HasTyCtxt},
-        Ty,
-    },
+    ty::{self, layout::HasParamEnv, Ty},
 };
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{Abi, Size};
@@ -146,10 +142,9 @@ impl<'tcx> NewPermission {
         // interior mutability and protectors interact poorly.
         // To eliminate the case of Protected Reserved IM we override interior mutability
         // in the case of a protected reference: protected references are always considered
-        // "freeze".
+        // "freeze" in their reservation phase.
         let initial_state = match mutability {
-            Mutability::Mut if ty_is_unpin =>
-                Permission::new_reserved(ty_is_freeze || is_protected),
+            Mutability::Mut if ty_is_unpin => Permission::new_reserved(ty_is_freeze, is_protected),
             Mutability::Not if ty_is_freeze => Permission::new_frozen(),
             // Raw pointers never enter this function so they are not handled.
             // However raw pointers are not the only pointers that take the parent
@@ -176,10 +171,12 @@ impl<'tcx> NewPermission {
             // Regular `Unpin` box, give it `noalias` but only a weak protector
             // because it is valid to deallocate it within the function.
             let ty_is_freeze = ty.is_freeze(*cx.tcx, cx.param_env());
+            let protected = kind == RetagKind::FnEntry;
+            let initial_state = Permission::new_reserved(ty_is_freeze, protected);
             Self {
                 zero_size,
-                initial_state: Permission::new_reserved(ty_is_freeze),
-                protector: (kind == RetagKind::FnEntry).then_some(ProtectorKind::WeakProtector),
+                initial_state,
+                protector: protected.then_some(ProtectorKind::WeakProtector),
             }
         })
     }
@@ -521,11 +518,13 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
     fn tb_protect_place(&mut self, place: &MPlaceTy<'tcx>) -> InterpResult<'tcx, MPlaceTy<'tcx>> {
         let this = self.eval_context_mut();
 
+        // Note: if we were to inline `new_reserved` below we would find out that
+        // `ty_is_freeze` is eventually unused because it appears in a `ty_is_freeze || true`.
+        // We are nevertheless including it here for clarity.
+        let ty_is_freeze = place.layout.ty.is_freeze(*this.tcx, this.param_env());
         // Retag it. With protection! That is the entire point.
         let new_perm = NewPermission {
-            initial_state: Permission::new_reserved(
-                place.layout.ty.is_freeze(this.tcx(), this.param_env()),
-            ),
+            initial_state: Permission::new_reserved(ty_is_freeze, /* protected */ true),
             zero_size: false,
             protector: Some(ProtectorKind::StrongProtector),
         };
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 8e23257b6c0..5461edb51d3 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
@@ -8,10 +8,16 @@ use crate::AccessKind;
 /// The activation states of a pointer.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 enum PermissionPriv {
-    /// represents: a local reference that has not yet been written to;
-    /// allows: child reads, foreign reads, foreign writes if type is freeze;
+    /// represents: a local mutable reference that has not yet been written to;
+    /// allows: child reads, foreign reads;
     /// affected by: child writes (becomes Active),
-    /// rejects: foreign writes (Disabled, except if type is not freeze).
+    /// rejects: foreign writes (Disabled).
+    ///
+    /// `ReservedFrz` is mostly for types that are `Freeze` (no interior mutability).
+    /// If the type has interior mutability, see `ReservedIM` instead.
+    /// (Note: since the discovery of `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
+    /// we also use `ReservedFreeze` for mutable references that were retagged with a protector
+    /// independently of interior mutability)
     ///
     /// special case: behaves differently when protected, which is where `conflicted`
     /// is relevant
@@ -22,12 +28,12 @@ enum PermissionPriv {
     /// - foreign-read then child-write is UB due to `conflicted`,
     /// - child-write then foreign-read is UB since child-write will activate and then
     ///   foreign-read disables a protected `Active`, which is UB.
-    ///
-    /// Note: since the discovery of `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
-    /// `ty_is_freeze` does not strictly mean that the type has no interior mutability,
-    /// it could be an interior mutable type that lost its interior mutability privileges
-    /// when retagged with a protector.
-    Reserved { ty_is_freeze: bool, conflicted: bool },
+    ReservedFrz { conflicted: bool },
+    /// Alternative version of `ReservedFrz` made for types with interior mutability.
+    /// allows: child reads, foreign reads, foreign writes (extra);
+    /// affected by: child writes (becomes Active);
+    /// rejects: nothing.
+    ReservedIM,
     /// represents: a unique pointer;
     /// allows: child reads, child writes;
     /// rejects: foreign reads (Frozen), foreign writes (Disabled).
@@ -59,17 +65,14 @@ impl PartialOrd for PermissionPriv {
             (_, Frozen) => Less,
             (Active, _) => Greater,
             (_, Active) => Less,
-            (
-                Reserved { ty_is_freeze: f1, conflicted: c1 },
-                Reserved { ty_is_freeze: f2, conflicted: c2 },
-            ) => {
-                // No transition ever changes `ty_is_freeze`.
-                if f1 != f2 {
-                    return None;
-                }
+            (ReservedIM, ReservedIM) => Equal,
+            (ReservedFrz { conflicted: c1 }, ReservedFrz { conflicted: c2 }) => {
                 // `bool` is ordered such that `false <= true`, so this works as intended.
                 c1.cmp(c2)
             }
+            // Versions of `Reserved` with different interior mutability are incomparable with each
+            // other.
+            (ReservedIM, ReservedFrz { .. }) | (ReservedFrz { .. }, ReservedIM) => return None,
         })
     }
 }
@@ -77,7 +80,12 @@ impl PartialOrd for PermissionPriv {
 impl PermissionPriv {
     /// Check if `self` can be the initial state of a pointer.
     fn is_initial(&self) -> bool {
-        matches!(self, Reserved { conflicted: false, .. } | Frozen)
+        matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM)
+    }
+
+    /// Reject `ReservedIM` that cannot exist in the presence of a protector.
+    fn compatible_with_protector(&self) -> bool {
+        !matches!(self, ReservedIM)
     }
 }
 
@@ -93,7 +101,7 @@ mod transition {
             Disabled => return None,
             // The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
             // accesses, since the data is not being mutated. Hence the `{ .. }`.
-            readable @ (Reserved { .. } | Active | Frozen) => readable,
+            readable @ (ReservedFrz { .. } | ReservedIM | Active | Frozen) => readable,
         })
     }
 
@@ -109,11 +117,16 @@ mod transition {
 
             // Someone else read. To make sure we won't write before function exit,
             // we set the "conflicted" flag, which will disallow writes while we are protected.
-            Reserved { ty_is_freeze, .. } if protected =>
-                Reserved { ty_is_freeze, conflicted: true },
+            ReservedFrz { .. } if protected => ReservedFrz { conflicted: true },
             // Before activation and without protectors, foreign reads are fine.
             // That's the entire point of 2-phase borrows.
-            res @ Reserved { .. } => res,
+            res @ (ReservedFrz { .. } | ReservedIM) => {
+                // Even though we haven't checked `ReservedIM if protected` separately,
+                // it is a state that cannot occur because under a protector we only
+                // create `ReservedFrz` never `ReservedIM`.
+                assert!(!protected);
+                res
+            }
             Active =>
                 if protected {
                     // We wrote, someone else reads -- that's bad.
@@ -134,10 +147,10 @@ mod transition {
             // If the `conflicted` flag is set, then there was a foreign read during
             // the function call that is still ongoing (still `protected`),
             // this is UB (`noalias` violation).
-            Reserved { conflicted: true, .. } if protected => return None,
+            ReservedFrz { conflicted: true } if protected => return None,
             // A write always activates the 2-phase borrow, even with interior
             // mutability
-            Reserved { .. } | Active => Active,
+            ReservedFrz { .. } | ReservedIM | Active => Active,
             Frozen | Disabled => return None,
         })
     }
@@ -145,15 +158,15 @@ mod transition {
     /// A non-child node was write-accessed: this makes everything `Disabled` except for
     /// non-protected interior mutable `Reserved` which stay the same.
     fn foreign_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
+        // There is no explicit dependency on `protected`, but recall that interior mutable
+        // types receive a `ReservedFrz` instead of `ReservedIM` when retagged under a protector,
+        // so the result of this function does indirectly depend on (past) protector status.
         Some(match state {
-            // FIXME: since the fix related to reservedim_spurious_write, it is now possible
-            // to express these transitions of the state machine without an explicit dependency
-            // on `protected`: because `ty_is_freeze: false` implies `!protected` then
-            // the line handling `Reserved { .. } if protected` could be deleted.
-            // This will however require optimizations to the exhaustive tests because
-            // fewer initial conditions are valid.
-            Reserved { .. } if protected => Disabled,
-            res @ Reserved { ty_is_freeze: false, .. } => res,
+            res @ ReservedIM => {
+                // We can never create a `ReservedIM` under a protector, only `ReservedFrz`.
+                assert!(!protected);
+                res
+            }
             _ => Disabled,
         })
     }
@@ -208,9 +221,23 @@ impl Permission {
         Self { inner: Active }
     }
 
-    /// Default initial permission of a reborrowed mutable reference.
-    pub fn new_reserved(ty_is_freeze: bool) -> Self {
-        Self { inner: Reserved { ty_is_freeze, conflicted: false } }
+    /// Default initial permission of a reborrowed mutable reference that is either
+    /// protected or not interior mutable.
+    fn new_reserved_frz() -> Self {
+        Self { inner: ReservedFrz { conflicted: false } }
+    }
+
+    /// Default initial permission of an unprotected interior mutable reference.
+    fn new_reserved_im() -> Self {
+        Self { inner: ReservedIM }
+    }
+
+    /// Wrapper around `new_reserved_frz` and `new_reserved_im` that decides
+    /// which to call based on the interior mutability and the retag kind (whether there
+    /// is a protector is relevant because being protected takes priority over being
+    /// interior mutable)
+    pub fn new_reserved(ty_is_freeze: bool, protected: bool) -> Self {
+        if ty_is_freeze || protected { Self::new_reserved_frz() } else { Self::new_reserved_im() }
     }
 
     /// Default initial permission of a reborrowed shared reference.
@@ -224,6 +251,11 @@ impl Permission {
         Self { inner: Disabled }
     }
 
+    /// Reject `ReservedIM` that cannot exist in the presence of a protector.
+    pub fn compatible_with_protector(&self) -> bool {
+        self.inner.compatible_with_protector()
+    }
+
     /// Apply the transition to the inner PermissionPriv.
     pub fn perform_access(
         kind: AccessKind,
@@ -279,12 +311,9 @@ pub mod diagnostics {
                 f,
                 "{}",
                 match self {
-                    Reserved { ty_is_freeze: true, conflicted: false } => "Reserved",
-                    Reserved { ty_is_freeze: true, conflicted: true } => "Reserved (conflicted)",
-                    Reserved { ty_is_freeze: false, conflicted: false } =>
-                        "Reserved (interior mutable)",
-                    Reserved { ty_is_freeze: false, conflicted: true } =>
-                        "Reserved (interior mutable, conflicted)",
+                    ReservedFrz { conflicted: false } => "Reserved",
+                    ReservedFrz { conflicted: true } => "Reserved (conflicted)",
+                    ReservedIM => "Reserved (interior mutable)",
                     Active => "Active",
                     Frozen => "Frozen",
                     Disabled => "Disabled",
@@ -312,10 +341,9 @@ pub mod diagnostics {
             // and also as `diagnostics::DisplayFmtPermission.uninit` otherwise
             // alignment will be incorrect.
             match self.inner {
-                Reserved { ty_is_freeze: true, conflicted: false } => "Rs  ",
-                Reserved { ty_is_freeze: true, conflicted: true } => "RsC ",
-                Reserved { ty_is_freeze: false, conflicted: false } => "RsM ",
-                Reserved { ty_is_freeze: false, conflicted: true } => "RsCM",
+                ReservedFrz { conflicted: false } => "Res ",
+                ReservedFrz { conflicted: true } => "ResC",
+                ReservedIM => "ReIM",
                 Active => "Act ",
                 Frozen => "Frz ",
                 Disabled => "Dis ",
@@ -325,13 +353,14 @@ pub mod diagnostics {
 
     impl PermTransition {
         /// Readable explanation of the consequences of an event.
-        /// Fits in the sentence "This accessed caused {trans.summary()}".
+        /// Fits in the sentence "This transition corresponds to {trans.summary()}".
         pub fn summary(&self) -> &'static str {
             assert!(self.is_possible());
+            assert!(!self.is_noop());
             match (self.from, self.to) {
                 (_, Active) => "the first write to a 2-phase borrowed mutable reference",
                 (_, Frozen) => "a loss of write permissions",
-                (Reserved { conflicted: false, .. }, Reserved { conflicted: true, .. }) =>
+                (ReservedFrz { conflicted: false }, ReservedFrz { conflicted: true }) =>
                     "a temporary loss of write permissions until function exit",
                 (Frozen, Disabled) => "a loss of read permissions",
                 (_, Disabled) => "a loss of read and write permissions",
@@ -380,28 +409,33 @@ pub mod diagnostics {
                         (Frozen, Frozen) => true,
                         (Active, Frozen) => true,
                         (Disabled, Disabled) => true,
-                        (Reserved { conflicted: true, .. }, Reserved { conflicted: true, .. }) =>
-                            true,
+                        (
+                            ReservedFrz { conflicted: true, .. },
+                            ReservedFrz { conflicted: true, .. },
+                        ) => true,
                         // A pointer being `Disabled` is a strictly stronger source of
                         // errors than it being `Frozen`. If we try to access a `Disabled`,
                         // then where it became `Frozen` (or `Active` or `Reserved`) is the least
                         // of our concerns for now.
-                        (Reserved { conflicted: true, .. } | Active | Frozen, Disabled) => false,
-                        (Reserved { conflicted: true, .. }, Frozen) => false,
+                        (ReservedFrz { conflicted: true } | Active | Frozen, Disabled) => false,
+                        (ReservedFrz { conflicted: true }, Frozen) => false,
 
                         // `Active` and `Reserved` have all permissions, so a
                         // `ChildAccessForbidden(Reserved | Active)` can never exist.
-                        (_, Active) | (_, Reserved { conflicted: false, .. }) =>
+                        (_, Active) | (_, ReservedFrz { conflicted: false }) =>
                             unreachable!("this permission cannot cause an error"),
-                        // No transition has `Reserved(conflicted=false)` as its `.to` unless it's a noop.
-                        (Reserved { conflicted: false, .. }, _) =>
+                        // No transition has `Reserved { conflicted: false }` or `ReservedIM`
+                        // as its `.to` unless it's a noop.
+                        (ReservedFrz { conflicted: false } | ReservedIM, _) =>
                             unreachable!("self is a noop transition"),
                         // All transitions produced in normal executions (using `apply_access`)
                         // change permissions in the order `Reserved -> Active -> Frozen -> Disabled`.
                         // We assume that the error was triggered on the same location that
                         // the transition `self` applies to, so permissions found must be increasing
                         // in the order `self.from < self.to <= insufficient.inner`
-                        (Active | Frozen | Disabled, Reserved { .. }) | (Disabled, Frozen) =>
+                        (Active | Frozen | Disabled, ReservedFrz { .. } | ReservedIM)
+                        | (Disabled, Frozen)
+                        | (ReservedFrz { .. }, ReservedIM) =>
                             unreachable!("permissions between self and err must be increasing"),
                     }
                 }
@@ -415,8 +449,10 @@ pub mod diagnostics {
                         // conflicted.
                         (Active, Active) => true,
                         (Frozen, Frozen) => true,
-                        (Reserved { conflicted: true, .. }, Reserved { conflicted: true, .. }) =>
-                            true,
+                        (
+                            ReservedFrz { conflicted: true, .. },
+                            ReservedFrz { conflicted: true, .. },
+                        ) => true,
                         // If the error is a transition `Frozen -> Disabled`, then we don't really
                         // care whether before that was `Reserved -> Active -> Frozen` or
                         // `Frozen` directly.
@@ -429,23 +465,23 @@ pub mod diagnostics {
                         //   -> Reserved { conflicted: true }` is inexistant or irrelevant,
                         // and so is the `Reserved { conflicted: false } -> Active`
                         (Active, Frozen) => false,
-                        (Reserved { conflicted: true, .. }, _) => false,
+                        (ReservedFrz { conflicted: true }, _) => false,
 
                         (_, Disabled) =>
                             unreachable!(
                                 "permission that results in Disabled should not itself be Disabled in the first place"
                             ),
-                        // No transition has `Reserved { conflicted: false }` as its `.to`
+                        // No transition has `Reserved { conflicted: false }` or `ReservedIM` as its `.to`
                         // unless it's a noop.
-                        (Reserved { conflicted: false, .. }, _) =>
+                        (ReservedFrz { conflicted: false } | ReservedIM, _) =>
                             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, ReservedFrz { .. } | ReservedIM | Active | Frozen)
+                        | (Frozen, ReservedFrz { .. } | ReservedIM | Active)
+                        | (Active, ReservedFrz { .. } | ReservedIM) =>
                             unreachable!("permissions between self and err must be increasing"),
                     }
                 }
@@ -466,9 +502,9 @@ pub mod diagnostics {
 
 #[cfg(test)]
 impl Permission {
-    pub fn is_reserved_with_conflicted(&self, expected_conflicted: bool) -> bool {
+    pub fn is_reserved_frz_with_conflicted(&self, expected_conflicted: bool) -> bool {
         match self.inner {
-            Reserved { conflicted, .. } => conflicted == expected_conflicted,
+            ReservedFrz { conflicted } => conflicted == expected_conflicted,
             _ => false,
         }
     }
@@ -482,10 +518,9 @@ mod propagation_optimization_checks {
     impl Exhaustive for PermissionPriv {
         fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
             Box::new(
-                vec![Active, Frozen, Disabled].into_iter().chain(
-                    <[bool; 2]>::exhaustive()
-                        .map(|[ty_is_freeze, conflicted]| Reserved { ty_is_freeze, conflicted }),
-                ),
+                vec![Active, Frozen, Disabled, ReservedIM]
+                    .into_iter()
+                    .chain(<bool>::exhaustive().map(|conflicted| ReservedFrz { conflicted })),
             )
         }
     }
@@ -525,6 +560,9 @@ mod propagation_optimization_checks {
                 // We thus eliminate from this test and all other tests
                 // the case where the tag is initially unprotected and later becomes protected.
                 precondition!(old_protected || !new_protected);
+                if old_protected {
+                    precondition!(old.compatible_with_protector());
+                }
                 for (access, rel_pos) in <(AccessKind, AccessRelatedness)>::exhaustive() {
                     if let Some(new) = perform_access(access, rel_pos, old, old_protected) {
                         assert_eq!(
@@ -546,6 +584,9 @@ mod propagation_optimization_checks {
         for old in PermissionPriv::exhaustive() {
             for [old_protected, new_protected] in <[bool; 2]>::exhaustive() {
                 precondition!(old_protected || !new_protected);
+                if old_protected {
+                    precondition!(old.compatible_with_protector());
+                }
                 for rel_pos in AccessRelatedness::exhaustive() {
                     precondition!(rel_pos.is_foreign());
                     if let Some(new) = perform_access(old_access, rel_pos, old, old_protected) {
@@ -570,6 +611,9 @@ mod propagation_optimization_checks {
                 reach.insert((start, start));
                 for (access, rel) in <(AccessKind, AccessRelatedness)>::exhaustive() {
                     for prot in bool::exhaustive() {
+                        if prot {
+                            precondition!(start.compatible_with_protector());
+                        }
                         if let Some(end) = transition::perform_access(access, rel, start, prot) {
                             reach.insert((start, end));
                         }
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
index 73717014e89..654419c099d 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
@@ -14,6 +14,15 @@ impl Exhaustive for LocationState {
     }
 }
 
+impl LocationState {
+    /// Ensure that the current internal state can exist at the same time as a protector.
+    /// In practice this only eliminates `ReservedIM` that is never used in the presence
+    /// of a protector (we instead emit `ReservedFrz` on retag).
+    pub fn compatible_with_protector(&self) -> bool {
+        self.permission.compatible_with_protector()
+    }
+}
+
 #[test]
 #[rustfmt::skip]
 // Exhaustive check that for any starting configuration loc,
@@ -30,6 +39,9 @@ fn all_read_accesses_commute() {
         // so the two read accesses occur under the same protector.
         for protected in bool::exhaustive() {
             for loc in LocationState::exhaustive() {
+                if protected {
+                    precondition!(loc.compatible_with_protector());
+                }
                 // 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;
@@ -61,8 +73,8 @@ fn protected_enforces_noalias() {
         // We want to check pairs of accesses where one is foreign and one is not.
         precondition!(rel1.is_foreign() != rel2.is_foreign());
         for [kind1, kind2] in <[AccessKind; 2]>::exhaustive() {
-            for mut state in LocationState::exhaustive() {
-                let protected = true;
+            let protected = true;
+            for mut state in LocationState::exhaustive().filter(|s| s.compatible_with_protector()) {
                 precondition!(state.perform_access(kind1, rel1, protected).is_ok());
                 precondition!(state.perform_access(kind2, rel2, protected).is_ok());
                 // If these were both allowed, it must have been two reads.
@@ -387,6 +399,9 @@ mod spurious_read {
 
         fn retag_y(self, new_y: LocStateProt) -> Result<Self, ()> {
             assert!(new_y.is_initial());
+            if new_y.prot && !new_y.state.compatible_with_protector() {
+                return Err(());
+            }
             // `xy_rel` changes to "mutually foreign" now: `y` can no longer be a parent of `x`.
             Self { y: new_y, xy_rel: RelPosXY::MutuallyForeign, ..self }
                 .read_if_initialized(PtrSelector::Y)
@@ -511,7 +526,7 @@ mod spurious_read {
     }
 
     #[test]
-    // `Reserved(aliased=false)` and `Reserved(aliased=true)` are properly indistinguishable
+    // `Reserved { conflicted: false }` and `Reserved { conflicted: true }` are properly indistinguishable
     // under the conditions where we want to insert a spurious read.
     fn reserved_aliased_protected_indistinguishable() {
         let source = LocStateProtPair {
@@ -521,14 +536,16 @@ mod spurious_read {
                 prot: true,
             },
             y: LocStateProt {
-                state: LocationState::new_uninit(Permission::new_reserved(false)),
+                state: LocationState::new_uninit(Permission::new_reserved(
+                    /* freeze */ true, /* protected */ true,
+                )),
                 prot: true,
             },
         };
         let acc = TestAccess { ptr: PtrSelector::X, kind: AccessKind::Read };
         let target = source.clone().perform_test_access(&acc).unwrap();
-        assert!(source.y.state.permission.is_reserved_with_conflicted(false));
-        assert!(target.y.state.permission.is_reserved_with_conflicted(true));
+        assert!(source.y.state.permission.is_reserved_frz_with_conflicted(false));
+        assert!(target.y.state.permission.is_reserved_frz_with_conflicted(true));
         assert!(!source.distinguishable::<(), ()>(&target))
     }
 
@@ -563,7 +580,13 @@ mod spurious_read {
                     precondition!(x_retag_perm.initialized);
                     // And `x` just got retagged, so it must be initial.
                     precondition!(x_retag_perm.permission.is_initial());
+                    // As stated earlier, `x` is always protected in the patterns we consider here.
+                    precondition!(x_retag_perm.compatible_with_protector());
                     for y_protected in bool::exhaustive() {
+                        // Finally `y` that is optionally protected must have a compatible permission.
+                        if y_protected {
+                            precondition!(y_current_perm.compatible_with_protector());
+                        }
                         v.push(Pattern { xy_rel, x_retag_perm, y_current_perm, y_protected });
                     }
                 }
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 ce9a5b7f158..133a50938f2 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
@@ -2,11 +2,11 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| RsM |      └─┬──<TAG=base>
-| RsM |        ├─┬──<TAG=x>
-| RsM |        │ └─┬──<TAG=caller:x>
-| Rs  |        │   └────<TAG=callee:x> Strongly protected
-| RsM |        └────<TAG=y, callee:y, caller:y>
+| ReIM|      └─┬──<TAG=base>
+| ReIM|        ├─┬──<TAG=x>
+| ReIM|        │ └─┬──<TAG=caller:x>
+| Res |        │   └────<TAG=callee:x> Strongly protected
+| ReIM|        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────
 error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
   --> $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 41559587bda..a4dc123979e 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
@@ -2,11 +2,11 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=n>
-| Rs  |        ├─┬──<TAG=x>
-| Rs  |        │ └─┬──<TAG=caller:x>
-| Rs  |        │   └────<TAG=callee:x> Strongly protected
-| Rs  |        └────<TAG=y, callee:y, caller:y>
+| Res |      └─┬──<TAG=n>
+| Res |        ├─┬──<TAG=x>
+| Res |        │ └─┬──<TAG=caller:x>
+| Res |        │   └────<TAG=callee:x> Strongly protected
+| Res |        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────
 error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
   --> $DIR/int-protected-write.rs:LL:CC
diff --git a/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr b/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr
index 57caa09c888..d13e9ad0215 100644
--- a/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr
@@ -2,7 +2,7 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| RsM |      └────<TAG=data, x, y>
+| ReIM|      └────<TAG=data, x, y>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
diff --git a/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr b/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr
index 69b8a17dc5e..4d77d96776d 100644
--- a/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr
@@ -2,27 +2,27 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=data>
-| Rs  |        └────<TAG=x>
+| Res |      └─┬──<TAG=data>
+| Res |        └────<TAG=x>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=data>
-| Rs  |        └─┬──<TAG=x>
-| Rs  |          └─┬──<TAG=caller:x>
-| Rs  |            └────<TAG=callee:x> Strongly protected
+| Res |      └─┬──<TAG=data>
+| Res |        └─┬──<TAG=x>
+| Res |          └─┬──<TAG=caller:x>
+| Res |            └────<TAG=callee:x> Strongly protected
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=data>
-| Rs  |        ├─┬──<TAG=x>
-| Rs  |        │ └─┬──<TAG=caller:x>
-| Rs  |        │   └────<TAG=callee:x>
-| Rs  |        └────<TAG=y>
+| Res |      └─┬──<TAG=data>
+| Res |        ├─┬──<TAG=x>
+| Res |        │ └─┬──<TAG=caller:x>
+| Res |        │   └────<TAG=callee:x>
+| Res |        └────<TAG=y>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
diff --git a/src/tools/miri/tests/pass/tree_borrows/formatting.stderr b/src/tools/miri/tests/pass/tree_borrows/formatting.stderr
index 235ab68fe01..29f99034bab 100644
--- a/src/tools/miri/tests/pass/tree_borrows/formatting.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/formatting.stderr
@@ -2,7 +2,7 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1..   2..  10..  11.. 100.. 101..1000..1001..1024
 | Act | Act | Act | Act | Act | Act | Act | Act | Act |    └─┬──<TAG=root of the allocation>
-| Rs  | Act | Rs  | Act | Rs  | Act | Rs  | Act | Rs  |      └─┬──<TAG=data, data>
+| Res | Act | Res | Act | Res | Act | Res | Act | Res |      └─┬──<TAG=data, data>
 |-----| Act |-----|?Dis |-----|?Dis |-----|?Dis |-----|        ├────<TAG=data[1]>
 |-----|-----|-----| Act |-----|?Dis |-----|?Dis |-----|        ├────<TAG=data[10]>
 |-----|-----|-----|-----|-----| Frz |-----|?Dis |-----|        ├────<TAG=data[100]>
diff --git a/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr b/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr
index f09aa52f1a1..d589a062111 100644
--- a/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr
@@ -11,5 +11,5 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 | Act |    └─┬──<TAG=root of the allocation>
 | Act |      └─┬──<TAG=parent>
 | Frz |        ├────<TAG=x>
-| Rs  |        └────<TAG=y>
+| Res |        └────<TAG=y>
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
index d149a4065f9..be90382640b 100644
--- a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
@@ -3,20 +3,20 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| RsM |      └─┬──<TAG=base>
-| RsM |        ├─┬──<TAG=x>
-| RsM |        │ └─┬──<TAG=caller:x>
-| RsC |        │   └────<TAG=callee:x>
-| RsM |        └────<TAG=y, caller:y, callee:y>
+| ReIM|      └─┬──<TAG=base>
+| ReIM|        ├─┬──<TAG=x>
+| ReIM|        │ └─┬──<TAG=caller:x>
+| ResC|        │   └────<TAG=callee:x>
+| ReIM|        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────
 [interior mut] Foreign Read: Re* -> Re*
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   8
 | Act |    └─┬──<TAG=root of the allocation>
-| RsM |      └─┬──<TAG=base>
-| RsM |        ├────<TAG=x>
-| RsM |        └────<TAG=y>
+| ReIM|      └─┬──<TAG=base>
+| ReIM|        ├────<TAG=x>
+| ReIM|        └────<TAG=y>
 ──────────────────────────────────────────────────
 [interior mut] Foreign Write: Re* -> Re*
 ──────────────────────────────────────────────────
@@ -24,7 +24,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 0..   8
 | Act |    └─┬──<TAG=root of the allocation>
 | Act |      └─┬──<TAG=base>
-| RsM |        ├────<TAG=x>
+| ReIM|        ├────<TAG=x>
 | Act |        └────<TAG=y>
 ──────────────────────────────────────────────────
 [protected] Foreign Read: Res -> Frz
@@ -32,20 +32,20 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=base>
-| Rs  |        ├─┬──<TAG=x>
-| Rs  |        │ └─┬──<TAG=caller:x>
-| RsC |        │   └────<TAG=callee:x>
-| Rs  |        └────<TAG=y, caller:y, callee:y>
+| Res |      └─┬──<TAG=base>
+| Res |        ├─┬──<TAG=x>
+| Res |        │ └─┬──<TAG=caller:x>
+| ResC|        │   └────<TAG=callee:x>
+| Res |        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────
 [] Foreign Read: Res -> Res
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=base>
-| Rs  |        ├────<TAG=x>
-| Rs  |        └────<TAG=y>
+| Res |      └─┬──<TAG=base>
+| Res |        ├────<TAG=x>
+| Res |        └────<TAG=y>
 ──────────────────────────────────────────────────
 [] Foreign Write: Res -> Dis
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr b/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr
index 6e774e5014d..6098c855bde 100644
--- a/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr
@@ -2,8 +2,8 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=base>
-| Rs  |        └────<TAG=raw, uniq, uniq>
+| Res |      └─┬──<TAG=base>
+| Res |        └────<TAG=raw, uniq, uniq>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
diff --git a/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr b/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr
index 26d9ad2ad38..960c7e216e1 100644
--- a/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr
@@ -2,8 +2,8 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   1
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └─┬──<TAG=base>
-| Rs  |        └─┬──<TAG=raw>
+| Res |      └─┬──<TAG=base>
+| Res |        └─┬──<TAG=raw>
 |-----|          └────<TAG=uniq, uniq>
 ──────────────────────────────────────────────────
 ──────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr b/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr
index f63aa1f6834..254eba061f4 100644
--- a/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr
+++ b/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr
@@ -2,5 +2,5 @@
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..   2
 | Act |    └─┬──<TAG=root of the allocation>
-| Rs  |      └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
+| Res |      └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
 ──────────────────────────────────────────────────