Skip to content

Commit

Permalink
Simple Stubbing with Contracts (model-checking#2746)
Browse files Browse the repository at this point in the history 
### Description of changes: 

Expands the contract features introduced in model-checking#2655 by completing the
checking with stubbing/replacement capabilities.

### Resolved issues:

Resolves model-checking#2621 

### Related RFC: [0009 Function
Contracts](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>
  • Loading branch information
@JustusAdam @celinval @feliperodri
3 people authored Sep 27, 2023
1 parent 8480dc6 commit dba1674
Show file tree
Hide file tree
Showing 21 changed files with 1,225 additions and 257 deletions.
185 changes: 145 additions & 40 deletions kani-compiler/src/kani_middle/attributes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ use strum_macros::{AsRefStr, EnumString};

use tracing::{debug, trace};

use super::resolve::{self, resolve_fn};
use super::resolve::{self, resolve_fn, ResolveError};

#[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
#[strum(serialize_all = "snake_case")]
Expand All @@ -31,13 +31,20 @@ enum KaniAttributeKind {
/// Attribute used to mark unstable APIs.
Unstable,
Unwind,
/// A sound [`Self::Stub`] that replaces a function by a stub generated from
/// its contract.
StubVerified,
/// A harness, similar to [`Self::Proof`], but for checking a function
/// contract, e.g. the contract check is substituted for the target function
/// before the the verification runs.
ProofForContract,
/// Attribute on a function with a contract that identifies the code
/// implementing the check for this contract.
CheckedWith,
/// Internal attribute of the contracts implementation that identifies the
/// name of the function which was generated as the sound stub from the
/// contract of this function.
ReplacedWith,
/// Attribute on a function that was auto-generated from expanding a
/// function contract.
IsContractGenerated,
Expand All @@ -52,8 +59,10 @@ impl KaniAttributeKind {
| KaniAttributeKind::Solver
| KaniAttributeKind::Stub
| KaniAttributeKind::ProofForContract
| KaniAttributeKind::StubVerified
| KaniAttributeKind::Unwind => true,
KaniAttributeKind::Unstable
| KaniAttributeKind::ReplacedWith
| KaniAttributeKind::CheckedWith
| KaniAttributeKind::IsContractGenerated => false,
}
Expand Down Expand Up @@ -134,6 +143,30 @@ impl<'tcx> KaniAttributes<'tcx> {
}
}

/// Parse, extract and resolve the target of `stub_verified(TARGET)`. The
/// returned `Symbol` and `DefId` are respectively the name and id of
/// `TARGET`. The `Span` is that of the contents of the attribute and used
/// for error reporting.
fn interpret_stub_verified_attribute(
&self,
) -> Vec<Result<(Symbol, DefId, Span), ErrorGuaranteed>> {
self.map
.get(&KaniAttributeKind::StubVerified)
.map_or([].as_slice(), Vec::as_slice)
.iter()
.map(|attr| {
let name = expect_key_string_value(self.tcx.sess, attr)?;
let ok = self.resolve_sibling(name.as_str()).map_err(|e| {
self.tcx.sess.span_err(
attr.span,
format!("Failed to resolve replacement function {}: {e}", name.as_str()),
)
})?;
Ok((name, ok, attr.span))
})
.collect()
}

/// Parse and extract the `proof_for_contract(TARGET)` attribute. The
/// returned symbol and DefId are respectively the name and id of `TARGET`,
/// the span in the span for the attribute (contents).
Expand All @@ -142,30 +175,50 @@ impl<'tcx> KaniAttributes<'tcx> {
) -> Option<Result<(Symbol, DefId, Span), ErrorGuaranteed>> {
self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| {
let name = expect_key_string_value(self.tcx.sess, target)?;
let resolved = resolve_fn(
self.tcx,
self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(),
name.as_str(),
);
resolved.map(|ok| (name, ok, target.span)).map_err(|resolve_err| {
self.tcx.sess.span_err(
target.span,
format!(
"Failed to resolve replacement function {} because {resolve_err}",
name.as_str()
),
)
})
self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err(
|resolve_err| {
self.tcx.sess.span_err(
target.span,
format!(
"Failed to resolve checking function {} because {resolve_err}",
name.as_str()
),
)
},
)
})
}

