diff --git a/docs/src/verification-results.md b/docs/src/verification-results.md index 5b84c74def3..3a98aa80c9e 100644 --- a/docs/src/verification-results.md +++ b/docs/src/verification-results.md @@ -185,4 +185,4 @@ cargo kani -Z export-json --export-json kani.json The file describes the tool versions, the configuration and the outcome of every harness. The format is unstable and may change between releases; see [RFC 0015](https://model-checking.github.io/kani/rfc/rfcs/0015-export-json.html) for the schema. The flag requires `-Z export-json`; `-Z unstable-options` alone is no longer enough. -This version never writes the `INCOMPLETE` marker that the RFC describes. If a run is killed, the file from an earlier run can stay in place and look complete. Compare its `started_at` with the time of your run. +After a successful build and harness selection, Kani replaces any earlier file with an `INCOMPLETE` marker before verification starts, and replaces the marker with the final document at the end. A killed or failed run can leave the marker. A failure before the marker is written leaves any earlier file in place; compare its `started_at` with the time of your run. diff --git a/kani-driver/src/frontend/schema_utils.rs b/kani-driver/src/frontend/schema_utils.rs index 54becf0eb01..68dc394937c 100644 --- a/kani-driver/src/frontend/schema_utils.rs +++ b/kani-driver/src/frontend/schema_utils.rs @@ -32,7 +32,7 @@ const KANI_GIT_SHA: Option<&str> = option_env!("KANI_GIT_SHA"); /// `None` exactly when `KANI_GIT_SHA` is `None`. const KANI_GIT_DIRTY: Option<&str> = option_env!("KANI_GIT_DIRTY"); -struct RunContext { +pub(crate) struct RunContext { cbmc_version: Option, rustc_version: Option, kani_commit: Option<&'static str>, @@ -42,21 +42,29 @@ struct RunContext { harness_timeout_s: Option, configuration: ConfigurationExport, started_at: OffsetDateTime, - wall_time: Duration, } impl KaniSession { - /// Writes `--export-json` for a completed run; no-op if unset. `matched_harnesses` must be - /// the pre-verification list, not `results`, which `--fail-fast` can truncate. - pub fn write_export_json( + /// Writes the `--export-json` marker and returns its context; no-op if unset. + pub(crate) fn begin_export_json( &self, matched_harnesses: &[&HarnessMetadata], - results: &[HarnessResult<'_>], started_at: OffsetDateTime, + ) -> Result> { + let Some(path) = &self.args.export_json else { return Ok(None) }; + let ctx = self.build_run_context(matched_harnesses, started_at); + write_json_atomically(path, &IncompleteRun::from(&ctx))?; + Ok(Some(ctx)) + } + + /// Writes the terminal `--export-json` document; no-op if unset. + pub fn write_export_json( + &self, + results: &[HarnessResult<'_>], + ctx: Option, wall_time: Duration, ) -> Result<()> { - let Some(path) = &self.args.export_json else { return Ok(()) }; - let ctx = self.build_run_context(matched_harnesses, started_at, wall_time); + let (Some(path), Some(ctx)) = (&self.args.export_json, ctx) else { return Ok(()) }; let export = ExportedRun::from_harness_results( results, |harness| { @@ -67,6 +75,7 @@ impl KaniSession { ) }, ctx, + wall_time, ); write_json_atomically(path, &export) } @@ -75,7 +84,6 @@ impl KaniSession { &self, matched_harnesses: &[&HarnessMetadata], started_at: OffsetDateTime, - wall_time: Duration, ) -> RunContext { let enabled_unstable_features: BTreeSet = self .args @@ -104,7 +112,6 @@ impl KaniSession { harness_timeout_s: self.args.harness_timeout.map(|t| Duration::from(t).as_secs_f64()), configuration: configuration_from(&self.args), started_at, - wall_time, } } } @@ -287,6 +294,49 @@ struct ToolsExport { cbmc: Option, } +#[derive(Serialize)] +struct IncompleteRun<'a> { + schema_version: &'static str, + kani_commit: Option<&'static str>, + kani_commit_dirty: Option, + tools: ToolsExport, + enabled_unstable_features: &'a BTreeSet, + harness_selection: &'a HarnessSelectionExport, + harness_timeout_s: Option, + configuration: &'a ConfigurationExport, + run_state: IncompleteState, + target: &'static str, + started_at: String, +} + +#[derive(Serialize)] +#[serde(rename_all = "SCREAMING_SNAKE_CASE")] +enum IncompleteState { + Incomplete, +} + +impl<'a> From<&'a RunContext> for IncompleteRun<'a> { + fn from(ctx: &'a RunContext) -> Self { + Self { + schema_version: SCHEMA_VERSION, + kani_commit: ctx.kani_commit, + kani_commit_dirty: ctx.kani_commit_dirty, + tools: ToolsExport { + kani: KANI_VERSION, + rustc: ctx.rustc_version.clone(), + cbmc: ctx.cbmc_version.clone(), + }, + enabled_unstable_features: &ctx.enabled_unstable_features, + harness_selection: &ctx.harness_selection, + harness_timeout_s: ctx.harness_timeout_s, + configuration: &ctx.configuration, + run_state: IncompleteState::Incomplete, + target: env!("TARGET"), + started_at: format_started_at(ctx.started_at), + } + } +} + #[derive(Serialize)] struct ExportedRun { schema_version: &'static str, @@ -616,6 +666,7 @@ impl ExportedRun { results: &[HarnessResult<'_>], resolve: impl Fn(&HarnessMetadata) -> (Option, Option), ctx: RunContext, + wall_time: Duration, ) -> Self { let mut harnesses: Vec = results .iter() @@ -660,7 +711,7 @@ impl ExportedRun { run_state, target: env!("TARGET"), started_at: format_started_at(ctx.started_at), - wall_time_s: ctx.wall_time.as_secs_f64(), + wall_time_s: wall_time.as_secs_f64(), harnesses, summary, } @@ -885,7 +936,6 @@ mod tests { harness_timeout_s: None, configuration: test_ctx_config(), started_at: started(), - wall_time: Duration::from_millis(1), } } @@ -894,13 +944,86 @@ mod tests { } fn export_with(results: &[HarnessResult<'_>], ctx: RunContext) -> ExportedRun { - ExportedRun::from_harness_results(results, cadical, ctx) + ExportedRun::from_harness_results(results, cadical, ctx, Duration::from_millis(1)) } fn export_one(hr: HarnessResult<'_>) -> ExportedRun { export_with(&[hr], test_context()) } + #[test] + fn incomplete_marker_serializes_only_marker_fields() { + let mut ctx = test_context(); + ctx.kani_commit = Some("abc123"); + ctx.kani_commit_dirty = Some(true); + ctx.rustc_version = Some("rustc test".to_string()); + ctx.cbmc_version = Some("CBMC test".to_string()); + ctx.enabled_unstable_features.insert("export-json".to_string()); + + let marker = serde_json::to_value(IncompleteRun::from(&ctx)).unwrap(); + let keys: BTreeSet<&str> = marker.as_object().unwrap().keys().map(String::as_str).collect(); + assert_eq!( + keys, + BTreeSet::from([ + "configuration", + "enabled_unstable_features", + "harness_selection", + "harness_timeout_s", + "kani_commit", + "kani_commit_dirty", + "run_state", + "schema_version", + "started_at", + "target", + "tools", + ]) + ); + assert_eq!(marker["run_state"], "INCOMPLETE"); + assert_eq!(marker["kani_commit"], "abc123"); + assert_eq!(marker["kani_commit_dirty"], true); + assert_eq!(marker["tools"]["rustc"], "rustc test"); + assert_eq!(marker["tools"]["cbmc"], "CBMC test"); + let null_marker = serde_json::to_value(IncompleteRun::from(&test_context())).unwrap(); + assert!(null_marker["kani_commit"].is_null()); + assert!(null_marker["kani_commit_dirty"].is_null()); + assert!(null_marker["tools"]["rustc"].is_null()); + assert!(null_marker["tools"]["cbmc"].is_null()); + } + + #[test] + fn incomplete_marker_and_terminal_export_share_context() { + let mut ctx = test_context(); + ctx.kani_commit = Some("shared-commit"); + ctx.cbmc_version = Some("shared CBMC".to_string()); + ctx.enabled_unstable_features.insert("export-json".to_string()); + let marker = serde_json::to_value(IncompleteRun::from(&ctx)).unwrap(); + + let h = harness("h"); + let hr = HarnessResult { harness: &h, result: success_result(vec![]) }; + let terminal = serde_json::to_value(ExportedRun::from_harness_results( + &[hr], + cadical, + ctx, + Duration::from_millis(500), + )) + .unwrap(); + + for key in [ + "schema_version", + "kani_commit", + "kani_commit_dirty", + "tools", + "enabled_unstable_features", + "harness_selection", + "harness_timeout_s", + "configuration", + "target", + "started_at", + ] { + assert_eq!(marker[key], terminal[key], "shared field {key}"); + } + } + #[test] fn export_all_successful() { let h = harness("my_harness"); @@ -911,12 +1034,9 @@ mod tests { let result = success_result(properties); let hr = HarnessResult { harness: &h, result }; - let ctx = RunContext { - cbmc_version: Some("CBMC 6.8.0".to_string()), - wall_time: Duration::from_millis(500), - ..test_context() - }; - let export = export_with(&[hr], ctx); + let ctx = RunContext { cbmc_version: Some("CBMC 6.8.0".to_string()), ..test_context() }; + let export = + ExportedRun::from_harness_results(&[hr], cadical, ctx, Duration::from_millis(500)); let v = serde_json::to_value(&export).unwrap(); assert_eq!(v["schema_version"], "0.1.0"); @@ -1797,6 +1917,7 @@ mod tests { &[hr], |_| (Some("cadical".to_string()), Some(7)), test_context(), + Duration::from_millis(1), )) .unwrap(); let hj = &v["harnesses"][0]; @@ -1936,6 +2057,7 @@ mod tests { &[hr], |_| (Some("totally-unfamiliar-solver-v9".to_string()), None), test_context(), + Duration::from_millis(1), )) .unwrap(); assert_eq!(v["harnesses"][0]["resolved_solver"], "totally-unfamiliar-solver-v9"); diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 1bce00357e6..97232f8ada5 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -191,6 +191,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { let harnesses = session.determine_targets(project.get_all_harnesses())?; debug!(n = harnesses.len(), ?harnesses, "verify_project"); + let export_context = session.begin_export_json(&harnesses, started_at)?; // Verification let runner = harness_runner::HarnessRunner { sess: &session, project: &project }; @@ -215,7 +216,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { session.save_coverage_results(&project, &results, ×tamp)?; } - session.write_export_json(&harnesses, &results, started_at, start_instant.elapsed())?; + session.write_export_json(&results, export_context, start_instant.elapsed())?; session.write_sarif(&results)?; if !session.args.common_args.quiet { session.print_final_summary(&results)?; diff --git a/rfc/src/rfcs/0015-export-json.md b/rfc/src/rfcs/0015-export-json.md index a8df498d0a4..c4122cd4b0d 100644 --- a/rfc/src/rfcs/0015-export-json.md +++ b/rfc/src/rfcs/0015-export-json.md @@ -244,7 +244,8 @@ Each write puts full JSON in a temporary file in the target directory, then atom the target (same-filesystem POSIX rename). A mid-write kill leaves the previous target and possibly an orphaned temp file, never a partially written target. After building and selecting harnesses, when verification begins, an atomic `INCOMPLETE` marker replaces any earlier file. It contains known -pre-verification fields, without `outcome`, `wall_time_s`, `summary` or `harnesses[]`. +pre-verification fields, without `outcome`, `wall_time_s`, `summary` or `harnesses[]`. The marker is also +written for an empty, unfiltered harness selection before the terminal `NO_HARNESSES_SELECTED` document replaces it. First check `schema_version` (refuse unsupported major or, pre-1.0, minor), then `run_state`: - Only `COMPLETE` is complete verification evidence: every selected harness has an entry, regardless of outcome. @@ -257,7 +258,7 @@ deletion fails closed on `ENOENT`. Concurrent writers to one path are unsupporte `NO_HARNESSES_SELECTED` means an unfiltered project/workspace with no selectable proof harness or eligible autoharness function: `requested_filters == []`, `unmatched_filters == []`, `matched_count == 0`. A wholly unmatched filter set, or any unmatched `--exact` filter, errors non-zero before export (#4743). -Nonempty `unmatched_filters` occurs only without `--exact` in `COMPLETE`/`PARTIAL` when another filter matched. +Nonempty `unmatched_filters` occurs only without `--exact` in `INCOMPLETE`/`COMPLETE`/`PARTIAL` when another filter matched. ## Rationale and alternatives @@ -420,7 +421,7 @@ The narrower `INCOMPLETE` marker follows its presence matrix below. | `run_state` | `"INCOMPLETE"` \| `"COMPLETE"` \| `"PARTIAL"` \| `"NO_HARNESSES_SELECTED"` | — | Trust is based on this field; see Completeness under Reading the results. | | `target` | string | — | The Rust target triple Kani itself was built for. | | `started_at` | string | — | UTC, `YYYY-MM-DDTHH:MM:SSZ` (second resolution). Taken after the build, when target selection starts. | -| `wall_time_s` | number | — | Seconds from target selection to the start of the export write: target selection, verification and coverage output. The build is not included. Volatile between runs by design (see "Interaction with other flags"). | +| `wall_time_s` | number | — | Seconds from target selection to the start of the terminal export write: target selection, the tool version probes and the marker write, verification and coverage output. The build is not included. Volatile between runs by design (see "Interaction with other flags"). | | `harnesses[]` | array of harness objects | never null, may be empty (e.g. under `NO_HARNESSES_SELECTED`) | Sorted by `(crate_name, file, line, name)`. | | `harnesses[].name` | string | — | Fully qualified `pretty_name`; see Selection under Reading the results. | | `harnesses[].crate_name` | string | — | Distinguishes same-named harnesses across crates in one workspace. | diff --git a/tests/json-handler/incomplete-marker/config.yml b/tests/json-handler/incomplete-marker/config.yml new file mode 100644 index 00000000000..8258439d3e3 --- /dev/null +++ b/tests/json-handler/incomplete-marker/config.yml @@ -0,0 +1,3 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: test.sh diff --git a/tests/json-handler/incomplete-marker/fake_cbmc.py b/tests/json-handler/incomplete-marker/fake_cbmc.py new file mode 100755 index 00000000000..2f996c12117 --- /dev/null +++ b/tests/json-handler/incomplete-marker/fake_cbmc.py @@ -0,0 +1,34 @@ +#!/usr/bin/env python3 +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +import json +import os +import sys +import time + + +def main(): + real_cbmc = os.environ["REAL_CBMC"] + if sys.argv[1:] == ["--version"]: + os.execv(real_cbmc, [real_cbmc, "--version"]) + + ready = os.environ["FAKE_CBMC_READY"] + record = {"pid": os.getpid(), "ppid": os.getppid()} + temporary = f"{ready}.{os.getpid()}.tmp" + with open(temporary, "w", encoding="utf-8") as output: + json.dump(record, output) + os.replace(temporary, ready) + + deadline = time.monotonic() + float(os.environ.get("FAKE_CBMC_TIMEOUT_S", "25")) + release = os.environ["FAKE_CBMC_RELEASE"] + while time.monotonic() < deadline: + if os.path.exists(release): + os.execv(real_cbmc, [real_cbmc, *sys.argv[1:]]) + time.sleep(0.02) + print("fake cbmc timed out waiting for release", file=sys.stderr) + return 124 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tests/json-handler/incomplete-marker/run.py b/tests/json-handler/incomplete-marker/run.py new file mode 100755 index 00000000000..272c2375a7a --- /dev/null +++ b/tests/json-handler/incomplete-marker/run.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +import datetime +import json +import os +import pathlib +import shutil +import signal +import subprocess +import sys +import tempfile +import time + + +POLL_TIMEOUT_S = 30 + + +def load_json(path): + with path.open(encoding="utf-8") as source: + return json.load(source) + + +def remove(path): + try: + path.unlink() + except FileNotFoundError: + pass + + +def cleanup_group(pid): + try: + os.killpg(pid, signal.SIGKILL) + except (ProcessLookupError, PermissionError): + pass + + +def wait_for_marker(process, ready, output): + deadline = time.monotonic() + POLL_TIMEOUT_S + while time.monotonic() < deadline: + if process.poll() is not None: + raise AssertionError(f"Kani exited before CBMC blocked: {process.returncode}") + try: + record = load_json(ready) + marker = load_json(output) + except (FileNotFoundError, json.JSONDecodeError): + time.sleep(0.02) + continue + if marker.get("run_state") == "INCOMPLETE": + return record, marker + time.sleep(0.02) + raise AssertionError("timed out waiting for fake CBMC and the INCOMPLETE marker") + + +def start_kani(command, environment, root, groups): + process = subprocess.Popen( + command, + cwd=root, + env=environment, + stdout=subprocess.DEVNULL, + stderr=subprocess.DEVNULL, + start_new_session=True, + ) + groups.append(process.pid) + return process + + +def wait_for_next_utc_second(): + previous = datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ") + deadline = time.monotonic() + 2 + while time.monotonic() < deadline: + current = datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ") + if current != previous: + return + time.sleep(0.01) + raise AssertionError("UTC second did not advance") + + +def main(): + kani = pathlib.Path(sys.argv[1]) + real_cbmc = pathlib.Path(sys.argv[2]).resolve() + suite_dir = pathlib.Path(sys.argv[3]).resolve() + with tempfile.TemporaryDirectory(prefix="kani-incomplete-marker-") as temporary: + groups = [] + root = pathlib.Path(temporary) + output = root / "export.json" + ready = root / "ready.json" + release = root / "release" + fake_bin = root / "bin" + fake_bin.mkdir() + os.symlink(suite_dir / "fake_cbmc.py", fake_bin / "cbmc") + test = root / "test.rs" + shutil.copyfile(suite_dir / "test.rs", test) + + base_command = [ + str(kani), + "-Z", + "export-json", + str(test), + "--export-json", + str(output), + "--quiet", + ] + seeded = subprocess.run(base_command, cwd=root, capture_output=True, text=True) + assert seeded.returncode == 0, seeded.stderr + seeded_export = load_json(output) + assert seeded_export["run_state"] == "COMPLETE" + wait_for_next_utc_second() + + environment = os.environ.copy() + environment.update( + { + "PATH": f"{fake_bin}{os.pathsep}{environment['PATH']}", + "REAL_CBMC": str(real_cbmc), + "FAKE_CBMC_READY": str(ready), + "FAKE_CBMC_RELEASE": str(release), + "FAKE_CBMC_TIMEOUT_S": "25", + } + ) + + try: + # A killed driver leaves the INCOMPLETE marker bytes in place. + remove(ready) + remove(release) + process = start_kani(base_command, environment, root, groups) + record, marker = wait_for_marker(process, ready, output) + assert record["ppid"] == process.pid, (record, process.pid) + marker_bytes = output.read_bytes() + os.kill(process.pid, signal.SIGKILL) + assert process.wait(timeout=5) == -signal.SIGKILL + assert output.read_bytes() == marker_bytes + assert marker["run_state"] == "INCOMPLETE" + assert marker["started_at"] != seeded_export["started_at"] + for key in ["outcome", "wall_time_s", "summary", "harnesses"]: + assert key not in marker, key + cleanup_group(process.pid) + + # Releasing CBMC replaces the marker with a terminal document from the same context. + remove(ready) + remove(release) + process = start_kani(base_command, environment, root, groups) + record, marker = wait_for_marker(process, ready, output) + assert record["ppid"] == process.pid, (record, process.pid) + wait_for_next_utc_second() + release.touch() + assert process.wait(timeout=POLL_TIMEOUT_S) == 0 + terminal = load_json(output) + assert terminal["run_state"] == "COMPLETE" + assert terminal["started_at"] == marker["started_at"], ( + terminal["started_at"], + marker["started_at"], + ) + for key, value in marker.items(): + if key != "run_state": + assert terminal[key] == value, key + + # A marker write error prevents CBMC from starting. + remove(ready) + remove(release) + regular_file = root / "regular-file" + regular_file.write_text("not a directory", encoding="utf-8") + bad_parent = regular_file / "child" / "export.json" + command = [*base_command] + command[command.index(str(output))] = str(bad_parent) + result = subprocess.run( + command, + cwd=root, + env=environment, + capture_output=True, + text=True, + timeout=POLL_TIMEOUT_S, + ) + diagnostic = result.stdout + result.stderr + assert result.returncode != 0, diagnostic + assert "Failed to create --export-json output directory" in diagnostic, diagnostic + assert not ready.exists() + + # Rejected selection leaves the seeded terminal file unchanged. + remove(ready) + remove(release) + seeded_bytes = output.read_bytes() + command = [*base_command, "--harness", "does-not-exist"] + result = subprocess.run( + command, + cwd=root, + env=environment, + capture_output=True, + text=True, + timeout=POLL_TIMEOUT_S, + ) + diagnostic = result.stdout + result.stderr + expected = ( + "Failed to match the following harness(es):\n" + "does-not-exist\n" + "Please specify the fully-qualified name of a harness." + ) + assert result.returncode != 0, diagnostic + assert expected in diagnostic, diagnostic + assert output.read_bytes() == seeded_bytes + assert not ready.exists() + finally: + for pid in groups: + cleanup_group(pid) + + +if __name__ == "__main__": + main() diff --git a/tests/json-handler/incomplete-marker/test.rs b/tests/json-handler/incomplete-marker/test.rs new file mode 100644 index 00000000000..b216a49f130 --- /dev/null +++ b/tests/json-handler/incomplete-marker/test.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn check_true() { + assert!(true); +} diff --git a/tests/json-handler/incomplete-marker/test.sh b/tests/json-handler/incomplete-marker/test.sh new file mode 100755 index 00000000000..22208e6b4ab --- /dev/null +++ b/tests/json-handler/incomplete-marker/test.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +KANI_BIN="$(command -v kani)" +CBMC_BIN="$(command -v cbmc)" + +python3 "$SCRIPT_DIR/run.py" "$KANI_BIN" "$CBMC_BIN" "$SCRIPT_DIR"