diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index d5b97aa5406c..510c9a0e78bf 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -75,6 +75,8 @@ pub enum KaniModel { LoadArgument, #[strum(serialize = "InitializeMemoryInitializationStateModel")] InitializeMemoryInitializationState, + #[strum(serialize = "InContractClauseModel")] + InContractClause, #[strum(serialize = "IsPtrInitializedModel")] IsPtrInitialized, #[strum(serialize = "IsStrPtrInitializedModel")] @@ -89,6 +91,8 @@ pub enum KaniModel { PtrOffsetFrom, #[strum(serialize = "PtrOffsetFromUnsignedModel")] PtrOffsetFromUnsigned, + #[strum(serialize = "ResetContractClauseDepthModel")] + ResetContractClauseDepth, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 59ca3bd34abf..143d567b4a5a 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -286,6 +286,7 @@ impl AutomaticArbitraryPass { pub struct AutomaticHarnessPass { kani_any: FnDef, init_contracts_hook: Instance, + reset_clause_depth: Instance, kani_autoharness_intrinsic: FnDef, } @@ -298,7 +299,11 @@ impl AutomaticHarnessPass { let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap(); let init_contracts_hook = Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap(); - Self { kani_any, init_contracts_hook, kani_autoharness_intrinsic } + let reset_clause_depth = + *kani_fns.get(&KaniModel::ResetContractClauseDepth.into()).unwrap(); + let reset_clause_depth = + Instance::resolve(reset_clause_depth, &GenericArgs(vec![])).unwrap(); + Self { kani_any, init_contracts_hook, reset_clause_depth, kani_autoharness_intrinsic } } } @@ -350,6 +355,18 @@ impl TransformPass for AutomaticHarnessPass { vec![], Place::from(ret_local), ); + let reset_ret = harness_body.new_local( + Ty::new_tuple(&[]), + source.span(harness_body.blocks()), + Mutability::Not, + ); + harness_body.insert_call( + &self.reset_clause_depth, + &mut source, + InsertPosition::Before, + vec![], + Place::from(reset_ret), + ); } // For each argument of `fn_to_verify`, create a nondeterministic value of its type diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index d555bbbaf66e..4669f79e8fff 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -13,10 +13,13 @@ use rustc_middle::ty::TyCtxt; use rustc_public::CrateDef; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ - Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents, + BinOp, Body, CastKind, ConstOperand, Mutability, Operand, Place, Rvalue, Terminator, + TerminatorKind, VarDebugInfoContents, }; use rustc_public::rustc_internal; -use rustc_public::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy}; +use rustc_public::ty::{ + ClosureDef, FnDef, GenericArgs, MirConst, RigidTy, Ty, TyKind, TypeAndMut, UintTy, +}; use rustc_span::Symbol; use std::collections::HashSet; use std::fmt::Debug; @@ -279,6 +282,10 @@ pub struct FunctionWithContractPass { unused_closures: HashSet, /// Cache KaniRunContract function used to implement contracts. run_contract_fn: Option, + /// Cache of the InContractClauseModel function used to dispatch calls to + /// the function under contract verification to its contract replacement + /// when they occur during evaluation of another contract's clauses. + in_clause_fn: Option, } impl TransformPass for FunctionWithContractPass { @@ -365,12 +372,16 @@ impl FunctionWithContractPass { let run_contract_fn = queries.kani_functions().get(&KaniModel::RunContract.into()).copied(); assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); + let in_clause_fn = + queries.kani_functions().get(&KaniModel::InContractClause.into()).copied(); + assert!(in_clause_fn.is_some(), "Failed to find Kani in-contract-clause function"); FunctionWithContractPass { check_fn, replace_fns, assert_contracts: !queries.args().no_assert_contracts, unused_closures: Default::default(), run_contract_fn, + in_clause_fn, } } else { // If reachability mode is PubFns or Tests, we just remove any contract logic. @@ -442,12 +453,77 @@ impl FunctionWithContractPass { let span = mode_call.span(new_body.blocks()); let mode_const = new_body.new_uint_operand(mode as _, UintTy::U8, span); - new_body.assign_to( - ret.clone(), - Rvalue::Use(mode_const), - &mut mode_call, - InsertPosition::Before, - ); + if matches!( + mode, + ContractMode::SimpleCheck | ContractMode::RecursiveCheck | ContractMode::Assert + ) { + // Calls occurring during the evaluation of *contract clauses* of + // other functions are dispatched to the original body (mode 0, + // exact semantics) rather than the mode selected for normal + // calls, by computing the mode at runtime as + // `mode * (1 - in_contract_clause())`: + // + // * For check modes: while the harness is checking the contract + // of this function, the function may also be called from + // contract clauses of other functions in the harness's call + // graph (e.g. a postcondition mentioning `NonNull::as_ptr` + // evaluated while `as_ptr` itself is under verification). Such + // calls must not be dispatched to the check closure: they + // would consume the single top-level contract check and run + // write-set instrumentation in the clause's context. (Unlike + // dispatching to the contract replacement, the original body + // does not require the return type to implement Arbitrary.) + // + // * For assert mode: asserting the contracts of dependencies + // (the default since #3802) is an aid for detecting API misuse + // in user code; re-asserting them for calls made by *contract + // clauses* checks specification-level plumbing at a + // multiplicative cost. Clause evaluation is meant to compute a + // predicate over the pre-/post-states, and the functions it + // calls are best executed with their exact semantics (their + // bodies remain fully inlined and UB-checked either way). + let in_clause_instance = + Instance::resolve(self.in_clause_fn.unwrap(), &GenericArgs(vec![])).unwrap(); + let in_clause_local = new_body.new_local(Ty::bool_ty(), span, Mutability::Mut); + new_body.insert_call( + &in_clause_instance, + &mut mode_call, + InsertPosition::Before, + vec![], + Place::from(in_clause_local), + ); + let u8_ty = Ty::from_rigid_kind(RigidTy::Uint(UintTy::U8)); + let in_clause_u8 = new_body.insert_assignment( + Rvalue::Cast( + CastKind::IntToInt, + Operand::Move(Place::from(in_clause_local)), + u8_ty, + ), + &mut mode_call, + InsertPosition::Before, + ); + let one_const = new_body.new_uint_operand(1, UintTy::U8, span); + let not_in_clause = new_body.insert_binary_op( + BinOp::Sub, + one_const, + Operand::Move(Place::from(in_clause_u8)), + &mut mode_call, + InsertPosition::Before, + ); + new_body.assign_to( + ret.clone(), + Rvalue::BinaryOp(BinOp::Mul, mode_const, Operand::Move(Place::from(not_in_clause))), + &mut mode_call, + InsertPosition::Before, + ); + } else { + new_body.assign_to( + ret.clone(), + Rvalue::Use(mode_const), + &mut mode_call, + InsertPosition::Before, + ); + } new_body.replace_terminator( &mode_call, Terminator { kind: TerminatorKind::Goto { target }, span }, diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index b3dbc80e25a1..82a595ef1567 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -618,6 +618,81 @@ macro_rules! kani_intrinsics { /// Insert the contract into the body of the function as assertion(s). pub const ASSERT: Mode = 4; + /// Tracks whether execution is currently evaluating a contract + /// clause (requires / ensures / modifies expression). Nesting is + /// possible when a clause calls a function whose own contract + /// clauses are evaluated, hence a depth counter rather than a + /// flag. Verification is single-threaded, so a static is sound. + static mut CONTRACT_CLAUSE_DEPTH: usize = 0; + + /// Resets the clause-depth counter at harness entry. Static + /// variables are not reliably zero-initialized in every + /// verification configuration, so harnesses reset the counter + /// explicitly before the first contract dispatch. + #[doc(hidden)] + #[inline(never)] + #[kanitool::fn_marker = "ResetContractClauseDepthModel"] + pub fn reset_contract_clause_depth() { + unsafe { + CONTRACT_CLAUSE_DEPTH = 0; + } + } + + /// Marks the beginning of the evaluation of a contract clause. + /// Inserted by the contract macros around every clause expression. + /// + /// The `__VERIFIER` symbol prefix makes CBMC's function-contract + /// instrumentation (DFCC) treat this function as + /// verification-internal (see `dfcc_is_cprover_function_symbol`), + /// so the counter update is not flagged as an illegal side effect + /// (assigns-clause violation) of a function under contract + /// checking. + #[doc(hidden)] + #[inline(never)] + #[unsafe(export_name = "__VERIFIER_kani_enter_contract_clause")] + pub fn enter_contract_clause() { + // Saturating arithmetic: when a contract check is enforced, + // CBMC havocs static state, so the counter value inside the + // enforced region is arbitrary. Saturation avoids spurious + // overflow failures while keeping `in_contract_clause` + // correct at every read (all reads occur between an + // enter/exit pair, where the depth is at least 1 regardless + // of the havocked base value). + unsafe { + CONTRACT_CLAUSE_DEPTH = CONTRACT_CLAUSE_DEPTH.saturating_add(1); + } + } + + /// Marks the end of the evaluation of a contract clause. + /// + /// See [enter_contract_clause] regarding the symbol name. + #[doc(hidden)] + #[inline(never)] + #[unsafe(export_name = "__VERIFIER_kani_exit_contract_clause")] + pub fn exit_contract_clause() { + unsafe { + CONTRACT_CLAUSE_DEPTH = CONTRACT_CLAUSE_DEPTH.saturating_sub(1); + } + } + + /// Whether execution is currently evaluating a contract clause. + /// + /// The contract transformation pass dispatches calls to the + /// function under contract verification to its *original body* + /// rather than its contract *check* when they occur during clause + /// evaluation: clauses of other functions in the harness's call + /// graph may legitimately call the function under verification + /// (e.g. a postcondition mentioning `NonNull::as_ptr` while + /// `as_ptr` itself is being verified), and such calls must + /// neither consume the single top-level contract check nor be + /// checked inside the clause's write-set context. + #[doc(hidden)] + #[inline(never)] + #[kanitool::fn_marker = "InContractClauseModel"] + pub fn in_contract_clause() -> bool { + unsafe { CONTRACT_CLAUSE_DEPTH > 0 } + } + /// Creates a non-fatal property with the specified condition and message. /// /// This check will not impact the program control flow even when it fails. diff --git a/library/kani_macros/src/sysroot/contracts/assert.rs b/library/kani_macros/src/sysroot/contracts/assert.rs index fb1d0e11a31b..45431c4582c6 100644 --- a/library/kani_macros/src/sysroot/contracts/assert.rs +++ b/library/kani_macros/src/sysroot/contracts/assert.rs @@ -64,16 +64,18 @@ impl<'a> ContractConditionsHandler<'a> { let Self { attr_copy, .. } = self; match &self.condition_type { ContractConditionsData::Requires { attr } => { + let attr_bracketed = bracket_clause_expr(quote!(#attr)); quote!({ - kani::assert(#attr, stringify!(#attr_copy)); + kani::assert(#attr_bracketed, stringify!(#attr_copy)); #(#body_stmts)* }) } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); + let ensures_bracketed = bracket_clause_expr(quote!(#ensures_clause)); let exec_postconditions = quote!( - kani::assert(#ensures_clause, stringify!(#attr_copy)); + kani::assert(#ensures_bracketed, stringify!(#attr_copy)); ); let return_expr = body_stmts.pop(); diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index c3d459f13cba..e819f2b2cfe7 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -24,8 +24,9 @@ impl<'a> ContractConditionsHandler<'a> { let Self { attr_copy, .. } = self; match &self.condition_type { ContractConditionsData::Requires { attr } => { + let attr_bracketed = bracket_clause_expr(quote!(#attr)); quote!({ - kani::assume(#attr); + kani::assume(#attr_bracketed); #(#body_stmts)* }) } @@ -34,8 +35,9 @@ impl<'a> ContractConditionsHandler<'a> { // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). + let ensures_bracketed = bracket_clause_expr(quote!(#ensures_clause)); let exec_postconditions = quote!( - kani::assert(#ensures_clause, stringify!(#attr_copy)); + kani::assert(#ensures_bracketed, stringify!(#attr_copy)); ); let return_expr = body_stmts.pop(); @@ -67,8 +69,8 @@ impl<'a> ContractConditionsHandler<'a> { }); if let Some(Expr::Tuple(values)) = wrapper_tuple { values.elems.extend(attr.iter().map(|attr| { - let expr: Expr = parse_quote!(#attr - as *const _); + let bracketed = bracket_clause_expr(quote!(#attr as *const _)); + let expr: Expr = parse_quote!(#bracketed); expr })); } else { diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index a9e83c4ad5df..4a4607bdf391 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -205,3 +205,20 @@ macro_rules! assert_spanned_err { assert_spanned_err!($condition, $span_source, concat!("Failed assertion ", stringify!($condition))) }; } + +/// Wrap the evaluation of a contract clause expression so that the +/// kani_core clause-depth counter is incremented around it. +/// +/// While a clause is being evaluated, calls to the function whose contract is +/// currently under verification are dispatched to its contract *replacement* +/// instead of its contract *check* (see `FunctionWithContractPass::set_mode` +/// in the Kani compiler). The linear `let` form (rather than a closure) +/// avoids altering the borrow semantics of the expression. +pub fn bracket_clause_expr(expr: proc_macro2::TokenStream) -> proc_macro2::TokenStream { + quote::quote!({ + kani::internal::enter_contract_clause(); + let __kani_clause_value = #expr; + kani::internal::exit_contract_clause(); + __kani_clause_value + }) +} diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 065da57fd514..6df31e038262 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -570,6 +570,11 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { let args = proc_macro2::TokenStream::from(attr); let mut fn_item = parse_macro_input!(item as ItemFn); fn_item.block.stmts.insert(0, parse_quote!(kani::internal::init_contracts();)); + // Reset the contract-clause depth counter before anything else: statics + // are not reliably zero-initialized, and the counter steers the dispatch + // of calls to the function under verification (see `set_mode` in the + // Kani compiler). + fn_item.block.stmts.insert(0, parse_quote!(kani::internal::reset_contract_clause_depth();)); quote!( #[allow(dead_code)] #[kanitool::proof_for_contract = stringify!(#args)] diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 719a96dcc429..1260dacd084b 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -85,8 +85,9 @@ impl<'a> ContractConditionsHandler<'a> { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + let attr_bracketed = bracket_clause_expr(quote!(#attr)); quote!({ - kani::assert(#attr, stringify!(#attr_copy)); + kani::assert(#attr_bracketed, stringify!(#attr_copy)); #(#before)* #(#after)* #result @@ -94,6 +95,7 @@ impl<'a> ContractConditionsHandler<'a> { } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); + let ensures_bracketed = bracket_clause_expr(quote!(#ensures_clause)); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); let (asserts, rest_of_before) = split_for_remembers(before, ContractMode::Replace); @@ -103,15 +105,27 @@ impl<'a> ContractConditionsHandler<'a> { #remembers #(#rest_of_before)* #(#after)* - kani::assume(#ensures_clause); + kani::assume(#ensures_bracketed); #result }) } ContractConditionsData::Modifies { attr } => { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + let havoc_stmts: Vec<_> = attr + .iter() + .map(|attr| { + let bracketed = + bracket_clause_expr(quote!(kani::internal::untracked_deref(&#attr))); + quote!(unsafe { + kani::internal::write_any(kani::internal::Pointer::assignable( + #bracketed, + )) + };) + }) + .collect(); quote!({ #(#before)* - #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)* + #(#havoc_stmts)* #(#after)* #result }) diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 930dc6dc1292..db6d09893bee 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -122,9 +122,12 @@ pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { let expr = &mut data.clone(); vis.visit_expr_closure_mut(expr); - let remembers_stmts: TokenStream2 = remembers_exprs - .iter() - .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = (#expr).clone(); #collect)); + let remembers_stmts: TokenStream2 = + remembers_exprs.iter().fold(quote!(), |collect, (ident, expr)| { + let bracketed = + crate::sysroot::contracts::helpers::bracket_clause_expr(quote!((#expr).clone())); + quote!(let #ident = #bracketed; #collect) + }); let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); (remembers_stmts, Expr::Verbatim(quote!(kani::internal::apply_closure(#expr, &#result)))) diff --git a/tests/expected/function-contract/clause_calls_check_target.expected b/tests/expected/function-contract/clause_calls_check_target.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/clause_calls_check_target.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/clause_calls_check_target.rs b/tests/expected/function-contract/clause_calls_check_target.rs new file mode 100644 index 000000000000..e940ab7ae2cb --- /dev/null +++ b/tests/expected/function-contract/clause_calls_check_target.rs @@ -0,0 +1,40 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! When checking the contract of a function F, other functions' contract +//! clauses in the harness's call graph may themselves call F (here: +//! `make_positive`'s postcondition calls `get`, while `get` is the target of +//! proof_for_contract). Such calls must be dispatched to F's contract +//! *replacement*, not its contract *check*: they must neither consume the +//! single top-level contract check nor be write-set-checked in the clause's +//! context. See https://github.com/model-checking/kani/issues/... (clause +//! dispatch) and diffblue/cbmc#9149 (sequential top-level calls). + +#[derive(Copy, Clone)] +struct Wrapper { + v: i32, +} + +impl Wrapper { + #[kani::ensures(|result| **result == self.v)] + fn get(&self) -> &i32 { + &self.v + } +} + +// The postcondition evaluates `result.get()`, calling the function whose +// contract is under verification in the harness below. +#[kani::requires(v > 0)] +#[kani::ensures(|result| *result.get() == v)] +fn make_positive(v: i32) -> Wrapper { + Wrapper { v } +} + +#[kani::proof_for_contract(Wrapper::get)] +fn check_get() { + let v: i32 = kani::any(); + kani::assume(v > 0); + let w = make_positive(v); + let _ = w.get(); +} diff --git a/tests/expected/function-contract/clause_calls_check_target_fail.expected b/tests/expected/function-contract/clause_calls_check_target_fail.expected new file mode 100644 index 000000000000..5debbe136dcd --- /dev/null +++ b/tests/expected/function-contract/clause_calls_check_target_fail.expected @@ -0,0 +1,3 @@ +Failed Checks: |result| **result == self.v.wrapping_add(1) + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/clause_calls_check_target_fail.rs b/tests/expected/function-contract/clause_calls_check_target_fail.rs new file mode 100644 index 000000000000..a51c97bd3d43 --- /dev/null +++ b/tests/expected/function-contract/clause_calls_check_target_fail.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! Companion to clause_calls_check_target.rs: ensure that the clause-context +//! dispatch of calls to the verification target does NOT weaken the actual +//! contract check performed for the harness's top-level call. The +//! postcondition of `get` below is wrong, and verification must fail even +//! though `make_positive`'s postcondition also calls `get` (which dispatches +//! to the original body in clause context). + +#[derive(Copy, Clone)] +struct Wrapper { + v: i32, +} + +impl Wrapper { + #[kani::ensures(|result| **result == self.v.wrapping_add(1))] + fn get(&self) -> &i32 { + &self.v + } +} + +#[kani::requires(v > 0)] +#[kani::ensures(|result| *result.get() == v)] +fn make_positive(v: i32) -> Wrapper { + Wrapper { v } +} + +#[kani::proof_for_contract(Wrapper::get)] +fn check_get() { + let v: i32 = kani::any(); + kani::assume(v > 0); + let w = make_positive(v); + let _ = w.get(); +} diff --git a/tests/expected/function-contract/clause_context_no_assert.expected b/tests/expected/function-contract/clause_context_no_assert.expected new file mode 100644 index 000000000000..529e4939a609 --- /dev/null +++ b/tests/expected/function-contract/clause_context_no_assert.expected @@ -0,0 +1,4 @@ +Failed Checks: x >= 10 + +Verification failed for - check_misuse_still_caught +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/function-contract/clause_context_no_assert.rs b/tests/expected/function-contract/clause_context_no_assert.rs new file mode 100644 index 000000000000..f31e0784ab46 --- /dev/null +++ b/tests/expected/function-contract/clause_context_no_assert.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! Contracts of dependencies are asserted by default (#3802) as an aid for +//! detecting API misuse in user code. Calls made while evaluating *contract +//! clauses*, however, execute the original body (exact semantics, still fully +//! UB-checked) without re-asserting the callee's contract: clause expressions +//! are specifications, and asserting specification-level plumbing multiplies +//! verification cost without checking user code. +//! +//! `one`'s postcondition below calls `plus_one(0)`, which violates +//! `plus_one`'s (overly strict) precondition but is well-defined: the clause +//! must evaluate to true without a contract-assertion failure. The same +//! misuse in *user code* (`check_misuse`) must still be caught. + +#[kani::requires(x >= 10)] +fn plus_one(x: u8) -> u8 { + x.wrapping_add(1) +} + +#[kani::ensures(|result| *result == plus_one(0))] +fn one() -> u8 { + 1 +} + +#[kani::proof] +fn check_clause_call_not_asserted() { + let _ = one(); +} + +#[kani::proof] +fn check_misuse_still_caught() { + let _ = plus_one(0); +}