diff --git a/src/borrow_tracker/tree_borrows/perms.rs b/src/borrow_tracker/tree_borrows/perms.rs index 6e157d3fcd..5d7c3d8c21 100644 --- a/src/borrow_tracker/tree_borrows/perms.rs +++ b/src/borrow_tracker/tree_borrows/perms.rs @@ -237,6 +237,10 @@ impl Permission { pub fn is_active(&self) -> bool { self.inner == Active } + /// Check if `self` is the never-allow-writes-again state of a pointer (is `Frozen`). + pub fn is_frozen(&self) -> bool { + self.inner == Frozen + } /// Default initial permission of the root of a new tree at inbounds positions. /// Must *only* be used for the root, this is not in general an "initial" permission! diff --git a/src/borrow_tracker/tree_borrows/tree.rs b/src/borrow_tracker/tree_borrows/tree.rs index 3f524dc589..fd69278f20 100644 --- a/src/borrow_tracker/tree_borrows/tree.rs +++ b/src/borrow_tracker/tree_borrows/tree.rs @@ -153,8 +153,31 @@ impl LocationState { ) -> ContinueTraversal { if rel_pos.is_foreign() { let happening_now = IdempotentForeignAccess::from_foreign(access_kind); - let new_access_noop = + let mut new_access_noop = self.idempotent_foreign_access.can_skip_foreign_access(happening_now); + if self.permission.is_disabled() { + // A foreign access to a `Disabled` tag will have almost no observable effect. + // It's a theorem that `Disabled` node have no protected initialized children, + // and so this foreign access will never trigger any protector. + // (Intuition: You're either protected initialized, and thus can't become Disabled + // or you're already Disabled protected, but not initialized, and then can't + // become initialized since that requires a child access, which Disabled blocks.) + // Further, the children will never be able to read or write again, since they + // have a `Disabled` parent. So this only affects diagnostics, such that the + // blocking write will still be identified directly, just at a different tag. + new_access_noop = true; + } + if self.permission.is_frozen() && access_kind == AccessKind::Read { + // A foreign read to a `Frozen` tag will have almost no observable effect. + // It's a theorem that `Frozen` nodes have no active children, so all children + // already survive foreign reads. Foreign reads in general have almost no + // effect, the only further thing they could do is make protected `Reserved` + // nodes become conflicted, i.e. make them reject child writes for the further + // duration of their protector. But such a child write is already rejected + // because this node is frozen. So this only affects diagnostics, but the + // blocking read will still be identified directly, just at a different tag. + new_access_noop = true; + } if new_access_noop { // Abort traversal if the new access is indeed guaranteed // to be noop. diff --git a/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs b/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs new file mode 100644 index 0000000000..6514334b09 --- /dev/null +++ b/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs @@ -0,0 +1,29 @@ +//@compile-flags: -Zmiri-tree-borrows -Zmiri-provenance-gc=0 + +// Shows the effect of the optimization of #4008. +// The diagnostics change, but not the error itself. + +// When this method is called, the tree will be a single line and look like this, +// with other_ptr being the root at the top +// other_ptr = root : Active +// intermediary : Frozen // an intermediary node +// m : Reserved +fn write_to_mut(m: &mut u8, other_ptr: *const u8) { + unsafe { + std::hint::black_box(*other_ptr); + } + // In line 17 above, m should have become Reserved (protected) so that this write is impossible. + // However, that does not happen because the read above is not forwarded to the subtree below + // the Frozen intermediary node. This does not affect UB, however, because the Frozen that blocked + // the read already prevents any child writes. + *m = 42; //~ERROR: /write access through .* is forbidden/ +} + +fn main() { + let root = 42u8; + unsafe { + let intermediary = &root; + let data = &mut *(core::ptr::addr_of!(*intermediary) as *mut u8); + write_to_mut(data, core::ptr::addr_of!(root)); + } +} diff --git a/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr b/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr new file mode 100644 index 0000000000..d3ad2a39f2 --- /dev/null +++ b/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr @@ -0,0 +1,31 @@ +error: Undefined Behavior: write access through at ALLOC[0x0] is forbidden + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | *m = 42; + | ^^^^^^^ 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 is a child of the conflicting tag + = help: the conflicting tag has state Frozen which forbids this child write access +help: the accessed tag was created here + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | fn write_to_mut(m: &mut u8, other_ptr: *const u8) { + | ^ +help: the conflicting tag was created here, in the initial state Frozen + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | let intermediary = &root; + | ^^^^^ + = note: BACKTRACE (of the first span): + = note: inside `write_to_mut` at tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC +note: inside `main` + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | write_to_mut(data, core::ptr::addr_of!(root)); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +error: aborting due to 1 previous error +