From b590998bfafa61ff8fdf1f78d978542ffc99928e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 30 Jul 2024 16:16:54 -0700 Subject: [PATCH 1/5] Extend name resolution to support qualified paths This is the first part needed for us to add support to stubbing trait implementations and primitive types. 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. --- Cargo.lock | 2 + kani-compiler/Cargo.toml | 10 +- kani-compiler/src/kani_middle/attributes.rs | 162 ++++++---- 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, 411 insertions(+), 138 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 4f371c8356e5..26cfe27079a0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -467,12 +467,14 @@ dependencies = [ "kani_metadata", "lazy_static", "num", + "quote", "regex", "serde", "serde_json", "shell-words", "strum", "strum_macros", + "syn 2.0.74", "tracing", "tracing-subscriber", ] diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 24ed00f54338..8bb82bd7fb7f 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -13,17 +13,19 @@ 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"]} +tracing = { version = "0.1", features = ["max_level_trace", "release_max_level_debug"] } +tracing-subscriber = { version = "0.3.8", features = ["env-filter", "json", "fmt"] } # Future proofing: enable backend dependencies using feature. [features] @@ -33,4 +35,4 @@ write_json_symtab = [] [package.metadata.rust-analyzer] # This package uses rustc crates. -rustc_private=true +rustc_private = true diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index f75c0607e1bc..1065c2e3bdad 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,47 @@ 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 implementation.", + ); + } + 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, + "attribute `kani::stub` takes two path arguments; found argument that is not \ + a path", + ); + 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 +842,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 +919,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 +990,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..575436c674fd 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 a 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..94f5b2a2daba --- /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 implementation. +error: failed to resolve `::foo`: Kani currently cannot resolve qualified bare function paths \ No newline at end of file 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)]\ From 893d1dd40001e196912ea33f805e5cd9c39d2596 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 22 Aug 2024 11:49:22 -0700 Subject: [PATCH 2/5] Update Cargo.lock --- Cargo.lock | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 26cfe27079a0..27e1d4dd631e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -474,7 +474,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.74", + "syn 2.0.75", "tracing", "tracing-subscriber", ] From 451acb5338766e178fe055e44009e04eea61fcba Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 29 Aug 2024 10:44:25 -0700 Subject: [PATCH 3/5] Update kani-compiler/src/kani_middle/attributes.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-compiler/src/kani_middle/attributes.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 1065c2e3bdad..976f104e0323 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -797,7 +797,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { tcx.dcx().span_err( attr.span, - "Kani currently does not support stubbing trait implementation.", + "Kani currently does not support stubbing trait implementations.", ); } Err(err) => { From 2a0a84db724f681135558ac4277800dca93797d2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 29 Aug 2024 14:34:14 -0700 Subject: [PATCH 4/5] PR feedback comments --- kani-compiler/src/kani_middle/attributes.rs | 5 +++-- .../function-stubbing-error/unsupported_resolutions.expected | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 976f104e0323..9a3ff7c1d6a6 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -814,8 +814,9 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec::foo`: Kani currently cannot resolve 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 implementation. +error: Kani currently does not support stubbing trait implementations error: failed to resolve `::foo`: Kani currently cannot resolve qualified bare function paths \ No newline at end of file From 97af20d574d3bbec376ded44ba4b88a3f6c5b977 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 30 Aug 2024 11:52:47 -0700 Subject: [PATCH 5/5] Apply suggestions from code review Co-authored-by: Felipe R. Monteiro --- kani-compiler/src/kani_middle/mod.rs | 2 +- .../ui/function-stubbing-error/unsupported_resolutions.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 575436c674fd..f281e5de5e88 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -228,7 +228,7 @@ fn find_fn_def(tcx: TyCtxt, diagnostic: &str) -> Option { stable_fn_def(tcx, *attr_id) } -/// Try to convert a internal DefId to a FnDef. +/// 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() diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.expected b/tests/ui/function-stubbing-error/unsupported_resolutions.expected index dc0fcc61af2e..1b4c00d22f4f 100644 --- a/tests/ui/function-stubbing-error/unsupported_resolutions.expected +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.expected @@ -5,4 +5,4 @@ error: failed to resolve `<(i32 , i32) as Foo>::foo`: Kani currently cannot reso 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 \ No newline at end of file +error: failed to resolve `::foo`: Kani currently cannot resolve qualified bare function paths