Second byte is not involved in the example; use a Cell<()> instead

3 files changed, 19 insertions, 16 deletions

diff --git a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs
index 611f64dce5e..6ae79be6cc7 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs
+++ b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs
@@ -41,10 +41,10 @@ macro_rules! synchronized {
 }
 
 fn main() {
-    // For this example it is important that we have at least two bytes
-    // because lazyness is involved.
-    let mut data = [0u8; 2];
-    let ptr = SendPtr(std::ptr::addr_of_mut!(data[0]));
+    // The conflict occurs one one single location but the example involves
+    // lazily initialized permissions.
+    let mut data = 0u8;
+    let ptr = SendPtr(std::ptr::addr_of_mut!(data));
     let barrier = Arc::new(Barrier::new(2));
     let bx = Arc::clone(&barrier);
     let by = Arc::clone(&barrier);
@@ -84,17 +84,20 @@ fn main() {
         let ptr = ptr;
         synchronized!(b, "retag x (&mut, protect)");
         synchronized!(b, "[lazy] retag y (&mut, protect, IM)");
-        fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
+        fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
             synchronized!(b, "spurious write x");
             synchronized!(b, "ret y");
-            y as *mut Cell<u8> as *mut u8
+            // `y` is not retagged for any bytes, so the pointer we return
+            // has its permission lazily initialized.
+            y as *mut Cell<()> as *mut u8
         }
-        // Currently `ptr` points to `data[0]`. We retag it for `data[1]`
-        // then use it for `data[0]` where its initialization has been deferred.
-        let y = inner(unsafe { &mut *(ptr.0 as *mut Cell<u8>).wrapping_add(1) }, b.clone());
+        // Currently `ptr` points to `data`.
+        // We do a zero-sized retag so that its permission is lazy.
+        let y_zst = unsafe { &mut *(ptr.0 as *mut Cell<()>) };
+        let y = inner(y_zst, b.clone());
         synchronized!(b, "ret x");
         synchronized!(b, "write y");
-        unsafe { *y.wrapping_sub(1) = 13 } //~ERROR: /write access through .* is forbidden/
+        unsafe { *y = 13 } //~ERROR: /write access through .* is forbidden/
         synchronized!(b, "end");
     });
 
diff --git a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr
index 5ac9c912ba9..0e4517e9010 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr
@@ -15,15 +15,15 @@ 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
+LL |         unsafe { *y = 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 {
+LL |         fn inner(y: &mut Cell<()>, 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
diff --git a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr
index 97c71fdedef..cbeef90243b 100644
--- a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr
+++ b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr
@@ -15,15 +15,15 @@ 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
+LL |         unsafe { *y = 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 {
+LL |         fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
    |                  ^
 help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag
   --> $DIR/reservedim_spurious_write.rs:LL:CC