user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Second byte is not involved in the example; use a Cell<()> instead

Browse source
This commit is contained in:
Neven Villani 2024-07-10 14:32:02 +02:00
parent 22996ad073
commit 68aed4a5ce
No known key found for this signature in database
GPG key ID: 00E765FA7F4F2EDE
3 changed files with 19 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.rs
View file

@ -41,10 +41,10 @@ macro_rules! synchronized {
}
fn main() {
// For this example it is important that we have at least two bytes
// because lazyness is involved.
let mut data = [0u8; 2];
let ptr = SendPtr(std::ptr::addr_of_mut!(data[0]));
// The conflict occurs one one single location but the example involves
// lazily initialized permissions.
let mut data = 0u8;
let ptr = SendPtr(std::ptr::addr_of_mut!(data));
let barrier = Arc::new(Barrier::new(2));
let bx = Arc::clone(&barrier);
let by = Arc::clone(&barrier);
@ -84,17 +84,20 @@ fn main() {
let ptr = ptr;
synchronized!(b, "retag x (&mut, protect)");
synchronized!(b, "[lazy] retag y (&mut, protect, IM)");
fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
synchronized!(b, "spurious write x");
synchronized!(b, "ret y");
y as *mut Cell<u8> as *mut u8
// `y` is not retagged for any bytes, so the pointer we return
// has its permission lazily initialized.
y as *mut Cell<()> as *mut u8
}
// Currently `ptr` points to `data[0]`. We retag it for `data[1]`
// then use it for `data[0]` where its initialization has been deferred.
let y = inner(unsafe { &mut *(ptr.0 as *mut Cell<u8>).wrapping_add(1) }, b.clone());
// Currently `ptr` points to `data`.
// We do a zero-sized retag so that its permission is lazy.
let y_zst = unsafe { &mut *(ptr.0 as *mut Cell<()>) };
let y = inner(y_zst, b.clone());
synchronized!(b, "ret x");
synchronized!(b, "write y");
unsafe { *y.wrapping_sub(1) = 13 } //~ERROR: /write access through .* is forbidden/
unsafe { *y = 13 } //~ERROR: /write access through .* is forbidden/
synchronized!(b, "end");
});

6
src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.with.stderr
View file

@ -15,15 +15,15 @@ Thread 2 executing: write y
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | unsafe { *y.wrapping_sub(1) = 13 }
| ^^^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
LL | unsafe { *y = 13 }
| ^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> has state Disabled which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
LL | fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
| ^
help: the accessed tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x1]
--> $DIR/reservedim_spurious_write.rs:LL:CC

6
src/tools/miri/tests/fail/tree_borrows/reservedim_spurious_write.without.stderr
View file

@ -15,15 +15,15 @@ Thread 2 executing: write y
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | unsafe { *y.wrapping_sub(1) = 13 }
| ^^^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
LL | unsafe { *y = 13 }
| ^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> has state Disabled which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
LL | fn inner(y: &mut Cell<()>, b: IdxBarrier) -> *mut u8 {
| ^
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
--> $DIR/reservedim_spurious_write.rs:LL:CC