Auto merge of rust-lang#3343 - RalfJung:tree-borrows-diag, r=RalfJung

Tree Borrows diagnostic improvements print where the forbidden access happens; make tag tracking less verbose

Author: bors

src/tools/miri/src/borrow_tracker/mod.rs

@@ -377,7 +377,12 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
  if matches!(kind, AllocKind::LiveData) {
  let alloc_extra = this.get_alloc_extra(*alloc_id)?; // can still fail for `extern static`
  let alloc_borrow_tracker = &alloc_extra.borrow_tracker.as_ref().unwrap();
- alloc_borrow_tracker.release_protector(&this.machine, borrow_tracker, *tag)?;
+ alloc_borrow_tracker.release_protector(
+ &this.machine,
+ borrow_tracker,
+ *tag,
+ *alloc_id,
+ )?;
  }
  }
  borrow_tracker.borrow_mut().end_call(&frame.extra);
@@ -491,10 +496,12 @@ impl AllocState {
  machine: &MiriMachine<'_, 'tcx>,
  global: &GlobalState,
  tag: BorTag,
+ alloc_id: AllocId, // diagnostics
  ) -> InterpResult<'tcx> {
  match self {
  AllocState::StackedBorrows(_sb) => Ok(()),
- AllocState::TreeBorrows(tb) => tb.borrow_mut().release_protector(machine, global, tag),
+ AllocState::TreeBorrows(tb) =>
+ tb.borrow_mut().release_protector(machine, global, tag, alloc_id),
  }
  }
 }

src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs

@@ -278,6 +278,8 @@ impl History {
 pub(super) struct TbError<'node> {
  /// What failure occurred.
  pub error_kind: TransitionError,
+ /// The allocation in which the error is happening.
+ pub alloc_id: AllocId,
  /// The offset (into the allocation) at which the conflict occurred.
  pub error_offset: u64,
  /// The tag on which the error was triggered.
@@ -300,7 +302,11 @@ impl TbError<'_> {
  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 = format!(
+ "{cause} through {accessed} at {alloc_id:?}[{offset:#x}] is forbidden",
+ alloc_id = self.alloc_id,
+ offset = self.error_offset
+ );
  let (title, details, conflicting_tag_name) = match self.error_kind {
  ChildAccessForbidden(perm) => {
  let conflicting_tag_name =

src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

@@ -1,6 +1,3 @@
-use rustc_target::abi::{Abi, Size};
-
-use crate::borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind};
 use rustc_middle::{
  mir::{Mutability, RetagKind},
  ty::{
@@ -10,7 +7,9 @@ use rustc_middle::{
  },
 };
 use rustc_span::def_id::DefId;
+use rustc_target::abi::{Abi, Size};
 
+use crate::borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind};
 use crate::*;
 
 pub mod diagnostics;
@@ -70,6 +69,7 @@ impl<'tcx> Tree {
  tag,
  Some(range),
  global,
+ alloc_id,
  span,
  diagnostics::AccessCause::Explicit(access_kind),
  )
@@ -78,7 +78,7 @@ impl<'tcx> Tree {
  /// Check that this pointer has permission to deallocate this range.
  pub fn before_memory_deallocation(
  &mut self,
- _alloc_id: AllocId,
+ alloc_id: AllocId,
  prov: ProvenanceExtra,
  range: AllocRange,
  machine: &MiriMachine<'_, 'tcx>,
@@ -91,7 +91,7 @@ impl<'tcx> Tree {
  };
  let global = machine.borrow_tracker.as_ref().unwrap();
  let span = machine.current_span();
- self.dealloc(tag, range, global, span)
+ self.dealloc(tag, range, global, alloc_id, span)
  }
 
  pub fn expose_tag(&mut self, _tag: BorTag) {
@@ -109,13 +109,15 @@ impl<'tcx> Tree {
  machine: &MiriMachine<'_, 'tcx>,
  global: &GlobalState,
  tag: BorTag,
+ alloc_id: AllocId, // diagnostics
  ) -> InterpResult<'tcx> {
  let span = machine.current_span();
  self.perform_access(
  AccessKind::Read,
  tag,
  None, // no specified range because it occurs on the entire allocation
  global,
+ alloc_id,
  span,
  diagnostics::AccessCause::FnExit,
  )
