Skip to content

Commit d87cf5a

Browse files
committed
add Miri tests
1 parent a29caab commit d87cf5a

File tree

4 files changed

+131
-0
lines changed

4 files changed

+131
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
//! FIXME: This test should pass! However, `async fn` does not yet use `UnsafePinned`.
2+
//! This is a regression test for <https://github.com/rust-lang/rust/issues/137750>:
3+
//! `UnsafePinned` must include the effects of `UnsafeCell`.
4+
//@revisions: stack tree
5+
//@[tree]compile-flags: -Zmiri-tree-borrows
6+
//@normalize-stderr-test: "ALLOC\[[0xa-f\d.]+\]" -> "ALLOC[OFFSET]"
7+
8+
use core::future::Future;
9+
use core::pin::{Pin, pin};
10+
use core::task::{Context, Poll, Waker};
11+
12+
fn main() {
13+
let mut f = pin!(async move {
14+
let x = &mut 0u8;
15+
core::future::poll_fn(move |_| {
16+
*x = 1; //~ERROR: write access
17+
Poll::<()>::Pending
18+
})
19+
.await
20+
});
21+
let mut cx = Context::from_waker(&Waker::noop());
22+
assert_eq!(f.as_mut().poll(&mut cx), Poll::Pending);
23+
let _: Pin<&_> = f.as_ref(); // Or: `f.as_mut().into_ref()`.
24+
assert_eq!(f.as_mut().poll(&mut cx), Poll::Pending);
25+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
error: Undefined Behavior: attempting a write access using <TAG> at ALLOC[OFFSET], but that tag does not exist in the borrow stack for this location
2+
--> tests/fail/async-shared-mutable.rs:LL:CC
3+
|
4+
LL | *x = 1;
5+
| ^^^^^^
6+
| |
7+
| attempting a write access using <TAG> at ALLOC[OFFSET], but that tag does not exist in the borrow stack for this location
8+
| this error occurs as part of an access at ALLOC[OFFSET]
9+
|
10+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
11+
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
12+
help: <TAG> was created by a Unique retag at offsets [0x8..0x9]
13+
--> tests/fail/async-shared-mutable.rs:LL:CC
14+
|
15+
LL | / core::future::poll_fn(move |_| {
16+
LL | | *x = 1;
17+
LL | | Poll::<()>::Pending
18+
LL | | })
19+
LL | | .await
20+
| |______________^
21+
help: <TAG> was later invalidated at offsets [0x0..0x10] by a SharedReadOnly retag
22+
--> tests/fail/async-shared-mutable.rs:LL:CC
23+
|
24+
LL | let _: Pin<&_> = f.as_ref(); // Or: `f.as_mut().into_ref()`.
25+
| ^^^^^^^^^^
26+
= note: BACKTRACE (of the first span):
27+
= note: inside closure at tests/fail/async-shared-mutable.rs:LL:CC
28+
= note: inside `<std::future::PollFn<{closure@tests/fail/async-shared-mutable.rs:LL:CC}> as std::future::Future>::poll` at RUSTLIB/core/src/future/poll_fn.rs:LL:CC
29+
note: inside closure
30+
--> tests/fail/async-shared-mutable.rs:LL:CC
31+
|
32+
LL | .await
33+
| ^^^^^
34+
note: inside `main`
35+
--> tests/fail/async-shared-mutable.rs:LL:CC
36+
|
37+
LL | assert_eq!(f.as_mut().poll(&mut cx), Poll::Pending);
38+
| ^^^^^^^^^^^^^^^^^^^^^^^^
39+
40+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
41+
42+
error: aborting due to 1 previous error
43+
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
error: Undefined Behavior: write access through <TAG> at ALLOC[OFFSET] is forbidden
2+
--> tests/fail/async-shared-mutable.rs:LL:CC
3+
|
4+
LL | *x = 1;
5+
| ^^^^^^ write access through <TAG> at ALLOC[OFFSET] is forbidden
6+
|
7+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
8+
= help: the accessed tag <TAG> has state Frozen which forbids this child write access
9+
help: the accessed tag <TAG> was created here, in the initial state Reserved
10+
--> tests/fail/async-shared-mutable.rs:LL:CC
11+
|
12+
LL | / core::future::poll_fn(move |_| {
13+
LL | | *x = 1;
14+
LL | | Poll::<()>::Pending
15+
LL | | })
16+
LL | | .await
17+
| |______________^
18+
help: the accessed tag <TAG> later transitioned to Active due to a child write access at offsets [0x8..0x9]
19+
--> tests/fail/async-shared-mutable.rs:LL:CC
20+
|
21+
LL | *x = 1;
22+
| ^^^^^^
23+
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference
24+
help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x10]
25+
--> tests/fail/async-shared-mutable.rs:LL:CC
26+
|
27+
LL | let _: Pin<&_> = f.as_ref(); // Or: `f.as_mut().into_ref()`.
28+
| ^^^^^^^^^^
29+
= help: this transition corresponds to a loss of write permissions
30+
= note: BACKTRACE (of the first span):
31+
= note: inside closure at tests/fail/async-shared-mutable.rs:LL:CC
32+
= note: inside `<std::future::PollFn<{closure@tests/fail/async-shared-mutable.rs:LL:CC}> as std::future::Future>::poll` at RUSTLIB/core/src/future/poll_fn.rs:LL:CC
33+
note: inside closure
34+
--> tests/fail/async-shared-mutable.rs:LL:CC
35+
|
36+
LL | .await
37+
| ^^^^^
38+
note: inside `main`
39+
--> tests/fail/async-shared-mutable.rs:LL:CC
40+
|
41+
LL | assert_eq!(f.as_mut().poll(&mut cx), Poll::Pending);
42+
| ^^^^^^^^^^^^^^^^^^^^^^^^
43+
44+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
45+
46+
error: aborting due to 1 previous error
47+
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
#![feature(unsafe_pinned)]
4+
5+
use std::pin::UnsafePinned;
6+
7+
fn mutate(x: &UnsafePinned<i32>) {
8+
let ptr = x as *const _ as *mut i32;
9+
unsafe { ptr.write(42) };
10+
}
11+
12+
fn main() {
13+
let x = UnsafePinned::new(0);
14+
mutate(&x);
15+
assert_eq!(x.into_inner(), 42);
16+
}

0 commit comments

Comments
 (0)