From fe178ccb72ab824bc62a011a00e8a821332a068c Mon Sep 17 00:00:00 2001
From: Neven Villani <vanille@crans.org>
Date: Wed, 29 Mar 2023 22:17:33 +0200
Subject: [PATCH 1/2] Tree Borrows: improved diagnostics

---
 .../tree_borrows/diagnostics.rs               | 240 +++++++++++++++---
 .../src/borrow_tracker/tree_borrows/mod.rs    |  21 +-
 .../src/borrow_tracker/tree_borrows/perms.rs  | 200 ++++++++++-----
 .../src/borrow_tracker/tree_borrows/tree.rs   |  93 ++++---
 src/tools/miri/src/diagnostics.rs             |  23 +-
 .../tree-borrows/alternate-read-write.stderr  |  30 ++-
 .../tests/fail/tree-borrows/error-range.rs    |  27 ++
 .../fail/tree-borrows/error-range.stderr      |  44 ++++
 .../tree-borrows/fragile-data-race.stderr     |  24 +-
 .../fail/tree-borrows/outside-range.stderr    |  18 +-
 .../fail/tree-borrows/read-to-local.stderr    |  25 +-
 .../reserved/cell-protected-write.stderr      |  29 ++-
 .../reserved/int-protected-write.stderr       |  29 ++-
 .../fail/tree-borrows/strongly-protected.rs   |  14 +
 .../tree-borrows/strongly-protected.stderr    |  49 ++++
 .../tree-borrows/write-during-2phase.stderr   |  25 +-
 .../tree-borrows/cell-alternate-writes.stderr |   6 +-
 .../pass/tree-borrows/end-of-protector.stderr |  36 +--
 .../tests/pass/tree-borrows/formatting.stderr |  48 ++--
 .../pass/tree-borrows/reborrow-is-read.stderr |  12 +-
 .../tests/pass/tree-borrows/reserved.stderr   |  50 ++--
 21 files changed, 799 insertions(+), 244 deletions(-)
 create mode 100644 src/tools/miri/tests/fail/tree-borrows/error-range.rs
 create mode 100644 src/tools/miri/tests/fail/tree-borrows/error-range.stderr
 create mode 100644 src/tools/miri/tests/fail/tree-borrows/strongly-protected.rs
 create mode 100644 src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
index 97bbdee1d4424..18d540dfd1a69 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
@@ -1,14 +1,90 @@
-use rustc_data_structures::fx::FxHashMap;
-
 use std::fmt;
 use std::ops::Range;
 
+use rustc_data_structures::fx::FxHashMap;
+use rustc_span::{Span, SpanData};
+use rustc_target::abi::Size;
+
 use crate::borrow_tracker::tree_borrows::{
-    err_tb_ub, perms::Permission, tree::LocationState, unimap::UniIndex,
+    perms::{PermTransition, Permission},
+    tree::LocationState,
+    unimap::UniIndex,
 };
 use crate::borrow_tracker::{AccessKind, ProtectorKind};
 use crate::*;
 
+/// Complete data for an event:
+/// - `kind` is what happened to the permissions
+/// - `access_kind` and `access_range` describe the access that caused the event
+/// - `offset` allows filtering only the relevant events for a given memory location
+/// (see how we perform the filtering in `History::extract_relevant`.
+/// - `span` is the line of code in question
+#[derive(Clone, Debug)]
+pub struct Event {
+    pub transition: PermTransition,
+    pub access_kind: AccessKind,
+    pub is_foreign: bool,
+    pub access_range: AllocRange,
+    pub offset: Size,
+    pub span: Span,
+}
+
+/// List of all events that affected a tag.
+/// NOTE: not all of these events are relevant for a particular location,
+/// the events should be filtered before the generation of diagnostics.
+/// Available filtering methods include `History::forget` and `History::extract_relevant`.
+#[derive(Clone, Debug)]
+pub struct History {
+    pub tag: BorTag,
+    pub created: (Span, Permission),
+    pub events: Vec<Event>,
+}
+
+/// History formatted for use by `src/diagnostics.rs`.
+///
+/// NOTE: needs to be `Send` because of a bound on `MachineStopType`, hence
+/// the use of `SpanData` rather than `Span`.
+#[derive(Debug, Clone, Default)]
+pub struct HistoryData {
+    pub events: Vec<(Option<SpanData>, String)>, // includes creation
+}
+
+impl History {
+    /// Record an additional event to the history.
+    pub fn push(&mut self, event: Event) {
+        self.events.push(event);
+    }
+}
+
+impl HistoryData {
+    // Format events from `new_history` into those recorded by `self`.
+    //
+    // NOTE: also converts `Span` to `SpanData`.
+    pub fn extend(
+        &mut self,
+        new_history: History,
+        tag_name: &'static str,
+        show_initial_state: bool,
+    ) {
+        let History { tag, created, events } = new_history;
+        let this = format!("the {tag_name} tag {tag:?}");
+        let msg_initial_state = format!(", in the initial state {}", created.1);
+        let msg_creation = format!(
+            "{this} was created here{maybe_msg_initial_state}.",
+            maybe_msg_initial_state = if show_initial_state { &msg_initial_state } else { "" },
+        );
+
+        self.events.push((Some(created.0.data()), msg_creation));
+        for &Event { transition, access_kind, is_foreign, access_range, span, offset: _ } in &events
+        {
+            // NOTE: `offset` 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} then transitioned {transition} due to a {rel} {access_kind} at offsets {access_range:?}.", rel = if is_foreign { "foreign" } else { "child" })));
+            self.events.push((None, format!("this corresponds to {}.", transition.summary())));
+        }
+    }
+}
+
 /// Some information that is irrelevant for the algorithm but very
 /// convenient to know about a tag for debugging and testing.
 #[derive(Clone, Debug)]
@@ -20,18 +96,29 @@ pub struct NodeDebugInfo {
     /// pointer in the source code.
     /// Helps match tag numbers to human-readable names.
     pub name: Option<String>,
+    /// Notable events in the history of this tag, used for
+    /// diagnostics.
+    ///
+    /// NOTE: by virtue of being part of `NodeDebugInfo`,
+    /// the history is automatically cleaned up by the GC.
+    /// NOTE: this is `!Send`, it needs to be converted before displaying
+    /// the actual diagnostics because `src/diagnostics.rs` requires `Send`.
+    pub history: History,
 }
