diff --git a/src/borrow_tracker/tree_borrows/mod.rs b/src/borrow_tracker/tree_borrows/mod.rs index 8607438408..123d4b407f 100644 --- a/src/borrow_tracker/tree_borrows/mod.rs +++ b/src/borrow_tracker/tree_borrows/mod.rs @@ -141,8 +141,15 @@ 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: protected references are always considered + // "freeze". 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 +158,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/borrow_tracker/tree_borrows/perms.rs b/src/borrow_tracker/tree_borrows/perms.rs index 7aa9c3e862..8e23257b6c 100644 --- a/src/borrow_tracker/tree_borrows/perms.rs +++ b/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; @@ -141,6 +146,12 @@ mod transition { /// non-protected interior mutable `Reserved` which stay the same. fn foreign_write(state: PermissionPriv, protected: bool) -> Option { Some(match state { + // FIXME: since the fix related to reservedim_spurious_write, it is now possible + // to express these transitions of the state machine without an explicit dependency + // on `protected`: because `ty_is_freeze: false` implies `!protected` then + // the line handling `Reserved { .. } if protected` could be deleted. + // This will however require optimizations to the exhaustive tests because + // fewer initial conditions are valid. Reserved { .. } if protected => Disabled, res @ Reserved { ty_is_freeze: false, .. } => res, _ => Disabled, diff --git a/tests/fail/tree_borrows/reserved/cell-protected-write.stderr b/tests/fail/tree_borrows/reserved/cell-protected-write.stderr index 7d000ba55e..ce9a5b7f15 100644 --- a/tests/fail/tree_borrows/reserved/cell-protected-write.stderr +++ b/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/tests/fail/tree_borrows/reservedim_spurious_write.rs b/tests/fail/tree_borrows/reservedim_spurious_write.rs new file mode 100644 index 0000000000..73f227fee2 --- /dev/null +++ b/tests/fail/tree_borrows/reservedim_spurious_write.rs @@ -0,0 +1,107 @@ +// Illustrating a problematic interaction between Reserved, interior mutability, +// 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: 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) +// - thread 2: write through `y` +// In the source code nothing happens to `y` + +// `Send`able raw pointer wrapper. +#[derive(Copy, Clone)] +struct SendPtr(*mut u8); +unsafe impl Send for SendPtr {} + +type IdxBarrier = (usize, Arc); + +// Barriers to enforce the interleaving. +// This macro expects `synchronized!(thread, msg)` where `thread` is a `IdxBarrier`, +// and `msg` is the message to be displayed when the thread reaches this point in the execution. +macro_rules! synchronized { + ($thread:expr, $msg:expr) => {{ + let (thread_id, barrier) = &$thread; + eprintln!("Thread {} executing: {}", thread_id, $msg); + barrier.wait(); + }}; +} + +fn main() { + // The conflict occurs on one single location but the example involves + // lazily initialized permissions. We will use `&mut Cell<()>` references + // to `data` to achieve this. + 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); + + // Retag and activate `x`, wait until the other thread creates a lazy permission. + // Then do a spurious write. Finally exit the function after the other thread. + let thread_1 = thread::spawn(move || { + let b = (1, bx); + synchronized!(b, "start"); + let ptr = ptr; + synchronized!(b, "retag x (&mut, protect)"); + 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 cfg!(with) { + synchronized!(b, "spurious write x (executed)"); + *x = 64; + } else { + synchronized!(b, "spurious write x (skipped)"); + } + synchronized!(b, "ret y"); + synchronized!(b, "ret x"); + } + inner(unsafe { &mut *ptr.0 }, b.clone()); + synchronized!(b, "write y"); + synchronized!(b, "end"); + }); + + // Create a lazy Reserved with interior mutability. + // Wait for the other thread's spurious write then observe the side effects + // of that write. + let thread_2 = thread::spawn(move || { + let b = (2, by); + synchronized!(b, "start"); + let ptr = ptr; + synchronized!(b, "retag x (&mut, protect)"); + synchronized!(b, "[lazy] retag y (&mut, protect, IM)"); + fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 { + synchronized!(b, "spurious write x"); + synchronized!(b, "ret y"); + // `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`. + // 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 = 13 } //~ERROR: /write access through .* is forbidden/ + synchronized!(b, "end"); + }); + + thread_1.join().unwrap(); + thread_2.join().unwrap(); +} diff --git a/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr b/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr new file mode 100644 index 0000000000..0e4517e901 --- /dev/null +++ b/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 at ALLOC[0x0] is forbidden + --> $DIR/reservedim_spurious_write.rs:LL:CC + | +LL | unsafe { *y = 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 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 + diff --git a/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr b/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr new file mode 100644 index 0000000000..cbeef90243 --- /dev/null +++ b/tests/fail/tree_borrows/reservedim_spurious_write.without.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 (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 = 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/tests/pass/tree_borrows/reserved.stderr b/tests/pass/tree_borrows/reserved.stderr index 0d0d52c717..d149a4065f 100644 --- a/tests/pass/tree_borrows/reserved.stderr +++ b/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*