Repository navigation
Fail verification when the solver backend drops quantifiers - #4719
Merged
tautschnig merged 5 commits intoAug 29, 2026
Merged
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>
Member
Author
Yes, I think that's the right behaviour. |
Merged
via the queue into
model-checking:main
with commit Aug 29, 2026
10bc1ae
34 of 37 checks passed
srivatsansamraj
pushed a commit
to srivatsansamraj/kani
that referenced
this pull request
Sep 24, 2026
## Part A — Normative summary RFC 0015 proposes a consumer contract for Kani's `--export-json <path>` output. The flag shipped in model-checking#4472 behind `-Z unstable-options`. This RFC proposes a dedicated `-Z export-json` gate and a versioned JSON document describing one verification run. The contract defines: - Per-harness outcomes, failed properties, and check and cover results grouped by status. - Tool versions, effective configuration, and harness selection needed to interpret results. - Vacuity predicates and the settings needed to interpret unreachable assertions. - Completeness states, atomic file writes, and rules for missing results, failures, and schema compatibility. Shipped JSON already exposes processed property statuses and unreachable counts. This proposal specifies how consumers should interpret them, including when a successful harness has unreachable assertions and whether the export accounts for every selected harness. The export complements `--sarif`, which reports findings for code-scanning tools. The proposed JSON also includes successful-check counts and cover results. The schema remains unstable. Whether it should replace the shipped v1 shape, and how to resolve the remaining configuration and provenance gaps before stabilization, remain open questions. The RFC example illustrates the proposed schema; it is not captured verification output. This PR changes documentation only. The RFC file contains the complete normative proposal. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- ## Part B — Extended reference (informative — not part of the normative RFC) Part B is informative and is **not part of the normative RFC**. It preserves the longer explanations and implementation notes moved out of the RFC and adds no normative requirements. <details> <summary><b>Read the extended reference</b></summary> # Extended reference (informative) Supporting reference for RFC 0015 / [PR model-checking#4727](model-checking#4727). The RFC contains the proposed contract. This reference preserves explanations, implementation comparisons and deferred-work detail moved out of it; it adds no normative requirements. Interim home: a PR body comment. The explanatory material can later be adapted for the Kani book or implementation documentation. Revision-specific observations below describe those revisions, not a claim that one implementation already emits the entire proposed schema. ## 1. Revisions and illustrative example Source descriptions below use checkout `902daa525`. Historical PoC behavior is qualified by `7b125f1b`; later upstream behavior from model-checking#4717/model-checking#4719 is qualified by `10bc1ae04`. These revisions have different capabilities; the proposed schema is not a description of any one of their emitted files. The RFC output example is **an example of the proposed 0015 document**, for the vacuity case the motivation describes: two ordinary assertions made unreachable by one contradictory `kani::assume`. The PoC at `7b125f1b47e36ca4cc50c4041abeca01912f80f9` contains a synthetic unit test, `export_checks_unreachable_under_contradictory_assume`, that constructs two unreachable assertions and a successful result. It supports the illustrated result semantics, but is not a captured verification run. The RFC's harness, provenance, timings, and JSON are illustrative, not a measured run or verbatim PoC output. That PoC emits flat `kani_version`/`cbmc_version` fields (not the grouped `tools` object) and a boolean `run_complete` (not `run_state`), and lacks `is_bounded` and `configuration.coverage_enabled`. It already has `summary` and all seven totals; this RFC refines their treatment of non-completed harnesses, as specified in the RFC. The marker, warning caps and directory-path validation are proposed changes, not PoC capabilities. At `902daa525`, `--fail-fast` collects a `Result<Vec<_>>` and returns only the failing result on error, discarding other results even if those harnesses completed. The later model-checking#4744 fix retains completed results. Completeness measures reported entries, not which missing harnesses ran. ## 2. Field explanations and warnings **Tool provenance (`tools`).** The `tools` object records the versions of the core tools whose behaviour can change a result: `kani` itself (always known, so never `null`), the `rustc` toolchain `kani-compiler` was built against, and `cbmc`. It is the machine-readable form of the versions Kani already prints, narrowing the gap in [model-checking#2572](model-checking#2572). One rule for the two probed entries: **a version that cannot be determined is `null`, never guessed** — whether the probe binary is missing, refuses `--version`, or prints nothing parseable. (An earlier draft also carried `goto_cc`/`goto_instrument`/`goto_synthesizer` versions and a `solvers[]` array of every resolved solver; those are cut from v1 to keep it to the core — see the "Full tool & solver provenance" future-work item. The solver CBMC actually ran with is still recoverable per harness from `harnesses[].resolved_solver`.) **Harnesses that are not `--harness`-selectable.** An `is_automatically_generated` harness (from `kani autoharness`) cannot be selected by `--harness`/`--exact` at all: `find_proof_harnesses` skips generated harnesses regardless of filter. Its `name` is still reported (a real, unique identifier), but a consumer must not use it as a `--harness` argument when `is_automatically_generated` is `true`. A `#[kani::proof_for_contract]` harness, by contrast, *is* selectable, and its `name` is the harness function's own path — not the target it proves a contract for (that is `attributes.kind.ProofForContract.target_fn`, see §7). **Why not `mangled_name`.** `HarnessMetadata` also carries a `mangled_name` (the harness's name in CBMC's symbol table), but this schema does not export it and it would not serve as a selector: it identifies the harness to CBMC, not to Kani's CLI, and `--harness` does not accept it. `name` (`pretty_name`) is chosen because it is simultaneously human-readable, module-qualified, and directly re-runnable. `checks`/`covers` bucket every included property exhaustively by CBMC status. This partition and `n_properties` cover exactly what they bucket; `code_coverage` (COVERED/UNCOVERED) properties under `--coverage` are outside both and `n_properties` (no dedicated place today), so `n_properties == checks.total + covers.total` holds on a `COMPLETED` harness. `checks.success` is a bare count, unlike every other bucket: successful-check identities are numerous and of little value, whereas `covers.satisfied` names its properties because covers are user-authored and few. Exporting successful-check identities is future work. **The `checks` / `covers` partition criterion.** A property goes into `covers` exactly when `property_id.class == "cover"` (`Property::is_cover_property`, `kani-driver/src/cbmc_output_parser.rs`); every property whose class is neither `"cover"` nor `"code_coverage"` goes into `checks` (including `"assertion"`, which carries ordinary `assert!`/panic checks). This is a syntactic test on the CBMC-assigned class, independent of `status`: a cover-class property carrying a status normally seen among checks (or vice versa) still partitions by `class` and is recorded in that domain's `other[]` array rather than crossing over (see the RFC’s Value domains). `code_coverage`-class properties are excluded from both buckets entirely. **`failed_properties[]` membership.** `failed_properties[]` names exactly the properties in `checks.failure` (`class` is neither `"cover"` nor `"code_coverage"`, with `status == "FAILURE"`), with the full per-property shape rather than `checks.failure`'s bare id list. It does **not** include `checks.error` (an `ERROR` is solver-level "could not determine," bucketed separately — see `failure_kind == "ERROR"`) or any cover-class property (`covers.unsatisfiable` is that bucket's own list). This is why `n_failed == len(checks.failure)` on a `COMPLETED` harness: `n_failed` is `failed_properties.len()`, whose membership *is* `checks.failure`'s. **`warnings`** is empty in the illustrative vacuity example. The synthetic fragment below shows the shape of an untruncated warning, not a captured CBMC message or a warning-size measurement. The `warnings_truncated` field and the `truncated`/`original_chars` pair are this proposal's additions, not emitted by the PoC at `7b125f1b`, which collects warning strings without truncation: ```json { "warnings": [ { "message": "Example warning", "truncated": false, "original_chars": null } ], "warnings_truncated": 0 } ``` `truncated`/`original_chars` replace a `[truncated; N chars total]` suffix inside `message`: a structural field a consumer checks without pattern-matching free text, avoiding the text parsing this RFC argues against. `original_chars` is `null` when `truncated` is `false` (nothing was cut). See “Statistics and truncation” below for what this field does and does not promise. ### Statistics and truncation Symex time, VCC counts and solver time exist only inside CBMC's free-text messages; extracting them requires pattern-matching human-readable output, which causes the fragility this RFC is intended to prevent. `benchcomp` does exactly this today; the right fix is structured data from CBMC, not more scraping. The `warnings` field carries CBMC's messages as non-contractual free text, subject to the caps below: CBMC's `--json-ui` stream tags each message with a `messageType` (e.g. `"WARNING"`), and this schema includes the `WARNING`-typed messages, for example the SAT backend's `warning: ignoring forall` / `warning: ignoring exists`, emitted when it cannot encode a quantifier with non-constant bounds. Later upstream [PR model-checking#4719](model-checking#4719), present at `10bc1ae04` but absent at `902daa525`, explicitly parses these prefixes, counts the ignored quantifiers, and overrides the property-derived result with failure and `FailedProperties::Error`. This internal interpretation does not make warning text a versioned interface: an export consumer treats each message as opaque display text and uses Kani's computed outcome instead of pattern-matching it. Two consequences: - **`warnings` is outside the `schema_version` compatibility guarantees.** The field's presence and its `[{ "message": …, "truncated": …, "original_chars": … }]` shape are contractual; the *contents* of `message` are not, and must not be pattern-matched or assumed stable across versions. - **`warnings` is bounded, with explicit, structural truncation markers.** The PoC collects warning strings without a length or count cap, so it places no fixed bound on their contribution to file size. This proposal caps each `message` at a fixed, implementation-defined length and truncates it on a character boundary, with the fact and extent carried as siblings `truncated: bool` and `original_chars: integer | null` (pre-truncation count, `null` exactly when `truncated` is `false`) rather than a suffix inside `message`. The per-harness `warnings` array is separately capped at a fixed count, with a sibling `warnings_truncated` integer per harness (`0` when nothing was dropped) recording how many *entries* were omitted. A consumer can always tell "no more warnings" from "we stopped recording". These structural fields are schema-versioned; the `message` text is not. ### Warning retention by outcome Warnings do not depend on a property result array: CBMC may emit messages and then crash or be killed. The PoC at `7b125f1b` preserves collected warnings on its no-results crash/OOM path. Its timeout path instead constructs a fresh result with no warnings. The export preserves whatever warnings the driver retains, applying the same caps for every outcome; `[]` means none were retained, not proof that CBMC emitted none. ## 3. Migration inventory The inventory wording below is retained from the longer draft. Its shorthand for per-property detail is inconsistent with that draft’s field tables: successful checks are counts, and `other[]` holds only `{id, status}`. The RFC retains those field-table definitions unchanged. - **Shipped fields dropped or transformed in this shape — keep, drop, or make mandatory?** model-checking#4472's document (`create_metadata_json`, `create_harness_metadata_json`, `process_cbmc_results` in `kani-driver/src/frontend/schema_utils.rs`) carries a number of fields this schema does not restore as-is. Grouped by proposed treatment: - **Dropped, no successor field today:** `build_mode` (`"debug"`/`"release"`); `harnesses[].mangled_name` (see “Why not `mangled_name`” in §2); the source range's `end_line` (only `original_start_line` survives, as `harnesses[].line`); `goto_file` (the generated modeling file path); per-check `description`/`location` for every property, not just the failed and `other`-bucketed ones (the shipped shape records full detail for every check; this schema records identities only for `success`/`unreachable`/`undetermined`/`error`/`unknown`, and full records only for `failed_properties`/`unsupported_constructs`/`other[]`); CBMC's OS banner (`cbmc_metadata.os_info`); and CBMC execution statistics (`cbmc_stats`: symex time, VCC counts, solver time — see "Why is CBMC statistics data excluded?" and the "Per-check timing" future-work item). - **The effective `--object-bits` value stays an open question.** It configures CBMC's pointer-object encoding and is useful verification provenance. The shipped writer already records it per harness at `cbmc[].configuration.object_bits`, resolving either Kani's default or the explicit `--cbmc-args` value. Its source is per-run state, so this schema could restore it under `configuration` or retain a per-harness field. On triage (model-checking#4731) a maintainer (feliperodri) classed it niche relative to `is_bounded`. Leaving it dropped is a provenance gap: adopting this RFC should file (or update) a tracking issue for its representation, resolved before or as part of stabilization. - **The Cargo provenance `project.workspace_root` / `output_dir`, and `harnesses[].file`'s base directory.** `harnesses[].file` is written relative to the invocation directory (`std::env::current_dir()`), not any field this document carries; for a `cargo kani` run from the workspace root the two coincide, but for a standalone `kani-driver` invocation or a script that `cd`s first they need not. Restoring `workspace_root` (or defining `file` as workspace-relative) makes `file` resolvable by a consumer that does not trust the launch directory. `--target-dir` does affect `output_dir`: Cargo builds derive it as `<target-dir>/kani/<triple>/debug/deps` (using Cargo's target directory when the flag is absent). It can stay dropped as an artifact-location field, but cannot be assumed to use the default path. - **`is_ctor_based`** is absent from `HarnessMetadata` and the shipped writer at `902daa525`, but present in both at later upstream `10bc1ae04`. There it records constructor-based generation or mined-invariant filtering: success covers only values admitted by that mechanism. This is a soundness-relevant restriction, independently of `is_bounded`. Its representation remains open in this draft, but support for exporting these harnesses must carry the restriction explicitly before stabilization; omitting it cannot justify reading their results as unrestricted proofs. ## 4. Configuration explanations and implementation inventory **`configuration.checks.assertion_reach_checks`.** Whether Kani inserted reachability checks ahead of ordinary assertions (`true` unless `--no-assertion-reach-checks` was passed). With reach-checks off, an assertion made unreachable by a contradictory `kani::assume` is recorded in `checks.success` instead of `checks.unreachable`, silently preventing the vacuity indication this schema provides; `configuration` records exactly such toggles that change how a result must be read. **`configuration.checks.ignore_global_asm` and `.extra_pointer_checks`.** Two more flags recorded for the same reason. `ignore_global_asm` mirrors `--ignore-global-asm`: when `true`, Kani did not error on `global_asm!`, so any behavior reachable only through that inline assembly is absent from the model and a proof can pass vacuously with respect to its effects. `extra_pointer_checks` mirrors `--extra-pointer-checks`: when `true`, Kani adds obligations for invalid pointers in relational operations and pointer-arithmetic overflow, so two runs differing only in this flag check different property sets, and `checks.total`/`checks.success` are not comparable between them. **`configuration.checks.memory_safety`, `.overflow`, `.unwinding`, and `.undefined_function`.** The remaining four `checks` bools, each mirroring a `--no-*-checks` flag (all default `true`; the field name records the check being *on*, not the flag that turns it off): - `memory_safety` mirrors `--no-memory-safety-checks` (and `--no-default-checks`, the whole group). `false` leaves out-of-bounds accesses and invalid-pointer dereferences unchecked; such a run can pass while containing the memory-safety bugs Kani is intended to detect. - `overflow` mirrors `--no-overflow-checks`. `false` omits CBMC's NaN check and disables its division-by-zero check. It does **not** disable Rust/MIR arithmetic-overflow or integer division-by-zero assertions: Kani still compiles with `-C overflow-checks=on` and emits those MIR assertions (subject separately to `prove_safety_only`). - `unwinding` mirrors `--no-unwinding-checks`. `false` stops CBMC asserting the loop/recursion bound covered every execution, so a bounded proof can silently miss behavior past the bound. - `undefined_function` mirrors `--no-undefined-function-checks`. `false` skips Kani's generation of `assert-false-assume-false` bodies for undefined functions. Calls remain, with CBMC's default nondeterministic-return behavior; this does not model their possible side effects. **`configuration.checks.assert_contracts` and `.prove_safety_only`.** These flags change generated checks and assumptions, and therefore what a successful result establishes: - `assert_contracts` mirrors `--no-assert-contracts` (`true` unless it was passed; it requires `-Z function-contracts`). When `false`, ordinary calls to contracted functions use `ContractMode::Original`: the original body executes and its contract instrumentation is omitted (`kani_middle/transform/contracts.rs`). The contracts are neither asserted nor assumed, so success does not establish those contract obligations. Explicit `proof_for_contract` checking and `stub_verified` replacement modes take precedence and retain their respective instrumentation. - `prove_safety_only` mirrors `--prove-safety-only` (default `false`; requires `-Z unstable-options`). When `true`, `codegen_assert_assume` emits only an assumption for `PropertyClass::Assertion`. This includes ordinary user assertions and panic checks; success is conditional on those assumptions, not evidence that the converted assertions hold. Direct `codegen_assert` calls remain checks, including the internal `CheckHook`'s `Assertion`-class properties. The conversion is specific to the code-generation path, not every property with that class. All nine meet the same "changes which properties are generated, or what a status means" test. **Partial inventory of `VerificationArgs` (at `902daa525`).** Recorded directly: the nine `checks` bools, `coverage_enabled`, and `cbmc_args`. Recorded elsewhere in the document, so not duplicated here: `-Z` features that add or remove properties (`uninit-checks`, `function-contracts`, `loop-contracts`, `mem-predicates`, `quantifiers`, `stubbing`) are visible by name in `enabled_unstable_features`; `--unwind`/`--default-unwind` in per-harness `resolved_unwind`, resolved in the order CLI `--unwind` > harness `#[kani::unwind]` > `--default-unwind` (`is_bounded` instead describes autoharness argument generation); `--solver` in the per-harness `resolved_solver`; `--harness-timeout` in `harness_timeout_s` and the per-harness `outcome.kind`. This inventory is **incomplete**: `--synthesize-loop-contracts` transforms each goto model before CBMC, while `-Z restrict-vtable --no-restrict-vtable` disables virtual-call restriction without changing the recorded `-Z` feature set. Neither effective setting is represented in the proposed fields. Their representation and the rest of the inventory must be resolved under the policy before stabilization; `cbmc_args` does not capture Kani-generated options. The proposed exclusion of `--randomize-layout [seed]` is a scope choice: it changes the *program under test* (type layout), so its seed belongs in a future subject/provenance block. Presentation and execution options also need individual treatment: regular/terse output controls rendering, but `--output-format=old` uses mock results and is rejected with export. At `902daa525`, `--quiet` suppresses the failure exit in `print_final_summary`, so a failed harness can be exported as failed while Kani exits 0. That is a driver bug, not a different verification verdict. `--jobs` changes concurrency and can affect resource outcomes and which results exist under fail-fast; `--concrete-playback` changes trace generation and formula slicing as well as producing tests. These options cannot all be classified as affecting only presentation. Future flags must be assessed under the same policy in the PR that adds them. **`configuration.coverage_enabled`.** Mirrors `--coverage` (mandatory bool, default `false`). It causes `code_coverage` (`COVERED`/`UNCOVERED`) properties to exist; these are excluded from `checks`, `covers`, and `n_properties`, so it meets the `configuration` policy, and without it a consumer cannot tell "no coverage properties in this schema yet" from "`--coverage` never passed." It sits alongside `checks.*`, not nested under it. The configuration policy itself remains in the RFC. ## 5. Deferred provenance and memory work - **Full tool & solver provenance beyond `kani`/`rustc`/`cbmc`.** An earlier draft of this schema recorded `goto_cc`/`goto_instrument`/`goto_synthesizer` versions and a `tools.solvers[]` array of `{name, version}` per resolved solver (the shape the shipped model-checking#4472 writer already emits), plus a proposed `source: "builtin"|"external"` discriminator (this schema's own addition, not part of model-checking#4472) to disambiguate a `null` version. Cut from v1 to keep it to the core (per [model-checking#4731](model-checking#4731)): probing the extra tools' and external solvers' `--version` spawns a process per tool beyond the probes v1 already needs, and the solver CBMC ran with is already recoverable per harness from `harnesses[].resolved_solver`. A follow-up can restore the fuller `tools.solvers[]` block if a consumer needs the solver *binary* versions. **File a tracking issue on adoption.** - **Host machine environment (`machine`).** An earlier draft carried `machine.cpu_count`, `.total_memory_bytes`, `.memory_limit_bytes`, `.os`, `.arch`. Cut from v1: environment metadata that helps triage performance/OOM but is not needed to reproduce a verdict. A follow-up can reintroduce a `machine` block if performance-oriented consumers ask for it. **File a tracking issue on adoption.** - **Per-check timing and resource data.** Used elsewhere (GNATprove reports per-obligation prover data), but not available from CBMC's structured output today. - **A machine-reproducible counterexample.** `--concrete-playback` already derives a concrete value vector; exposing it would let a consumer reproduce a failure without modifying source. - **A finer failure classification.** Kani computes whether a failure involved unwinding assertions or reachable undefined functions, then collapses them; separating them would let a consumer tell "raise `--unwind` and retry" from "fix the code". - **A harness-level triviality signal**, aggregating what RFC 0003 already identifies as the vacuity concern. - **Aggregate coverage**, deferring to `kani-cov` and RFC 0011. - **The contract trust chain.** A harness using `stub_verified` is sound only if the contract's own proof passed. Kani already enforces at compile time that such a harness exists; because this schema records both relationships, a consumer can check the run-time condition itself today, and Kani could report the resolved status later. - **Per-harness peak memory.** A `getrusage(RUSAGE_CHILDREN)`-based approach was prototyped and rejected: `ru_maxrss` is a process-wide running *maximum*, not a per-child figure, so the result is order-dependent (only a harness whose peak memory exceeds that of every earlier harness gets a value; a later one with a lower peak reads `null` even under memory pressure) and is not attempted under `--jobs`, where the counter is shared across siblings. An accurate figure needs per-child accounting (e.g. `wait4()`-based rusage per child, or a per-child cgroup with its own `memory.peak`), which this schema does not attempt. Kani infers OOM from the **CBMC child's** status 137 when no property result array is available, and this schema exposes that inference as `outcome.kind == "OUT_OF_MEMORY"`. Kani normally exits 1 for the failed harness, not 137; at `902daa525`, the `--quiet` bug can instead leave its exit code at 0. ## 6. Failure and completeness explanations **Failure scenarios.** - The output path is not writable → reported as an error with a non-zero exit, never silently ignored. The verification *verdict* is computed independently and never rewritten by an export problem. The up-front marker write fails before verification starts; the terminal export runs after the harness verdicts but *before* the SARIF artifact and final summary line, so a terminal export failure aborts those remaining steps. (Whether it should suppress the SARIF write is an implementation question, not settled here.) - Any `tools.*` version cannot be determined → that field is `null`, never guessed; see "Tool provenance" above. - A harness times out, is OOM-killed, or CBMC crashes on it → that harness's `outcome.kind` (`TIMEOUT`/`OUT_OF_MEMORY`/`CRASHED`) records it and the file is still written. Run completeness is *verdict-independent*: as long as every selected harness has an entry in the terminal document, `run_state` is `COMPLETE` (a suite where every harness times out is complete accounting for unsuccessful verification attempts). `PARTIAL` means the terminal document lacks some selected harness results; `INCOMPLETE` means only the marker was published. - Kani itself crashes (a `kani-compiler` ICE, a panic in `kani-driver`, a `SIGKILL`) → no terminal document is written: the single terminal write happens once at the very end (`verify_project`), and any hard error before it unwinds past it. There is no run-level `"CRASHED"` value; all that remains is a stale `INCOMPLETE` marker (or, if the crash preceded it, whatever file already existed). See "How `run_state` and `outcome.kind` co-occur" below. - The `--export-json` path already holds a file → it is **overwritten up front with an atomic `run_state: "INCOMPLETE"` marker** once harness verification begins (after the crate is built), so an earlier run's results cannot be misread as this run's, and a run that terminates after that without finishing leaves a file that records that it did not finish (replacing an earlier delete-up-front design; see the RFC’s completeness contract and open question). - The parent directory does not exist → it is created (`create_dir_all`), matching `--sarif`. A path that is itself an existing directory fails today only when the write is attempted (the same-directory temp write cannot be created inside a file-shaped target); adopting this RFC moves that to the argument-parse-time rejection proposed under *Interaction with other flags*, so the failure occurs before any verification work, as for `--sarif`. The shipped difference is an accident of implementation order, not intentional. **How `run_state` and `outcome.kind` co-occur.** `outcome` is meaningful only once Kani reaches a terminal write, and at run level its `kind` has exactly one value: `COMPLETED`. The marker (`run_state == "INCOMPLETE"`) is written *before* that and carries no `outcome`. A run-level `outcome.kind == "CRASHED"` does not exist (see the crash scenario above); what a consumer observes instead is a stale `INCOMPLETE` marker, or a missing file. The crash indication is that staleness rather than a field value. Every producible combination: | `run_state` | `outcome` | |---|---| | `INCOMPLETE` (marker) | absent | | `COMPLETE` | `{"kind": "COMPLETED"}` | | `PARTIAL` | `{"kind": "COMPLETED"}` | | `NO_HARNESSES_SELECTED` | `{"kind": "COMPLETED"}` | Per-harness `outcome.kind == "CRASHED"` is unaffected and remains possible: the run can finish, reach its terminal write, and report that CBMC crashed on one harness. This describes one harness in a completed document, distinct from Kani never reaching the write. **`NO_HARNESSES_SELECTED` means exactly one thing: an unfiltered run of a selected project or workspace with no selectable harness** (no `#[kani::proof]`, or under `autoharness` no eligible function). It cannot arise from a `--harness` filter: a filter set that matches nothing — and, with `--exact`, any single filter that matches nothing — is rejected at harness selection (`no_harness_match_error` in `kani-driver/src/metadata.rs`, since model-checking#4743) with a non-zero exit. Harness selection precedes the `INCOMPLETE` marker write and every export, so that case produces **no document at all**, not a terminal document with a non-empty `requested_filters`. Hence in a `NO_HARNESSES_SELECTED` document `harness_selection.requested_filters == []`, `unmatched_filters == []`, and `matched_count == 0`. `unmatched_filters` is non-empty only in a `COMPLETE`/`PARTIAL` document written without `--exact`, where at least one filter matched and the named ones did not. **Cover-only vacuity is not detected by this schema alone.** The RFC’s normative and advisory vacuity predicates read only `checks.*`; an `unreachable` *cover* is recorded in `covers.unreachable` and satisfies neither. A consumer wanting the corresponding indication for covers should additionally apply `covers.total > 0 && covers.unreachable.len() == covers.total` per harness, since this schema does not apply it for them. `null` always means *not measured or not applicable*, never a guess, and is always distinguishable from `0`, `false`, and `[]`. ## 7. Casing and requested versus resolved values **Casing.** The file mixes three conventions, and one rule explains all three: *a value keeps the serialization of the Rust type it comes from, and this schema does not fork types to re-case them.* - **snake_case keys**, because the schema reuses `kani_metadata` and `cbmc_output_parser` types directly (`HarnessAttributes`, `AssignsContract`, `CheckStatus`); re-casing would fork those types, recreate the duplication problem in [model-checking#3541](model-checking#3541), or break existing `.kani-metadata.json` consumers. Those three already derive `Serialize`; but `Property`, `PropertyId`, and `SourceLocation` derive only `Deserialize` (never serialized out), so `failed_properties[]`/`unsupported_constructs[]`/`checks.other[]`/`covers.other[]` are purpose-built export structs rather than a direct embedding of `Property`. - **SCREAMING_SNAKE_CASE enum values** (`outcome.kind`, `verdict`, `failure_kind`, `run_state`, every `status`), mirroring the reused CBMC-status types (`CheckStatus`, `FailedProperties`); the new enums (`Outcome`, `verdict`, `run_state`) use it too, so a consumer sees one value convention across the file. (Multi-word values like `NO_HARNESSES_SELECTED` need an explicit `SCREAMING_SNAKE_CASE` rename, since `CheckStatus`'s `UPPERCASE` coincides with it only for single-word variants.) - **PascalCase, object-shaped**, for the two embedded `kani_metadata` attribute enums below, which keep their own serde derivation untouched for the same no-forking reason. **Fields that are not always strings.** Two reused `kani_metadata` enums have non-unit variants and so serialize as *objects*, not strings: - `harnesses[].attributes.kind` is `"Proof"` or `"Test"`, but `{"ProofForContract": {"target_fn": "…"}}` for a contract-proof harness. - `harnesses[].attributes.solver` is `"Cadical"`, `"Z3"`, etc. for a named solver, but `{"Binary": "…"}` for a custom solver path. These are the *requested* attributes, carried verbatim from `.kani-metadata.json`; the resolved counterparts (`resolved_solver`, `resolved_unwind`) are plain scalars (a string or number, or `null`), never the object forms above. **Reconciling the two solver spellings.** `attributes.solver` is the *requested* value in `CbmcSolver`'s PascalCase (`"Cadical"`, or `{"Binary": "<path>"}` for a custom solver); `resolved_solver` is the lowercase built-in name or custom binary path CBMC actually ran with. Effective precedence is the last solver-selecting `--cbmc-args` override > CLI `--solver` > harness attribute > default: Kani appends `cbmc_args` after its own solver flags. Bare `--smt2` leaves the choice to CBMC and yields `null`. Compare `attributes.solver` against `resolved_solver` for "asked for" vs "ran". This proposal follows `kani list` by recording tool version and schema version in separate fields; see the RFC’s **Compatibility policy**. </details> --------- 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
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.