suppressions support

[spacejam]

Hey, I'd like to make miri a part of sled's standard testsuite, as I use a lot of unsafe code for handling lock-free algorithms etc... However, I'm hitting issues in dependencies long before I'm making much progress in my own code. I'd like to be able to have miri follow a TSAN-like suppressions list that allows me to notify the upstream authors of findings but then ignore issues in their code for future tests.

Did I miss already existing functionality that would satisfy this? If not, would it be feasible to implement similar filtering logic? I'm happy to help code some parts if you give me a high-level set of opinions about the best touchpoints and any dos and don'ts that pop into your head before jumping into coding.

[RalfJung]

Did I miss already existing functionality that would satisfy this?

You did not.

If not, would it be feasible to implement similar filtering logic?

That depends on the errors you are hitting. Many things Miri raises are of the form "I need some data to continue, and there just isn't any code path handling what to do without that data", and you couldn't suppress those without a lot of work (out-of-bounds memory accessed come to mind). Others are of the form "let's call these extra checks because those are invariants we want", and just skipping those would not be a big deal (this includes things such as alignment checks, validity invariants and Stacked Borrows).

So, some errors could be suppressed with limited amount of work, while for others I wouldn't even know what that would mean. We can start with those where it is easy though. Also I am a bit worried that this might clutter all our code with "catch that error and find some way to continue in case it is suppressed". We also in some places have assert! or unwrap that we know is okay because we would have terminated execution before if it is not, and I'd like to avoid making more operations fallible or decreasing our test coverage by removing assertions. We have to weigh this new feature against maintainability of the code base. It's very hard to exhaustively test an interpreter, so having the code well-structured and well-readable is very important to me. But there might be ways, such as skipping some assertions if suppressing is enabled or so.

I generally like this idea though! It probably makes sense to do a bit of design work (in particular around what the suppression file looks like and how one would go about checking if some failure is suppressed) before starting coding. In particular, the wording of our error messages is not very stable (and will likely change again when I finally get around to #417), so there is the question of how to specify which error is being suppressed. Maybe it's best to start with a mechanism that can just basically filter the stack trace to suppress any kind of error.

Also many of these errors that you could suppress currently relentlessly allocate strings because we know they will not be caught, so there is no performance penalty. And I'd rather not create a dedicated error enum variant for every one of them, that's just so painful. So at least in a first iteration you might experience some performance problems. That said, Miri is so slow that you might not even notice. ;)

[spacejam]

Thinking about my issue a bit more, the main thing I need to do is skip over other people's code that I don't control, so I can focus on my own problems first. I'm not sure if there's an opportunity to bridge interpreted and non-interpreted code in a way that does not incur as much complexity, but maybe that's another way that complexity could be distributed.

[RalfJung]

I don't see any feasible way in which we could jump between interpreted mode and the LLVM-generated binary.

[RalfJung]

Maybe this could be folded into #797, where we turn these "suppressable" errors into err-by-default "lints" that can be "allowed" in a way that depends on the current stack, or so.

[RalfJung]

Closing as duplicate of #797