From 492e646e0f1699c36820a18eb7b545c08d327ffa Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 4 Sep 2024 21:22:52 -0700 Subject: [PATCH 1/6] Add support for stubbing primitive methods TODO: Still need to polish code and fix tests --- kani-compiler/src/kani_middle/resolve.rs | 230 ++++++++++++++++++----- tests/kani/Stubbing/primitive_methods.rs | 136 ++++++++++++++ 2 files changed, 322 insertions(+), 44 deletions(-) create mode 100644 tests/kani/Stubbing/primitive_methods.rs diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 88b1af86efe9..135e96b06299 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -15,16 +15,18 @@ 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}; +use stable_mir::mir::Mutability; +use stable_mir::ty::{FloatTy, FnDef, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy}; 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 syn::{Expr, ExprLit, Lit, PathSegment, QSelf, Type, TypePath}; use tracing::debug; #[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)] @@ -51,6 +53,32 @@ enum PrimitiveIdent { Usize, } +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), + } + } +} + macro_rules! validate_kind { ($tcx:ident, $id:ident, $expected:literal, $kind:pat) => {{ let def_kind = $tcx.def_kind($id); @@ -76,20 +104,26 @@ 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)?; + match &path.qself { + // Qualified path for a trait method implementation + Some(QSelf { ty: syn_ty, position, .. }) if *position > 0 => { + let ty = 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 + Some(QSelf { ty: syn_ty, .. }) if is_type_primitive(&syn_ty) => { + let ty = 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" }) + } + } + // Simple path + _ => { 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())) @@ -158,26 +192,63 @@ pub fn resolve_ty<'tcx>( }; #[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(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::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::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!() } @@ -185,9 +256,16 @@ pub fn resolve_ty<'tcx>( } /// 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 }; +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) +} + +fn is_type_primitive(typ: &syn::Type) -> bool { #[warn(non_exhaustive_omitted_patterns)] match typ { Type::Array(_) @@ -196,7 +274,12 @@ fn is_primitive(ident: &Ident) -> bool { | Type::Slice(_) | Type::Never(_) | Type::Tuple(_) => true, - Type::Path(_) => PrimitiveIdent::from_str(&token).is_ok(), + 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(_) @@ -250,6 +333,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 +376,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 +422,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 +437,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 +451,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 is_primitive(&segment) => { + let syn_ty = syn::parse2(segment.to_token_stream()).unwrap(); + let ty = 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. @@ -576,11 +672,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 +686,64 @@ 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 the Simplified Type 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 +} + +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/primitive_methods.rs b/tests/kani/Stubbing/primitive_methods.rs new file mode 100644 index 000000000000..8bef8573ace6 --- /dev/null +++ b/tests/kani/Stubbing/primitive_methods.rs @@ -0,0 +1,136 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing +// +//! This tests that we can correctly stub primitive type 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); + +/// Check that we can stub is_ascii from `char`. +pub mod char_check { + pub fn stub_is_ascii_true(_: &char) -> bool { + true + } + + #[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()); + } +} + +/// 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)] + pub struct MyStruct(u8, i32); + + pub fn stub_len_is_10(v: &[T]) -> usize { + 10 + } + + #[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); + } +} + +/// Check that we can stub raw pointer methods. +pub mod raw_ptr_check { + 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() }); + } +} + +pub mod array_check { + pub fn stub_as_slice_panic(_: &[T; N]) -> &[T] { + panic!("oops") + } + + #[kani::proof] + #[kani::should_panic] + #[kani::stub(<[i32; 10]>::as_slice, stub_as_slice_panic)] + pub fn check_stub_as_slice_panic() { + let input: [i32; 10] = kani::any(); + let slice = input.as_slice(); + assert!(slice.get(0).is_some()); + } +} From c0f21e90c9a89f29222f4834b2117da1c20652d5 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 5 Sep 2024 12:08:14 -0700 Subject: [PATCH 2/6] Split tests and add a fixme test to capture limitation --- .../fixme_stub_lowered_methods.rs | 26 ++++ .../StubPrimitives/stub_char_methods.rs | 18 +++ .../StubPrimitives/stub_int_methods.rs | 39 +++++ .../StubPrimitives/stub_ptr_methods.rs | 38 +++++ .../StubPrimitives/stub_slice_methods.rs | 37 +++++ tests/kani/Stubbing/primitive_methods.rs | 136 ------------------ 6 files changed, 158 insertions(+), 136 deletions(-) create mode 100644 tests/kani/Stubbing/StubPrimitives/fixme_stub_lowered_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_char_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 delete mode 100644 tests/kani/Stubbing/primitive_methods.rs 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_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_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/kani/Stubbing/primitive_methods.rs b/tests/kani/Stubbing/primitive_methods.rs deleted file mode 100644 index 8bef8573ace6..000000000000 --- a/tests/kani/Stubbing/primitive_methods.rs +++ /dev/null @@ -1,136 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-flags: -Z stubbing -// -//! This tests that we can correctly stub primitive type 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); - -/// Check that we can stub is_ascii from `char`. -pub mod char_check { - pub fn stub_is_ascii_true(_: &char) -> bool { - true - } - - #[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()); - } -} - -/// 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)] - pub struct MyStruct(u8, i32); - - pub fn stub_len_is_10(v: &[T]) -> usize { - 10 - } - - #[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); - } -} - -/// Check that we can stub raw pointer methods. -pub mod raw_ptr_check { - 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() }); - } -} - -pub mod array_check { - pub fn stub_as_slice_panic(_: &[T; N]) -> &[T] { - panic!("oops") - } - - #[kani::proof] - #[kani::should_panic] - #[kani::stub(<[i32; 10]>::as_slice, stub_as_slice_panic)] - pub fn check_stub_as_slice_panic() { - let input: [i32; 10] = kani::any(); - let slice = input.as_slice(); - assert!(slice.get(0).is_some()); - } -} From 9bed3140cb346038c938b3f43678c70b1d8d8f05 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 5 Sep 2024 14:14:44 -0700 Subject: [PATCH 3/6] Fix type resolution for redundant qualified paths More tests adjustments --- kani-compiler/src/kani_middle/resolve.rs | 271 +++++------------- .../kani_middle/resolve/type_resolution.rs | 202 +++++++++++++ .../resolution_errors.rs | 23 ++ .../unsupported_resolutions.expected | 10 +- .../unsupported_resolutions.rs | 10 +- 5 files changed, 300 insertions(+), 216 deletions(-) create mode 100644 kani-compiler/src/kani_middle/resolve/type_resolution.rs 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 135e96b06299..46cb5e12efb1 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. @@ -18,66 +19,15 @@ 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::mir::Mutability; -use stable_mir::ty::{FloatTy, FnDef, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy}; +use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind}; 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::{Expr, ExprLit, Lit, PathSegment, QSelf, 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}; -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), - } - } -} +mod type_resolution; macro_rules! validate_kind { ($tcx:ident, $id:ident, $expected:literal, $kind:pat) => {{ @@ -89,6 +39,7 @@ macro_rules! validate_kind { } }}; } +pub(crate) use validate_kind; #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum FnResolution { @@ -104,17 +55,18 @@ pub fn resolve_fn_path<'tcx>( current_module: LocalDefId, path: &TypePath, ) -> Result> { + let _span = debug_span!("resolve_fn_path", ?path).entered(); match &path.qself { - // Qualified path for a trait method implementation + // Qualified path for a trait method implementation, like `::bar`. Some(QSelf { ty: syn_ty, position, .. }) if *position > 0 => { - let ty = resolve_ty(tcx, current_module, &syn_ty)?; + 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 }) } - // Qualified path for a primitive type - Some(QSelf { ty: syn_ty, .. }) if is_type_primitive(&syn_ty) => { - let ty = resolve_ty(tcx, current_module, &syn_ty)?; + // 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())) @@ -122,8 +74,15 @@ pub fn resolve_fn_path<'tcx>( 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())) @@ -131,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}"), })?; @@ -177,123 +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(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!() - } - } -} - -/// Checks if a Path segment represents a primitive -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) -} - -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!() - } - } -} - /// 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. @@ -303,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"); @@ -377,7 +220,7 @@ impl<'tcx> fmt::Display for ResolveError<'tcx> { write!(f, "unable to find `{unresolved}` inside {def_desc}") } ResolveError::MissingPrimitiveItem { base, unresolved } => { - write!(f, "unable to find `{unresolved}` inside {base}") + write!(f, "unable to find `{unresolved}` inside `{base}`") } ResolveError::UnsupportedPath { kind } => { write!(f, "Kani currently cannot resolve {kind}") @@ -460,9 +303,9 @@ fn resolve_prefix<'tcx>( resolve_super(tcx, current_module, path.segments.iter().peekable()) } // Path starting with a primitive, such as "u8::" - (None, Some(segment)) if is_primitive(&segment) => { + (None, Some(segment)) if type_resolution::is_primitive(&segment) => { let syn_ty = syn::parse2(segment.to_token_stream()).unwrap(); - let ty = resolve_ty(tcx, current_module, &syn_ty)?; + let ty = type_resolution::resolve_ty(tcx, current_module, &syn_ty)?; resolve_in_primitive(tcx, ty, segments) } (None, Some(segment)) => { @@ -657,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, @@ -736,14 +612,3 @@ fn is_item_name(tcx: TyCtxt, item: DefId, name: &str) -> bool { let last = item_path.split("::").last().unwrap(); last == name } - -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/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/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() {} From 7e68a323aa9ebc06ea0b4cc2564e91edde2dde62 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 5 Sep 2024 15:41:19 -0700 Subject: [PATCH 4/6] Add missing file --- .../resolution_errors.expected | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 tests/ui/function-stubbing-error/resolution_errors.expected 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)] +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + From 3242bf8992e7f27756aafdf4f2353aefe5a1d712 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Sep 2024 11:18:01 -0700 Subject: [PATCH 5/6] Add tests for stubbing bool and float types --- .../StubPrimitives/stub_bool_methods.rs | 35 +++++++++++++++++++ .../StubPrimitives/stub_float_methods.rs | 32 +++++++++++++++++ 2 files changed, 67 insertions(+) create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_bool_methods.rs create mode 100644 tests/kani/Stubbing/StubPrimitives/stub_float_methods.rs 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_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); From ee20fcacaff461751abc3573643d072991778801 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Sep 2024 11:21:44 -0700 Subject: [PATCH 6/6] Update kani-compiler/src/kani_middle/resolve.rs --- kani-compiler/src/kani_middle/resolve.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 46cb5e12efb1..b2b00c1e4a40 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -572,7 +572,7 @@ fn resolve_in_trait<'tcx>( /// Resolves a primitive type function. /// -/// This function assumes that the Simplified Type is a primitive. +/// This function assumes that `ty` is a primitive. fn resolve_in_primitive<'tcx, 'a, I>( tcx: TyCtxt<'tcx>, ty: Ty,