Do not assert dependency contracts for calls made by contract clauses

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")]

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

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<ClosureDef>,
     /// Cache KaniRunContract function used to implement contracts.
     run_contract_fn: Option<FnDef>,
+    /// 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<FnDef>,
 }
 
 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 },

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.

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();

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 {

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
+    })
+}

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)]