Summarise sequential top-level calls by replacement in DFCC checks - #9149
Open
tautschnig wants to merge 1 commit into
Open
Summarise sequential top-level calls by replacement in DFCC checks#9149tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
When enforcing a contract, the DFCC wrapper so far rejected any second top-level call to the checked function with a "Only a single top-level call" assertion failure. This is stricter than necessary: once (or while) one call is being checked against the contract, any further call can soundly be summarised by contract replacement, exactly like calls to --replace-call-with-contract functions: the preconditions are asserted in the calling context, the assigns clause is havocked, and the postconditions are assumed. Replace the assertion by a branch to a replacement section, which is now emitted unconditionally (previously it was only emitted for recursive checks with --dfcc-allow-recursive-calls; the behaviour for recursive calls is unchanged). This restriction was a long-standing usability papercut: harnesses had to be written so that exactly one call to the function under verification was reachable. It has become a correctness problem for Rust verification via Kani, where contracts of dependencies are asserted by default (model-checking/kani#3802): the contract clauses of other functions in the harness's call graph may themselves call the function under verification - 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 fails the single-top-level-call assertion through no fault of the harness. Two regression tests: a second sequential call is verified via replacement (with its ensures usable by the caller), and a second call violating the contract's requires is reported as a precondition failure. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
requested review from
feliperodri,
kroening,
peterschrammel and
remi-delmas-3000
as code owners
August 3, 2026 18:33
There was a problem hiding this comment.
Pull request overview
This PR relaxes DFCC contract-enforcement wrappers so that sequential (non-recursive) second and subsequent top-level calls to the checked function are no longer rejected, but are instead soundly summarised using contract replacement (assert requires in caller, havoc assigns, assume ensures). This improves usability (harnesses no longer need to ensure exactly one reachable call) and avoids failures in call graphs where other contracts invoke the checked function (e.g., Rust/Kani scenarios).
Changes:
- Update DFCC wrapper generation to branch to a replacement section when a completed top-level check has already occurred (instead of asserting “single top-level call”).
- Emit the replacement section unconditionally; recursive-call behaviour remains controlled by
allow_recursive_calls. - Add two regression tests covering (1) successful sequential re-invocation via replacement and (2) failure when the sequential re-invocation violates
requires.
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp | Change wrapper control flow to summarise sequential top-level re-invocations via contract replacement instead of asserting. |
| regression/contracts-dfcc/check_multiple_top_level_calls/test.desc | New regression test expecting success when a second sequential call is summarised by replacement. |
| regression/contracts-dfcc/check_multiple_top_level_calls/main.c | Test program calling the enforced function twice and using the ensures of the replacement on the second call. |
| regression/contracts-dfcc/check_multiple_top_level_calls_fail/test.desc | New regression test expecting a precondition failure on a second sequential call that violates requires. |
| regression/contracts-dfcc/check_multiple_top_level_calls_fail/main.c | Test program triggering a requires failure via sequential replacement call. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+180
to
+181
| // At most a single top level call to the checked function is checked | ||
| // against the contract in any execution. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9149 +/- ##
========================================
Coverage 80.83% 80.83%
========================================
Files 1715 1715
Lines 189948 189986 +38
Branches 73 73
========================================
+ Hits 153540 153574 +34
- Misses 36408 36412 +4 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
feliperodri
added a commit
to tautschnig/kani
that referenced
this pull request
Aug 15, 2026
model-checking#4709) 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 (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 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, model-checking#623, model-checking#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. --------- Signed-off-by: Felipe Monteiro <felisous@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>
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.
When enforcing a contract, the DFCC wrapper so far rejected any second top-level call to the checked function with a "Only a single top-level call" assertion failure. This is stricter than necessary: once (or while) one call is being checked against the contract, any further call can soundly be summarised by contract replacement, exactly like calls to --replace-call-with-contract functions: the preconditions are asserted in the calling context, the assigns clause is havocked, and the postconditions are assumed.
Replace the assertion by a branch to a replacement section, which is now emitted unconditionally (previously it was only emitted for recursive checks with --dfcc-allow-recursive-calls; the behaviour for recursive calls is unchanged).
This restriction was a long-standing usability papercut: harnesses had to be written so that exactly one call to the function under verification was reachable. It has become a correctness problem for Rust verification via Kani, where contracts of dependencies are asserted by default (model-checking/kani#3802): the contract clauses of other functions in the harness's call graph may themselves call the function under verification - 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 fails the single-top-level-call assertion through no fault of the harness.
Two regression tests: a second sequential call is verified via replacement (with its ensures usable by the caller), and a second call violating the contract's requires is reported as a precondition failure.