Skip to content
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

update Miri #113151

Merged
merged 64 commits into from
Jun 29, 2023
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
64 commits
Select commit Hold shift click to select a range
13c20f2
deref shim arguments with actual ty instead of declared ty
beepster4096 Nov 9, 2022
9d1d651
add deref_pointer_as
beepster4096 Jun 2, 2023
7380a4d
explain windows sync layouts
beepster4096 Jun 3, 2023
580e2b3
Select more TB fail tests
Vanille-N May 10, 2023
9667886
Auto merge of #2887 - Vanille-N:tb-mut-transmute, r=RalfJung
bors Jun 3, 2023
7444a50
use as_os_str_bytes
RalfJung Jun 3, 2023
c1a7783
Auto merge of #2915 - RalfJung:as_os_str_bytes, r=RalfJung
bors Jun 3, 2023
53187d7
Remove rustc-workspace-hack
ehuss Jun 4, 2023
5d01a6b
Auto merge of #2916 - ehuss:remove-workspace-hack, r=RalfJung
bors Jun 4, 2023
7a1cdf7
Differentiate between explicit accesses and accesses inserted by TB
Vanille-N Jun 5, 2023
98c5fce
Auto merge of #2918 - Vanille-N:tb-diags, r=RalfJung
bors Jun 5, 2023
c87f6d9
Revert error in doc comment
Vanille-N Jun 5, 2023
634c21f
Auto merge of #2919 - Vanille-N:tb-diags, r=RalfJung
bors Jun 5, 2023
be5f6b2
box_exclusive_violation
Vanille-N Jun 10, 2023
85533a3
Auto merge of #2922 - Vanille-N:tb-tests, r=RalfJung
bors Jun 11, 2023
6147833
Preparing for merge from rustc
RalfJung Jun 11, 2023
6ab7af4
Merge from rustc
RalfJung Jun 11, 2023
15a6362
Auto merge of #2924 - RalfJung:rustup, r=RalfJung
bors Jun 12, 2023
36e0c42
Preparing for merge from rustc
oli-obk Jun 15, 2023
24595f5
Merge from rustc
oli-obk Jun 15, 2023
52036f5
Auto merge of #2928 - oli-obk:rustup, r=oli-obk
bors Jun 15, 2023
b4b7cd6
Auto merge of #2661 - DrMeepster:deref_operand_as, r=oli-obk
bors Jun 15, 2023
8e930fd
Preparing for merge from rustc
RalfJung Jun 16, 2023
508675b
Merge from rustc
RalfJung Jun 16, 2023
c853744
Auto merge of #2930 - RalfJung:rustup, r=RalfJung
bors Jun 16, 2023
e2d2266
add tests for panicky drop in thread_local destructor
RalfJung Jun 16, 2023
f3b52fd
make test work cross-platform
RalfJung Jun 16, 2023
6f771c8
Auto merge of #2929 - RalfJung:tls-panic, r=RalfJung
bors Jun 16, 2023
5c9ad8b
comment tweaks
RalfJung Jun 16, 2023
20a2a24
Auto merge of #2932 - RalfJung:comment, r=RalfJung
bors Jun 16, 2023
dfd5037
Preparing for merge from rustc
RalfJung Jun 17, 2023
14155e9
Merge from rustc
RalfJung Jun 17, 2023
5f81d83
Auto merge of #2933 - RalfJung:rustup, r=RalfJung
bors Jun 17, 2023
e696299
Preparing for merge from rustc
RalfJung Jun 18, 2023
7cef286
Merge from rustc
RalfJung Jun 18, 2023
6ea5035
bless new tests
RalfJung Jun 19, 2023
f769045
Auto merge of #2935 - RalfJung:rustup, r=RalfJung
bors Jun 19, 2023
a004056
mmap/munmap/mremamp shims
saethlin Aug 13, 2022
69dc735
Make munmap throw unsup errors instead of trying to work
saethlin Jun 16, 2023
8fc8f13
Improve organization
saethlin Jun 17, 2023
b621c4d
Auto merge of #2520 - saethlin:mmap-shim, r=RalfJung
bors Jun 20, 2023
2bd9ade
Preparing for merge from rustc
RalfJung Jun 22, 2023
940cd59
Merge from rustc
RalfJung Jun 22, 2023
878c6ae
Auto merge of #2938 - RalfJung:rustup, r=RalfJung
bors Jun 22, 2023
65d60f9
drop perform_read_access (always read) in favor of zero_size
Vanille-N Jun 19, 2023
732f127
Update ui test crate
oli-obk Jun 26, 2023
3917774
Auto merge of #2941 - oli-obk:ui_test_bump, r=oli-obk
bors Jun 26, 2023
0ba4cdb
Make `--quiet` actually do something
oli-obk Jun 27, 2023
b567773
Auto merge of #2942 - oli-obk:ui_test_bump, r=RalfJung
bors Jun 27, 2023
c91fb78
Add trophy
cbeuw Jun 27, 2023
662388e
Auto merge of #2943 - cbeuw:patch-1, r=oli-obk
bors Jun 27, 2023
48294e4
Preparing for merge from rustc
oli-obk Jun 28, 2023
c10656e
Merge from rustc
oli-obk Jun 28, 2023
de9dc59
fmt
oli-obk Jun 28, 2023
984d29d
Auto merge of #2944 - oli-obk:rustup, r=oli-obk
bors Jun 28, 2023
e1b2951
Try running a sync automatically
oli-obk Jun 28, 2023
1ffe627
Auto merge of #2945 - oli-obk:gha_mk_pr, r=RalfJung
bors Jun 28, 2023
0671f14
Unique gets special treatment when -Zmiri-unique-is-unique
Vanille-N Jun 19, 2023
cec5ec4
Auto merge of #2936 - Vanille-N:unique, r=RalfJung
bors Jun 28, 2023
8d4b2bd
Preparing for merge from rustc
RalfJung Jun 29, 2023
cca0c81
Merge from rustc
RalfJung Jun 29, 2023
feed376
Auto merge of #2946 - RalfJung:rustup, r=RalfJung
bors Jun 29, 2023
a3cea7f
update lockfile
RalfJung Jun 29, 2023
78f58f9
Use a valid `target` directory in miri ui tests
oli-obk Jun 29, 2023
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
61 changes: 46 additions & 15 deletions src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,16 12,46 @@ use crate::borrow_tracker::tree_borrows::{
use crate::borrow_tracker::{AccessKind, ProtectorKind};
use crate::*;

/// Cause of an access: either a real access or one
/// inserted by Tree Borrows due to a reborrow or a deallocation.
#[derive(Clone, Copy, Debug)]
pub enum AccessCause {
Explicit(AccessKind),
Reborrow,
Dealloc,
}

impl fmt::Display for AccessCause {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Self::Explicit(kind) => write!(f, "{kind}"),
Self::Reborrow => write!(f, "reborrow"),
Self::Dealloc => write!(f, "deallocation"),
}
}
}

