diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 6a8137e1c744..735cd4671034 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -35,6 +35,7 @@ use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; use rustc_public::mir::mono::{Instance, MonoItem}; use rustc_public::rustc_internal; +use rustc_public::ty::FnDef; use rustc_public::{CrateDef, DefId}; use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; @@ -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 ebd20f0d53f1..f5b4dd4e85ed 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -37,6 +37,7 @@ use rustc_middle::util::Providers; use rustc_public::CrateDef; use rustc_public::mir::mono::{Instance, MonoItem}; use rustc_public::rustc_internal; +use rustc_public::ty::FnDef; use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; @@ -215,24 +216,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() } } } @@ -343,13 +343,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 ccd9607b329e..92b0b02bc52a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -8,12 +8,17 @@ 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, LocalDefId}, +}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_public::crate_def::Attribute as AttributeStable; use rustc_public::mir::mono::Instance as InstanceStable; use rustc_public::rustc_internal; -use rustc_public::{CrateDef, DefId as StableDefId, Symbol as SymbolStable}; +use rustc_public::ty::FnDef as FnDefStable; +use rustc_public::{CrateDef, DefId as DefIdStable, Symbol as SymbolStable}; use rustc_session::Session; use rustc_span::{Span, Symbol}; use std::str::FromStr; @@ -22,7 +27,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)] @@ -161,7 +166,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)) } @@ -203,33 +208,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 +229,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 +299,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 +334,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 +361,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 @@ -508,16 +472,26 @@ 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) { - if let Some((symbol, function, span)) = self.interpret_for_contract_attribute() - && !reachable_functions.contains(&function) + /// 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(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(); } } @@ -547,13 +521,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. @@ -580,61 +554,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; } } } @@ -645,8 +624,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()) } } @@ -686,6 +665,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`]. @@ -728,11 +799,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()) }); @@ -841,66 +912,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 36ae08f32127..3a0aa45ae090 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -14,14 +14,13 @@ 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_middle::{can_derive_arbitrary, implements_arbitrary}; use crate::kani_queries::QueryDb; use fxhash::{FxHashMap, FxHashSet}; use kani_metadata::{ - ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind, - HarnessMetadata, KaniMetadata, find_proof_harnesses, + ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata, + KaniMetadata, find_proof_harnesses, }; use regex::RegexSet; use rustc_hir::def_id::DefId; @@ -209,7 +208,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))) @@ -239,22 +238,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 e88d66da68ea..70917e20e678 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 3f19525c8dd7..e21b916e0a82 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -98,10 +98,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(); @@ -117,8 +117,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); } } diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 500b36bd5745..fb35b5fe996e 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 dbc248db8537..b0b4953ae4b9 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_public::CrateDef; use rustc_public::mir::mono::Instance; @@ -269,9 +268,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 @@ -351,19 +350,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) } }; @@ -468,14 +460,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`