diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs index 86074384084d..4d9595b352f2 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs @@ -141,8 +141,14 @@ impl<'tcx> NewPermission { ) -> Option { 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 }) } diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs index 7aa9c3e862bc..9c19ae76a2d0 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs +++ b/src/tools/miri/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; diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr index 7d000ba55e60..ce9a5b7f1586 100644 --- a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr +++ b/src/tools/miri/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 | └─┬── | RsM | ├─┬── | RsM | │ └─┬── -| RsM | │ └──── Strongly protected +| Rs | │ └──── Strongly protected | RsM | └──── ────────────────────────────────────────────────── error: Undefined Behavior: write access through (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 (y, callee:y, caller:y) is foreign to the protected tag (callee:x) (i.e., it is not a child) - = help: this foreign write access would cause the protected tag (callee:x) (currently Reserved (interior mutable)) to become Disabled + = help: this foreign write access would cause the protected tag (callee:x) (currently Reserved) to become Disabled = help: protected tags must never be Disabled help: the accessed tag was created here --> $DIR/cell-protected-write.rs:LL:CC | LL | let y = (&mut *n).get(); | ^^^^^^^^^ -help: the protected tag was created here, in the initial state Reserved (interior mutable) +help: the protected tag was created here, in the initial state Reserved --> $DIR/cell-protected-write.rs:LL:CC | LL | unsafe fn write_second(x: &mut UnsafeCell, y: *mut u8) { 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 1f52537f9a29..5e7cb5e34cc2 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 @@ -100,7 +100,7 @@ fn example(spurious: bool) { let y = inner(unsafe { &mut *(ptr.0 as *mut Cell).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"); }); diff --git a/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.stderr b/src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.stderr new file mode 100644 index 000000000000..9be6c157c0cb --- /dev/null +++ b/src/tools/miri/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 at ALLOC[0x0] is forbidden + --> $DIR/reservedim_spurious_write.rs:LL:CC + | +LL | unsafe { *y.wrapping_sub(1) = 13 } + | ^^^^^^^^^^^^^^^^^^^^^^^ write access through 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 has state Disabled which forbids this child write access +help: the accessed tag was created here, in the initial state Reserved + --> $DIR/reservedim_spurious_write.rs:LL:CC + | +LL | fn inner(y: &mut Cell, b: IdxBarrier) -> *mut u8 { + | ^ +help: the accessed 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 + diff --git a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr index 0d0d52c717fe..d149a4065f92 100644 --- a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr @@ -6,7 +6,7 @@ Warning: this tree is indicative only. Some tags may have been hidden. | RsM | └─┬── | RsM | ├─┬── | RsM | │ └─┬── -| RsCM| │ └──── +| RsC | │ └──── | RsM | └──── ────────────────────────────────────────────────── [interior mut] Foreign Read: Re* -> Re*