diff --git a/Cargo.toml b/Cargo.toml index 216092bed76..9266d2e61cf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -81,6 +81,7 @@ exclude = [ "tests/script-based-pre/kani_lib_dep", "tests/script-based-pre/no_codegen", "tests/script-based-pre/no_codegen_error", + "tests/script-based-pre/verify_artifacts_cmd", ] [workspace.lints.clippy] diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 13e1321d649..9ce64c08548 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -8,6 +8,7 @@ pub mod common; pub mod list_args; pub mod playback_args; pub mod std_args; +pub mod verify_artifacts_args; use self::common::*; use crate::args::cargo::CargoTargetArgs; @@ -175,6 +176,8 @@ pub enum StandaloneSubcommand { Playback(Box), /// Verify the rust standard library. VerifyStd(Box), + /// Verify pre-built compiler artifacts without rebuilding. + VerifyArtifacts(Box), } #[derive(Debug, clap::Parser)] @@ -570,6 +573,7 @@ impl ValidateArgs for StandaloneArgs { match &self.command { Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?, + Some(StandaloneSubcommand::VerifyArtifacts(args)) => args.validate()?, Some(StandaloneSubcommand::List(args)) => args.validate()?, Some(StandaloneSubcommand::Autoharness(args)) => args.validate()?, // TODO: Invoke PlaybackArgs::validate() @@ -1259,4 +1263,28 @@ mod tests { let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err(); assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument); } + + #[test] + fn check_verify_artifacts() { + let args = StandaloneArgs::try_parse_from(vec![ + "kani", + "verify-artifacts", + "/some/artifact/dir", + "/another/dir", + ]) + .unwrap(); + let Some(StandaloneSubcommand::VerifyArtifacts(va)) = args.command else { + panic!("expected VerifyArtifacts subcommand, got {:?}", args.command); + }; + assert_eq!( + va.artifact_dirs, + vec![PathBuf::from("/some/artifact/dir"), PathBuf::from("/another/dir")] + ); + } + + #[test] + fn check_verify_artifacts_requires_dir() { + let result = StandaloneArgs::try_parse_from(vec!["kani", "verify-artifacts"]); + assert!(result.is_err(), "verify-artifacts with no dirs should fail to parse"); + } } diff --git a/kani-driver/src/args/verify_artifacts_args.rs b/kani-driver/src/args/verify_artifacts_args.rs new file mode 100644 index 00000000000..6c3e1c488d2 --- /dev/null +++ b/kani-driver/src/args/verify_artifacts_args.rs @@ -0,0 +1,64 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Implements the `verify-artifacts` subcommand handling. + +use crate::args::{ValidateArgs, VerificationArgs}; +use clap::error::ErrorKind; +use clap::{Error, Parser}; +use kani_metadata::UnstableFeature; +use std::path::PathBuf; + +/// Verify pre-built compiler artifacts without rebuilding. +/// +/// Reads `*.kani-metadata.json` and `*.symtab.out` files produced by a previous +/// `kani-compiler` invocation (e.g. `cargo kani --only-codegen`, or an external +/// build system that drives `kani-compiler` directly) and runs the verification +/// pipeline. Artifacts must be co-located with their metadata file — this is +/// kani-compiler's emit layout. The directory must be writable: the linker +/// writes the linked goto binary next to each `.symtab.out`. +/// +/// This is an **unstable option**. The artifacts must have been produced by the +/// same kani version that verifies them; `kani-driver` does not check. +#[derive(Debug, Parser)] +pub struct VerifyArtifactsArgs { + /// Directories containing pre-built `*.kani-metadata.json` and + /// `*.symtab.out` artifacts. + #[arg(required = true)] + pub artifact_dirs: Vec, + + #[command(flatten)] + pub verify_opts: VerificationArgs, +} + +impl ValidateArgs for VerifyArtifactsArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + + if !self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::UnstableOptions) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `verify-artifacts` subcommand is unstable and requires -Z unstable-options", + )); + } + + for dir in &self.artifact_dirs { + if !dir.is_dir() { + return Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Artifact directory `{}` does not exist or is not a directory", + dir.display() + ), + )); + } + } + + Ok(()) + } +} diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 44b3e242b43..ecf07d4df85 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -119,6 +119,15 @@ fn standalone_main() -> Result<()> { let project = project::std_project(&args.std_path, &session)?; (session, project) } + Some(StandaloneSubcommand::VerifyArtifacts(args)) => { + let session = KaniSession::new(args.verify_opts)?; + if !session.args.common_args.quiet { + print_kani_version(InvocationType::Standalone); + } + + let project = project::prebuilt_project(&args.artifact_dirs, &session)?; + (session, project) + } None => { let session = KaniSession::new(args.verify_opts)?; if !session.args.common_args.quiet { diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index b1740503228..9b6df564f1c 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -7,11 +7,12 @@ use crate::metadata::from_json; use crate::session::KaniSession; use crate::util::{crate_name, info_operation}; -use anyhow::{Context, Result}; +use anyhow::{Context, Result, bail}; use kani_metadata::{ ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, artifact::convert_type, }; use std::env::current_dir; +use std::ffi::OsStr; use std::fs; use std::ops::Deref; use std::path::{Path, PathBuf}; @@ -304,3 +305,172 @@ pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result>>()?; Project::try_new(session, outdir, None, metadata, None) } + +/// Parse all `*.kani-metadata.json` files under the given directories, rewriting +/// each harness's `goto_file` to be relative to the directory the metadata was +/// found in. +/// +/// kani-compiler records `goto_file` as the absolute path it was emitted to — +/// which is the build machine's `OUT_DIR` and is wrong after the artifacts are +/// relocated (a CI cache, an archive, a build-system store). The artifacts are +/// always co-located with the metadata file (kani-compiler emits them to the +/// same directory), so resolving by basename next to the metadata is correct. +fn read_prebuilt_metadata(artifact_dirs: &[PathBuf]) -> Result> { + let mut metadata = vec![]; + for dir in artifact_dirs { + let dir = dir.canonicalize().with_context(|| { + format!("Failed to canonicalize artifact directory `{}`", dir.display()) + })?; + let mut found_any = false; + for entry in fs::read_dir(&dir) + .with_context(|| format!("Failed to read artifact directory `{}`", dir.display()))? + { + let path = entry?.path(); + let is_metadata = path + .file_name() + .and_then(OsStr::to_str) + .is_some_and(|n| n.ends_with(".kani-metadata.json")); + if !is_metadata { + continue; + } + found_any = true; + let mut md: KaniMetadata = from_json(&path)?; + for h in md.proof_harnesses.iter_mut().chain(md.test_harnesses.iter_mut()) { + if let Some(gf) = &h.goto_file { + // Take only the basename; resolve against the directory + // the metadata file was found in. + let basename = gf.file_name().with_context(|| { + format!( + "Harness `{}` has a goto_file with no file name component", + h.pretty_name + ) + })?; + h.goto_file = Some(dir.join(basename)); + } + } + metadata.push(md); + } + if !found_any { + bail!( + "No `*.kani-metadata.json` files found in `{}`. \ + Was this directory produced by a `kani-compiler` build?", + dir.display() + ); + } + } + Ok(metadata) +} + +/// Generate a project from pre-built artifacts in the given directories. +/// +/// Each directory is scanned for `*.kani-metadata.json` files. For each +/// harness, `goto_file` is resolved relative to the directory the metadata was +/// found in. Artifacts must be co-located with the metadata file — this is +/// kani-compiler's emit layout, which `read_prebuilt_metadata()` documents. +/// +/// Note: `Project::try_new()` writes the linked `.out` file next to each +/// `.symtab.out`, so `artifact_dirs` must be writable. Callers reading from a +/// read-only artifact source (build cache, archive) should copy to a scratch +/// directory first. +pub fn prebuilt_project(artifact_dirs: &[PathBuf], session: &KaniSession) -> Result { + let outdir = if let Some(target_dir) = &session.args.target_dir { + std::fs::create_dir_all(target_dir)?; + target_dir.canonicalize()? + } else { + current_dir()?.canonicalize()? + }; + let metadata = read_prebuilt_metadata(artifact_dirs)?; + Project::try_new(session, outdir, None, metadata, None) +} + +#[cfg(test)] +mod tests { + use super::*; + use kani_metadata::{HarnessAttributes, HarnessKind}; + use std::fs; + + /// Build a minimal `KaniMetadata` with one proof harness whose `goto_file` + /// is the given path. Only `goto_file` matters; everything else is filler. + fn metadata_with_goto_file(goto_file: Option) -> KaniMetadata { + KaniMetadata { + crate_name: "fixture".to_string(), + proof_harnesses: vec![HarnessMetadata { + pretty_name: "fixture::check".to_string(), + mangled_name: "_RNvNtCsfixture_5check".to_string(), + crate_name: "fixture".to_string(), + original_file: "src/lib.rs".to_string(), + original_start_line: 1, + original_end_line: 5, + goto_file, + attributes: HarnessAttributes::new(HarnessKind::Proof), + contract: None, + has_loop_contracts: false, + is_automatically_generated: false, + }], + unsupported_features: vec![], + test_harnesses: vec![], + contracted_functions: vec![], + autoharness_md: None, + } + } + + /// `read_prebuilt_metadata()` rewrites each harness's `goto_file` to live + /// next to the metadata file it was found in — the recorded build-machine + /// path is meaningless after relocation. + #[test] + fn prebuilt_project_relocates_goto_file() { + let tmp = tempfile::tempdir().unwrap(); + let dir = tmp.path(); + // The recorded path is an absolute path from a different machine. + let recorded = PathBuf::from("/build/some-other-machine/fixture__hash.symtab.out"); + let basename = "fixture__hash.symtab.out"; + // Co-located artifact, documenting the layout the function assumes. + // `read_prebuilt_metadata()` does not validate existence — it rewrites + // unconditionally; the symtab is only read later by `Project::try_new()`. + fs::write(dir.join(basename), b"").unwrap(); + fs::write( + dir.join("fixture.kani-metadata.json"), + serde_json::to_string(&metadata_with_goto_file(Some(recorded))).unwrap(), + ) + .unwrap(); + + let parsed = read_prebuilt_metadata(&[dir.to_path_buf()]).unwrap(); + assert_eq!(parsed.len(), 1); + // The rewritten path must point inside the temp dir, not /build/.... + // Compare against the canonicalized dir — read_prebuilt_metadata() + // canonicalizes the input dir before joining, and on macOS /tmp is a + // symlink so a non-canonicalized comparison would spuriously fail. + let h = &parsed[0].proof_harnesses[0]; + assert_eq!( + h.goto_file.as_deref(), + Some(dir.canonicalize().unwrap().join(basename).as_path()) + ); + } + + /// A harness with no `goto_file` (reachability=none deps) must not panic; + /// `read_prebuilt_metadata()` leaves `None` alone. + #[test] + fn prebuilt_project_skips_none_goto_file() { + let tmp = tempfile::tempdir().unwrap(); + let dir = tmp.path(); + fs::write( + dir.join("fixture.kani-metadata.json"), + serde_json::to_string(&metadata_with_goto_file(None)).unwrap(), + ) + .unwrap(); + + let parsed = read_prebuilt_metadata(&[dir.to_path_buf()]).unwrap(); + assert_eq!(parsed[0].proof_harnesses[0].goto_file, None); + } + + /// An empty directory (no `*.kani-metadata.json`) is an error, not a vacuous + /// success — silence here would look like a verification that found nothing + /// to verify. + #[test] + fn prebuilt_project_errors_on_empty_dir() { + let tmp = tempfile::tempdir().unwrap(); + let result = read_prebuilt_metadata(&[tmp.path().to_path_buf()]); + assert!(result.is_err()); + assert!(result.unwrap_err().to_string().contains("No `*.kani-metadata.json`")); + } +} diff --git a/tests/script-based-pre/verify_artifacts_cmd/Cargo.toml b/tests/script-based-pre/verify_artifacts_cmd/Cargo.toml new file mode 100644 index 00000000000..f236ac80fec --- /dev/null +++ b/tests/script-based-pre/verify_artifacts_cmd/Cargo.toml @@ -0,0 +1,7 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "verify_artifacts_fixture" +version = "0.1.0" +edition = "2024" diff --git a/tests/script-based-pre/verify_artifacts_cmd/config.yml b/tests/script-based-pre/verify_artifacts_cmd/config.yml new file mode 100644 index 00000000000..4edce27340f --- /dev/null +++ b/tests/script-based-pre/verify_artifacts_cmd/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: verify_artifacts.sh +expected: verify_artifacts.expected diff --git a/tests/script-based-pre/verify_artifacts_cmd/src/lib.rs b/tests/script-based-pre/verify_artifacts_cmd/src/lib.rs new file mode 100644 index 00000000000..cf0059e4df7 --- /dev/null +++ b/tests/script-based-pre/verify_artifacts_cmd/src/lib.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Fixture for the verify-artifacts integration test. Two harnesses: one that +//! verifies, one that fails — proving the verdict is honest, not vacuous. + +#[cfg(kani)] +mod proofs { + #[kani::proof] + fn check_add_identity() { + let x: u8 = kani::any(); + assert_eq!(x.wrapping_add(0), x); + } + + #[kani::proof] + fn check_intentional_failure() { + let x: u8 = kani::any(); + // Fails for x == 255. The deliberate failure proves the pipeline + // reaches CBMC and reads the verdict — not merely that the command + // exited without crashing. + assert!(x < 255); + } +} diff --git a/tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.expected b/tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.expected new file mode 100644 index 00000000000..d4021b078ec --- /dev/null +++ b/tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.expected @@ -0,0 +1,8 @@ +[TEST] Build artifacts with --only-codegen +[TEST] Artifacts produced +[TEST] Verify pre-built artifacts +Checking harness proofs::check_add_identity... +Checking harness proofs::check_intentional_failure... +Verification failed for - proofs::check_intentional_failure +Complete - 1 successfully verified harnesses, 1 failures, 2 total. +[TEST] Exit code: 1 diff --git a/tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.sh b/tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.sh new file mode 100755 index 00000000000..48435df956a --- /dev/null +++ b/tests/script-based-pre/verify_artifacts_cmd/verify_artifacts.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Test `kani verify-artifacts`: build artifacts with `cargo kani --only-codegen`, +# then verify them with `kani verify-artifacts`. Round-trips the build/verify +# split that build systems with their own caching (nix, bazel, sccache, CI +# sharding) need. + +set -eu + +TARGET=$(rustc -vV | awk '/^host/ { print $2 }') +ARTIFACTS="target/kani/${TARGET}/debug/deps" + +# Clean up any prior run. +rm -rf target + +# Phase 1: produce artifacts only. +echo "[TEST] Build artifacts with --only-codegen" +cargo kani --only-codegen + +# Sanity: the artifacts the verify phase needs are present. +echo "[TEST] Artifacts produced" +ls "${ARTIFACTS}"/*.kani-metadata.json > /dev/null +ls "${ARTIFACTS}"/*.symtab.out > /dev/null + +# Phase 2: verify the pre-built artifacts. One harness passes, one fails by +# design — the exit code 1 proves the pipeline reached CBMC and propagated the +# verdict, not merely that the command ran. +echo "[TEST] Verify pre-built artifacts" +EXIT=0 +kani verify-artifacts "${ARTIFACTS}" -Z unstable-options || EXIT=$? + +echo "[TEST] Exit code: ${EXIT}" + +# Clean up. +rm -rf target