Differentiate between explicit accesses and accesses inserted by TB

rust-lang · bors · Jun 29, 2023 · Nov 9, 2022 · Jun 2, 2023 · Jun 3, 2023
commit 7a1cdf71103cababb81d3c8d9bb4a0ac18777957
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
@@ -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,
@@ -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())));
  }
  }
 }
@@ -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,
@@ -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}"

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
@@ -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.
@@ -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)?;
  }

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
@@ -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(
@@ -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,
@@ -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 }
@@ -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,
@@ -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,

diff --git a/src/tools/miri/tests/fail/both_borrows/alias_through_mutation.tree.stderr b/src/tools/miri/tests/fail/both_borrows/alias_through_mutation.tree.stderr
@@ -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
  |
@@ -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
 

diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr
@@ -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`

diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr
@@ -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
  |
@@ -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`

diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr
@@ -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`

diff --git a/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr b/src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr
@@ -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
  |

diff --git a/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr b/src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr
@@ -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
  |
@@ -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`

diff --git a/src/tools/miri/tests/fail/both_borrows/buggy_as_mut_slice.tree.stderr b/src/tools/miri/tests/fail/both_borrows/buggy_as_mut_slice.tree.stderr
@@ -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
  |
@@ -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
 

diff --git a/src/tools/miri/tests/fail/both_borrows/buggy_split_at_mut.tree.stderr b/src/tools/miri/tests/fail/both_borrows/buggy_split_at_mut.tree.stderr
@@ -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
  |
@@ -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
 

diff --git a/src/tools/miri/tests/fail/both_borrows/illegal_write1.tree.stderr b/src/tools/miri/tests/fail/both_borrows/illegal_write1.tree.stderr
@@ -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
  |