diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6ee5136e12e5..9baebe562227 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -43,60 +43,206 @@ impl KaniAttributeKind { } } -/// 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. -pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) { - let attributes = extract_kani_attributes(tcx, def_id); - - // Check that all attributes are correctly used and well formed. - let is_harness = attributes.contains_key(&KaniAttributeKind::Proof); - for (kind, attrs) in attributes { - if !is_harness && kind.is_harness_only() { - tcx.sess.span_err( - attrs[0].span, - format!( - "the `{}` attribute also requires the `#[kani::proof]` attribute", - kind.as_ref() - ), - ); - } - match kind { - KaniAttributeKind::ShouldPanic => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| { - expect_no_args(tcx, kind, attr); - }) - } - KaniAttributeKind::Solver => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| { - parse_solver(tcx, attr); - }) +/// Bundles together common data used when evaluating the attributes of a given +/// function. +#[derive(Clone)] +pub struct KaniAttributes<'tcx> { + /// Rustc type context/queries + tcx: TyCtxt<'tcx>, + /// The function which these attributes decorate. + item: DefId, + /// All attributes we found in raw format. + map: BTreeMap>, +} + +impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("KaniAttributes") + .field("item", &self.tcx.def_path_debug_str(self.item)) + .field("map", &self.map) + .finish() + } +} + +impl<'tcx> KaniAttributes<'tcx> { + /// Perform preliminary parsing and checking for the attributes on this + /// function + pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self { + let all_attributes = tcx.get_attrs_unchecked(def_id); + let map = all_attributes.iter().fold( + >>::default(), + |mut result, attribute| { + // Get the string the appears after "kanitool::" in each attribute string. + // Ex - "proof" | "unwind" etc. + if let Some(kind) = attr_kind(tcx, attribute) { + result.entry(kind).or_default().push(attribute) + } + result + }, + ); + Self { map, tcx, item: def_id } + } + + /// 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. + pub(super) fn check_attributes(&self) { + // Check that all attributes are correctly used and well formed. + let is_harness = self.is_harness(); + for (&kind, attrs) in self.map.iter() { + if !is_harness && kind.is_harness_only() { + self.tcx.sess.span_err( + attrs[0].span, + format!( + "the `{}` attribute also requires the `#[kani::proof]` attribute", + kind.as_ref() + ), + ); } - KaniAttributeKind::Stub => { - parse_stubs(tcx, def_id, attrs); + match kind { + KaniAttributeKind::ShouldPanic => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| { + expect_no_args(self.tcx, kind, attr); + }) + } + KaniAttributeKind::Solver => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| { + parse_solver(self.tcx, attr); + }) + } + KaniAttributeKind::Stub => { + parse_stubs(self.tcx, self.item, attrs); + } + KaniAttributeKind::Unwind => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| { + parse_unwind(self.tcx, attr); + }) + } + KaniAttributeKind::Proof => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| self.check_proof_attribute(attr)) + } + KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { + let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx)); + }), } - KaniAttributeKind::Unwind => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| { - parse_unwind(tcx, attr); - }) + } + } + + /// Check that any unstable API has been enabled. Otherwise, emit an error. + /// + /// TODO: Improve error message by printing the span of the harness instead of the definition. + pub fn check_unstable_features(&self, enabled_features: &[String]) { + if !matches!(self.tcx.type_of(self.item).skip_binder().kind(), TyKind::FnDef(..)) { + // Skip closures since it shouldn't be possible to add an unstable attribute to them. + // We have to explicitly skip them though due to an issue with rustc: + // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 + return; + } + if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) { + for attr in unstable_attrs { + let unstable_attr = UnstableAttribute::try_from(*attr).unwrap(); + if !enabled_features.contains(&unstable_attr.feature) { + // Reached an unstable attribute that was not enabled. + self.report_unstable_forbidden(&unstable_attr); + } else { + debug!(enabled=?attr, def_id=?self.item, "check_unstable_features"); + } } - KaniAttributeKind::Proof => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| check_proof_attribute(tcx, def_id, attr)) + } + } + + /// Report misusage of an unstable feature that was not enabled. + fn report_unstable_forbidden(&self, unstable_attr: &UnstableAttribute) -> ErrorGuaranteed { + let fn_name = self.tcx.def_path_str(self.item); + self.tcx + .sess + .struct_err(format!( + "Use of unstable feature `{}`: {}", + unstable_attr.feature, unstable_attr.reason + )) + .span_note( + self.tcx.def_span(self.item), + format!("the function `{fn_name}` is unstable:"), + ) + .note(format!("see issue {} for more information", unstable_attr.issue)) + .help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature)) + .emit() + } + + /// Is this item a harness? (either `proof` or `proof_for_contract` + /// attribute are present) + fn is_harness(&self) -> bool { + self.map.get(&KaniAttributeKind::Proof).is_some() + } + + /// Extract harness attributes for a given `def_id`. + /// + /// We only extract attributes for harnesses that are local to the current crate. + /// Note that all attributes should be valid by now. + pub fn harness_attributes(&self) -> HarnessAttributes { + // Abort if not local. + assert!(self.item.is_local(), "Expected a local item, but got: {:?}", self.item); + trace!(?self, "extract_harness_attributes"); + assert!(self.is_harness()); + self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { + match kind { + KaniAttributeKind::ShouldPanic => harness.should_panic = true, + KaniAttributeKind::Solver => { + harness.solver = parse_solver(self.tcx, attributes[0]); + } + KaniAttributeKind::Stub => { + harness.stubs = parse_stubs(self.tcx, self.item, attributes); + } + KaniAttributeKind::Unwind => { + harness.unwind_value = parse_unwind(self.tcx, attributes[0]) + } + KaniAttributeKind::Proof => harness.proof = true, + KaniAttributeKind::Unstable => { + // Internal attribute which shouldn't exist here. + unreachable!() + } + }; + harness + }) + } + + /// Check that if this item is tagged with a proof_attribute, it is a valid harness. + fn check_proof_attribute(&self, proof_attribute: &Attribute) { + let span = proof_attribute.span; + let tcx = self.tcx; + expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute); + if tcx.def_kind(self.item) != DefKind::Fn { + tcx.sess.span_err(span, "the `proof` attribute can only be applied to functions"); + } else if tcx.generics_of(self.item).requires_monomorphization(tcx) { + tcx.sess.span_err(span, "the `proof` attribute cannot be applied to generic functions"); + } else { + let instance = Instance::mono(tcx, self.item); + if !super::fn_abi(tcx, instance).args.is_empty() { + tcx.sess.span_err(span, "functions used as harnesses cannot have any arguments"); } - KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { - let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(tcx)); - }), - }; + } } } +/// An efficient check for the existence for a particular [`KaniAttributeKind`]. +/// Unlike querying [`KaniAttributes`] this method builds no new heap data +/// structures and has short circuiting. +fn has_kani_attribute bool>( + tcx: TyCtxt, + def_id: DefId, + predicate: F, +) -> bool { + tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) +} + +/// Same as [`KaniAttributes::is_harness`] but more efficient because less +/// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool { - let attributes = extract_kani_attributes(tcx, def_id); - attributes.contains_key(&KaniAttributeKind::Proof) + has_kani_attribute(tcx, def_id, |a| matches!(a, KaniAttributeKind::Proof)) } /// Does this `def_id` have `#[rustc_test_marker]`? @@ -112,77 +258,6 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { parse_str_value(&marker).unwrap() } -/// Extract harness attributes for a given `def_id`. -/// -/// We only extract attributes for harnesses that are local to the current crate. -/// Note that all attributes should be valid by now. -pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttributes { - // Abort if not local. - assert!(def_id.is_local(), "Expected a local item, but got: {def_id:?}"); - let attributes = extract_kani_attributes(tcx, def_id); - trace!(?def_id, ?attributes, "extract_harness_attributes"); - assert!(attributes.contains_key(&KaniAttributeKind::Proof)); - attributes.into_iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { - match kind { - KaniAttributeKind::ShouldPanic => harness.should_panic = true, - KaniAttributeKind::Solver => { - harness.solver = parse_solver(tcx, attributes[0]); - } - KaniAttributeKind::Stub => { - harness.stubs = parse_stubs(tcx, def_id, attributes); - } - KaniAttributeKind::Unwind => harness.unwind_value = parse_unwind(tcx, attributes[0]), - KaniAttributeKind::Proof => harness.proof = true, - KaniAttributeKind::Unstable => { - // Internal attribute which shouldn't exist here. - unreachable!() - } - }; - harness - }) -} - -/// Check that any unstable API has been enabled. Otherwise, emit an error. -/// -/// TODO: Improve error message by printing the span of the harness instead of the definition. -pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) { - if !matches!(tcx.type_of(def_id).skip_binder().kind(), TyKind::FnDef(..)) { - // skip closures due to an issue with rustc. - // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 - return; - } - let attributes = extract_kani_attributes(tcx, def_id); - if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) { - for attr in unstable_attrs { - let unstable_attr = UnstableAttribute::try_from(*attr).unwrap(); - if !enabled_features.contains(&unstable_attr.feature) { - // Reached an unstable attribute that was not enabled. - report_unstable_forbidden(tcx, def_id, &unstable_attr); - } else { - debug!(enabled=?attr, ?def_id, "check_unstable_features"); - } - } - } -} - -/// Report misusage of an unstable feature that was not enabled. -fn report_unstable_forbidden( - tcx: TyCtxt, - def_id: DefId, - unstable_attr: &UnstableAttribute, -) -> ErrorGuaranteed { - let fn_name = tcx.def_path_str(def_id); - tcx.sess - .struct_err(format!( - "Use of unstable feature `{}`: {}", - unstable_attr.feature, unstable_attr.reason - )) - .span_note(tcx.def_span(def_id), format!("the function `{fn_name}` is unstable:")) - .note(format!("see issue {} for more information", unstable_attr.issue)) - .help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature)) - .emit() -} - fn expect_single<'a>( tcx: TyCtxt, kind: KaniAttributeKind, @@ -200,38 +275,6 @@ fn expect_single<'a>( attr } -/// Check that if an item is tagged with a proof_attribute, it is a valid harness. -fn check_proof_attribute(tcx: TyCtxt, def_id: DefId, proof_attribute: &Attribute) { - let span = proof_attribute.span; - expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute); - if tcx.def_kind(def_id) != DefKind::Fn { - tcx.sess.span_err(span, "the `proof` attribute can only be applied to functions"); - } else if tcx.generics_of(def_id).requires_monomorphization(tcx) { - tcx.sess.span_err(span, "the `proof` attribute cannot be applied to generic functions"); - } else { - let instance = Instance::mono(tcx, def_id); - if !super::fn_abi(tcx, instance).args.is_empty() { - tcx.sess.span_err(span, "functions used as harnesses cannot have any arguments"); - } - } -} - -/// Partition all the attributes according to their kind. -fn extract_kani_attributes( - tcx: TyCtxt, - def_id: DefId, -) -> BTreeMap> { - let all_attributes = tcx.get_attrs_unchecked(def_id); - all_attributes.iter().fold(BTreeMap::default(), |mut result, attribute| { - // Get the string the appears after "kanitool::" in each attribute string. - // Ex - "proof" | "unwind" etc. - if let Some(kind) = attr_kind(tcx, attribute) { - result.entry(kind).or_default().push(attribute) - } - result - }) -} - /// Attribute used to mark a Kani lib API unstable. #[derive(Debug)] struct UnstableAttribute { @@ -328,7 +371,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { } } -fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: Vec<&Attribute>) -> Vec { +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, name); diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 506779001689..fbf69c2d4fa4 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -10,11 +10,11 @@ use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata}; use rustc_hir::def_id::DefId; use rustc_middle::ty::{Instance, InstanceDef, TyCtxt}; -use super::{attributes::extract_harness_attributes, SourceLocation}; +use super::{attributes::KaniAttributes, SourceLocation}; /// Create the harness metadata for a proof harness for a given function. pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata { - let attributes = extract_harness_attributes(tcx, def_id); + let attributes = KaniAttributes::for_item(tcx, def_id).harness_attributes(); let pretty_name = tcx.def_path_str(def_id); // Main function a special case in order to support `--function main` // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index ba235db26805..04fc2b67e26f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -25,7 +25,7 @@ use std::fs::File; use std::io::BufWriter; use std::io::Write; -use self::attributes::{check_attributes, check_unstable_features}; +use self::attributes::KaniAttributes; pub mod analysis; pub mod attributes; @@ -43,7 +43,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { let krate = tcx.crate_name(LOCAL_CRATE); for item in tcx.hir_crate_items(()).items() { let def_id = item.owner_id.def_id.to_def_id(); - check_attributes(tcx, def_id); + KaniAttributes::for_item(tcx, def_id).check_attributes(); if tcx.def_kind(def_id) == DefKind::GlobalAsm { if !ignore_asm { let error_msg = format!( @@ -72,7 +72,8 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) let def_id = item.def_id(); if !def_ids.contains(&def_id) { // Check if any unstable attribute was reached. - check_unstable_features(tcx, &queries.unstable_features, def_id); + KaniAttributes::for_item(tcx, def_id) + .check_unstable_features(&queries.unstable_features); def_ids.insert(def_id); } }