Emit a diagnostic for a misapplied checked size/align intrinsic marker

[MavenRain]

Description

Fixes a compiler panic when the internal CheckedSizeOfIntrinsic (or
CheckedAlignOfIntrinsic) fn_marker is attached to a function whose
signature does not match the intrinsic.

Context

From the reproducer in #4589:

enum BadRet {
    None,
}

#[kanitool::fn_marker = "CheckedSizeOfIntrinsic"]
fn fake_checked_size_of(ptr: *const u8) -> BadRet {
    let _ = ptr;
    BadRet::None
}

#[kani::proof]
fn check() {
    let p = &0u8 as *const u8;
    let _ = fake_checked_size_of(p);
}

Kani panicked during codegen:

thread 'rustc' panicked at kani-compiler/src/kani_middle/transform/kani_intrinsics.rs:
called `Option::unwrap()` on a `None` value
  ...
  kani_compiler::kani_middle::transform::kani_intrinsics::build_some

The checked_size_of / checked_align_of generators assume the marked
function has the signature of the real intrinsic (a raw pointer argument and an
Option<usize> return), and build_some / build_none locate the Some /
None variants by looking for a variant with (or without) a field. The
fn_marker attribute is internal, but nothing stops user code from attaching
it to a function returning some other type; BadRet has no variant with a
field, so build_some unwrapped a None and the compiler panicked.

Change

Validate the marked function's signature before generating the body. When it
is not a raw pointer argument with an Option-shaped return, emit a normal
compiler error instead of panicking. This matches how Kani already reports
other misapplied kani-internal attributes. The valid intrinsic path is
unchanged.

Testing

• Added tests/ui/invalid-intrinsic-marker/, which runs the reproducer and
  checks for the new diagnostic:

  error: the `CheckedSizeOfIntrinsic` intrinsic marker can only be applied to a function with a raw pointer argument that returns `Option<usize>`
  

  Verified it passes via compiletest --suite ui --mode expected.

• Confirmed no regression to the real intrinsic path: the existing
  tests/kani/SizeAndAlignOfDst/unsized_tail.rs still verifies successfully
  (9/9 harnesses).

• cargo check -p kani-compiler passes and the file is rustfmt-clean.

Resolves #4589

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This PR prevents a compiler panic when the internal CheckedSizeOfIntrinsic / CheckedAlignOfIntrinsic fn_marker is attached to a function with an incompatible signature, by validating the marked function signature and emitting a proper diagnostic instead of panicking during intrinsic body generation.

Changes:

• Add a signature guard for CheckedSizeOf / CheckedAlignOf marker-handling to emit a diagnostic on mismatches.
• Introduce has_checked_intrinsic_sig helper to validate the expected argument/return shape before running the generators.
• Add a new UI regression test reproducing issue #4589 and asserting the new diagnostic.

Reviewed changes

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

File	Description
kani-compiler/src/kani_middle/transform/kani_intrinsics.rs	Adds signature validation + diagnostic to avoid panics in checked size/align intrinsic body generation.
tests/ui/invalid-intrinsic-marker/bad_signature.rs	Adds a reproducer that misapplies the internal marker to a wrong-signature function.
tests/ui/invalid-intrinsic-marker/expected	Asserts the expected diagnostic text for the new UI test.

---

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