Issue of the current model: spurious reads are not possible

This occurs because in some interleavings, inserting
a spurious read turns a Reserved into Frozen.
We show here an exhaustive test (including arbitrary unknown
code in two different threads) that makes this issue
observable.

src/tools/miri/src/borrow_tracker/tree_borrows/exhaustive.rs

@@ -0,0 +1,111 @@
+//! Exhaustive testing utilities.
+//! (These are used in Tree Borrows `#[test]`s for thorough verification
+//! of the behavior of the state machine of permissions,
+//! but the contents of this file are extremely generic)
+#![cfg(test)]
+
+pub trait Exhaustive: Sized {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>>;
+}
+
+macro_rules! precondition {
+    ($cond:expr) => {
+        if !$cond {
+            continue;
+        }
+    };
+}
+pub(crate) use precondition;
+
+// Trivial impls of `Exhaustive` for the standard types with 0, 1 and 2 elements respectively.
+
+impl Exhaustive for ! {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(std::iter::empty())
+    }
+}
+
+impl Exhaustive for () {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(std::iter::once(()))
+    }
+}
+
+impl Exhaustive for bool {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(vec![true, false].into_iter())
+    }
+}
+
+// Some container impls for `Exhaustive`.
+
+impl<T> Exhaustive for Option<T>
+where
+    T: Exhaustive + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(std::iter::once(None).chain(T::exhaustive().map(Some)))
+    }
+}
+
+impl<T1, T2> Exhaustive for (T1, T2)
+where
+    T1: Exhaustive + Clone + 'static,
+    T2: Exhaustive + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(T1::exhaustive().flat_map(|t1| T2::exhaustive().map(move |t2| (t1.clone(), t2))))
+    }
+}
+
+impl<T> Exhaustive for [T; 1]
+where
+    T: Exhaustive + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(T::exhaustive().map(|t| [t]))
+    }
+}
+
+impl<T> Exhaustive for [T; 2]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(T::exhaustive().flat_map(|t1| T::exhaustive().map(move |t2| [t1.clone(), t2])))
+    }
+}
+
+impl<T> Exhaustive for [T; 3]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(
+            <[T; 2]>::exhaustive()
+                .flat_map(|[t1, t2]| T::exhaustive().map(move |t3| [t1.clone(), t2.clone(), t3])),
+        )
+    }
+}
+
+impl<T> Exhaustive for [T; 4]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(<[T; 2]>::exhaustive().flat_map(|[t1, t2]| {
+            <[T; 2]>::exhaustive().map(move |[t3, t4]| [t1.clone(), t2.clone(), t3, t4])
+        }))
+    }
+}
+
+impl<T> Exhaustive for [T; 5]
+where
+    T: Exhaustive + Clone + 'static,
+{
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        Box::new(<[T; 2]>::exhaustive().flat_map(|[t1, t2]| {
+            <[T; 3]>::exhaustive().map(move |[t3, t4, t5]| [t1.clone(), t2.clone(), t3, t4, t5])
+        }))
+    }
+}

src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

@@ -15,6 +15,10 @@ pub mod diagnostics;
 mod perms;
 mod tree;
 mod unimap;
+
+#[cfg(test)]
+mod exhaustive;
+
 use perms::Permission;
 pub use tree::Tree;
 
@@ -271,6 +275,10 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
             diagnostics::AccessCause::Reborrow,
         )?;
         // Record the parent-child pair in the tree.
+        // FIXME: We should eventually ensure that the following `assert` holds, because
+        // some "exhaustive" tests consider only the initial configurations that satisfy it.
+        // The culprit is `Permission::new_active` in `tb_protect_place`.
+        //assert!(new_perm.initial_state.is_initial());
         tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
         drop(tree_borrows);
 
@@ -283,7 +291,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                 // interleaving, but wether UB happens can depend on whether a write occurs in the
                 // future...
                 let is_write = new_perm.initial_state.is_active()
-                    || (new_perm.initial_state.is_reserved() && new_perm.protector.is_some());
+                    || (new_perm.initial_state.is_reserved(None) && new_perm.protector.is_some());
                 if is_write {
                     // Need to get mutable access to alloc_extra.
                     // (Cannot always do this as we can do read-only reborrowing on read-only allocations.)

src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs

@@ -6,7 +6,7 @@ use crate::borrow_tracker::tree_borrows::tree::AccessRelatedness;
 use crate::borrow_tracker::AccessKind;
 
 /// The activation states of a pointer.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[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;
@@ -48,6 +48,13 @@ 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 { ty_is_freeze: _ } | Frozen)
+    }
+}
+
 /// This module controls how each permission individually reacts to an access.
 /// Although these functions take `protected` as an argument, this is NOT because
 /// we check protector violations here, but because some permissions behave differently
