From 9675c87e7ebbd364b9f4bb2219b294655178dcbb Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 30 May 2025 11:22:04 -0400 Subject: [PATCH 1/4] clarify difference btwn reachability and parsing checks --- kani-compiler/src/kani_middle/attributes.rs | 6 ++++-- kani-compiler/src/kani_middle/mod.rs | 4 ++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 911e1682c143..38849313d2cf 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -508,8 +508,10 @@ impl<'tcx> KaniAttributes<'tcx> { } /// Check that the function specified in the `proof_for_contract` attribute - /// is reachable and emit an error if it isn't - pub fn check_proof_for_contract(&self, reachable_functions: &HashSet) { + /// is reachable and emit an error if it isn't. + /// This is different from the earlier `check_attributes` call: + /// that checks that the specified target exists, but not if we can reach that target from the harness. + pub fn check_proof_for_contract_reachability(&self, reachable_functions: &HashSet) { if let Some((symbol, function, span)) = self.interpret_for_contract_attribute() && !reachable_functions.contains(&function) { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index e6839487c046..adb76ed8b61e 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -113,8 +113,8 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) let attributes = KaniAttributes::for_def_id(tcx, def_id); // Check if any unstable attribute was reached. attributes.check_unstable_features(&queries.args().unstable_features); - // Check whether all `proof_for_contract` functions are reachable - attributes.check_proof_for_contract(&reachable_functions); + // Check whether all `proof_for_contract` targets are reachable + attributes.check_proof_for_contract_reachability(&reachable_functions); def_ids.insert(def_id); } } From 452c466d7948b9c4549b63ab1e7504f11dfda268 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 3 Jun 2025 22:12:30 -0400 Subject: [PATCH 2/4] nit: make stable the suffix in DefIdStable to be consistent w/ rest of module --- kani-compiler/src/kani_middle/attributes.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 38849313d2cf..21eb0f96cf4b 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -15,7 +15,7 @@ use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; use stable_mir::crate_def::Attribute as AttributeStable; use stable_mir::mir::mono::Instance as InstanceStable; -use stable_mir::{CrateDef, DefId as StableDefId, Symbol as SymbolStable}; +use stable_mir::{CrateDef, DefId as DefIdStable, Symbol as SymbolStable}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; use syn::parse::Parser; @@ -161,7 +161,7 @@ impl<'tcx> KaniAttributes<'tcx> { } /// Look up the attributes by a stable MIR DefID - pub fn for_def_id(tcx: TyCtxt<'tcx>, def_id: StableDefId) -> Self { + pub fn for_def_id(tcx: TyCtxt<'tcx>, def_id: DefIdStable) -> Self { KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, def_id)) } From 71c2d19797fc97235bffe44871c752a5f7730cc6 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 3 Jun 2025 22:19:13 -0400 Subject: [PATCH 3/4] nit: change lifetimes in expect_single to match rest of module the attribute lifetime is tied to TyCtxt, so we should make that explicit --- kani-compiler/src/kani_middle/attributes.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 21eb0f96cf4b..1724912d06a3 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -730,11 +730,11 @@ fn expect_key_string_value( } } -fn expect_single<'a>( +fn expect_single<'tcx>( tcx: TyCtxt, kind: KaniAttributeKind, - attributes: &'a Vec<&'a Attribute>, -) -> &'a Attribute { + attributes: &Vec<&'tcx Attribute>, +) -> &'tcx Attribute { let attr = attributes.first().unwrap_or_else(|| { panic!("expected at least one attribute {} in {attributes:?}", kind.as_ref()) }); From 0bfc261717c6b4cc2f4112b110177f14e8a2c5e0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 3 Jun 2025 22:31:15 -0400 Subject: [PATCH 4/4] rewrite `interpret_stub_verified_attribute` and `interpret_for_contract_attribute` to call `resolve_fn_path` and thereby be able to resolve qualified paths, which they can't do in the current impl because `resolve_from_mod` only handled simple paths --- .../codegen_aeneas_llbc/compiler_interface.rs | 8 +- .../compiler_interface.rs | 19 +- kani-compiler/src/kani_middle/attributes.rs | 330 +++++++++--------- .../src/kani_middle/codegen_units.rs | 26 +- kani-compiler/src/kani_middle/metadata.rs | 10 +- kani-compiler/src/kani_middle/mod.rs | 4 +- kani-compiler/src/kani_middle/resolve.rs | 37 +- .../src/kani_middle/transform/contracts.rs | 25 +- .../missing_contract_for_check.expected | 2 +- .../missing_contract_for_replace.expected | 2 +- .../expected/stubbing-ambiguous-path/expected | 10 +- .../invalid_target_path.expected | 16 +- .../unsupported_resolutions.expected | 3 +- .../invalid_inherent_impls.expected | 18 +- tests/ui/unknown-contract-harness/expected | 9 +- 15 files changed, 246 insertions(+), 273 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 0ee1e00ba6f1..eab0d04a6770 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -38,6 +38,7 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::ty::FnDef; use stable_mir::{CrateDef, DefId}; use std::any::Any; use std::fs::File; @@ -233,7 +234,8 @@ impl CodegenBackend for LlbcCodegenBackend { tcx, &[MonoItem::Fn(*harness)], model_path, - contract_metadata, + contract_metadata + .map(|def| rustc_internal::internal(tcx, def.def_id())), transformer, ); transformer = BodyTransformation::new(&queries, tcx, &unit); @@ -351,9 +353,9 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { fn contract_metadata_for_harness( tcx: TyCtxt, def_id: DefId, -) -> Result, ErrorGuaranteed> { +) -> Result, ErrorGuaranteed> { let attrs = KaniAttributes::for_def_id(tcx, def_id); - Ok(attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)) + Ok(attrs.interpret_for_contract_attribute()) } /// Return a struct that contains information about the codegen results as expected by `rustc`. diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index de082cb1c903..3bc5d6abf8eb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -42,6 +42,7 @@ use rustc_span::{Symbol, sym}; use rustc_target::spec::PanicStrategy; use stable_mir::CrateDef; use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::ty::FnDef; use std::any::Any; use std::collections::BTreeMap; use std::fmt::Write; @@ -213,24 +214,23 @@ impl GotocCodegenBackend { (gcx, items, contract_info) } - /// Given a contract harness, get the DefId of its target. + /// Given a harness, return the DefId of its target if it's a contract harness. /// For manual harnesses, extract it from the #[proof_for_contract] attribute. /// For automatic harnesses, extract the target from the harness's GenericArgs. - fn target_def_id_for_harness( + fn target_if_contract_harness( &self, tcx: TyCtxt, harness: &Instance, is_automatic_harness: bool, - ) -> Option { + ) -> Option { if is_automatic_harness { let kind = harness.args().0[0].expect_ty().kind(); let (fn_to_verify_def, _) = kind.fn_def().unwrap(); - let def_id = fn_to_verify_def.def_id(); - let attrs = KaniAttributes::for_def_id(tcx, def_id); - if attrs.has_contract() { Some(rustc_internal::internal(tcx, def_id)) } else { None } + let attrs = KaniAttributes::for_def_id(tcx, fn_to_verify_def.def_id()); + if attrs.has_contract() { Some(fn_to_verify_def) } else { None } } else { let harness_attrs = KaniAttributes::for_def_id(tcx, harness.def.def_id()); - harness_attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) + harness_attrs.interpret_for_contract_attribute() } } } @@ -341,13 +341,14 @@ impl CodegenBackend for GotocCodegenBackend { let model_path = units.harness_model_path(*harness).unwrap(); let is_automatic_harness = units.is_automatic_harness(harness); let contract_metadata = - self.target_def_id_for_harness(tcx, harness, is_automatic_harness); + self.target_if_contract_harness(tcx, harness, is_automatic_harness); let (gcx, items, contract_info) = self.codegen_items( tcx, &[MonoItem::Fn(*harness)], model_path, &results.machine_model, - contract_metadata, + contract_metadata + .map(|def| rustc_internal::internal(tcx, def.def_id())), transformer, ); if gcx.has_loop_contracts { diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 1724912d06a3..6fba15e66350 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -8,13 +8,13 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; use rustc_ast::{LitKind, MetaItem, MetaItemKind}; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId}; +use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId, def_id::LocalDefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; -use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; use stable_mir::crate_def::Attribute as AttributeStable; use stable_mir::mir::mono::Instance as InstanceStable; +use stable_mir::ty::FnDef as FnDefStable; use stable_mir::{CrateDef, DefId as DefIdStable, Symbol as SymbolStable}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -22,7 +22,7 @@ use syn::parse::Parser; use syn::punctuated::Punctuated; use syn::{Expr, ExprLit, Lit, PathSegment, TypePath}; -use super::resolve::{FnResolution, ResolveError, resolve_fn, resolve_fn_path}; +use super::resolve::{FnResolution, ResolveError, resolve_fn_path}; use tracing::{debug, trace}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] @@ -203,33 +203,14 @@ impl<'tcx> KaniAttributes<'tcx> { /// for error reporting. /// /// Any error is emitted and the attribute is filtered out. - pub fn interpret_stub_verified_attribute(&self) -> Vec<(Symbol, DefId, Span)> { + pub fn interpret_stub_verified_attribute(&self) -> Vec { self.map .get(&KaniAttributeKind::StubVerified) .map_or([].as_slice(), Vec::as_slice) .iter() .filter_map(|attr| { - let name = expect_key_string_value(self.tcx.sess, attr).ok()?; - let def = self - .resolve_from_mod(name.as_str()) - .map_err(|e| { - let mut err = self.tcx.dcx().struct_span_err( - attr.span(), - format!( - "Failed to resolve replacement function {}: {e}", - name.as_str() - ), - ); - if let ResolveError::AmbiguousPartialPath { .. } = e { - err = err.with_help(format!( - "Replace {} with a specific implementation.", - name.as_str() - )); - } - err.emit(); - }) - .ok()?; - Some((name, def, attr.span())) + let target = self.parse_single_path_attr(attr).ok()?; + Some(target.def().to_owned()) }) .collect() } @@ -243,28 +224,10 @@ impl<'tcx> KaniAttributes<'tcx> { /// the span in the span for the attribute (contents). /// /// In the case of an error, this function will emit the error and return `None`. - pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> { - self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { - let name = expect_key_string_value(self.tcx.sess, target).ok()?; - self.resolve_from_mod(name.as_str()) - .map(|ok| (name, ok, target.span())) - .map_err(|resolve_err| { - let mut err = self.tcx.dcx().struct_span_err( - target.span(), - format!( - "Failed to resolve checking function {} because {resolve_err}", - name.as_str() - ), - ); - if let ResolveError::AmbiguousPartialPath { .. } = resolve_err { - err = err.with_help(format!( - "Replace {} with a specific implementation.", - name.as_str() - )); - } - err.emit(); - }) - .ok() + pub(crate) fn interpret_for_contract_attribute(&self) -> Option { + self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|attr| { + let target = self.parse_single_path_attr(attr).ok()?; + Some(target.def().to_owned()) }) } @@ -331,15 +294,6 @@ impl<'tcx> KaniAttributes<'tcx> { self.map.contains_key(&KaniAttributeKind::CheckedWith) } - /// Resolve a path starting from this item's module context. - fn resolve_from_mod(&self, path_str: &str) -> Result> { - resolve_fn( - self.tcx, - self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), - path_str, - ) - } - /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. @@ -375,7 +329,7 @@ impl<'tcx> KaniAttributes<'tcx> { }) } KaniAttributeKind::Stub => { - parse_stubs(self.tcx, self.item, attrs); + self.parse_stubs(attrs); } KaniAttributeKind::Unwind => { expect_single(self.tcx, kind, attrs); @@ -402,10 +356,15 @@ impl<'tcx> KaniAttributes<'tcx> { ); } expect_single(self.tcx, kind, attrs); - attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) + attrs.iter().for_each(|attr| { + self.check_proof_attribute(kind, attr); + let _ = self.parse_single_path_attr(attr); + }) } KaniAttributeKind::StubVerified => { - self.check_stub_verified(); + attrs.iter().for_each(|attr| { + self.check_stub_verified(attr); + }); } KaniAttributeKind::FnMarker | KaniAttributeKind::CheckedWith @@ -511,15 +470,23 @@ impl<'tcx> KaniAttributes<'tcx> { /// is reachable and emit an error if it isn't. /// This is different from the earlier `check_attributes` call: /// that checks that the specified target exists, but not if we can reach that target from the harness. - pub fn check_proof_for_contract_reachability(&self, reachable_functions: &HashSet) { - if let Some((symbol, function, span)) = self.interpret_for_contract_attribute() - && !reachable_functions.contains(&function) + pub fn check_proof_for_contract_reachability( + &self, + reachable_functions: &HashSet, + ) { + if let Some(def) = self.interpret_for_contract_attribute() + && !reachable_functions.contains(&def.def_id()) { - let err_msg = format!( - "The function specified in the `proof_for_contract` attribute, `{symbol}`, was not found.\ - \nMake sure the function is reachable from the harness." - ); - self.tcx.dcx().span_err(span, err_msg); + let item_name = self.item_name(); + let target_name = def.trimmed_name(); + self.tcx.dcx().struct_span_err( + self.tcx.def_span(self.item), + format!( + "The function specified in the `proof_for_contract` attribute, `{target_name}`, is not reachable from the harness `{item_name}`.", + ) + ) + .with_help(format!("Make sure that `{item_name}` calls `{target_name}`")) + .emit(); } } @@ -549,13 +516,13 @@ impl<'tcx> KaniAttributes<'tcx> { harness.solver = parse_solver(self.tcx, attributes[0]); } KaniAttributeKind::Stub => { - harness.stubs.extend_from_slice(&parse_stubs(self.tcx, self.item, attributes)); + harness.stubs.extend_from_slice(&self.parse_stubs(attributes)); } KaniAttributeKind::Unwind => { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } KaniAttributeKind::Proof => { /* no-op */ } - KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness), + KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(attributes[0]), KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness), KaniAttributeKind::Unstable => { // Internal attribute which shouldn't exist here. @@ -582,61 +549,66 @@ impl<'tcx> KaniAttributes<'tcx> { }) } - fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) { - let dcx = self.tcx.dcx(); - let (name, id, span) = match self.interpret_for_contract_attribute() { + fn handle_proof_for_contract(&self, attr: &Attribute) { + let target_def = match self.interpret_for_contract_attribute() { None => return, // This error was already emitted - Some(values) => values, + Some(def) => def, }; - assert!(matches!( - &harness.kind, HarnessKind::ProofForContract { target_fn } - if *target_fn == name.to_string())); - if KaniAttributes::for_item(self.tcx, id).contract_attributes().is_none() { - dcx.struct_span_err( - span, - format!( - "Failed to check contract: Function `{}` has no contract.", - self.item_name(), - ), - ) - .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.") - .emit(); + let target_attributes = KaniAttributes::for_def_id(self.tcx, target_def.def_id()); + if target_attributes.contract_attributes().is_none() { + self.tcx + .dcx() + .struct_span_err( + attr.span(), + format!( + "Failed to check contract: `{}` has no contract.", + target_attributes.item_name(), + ), + ) + .with_span_note( + rustc_internal::internal(self.tcx, target_def.span()), + "Try adding a contract to this function.", + ) + .emit(); } } - fn check_stub_verified(&self) { + fn check_stub_verified(&self, attr: &Attribute) { let dcx = self.tcx.dcx(); let mut seen = HashSet::new(); - for (name, def_id, span) in self.interpret_stub_verified_attribute() { - if seen.contains(&name) { + for stub_target in self.interpret_stub_verified_attribute() { + if seen.contains(&stub_target) { dcx.struct_span_warn( - span, - format!("Multiple occurrences of `stub_verified({name})`."), - ) - .with_span_note( - self.tcx.def_span(def_id), - format!("Use a single `stub_verified({name})` annotation."), + rustc_internal::internal(self.tcx, stub_target.span()), + format!( + "Multiple occurrences of `stub_verified({})`.", + stub_target.trimmed_name() + ), ) + .with_help("Use a single annotation instead.") .emit(); } else { - seen.insert(name); + seen.insert(stub_target); } - if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() { + if KaniAttributes::for_def_id(self.tcx, stub_target.def_id()) + .contract_attributes() + .is_none() + { dcx.struct_span_err( - span, + attr.span(), format!( - "Target function in `stub_verified({name})` has no contract.", + "Target function in stub_verified, `{}`, has no contract.", + stub_target.trimmed_name() ), ) .with_span_note( - self.tcx.def_span(def_id), + rustc_internal::internal(self.tcx, stub_target.span()), format!( "Try adding a contract to this function or use the unsound `{}` attribute instead.", KaniAttributeKind::Stub.as_ref(), ), ) .emit(); - return; } } } @@ -647,8 +619,8 @@ impl<'tcx> KaniAttributes<'tcx> { /// the target names are known and have contracts, and there are no /// duplicate target names. fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { - for (name, _, _) in self.interpret_stub_verified_attribute() { - harness.verified_stubs.push(name.to_string()) + for stub in self.interpret_stub_verified_attribute() { + harness.verified_stubs.push(stub.name()) } } @@ -688,6 +660,98 @@ impl<'tcx> KaniAttributes<'tcx> { } } } + + fn resolve_path( + &self, + current_module: LocalDefId, + path: &TypePath, + span: Span, + ) -> Result> { + let result = resolve_fn_path(self.tcx, current_module, path); + + if let Err(ref resolve_err) = result { + let mut err = self.tcx.dcx().struct_span_err( + span, + format!("failed to resolve `{}`: {resolve_err}", pretty_type_path(path)), + ); + if let ResolveError::AmbiguousPartialPath { .. } = resolve_err { + err = err.with_help(format!( + "replace `{}` with a specific implementation.", + pretty_type_path(path) + )); + } + err.emit(); + } + + result + } + + /// Parse an attribute of the form #[kanitool::key = value], where value is the path to a function. + fn parse_single_path_attr( + &self, + attr: &'tcx Attribute, + ) -> Result> { + let current_module = + self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(); + let target = expect_key_string_value(self.tcx.sess, attr) + .unwrap_or_else(|_| panic!("malformed attribute")); + let target_str = target.as_str(); + let path = syn::parse_str(target_str).map_err(|err| ResolveError::InvalidPath { + msg: format!("Expected a path, but found `{target_str}`. {err}"), + }); + + match path { + Ok(path) => self.resolve_path(current_module, &path, attr.span()), + Err(err) => { + self.tcx.dcx().span_err(attr.span(), err.to_string()); + Err(err) + } + } + } + + fn parse_stubs(&self, attributes: &[&'tcx Attribute]) -> Vec { + let current_module = + self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(); + + attributes + .iter() + .filter_map(|attr| { + let paths = parse_paths(self.tcx, attr).unwrap_or_else(|_| { + self.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] => { + let _ = self.resolve_path(current_module, orig, attr.span()); + let _ = self.resolve_path(current_module, replace, attr.span()); + Some(Stub { + original: orig.to_token_stream().to_string(), + replacement: replace.to_token_stream().to_string(), + }) + } + [] => { + /* Error was already emitted */ + None + } + _ => { + self.tcx.dcx().span_err( + attr.span(), + format!( + "attribute `kani::stub` takes two path arguments; found {}", + paths.len() + ), + ); + None + } + } + }) + .collect() + } } /// An efficient check for the existence for a particular [`KaniAttributeKind`]. @@ -843,66 +907,6 @@ 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, 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| { - let paths = parse_paths(tcx, 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.to_token_stream().to_string(), - replacement: replace.to_token_stream().to_string(), - }) - } - [] => { - /* Error was already emitted */ - None - } - _ => { - tcx.dcx().span_err( - attr.span(), - format!( - "attribute `kani::stub` takes two path arguments; found {}", - paths.len() - ), - ); - None - } - } - }) - .collect() -} - fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { // TODO: Argument validation should be done as part of the `kani_macros` crate // diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 9715d9976b61..872d7944dfd1 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -14,12 +14,11 @@ use crate::kani_middle::metadata::{ gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata, }; use crate::kani_middle::reachability::filter_crate_items; -use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; use kani_metadata::{ - ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind, - HarnessMetadata, KaniMetadata, + ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata, + KaniMetadata, }; use regex::RegexSet; use rustc_hir::def_id::DefId; @@ -198,7 +197,7 @@ fn group_by_stubs( let mut per_stubs: HashMap<_, CodegenUnit> = HashMap::default(); for (harness, metadata) in all_harnesses { let stub_ids = harness_stub_map(tcx, *harness, metadata); - let contracts = extract_contracts(tcx, *harness, metadata); + let contracts = extract_contracts(tcx, *harness); let stub_map = stub_ids .iter() .map(|(k, v)| (tcx.def_path_hash(*k), tcx.def_path_hash(*v))) @@ -228,22 +227,15 @@ enum ContractUsage { /// /// Note that any error interpreting the result is emitted, but we delay aborting, so we emit as /// many errors as possible. -fn extract_contracts( - tcx: TyCtxt, - harness: Harness, - metadata: &HarnessMetadata, -) -> BTreeSet { +fn extract_contracts(tcx: TyCtxt, harness: Harness) -> BTreeSet { let def = harness.def; let mut result = BTreeSet::new(); - if let HarnessKind::ProofForContract { target_fn } = &metadata.attributes.kind - && let Ok(check_def) = expect_resolve_fn(tcx, def, target_fn, "proof_for_contract") - { - result.insert(ContractUsage::Check(check_def.def_id().to_index())); + let attributes = KaniAttributes::for_def_id(tcx, def.def_id()); + if let Some(target) = attributes.interpret_for_contract_attribute() { + result.insert(ContractUsage::Check(target.def_id().to_index())); } - - for stub in &metadata.attributes.verified_stubs { - let Ok(stub_def) = expect_resolve_fn(tcx, def, stub, "stub_verified") else { continue }; - result.insert(ContractUsage::Stub(stub_def.def_id().to_index())); + for stub in attributes.interpret_stub_verified_attribute() { + result.insert(ContractUsage::Stub(stub.def_id().to_index())); } result diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index f4f0a99517d4..6fcbca7477e3 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -6,9 +6,8 @@ use std::collections::HashMap; use std::path::Path; -use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::Harness; -use crate::kani_middle::{SourceLocation, stable_fn_def}; +use crate::kani_middle::{KaniAttributes, SourceLocation}; use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; @@ -66,11 +65,8 @@ pub fn gen_contracts_metadata( fn_to_data .insert(item.def_id(), ContractedFunction { function, file, harnesses: vec![] }); // This logic finds manual contract harnesses only (automatic harnesses are a Kani intrinsic, not crate items annotated with the proof_for_contract attribute). - } else if let Some((_, internal_def_id, _)) = attributes.interpret_for_contract_attribute() - { - let target_def_id = stable_fn_def(tcx, internal_def_id) - .expect("The target of a proof for contract should be a function definition") - .def_id(); + } else if let Some(def) = attributes.interpret_for_contract_attribute() { + let target_def_id = def.def_id(); if let Some(cf) = fn_to_data.get_mut(&target_def_id) { cf.harnesses.push(function); } else { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index adb76ed8b61e..41ebb03e70fa 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -94,10 +94,10 @@ impl TyVisitor for FindUnsafeCell<'_> { pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); - let reachable_functions: HashSet = items + let reachable_functions: HashSet = items .iter() .filter_map(|i| match i { - MonoItem::Fn(instance) => Some(rustc_internal::internal(tcx, instance.def.def_id())), + MonoItem::Fn(instance) => Some(instance.def.def_id()), _ => None, }) .collect(); diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 865a96d408e4..f94913b327ff 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -12,7 +12,6 @@ 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::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModDefId}; use rustc_hir::{ItemKind, UseKind}; @@ -47,6 +46,15 @@ pub enum FnResolution { FnImpl { def: FnDef, ty: Ty }, } +impl FnResolution { + pub fn def(&self) -> FnDef { + match self { + Self::Fn(def) => *def, + Self::FnImpl { def, .. } => *def, + } + } +} + /// Resolve a path to a function / method. /// /// The path can either be a simple path or a qualified path. @@ -110,33 +118,6 @@ pub fn resolve_fn<'tcx>( } } -/// Resolve the name of a function from the context of the definition provided. -/// -/// Ideally this should pass a more precise span, but we don't keep them around. -pub fn expect_resolve_fn( - tcx: TyCtxt, - res_cx: T, - name: &str, - reason: &str, -) -> Result { - let internal_def_id = rustc_internal::internal(tcx, res_cx.def_id()); - let current_module = tcx.parent_module_from_def_id(internal_def_id.as_local().unwrap()); - let maybe_resolved = resolve_fn(tcx, current_module.to_local_def_id(), name); - let resolved = maybe_resolved.map_err(|err| { - tcx.dcx().span_err( - rustc_internal::internal(tcx, res_cx.span()), - format!("Failed to resolve `{name}` for `{reason}`: {err}"), - ) - })?; - let ty_internal = tcx.type_of(resolved).instantiate_identity(); - let ty = rustc_internal::stable(ty_internal); - if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = ty.kind() { - Ok(def) - } else { - unreachable!("Expected function for `{name}`, but found: {ty}") - } -} - /// 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. diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index e3ca9a53c66b..91ecbf70a9a2 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -9,7 +9,6 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceIns use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; -use rustc_hir::def_id::DefId as InternalDefId; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use rustc_span::Symbol; @@ -271,9 +270,9 @@ impl AnyModifiesPass { #[derive(Debug, Default)] pub struct FunctionWithContractPass { /// Function that is being checked, if any. - check_fn: Option, + check_fn: Option, /// Functions that should be stubbed by their contract. - replace_fns: HashSet, + replace_fns: HashSet, /// Should we interpret contracts as assertions? (true iff the no-assert-contracts option is not passed) assert_contracts: bool, /// Functions annotated with contract attributes will contain contract closures even if they @@ -353,19 +352,12 @@ impl FunctionWithContractPass { let (fn_to_verify_def, _) = kind.fn_def().unwrap(); // For automatic harnesses, the target is the function to verify, // and stubs are empty. - ( - Some(rustc_internal::internal(tcx, fn_to_verify_def.def_id())), - HashSet::default(), - ) + (Some(fn_to_verify_def), HashSet::default()) } else { let attrs = KaniAttributes::for_instance(tcx, *harness); - let check_fn = - attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); - let replace_fns: HashSet<_> = attrs - .interpret_stub_verified_attribute() - .iter() - .map(|(_, def_id, _)| *def_id) - .collect(); + let check_fn = attrs.interpret_for_contract_attribute(); + let replace_fns: HashSet<_> = + attrs.interpret_stub_verified_attribute().into_iter().collect(); (check_fn, replace_fns) } }; @@ -470,14 +462,13 @@ impl FunctionWithContractPass { fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option { let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id()); kani_attributes.has_contract().then(|| { - let fn_def_id = rustc_internal::internal(tcx, fn_def.def_id()); - if self.check_fn == Some(fn_def_id) { + if self.check_fn == Some(fn_def) { if kani_attributes.has_recursion() { ContractMode::RecursiveCheck } else { ContractMode::SimpleCheck } - } else if self.replace_fns.contains(&fn_def_id) { + } else if self.replace_fns.contains(&fn_def) { ContractMode::Replace } else if self.assert_contracts { ContractMode::Assert diff --git a/tests/expected/function-contract/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected index 6836fb06f0a6..f3235c4460da 100644 --- a/tests/expected/function-contract/missing_contract_for_check.expected +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -1,4 +1,4 @@ -error: Failed to check contract: Function `harness` has no contract. +error: Failed to check contract: `no_contract` has no contract. | 7 | #[kani::proof_for_contract(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected index 198838feca03..1c42b8186295 100644 --- a/tests/expected/function-contract/missing_contract_for_replace.expected +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -1,4 +1,4 @@ -error: Target function in `stub_verified(no_contract)` has no contract. +error: Target function in stub_verified, `no_contract`, has no contract. | 8 | #[kani::stub_verified(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/expected/stubbing-ambiguous-path/expected b/tests/expected/stubbing-ambiguous-path/expected index 387fee15b3f0..b46f367c25d1 100644 --- a/tests/expected/stubbing-ambiguous-path/expected +++ b/tests/expected/stubbing-ambiguous-path/expected @@ -1,3 +1,7 @@ -error: failed to resolve `foo`: `foo` is ambiguous because of multiple glob imports in module `main`. Found:\ -mod2::foo\ -mod1::foo\ +error: failed to resolve `foo`: `foo` is ambiguous because of multiple glob imports in module `main`. Found: + mod2::foo\ + mod1::foo +| +| #[kani::stub(foo, stub)] +| ^^^^^^^^^^^^^^^^^^^^^^^^ +| diff --git a/tests/ui/function-contracts/invalid_target_path.expected b/tests/ui/function-contracts/invalid_target_path.expected index bdf28539002c..d1478aed5f9b 100644 --- a/tests/ui/function-contracts/invalid_target_path.expected +++ b/tests/ui/function-contracts/invalid_target_path.expected @@ -1,15 +1,17 @@ -Failed to resolve checking function NonZero::::unchecked_mul because the generic arguments :: are invalid. The available implementations are: - NonZero::::unchecked_mul - NonZero::::unchecked_mul +error: failed to resolve `NonZero :: < g32 >::unchecked_mul`: the generic arguments :: are invalid. The available implementations are:\ + NonZero::::unchecked_mul\ + NonZero::::unchecked_mul\ +invalid_target_path.rs\ | | #[kani::proof_for_contract(NonZero::::unchecked_mul)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Failed to resolve checking function NonZero::unchecked_mul because there are multiple implementations of unchecked_mul in struct `NonZero`. Found: - NonZero::::unchecked_mul - NonZero::::unchecked_mul +error: failed to resolve `NonZero::unchecked_mul`: there are multiple implementations of unchecked_mul in struct `NonZero`. Found:\ + NonZero::::unchecked_mul\ + NonZero::::unchecked_mul\ +invalid_target_path.rs\ | | #[kani::proof_for_contract(NonZero::unchecked_mul)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | - = help: Replace NonZero::unchecked_mul with a specific implementation. + = help: replace `NonZero::unchecked_mul` with a specific implementation. diff --git a/tests/ui/function-stubbing-error/unsupported_resolutions.expected b/tests/ui/function-stubbing-error/unsupported_resolutions.expected index e723ac97813d..f8ed4b0c526b 100644 --- a/tests/ui/function-stubbing-error/unsupported_resolutions.expected +++ b/tests/ui/function-stubbing-error/unsupported_resolutions.expected @@ -1,4 +1,3 @@ -error: Kani currently does not support stubbing trait implementations. error: failed to resolve `::bar`: unable to find `bar` inside trait `Foo` -error: aborting due to 4 previous errors +error: aborting due to 1 previous error diff --git a/tests/ui/stubbing/invalid-path/invalid_inherent_impls.expected b/tests/ui/stubbing/invalid-path/invalid_inherent_impls.expected index f050072530f7..ebb082d250e4 100644 --- a/tests/ui/stubbing/invalid-path/invalid_inherent_impls.expected +++ b/tests/ui/stubbing/invalid-path/invalid_inherent_impls.expected @@ -1,17 +1,17 @@ -error: Failed to resolve replacement function NonZero::unchecked_mul: there are multiple implementations of unchecked_mul in struct `NonZero`. Found: - NonZero::::unchecked_mul - NonZero::::unchecked_mul -invalid_inherent_impls.rs +error: failed to resolve `NonZero::unchecked_mul`: there are multiple implementations of unchecked_mul in struct `NonZero`. Found:\ + NonZero::::unchecked_mul\ + NonZero::::unchecked_mul\ +invalid_inherent_impls.rs\ | | #[kani::stub_verified(NonZero::unchecked_mul)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | - = help: Replace NonZero::unchecked_mul with a specific implementation. + = help: replace `NonZero::unchecked_mul` with a specific implementation. -error: Failed to resolve replacement function NonZero::::unchecked_mul: the generic arguments :: are invalid. The available implementations are: - NonZero::::unchecked_mul - NonZero::::unchecked_mul -invalid_inherent_impls.rs +error: failed to resolve `NonZero :: < g32 >::unchecked_mul`: the generic arguments :: are invalid. The available implementations are:\ + NonZero::::unchecked_mul\ + NonZero::::unchecked_mul\ +invalid_inherent_impls.rs\ | | #[kani::stub_verified(NonZero::::unchecked_mul)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/ui/unknown-contract-harness/expected b/tests/ui/unknown-contract-harness/expected index dec02f9b0a50..d474678d1460 100644 --- a/tests/ui/unknown-contract-harness/expected +++ b/tests/ui/unknown-contract-harness/expected @@ -1,6 +1,7 @@ -error: The function specified in the `proof_for_contract` attribute, `foo`, was not found.\ -Make sure the function is reachable from the harness. +error: The function specified in the `proof_for_contract` attribute, `foo`, is not reachable from the harness `check_foo`.\ test.rs:\ -|\ -| #[kani::proof_for_contract(foo)]\ +| +| fn check_foo() { | ^^^^^^^^^^^^^^ +| += help: Make sure that `check_foo` calls `foo`