Skip to content

Commit

Permalink
ask people to reach out if we declare too much UB
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Jul 21, 2023
1 parent c5c0f85 commit ae3b961
Show file tree
Hide file tree
Showing 10 changed files with 31 additions and 22 deletions.
26 changes: 19 additions & 7 deletions src/borrow_tracker/stacked_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,19 @@ use rustc_span::{Span, SpanData};
use rustc_target::abi::Size;

use crate::borrow_tracker::{
stacked_borrows::{err_sb_ub, Permission},
AccessKind, GlobalStateInner, ProtectorKind,
stacked_borrows::Permission, AccessKind, GlobalStateInner, ProtectorKind,
};
use crate::*;

/// Error reporting
fn err_sb_ub<'tcx>(
msg: String,
help: Vec<String>,
history: Option<TagHistory>,
) -> InterpError<'tcx> {
err_machine_stop!(TerminationInfo::StackedBorrowsUb { msg, help, history })
}

#[derive(Clone, Debug)]
pub struct AllocHistory {
id: AllocId,
Expand Down Expand Up @@ -381,9 +389,13 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
self.history.id,
self.offset.bytes(),
);
let mut helps = vec![operation_summary(&op.info.summary(), self.history.id, op.range)];
if op.info.in_field {
helps.push(format!("errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling"));
}
err_sb_ub(
format!("{action}{}", error_cause(stack, op.orig_tag)),
Some(operation_summary(&op.info.summary(), self.history.id, op.range)),
helps,
op.orig_tag.and_then(|orig_tag| self.get_logs_relevant_to(orig_tag, None)),
)
}
Expand All @@ -406,7 +418,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
);
err_sb_ub(
format!("{action}{}", error_cause(stack, op.tag)),
Some(operation_summary("an access", self.history.id, op.range)),
vec![operation_summary("an access", self.history.id, op.range)],
op.tag.and_then(|tag| self.get_logs_relevant_to(tag, None)),
)
}
Expand All @@ -432,7 +444,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
Operation::Dealloc(_) =>
err_sb_ub(
format!("deallocating while item {item:?} is {protected} by call {call_id:?}",),
None,
vec![],
None,
),
Operation::Retag(RetagOp { orig_tag: tag, .. })
Expand All @@ -441,7 +453,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
format!(
"not granting access to tag {tag:?} because that would remove {item:?} which is {protected} because it is an argument of call {call_id:?}",
),
None,
vec![],
tag.and_then(|tag| self.get_logs_relevant_to(tag, Some(item.tag()))),
),
}
Expand All @@ -459,7 +471,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
alloc_id = self.history.id,
cause = error_cause(stack, op.tag),
),
None,
vec![],
op.tag.and_then(|tag| self.get_logs_relevant_to(tag, None)),
)
}
Expand Down
11 changes: 1 addition & 10 deletions src/borrow_tracker/stacked_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ use rustc_middle::ty::{
use rustc_target::abi::{Abi, Size};

use crate::borrow_tracker::{
stacked_borrows::diagnostics::{AllocHistory, DiagnosticCx, DiagnosticCxBuilder, TagHistory},
stacked_borrows::diagnostics::{AllocHistory, DiagnosticCx, DiagnosticCxBuilder},
AccessKind, GlobalStateInner, ProtectorKind, RetagFields,
};
use crate::*;
Expand Down Expand Up @@ -170,15 +170,6 @@ impl NewPermission {
}
}

/// Error reporting
pub fn err_sb_ub<'tcx>(
msg: String,
help: Option<String>,
history: Option<TagHistory>,
) -> InterpError<'tcx> {
err_machine_stop!(TerminationInfo::StackedBorrowsUb { msg, help, history })
}

// # Stacked Borrows Core Begin

/// We need to make at least the following things true:
Expand Down
5 changes: 2 additions & 3 deletions src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ pub enum TerminationInfo {
UnsupportedInIsolation(String),
StackedBorrowsUb {
msg: String,
help: Option<String>,
help: Vec<String>,
history: Option<TagHistory>,
},
TreeBorrowsUb {
Expand Down Expand Up @@ -224,11 +224,10 @@ pub fn report_error<'tcx, 'mir>(
(None, format!("or pass `-Zmiri-isolation-error=warn` to configure Miri to return an error code from isolated operations (if supported for that operation) and continue with a warning")),
],
StackedBorrowsUb { help, history, .. } => {
let url = "https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md";
msg.extend(help.clone());
let mut helps = vec![
(None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental")),
(None, format!("see {url} for further information")),
(None, format!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information")),
];
if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
helps.push((Some(created.1), created.0));
Expand Down
5 changes: 3 additions & 2 deletions tests/fail/both_borrows/buggy_split_at_mut.stack.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,9 @@ LL | | from_raw_parts_mut(ptr.offset(mid as isize), len - mid),
LL | | )
| | ^
| | |
| |_____________trying to retag from <TAG> for Unique permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x0..0x10]
| | trying to retag from <TAG> for Unique permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| |_____________this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x0..0x10]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ LL | foo(some_xref);
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x0..0x4]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ LL | foo(pair_xref);
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x0..0x4]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ LL | ret
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x4..0x8]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ LL | ret
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x4..0x8]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ LL | ret
| |
| trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x4..0x8]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
1 change: 1 addition & 0 deletions tests/fail/stacked_borrows/return_invalid_mut_tuple.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ LL | ret
| |
| trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag (of a reference/box inside this compound value) at ALLOC[0x4..0x8]
| errors for retagging in fields are fairly new; please reach out to us (e.g. at <https://rust-lang.zulipchat.com/#narrow/stream/269128-miri>) if you find this error troubling
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down

0 comments on commit ae3b961

Please sign in to comment.