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

Auto merge of #3964 - RalfJung:write-during-2phase, r=RalfJung

Browse Source 
simplify Tree Borrows write-during-2phase example
This commit is contained in:
bors 2024-10-11 10:41:15 +00:00
commit 2eda6a4e6e
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() {
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);
}

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
--> 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):
@ -22,13 +22,12 @@ LL | *inner = 42;
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 | | });
| |______^