about summary refs log tree commit diff
diff options
context:
space:
mode:
authorRalf Jung <post@ralfj.de>2023-04-28 12:58:19 +0200
committerRalf Jung <post@ralfj.de>2023-04-28 13:22:08 +0200
commit7566ed8ff4db1549feeaebe0ed1ca2e0de2c9c01 (patch)
treef66166af298faa6292fc065cb6cc96c9bb4a66e5
parentfe178ccb72ab824bc62a011a00e8a821332a068c (diff)
downloadrust-7566ed8ff4db1549feeaebe0ed1ca2e0de2c9c01.tar.gz
rust-7566ed8ff4db1549feeaebe0ed1ca2e0de2c9c01.zip
tweak wording
-rw-r--r--src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs67
-rw-r--r--src/tools/miri/src/diagnostics.rs15
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr20
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/error-range.stderr24
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr16
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/outside-range.stderr13
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr16
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr13
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr13
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr12
-rw-r--r--src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr12
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 18d540dfd1a..2c6d27ced01 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 b4bf93a73d9..aeba0ea5a95 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 1c9fe57bfb3..bb601fc8835 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 870beeda04d..bc829fd86d3 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 9ef4b10a1bf..8e80bdd63c0 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 5e76a3f2c0d..14696c704fc 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 4486f7a5a6f..8c9c2f8f965 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 efeea52b722..b85793ff063 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 18157778765..5de7dc0c7c5 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 174951d6f00..97088d5854c 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 b27d650d9f8..f6285bdcf16 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`