Skip to content

Commit

Permalink
Auto merge of #114211 - RalfJung:miri, r=RalfJung
Browse files Browse the repository at this point in the history
update Miri

r? `@ghost`
  • Loading branch information
bors committed Jul 29, 2023
2 parents 03a5725 + 70757fb commit 32303b2
Show file tree
Hide file tree
Showing 34 changed files with 336 additions and 233 deletions.
13 changes: 5 additions & 8 deletions src/tools/miri/.github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,21 +10,14 @@ on:
branches:
- 'master'
schedule:
- cron: '6 6 * * *' # At 6:06 UTC every day.

env:
CARGO_UNSTABLE_SPARSE_REGISTRY: 'true'
- cron: '11 5 * * *' # At 5:11 UTC every day.

defaults:
run:
shell: bash

jobs:
build:
runs-on: ${{ matrix.os }}
env:
RUST_BACKTRACE: 1
HOST_TARGET: ${{ matrix.host_target }}
strategy:
fail-fast: false
matrix:
Expand All @@ -35,6 +28,10 @@ jobs:
host_target: x86_64-apple-darwin
- os: windows-latest
host_target: i686-pc-windows-msvc
runs-on: ${{ matrix.os }}
env:
RUST_BACKTRACE: 1
HOST_TARGET: ${{ matrix.host_target }}
steps:
- uses: actions/checkout@v3

Expand Down
2 changes: 1 addition & 1 deletion src/tools/miri/rust-version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
cec34a43b1b14f4e39363f3b283d7ac4f593ee81
d150dbb067e66f351a0b33a54e7d4b464ef51e47
15 changes: 6 additions & 9 deletions src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -302,20 +302,17 @@ 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![
format!(
"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 never be Disabled"),
];
(title, details, conflicting_tag_name)
}
Expand Down
87 changes: 34 additions & 53 deletions src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
})
}
Expand Down Expand Up @@ -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
}
}

Expand Down Expand Up @@ -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());
Expand Down Expand Up @@ -342,45 +323,39 @@ 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.
// The error will only show either
// - 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
Expand All @@ -406,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 },
Expand All @@ -418,17 +393,23 @@ 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()
}
}

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()
}
Expand Down
Loading

0 comments on commit 32303b2

Please sign in to comment.