Repository navigation
Conversation
RFC 0015 says an earlier --export-json file is replaced by an INCOMPLETE marker when verification begins, so a killed run cannot leave an older COMPLETE document that looks current. Kani now builds the run context once after harness selection, writes the marker atomically, and then replaces it with the terminal document from the same context. A failed marker write stops the run before any harness is verified. The new json-handler/incomplete-marker test blocks a fake cbmc, then kills the driver (the marker stays) or releases it (the terminal document keeps the marker's fields), and checks a bad export path and a rejected harness filter.
Adds end-to-end tests for `--export-json` and fixture-based tests for the reading-rule helpers. The end-to-end tests run `kani` or `cargo kani` and check exported documents or rejected requests. Only `structured-warnings` substitutes a CBMC wrapper, which injects warnings or simulates non-completed outcomes. Gate-rejection and no-harness cases do not reach verification. New suites: - additive-output: checks that `--export-json` preserves exit status and SARIF output for one passing and one failing harness, and preserves stdout and per-harness `--output-into-files` output after masking runtime and verification-time lines; `-` names a file. - autoharness-export: `kani autoharness --bounded-arguments` exports `is_automatically_generated` and `is_bounded` per harness. - gate-rejections: argument errors are reported before compilation and leave an existing file or directory at the target untouched. - jobs-ordering-stable: checks that `harnesses[]` is sorted by (crate_name, file, line, name) and matches between `--jobs 4` and `--jobs 1` after excluding `resources.verification_time_s`. - live-configuration: unwind and solver precedence, verbatim cbmc_args, bare `--smt2`, `--coverage` and the check-flag toggles. - multi-crate-export: one document for `cargo kani --workspace`, with same-named harnesses in two crates kept apart by crate_name. - no-harnesses-selected: `run_state` NO_HARNESSES_SELECTED with zero counts. - structured-warnings: warnings[] caps and exact record text, the ignored-quantifier ERROR classification, and the CRASHED, TIMEOUT and OUT_OF_MEMORY shapes and elapsed times, against a fake `cbmc`. - vacuity-check: the vacuous_pass and vacuity_suspect predicates on live exports, with and without reach checks. Existing tests changed: fail-fast (a completed harness survives the abort; PARTIAL versus COMPLETE), multiple-harnesses (`matched_count` and `run_state`) and script-based-pre/harness_filter_no_match (checks that an unmatched filter reports an error under `--quiet`; a separate run with `--export-json` checks that the existing target file remains unchanged). validate_json_export.py gains five helpers. vacuity-check imports two of them, vacuous_pass and vacuity_suspect. The other three are reading-rule helpers that only check_fixtures.py uses: cover_only_vacuous, warnings_shape_equivalent and join_key, which warnings_shape_equivalent uses. schema-validation tests all five directly on a new fixture, fixture-completed-success.json.
- live-configuration: compare each exported resolved_solver with the solver line CBMC prints, and remove the kanicov_* directory that --coverage writes next to the fixture. - vacuity-check: add a partly vacuous harness (vacuous_pass false, vacuity_suspect true), check vacuity_suspect on the contradictory assume, and check that without reach checks its assertions are reported as successes. Drop the unneeded -Z unstable-options. - gate-rejections: a compilation error leaves an existing export file unchanged; --no-codegen and -Z lean are rejected with --export-json. - fail-fast, multiple-harnesses: restore the comments this branch had removed; drop a check that the exact counts already imply. - harness_filter_no_match: revert to main; incomplete-marker already checks that a rejected selection leaves the target file unchanged. - structured-warnings: say the caps match the implementation's constants, which the RFC leaves implementation-defined.
join_key, cover_only_vacuous and warnings_shape_equivalent have no end-to-end user here; only schema-validation's check_fixtures.py tested them. They move, with their fixture cases, to the reference consumer that uses join_key. vacuous_pass and vacuity_suspect stay, because vacuity-check imports them.
This branch has not been deployed
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.
Part of #942 (RFC 0015, #4727). Follows #5062 (the INCOMPLETE marker). This PR changes only tests and the test helper
scripts/validate_json_export.py.Description
Adds end-to-end tests for
--export-jsonand fixture-based tests for two reading-rule helpers. The unit tests inkani-driverbuild their inputs by hand; each suite below runskaniorcargo kaniand covers a path those unit tests do not reach. The end-to-end tests runkaniorcargo kaniand check the exported documents or the rejected requests. Onlystructured-warningssubstitutes a CBMC wrapper, which injects warnings or simulates non-completed outcomes. The gate-rejection and no-harness cases do not reach verification.New suites in
tests/json-handler/:additive-output: checks that--export-jsonpreserves exit status and SARIF output for one passing and one failing harness, and preserves stdout and per-harness--output-into-filesoutput after masking runtime and verification-time lines. The expected exit status and the exported verdict are checked.--export-json -writes a file named-. Covers the real stdout, SARIF and per-harness file writers running next to the export.autoharness-export:kani autoharness --bounded-argumentsexportsis_automatically_generatedandis_boundedfor each harness. Covers the harness metadata that the autoharness pipeline passes to the export.gate-rejections: argument errors (a missing-Z export-json,--output-format=old,--only-codegen,--no-codegen,-Z lean, a directory as the target) are reported before compilation. A rejected argument and a compilation error both leave an existing file or directory at the target untouched. Covers the argument checks of the real command line and their order relative to compilation.jobs-ordering-stable: checks thatharnesses[]is sorted by(crate_name, file, line, name)and matches between--jobs 4and--jobs 1after excludingresources.verification_time_s. Covers the order of real parallel and sequential runs.live-configuration: the precedence of unwind and solver settings,cbmc_argskept verbatim, a bare--smt2,--coverageand the check-flag toggles. For each solver case, the exportedresolved_solveris compared with the solver line that CBMC prints. Covers the configuration of real runs, and the solver that CBMC actually runs.multi-crate-export:cargo kani --workspacewrites one document, and harnesses with the same name in two crates stay apart bycrate_name. Covers a real Cargo workspace.no-harnesses-selected:run_stateisNO_HARNESSES_SELECTED, with zero counts. Covers a real project without proof harnesses.structured-warnings: the caps and the exact text ofwarnings[]records, the ERROR classification of an ignored quantifier, and the CRASHED, TIMEOUT and OUT_OF_MEMORY shapes and elapsed times, against a fakecbmc. Covers the handling of a real child process: its output stream, a timeout kill, a crash exit and a kill signal.vacuity-check: thevacuous_passandvacuity_suspectpredicates on live exports, including a partly vacuous harness, with and without reach checks. Covers the reach checks that CBMC reports for real harnesses.Existing tests changed:
fail-fast: also checksharness_selection.matched_count, and that the run isPARTIALwhen a selected harness was skipped andCOMPLETEwhen the abort lands on the last selected harness.multiple-harnesses: also checksmatched_countandrun_state.schema-validation: also tests the two new reading-rule helpers (below) directly, on a new fixture,fixture-completed-success.json.scripts/validate_json_export.pygains two helpers that implement the vacuity reading rules of the RFC:vacuous_passandvacuity_suspect.vacuity-checkimports them, andschema-validation'scheck_fixtures.pytests them on fixtures.The branch merges
maininstead of rebasing, so its commit list includes an earlier version of the #5062 commit. The diff againstmaincontains only the changes above.Testing
./scripts/kani-regression.shpassed on Linux with CBMC 6.11.0, including the 17tests/json-handlertests, and the twocargo clippycommands of the clippy CI job passed.A record of which RFC 0015 clauses these tests assert, with the mutations observed to turn a test red, is kept outside this PR: https://github.com/ivmat/kani/tree/export-json-rfc0015-acceptance-2026-11/acceptance/rfc0015
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.