Skip to content

Commit

Permalink
Auto merge of #3754 - Vanille-N:master, r=RalfJung
Browse files Browse the repository at this point in the history
Make unused states of Reserved unrepresentable

In the [previous TB update](#3742) we discovered that the existence of `Reserved + !ty_is_freeze + protected` is undesirable.

This has the side effect of making `Reserved { conflicted: true, ty_is_freeze: false }` unreachable.
As such it is desirable that this state would also be unrepresentable.

This PR eliminates the unused configuration by changing
```rs
enum PermissionPriv {
    Reserved { ty_is_freeze: bool, conflicted: bool },
    ...
}
```
into
```rs
enum PermissionPriv {
    ReservedFrz { conflicted: bool },
    ReservedIM,
    ...
}
```
but this is not the only solution and `Reserved(Activable | Conflicted | InteriorMut)` could be discussed.
In addition to making the unreachable state not representable anymore, this change has the nice side effect of enabling `foreign_read` to no longer depend explicitly on the `protected` flag.

Currently waiting for
- `@JoJoDeveloping` to confirm that this is the same representation of `Reserved` as what is being implemented in simuliris,
- `@RalfJung` to approve that this does not introduce too much overhead in the trusted codebase.
  • Loading branch information
bors committed Aug 16, 2024
2 parents cd5d255 + ae183fd commit eeb6e96
Show file tree
Hide file tree
Showing 13 changed files with 200 additions and 134 deletions.
25 changes: 12 additions & 13 deletions src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,6 @@
use rustc_middle::{
mir::{Mutability, RetagKind},
ty::{
self,
layout::{HasParamEnv, HasTyCtxt},
Ty,
},
ty::{self, layout::HasParamEnv, Ty},
};
use rustc_span::def_id::DefId;
use rustc_target::abi::{Abi, Size};
Expand Down Expand Up @@ -146,10 +142,9 @@ impl<'tcx> NewPermission {
// 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: protected references are always considered
// "freeze".
// "freeze" in their reservation phase.
let initial_state = match mutability {
Mutability::Mut if ty_is_unpin =>
Permission::new_reserved(ty_is_freeze || is_protected),
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
Expand All @@ -176,10 +171,12 @@ impl<'tcx> NewPermission {
// Regular `Unpin` box, give it `noalias` but only a weak protector
// because it is valid to deallocate it within the function.
let ty_is_freeze = ty.is_freeze(*cx.tcx, cx.param_env());
let protected = kind == RetagKind::FnEntry;
let initial_state = Permission::new_reserved(ty_is_freeze, protected);
Self {
zero_size,
initial_state: Permission::new_reserved(ty_is_freeze),
protector: (kind == RetagKind::FnEntry).then_some(ProtectorKind::WeakProtector),
initial_state,
protector: protected.then_some(ProtectorKind::WeakProtector),
}
})
}
Expand Down Expand Up @@ -521,11 +518,13 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
fn tb_protect_place(&mut self, place: &MPlaceTy<'tcx>) -> InterpResult<'tcx, MPlaceTy<'tcx>> {
let this = self.eval_context_mut();

// Note: if we were to inline `new_reserved` below we would find out that
// `ty_is_freeze` is eventually unused because it appears in a `ty_is_freeze || true`.
// We are nevertheless including it here for clarity.
let ty_is_freeze = place.layout.ty.is_freeze(*this.tcx, this.param_env());
// Retag it. With protection! That is the entire point.
let new_perm = NewPermission {
initial_state: Permission::new_reserved(
place.layout.ty.is_freeze(this.tcx(), this.param_env()),
),
initial_state: Permission::new_reserved(ty_is_freeze, /* protected */ true),
zero_size: false,
protector: Some(ProtectorKind::StrongProtector),
};
Expand Down
182 changes: 113 additions & 69 deletions src/borrow_tracker/tree_borrows/perms.rs

Large diffs are not rendered by default.

35 changes: 29 additions & 6 deletions src/borrow_tracker/tree_borrows/tree/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,15 @@ impl Exhaustive for LocationState {
}
}

