Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Function Contracts: Support for defining and checking requires and ensures clauses #2655

Merged
merged 41 commits into from
Sep 7, 2023
Merged
Show file tree
Hide file tree
Changes from 37 commits
Commits
Show all changes
41 commits
Select commit Hold shift + click to select a range
32b37f3
Everything needed for requires/ensures checking
JustusAdam Aug 3, 2023
a2535d7
Formatting
JustusAdam Aug 3, 2023
624f406
The only clippy suggestion 🙌🏻
JustusAdam Aug 3, 2023
5a4ad83
Adjust test case
JustusAdam Aug 3, 2023
a272350
Seriously?
JustusAdam Aug 3, 2023
f0a011b
A check for mutable pointers
JustusAdam Aug 3, 2023
1429564
Whoops
JustusAdam Aug 3, 2023
1dd96dc
Last minute pivot in check function implementation
JustusAdam Aug 4, 2023
78739d8
Postcondition injection on every return
JustusAdam Aug 4, 2023
81cd5c8
Whoops
JustusAdam Aug 4, 2023
e07eec9
Documentation and emit block in injector
JustusAdam Aug 4, 2023
9b2d9a0
Incorporate more sysroot comments.
JustusAdam Aug 4, 2023
01dfbc0
More comments addressed
JustusAdam Aug 4, 2023
16b9cc5
Whitespace
JustusAdam Aug 4, 2023
5ee744c
Reverting proc macro refactoring
JustusAdam Aug 9, 2023
665b271
Merge remote-tracking branch 'fork/main' into simple-contacts-checking
JustusAdam Aug 10, 2023
fe71b62
Apply suggestions from code review
JustusAdam Aug 10, 2023
387280f
Reformatting tests after celina's feeback
JustusAdam Aug 10, 2023
a8f0929
Rename harnesses
JustusAdam Aug 10, 2023
ac73461
Remove enum map dependency
JustusAdam Aug 10, 2023
e558226
Lots of docuemntation expansion and a few fixes
JustusAdam Aug 10, 2023
ba84599
Yes I didn't need this
JustusAdam Aug 10, 2023
c8b137c
Update library/kani/src/lib.rs
JustusAdam Aug 16, 2023
d53a5a8
Add documentation for attribute enum and remove unused attribute
JustusAdam Aug 16, 2023
b81c45a
Adding requested changes
JustusAdam Aug 16, 2023
6aa6b22
Remove unused compiler flag
JustusAdam Aug 16, 2023
4c475b6
Expand test case
JustusAdam Aug 16, 2023
71711a0
An unused collect
JustusAdam Aug 16, 2023
98ccfa5
Split pointer prohibition tests
JustusAdam Aug 21, 2023
1a331a2
Merge branch 'main' into simple-contacts-checking
JustusAdam Aug 21, 2023
98db699
Merge remote-tracking branch 'fork/main' into simple-contacts-checking
JustusAdam Aug 21, 2023
1938aa5
Format?
JustusAdam Aug 21, 2023
36b0dee
Seriously?
JustusAdam Aug 22, 2023
107b582
Comply with lifetime variables in fun sigs
JustusAdam Aug 23, 2023
c6a4a0e
Only complain for active contract attributes
JustusAdam Aug 23, 2023
e1fadd4
Addressing more comments
JustusAdam Aug 25, 2023
a0b00a2
I always forget to run thi script instead of `cargo fmt`
JustusAdam Aug 26, 2023
5447973
Apply suggestions from code review
JustusAdam Sep 6, 2023
e424b26
Suggestions from code review
JustusAdam Sep 6, 2023
702571b
Merge remote-tracking branch 'fork/main' into simple-contacts-checking
JustusAdam Sep 6, 2023
b5499f6
Merge remote-tracking branch 'fork/main' into simple-contacts-checking
JustusAdam Sep 7, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 38 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,43 @@ impl<'tcx> GotocHook<'tcx> for MemCmp {
}
}

/// A builtin that is essentially a C-style dereference operation, creating an
/// unsafe challow copy. Importantly either this copy or the original needs to
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
/// be `mem::forget`en or a double-free will occur.
///
/// Takes in a `&T` reference and returns a `T` (like clone would but without
/// cloning). Breaks ownership rules and is only used in the context of function
/// contracts where we can structurally guarantee the use is safe.
struct UntrackedDeref;

impl<'tcx> GotocHook<'tcx> for UntrackedDeref {
fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
matches_function(tcx, instance, "KaniUntrackedDeref")
}

