Avoid duplicating error message in title

[ibraheemdev]

Error output currently repeats the full error message in the title as well as the span message:

error: Undefined Behavior: no item granting read access to tag <1997> at alloc994+0x1 found in borrow stack.
 --> src/main.rs:5:9
  |
5 |         dbg!(*ptr.add(1));
  |         ^^^^^^^^^^^^^^^^^ no item granting read access to tag <1997> at alloc994+0x1 found in borrow stack.

This gets noisy because messages are often quite long. This PR changes the title to a constant Undefined Behavior:

error: Undefined Behavior
 --> src/main.rs:5:9
  |
5 |         dbg!(*ptr.add(1));
  |         ^^^^^^^^^^^^^^^^^ no item granting read access to tag <1997> at alloc994+0x1 found in borrow stack.

[RalfJung]

Thanks for the PR!

This was to an extend deliberate since I figured the title might be easier to find/read than a message attached to the span. I take your point about redundancy and long messages though.

@saethlin I wonder what you think about this, given you have been working on SB error messages recently?

[RalfJung]

If the goal is to avoid redundancy, we should also do something about the title == None case here.

The only errors that can trigger this are MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. }... so maybe we should just come up with a title for them? Any suggestions?

[saethlin]

@saethlin I wonder what you think about this, given you have been working on SB error messages recently?

I think this PR is moving in a good direction.

IMO the biggest problem with the SB errors is that they emit a lot of text, and most of it doesn't help the user fix the problem that's being reported. At the moment it basically emits the same text twice, then suggests a user may want to ignore the error or perhaps consult a piece of reference material.

I think for this PR, it would be really nice if we could make better use of the top line. I don't know about other users, but my eyes jump to text in the span. I suspect I've been trained by rustc errors that all of the useful stuff is there. What if SB errors looked like this:

error: this operation is undefined behavior according to stacked borrows, an experimental aliasing model
  --> src/main.rs:5:18
   |
5  |         let _x = *ptr.add(1);
   |                  ^^^^^^^^^^^ no item granting read access to tag <1981> at alloc954+0x1 found in borrow stack.
   |

note: inside `main` at src/main.rs:10:5
  --> src/main.rs:10:5
   |
10 |     func()
   |     ^^^^^^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error

In this sketch, I'm focusing on moving boilerplate out of the middle of the output. I think we can rely on new users putting stacked borrows into a search engine, if by some miracle they managed to find Miri before learning about stacked borrows. But if we must have a URL in there, it could be on its own line at the top to not sandwich it in the middle of the stacktrace (because the top span is part of the trace).

[RalfJung]

We use that info line below the first span for other error types besides Stacked Borrows though. We started doing that when there was feedback that users didn't know whether an error they got was a bug in their program or a gap in what Miri can support. I think we should continue to make that very explicit, like we do now.

IMO the biggest problem with the SB errors is that they emit a lot of text, and most of it doesn't help the user fix the problem that's being reported.

The primary goal of that text is to make the user even understand what the problem is. That's already hard enough. I haven't even started thinking about automatically helping people to fix the problem, that seems near impossible.^^

I think your proposed message removes too much context. People pick up Miri for various reasons, I would not expect that they even have a good understanding of Undefined Behavior, let alone have heard about Stacked Borrows.

[RalfJung]

The failing test suite also shows that there is another reason why we have the error in the title: we need that for compile-fail tests.

So I think if we want to do this, we first need to switch those to ui tests. That is something that has been loosely on my radar for a bit, but never rose to the top of my list.

[saethlin]

The primary goal of that text is to make the user even understand what the problem is. That's already hard enough. I haven't even started thinking about automatically helping people to fix the problem, that seems near impossible.^^

I agree that we should be helping people understand what the problem is. I'm just determined to pull this off with the error messages, not a URL to reference material. Perhaps I'm still suffering the optimism of youth, but I have quite a few more PRs to go yet.

[RalfJung]

I think including URLs to external material is a great way to connect the little information we can provide here, to the greater context. I view this as akin to rustc's --explain.

But this is steering rather off-topic for this PR. :D The question is whether we want to stop repeating ourselves in the error message. I agree redundancy is a waste of space. Then the question is which of the repeated messages to remove, and indeed the one in the title probably makes more sense as Rust often has the detailed info on the span (though I have also seen people argue that we should keep the "short" error output, which only prints the titles and not the span-labels, useful).

I think we should always have a rather general title then (so, turn title into a String, making it no longer Optional). However, the harder part of this is to stop relying on the title for our compile-fail test suite. We can't remove the error details from the title until we did that. I might be doing some experimenting later.

[RalfJung]

So, this is blocked on #2027.

[bors]

☔ The latest upstream changes (presumably #1971) made this pull request unmergeable. Please resolve the merge conflicts.

[RalfJung]

#2027 has landed, so we can now match against notes attached to the span, not just the top-level errors. (And #2167 will make this work the way it should.)

However, I am not sure if making the error text just 'Undefined Behavior' is truly what we want. Consider this error:

error: Undefined Behavior: pointer arithmetic failed: alloc1655 has size 4, so pointer to 1 byte starting at offset -1 is out-of-bounds
   --> /home/r/.rustup/toolchains/miri/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:455:18
    |
455 |         unsafe { intrinsics::offset(self, count) }
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ pointer arithmetic failed: alloc1655 has size 4, so pointer to 1 byte starting at offset -1 is out-of-bounds
    |
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information

IMO a good way to avoid redundancy would be something like

error: Undefined Behavior: pointer arithmetic failed
   --> /home/r/.rustup/toolchains/miri/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:455:18
    |
455 |         unsafe { intrinsics::offset(self, count) }
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ alloc1655 has size 4, so pointer to 1 byte starting at offset -1 is out-of-bounds
    |
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information

Basically, the error title should probably still contain something slightly more specific than just 'Undefined Behavior'. This will require a change on the rustc side to enable getting both the 'title' and 'text' of an error message (or so).

@ibraheemdev is that something that you would still like to work on?

[RalfJung]

@ibraheemdev I haven't heard from you in a while, so I am going to close this PR. I'll open an issue to track reducing our redundancy here. If you want to pick this up some day, just let us know. :) However, anyone else reading this should also feel free to pick this up if they want to.

[RalfJung]

Tracking this in #2200

[ibraheemdev]

@RalfJung sorry, I don't really have the motivation to work on this. Opened because it seemed like a quick fix :)

[RalfJung]

That's totally fair; thanks for the inspiration!