Warn when the CBMC on PATH does not match the pinned version

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<CbmcInfo> {
-        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!(

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<String> {
+    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<String> {
+    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<String> {
+    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<String> {
+    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 <version>[ (<git-revision>)] (<invocation>)`
@@ -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);
+    }
+}