Skip to content

Commit

Permalink
Add kind to harness metadata
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@celinval
celinval committed Jul 26, 2024
1 parent b18698f commit 2a95fe2
Show file tree
Hide file tree
Showing 5 changed files with 67 additions and 32 deletions.
45 changes: 25 additions & 20 deletions kani-compiler/src/kani_middle/attributes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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)
}
Expand All @@ -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]);
}
Expand All @@ -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 => {
Expand All @@ -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!()
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -689,7 +694,7 @@ fn has_kani_attribute<F: Fn(KaniAttributeKind) -> 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());
Expand Down Expand Up @@ -896,7 +901,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
Err(error_span) => {
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
}
Expand All @@ -910,9 +915,9 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
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=\"<SAT_SOLVER_BINARY>\"`)")
)
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=\"<SAT_SOLVER_BINARY>\"`)"),
)
};

let attr_args = attr.meta_item_list().unwrap();
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/codegen_units.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/metadata.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(),
Expand Down
16 changes: 9 additions & 7 deletions kani-driver/src/metadata.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -209,14 +209,16 @@ pub mod tests {
krate: Option<&str>,
model_file: Option<PathBuf>,
) -> HarnessMetadata {
let mut attributes = HarnessAttributes::new(HarnessKind::Proof);
attributes.unwind_value = unwind_value;
HarnessMetadata {
pretty_name: name.into(),
mangled_name: name.into(),
crate_name: krate.unwrap_or("<unknown>").into(),
original_file: "<unknown>".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(),
}
Expand All @@ -236,7 +238,7 @@ pub mod tests {
find_proof_harnesses(
&BTreeSet::from([&"check_three".to_string()]),
&ref_harnesses,
false
false,
)
.len(),
1
Expand All @@ -245,7 +247,7 @@ pub mod tests {
find_proof_harnesses(
&BTreeSet::from([&"check_two".to_string()]),
&ref_harnesses,
false
false,
)
.first()
.unwrap()
Expand All @@ -256,7 +258,7 @@ pub mod tests {
find_proof_harnesses(
&BTreeSet::from([&"check_one".to_string()]),
&ref_harnesses,
false
false,
)
.first()
.unwrap()
Expand All @@ -280,7 +282,7 @@ pub mod tests {
find_proof_harnesses(
&BTreeSet::from([&"check_three".to_string()]),
&ref_harnesses,
true
true,
)
.is_empty()
);
Expand All @@ -299,7 +301,7 @@ pub mod tests {
find_proof_harnesses(
&BTreeSet::from([&"module::not_check_three".to_string()]),
&ref_harnesses,
true
true,
)
.first()
.unwrap()
Expand Down
32 changes: 30 additions & 2 deletions kani_metadata/src/harness.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -52,6 +52,34 @@ pub struct HarnessAttributes {
pub stubs: Vec<Stub>,
}

#[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 {
Expand Down

0 comments on commit 2a95fe2

Please sign in to comment.