Skip to content

Make unused states of Reserved unrepresentable #3754

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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()>
──────────────────────────────────────────────────