+
 impl NodeDebugInfo {
-    /// New node info with a name.
-    pub fn new(tag: BorTag) -> Self {
-        Self { tag, name: None }
+    /// Information for a new node. By default it has no
+    /// name and an empty history.
+    pub fn new(tag: BorTag, initial: Permission, span: Span) -> Self {
+        let history = History { tag, created: (span, initial), events: Vec::new() };
+        Self { tag, name: None, history }
     }
 
     /// Add a name to the tag. If a same tag is associated to several pointers,
     /// it can have several names which will be separated by commas.
-    fn add_name(&mut self, name: &str) {
+    pub fn add_name(&mut self, name: &str) {
         if let Some(ref mut prev_name) = &mut self.name {
-            prev_name.push(',');
+            prev_name.push_str(", ");
             prev_name.push_str(name);
         } else {
             self.name = Some(String::from(name));
@@ -42,7 +129,7 @@ impl NodeDebugInfo {
 impl fmt::Display for NodeDebugInfo {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         if let Some(ref name) = self.name {
-            write!(f, "{tag:?} (also named '{name}')", tag = self.tag)
+            write!(f, "{tag:?} ({name})", tag = self.tag)
         } else {
             write!(f, "{tag:?}", tag = self.tag)
         }
@@ -86,7 +173,7 @@ impl<'tcx> Tree {
     }
 }
 
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone, Copy, PartialEq)]
 pub(super) enum TransitionError {
     /// This access is not allowed because some parent tag has insufficient permissions.
     /// For example, if a tag is `Frozen` and encounters a child write this will
@@ -96,63 +183,146 @@ pub(super) enum TransitionError {
     /// A protector was triggered due to an invalid transition that loses
     /// too much permissions.
     /// For example, if a protected tag goes from `Active` to `Frozen` due
-    /// to a foreign write this will produce a `ProtectedTransition(Active, Frozen)`.
+    /// to a foreign write this will produce a `ProtectedTransition(PermTransition(Active, Frozen))`.
     /// This kind of error can only occur on foreign accesses.
-    ProtectedTransition(Permission, Permission),
+    ProtectedTransition(PermTransition),
     /// Cannot deallocate because some tag in the allocation is strongly protected.
     /// This kind of error can only occur on deallocations.
     ProtectedDealloc,
 }
 
+impl History {
+    /// Keep only the tag and creation
+    fn forget(&self) -> Self {
+        History { events: Vec::new(), created: self.created, tag: self.tag }
+    }
+
+    /// Reconstruct the history relevant to `error_offset` knowing that
+    /// its permission followed `complete_transition`.
+    ///
+    /// Here's how we do this:
+    /// - we know `full := complete_transition` the transition of the permission from
+    /// its initialization to the state just before the error was caused,
+    /// we want to find a chain of events that produces `full`
+    /// - we decompose `full` into `pre o post` where
+    /// `pre` is the best applicable transition from recorded events
+    /// - we select the event that caused `pre` and iterate
+    /// to find the chain of events that produces `full := post`
+    ///
+    /// To find the "best applicable transition" for full:
+    /// - eliminate events that cannot be applied because their offset is too big
+    /// - eliminate events that cannot be applied because their starting point is wrong
+    /// - select the one that happened closest to the range of interest
+    fn extract_relevant(&self, complete_transition: PermTransition, error_offset: Size) -> Self {
+        let mut selected_events: Vec<Event> = Vec::new();
+        let mut full = complete_transition;
+        while !full.is_noop() {
+            let (pre, post) = self
+                .events
+                .iter()
+                .filter(|e| e.offset <= error_offset)
+                .filter_map(|pre_canditate| {
+                    full.apply_start(pre_canditate.transition)
+                        .map(|post_canditate| (pre_canditate, post_canditate))
+                })
+                .max_by_key(|(pre_canditate, _post_candidate)| pre_canditate.offset)
+                .unwrap();
+            // If this occurs we will loop infinitely !
+            // Make sure to only put non-noop transitions in `History`.
+            assert!(!pre.transition.is_noop());
+            full = post;
+            selected_events.push(pre.clone());
+        }
+
+        History { events: selected_events, created: self.created, tag: self.tag }
+    }
+}
+
 /// Failures that can occur during the execution of Tree Borrows procedures.
 pub(super) struct TbError<'node> {
     /// What failure occurred.
     pub error_kind: TransitionError,
+    /// The byte at which the conflict occured.
+    pub error_offset: Size,
     /// The tag on which the error was triggered.
     /// On protector violations, this is the tag that was protected.
     /// On accesses rejected due to insufficient permissions, this is the
     /// tag that lacked those permissions.
-    pub faulty_tag: &'node NodeDebugInfo,
+    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,
     /// Which tag the access that caused this error was made through, i.e.
     /// which tag was used to read/write/deallocate.
-    pub tag_of_access: &'node NodeDebugInfo,
+    pub accessed_info: &'node NodeDebugInfo,
 }
 
 impl TbError<'_> {
     /// Produce a UB error.
-    pub fn build<'tcx>(self) -> InterpErrorInfo<'tcx> {
+    pub fn build<'tcx>(self) -> InterpError<'tcx> {
         use TransitionError::*;
-        err_tb_ub(match self.error_kind {
+        let started_as = self.conflicting_info.history.created.1;
+        let kind = self.access_kind;
+        let accessed = self.accessed_info;
+        let conflicting = self.conflicting_info;
+        let accessed_is_conflicting = accessed.tag == conflicting.tag;
+        let (pre_error, title, relation, problem, conflicting_tag_name) = match self.error_kind {
             ChildAccessForbidden(perm) => {
-                format!(
-                    "{kind} through {initial} is forbidden because it is a child of {current} which is {perm}.",
-                    kind=self.access_kind,
-                    initial=self.tag_of_access,
-                    current=self.faulty_tag,
-                    perm=perm,
+                let conflicting_tag_name =
+                    if accessed_is_conflicting { "accessed" } else { "conflicting" };
+                (
+                    perm,
+                    format!("{kind} through {accessed} is forbidden."),
+                    (!accessed_is_conflicting).then_some(format!(
+                        "the accessed tag {accessed} is a child of the conflicting tag {conflicting}."
+                    )),
+                    format!(
+                        "the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids child {kind}es."
+                    ),
+                    conflicting_tag_name,
                 )
             }
-            ProtectedTransition(start, end) => {
-                format!(
-                    "{kind} through {initial} is forbidden because it is a foreign tag for {current}, which would hence change from {start} to {end}, but {current} is protected",
-                    current=self.faulty_tag,
-                    start=start,
-                    end=end,
-                    kind=self.access_kind,
-                    initial=self.tag_of_access,
+            ProtectedTransition(transition) => {
+                let conflicting_tag_name = "protected";
+                (
+                    transition.started(),
+                    format!("{kind} through {accessed} is forbidden."),
+                    Some(format!(
+                        "the accessed tag {accessed} is a foreign tag for the {conflicting_tag_name} tag {conflicting}."
+                    )),
+                    format!(
+                        "the access would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}. This is {loss}, which is not allowed for protected tags.",
+                        loss = transition.summary(),
+                    ),
+                    conflicting_tag_name,
                 )
             }
             ProtectedDealloc => {
-                format!(
-                    "the allocation of {initial} also contains {current} which is strongly protected, cannot deallocate",
-                    initial=self.tag_of_access,
-                    current=self.faulty_tag,
+                let conflicting_tag_name = "strongly protected";
+                (
+                    started_as,
+                    format!("deallocation through {accessed} is forbidden."),
+                    Some(format!(
+                        "the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}."
+                    )),
+                    format!(
+                        "the {conflicting_tag_name} tag {conflicting} disallows deallocations."
+                    ),
+                    conflicting_tag_name,
                 )
             }
-        }).into()
+        };
+        let pre_transition = PermTransition::from(started_as, pre_error).unwrap();
+        let mut history = HistoryData::default();
+        if !accessed_is_conflicting {
+            history.extend(self.accessed_info.history.forget(), "accessed", false);
+        }
+        history.extend(
+            self.conflicting_info.history.extract_relevant(pre_transition, self.error_offset),
+            conflicting_tag_name,
+            true,
+        );
+        err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, relation, problem, history })
     }
 }
 
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
index f73b2554ad88b..3361d212f2c08 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
@@ -14,7 +14,7 @@ use rustc_middle::{
 
 use crate::*;
 
-mod diagnostics;
+pub mod diagnostics;
 mod perms;
 mod tree;
 mod unimap;
@@ -23,10 +23,6 @@ pub use tree::Tree;
 
 pub type AllocState = Tree;
 
-pub fn err_tb_ub<'tcx>(msg: String) -> InterpError<'tcx> {
-    err_machine_stop!(TerminationInfo::TreeBorrowsUb { msg })
-}
-
 impl<'tcx> Tree {
     /// Create a new allocation, i.e. a new tree
     pub fn new_allocation(
@@ -37,7 +33,8 @@ impl<'tcx> Tree {
         machine: &MiriMachine<'_, 'tcx>,
     ) -> Self {
         let tag = state.base_ptr_tag(id, machine); // Fresh tag for the root
-        Tree::new(tag, size)
+        let span = machine.current_span();
+        Tree::new(tag, size, span)
     }
 
     /// Check that an access on the entire range is permitted, and update
@@ -64,7 +61,8 @@ impl<'tcx> Tree {
             ProvenanceExtra::Wildcard => return Ok(()),
         };
         let global = machine.borrow_tracker.as_ref().unwrap();
-        self.perform_access(access_kind, tag, range, global)
+        let span = machine.current_span();
+        self.perform_access(access_kind, tag, range, global, span)
     }
 
     /// Check that this pointer has permission to deallocate this range.
@@ -82,7 +80,8 @@ impl<'tcx> Tree {
             ProvenanceExtra::Wildcard => return Ok(()),
         };
         let global = machine.borrow_tracker.as_ref().unwrap();
-        self.dealloc(tag, range, global)
+        let span = machine.current_span();
+        self.dealloc(tag, range, global, span)
     }
 
     pub fn expose_tag(&mut self, _tag: BorTag) {
@@ -265,6 +264,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                 .insert(new_tag, protect);
         }
 
+        let span = this.machine.current_span();
         let alloc_extra = this.get_alloc_extra(alloc_id)?;
         let range = alloc_range(base_offset, ptr_size);
         let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
@@ -272,14 +272,15 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
         if new_perm.perform_read_access {
             // Count this reborrow as a read access
             let global = &this.machine.borrow_tracker.as_ref().unwrap();
-            tree_borrows.perform_access(AccessKind::Read, orig_tag, range, global)?;
+            let span = this.machine.current_span();
+            tree_borrows.perform_access(AccessKind::Read, orig_tag, range, global, span)?;
             if let Some(data_race) = alloc_extra.data_race.as_ref() {
                 data_race.read(alloc_id, range, &this.machine)?;
             }
         }
 
         // Record the parent-child pair in the tree.
-        tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range)?;
+        tree_borrows.new_child(orig_tag, new_tag, new_perm.initial_state, range, span)?;
         Ok(Some((alloc_id, new_tag)))
     }
 
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
index 3b4fcfd190be9..7e3e587db7248 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
@@ -4,7 +4,7 @@ use std::fmt;
 use crate::borrow_tracker::tree_borrows::tree::AccessRelatedness;
 use crate::borrow_tracker::AccessKind;
 
-/// The activation states of a pointer
+/// The activation states of a pointer.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 enum PermissionPriv {
     /// represents: a local reference that has not yet been written to;
@@ -112,47 +112,14 @@ mod transition {
     }
 }
 
-impl PermissionPriv {
-    /// Determines whether a transition that occurred is compatible with the presence
-    /// of a Protector. This is not included in the `transition` functions because
-    /// it would distract from the few places where the transition is modified
-    /// because of a protector, but not forbidden.
-    fn protector_allows_transition(self, new: Self) -> bool {
-        match (self, new) {
-            _ if self == new => true,
-            // It is always a protector violation to not be readable anymore
-            (_, Disabled) => false,
-            // In the case of a `Reserved` under a protector, both transitions
-            // `Reserved => Active` and `Reserved => Frozen` can legitimately occur.
-            // The first is standard (Child Write), the second is for Foreign Writes
-            // on protected Reserved where we must ensure that the pointer is not
-            // written to in the future.
-            (Reserved { .. }, Active) | (Reserved { .. }, Frozen) => true,
-            // This pointer should have stayed writeable for the whole function
-            (Active, Frozen) => false,
-            _ => unreachable!("Transition from {self:?} to {new:?} should never be possible"),
-        }
-    }
-}
-
 /// Public interface to the state machine that controls read-write permissions.
+/// This is the "private `enum`" pattern.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub struct Permission(PermissionPriv);
 
-impl fmt::Display for Permission {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(
-            f,
-            "{}",
-            match self.0 {
-                PermissionPriv::Reserved { .. } => "Reserved",
-                PermissionPriv::Active => "Active",
-                PermissionPriv::Frozen => "Frozen",
-                PermissionPriv::Disabled => "Disabled",
-            }
-        )
-    }
-}
+/// Transition from one permission to the next.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct PermTransition(PermissionPriv, PermissionPriv);
 
 impl Permission {
     /// Default initial permission of the root of a new tree.
@@ -170,43 +137,148 @@ impl Permission {
         Self(Frozen)
     }
 
-    /// Pretty-printing. Needs to be here and not in diagnostics.rs
-    /// because `Self` is private.
-    pub fn short_name(self) -> &'static str {
-        // Make sure there are all of the same length as each other
-        // and also as `diagnostics::DisplayFmtPermission.uninit` otherwise
-        // alignment will be incorrect.
-        match self.0 {
-            Reserved { ty_is_freeze: true } => "Res",
-            Reserved { ty_is_freeze: false } => "Re*",
-            Active => "Act",
-            Frozen => "Frz",
-            Disabled => "Dis",
-        }
+    /// Apply the transition to the inner PermissionPriv.
+    pub fn perform_access(
+        kind: AccessKind,
+        rel_pos: AccessRelatedness,
+        old_perm: Self,
+        protected: bool,
+    ) -> Option<PermTransition> {
+        let old_state = old_perm.0;
+        transition::perform_access(kind, rel_pos, old_state, protected)
+            .map(|new_state| PermTransition(old_state, new_state))
     }
+}
 
