-
Notifications
You must be signed in to change notification settings - Fork 349
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
running miri in release mode should disable debug assertions #2797
Comments
This is currently a deliberate choice -- unfortunately undocumented. (We should definitely at least fix the docs.) The reasoning is that Miri is anyway so slow that the benefit from the extra sanity checks outweighs the costs. OTOH I do agree that it can be confusing. I think we definitely want to keep overflow checks enabled (their cost in Miri is definitely negligible and this can find real bugs), I am less sure about regular debug assertions (which can actually be quite expensive). You can force debug assertions to be disabled with |
I just ran into this today when writing a reproducer for a reachable Also,
Soundness can often be sensitive to the particular profile settings. I've seen some crates which are unsound only when |
So are you advocating for Miri not setting any values here? What do you think about this consideration: #2497 |
I'm fine with Miri setting whatever it wants for |
There's no problem here though, is there? Reaching the
With overflow checks enabled, those crates then raise panics, which are still clearly pointing out there is a bug.
Yeah that is fair, I can see how this can be baffling when it comes unexpected. So it's about trading off the extra test coverage from having debug assertions and overflow checks enabled in more cases, against this element of surprise. |
Only once you examine the stack trace to find that it's the maybe-unchecked
In general, crates don't guarantee correct behavior following a panic, so you can end up hitting a bunch of overflows and the like from trying to use the broken state. But powering through them can be necessary to demonstrate that the broken state is truly unsound. (For instance, sometimes a data structure can be in a broken-but-still-sound state following a panic, but then it can enter a truly unsound state following another panic. To expose things like that, sometimes you need to panic in the right place.) Also, sometimes there's "nonsense" states, like with semantically incorrect implementations of traits (e.g., my example with a cryptographic block size of 0). These can rightly cause integer overflows and other incorrect behavior, but only violate an unsafe invariant further down the line. That is to say, not all incorrect behavior is necessarily a bug, if the library does not define any correct behavior for the given input. But it's important that this expected incorrect behavior does not make the library unsound.
If someone wanted that, couldn't they just run Miri without |
That might seem obvious to you but I don't think it is obvious in general. Anyway I explained my rationale above and that I think this is a trade-off. I am not dead set on the current behavior, but it's also not entirely clear to me that we want to change anything (except for the docs). I wonder what @saethlin and @oli-obk think. |
I suppose that's where we differ. To me, "please find some ordinary bugs" is |
My opinion is that Miri should do the least-surprising thing. Perhaps that means we should issue a warning when a user passes Maybe we could expand that to detecting if the selected profile has any non-zero |
I assume they didn't realize that applying optimizations means missing some UB? We certainly can't stop passing |
Yes, I think it is likely that they did not think through that, and that is why a sentence or two of warning could be the right thing here. At least in my experience, tools like ASan and UBsan are often used with optimizations and tend to find just as many bugs with optimizations on and off. So I suggest we should check the optimization level, and if it is not set to off, warn the user that optimizations will hide UB and therefore Miri is not doing them. |
FWIW Miri could totally run with optimizations and would still find at least as many bugs as ASan and UBSan. But I don't think we want to do that. |
Emit a warning when Miri is used with optimizations This may address rust-lang/miri#2797, by clarifying to the user what is going on and what the consequences of their choices are. Fixes rust-lang/miri#2797
Code
This currently passes with
cargo run --release
, but panics withcargo miri run --release
.Since debug assertions can actually change the behavior of a program, I think it would be useful to allow running miri with debug assertions disabled.
The text was updated successfully, but these errors were encountered: