tweak wording

Author: RalfJung

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 })
     }
 }
 

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);
                 }

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
 

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
 

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
 

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) {

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)