Implement fix for reservedim_spurious_write: ignore IM on protected

This commit is contained in:
Neven Villani 2024-07-09 14:36:46 +02:00
parent 22364f86ae
commit 2de6e7f3a6
No known key found for this signature in database
GPG key ID: 00E765FA7F4F2EDE
6 changed files with 59 additions and 7 deletions

View file

@ -141,8 +141,14 @@ impl<'tcx> NewPermission {
) -> Option<Self> {
let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.param_env());
let ty_is_unpin = pointee.is_unpin(*cx.tcx, cx.param_env());
let is_protected = kind == RetagKind::FnEntry;
// As demonstrated by `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
// interior mutability and protectors interact poorly.
// To eliminate the case of Protected Reserved IM we override interior mutability
// in the case of a protected reference.
let initial_state = match mutability {
Mutability::Mut if ty_is_unpin => Permission::new_reserved(ty_is_freeze),
Mutability::Mut if ty_is_unpin =>
Permission::new_reserved(ty_is_freeze || is_protected),
Mutability::Not if ty_is_freeze => Permission::new_frozen(),
// Raw pointers never enter this function so they are not handled.
// However raw pointers are not the only pointers that take the parent
@ -151,7 +157,7 @@ impl<'tcx> NewPermission {
_ => return None,
};
let protector = (kind == RetagKind::FnEntry).then_some(ProtectorKind::StrongProtector);
let protector = is_protected.then_some(ProtectorKind::StrongProtector);
Some(Self { zero_size: false, initial_state, protector })
}

View file

@ -22,6 +22,11 @@ enum PermissionPriv {
/// - foreign-read then child-write is UB due to `conflicted`,
/// - child-write then foreign-read is UB since child-write will activate and then
/// foreign-read disables a protected `Active`, which is UB.
///
/// Note: since the discovery of `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
/// `ty_is_freeze` does not strictly mean that the type has no interior mutability,
/// it could be an interior mutable type that lost its interior mutability privileges
/// when retagged with a protector.
Reserved { ty_is_freeze: bool, conflicted: bool },
/// represents: a unique pointer;
/// allows: child reads, child writes;

View file

@ -5,7 +5,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
| RsM | └─┬──<TAG=base>
| RsM | ├─┬──<TAG=x>
| RsM | │ └─┬──<TAG=caller:x>
| RsM | │ └────<TAG=callee:x> Strongly protected
| Rs | │ └────<TAG=callee:x> Strongly protected
| RsM | └────<TAG=y, callee:y, caller:y>
──────────────────────────────────────────────────
error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
@ -16,14 +16,14 @@ LL | *y = 1;
|
= 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> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved (interior mutable)) to become Disabled
= help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/cell-protected-write.rs:LL:CC
|
LL | let y = (&mut *n).get();
| ^^^^^^^^^
help: the protected tag <TAG> was created here, in the initial state Reserved (interior mutable)
help: the protected tag <TAG> was created here, in the initial state Reserved
--> $DIR/cell-protected-write.rs:LL:CC
|
LL | unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {

View file

@ -100,7 +100,7 @@ fn example(spurious: bool) {
let y = inner(unsafe { &mut *(ptr.0 as *mut Cell<u8>).wrapping_add(1) }, b.clone());
synchronized!(b, "ret x");
synchronized!(b, "write y");
unsafe { *y.wrapping_sub(1) = 13 }
unsafe { *y.wrapping_sub(1) = 13 } //~ERROR: /write access through .* is forbidden/
synchronized!(b, "end");
});

View file

@ -0,0 +1,41 @@
Without spurious write
Thread 1 executing: start
Thread 2 executing: start
Thread 2 executing: retag x (&mut, protect)
Thread 1 executing: retag x (&mut, protect)
Thread 1 executing: [lazy] retag y (&mut, protect, IM)
Thread 2 executing: [lazy] retag y (&mut, protect, IM)
Thread 2 executing: spurious write x
Thread 1 executing: spurious write x (skipped)
Thread 1 executing: ret y
Thread 2 executing: ret y
Thread 2 executing: ret x
Thread 1 executing: ret x
Thread 1 executing: write y
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
|
= 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 {
| ^
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
|
LL | }
| ^
= help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
= note: inside closure at $DIR/reservedim_spurious_write.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to 1 previous error

View file

@ -6,7 +6,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
| RsM | └─┬──<TAG=base>
| RsM | ├─┬──<TAG=x>
| RsM | │ └─┬──<TAG=caller:x>
| RsCM| │ └────<TAG=callee:x>
| RsC | │ └────<TAG=callee:x>
| RsM | └────<TAG=y, caller:y, callee:y>
──────────────────────────────────────────────────
[interior mut] Foreign Read: Re* -> Re*