Do not assert dependency contracts for calls made by contract clauses - #4710
Open
tautschnig wants to merge 2 commits into
Open
Do not assert dependency contracts for calls made by contract clauses#4710tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
When checking the contract of a function F (proof_for_contract), every call to F in the harness's call graph was dispatched to F's contract check closure - including calls made while evaluating *other functions' contract clauses*. Since contracts of dependencies are asserted by default (model-checking#3802), such calls are common: e.g. NonNull::new's postcondition calls NonNull::as_ptr, so a proof_for_contract(as_ptr) harness that constructs its input via NonNull::new dispatched a clause-context call to the check closure, which fails CBMC's single-top-level-call assertion (and, with diffblue/cbmc#9149, would instead run write-set checking in the clause's context, producing spurious assigns-clause violations). 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, 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: * proof_for_contract harnesses (and automatic harnesses) reset the depth counter at harness entry, since statics are not reliably zero-initialized in every configuration. * enter/exit_contract_clause are exported with a __VERIFIER symbol prefix so that CBMC's function-contract instrumentation (DFCC) treats them as verification-internal and does not flag the counter update as an assigns-clause violation of the function under contract checking (see dfcc_is_cprover_function_symbol). * 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. New regression tests check that a harness constructing its input through a function whose postcondition calls the verification target passes, and that the target's own contract check is still genuinely performed (a wrong postcondition on the target still fails). Resolves the ptr::non_null::verify::non_null_check_as_ptr failure in model-checking/verify-rust-std when running without --no-assert-contracts. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contracts of dependencies are asserted by default (model-checking#3802) as an aid for detecting API misuse in user code. Calls made while evaluating *contract clauses*, however, are specification-level plumbing: clause expressions compute a predicate over pre-/post-states, and the functions they call are best executed with their exact semantics. Re-asserting dependency contracts inside every clause evaluation multiplies verification cost - clauses of contract-dense code (e.g. the Rust standard library in model-checking/verify-rust-std) routinely call contracted functions like NonNull::as_ptr, paying the assert-closure overhead per clause instance - without checking any user code. Extend the clause-context dispatch introduced for check modes to assert mode: calls to a contracted dependency that occur during clause evaluation now execute the original body (mode 0). The body remains fully inlined and UB-checked; only the requires/ensures assertions of the *callee's* contract are skipped in this context. The new regression test checks both halves: a clause calling a contracted function with precondition-violating (but well-defined) arguments verifies successfully, while the same misuse in user code is still caught. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR refines Kani’s function-contract instrumentation so that calls made while evaluating contract clauses (requires/ensures/modifies) do not re-assert dependency contracts. Instead, clause-context calls execute the callee’s original body (mode 0), reducing verification overhead on contract-dense code while preserving UB checking of the executed bodies.
Changes:
- Add clause-evaluation tracking via a depth counter in
kani_core, and bracket contract-clause expression evaluation to toggle clause context. - Extend compiler dispatch logic to compute contract mode dynamically for ASSERT (and existing CHECK) modes, so clause-context calls use mode 0.
- Add regression tests covering (1) “no assert inside clauses” and (2) “clause calls into check target” scenarios.
Reviewed changes
Copilot reviewed 16 out of 16 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/expected/function-contract/clause_context_no_assert.rs | New regression test ensuring dependency contract assertions are skipped during clause evaluation (but still enforced in user code). |
| tests/expected/function-contract/clause_context_no_assert.expected | Expected output for the above test (misuse in user code still fails). |
| tests/expected/function-contract/clause_calls_check_target.rs | New regression test ensuring clause-context calls into the contract-check target don’t consume the top-level check / DFCC context. |
| tests/expected/function-contract/clause_calls_check_target.expected | Expected success output for the above test. |
| tests/expected/function-contract/clause_calls_check_target_fail.rs | Companion negative test ensuring the actual top-level contract check is not weakened. |
| tests/expected/function-contract/clause_calls_check_target_fail.expected | Expected failure output for the above negative test. |
| library/kani_macros/src/sysroot/contracts/helpers.rs | Introduce bracket_clause_expr to bracket clause expression evaluation with enter/exit hooks. |
| library/kani_macros/src/sysroot/contracts/shared.rs | Ensure “remembers” expressions are also bracketed as clause-context evaluations. |
| library/kani_macros/src/sysroot/contracts/check.rs | Bracket requires/ensures/modifies-related clause expressions in check-mode generation. |
| library/kani_macros/src/sysroot/contracts/assert.rs | Bracket requires/ensures clause expressions in assert-mode generation. |
| library/kani_macros/src/sysroot/contracts/replace.rs | Bracket requires/ensures/modifies clause expressions in replacement-mode generation. |
| library/kani_macros/src/sysroot/contracts/mod.rs | Reset clause-depth counter at #[kani::proof_for_contract] harness entry. |
| library/kani_core/src/lib.rs | Add depth counter + enter/exit/reset/in-query functions for clause-context tracking. |
| kani-compiler/src/kani_middle/kani_functions.rs | Add new Kani model functions for InContractClause and ResetContractClauseDepth. |
| kani-compiler/src/kani_middle/transform/contracts.rs | Extend set_mode to consult in_contract_clause() for ASSERT (and existing CHECK) modes. |
| kani-compiler/src/kani_middle/transform/automatic.rs | Reset clause-depth counter in automatic contract harnesses. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+212
to
+216
| /// 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. |
Comment on lines
+217
to
+224
| 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 | ||
| }) | ||
| } |
Comment on lines
+358
to
+362
| let reset_ret = harness_body.new_local( | ||
| Ty::new_tuple(&[]), | ||
| source.span(harness_body.blocks()), | ||
| Mutability::Not, | ||
| ); |
Comment on lines
+8
to
+12
| //! 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). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #4709 (first commit; review only the last commit here).
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, are specification-level plumbing: clause expressions compute a predicate over pre-/post-states, and the functions they call are best executed with their exact semantics. Re-asserting dependency contracts inside every clause evaluation multiplies verification cost on contract-dense code (clauses in model-checking/verify-rust-std routinely call contracted functions such as
NonNull::as_ptr, paying the assert-closure overhead per clause instance) without checking any user code.This PR extends the clause-context dispatch introduced in #4709 from check modes to assert mode: calls to a contracted dependency occurring during clause evaluation execute the original body (mode 0). The body remains fully inlined and UB-checked; only the requires/ensures assertions of the callee's contract are skipped in this context — a genuine UB-causing misuse inside a clause is still caught by the UB checks themselves.
The regression test covers both halves: a clause calling a contracted function with precondition-violating (but well-defined) arguments verifies successfully, while the same misuse in user code still fails on the asserted precondition.
Measurements on verify-rust-std (Kani pin 152c6a8 + CBMC 6.10.0, contracts asserted): semantics-driven change with modest performance impact on sampled harnesses after the fixes in verify-rust-std#622/#623/#624 landed (
check_to_bytesandnon_null_check_readwithin noise;num::nonzero::verify::check_mul_i128_edge_posimproved from 29.4s to 8.1s measured against the pre-fix baseline, attribution shared with verify-rust-std#624). The fullexpected/function-contractsuite passes with--force-rerun(112/112).By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.