Skip to content

Fix codegen panic for calls through a function pointer returning !#4647

Open
MavenRain wants to merge 1 commit into
model-checking:mainfrom
MavenRain:4577-fnptr-never-codegen
Open

Fix codegen panic for calls through a function pointer returning !#4647
MavenRain wants to merge 1 commit into
model-checking:mainfrom
MavenRain:4577-fnptr-never-codegen

Conversation

@MavenRain

Copy link
Copy Markdown

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:

fn diverge() -> ! {
    loop {}
}

#[kani::proof]
fn check_fnptr_never() {
    let f: fn() -> ! = diverge;
    f();
}

Kani panicked during codegen:

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:
called `Option::unwrap()` on a `None` value
  ...
  <GotocCtx>::codegen_funcall

In codegen_funcall, the function-pointer (RigidTy::FnPtr) branch ended the
call with:

Stmt::goto(bb_label(target.unwrap()), loc)

A call whose callee returns ! diverges, so MIR gives it no return target and
target is None; the unconditional unwrap() then panics. The sibling
branch for direct (RigidTy::FnDef) calls does not have this problem because
it ends the call with codegen_end_call, which already handles a missing
target 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_call helper,
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

  • Added tests/kani/Never/fn_ptr_never_return.rs, a regression test that calls
    a fn() -> ! pointer. The callee panics, so the harness reaches the panic
    and verification fails as expected (// kani-verify-fail); before this fix
    the compiler crashed instead of producing any verification result. Built
    Kani (cargo build-dev) and ran it: the harness reports
    VERIFICATION:- FAILED with Failed Checks: EXPECTED FAIL: diverging function was called, i.e. codegen completes and CBMC runs.
  • Ran the exact reproducer from the issue (the loop {} variant) against the
    built Kani: it no longer panics during codegen and proceeds into CBMC.
  • cargo check -p kani-compiler passes.

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.

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>
@MavenRain
MavenRain requested a review from a team as a code owner July 16, 2026 06:23
@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 16, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Reachable unwrap() panic in statement codegen for function pointer returning !

1 participant