-    /// Check that there are no complaints from a possible protector.
+impl PermTransition {
+    /// All transitions created through normal means (using `perform_access`)
+    /// should be possible, but the same is not guaranteed by construction of
+    /// transitions inferred by diagnostics. This checks that a transition
+    /// reconstructed by diagnostics is indeed one that could happen.
+    fn is_possible(old: PermissionPriv, new: PermissionPriv) -> bool {
+        old <= new
+    }
+
+    pub fn from(old: Permission, new: Permission) -> Option<Self> {
+        Self::is_possible(old.0, new.0).then_some(Self(old.0, new.0))
+    }
+
+    pub fn is_noop(self) -> bool {
+        self.0 == self.1
+    }
+
+    /// Extract result of a transition (checks that the starting point matches).
+    pub fn applied(self, starting_point: Permission) -> Option<Permission> {
+        (starting_point.0 == self.0).then_some(Permission(self.1))
+    }
+
+    /// Extract starting point of a transition
+    pub fn started(self) -> Permission {
+        Permission(self.0)
+    }
+
+    /// Determines whether a transition that occured is compatible with the presence
+    /// of a Protector. This is not included in the `transition` functions because
+    /// it would distract from the few places where the transition is modified
+    /// because of a protector, but not forbidden.
     ///
     /// Note: this is not in charge of checking that there *is* a protector,
     /// it should be used as
     /// ```
     /// let no_protector_error = if is_protected(tag) {
-    ///     old_perm.protector_allows_transition(new_perm)
+    ///     transition.is_allowed_by_protector()
     /// };
     /// ```
-    pub fn protector_allows_transition(self, new: Self) -> bool {
-        self.0.protector_allows_transition(new.0)
+    pub fn is_allowed_by_protector(&self) -> bool {
+        let &Self(old, new) = self;
+        assert!(Self::is_possible(old, new));
+        match (old, new) {
+            _ if old == new => true,
+            // It is always a protector violation to not be readable anymore
+            (_, Disabled) => false,
+            // In the case of a `Reserved` under a protector, both transitions
+            // `Reserved => Active` and `Reserved => Frozen` can legitimately occur.
+            // The first is standard (Child Write), the second is for Foreign Writes
+            // on protected Reserved where we must ensure that the pointer is not
+            // written to in the future.
+            (Reserved { .. }, Active) | (Reserved { .. }, Frozen) => true,
+            // This pointer should have stayed writeable for the whole function
+            (Active, Frozen) => false,
+            _ => unreachable!("Transition from {old:?} to {new:?} should never be possible"),
+        }
     }
 
-    /// Apply the transition to the inner PermissionPriv.
-    pub fn perform_access(
-        kind: AccessKind,
-        rel_pos: AccessRelatedness,
-        old_perm: Self,
-        protected: bool,
-    ) -> Option<Self> {
-        let old_state = old_perm.0;
-        transition::perform_access(kind, rel_pos, old_state, protected).map(Self)
+    /// Composition function: get the transition that can be added after `app` to
+    /// produce `self`.
+    pub fn apply_start(self, app: Self) -> Option<Self> {
+        let new_start = app.applied(Permission(self.0))?;
+        Self::from(new_start, Permission(self.1))
+    }
+}
+
+pub mod diagnostics {
+    use super::*;
+    impl fmt::Display for PermissionPriv {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(
+                f,
+                "{}",
+                match self {
+                    PermissionPriv::Reserved { .. } => "Reserved",
+                    PermissionPriv::Active => "Active",
+                    PermissionPriv::Frozen => "Frozen",
+                    PermissionPriv::Disabled => "Disabled",
+                }
+            )
+        }
+    }
+
+    impl fmt::Display for PermTransition {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "from {} to {}", self.0, self.1)
+        }
+    }
+
+    impl fmt::Display for Permission {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "{}", self.0)
+        }
+    }
+
+    impl Permission {
+        /// Abbreviated name of the permission (uniformly 3 letters for nice alignment).
+        pub fn short_name(self) -> &'static str {
+            // Make sure there are all of the same length as each other
+            // and also as `diagnostics::DisplayFmtPermission.uninit` otherwise
+            // alignment will be incorrect.
+            match self.0 {
+                Reserved { ty_is_freeze: true } => "Res",
+                Reserved { ty_is_freeze: false } => "Re*",
+                Active => "Act",
+                Frozen => "Frz",
+                Disabled => "Dis",
+            }
+        }
+    }
+
+    impl PermTransition {
+        /// Readable explanation of the consequences of an event.
+        /// Fits in the sentence "This accessed caused {trans.summary()}".
+        ///
+        /// Important: for the purposes of this explanation, `Reserved` is considered
+        /// to have write permissions, because that's what the diagnostics care about
+        /// (otherwise `Reserved -> Frozen` would be considered a noop).
+        pub fn summary(&self) -> &'static str {
+            assert!(Self::is_possible(self.0, self.1));
+            match (self.0, self.1) {
+                (_, Active) => "an activation",
+                (_, Frozen) => "a loss of write permissions",
+                (Frozen, Disabled) => "a loss of read permissions",
+                (_, Disabled) => "a loss of read and write permissions",
+                (old, new) =>
+                    unreachable!("Transition from {old:?} to {new:?} should never be possible"),
+            }
+        }
     }
 }
 
diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
index 4477ce0191fee..6392f5101ad5f 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
@@ -14,10 +14,11 @@ use smallvec::SmallVec;
 
 use rustc_const_eval::interpret::InterpResult;
 use rustc_data_structures::fx::FxHashSet;
+use rustc_span::Span;
 use rustc_target::abi::Size;
 
 use crate::borrow_tracker::tree_borrows::{
-    diagnostics::{NodeDebugInfo, TbError, TransitionError},
+    diagnostics::{self, NodeDebugInfo, TbError, TransitionError},
     unimap::{UniEntry, UniIndex, UniKeyMap, UniValMap},
     Permission,
 };
@@ -118,7 +119,7 @@ pub(super) struct Node {
 /// Data given to the transition function
 struct NodeAppArgs<'node> {
     /// Node on which the transition is currently being applied
-    node: &'node Node,
+    node: &'node mut Node,
     /// Mutable access to its permissions
     perm: UniEntry<'node, LocationState>,
     /// Relative position of the access
@@ -131,14 +132,17 @@ struct ErrHandlerArgs<'node, InErr> {
     /// Tag that triggered the error (not the tag that was accessed,
     /// rather the parent tag that had insufficient permissions or the
     /// non-parent tag that had a protector).
-    faulty_tag: &'node NodeDebugInfo,
+    conflicting_info: &'node NodeDebugInfo,
+    /// Information about the tag that was accessed just before the
+    /// error was triggered.
+    accessed_info: &'node NodeDebugInfo,
 }
 /// Internal contents of `Tree` with the minimum of mutable access for
 /// the purposes of the tree traversal functions: the permissions (`perms`) can be
 /// updated but not the tree structure (`tag_mapping` and `nodes`)
 struct TreeVisitor<'tree> {
     tag_mapping: &'tree UniKeyMap<BorTag>,
-    nodes: &'tree UniValMap<Node>,
+    nodes: &'tree mut UniValMap<Node>,
     perms: &'tree mut UniValMap<LocationState>,
 }
 
