Repository navigation
Fail a zero-match harness filter before codegen and export - #4743
Merged
Merged
Conversation
A `--harness` filter that matches no harness only fails in the final summary. `--quiet` skips that summary, so the run exits 0. With `--export-json`, the run also writes a file that reports a clean, empty run. Bail out in `determine_targets` instead. This runs before codegen and before any export. The final-summary check stays as a last guard for paths that skip harness filtering. Add a script-based regression test covering the `--quiet` exit code, the absent export file, and the several-filters error message. Resolves the first driver bug from model-checking#4731.
feliperodri
added
the
[I] Refactoring / Clean Up
Contributor
There was a problem hiding this comment.
Pull request overview
Moves zero-match harness-filter validation earlier so failed selections exit non-zero before verification or JSON export.
Changes:
- Rejects empty filtered harness sets with existing error wording.
- Updates JSON export documentation.
- Adds regression coverage for quiet mode, export suppression, and multiple filters.
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
kani-driver/src/metadata.rs |
Adds early zero-match validation. |
kani-driver/src/main.rs |
Updates empty-export commentary. |
tests/script-based-pre/harness_filter_no_match/no_match.sh |
Tests failure and export behavior. |
tests/script-based-pre/harness_filter_no_match/no_match.expected |
Defines expected test output. |
tests/script-based-pre/harness_filter_no_match/fixture.rs |
Provides a proof-harness fixture. |
tests/script-based-pre/harness_filter_no_match/config.yml |
Registers the script-based test. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
feliperodri
approved these changes
Aug 18, 2026
feliperodri
reviewed
Aug 18, 2026
feliperodri
reviewed
Aug 18, 2026
feliperodri
reviewed
Aug 18, 2026
feliperodri
enabled auto-merge
August 18, 2026 17:33
Extract the zero-match filter error into `no_harness_match_error` and use it from both `determine_targets` and the summary-stage guard, so the two sites cannot drift. The wording unifies with the `--exact` message. The summary-stage arm now carries its narrowed scope: `determine_targets` fails a zero-match filter before codegen, so the arm only guards paths that skip harness filtering. Tests that pinned the old wording are updated.
auto-merge was automatically disabled
August 18, 2026 19:01
Head branch was pushed to by a user without write access
Merged
via the queue into
model-checking:main
with commit Aug 21, 2026
46aa1a9
39 of 42 checks passed
ivmat
added a commit
to ivmat/kani
that referenced
this pull request
Sep 8, 2026
- configuration: add checks.assert_contracts and checks.prove_safety_only, the two shipped flags that weaken what a SUCCESS means without changing which properties exist; record the audit of VerificationArgs under the configuration policy (what is recorded where, what is excluded and why). - NO_HARNESSES_SELECTED: since model-checking#4743 a --harness filter that matches nothing is an error before the marker write and any export, so the state denotes only an unfiltered crate with no selectable harness; requested_filters is empty there and unmatched_filters is never the whole filter set. - Stabilization: drop the benchcomp migration prerequisite; its parser needs CBMC statistics this schema excludes by design, so it moves in the statistics follow-up, not before -Z is lifted.
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.
A
--harnessfilter that matches no harness only fails in the end-of-run summary.--quietskips that summary, so the run exits 0. With--export-json, the run also writes a file that reports a clean, empty run.This PR moves the zero-match check into
determine_targets, before codegen and before any export. The error is built by one shared helper, used by both the pre-codegen check and the summary-stage guard, and its wording is unified with the--exactmessage. The summary check stays as a last guard for paths that skip harness filtering.Testing: a new script-based test covers the
--quietexit code, the absent export file, and the several-filters message. The test fails onmainand passes with this change.cargo test -p kani-driver,rustfmt, andclippyare clean.First of the two driver fixes agreed in #4731.