Fix --export-json reporting a failed, skipped, or zero-match run as clean - #4732
Open
ivmat wants to merge 3 commits into
Open
Fix --export-json reporting a failed, skipped, or zero-match run as clean#4732ivmat wants to merge 3 commits into
--export-json reporting a failed, skipped, or zero-match run as clean#4732ivmat wants to merge 3 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.
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
1 participant
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.