@@ -167,6 +171,7 @@ impl<'tree> TreeVisitor<'tree> {
     ) -> Result<(), OutErr>
 where {
         struct TreeVisitAux<NodeApp, ErrHandler> {
+            accessed_tag: UniIndex,
             f_propagate: NodeApp,
             err_builder: ErrHandler,
             stack: Vec<(UniIndex, AccessRelatedness)>,
@@ -190,15 +195,21 @@ where {
                 rel_pos: AccessRelatedness,
             ) -> Result<(), OutErr> {
                 // 1. apply the propagation function
-                let node = this.nodes.get(tag).unwrap();
+                let node = this.nodes.get_mut(tag).unwrap();
                 let recurse =
                     (self.f_propagate)(NodeAppArgs { node, perm: this.perms.entry(tag), rel_pos })
                         .map_err(|error_kind| {
                             (self.err_builder)(ErrHandlerArgs {
                                 error_kind,
-                                faulty_tag: &node.debug_info,
+                                conflicting_info: &this.nodes.get(tag).unwrap().debug_info,
+                                accessed_info: &this
+                                    .nodes
+                                    .get(self.accessed_tag)
+                                    .unwrap()
+                                    .debug_info,
                             })
                         })?;
+                let node = this.nodes.get(tag).unwrap();
                 // 2. add the children to the stack for future traversal
                 if matches!(recurse, ContinueTraversal::Recurse) {
                     let child_rel = rel_pos.for_child();
@@ -214,7 +225,8 @@ where {
         }
 
         let start_idx = self.tag_mapping.get(&start).unwrap();
-        let mut stack = TreeVisitAux { f_propagate, err_builder, stack: Vec::new() };
+        let mut stack =
+            TreeVisitAux { accessed_tag: start_idx, f_propagate, err_builder, stack: Vec::new() };
         {
             let mut path_ascend = Vec::new();
             // First climb to the root while recording the path
@@ -262,12 +274,15 @@ where {
 
 impl Tree {
     /// Create a new tree, with only a root pointer.
-    pub fn new(root_tag: BorTag, size: Size) -> Self {
+    pub fn new(root_tag: BorTag, size: Size, span: Span) -> Self {
         let root_perm = Permission::new_root();
         let mut tag_mapping = UniKeyMap::default();
         let root_idx = tag_mapping.insert(root_tag);
         let nodes = {
             let mut nodes = UniValMap::<Node>::default();
+            let mut debug_info = NodeDebugInfo::new(root_tag, root_perm, span);
+            // name the root so that all allocations contain one named pointer
+            debug_info.add_name("root of the allocation");
             nodes.insert(
                 root_idx,
                 Node {
@@ -275,7 +290,7 @@ impl Tree {
                     parent: None,
                     children: SmallVec::default(),
                     default_initial_perm: root_perm,
-                    debug_info: NodeDebugInfo::new(root_tag),
+                    debug_info,
                 },
             );
             nodes
@@ -297,6 +312,7 @@ impl<'tcx> Tree {
         new_tag: BorTag,
         default_initial_perm: Permission,
         range: AllocRange,
+        span: Span,
     ) -> InterpResult<'tcx> {
         assert!(!self.tag_mapping.contains_key(&new_tag));
         let idx = self.tag_mapping.insert(new_tag);
@@ -309,7 +325,7 @@ impl<'tcx> Tree {
                 parent: Some(parent_idx),
                 children: SmallVec::default(),
                 default_initial_perm,
-                debug_info: NodeDebugInfo::new(new_tag),
+                debug_info: NodeDebugInfo::new(new_tag, default_initial_perm, span),
             },
         );
         // Register new_tag as a child of parent_tag
@@ -330,11 +346,11 @@ impl<'tcx> Tree {
         tag: BorTag,
         range: AllocRange,
         global: &GlobalState,
+        span: Span, // diagnostics
     ) -> InterpResult<'tcx> {
-        self.perform_access(AccessKind::Write, tag, range, global)?;
-        let access_info = &self.nodes.get(self.tag_mapping.get(&tag).unwrap()).unwrap().debug_info;
-        for (_range, perms) in self.rperms.iter_mut(range.start, range.size) {
-            TreeVisitor { nodes: &self.nodes, tag_mapping: &self.tag_mapping, perms }
+        self.perform_access(AccessKind::Write, tag, range, global, span)?;
+        for (offset, perms) in self.rperms.iter_mut(range.start, range.size) {
+            TreeVisitor { nodes: &mut self.nodes, tag_mapping: &self.tag_mapping, perms }
                 .traverse_parents_this_children_others(
                     tag,
                     |args: NodeAppArgs<'_>| -> Result<ContinueTraversal, TransitionError> {
@@ -347,13 +363,14 @@ impl<'tcx> Tree {
                             Ok(ContinueTraversal::Recurse)
                         }
                     },
-                    |args: ErrHandlerArgs<'_, TransitionError>| -> InterpErrorInfo<'tcx> {
-                        let ErrHandlerArgs { error_kind, faulty_tag } = args;
+                    |args: ErrHandlerArgs<'_, TransitionError>| -> InterpError<'tcx> {
+                        let ErrHandlerArgs { error_kind, conflicting_info, accessed_info } = args;
                         TbError {
-                            faulty_tag,
+                            conflicting_info,
                             access_kind: AccessKind::Write,
+                            error_offset: offset,
                             error_kind,
-                            tag_of_access: access_info,
+                            accessed_info,
                         }
                         .build()
                     },
@@ -373,10 +390,10 @@ impl<'tcx> Tree {
         tag: BorTag,
         range: AllocRange,
         global: &GlobalState,
+        span: Span, // diagnostics
     ) -> InterpResult<'tcx> {
-        let access_info = &self.nodes.get(self.tag_mapping.get(&tag).unwrap()).unwrap().debug_info;
-        for (_range, perms) in self.rperms.iter_mut(range.start, range.size) {
-            TreeVisitor { nodes: &self.nodes, tag_mapping: &self.tag_mapping, perms }
+        for (offset, perms) in self.rperms.iter_mut(range.start, range.size) {
+            TreeVisitor { nodes: &mut self.nodes, tag_mapping: &self.tag_mapping, perms }
                 .traverse_parents_this_children_others(
                     tag,
                     |args: NodeAppArgs<'_>| -> Result<ContinueTraversal, TransitionError> {
@@ -424,24 +441,42 @@ impl<'tcx> Tree {
 
                         let old_perm = old_state.permission;
                         let protected = global.borrow().protected_tags.contains_key(&node.tag);
-                        let new_perm =
+                        let transition =
                             Permission::perform_access(access_kind, rel_pos, old_perm, protected)
                                 .ok_or(TransitionError::ChildAccessForbidden(old_perm))?;
                         if protected
                             // Can't trigger Protector on uninitialized locations
                             && old_state.initialized
-                            && !old_perm.protector_allows_transition(new_perm)
+                            && !transition.is_allowed_by_protector()
                         {
-                            return Err(TransitionError::ProtectedTransition(old_perm, new_perm));
+                            return Err(TransitionError::ProtectedTransition(transition));
+                        }
+                        // Record the event as part of the history
+                        if !transition.is_noop() {
+                            node.debug_info.history.push(diagnostics::Event {
+                                transition,
+                                access_kind,
+                                access_range: range,
+                                is_foreign: rel_pos.is_foreign(),
+                                offset,
+                                span,
+                            });
+                            old_state.permission =
+                                transition.applied(old_state.permission).unwrap();
                         }
-                        old_state.permission = new_perm;
                         old_state.initialized |= !rel_pos.is_foreign();
                         Ok(ContinueTraversal::Recurse)
                     },
-                    |args: ErrHandlerArgs<'_, TransitionError>| -> InterpErrorInfo<'tcx> {
-                        let ErrHandlerArgs { error_kind, faulty_tag } = args;
-                        TbError { faulty_tag, access_kind, error_kind, tag_of_access: access_info }
-                            .build()
+                    |args: ErrHandlerArgs<'_, TransitionError>| -> InterpError<'tcx> {
+                        let ErrHandlerArgs { error_kind, conflicting_info, accessed_info } = args;
+                        TbError {
+                            conflicting_info,
+                            access_kind,
+                            error_offset: offset,
+                            error_kind,
+                            accessed_info,
+                        }
+                        .build()
                     },
                 )?;
         }
diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs
index 7a726be00da4e..b4bf93a73d989 100644
--- a/src/tools/miri/src/diagnostics.rs
+++ b/src/tools/miri/src/diagnostics.rs
@@ -7,6 +7,7 @@ use rustc_span::{source_map::DUMMY_SP, SpanData, Symbol};
 use rustc_target::abi::{Align, Size};
 
 use crate::borrow_tracker::stacked_borrows::diagnostics::TagHistory;
+use crate::borrow_tracker::tree_borrows::diagnostics as tree_diagnostics;
 use crate::*;
 
 /// Details of premature program termination.
@@ -23,8 +24,10 @@ pub enum TerminationInfo {
         history: Option<TagHistory>,
     },
     TreeBorrowsUb {
-        msg: String,
-        // FIXME: incomplete
+        title: String,
+        relation: Option<String>,
+        problem: String,
+        history: tree_diagnostics::HistoryData,
     },
     Int2PtrWithStrictProvenance,
     Deadlock,
@@ -65,7 +68,7 @@ impl fmt::Display for TerminationInfo {
                     "integer-to-pointer casts and `ptr::from_exposed_addr` are not supported with `-Zmiri-strict-provenance`"
                 ),
             StackedBorrowsUb { msg, .. } => write!(f, "{msg}"),
-            TreeBorrowsUb { msg } => write!(f, "{msg}"),
+            TreeBorrowsUb { title, .. } => write!(f, "{title}"),
             Deadlock => write!(f, "the evaluated program deadlocked"),
             MultipleSymbolDefinitions { link_name, .. } =>
                 write!(f, "multiple definitions of symbol `{link_name}`"),
@@ -219,10 +222,16 @@ pub fn report_error<'tcx, 'mir>(
                 }
                 helps
             },
-            TreeBorrowsUb { .. } => {
-                let helps = vec![
-                    (None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")),
-                ];
+            TreeBorrowsUb { title: _, relation, problem, history } => {
+                let mut helps = Vec::new();
+                if let Some(relation) = relation {
+                    helps.push((None, relation.clone()));
+                }
+                helps.push((None, problem.clone()));
+                helps.push((None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")));
+                for event in history.events.clone() {
+                    helps.push(event);
+                }
                 helps
             }
             MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
diff --git a/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr b/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr
index 7c5bcd4e7b04b..1c9fe57bfb381 100644
--- a/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr
@@ -1,11 +1,35 @@
-error: Undefined Behavior: write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
+error: Undefined Behavior: write access through <TAG> is forbidden.
   --> $DIR/alternate-read-write.rs:LL:CC
    |
 LL |     *y += 1; // Failure
-   |     ^^^^^^^ write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
+   |     ^^^^^^^ write access through <TAG> is forbidden.
    |
+   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>.
+   = help: the conflicting tag <TAG> has state Frozen which forbids child write accesses.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here.
+  --> $DIR/alternate-read-write.rs:LL:CC
+   |
+LL |     let y = unsafe { &mut *(x as *mut u8) };
+   |                      ^^^^^^^^^^^^^^^^^^^^
+help: the conflicting tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/alternate-read-write.rs:LL:CC
+   |
+LL |     let y = unsafe { &mut *(x as *mut u8) };
+   |                      ^^^^^^^^^^^^^^^^^^^^
+help: the conflicting tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1].
+  --> $DIR/alternate-read-write.rs:LL:CC
+   |
+LL |     *y += 1; // Success
+   |     ^^^^^^^
+   = help: this corresponds to an activation.
+help: the conflicting tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1].
+  --> $DIR/alternate-read-write.rs:LL:CC
+   |
+LL |     let _val = *x;
+   |                ^^
+   = help: this corresponds to a loss of write permissions.
+   = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/alternate-read-write.rs:LL:CC
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
diff --git a/src/tools/miri/tests/fail/tree-borrows/error-range.rs b/src/tools/miri/tests/fail/tree-borrows/error-range.rs
new file mode 100644
index 0000000000000..d9980e75d6051
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree-borrows/error-range.rs
@@ -0,0 +1,27 @@
+//@compile-flags: -Zmiri-tree-borrows
+
+use core::ptr::addr_of_mut;
+
+// Check that the diagnostics correctly report the exact range at fault
+// and trim irrelevant events.
+fn main() {
+    unsafe {
+        let data = &mut [0u8; 16];
+
+        // Create and activate a few bytes
+        let rmut = &mut *addr_of_mut!(data[0..6]);
+        rmut[3] += 1;
+        rmut[4] += 1;
+        rmut[5] += 1;
+
+        // Now make them lose some perms
+        let _v = data[3];
+        let _v = data[4];
+        let _v = data[5];
+        data[4] = 1;
+        data[5] = 1;
+
+        // Final test
+        rmut[5] += 1; //~ ERROR: /read access through .* is forbidden/
+    }
+}
diff --git a/src/tools/miri/tests/fail/tree-borrows/error-range.stderr b/src/tools/miri/tests/fail/tree-borrows/error-range.stderr
new file mode 100644
index 0000000000000..870beeda04df6
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree-borrows/error-range.stderr
@@ -0,0 +1,44 @@
+error: Undefined Behavior: read access through <TAG> is forbidden.
+  --> $DIR/error-range.rs:LL:CC
+   |
+LL |         rmut[5] += 1;
+   |         ^^^^^^^^^^^^ read access through <TAG> is forbidden.
+   |
+   = 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: 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> was created here.
+  --> $DIR/error-range.rs:LL:CC
+   |
+LL |         let rmut = &mut *addr_of_mut!(data[0..6]);
+   |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+help: the conflicting tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/error-range.rs:LL:CC
+   |
+LL |         let rmut = &mut *addr_of_mut!(data[0..6]);
+   |                                       ^^^^
+help: the conflicting tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x5..0x6].
+  --> $DIR/error-range.rs:LL:CC
+   |
+LL |         rmut[5] += 1;
+   |         ^^^^^^^^^^^^
+   = help: this corresponds to an activation.
+help: the conflicting tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x5..0x6].
+  --> $DIR/error-range.rs:LL:CC
+   |
+LL |         let _v = data[5];
+   |                  ^^^^^^^
+   = help: this corresponds to a loss of write permissions.
+help: the conflicting tag <TAG> then transitioned from Frozen to Disabled due to a foreign write access at offsets [0x5..0x6].
+  --> $DIR/error-range.rs:LL:CC
+   |
+LL |         data[5] = 1;
+   |         ^^^^^^^^^^^
+   = help: this corresponds to a loss of read permissions.
+   = note: BACKTRACE (of the first span):
+   = note: inside `main` at $DIR/error-range.rs:LL:CC
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+
diff --git a/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr b/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr
index a078d18d3b02b..9ef4b10a1bf35 100644
--- a/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr
@@ -1,11 +1,29 @@
-error: Undefined Behavior: write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
+error: Undefined Behavior: write access through <TAG> is forbidden.
   --> $DIR/fragile-data-race.rs:LL:CC
    |
 LL |     unsafe { *p = 1 };
-   |              ^^^^^^ write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
+   |              ^^^^^^ write access through <TAG> is forbidden.
    |
+   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>.
+   = help: the conflicting tag <TAG> has state Frozen which forbids child write accesses.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here.
+  --> $DIR/fragile-data-race.rs:LL:CC
+   |
+LL | fn thread_1(x: &mut u8) -> SendPtr {
+   |             ^
+help: the conflicting tag <TAG> was created here, in the initial state Reserved.
+  --> RUSTLIB/std/src/panic.rs:LL:CC
+   |
+LL | pub fn catch_unwind<F: FnOnce() -> R + UnwindSafe, R>(f: F) -> Result<R> {
+   |                                                       ^
+help: the conflicting tag <TAG> then transitioned from Reserved to Frozen due to a foreign read access at offsets [0x0..0x1].
+  --> RUSTLIB/core/src/ptr/mod.rs:LL:CC
+   |
+LL |             crate::intrinsics::read_via_copy(src)
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = help: this corresponds to a loss of write permissions.
+   = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/fragile-data-race.rs:LL:CC
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
diff --git a/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr b/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr
index 4396c63679e10..5e76a3f2c0dda 100644
--- a/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr
@@ -1,11 +1,23 @@
-error: Undefined Behavior: write access through <TAG> is forbidden because it is a foreign tag for <TAG>, which would hence change from Reserved to Disabled, but <TAG> is protected
+error: Undefined Behavior: write access through <TAG> is forbidden.
   --> $DIR/outside-range.rs:LL:CC
    |
 LL |     *y.add(3) = 42;
-   |     ^^^^^^^^^^^^^^ write access through <TAG> is forbidden because it is a foreign tag for <TAG>, which would hence change from Reserved to Disabled, but <TAG> is protected
+   |     ^^^^^^^^^^^^^^ write access through <TAG> is forbidden.
    |
+   = help: the accessed tag <TAG> is a foreign tag for the protected tag <TAG>.
+   = help: the access would cause the protected tag <TAG> to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here.
+  --> $DIR/outside-range.rs:LL:CC
+   |
+LL |         let raw = data.as_mut_ptr();
+   |                   ^^^^^^^^^^^^^^^^^
+help: the protected tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/outside-range.rs:LL:CC
+   |
+LL | unsafe fn stuff(x: &mut u8, y: *mut u8) {
+   |                 ^
+   = note: BACKTRACE (of the first span):
    = note: inside `stuff` at $DIR/outside-range.rs:LL:CC
 note: inside `main`
   --> $DIR/outside-range.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr b/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr
index 7d9367c87d051..4486f7a5a6fe6 100644
--- a/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr
@@ -1,12 +1,31 @@
-error: Undefined Behavior: write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
+error: Undefined Behavior: write access through <TAG> is forbidden.
   --> $DIR/read-to-local.rs:LL:CC
    |
 LL |         *ptr = 0;
-   |         ^^^^^^^^ write access through <TAG> is forbidden because it is a child of <TAG> which is Frozen.
+   |         ^^^^^^^^ write access through <TAG> is forbidden.
    |
+   = help: the accessed tag <TAG> has state Frozen which forbids child write accesses.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/read-to-local.rs:LL:CC
+   |
+LL |         let mref = &mut root;
+   |                    ^^^^^^^^^
+help: the accessed tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1].
+  --> $DIR/read-to-local.rs:LL:CC
+   |
+LL |         *ptr = 0; // Write
+   |         ^^^^^^^^
+   = help: this corresponds to an activation.
+help: the accessed tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1].
+  --> $DIR/read-to-local.rs:LL:CC
+   |
+LL |         assert_eq!(root, 0); // Parent Read
+   |         ^^^^^^^^^^^^^^^^^^^
+   = help: this corresponds to a loss of write permissions.
+   = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/read-to-local.rs:LL:CC
+   = note: this error originates in the macro `assert_eq` (in Nightly builds, run with -Z macro-backtrace for more info)
 
 note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
 
diff --git a/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr
index 8ae1c09470a57..efeea52b72253 100644
--- a/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr
@@ -1,20 +1,33 @@
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Re*|    └─┬──<TAG=base>
-| Re*|      ├─┬──<TAG=x>
-| Re*|      │ └─┬──<TAG=caller:x>
-| Re*|      │   └────<TAG=callee:x> Strongly protected
-| Re*|      └────<TAG=y,callee:y,caller:y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Re*|      └─┬──<TAG=base>
+| Re*|        ├─┬──<TAG=x>
+| Re*|        │ └─┬──<TAG=caller:x>
+| Re*|        │   └────<TAG=callee:x> Strongly protected
+| Re*|        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────────────────────────
-error: Undefined Behavior: write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
+error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden.
   --> $DIR/cell-protected-write.rs:LL:CC
    |
 LL |             *y = 1;
-   |             ^^^^^^ write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
+   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden.
    |
+   = help: the accessed tag <TAG> (y, callee:y, caller:y) is a foreign tag for the protected tag <TAG> (callee:x).
+   = help: the access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here.
+  --> $DIR/cell-protected-write.rs:LL:CC
+   |
+LL |         let y = (&mut *n).get();
+   |                 ^^^^^^^^^
+help: the protected tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/cell-protected-write.rs:LL:CC
+   |
+LL |         unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {
+   |                                ^
+   = note: BACKTRACE (of the first span):
    = note: inside `main::write_second` at $DIR/cell-protected-write.rs:LL:CC
 note: inside `main`
   --> $DIR/cell-protected-write.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr
index a199fc0f0dacc..181577787651b 100644
--- a/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr
@@ -1,20 +1,33 @@
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Res|    └─┬──<TAG=n>
-| Res|      ├─┬──<TAG=x>
-| Res|      │ └─┬──<TAG=caller:x>
-| Res|      │   └────<TAG=callee:x> Strongly protected
-| Res|      └────<TAG=y,callee:y,caller:y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Res|      └─┬──<TAG=n>
+| Res|        ├─┬──<TAG=x>
+| Res|        │ └─┬──<TAG=caller:x>
+| Res|        │   └────<TAG=callee:x> Strongly protected
+| Res|        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────────────────────────
-error: Undefined Behavior: write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
+error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden.
   --> $DIR/int-protected-write.rs:LL:CC
    |
 LL |             *y = 0;
-   |             ^^^^^^ write access through <TAG> (also named 'y,callee:y,caller:y') is forbidden because it is a foreign tag for <TAG> (also named 'callee:x'), which would hence change from Reserved to Disabled, but <TAG> (also named 'callee:x') is protected
+   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden.
    |
+   = help: the accessed tag <TAG> (y, callee:y, caller:y) is a foreign tag for the protected tag <TAG> (callee:x).
+   = help: the access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here.
+  --> $DIR/int-protected-write.rs:LL:CC
+   |
+LL |         let y = (&mut *n) as *mut _;
+   |                 ^^^^^^^^^
+help: the protected tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/int-protected-write.rs:LL:CC
+   |
+LL |         unsafe fn write_second(x: &mut u8, y: *mut u8) {
+   |                                ^
+   = note: BACKTRACE (of the first span):
    = note: inside `main::write_second` at $DIR/int-protected-write.rs:LL:CC
 note: inside `main`
   --> $DIR/int-protected-write.rs:LL:CC
diff --git a/src/tools/miri/tests/fail/tree-borrows/strongly-protected.rs b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.rs
new file mode 100644
index 0000000000000..a68efea890cf7
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.rs
@@ -0,0 +1,14 @@
+//@compile-flags: -Zmiri-tree-borrows
+//@error-pattern: /deallocation through .* is forbidden/
+
+fn inner(x: &mut i32, f: fn(&mut i32)) {
+    // `f` may mutate, but it may not deallocate!
+    f(x)
+}
+
+fn main() {
+    inner(Box::leak(Box::new(0)), |x| {
+        let raw = x as *mut _;
+        drop(unsafe { Box::from_raw(raw) });
+    });
+}
diff --git a/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr
new file mode 100644
index 0000000000000..174951d6f00d4
--- /dev/null
+++ b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr
@@ -0,0 +1,49 @@
+error: Undefined Behavior: deallocation through <TAG> is forbidden.
+  --> RUSTLIB/alloc/src/alloc.rs:LL:CC
+   |
+LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
+   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocation through <TAG> is forbidden.
+   |
+   = help: the allocation of the accessed tag <TAG> also contains the strongly protected tag <TAG>.
+   = help: the strongly protected tag <TAG> disallows deallocations.
+   = 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> was created here.
+  --> $DIR/strongly-protected.rs:LL:CC
+   |
+LL |         drop(unsafe { Box::from_raw(raw) });
+   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+help: the strongly protected tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/strongly-protected.rs:LL:CC
+   |
+LL | fn inner(x: &mut i32, f: fn(&mut i32)) {
+   |          ^
+   = note: BACKTRACE (of the first span):
+   = note: inside `std::alloc::dealloc` at RUSTLIB/alloc/src/alloc.rs:LL:CC
+   = note: inside `<std::alloc::Global as std::alloc::Allocator>::deallocate` at RUSTLIB/alloc/src/alloc.rs:LL:CC
+   = note: inside `alloc::alloc::box_free::<i32, std::alloc::Global>` at RUSTLIB/alloc/src/alloc.rs:LL:CC
+   = note: inside `std::ptr::drop_in_place::<std::boxed::Box<i32>> - shim(Some(std::boxed::Box<i32>))` at RUSTLIB/core/src/ptr/mod.rs:LL:CC
+   = note: inside `std::mem::drop::<std::boxed::Box<i32>>` at RUSTLIB/core/src/mem/mod.rs:LL:CC
+note: inside closure
+  --> $DIR/strongly-protected.rs:LL:CC
+   |
+LL |         drop(unsafe { Box::from_raw(raw) });
+   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   = note: inside `<[closure@$DIR/strongly-protected.rs:LL:CC] as std::ops::FnOnce<(&mut i32,)>>::call_once - shim` at RUSTLIB/core/src/ops/function.rs:LL:CC
+note: inside `inner`
+  --> $DIR/strongly-protected.rs:LL:CC
+   |
+LL |     f(x)
+   |     ^^^^
+note: inside `main`
+  --> $DIR/strongly-protected.rs:LL:CC
+   |
+LL | /     inner(Box::leak(Box::new(0)), |x| {
+LL | |         let raw = x as *mut _;
+LL | |         drop(unsafe { Box::from_raw(raw) });
+LL | |     });
+   | |______^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+
diff --git a/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr b/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr
index e511eb9cf8fbb..b27d650d9f81d 100644
--- a/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr
@@ -1,11 +1,30 @@
-error: Undefined Behavior: read access through <TAG> is forbidden because it is a child of <TAG> which is Disabled.
+error: Undefined Behavior: read access through <TAG> is forbidden.
   --> $DIR/write-during-2phase.rs:LL:CC
    |
 LL |     fn add(&mut self, n: u64) -> u64 {
-   |            ^^^^^^^^^ read access through <TAG> is forbidden because it is a child of <TAG> which is Disabled.
+   |            ^^^^^^^^^ read access through <TAG> is forbidden.
    |
+   = help: the accessed tag <TAG> has state Disabled which forbids child read accesses.
    = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
-   = note: BACKTRACE:
+help: the accessed tag <TAG> was created here, in the initial state Reserved.
+  --> $DIR/write-during-2phase.rs:LL:CC
+   |
+LL |       let _res = f.add(unsafe {
+   |  ________________^
+LL | |         let n = f.0;
+LL | |         // This is the access at fault, but it's not immediately apparent because
+LL | |         // the reference that got invalidated is not under a Protector.
+LL | |         *inner = 42;
+LL | |         n
+LL | |     });
+   | |______^
+help: the accessed tag <TAG> then transitioned from Reserved to Disabled due to a foreign write access at offsets [0x0..0x8].
+  --> $DIR/write-during-2phase.rs:LL:CC
+   |
+LL |         *inner = 42;
+   |         ^^^^^^^^^^^
+   = help: this corresponds to a loss of read and write permissions.
+   = note: BACKTRACE (of the first span):
    = note: inside `Foo::add` at $DIR/write-during-2phase.rs:LL:CC
 note: inside `main`
   --> $DIR/write-during-2phase.rs:LL:CC
diff --git a/src/tools/miri/tests/pass/tree-borrows/cell-alternate-writes.stderr b/src/tools/miri/tests/pass/tree-borrows/cell-alternate-writes.stderr
index d4bc822b4bb06..1eab4685a35f5 100644
--- a/src/tools/miri/tests/pass/tree-borrows/cell-alternate-writes.stderr
+++ b/src/tools/miri/tests/pass/tree-borrows/cell-alternate-writes.stderr
@@ -1,10 +1,12 @@
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Re*|    └────<TAG=data,x,y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Re*|      └────<TAG=data, x, y>
 ──────────────────────────────────────────────────────────────────────
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Act|    └────<TAG=data,x,y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Act|      └────<TAG=data, x, y>
 ──────────────────────────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree-borrows/end-of-protector.stderr b/src/tools/miri/tests/pass/tree-borrows/end-of-protector.stderr
index d08d69483203b..c20da1a593fc0 100644
--- a/src/tools/miri/tests/pass/tree-borrows/end-of-protector.stderr
+++ b/src/tools/miri/tests/pass/tree-borrows/end-of-protector.stderr
@@ -1,32 +1,36 @@
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Res|    └─┬──<TAG=data>
-| Res|      └────<TAG=x>
+| Act|    └─┬──<TAG=root of the allocation>
+| Res|      └─┬──<TAG=data>
+| Res|        └────<TAG=x>
 ──────────────────────────────────────────────────────────────────────
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Res|    └─┬──<TAG=data>
-| Res|      └─┬──<TAG=x>
-| Res|        └─┬──<TAG=caller:x>
-| Res|          └────<TAG=callee:x> Strongly protected
+| Act|    └─┬──<TAG=root of the allocation>
+| Res|      └─┬──<TAG=data>
+| Res|        └─┬──<TAG=x>
+| Res|          └─┬──<TAG=caller:x>
+| Res|            └────<TAG=callee:x> Strongly protected
 ──────────────────────────────────────────────────────────────────────
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Res|    └─┬──<TAG=data>
-| Res|      ├─┬──<TAG=x>
-| Res|      │ └─┬──<TAG=caller:x>
-| Res|      │   └────<TAG=callee:x>
-| Res|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Res|      └─┬──<TAG=data>
+| Res|        ├─┬──<TAG=x>
+| Res|        │ └─┬──<TAG=caller:x>
+| Res|        │   └────<TAG=callee:x>
+| Res|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Act|    └─┬──<TAG=data>
-| Dis|      ├─┬──<TAG=x>
-| Dis|      │ └─┬──<TAG=caller:x>
-| Dis|      │   └────<TAG=callee:x>
-| Act|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Act|      └─┬──<TAG=data>
+| Dis|        ├─┬──<TAG=x>
+| Dis|        │ └─┬──<TAG=caller:x>
+| Dis|        │   └────<TAG=callee:x>
+| Act|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree-borrows/formatting.stderr b/src/tools/miri/tests/pass/tree-borrows/formatting.stderr
index a59775cf21f10..8c3779fe1f7f7 100644
--- a/src/tools/miri/tests/pass/tree-borrows/formatting.stderr
+++ b/src/tools/miri/tests/pass/tree-borrows/formatting.stderr
@@ -1,29 +1,31 @@
-─────────────────────────────────────────────────────────────────────────────
+───────────────────────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1..  2.. 10.. 11..100..101..1000..1001..1024
-| Res| Act| Res| Act| Res| Act|  Res|  Act|  Res|    └─┬──<TAG=data>
-|----| Act|----|?Dis|----|?Dis| ----| ?Dis| ----|      ├────<TAG=data[1]>
-|----|----|----| Act|----|?Dis| ----| ?Dis| ----|      ├────<TAG=data[10]>
-|----|----|----|----|----| Frz| ----| ?Dis| ----|      ├────<TAG=data[100]>
-|----|----|----|----|----|----| ----|  Act| ----|      └────<TAG=data[1000]>
-─────────────────────────────────────────────────────────────────────────────
+| Act| Act| Act| Act| Act| Act|  Act|  Act|  Act|    └─┬──<TAG=root of the allocation>
+| Res| Act| Res| Act| Res| Act|  Res|  Act|  Res|      └─┬──<TAG=data>
+|----| Act|----|?Dis|----|?Dis| ----| ?Dis| ----|        ├────<TAG=data[1]>
+|----|----|----| Act|----|?Dis| ----| ?Dis| ----|        ├────<TAG=data[10]>
+|----|----|----|----|----| Frz| ----| ?Dis| ----|        ├────<TAG=data[100]>
+|----|----|----|----|----|----| ----|  Act| ----|        └────<TAG=data[1000]>
+───────────────────────────────────────────────────────────────────────────────────────
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Frz|    └─┬──<TAG=x>
-| Frz|      ├─┬──<TAG=xa>
-| Frz|      │ ├────<TAG=xaa>
-| Frz|      │ └────<TAG=xab>
-| Frz|      ├─┬──<TAG=xb>
-| Frz|      │ └─┬──<TAG=xba>
-| Frz|      │   └─┬──<TAG=xbaa>
-| Frz|      │     └─┬──<TAG=xbaaa>
-| Frz|      │       └────<TAG=xbaaaa>
-| Frz|      └─┬──<TAG=xc>
-| Frz|        ├─┬──<TAG=xca>
-| Frz|        │ ├────<TAG=xcaa>
-| Frz|        │ └────<TAG=xcab>
-| Frz|        └─┬──<TAG=xcb>
-| Frz|          ├────<TAG=xcba>
-| Frz|          └────<TAG=xcbb>
+| Act|    └─┬──<TAG=root of the allocation>
+| Frz|      └─┬──<TAG=x>
+| Frz|        ├─┬──<TAG=xa>
+| Frz|        │ ├────<TAG=xaa>
+| Frz|        │ └────<TAG=xab>
+| Frz|        ├─┬──<TAG=xb>
+| Frz|        │ └─┬──<TAG=xba>
+| Frz|        │   └─┬──<TAG=xbaa>
+| Frz|        │     └─┬──<TAG=xbaaa>
+| Frz|        │       └────<TAG=xbaaaa>
+| Frz|        └─┬──<TAG=xc>
+| Frz|          ├─┬──<TAG=xca>
+| Frz|          │ ├────<TAG=xcaa>
+| Frz|          │ └────<TAG=xcab>
+| Frz|          └─┬──<TAG=xcb>
+| Frz|            ├────<TAG=xcba>
+| Frz|            └────<TAG=xcbb>
 ──────────────────────────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree-borrows/reborrow-is-read.stderr b/src/tools/miri/tests/pass/tree-borrows/reborrow-is-read.stderr
index b9c52c2064056..8c4323b2f7fa7 100644
--- a/src/tools/miri/tests/pass/tree-borrows/reborrow-is-read.stderr
+++ b/src/tools/miri/tests/pass/tree-borrows/reborrow-is-read.stderr
@@ -1,13 +1,15 @@
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Act|    └─┬──<TAG=parent>
-| Act|      └────<TAG=x>
+| Act|    └─┬──<TAG=root of the allocation>
+| Act|      └─┬──<TAG=parent>
+| Act|        └────<TAG=x>
 ──────────────────────────────────────────────────────────────────────
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Act|    └─┬──<TAG=parent>
-| Frz|      ├────<TAG=x>
-| Res|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Act|      └─┬──<TAG=parent>
+| Frz|        ├────<TAG=x>
+| Res|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────
diff --git a/src/tools/miri/tests/pass/tree-borrows/reserved.stderr b/src/tools/miri/tests/pass/tree-borrows/reserved.stderr
index d76ee0f826607..afb917002221e 100644
--- a/src/tools/miri/tests/pass/tree-borrows/reserved.stderr
+++ b/src/tools/miri/tests/pass/tree-borrows/reserved.stderr
@@ -2,51 +2,57 @@
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Re*|    └─┬──<TAG=base>
-| Re*|      ├─┬──<TAG=x>
-| Re*|      │ └─┬──<TAG=caller:x>
-| Frz|      │   └────<TAG=callee:x>
-| Re*|      └────<TAG=y,caller:y,callee:y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Re*|      └─┬──<TAG=base>
+| Re*|        ├─┬──<TAG=x>
+| Re*|        │ └─┬──<TAG=caller:x>
+| Frz|        │   └────<TAG=callee:x>
+| Re*|        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────────────────────────
 [interior mut] Foreign Read: Re* -> Re*
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  8
-| Re*|    └─┬──<TAG=base>
-| Re*|      ├────<TAG=x>
-| Re*|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Re*|      └─┬──<TAG=base>
+| Re*|        ├────<TAG=x>
+| Re*|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────
 [interior mut] Foreign Write: Re* -> Re*
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  8
-| Act|    └─┬──<TAG=base>
-| Re*|      ├────<TAG=x>
-| Act|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Act|      └─┬──<TAG=base>
+| Re*|        ├────<TAG=x>
+| Act|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────
 [protected] Foreign Read: Res -> Frz
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Res|    └─┬──<TAG=base>
-| Res|      ├─┬──<TAG=x>
-| Res|      │ └─┬──<TAG=caller:x>
-| Frz|      │   └────<TAG=callee:x>
-| Res|      └────<TAG=y,caller:y,callee:y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Res|      └─┬──<TAG=base>
+| Res|        ├─┬──<TAG=x>
+| Res|        │ └─┬──<TAG=caller:x>
+| Frz|        │   └────<TAG=callee:x>
+| Res|        └────<TAG=y, caller:y, callee:y>
 ──────────────────────────────────────────────────────────────────────
 [] Foreign Read: Res -> Res
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Res|    └─┬──<TAG=base>
-| Res|      ├────<TAG=x>
-| Res|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Res|      └─┬──<TAG=base>
+| Res|        ├────<TAG=x>
+| Res|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────
 [] Foreign Write: Res -> Dis
 ──────────────────────────────────────────────────────────────────────
 Warning: this tree is indicative only. Some tags may have been hidden.
 0..  1
-| Act|    └─┬──<TAG=base>
-| Dis|      ├────<TAG=x>
-| Act|      └────<TAG=y>
+| Act|    └─┬──<TAG=root of the allocation>
+| Act|      └─┬──<TAG=base>
+| Dis|        ├────<TAG=x>
+| Act|        └────<TAG=y>
 ──────────────────────────────────────────────────────────────────────

From 7566ed8ff4db1549feeaebe0ed1ca2e0de2c9c01 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 28 Apr 2023 12:58:19 +0200
Subject: [PATCH 2/2] tweak wording

---
 .../tree_borrows/diagnostics.rs               | 67 +++++++++----------
 src/tools/miri/src/diagnostics.rs             | 15 ++---
 .../tree-borrows/alternate-read-write.stderr  | 20 +++---
 .../fail/tree-borrows/error-range.stderr      | 24 +++----
 .../tree-borrows/fragile-data-race.stderr     | 16 ++---
 .../fail/tree-borrows/outside-range.stderr    | 13 ++--
 .../fail/tree-borrows/read-to-local.stderr    | 16 ++---
 .../reserved/cell-protected-write.stderr      | 13 ++--
 .../reserved/int-protected-write.stderr       | 13 ++--
 .../tree-borrows/strongly-protected.stderr    | 12 ++--
 .../tree-borrows/write-during-2phase.stderr   | 12 ++--
 11 files changed, 111 insertions(+), 110 deletions(-)

diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
index 18d540dfd1a69..2c6d27ced0180 100644
--- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
+++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs
@@ -70,7 +70,7 @@ impl HistoryData {
         let this = format!("the {tag_name} tag {tag:?}");
         let msg_initial_state = format!(", in the initial state {}", created.1);
         let msg_creation = format!(
-            "{this} was created here{maybe_msg_initial_state}.",
+            "{this} was created here{maybe_msg_initial_state}",
             maybe_msg_initial_state = if show_initial_state { &msg_initial_state } else { "" },
         );
 
@@ -79,8 +79,8 @@ impl HistoryData {
         {
             // NOTE: `offset` 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} then transitioned {transition} due to a {rel} {access_kind} at offsets {access_range:?}.", rel = if is_foreign { "foreign" } else { "child" })));
-            self.events.push((None, format!("this corresponds to {}.", transition.summary())));
+            self.events.push((Some(span.data()), format!("{this} then transitioned {transition} due to a {rel} {access_kind} at offsets {access_range:?}", rel = if is_foreign { "foreign" } else { "child" })));
+            self.events.push((None, format!("this corresponds to {}", transition.summary())));
         }
     }
 }
@@ -266,50 +266,49 @@ impl TbError<'_> {
         let accessed = self.accessed_info;
         let conflicting = self.conflicting_info;
         let accessed_is_conflicting = accessed.tag == conflicting.tag;
-        let (pre_error, title, relation, problem, conflicting_tag_name) = match self.error_kind {
+        let (pre_error, title, details, conflicting_tag_name) = match self.error_kind {
             ChildAccessForbidden(perm) => {
                 let conflicting_tag_name =
                     if accessed_is_conflicting { "accessed" } else { "conflicting" };
-                (
-                    perm,
-                    format!("{kind} through {accessed} is forbidden."),
-                    (!accessed_is_conflicting).then_some(format!(
-                        "the accessed tag {accessed} is a child of the conflicting tag {conflicting}."
-                    )),
-                    format!(
-                        "the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids child {kind}es."
-                    ),
-                    conflicting_tag_name,
-                )
+                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}"
+                    ));
+                }
+                details.push(format!(
+                    "the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids child {kind}es"
+                ));
+                (perm, title, details, conflicting_tag_name)
             }
             ProtectedTransition(transition) => {
                 let conflicting_tag_name = "protected";
-                (
-                    transition.started(),
-                    format!("{kind} through {accessed} is forbidden."),
-                    Some(format!(
-                        "the accessed tag {accessed} is a foreign tag for the {conflicting_tag_name} tag {conflicting}."
-                    )),
+                let title = format!("{kind} through {accessed} is forbidden");
+                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}"
+                    ),
                     format!(
-                        "the access would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}. This is {loss}, which is not allowed for protected tags.",
+                        "this is {loss}, which is not allowed for protected tags",
                         loss = transition.summary(),
                     ),
-                    conflicting_tag_name,
-                )
+                ];
+                (transition.started(), title, details, conflicting_tag_name)
             }
             ProtectedDealloc => {
                 let conflicting_tag_name = "strongly protected";
-                (
-                    started_as,
-                    format!("deallocation through {accessed} is forbidden."),
-                    Some(format!(
-                        "the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}."
-                    )),
+                let title = format!("deallocation through {accessed} is forbidden");
+                let details = vec![
                     format!(
-                        "the {conflicting_tag_name} tag {conflicting} disallows deallocations."
+                        "the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}"
                     ),
-                    conflicting_tag_name,
-                )
+                    format!("the {conflicting_tag_name} tag {conflicting} disallows deallocations"),
+                ];
+                (started_as, title, details, conflicting_tag_name)
             }
         };
         let pre_transition = PermTransition::from(started_as, pre_error).unwrap();
@@ -322,7 +321,7 @@ impl TbError<'_> {
             conflicting_tag_name,
             true,
         );
-        err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, relation, problem, history })
+        err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history })
     }
 }
 
diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs
index b4bf93a73d989..aeba0ea5a9524 100644
--- a/src/tools/miri/src/diagnostics.rs
+++ b/src/tools/miri/src/diagnostics.rs
@@ -25,8 +25,7 @@ pub enum TerminationInfo {
     },
     TreeBorrowsUb {
         title: String,
-        relation: Option<String>,
-        problem: String,
+        details: Vec<String>,
         history: tree_diagnostics::HistoryData,
     },
     Int2PtrWithStrictProvenance,
@@ -222,13 +221,13 @@ pub fn report_error<'tcx, 'mir>(
                 }
                 helps
             },
-            TreeBorrowsUb { title: _, relation, problem, history } => {
-                let mut helps = Vec::new();
-                if let Some(relation) = relation {
-                    helps.push((None, relation.clone()));
+            TreeBorrowsUb { title: _, details, history } => {
+                let mut helps = vec![
+                    (None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental"))
+                ];
+                for m in details {
+                    helps.push((None, m.clone()));
                 }
-                helps.push((None, problem.clone()));
-                helps.push((None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")));
                 for event in history.events.clone() {
                     helps.push(event);
                 }
diff --git a/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr b/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr
index 1c9fe57bfb381..bb601fc88352d 100644
--- a/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr
@@ -1,34 +1,34 @@
-error: Undefined Behavior: write access through <TAG> is forbidden.
+error: Undefined Behavior: write access through <TAG> is forbidden
   --> $DIR/alternate-read-write.rs:LL:CC
    |
 LL |     *y += 1; // Failure
-   |     ^^^^^^^ write access through <TAG> is forbidden.
+   |     ^^^^^^^ write access through <TAG> is forbidden
    |
-   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>.
-   = help: the conflicting tag <TAG> has state Frozen which forbids child write accesses.
    = 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> was created here.
+   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
+   = help: the conflicting tag <TAG> has state Frozen which forbids child write accesses
+help: the accessed tag <TAG> was created here
   --> $DIR/alternate-read-write.rs:LL:CC
    |
 LL |     let y = unsafe { &mut *(x as *mut u8) };
    |                      ^^^^^^^^^^^^^^^^^^^^
-help: the conflicting tag <TAG> was created here, in the initial state Reserved.
+help: the conflicting tag <TAG> was created here, in the initial state Reserved
   --> $DIR/alternate-read-write.rs:LL:CC
    |
 LL |     let y = unsafe { &mut *(x as *mut u8) };
    |                      ^^^^^^^^^^^^^^^^^^^^
-help: the conflicting tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1].
+help: the conflicting tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1]
   --> $DIR/alternate-read-write.rs:LL:CC
    |
 LL |     *y += 1; // Success
    |     ^^^^^^^
-   = help: this corresponds to an activation.
-help: the conflicting tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1].
+   = help: this corresponds to an activation
+help: the conflicting tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1]
   --> $DIR/alternate-read-write.rs:LL:CC
    |
 LL |     let _val = *x;
    |                ^^
-   = help: this corresponds to a loss of write permissions.
+   = help: this corresponds to a loss of write permissions
    = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/alternate-read-write.rs:LL:CC
 
diff --git a/src/tools/miri/tests/fail/tree-borrows/error-range.stderr b/src/tools/miri/tests/fail/tree-borrows/error-range.stderr
index 870beeda04df6..bc829fd86d350 100644
--- a/src/tools/miri/tests/fail/tree-borrows/error-range.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/error-range.stderr
@@ -1,40 +1,40 @@
-error: Undefined Behavior: read access through <TAG> is forbidden.
+error: Undefined Behavior: read access through <TAG> is forbidden
   --> $DIR/error-range.rs:LL:CC
    |
 LL |         rmut[5] += 1;
-   |         ^^^^^^^^^^^^ read access through <TAG> is forbidden.
+   |         ^^^^^^^^^^^^ read access through <TAG> is forbidden
    |
-   = 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: 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> was created here.
+   = 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 accessed tag <TAG> was created here
   --> $DIR/error-range.rs:LL:CC
    |
 LL |         let rmut = &mut *addr_of_mut!(data[0..6]);
    |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-help: the conflicting tag <TAG> was created here, in the initial state Reserved.
+help: the conflicting tag <TAG> was created here, in the initial state Reserved
   --> $DIR/error-range.rs:LL:CC
    |
 LL |         let rmut = &mut *addr_of_mut!(data[0..6]);
    |                                       ^^^^
-help: the conflicting tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x5..0x6].
+help: the conflicting tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x5..0x6]
   --> $DIR/error-range.rs:LL:CC
    |
 LL |         rmut[5] += 1;
    |         ^^^^^^^^^^^^
