Fix ICE on non-literal `cover`/`assert`/`check` message expressions by ivmat · Pull Request #4711 · model-checking/kani

ivmat · 2026-08-03T22:50:10Z

Problem

kani-compiler's codegen hooks for kani::cover, kani::assert, kani::check and the internal
safety-check/unsupported-check hooks all call gcx.extract_const_message(&msg).unwrap() to recover the
message string.

extract_const_message returns None whenever the message operand does not codegen down to a
string-literal constant — for example when it is a function parameter — so the .unwrap() produces an
internal compiler error rather than a normal diagnostic.

Reproducer (kani::cover case):

#[kani::proof]
fn main() {
    let msg = "not a literal";
    kani::cover!(true, msg);
}

This still reproduces on main: all six extract_const_message(&msg).unwrap() call sites are present
in kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs.

Fix

Add extract_msg_or_err, which mirrors the existing utils::span_err + abort_if_errors pattern
already used by neighbouring intrinsic codegen in the same file, and use it at all six call sites
(Cover, Assert, UnsupportedCheck, SafetyCheck, SafetyCheckNoAssume, Check).

Each now emits a spanned `<construct>` message must be a string literal error and aborts
compilation cleanly instead of panicking.

Tests

UI regression tests modelled on the existing tests/ui/ice-size-overflow test (a prior
"ICE → clean error" regression test):

tests/ui/cover-non-literal-message/
tests/ui/assert-non-literal-message/

kani::check is pub(crate) in library/kani_core/src/lib.rs with no public re-export, so user code
cannot invoke it directly (it fails earlier with E0425). The remaining hooks
(safety_check, safety_check_no_assume, unsupported_check) are compiler-generated and not
reachable from user code either, so neither is given a UI test.

Testing performed

cargo build -p kani-compiler and cargo check -p kani-compiler on this branch — pass.
Full local regression via compiletest (--force-rerun, all suites + unit tests): 1472 passed,
3 failed — all 3 reproduce identically on a clean main checkout (2b7972b7c), so they are
pre-existing environment issues (one requires z3, which is not installed here), not caused by this
change.
cargo clippy on the pinned nightly — clean.
scripts/kani-fmt.sh --check and the copyright/format checks — clean.
The two new UI tests fail as expected when the fix is reverted (negative control).

Happy to adjust the diagnostic wording or the test placement if you'd prefer something different.

`kani-compiler`'s codegen hooks for `kani::cover`, `kani::assert`, `kani::check` and the internal safety-check/unsupported-check hooks all called `gcx.extract_const_message(&msg).unwrap()` to recover the message string. `extract_const_message` returns `None` whenever the message operand does not codegen down to a string-literal constant -- for example when it is a function parameter -- which turned the `.unwrap()` into an internal compiler error instead of a normal diagnostic. Add `extract_msg_or_err`, mirroring the existing `utils::span_err` + `abort_if_errors` pattern already used by neighbouring intrinsic codegen in this file, and use it at all six call sites in `hooks.rs` (Cover, Assert, UnsupportedCheck, SafetyCheck, SafetyCheckNoAssume, Check). Each now emits a spanned "`<construct>` message must be a string literal" error and aborts compilation cleanly instead of panicking. Add UI regression tests for the two publicly reachable constructs, `kani::cover` and `kani::assert`, modelled on the existing `tests/ui/ice-size-overflow` test. `kani::check` is `pub(crate)` with no public re-export, so user code cannot invoke it directly.

Copilot

Pull request overview

This PR prevents internal compiler errors in kani-compiler when kani::cover, kani::assert, kani::check, and related internal hooks are given a non-literal message expression by emitting a proper diagnostic and aborting compilation cleanly instead of panicking.

Changes:

Added extract_msg_or_err helper in kani-compiler hook codegen to replace extract_const_message(...).unwrap() at the six affected hook sites.
Updated the hook implementations to produce a spanned error: `<construct>` message must be a string literal.
Added UI regression tests for the kani::cover and kani::assert non-literal message cases.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs	Replaces `unwrap()` on non-literal hook messages with a diagnostic + abort path via `extract_msg_or_err`.
tests/ui/cover-non-literal-message/main.rs	New UI test ensuring `kani::cover` with a non-literal message produces a clean compiler error (no ICE).
tests/ui/cover-non-literal-message/expected	Expected diagnostic output for the new `cover` UI test.
tests/ui/assert-non-literal-message/main.rs	New UI test ensuring `kani::assert` with a non-literal message produces a clean compiler error (no ICE).
tests/ui/assert-non-literal-message/expected	Expected diagnostic output for the new `assert` UI test.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

`extract_msg_or_err` documents itself as aborting compilation when a hook message is not a string literal, but the `unwrap_or_else` fallback returned `String::new()` after `abort_if_errors()`. `abort_if_errors()` returns `()`, not `!`, so nothing in the types stopped codegen from continuing with an empty message if it ever failed to fire. Return `unreachable!("Rustc should have aborted already")` instead, matching the `abort_if_errors()` + `unreachable!()` pairing already used in `codegen/intrinsic.rs`, `context/goto_ctx.rs` and `kani_middle/transform/contracts.rs`. The `unreachable!` is not reachable in practice: `DiagCtxtHandle::span_err` returns `ErrorGuaranteed` and pushes onto `err_guars`, so the following `abort_if_errors()` always finds an error and unwinds with `FatalError`. Both UI tests added by this PR still produce a clean `error:` diagnostic and no ICE.

Copilot

Pull request overview

Copilot reviewed 5 out of 5 changed files in this pull request and generated no new comments.

Suppressed comments (2)

tests/ui/cover-non-literal-message/main.rs:21

This UI test relies on passing the message through a helper function parameter to make it “non-literal at the call site”. Because cover_with_msg is tiny, rustc/MIR optimizations could inline it and turn this back into a direct kani::cover(true, "...") call, which would stop exercising the non-literal-message path and weaken the regression test.

fn cover_with_msg(cond: bool, msg: &'static str) {
    kani::cover(cond, msg);
}

tests/ui/assert-non-literal-message/main.rs:21

This UI test depends on the message being a function parameter at the kani::assert call site. Since assert_with_msg is small, it may be inlined by optimizations, turning the call back into a direct literal and no longer covering the intended non-literal-message behavior.

fn assert_with_msg(cond: bool, msg: &'static str) {
    kani::assert(cond, msg);
}

feliperodri · 2026-08-05T20:20:17Z

+    gcx.extract_const_message(msg_expr).unwrap_or_else(|| {
+        utils::span_err(gcx.tcx, span, format!("`{construct}` message must be a string literal"));
+        gcx.tcx.dcx().abort_if_errors();
+        unreachable!("Rustc should have aborted already")


This message could be way more descriptive to tell the user when it sees this message why rustc should have aborted already.

Both tests make the hook message non-literal by passing it through a helper function parameter. Kani passes no `-C opt-level` or `-Z mir-opt-level`, so the MIR inliner is off and the helpers survive today, but nothing in the tests said so. If the helpers were ever inlined the message would fold back into a literal and the tests would stop exercising the path they exist to cover. `#[inline(never)]` pins that down. Verified: with `#[inline(always)]` and `-Zmir-opt-level=4 -Zinline-mir=yes` the diagnostic disappears and codegen proceeds; with `#[inline(never)]` it is still emitted under the same flags.

feliperodri · 2026-08-05T20:21:02Z

@ivmat could you also tackle the two suppressed Copliot comments? Almost there.

…sage The fallback in `extract_msg_or_err` runs only if `abort_if_errors` returns after an error has been emitted, which cannot happen: `span_err` emits a hard error, so `abort_if_errors` observes it and raises a fatal error first. State that invariant in the code rather than asserting it. The panic message now says what must have gone wrong if it ever does fire -- the error was not counted by the diagnostic context -- and interpolates `construct` so it names the hook being codegen'd.

ivmat · 2026-08-06T17:35:16Z

@ivmat could you also tackle the two suppressed Copliot comments? Almost there.

@feliperodri i think i covered everyting now. i also could not rerrun all same CI tests locally but i dont think there should be any issues

ivmat requested a review from a team as a code owner August 3, 2026 22:50

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 3, 2026

ivmat force-pushed the fix-ice-non-literal-message branch from 72f4f5a to 4fa8466 Compare August 3, 2026 23:34

feliperodri added this to the Maintenance milestone Aug 4, 2026

feliperodri requested a lite review from Copilot August 5, 2026 16:54

Copilot started reviewing on behalf of feliperodri August 5, 2026 16:55 View session

Copilot AI reviewed Aug 5, 2026

View reviewed changes

Comment thread kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

feliperodri assigned ivmat Aug 5, 2026

feliperodri requested a lite review from Copilot August 5, 2026 19:53

Copilot started reviewing on behalf of feliperodri August 5, 2026 19:53 View session

Copilot AI reviewed Aug 5, 2026

View reviewed changes

feliperodri requested changes Aug 5, 2026

View reviewed changes

feliperodri added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Aug 5, 2026

feliperodri approved these changes Aug 6, 2026

View reviewed changes

feliperodri enabled auto-merge August 6, 2026 18:17

Navigation Menu

Uh oh!

Fix ICE on non-literal `cover`/`assert`/`check` message expressions - #4711

Fix ICE on non-literal `cover`/`assert`/`check` message expressions#4711
ivmat wants to merge 4 commits into
model-checking:mainfrom
ivmat:fix-ice-non-literal-message

ivmat commented Aug 3, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

feliperodri Aug 5, 2026

Uh oh!

feliperodri commented Aug 5, 2026

Uh oh!

ivmat commented Aug 6, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

ivmat commented Aug 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem

Fix

Tests

Testing performed

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

feliperodri Aug 5, 2026

Choose a reason for hiding this comment

Uh oh!

feliperodri commented Aug 5, 2026

Uh oh!

ivmat commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ivmat commented Aug 3, 2026 •

edited

Loading

ivmat commented Aug 6, 2026 •

edited

Loading