impl LocationState {
/// Ensure that the current internal state can exist at the same time as a protector.
/// In practice this only eliminates `ReservedIM` that is never used in the presence
/// of a protector (we instead emit `ReservedFrz` on retag).
pub fn compatible_with_protector(&self) -> bool {
self.permission.compatible_with_protector()
}
}

#[test]
#[rustfmt::skip]
// Exhaustive check that for any starting configuration loc,
Expand All @@ -30,6 +39,9 @@ fn all_read_accesses_commute() {
// so the two read accesses occur under the same protector.
for protected in bool::exhaustive() {
for loc in LocationState::exhaustive() {
if protected {
precondition!(loc.compatible_with_protector());
}
// Apply 1 then 2. Failure here means that there is UB in the source
// and we skip the check in the target.
let mut loc12 = loc;
Expand Down Expand Up @@ -61,8 +73,8 @@ fn protected_enforces_noalias() {
// We want to check pairs of accesses where one is foreign and one is not.
precondition!(rel1.is_foreign() != rel2.is_foreign());
for [kind1, kind2] in <[AccessKind; 2]>::exhaustive() {
for mut state in LocationState::exhaustive() {
let protected = true;
let protected = true;
for mut state in LocationState::exhaustive().filter(|s| s.compatible_with_protector()) {
precondition!(state.perform_access(kind1, rel1, protected).is_ok());
precondition!(state.perform_access(kind2, rel2, protected).is_ok());
// If these were both allowed, it must have been two reads.
Expand Down Expand Up @@ -387,6 +399,9 @@ mod spurious_read {

fn retag_y(self, new_y: LocStateProt) -> Result<Self, ()> {
assert!(new_y.is_initial());
if new_y.prot && !new_y.state.compatible_with_protector() {
return Err(());
}
// `xy_rel` changes to "mutually foreign" now: `y` can no longer be a parent of `x`.
Self { y: new_y, xy_rel: RelPosXY::MutuallyForeign, ..self }
.read_if_initialized(PtrSelector::Y)
Expand Down Expand Up @@ -511,7 +526,7 @@ mod spurious_read {
}

#[test]
// `Reserved(aliased=false)` and `Reserved(aliased=true)` are properly indistinguishable
// `Reserved { conflicted: false }` and `Reserved { conflicted: true }` are properly indistinguishable
// under the conditions where we want to insert a spurious read.
fn reserved_aliased_protected_indistinguishable() {
let source = LocStateProtPair {
Expand All @@ -521,14 +536,16 @@ mod spurious_read {
prot: true,
},
y: LocStateProt {
state: LocationState::new_uninit(Permission::new_reserved(false)),
state: LocationState::new_uninit(Permission::new_reserved(
/* freeze */ true, /* protected */ true,
)),
prot: true,
},
};
let acc = TestAccess { ptr: PtrSelector::X, kind: AccessKind::Read };
let target = source.clone().perform_test_access(&acc).unwrap();
assert!(source.y.state.permission.is_reserved_with_conflicted(false));
assert!(target.y.state.permission.is_reserved_with_conflicted(true));
assert!(source.y.state.permission.is_reserved_frz_with_conflicted(false));
assert!(target.y.state.permission.is_reserved_frz_with_conflicted(true));
assert!(!source.distinguishable::<(), ()>(&target))
}

Expand Down Expand Up @@ -563,7 +580,13 @@ mod spurious_read {
precondition!(x_retag_perm.initialized);
// And `x` just got retagged, so it must be initial.
precondition!(x_retag_perm.permission.is_initial());
// As stated earlier, `x` is always protected in the patterns we consider here.
precondition!(x_retag_perm.compatible_with_protector());
for y_protected in bool::exhaustive() {
// Finally `y` that is optionally protected must have a compatible permission.
if y_protected {
precondition!(y_current_perm.compatible_with_protector());
}
v.push(Pattern { xy_rel, x_retag_perm, y_current_perm, y_protected });
}
}
Expand Down
10 changes: 5 additions & 5 deletions tests/fail/tree_borrows/reserved/cell-protected-write.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| RsM | └─┬──<TAG=base>
| RsM | ├─┬──<TAG=x>
| RsM | │ └─┬──<TAG=caller:x>
| Rs | │ └────<TAG=callee:x> Strongly protected
| RsM | └────<TAG=y, callee:y, caller:y>
| ReIM| └─┬──<TAG=base>
| ReIM| ├─┬──<TAG=x>
| ReIM| │ └─┬──<TAG=caller:x>
| Res | │ └────<TAG=callee:x> Strongly protected
| ReIM| └────<TAG=y, callee:y, caller:y>
──────────────────────────────────────────────────
error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
--> $DIR/cell-protected-write.rs:LL:CC
Expand Down
10 changes: 5 additions & 5 deletions tests/fail/tree_borrows/reserved/int-protected-write.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=n>
| Rs | ├─┬──<TAG=x>
| Rs | │ └─┬──<TAG=caller:x>
| Rs | │ └────<TAG=callee:x> Strongly protected
| Rs | └────<TAG=y, callee:y, caller:y>
| Res | └─┬──<TAG=n>
| Res | ├─┬──<TAG=x>
| Res | │ └─┬──<TAG=caller:x>
| Res | │ └────<TAG=callee:x> Strongly protected
| Res | └────<TAG=y, callee:y, caller:y>
──────────────────────────────────────────────────
error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
--> $DIR/int-protected-write.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/pass/tree_borrows/cell-alternate-writes.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| RsM | └────<TAG=data, x, y>
| ReIM| └────<TAG=data, x, y>
──────────────────────────────────────────────────
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
Expand Down
22 changes: 11 additions & 11 deletions tests/pass/tree_borrows/end-of-protector.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,27 +2,27 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=data>
| Rs | └────<TAG=x>
| Res | └─┬──<TAG=data>
| Res | └────<TAG=x>
──────────────────────────────────────────────────
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=data>
| Rs | └─┬──<TAG=x>
| Rs | └─┬──<TAG=caller:x>
| Rs | └────<TAG=callee:x> Strongly protected
| Res | └─┬──<TAG=data>
| Res | └─┬──<TAG=x>
| Res | └─┬──<TAG=caller:x>
| Res | └────<TAG=callee:x> Strongly protected
──────────────────────────────────────────────────
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=data>
| Rs | ├─┬──<TAG=x>
| Rs | │ └─┬──<TAG=caller:x>
| Rs | │ └────<TAG=callee:x>
| Rs | └────<TAG=y>
| Res | └─┬──<TAG=data>
| Res | ├─┬──<TAG=x>
| Res | │ └─┬──<TAG=caller:x>
| Res | │ └────<TAG=callee:x>
| Res | └────<TAG=y>
──────────────────────────────────────────────────
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
Expand Down
2 changes: 1 addition & 1 deletion tests/pass/tree_borrows/formatting.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1.. 2.. 10.. 11.. 100.. 101..1000..1001..1024
| Act | Act | Act | Act | Act | Act | Act | Act | Act | └─┬──<TAG=root of the allocation>
| Rs | Act | Rs | Act | Rs | Act | Rs | Act | Rs | └─┬──<TAG=data, data>
| Res | Act | Res | Act | Res | Act | Res | Act | Res | └─┬──<TAG=data, data>
|-----| Act |-----|?Dis |-----|?Dis |-----|?Dis |-----| ├────<TAG=data[1]>
|-----|-----|-----| Act |-----|?Dis |-----|?Dis |-----| ├────<TAG=data[10]>
|-----|-----|-----|-----|-----| Frz |-----|?Dis |-----| ├────<TAG=data[100]>
Expand Down
2 changes: 1 addition & 1 deletion tests/pass/tree_borrows/reborrow-is-read.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -11,5 +11,5 @@ Warning: this tree is indicative only. Some tags may have been hidden.
| Act | └─┬──<TAG=root of the allocation>
| Act | └─┬──<TAG=parent>
| Frz | ├────<TAG=x>
| Rs | └────<TAG=y>
| Res | └────<TAG=y>
──────────────────────────────────────────────────
34 changes: 17 additions & 17 deletions tests/pass/tree_borrows/reserved.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -3,49 +3,49 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| RsM | └─┬──<TAG=base>
| RsM | ├─┬──<TAG=x>
| RsM | │ └─┬──<TAG=caller:x>
| RsC | │ └────<TAG=callee:x>
| RsM | └────<TAG=y, caller:y, callee:y>
| ReIM| └─┬──<TAG=base>
| ReIM| ├─┬──<TAG=x>
| ReIM| │ └─┬──<TAG=caller:x>
| ResC| │ └────<TAG=callee:x>
| ReIM| └────<TAG=y, caller:y, callee:y>
──────────────────────────────────────────────────
[interior mut] Foreign Read: Re* -> Re*
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 8
| Act | └─┬──<TAG=root of the allocation>
| RsM | └─┬──<TAG=base>
| RsM | ├────<TAG=x>
| RsM | └────<TAG=y>
| ReIM| └─┬──<TAG=base>
| ReIM| ├────<TAG=x>
| ReIM| └────<TAG=y>
──────────────────────────────────────────────────
[interior mut] Foreign Write: Re* -> Re*
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 8
| Act | └─┬──<TAG=root of the allocation>
| Act | └─┬──<TAG=base>
| RsM | ├────<TAG=x>
| ReIM| ├────<TAG=x>
| Act | └────<TAG=y>
──────────────────────────────────────────────────
[protected] Foreign Read: Res -> Frz
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=base>
| Rs | ├─┬──<TAG=x>
| Rs | │ └─┬──<TAG=caller:x>
| RsC | │ └────<TAG=callee:x>
| Rs | └────<TAG=y, caller:y, callee:y>
| Res | └─┬──<TAG=base>
| Res | ├─┬──<TAG=x>
| Res | │ └─┬──<TAG=caller:x>
| ResC| │ └────<TAG=callee:x>
| Res | └────<TAG=y, caller:y, callee:y>
──────────────────────────────────────────────────
[] Foreign Read: Res -> Res
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=base>
| Rs | ├────<TAG=x>
| Rs | └────<TAG=y>
| Res | └─┬──<TAG=base>
| Res | ├────<TAG=x>
| Res | └────<TAG=y>
──────────────────────────────────────────────────
[] Foreign Write: Res -> Dis
──────────────────────────────────────────────────
Expand Down
4 changes: 2 additions & 2 deletions tests/pass/tree_borrows/unique.default.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=base>
| Rs | └────<TAG=raw, uniq, uniq>
| Res | └─┬──<TAG=base>
| Res | └────<TAG=raw, uniq, uniq>
──────────────────────────────────────────────────
──────────────────────────────────────────────────
Warning: this tree is indicative only. Some tags may have been hidden.
Expand Down
4 changes: 2 additions & 2 deletions tests/pass/tree_borrows/unique.uniq.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 1
| Act | └─┬──<TAG=root of the allocation>
| Rs | └─┬──<TAG=base>
| Rs | └─┬──<TAG=raw>
| Res | └─┬──<TAG=base>
| Res | └─┬──<TAG=raw>
|-----| └────<TAG=uniq, uniq>
──────────────────────────────────────────────────
──────────────────────────────────────────────────
Expand Down
2 changes: 1 addition & 1 deletion tests/pass/tree_borrows/vec_unique.default.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
Warning: this tree is indicative only. Some tags may have been hidden.
0.. 2
| Act | └─┬──<TAG=root of the allocation>
| Rs | └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
| Res | └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
──────────────────────────────────────────────────

0 comments on commit eeb6e96

Please sign in to comment.