-   = help: this corresponds to an activation.
-help: the conflicting tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x5..0x6].
+   = help: this corresponds to an activation
+help: the conflicting tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x5..0x6]
   --> $DIR/error-range.rs:LL:CC
    |
 LL |         let _v = data[5];
    |                  ^^^^^^^
-   = help: this corresponds to a loss of write permissions.
-help: the conflicting tag <TAG> then transitioned from Frozen to Disabled due to a foreign write access at offsets [0x5..0x6].
+   = help: this corresponds to a loss of write permissions
+help: the conflicting tag <TAG> then transitioned from Frozen to Disabled due to a foreign write access at offsets [0x5..0x6]
   --> $DIR/error-range.rs:LL:CC
    |
 LL |         data[5] = 1;
    |         ^^^^^^^^^^^
-   = help: this corresponds to a loss of read permissions.
+   = help: this corresponds to a loss of read permissions
    = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/error-range.rs:LL:CC
 
diff --git a/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr b/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr
index 9ef4b10a1bf35..8e80bdd63c0be 100644
--- a/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr
@@ -1,28 +1,28 @@
-error: Undefined Behavior: write access through <TAG> is forbidden.
+error: Undefined Behavior: write access through <TAG> is forbidden
   --> $DIR/fragile-data-race.rs:LL:CC
    |
 LL |     unsafe { *p = 1 };
