From 7dc93d466da5cb306d87356b54951d6034d7dfb9 Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Tue, 18 Aug 2026 00:00:12 +0200 Subject: [PATCH] Warn when the CBMC on PATH does not match the pinned version `kani --version` and the startup banner now also print the CBMC version found on PATH. When it differs from the `CBMC_VERSION` pin in `kani-dependencies`, Kani prints a warning and continues: an unpinned CBMC should not block users, but its results may not match CI. The pin file is embedded with `include_str!` because release bundles do not ship `kani-dependencies`, so a runtime read would disable the check for exactly the installs that can least audit their toolchain. `cargo kani --version` now also answers when a malformed `Cargo.toml` makes `join_args` fail, via a raw-argument scan used only on that path. The check is silent under `--quiet` (tested zero-output contract) and absent when `cbmc` is not on PATH: a missing CBMC fails loudly at verification time. --- kani-driver/src/args/mod.rs | 26 ++++++++ kani-driver/src/main.rs | 13 +++- kani-driver/src/version.rs | 118 ++++++++++++++++++++++++++++++++++++ 3 files changed, 156 insertions(+), 1 deletion(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index e7636d1a45a..bf97d318ffa 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -22,6 +22,20 @@ use std::str::FromStr; use std::time::Duration; use strum::VariantNames; +/// Detect a whole-argument `--version`/`-V` in raw args, stopping at a `--` or +/// `--cbmc-args` boundary. Used when `join_args` fails and clap never parses. +pub fn requests_version(args: &[OsString]) -> bool { + for arg in args.iter().skip(1) { + if arg == "--" || arg == "--cbmc-args" { + return false; + } + if arg == "--version" || arg == "-V" { + return true; + } + } + false +} + /// Trait used to perform extra validation after parsing. pub trait ValidateArgs { /// Perform post-parsing validation but do not abort. @@ -1048,6 +1062,18 @@ mod tests { use super::*; + #[test] + fn requests_version_matches_whole_flags_only() { + let to_args = |args: &[&str]| args.iter().map(OsString::from).collect::>(); + assert!(requests_version(&to_args(&["cargo-kani", "--version"]))); + assert!(requests_version(&to_args(&["cargo-kani", "-V"]))); + assert!(requests_version(&to_args(&["cargo-kani", "--quiet", "-V"]))); + assert!(!requests_version(&to_args(&["cargo-kani"]))); + assert!(!requests_version(&to_args(&["cargo-kani", "--", "--version"]))); + assert!(!requests_version(&to_args(&["cargo-kani", "--cbmc-args", "--version"]))); + assert!(!requests_version(&to_args(&["cargo-kani", "-qV"]))); + } + #[test] fn check_arg_parsing() { let a = StandaloneArgs::try_parse_from(vec![ diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index e8a1ba11033..5447823089e 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -81,7 +81,18 @@ fn main() -> ExitCode { /// The main function for the `cargo kani` command. fn cargokani_main(input_args: Vec) -> Result<()> { - let input_args = join_args(input_args)?; + let input_args = match join_args(input_args.clone()) { + Ok(joined) => joined, + // `--version` must answer even when a malformed `Cargo.toml` breaks `join_args`. + Err(err) => { + return if args::requests_version(&input_args) { + print_kani_version(InvocationType::CargoKani(input_args), false); + Ok(()) + } else { + Err(err) + }; + } + }; let args = args::CargoKaniArgs::parse_from(&input_args); check_is_valid(&args); diff --git a/kani-driver/src/version.rs b/kani-driver/src/version.rs index 55745e0c014..be01ba7f476 100644 --- a/kani-driver/src/version.rs +++ b/kani-driver/src/version.rs @@ -2,6 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::InvocationType; +use crate::util; +use std::process::Command; const KANI_RUST_VERIFIER: &str = "Kani Rust Verifier"; /// We assume this is the same as the `kani-verifier` version, but we should @@ -27,6 +29,67 @@ pub(crate) fn print_kani_version(invocation_type: InvocationType, verbose: bool) if verbose && !KANI_RUSTC_VERSION.is_empty() { println!("{KANI_RUSTC_VERSION}"); } + // Callers gate this function on `--quiet`, so the pin check keeps the + // tested zero-output contract of `--quiet`. + print_cbmc_version_info(); +} + +const CBMC_VERSION_VAR: &str = "CBMC_VERSION"; + +/// Embedded at compile time because release bundles do not ship +/// `kani-dependencies`, so a runtime read would fail there. +const KANI_DEPENDENCIES: &str = include_str!("../../kani-dependencies"); + +/// The CBMC version found on `PATH`, or `None` if `cbmc` is absent or says +/// nothing. +fn cbmc_version_on_path() -> Option { + let output = Command::new("cbmc").arg("--version").output().ok()?; + if !output.status.success() { + return None; + } + let stdout = String::from_utf8_lossy(&output.stdout); + stdout.split_whitespace().next().map(str::to_string) +} + +fn pinned_cbmc_version() -> Option { + parse_dependency_var(KANI_DEPENDENCIES, CBMC_VERSION_VAR) +} + +/// Extract `KEY=VALUE` (optionally quoted) from a shell-style assignment file. +fn parse_dependency_var(contents: &str, key: &str) -> Option { + let prefix = format!("{key}="); + contents + .lines() + .find_map(|line| line.trim().strip_prefix(prefix.as_str())) + .map(|value| value.trim().trim_matches(|c| c == '"' || c == '\'').to_string()) + .filter(|value| !value.is_empty()) +} + +/// Print the `PATH` CBMC version. Warn, but do not fail, when it does not +/// match the pin: an unpinned CBMC must not block users. +fn print_cbmc_version_info() { + let Some(found) = cbmc_version_on_path() else { + return; + }; + println!("CBMC {found}"); + + if let Some(pinned) = pinned_cbmc_version() + && let Some(warning) = cbmc_version_mismatch_warning(&found, &pinned) + { + util::warning(&warning); + } +} + +/// The mismatch warning, or `None` on a match. Split out for unit tests. +fn cbmc_version_mismatch_warning(found: &str, pinned: &str) -> Option { + if found == pinned { + None + } else { + Some(format!( + "found CBMC {found} on PATH, but Kani pins CBMC {pinned} (see `kani-dependencies`). \ + Verification results may not reflect the pinned toolchain." + )) + } } /// Print Kani release version as `Kani Rust Verifier [ ()] ()` @@ -48,3 +111,58 @@ fn kani_version_release(invocation_type: InvocationType, verbose: bool) -> Strin }; format!("{KANI_RUST_VERIFIER} {KANI_VERSION}{git_info} ({invocation_str})") } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn parses_quoted_dependency_var() { + let contents = "CBMC_MAJOR=\"6\"\nCBMC_VERSION=\"6.8.0\"\n\nKISSAT_VERSION=\"4.0.1\"\n"; + assert_eq!(parse_dependency_var(contents, "CBMC_VERSION"), Some("6.8.0".to_string())); + assert_eq!(parse_dependency_var(contents, "KISSAT_VERSION"), Some("4.0.1".to_string())); + } + + #[test] + fn parses_unquoted_dependency_var() { + assert_eq!( + parse_dependency_var("CBMC_VERSION=6.8.0\n", "CBMC_VERSION"), + Some("6.8.0".to_string()) + ); + } + + #[test] + fn parses_single_quoted_dependency_var() { + assert_eq!( + parse_dependency_var("CBMC_VERSION='6.8.0'\n", "CBMC_VERSION"), + Some("6.8.0".to_string()) + ); + } + + #[test] + fn parses_real_kani_dependencies_file() { + assert!(pinned_cbmc_version().is_some(), "kani-dependencies must define CBMC_VERSION"); + } + + #[test] + fn missing_dependency_var_is_none() { + assert_eq!(parse_dependency_var("KISSAT_VERSION=\"4.0.1\"\n", "CBMC_VERSION"), None); + } + + #[test] + fn empty_dependency_var_is_none() { + assert_eq!(parse_dependency_var("CBMC_VERSION=\"\"\n", "CBMC_VERSION"), None); + } + + #[test] + fn mismatched_versions_produce_a_warning_naming_both() { + let warning = cbmc_version_mismatch_warning("6.7.1", "6.8.0").unwrap(); + assert!(warning.contains("6.7.1")); + assert!(warning.contains("6.8.0")); + } + + #[test] + fn matching_versions_produce_no_warning() { + assert_eq!(cbmc_version_mismatch_warning("6.8.0", "6.8.0"), None); + } +}