Add a lot more information to SB fatal errors

[saethlin]

In fatal errors, this clarifies the difference between a tag not being present in the borrow stack at all, and the tag being present but granting SRO. It also introduces a little notation for memory ranges so we can mention to the user that the span may point to code that operates on multiple memory locations, but we are reporting an error at a particular offset.

This also gets rid of the unqualified phrase "the borrow stack" in errors, and clarifies that it is the borrow stack for some location.

The crate pdqselect v0.1.1:
Before:

2103 |     unsafe { copy_nonoverlapping(src, dst, count) }
     |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ no item granting read access to tag <2357> at alloc1029 found in borrow stack.

After:

2103 |     unsafe { copy_nonoverlapping(src, dst, count) }
     |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     |              |
     |              attempting a read access using <2357> at alloc1029[0x0], but that tag does not exist in the borrow stack for this location
     |              this error occurs as part of an access at alloc1029[0x0..0x4]

And the crate half v1.8.2
Before:

131 |     unsafe { &mut *ptr::slice_from_raw_parts_mut(data, len) }
    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ trying to reborrow for Unique at alloc1051, but parent tag <2091> does not have an appropriate item in the borrow stack

After:

131 |     unsafe { &mut *ptr::slice_from_raw_parts_mut(data, len) }
    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |              |
    |              trying to reborrow <2091> for Unique permission at alloc1051[0x0], but that tag only grants SharedReadOnly permission for this location
    |              this error occurs as part of a reborrow at alloc1051[0x0..0x6]

[saethlin]

Also, this is going to break the tests. I could do with some advice on fixing them. I'm not entirely sure what the methodology is.

[RalfJung]

Thanks a lot for the PR!

Just as a heads-up, I am busy with job interviews for probably at least another month, so it will be a while until I will be able to review this PR.

[saethlin]

Hm, I ran into this with ascii version 1.0.0. Not yet sure what's going on here, but this looks bug-like

test ascii_str::tests::as_mut_ascii_str ... note: tracking was triggered
    --> src/ascii_str.rs:998:16
     |
998  |             Ok(slice.into())
     |                ^^^^^^^^^^^^ created tag <271733>, granting Unique over alloc100517[0x0..0x2]
     |

... no other diagnostics...

error: Undefined Behavior: trying to reborrow for SharedReadOnly over alloc100517[0x0..0x2], but parent tag <271733> does not grant the required permission over this memory range
    --> /home/ben/.rustup/toolchains/miri/lib/rustlib/src/rust/library/core/src/cmp.rs:1538:27
     |
1538 |             PartialEq::eq(*self, *other)
     |                           ^^^^^ trying to reborrow for SharedReadOnly over alloc100517[0x0..0x2], but parent tag <271733> does not grant the required permission over this memory range
     |

[RalfJung]

This is a diagnostics PR, I fail to see the connection with that bug?

[saethlin]

You of course know SB better than I do, but this looks to me like a bug in Miri, probably a bug in this PR. I feel like a pointer that grants Unique over alloc100517[0x0..0x2] should be able to be reborrows into SRO over that same memory range.

I'm going to try minimizing whatever is causing this, just posting here for general awareness that this PR may be buggy.

[RalfJung]

I started to review this, but then noticed I am confused since I thought the main motivation is about better errors when a tag is missing. But then the PR also does a lot of things with CreatedPointerTag, introducing code duplication and odd functions like kind_to_perm_approximate that I am not sure really make sense. I think I would prefer for these changes to be done separately; in particular I am not convinced the new tag creation message is really better (printing "approximate" information seems potentially more damaging than helpful).

So, could you reduce this PR to just the part about better diagnostics on missing tags, and make a separate PR for the tag creation message change, including a motivation for that change? In particular, as you noticed, there is no such thing as the single permission that is granted to a new tag -- the same tag can have different permissions for different parts of memory, and when that is the case, the message needs to reflect this to avoid being plain wrong. This mismatch between the structure of Stacked Borrows and the message you want to print explains a lot of the complexity in this PR (the kind_to_perm_approximate function, and the code duplication for triggering CreatedPointerTag).

I'm also getting rid of the phrase "the borrow stack" in errors. From my own experience certainly and I think from my experience talking to people on the community Discord, it seems like people initially have the impression that there is one borrow stack. So a diagnostic that says "does not exist in the borrow stack" when tag-tracking only shows a creation of the tag and never removing it can be quite confusing.

I feel like the borrow stack is a core concept of Stacked Borrows (the name kind of gives it away ;), so I am not convinced that removing it from the messages is really helpful. What do you think about rewording the message to make it clear that this is "the borrow stack for location alloc1337+42", which hopefully should clarify that there is no single global borrow stack?

[RalfJung]

You of course know SB better than I do, but this looks to me like a bug in Miri, probably a bug in this PR. I feel like a pointer that grants Unique over alloc100517[0x0..0x2] should be able to be reborrows into SRO over that same memory range.

My guess would be that the parent tag simply does not exist in the borrow stack any more, and hence also cannot grant that permission.

EDIT: Oh, the point is that should have triggered a message that 271733 got removed? Hm, true. Would be good to have a small example reproducing the problem.

[saethlin]

What do you think about rewording the message to make it clear that this is "the borrow stack for location alloc1337+42", which hopefully should clarify that there is no single global borrow stack?

I'm really struggling to do this. I made a point of wording the diagnostics as "Tried to do X but not possible because Y" because I think that is a very easy form to read, and for the most part trying to mention borrow stacks seems to make them convoluted. Can you suggest a diff?

[RalfJung]

I'm really struggling to do this. I made a point of wording the diagnostics as "Tried to do X but not possible because Y" because I think that is a very easy form to read, and for the most part trying to mention borrow stacks seems to make them convoluted. Can you suggest a diff?

Looking at the source, the message actually uses the term "borrow stack" where I would expect it to show up. :)

However, are the messages in the OP still up to date? In particular the last one seems odd, since in the code it looks like "does not grant the required permission over" is only printed for untagged parents.

[saethlin]

Just over a week ago I was trying to turn off GitHub email notifications and I accidentally turned them all off for a few days. I knew something would slip through. Gah!

I've updated the diagnostic you mentioned in the OP (and I rebased onto master).

[saethlin]

Along with addressing your feedback, I squashed this back down and rebased it onto master. I'm working on some other branches and I didn't want to deal with swapping between miri toolchains.

[RalfJung]

"via tag" sounds odd to me, I think something about "derived from tag" or "from parent tag" or so is more evocative.

[saethlin]

I'm concerned that both "derived from tag" and "from parent tag" are both too suggestive that only the permission is from the tag.

I went back and forth with some other people and came up with other wordings which are very similar to your original ones 😂

[RalfJung]

Yeah I think I like these wordings you have now. :)

[saethlin]

Squashed down and apparently I got too fancy somewhere so this is now rebased onto master.

[oli-obk]

@bors r=RalfJung

[bors]

📌 Commit 730cd27 has been approved by RalfJung

[bors]

⌛ Testing commit 730cd27 with merge 670dc7d...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 670dc7d to master...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 670dc7d to master...