From c1875bfc24dbb88b1cd014cbb94099f708b5242b Mon Sep 17 00:00:00 2001 From: Johannes Hostert Date: Wed, 4 Dec 2024 15:10:05 +0100 Subject: [PATCH] add test to demonstrate the effect of #4008 --- .../subtree_traversal_skipping_diagnostics.rs | 29 +++++++++++++++++ ...tree_traversal_skipping_diagnostics.stderr | 31 +++++++++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs create mode 100644 src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr diff --git a/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs new file mode 100644 index 000000000000..6514334b09df --- /dev/null +++ b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs @@ -0,0 +1,29 @@ +//@compile-flags: -Zmiri-tree-borrows -Zmiri-provenance-gc=0 + +// Shows the effect of the optimization of #4008. +// The diagnostics change, but not the error itself. + +// When this method is called, the tree will be a single line and look like this, +// with other_ptr being the root at the top +// other_ptr = root : Active +// intermediary : Frozen // an intermediary node +// m : Reserved +fn write_to_mut(m: &mut u8, other_ptr: *const u8) { + unsafe { + std::hint::black_box(*other_ptr); + } + // In line 17 above, m should have become Reserved (protected) so that this write is impossible. + // However, that does not happen because the read above is not forwarded to the subtree below + // the Frozen intermediary node. This does not affect UB, however, because the Frozen that blocked + // the read already prevents any child writes. + *m = 42; //~ERROR: /write access through .* is forbidden/ +} + +fn main() { + let root = 42u8; + unsafe { + let intermediary = &root; + let data = &mut *(core::ptr::addr_of!(*intermediary) as *mut u8); + write_to_mut(data, core::ptr::addr_of!(root)); + } +} diff --git a/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr new file mode 100644 index 000000000000..4968047d872b --- /dev/null +++ b/src/tools/miri/tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.stderr @@ -0,0 +1,31 @@ +error: Undefined Behavior: write access through at ALLOC[0x0] is forbidden + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | *m = 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 + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | fn write_to_mut(m: &mut u8, other_ptr: *const u8) { + | ^ +help: the accessed tag later transitioned to Reserved (conflicted) due to a foreign read access at offsets [0x0..0x1] + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | std::hint::black_box(*other_ptr); + | ^^^^^^^^^^ + = help: this transition corresponds to a temporary loss of write permissions until function exit + = note: BACKTRACE (of the first span): + = note: inside `write_to_mut` at tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC +note: inside `main` + --> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC + | +LL | write_to_mut(data, core::ptr::addr_of!(root)); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +error: aborting due to 1 previous error +