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

Provide better notes when tracking a pointer tag

Browse Source
This commit is contained in:
Ben Kimock 2021-12-19 18:45:56 -05:00
parent e969615937
commit cd6921923c
2 changed files with 31 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/diagnostics.rs
View File

@ -7,6 +7,7 @@ use log::trace;
use rustc_middle::ty::{self, TyCtxt};
use rustc_span::{source_map::DUMMY_SP, Span, SpanData, Symbol};
use crate::stacked_borrows::{AccessKind, SbTag};
use crate::*;
/// Details of premature program termination.
@ -58,7 +59,9 @@ impl MachineStopType for TerminationInfo {}
/// Miri specific diagnostics
pub enum NonHaltingDiagnostic {
CreatedPointerTag(NonZeroU64),
PoppedPointerTag(Item),
/// This `Item` was popped from the borrow stack, either due to a grant of
/// `AccessKind` to `SbTag` or a deallocation when the second argument is `None`.
PoppedPointerTag(Item, Option<(SbTag, AccessKind)>),
CreatedCallId(CallId),
CreatedAlloc(AllocId),
FreedAlloc(AllocId),
@ -321,7 +324,20 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
use NonHaltingDiagnostic::*;
let msg = match e {
CreatedPointerTag(tag) => format!("created tag {:?}", tag),
PoppedPointerTag(item) => format!("popped tracked tag for item {:?}", item),
PoppedPointerTag(item, tag) =>
match tag {
None =>
format!(
"popped tracked tag for item {:?} due to deallocation",
item
),
Some((tag, access)) => {
format!(
"popped tracked tag for item {:?} due to {:?} access for {:?}",
item, access, tag
)
}
},
CreatedCallId(id) => format!("function call with id {}", id),
CreatedAlloc(AllocId(id)) => format!("created allocation with id {}", id),
FreedAlloc(AllocId(id)) => format!("freed allocation with id {}", id),

19
src/stacked_borrows.rs
View File

@ -111,7 +111,7 @@ pub struct GlobalState {
pub type MemoryExtra = RefCell<GlobalState>;
/// Indicates which kind of access is being performed.
#[derive(Copy, Clone, Hash, PartialEq, Eq)]
#[derive(Copy, Clone, Hash, PartialEq, Eq, Debug)]
pub enum AccessKind {
Read,
Write,
@ -296,19 +296,26 @@ impl<'tcx> Stack {
}
/// Check if the given item is protected.
///
/// The `provoking_access` argument is only used to produce diagnostics.
/// It is `Some` when we are granting the contained access for said tag, and it is
/// `None` during a deallocation.
fn check_protector(
item: &Item,
tag: Option<SbTag>,
provoking_access: Option<(SbTag, AccessKind)>,
global: &GlobalState,
) -> InterpResult<'tcx> {
if let SbTag::Tagged(id) = item.tag {
if Some(id) == global.tracked_pointer_tag {
register_diagnostic(NonHaltingDiagnostic::PoppedPointerTag(item.clone()));
register_diagnostic(NonHaltingDiagnostic::PoppedPointerTag(
item.clone(),
provoking_access,
));
}
}
if let Some(call) = item.protector {
if global.is_active(call) {
if let Some(tag) = tag {
if let Some((tag, _)) = provoking_access {
Err(err_sb_ub(format!(
"not granting access to tag {:?} because incompatible item is protected: {:?}",
tag, item
@ -348,7 +355,7 @@ impl<'tcx> Stack {
let first_incompatible_idx = self.find_first_write_incompatible(granting_idx);
for item in self.borrows.drain(first_incompatible_idx..).rev() {
trace!("access: popping item {:?}", item);
Stack::check_protector(&item, Some(tag), global)?;
Stack::check_protector(&item, Some((tag, access)), global)?;
}
} else {
// On a read, *disable* all `Unique` above the granting item. This ensures U2 for read accesses.
@ -363,7 +370,7 @@ impl<'tcx> Stack {
let item = &mut self.borrows[idx];
if item.perm == Permission::Unique {
trace!("access: disabling item {:?}", item);
Stack::check_protector(item, Some(tag), global)?;
Stack::check_protector(item, Some((tag, access)), global)?;
item.perm = Permission::Disabled;
}
}