Remove the unreachable deref_box - #4861
srivatsansamraj wants to merge 1 commit into
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Copilot review overview
Review effort: Lite
Findings: 1
Open (2)
What changed in this PR
Removes the unreachable deref_box path in Kani’s MIR Deref projection handling by relying on rustc’s ElaborateBoxDerefs lowering, and adjusts pointer-wrapper handling to better match current std layouts.
Changes:
- Deleted
GotocCtx::deref_boxand removed theBoxderef branch inProjectionElem::Deref, replacing it with an assertion. - Updated pointer wrapper (un)wrapping utilities to treat Rust fat pointers as pointers rather than wrappers.
- Added a codegen-only regression test for boxed
dyn Fncreated from a function item.
| File | Description |
|---|---|
| tests/kani/DynTrait/boxed_fn_item.rs | Adds a codegen-only regression test exercising boxed trait-object function items. |
| kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs | Removes deref_box and refines wrapper handling (fat pointers, wrapper peeling, NonNull layout checks). |
| kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | Removes the Box deref branch and asserts Box deref is unreachable after rustc lowering. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| /// pointer: pattern_type!(*const T is !null), | ||
| /// } | ||
| /// ``` | ||
| /// The `pointer` field is not a bare pointer: the pattern type is itself codegenned as a |
rustc's `ElaborateBoxDerefs` pass, whose policy is `Required`, rewrites every deref of a `Box` into a deref of its raw pointer, so the `is_box()` branch of the `Deref` projection is never taken. With a panic at the top of `deref_box`, no test in the kani, expected, cargo-kani or script-based-pre suites reached it. The `Deref` arm now asserts that its base is not a `Box`.
33282e8 to
84ca4d3
Compare
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
Approving the change, which is correct. It needs a rebase first: #4801 was squash-merged, so its commits here conflict with main, and only the last commit should remain.
I checked the one case the description doesn't cover: shims. make_shim doesn't run ElaborateBoxDerefs, so a shim that derefs a Box directly would now hit the assertion. None does in practice. Drop glue (Box<Vec<_>>, Box<dyn Debug>, Box<Box<_>>, Box<[String]>), a Box<dyn FnOnce> call through the vtable shim, a Box<Self> receiver via dyn, and closure-once and clone shims all verify without reaching it. With the assertion in place, kani, expected, cargo-kani and script-based-pre pass: 1,237 tests, no hits.
On Copilot's point about assert!: I'd keep it. It guards an invariant of rustc's MIR, not something a user can trigger, so an ICE naming the type is the right failure.
| }; | ||
| // rustc's `ElaborateBoxDerefs` pass replaces every deref of a `Box` with a deref | ||
| // of its raw pointer. | ||
| assert!(!base_type.kind().is_box(), "Unexpected deref of {base_type:?}"); |
There was a problem hiding this comment.
Suggestion: Worth adding to this comment that shims don't run ElaborateBoxDerefs, and are still covered because the ones that touch a Box reach its contents through the raw pointer: drop elaboration does so explicitly. That's the case someone will wonder about when this fires, and the first place to look.
Removes
deref_boxand theis_box()branch of theDerefprojection that called it. rustc'sElaborateBoxDerefspass rewrites every deref of aBoxinto a deref of its raw pointer before Kani sees the body, so the branch could not be reached. The pass always runs: its policy isRequired, with the comment that it implements Box dereference semantics so that backends and Miri do not have to.The
Derefarm now asserts that its base is not aBox. If a future rustc, or a body Kani builds itself, ever derefs aBoxdirectly, compilation stops and names the type.Tested as proposed in #4858. With a
panic!at the top ofderef_box, no test in thekani,expected,cargo-kaniorscript-based-presuites reached it: 1,234 tests, includingverify_std_cmd, which compiles the standard library. The same four suites pass with this change.box_valueandcodegen_ptr_out_of_wrappersare now the only code that walks theBoxfield chain.This builds on #4801, which changed
deref_box. Only the last commit is new here.Resolves #4858
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.