mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

ask people to reach out if we declare too much UB

Browse Source
This commit is contained in:
Ralf Jung 2023-07-21 16:28:29 +02:00
parent b8b92db1ee
commit 3cdd2922cb
10 changed files with 31 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs
View File

@ -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,
@ -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)),
)
}
@ -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)),
)
}
@ -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, .. })
@ -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()))),
),
}
@ -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)),
)
}

11
src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
View File

@ -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::*;
@ -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:

5
src/tools/miri/src/diagnostics.rs
View File

@ -22,7 +22,7 @@ pub enum TerminationInfo {
UnsupportedInIsolation(String),
StackedBorrowsUb {
msg: String,
help: Option<String>,
help: Vec<String>,
history: Option<TagHistory>,
},
TreeBorrowsUb {
@ -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));

5
src/tools/miri/tests/fail/both_borrows/buggy_split_at_mut.stack.stderr
View File

@ -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

1
src/tools/miri/tests/fail/both_borrows/pass_invalid_shr_option.stack.stderr
View File

@ -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

1
src/tools/miri/tests/fail/both_borrows/pass_invalid_shr_tuple.stack.stderr
View File

@ -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

1
src/tools/miri/tests/fail/both_borrows/return_invalid_shr_option.stack.stderr
View File

@ -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

1
src/tools/miri/tests/fail/both_borrows/return_invalid_shr_tuple.stack.stderr
View File

@ -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

1
src/tools/miri/tests/fail/stacked_borrows/return_invalid_mut_option.stderr
View File

@ -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

1
src/tools/miri/tests/fail/stacked_borrows/return_invalid_mut_tuple.stderr
View File

@ -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