Auto merge of #3754 - Vanille-N:master, r=RalfJung
Make unused states of Reserved unrepresentable In the [previous TB update](https://github.com/rust-lang/miri/pull/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.
This commit is contained in:
commit
1a51dd9247
13 changed files with 200 additions and 134 deletions
|
@ -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};
|
||||
|
@ -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
|
||||
|
@ -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),
|
||||
}
|
||||
})
|
||||
}
|
||||
|
@ -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),
|
||||
};
|
||||
|
|
|
@ -8,10 +8,16 @@ use crate::AccessKind;
|
|||
/// The activation states of a pointer.
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
||||
enum PermissionPriv {
|
||||
/// represents: a local reference that has not yet been written to;
|
||||
/// allows: child reads, foreign reads, foreign writes if type is freeze;
|
||||
/// represents: a local mutable reference that has not yet been written to;
|
||||
/// allows: child reads, foreign reads;
|
||||
/// affected by: child writes (becomes Active),
|
||||
/// rejects: foreign writes (Disabled, except if type is not freeze).
|
||||
/// rejects: foreign writes (Disabled).
|
||||
///
|
||||
/// `ReservedFrz` is mostly for types that are `Freeze` (no interior mutability).
|
||||
/// If the type has interior mutability, see `ReservedIM` instead.
|
||||
/// (Note: since the discovery of `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
|
||||
/// we also use `ReservedFreeze` for mutable references that were retagged with a protector
|
||||
/// independently of interior mutability)
|
||||
///
|
||||
/// special case: behaves differently when protected, which is where `conflicted`
|
||||
/// is relevant
|
||||
|
@ -22,12 +28,12 @@ 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 },
|
||||
ReservedFrz { conflicted: bool },
|
||||
/// Alternative version of `ReservedFrz` made for types with interior mutability.
|
||||
/// allows: child reads, foreign reads, foreign writes (extra);
|
||||
/// affected by: child writes (becomes Active);
|
||||
/// rejects: nothing.
|
||||
ReservedIM,
|
||||
/// represents: a unique pointer;
|
||||
/// allows: child reads, child writes;
|
||||
/// rejects: foreign reads (Frozen), foreign writes (Disabled).
|
||||
|
@ -59,17 +65,14 @@ impl PartialOrd for PermissionPriv {
|
|||
(_, Frozen) => Less,
|
||||
(Active, _) => Greater,
|
||||
(_, Active) => Less,
|
||||
(
|
||||
Reserved { ty_is_freeze: f1, conflicted: c1 },
|
||||
Reserved { ty_is_freeze: f2, conflicted: c2 },
|
||||
) => {
|
||||
// No transition ever changes `ty_is_freeze`.
|
||||
if f1 != f2 {
|
||||
return None;
|
||||
}
|
||||
(ReservedIM, ReservedIM) => Equal,
|
||||
(ReservedFrz { conflicted: c1 }, ReservedFrz { conflicted: c2 }) => {
|
||||
// `bool` is ordered such that `false <= true`, so this works as intended.
|
||||
c1.cmp(c2)
|
||||
}
|
||||
// Versions of `Reserved` with different interior mutability are incomparable with each
|
||||
// other.
|
||||
(ReservedIM, ReservedFrz { .. }) | (ReservedFrz { .. }, ReservedIM) => return None,
|
||||
})
|
||||
}
|
||||
}
|
||||
|
@ -77,7 +80,12 @@ impl PartialOrd for PermissionPriv {
|
|||
impl PermissionPriv {
|
||||
/// Check if `self` can be the initial state of a pointer.
|
||||
fn is_initial(&self) -> bool {
|
||||
matches!(self, Reserved { conflicted: false, .. } | Frozen)
|
||||
matches!(self, ReservedFrz { conflicted: false } | Frozen | ReservedIM)
|
||||
}
|
||||
|
||||
/// Reject `ReservedIM` that cannot exist in the presence of a protector.
|
||||
fn compatible_with_protector(&self) -> bool {
|
||||
!matches!(self, ReservedIM)
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -93,7 +101,7 @@ mod transition {
|
|||
Disabled => return None,
|
||||
// The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
|
||||
// accesses, since the data is not being mutated. Hence the `{ .. }`.
|
||||
readable @ (Reserved { .. } | Active | Frozen) => readable,
|
||||
readable @ (ReservedFrz { .. } | ReservedIM | Active | Frozen) => readable,
|
||||
})
|
||||
}
|
||||
|
||||
|
@ -109,11 +117,16 @@ mod transition {
|
|||
|
||||
// Someone else read. To make sure we won't write before function exit,
|
||||
// we set the "conflicted" flag, which will disallow writes while we are protected.
|
||||
Reserved { ty_is_freeze, .. } if protected =>
|
||||
Reserved { ty_is_freeze, conflicted: true },
|
||||
ReservedFrz { .. } if protected => ReservedFrz { conflicted: true },
|
||||
// Before activation and without protectors, foreign reads are fine.
|
||||
// That's the entire point of 2-phase borrows.
|
||||
res @ Reserved { .. } => res,
|
||||
res @ (ReservedFrz { .. } | ReservedIM) => {
|
||||
// Even though we haven't checked `ReservedIM if protected` separately,
|
||||
// it is a state that cannot occur because under a protector we only
|
||||
// create `ReservedFrz` never `ReservedIM`.
|
||||
assert!(!protected);
|
||||
res
|
||||
}
|
||||
Active =>
|
||||
if protected {
|
||||
// We wrote, someone else reads -- that's bad.
|
||||
|
@ -134,10 +147,10 @@ mod transition {
|
|||
// If the `conflicted` flag is set, then there was a foreign read during
|
||||
// the function call that is still ongoing (still `protected`),
|
||||
// this is UB (`noalias` violation).
|
||||
Reserved { conflicted: true, .. } if protected => return None,
|
||||
ReservedFrz { conflicted: true } if protected => return None,
|
||||
// A write always activates the 2-phase borrow, even with interior
|
||||
// mutability
|
||||
Reserved { .. } | Active => Active,
|
||||
ReservedFrz { .. } | ReservedIM | Active => Active,
|
||||
Frozen | Disabled => return None,
|
||||
})
|
||||
}
|
||||
|
@ -145,15 +158,15 @@ mod transition {
|
|||
/// A non-child node was write-accessed: this makes everything `Disabled` except for
|
||||
/// non-protected interior mutable `Reserved` which stay the same.
|
||||
fn foreign_write(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
|
||||
// There is no explicit dependency on `protected`, but recall that interior mutable
|
||||
// types receive a `ReservedFrz` instead of `ReservedIM` when retagged under a protector,
|
||||
// so the result of this function does indirectly depend on (past) protector status.
|
||||
Some(match state {
|
||||
// FIXME: since the fix related to reservedim_spurious_write, it is now possible
|
||||
// to express these transitions of the state machine without an explicit dependency
|
||||
// on `protected`: because `ty_is_freeze: false` implies `!protected` then
|
||||
// the line handling `Reserved { .. } if protected` could be deleted.
|
||||
// This will however require optimizations to the exhaustive tests because
|
||||
// fewer initial conditions are valid.
|
||||
Reserved { .. } if protected => Disabled,
|
||||
res @ Reserved { ty_is_freeze: false, .. } => res,
|
||||
res @ ReservedIM => {
|
||||
// We can never create a `ReservedIM` under a protector, only `ReservedFrz`.
|
||||
assert!(!protected);
|
||||
res
|
||||
}
|
||||
_ => Disabled,
|
||||
})
|
||||
}
|
||||
|
@ -208,9 +221,23 @@ impl Permission {
|
|||
Self { inner: Active }
|
||||
}
|
||||
|
||||
/// Default initial permission of a reborrowed mutable reference.
|
||||
pub fn new_reserved(ty_is_freeze: bool) -> Self {
|
||||
Self { inner: Reserved { ty_is_freeze, conflicted: false } }
|
||||
/// Default initial permission of a reborrowed mutable reference that is either
|
||||
/// protected or not interior mutable.
|
||||
fn new_reserved_frz() -> Self {
|
||||
Self { inner: ReservedFrz { conflicted: false } }
|
||||
}
|
||||
|
||||
/// Default initial permission of an unprotected interior mutable reference.
|
||||
fn new_reserved_im() -> Self {
|
||||
Self { inner: ReservedIM }
|
||||
}
|
||||
|
||||
/// Wrapper around `new_reserved_frz` and `new_reserved_im` that decides
|
||||
/// which to call based on the interior mutability and the retag kind (whether there
|
||||
/// is a protector is relevant because being protected takes priority over being
|
||||
/// interior mutable)
|
||||
pub fn new_reserved(ty_is_freeze: bool, protected: bool) -> Self {
|
||||
if ty_is_freeze || protected { Self::new_reserved_frz() } else { Self::new_reserved_im() }
|
||||
}
|
||||
|
||||
/// Default initial permission of a reborrowed shared reference.
|
||||
|
@ -224,6 +251,11 @@ impl Permission {
|
|||
Self { inner: Disabled }
|
||||
}
|
||||
|
||||
/// Reject `ReservedIM` that cannot exist in the presence of a protector.
|
||||
pub fn compatible_with_protector(&self) -> bool {
|
||||
self.inner.compatible_with_protector()
|
||||
}
|
||||
|
||||
/// Apply the transition to the inner PermissionPriv.
|
||||
pub fn perform_access(
|
||||
kind: AccessKind,
|
||||
|
@ -279,12 +311,9 @@ pub mod diagnostics {
|
|||
f,
|
||||
"{}",
|
||||
match self {
|
||||
Reserved { ty_is_freeze: true, conflicted: false } => "Reserved",
|
||||
Reserved { ty_is_freeze: true, conflicted: true } => "Reserved (conflicted)",
|
||||
Reserved { ty_is_freeze: false, conflicted: false } =>
|
||||
"Reserved (interior mutable)",
|
||||
Reserved { ty_is_freeze: false, conflicted: true } =>
|
||||
"Reserved (interior mutable, conflicted)",
|
||||
ReservedFrz { conflicted: false } => "Reserved",
|
||||
ReservedFrz { conflicted: true } => "Reserved (conflicted)",
|
||||
ReservedIM => "Reserved (interior mutable)",
|
||||
Active => "Active",
|
||||
Frozen => "Frozen",
|
||||
Disabled => "Disabled",
|
||||
|
@ -312,10 +341,9 @@ pub mod diagnostics {
|
|||
// and also as `diagnostics::DisplayFmtPermission.uninit` otherwise
|
||||
// alignment will be incorrect.
|
||||
match self.inner {
|
||||
Reserved { ty_is_freeze: true, conflicted: false } => "Rs ",
|
||||
Reserved { ty_is_freeze: true, conflicted: true } => "RsC ",
|
||||
Reserved { ty_is_freeze: false, conflicted: false } => "RsM ",
|
||||
Reserved { ty_is_freeze: false, conflicted: true } => "RsCM",
|
||||
ReservedFrz { conflicted: false } => "Res ",
|
||||
ReservedFrz { conflicted: true } => "ResC",
|
||||
ReservedIM => "ReIM",
|
||||
Active => "Act ",
|
||||
Frozen => "Frz ",
|
||||
Disabled => "Dis ",
|
||||
|
@ -325,13 +353,14 @@ pub mod diagnostics {
|
|||
|
||||
impl PermTransition {
|
||||
/// Readable explanation of the consequences of an event.
|
||||
/// Fits in the sentence "This accessed caused {trans.summary()}".
|
||||
/// Fits in the sentence "This transition corresponds to {trans.summary()}".
|
||||
pub fn summary(&self) -> &'static str {
|
||||
assert!(self.is_possible());
|
||||
assert!(!self.is_noop());
|
||||
match (self.from, self.to) {
|
||||
(_, Active) => "the first write to a 2-phase borrowed mutable reference",
|
||||
(_, Frozen) => "a loss of write permissions",
|
||||
(Reserved { conflicted: false, .. }, Reserved { conflicted: true, .. }) =>
|
||||
(ReservedFrz { conflicted: false }, ReservedFrz { conflicted: true }) =>
|
||||
"a temporary loss of write permissions until function exit",
|
||||
(Frozen, Disabled) => "a loss of read permissions",
|
||||
(_, Disabled) => "a loss of read and write permissions",
|
||||
|
@ -380,28 +409,33 @@ pub mod diagnostics {
|
|||
(Frozen, Frozen) => true,
|
||||
(Active, Frozen) => true,
|
||||
(Disabled, Disabled) => true,
|
||||
(Reserved { conflicted: true, .. }, Reserved { conflicted: true, .. }) =>
|
||||
true,
|
||||
(
|
||||
ReservedFrz { conflicted: true, .. },
|
||||
ReservedFrz { conflicted: true, .. },
|
||||
) => true,
|
||||
// A pointer being `Disabled` is a strictly stronger source of
|
||||
// errors than it being `Frozen`. If we try to access a `Disabled`,
|
||||
// then where it became `Frozen` (or `Active` or `Reserved`) is the least
|
||||
// of our concerns for now.
|
||||
(Reserved { conflicted: true, .. } | Active | Frozen, Disabled) => false,
|
||||
(Reserved { conflicted: true, .. }, Frozen) => false,
|
||||
(ReservedFrz { conflicted: true } | Active | Frozen, Disabled) => false,
|
||||
(ReservedFrz { conflicted: true }, Frozen) => false,
|
||||
|
||||
// `Active` and `Reserved` have all permissions, so a
|
||||
// `ChildAccessForbidden(Reserved | Active)` can never exist.
|
||||
(_, Active) | (_, Reserved { conflicted: false, .. }) =>
|
||||
(_, Active) | (_, ReservedFrz { conflicted: false }) =>
|
||||
unreachable!("this permission cannot cause an error"),
|
||||
// No transition has `Reserved(conflicted=false)` as its `.to` unless it's a noop.
|
||||
(Reserved { conflicted: false, .. }, _) =>
|
||||
// No transition has `Reserved { conflicted: false }` or `ReservedIM`
|
||||
// as its `.to` unless it's a noop.
|
||||
(ReservedFrz { conflicted: false } | ReservedIM, _) =>
|
||||
unreachable!("self is a noop transition"),
|
||||
// All transitions produced in normal executions (using `apply_access`)
|
||||
// change permissions in the order `Reserved -> Active -> Frozen -> Disabled`.
|
||||
// We assume that the error was triggered on the same location that
|
||||
// the transition `self` applies to, so permissions found must be increasing
|
||||
// in the order `self.from < self.to <= insufficient.inner`
|
||||
(Active | Frozen | Disabled, Reserved { .. }) | (Disabled, Frozen) =>
|
||||
(Active | Frozen | Disabled, ReservedFrz { .. } | ReservedIM)
|
||||
| (Disabled, Frozen)
|
||||
| (ReservedFrz { .. }, ReservedIM) =>
|
||||
unreachable!("permissions between self and err must be increasing"),
|
||||
}
|
||||
}
|
||||
|
@ -415,8 +449,10 @@ pub mod diagnostics {
|
|||
// conflicted.
|
||||
(Active, Active) => true,
|
||||
(Frozen, Frozen) => true,
|
||||
(Reserved { conflicted: true, .. }, Reserved { conflicted: true, .. }) =>
|
||||
true,
|
||||
(
|
||||
ReservedFrz { conflicted: true, .. },
|
||||
ReservedFrz { conflicted: true, .. },
|
||||
) => true,
|
||||
// If the error is a transition `Frozen -> Disabled`, then we don't really
|
||||
// care whether before that was `Reserved -> Active -> Frozen` or
|
||||
// `Frozen` directly.
|
||||
|
@ -429,23 +465,23 @@ pub mod diagnostics {
|
|||
// -> Reserved { conflicted: true }` is inexistant or irrelevant,
|
||||
// and so is the `Reserved { conflicted: false } -> Active`
|
||||
(Active, Frozen) => false,
|
||||
(Reserved { conflicted: true, .. }, _) => false,
|
||||
(ReservedFrz { conflicted: true }, _) => false,
|
||||
|
||||
(_, Disabled) =>
|
||||
unreachable!(
|
||||
"permission that results in Disabled should not itself be Disabled in the first place"
|
||||
),
|
||||
// No transition has `Reserved { conflicted: false }` as its `.to`
|
||||
// No transition has `Reserved { conflicted: false }` or `ReservedIM` as its `.to`
|
||||
// unless it's a noop.
|
||||
(Reserved { conflicted: false, .. }, _) =>
|
||||
(ReservedFrz { conflicted: false } | ReservedIM, _) =>
|
||||
unreachable!("self is a noop transition"),
|
||||
|
||||
// Permissions only evolve in the order `Reserved -> Active -> Frozen -> Disabled`,
|
||||
// so permissions found must be increasing in the order
|
||||
// `self.from < self.to <= forbidden.from < forbidden.to`.
|
||||
(Disabled, Reserved { .. } | Active | Frozen)
|
||||
| (Frozen, Reserved { .. } | Active)
|
||||
| (Active, Reserved { .. }) =>
|
||||
(Disabled, ReservedFrz { .. } | ReservedIM | Active | Frozen)
|
||||
| (Frozen, ReservedFrz { .. } | ReservedIM | Active)
|
||||
| (Active, ReservedFrz { .. } | ReservedIM) =>
|
||||
unreachable!("permissions between self and err must be increasing"),
|
||||
}
|
||||
}
|
||||
|
@ -466,9 +502,9 @@ pub mod diagnostics {
|
|||
|
||||
#[cfg(test)]
|
||||
impl Permission {
|
||||
pub fn is_reserved_with_conflicted(&self, expected_conflicted: bool) -> bool {
|
||||
pub fn is_reserved_frz_with_conflicted(&self, expected_conflicted: bool) -> bool {
|
||||
match self.inner {
|
||||
Reserved { conflicted, .. } => conflicted == expected_conflicted,
|
||||
ReservedFrz { conflicted } => conflicted == expected_conflicted,
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
|
@ -482,10 +518,9 @@ mod propagation_optimization_checks {
|
|||
impl Exhaustive for PermissionPriv {
|
||||
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
|
||||
Box::new(
|
||||
vec![Active, Frozen, Disabled].into_iter().chain(
|
||||
<[bool; 2]>::exhaustive()
|
||||
.map(|[ty_is_freeze, conflicted]| Reserved { ty_is_freeze, conflicted }),
|
||||
),
|
||||
vec![Active, Frozen, Disabled, ReservedIM]
|
||||
.into_iter()
|
||||
.chain(<bool>::exhaustive().map(|conflicted| ReservedFrz { conflicted })),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
@ -525,6 +560,9 @@ mod propagation_optimization_checks {
|
|||
// We thus eliminate from this test and all other tests
|
||||
// the case where the tag is initially unprotected and later becomes protected.
|
||||
precondition!(old_protected || !new_protected);
|
||||
if old_protected {
|
||||
precondition!(old.compatible_with_protector());
|
||||
}
|
||||
for (access, rel_pos) in <(AccessKind, AccessRelatedness)>::exhaustive() {
|
||||
if let Some(new) = perform_access(access, rel_pos, old, old_protected) {
|
||||
assert_eq!(
|
||||
|
@ -546,6 +584,9 @@ mod propagation_optimization_checks {
|
|||
for old in PermissionPriv::exhaustive() {
|
||||
for [old_protected, new_protected] in <[bool; 2]>::exhaustive() {
|
||||
precondition!(old_protected || !new_protected);
|
||||
if old_protected {
|
||||
precondition!(old.compatible_with_protector());
|
||||
}
|
||||
for rel_pos in AccessRelatedness::exhaustive() {
|
||||
precondition!(rel_pos.is_foreign());
|
||||
if let Some(new) = perform_access(old_access, rel_pos, old, old_protected) {
|
||||
|
@ -570,6 +611,9 @@ mod propagation_optimization_checks {
|
|||
reach.insert((start, start));
|
||||
for (access, rel) in <(AccessKind, AccessRelatedness)>::exhaustive() {
|
||||
for prot in bool::exhaustive() {
|
||||
if prot {
|
||||
precondition!(start.compatible_with_protector());
|
||||
}
|
||||
if let Some(end) = transition::perform_access(access, rel, start, prot) {
|
||||
reach.insert((start, end));
|
||||
}
|
||||
|
|
|
@ -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,
|
||||
|
@ -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;
|
||||
|
@ -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.
|
||||
|
@ -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)
|
||||
|
@ -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 {
|
||||
|
@ -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))
|
||||
}
|
||||
|
||||
|
@ -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 });
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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]>
|
||||
|
|
|
@ -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>
|
||||
──────────────────────────────────────────────────
|
||||
|
|
|
@ -3,20 +3,20 @@
|
|||
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*
|
||||
──────────────────────────────────────────────────
|
||||
|
@ -24,7 +24,7 @@ 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
|
||||
|
@ -32,20 +32,20 @@ Warning: this tree is indicative only. Some tags may have been hidden.
|
|||
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
|
||||
──────────────────────────────────────────────────
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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>
|
||||
──────────────────────────────────────────────────
|
||||
──────────────────────────────────────────────────
|
||||
|
|
|
@ -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()>
|
||||
──────────────────────────────────────────────────
|
||||
|
|
Loading…
Add table
Reference in a new issue