add test to demonstrate the effect of #4008

This commit is contained in:
Johannes Hostert 2024-12-04 15:10:05 +01:00
parent fceb304dfd
commit c1875bfc24
No known key found for this signature in database
GPG key ID: 0BA6032B5A38D049
2 changed files with 60 additions and 0 deletions

View file

@ -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));
}
}

View file

@ -0,0 +1,31 @@
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
--> tests/fail/tree_borrows/subtree_traversal_skipping_diagnostics.rs:LL:CC
|
LL | *m = 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
--> 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 <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