Add miri specific attributes to selectively turn errors into warnings

[Robbepop]

Problem Description

In the codebase I am working on I have the problem that miri identified some stacked borrows violation that could potentially point to a bug in my code.
Using -Zmiri-track-pointer-tag=N I was able to pin down the source but still couldn't identify a real problem with the code.
Since the future goal is to include miri into our CI toolchain and reject patches that are troublesome to miri (e.g. undefined behaviour) it would be nice to have a way to ignore certain miri errors in case they are false positives.

Current State

What is currently possible is to disable a whole category of checks entirely using some -Zmiri-* flags, however, this is bad because then miri is more likely to accept incorrect code.

Proposed Solution

So what I'd actually would like to have is some recognized built-in attributes with which I can tell miri to disable certain checks or turn them into warnings instead just as it is already been done in other Rust tools such as rustc, clippy or rustfmt etc.

Example

For example, if I want to turn the stacked borrows check for a scope into a mere warning I'd do the following:

fn foo() {
    // code that is checked with default settings
    #[miri::warn(stacked_borrows)]
    {
        // code that is checked with stacked borrows turned into warnings instead of errors
    }
    // code is checked with default settings at this point again
}

Other syntax could be #[warn(miri::stacked_borrows)] etc.
As with attributes of other Rust tools they should be ignored if the source code is not compiled or inspected by those.

Motivation

Having this would allow us to incrementally decide whether some code is correctly identified by miri as incorrect and allows to filter out certain false positives. Turning them into warnings instead of disabling them for specific parts of the code allows us to monitor filtered miri false positives over a longer period of time and track them better in case miri fixes them.

[RalfJung]

Thanks for the detailed proposal!

I think that this is basically a duplicate of #797, but with a more concrete proposal for what the interface for locally controlling these warnings could look like. Would you agree?

I should also note that it is entirely unclear if "selectively disable Stacked Borrows" makes sense. It might well be that the Stacked-Borrows-incorrect code screws up the aliasing state so much that there is no way to meaningfully continue checking aliases. But that is something only experiments will be able to show.

Using -Zmiri-track-pointer-tag=N I was able to pin down the source but still couldn't identify a real problem with the code.

Could you open a separate issue for that, with a pointer to the code or ideally a small self-contained example demonstrating the problem? I hope we can help you figure out what the problem is.

[RalfJung]

Oh also I should say, I really like your idea of using attributes and scopes to control these warnings! I have no idea how to implement that, but the concept is great. :)

[Robbepop]

I think that this is basically a duplicate of #797, but with a more concrete proposal for what the interface for locally controlling these warnings could look like. Would you agree?

Haven't noticed the issue before but I agree. I just thought that miri could just do what the other established Rust tools already are doing. This way the analyzed crate decides how miri works on it. E.g. if you want to disable stacked borrow analysis on the crate-level you'd simply put a #![allow(miri::stacked_borrows)] on your lib.rs file very similar to how you enable or disable certain clippy lints. Same applies to other tools such as rustfmt where you can for example skip certain parts (scope based) of your code using #[rustfmt::skip].

Could you open a separate issue for that, with a pointer to the code or ideally a small self-contained example demonstrating the problem? I hope we can help you figure out what the problem is.

Cool! I didn't know that issues like these were actually welcome in this repository. Will make a detailed post about the problem, how to reproduce and hopefully with some minimization of the underlying code. In the end we can either earn a trophy for miri or we find insights for the stacked borrow model.

[RalfJung]

Cool! I didn't know that issues like these were actually welcome in this repository.

They definitely are. :)

I just thought that miri could just do what the other established Rust tools already are doing.

The other tools all just take a static look at the code, Miri actually runs the code. That's very different.

But let's close this as a duplicate of #797 then, and continue the discussion there.