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..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 { @@ -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) } 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..17feffef10 --- /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 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 + 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..a916a555ee --- /dev/null +++ b/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 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 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 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 + +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/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;