impl AccessCause {
fn print_as_access(self, is_foreign: bool) -> String {
let rel = if is_foreign { "foreign" } else { "child" };
match self {
Self::Explicit(kind) => format!("{rel} {kind}"),
Self::Reborrow => format!("reborrow (acting as a {rel} read access)"),
Self::Dealloc => format!("deallocation (acting as a {rel} write access)"),
}
}
}

/// Complete data for an event:
#[derive(Clone, Debug)]
pub struct Event {
/// Transformation of permissions that occured because of this event
pub transition: PermTransition,
/// Kind of the access that triggered this event
pub access_kind: AccessKind,
pub access_cause: AccessCause,
/// Relative position of the tag to the one used for the access
pub is_foreign: bool,
/// User-visible range of the access
/// Whether this access was explicit or inserted implicitly by Tree Borrows.
pub access_range: AllocRange,
/// The transition recorded by this event only occured on a subrange of
/// `access_range`: a single access on `access_range` triggers several events,
Expand Down Expand Up @@ -83,17 113,19 @@ impl HistoryData {
self.events.push((Some(created.0.data()), msg_creation));
for &Event {
transition,
access_kind,
is_foreign,
access_cause,
access_range,
span,
transition_range: _,
} in &events
{
// NOTE: `transition_range` is explicitly absent from the error message, it has no significance
// to the user. The meaningful one is `access_range`.
self.events.push((Some(span.data()), format!("{this} later transitioned to {endpoint} due to a {rel} {access_kind} at offsets {access_range:?}", endpoint = transition.endpoint(), rel = if is_foreign { "foreign" } else { "child" })));
self.events.push((None, format!("this corresponds to {}", transition.summary())));
let access = access_cause.print_as_access(is_foreign);
self.events.push((Some(span.data()), format!("{this} later transitioned to {endpoint} due to a {access} at offsets {access_range:?}", endpoint = transition.endpoint())));
self.events
.push((None, format!("this transition corresponds to {}", transition.summary())));
}
}
}
Expand Down Expand Up @@ -238,9 270,8 @@ pub(super) struct TbError<'node> {
/// On accesses rejected due to insufficient permissions, this is the
/// tag that lacked those permissions.
pub conflicting_info: &'node NodeDebugInfo,
/// Whether this was a Read or Write access. This field is ignored
/// when the error was triggered by a deallocation.
pub access_kind: AccessKind,
// What kind of access caused this error (read, write, reborrow, deallocation)
pub access_cause: AccessCause,
/// Which tag the access that caused this error was made through, i.e.
/// which tag was used to read/write/deallocate.
pub accessed_info: &'node NodeDebugInfo,
Expand All @@ -250,46 281,46 @@ impl TbError<'_> {
/// Produce a UB error.
pub fn build<'tcx>(self) -> InterpError<'tcx> {
use TransitionError::*;
let kind = self.access_kind;
let cause = self.access_cause;
let accessed = self.accessed_info;
let conflicting = self.conflicting_info;
let accessed_is_conflicting = accessed.tag == conflicting.tag;
let title = format!("{cause} through {accessed} is forbidden");
let (title, details, conflicting_tag_name) = match self.error_kind {
ChildAccessForbidden(perm) => {
let conflicting_tag_name =
if accessed_is_conflicting { "accessed" } else { "conflicting" };
let title = format!("{kind} through {accessed} is forbidden");
let mut details = Vec::new();
if !accessed_is_conflicting {
details.push(format!(
"the accessed tag {accessed} is a child of the conflicting tag {conflicting}"
));
}
let access = cause.print_as_access(/* is_foreign */ false);
details.push(format!(
"the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids child {kind}es"
"the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids this {access}"
));
(title, details, conflicting_tag_name)
}
ProtectedTransition(transition) => {
let conflicting_tag_name = "protected";
let title = format!("{kind} through {accessed} is forbidden");
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!(
"the access would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}"
"this {access} would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}"
),
format!(
"this is {loss}, which is not allowed for protected tags",
"this transition would be {loss}, which is not allowed for protected tags",
loss = transition.summary(),
),
];
(title, details, conflicting_tag_name)
}
ProtectedDealloc => {
let conflicting_tag_name = "strongly protected";
let title = format!("deallocation through {accessed} is forbidden");
let details = vec![
format!(
"the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}"
Expand Down
18 changes: 16 additions & 2 deletions src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 62,14 @@ impl<'tcx> Tree {
};
let global = machine.borrow_tracker.as_ref().unwrap();
let span = machine.current_span();
self.perform_access(access_kind, tag, range, global, span)
self.perform_access(
access_kind,
tag,
range,
global,
span,
diagnostics::AccessCause::Explicit(access_kind),
)
}

/// Check that this pointer has permission to deallocate this range.
Expand Down Expand Up @@ -273,7 280,14 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
// Count this reborrow as a read access
let global = &this.machine.borrow_tracker.as_ref().unwrap();
let span = this.machine.current_span();
tree_borrows.perform_access(AccessKind::Read, orig_tag, range, global, span)?;
tree_borrows.perform_access(
AccessKind::Read,
orig_tag,
range,
global,
span,
diagnostics::AccessCause::Reborrow,
)?;
if let Some(data_race) = alloc_extra.data_race.as_ref() {
data_race.read(alloc_id, range, &this.machine)?;
}
Expand Down
18 changes: 13 additions & 5 deletions src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -349,7 349,14 @@ impl<'tcx> Tree {
global: &GlobalState,
span: Span, // diagnostics
) -> InterpResult<'tcx> {
self.perform_access(AccessKind::Write, tag, access_range, global, span)?;
self.perform_access(
AccessKind::Write,
tag,
access_range,
global,
span,
diagnostics::AccessCause::Dealloc,
)?;
for (perms_range, perms) in self.rperms.iter_mut(access_range.start, access_range.size) {
TreeVisitor { nodes: &mut self.nodes, tag_mapping: &self.tag_mapping, perms }
.traverse_parents_this_children_others(
Expand All @@ -368,7 375,7 @@ impl<'tcx> Tree {
let ErrHandlerArgs { error_kind, conflicting_info, accessed_info } = args;
TbError {
conflicting_info,
access_kind: AccessKind::Write,
access_cause: diagnostics::AccessCause::Dealloc,
error_offset: perms_range.start,
error_kind,
accessed_info,
Expand All @@ -391,7 398,8 @@ impl<'tcx> Tree {
tag: BorTag,
access_range: AllocRange,
global: &GlobalState,
span: Span, // diagnostics
span: Span, // diagnostics
access_cause: diagnostics::AccessCause, // diagnostics
) -> InterpResult<'tcx> {
for (perms_range, perms) in self.rperms.iter_mut(access_range.start, access_range.size) {
TreeVisitor { nodes: &mut self.nodes, tag_mapping: &self.tag_mapping, perms }
Expand Down Expand Up @@ -456,8 464,8 @@ impl<'tcx> Tree {
if !transition.is_noop() {
node.debug_info.history.push(diagnostics::Event {
transition,
access_kind,
is_foreign: rel_pos.is_foreign(),
access_cause,
access_range,
transition_range: perms_range.clone(),
span,
Expand All @@ -472,7 480,7 @@ impl<'tcx> Tree {
let ErrHandlerArgs { error_kind, conflicting_info, accessed_info } = args;
TbError {
conflicting_info,
access_kind,
access_cause,
error_offset: perms_range.start,
error_kind,
accessed_info,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 6,7 @@ LL | let _val = *target_alias;
|
= 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 a child of the conflicting tag <TAG>
= help: the conflicting tag <TAG> has state Disabled which forbids child read accesses
= help: the conflicting tag <TAG> has state Disabled which forbids this child read access
help: the accessed tag <TAG> was created here
--> $DIR/alias_through_mutation.rs:LL:CC
|
Expand All @@ -22,7 22,7 @@ help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign
|
LL | *target = 13;
| ^^^^^^^^^^^^
= help: this corresponds to a loss of read and write permissions
= help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span):
= note: inside `main` at $DIR/alias_through_mutation.rs:LL:CC

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 5,18 @@ LL | *x = 1;
| ^^^^^^ write access through <TAG> is forbidden
|
= 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> has state Frozen which forbids child write accesses
= help: the accessed tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/aliasing_mut1.rs:LL:CC
|
LL | pub fn safe(x: &mut i32, y: &mut i32) {
| ^
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4]
help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
--> $DIR/aliasing_mut1.rs:LL:CC
|
LL | pub fn safe(x: &mut i32, y: &mut i32) {
| ^
= help: this corresponds to a loss of write permissions
= help: this transition corresponds to a loss of write permissions
= note: BACKTRACE (of the first span):
= note: inside `safe` at $DIR/aliasing_mut1.rs:LL:CC
note: inside `main`
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 5,7 @@ LL | *y = 2;
| ^^^^^^ write access through <TAG> is forbidden
|
= 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> has state Frozen which forbids child write accesses
= help: the accessed tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/aliasing_mut2.rs:LL:CC
|
Expand All @@ -16,7 16,7 @@ help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read
|
LL | let _v = *x;
| ^^
= help: this corresponds to a loss of write permissions
= help: this transition corresponds to a loss of write permissions
= note: BACKTRACE (of the first span):
= note: inside `safe` at $DIR/aliasing_mut2.rs:LL:CC
note: inside `main`
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 5,18 @@ LL | *x = 1;
| ^^^^^^ write access through <TAG> is forbidden
|
= 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> has state Frozen which forbids child write accesses
= help: the accessed tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/aliasing_mut3.rs:LL:CC
|
LL | pub fn safe(x: &mut i32, y: &i32) {
| ^
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4]
help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
--> $DIR/aliasing_mut3.rs:LL:CC
|
LL | pub fn safe(x: &mut i32, y: &i32) {
| ^
= help: this corresponds to a loss of write permissions
= help: this transition corresponds to a loss of write permissions
= note: BACKTRACE (of the first span):
= note: inside `safe` at $DIR/aliasing_mut3.rs:LL:CC
note: inside `main`
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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: the access would cause the protected tag <TAG> to transition from Frozen to Disabled
= help: this is a loss of read permissions, which is not allowed for protected tags
= help: this foreign write access would cause the protected tag <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: the accessed tag <TAG> was created here
--> $DIR/aliasing_mut4.rs:LL:CC
|
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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: the access would cause the protected tag <TAG> to transition from Active to Frozen
= help: this is a loss of write permissions, which is not allowed for protected tags
= help: this foreign read access would cause the protected tag <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: the accessed tag <TAG> was created here
--> $DIR/box_noalias_violation.rs:LL:CC
|
Expand All @@ -23,7 23,7 @@ help: the protected tag <TAG> later transitioned to Active due to a child write
|
LL | *x = 5;
| ^^^^^^
= help: this corresponds to the first write to a 2-phase borrowed mutable reference
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference
= note: BACKTRACE (of the first span):
= note: inside `test` at $DIR/box_noalias_violation.rs:LL:CC
note: inside `main`
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 6,7 @@ LL | v2[1] = 7;
|
= 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 a child of the conflicting tag <TAG>
= help: the conflicting tag <TAG> has state Disabled which forbids child write accesses
= help: the conflicting tag <TAG> has state Disabled which forbids this child write access
help: the accessed tag <TAG> was created here
--> $DIR/buggy_as_mut_slice.rs:LL:CC
|
Expand All @@ -22,7 22,7 @@ help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign
|
LL | v1[1] = 5;
| ^^^^^^^^^
= help: this corresponds to a loss of read and write permissions
= help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span):
= note: inside `main` at $DIR/buggy_as_mut_slice.rs:LL:CC

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 6,7 @@ LL | b[1] = 6;
|
= 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 a child of the conflicting tag <TAG>
= help: the conflicting tag <TAG> has state Disabled which forbids child write accesses
= help: the conflicting tag <TAG> has state Disabled which forbids this child write access
help: the accessed tag <TAG> was created here
--> $DIR/buggy_split_at_mut.rs:LL:CC
|
Expand All @@ -22,7 22,7 @@ help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign
|
LL | a[1] = 5;
| ^^^^^^^^
= help: this corresponds to a loss of read and write permissions
= help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span):
= note: inside `main` at $DIR/buggy_split_at_mut.rs:LL:CC

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 5,7 @@ LL | unsafe { *x = 42 };
| ^^^^^^^ write access through <TAG> is forbidden
|
= 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> has state Frozen which forbids child write accesses
= help: the accessed tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Frozen
--> $DIR/illegal_write1.rs:LL:CC
|
Expand Down
Loading