/// Extract the name of the sibling function this contract is checked with
/// (if any).
/// Extract the name of the sibling function this function's contract is
/// checked with (if any).
///
/// `None` indicates this function does not use a contract, `Some(Err(_))`
/// indicates a contract does exist but an error occurred during resolution.
pub fn checked_with(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
self.expect_maybe_one(KaniAttributeKind::CheckedWith)
.map(|target| expect_key_string_value(self.tcx.sess, target))
}

/// Extract the name of the sibling function this function's contract is
/// stubbed as (if any).
///
/// `None` indicates this function does not use a contract, `Some(Err(_))`
/// indicates a contract does exist but an error occurred during resolution.
pub fn replaced_with(&self) -> Option<Result<Symbol, ErrorGuaranteed>> {
self.expect_maybe_one(KaniAttributeKind::ReplacedWith)
.map(|target| expect_key_string_value(self.tcx.sess, target))
}

/// Resolve a function that is known to reside in the same module as the one
/// these attributes belong to (`self.item`).
fn resolve_sibling(&self, path_str: &str) -> Result<DefId, ResolveError<'tcx>> {
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.
Expand Down Expand Up @@ -223,7 +276,10 @@ impl<'tcx> KaniAttributes<'tcx> {
}
expect_single(self.tcx, kind, &attrs);
}
KaniAttributeKind::CheckedWith => {
KaniAttributeKind::StubVerified => {
expect_single(self.tcx, kind, &attrs);
}
KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => {
self.expect_maybe_one(kind)
.map(|attr| expect_key_string_value(&self.tcx.sess, attr));
}
Expand Down Expand Up @@ -325,38 +381,87 @@ impl<'tcx> KaniAttributes<'tcx> {
harness.unwind_value = parse_unwind(self.tcx, attributes[0])
}
KaniAttributeKind::Proof => harness.proof = true,
KaniAttributeKind::ProofForContract => {
harness.proof = true;
let Some(Ok((name, id, span))) = self.interpret_the_for_contract_attribute()
else {
self.tcx.sess.span_err(
self.tcx.def_span(self.item),
format!("Invalid `{}` attribute format", kind.as_ref()),
);
return harness;
};
let Some(Ok(replacement_name)) =
KaniAttributes::for_item(self.tcx, id).checked_with()
else {
self.tcx
.sess
.span_err(span, "Target function for this check has no contract");
return harness;
};
harness.stubs.push(self.stub_for_relative_item(name, replacement_name));
}
KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness),
KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness),
KaniAttributeKind::Unstable => {
// Internal attribute which shouldn't exist here.
unreachable!()
}
KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => {
todo!("Contract attributes are not supported on proofs")
KaniAttributeKind::CheckedWith
| KaniAttributeKind::IsContractGenerated
| KaniAttributeKind::ReplacedWith => {
self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
}
};
harness
})
}

fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) {
let sess = self.tcx.sess;
let (name, id, span) = match self.interpret_the_for_contract_attribute() {
None => unreachable!(
"impossible, was asked to handle `proof_for_contract` but didn't find such an attribute."
),
Some(Err(_)) => return, // This error was already emitted
Some(Ok(values)) => values,
};
let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with()
else {
sess.struct_span_err(
span,
format!(
"Failed to check contract: Function `{}` has no contract.",
self.item_name(),
),
)
.span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
.emit();
return;
};
harness.stubs.push(self.stub_for_relative_item(name, replacement_name));
}

fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
let sess = self.tcx.sess;
for contract in self.interpret_stub_verified_attribute() {
let Ok((name, def_id, span)) = contract else {
// This error has already been emitted so we can ignore it now.
// Later the session will fail anyway so we can just
// optimistically forge on and try to find more errors.
continue;
};
let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with()
{
None => {
sess.struct_span_err(
span,
format!(
"Failed to generate verified stub: Function `{}` has no contract.",
self.item_name(),
),
)
.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();
continue;
}
Some(Ok(replacement_name)) => replacement_name,
Some(Err(_)) => continue,
};
harness.stubs.push(self.stub_for_relative_item(name, replacement_name))
}
}

fn item_name(&self) -> Symbol {
self.tcx.item_name(self.item)
}

/// 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;
Expand Down
Loading

0 comments on commit dba1674

Please sign in to comment.