Add strong mode for tree borrows

src/bin/miri.rs

@@ -517,6 +517,14 @@ fn main() {
             miri_config.borrow_tracker =
                 Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
                     precise_interior_mut: true,
+                    start_mut_ref_on_fn_entry_as_active: false,
+                }));
+            miri_config.provenance_mode = ProvenanceMode::Strict;
+        } else if arg == "-Zmiri-tree-borrows-strong" {
+            miri_config.borrow_tracker =
+                Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
+                    precise_interior_mut: true,
+                    start_mut_ref_on_fn_entry_as_active: true,
                 }));
             miri_config.provenance_mode = ProvenanceMode::Strict;
         } else if arg == "-Zmiri-tree-borrows-no-precise-interior-mut" {

src/borrow_tracker/mod.rs

@@ -233,6 +233,7 @@ pub enum BorrowTrackerMethod {
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
 pub struct TreeBorrowsParams {
     pub precise_interior_mut: bool,
+    pub start_mut_ref_on_fn_entry_as_active: bool,
 }
 
 impl BorrowTrackerMethod {

src/borrow_tracker/tree_borrows/mod.rs

@@ -1,7 +1,7 @@
 use rustc_abi::{BackendRepr, Size};
 use rustc_middle::mir::{Mutability, RetagKind};
 use rustc_middle::ty::layout::HasTypingEnv;
-use rustc_middle::ty::{self, Ty};
+use rustc_middle::ty::{self, InstanceKind, Ty};
 
 use self::foreign_access_skipping::IdempotentForeignAccess;
 use self::tree::LocationState;
@@ -146,19 +146,53 @@ impl<'tcx> NewPermission {
         let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.typing_env());
         let is_protected = retag_kind == RetagKind::FnEntry;
 
+        let start_mut_ref_on_fn_entry_as_active = cx
+            .machine
+            .borrow_tracker
+            .as_ref()
+            .unwrap()
+            .borrow()
+            .borrow_tracker_method
+            .get_tree_borrows_params()
+            .start_mut_ref_on_fn_entry_as_active;
+
+        let current_function_involves_raw_pointers = 'b: {
+            let instance = cx
+                .machine
+                .threads
+                .active_thread_stack()
+                .last()
+                .expect("Current frame has no stack")
+                .instance();
+            let ty = instance.ty(*cx.tcx, cx.typing_env());
+            if !ty.is_fn() {
+                break 'b false;
+            }
+            let sig = ty.fn_sig(*cx.tcx);
+            matches!(instance.def, InstanceKind::Item(_))
+                && sig.inputs_and_output().skip_binder().iter().any(|x| x.is_raw_ptr())
+        };
+
         if matches!(ref_mutability, Some(Mutability::Mut) | None if !ty_is_unpin) {
             // Mutable reference / Box to pinning type: retagging is a NOP.
             // FIXME: with `UnsafePinned`, this should do proper per-byte tracking.
             return None;
         }
 
+        let start_as_unique = start_mut_ref_on_fn_entry_as_active
+            && is_protected
+            && !current_function_involves_raw_pointers
+            && matches!(ref_mutability, Some(Mutability::Mut));
+
         let freeze_perm = match ref_mutability {
+            _ if start_as_unique => Permission::new_unique(),
             // Shared references are frozen.
             Some(Mutability::Not) => Permission::new_frozen(),
             // Mutable references and Boxes are reserved.
             _ => Permission::new_reserved_frz(),
         };
         let nonfreeze_perm = match ref_mutability {
+            _ if start_as_unique => Permission::new_unique(),
             // Shared references are "transparent".
             Some(Mutability::Not) => Permission::new_cell(),
             // *Protected* mutable references and boxes are reserved without regarding for interior mutability.
@@ -355,9 +389,15 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                     size: Size::from_bytes(perm_range.end - perm_range.start),
                 };
 
+                let access_kind = if new_perm.freeze_perm.is_unique() {
+                    AccessKind::Write
+                } else {
+                    AccessKind::Read
+                };
+
                 tree_borrows.perform_access(
                     orig_tag,
-                    Some((range_in_alloc, AccessKind::Read, diagnostics::AccessCause::Reborrow)),
+                    Some((range_in_alloc, access_kind, diagnostics::AccessCause::Reborrow)),
                     this.machine.borrow_tracker.as_ref().unwrap(),
                     alloc_id,
                     this.machine.current_span(),
@@ -383,7 +423,7 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             base_offset,
             orig_tag,
             new_tag,
-            inside_perms,
+            inside_perms.clone(),
             new_perm.outside_perm,
             protected,
             this.machine.current_span(),

src/borrow_tracker/tree_borrows/perms.rs

@@ -90,7 +90,7 @@ impl PartialOrd for PermissionPriv {
 impl PermissionPriv {
     /// Check if `self` can be the initial state of a pointer.
     fn is_initial(&self) -> bool {
-        matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell)
+        matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell | Unique)
     }
 
     /// Reject `ReservedIM` that cannot exist in the presence of a protector.
@@ -258,6 +258,10 @@ impl Permission {
     pub fn is_frozen(&self) -> bool {
         self.inner == Frozen
     }
+    /// Check if `self` is the allow-child-access-reject-foreign-access state of a pointer (is `Unique`).
+    pub fn is_unique(&self) -> bool {
+        self.inner == Unique
+    }
 
     /// Check if `self` is the shared-reference-to-interior-mutable-data state of a pointer.
     pub fn is_cell(&self) -> bool {

tests/fail/both_borrows/spurious_write_may_be_added.rs

@@ -0,0 +1,15 @@
+//@revisions: stack tree
+//@[tree]compile-flags: -Zmiri-tree-borrows-strong
+
+fn may_insert_spurious_write(_x: &mut u32) {}
+
+fn main() {
+    let target = &mut 42;
+    let target_alias = &*target;
+    let target_alias_ptr = target_alias as *const _;
+    may_insert_spurious_write(target);
+    // now `target_alias` is invalid
+    let _val = unsafe { *target_alias_ptr };
+    //~[stack]^ ERROR: /read access .* tag does not exist in the borrow stack/
+    //~[tree]| ERROR: /read access through .* is forbidden/
+}

tests/fail/both_borrows/spurious_write_may_be_added.stack.stderr

@@ -0,0 +1,25 @@
+error: Undefined Behavior: attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let _val = unsafe { *target_alias_ptr };
+   |                         ^^^^^^^^^^^^^^^^^ this error occurs as part of an access at ALLOC[0x0..0x4]
+   |
+   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
+   = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
+help: <TAG> was created by a SharedReadOnly retag at offsets [0x0..0x4]
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let target_alias_ptr = target_alias as *const _;
+   |                            ^^^^^^^^^^^^
+help: <TAG> was later invalidated at offsets [0x0..0x4] by a Unique function-entry retag inside this call
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     may_insert_spurious_write(target);
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = note: BACKTRACE (of the first span):
+   = note: inside `main` at tests/fail/both_borrows/spurious_write_may_be_added.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
+

tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr

@@ -0,0 +1,27 @@
+error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let _val = unsafe { *target_alias_ptr };
+   |                         ^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
+   |
+   = 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: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information
+   = help: the accessed tag <TAG> has state Disabled which forbids this child read access
+help: the accessed tag <TAG> was created here, in the initial state Frozen
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL |     let target_alias = &*target;
+   |                        ^^^^^^^^
+help: the accessed tag <TAG> later transitioned to Disabled due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
+  --> tests/fail/both_borrows/spurious_write_may_be_added.rs:LL:CC
+   |
+LL | fn may_insert_spurious_write(_x: &mut u32) {}
+   |                              ^^
+   = help: this transition corresponds to a loss of read permissions
+   = note: BACKTRACE (of the first span):
+   = note: inside `main` at tests/fail/both_borrows/spurious_write_may_be_added.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
+

tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs

@@ -0,0 +1,49 @@
+//@revisions: stack tree
+//@[tree]compile-flags: -Zmiri-tree-borrows-strong
+use std::sync::{Arc, Barrier};
+
+#[derive(Copy, Clone)]
+struct SendPtr(*const u32);
+
+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 may_insert_spurious_write(_x: &mut u32, b: IdxBarrier) {
+    synchronized!(b, "after enter");
+    synchronized!(b, "before exit");
+}
+
+fn main() {
+    let target = &mut 42;
+    let target_alias = &*target;
+    let target_alias_ptr = SendPtr(target_alias as *const _);
+
+    let barrier = Arc::new(Barrier::new(2));
+    let bx = (1, Arc::clone(&barrier));
+    let by = (2, Arc::clone(&barrier));
+
+    let join_handle = std::thread::spawn(move || {
+        synchronized!(bx, "before read");
+        let ptr = target_alias_ptr;
+        // now `target_alias` is invalid
+        let _val = unsafe { *ptr.0 };
+        //~[stack]^ ERROR: /read access .* tag does not exist in the borrow stack/
+        //~[tree]| ERROR: /read access through .* is forbidden/
+        synchronized!(bx, "after read");
+    });
+
+    may_insert_spurious_write(target, by);
+    let _ = join_handle.join();
+}

tests/fail/both_borrows/spurious_write_may_be_added_data_race.stack.stderr

@@ -0,0 +1,27 @@
+Thread 2 executing: after enter
+Thread 1 executing: before read
+error: Undefined Behavior: attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
+  --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
+   |
+LL |         let _val = unsafe { *ptr.0 };
+   |                             ^^^^^^ this error occurs as part of an access at ALLOC[0x0..0x4]
+   |
+   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
+   = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
+help: <TAG> was created by a SharedReadOnly retag at offsets [0x0..0x4]
+  --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
+   |
+LL |     let target_alias_ptr = SendPtr(target_alias as *const _);
+   |                                    ^^^^^^^^^^^^
+help: <TAG> was later invalidated at offsets [0x0..0x4] by a Unique function-entry retag inside this call
+  --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
+   |
+LL |     may_insert_spurious_write(target, by);
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = note: BACKTRACE (of the first span) on thread `unnamed-ID`:
+   = note: inside closure at tests/fail/both_borrows/spurious_write_may_be_added_data_race.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
+

tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr

@@ -0,0 +1,29 @@
+Thread 2 executing: after enter
+Thread 1 executing: before read
+error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden
+  --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
+   |
+LL |         let _val = unsafe { *ptr.0 };
+   |                             ^^^^^^ Undefined Behavior occurred here
+   |
+   = 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: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information
+   = help: the accessed tag <TAG> has state Disabled which forbids this child read access
+help: the accessed tag <TAG> was created here, in the initial state Frozen
+  --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
+   |
+LL |     let target_alias = &*target;
+   |                        ^^^^^^^^
+help: the accessed tag <TAG> later transitioned to Disabled due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
+  --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC
+   |
+LL | fn may_insert_spurious_write(_x: &mut u32, b: IdxBarrier) {
+   |                              ^^
+   = help: this transition corresponds to a loss of read permissions
+   = note: BACKTRACE (of the first span) on thread `unnamed-ID`:
+   = note: inside closure at tests/fail/both_borrows/spurious_write_may_be_added_data_race.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
+

tests/pass/both_borrows/2phase.rs

@@ -1,5 +1,6 @@
-//@revisions: stack tree
+//@revisions: stack tree tree_strong
 //@[tree]compile-flags: -Zmiri-tree-borrows
+//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
 
 trait S: Sized {
     fn tpb(&mut self, _s: Self) {}

tests/pass/both_borrows/basic_aliasing_model.rs

@@ -1,5 +1,6 @@
-//@revisions: stack tree
+//@revisions: stack tree tree_strong
 //@[tree]compile-flags: -Zmiri-tree-borrows
+//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
 #![feature(allocator_api)]
 use std::alloc::{Layout, alloc, dealloc};
 use std::cell::Cell;

tests/pass/both_borrows/interior_mutability.rs

@@ -1,5 +1,6 @@
-//@revisions: stack tree
+//@revisions: stack tree tree_strong
 //@[tree]compile-flags: -Zmiri-tree-borrows
+//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
 #![allow(dangerous_implicit_autorefs)]
 
 use std::cell::{Cell, Ref, RefCell, RefMut, UnsafeCell};

tests/pass/both_borrows/smallvec.rs

@@ -2,8 +2,9 @@
 //! What makes it interesting as a test is that it relies on Stacked Borrow's "quirk"
 //! in a fundamental, hard-to-fix-without-full-trees way.
 
-//@revisions: stack tree
+//@revisions: stack tree tree_strong
 //@[tree]compile-flags: -Zmiri-tree-borrows
+//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
 
 use std::marker::PhantomData;
 use std::mem::{ManuallyDrop, MaybeUninit};

tests/pass/both_borrows/unsafe_pinned.rs

@@ -1,5 +1,6 @@
-//@revisions: stack tree
+//@revisions: stack tree tree_strong
 //@[tree]compile-flags: -Zmiri-tree-borrows
+//@[tree_strong]compile-flags: -Zmiri-tree-borrows-strong
 #![feature(unsafe_pinned)]
 
 use std::pin::UnsafePinned;