Fix codegen panic for calls through a function pointer returning !#4647
Open
MavenRain wants to merge 1 commit into
Open
Fix codegen panic for calls through a function pointer returning !#4647MavenRain wants to merge 1 commit into
!#4647MavenRain wants to merge 1 commit into
Conversation
Calling a function pointer whose return type is the never type `!` panicked
the compiler in `codegen_funcall`. The function-pointer branch built the
call's continuation with `Stmt::goto(bb_label(target.unwrap()), loc)`, but a
call that diverges (return type `!`) has no return target, so `target` is
`None` and the `unwrap()` panicked:
thread 'rustc' panicked at .../codegen/statement.rs:
called `Option::unwrap()` on a `None` value
The sibling branch for direct (`FnDef`) calls already handles this: it ends
the call with `codegen_end_call`, which emits an unreachable sanity check when
there is no return target. Route the function-pointer branch through the same
helper so both paths behave identically.
Resolves model-checking#4577
Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Fixes a compiler panic when Kani codegens a call through a function pointer
whose return type is the never type
!.Context
Given the minimal reproducer from #4577:
Kani panicked during codegen:
In
codegen_funcall, the function-pointer (RigidTy::FnPtr) branch ended thecall with:
A call whose callee returns
!diverges, so MIR gives it no return target andtargetisNone; the unconditionalunwrap()then panics. The siblingbranch for direct (
RigidTy::FnDef) calls does not have this problem becauseit ends the call with
codegen_end_call, which already handles a missingtarget by emitting an unreachable "Unexpected return from Never function"
sanity check instead of a goto.
Change
Route the function-pointer branch through the same
codegen_end_callhelper,so a diverging call through a function pointer is handled exactly like a
diverging direct call. This is a one-line change; the diverging case is now
covered by the existing, tested code path.
Testing
tests/kani/Never/fn_ptr_never_return.rs, a regression test that callsa
fn() -> !pointer. The callee panics, so the harness reaches the panicand verification fails as expected (
// kani-verify-fail); before this fixthe compiler crashed instead of producing any verification result. Built
Kani (
cargo build-dev) and ran it: the harness reportsVERIFICATION:- FAILEDwithFailed Checks: EXPECTED FAIL: diverging function was called, i.e. codegen completes and CBMC runs.loop {}variant) against thebuilt Kani: it no longer panics during codegen and proceeds into CBMC.
cargo check -p kani-compilerpasses.Resolves #4577
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.