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/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/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.)