Emit a diagnostic for a misapplied checked size/align intrinsic marker by MavenRain · Pull Request #4648 · model-checking/kani

MavenRain · 2026-07-16T06:23:05Z

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.

feliperodri · 2026-08-01T21:25:15Z

+fn has_checked_intrinsic_sig(body: &Body) -> bool {
+    let arg_is_ptr = matches!(
+        body.arg_locals().first().map(|arg| arg.ty.kind()),
+        Some(TyKind::RigidTy(RigidTy::RawPtr(..)))
+    );
+    let ret_is_option = matches!(
+        body.ret_local().ty.kind(),
+        TyKind::RigidTy(RigidTy::Adt(def, _))
+            if def.variants_iter().any(|var| !var.fields().is_empty())
+                && def.variants_iter().any(|var| var.fields().is_empty())
+    );
+    arg_is_ptr && ret_is_option
+}


@MavenRain could you address this issue?

Guard seems too permissive. has_checked_intrinsic_sig currently only checks:

first argument is a raw pointer

return type is some enum with one empty and one non-empty variant

That still allows cases like:

extra parameters

Option<u8>-style returns

other enum shapes that just happen to look Option-like

The risk is the validation passes, but later code still assumes the exact intrinsic shape and could fail or misbehave.

The `CheckedSizeOf` and `CheckedAlignOf` intrinsic generators assume the marked function has the signature of the corresponding Kani intrinsic: a raw pointer argument and an `Option<usize>` return. The `fn_marker` attribute is internal, but nothing stops user code from attaching it to a function with a different signature. When that happened, `build_some` unwrapped a missing `Some` variant and the compiler panicked: thread 'rustc' panicked at kani_intrinsics.rs: called `Option::unwrap()` on a `None` value Validate the signature before generating the body and emit a normal compiler error when it does not match, following how other misapplied kani-internal attributes are already reported. Resolves model-checking#4589 Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>

feliperodri

There is a potential future maintenance hazard: the helper duplicates the intrinsic generator’s assumptions, so if the generator changes later the validation could drift unless it is kept in sync; a tighter type-shape check would reduce that risk. Also, while the change applies to both CheckedSizeOf and CheckedAlignOf, the test only covers CheckedSizeOfIntrinsic, so there is still no explicit proof that the sibling CheckedAlignOf path is equally safe, and a subtle edge case could remain if its body generation differs.

feliperodri · 2026-08-01T21:25:15Z

+fn has_checked_intrinsic_sig(body: &Body) -> bool {
+    let arg_is_ptr = matches!(
+        body.arg_locals().first().map(|arg| arg.ty.kind()),
+        Some(TyKind::RigidTy(RigidTy::RawPtr(..)))
+    );
+    let ret_is_option = matches!(
+        body.ret_local().ty.kind(),
+        TyKind::RigidTy(RigidTy::Adt(def, _))
+            if def.variants_iter().any(|var| !var.fields().is_empty())
+                && def.variants_iter().any(|var| var.fields().is_empty())
+    );
+    arg_is_ptr && ret_is_option
+}


@MavenRain could you address this issue?

feliperodri · 2026-08-01T21:27:50Z

+fn has_checked_intrinsic_sig(body: &Body) -> bool {
+    let arg_is_ptr = matches!(
+        body.arg_locals().first().map(|arg| arg.ty.kind()),
+        Some(TyKind::RigidTy(RigidTy::RawPtr(..)))
+    );
+    let ret_is_option = matches!(
+        body.ret_local().ty.kind(),
+        TyKind::RigidTy(RigidTy::Adt(def, _))
+            if def.variants_iter().any(|var| !var.fields().is_empty())
+                && def.variants_iter().any(|var| var.fields().is_empty())
+    );
+    arg_is_ptr && ret_is_option
+}


Guard seems too permissive. has_checked_intrinsic_sig currently only checks:

first argument is a raw pointer

return type is some enum with one empty and one non-empty variant

That still allows cases like:

extra parameters

Option<u8>-style returns

other enum shapes that just happen to look Option-like

The risk is the validation passes, but later code still assumes the exact intrinsic shape and could fail or misbehave.

feliperodri · 2026-08-01T21:33:01Z

+                    tcx.dcx().span_err(
+                        rustc_internal::internal(tcx, body.span),
+                        format!(
+                            "the `{name}` intrinsic marker can only be applied to a function \
+                             with a raw pointer argument that returns `Option<usize>`"
+                        ),
+                    );


The error says the marker can only be applied to a function returning Option<usize>, but the helper does not verify usize specifically. It looks like the users will get a precise error message, but the checker enforces a looser condition.

feliperodri · 2026-08-01T21:33:55Z

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


The new UI test covers one bad return type, but it does not cover:

extra arguments

wrong Option inner type

the matching valid intrinsic signature

