Skip to content

Commit

Permalink
add option to use Assert ContractMode
Browse files Browse the repository at this point in the history
  • Loading branch information
carolynzech committed Dec 29, 2024
1 parent 11f3e04 commit 1f135c9
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 2 deletions.
15 changes: 13 additions & 2 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,9 @@ enum KaniAttributeKind {
/// contract, e.g. the contract check is substituted for the target function
/// before the the verification runs.
ProofForContract,
/// Internal attribute of the contracts implementation that identifies the
/// code implementing the function with the contract clauses as assertions.
AssertedWith,
/// Attribute on a function with a contract that identifies the code
/// implementing the check for this contract.
CheckedWith,
Expand Down Expand Up @@ -96,6 +99,7 @@ impl KaniAttributeKind {
| KaniAttributeKind::RecursionCheck
| KaniAttributeKind::CheckedWith
| KaniAttributeKind::ModifiesWrapper
| KaniAttributeKind::AssertedWith
| KaniAttributeKind::IsContractGenerated
| KaniAttributeKind::DisableChecks => false,
}
Expand Down Expand Up @@ -138,6 +142,8 @@ pub struct ContractAttributes {
pub replaced_with: Symbol,
/// The name of the inner check used to modify clauses.
pub modifies_wrapper: Symbol,
/// The name of the contract assert closure
pub asserted_with: Symbol,
}

impl std::fmt::Debug for KaniAttributes<'_> {
Expand Down Expand Up @@ -266,17 +272,19 @@ impl<'tcx> KaniAttributes<'tcx> {
let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith);
let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith);
let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper);
let asserted_with = self.attribute_value(KaniAttributeKind::AssertedWith);

let total = recursion_check
.iter()
.chain(&checked_with)
.chain(&replace_with)
.chain(&modifies_wrapper)
.chain(&asserted_with)
.count();
if total != 0 && total != 4 {
if total != 0 && total != 5 {
self.tcx.sess.dcx().err(format!(
"Failed to parse contract instrumentation tags in function `{}`.\
Expected `4` attributes, but was only able to process `{total}`",
Expected `5` attributes, but was only able to process `{total}`",
self.tcx.def_path_str(self.item)
));
}
Expand All @@ -286,6 +294,7 @@ impl<'tcx> KaniAttributes<'tcx> {
checked_with: checked_with?,
replaced_with: replace_with?,
modifies_wrapper: modifies_wrapper?,
asserted_with: asserted_with?,
})
}

