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

[ivmat]

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.

[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.

[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]

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

[ivmat]

@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