From 6f8ca94edf70eb1fd95716dbedef1e40e9bef701 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Sep 2024 12:16:19 -0700 Subject: [PATCH] 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.rs | 267 +++++++++--------- .../kani_middle/resolve/type_resolution.rs | 202 +++++++++++++ .../fixme_stub_lowered_methods.rs | 26 ++ .../StubPrimitives/stub_bool_methods.rs | 35 +++ .../StubPrimitives/stub_char_methods.rs | 18 ++ .../StubPrimitives/stub_float_methods.rs | 32 +++ .../StubPrimitives/stub_int_methods.rs | 39 +++ .../StubPrimitives/stub_ptr_methods.rs | 38 +++ .../StubPrimitives/stub_slice_methods.rs | 37 +++ .../resolution_errors.expected | 36 +++ .../resolution_errors.rs | 23 ++ .../unsupported_resolutions.expected | 10 +- .../unsupported_resolutions.rs | 10 +- 13 files changed, 630 insertions(+), 143 deletions(-) create mode 100644 kani-compiler/src/kani_middle/resolve/type_resolution.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs create mode 100644 tests/ui/function-stubbing-error/resolution_errors.expected create mode 100644 tests/ui/function-stubbing-error/resolution_errors.rs diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 88b1af86efe9..b2b00c1e4a40 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -1,10 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains code for resolving strings representing simple paths to -//! `DefId`s for functions and methods. For the definition of a simple path, see -//! . +// +//! This module contains code for resolving strings representing paths (simple and qualified) to +//! `DefId`s for functions and methods. For the definition of a path, see +//! . //! -//! TODO: Extend this logic to support resolving qualified paths. +//! TODO: Change `resolve_fn` in order to return information about trait implementations. //! //! //! Note that glob use statements can form loops. The paths can also walk through the loop. @@ -15,6 +16,7 @@ use rustc_errors::ErrorGuaranteed; use rustc_hir::def::{DefKind, Res}; use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE}; use rustc_hir::{ItemKind, UseKind}; +use rustc_middle::ty::fast_reject::{self, TreatParams}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind}; @@ -22,34 +24,10 @@ use stable_mir::CrateDef; use std::collections::HashSet; use std::fmt; use std::iter::Peekable; -use std::str::FromStr; -use strum_macros::{EnumString, IntoStaticStr}; -use syn::{Ident, PathSegment, Type, TypePath}; -use tracing::debug; - -#[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)] -#[strum(serialize_all = "lowercase")] -enum PrimitiveIdent { - Bool, - Char, - F16, - F32, - F64, - F128, - I8, - I16, - I32, - I64, - I128, - Isize, - Str, - U8, - U16, - U32, - U64, - U128, - Usize, -} +use syn::{PathSegment, QSelf, TypePath}; +use tracing::{debug, debug_span}; + +mod type_resolution; macro_rules! validate_kind { ($tcx:ident, $id:ident, $expected:literal, $kind:pat) => {{ @@ -61,6 +39,7 @@ macro_rules! validate_kind { } }}; } +pub(crate) use validate_kind; #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum FnResolution { @@ -76,20 +55,34 @@ pub fn resolve_fn_path<'tcx>( current_module: LocalDefId, path: &TypePath, ) -> Result> { - match (&path.qself, &path.path.leading_colon) { - (Some(qself), Some(_)) => { - // Qualified path that does not define a trait. - resolve_ty(tcx, current_module, &qself.ty)?; - Err(ResolveError::UnsupportedPath { kind: "qualified bare function paths" }) - } - (Some(qself), None) => { - let ty = resolve_ty(tcx, current_module, &qself.ty)?; + let _span = debug_span!("resolve_fn_path", ?path).entered(); + match &path.qself { + // Qualified path for a trait method implementation, like `::bar`. + Some(QSelf { ty: syn_ty, position, .. }) if *position > 0 => { + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; let def_id = resolve_path(tcx, current_module, &path.path)?; validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?; Ok(FnResolution::FnImpl { def: stable_fn_def(tcx, def_id).unwrap(), ty }) } - (None, _) => { - // Simple path + // Qualified path for a primitive type, such as `<[u8]::sort>`. + Some(QSelf { ty: syn_ty, .. }) if type_resolution::is_type_primitive(syn_ty) => { + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; + let resolved = resolve_in_primitive(tcx, ty, path.path.segments.iter())?; + if resolved.segments.is_empty() { + Ok(FnResolution::Fn(stable_fn_def(tcx, resolved.base).unwrap())) + } else { + Err(ResolveError::UnexpectedType { tcx, item: resolved.base, expected: "module" }) + } + } + // Qualified path for a non-primitive type, such as `::foo>`. + Some(QSelf { ty: syn_ty, .. }) => { + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; + let def_id = resolve_in_user_type(tcx, ty, path.path.segments.iter())?; + validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?; + Ok(FnResolution::Fn(stable_fn_def(tcx, def_id).unwrap())) + } + // Simple path + None => { let def_id = resolve_path(tcx, current_module, &path.path)?; validate_kind!(tcx, def_id, "function / method", DefKind::Fn | DefKind::AssocFn)?; Ok(FnResolution::Fn(stable_fn_def(tcx, def_id).unwrap())) @@ -97,14 +90,15 @@ pub fn resolve_fn_path<'tcx>( } } -/// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`. +/// Attempts to resolve a *simple path* (in the form of a string) to a function / method `DefId`. /// -/// Use `[resolve_fn_path]` if you want to handle qualified paths and simple paths +/// Use `[resolve_fn_path]` if you want to handle qualified paths and simple paths. pub fn resolve_fn<'tcx>( tcx: TyCtxt<'tcx>, current_module: LocalDefId, path_str: &str, ) -> Result> { + let _span = debug_span!("resolve_fn", ?path_str, ?current_module).entered(); let path = syn::parse_str(path_str).map_err(|err| ResolveError::InvalidPath { msg: format!("Expected a path, but found `{path_str}`. {err}"), })?; @@ -143,74 +137,6 @@ pub fn expect_resolve_fn( } } -/// Attempts to resolve a type. -pub fn resolve_ty<'tcx>( - tcx: TyCtxt<'tcx>, - current_module: LocalDefId, - typ: &syn::Type, -) -> Result> { - 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(path) if path.qself.is_none() => { - let def_id = resolve_path(tcx, current_module, &path.path)?; - validate_kind!(tcx, def_id, "type", DefKind::Struct | DefKind::Union | DefKind::Enum)?; - Ok(rustc_internal::stable(tcx.type_of(def_id)).value) - } - Type::Path(_) => unsupported("qualified paths"), - Type::Array(_) - | Type::BareFn(_) - | Type::Macro(_) - | Type::Never(_) - | Type::Paren(_) - | Type::Ptr(_) - | Type::Reference(_) - | Type::Slice(_) - | Type::Tuple(_) => unsupported("path including primitive types"), - Type::Verbatim(_) => unsupported("unknown paths"), - Type::Group(_) => invalid("group paths"), - Type::ImplTrait(_) => invalid("trait impl paths"), - Type::Infer(_) => invalid("inferred paths"), - Type::TraitObject(_) => invalid("trait object paths"), - _ => { - unreachable!() - } - } -} - -/// Checks if a Path segment represents a primitive -fn is_primitive(ident: &Ident) -> bool { - let token = ident.to_string(); - let Ok(typ) = syn::parse_str(&token) else { return false }; - #[warn(non_exhaustive_omitted_patterns)] - match typ { - Type::Array(_) - | Type::Ptr(_) - | Type::Reference(_) - | Type::Slice(_) - | Type::Never(_) - | Type::Tuple(_) => true, - Type::Path(_) => PrimitiveIdent::from_str(&token).is_ok(), - Type::BareFn(_) - | Type::Group(_) - | Type::ImplTrait(_) - | Type::Infer(_) - | Type::Macro(_) - | Type::Paren(_) - | Type::TraitObject(_) - | Type::Verbatim(_) => false, - _ => { - unreachable!() - } - } -} - /// Attempts to resolve a simple path (in the form of a string) to a `DefId`. /// The current module is provided as an argument in order to resolve relative /// paths. @@ -220,15 +146,15 @@ fn resolve_path<'tcx>( path: &syn::Path, ) -> Result> { debug!(?path, "resolve_path"); - let _span = tracing::span!(tracing::Level::DEBUG, "path_resolution").entered(); - let path = resolve_prefix(tcx, current_module, path)?; path.segments.into_iter().try_fold(path.base, |base, segment| { let name = segment.ident.to_string(); let def_kind = tcx.def_kind(base); let next_item = match def_kind { DefKind::ForeignMod | DefKind::Mod => resolve_in_module(tcx, base, &name), - DefKind::Struct | DefKind::Enum | DefKind::Union => resolve_in_type(tcx, base, &name), + DefKind::Struct | DefKind::Enum | DefKind::Union => { + resolve_in_type_def(tcx, base, &name) + } DefKind::Trait => resolve_in_trait(tcx, base, &name), kind => { debug!(?base, ?kind, "resolve_path: unexpected item"); @@ -250,6 +176,8 @@ pub enum ResolveError<'tcx> { InvalidPath { msg: String }, /// Unable to find an item. MissingItem { tcx: TyCtxt<'tcx>, base: DefId, unresolved: String }, + /// Unable to find an item in a primitive type. + MissingPrimitiveItem { base: Ty, unresolved: String }, /// Error triggered when the identifier points to an item with unexpected type. UnexpectedType { tcx: TyCtxt<'tcx>, item: DefId, expected: &'static str }, /// Error triggered when the identifier is not currently supported. @@ -291,6 +219,9 @@ impl<'tcx> fmt::Display for ResolveError<'tcx> { let def_desc = description(*tcx, *base); write!(f, "unable to find `{unresolved}` inside {def_desc}") } + ResolveError::MissingPrimitiveItem { base, unresolved } => { + write!(f, "unable to find `{unresolved}` inside `{base}`") + } ResolveError::UnsupportedPath { kind } => { write!(f, "Kani currently cannot resolve {kind}") } @@ -334,6 +265,7 @@ fn resolve_prefix<'tcx>( // Resolve qualifiers `crate`, initial `::`, and `self`. The qualifier // `self` may be followed be `super` (handled below). match (path.leading_colon, segments.next()) { + // Leading `::` indicates that the path points to an item inside an external crate. (Some(_), Some(segment)) => { // Skip root and get the external crate from the name that follows `::`. let next_name = segment.ident.to_string(); @@ -348,9 +280,11 @@ fn resolve_prefix<'tcx>( }) } } + // Path with `::` alone is invalid. (Some(_), None) => { Err(ResolveError::InvalidPath { msg: "expected identifier after `::`".to_string() }) } + // Path starting with `crate::`. (None, Some(segment)) if segment.ident == CRATE => { // Find the module at the root of the crate. let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); @@ -360,14 +294,19 @@ fn resolve_prefix<'tcx>( }; Ok(Path { base: crate_root.to_def_id(), segments: segments.cloned().collect() }) } + // Path starting with "self::" (None, Some(segment)) if segment.ident == SELF => { resolve_super(tcx, current_module, segments.peekable()) } + // Path starting with "super::" (None, Some(segment)) if segment.ident == SUPER => { resolve_super(tcx, current_module, path.segments.iter().peekable()) } - (None, Some(segment)) if is_primitive(&segment.ident) => { - Err(ResolveError::UnsupportedPath { kind: "path including primitive types" }) + // Path starting with a primitive, such as "u8::" + (None, Some(segment)) if type_resolution::is_primitive(&segment) => { + let syn_ty = syn::parse2(segment.to_token_stream()).unwrap(); + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; + resolve_in_primitive(tcx, ty, segments) } (None, Some(segment)) => { // No special key word was used. Try local first otherwise try external name. @@ -561,8 +500,41 @@ fn resolve_in_glob_use(tcx: TyCtxt, res: &Res, name: &str) -> RelativeResolution } } -/// Resolves a function in a type. -fn resolve_in_type<'tcx>( +/// Resolves a function in a user type (non-primitive). +fn resolve_in_user_type<'tcx, 'a, I>( + tcx: TyCtxt<'tcx>, + ty: Ty, + mut segments: I, +) -> Result> +where + I: Iterator, +{ + let def_id = match ty.kind() { + TyKind::RigidTy(rigid_ty) => match rigid_ty { + RigidTy::Adt(def, _) => rustc_internal::internal(tcx, def.def_id()), + RigidTy::Foreign(_) => { + return Err(ResolveError::UnsupportedPath { kind: "foreign type" }); + } + _ => { + unreachable!("Unexpected type {ty}") + } + }, + TyKind::Alias(_, _) => return Err(ResolveError::UnsupportedPath { kind: "alias" }), + TyKind::Param(_) | TyKind::Bound(_, _) => { + // Name resolution can not resolve in a parameter or bound. + unreachable!() + } + }; + let Some(name) = segments.next() else { unreachable!() }; + if segments.next().is_some() { + Err(ResolveError::UnexpectedType { tcx, item: def_id, expected: "module" }) + } else { + resolve_in_type_def(tcx, def_id, &name.ident.to_string()) + } +} + +/// Resolves a function in a type given its `def_id`. +fn resolve_in_type_def<'tcx>( tcx: TyCtxt<'tcx>, type_id: DefId, name: &str, @@ -576,11 +548,7 @@ fn resolve_in_type<'tcx>( .iter() .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id)) .cloned() - .find(|item| { - let item_path = tcx.def_path_str(*item); - let last = item_path.split("::").last().unwrap(); - last == name - }) + .find(|item| is_item_name(tcx, *item, name)) .ok_or_else(missing_item_err) } @@ -594,14 +562,53 @@ fn resolve_in_trait<'tcx>( let missing_item_err = || ResolveError::MissingItem { tcx, base: trait_id, unresolved: name.to_string() }; let trait_def = tcx.trait_def(trait_id); - // Try the inherent `impl` blocks (i.e., non-trait `impl`s). + // Look for the given name in the list of associated items for the trait definition. tcx.associated_item_def_ids(trait_def.def_id) .iter() .copied() - .find(|item| { - let item_path = tcx.def_path_str(*item); - let last = item_path.split("::").last().unwrap(); - last == name - }) + .find(|item| is_item_name(tcx, *item, name)) .ok_or_else(missing_item_err) } + +/// Resolves a primitive type function. +/// +/// This function assumes that `ty` is a primitive. +fn resolve_in_primitive<'tcx, 'a, I>( + tcx: TyCtxt<'tcx>, + ty: Ty, + mut segments: I, +) -> Result> +where + I: Iterator, +{ + if let Some(next) = segments.next() { + let name = next.ident.to_string(); + debug!(?name, ?ty, "resolve_in_primitive"); + let internal_ty = rustc_internal::internal(tcx, ty); + let simple_ty = + fast_reject::simplify_type(tcx, internal_ty, TreatParams::AsCandidateKey).unwrap(); + let impls = tcx.incoherent_impls(simple_ty).unwrap(); + // Find the primitive impl. + let item = impls + .iter() + .find_map(|item_impl| { + tcx.associated_item_def_ids(item_impl) + .iter() + .copied() + .find(|item| is_item_name(tcx, *item, &name)) + }) + .ok_or_else(|| ResolveError::MissingPrimitiveItem { + base: ty, + unresolved: name.to_string(), + })?; + Ok(Path { base: item, segments: segments.cloned().collect() }) + } else { + Err(ResolveError::InvalidPath { msg: format!("Unexpected primitive type `{ty}`") }) + } +} + +fn is_item_name(tcx: TyCtxt, item: DefId, name: &str) -> bool { + let item_path = tcx.def_path_str(item); + let last = item_path.split("::").last().unwrap(); + last == name +} diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs new file mode 100644 index 000000000000..790019ab2998 --- /dev/null +++ b/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> { + 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::, _>>()?; + 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 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(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 { + 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())) +} diff --git a/tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs b/tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs new file mode 100644 index 000000000000..130a062071ba --- /dev/null +++ b/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]) -> 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); + } +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs new file mode 100644 index 000000000000..44f926552c74 --- /dev/null +++ b/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(_: bool, _: T) -> Option { + 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(_: bool, _: F) -> Option +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); +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_char_methods.rs new file mode 100644 index 000000000000..a012208c7761 --- /dev/null +++ b/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()); +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs new file mode 100644 index 000000000000..196c1be3053e --- /dev/null +++ b/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); diff --git a/tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_int_methods.rs new file mode 100644 index 000000000000..bebbc47df245 --- /dev/null +++ b/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); diff --git a/tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_ptr_methods.rs new file mode 100644 index 000000000000..1bce08059d4d --- /dev/null +++ b/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(_: *const [T]) -> usize { + 10 +} + +pub fn stub_mut_len_is_0(_: *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(_: *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 = kani::any(); + let ptr = &input as *const Option; + assert!(unsafe { ptr.is_null() }); +} diff --git a/tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs b/tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs new file mode 100644 index 000000000000..b7e4fafaa638 --- /dev/null +++ b/tests/kani/Stubbing/StubPrimitives/stub_slice_methods.rs @@ -0,0 +1,37 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub slices and string slices functions. + +/// Check that we can stub str::is_ascii +pub mod str_check { + pub fn stub_is_ascii_false(_: &str) -> bool { + false + } + + #[kani::proof] + #[kani::stub(str::is_ascii, stub_is_ascii_false)] + pub fn check_stub_is_ascii() { + let input = "is_ascii"; + assert!(!input.is_ascii()); + } +} + +/// Check that we can stub slices +pub mod slices_check { + #[derive(kani::Arbitrary, Ord, PartialOrd, Copy, Clone, PartialEq, Eq)] + pub struct MyStruct(u8, i32); + + pub fn stub_sort_noop(_: &mut [T]) {} + + #[kani::proof] + #[kani::stub(<[MyStruct]>::sort, stub_sort_noop)] + pub fn check_stub_sort_noop() { + let mut input: [MyStruct; 5] = kani::any(); + let copy = input.clone(); + input.sort(); + assert_eq!(input, copy); + } +} diff --git a/tests/ui/function-stubbing-error/resolution_errors.expected b/tests/ui/function-stubbing-error/resolution_errors.expected new file mode 100644 index 000000000000..d722f13bd691 --- /dev/null +++ b/tests/ui/function-stubbing-error/resolution_errors.expected @@ -0,0 +1,36 @@ +error: failed to resolve `<[char ; 10]>::foo`: unable to find `foo` inside `[char; 10]` +resolution_errors.rs +| +| #[kani::stub(<[char; 10]>::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `str::foo`: unable to find `foo` inside `str` +resolution_errors.rs +| +| #[kani::stub(str::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `<[u32]>::foo`: unable to find `foo` inside `[u32]` +resolution_errors.rs +| +| #[kani::stub(<[u32]>::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `<(i32 , i32)>::foo`: unable to find `foo` inside `(i32, i32)` +resolution_errors.rs +| +| #[kani::stub(<(i32, i32)>::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `u8::foo`: unable to find `foo` inside `u8` +resolution_errors.rs +| +| #[kani::stub(u8::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error: failed to resolve `::foo`: unable to find `foo` inside struct `Bar` +resolution_errors.rs +| +| #[kani::stub(::foo, stub_foo)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/ui/function-stubbing-error/resolution_errors.rs b/tests/ui/function-stubbing-error/resolution_errors.rs new file mode 100644 index 000000000000..efb87efad08e --- /dev/null +++ b/tests/ui/function-stubbing-error/resolution_errors.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we emit a nice error message for resolution failures. + +/// Dummy structure +pub struct Bar; + +/// Dummy stub +pub fn stub_foo() -> bool { + true +} + +#[kani::proof] +#[kani::stub(::foo, stub_foo)] +#[kani::stub(u8::foo, stub_foo)] +#[kani::stub(<(i32, i32)>::foo, stub_foo)] +#[kani::stub(<[u32]>::foo, stub_foo)] +#[kani::stub(str::foo, stub_foo)] +#[kani::stub(<[char; 10]>::foo, stub_foo)] +fn invalid_methods() {} diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.expected b/tests/ui/function-stubbing-error/unsupported_resolutions.expected index 1b4c00d22f4f..e723ac97813d 100644 --- a/tests/ui/function-stubbing-error/unsupported_resolutions.expected +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.expected @@ -1,8 +1,4 @@ -error: failed to resolve `<[char ; 10]>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `<& [u32]>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `<& [u32] as Foo>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `<(i32 , i32) as Foo>::foo`: Kani currently cannot resolve path including primitive types -error: failed to resolve `u8::foo`: Kani currently cannot resolve path including primitive types +error: Kani currently does not support stubbing trait implementations. error: failed to resolve `::bar`: unable to find `bar` inside trait `Foo` -error: Kani currently does not support stubbing trait implementations -error: failed to resolve `::foo`: Kani currently cannot resolve qualified bare function paths + +error: aborting due to 4 previous errors diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.rs b/tests/ui/function-stubbing-error/unsupported_resolutions.rs index 2fc74a0fd44f..0fcf102741eb 100644 --- a/tests/ui/function-stubbing-error/unsupported_resolutions.rs +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.rs @@ -19,7 +19,7 @@ impl Foo for Bar {} impl Foo for u8 {} -impl Foo for &[T] {} +impl Foo for [T] {} impl Foo for [char; 10] {} @@ -30,13 +30,11 @@ pub fn stub_foo() -> bool { true } +/// We still do not support stubbing for trait methods. +/// #[kani::proof] -#[kani::stub(::foo, stub_foo)] #[kani::stub(::foo, stub_foo)] #[kani::stub(::bar, stub_foo)] -#[kani::stub(u8::foo, stub_foo)] #[kani::stub(<(i32, i32) as Foo>::foo, stub_foo)] -#[kani::stub(<&[u32] as Foo>::foo, stub_foo)] -#[kani::stub(<&[u32]>::foo, stub_foo)] -#[kani::stub(<[char; 10]>::foo, stub_foo)] +#[kani::stub(<[u32] as Foo>::foo, stub_foo)] fn unsupported_args() {}