-   |              ^^^^^^ write access through <TAG> is forbidden.
+   |              ^^^^^^ write access through <TAG> is forbidden
    |
-   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>.
-   = help: the conflicting tag <TAG> has state Frozen which forbids child write accesses.
    = 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> was created here.
+   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
+   = help: the conflicting tag <TAG> has state Frozen which forbids child write accesses
+help: the accessed tag <TAG> was created here
   --> $DIR/fragile-data-race.rs:LL:CC
    |
 LL | fn thread_1(x: &mut u8) -> SendPtr {
    |             ^
-help: the conflicting tag <TAG> was created here, in the initial state Reserved.
+help: the conflicting tag <TAG> was created here, in the initial state Reserved
   --> RUSTLIB/std/src/panic.rs:LL:CC
    |
 LL | pub fn catch_unwind<F: FnOnce() -> R + UnwindSafe, R>(f: F) -> Result<R> {
    |                                                       ^
-help: the conflicting tag <TAG> then transitioned from Reserved to Frozen due to a foreign read access at offsets [0x0..0x1].
+help: the conflicting tag <TAG> then transitioned from Reserved to Frozen due to a foreign read access at offsets [0x0..0x1]
   --> RUSTLIB/core/src/ptr/mod.rs:LL:CC
    |
 LL |             crate::intrinsics::read_via_copy(src)
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   = help: this corresponds to a loss of write permissions.
+   = help: this corresponds to a loss of write permissions
    = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/fragile-data-race.rs:LL:CC
 
diff --git a/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr b/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr
index 5e76a3f2c0dda..14696c704fc1b 100644
--- a/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr
@@ -1,18 +1,19 @@
-error: Undefined Behavior: write access through <TAG> is forbidden.
+error: Undefined Behavior: write access through <TAG> is forbidden
   --> $DIR/outside-range.rs:LL:CC
    |
 LL |     *y.add(3) = 42;
-   |     ^^^^^^^^^^^^^^ write access through <TAG> is forbidden.
+   |     ^^^^^^^^^^^^^^ write access through <TAG> is forbidden
    |
-   = help: the accessed tag <TAG> is a foreign tag for the protected tag <TAG>.
-   = help: the access would cause the protected tag <TAG> to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags.
    = 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> was created here.
+   = 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 Reserved to Disabled
+   = help: this is a loss of read and write permissions, which is not allowed for protected tags
+help: the accessed tag <TAG> was created here
   --> $DIR/outside-range.rs:LL:CC
    |
 LL |         let raw = data.as_mut_ptr();
    |                   ^^^^^^^^^^^^^^^^^
-help: the protected tag <TAG> was created here, in the initial state Reserved.
+help: the protected tag <TAG> was created here, in the initial state Reserved
   --> $DIR/outside-range.rs:LL:CC
    |
 LL | unsafe fn stuff(x: &mut u8, y: *mut u8) {
diff --git a/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr b/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr
index 4486f7a5a6fe6..8c9c2f8f9656b 100644
--- a/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr
@@ -1,28 +1,28 @@
-error: Undefined Behavior: write access through <TAG> is forbidden.
+error: Undefined Behavior: write access through <TAG> is forbidden
   --> $DIR/read-to-local.rs:LL:CC
    |
 LL |         *ptr = 0;
-   |         ^^^^^^^^ write access through <TAG> is forbidden.
+   |         ^^^^^^^^ write access through <TAG> is forbidden
    |
-   = help: the accessed tag <TAG> has state Frozen which forbids child write accesses.
    = 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> was created here, in the initial state Reserved.
+   = help: the accessed tag <TAG> has state Frozen which forbids child write accesses
+help: the accessed tag <TAG> was created here, in the initial state Reserved
   --> $DIR/read-to-local.rs:LL:CC
    |
 LL |         let mref = &mut root;
    |                    ^^^^^^^^^
-help: the accessed tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1].
+help: the accessed tag <TAG> then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1]
   --> $DIR/read-to-local.rs:LL:CC
    |
 LL |         *ptr = 0; // Write
    |         ^^^^^^^^
-   = help: this corresponds to an activation.
-help: the accessed tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1].
+   = help: this corresponds to an activation
+help: the accessed tag <TAG> then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1]
   --> $DIR/read-to-local.rs:LL:CC
    |
 LL |         assert_eq!(root, 0); // Parent Read
    |         ^^^^^^^^^^^^^^^^^^^
