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

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::<Vec<_>>();
+        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![

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<OsString>) -> 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);
 

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<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 +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);
+    }
+}