From efc2af48510b52cb7a917b9e482d0a6abe5a0617 Mon Sep 17 00:00:00 2001 From: Neven Villani Date: Wed, 26 Jul 2023 13:00:53 +0200 Subject: [PATCH] fix protectors so that all reads actually commute --- .../tree_borrows/diagnostics.rs | 15 ++-- .../src/borrow_tracker/tree_borrows/perms.rs | 75 +++++++------------ .../src/borrow_tracker/tree_borrows/tree.rs | 4 +- .../both_borrows/aliasing_mut4.tree.stderr | 4 +- .../box_noalias_violation.tree.stderr | 4 +- .../both_borrows/illegal_write6.tree.stderr | 4 +- .../invalidate_against_protector2.tree.stderr | 4 +- .../invalidate_against_protector3.tree.stderr | 4 +- .../newtype_pair_retagging.tree.stderr | 4 +- .../newtype_retagging.tree.stderr | 4 +- .../arg_inplace_mutate.tree.stderr | 4 +- .../arg_inplace_observe_during.tree.stderr | 4 +- .../return_pointer_aliasing.tree.stderr | 4 +- .../fail/tree_borrows/outside-range.stderr | 4 +- .../reserved/cell-protected-write.stderr | 4 +- .../reserved/int-protected-write.stderr | 4 +- 16 files changed, 59 insertions(+), 87 deletions(-) diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs index 3b2d6f9608ee..5fb298a54af3 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs @@ -227,10 +227,10 @@ pub(super) enum TransitionError { ChildAccessForbidden(Permission), /// A protector was triggered due to an invalid transition that loses /// too much permissions. - /// For example, if a protected tag goes from `Active` to `Frozen` due - /// to a foreign write this will produce a `ProtectedTransition(PermTransition(Active, Frozen))`. + /// For example, if a protected tag goes from `Active` to `Disabled` due + /// to a foreign write this will produce a `ProtectedDisabled(Active)`. /// This kind of error can only occur on foreign accesses. - ProtectedTransition(PermTransition), + ProtectedDisabled(Permission), /// Cannot deallocate because some tag in the allocation is strongly protected. /// This kind of error can only occur on deallocations. ProtectedDealloc, @@ -302,7 +302,7 @@ impl TbError<'_> { )); (title, details, conflicting_tag_name) } - ProtectedTransition(transition) => { + ProtectedDisabled(before_disabled) => { let conflicting_tag_name = "protected"; let access = cause.print_as_access(/* is_foreign */ true); let details = vec![ @@ -310,12 +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} to transition {transition}" - ), - format!( - "this transition would be {loss}, which is not allowed for protected tags", - loss = transition.summary(), + "this {access} would cause the {conflicting_tag_name} tag {conflicting} currently {before_disabled} to become Disabled" ), + format!("protected tags must not become Disabled"), ]; (title, details, conflicting_tag_name) } diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs index 362070f18578..f68da455378b 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs @@ -72,7 +72,12 @@ mod transition { // accesses, since the data is not being mutated. Hence the `{ .. }` res @ Reserved { .. } if !protected => res, Reserved { .. } => Frozen, // protected reserved - Active => Frozen, + Active => + if protected { + Disabled + } else { + Frozen + }, non_writeable @ (Frozen | Disabled) => non_writeable, }) } @@ -189,34 +194,9 @@ impl PermTransition { Permission { inner: self.from } } - /// Determines whether a transition that occured is compatible with the presence - /// of a Protector. This is not included in the `transition` functions because - /// it would distract from the few places where the transition is modified - /// because of a protector, but not forbidden. - /// - /// Note: this is not in charge of checking that there *is* a protector, - /// it should be used as - /// ``` - /// let no_protector_error = if is_protected(tag) { - /// transition.is_allowed_by_protector() - /// }; - /// ``` - pub fn is_allowed_by_protector(&self) -> bool { - assert!(self.is_possible()); - match (self.from, self.to) { - _ if self.from == self.to => true, - // It is always a protector violation to not be readable anymore - (_, Disabled) => false, - // In the case of a `Reserved` under a protector, both transitions - // `Reserved => Active` and `Reserved => Frozen` can legitimately occur. - // The first is standard (Child Write), the second is for Foreign Writes - // on protected Reserved where we must ensure that the pointer is not - // written to in the future. - (Reserved { .. }, Active) | (Reserved { .. }, Frozen) => true, - // This pointer should have stayed writeable for the whole function - (Active, Frozen) => false, - _ => unreachable!("Transition {} should never be possible", self), - } + /// Determines if this transition would disable the permission. + pub fn produces_disabled(self) -> bool { + self.to == Disabled } } @@ -298,14 +278,15 @@ pub mod diagnostics { /// /// This function assumes that its arguments apply to the same location /// and that they were obtained during a normal execution. It will panic otherwise. - /// - `err` cannot be a `ProtectedTransition(_)` of a noop transition, as those - /// never trigger protectors; /// - all transitions involved in `self` and `err` should be increasing /// (Reserved < Active < Frozen < Disabled); /// - between `self` and `err` the permission should also be increasing, /// so all permissions inside `err` should be greater than `self.1`; /// - `Active` and `Reserved` cannot cause an error due to insufficient permissions, /// so `err` cannot be a `ChildAccessForbidden(_)` of either of them; + /// - `err` should not be `ProtectedDisabled(Disabled)`, because the protected + /// tag should not have been `Disabled` in the first place (if this occurs it means + /// we have unprotected tags that become protected) pub(in super::super) fn is_relevant(&self, err: TransitionError) -> bool { // NOTE: `super::super` is the visibility of `TransitionError` assert!(self.is_possible()); @@ -342,17 +323,16 @@ pub mod diagnostics { unreachable!("permissions between self and err must be increasing"), } } - TransitionError::ProtectedTransition(forbidden) => { - assert!(!forbidden.is_noop()); + TransitionError::ProtectedDisabled(before_disabled) => { // Show how we got to the starting point of the forbidden transition, // but ignore what came before. // This eliminates transitions like `Reserved -> Active` // when the error is a `Frozen -> Disabled`. - match (self.to, forbidden.from, forbidden.to) { + match (self.to, before_disabled.inner) { // We absolutely want to know where it was activated. - (Active, Active, Frozen | Disabled) => true, + (Active, Active) => true, // And knowing where it became Frozen is also important. - (Frozen, Frozen, Disabled) => true, + (Frozen, Frozen) => true, // If the error is a transition `Frozen -> Disabled`, then we don't really // care whether before that was `Reserved -> Active -> Frozen` or // `Reserved -> Frozen` or even `Frozen` directly. @@ -360,27 +340,22 @@ pub mod diagnostics { // - created as Frozen, then Frozen -> Disabled is forbidden // - created as Reserved, later became Frozen, then Frozen -> Disabled is forbidden // In both cases the `Reserved -> Active` part is inexistant or irrelevant. - (Active, Frozen, Disabled) => false, + (Active, Frozen) => false, - // `Reserved -> Frozen` does not trigger protectors. - (_, Reserved { .. }, Frozen) => - unreachable!("this transition cannot cause an error"), + (_, Disabled) => + unreachable!( + "permission that results in Disabled should not itself be Disabled in the first place" + ), // No transition has `Reserved` as its `.to` unless it's a noop. - (Reserved { .. }, _, _) => unreachable!("self is a noop transition"), - (_, Disabled, Disabled) | (_, Frozen, Frozen) | (_, Active, Active) => - unreachable!("err contains a noop transition"), + (Reserved { .. }, _) => 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, Reserved { .. } | Active | Frozen) + | (Frozen, Reserved { .. } | Active) + | (Active, Reserved { .. }) => unreachable!("permissions between self and err must be increasing"), - (_, Disabled, Reserved { .. } | Active | Frozen) - | (_, Frozen, Reserved { .. } | Active) - | (_, Active, Reserved { .. }) => - unreachable!("permissions within err must be increasing"), } } // We don't care because protectors evolve independently from diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs index 9e8b1e118991..d6e470010140 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs @@ -456,9 +456,9 @@ impl<'tcx> Tree { if protected // Can't trigger Protector on uninitialized locations && old_state.initialized - && !transition.is_allowed_by_protector() + && transition.produces_disabled() { - return Err(TransitionError::ProtectedTransition(transition)); + return Err(TransitionError::ProtectedDisabled(old_perm)); } // Record the event as part of the history if !transition.is_noop() { diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr index 4102c718af83..8f278d0184a5 100644 --- a/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this foreign write access would cause the protected tag to transition from Frozen to Disabled - = help: this transition would be a loss of read permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag currently Frozen to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/aliasing_mut4.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr b/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr index 1d1ed820324a..6b4e86fa0c52 100644 --- a/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this foreign read access would cause the protected tag to transition from Active to Frozen - = help: this transition would be a loss of write permissions, which is not allowed for protected tags + = help: this foreign read access would cause the protected tag currently Active to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/box_noalias_violation.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr b/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr index 7308d045d193..5cfbb87fe276 100644 --- a/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this foreign write access would cause the protected tag to transition from Active to Disabled - = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag currently Active to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/illegal_write6.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr index ee64a66cc21a..ee882db8ac8f 100644 --- a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this foreign write access would cause the protected tag to transition from Frozen to Disabled - = help: this transition would be a loss of read permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag currently Frozen to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/invalidate_against_protector2.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr index e217170afb9e..30fd8215b6e2 100644 --- a/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr @@ -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 (root of the allocation) is foreign to the protected tag (i.e., it is not a child) - = help: this foreign write access would cause the protected tag to transition from Frozen to Disabled - = help: this transition would be a loss of read permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag currently Frozen to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/invalidate_against_protector3.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr b/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr index 00b2708a651c..0263c906b9b6 100644 --- a/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this deallocation (acting as a foreign write access) would cause the protected tag to transition from Frozen to Disabled - = help: this transition would be a loss of read permissions, which is not allowed for protected tags + = help: this deallocation (acting as a foreign write access) would cause the protected tag currently Frozen to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/newtype_pair_retagging.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr b/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr index aed2e7abebc0..710308fb8658 100644 --- a/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr +++ b/src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this deallocation (acting as a foreign write access) would cause the protected tag to transition from Frozen to Disabled - = help: this transition would be a loss of read permissions, which is not allowed for protected tags + = help: this deallocation (acting as a foreign write access) would cause the protected tag currently Frozen to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/newtype_retagging.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr b/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr index 35c02cc2ebde..f1bfe138def2 100644 --- a/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr +++ b/src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr @@ -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 (root of the allocation) is foreign to the protected tag (i.e., it is not a child) - = help: this foreign write access would cause the protected tag to transition from Active to Disabled - = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag currently Active to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/arg_inplace_mutate.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr b/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr index cbd76c38f627..2cf61488e437 100644 --- a/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr +++ b/src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr @@ -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 (root of the allocation) is foreign to the protected tag (i.e., it is not a child) - = help: this foreign read access would cause the protected tag to transition from Active to Frozen - = help: this transition would be a loss of write permissions, which is not allowed for protected tags + = help: this foreign read access would cause the protected tag currently Active to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/arg_inplace_observe_during.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr b/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr index c2c9de3f4eed..0bda8e0e343b 100644 --- a/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr +++ b/src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr @@ -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 (root of the allocation) is foreign to the protected tag (i.e., it is not a child) - = help: this foreign read access would cause the protected tag to transition from Active to Frozen - = help: this transition would be a loss of write permissions, which is not allowed for protected tags + = help: this foreign read access would cause the protected tag currently Active to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/return_pointer_aliasing.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr b/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr index 0feafb1a71e6..f490f12b4c88 100644 --- a/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr +++ b/src/tools/miri/tests/fail/tree_borrows/outside-range.stderr @@ -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 is foreign to the protected tag (i.e., it is not a child) - = help: this foreign write access would cause the protected tag to transition from Reserved to Disabled - = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag currently Reserved to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/outside-range.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr index c77f1492a972..35361822af0b 100644 --- a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr +++ b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr @@ -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 (y, callee:y, caller:y) is foreign to the protected tag (callee:x) (i.e., it is not a child) - = help: this foreign write access would cause the protected tag (callee:x) to transition from Reserved to Disabled - = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag (callee:x) currently Reserved to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/cell-protected-write.rs:LL:CC | diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr index ac8788112e90..83e495ce1932 100644 --- a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr +++ b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr @@ -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 (y, callee:y, caller:y) is foreign to the protected tag (callee:x) (i.e., it is not a child) - = help: this foreign write access would cause the protected tag (callee:x) to transition from Reserved to Disabled - = help: this transition would be a loss of read and write permissions, which is not allowed for protected tags + = help: this foreign write access would cause the protected tag (callee:x) currently Reserved to become Disabled + = help: protected tags must not become Disabled help: the accessed tag was created here --> $DIR/int-protected-write.rs:LL:CC |