fn handle(
&self,
tcx: &mut GotocCtx<'tcx>,
_instance: Instance<'tcx>,
mut fargs: Vec<Expr>,
assign_to: Place<'tcx>,
_target: Option<BasicBlock>,
span: Option<Span>,
) -> Stmt {
assert_eq!(fargs.len(), 1);
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
let loc = tcx.codegen_span_option(span);
Stmt::block(
vec![Stmt::assign(
unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to))
.goto_expr,
fargs.pop().unwrap().dereference(),
loc,
)],
loc,
)
}
}

pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
GotocHooks {
hooks: vec![
Expand All @@ -335,6 +372,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
Rc::new(Nondet),
Rc::new(RustAlloc),
Rc::new(MemCmp),
Rc::new(UntrackedDeref),
],
}
}
Expand Down
213 changes: 205 additions & 8 deletions kani-compiler/src/kani_middle/attributes.rs
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,21 @@
use std::collections::BTreeMap;

use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
use rustc_ast::{
attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind,
NestedMetaItem,
};
use rustc_errors::ErrorGuaranteed;
use rustc_hir::{def::DefKind, def_id::DefId};
use rustc_middle::ty::{Instance, TyCtxt, TyKind};
use rustc_span::Span;
use rustc_session::Session;
use rustc_span::{Span, Symbol};
use std::str::FromStr;
use strum_macros::{AsRefStr, EnumString};

use tracing::{debug, trace};

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

#[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
#[strum(serialize_all = "snake_case")]
Expand All @@ -27,6 +31,16 @@ enum KaniAttributeKind {
/// Attribute used to mark unstable APIs.
Unstable,
Unwind,
/// 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,
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
/// Attribute on a function with a contract that identifies the code
/// implementing the check for this contract.
CheckedWith,
/// Attribute on a function that was auto-generated from expanding a
/// function contract.
IsContractGenerated,
}

impl KaniAttributeKind {
Expand All @@ -37,10 +51,31 @@ impl KaniAttributeKind {
| KaniAttributeKind::ShouldPanic
| KaniAttributeKind::Solver
| KaniAttributeKind::Stub
| KaniAttributeKind::ProofForContract
| KaniAttributeKind::Unwind => true,
KaniAttributeKind::Unstable => false,
KaniAttributeKind::Unstable
| KaniAttributeKind::CheckedWith
| KaniAttributeKind::IsContractGenerated => false,
}
}

/// Is this an "active" function contract attribute? This means it is is
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
/// part of the function contract interface *and* it implies that a contract
/// will be used (stubbed or checked) in some way, thus requiring that the
/// user activate the unstable feature.
///
/// If we find an "inactive" contract attribute we chose not to error,
/// because it wouldn't have any effect anyway.
feliperodri marked this conversation as resolved.
Show resolved Hide resolved
pub fn demands_function_contract_use(self) -> bool {
matches!(self, KaniAttributeKind::ProofForContract)
}

/// Would this attribute be placed on a function as part of a function
/// contract. E.g. created by `requires`, `ensures`
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
pub fn is_function_contract(self) -> bool {
use KaniAttributeKind::*;
matches!(self, CheckedWith | IsContractGenerated)
}
}

/// Bundles together common data used when evaluating the attributes of a given
Expand Down Expand Up @@ -83,6 +118,54 @@ impl<'tcx> KaniAttributes<'tcx> {
Self { map, tcx, item: def_id }
}

/// Expect that at most one attribute of this kind exists on the function
/// and return it.
fn expect_maybe_one(&self, kind: KaniAttributeKind) -> Option<&'tcx Attribute> {
match self.map.get(&kind)?.as_slice() {
[one] => Some(one),
_ => {
self.tcx.sess.err(format!(
"Too many {} attributes on {}, expected 0 or 1",
kind.as_ref(),
self.tcx.def_path_debug_str(self.item)
));
None
}
}
}

/// Parse and extract the `proof_for_contract(TARGET)` attribute. The
/// returned symbol and defid are respectively the name and id of `TARGET`,
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
/// the span in the span for the attribute (contents).
fn interpret_the_for_contract_attribute(
&self,
) -> 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()
),
)
})
})
}

/// Extract the name of the sibling function this contract is checked with
/// (if any)
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
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))
}

/// 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 @@ -122,12 +205,26 @@ impl<'tcx> KaniAttributes<'tcx> {
})
}
KaniAttributeKind::Proof => {
assert!(!self.map.contains_key(&KaniAttributeKind::ProofForContract));
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
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::ProofForContract => {
assert!(!self.map.contains_key(&KaniAttributeKind::Proof));
expect_single(self.tcx, kind, &attrs);
}
KaniAttributeKind::CheckedWith => {
self.expect_maybe_one(kind)
.map(|attr| expect_key_string_value(&self.tcx.sess, attr));
}
KaniAttributeKind::IsContractGenerated => {
// Ignored here because this is only used by the proc macros
// to communicate with one another. So by the time it gets
// here we don't care if it's valid or not.
}
}
}
}
Expand All @@ -142,6 +239,23 @@ impl<'tcx> KaniAttributes<'tcx> {
// https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
return;
}

