Apply suggestions

- split test into two revisions
- clarify comments

Author: Vanille-N

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

@@ -145,7 +145,8 @@ impl<'tcx> NewPermission {
         // As demonstrated by `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
         // 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.
+        // in the case of a protected reference: protected references are always considered
+        // "freeze".
         let initial_state = match mutability {
             Mutability::Mut if ty_is_unpin =>
                 Permission::new_reserved(ty_is_freeze || is_protected),

src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs

@@ -2,14 +2,20 @@
 // and protectors, that makes spurious writes fail in the previous model of Tree Borrows.
 // As for all similar tests, we disable preemption so that the error message is deterministic.
 //@compile-flags: -Zmiri-tree-borrows -Zmiri-preemption-rate=0
+//
+// One revision without spurious read (default source code) and one with spurious read.
+// Both are expected to be UB. Both revisions are expected to have the *same* error
+// because we are aligning the behavior of `without` to that of `with` so that the
+// spurious write is effectively a noop in the long term.
+//@revisions: without with
 
 use std::cell::Cell;
 use std::sync::{Arc, Barrier};
 use std::thread;
 
 // Here is the problematic interleaving:
 // - thread 1: retag and activate `x` (protected)
-// - thread 2: create but do not retag (lazy) `y` as Reserved with interior mutability
+// - thread 2: retag but do not initialize (lazy) `y` as Reserved with interior mutability
 // - thread 1: spurious write through `x` would go here
 // - thread 2: function exit (noop due to lazyness)
 // - thread 1: function exit (no permanent effect on `y` because it is now Reserved IM unprotected)
@@ -35,18 +41,6 @@ macro_rules! synchronized {
 }
 
 fn main() {
-    eprintln!("Without spurious write");
-    example(false);
-
-    eprintln!("\nIf this text is visible then the model forbids spurious writes.\n");
-
-    eprintln!("With spurious write");
-    example(true);
-
-    eprintln!("\nIf this text is visible then the model fails to detect a noalias violation.\n");
-}
-
-fn example(spurious: bool) {
     // For this example it is important that we have at least two bytes
     // because lazyness is involved.
     let mut data = [0u8; 2];
@@ -62,12 +56,12 @@ fn example(spurious: bool) {
         synchronized!(b, "start");
         let ptr = ptr;
         synchronized!(b, "retag x (&mut, protect)");
-        fn inner(x: &mut u8, b: IdxBarrier, spurious: bool) {
+        fn inner(x: &mut u8, b: IdxBarrier) {
             *x = 42; // activate immediately
             synchronized!(b, "[lazy] retag y (&mut, protect, IM)");
             // A spurious write should be valid here because `x` is
             // `Active` and protected.
-            if spurious {
+            if cfg!(with) {
                 synchronized!(b, "spurious write x (executed)");
                 *x = 64;
             } else {
@@ -76,7 +70,7 @@ fn example(spurious: bool) {
             synchronized!(b, "ret y");
             synchronized!(b, "ret x");
         }
-        inner(unsafe { &mut *ptr.0 }, b.clone(), spurious);
+        inner(unsafe { &mut *ptr.0 }, b.clone());
         synchronized!(b, "write y");
         synchronized!(b, "end");
     });

src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr

@@ -0,0 +1,40 @@
+Thread 1 executing: start
+Thread 2 executing: start
+Thread 2 executing: retag x (&mut, protect)
+Thread 1 executing: retag x (&mut, protect)
+Thread 1 executing: [lazy] retag y (&mut, protect, IM)
+Thread 2 executing: [lazy] retag y (&mut, protect, IM)
+Thread 2 executing: spurious write x
+Thread 1 executing: spurious write x (executed)
+Thread 1 executing: ret y
+Thread 2 executing: ret y
+Thread 2 executing: ret x
+Thread 1 executing: ret x
+Thread 1 executing: write y
+Thread 2 executing: write y
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
+  --> $DIR/reservedim_spurious_write.rs:LL:CC
+   |
+LL |         unsafe { *y.wrapping_sub(1) = 13 }
+   |                  ^^^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
+   |
+   = 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> has state Disabled which forbids this child write access
+help: the accessed tag <TAG> was created here, in the initial state Reserved
+  --> $DIR/reservedim_spurious_write.rs:LL:CC
+   |
+LL |         fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
+   |                  ^
+help: the accessed tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x1]
+  --> $DIR/reservedim_spurious_write.rs:LL:CC
+   |
+LL |                 *x = 64;
+   |                 ^^^^^^^
+   = help: this transition corresponds to a loss of read and write permissions
+   = note: BACKTRACE (of the first span) on thread `unnamed-ID`:
+   = note: inside closure at $DIR/reservedim_spurious_write.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to 1 previous error
+

src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.stderr renamed to src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr

@@ -1,4 +1,3 @@
-Without spurious write
 Thread 1 executing: start
 Thread 2 executing: start
 Thread 2 executing: retag x (&mut, protect)