Dispatch clause-context calls to the check target to the original body

[tautschnig]

When checking the contract of a function F (proof_for_contract), every call to F in the harness's call graph is dispatched to F's contract check closure — including calls made while evaluating other functions' contract clauses. Since contracts of dependencies are asserted by default (#3802), such calls are common: e.g. NonNull::new's postcondition calls NonNull::as_ptr, so a proof_for_contract(as_ptr) harness in model-checking/verify-rust-std that constructs its input via NonNull::new dispatches a clause-context call to the check closure, which fails CBMC's single-top-level-call assertion:

Failed Checks: Only a single top-level call to function ... when checking contract ...

(With diffblue/cbmc#9149, the failure mode would change to spurious assigns-clause violations from running write-set checking in the clause's context — the dispatch itself is the bug.)

Fix

Track clause evaluation at runtime: the contract macros bracket every requires / ensures / modifies / history expression with enter_contract_clause / exit_contract_clause, which maintain a depth counter in kani_core. The contract transformation pass then computes the contract mode for check modes as mode * (1 - in_contract_clause()) instead of a constant (branch-free: one call, one cast, two integer ops), dispatching clause-context calls to the original body (mode 0). The original body has exact semantics and — unlike dispatching to the contract replacement — does not require the return type to implement Arbitrary.

Details worth reviewer attention:

• proof_for_contract harnesses (and automatic harnesses) reset the depth counter at harness entry, since statics are not reliably zero-initialized in every configuration (caught by modifies/field_pass.rs).
• enter/exit_contract_clause are exported with a __VERIFIER symbol prefix so CBMC's DFCC treats them as verification-internal and does not flag the counter update as an assigns-clause violation of the function under contract checking (caught by generic_infinity_recursion.rs; see dfcc_is_cprover_function_symbol in CBMC).
• The counter uses saturating arithmetic: DFCC havocs static state inside the enforced region, so the depth value there is arbitrary. All reads occur between an enter/exit pair where the depth is at least 1 regardless of the havocked base value, so dispatch remains correct.

Testing

New regression tests cover both directions: a harness constructing its input through a function whose postcondition calls the verification target now passes, and a wrong postcondition on the target still fails (the actual check is not weakened). Full expected/function-contract (111) and kani/FunctionContracts (8) suites pass. End-to-end on verify-rust-std (Kani pin 152c6a8 + CBMC 6.10.0): ptr::non_null::verify::non_null_check_as_ptr passes without --no-assert-contracts, with no regression on a 9-harness validation batch.

Part of the effort to make dropping --no-assert-contracts from verify-rust-std's run-kani.sh feasible (see also model-checking/verify-rust-std#622, #623, #624, and diffblue/cbmc#9149).

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

[Copilot]

Pull request overview

This PR fixes function-contract checking (proof_for_contract) so that calls to the verification target that occur while evaluating other functions’ contract clauses are dispatched to the target’s original body (mode 0) instead of its contract-check closure. This avoids consuming the “single top-level check” and avoids DFCC write-set checking in the clause’s context, while preserving the correctness of the actual top-level contract check.

Changes:

• Add a runtime clause-evaluation depth counter in kani_core, with entry/exit hooks and a query function.
• Bracket contract clause expression evaluation in the proc-macros so clause-context execution can be detected at runtime.
• Update the compiler contract transform to compute check modes dynamically (mode * (1 - in_contract_clause())) and reset the depth counter at harness entry (including automatic harnesses), plus add regression tests.

Reviewed changes

Copilot reviewed 14 out of 14 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/expected/function-contract/clause_calls_check_target.rs	New regression test: dependency contract clause calls the contract-check target.
tests/expected/function-contract/clause_calls_check_target.expected	Expected “SUCCESSFUL” output for the new passing regression.
tests/expected/function-contract/clause_calls_check_target_fail.rs	Companion regression ensuring the top-level contract check still fails when it should.
tests/expected/function-contract/clause_calls_check_target_fail.expected	Expected failure output for the companion regression.
library/kani_macros/src/sysroot/contracts/shared.rs	Bracket “remember” (old/history) subexpressions so clause-context tracking is consistent.
library/kani_macros/src/sysroot/contracts/replace.rs	Bracket requires/ensures/modifies expressions in replace-mode generation.
library/kani_macros/src/sysroot/contracts/mod.rs	Reset clause-depth counter at #[kani::proof_for_contract] harness entry.
library/kani_macros/src/sysroot/contracts/helpers.rs	Introduce bracket_clause_expr helper to wrap clause evaluation with enter/exit hooks.
library/kani_macros/src/sysroot/contracts/check.rs	Bracket requires/ensures/modifies expressions in check-mode generation.
library/kani_macros/src/sysroot/contracts/assert.rs	Bracket requires/ensures expressions in assert-mode generation.
library/kani_core/src/lib.rs	Add the clause-depth counter and hooks/models (enter/exit/in/reset).
kani-compiler/src/kani_middle/transform/contracts.rs	Compute check modes dynamically using in_contract_clause() for clause-context calls.
kani-compiler/src/kani_middle/transform/automatic.rs	Reset clause-depth counter at automatic harness entry for contract-bearing functions.
kani-compiler/src/kani_middle/kani_functions.rs	Register new Kani model functions for clause-context detection/reset.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.