Implement fix for reservedim_spurious_write: ignore IM on protected

Author: Vanille-N

src/borrow_tracker/tree_borrows/mod.rs

@@ -141,8 +141,14 @@ impl<'tcx> NewPermission {
     ) -> Option<Self> {
         let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.param_env());
         let ty_is_unpin = pointee.is_unpin(*cx.tcx, cx.param_env());
+        let is_protected = kind == RetagKind::FnEntry;
+        // 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.
         let initial_state = match mutability {
-            Mutability::Mut if ty_is_unpin => Permission::new_reserved(ty_is_freeze),
+            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
@@ -151,7 +157,7 @@ impl<'tcx> NewPermission {
             _ => return None,
         };
 
-        let protector = (kind == RetagKind::FnEntry).then_some(ProtectorKind::StrongProtector);
+        let protector = is_protected.then_some(ProtectorKind::StrongProtector);
         Some(Self { zero_size: false, initial_state, protector })
     }
 

src/borrow_tracker/tree_borrows/perms.rs

@@ -22,6 +22,11 @@ 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 },
     /// represents: a unique pointer;
     /// allows: child reads, child writes;

tests/fail/tree_borrows/reserved/cell-protected-write.stderr

@@ -5,7 +5,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 | RsM |      └─┬──<TAG=base>
 | RsM |        ├─┬──<TAG=x>
 | RsM |        │ └─┬──<TAG=caller:x>
-| RsM |        │   └────<TAG=callee:x> Strongly protected
+| Rs  |        │   └────<TAG=callee:x> Strongly protected
 | RsM |        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────
 error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
@@ -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 (interior mutable)) to become Disabled
+   = help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved) 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 (interior mutable)
+help: the protected tag <TAG> was created here, in the initial state Reserved
   --> $DIR/cell-protected-write.rs:LL:CC
    |
 LL |         unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {

tests/fail/tree_borrows/reservedim_spurious_write.rs

@@ -100,7 +100,7 @@ fn example(spurious: bool) {
         let y = inner(unsafe { &mut *(ptr.0 as *mut Cell<u8>).wrapping_add(1) }, b.clone());
         synchronized!(b, "ret x");
         synchronized!(b, "write y");
-        unsafe { *y.wrapping_sub(1) = 13 }
+        unsafe { *y.wrapping_sub(1) = 13 } //~ERROR: /write access through .* is forbidden/
         synchronized!(b, "end");
     });
 

tests/fail/tree_borrows/reservedim_spurious_write.stderr

@@ -0,0 +1,41 @@
+Without spurious write
+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 (skipped)
+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 protector release (acting as a foreign write access) on every location previously accessed by this tag
+  --> $DIR/reservedim_spurious_write.rs:LL:CC
+   |
+LL |         }
+   |          ^
+   = 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
+

tests/pass/tree_borrows/reserved.stderr

@@ -6,7 +6,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 | RsM |      └─┬──<TAG=base>
 | RsM |        ├─┬──<TAG=x>
 | RsM |        │ └─┬──<TAG=caller:x>
-| RsCM|        │   └────<TAG=callee:x>
+| RsC |        │   └────<TAG=callee:x>
 | RsM |        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────
 [interior mut] Foreign Read: Re* -> Re*