@@ -211,7 +213,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
  let global = this.machine.borrow_tracker.as_ref().unwrap().borrow();
  let ty = place.layout.ty;
  if global.tracked_pointer_tags.contains(&new_tag) {
- let kind_str = format!("{new_perm:?} (pointee type {ty})");
+ let kind_str = format!("initial state {} (pointee type {ty})", new_perm.initial_state);
  this.emit_diagnostic(NonHaltingDiagnostic::CreatedPointerTag(
  new_tag.inner(),
  Some(kind_str),
@@ -299,6 +301,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
  orig_tag,
  Some(range),
  this.machine.borrow_tracker.as_ref().unwrap(),
+ alloc_id,
  this.machine.current_span(),
  diagnostics::AccessCause::Reborrow,
  )?;

src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs

@@ -516,13 +516,15 @@ impl<'tcx> Tree {
  tag: BorTag,
  access_range: AllocRange,
  global: &GlobalState,
- span: Span, // diagnostics
+ alloc_id: AllocId, // diagnostics
+ span: Span, // diagnostics
  ) -> InterpResult<'tcx> {
  self.perform_access(
  AccessKind::Write,
  tag,
  Some(access_range),
  global,
+ alloc_id,
  span,
  diagnostics::AccessCause::Dealloc,
  )?;
@@ -545,6 +547,7 @@ impl<'tcx> Tree {
  TbError {
  conflicting_info,
  access_cause: diagnostics::AccessCause::Dealloc,
+ alloc_id,
  error_offset: perms_range.start,
  error_kind,
  accessed_info,
@@ -576,6 +579,7 @@ impl<'tcx> Tree {
  tag: BorTag,
  access_range: Option<AllocRange>,
  global: &GlobalState,
+ alloc_id: AllocId, // diagnostics
  span: Span, // diagnostics
  access_cause: diagnostics::AccessCause, // diagnostics
  ) -> InterpResult<'tcx> {
@@ -628,6 +632,7 @@ impl<'tcx> Tree {
  TbError {
  conflicting_info,
  access_cause,
+ alloc_id,
  error_offset: perms_range.start,
  error_kind,
  accessed_info,

src/tools/miri/tests/fail/both_borrows/alias_through_mutation.tree.stderr

@@ -1,8 +1,8 @@
-error: Undefined Behavior: read access through <TAG> is forbidden
+error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden
  --> $DIR/alias_through_mutation.rs:LL:CC
  |
 LL | let _val = *target_alias;
- | ^^^^^^^^^^^^^ read access through <TAG> is forbidden
+ | ^^^^^^^^^^^^^ read access through <TAG> at ALLOC[0x0] 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> is a child of the conflicting tag <TAG>

src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr

@@ -1,8 +1,8 @@
-error: Undefined Behavior: write access through <TAG> is forbidden
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
  --> $DIR/aliasing_mut1.rs:LL:CC
  |
 LL | *x = 1;
- | ^^^^^^ write access through <TAG> is forbidden
+ | ^^^^^^ write access through <TAG> at ALLOC[0x0] 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 Reserved (conflicted) which forbids this child write access

src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr

@@ -1,8 +1,8 @@
-error: Undefined Behavior: write access through <TAG> is forbidden
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
  --> $DIR/aliasing_mut2.rs:LL:CC
  |
 LL | *y = 2;
- | ^^^^^^ write access through <TAG> is forbidden
+ | ^^^^^^ write access through <TAG> at ALLOC[0x0] 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 Reserved (conflicted) which forbids this child write access

src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr

@@ -1,8 +1,8 @@
-error: Undefined Behavior: write access through <TAG> is forbidden
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
  --> $DIR/aliasing_mut3.rs:LL:CC
  |
 LL | *x = 1;
- | ^^^^^^ write access through <TAG> is forbidden
+ | ^^^^^^ write access through <TAG> at ALLOC[0x0] 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 Reserved (conflicted) which forbids this child write access

src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr

@@ -1,8 +1,8 @@
-error: Undefined Behavior: write access through <TAG> is forbidden
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
  --> RUSTLIB/core/src/mem/mod.rs:LL:CC
  |
 LL | ptr::write(dest, src);
- | ^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> is forbidden
+ | ^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] 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> is foreign to the protected tag <TAG> (i.e., it is not a child)

src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr

@@ -1,8 +1,8 @@
-error: Undefined Behavior: write access through <TAG> is forbidden
+error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
  --> $DIR/box_exclusive_violation1.rs:LL:CC
  |
 LL | *LEAK = 7;
- | ^^^^^^^^^ write access through <TAG> is forbidden
+ | ^^^^^^^^^ write access through <TAG> at ALLOC[0x0] 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> is a child of the conflicting tag <TAG>