mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

simplify Tree Borrows write-during-2phase example

Browse Source
This commit is contained in:
Ralf Jung 2024-10-11 12:38:58 +02:00
parent 256d63f444
commit ccdea3ee36
2 changed files with 15 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/tools/miri/tests/fail/tree_borrows/write-during-2phase.rs
View File

@ -16,12 +16,15 @@ fn add(&mut self, n: u64) -> u64 { //~ ERROR: /reborrow through .* is forbidden/
pub fn main() { pub fn main() {
let mut f = Foo(0); let mut f = Foo(0);
let inner = &mut f.0 as *mut u64; let alias = &mut f.0 as *mut u64;
let _res = f.add(unsafe { let res = f.add(unsafe {
let n = f.0;
// This is the access at fault, but it's not immediately apparent because // This is the access at fault, but it's not immediately apparent because
// the reference that got invalidated is not under a Protector. // the reference that got invalidated is not under a Protector.
*inner = 42; *alias = 42;
n 0
}); });
// `res` could be optimized to be `0`, since at the time the reference for the `self` argument
// is created, it has value `0`, and then later we add `0` to that. But turns out there is
// a sneaky alias that's used to change the value of `*self` before it is read...
assert_eq!(res, 42);
} }

15
src/tools/miri/tests/fail/tree_borrows/write-during-2phase.stderr
View File

@ -9,12 +9,12 @@ LL | fn add(&mut self, n: u64) -> u64 {
help: the accessed tag <TAG> was created here, in the initial state Reserved help: the accessed tag <TAG> was created here, in the initial state Reserved
--> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC --> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC
| |
LL | let _res = f.add(unsafe { LL | let res = f.add(unsafe {
| ^ | ^
help: the accessed tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x8] help: the accessed tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x8]
--> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC --> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC
| |
LL | *inner = 42; LL | *alias = 42;
| ^^^^^^^^^^^ | ^^^^^^^^^^^
= help: this transition corresponds to a loss of read and write permissions = help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span): = note: BACKTRACE (of the first span):
@ -22,13 +22,12 @@ LL | *inner = 42;
note: inside `main` note: inside `main`
--> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC --> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC
| |
LL | let _res = f.add(unsafe { LL | let res = f.add(unsafe {
| ________________^ | _______________^
LL | | let n = f.0;
LL | | // This is the access at fault, but it's not immediately apparent because LL | | // This is the access at fault, but it's not immediately apparent because
LL | | // the reference that got invalidated is not under a Protector. LL | | // the reference that got invalidated is not under a Protector.
LL | | *inner = 42; LL | | *alias = 42;
LL | | n LL | | 0
LL | | }); LL | | });
| |______^ | |______^