diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 29c12f6cf96c..3998d40eb702 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -27,6 +27,7 @@ use rustc_public::mir::{ AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place, RETURN_LOCAL, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnOp, UnwindAction, }; +use rustc_public::rustc_internal; use rustc_public::target::MachineInfo; use rustc_public::ty::{ AdtDef, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, @@ -70,6 +71,24 @@ impl TransformPass for IntrinsicGeneratorPass { attributes.fn_marker().and_then(|name| KaniIntrinsic::from_str(name.as_str()).ok()) { match kani_intrinsic { + // `fn_marker` is an internal attribute, but nothing prevents user code from + // attaching it to a function with an incompatible signature. The size/align + // generators below assume a raw pointer argument and an `Option` return; + // reject anything else with a diagnostic rather than panicking while building the + // `Some`/`None` return value (see issue #4589). + KaniIntrinsic::CheckedAlignOf | KaniIntrinsic::CheckedSizeOf + if !has_checked_intrinsic_sig(&body) => + { + let name: &str = kani_intrinsic.into(); + 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`" + ), + ); + (false, body) + } KaniIntrinsic::CheckedAlignOf => (true, self.checked_align_of(body, instance)), KaniIntrinsic::CheckedSizeOf => (true, self.checked_size_of(body, instance)), KaniIntrinsic::IsInitialized => (true, self.is_initialized_body(body)), @@ -582,6 +601,25 @@ impl IntrinsicGeneratorPass { } } +/// Whether `body` has the signature that the `checked_size_of` and `checked_align_of` +/// generators require: a raw pointer argument and an `Option`-shaped return type (a variant +/// with a field for `Some`, and one without for `None`). The internal `fn_marker` attribute can +/// be attached to an arbitrary function, so this guards `build_some`/`build_none` against a +/// mismatched return type instead of unwrapping a missing variant. +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 +} + /// Build an Rvalue `Some(val)`. /// Since the variants of `Option` are `Some(val)` and `None`, we know we've found the `Some` variant when we find the first variant with a field. fn build_some(option: AdtDef, args: GenericArgs, val_op: Operand) -> Rvalue { diff --git a/tests/ui/invalid-intrinsic-marker/bad_signature.rs b/tests/ui/invalid-intrinsic-marker/bad_signature.rs new file mode 100644 index 000000000000..06e1ac86d0d5 --- /dev/null +++ b/tests/ui/invalid-intrinsic-marker/bad_signature.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Attaching the internal `CheckedSizeOfIntrinsic` marker to a function with an +//! incompatible signature should produce a diagnostic instead of an internal +//! compiler error. See https://github.com/model-checking/kani/issues/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); +} diff --git a/tests/ui/invalid-intrinsic-marker/expected b/tests/ui/invalid-intrinsic-marker/expected new file mode 100644 index 000000000000..1c4edd677d5a --- /dev/null +++ b/tests/ui/invalid-intrinsic-marker/expected @@ -0,0 +1 @@ +error: the `CheckedSizeOfIntrinsic` intrinsic marker can only be applied to a function with a raw pointer argument that returns `Option`