Skip to content

Commit

Permalink
Auto merge of #3964 - RalfJung:write-during-2phase, r=RalfJung
Browse files Browse the repository at this point in the history
simplify Tree Borrows write-during-2phase example
  • Loading branch information
bors committed Oct 11, 2024
2 parents 256d63f + ccdea3e commit 2eda6a4
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 13 deletions.
13 changes: 8 additions & 5 deletions src/tools/miri/tests/fail/tree_borrows/write-during-2phase.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,15 @@ impl Foo {

pub fn main() {
let mut f = Foo(0);
let inner = &mut f.0 as *mut u64;
let _res = f.add(unsafe {
let n = f.0;
let alias = &mut f.0 as *mut u64;
let res = f.add(unsafe {
// This is the access at fault, but it's not immediately apparent because
// the reference that got invalidated is not under a Protector.
*inner = 42;
n
*alias = 42;
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);
}
Original file line number Diff line number Diff line change
Expand Up @@ -9,26 +9,25 @@ LL | fn add(&mut self, n: u64) -> u64 {
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> 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]
--> 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
= note: BACKTRACE (of the first span):
= note: inside `Foo::add` at tests/fail/tree_borrows/write-during-2phase.rs:LL:CC
note: inside `main`
--> tests/fail/tree_borrows/write-during-2phase.rs:LL:CC
|
LL | let _res = f.add(unsafe {
| ________________^
LL | | let n = f.0;
LL | let res = f.add(unsafe {
| _______________^
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 | | *inner = 42;
LL | | n
LL | | *alias = 42;
LL | | 0
LL | | });
| |______^

Expand Down

0 comments on commit 2eda6a4

Please sign in to comment.