Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Disable tree traversal optimization that is wrong due to lazy nodes. #3847

Merged
merged 2 commits into from
Aug 27, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions src/borrow_tracker/tree_borrows/tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)?;
Expand Down
23 changes: 23 additions & 0 deletions tests/fail/tree_borrows/repeated_foreign_read_lazy_conflicted.rs
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
error: Undefined Behavior: write access through <TAG> 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 <TAG> 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 <TAG> has state Reserved (conflicted) which forbids this child write access
help: the accessed tag <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 <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