-   = help: this corresponds to a loss of write permissions.
+   = help: this corresponds to a loss of write permissions
    = note: BACKTRACE (of the first span):
    = note: inside `main` at $DIR/read-to-local.rs:LL:CC
    = note: this error originates in the macro `assert_eq` (in Nightly builds, run with -Z macro-backtrace for more info)
diff --git a/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr
index efeea52b72253..b85793ff06337 100644
--- a/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr
@@ -8,21 +8,22 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 | Re*|        │   └────<TAG=callee:x> Strongly protected
 | Re*|        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────────────────────────
-error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden.
+error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden
   --> $DIR/cell-protected-write.rs:LL:CC
    |
 LL |             *y = 1;
-   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden.
+   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden
    |
-   = help: the accessed tag <TAG> (y, callee:y, caller:y) is a foreign tag for the protected tag <TAG> (callee:x).
-   = help: the access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags.
    = 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> was created here.
+   = help: the accessed tag <TAG> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
+   = help: the access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled
+   = help: this is a loss of read and write permissions, which is not allowed for protected tags
+help: the accessed tag <TAG> was created here
   --> $DIR/cell-protected-write.rs:LL:CC
    |
 LL |         let y = (&mut *n).get();
    |                 ^^^^^^^^^
-help: the protected tag <TAG> was created here, in the initial state Reserved.
+help: the protected tag <TAG> was created here, in the initial state Reserved
   --> $DIR/cell-protected-write.rs:LL:CC
    |
 LL |         unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {
diff --git a/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr
index 181577787651b..5de7dc0c7c51f 100644
--- a/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr
@@ -8,21 +8,22 @@ Warning: this tree is indicative only. Some tags may have been hidden.
 | Res|        │   └────<TAG=callee:x> Strongly protected
 | Res|        └────<TAG=y, callee:y, caller:y>
 ──────────────────────────────────────────────────────────────────────
-error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden.
+error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) is forbidden
   --> $DIR/int-protected-write.rs:LL:CC
    |
 LL |             *y = 0;
-   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden.
+   |             ^^^^^^ write access through <TAG> (y, callee:y, caller:y) is forbidden
    |
-   = help: the accessed tag <TAG> (y, callee:y, caller:y) is a foreign tag for the protected tag <TAG> (callee:x).
-   = help: the access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags.
    = 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> was created here.
+   = help: the accessed tag <TAG> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
+   = help: the access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled
+   = help: this is a loss of read and write permissions, which is not allowed for protected tags
+help: the accessed tag <TAG> was created here
   --> $DIR/int-protected-write.rs:LL:CC
    |
 LL |         let y = (&mut *n) as *mut _;
    |                 ^^^^^^^^^
-help: the protected tag <TAG> was created here, in the initial state Reserved.
+help: the protected tag <TAG> was created here, in the initial state Reserved
   --> $DIR/int-protected-write.rs:LL:CC
    |
 LL |         unsafe fn write_second(x: &mut u8, y: *mut u8) {
diff --git a/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr
index 174951d6f00d4..97088d5854cc9 100644
--- a/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr
@@ -1,18 +1,18 @@
-error: Undefined Behavior: deallocation through <TAG> is forbidden.
+error: Undefined Behavior: deallocation through <TAG> is forbidden
   --> RUSTLIB/alloc/src/alloc.rs:LL:CC
    |
 LL |     unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
-   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocation through <TAG> is forbidden.
+   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocation through <TAG> is forbidden
    |
-   = help: the allocation of the accessed tag <TAG> also contains the strongly protected tag <TAG>.
-   = help: the strongly protected tag <TAG> disallows deallocations.
    = 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> was created here.
+   = help: the allocation of the accessed tag <TAG> also contains the strongly protected tag <TAG>
+   = help: the strongly protected tag <TAG> disallows deallocations
+help: the accessed tag <TAG> was created here
   --> $DIR/strongly-protected.rs:LL:CC
    |
 LL |         drop(unsafe { Box::from_raw(raw) });
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-help: the strongly protected tag <TAG> was created here, in the initial state Reserved.
+help: the strongly protected tag <TAG> was created here, in the initial state Reserved
   --> $DIR/strongly-protected.rs:LL:CC
    |
 LL | fn inner(x: &mut i32, f: fn(&mut i32)) {
diff --git a/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr b/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr
index b27d650d9f81d..f6285bdcf16d4 100644
--- a/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr
+++ b/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr
@@ -1,12 +1,12 @@
-error: Undefined Behavior: read access through <TAG> is forbidden.
+error: Undefined Behavior: read access through <TAG> is forbidden
   --> $DIR/write-during-2phase.rs:LL:CC
    |
 LL |     fn add(&mut self, n: u64) -> u64 {
-   |            ^^^^^^^^^ read access through <TAG> is forbidden.
+   |            ^^^^^^^^^ read access through <TAG> is forbidden
    |
-   = help: the accessed tag <TAG> has state Disabled which forbids child read accesses.
    = 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> was created here, in the initial state Reserved.
+   = help: the accessed tag <TAG> has state Disabled which forbids child read accesses
+help: the accessed tag <TAG> was created here, in the initial state Reserved
   --> $DIR/write-during-2phase.rs:LL:CC
    |
 LL |       let _res = f.add(unsafe {
@@ -18,12 +18,12 @@ LL | |         *inner = 42;
 LL | |         n
 LL | |     });
    | |______^
-help: the accessed tag <TAG> then transitioned from Reserved to Disabled due to a foreign write access at offsets [0x0..0x8].
+help: the accessed tag <TAG> then transitioned from Reserved to Disabled due to a foreign write access at offsets [0x0..0x8]
   --> $DIR/write-during-2phase.rs:LL:CC
    |
 LL |         *inner = 42;
    |         ^^^^^^^^^^^
-   = help: this corresponds to a loss of read and write permissions.
+   = help: this corresponds to a loss of read and write permissions
    = note: BACKTRACE (of the first span):
    = note: inside `Foo::add` at $DIR/write-during-2phase.rs:LL:CC
 note: inside `main`