Auto merge of #3742 - Vanille-N:master, r=RalfJung
TB: Reserved + Protected + IM + lazy is a horrible combination that should not exist
As discovered by `@JoJoDeveloping,` the result of having both Protector exceptions on lazy locations (protectors only protect initialized bytes) and interior mutability exceptions for protected tags (Reserved IM does not accept foreign writes when protected) leads to some very undesirable results, namely that we cannot do spurious writes even on protected activated locations.
We propose that Protected Reserved IM should no longer exist and instead when a type is retagged as part of a `FnEntry` it is assumed to lose interior mutability.
In fact, this was already being done implicitly because relevant transitions were guarded by an `if protected`, but the difference is that now it also applies to transitions that occur after the end of the protector.
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 8607438..123d4b4 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,15 @@
) -> 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: 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 @@
_ => 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 7aa9c3e..8e23257 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 @@
/// - 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 @@
/// non-protected interior mutable `Reserved` which stay the same.
fn foreign_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
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/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 7d000ba..ce9a5b7 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 @@
| 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 @@
|
= 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) {
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
new file mode 100644
index 0000000..73f227f
--- /dev/null
+++ b/src/tools/miri/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<Barrier>);
+
+// 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/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
new file mode 100644
index 0000000..0e4517e
--- /dev/null
+++ b/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 = 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<()>, 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
+
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
new file mode 100644
index 0000000..cbeef90
--- /dev/null
+++ b/src/tools/miri/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 <TAG> at ALLOC[0x0] is forbidden
+ --> $DIR/reservedim_spurious_write.rs:LL:CC
+ |
+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<()>, 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
+
diff --git a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr
index 0d0d52c..d149a40 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 @@
| 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*
