From 4e806fbaac887432cba88e08e5e6294dc5215ba4 Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Fri, 12 Sep 2025 23:28:37 +0330 Subject: [PATCH 1/4] Add strong mode for tree borrows --- src/bin/miri.rs | 8 ++++++ src/borrow_tracker/mod.rs | 1 + src/borrow_tracker/tree_borrows/mod.rs | 13 +++++++++ src/borrow_tracker/tree_borrows/perms.rs | 2 +- .../spurious_write_may_be_added.rs | 15 +++++++++++ .../spurious_write_may_be_added.stack.stderr | 25 +++++++++++++++++ .../spurious_write_may_be_added.tree.stderr | 27 +++++++++++++++++++ 7 files changed, 90 insertions(+), 1 deletion(-) create mode 100644 tests/fail/both_borrows/spurious_write_may_be_added.rs create mode 100644 tests/fail/both_borrows/spurious_write_may_be_added.stack.stderr create mode 100644 tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr diff --git a/src/bin/miri.rs b/src/bin/miri.rs index 8b15a78634..5ec3a0ab8b 100644 --- a/src/bin/miri.rs +++ b/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" { diff --git a/src/borrow_tracker/mod.rs b/src/borrow_tracker/mod.rs index 89bd93edae..e231b35f62 100644 --- a/src/borrow_tracker/mod.rs +++ b/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 { diff --git a/src/borrow_tracker/tree_borrows/mod.rs b/src/borrow_tracker/tree_borrows/mod.rs index 6e5b5c807a..6b960654a2 100644 --- a/src/borrow_tracker/tree_borrows/mod.rs +++ b/src/borrow_tracker/tree_borrows/mod.rs @@ -146,6 +146,16 @@ 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; + 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. @@ -155,6 +165,9 @@ impl<'tcx> NewPermission { let freeze_perm = match ref_mutability { // Shared references are frozen. Some(Mutability::Not) => Permission::new_frozen(), + // Mutable references on fn entry are activated based on config + Some(Mutability::Mut) if start_mut_ref_on_fn_entry_as_active && is_protected => + Permission::new_active(), // Mutable references and Boxes are reserved. _ => Permission::new_reserved_frz(), }; diff --git a/src/borrow_tracker/tree_borrows/perms.rs b/src/borrow_tracker/tree_borrows/perms.rs index e21775c9f2..4013c76b73 100644 --- a/src/borrow_tracker/tree_borrows/perms.rs +++ b/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 | Active) } /// Reject `ReservedIM` that cannot exist in the presence of a protector. diff --git a/tests/fail/both_borrows/spurious_write_may_be_added.rs b/tests/fail/both_borrows/spurious_write_may_be_added.rs new file mode 100644 index 0000000000..a34be15bdc --- /dev/null +++ b/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/ +} diff --git a/tests/fail/both_borrows/spurious_write_may_be_added.stack.stderr b/tests/fail/both_borrows/spurious_write_may_be_added.stack.stderr new file mode 100644 index 0000000000..9751dfd835 --- /dev/null +++ b/tests/fail/both_borrows/spurious_write_may_be_added.stack.stderr @@ -0,0 +1,25 @@ +error: Undefined Behavior: attempting a read access using 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: 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: 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 + diff --git a/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr b/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr new file mode 100644 index 0000000000..f196a2ca7d --- /dev/null +++ b/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr @@ -0,0 +1,27 @@ +error: Undefined Behavior: read access through 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 has state Disabled which forbids this child read access +help: the accessed 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 later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag + --> 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 + From 52b02f924f68c5a55410b7c423318c2ce7a76bfe Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Tue, 16 Sep 2025 00:40:11 +0330 Subject: [PATCH 2/4] Add a data race test --- .../spurious_write_may_be_added_data_race.rs | 49 +++++++++++++++++++ ..._write_may_be_added_data_race.stack.stderr | 27 ++++++++++ ...s_write_may_be_added_data_race.tree.stderr | 30 ++++++++++++ 3 files changed, 106 insertions(+) create mode 100644 tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs create mode 100644 tests/fail/both_borrows/spurious_write_may_be_added_data_race.stack.stderr create mode 100644 tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr diff --git a/tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs b/tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs new file mode 100644 index 0000000000..ddd5b344f7 --- /dev/null +++ b/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); + +// 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(); +} diff --git a/tests/fail/both_borrows/spurious_write_may_be_added_data_race.stack.stderr b/tests/fail/both_borrows/spurious_write_may_be_added_data_race.stack.stderr new file mode 100644 index 0000000000..8af94438fb --- /dev/null +++ b/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 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: 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: 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 + diff --git a/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr b/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr new file mode 100644 index 0000000000..a5aa9304ea --- /dev/null +++ b/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr @@ -0,0 +1,30 @@ +Thread 2 executing: after enter +Thread 1 executing: before read +error: Undefined Behavior: read access through 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 is foreign to the protected tag (i.e., it is not a child) + = help: this foreign read access would cause the protected tag (currently Active) to become Disabled + = help: protected tags must never be Disabled +help: the accessed tag was created here + --> tests/fail/both_borrows/spurious_write_may_be_added_data_race.rs:LL:CC + | +LL | let target_alias = &*target; + | ^^^^^^^^ +help: the protected tag was created here, in the initial state Active + --> 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) { + | ^^ + = 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 + From 9b29953ec7c0e08ac63be7fafd951caebc97fd7e Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Thu, 25 Sep 2025 00:07:42 +0330 Subject: [PATCH 3/4] Use an implicit write and disable it for functions with raw pointers in signature --- src/borrow_tracker/tree_borrows/mod.rs | 49 +++++++++++++++++-- src/borrow_tracker/tree_borrows/perms.rs | 2 +- .../spurious_write_may_be_added.tree.stderr | 4 +- ...s_write_may_be_added_data_race.tree.stderr | 9 ++-- tests/pass/both_borrows/2phase.rs | 3 +- .../pass/both_borrows/basic_aliasing_model.rs | 3 +- .../pass/both_borrows/interior_mutability.rs | 3 +- tests/pass/both_borrows/smallvec.rs | 3 +- tests/pass/both_borrows/unsafe_pinned.rs | 3 +- 9 files changed, 61 insertions(+), 18 deletions(-) diff --git a/src/borrow_tracker/tree_borrows/mod.rs b/src/borrow_tracker/tree_borrows/mod.rs index 6b960654a2..62f95356a9 100644 --- a/src/borrow_tracker/tree_borrows/mod.rs +++ b/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, + /// Whether an implicit write should be performed on retag. + do_a_write: bool, } impl<'tcx> NewPermission { @@ -156,6 +159,23 @@ impl<'tcx> NewPermission { .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. @@ -165,9 +185,6 @@ impl<'tcx> NewPermission { let freeze_perm = match ref_mutability { // Shared references are frozen. Some(Mutability::Not) => Permission::new_frozen(), - // Mutable references on fn entry are activated based on config - Some(Mutability::Mut) if start_mut_ref_on_fn_entry_as_active && is_protected => - Permission::new_active(), // Mutable references and Boxes are reserved. _ => Permission::new_reserved_frz(), }; @@ -196,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)), }) } } @@ -396,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 })) @@ -600,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) } diff --git a/src/borrow_tracker/tree_borrows/perms.rs b/src/borrow_tracker/tree_borrows/perms.rs index 4013c76b73..e21775c9f2 100644 --- a/src/borrow_tracker/tree_borrows/perms.rs +++ b/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 | Active) + matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM | Cell) } /// Reject `ReservedIM` that cannot exist in the presence of a protector. diff --git a/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr b/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr index f196a2ca7d..17feffef10 100644 --- a/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr +++ b/tests/fail/both_borrows/spurious_write_may_be_added.tree.stderr @@ -12,11 +12,11 @@ help: the accessed tag was created here, in the initial state Frozen | LL | let target_alias = &*target; | ^^^^^^^^ -help: the accessed tag later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag +help: the accessed 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 diff --git a/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr b/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr index a5aa9304ea..a916a555ee 100644 --- a/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr +++ b/tests/fail/both_borrows/spurious_write_may_be_added_data_race.tree.stderr @@ -8,19 +8,18 @@ LL | let _val = unsafe { *ptr.0 }; | = 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 is foreign to the protected tag (i.e., it is not a child) - = help: this foreign read access would cause the protected tag (currently Active) to become Disabled - = help: protected tags must never be Disabled -help: the accessed tag was created here + = help: the accessed tag has state Disabled which forbids this child read access +help: the accessed 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 protected tag was created here, in the initial state Active +help: the accessed 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 diff --git a/tests/pass/both_borrows/2phase.rs b/tests/pass/both_borrows/2phase.rs index 7a3962a7c1..41bfcfd383 100644 --- a/tests/pass/both_borrows/2phase.rs +++ b/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) {} diff --git a/tests/pass/both_borrows/basic_aliasing_model.rs b/tests/pass/both_borrows/basic_aliasing_model.rs index 115e232dde..95287f6458 100644 --- a/tests/pass/both_borrows/basic_aliasing_model.rs +++ b/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; diff --git a/tests/pass/both_borrows/interior_mutability.rs b/tests/pass/both_borrows/interior_mutability.rs index f095e215e0..16159922b0 100644 --- a/tests/pass/both_borrows/interior_mutability.rs +++ b/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}; diff --git a/tests/pass/both_borrows/smallvec.rs b/tests/pass/both_borrows/smallvec.rs index f48815e37b..fafdb75695 100644 --- a/tests/pass/both_borrows/smallvec.rs +++ b/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}; diff --git a/tests/pass/both_borrows/unsafe_pinned.rs b/tests/pass/both_borrows/unsafe_pinned.rs index 0c75a07bfa..4292505043 100644 --- a/tests/pass/both_borrows/unsafe_pinned.rs +++ b/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; From 572b1a2f474116bf060f7cb3e84b8096711921bd Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Sat, 11 Oct 2025 01:50:44 +0330 Subject: [PATCH 4/4] Remove extra field --- src/borrow_tracker/tree_borrows/mod.rs | 40 +++++++++--------------- src/borrow_tracker/tree_borrows/perms.rs | 6 +++- 2 files changed, 19 insertions(+), 27 deletions(-) diff --git a/src/borrow_tracker/tree_borrows/mod.rs b/src/borrow_tracker/tree_borrows/mod.rs index 62f95356a9..25fd28d356 100644 --- a/src/borrow_tracker/tree_borrows/mod.rs +++ b/src/borrow_tracker/tree_borrows/mod.rs @@ -5,7 +5,6 @@ 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::*; @@ -131,8 +130,6 @@ 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, - /// Whether an implicit write should be performed on retag. - do_a_write: bool, } impl<'tcx> NewPermission { @@ -182,13 +179,20 @@ impl<'tcx> NewPermission { 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. @@ -213,10 +217,6 @@ 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)), }) } } @@ -389,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(), @@ -422,23 +428,6 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { 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 })) @@ -638,7 +627,6 @@ 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) } diff --git a/src/borrow_tracker/tree_borrows/perms.rs b/src/borrow_tracker/tree_borrows/perms.rs index e21775c9f2..5528d2ab33 100644 --- a/src/borrow_tracker/tree_borrows/perms.rs +++ b/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 {