Merge pull request #4008 from JoJoDeveloping/tb-access-state-based-skipping

[TB Optimization] Skip subtrees based on the subtree's root node's permissions

4 files changed, 88 insertions, 1 deletions

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 6e157d3fcd3..5d7c3d8c219 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/tools/miri/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/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
index 3f524dc589f..fd69278f20a 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
+++ b/src/tools/miri/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/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs
new file mode 100644
index 00000000000..6514334b09d
--- /dev/null
+++ b/src/tools/miri/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/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr
new file mode 100644
index 00000000000..d3ad2a39f2d
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr
@@ -0,0 +1,31 @@
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
+  --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
+   |
+LL |     *m = 42;
+   |     ^^^^^^^ 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> is a child of the conflicting tag <TAG>
+   = help: the conflicting tag <TAG> has state Frozen which forbids this child write access
+help: the accessed tag <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 <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
+