// If the `function-contracts` unstable feature is not enabled then no
// function should use any of those APIs.
if !enabled_features.iter().any(|feature| feature == "function-contracts") {
for kind in self.map.keys().copied().filter(|a| a.demands_function_contract_use()) {
let msg = format!(
"Using the {} attribute requires activating the unstable `function-contracts` feature",
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
kind.as_ref()
);
if let Some(attr) = self.map.get(&kind).unwrap().first() {
self.tcx.sess.span_err(attr.span, msg);
} else {
self.tcx.sess.err(msg);
}
}
}

if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) {
for attr in unstable_attrs {
let unstable_attr = UnstableAttribute::try_from(*attr).unwrap();
Expand Down Expand Up @@ -176,7 +290,8 @@ impl<'tcx> KaniAttributes<'tcx> {
/// 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()
self.map.contains_key(&KaniAttributeKind::Proof)
|| self.map.contains_key(&KaniAttributeKind::ProofForContract)
}

/// Extract harness attributes for a given `def_id`.
Expand All @@ -185,7 +300,9 @@ impl<'tcx> KaniAttributes<'tcx> {
/// 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);
if !self.item.is_local() {
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)| {
Expand All @@ -195,16 +312,39 @@ impl<'tcx> KaniAttributes<'tcx> {
harness.solver = parse_solver(self.tcx, attributes[0]);
}
KaniAttributeKind::Stub => {
harness.stubs = parse_stubs(self.tcx, self.item, attributes);
harness.stubs.extend_from_slice(&parse_stubs(self.tcx, self.item, attributes));
}
KaniAttributeKind::Unwind => {
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::Unstable => {
// Internal attribute which shouldn't exist here.
unreachable!()
}
KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => {
todo!("Contract attributes are not supported on proofs")
}
};
harness
})
Expand All @@ -226,6 +366,18 @@ impl<'tcx> KaniAttributes<'tcx> {
}
}
}

fn stub_for_relative_item(&self, anchor: Symbol, replacement: Symbol) -> Stub {
let local_id = self.item.expect_local();
let current_module = self.tcx.parent_module_from_def_id(local_id);
let replace_str = replacement.as_str();
let original_str = anchor.as_str();
let replacement = original_str
.rsplit_once("::")
.map_or_else(|| replace_str.to_string(), |t| t.0.to_string() + "::" + replace_str);
resolve::resolve_fn(self.tcx, current_module.to_local_def_id(), &replacement).unwrap();
Stub { original: original_str.to_string(), replacement }
}
}

/// An efficient check for the existence for a particular [`KaniAttributeKind`].
Expand All @@ -239,10 +391,18 @@ fn has_kani_attribute<F: Fn(KaniAttributeKind) -> bool>(
tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate)
}

/// Test is this function was generated by expanding a contract attribute like
/// `requires` and `ensures`
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool {
has_kani_attribute(tcx, def_id, KaniAttributeKind::is_function_contract)
}

/// 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 {
has_kani_attribute(tcx, def_id, |a| matches!(a, KaniAttributeKind::Proof))
has_kani_attribute(tcx, def_id, |a| {
matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract)
})
}

/// Does this `def_id` have `#[rustc_test_marker]`?
Expand All @@ -258,6 +418,43 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String {
parse_str_value(&marker).unwrap()
}

/// Expect the contents of this attribute to be of the format #[attribute =
/// "value"] and return the `"value"`
JustusAdam marked this conversation as resolved.
Show resolved Hide resolved
fn expect_key_string_value(
sess: &Session,
attr: &Attribute,
) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
let span = attr.span;
let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else {
return Err(sess.span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
};
let maybe_str = match it {
AttrArgsEq::Ast(expr) => {
if let ExprKind::Lit(tok) = expr.kind {
match LitKind::from_token_lit(tok) {
Ok(l) => l.str(),
Err(err) => {
return Err(sess.span_err(
span,
format!("Invalid string literal on right hand side of `=` {err:?}"),
));
}
}
} else {
return Err(
sess.span_err(span, "Expected literal string as right hand side of `=`")
);
}
}
AttrArgsEq::Hir(lit) => lit.kind.str(),
};
if let Some(str) = maybe_str {
Ok(str)
} else {
Err(sess.span_err(span, "Expected literal string as right hand side of `=`"))
}
}

fn expect_single<'a>(
tcx: TyCtxt,
kind: KaniAttributeKind,
Expand Down
Loading