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,10 +1,11 @@
 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;
+use crate::borrow_tracker::tree_borrows::diagnostics::AccessCause;
 use crate::borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind};
 use crate::concurrency::data_race::NaReadType;
 use crate::*;
@@ -130,6 +131,8 @@ pub struct NewPermission {
     /// Whether this pointer is part of the arguments of a function call.
     /// `protector` is `Some(_)` for all pointers marked `noalias`.
     protector: Option<ProtectorKind>,
+    /// Whether an implicit write should be performed on retag.
+    do_a_write: bool,
 }
 
 impl<'tcx> NewPermission {
@@ -146,6 +149,33 @@ 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.
@@ -183,6 +213,10 @@ impl<'tcx> NewPermission {
                 // Weak protector for boxes
                 ProtectorKind::WeakProtector
             }),
+            do_a_write: start_mut_ref_on_fn_entry_as_active
+                && is_protected
+                && !current_function_involves_raw_pointers
+                && matches!(ref_mutability, Some(Mutability::Mut)),
         })
     }
 }
@@ -383,11 +417,28 @@ 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(),
         )?;
+        if new_perm.do_a_write {
+            for (perm_range, _) in inside_perms.iter_all() {
+                // Some reborrows incur a write access to the new pointer, to make it active.
+                // Adjust range to be relative to allocation start (rather than to `place`).
+                let range_in_alloc = AllocRange {
+                    start: Size::from_bytes(perm_range.start) + base_offset,
+                    size: Size::from_bytes(perm_range.end - perm_range.start),
+                };
+                tree_borrows.perform_access(
+                    new_tag,
+                    Some((range_in_alloc, AccessKind::Write, AccessCause::Reborrow)),
+                    this.machine.borrow_tracker.as_ref().unwrap(),
+                    alloc_id,
+                    this.machine.current_span(),
+                )?;
+            }
+        }
         drop(tree_borrows);
 
         interp_ok(Some(Provenance::Concrete { alloc_id, tag: new_tag }))
@@ -587,6 +638,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             nonfreeze_access: true,
             outside_perm: Permission::new_reserved_frz(),
             protector: Some(ProtectorKind::StrongProtector),
+            do_a_write: false,
         };
         this.tb_retag_place(place, new_perm)
     }

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;