Enable stubbing and function contracts for primitive types

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() });
+}