Fail verification when the solver backend drops quantifiers - #4719
Open
tautschnig wants to merge 5 commits into
Open
Fail verification when the solver backend drops quantifiers#4719tautschnig wants to merge 5 commits into
tautschnig wants to merge 5 commits into
Conversation
CBMC's SAT-based backends only support quantifiers with constant bounds. A quantifier with a symbolic bound reaches the backend's quantifier post-processing, which has no handling and replaces the expression with unconstrained values, reporting only a low-visibility 'warning: ignoring forall' among CBMC's status messages (which Kani does not surface). The consequences are severe for usability: a kani::assume containing such a quantifier is silently NOT enforced -- the harness may verify successfully while covering none of the intended property -- and a kani::assert containing one may fail spuriously. Detect CBMC's ignoring-quantifier messages in the output parser, count them on VerificationResult, and render a prominent warning after the result (on both successful and failed outcomes) explaining the effect and suggesting an SMT solver backend (#[kani::solver(z3)]), which supports these quantifiers. The new expected test pins the dangerous case: a harness that SUCCEEDS only because its final assertion does not depend on the (unenforced) quantified assumption, with the warning attached. 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 improves Kani’s user-facing diagnostics around CBMC SAT-backend quantifiers by detecting CBMC “ignoring forall/exists” messages, tracking how many quantifier expressions were dropped, and emitting a prominent warning so users don’t mistake vacuous assumes (or spurious assert failures) for reliable results.
Changes:
- Add parsing/counting of CBMC “ignoring forall/exists” messages and plumb the count into
VerificationResult. - Render a prominent, multi-line warning when dropped quantifiers are detected.
- Add a new expected test that pins the dangerous “vacuous assume” scenario and asserts the warning is emitted.
Reviewed changes
Copilot reviewed 4 out of 5 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| tests/expected/quantifiers/ignored_quantifier_warning.rs | New regression test harness that triggers a symbolic-bound quantifier being dropped. |
| tests/expected/quantifiers/ignored_quantifier_warning.expected | Expected output asserting the new prominent warning is printed. |
| kani-driver/src/call_cbmc.rs | Counts ignored-quantifier messages and renders a warning via VerificationResult. |
| Cargo.lock | Updates locked charon version (appears unrelated to the PR’s stated scope). |
Suppressed comments (1)
kani-driver/src/call_cbmc.rs:461
- The ignored-quantifier warning is appended after
format_result/format_coverage, which already ends with the finalVERIFICATION:- ...line. This means the warning currently prints after the overall status line (and with an extra blank line), but the new expected test output places the warning beforeVERIFICATION:- ...so it’s not missed on successful runs.
if self.ignored_quantifiers > 0 {
result.push('\n');
result.push_str(&ignored_quantifiers_warning(self.ignored_quantifiers));
}
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
… verdict Three fixes to the ignored-quantifier warning change: - Add the new `ignored_quantifiers` field to the two `VerificationResult` literals in `sarif.rs`'s test module. Without them `cargo test`/ `cargo clippy --tests` fail to compile (`missing field ignored_quantifiers`), which is what broke the clippy-check and the kani-driver unit tests in the regression job. - Rename the regression test from `ignored_quantifier_warning` to `dropped_quantifier_warning`. compiletest skips any test whose path contains "ignore" (see `tools/compiletest/src/header.rs`), so the test was silently ignored and never actually ran. - Render the warning immediately before the `VERIFICATION:- ...` line rather than after it, so a reliability warning is not missed when the run otherwise reports success (this also matches the order in the `.expected` file). Falls back to appending when there is no such line (e.g. coverage output). Signed-off-by: Felipe Monteiro <felisous@amazon.com>
Commit 65c183c ("Warn prominently when the solver backend drops quantifiers") inadvertently swept in a stale charon submodule pointer (607f5683 -> dee66030, a downgrade from 0.1.88 to 0.1.73) and the matching Cargo.lock change. These are unrelated to the quantifier warning feature. Restore charon to 607f5683 / 0.1.88.
…ntifiers-fixes # Conflicts: # kani-driver/src/call_cbmc.rs
When CBMC's SAT backend cannot encode a quantifier with non-constant bounds, it drops it and replaces it with an unconstrained value. A `kani::assume` containing such a quantifier is then silently not enforced, so a "SUCCESSFUL" verdict can be vacuous -- an unsound false negative, which Kani must never produce. Instead of only printing a warning, force the verification to FAIL (VerificationStatus::Failure / FailedProperties::Error) when any quantifier was dropped, and render an error directing users to an SMT solver backend that supports quantifiers, e.g. `#[kani::solver(z3)]`. Also: - Fix a merge-integration bug: schema_utils_test.rs constructed VerificationResult without the `ignored_quantifiers` field, breaking the test build. - Rename the dropped_quantifier_warning expected test to dropped_quantifier_error and update it to assert VERIFICATION:- FAILED. - Document the solver-backend limitation in the quantifiers reference.
Member
|
Behavior change (experimental @tautschnig do you agree to merge it with this new behavior? |
feliperodri
changed the title
feliperodri
approved these changes
Aug 14, 2026
feliperodri
pushed a commit
to tautschnig/kani
that referenced
this pull request
Aug 25, 2026
Arguments of type &[T], &mut [T] and Vec<T> whose element type is a primitive integer or float are now supported, generated UNBOUNDED: the new optional (alloc-requiring) models allocate nondeterministic-size storage, so verification results hold for ALL lengths. Functions that iterate over the data surface insufficient loop bounds as visible unwinding-assertion failures rather than silently bounded successes. Mutable slices are exclusive by construction (each call leaks a fresh allocation); Vec uses from_raw_parts with capacity matching the allocation layout and frees on drop (ZST elements use the documented dangling-pointer pattern, loop-free). Element types are restricted to those where raw nondeterministic memory needs NO validity assumption (every bit pattern valid): the companion SliceValidityAssume hook, lowered directly to pure quantified goto expressions, exists for niched element types (bool, NonZero*), but CBMC's SAT backend only instantiates constant-bound quantifiers and silently drops symbolic-bound ones (see model-checking#4719), so those element types remain unsupported until the in-progress CBMC quantifier work lands. Rebased onto the mining-constructor PR (model-checking#4718): folds `unbounded_models` into the `AnyModels` bundle and registers `cfg(kani)` for the library build. Also folds in review-driven hardening: require all three unbounded models present before admitting slice/Vec args in partitioning (so eligibility cannot diverge from generation), verify the resolved model's return type matches the argument type in `instance_for`, and match the `Global` allocator exactly rather than by substring in `vec_elem_ty`. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
feliperodri
pushed a commit
to tautschnig/kani
that referenced
this pull request
Aug 25, 2026
Arguments of type &[T], &mut [T] and Vec<T> whose element type is a primitive integer or float are now supported, generated UNBOUNDED: the new optional (alloc-requiring) models allocate nondeterministic-size storage, so verification results hold for ALL lengths. Functions that iterate over the data surface insufficient loop bounds as visible unwinding-assertion failures rather than silently bounded successes. Mutable slices are exclusive by construction (each call leaks a fresh allocation); Vec uses from_raw_parts with capacity matching the allocation layout and frees on drop (ZST elements use the documented dangling-pointer pattern, loop-free). Element types are restricted to those where raw nondeterministic memory needs NO validity assumption (every bit pattern valid): the companion SliceValidityAssume hook, lowered directly to pure quantified goto expressions, exists for niched element types (bool, NonZero*), but CBMC's SAT backend only instantiates constant-bound quantifiers and silently drops symbolic-bound ones (see model-checking#4719), so those element types remain unsupported until the in-progress CBMC quantifier work lands. Rebased onto the mining-constructor PR (model-checking#4718): folds `unbounded_models` into the `AnyModels` bundle and registers `cfg(kani)` for the library build. Also folds in review-driven hardening: require all three unbounded models present before admitting slice/Vec args in partitioning (so eligibility cannot diverge from generation), verify the resolved model's return type matches the argument type in `instance_for`, and match the `Global` allocator exactly rather than by substring in `vec_elem_ty`. Update existing autoharness .expected tests (slices, bounded, filter) for the new unbounded behavior: `&[T]`/`&mut [T]`/`Vec<T>` of primitive integer/float elements are now generated unbounded (no "(bounded)" marker) and are eligible without --bounded-arguments. In particular vec_sum now overflows u64 with an unbounded Vec (Failure), and filter's no_harness slice/Vec functions are now selected (47 -> 50). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
feliperodri
pushed a commit
to tautschnig/kani
that referenced
this pull request
Aug 26, 2026
…checking#4721) ### Description Stacked on model-checking#4716/model-checking#4717/model-checking#4718 (review only the last commit). Adds autoharness support for `&[T]`, `&mut [T]` and `Vec<T>` arguments with primitive integer/float element types, generated **unbounded**: fresh allocations of nondeterministic size, so verification results hold for **all** lengths. Loops that cannot be fully unwound surface as *visible* unwinding-assertion failures instead of silently bounded successes — the soundness-signaling design validated in the top-500 evaluations (model-checking#3832). - `&mut [T]`: each call leaks a fresh allocation, so the slice is exclusive by construction. - `Vec<T>`: `from_raw_parts` with capacity matching the allocation layout (freed on drop); ZST elements use the documented dangling-pointer pattern (loop-free, as generation code must be). - The models are optional (require `alloc`), following the smart-pointer-model precedent: absent in `verify-std`'s no-core flow, where these argument types simply stay unsupported. - Element scope: only types where raw nondeterministic memory is valid as-is. The companion `SliceValidityAssume` hook (lowered directly to pure quantified goto expressions, bypassing the closure-based quantifier path) exists for niched element types, but CBMC's SAT backend silently drops symbolic-bound quantifiers (model-checking#4719), so `bool`/`NonZero*` elements remain unsupported until the in-progress CBMC quantifier-instantiation work lands — at which point `slice_elem_unbounded_ok` re-admits them. Corpus measurement (top-500, full-stack sweep): zero ICEs; the expected shift of silently-bounded loop successes into visible unwinding failures (http 6→18, prost 0→14, encoding_rs 26→35) with loop-free properties over slices/Vecs verifying for all lengths (covers pin lengths beyond 100,000). ### Testing New `cargo_autoharness_vec_unbounded` test: loop-free accessors pass for all lengths, covers verify large lengths/extreme contents/empty values reachable, a looping consumer pins the visible unwinding-failure contract, and a mutable-slice writer verifies. Constructor/niche/autoderive suites pass. Towards model-checking#3832. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.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.
Description
CBMC's SAT-based backends only support quantifiers with constant bounds (
boolbv_quantifier.cpp's eager instantiation). Akani::forall!/kani::exists!with a symbolic bound reaches the backend's quantifier post-processing, which has no handling: the expression is replaced with unconstrained values, and CBMC reports only a low-visibilitywarning: ignoring forallamong its status messages — which Kani currently swallows entirely.The consequences are severe for usability:
kani::assumecontaining such a quantifier is silently not enforced: the harness may reportVERIFICATION:- SUCCESSFULwhile covering none of the intended property (found while building quantified element-validity assumptions for autoharness slice generation, where the vacuous assume was only caught by a non-tautological probe);kani::assertcontaining one may fail spuriously.This PR detects CBMC's ignoring-quantifier messages in the output parser, counts them on
VerificationResult, and renders a prominent warning after the result (on both successful and failed outcomes), explaining the effect and suggesting#[kani::solver(z3)], which handles these quantifiers (verified: the same harnesses verify correctly, fast, under z3).A proper fix (quantifier instantiation in CBMC's SAT backend) is in progress upstream; this warning closes the silent-degradation window until it lands.
Testing
New expected test pins the dangerous case: a harness that succeeds only because its assertion does not depend on the (unenforced) quantified assumption, with the warning attached. Verified no-warning behavior for constant-bound quantifiers (eagerly instantiated) and under
--solver z3. All quantifier expected tests and kani-driver unit tests pass.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.