Skip to content

Commit 68aed4a

Browse files
committed
Second byte is not involved in the example; use a Cell<()> instead
1 parent 22996ad commit 68aed4a

File tree

3 files changed

+19
-16
lines changed

3 files changed

+19
-16
lines changed

src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -41,10 +41,10 @@ macro_rules! synchronized {
4141
}
4242

4343
fn main() {
44-
// For this example it is important that we have at least two bytes
45-
// because lazyness is involved.
46-
let mut data = [0u8; 2];
47-
let ptr = SendPtr(std::ptr::addr_of_mut!(data[0]));
44+
// The conflict occurs one one single location but the example involves
45+
// lazily initialized permissions.
46+
let mut data = 0u8;
47+
let ptr = SendPtr(std::ptr::addr_of_mut!(data));
4848
let barrier = Arc::new(Barrier::new(2));
4949
let bx = Arc::clone(&barrier);
5050
let by = Arc::clone(&barrier);
@@ -84,17 +84,20 @@ fn main() {
8484
let ptr = ptr;
8585
synchronized!(b, "retag x (&mut, protect)");
8686
synchronized!(b, "[lazy] retag y (&mut, protect, IM)");
87-
fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
87+
fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
8888
synchronized!(b, "spurious write x");
8989
synchronized!(b, "ret y");
90-
y as *mut Cell<u8> as *mut u8
90+
// `y` is not retagged for any bytes, so the pointer we return
91+
// has its permission lazily initialized.
92+
y as *mut Cell<()> as *mut u8
9193
}
92-
// Currently `ptr` points to `data[0]`. We retag it for `data[1]`
93-
// then use it for `data[0]` where its initialization has been deferred.
94-
let y = inner(unsafe { &mut *(ptr.0 as *mut Cell<u8>).wrapping_add(1) }, b.clone());
94+
// Currently `ptr` points to `data`.
95+
// We do a zero-sized retag so that its permission is lazy.
96+
let y_zst = unsafe { &mut *(ptr.0 as *mut Cell<()>) };
97+
let y = inner(y_zst, b.clone());
9598
synchronized!(b, "ret x");
9699
synchronized!(b, "write y");
97-
unsafe { *y.wrapping_sub(1) = 13 } //~ERROR: /write access through .* is forbidden/
100+
unsafe { *y = 13 } //~ERROR: /write access through .* is forbidden/
98101
synchronized!(b, "end");
99102
});
100103

src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,15 +15,15 @@ Thread 2 executing: write y
1515
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
1616
--> $DIR/reservedim_spurious_write.rs:LL:CC
1717
|
18-
LL | unsafe { *y.wrapping_sub(1) = 13 }
19-
| ^^^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
18+
LL | unsafe { *y = 13 }
19+
| ^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
2020
|
2121
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
2222
= help: the accessed tag <TAG> has state Disabled which forbids this child write access
2323
help: the accessed tag <TAG> was created here, in the initial state Reserved
2424
--> $DIR/reservedim_spurious_write.rs:LL:CC
2525
|
26-
LL | fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
26+
LL | fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
2727
| ^
2828
help: the accessed tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x1]
2929
--> $DIR/reservedim_spurious_write.rs:LL:CC

src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,15 +15,15 @@ Thread 2 executing: write y
1515
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
1616
--> $DIR/reservedim_spurious_write.rs:LL:CC
1717
|
18-
LL | unsafe { *y.wrapping_sub(1) = 13 }
19-
| ^^^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
18+
LL | unsafe { *y = 13 }
19+
| ^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
2020
|
2121
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
2222
= help: the accessed tag <TAG> has state Disabled which forbids this child write access
2323
help: the accessed tag <TAG> was created here, in the initial state Reserved
2424
--> $DIR/reservedim_spurious_write.rs:LL:CC
2525
|
26-
LL | fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
26+
LL | fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
2727
| ^
2828
help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag
2929
--> $DIR/reservedim_spurious_write.rs:LL:CC

0 commit comments

Comments
 (0)