From d307faaab0db745ca7953a57a94787eb5efc820c 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/call_cbmc.rs | 17 +---- kani-driver/src/version.rs | 119 +++++++++++++++++++++++++++++++++++ 2 files changed, 122 insertions(+), 14 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index b06a2c2362a..86be93eb8dc 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -51,20 +51,9 @@ pub struct CbmcStats { impl KaniSession { /// Get CBMC version and system information pub fn get_cbmc_info(&self) -> Result { - let output = std::process::Command::new("cbmc") - .arg("--version") - .output() - .map_err(|_| anyhow::Error::msg("Failed to run cbmc --version"))?; - - let version_output = String::from_utf8_lossy(&output.stdout); - let lines: Vec<&str> = version_output.lines().collect(); - - // Extract version from first line (e.g., "6.7.1 (cbmc-6.7.1)") - let version = lines - .first() - .and_then(|line| line.split_whitespace().next()) - .unwrap_or("unknown") - .to_string(); + // Shares the single `cbmc --version` probe with the version-pin check. + let version = + crate::version::cbmc_version_on_path().unwrap_or_else(|| "unknown".to_string()); // For OS info, we'll use the system information since CBMC --version doesn't provide it let os_info = format!( diff --git a/kani-driver/src/version.rs b/kani-driver/src/version.rs index 55745e0c014..4a9f21f0398 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,68 @@ 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. Single source of truth for the `cbmc --version` probe (also used by +/// `KaniSession::get_cbmc_info`). +pub(crate) 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 +112,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); + } +}