From 01a00b069d3fb81cf3a94ac0fc8e2a18507e8746 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 30 Aug 2024 15:07:39 -0700 Subject: [PATCH] Extend name resolution to support qualified paths (Partial Fix) (#3457) This is the first part needed for us to add support to stubbing trait implementations (https://github.com/model-checking/kani/issues/1997) and primitive types (https://github.com/model-checking/kani/issues/2646). After this change, we need to change stubs to accept a `FnResolution` instead of `FnDef`. We also need to find out how to retrieve methods of primitive types. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro --- Cargo.lock | 2 + kani-compiler/Cargo.toml | 6 +- kani-compiler/src/kani_middle/attributes.rs | 163 ++++++---- kani-compiler/src/kani_middle/mod.rs | 20 +- kani-compiler/src/kani_middle/resolve.rs | 300 ++++++++++++++---- kani-compiler/src/main.rs | 1 + .../{expected => invalid_stub_args.expected} | 0 .../{main.rs => invalid_stub_args.rs} | 2 +- .../unsupported_resolutions.expected | 8 + .../unsupported_resolutions.rs | 42 +++ tests/ui/invalid-attribute/expected | 2 +- 11 files changed, 410 insertions(+), 136 deletions(-) rename tests/ui/function-stubbing-error/{expected => invalid_stub_args.expected} (100%) rename tests/ui/function-stubbing-error/{main.rs => invalid_stub_args.rs} (87%) create mode 100644 tests/ui/function-stubbing-error/unsupported_resolutions.expected create mode 100644 tests/ui/function-stubbing-error/unsupported_resolutions.rs diff --git a/Cargo.lock b/Cargo.lock index 0b8f681ae6c1..0da9ff2e2159 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -476,12 +476,14 @@ dependencies = [ "kani_metadata", "lazy_static", "num", + "quote", "regex", "serde", "serde_json", "shell-words", "strum", "strum_macros", + "syn 2.0.76", "tracing", "tracing-subscriber", "tracing-tree", diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index fc06c393f3eb..e8e564f9616a 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -13,14 +13,16 @@ cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = clap = { version = "4.4.11", features = ["derive", "cargo"] } home = "0.5" itertools = "0.13" -kani_metadata = {path = "../kani_metadata"} +kani_metadata = { path = "../kani_metadata" } lazy_static = "1.4.0" num = { version = "0.4.0", optional = true } +quote = "1.0.36" regex = "1.7.0" serde = { version = "1", optional = true } serde_json = "1" strum = "0.26" strum_macros = "0.26" +syn = { version = "2.0.72", features = ["parsing", "extra-traits"] } shell-words = "1.0.0" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} @@ -34,7 +36,7 @@ write_json_symtab = [] [package.metadata.rust-analyzer] # This package uses rustc crates. -rustc_private=true +rustc_private = true [lints] workspace = true diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index f75c0607e1bc..9a3ff7c1d6a6 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -5,9 +5,9 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; +use quote::ToTokens; use rustc_ast::{ attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, - NestedMetaItem, }; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; @@ -19,10 +19,13 @@ use stable_mir::mir::mono::Instance as InstanceStable; use stable_mir::{CrateDef, DefId as StableDefId}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; +use syn::parse::Parser; +use syn::punctuated::Punctuated; +use syn::{PathSegment, TypePath}; use tracing::{debug, trace}; -use super::resolve::{self, resolve_fn, ResolveError}; +use super::resolve::{resolve_fn, resolve_fn_path, FnResolution, ResolveError}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] @@ -555,19 +558,19 @@ impl<'tcx> KaniAttributes<'tcx> { for (name, def_id, span) in self.interpret_stub_verified_attribute() { if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() { dcx.struct_span_err( - span, + span, + format!( + "Failed to generate verified stub: Function `{}` has no contract.", + self.item_name(), + ), + ) + .with_span_note( + self.tcx.def_span(def_id), format!( - "Failed to generate verified stub: Function `{}` has no contract.", - self.item_name(), + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), ), ) - .with_span_note( - self.tcx.def_span(def_id), - format!( - "Try adding a contract to this function or use the unsound `{}` attribute instead.", - KaniAttributeKind::Stub.as_ref(), - ), - ) .emit(); return; } @@ -787,20 +790,48 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { let current_module = tcx.parent_module_from_def_id(harness.expect_local()); - let check_resolve = |attr: &Attribute, name: &str| { - let result = resolve::resolve_fn(tcx, current_module.to_local_def_id(), name); - if let Err(err) = result { - tcx.dcx().span_err(attr.span, format!("failed to resolve `{name}`: {err}")); + let check_resolve = |attr: &Attribute, path: &TypePath| { + let result = resolve_fn_path(tcx, current_module.to_local_def_id(), path); + match result { + Ok(FnResolution::Fn(_)) => { /* no-op */ } + Ok(FnResolution::FnImpl { .. }) => { + tcx.dcx().span_err( + attr.span, + "Kani currently does not support stubbing trait implementations.", + ); + } + Err(err) => { + tcx.dcx().span_err( + attr.span, + format!("failed to resolve `{}`: {err}", pretty_type_path(path)), + ); + } } }; attributes .iter() - .filter_map(|attr| match parse_paths(attr) { - Ok(paths) => match paths.as_slice() { + .filter_map(|attr| { + let paths = parse_paths(attr).unwrap_or_else(|_| { + tcx.dcx().span_err( + attr.span, + format!( + "attribute `kani::{}` takes two path arguments; found argument that is not a path", + KaniAttributeKind::Stub.as_ref()) + ); + vec![] + }); + match paths.as_slice() { [orig, replace] => { check_resolve(attr, orig); check_resolve(attr, replace); - Some(Stub { original: orig.clone(), replacement: replace.clone() }) + Some(Stub { + original: orig.to_token_stream().to_string(), + replacement: replace.to_token_stream().to_string(), + }) + } + [] => { + /* Error was already emitted */ + None } _ => { tcx.dcx().span_err( @@ -812,13 +843,6 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { - tcx.dcx().span_err( - error_span, - "attribute `kani::stub` takes two path arguments; found argument that is not a path", - ); - None } }) .collect() @@ -896,35 +920,13 @@ fn parse_integer(attr: &Attribute) -> Option { } /// Extracts a vector with the path arguments of an attribute. -/// Emits an error if it couldn't convert any of the arguments. -fn parse_paths(attr: &Attribute) -> Result, Span> { - let attr_args = attr.meta_item_list(); - attr_args - .unwrap_or_default() - .iter() - .map(|arg| match arg { - NestedMetaItem::Lit(item) => Err(item.span), - NestedMetaItem::MetaItem(item) => parse_path(item).ok_or(item.span), - }) - .collect() -} - -/// Extracts a path from an attribute item, returning `None` if the item is not -/// syntactically a path. -fn parse_path(meta_item: &MetaItem) -> Option { - if meta_item.is_word() { - Some( - meta_item - .path - .segments - .iter() - .map(|seg| seg.ident.as_str()) - .collect::>() - .join("::"), - ) - } else { - None - } +/// +/// Emits an error if it couldn't convert any of the arguments and return an empty vector. +fn parse_paths(attr: &Attribute) -> Result, syn::Error> { + let syn_attr = syn_attr(attr); + let parser = Punctuated::::parse_terminated; + let paths = syn_attr.parse_args_with(parser)?; + Ok(paths.into_iter().collect()) } /// Parse the arguments of the attribute into a (key, value) map. @@ -989,3 +991,54 @@ pub fn matches_diagnostic(tcx: TyCtxt, def: T, attr_name: &str) -> } false } + +/// Parse an attribute using `syn`. +/// +/// This provides a user-friendly interface to manipulate than the internal compiler AST. +fn syn_attr(attr: &Attribute) -> syn::Attribute { + let attr_str = rustc_ast_pretty::pprust::attribute_to_string(attr); + let parser = syn::Attribute::parse_outer; + parser.parse_str(&attr_str).unwrap().pop().unwrap() +} + +/// Return a more user-friendly string for path by trying to remove unneeded whitespace. +/// +/// `quote!()` and `TokenString::to_string()` introduce unnecessary space around separators. +/// This happens because these methods end up using TokenStream display, which has no +/// guarantees on the format printed. +/// +/// +/// E.g.: The path `<[char; 10]>::foo` printed with token stream becomes `< [ char ; 10 ] > :: foo`. +/// while this function turns this into `<[char ; 10]>::foo`. +/// +/// Thus, this can still be improved to handle the `qself.ty`. +/// +/// We also don't handle path segments, but users shouldn't pass generic arguments to our +/// attributes. +fn pretty_type_path(path: &TypePath) -> String { + fn segments_str<'a, I>(segments: I) -> String + where + I: IntoIterator, + { + // We don't bother with path arguments for now since users shouldn't provide them. + segments + .into_iter() + .map(|segment| segment.to_token_stream().to_string()) + .intersperse("::".to_string()) + .collect() + } + let leading = if path.path.leading_colon.is_some() { "::" } else { "" }; + if let Some(qself) = &path.qself { + let pos = qself.position; + let qself_str = qself.ty.to_token_stream().to_string(); + if pos == 0 { + format!("<{qself_str}>::{}", segments_str(&path.path.segments)) + } else { + let before = segments_str(path.path.segments.iter().take(pos)); + let after = segments_str(path.path.segments.iter().skip(pos)); + format!("<{qself_str} as {before}>::{after}") + } + } else { + format!("{leading}{}", segments_str(&path.path.segments)) + } +} diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index a5d077d9c16e..f281e5de5e88 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -6,7 +6,7 @@ use std::collections::HashSet; use crate::kani_queries::QueryDb; -use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE}; +use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE}; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, @@ -225,10 +225,16 @@ fn find_fn_def(tcx: TyCtxt, diagnostic: &str) -> Option { .all_diagnostic_items(()) .name_to_id .get(&rustc_span::symbol::Symbol::intern(diagnostic))?; - let TyKind::RigidTy(RigidTy::FnDef(def, _)) = - rustc_internal::stable(tcx.type_of(attr_id)).value.kind() - else { - return None; - }; - Some(def) + stable_fn_def(tcx, *attr_id) +} + +/// Try to convert an internal `DefId` to a `FnDef`. +pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option { + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = + rustc_internal::stable(tcx.type_of(def_id)).value.kind() + { + Some(def) + } else { + None + } } diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index ca4e8e749b75..88b1af86efe9 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -9,45 +9,110 @@ //! //! Note that glob use statements can form loops. The paths can also walk through the loop. -use rustc_smir::rustc_internal; -use std::collections::HashSet; -use std::fmt; -use std::iter::Peekable; - +use crate::kani_middle::stable_fn_def; +use quote::ToTokens; 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::TyCtxt; -use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use rustc_smir::rustc_internal; +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::{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, +} + +macro_rules! validate_kind { + ($tcx:ident, $id:ident, $expected:literal, $kind:pat) => {{ + let def_kind = $tcx.def_kind($id); + if matches!(def_kind, $kind) { + Ok($id) + } else { + Err(ResolveError::UnexpectedType { $tcx, item: $id, expected: $expected }) + } + }}; +} + +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +pub enum FnResolution { + Fn(FnDef), + FnImpl { def: FnDef, ty: Ty }, +} + +/// Resolve a path to a function / method. +/// +/// The path can either be a simple path or a qualified path. +pub fn resolve_fn_path<'tcx>( + tcx: TyCtxt<'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 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 + 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())) + } + } +} + /// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`. /// -/// TODO: Extend this implementation to handle qualified paths and simple paths -/// corresponding to trait methods. -/// +/// 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 result = resolve_path(tcx, current_module, path_str); - match result { - Ok(def_id) => { - let def_kind = tcx.def_kind(def_id); - if matches!(def_kind, DefKind::AssocFn | DefKind::Fn) { - Ok(def_id) - } else { - Err(ResolveError::UnexpectedType { - tcx, - item: def_id, - expected: "function / method", - }) - } - } - err => err, + let path = syn::parse_str(path_str).map_err(|err| ResolveError::InvalidPath { + msg: format!("Expected a path, but found `{path_str}`. {err}"), + })?; + let result = resolve_fn_path(tcx, current_module, &path)?; + if let FnResolution::Fn(def) = result { + Ok(rustc_internal::internal(tcx, def.def_id())) + } else { + Err(ResolveError::UnsupportedPath { kind: "qualified paths" }) } } @@ -78,25 +143,93 @@ 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. -/// -/// Note: This function was written to be generic, however, it has only been tested for functions. -pub(crate) fn resolve_path<'tcx>( +fn resolve_path<'tcx>( tcx: TyCtxt<'tcx>, current_module: LocalDefId, - path_str: &str, + 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_str)?; - path.segments.into_iter().try_fold(path.base, |base, name| { - debug!(?base, ?name, "resolve_path"); + 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::Trait => resolve_in_trait(tcx, base, &name), kind => { debug!(?base, ?kind, "resolve_path: unexpected item"); Err(ResolveError::UnexpectedType { tcx, item: base, expected: "module" }) @@ -119,6 +252,8 @@ pub enum ResolveError<'tcx> { MissingItem { tcx: TyCtxt<'tcx>, base: DefId, 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. + UnsupportedPath { kind: &'static str }, } impl<'tcx> fmt::Debug for ResolveError<'tcx> { @@ -156,12 +291,15 @@ impl<'tcx> fmt::Display for ResolveError<'tcx> { let def_desc = description(*tcx, *base); write!(f, "unable to find `{unresolved}` inside {def_desc}") } + ResolveError::UnsupportedPath { kind } => { + write!(f, "Kani currently cannot resolve {kind}") + } } } } /// The segments of a path. -type Segments = Vec; +type Segments = Vec; /// A path consisting of a starting point and a bunch of segments. If `base` /// matches `Base::LocalModule { id: _, may_be_external_path : true }`, then @@ -174,8 +312,6 @@ struct Path { /// Identifier for the top module of the crate. const CRATE: &str = "crate"; -/// rustc represents initial `::` as `{{root}}`. -const ROOT: &str = "{{root}}"; /// Identifier for the current module. const SELF: &str = "self"; /// Identifier for the parent of the current module. @@ -186,56 +322,56 @@ const SUPER: &str = "super"; fn resolve_prefix<'tcx>( tcx: TyCtxt<'tcx>, current_module: LocalDefId, - name: &str, + path: &syn::Path, ) -> Result> { - debug!(?name, ?current_module, "resolve_prefix"); + debug!(?path, ?current_module, "resolve_prefix"); // Split the string into segments separated by `::`. Trim the whitespace // since path strings generated from macros sometimes add spaces around // `::`. - let mut segments = name.split("::").map(|s| s.trim().to_string()).peekable(); - assert!(segments.peek().is_some(), "expected identifier, found `{name}`"); + let mut segments = path.segments.iter(); // Resolve qualifiers `crate`, initial `::`, and `self`. The qualifier // `self` may be followed be `super` (handled below). - let first = segments.peek().unwrap().as_str(); - match first { - ROOT => { + match (path.leading_colon, segments.next()) { + (Some(_), Some(segment)) => { // Skip root and get the external crate from the name that follows `::`. - let next = segments.nth(1); - if let Some(next_name) = next { - let result = resolve_external(tcx, &next_name); - if let Some(def_id) = result { - Ok(Path { base: def_id, segments: segments.collect() }) - } else { - Err(ResolveError::MissingItem { - tcx, - base: current_module.to_def_id(), - unresolved: next_name, - }) - } + let next_name = segment.ident.to_string(); + let result = resolve_external(tcx, &next_name); + if let Some(def_id) = result { + Ok(Path { base: def_id, segments: segments.cloned().collect() }) } else { - Err(ResolveError::InvalidPath { msg: "expected identifier after `::`".to_string() }) + Err(ResolveError::MissingItem { + tcx, + base: current_module.to_def_id(), + unresolved: next_name, + }) } } - CRATE => { - segments.next(); + (Some(_), None) => { + Err(ResolveError::InvalidPath { msg: "expected identifier after `::`".to_string() }) + } + (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); let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() { None => current_module, Some((hir_id, _)) => hir_id.owner.def_id, }; - Ok(Path { base: crate_root.to_def_id(), segments: segments.collect() }) + Ok(Path { base: crate_root.to_def_id(), segments: segments.cloned().collect() }) } - SELF => { - segments.next(); - resolve_super(tcx, current_module, segments) + (None, Some(segment)) if segment.ident == SELF => { + resolve_super(tcx, current_module, segments.peekable()) } - SUPER => resolve_super(tcx, current_module, segments), - _ => { + (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" }) + } + (None, Some(segment)) => { // No special key word was used. Try local first otherwise try external name. - let next_name = segments.next().unwrap(); + let next_name = segment.ident.to_string(); let def_id = resolve_in_module(tcx, current_module.to_def_id(), &next_name).or_else(|err| { if matches!(err, ResolveError::MissingItem { .. }) { @@ -245,25 +381,28 @@ fn resolve_prefix<'tcx>( Err(err) } })?; - Ok(Path { base: def_id, segments: segments.collect() }) + Ok(Path { base: def_id, segments: segments.cloned().collect() }) + } + _ => { + unreachable!("Empty path: `{path:?}`") } } } /// Pop up the module stack until we account for all the `super` prefixes. /// This method will error out if it tries to backtrace from the root crate. -fn resolve_super<'tcx, I>( +fn resolve_super<'tcx, 'a, I>( tcx: TyCtxt, current_module: LocalDefId, mut segments: Peekable, ) -> Result> where - I: Iterator, + I: Iterator, { let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); let mut parents = tcx.hir().parent_iter(current_module_hir_id); let mut base_module = current_module; - while segments.next_if(|segment| segment == SUPER).is_some() { + while segments.next_if(|segment| segment.ident == SUPER).is_some() { if let Some((parent, _)) = parents.next() { debug!("parent: {parent:?}"); base_module = parent.owner.def_id; @@ -272,7 +411,7 @@ where } } debug!("base: {base_module:?}"); - Ok(Path { base: base_module.to_def_id(), segments: segments.collect() }) + Ok(Path { base: base_module.to_def_id(), segments: segments.cloned().collect() }) } /// Resolves an external crate name. @@ -422,8 +561,7 @@ fn resolve_in_glob_use(tcx: TyCtxt, res: &Res, name: &str) -> RelativeResolution } } -/// Resolves a method in a type. It currently does not resolve trait methods -/// (see ). +/// Resolves a function in a type. fn resolve_in_type<'tcx>( tcx: TyCtxt<'tcx>, type_id: DefId, @@ -445,3 +583,25 @@ fn resolve_in_type<'tcx>( }) .ok_or_else(missing_item_err) } + +/// Resolves a function in a trait. +fn resolve_in_trait<'tcx>( + tcx: TyCtxt<'tcx>, + trait_id: DefId, + name: &str, +) -> Result> { + debug!(?name, ?trait_id, "resolve_in_trait"); + 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). + 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 + }) + .ok_or_else(missing_item_err) +} diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index e47483fb4fa5..3a7816c1b084 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -15,6 +15,7 @@ #![feature(let_chains)] #![feature(f128)] #![feature(f16)] +#![feature(non_exhaustive_omitted_patterns_lint)] extern crate rustc_abi; extern crate rustc_ast; extern crate rustc_ast_pretty; diff --git a/tests/ui/function-stubbing-error/expected b/tests/ui/function-stubbing-error/invalid_stub_args.expected similarity index 100% rename from tests/ui/function-stubbing-error/expected rename to tests/ui/function-stubbing-error/invalid_stub_args.expected diff --git a/tests/ui/function-stubbing-error/main.rs b/tests/ui/function-stubbing-error/invalid_stub_args.rs similarity index 87% rename from tests/ui/function-stubbing-error/main.rs rename to tests/ui/function-stubbing-error/invalid_stub_args.rs index c433e352e740..baed360b2dda 100644 --- a/tests/ui/function-stubbing-error/main.rs +++ b/tests/ui/function-stubbing-error/invalid_stub_args.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main -Z stubbing +// kani-flags: -Z stubbing // //! This tests whether we detect syntactically misformed `kani::stub` annotations. diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.expected b/tests/ui/function-stubbing-error/unsupported_resolutions.expected new file mode 100644 index 000000000000..1b4c00d22f4f --- /dev/null +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.expected @@ -0,0 +1,8 @@ +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: 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 diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.rs b/tests/ui/function-stubbing-error/unsupported_resolutions.rs new file mode 100644 index 000000000000..2fc74a0fd44f --- /dev/null +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.rs @@ -0,0 +1,42 @@ +// 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 unsupported paths. + +/// Dummy structure +pub struct Bar; + +/// Dummy trait +pub trait Foo { + fn foo() -> bool { + false + } +} + +impl Foo for Bar {} + +impl Foo for u8 {} + +impl Foo for &[T] {} + +impl Foo for [char; 10] {} + +impl Foo for (i32, i32) {} + +/// Dummy stub +pub fn stub_foo() -> bool { + true +} + +#[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)] +fn unsupported_args() {} diff --git a/tests/ui/invalid-attribute/expected b/tests/ui/invalid-attribute/expected index 75be29c13e83..a5623dba5b6e 100644 --- a/tests/ui/invalid-attribute/expected +++ b/tests/ui/invalid-attribute/expected @@ -5,7 +5,7 @@ attrs.rs | ^^^^^^^^^^^^^^^^^^^^^^^^^^\ | -error: attribute `kani::stub` takes two path arguments; found 0\ +error: attribute `kani::stub` takes two path arguments; found argument that is not a path\ attrs.rs |\ | #[kani::stub(invalid=opt)]\