Expand Down Expand Up @@ -379,6 +388,7 @@ impl<'tcx> KaniAttributes<'tcx> {
| KaniAttributeKind::CheckedWith
| KaniAttributeKind::ModifiesWrapper
| KaniAttributeKind::RecursionCheck
| KaniAttributeKind::AssertedWith
| KaniAttributeKind::ReplacedWith => {
self.attribute_value(kind);
}
Expand Down Expand Up @@ -531,6 +541,7 @@ impl<'tcx> KaniAttributes<'tcx> {
| KaniAttributeKind::ModifiesWrapper
| KaniAttributeKind::RecursionCheck
| KaniAttributeKind::RecursionTracker
| KaniAttributeKind::AssertedWith
| 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()));
}
Expand Down
29 changes: 29 additions & 0 deletions kani-compiler/src/kani_middle/transform/contracts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -224,6 +224,7 @@ impl AnyModifiesPass {
/// #[kanitool::recursion_check = "__kani_recursion_check_modify"]
/// #[kanitool::checked_with = "__kani_check_modify"]
/// #[kanitool::replaced_with = "__kani_replace_modify"]
/// #[kanitool::asserted_with = "__kani_assert_modify"]
/// #[kanitool::modifies_wrapper = "__kani_modifies_modify"]
/// fn name_fn(ptr: &mut u32) {
/// #[kanitool::fn_marker = "kani_register_contract"]
Expand All @@ -247,6 +248,11 @@ impl AnyModifiesPass {
/// let mut __kani_check_name_fn = || { /* check body */ };
/// kani_register_contract(__kani_check_name_fn)
/// }
/// kani::internal::ASSERT => {
/// #[kanitool::is_contract_generated(assert)]
/// let mut __kani_check_name_fn = || { /* assert body */ };
/// kani_register_contract(__kani_assert_name_fn)
/// }
/// _ => { /* original body */ }
/// }
/// }
Expand All @@ -267,6 +273,8 @@ pub struct FunctionWithContractPass {
check_fn: Option<InternalDefId>,
/// Functions that should be stubbed by their contract.
replace_fns: HashSet<InternalDefId>,
/// Should we interpret contracts as assertions? (true iff the contracts-as-assertions option is passed)
are_contracts_asserted: bool,
/// Functions annotated with contract attributes will contain contract closures even if they
/// are not to be used in this harness.
/// In order to avoid bringing unnecessary logic, we clear their body.
Expand Down Expand Up @@ -346,6 +354,10 @@ impl FunctionWithContractPass {
FunctionWithContractPass {
check_fn,
replace_fns,
are_contracts_asserted: queries
.args()
.unstable_features
.contains(&"contracts-as-assertions".to_string()),
unused_closures: Default::default(),
run_contract_fn,
}
Expand All @@ -371,6 +383,9 @@ impl FunctionWithContractPass {
/// kani::internal::SIMPLE_CHECK => {
/// // same as above
/// }
/// kani::internal::ASSERT => {
/// // same as above
/// }
/// _ => { /* original code */}
/// }
/// }
Expand Down Expand Up @@ -431,6 +446,7 @@ impl FunctionWithContractPass {
}

/// Return which contract mode to use for this function if any.
/// TODO document precedence
fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option<ContractMode> {
let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id());
kani_attributes.has_contract().then(|| {
Expand All @@ -443,6 +459,8 @@ impl FunctionWithContractPass {
}
} else if self.replace_fns.contains(&fn_def_id) {
ContractMode::Replace
} else if self.are_contracts_asserted {
ContractMode::Assert
} else {
ContractMode::Original
}
Expand All @@ -456,24 +474,34 @@ impl FunctionWithContractPass {
let recursion_closure = find_closure(tcx, fn_def, &body, contract.recursion_check.as_str());
let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str());
let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str());
let assert_closure = find_closure(tcx, fn_def, &body, contract.asserted_with.as_str());
match mode {
ContractMode::Original => {
// No contract instrumentation needed. Add all closures to the list of unused.
self.unused_closures.insert(recursion_closure);
self.unused_closures.insert(check_closure);
self.unused_closures.insert(replace_closure);
self.unused_closures.insert(assert_closure);
}
ContractMode::RecursiveCheck => {
self.unused_closures.insert(replace_closure);
self.unused_closures.insert(check_closure);
self.unused_closures.insert(assert_closure);
}
ContractMode::SimpleCheck => {
self.unused_closures.insert(replace_closure);
self.unused_closures.insert(recursion_closure);
self.unused_closures.insert(assert_closure);
}
ContractMode::Replace => {
self.unused_closures.insert(recursion_closure);
self.unused_closures.insert(check_closure);
self.unused_closures.insert(assert_closure);
}
ContractMode::Assert => {
self.unused_closures.insert(recursion_closure);
self.unused_closures.insert(check_closure);
self.unused_closures.insert(replace_closure);
}
}
}
Expand All @@ -488,6 +516,7 @@ enum ContractMode {
RecursiveCheck = 1,
SimpleCheck = 2,
Replace = 3,
Assert = 4,
}

fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef {
Expand Down
2 changes: 2 additions & 0 deletions kani_metadata/src/unstable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,8 @@ pub enum UnstableFeature {
FunctionContracts,
/// Enable loop contracts [RFC 12](https://model-checking.github.io/kani/rfc/rfcs/0012-loop-contracts.html)
LoopContracts,
/// Enable function contracts to be interpreted as assertions. (Requires function-contracts option).
ContractsAsAssertions,
/// Memory predicate APIs.
MemPredicates,
/// Automatically check that no invalid value is produced which is considered UB in Rust.
Expand Down

0 comments on commit 1f135c9

Please sign in to comment.