diff --git a/src/borrow_tracker/tree_borrows/tree.rs b/src/borrow_tracker/tree_borrows/tree.rs index d51e1109ed..5fbb7b9277 100644 --- a/src/borrow_tracker/tree_borrows/tree.rs +++ b/src/borrow_tracker/tree_borrows/tree.rs @@ -150,7 +150,10 @@ impl LocationState { // the propagation can be skipped next time. // It is a performance loss not to call this function when a foreign access occurs. // It is unsound not to call this function when a child access occurs. - fn skip_if_known_noop( + // FIXME: This optimization is wrong, and is currently disabled (by ignoring the + // result returned here). Since we presumably want an optimization like this, + // we should add it back. See #3864 for more information. + fn update_last_foreign_access( &mut self, access_kind: AccessKind, rel_pos: AccessRelatedness, @@ -613,10 +616,7 @@ impl<'tcx> Tree { let old_state = perm.or_insert(LocationState::new_uninit(node.default_initial_perm)); - match old_state.skip_if_known_noop(access_kind, rel_pos) { - ContinueTraversal::SkipChildren => return Ok(ContinueTraversal::SkipChildren), - _ => {} - } + old_state.update_last_foreign_access(access_kind, rel_pos); let protected = global.borrow().protected_tags.contains_key(&node.tag); let transition = old_state.perform_access(access_kind, rel_pos, protected)?; diff --git a/tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.rs b/tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.rs new file mode 100644 index 0000000000..36b47a33b1 --- /dev/null +++ b/tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.rs @@ -0,0 +1,23 @@ +//@compile-flags: -Zmiri-tree-borrows + +use std::ptr::addr_of_mut; + +fn do_something(_: u8) {} + +unsafe fn access_after_sub_1(x: &mut u8, orig_ptr: *mut u8) { + // causes a second access, which should make the lazy part of `x` be `Reserved {conflicted: true}` + do_something(*orig_ptr); + // read from the conflicted pointer + *(x as *mut u8).byte_sub(1) = 42; //~ ERROR: /write access through .* is forbidden/ +} + +pub fn main() { + unsafe { + let mut alloc = [0u8, 0u8]; + let orig_ptr = addr_of_mut!(alloc) as *mut u8; + let foo = &mut *orig_ptr; + // cause a foreign read access to foo + do_something(alloc[0]); + access_after_sub_1(&mut *(foo as *mut u8).byte_add(1), orig_ptr); + } +} diff --git a/tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.stderr b/tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.stderr new file mode 100644 index 0000000000..963e8e5eca --- /dev/null +++ b/tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.stderr @@ -0,0 +1,31 @@ +error: Undefined Behavior: write access through at ALLOC[0x0] is forbidden + --> $DIR/repeated_foreign_read_lazy_conflicted.rs:LL:CC + | +LL | *(x as *mut u8).byte_sub(1) = 42; + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ write access through 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 has state Reserved (conflicted) which forbids this child write access +help: the accessed tag was created here, in the initial state Reserved + --> $DIR/repeated_foreign_read_lazy_conflicted.rs:LL:CC + | +LL | unsafe fn access_after_sub_1(x: &mut u8, orig_ptr: *mut u8) { + | ^ +help: the accessed tag later transitioned to Reserved (conflicted) due to a foreign read access at offsets [0x0..0x1] + --> $DIR/repeated_foreign_read_lazy_conflicted.rs:LL:CC + | +LL | do_something(*orig_ptr); + | ^^^^^^^^^ + = help: this transition corresponds to a temporary loss of write permissions until function exit + = note: BACKTRACE (of the first span): + = note: inside `access_after_sub_1` at $DIR/repeated_foreign_read_lazy_conflicted.rs:LL:CC +note: inside `main` + --> $DIR/repeated_foreign_read_lazy_conflicted.rs:LL:CC + | +LL | access_after_sub_1(&mut *(foo as *mut u8).byte_add(1), orig_ptr); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +error: aborting due to 1 previous error +