@@ -66,7 +73,6 @@ mod transition {
 
     /// A non-child node was read-accessed: noop on non-protected Reserved, advance to Frozen otherwise.
     fn foreign_read(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
-        use Option::*;
         Some(match state {
             // Non-writeable states just ignore foreign reads.
             non_writeable @ (Frozen | Disabled) => non_writeable,
@@ -134,7 +140,7 @@ mod transition {
 
 /// Public interface to the state machine that controls read-write permissions.
 /// This is the "private `enum`" pattern.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd)]
 pub struct Permission {
     inner: PermissionPriv,
 }
@@ -147,6 +153,11 @@ pub struct PermTransition {
 }
 
 impl Permission {
+    /// Check if `self` can be the initial state of a pointer.
+    pub fn is_initial(&self) -> bool {
+        self.inner.is_initial()
+    }
+
     /// Default initial permission of the root of a new tree.
     pub fn new_active() -> Self {
         Self { inner: Active }
@@ -166,14 +177,24 @@ impl Permission {
         matches!(self.inner, Active)
     }
 
-    pub fn is_reserved(self) -> bool {
-        matches!(self.inner, Reserved { .. })
+    // Leave `interior_mut` as `None` if interior mutability
+    // is irrelevant.
+    pub fn is_reserved(self, interior_mut: Option<bool>) -> bool {
+        match (interior_mut, self.inner) {
+            (None, Reserved { .. }) => true,
+            (Some(b1), Reserved { ty_is_freeze: b2 }) => b1 == b2,
+            _ => false,
+        }
     }
 
     pub fn is_frozen(self) -> bool {
         matches!(self.inner, Frozen)
     }
 
+    pub fn is_disabled(self) -> bool {
+        matches!(self.inner, Disabled)
+    }
+
     /// Apply the transition to the inner PermissionPriv.
     pub fn perform_access(
         kind: AccessKind,
@@ -229,7 +250,8 @@ pub mod diagnostics {
                 f,
                 "{}",
                 match self {
-                    Reserved { .. } => "Reserved",
+                    Reserved { ty_is_freeze: true } => "Reserved",
+                    Reserved { ty_is_freeze: false } => "Reserved (interior mutable)",
                     Active => "Active",
                     Frozen => "Frozen",
                     Disabled => "Disabled",
@@ -397,43 +419,35 @@ pub mod diagnostics {
 #[cfg(test)]
 mod propagation_optimization_checks {
     pub use super::*;
+    use crate::borrow_tracker::tree_borrows::exhaustive::{precondition, Exhaustive};
 
-    mod util {
-        pub use super::*;
-        impl PermissionPriv {
-            /// Enumerate all states
-            pub fn all() -> impl Iterator<Item = Self> {
-                vec![
-                    Active,
-                    Reserved { ty_is_freeze: true },
-                    Reserved { ty_is_freeze: false },
-                    Frozen,
-                    Disabled,
-                ]
-                .into_iter()
-            }
+    impl Exhaustive for PermissionPriv {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            Box::new(
+                vec![Active, Frozen, Disabled]
+                    .into_iter()
+                    .chain(bool::exhaustive().map(|ty_is_freeze| Reserved { ty_is_freeze })),
+            )
         }
+    }
 
-        impl Permission {
-            pub fn all() -> impl Iterator<Item = Self> {
-                PermissionPriv::all().map(|inner| Self { inner })
-            }
+    impl Exhaustive for Permission {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            Box::new(PermissionPriv::exhaustive().map(|inner| Self { inner }))
         }
+    }
 
-        impl AccessKind {
-            /// Enumerate all AccessKind.
-            pub fn all() -> impl Iterator<Item = Self> {
-                use AccessKind::*;
-                [Read, Write].into_iter()
-            }
+    impl Exhaustive for AccessKind {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            use AccessKind::*;
+            Box::new(vec![Read, Write].into_iter())
         }
+    }
 
-        impl AccessRelatedness {
-            /// Enumerate all relative positions
-            pub fn all() -> impl Iterator<Item = Self> {
-                use AccessRelatedness::*;
-                [This, StrictChildAccess, AncestorAccess, DistantAccess].into_iter()
-            }
+    impl Exhaustive for AccessRelatedness {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            use AccessRelatedness::*;
+            Box::new(vec![This, StrictChildAccess, AncestorAccess, DistantAccess].into_iter())
         }
     }
 
@@ -442,16 +456,22 @@ mod propagation_optimization_checks {
     // Even if the protector has disappeared.
     fn all_transitions_idempotent() {
         use transition::*;
-        for old in PermissionPriv::all() {
-            for (old_protected, new_protected) in [(true, true), (true, false), (false, false)] {
-                for access in AccessKind::all() {
-                    for rel_pos in AccessRelatedness::all() {
-                        if let Some(new) = perform_access(access, rel_pos, old, old_protected) {
-                            assert_eq!(
-                                new,
-                                perform_access(access, rel_pos, new, new_protected).unwrap()
-                            );
-                        }
+        for old in PermissionPriv::exhaustive() {
+            for (old_protected, new_protected) in <(bool, bool)>::exhaustive() {
+                // Protector can't appear out of nowhere: either the permission was
+                // created with a protector (`old_protected = true`) and it then may
+                // or may not lose it (`new_protected = false`, resp. `new_protected = true`),
+                // or it didn't have one upon creation and never will
+                // (`old_protected = new_protected = false`).
+                // 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);
+                for (access, rel_pos) in <(AccessKind, AccessRelatedness)>::exhaustive() {
+                    if let Some(new) = perform_access(access, rel_pos, old, old_protected) {
+                        assert_eq!(
+                            new,
+                            perform_access(access, rel_pos, new, new_protected).unwrap()
+                        );
                     }
                 }
             }
@@ -459,13 +479,16 @@ mod propagation_optimization_checks {
     }
 
     #[test]
+    #[rustfmt::skip]
     fn foreign_read_is_noop_after_foreign_write() {
         use transition::*;
         let old_access = AccessKind::Write;
         let new_access = AccessKind::Read;
-        for old in PermissionPriv::all() {
-            for (old_protected, new_protected) in [(true, true), (true, false), (false, false)] {
-                for rel_pos in AccessRelatedness::all().filter(|rel| rel.is_foreign()) {
+        for old in PermissionPriv::exhaustive() {
+            for [old_protected, new_protected] in <[bool; 2]>::exhaustive() {
+                precondition!(old_protected || !new_protected);
+                for rel_pos in AccessRelatedness::exhaustive() {
+                    precondition!(rel_pos.is_foreign());
                     if let Some(new) = perform_access(old_access, rel_pos, old, old_protected) {
                         assert_eq!(
                             new,
@@ -480,18 +503,44 @@ mod propagation_optimization_checks {
     #[test]
     // Check that all transitions are consistent with the order on PermissionPriv,
     // i.e. Reserved -> Active -> Frozen -> Disabled
-    fn access_transitions_progress_increasing() {
-        use transition::*;
-        for old in PermissionPriv::all() {
-            for protected in [true, false] {
-                for access in AccessKind::all() {
-                    for rel_pos in AccessRelatedness::all() {
-                        if let Some(new) = perform_access(access, rel_pos, old, protected) {
-                            assert!(old <= new);
+    fn permissionpriv_partialord_is_reachability() {
+        let reach = {
+            let mut reach = rustc_data_structures::fx::FxHashSet::default();
+            // One-step transitions + reflexivity
+            for start in PermissionPriv::exhaustive() {
+                reach.insert((start, start));
+                for (access, rel) in <(AccessKind, AccessRelatedness)>::exhaustive() {
+                    for prot in bool::exhaustive() {
+                        if let Some(end) = transition::perform_access(access, rel, start, prot) {
+                            reach.insert((start, end));
                         }
                     }
                 }
             }
+            // Transitive closure
+            let mut finished = false;
+            while !finished {
+                finished = true;
+                for [start, mid, end] in <[PermissionPriv; 3]>::exhaustive() {
+                    if reach.contains(&(start, mid))
+                        && reach.contains(&(mid, end))
+                        && !reach.contains(&(start, end))
+                    {
+                        finished = false;
+                        reach.insert((start, end));
+                    }
+                }
+            }
+            reach
+        };
+        // Check that it matches `<`
+        for [p1, p2] in <[PermissionPriv; 2]>::exhaustive() {
+            let le12 = p1 <= p2;
+            let reach12 = reach.contains(&(p1, p2));
+            assert!(
+                le12 == reach12,
+                "`{p1} reach {p2}` ({reach12}) does not match `{p1} <= {p2}` ({le12})"
+            );
         }
     }
 }

src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs

@@ -10,6 +10,8 @@
 //!   and the relative position of the access;
 //! - idempotency properties asserted in `perms.rs` (for optimizations)
 
+use std::fmt;
+
 use smallvec::SmallVec;
 
 use rustc_const_eval::interpret::InterpResult;
@@ -26,8 +28,10 @@ use crate::borrow_tracker::tree_borrows::{
 use crate::borrow_tracker::{AccessKind, GlobalState, ProtectorKind};
 use crate::*;
 
+mod tests;
+
 /// Data for a single *location*.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub(super) struct LocationState {
     /// 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
@@ -65,10 +69,25 @@ impl LocationState {
         self
     }
 
+    /// Check if the location has been initialized, i.e. if it has
+    /// ever been accessed through a child pointer.
     pub fn is_initialized(&self) -> bool {
         self.initialized
     }
 
+    /// Check if the state can exist as the initial permission of a pointer.
+    ///
+    /// Do not confuse with `is_initialized`, the two are almost orthogonal
+    /// as apart from `Active` which is not initial and must be initialized,
+    /// any other permission can have an arbitrary combination of being
+    /// initial/initialized.
+    /// FIXME: when the corresponding `assert` in `tree_borrows/mod.rs` finally
+    /// passes and can be uncommented, remove this `#[allow(dead_code)]`.
+    #[cfg_attr(not(test), allow(dead_code))]
+    pub fn is_initial(&self) -> bool {
+        self.permission.is_initial()
+    }
+
     pub fn permission(&self) -> Permission {
         self.permission
     }
@@ -172,6 +191,16 @@ impl LocationState {
     }
 }
 
+impl fmt::Display for LocationState {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}", self.permission)?;
+        if !self.initialized {
+            write!(f, "?")?;
+        }
+        Ok(())
+    }
+}
+
 /// Tree structure with both parents and children since we want to be
 /// able to traverse the tree efficiently in both directions.
 #[derive(Clone, Debug)]
@@ -665,87 +694,3 @@ impl AccessRelatedness {
         }
     }
 }
-
-#[cfg(test)]
-mod commutation_tests {
-    use super::*;
-    impl LocationState {
-        pub fn all() -> impl Iterator<Item = Self> {
-            // We keep `latest_foreign_access` at `None` as that's just a cache.
-            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() {
-                        // 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
-                        );
-                    }
-                }
-            }
-        }
-    }
-
-    #[test]
-    #[rustfmt::skip]
-    // Ensure that of 2 accesses happen, one foreign and one a child, and we are protected, that we
-    // get UB unless they are both reads.
-    fn protected_enforces_noalias() {
-        for rel1 in AccessRelatedness::all() {
-            for rel2 in AccessRelatedness::all() {
-                if rel1.is_foreign() == rel2.is_foreign() {
-                    // We want to check pairs of accesses where one is foreign and one is not.
-                    continue;
-                }
-                for kind1 in AccessKind::all() {
-                    for kind2 in AccessKind::all() {
-                        for mut state in LocationState::all() {
-                            let protected = true;
-                            let Ok(_) = state.perform_access(kind1, rel1, protected) else { continue };
-                            let Ok(_) = state.perform_access(kind2, rel2, protected) else { continue };
-                            // If these were both allowed, it must have been two reads.
-                            assert!(
-                                kind1 == AccessKind::Read && kind2 == AccessKind::Read,
-                                "failed to enforce noalias between two accesses that are not both reads"
-                            );
-                        }
-                    }
-                }
-            }
-        }
-    }
-}

src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs

@@ -0,0 +1,658 @@
+//! Tests for the tree
+#![cfg(test)]
+
+use super::*;
+use crate::borrow_tracker::tree_borrows::exhaustive::{precondition, Exhaustive};
+use std::fmt;
+
+impl Exhaustive for LocationState {
+    fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+        // We keep `latest_foreign_access` at `None` as that's just a cache.
+        Box::new(<(Permission, bool)>::exhaustive().map(|(permission, 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, rel2] in <[AccessRelatedness; 2]>::exhaustive() {
+        // 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 bool::exhaustive() {
+            for loc in LocationState::exhaustive() {
+                // 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;
+                precondition!(loc12.perform_access(kind, rel1, protected).is_ok());
+                precondition!(loc12.perform_access(kind, rel2, protected).is_ok());
+
+                // 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
+                );
+            }
+        }
+    }
+}
+
+#[test]
+#[rustfmt::skip]
+// Ensure that of 2 accesses happen, one foreign and one a child, and we are protected, that we
+// get UB unless they are both reads.
+fn protected_enforces_noalias() {
+    for [rel1, rel2] in <[AccessRelatedness; 2]>::exhaustive() {
+        // 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;
+                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.
+                assert!(
+                    kind1 == AccessKind::Read && kind2 == AccessKind::Read,
+                    "failed to enforce noalias between two accesses that are not both reads"
+                );
+            }
+        }
+    }
+}
+
+/// We are going to exhaustively test the possibily of inserting
+/// a spurious read in some code.
+///
+/// We choose some pointer `x` through which we want a spurious read to be inserted.
+/// `x` must thus be reborrowed, not have any children, and initially start protected.
+///
+/// To check if inserting a spurious read is possible, we observe the behavior
+/// of some pointer `y` different from `x` (possibly from a different thread, thus
+/// the protectors on `x` and `y` are not necessarily well-nested).
+/// It must be the case that no matter the context, the insertion of a spurious read
+/// through `x` does not introduce UB in code that did not already have UB.
+///
+/// Testing this will need some setup to simulate the evolution of the permissions
+/// of `x` and `y` under arbitrary code. This arbitrary code of course includes
+/// read and write accesses through `x` and `y`, but it must also consider
+/// the less obvious:
+/// - accesses through pointers that are *neither* `x` nor `y`,
+/// - retags of `y` that change its relative position to `x`.
+///
+///
+/// The general code pattern thus looks like
+///     [thread 1]             || [thread 2]
+///                            || y exists
+///     retag x (protect)      ||
+///                      arbitrary code
+///                           read/write x/y/other
+///                        or retag y
+///                        or unprotect y
+///     <spurious read x>      ||
+///                      arbitrary code
+///                           read/write x/y/other
+///                        or retag y
+///                        or unprotect y
+///                        or unprotect x
+///
+/// `x` must still be protected at the moment the spurious read is inserted
+/// because spurious reads are impossible in general on unprotected tags.
+mod spurious_read {
+    use super::*;
+
+    /// Accessed pointer.
+    #[derive(Debug, Clone, Copy, PartialEq, Eq)]
+    enum PtrSelector {
+        X,
+        Y,
+        Other,
+    }
+
+    /// Relative position of `x` and `y`.
+    /// `y` cannot be a child of `x` because `x` gets retagged as the first
+    /// thing in the pattern, so it cannot have children.
+    #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+    enum RelPosXY {
+        MutuallyForeign,
+        /// X is a child of Y.
+        XChildY,
+    }
+
+    impl Exhaustive for PtrSelector {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            use PtrSelector::*;
+            Box::new(vec![X, Y, Other].into_iter())
+        }
+    }
+
+    impl fmt::Display for PtrSelector {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            match self {
+                PtrSelector::X => write!(f, "x"),
+                PtrSelector::Y => write!(f, "y"),
+                PtrSelector::Other => write!(f, "z"),
+            }
+        }
+    }
+
+    impl Exhaustive for RelPosXY {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            use RelPosXY::*;
+            Box::new(vec![MutuallyForeign, XChildY].into_iter())
+        }
+    }
+
+    impl fmt::Display for RelPosXY {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            match self {
+                RelPosXY::MutuallyForeign => write!(f, "x and y are mutually foreign"),
+                RelPosXY::XChildY => write!(f, "x is a child of y"),
+            }
+        }
+    }
+
+    impl PtrSelector {
+        /// Knowing the relative position of `x` to `y`, determine the relative
+        /// position of the accessed pointer defined by `self` relative to each `x`
+        /// and `y`.
+        ///
+        /// The output is not necessarily well-defined in general, but it
+        /// is unique when considered up to equivalence by `AccessRelatedness::is_foreign`
+        /// (e.g. having `RelPosXY::XChildY` and `PtrSelector::Other`, strictly
+        /// speaking it is impossible to determine if `Other` is a `DistantAccess`
+        /// or an `AncestorAccess` relative to `y`, but it doesn't really matter
+        /// because `DistantAccess.is_foreign() == AncestorAccess.is_foreign()`).
+        fn rel_pair(self, xy_rel: RelPosXY) -> (AccessRelatedness, AccessRelatedness) {
+            use AccessRelatedness::*;
+            match xy_rel {
+                RelPosXY::MutuallyForeign =>
+                    match self {
+                        PtrSelector::X => (This, DistantAccess),
+                        PtrSelector::Y => (DistantAccess, This),
+                        PtrSelector::Other => (DistantAccess, DistantAccess),
+                    },
+                RelPosXY::XChildY =>
+                    match self {
+                        PtrSelector::X => (This, StrictChildAccess),
+                        PtrSelector::Y => (AncestorAccess, This),
+                        PtrSelector::Other => (DistantAccess, DistantAccess),
+                    },
+            }
+        }
+    }
+
+    /// Arbitrary access parametrized by the relative position of `x` and `y`
+    /// to each other.
+    #[derive(Debug, Clone, Copy)]
+    struct TestAccess {
+        ptr: PtrSelector,
+        kind: AccessKind,
+    }
+
+    impl Exhaustive for TestAccess {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            Box::new(
+                <(PtrSelector, AccessKind)>::exhaustive()
+                    .map(|(ptr, kind)| TestAccess { ptr, kind }),
+            )
+        }
+    }
+
+    impl fmt::Display for TestAccess {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            let kind_text = match self.kind {
+                AccessKind::Read => "read",
+                AccessKind::Write => "write",
+            };
+            write!(f, "{kind_text} {}", self.ptr)
+        }
+    }
+
+    type AllowRet = ();
+    type NoRet = !;
+    #[derive(Clone)]
+    /// Events relevant to the evolution of 2 pointers are
+    /// - any access to the same location
+    /// - end of one of them being protected
+    /// - a retag that would change their relative position
+    /// The type `TestEvent` models these kinds of events.
+    ///
+    /// In order to prevent `x` or `y` from losing their protector,
+    /// choose a type `RetX` or `RetY` that is not inhabited.
+    /// e.g.
+    /// - `TestEvent<AllowRet, AllowRet>` is any event including end of protector on either `x` or `y`
+    /// - `TestEvent<NoRet, NoRet>` is any access
+    /// - `TestEvent<NoRet, AllowRet>` allows for `y` to lose its protector but not `x`
+    enum TestEvent<RetX, RetY> {
+        Access(TestAccess),
+        RetX(RetX),
+        RetY(RetY),
+        /// The inner `LocStateProt` must be an initial state (as per the `is_initial` function)
+        RetagY(LocStateProt),
+    }
+
+    impl<RetX, RetY> Exhaustive for TestEvent<RetX, RetY>
+    where
+        RetX: Exhaustive + 'static,
+        RetY: Exhaustive + 'static,
+    {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            Box::new(
+                <TestAccess>::exhaustive()
+                    .map(|acc| Self::Access(acc))
+                    .chain(RetX::exhaustive().map(|retx| Self::RetX(retx)))
+                    .chain(RetY::exhaustive().map(|rety| Self::RetY(rety)))
+                    .chain(
+                        LocStateProt::exhaustive()
+                            .filter_map(|s| s.is_initial().then_some(Self::RetagY(s))),
+                    ),
+            )
+        }
+    }
+
+    impl<RetX, RetY> fmt::Display for TestEvent<RetX, RetY> {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            match self {
+                TestEvent::Access(acc) => write!(f, "{acc}"),
+                // The fields of the `Ret` variants just serve to make them
+                // impossible to instanciate via the `RetX = NoRet` type; we can
+                // always ignore their value.
+                TestEvent::RetX(_) => write!(f, "ret x"),
+                TestEvent::RetY(_) => write!(f, "ret y"),
+                TestEvent::RetagY(newp) => write!(f, "retag y ({newp})"),
+            }
+        }
+    }
+
+    #[derive(Clone, PartialEq, Eq, Hash)]
+    /// The state of a pointer on a location, including the protector.
+    /// It is represented here with the protector bound to the `LocationState` rather
+    /// than the `Map<Location, LocationState>` as is normally the case,
+    /// but since all our exhaustive tests look at a  single location
+    /// there's no risk of `prot` for different locations of the same tag getting
+    /// out of sync.
+    struct LocStateProt {
+        state: LocationState,
+        prot: bool,
+    }
+
+    impl LocStateProt {
+        fn is_initial(&self) -> bool {
+            self.state.is_initial()
+        }
+
+        fn perform_access(&self, kind: AccessKind, rel: AccessRelatedness) -> Result<Self, ()> {
+            let mut state = self.state;
+            state.perform_access(kind, rel, self.prot).map_err(|_| ())?;
+            Ok(Self { state, prot: self.prot })
+        }
+
+        fn end_protector(&self) -> Self {
+            Self { prot: false, state: self.state }
+        }
+    }
+
+    impl Exhaustive for LocStateProt {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            Box::new(
+                <(LocationState, bool)>::exhaustive().map(|(state, prot)| Self { state, prot }),
+            )
+        }
+    }
+
+    impl fmt::Display for LocStateProt {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "{}", self.state)?;
+            if self.prot {
+                write!(f, ", protect")?;
+            }
+            Ok(())
+        }
+    }
+
+    #[derive(Clone, PartialEq, Eq, Hash)]
+    /// The states of two pointers to the same location,
+    /// and their relationship to each other in the tree.
+    ///
+    /// Note that the two states interact: using one pointer can have
+    /// an impact on the other.
+    /// This makes `LocStateProtPair` more meaningful than a simple
+    /// `(LocStateProt, LocStateProt)` where the two states are not guaranteed
+    /// to be updated at the same time.
+    /// Some `LocStateProtPair` may be unreachable through normal means
+    /// such as `x: Active, y: Active` in the case of mutually foreign pointers.
+    struct LocStateProtPair {
+        xy_rel: RelPosXY,
+        x: LocStateProt,
+        y: LocStateProt,
+    }
+
+    impl LocStateProtPair {
+        fn perform_test_access(self, acc: &TestAccess) -> Result<Self, ()> {
+            let (xrel, yrel) = acc.ptr.rel_pair(self.xy_rel);
+            let x = self.x.perform_access(acc.kind, xrel)?;
+            let y = self.y.perform_access(acc.kind, yrel)?;
+            Ok(Self { x, y, ..self })
+        }
+
+        /// Perform a read on the given pointer if its state is `initialized`.
+        /// Must be called just after reborrowing a pointer.
+        fn read_if_initialized(self, ptr: PtrSelector) -> Result<Self, ()> {
+            let initialized = match ptr {
+                PtrSelector::X => self.x.state.initialized,
+                PtrSelector::Y => self.y.state.initialized,
+                PtrSelector::Other =>
+                    panic!(
+                        "the `initialized` status of `PtrSelector::Other` is unknown, do not pass it to `read_if_initialized`"
+                    ),
+            };
+            if initialized {
+                self.perform_test_access(&TestAccess { ptr, kind: AccessKind::Read })
+            } else {
+                Ok(self)
+            }
+        }
+
+        fn end_protector_x(self) -> Result<Self, ()> {
+            let x = self.x.end_protector();
+            Ok(Self { x, ..self })
+        }
+
+        fn end_protector_y(self) -> Result<Self, ()> {
+            let y = self.y.end_protector();
+            Ok(Self { y, ..self })
+        }
+
+        fn retag_y(self, new_y: LocStateProt) -> Result<Self, ()> {
+            assert!(new_y.is_initial());
+            // `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)
+        }
+
+        fn perform_test_event<RetX, RetY>(self, evt: &TestEvent<RetX, RetY>) -> Result<Self, ()> {
+            match evt {
+                TestEvent::Access(acc) => self.perform_test_access(acc),
+                // The fields of the `Ret` variants just serve to make them
+                // impossible to instanciate via the `RetX = NoRet` type; we can
+                // always ignore their value.
+                TestEvent::RetX(_) => self.end_protector_x(),
+                TestEvent::RetY(_) => self.end_protector_y(),
+                TestEvent::RetagY(newp) => self.retag_y(newp.clone()),
+            }
+        }
+    }
+
+    impl Exhaustive for LocStateProtPair {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            Box::new(<[LocStateProt; 2]>::exhaustive().flat_map(|[x, y]| {
+                RelPosXY::exhaustive()
+                    .map(move |xy_rel| Self { x: x.clone(), y: y.clone(), xy_rel })
+            }))
+        }
+    }
+
+    impl fmt::Display for LocStateProtPair {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "x:{}, y:{}", self.x, self.y)
+        }
+    }
+
+    /// Arbitrary sequence of events, as experienced by two mutually foreign pointers
+    /// to the same location.
+    #[derive(Clone)]
+    struct OpaqueCode<RetX, RetY> {
+        events: Vec<TestEvent<RetX, RetY>>,
+    }
+
+    impl<RetX, RetY> fmt::Display for OpaqueCode<RetX, RetY> {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            for evt in &self.events {
+                write!(f, "{evt}; ")?;
+            }
+            Ok(())
+        }
+    }
+
+    impl LocStateProtPair {
+        /// List all sequences of operations that start at `self` and do not cause UB
+        /// There are no duplicates: all sequences returned lead to distinct final states
+        /// (though the sequence is not guaranteed to be the shortest possible sequence of events).
+        /// Yields the states it reaches, and the sequence of operations that got us there.
+        fn all_states_reachable_via_opaque_code<RetX, RetY>(
+            self,
+        ) -> impl Iterator<Item = (Self, OpaqueCode<RetX, RetY>)>
+        where
+            RetX: Exhaustive + Clone + 'static,
+            RetY: Exhaustive + Clone + 'static,
+        {
+            // We compute the reachable set of `Self` from `self` by non-UB `OpaqueCode`.
+            // Configurations are `(reach: Self, code: OpaqueCode)` tuples
+            // for which `code` applied to `self` returns `Ok(reach)`.
+
+            // Stack of all configurations left to handle.
+            let mut handle: Vec<(Self, OpaqueCode<_, _>)> =
+                vec![(self, OpaqueCode { events: Vec::new() })];
+            // Code that can be applied to `self`, and final state.
+            let mut paths: Vec<(Self, OpaqueCode<_, _>)> = Default::default();
+            // Already explored states reachable from `self`
+            let mut seen: FxHashSet<Self> = Default::default();
+            // This is essentially just computing the transitive closure by `perform_test_event`,
+            // most of the work lies in remembering the path up to the current state.
+            while let Some((state, path)) = handle.pop() {
+                for evt in <TestEvent<RetX, RetY>>::exhaustive() {
+                    if let Ok(next) = state.clone().perform_test_event(&evt) {
+                        if seen.insert(next.clone()) {
+                            let mut evts = path.clone();
+                            evts.events.push(evt);
+                            paths.push((next.clone(), evts.clone()));
+                            handle.push((next, evts));
+                        }
+                    }
+                }
+            }
+            paths.into_iter()
+        }
+    }
+
+    impl LocStateProtPair {
+        #[rustfmt::skip]
+        /// Two states (by convention `self` is the source and `other` is the target)
+        /// are "distinguishable" if there exists a sequence of instructions
+        /// that causes UB in the target but not in the source.
+        /// This implementation simply explores the reachable space
+        /// by all sequences of `TestEvent`.
+        /// This function can be instanciated with `RetX` and `RetY`
+        /// among `NoRet` or `AllowRet` to resp. forbid/allow `x`/`y` to lose their
+        /// protector.
+        fn distinguishable<RetX, RetY>(&self, other: &Self) -> bool
+        where
+            RetX: Exhaustive + 'static,
+            RetY: Exhaustive + 'static,
+        {
+            if self == other { return false; }
+            let mut states = vec![(self.clone(), other.clone())];
+            let mut seen = FxHashSet::default();
+            while let Some(state) = states.pop() {
+                if !seen.insert(state.clone()) { continue; };
+                let (source, target) = state;
+                for evt in <TestEvent<RetX, RetY>>::exhaustive() {
+                    // Generate successor states through events (accesses and protector ends)
+                    let Ok(new_source) = source.clone().perform_test_event(&evt) else { continue; };
+                    let Ok(new_target) = target.clone().perform_test_event(&evt) else { return true; };
+                    if new_source == new_target { continue; }
+                    states.push((new_source, new_target));
+                }
+            }
+            false
+        }
+    }
+
+    #[test]
+    #[should_panic]
+    // This is why `Reserved -> Frozen` on foreign read for protected references
+    // prevents the insertion of spurious reads: the transition can cause UB in the target
+    // later down the line.
+    fn reserved_frozen_protected_distinguishable() {
+        let source = LocStateProtPair {
+            xy_rel: RelPosXY::MutuallyForeign,
+            x: LocStateProt {
+                state: LocationState::new(Permission::new_frozen()).with_access(),
+                prot: true,
+            },
+            y: LocStateProt {
+                state: LocationState::new(Permission::new_reserved(false)),
+                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(None));
+        assert!(target.y.state.permission.is_frozen());
+        assert!(!source.distinguishable::<(), ()>(&target))
+    }
+
+    #[derive(Clone, Debug)]
+    struct Pattern {
+        /// The relative position of `x` and `y` at the beginning of the arbitrary
+        /// code (i.e., just after `x` got created).
+        /// Might change during the execution if said arbitrary code contains any `retag y`.
+        xy_rel: RelPosXY,
+        /// Permission that `x` will be created as
+        /// (always protected until a possible `ret x` in the second phase).
+        /// This one should be initial (as per `is_initial`).
+        x_retag_perm: LocationState,
+        /// Permission that `y` has at the beginning of the pattern.
+        /// Can be any state, not necessarily initial
+        /// (since `y` exists already before the pattern starts).
+        /// This state might be reset during the execution if the opaque code
+        /// contains any `retag y`, but only to an initial state this time.
+        y_current_perm: LocationState,
+        /// Whether `y` starts with a protector.
+        /// Might change if the opaque code contains any `ret y`.
+        y_protected: bool,
+    }
+
+    impl Exhaustive for Pattern {
+        fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
+            let mut v = Vec::new();
+            for xy_rel in RelPosXY::exhaustive() {
+                for (x_retag_perm, y_current_perm) in <(LocationState, LocationState)>::exhaustive()
+                {
+                    // We can only do spurious reads for initialized locations anyway.
+                    precondition!(x_retag_perm.initialized);
+                    // And `x` just got retagged, so it must be initial.
+                    precondition!(x_retag_perm.permission.is_initial());
+                    for y_protected in bool::exhaustive() {
+                        v.push(Pattern { xy_rel, x_retag_perm, y_current_perm, y_protected });
+                    }
+                }
+            }
+            Box::new(v.into_iter())
+        }
+    }
+
+    impl fmt::Display for Pattern {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            let (x, y) = self.retag_permissions();
+            write!(f, "{}; ", self.xy_rel)?;
+            write!(f, "y: ({}); ", y,)?;
+            write!(f, "retag x ({}); ", x)?;
+
+            write!(f, "<arbitrary code>; <spurious read x>;")?;
+            Ok(())
+        }
+    }
+
+    impl Pattern {
+        /// Return the permission that `y` starts as, and the permission that we
+        /// will retag `x` with.
+        /// This does not yet include a possible read-on-reborrow through `x`.
+        fn retag_permissions(&self) -> (LocStateProt, LocStateProt) {
+            let x = LocStateProt { state: self.x_retag_perm, prot: true };
+            let y = LocStateProt { state: self.y_current_perm, prot: self.y_protected };
+            (x, y)
+        }
+
+        /// State that the pattern deterministically produces immediately after
+        /// the retag of `x`.
+        fn initial_state(&self) -> Result<LocStateProtPair, ()> {
+            let (x, y) = self.retag_permissions();
+            let state = LocStateProtPair { xy_rel: self.xy_rel, x, y };
+            state.read_if_initialized(PtrSelector::X)
+        }
+    }
+
+    #[test]
+    #[should_panic]
+    /// For each of the patterns described above, execute it once
+    /// as-is, and once with a spurious read inserted. Report any UB
+    /// in the target but not in the source.
+    fn test_all_patterns() {
+        let mut ok = 0;
+        let mut err = 0;
+        for pat in Pattern::exhaustive() {
+            let Ok(initial_source) = pat.initial_state() else {
+                // Failed to retag `x` in the source (e.g. `y` was protected Active)
+                continue;
+            };
+            // `x` must stay protected, but the function protecting `y` might return here
+            for (final_source, opaque) in
+                initial_source.all_states_reachable_via_opaque_code::</*X*/ NoRet, /*Y*/ AllowRet>()
+            {
+                // Both executions are identical up to here.
+                // Now we do nothing in the source and in the target we do a spurious read.
+                // Then we check if the resulting states are distinguishable.
+                let distinguishable = {
+                    assert!(final_source.x.prot);
+                    let spurious_read = TestAccess { ptr: PtrSelector::X, kind: AccessKind::Read };
+                    if let Ok(final_target) =
+                        final_source.clone().perform_test_access(&spurious_read)
+                    {
+                        // Only after the spurious read has been executed can `x` lose its
+                        // protector.
+                        final_source
+                            .distinguishable::</*X*/ AllowRet, /*Y*/ AllowRet>(&final_target)
+                            .then_some(format!("{}", final_target))
+                    } else {
+                        Some(format!("UB"))
+                    }
+                };
+                if let Some(final_target) = distinguishable {
+                    eprintln!(
+                        "For pattern '{}', inserting a spurious read through x makes the final state '{}' instead of '{}' which is observable",
+                        pat, final_target, final_source
+                    );
+                    eprintln!("  (arbitrary code instanciated with '{}')", opaque);
+                    err += 1;
+                    // We found an instanciation of the opaque code that makes this Pattern
+                    // fail, we don't really need to check the rest.
+                    break;
+                }
+                ok += 1;
+            }
+        }
+        if err > 0 {
+            panic!(
+                "Test failed after {}/{} patterns had UB in the target but not the source",
+                err,
+                ok + err
+            )
+        }
+    }
+}

src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr

@@ -16,14 +16,14 @@ 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) (currently Reserved) to become Disabled
+   = help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved (interior mutable)) 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
    |
 LL |         let y = (&mut *n).get();
    |                 ^^^^^^^^^
-help: the protected tag <TAG> was created here, in the initial state Reserved
+help: the protected tag <TAG> was created here, in the initial state Reserved (interior mutable)
   --> $DIR/cell-protected-write.rs:LL:CC
    |
 LL |         unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {