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, and what was not run

• cargo build -p kani-compiler on this branch — passes.
• The two UI tests were verified by direct invocation against a locally built driver/compiler,
  comparing output against expected the same way compiletest's verify_output does.

Stated plainly rather than left to be assumed:

• compiletest itself was not run. It invokes a binary named kani resolved through PATH, which
  in a source checkout is the kani-verifier proxy resolving ${KANI_HOME}, not the local build.
  Wiring that up would have meant installing over the machine's global Kani install.
• clippy was not run — it is not installed for the pinned nightly toolchain, and installing it
  would have mutated the pin.

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]

These new UI tests are likely too easy to inline away. Both cover-non-literal-message and assert-non-literal-message use tiny helper functions. Copilot noted these helpers may be inlined, which could turn the call back into a literal at the call site and stop exercising the intended non-literal-message path. That would weaken the regression test and make it flaky across optimization settings/toolchain changes. A stronger test would prevent inlining explicitly or use a setup that preserves the non-literal expression form.

[feliperodri]

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

[feliperodri]

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