Enable stubbing and function contracts for primitive types (#3496)

Previously, Kani was not able to resolve methods that belong to
primitive types, which would not allow users to specify primitive types
as stub target, neither for contracts.

Thus, extend the name resolution to be able to convert a type expression
into a `Ty` for primitive types, and add a new method to search for
function implementation for primitive types.

I also moved the type resolution logic to its own module to make it a
bit cleaner.

Resolves #2646 

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

kani-compiler/src/kani_middle/resolve/type_resolution.rs

@@ -0,0 +1,202 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains code used for resolve type / trait names
+
+use crate::kani_middle::resolve::{resolve_path, validate_kind, ResolveError};
+use quote::ToTokens;
+use rustc_hir::def::DefKind;
+use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use rustc_span::def_id::LocalDefId;
+use stable_mir::mir::Mutability;
+use stable_mir::ty::{FloatTy, IntTy, Region, RegionKind, RigidTy, Ty, UintTy};
+use std::str::FromStr;
+use strum_macros::{EnumString, IntoStaticStr};
+use syn::{Expr, ExprLit, Lit, Type, TypePath};
+use tracing::{debug, debug_span};
+
+/// Attempts to resolve a type from a type expression.
+pub fn resolve_ty<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ current_module: LocalDefId,
+ typ: &syn::Type,
+) -> Result<Ty, ResolveError<'tcx>> {
+ let _span = debug_span!("resolve_ty", ?typ).entered();
+ debug!(?typ, ?current_module, "resolve_ty");
+ let unsupported = |kind: &'static str| Err(ResolveError::UnsupportedPath { kind });
+ let invalid = |kind: &'static str| {
+ Err(ResolveError::InvalidPath {
+ msg: format!("Expected a type, but found {kind} `{}`", typ.to_token_stream()),
+ })
+ };
+ #[warn(non_exhaustive_omitted_patterns)]
+ match typ {
+ Type::Path(TypePath { qself, path }) => {
+ assert_eq!(*qself, None, "Unexpected qualified path");
+ if let Some(primitive) =
+ path.get_ident().and_then(|ident| PrimitiveIdent::from_str(&ident.to_string()).ok())
+ {
+ Ok(primitive.into())
+ } else {
+ let def_id = resolve_path(tcx, current_module, path)?;
+ validate_kind!(
+ tcx,
+ def_id,
+ "type",
+ DefKind::Struct | DefKind::Union | DefKind::Enum
+ )?;
+ Ok(rustc_internal::stable(tcx.type_of(def_id)).value)
+ }
+ }
+ Type::Array(array) => {
+ let elem_ty = resolve_ty(tcx, current_module, &array.elem)?;
+ let len = parse_len(&array.len).map_err(|msg| ResolveError::InvalidPath { msg })?;
+ Ty::try_new_array(elem_ty, len.try_into().unwrap()).map_err(|err| {
+ ResolveError::InvalidPath { msg: format!("Cannot instantiate array. {err}") }
+ })
+ }
+ Type::Paren(inner) => resolve_ty(tcx, current_module, &inner.elem),
+ Type::Ptr(ptr) => {
+ let elem_ty = resolve_ty(tcx, current_module, &ptr.elem)?;
+ let mutability =
+ if ptr.mutability.is_some() { Mutability::Mut } else { Mutability::Not };
+ Ok(Ty::new_ptr(elem_ty, mutability))
+ }
+ Type::Reference(reference) => {
+ let elem_ty = resolve_ty(tcx, current_module, &reference.elem)?;
+ let mutability =
+ if reference.mutability.is_some() { Mutability::Mut } else { Mutability::Not };
+ Ok(Ty::new_ref(Region { kind: RegionKind::ReErased }, elem_ty, mutability))
+ }
+ Type::Slice(slice) => {
+ let elem_ty = resolve_ty(tcx, current_module, &slice.elem)?;
+ Ok(Ty::from_rigid_kind(RigidTy::Slice(elem_ty)))
+ }
+ Type::Tuple(tuple) => {
+ let elems = tuple
+ .elems
+ .iter()
+ .map(|elem| resolve_ty(tcx, current_module, &elem))
+ .collect::<Result<Vec<_>, _>>()?;
+ Ok(Ty::new_tuple(&elems))
+ }
+ Type::Never(_) => Ok(Ty::from_rigid_kind(RigidTy::Never)),
+ Type::BareFn(_) => unsupported("bare function"),
+ Type::Macro(_) => invalid("macro"),
+ Type::Group(_) => invalid("group paths"),
+ Type::ImplTrait(_) => invalid("trait impl paths"),
+ Type::Infer(_) => invalid("inferred paths"),
+ Type::TraitObject(_) => invalid("trait object paths"),
+ Type::Verbatim(_) => unsupported("unknown paths"),
+ _ => {
+ unreachable!()
+ }
+ }
+}
+
+/// Enumeration of existing primitive types that are not parametric.
+#[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)]
+#[strum(serialize_all = "lowercase")]
+pub(super) enum PrimitiveIdent {
+ Bool,
+ Char,
+ F16,
+ F32,
+ F64,
+ F128,
+ I8,
+ I16,
+ I32,
+ I64,
+ I128,
+ Isize,
+ Str,
+ U8,
+ U16,
+ U32,
+ U64,
+ U128,
+ Usize,
+}
+
+/// Convert a primitive ident into a primitive `Ty`.
+impl From<PrimitiveIdent> for Ty {
+ fn from(value: PrimitiveIdent) -> Self {
+ match value {
+ PrimitiveIdent::Bool => Ty::bool_ty(),
+ PrimitiveIdent::Char => Ty::from_rigid_kind(RigidTy::Char),
+ PrimitiveIdent::F16 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F16)),
+ PrimitiveIdent::F32 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F32)),
+ PrimitiveIdent::F64 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F64)),
+ PrimitiveIdent::F128 => Ty::from_rigid_kind(RigidTy::Float(FloatTy::F128)),
+ PrimitiveIdent::I8 => Ty::signed_ty(IntTy::I8),
+ PrimitiveIdent::I16 => Ty::signed_ty(IntTy::I16),
+ PrimitiveIdent::I32 => Ty::signed_ty(IntTy::I32),
+ PrimitiveIdent::I64 => Ty::signed_ty(IntTy::I64),
+ PrimitiveIdent::I128 => Ty::signed_ty(IntTy::I128),
+ PrimitiveIdent::Isize => Ty::signed_ty(IntTy::Isize),
+ PrimitiveIdent::Str => Ty::from_rigid_kind(RigidTy::Str),
+ PrimitiveIdent::U8 => Ty::unsigned_ty(UintTy::U8),
+ PrimitiveIdent::U16 => Ty::unsigned_ty(UintTy::U16),
+ PrimitiveIdent::U32 => Ty::unsigned_ty(UintTy::U32),
+ PrimitiveIdent::U64 => Ty::unsigned_ty(UintTy::U64),
+ PrimitiveIdent::U128 => Ty::unsigned_ty(UintTy::U128),
+ PrimitiveIdent::Usize => Ty::unsigned_ty(UintTy::Usize),
+ }
+ }
+}
+
+/// Checks if a Path segment represents a primitive.
+///
+/// Note that this function will return false for expressions that cannot be parsed as a type.
+pub(super) fn is_primitive<T>(path: &T) -> bool
+where
+ T: ToTokens,
+{
+ let token = path.to_token_stream();
+ let Ok(typ) = syn::parse2(token) else { return false };
+ is_type_primitive(&typ)
+}
+
+/// Checks if a type is a primitive including composite ones.
+pub(super) fn is_type_primitive(typ: &syn::Type) -> bool {
+ #[warn(non_exhaustive_omitted_patterns)]
+ match typ {
+ Type::Array(_)
+ | Type::Ptr(_)
+ | Type::Reference(_)
+ | Type::Slice(_)
+ | Type::Never(_)
+ | Type::Tuple(_) => true,
+ Type::Path(TypePath { qself: Some(qself), path }) => {
+ path.segments.is_empty() && is_type_primitive(&qself.ty)
+ }
+ Type::Path(TypePath { qself: None, path }) => path
+ .get_ident()
+ .map_or(false, |ident| PrimitiveIdent::from_str(&ident.to_string()).is_ok()),
+ Type::BareFn(_)
+ | Type::Group(_)
+ | Type::ImplTrait(_)
+ | Type::Infer(_)
+ | Type::Macro(_)
+ | Type::Paren(_)
+ | Type::TraitObject(_)
+ | Type::Verbatim(_) => false,
+ _ => {
+ unreachable!()
+ }
+ }
+}
+
+/// Parse the length of the array.
+/// We currently only support a constant length.
+fn parse_len(len: &Expr) -> Result<usize, String> {
+ if let Expr::Lit(ExprLit { lit: Lit::Int(lit), .. }) = len {
+ if matches!(lit.suffix(), "" | "usize")
+ && let Ok(val) = usize::from_str(lit.base10_digits())
+ {
+ return Ok(val);
+ }
+ }
+ Err(format!("Expected a `usize` constant, but found `{}`", len.to_token_stream()))
+}

tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+
+//! Kani supports stubbing of most primitive methods, however, some methods, such as len, may be
+//! lowered to an Rvalue.
+
+/// Check that we can stub slices methods
+pub mod slices_check {
+ #[derive(kani::Arbitrary)]
+ pub struct MyStruct(u8, i32);
+
+ pub fn stub_len_is_10<T>(_: &[T]) -> usize {
+ 10
+ }
+
+ // This fails since `<[T]>::len` is lowered to `Rvalue::Len`.
+ #[kani::proof]
+ #[kani::stub(<[MyStruct]>::len, stub_len_is_10)]
+ pub fn check_stub_len_is_10() {
+ let input: [MyStruct; 5] = kani::any();
+ let slice = kani::slice::any_slice_of_array(&input);
+ assert_eq!(slice.len(), 10);
+ }
+}

tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! This tests that we can correctly stub bool functions.
+
+pub fn stub_then_some_is_none<T>(_: bool, _: T) -> Option<T> {
+ None
+}
+
+/// Check that we can stub `then_some`.
+#[kani::proof]
+#[kani::stub(bool::then_some, stub_then_some_is_none)]
+pub fn check_stub_then_some() {
+ let input: bool = kani::any();
+ assert_eq!(input.then_some("h"), None);
+}
+
+pub fn stub_then_panic<T, F>(_: bool, _: F) -> Option<T>
+where
+ F: FnOnce() -> T,
+{
+ panic!()
+}
+
+/// Check that we can stub `then`.
+#[kani::proof]
+#[kani::should_panic]
+#[kani::stub(bool::then, stub_then_panic)]
+pub fn check_stub_then() {
+ let input: bool = kani::any();
+ let output: char = kani::any();
+ assert_eq!(input.then(|| output).unwrap_or(output), output);
+}

tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! This tests that we can correctly stub char functions.
+/// Check that we can stub is_ascii from `char`.
+pub fn stub_is_ascii_true(_: &char) -> bool {
+ true
+}
+
+/// Check stubbing by directly calling `str::is_ascii`
+#[kani::proof]
+#[kani::stub(char::is_ascii, stub_is_ascii_true)]
+pub fn check_stub_is_ascii() {
+ let input: char = kani::any();
+ assert!(input.is_ascii());
+}

tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! This tests that we can correctly stub float functions.
+#![feature(f128)]
+#![feature(f16)]
+
+/// Generate stub and harness for floor method on floats.
+macro_rules! stub_floor {
+ ($ty:ty, $harness:ident, $stub:ident) => {
+ // Stub that always returns 0.
+ pub fn $stub(_: $ty) -> $ty {
+ 0.0
+ }
+
+ // Harness
+ #[kani::proof]
+ #[kani::stub($ty::floor, $stub)]
+ pub fn $harness() {
+ let input = kani::any();
+ let floor = <$ty>::floor(input);
+ assert_eq!(floor, 0.0);
+ }
+ };
+}
+
+stub_floor!(f16, f16_floor, stub_f16_floor);
+stub_floor!(f32, f32_floor, stub_f32_floor);
+stub_floor!(f64, f64_floor, stub_f64_floor);
+stub_floor!(f128, f128_floor, stub_f128_floor);

tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! This tests that we can correctly stub integer types functions.
+
+/// Generate stub and harness for count_ones method on integers.
+macro_rules! stub_count_ones {
+ ($ty:ty, $harness:ident, $stub:ident) => {
+ // Stub that always returns 0.
+ pub fn $stub(_: $ty) -> u32 {
+ 0
+ }
+
+ // Harness
+ #[kani::proof]
+ #[kani::stub($ty::count_ones, $stub)]
+ pub fn $harness() {
+ let input = kani::any();
+ let ones = <$ty>::count_ones(input);
+ assert_eq!(ones, 0);
+ }
+ };
+}
+
+stub_count_ones!(u8, u8_count_ones, stub_u8_count_ones);
+stub_count_ones!(u16, u16_count_ones, stub_u16_count_ones);
+stub_count_ones!(u32, u32_count_ones, stub_u32_count_ones);
+stub_count_ones!(u64, u64_count_ones, stub_u64_count_ones);
+stub_count_ones!(u128, u128_count_ones, stub_u128_count_ones);
+stub_count_ones!(usize, usize_count_ones, stub_usize_count_ones);
+
+stub_count_ones!(i8, i8_count_ones, stub_i8_count_ones);
+stub_count_ones!(i16, i16_count_ones, stub_i16_count_ones);
+stub_count_ones!(i32, i32_count_ones, stub_i32_count_ones);
+stub_count_ones!(i64, i64_count_ones, stub_i64_count_ones);
+stub_count_ones!(i128, i128_count_ones, stub_i128_count_ones);
+stub_count_ones!(isize, isize_count_ones, stub_isize_count_ones);

tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs

@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! This tests that we can correctly stub methods from raw pointer types.
+
+pub fn stub_len_is_10<T>(_: *const [T]) -> usize {
+ 10
+}
+
+pub fn stub_mut_len_is_0<T>(_: *mut [T]) -> usize {
+ 0
+}
+
+#[kani::proof]
+#[kani::stub(<*const [u8]>::len, stub_len_is_10)]
+#[kani::stub(<*mut [u8]>::len, stub_mut_len_is_0)]
+pub fn check_stub_len_raw_ptr() {
+ let mut input: [u8; 5] = kani::any();
+ let mut_ptr = &mut input as *mut [u8];
+ let ptr = &input as *const [u8];
+ assert_eq!(mut_ptr.len(), 0);
+ assert_eq!(ptr.len(), 10);
+}
+
+pub fn stub_is_always_null<T>(_: *const T) -> bool {
+ true
+}
+
+// Fix-me: Option doesn't seem to work without the fully qualified path.
+#[kani::proof]
+#[kani::stub(<*const std::option::Option>::is_null, stub_is_always_null)]
+pub fn check_stub_is_null() {
+ let input: Option<char> = kani::any();
+ let ptr = &input as *const Option<char>;
+ assert!(unsafe { ptr.is_null() });
+}