Replace the boolean signature guard with a checked_intrinsic_sig extractor requiring exactly one raw-pointer argument and a return type shaped exactly like Option<usize>. transform extracts once and passes the validated pieces into the generators and build_some/build_none, so validation cannot drift from what the generators assume. Add ui tests for extra arguments, a wrong Option<T> inner type, the CheckedAlignOf sibling path, and a positive control with the exact intrinsic signature. Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>

…-bad-sig

MavenRain · 2026-08-02T14:10:55Z

@feliperodri , thanks for the review! All points addressed:

Guard too permissive / usize not verified: the boolean guard is now a checked_intrinsic_sig extractor that requires exactly one argument (a raw pointer) and a return type shaped exactly like Option<usize>: exactly two variants, one field-less and one whose single field substitutes to usize. Extra parameters, Option<u8>-style returns, and other enum shapes are all rejected, so the checker now enforces exactly what the error message says.
Maintenance hazard / drift: transform extracts the signature pieces once and passes them into checked_size_of / checked_align_of, and build_some / build_none now take the validated variant indices, so the generators consume exactly what validation produced and the two cannot drift. The previous variant-lookup unwraps are gone as a side effect. Any type that passes the structural check is one the generators handle by construction (they only build the two validated variants), which is why I stopped short of requiring literally core::option::Option -- happy to add that check too if you'd prefer.
Test coverage: added ui tests for extra arguments (extra_args.rs), a wrong Option<T> inner type (wrong_option_inner.rs), the CheckedAlignOf sibling path (bad_signature_align.rs), and a positive control applying both markers to functions with the exact intrinsic signature, which must still generate the intrinsic bodies and verify successfully (valid_signature.rs).

Copilot

Pull request overview

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

Suppressed comments (1)

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs:634

The new signature guard rejects non-raw-pointer arguments, but the added UI coverage only exercises wrong return type and wrong arity. Consider adding a UI test where the marker is attached to a function with exactly one argument of a non-pointer type (e.g., usize) to ensure this diagnostic path stays covered.

fn checked_intrinsic_sig(body: &Body) -> Option<CheckedIntrinsicSig> {
    let ptr_arg = single(body.arg_locals())?;
    let pointee_ty = if let TyKind::RigidTy(RigidTy::RawPtr(pointee, _)) = ptr_arg.ty.kind() {
        Some(pointee)
    } else {
        None
    }?;

feliperodri · 2026-08-02T16:07:10Z

@MavenRain could you add the extra UI test pointed out by Copilot? Can we resolve all the comments you have addressed? Almost ready to merge...

MavenRain requested a review from a team as a code owner July 16, 2026 06:23

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

feliperodri requested a review from Copilot July 29, 2026 11:05

feliperodri added this to the Maintenance milestone Jul 29, 2026

Copilot started reviewing on behalf of feliperodri July 29, 2026 11:05 View session

Copilot AI reviewed Jul 29, 2026

View reviewed changes

feliperodri assigned MavenRain Jul 29, 2026

MavenRain force-pushed the 4589-intrinsic-marker-bad-sig branch from afc0a1e to 60ef55f Compare July 31, 2026 03:58

feliperodri requested changes Aug 1, 2026

View reviewed changes

MavenRain added 2 commits August 2, 2026 07:09

Merge remote-tracking branch 'origin/main' into 4589-intrinsic-marker…

f10ad2e

…-bad-sig

MavenRain requested a review from feliperodri August 2, 2026 14:11

feliperodri requested a review from Copilot August 2, 2026 15:51

Copilot started reviewing on behalf of feliperodri August 2, 2026 15:51 View session

Copilot AI reviewed Aug 2, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Emit a diagnostic for a misapplied checked size/align intrinsic marker - #4648

Emit a diagnostic for a misapplied checked size/align intrinsic marker#4648
MavenRain wants to merge 3 commits into
model-checking:mainfrom
MavenRain:4589-intrinsic-marker-bad-sig

MavenRain commented Jul 16, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

feliperodri Aug 1, 2026

Uh oh!

feliperodri Aug 1, 2026

Uh oh!

feliperodri left a comment

Uh oh!

feliperodri Aug 1, 2026

Uh oh!

feliperodri Aug 1, 2026

Uh oh!

feliperodri Aug 1, 2026

Uh oh!

feliperodri Aug 1, 2026

Uh oh!

MavenRain commented Aug 2, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

feliperodri commented Aug 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

MavenRain commented Jul 16, 2026

Description

Context

Change

Testing

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

feliperodri Aug 1, 2026

Choose a reason for hiding this comment

Uh oh!

feliperodri Aug 1, 2026

Choose a reason for hiding this comment

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

feliperodri Aug 1, 2026

Choose a reason for hiding this comment

Uh oh!

feliperodri Aug 1, 2026

Choose a reason for hiding this comment

Uh oh!

feliperodri Aug 1, 2026

Choose a reason for hiding this comment

Uh oh!

feliperodri Aug 1, 2026

Choose a reason for hiding this comment

Uh oh!

MavenRain commented Aug 2, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

feliperodri commented Aug 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants