exract a perform_access, check read-read commutation exhaustively

This commit is contained in:
Neven Villani 2023-07-28 18:43:25 +02:00
parent 5a460a08ae
commit de056754da
No known key found for this signature in database
GPG Key ID: 00E765FA7F4F2EDE
18 changed files with 193 additions and 100 deletions

View File

@ -310,9 +310,9 @@ impl TbError<'_> {
"the accessed tag {accessed} is foreign to the {conflicting_tag_name} tag {conflicting} (i.e., it is not a child)"
),
format!(
"this {access} would cause the {conflicting_tag_name} tag {conflicting} currently {before_disabled} to become Disabled"
"this {access} would cause the {conflicting_tag_name} tag {conflicting} (currently {before_disabled}) to become Disabled"
),
format!("protected tags must not become Disabled"),
format!("protected tags must never be Disabled"),
];
(title, details, conflicting_tag_name)
}

View File

@ -381,7 +381,7 @@ mod propagation_optimization_checks {
pub use super::*;
impl PermissionPriv {
/// Enumerate all states
pub fn all() -> impl Iterator<Item = PermissionPriv> {
pub fn all() -> impl Iterator<Item = Self> {
vec![
Active,
Reserved { ty_is_freeze: true },
@ -393,9 +393,15 @@ mod propagation_optimization_checks {
}
}
impl Permission {
pub fn all() -> impl Iterator<Item = Self> {
PermissionPriv::all().map(|inner| Self { inner })
}
}
impl AccessKind {
/// Enumerate all AccessKind.
pub fn all() -> impl Iterator<Item = AccessKind> {
pub fn all() -> impl Iterator<Item = Self> {
use AccessKind::*;
[Read, Write].into_iter()
}
@ -403,7 +409,7 @@ mod propagation_optimization_checks {
impl AccessRelatedness {
/// Enumerate all relative positions
pub fn all() -> impl Iterator<Item = AccessRelatedness> {
pub fn all() -> impl Iterator<Item = Self> {
use AccessRelatedness::*;
[This, StrictChildAccess, AncestorAccess, DistantAccess].into_iter()
}

View File

@ -19,6 +19,7 @@ use rustc_target::abi::Size;
use crate::borrow_tracker::tree_borrows::{
diagnostics::{self, NodeDebugInfo, TbError, TransitionError},
perms::PermTransition,
unimap::{UniEntry, UniIndex, UniKeyMap, UniValMap},
Permission,
};
@ -69,6 +70,74 @@ impl LocationState {
pub fn permission(&self) -> Permission {
self.permission
}
/// Apply the effect of an access to one location, including
/// - applying `Permission::perform_access` to the inner `Permission`,
/// - emitting protector UB if the location is initialized,
/// - updating the initialized status (child accesses produce initialized locations).
fn perform_access(
&mut self,
access_kind: AccessKind,
rel_pos: AccessRelatedness,
protected: bool,
) -> Result<PermTransition, TransitionError> {
let old_perm = self.permission;
let transition = Permission::perform_access(access_kind, rel_pos, old_perm, protected)
.ok_or(TransitionError::ChildAccessForbidden(old_perm))?;
if protected
// Can't trigger Protector on uninitialized locations
&& self.initialized
&& transition.produces_disabled()
{
return Err(TransitionError::ProtectedDisabled(old_perm));
}
self.permission = transition.applied(old_perm).unwrap();
self.initialized |= !rel_pos.is_foreign();
Ok(transition)
}
// Optimize the tree traversal.
// The optimization here consists of observing thanks to the tests
// `foreign_read_is_noop_after_write` and `all_transitions_idempotent`
// that if we apply twice in a row the effects of a foreign access
// we can skip some branches.
// "two foreign accesses in a row" occurs when `perm.latest_foreign_access` is `Some(_)`
// AND the `rel_pos` of the current access corresponds to a foreign access.
fn skip_if_known_noop(
&mut self,
access_kind: AccessKind,
rel_pos: AccessRelatedness,
) -> ContinueTraversal {
if rel_pos.is_foreign() {
let new_access_noop = match (self.latest_foreign_access, access_kind) {
// Previously applied transition makes the new one a guaranteed
// noop in the two following cases:
// (1) justified by `foreign_read_is_noop_after_write`
(Some(AccessKind::Write), AccessKind::Read) => true,
// (2) justified by `all_transitions_idempotent`
(Some(old), new) if old == new => true,
// In all other cases there has been a recent enough
// child access that the effects of the new foreign access
// need to be applied to this subtree.
_ => false,
};
if new_access_noop {
// Abort traversal if the new transition is indeed guaranteed
// to be noop.
return ContinueTraversal::SkipChildren;
} else {
// Otherwise propagate this time, and also record the
// access that just occurred so that we can skip the propagation
// next time.
self.latest_foreign_access = Some(access_kind);
}
} else {
// A child access occurred, this breaks the streak of "two foreign
// accesses in a row" and we reset this field.
self.latest_foreign_access = None;
}
ContinueTraversal::Recurse
}
}
/// Tree structure with both parents and children since we want to be
@ -387,11 +456,15 @@ impl<'tcx> Tree {
Ok(())
}
/// Maps the following propagation procedure to each range:
/// - initialize if needed;
/// - compute new state after transition;
/// - check that there is no protector that would forbid this;
/// - record this specific location as accessed.
/// Map the per-node and per-location `LocationState::perform_access`
/// to each location of `access_range`, on every tag of the allocation.
///
/// `LocationState::perform_access` will take care of raising transition
/// errors and updating the `initialized` status of each location,
/// this traversal adds to that:
/// - inserting into the map locations that do not exist yet,
/// - trimming the traversal,
/// - recording the history.
pub fn perform_access(
&mut self,
access_kind: AccessKind,
@ -411,55 +484,16 @@ impl<'tcx> Tree {
let old_state =
perm.or_insert_with(|| LocationState::new(node.default_initial_perm));
// Optimize the tree traversal.
// The optimization here consists of observing thanks to the tests
// `foreign_read_is_noop_after_write` and `all_transitions_idempotent`
// that if we apply twice in a row the effects of a foreign access
// we can skip some branches.
// "two foreign accesses in a row" occurs when `perm.latest_foreign_access` is `Some(_)`
// AND the `rel_pos` of the current access corresponds to a foreign access.
if rel_pos.is_foreign() {
let new_access_noop =
match (old_state.latest_foreign_access, access_kind) {
// Previously applied transition makes the new one a guaranteed
// noop in the two following cases:
// (1) justified by `foreign_read_is_noop_after_write`
(Some(AccessKind::Write), AccessKind::Read) => true,
// (2) justified by `all_transitions_idempotent`
(Some(old), new) if old == new => true,
// In all other cases there has been a recent enough
// child access that the effects of the new foreign access
// need to be applied to this subtree.
_ => false,
};
if new_access_noop {
// Abort traversal if the new transition is indeed guaranteed
// to be noop.
return Ok(ContinueTraversal::SkipChildren);
} else {
// Otherwise propagate this time, and also record the
// access that just occurred so that we can skip the propagation
// next time.
old_state.latest_foreign_access = Some(access_kind);
}
} else {
// A child access occurred, this breaks the streak of "two foreign
// accesses in a row" and we reset this field.
old_state.latest_foreign_access = None;
match old_state.skip_if_known_noop(access_kind, rel_pos) {
ContinueTraversal::SkipChildren =>
return Ok(ContinueTraversal::SkipChildren),
_ => {}
}
let old_perm = old_state.permission;
let protected = global.borrow().protected_tags.contains_key(&node.tag);
let transition =
Permission::perform_access(access_kind, rel_pos, old_perm, protected)
.ok_or(TransitionError::ChildAccessForbidden(old_perm))?;
if protected
// Can't trigger Protector on uninitialized locations
&& old_state.initialized
&& transition.produces_disabled()
{
return Err(TransitionError::ProtectedDisabled(old_perm));
}
old_state.perform_access(access_kind, rel_pos, protected)?;
// Record the event as part of the history
if !transition.is_noop() {
node.debug_info.history.push(diagnostics::Event {
@ -470,10 +504,7 @@ impl<'tcx> Tree {
transition_range: perms_range.clone(),
span,
});
old_state.permission =
transition.applied(old_state.permission).unwrap();
}
old_state.initialized |= !rel_pos.is_foreign();
Ok(ContinueTraversal::Recurse)
},
|args: ErrHandlerArgs<'_, TransitionError>| -> InterpError<'tcx> {
@ -602,3 +633,57 @@ impl AccessRelatedness {
}
}
}
#[cfg(test)]
mod commutation_tests {
use super::*;
impl LocationState {
pub fn all_without_access() -> impl Iterator<Item = Self> {
Permission::all().flat_map(|permission| {
[false, true].into_iter().map(move |initialized| {
Self { permission, initialized, latest_foreign_access: None }
})
})
}
}
#[test]
#[rustfmt::skip]
// Exhaustive check that for any starting configuration loc,
// for any two read accesses r1 and r2, if `loc + r1 + r2` is not UB
// and results in `loc'`, then `loc + r2 + r1` is also not UB and results
// in the same final state `loc'`.
// This lets us justify arbitrary read-read reorderings.
fn all_read_accesses_commute() {
let kind = AccessKind::Read;
// Two of the four combinations of `AccessRelatedness` are trivial,
// but we might as well check them all.
for rel1 in AccessRelatedness::all() {
for rel2 in AccessRelatedness::all() {
// Any protector state works, but we can't move reads across function boundaries
// so the two read accesses occur under the same protector.
for &protected in &[true, false] {
for loc in LocationState::all_without_access() {
// 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;
let Ok(_) = loc12.perform_access(kind, rel1, protected) else { continue; };
let Ok(_) = loc12.perform_access(kind, rel2, protected) else { continue; };
// If 1 followed by 2 succeeded, then 2 followed by 1 must also succeed...
let mut loc21 = loc;
loc21.perform_access(kind, rel2, protected).unwrap();
loc21.perform_access(kind, rel1, protected).unwrap();
// ... and produce the same final result.
assert_eq!(
loc12, loc21,
"Read accesses {:?} followed by {:?} do not commute !",
rel1, rel2
);
}
}
}
}
}
}

View File

@ -6,8 +6,8 @@ LL | ptr::write(dest, src);
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> currently Frozen to become Disabled
= help: protected tags must not become Disabled
= help: this foreign write access would cause the protected tag <TAG> (currently Frozen) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/aliasing_mut4.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | *y
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign read access would cause the protected tag <TAG> currently Active to become Disabled
= help: protected tags must not become Disabled
= help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/box_noalias_violation.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { *y = 2 };
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> currently Active to become Disabled
= help: protected tags must not become Disabled
= help: this foreign write access would cause the protected tag <TAG> (currently Active) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/illegal_write6.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { *x = 0 };
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> currently Frozen to become Disabled
= help: protected tags must not become Disabled
= help: this foreign write access would cause the protected tag <TAG> (currently Frozen) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/invalidate_against_protector2.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { *x = 0 };
|
= 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> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> currently Frozen to become Disabled
= help: protected tags must not become Disabled
= help: this foreign write access would cause the protected tag <TAG> (currently Frozen) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/invalidate_against_protector3.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> currently Frozen to become Disabled
= help: protected tags must not become Disabled
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Frozen) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/newtype_pair_retagging.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> currently Frozen to become Disabled
= help: protected tags must not become Disabled
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> (currently Frozen) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/newtype_retagging.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { ptr.write(S(0)) };
|
= 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> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> currently Active to become Disabled
= help: protected tags must not become Disabled
= help: this foreign write access would cause the protected tag <TAG> (currently Active) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/arg_inplace_mutate.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { ptr.read() };
|
= 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> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign read access would cause the protected tag <TAG> currently Active to become Disabled
= help: protected tags must not become Disabled
= help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/arg_inplace_observe_during.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | unsafe { ptr.read() };
|
= 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> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign read access would cause the protected tag <TAG> currently Active to become Disabled
= help: protected tags must not become Disabled
= help: this foreign read access would cause the protected tag <TAG> (currently Active) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/return_pointer_aliasing.rs:LL:CC
|

View File

@ -6,8 +6,8 @@ LL | *y.add(3) = 42;
|
= 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> currently Reserved to become Disabled
= help: protected tags must not become Disabled
= help: this foreign write access would cause the protected tag <TAG> (currently Reserved) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/outside-range.rs:LL:CC
|

View File

@ -16,8 +16,8 @@ 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 to become Disabled
= help: protected tags must not 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
|

View File

@ -16,8 +16,8 @@ LL | *y = 0;
|
= 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 to become Disabled
= help: protected tags must not 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/int-protected-write.rs:LL:CC
|

View File

@ -1,16 +0,0 @@
//@compile-flags: -Zmiri-tree-borrows
// Protectors should not trigger on uninitialized locations,
// otherwise we can write safe code that triggers UB.
// To test this we do a write access that disables a protected
// location, but the location is actually outside of the protected range.
// Both x and y are protected here
fn write_second(_x: &mut u8, y: &mut u8) {
*y = 1;
}
fn main() {
let mut data = (0u8, 1u8);
write_second(&mut data.0, &mut data.1);
}

View File

@ -9,6 +9,7 @@ use std::ptr;
fn main() {
aliasing_read_only_mutable_refs();
string_as_mut_ptr();
two_mut_protected_same_alloc();
// Stacked Borrows tests
read_does_not_invalidate1();
@ -62,6 +63,23 @@ pub fn string_as_mut_ptr() {
}
}
// This function checks that there is no issue with having two mutable references
// from the same allocation both under a protector.
// This is safe code, it must absolutely not be UB.
// This test failing is a symptom of forgetting to check that only initialized
// locations can cause protector UB.
fn two_mut_protected_same_alloc() {
fn write_second(_x: &mut u8, y: &mut u8) {
// write through `y` will make some locations of `x` (protected)
// become Disabled. Those locations are outside of the range on which
// `x` is initialized, and the protector must not trigger.
*y = 1;
}
let mut data = (0u8, 1u8);
write_second(&mut data.0, &mut data.1);
}
// ----- The tests below were taken from Stacked Borrows ----
// Make sure that reading from an `&mut` does, like reborrowing to `&`,