Get rid of skip monomorphizer hack (#485) - #624
Merged
Conversation
The latest fixes that we added to RMC was enough to allow us to run the monomorphizer as is. We no longer require the hooks to be moved to an mir_transformation. We can investigate that further before pushing to main.
danielsn
reviewed
Nov 4, 2021
| // Give an empty main to make rustc happy. | ||
| #[no_mangle] | ||
| pub fn main() { | ||
| //let var = rmc::nondet::<i32>(); |
Contributor
Author
There was a problem hiding this comment.
oops... we can. I modified this test while reading the MIR and I forgot to change it back. Let me fix it.
danielsn
approved these changes
Nov 4, 2021
tedinski
pushed a commit
to tedinski/rmc
that referenced
this pull request
Apr 26, 2022
…ng#624) Remove the hack we added to monomorphizer to skip functions that we were not able to handle. The latest fixes that we added to RMC was enough to allow us to run the monomorphizer as is.
tedinski
pushed a commit
that referenced
this pull request
Apr 27, 2022
This was referenced Aug 3, 2026
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>
feliperodri
added a commit
to AlexanderPortland/kani
that referenced
this pull request
Aug 16, 2026
…model-checking#4710) Stacked on model-checking#4709 (first commit; review only the last commit here). 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 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 model-checking#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/model-checking#623/model-checking#624 landed (`check_to_bytes` and `non_null_check_read` within noise; `num::nonzero::verify::check_mul_i128_edge_pos` improved from 29.4s to 8.1s measured against the pre-fix baseline, attribution shared with verify-rust-std#624). The full `expected/function-contract` suite 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. --------- Signed-off-by: Felipe Monteiro <felisous@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe R. 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
2 participants
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.
Description of changes:
Remove the hack we added to monomorphizer to skip functions that we were not able to handle.
The latest fixes that we added to RMC was enough to allow us to run the monomorphizer as is. We no longer require the hooks to be moved to an mir_transformation. We can investigate that further before pushing to main.
Resolved issues:
Resolves #485
Testing:
I added tests to the functions that were causing trouble before.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.