-
-
Notifications
You must be signed in to change notification settings - Fork 14.1k
miri genmc: fix exit() handling #148991
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
base: main
Are you sure you want to change the base?
miri genmc: fix exit() handling #148991
Conversation
|
|
|
@oli-obk anything I can do to move this along? :) Or should I find another reviewer? The core interpreter changes are very small, just slightly weakening a sanity check that is getting in the way. |
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
@saethlin maybe you could take a look at this? |
|
r? saethlin |
In genmc mode, Miri does not want to stop execution when
exitis called. Instead we want to continue running other threads to ensure we covered all possible concurrent behaviors (including the ones where the exiting thread was delayed so the other threads took their turns first). However, the core interpreter has a sanity check that prevents us from just doing nothing inexit. This leaves us in a pickle: there's nowhere we can jump to (exit has return type!so there's no next block), but if we don't jump anywhere we ICE.The first commit fixes that by disabling the sanity check when there is no block to jump to. That still catches the mistake of forgetting to jump for the vast majority of shims.
We currently don't build Miri's genmc integration in rustc CI so I had to hack the feature into the bootstrap miri integration. That turned out to use the wrong Miri binary, which is fixed by the second commit: we can just rely on CARGO_BIN_EXE_miri, there's no need for a MIRI environment variable.
r? @oli-obk