From 2a95fe23bbaeafcb79cba5f6386f6ea60d3a9768 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 13:48:22 -0700 Subject: [PATCH] Add kind to harness metadata This allow us to get more information in the Kani driver about which kind of proof it is. For proof_for_contract, we can now check which function is the target. --- kani-compiler/src/kani_middle/attributes.rs | 45 ++++++++++--------- .../src/kani_middle/codegen_units.rs | 2 +- kani-compiler/src/kani_middle/metadata.rs | 4 +- kani-driver/src/metadata.rs | 16 ++++--- kani_metadata/src/harness.rs | 32 ++++++++++++- 5 files changed, 67 insertions(+), 32 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 9eb6d3d6ee4e..8c729bbdec9f 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -4,7 +4,7 @@ use std::collections::BTreeMap; -use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; +use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use rustc_ast::{ attr, token::Token, @@ -310,7 +310,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// 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(); + let is_harness = self.is_proof_harness(); for (&kind, attrs) in self.map.iter() { let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg); @@ -454,7 +454,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Is this item a harness? (either `proof` or `proof_for_contract` /// attribute are present) - fn is_harness(&self) -> bool { + fn is_proof_harness(&self) -> bool { self.map.contains_key(&KaniAttributeKind::Proof) || self.map.contains_key(&KaniAttributeKind::ProofForContract) } @@ -469,13 +469,18 @@ impl<'tcx> KaniAttributes<'tcx> { panic!("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)| { + assert!(self.is_proof_harness()); + let harness_attrs = if let Some(Ok(harness)) = self.proof_for_contract() { + HarnessAttributes::new(HarnessKind::ProofForContract { target_fn: harness.to_string() }) + } else { + HarnessAttributes::new(HarnessKind::Proof) + }; + self.map.iter().fold(harness_attrs, |mut harness, (kind, attributes)| { match kind { KaniAttributeKind::ShouldPanic => harness.should_panic = true, KaniAttributeKind::Recursion => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), "The attribute `kani::recursion` should only be used in combination with function contracts."); - }, + } KaniAttributeKind::Solver => { harness.solver = parse_solver(self.tcx, attributes[0]); } @@ -485,7 +490,7 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::Unwind => { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } - KaniAttributeKind::Proof => harness.proof = true, + KaniAttributeKind::Proof => { /* no-op */ } KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness), KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness), KaniAttributeKind::Unstable => { @@ -498,7 +503,7 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::InnerCheck | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); - }, + } KaniAttributeKind::DisableChecks => { // Internal attribute which shouldn't exist here. unreachable!() @@ -552,14 +557,14 @@ impl<'tcx> KaniAttributes<'tcx> { self.item_name(), ), ) - .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(), + .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(); + .emit(); continue; } Some(Ok(replacement_name)) => replacement_name, @@ -689,7 +694,7 @@ fn has_kani_attribute 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 +/// Same as [`KaniAttributes::is_proof_harness`] but more efficient because less /// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { let def_id = rustc_internal::internal(tcx, instance.def.def_id()); @@ -896,7 +901,7 @@ 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", + "attribute `kani::stub` takes two path arguments; found argument that is not a path", ); None } @@ -910,9 +915,9 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { const ATTRIBUTE: &str = "#[kani::solver]"; let invalid_arg_err = |attr: &Attribute| { tcx.dcx().span_err( - attr.span, - format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)") - ) + attr.span, + format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)"), + ) }; let attr_args = attr.meta_item_list().unwrap(); diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 260b363a868a..3f88ad2ecd3b 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -104,7 +104,7 @@ impl CodegenUnits { /// Generate [KaniMetadata] for the target crate. fn generate_metadata(&self) -> KaniMetadata { let (proof_harnesses, test_harnesses) = - self.harness_info.values().cloned().partition(|md| md.attributes.proof); + self.harness_info.values().cloned().partition(|md| md.attributes.is_proof()); KaniMetadata { crate_name: self.crate_info.name.clone(), proof_harnesses, diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index c00f38be4cb0..2f0f22d49e1c 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -6,7 +6,7 @@ use std::path::Path; use crate::kani_middle::attributes::test_harness_name; -use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata}; +use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::CrateDef; @@ -61,7 +61,7 @@ pub fn gen_test_metadata( original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, - attributes: HarnessAttributes::default(), + attributes: HarnessAttributes::new(HarnessKind::Test), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), contract: Default::default(), diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index cd916358d92e..3f9cd8f2bf84 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -200,7 +200,7 @@ fn find_proof_harnesses<'a>( #[cfg(test)] pub mod tests { use super::*; - use kani_metadata::HarnessAttributes; + use kani_metadata::{HarnessAttributes, HarnessKind}; use std::path::PathBuf; pub fn mock_proof_harness( @@ -209,6 +209,8 @@ pub mod tests { krate: Option<&str>, model_file: Option, ) -> HarnessMetadata { + let mut attributes = HarnessAttributes::new(HarnessKind::Proof); + attributes.unwind_value = unwind_value; HarnessMetadata { pretty_name: name.into(), mangled_name: name.into(), @@ -216,7 +218,7 @@ pub mod tests { original_file: "".into(), original_start_line: 0, original_end_line: 0, - attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, + attributes, goto_file: model_file, contract: Default::default(), } @@ -236,7 +238,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_three".to_string()]), &ref_harnesses, - false + false, ) .len(), 1 @@ -245,7 +247,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_two".to_string()]), &ref_harnesses, - false + false, ) .first() .unwrap() @@ -256,7 +258,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_one".to_string()]), &ref_harnesses, - false + false, ) .first() .unwrap() @@ -280,7 +282,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_three".to_string()]), &ref_harnesses, - true + true, ) .is_empty() ); @@ -299,7 +301,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"module::not_check_three".to_string()]), &ref_harnesses, - true + true, ) .first() .unwrap() diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 3dd6c82ebd39..5ae16aae7a33 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -38,10 +38,10 @@ pub struct HarnessMetadata { } /// The attributes added by the user to control how a harness is executed. -#[derive(Debug, Clone, Serialize, Deserialize, Default, PartialEq)] +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct HarnessAttributes { /// Whether the harness has been annotated with proof. - pub proof: bool, + pub kind: HarnessKind, /// Whether the harness is expected to panic or not. pub should_panic: bool, /// Optional data to store solver. @@ -52,6 +52,34 @@ pub struct HarnessAttributes { pub stubs: Vec, } +#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)] +pub enum HarnessKind { + /// Function was annotated with `#[kani::proof]`. + Proof, + /// Function was annotated with `#[kani::proof_for_contract(target_fn)]`. + ProofForContract { target_fn: String }, + /// This is a test harness annotated with `#[test]`. + Test, +} + +impl HarnessAttributes { + /// Create a new harness with of the provided kind. + pub fn new(kind: HarnessKind) -> HarnessAttributes { + HarnessAttributes { + kind, + should_panic: false, + solver: None, + unwind_value: None, + stubs: vec![], + } + } + + /// Return whether this is a proof harness. + pub fn is_proof(&self) -> bool { + matches!(self.kind, HarnessKind::Proof | HarnessKind::ProofForContract { .. }) + } +} + /// The stubbing type. #[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct Stub {