Fix --export-json reporting a failed, skipped, or zero-match run as clean - #4732
Closed
ivmat wants to merge 5 commits into
Closed
Fix --export-json reporting a failed, skipped, or zero-match run as clean#4732ivmat wants to merge 5 commits into
--export-json reporting a failed, skipped, or zero-match run as clean#4732ivmat wants to merge 5 commits into
Conversation
…lete Close several ways a run that did not finish cleanly could still serialize as a clean, completed export: - A run reusing an --export-json path that died before the final write (compile error, OOM, Ctrl-C, or a harness-level error propagating out) left the *previous* run's complete-looking file at the target. verify_project now writes a run_state:"incomplete" marker to the target before verification starts, so a stale file can never be read as this run's result; the marker is promoted to "complete" only when the run finished. - A --harness filter that matched nothing wrote a completed / 0-failed document (the "no harnesses matched" error is only raised after the export). A zero-match run is now marked run_state:"no_harnesses_selected", and a harness_selection block records the requested filters, the matched count, and any unmatched filters. - Under --fail-fast, harnesses skipped after the first failure kept their harness_metadata entry but had no error_details/property_details entry, so a consumer correlating the arrays could read absence as success. Every selected harness now gets an explicit entry, and the terminal run_state is "complete" only when every selected harness produced a result, "partial" otherwise. - Per-harness details were joined to results on pretty_name, which two harnesses in different crates of a workspace can share, misattributing a result. The join now uses the unique mangled_name. Follow-up to model-checking#4472.
…erflow-safe The scraped CBMC statistics could be silently wrong: - A later status message that matched a recognized label but failed to parse overwrote an already-recorded valid value with null (indistinguishable from "not measured"). Parsing now only assigns on success and never clobbers a valid value. - Exact-suffix matching turned any harmless CBMC wording change into a silent null. Counts now parse the leading numeric token, tolerating trailing text. - record_seconds extracted the leading number regardless of unit, so a duration reported as "5ms" would be recorded as 5 seconds. It now accepts a value only when the unit is exactly "s"; any other unit is a parse failure, never a mis-scaled number. - The integer count fields were u32; a large enough run overflowed to null. Widened to u64. Follow-up to model-checking#4472.
The shipped validator checked structure but not values or semantics, so a structurally well-formed document that misreported -- failed:-1, successful:"yes", executed disagreeing with results, or run_state:"complete" with empty results -- validated as OK. It now checks leaf value types, non-negative and reconciled summary counts, and the run_state enum and its invariants, with a validator-negative test suite covering each. run_state and harness_selection are added to the schema template so their presence is required. Follow-up to model-checking#4472.
A standalone (non-Cargo) run has no workspace root, so `project.workspace_root` is legitimately null. The strengthened leaf-type validation rejected that null as a type mismatch against the string in the schema template, failing the json-handler exec tests on every standalone harness. Mark the field _nullable so a null is accepted while a wrong non-null type is still rejected.
The strengthened leaf-type validation rejected the nulls that --export-json emits on ordinary degraded runs: unmeasured per-harness property counts (a timed-out or OOM'd harness reports them as null, not zero, so a degraded run is not mistaken for "nothing failed"), partial cbmc_stats, an --smt2 run that names no solver, and unavailable tool/CBMC versions. Mark those leaves _nullable in the schema template so a null is accepted while a wrong non-null type is still rejected, and extend the validator test with degraded-run fixtures (and a null-in-a-required-field fixture that must still be rejected).
feliperodri
requested changes
Aug 13, 2026
feliperodri
left a comment
feliperodri
left a comment
Member
There was a problem hiding this comment.
This PR contradicts its own RFC #4727... We shouldn't merge it until RFC 0015 lands with my requested changes. It's a one-way door and it's currently being decided in follow-up PRs rather than the RFC itself. I added all my concerns to #4731.
The PR adds run_state ∈ {incomplete, no_harnesses_selected, partial, complete} and a harness_selection block to the #4472 schema. #4727 specifies a different vocabulary for the same information: schema_version, outcome.kind, outcome.verdict, failure_kind... and a different mechanism for the stale-file problem: temp-file-plus-rename so that "file exists implies complete," plus the up-front delete. That's the paragraph I called the best part of the RFC... This PR implements an in-band "incomplete" marker instead, written non-atomically.
The real bugs are in the wrong layer. Three of the four behavioral fixes patch the JSON writer instead of the thing that's broken:
- Zero-match should fail in determine_targets, before codegen, before any export. And there's a bigger bug hiding behind it:
print_final_summaryearly-returns on quiet before reaching the bail, so reading the code,kani --quiet --harnesstypo skips the "no harnesses matched" error entirely and exits 0. No test covers that combination. That affects every user and every CI that uses the exit code, not just JSON consumers and fixing it indetermine_targetsmakes issue item 2 disappear for free. (I did not build Kani to execute this; it's a code-path reading of harness_runner.rs:265 and metadata.rs:112.) --fail-fast— root cause iscollect::<Result<Vec<_>>>()short-circuiting and discarding already-completed Ok results (harness_runner.rs:105), see #4729. This PR doesn't fix it; it labels the lost harnesseshas_errors: true,error_type: "not_reported"asserting an error for a harness that may have passed. That trades one false statement for another, and the text summary and SARIF still under-report. Fix #4729 and item 3 is moot.harness_id— the PR moves the join predicate tomangled_namebut explicitly keeps emittingharness_id: pretty_name. The consumer-facing ambiguity it was filed to fix is still there.
ALSO... maintenance... 98 added comment lines to 125 added Rust lines. The comments narrate reasoning in first person in the tree. "I should note this was partly self-inflicted", "the honest, disjunctive truth", multi-paragraph justifications above three-line functions (likely AI slop). Some of that is already in main from #4472's rescue commits. It will rot the moment 0015 reshapes the schema, and it's the kind of prose a future contributor won't dare touch.
Contributor
Author
|
closing this PR, we go with plan from #4731. you are right, this PR is incomplete, sloppy and not aligned with atomic write design. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Follow-up to #4472. While using
--export-jsonas a CI pass/fail oracle I hit several cases where the exported file did not faithfully represent the run — a run that failed, was skipped, matched nothing, or wasn't fully measured could be read as a clean, complete pass by a consumer that trusts the file (which is the point of the file). This addresses them:verify_projectnow writes arun_state:"incomplete"marker to the target before verification, promoted to"complete"only when every selected harness produced a result — so a run that dies before finishing can't leave a previous run's clean file to be read as this run's result.completed / 0-faileddocument (the "no harnesses matched" error is only raised after the export). It's now markedrun_state:"no_harnesses_selected", with aharness_selectionblock recording the requested filters, matched count, and any unmatched filters.--fail-fast. Harnesses skipped after the first failure kept theirharness_metadataentry but had noerror_details/property_detailsentry, so a consumer correlating the arrays could read absence as success. Every selected harness now gets an explicit entry, andrun_stateis"partial"when some selected harnesses didn't run.mangled_namerather thanpretty_name, which two crates in one workspace can share.cbmc_stats. Parsing no longer clobbers a valid value withnullon a later malformed line, tolerates harmless CBMC wording changes, rejects a duration reported in the wrong unit rather than mis-scaling it, and widens counts tou64.scripts/validate_json_export.pypreviously checked structure only, sofailed:-1orsuccessful:"yes"passed. It now checks leaf value types, count reconciliation, and therun_stateenum and its invariants, with avalidator-negativetest suite;run_state/harness_selectionare added to the schema template so their presence is required.Rationale and the per-case scenarios are in #4731. One case from that report — a partial, non-timeout CBMC exit — is left as follow-up pending confirmation, and is not addressed here.
Testing:
cargo test -p kani-driver(incl. newcall_cbmc/validator unit tests),clippy -D warnings, andfmtare clean; thevalidator-negativesuite rejects the malformed fixtures. The compiletesttests/json-handler/*integration tests (which require CBMC) were not run in my environment, so the new validator leaf-type checks have been exercised against synthetic and reference fixtures but not yet a live CBMC-generated export.