Skip to content

Commit e243206

Browse files
committed
TB: new tests
1 parent 8741303 commit e243206

30 files changed

+888
-0
lines changed
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
//@compile-flags: -Zmiri-tree-borrows
2+
3+
// Check that TB properly rejects alternating Reads and Writes, but tolerates
4+
// alternating only Reads to Reserved mutable references.
5+
pub fn main() {
6+
let x = &mut 0u8;
7+
let y = unsafe { &mut *(x as *mut u8) };
8+
// Foreign Read, but this is a no-op from the point of view of y (still Reserved)
9+
let _val = *x;
10+
// Now we activate y, for this to succeed y needs to not have been Frozen
11+
// by the previous operation
12+
*y += 1; // Success
13+
// This time y gets Frozen...
14+
let _val = *x;
15+
// ... and the next Write attempt fails.
16+
*y += 1; // Failure //~ ERROR: /write access through .* is forbidden/
17+
let _val = *x;
18+
*y += 1; // Unreachable
19+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
2+
--> $DIR/alternate-read-write.rs:LL:CC
3+
|
4+
LL | *y += 1; // Failure
5+
| ^^^^^^^ write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
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+
= note: BACKTRACE:
9+
= note: inside `main` at $DIR/alternate-read-write.rs:LL:CC
10+
11+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
12+
13+
error: aborting due to previous error
14+
Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
//! Race-condition-like interaction between a read and a reborrow.
2+
//! Even though no write or fake write occurs, reads have an effect on protected
3+
//! Reserved. This is a protected-retag/read data race, but is not *detected* as
4+
//! a data race violation because reborrows are not writes.
5+
//!
6+
//! This test is sensitive to the exact schedule so we disable preemption.
7+
//@compile-flags: -Zmiri-tree-borrows -Zmiri-preemption-rate=0
8+
use std::ptr::addr_of_mut;
9+
use std::thread;
10+
11+
#[derive(Copy, Clone)]
12+
struct SendPtr(*mut u8);
13+
14+
unsafe impl Send for SendPtr {}
15+
16+
// First thread is just a reborrow, but for an instant `x` is
17+
// protected and thus vulnerable to foreign reads.
18+
fn thread_1(x: &mut u8) -> SendPtr {
19+
thread::yield_now(); // make the other thread go first
20+
SendPtr(x as *mut u8)
21+
}
22+
23+
// Second thread simply performs a read.
24+
fn thread_2(x: &u8) {
25+
let _val = *x;
26+
}
27+
28+
fn main() {
29+
let mut x = 0u8;
30+
let x_1 = unsafe { &mut *addr_of_mut!(x) };
31+
let xg = unsafe { &*addr_of_mut!(x) };
32+
33+
// The two threads are executed in parallel on aliasing pointers.
34+
// UB occurs if the read of thread_2 occurs while the protector of thread_1
35+
// is in place.
36+
let hf = thread::spawn(move || thread_1(x_1));
37+
let hg = thread::spawn(move || thread_2(xg));
38+
let SendPtr(p) = hf.join().unwrap();
39+
let () = hg.join().unwrap();
40+
41+
unsafe { *p = 1 }; //~ ERROR: /write access through .* is forbidden/
42+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
2+
--> $DIR/fragile-data-race.rs:LL:CC
3+
|
4+
LL | unsafe { *p = 1 };
5+
| ^^^^^^ write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
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+
= note: BACKTRACE:
9+
= note: inside `main` at $DIR/fragile-data-race.rs:LL:CC
10+
11+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
12+
13+
error: aborting due to previous error
14+
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
//@compile-flags: -Zmiri-tree-borrows
2+
3+
// Check that in the case of locations outside the range of a pointer,
4+
// protectors trigger if and only if the location has already been accessed
5+
fn main() {
6+
unsafe {
7+
let data = &mut [0u8, 1, 2, 3];
8+
let raw = data.as_mut_ptr();
9+
stuff(&mut *raw, raw);
10+
}
11+
}
12+
13+
unsafe fn stuff(x: &mut u8, y: *mut u8) {
14+
let xraw = x as *mut u8;
15+
// No issue here: location 1 is not accessed
16+
*y.add(1) = 42;
17+
// Still no issue: location 2 is not invalidated
18+
let _val = *xraw.add(2);
19+
// However protector triggers if location is both accessed and invalidated
20+
let _val = *xraw.add(3);
21+
*y.add(3) = 42; //~ ERROR: /write access through .* is forbidden/
22+
}
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden because it is a foreign tag for <TAG>, which would hence change from Reserved to Disabled, but <TAG> is protected
2+
--> $DIR/outside-range.rs:LL:CC
3+
|
4+
LL | *y.add(3) = 42;
5+
| ^^^^^^^^^^^^^^ write access through <TAG> is forbidden because it is a foreign tag for <TAG>, which would hence change from Reserved to Disabled, but <TAG> is protected
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+
= note: BACKTRACE:
9+
= note: inside `stuff` at $DIR/outside-range.rs:LL:CC
10+
note: inside `main`
11+
--> $DIR/outside-range.rs:LL:CC
12+
|
13+
LL | stuff(&mut *raw, raw);
14+
| ^^^^^^^^^^^^^^^^^^^^^
15+
16+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
17+
18+
error: aborting due to previous error
19+
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
//@compile-flags: -Zmiri-tree-borrows
2+
3+
// Read to local variable kills reborrows *and* raw pointers derived from them.
4+
// This test would succeed under Stacked Borrows.
5+
fn main() {
6+
unsafe {
7+
let mut root = 6u8;
8+
let mref = &mut root;
9+
let ptr = mref as *mut u8;
10+
*ptr = 0; // Write
11+
assert_eq!(root, 0); // Parent Read
12+
*ptr = 0; //~ ERROR: /write access through .* is forbidden/
13+
}
14+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
2+
--> $DIR/read-to-local.rs:LL:CC
3+
|
4+
LL | *ptr = 0;
5+
| ^^^^^^^^ write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
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+
= note: BACKTRACE:
9+
= note: inside `main` at $DIR/read-to-local.rs:LL:CC
10+
11+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
12+
13+
error: aborting due to previous error
14+
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
//@compile-flags: -Zmiri-tree-borrows -Zmiri-tag-gc=0
2+
3+
// Check how a Reserved with interior mutability
4+
// responds to a Foreign Write under a Protector
5+
#[path = "../../../utils/mod.rs"]
6+
mod utils;
7+
use utils::macros::*;
8+
9+
use std::cell::UnsafeCell;
10+
11+
fn main() {
12+
unsafe {
13+
let n = &mut UnsafeCell::new(0u8);
14+
name!(n.get(), "base");
15+
let x = &mut *(n as *mut UnsafeCell<_>);
16+
name!(x.get(), "x");
17+
let y = (&mut *n).get();
18+
name!(y);
19+
write_second(x, y);
20+
unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {
21+
let alloc_id = alloc_id!(x.get());
22+
name!(x.get(), "callee:x");
23+
name!(x.get()=>1, "caller:x");
24+
name!(y, "callee:y");
25+
name!(y, "caller:y");
26+
print_state!(alloc_id);
27+
// Right before the faulty Write, x is
28+
// - Reserved
29+
// - with interior mut
30+
// - Protected
31+
*y = 1; //~ ERROR: /write access through .* is forbidden/
32+
}
33+
}
34+
}
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
──────────────────────────────────────────────────────────────────────
2+
Warning: this tree is indicative only. Some tags may have been hidden.
3+
0.. 1
4+
| Re*| └─┬──<TAG=base>
5+
| Re*| ├─┬──<TAG=x>
6+
| Re*| │ └─┬──<TAG=caller:x>
7+
| Re*| │ └────<TAG=callee:x> Strongly protected
8+
| Re*| └────<TAG=y,callee:y,caller:y>
9+
──────────────────────────────────────────────────────────────────────
10+
error: Undefined Behavior: write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
11+
--> $DIR/cell-protected-write.rs:LL:CC
12+
|
13+
LL | *y = 1;
14+
| ^^^^^^ write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
15+
|
16+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
17+
= note: BACKTRACE:
18+
= note: inside `main::write_second` at $DIR/cell-protected-write.rs:LL:CC
19+
note: inside `main`
20+
--> $DIR/cell-protected-write.rs:LL:CC
21+
|
22+
LL | write_second(x, y);
23+
| ^^^^^^^^^^^^^^^^^^
24+
25+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
26+
27+
error: aborting due to previous error
28+
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
//@compile-flags: -Zmiri-tree-borrows -Zmiri-tag-gc=0
2+
3+
#[path = "../../../utils/mod.rs"]
4+
mod utils;
5+
use utils::macros::*;
6+
7+
// Check how a Reserved without interior mutability responds to a Foreign
8+
// Write when under a protector
9+
fn main() {
10+
unsafe {
11+
let n = &mut 0u8;
12+
name!(n);
13+
let x = &mut *(n as *mut _);
14+
name!(x);
15+
let y = (&mut *n) as *mut _;
16+
name!(y);
17+
write_second(x, y);
18+
unsafe fn write_second(x: &mut u8, y: *mut u8) {
19+
let alloc_id = alloc_id!(x);
20+
name!(x, "callee:x");
21+
name!(x=>1, "caller:x");
22+
name!(y, "callee:y");
23+
name!(y, "caller:y");
24+
print_state!(alloc_id);
25+
// Right before the faulty Write, x is
26+
// - Reserved
27+
// - Protected
28+
// The Write turns it Disabled
29+
*y = 0; //~ ERROR: /write access through .* is forbidden/
30+
}
31+
}
32+
}
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
──────────────────────────────────────────────────────────────────────
2+
Warning: this tree is indicative only. Some tags may have been hidden.
3+
0.. 1
4+
| Res| └─┬──<TAG=n>
5+
| Res| ├─┬──<TAG=x>
6+
| Res| │ └─┬──<TAG=caller:x>
7+
| Res| │ └────<TAG=callee:x> Strongly protected
8+
| Res| └────<TAG=y,callee:y,caller:y>
9+
──────────────────────────────────────────────────────────────────────
10+
error: Undefined Behavior: write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
11+
--> $DIR/int-protected-write.rs:LL:CC
12+
|
13+
LL | *y = 0;
14+
| ^^^^^^ write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
15+
|
16+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
17+
= note: BACKTRACE:
18+
= note: inside `main::write_second` at $DIR/int-protected-write.rs:LL:CC
19+
note: inside `main`
20+
--> $DIR/int-protected-write.rs:LL:CC
21+
|
22+
LL | write_second(x, y);
23+
| ^^^^^^^^^^^^^^^^^^
24+
25+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
26+
27+
error: aborting due to previous error
28+
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
//! Make sure that a retag acts like a read for the data race model.
2+
//! This is a retag/write race condition.
3+
//!
4+
//! This test is sensitive to the exact schedule so we disable preemption.
5+
//@compile-flags: -Zmiri-tree-borrows -Zmiri-preemption-rate=0
6+
#[derive(Copy, Clone)]
7+
struct SendPtr(*mut u8);
8+
9+
unsafe impl Send for SendPtr {}
10+
11+
unsafe fn thread_1(SendPtr(p): SendPtr) {
12+
let _r = &*p;
13+
}
14+
15+
unsafe fn thread_2(SendPtr(p): SendPtr) {
16+
*p = 5; //~ ERROR: Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>`
17+
}
18+
19+
fn main() {
20+
let mut x = 0;
21+
let p = std::ptr::addr_of_mut!(x);
22+
let p = SendPtr(p);
23+
24+
let t1 = std::thread::spawn(move || unsafe { thread_1(p) });
25+
let t2 = std::thread::spawn(move || unsafe { thread_2(p) });
26+
let _ = t1.join();
27+
let _ = t2.join();
28+
}
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
error: Undefined Behavior: Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
2+
--> $DIR/retag-data-race.rs:LL:CC
3+
|
4+
LL | *p = 5;
5+
| ^^^^^^ Data race detected between (1) Read on thread `<unnamed>` and (2) Write on thread `<unnamed>` at ALLOC. (2) just happened here
6+
|
7+
help: and (1) occurred earlier here
8+
--> $DIR/retag-data-race.rs:LL:CC
9+
|
10+
LL | let _r = &*p;
11+
| ^^^
12+
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
13+
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
14+
= note: BACKTRACE (of the first span):
15+
= note: inside `thread_2` at $DIR/retag-data-race.rs:LL:CC
16+
note: inside closure
17+
--> $DIR/retag-data-race.rs:LL:CC
18+
|
19+
LL | let t2 = std::thread::spawn(move || unsafe { thread_2(p) });
20+
| ^^^^^^^^^^^
21+
22+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
23+
24+
error: aborting due to previous error
25+
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
//@compile-flags: -Zmiri-tree-borrows
2+
3+
// We invalidate a reference during a 2-phase borrow by doing a Foreign
4+
// Write in between the initial reborrow and function entry. UB occurs
5+
// on function entry when reborrow from a Disabled fails.
6+
// This test would pass under Stacked Borrows, but Tree Borrows
7+
// is more strict on 2-phase borrows.
8+
9+
struct Foo(u64);
10+
impl Foo {
11+
#[rustfmt::skip] // rustfmt is wrong about which line contains an error
12+
fn add(&mut self, n: u64) -> u64 { //~ ERROR: /read access through .* is forbidden/
13+
self.0 + n
14+
}
15+
}
16+
17+
pub fn main() {
18+
let mut f = Foo(0);
19+
let inner = &mut f.0 as *mut u64;
20+
let _res = f.add(unsafe {
21+
let n = f.0;
22+
// This is the access at fault, but it's not immediately apparent because
23+
// the reference that got invalidated is not under a Protector.
24+
*inner = 42;
25+
n
26+
});
27+
}

0 commit comments

Comments
 (0)