Keep Miri off the decoder's tables rather than off Stacked Borrows - #147
Conversation
`main` is red for the first time in this job's life, from the merge that added `iced-x86`. The failure is inside that crate: its byte reader casts an integer to a pointer (`mk_read_xx`, `ptr::read_unaligned(data_ptr as *const _)`), so the pointer carries no provenance and Stacked Borrows refuses to retag it -- in the decoder's own handler tables, on every decode. Measured on nightly rather than reasoned about, one test each: the workflow's flags (Stacked Borrows) fail ... plus -Zmiri-permissive-provenance fail ... with -Zmiri-tree-borrows instead pass So it is an aliasing-model disagreement about a dependency's internals, not a defect here, and permissive provenance alone does not reach it. The eighteen tests that decode are excluded from Miri; the job keeps Stacked Borrows. Moving the whole job to Tree Borrows was the alternative and is worse value: this job exists for *this* crate's unsafe code -- `dbgeng.rs` and `pool/**` decoding raw kernel structures out of byte slices, as `miri.yml` says -- and relaxing the model for all of that to cover a dependency's tables we cannot change either way is a bad trade. Nothing on the excluded path is an `unsafe` block of ours: `decode_operation` is safe Rust calling a safe API, so the exclusion costs no coverage of this crate. Verified locally over the whole suite, not just the four tests CI reached before it fail-fasted: 148 passed, 0 failed, 18 ignored under Miri, and 210 passed under the ordinary runner. The workflow's own "it has never failed" is no longer true, so it now says what happened instead -- including that this is exactly the cost it predicted when Miri moved off pull requests, and that `workflow_dispatch` is what a change like this one should have used. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ayv1beKpAVkmDJDLfYqoyf
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c016ea95ae
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| #[cfg_attr( | ||
| miri, | ||
| ignore = "decodes through iced-x86; see MIRI AND THE DECODER above" | ||
| )] |
There was a problem hiding this comment.
For every input in this test, split_instruction produces an empty byte slice, so decode_operation returns from its bytes.is_empty() branch before constructing an iced-x86 decoder. The same is true of test_an_unreadable_rendering_is_not_walked_through, while test_an_unread_instruction_set_reports_no_operands_and_no_flow returns on InstructionSet::Other; therefore these three ignores unnecessarily remove Miri coverage from paths that cannot trigger the dependency failure this change is isolating.
Useful? React with 👍 / 👎.
1 participant
mainis red for the first time in this job's life, from the merge that addediced-x86(#145).The failure is inside that crate. Its byte reader casts an integer to a pointer —
mk_read_xx, anunsafe { ptr::read_unaligned(data_ptr as *const _) }— so the pointer carries no provenance and Stacked Borrows refuses to retag it, in the decoder's own handler tables, on every decode.Measured, not reasoned about
One test, three flag sets, on nightly:
MIRIFLAGS-Zmiri-permissive-provenance-Zmiri-tree-borrowsinsteadAn aliasing-model disagreement about a dependency's internals, then, rather than a defect here — and permissive provenance alone does not reach it, which is worth knowing because the integer-to-pointer cast is what Miri warns about and is not what it refuses.
Why exclude the tests instead of switching the model
Moving the whole job to Tree Borrows was the alternative. This job exists for this crate's unsafe code —
miri.ymlnamesdbgeng.rsandpool/**, "decoding raw kernel structures out of byte slices, which is the most UB-prone code here" — and relaxing the model for all of that, in order to cover a dependency's tables we cannot change either way, is a bad trade.Nothing on the excluded path is an
unsafeblock of ours:decode_operationis safe Rust calling a safe API. So the exclusion costs no coverage of this crate, and ificed-x86ever needs Miri coverage the answer is a second job with-Zmiri-tree-borrows, not a weaker first one.A new decoding test that forgets the attribute turns
mainred, which is how this one was found. Self-correcting, not silent.Verification
Locally over the whole suite, not just the four tests CI reached before it fail-fasted:
I have also dispatched this workflow against this branch, so the box below is a real run rather than my word for it.
One doc change
miri.ymlsaid "It has never failed: 92 successes … across the last hundred", which is no longer true. It now records what happened, including that this is precisely the cost that comment predicted when Miri moved off pull requests, and thatworkflow_dispatchis what a change like this one should have used.🤖 Generated with Claude Code
https://claude.ai/code/session_01Ayv1beKpAVkmDJDLfYqoyf