Add git revision and rustc version info to verbose version output

Cargo.toml

@@ -18,6 +18,7 @@ include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.m
 
 [dependencies]
 anyhow = "1"
+build-kani = { path = "tools/build-kani" }
 home = "0.5"
 os_info = { version = "3", default-features = false }
 

kani-driver/Cargo.toml

@@ -13,6 +13,7 @@ publish = false
 
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }
+build-kani = { path = "../tools/build-kani" }
 cargo_metadata = "0.23"
 anyhow = "1"
 console = "0.16"

kani-driver/src/args/mod.rs

@@ -140,17 +140,17 @@ impl From<Timeout> for Duration {
 
 #[derive(Debug, clap::Parser)]
 #[command(
-    version,
     name = "kani",
     about = "Verify a single Rust crate. For more information, see https://github.com/model-checking/kani",
     args_override_self = true,
     subcommand_negates_reqs = true,
     subcommand_precedence_over_arg = true,
-    args_conflicts_with_subcommands = true
+    args_conflicts_with_subcommands = true,
+    disable_version_flag = true
 )]
 pub struct StandaloneArgs {
     /// Rust file to verify
-    #[arg(required = true)]
+    #[arg(required_unless_present = "version")]
     pub input: Option<PathBuf>,
 
     #[command(flatten)]
@@ -161,6 +161,10 @@ pub struct StandaloneArgs {
 
     #[arg(long, hide = true)]
     pub crate_name: Option<String>,
+
+    /// Print version information
+    #[arg(long, short = 'V')]
+    pub version: bool,
 }
 
 /// Kani takes optional subcommands to request specialized behavior.
@@ -179,17 +183,21 @@ pub enum StandaloneSubcommand {
 
 #[derive(Debug, clap::Parser)]
 #[command(
-    version,
     name = "cargo-kani",
     about = "Verify a Rust crate. For more information, see https://github.com/model-checking/kani",
-    args_override_self = true
+    args_override_self = true,
+    disable_version_flag = true
 )]
 pub struct CargoKaniArgs {
     #[command(subcommand)]
     pub command: Option<CargoKaniSubcommand>,
 
     #[command(flatten)]
     pub verify_opts: VerificationArgs,
+
+    /// Print version information
+    #[arg(long, short = 'V')]
+    pub version: bool,
 }
 
 /// cargo-kani takes optional subcommands to request specialized behavior

kani-driver/src/autoharness/mod.rs

@@ -27,7 +27,7 @@ pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> {
     setup_session(&mut session, &args.common_autoharness_args);
 
     if !session.args.common_args.quiet {
-        print_kani_version(InvocationType::CargoKani(vec![]));
+        print_kani_version(InvocationType::CargoKani(vec![]), session.args.common_args.verbose);
     }
     let project = project::cargo_project(&mut session, false)?;
     postprocess_project(project, session, args.common_autoharness_args)
@@ -38,7 +38,7 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> {
     setup_session(&mut session, &args.common_autoharness_args);
 
     if !session.args.common_args.quiet {
-        print_kani_version(InvocationType::Standalone);
+        print_kani_version(InvocationType::Standalone, session.args.common_args.verbose);
     }
 
     let project = if args.std {

kani-driver/src/call_cargo.rs

@@ -11,6 +11,7 @@ use crate::session::{
 use crate::util;
 use crate::util::args::{CargoArg, CommandWrapper as _, KaniArg, PassTo, encode_as_rustc_arg};
 use anyhow::{Context, Result, bail};
+use build_kani::built_info;
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{
     Artifact as RustcArtifact, CrateType, Message, Metadata, MetadataCommand, Package, PackageId,
@@ -133,7 +134,7 @@ crate-type = ["lib"]
 
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
     pub fn cargo_build(&mut self, keep_going: bool) -> Result<CargoOutputs> {
-        let build_target = env!("TARGET"); // see build.rs
+        let build_target = built_info::TARGET;
         let metadata = self.cargo_metadata(build_target)?;
         let target_dir = self
             .args
@@ -475,7 +476,7 @@ crate-type = ["lib"]
 pub fn cargo_config_args() -> Vec<CargoArg> {
     [
         "--target",
-        env!("TARGET"),
+        built_info::TARGET,
         // Propagate `--cfg=kani_host` to build scripts.
         "-Zhost-config",
         "-Ztarget-applies-to-host",

kani-driver/src/coverage/cov_session.rs

@@ -9,6 +9,7 @@ use crate::KaniSession;
 use crate::harness_runner::HarnessResult;
 use crate::project::Project;
 use anyhow::{Result, bail};
+use build_kani::built_info;
 
 impl KaniSession {
     /// Saves metadata required for coverage-related features.
@@ -26,7 +27,7 @@ impl KaniSession {
     }
 
     fn save_coverage_metadata_cargo(&self, project: &Project, stamp: &String) -> Result<()> {
-        let build_target = env!("TARGET");
+        let build_target = built_info::TARGET;
         let metadata = self.cargo_metadata(build_target)?;
         let target_dir = self
             .args
@@ -109,7 +110,7 @@ impl KaniSession {
         results: &Vec<HarnessResult>,
         stamp: &String,
     ) -> Result<()> {
-        let build_target = env!("TARGET");
+        let build_target = built_info::TARGET;
         let metadata = self.cargo_metadata(build_target)?;
         let target_dir = self
             .args

kani-driver/src/list/collect_metadata.rs

@@ -72,10 +72,11 @@ pub fn process_metadata(metadata: Vec<KaniMetadata>) -> BTreeSet<ListMetadata> {
 
 pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
     let quiet = args.common_args.quiet;
+    let verbose = args.common_args.verbose;
     verify_opts.common_args = args.common_args;
     let mut session = KaniSession::new(verify_opts)?;
     if !quiet {
-        print_kani_version(InvocationType::CargoKani(vec![]));
+        print_kani_version(InvocationType::CargoKani(vec![]), verbose);
     }
 
     let project = cargo_project(&mut session, false)?;
@@ -86,10 +87,11 @@ pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Res
 
 pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
     let quiet = args.common_args.quiet;
+    let verbose = args.common_args.verbose;
     verify_opts.common_args = args.common_args;
     let session = KaniSession::new(verify_opts)?;
     if !quiet {
-        print_kani_version(InvocationType::Standalone);
+        print_kani_version(InvocationType::Standalone, verbose);
     }
 
     let project: Project = if args.std {

kani-driver/src/main.rs

@@ -68,6 +68,15 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
     let args = args::CargoKaniArgs::parse_from(&input_args);
     check_is_valid(&args);
 
+    // Handle version flag
+    if args.version {
+        print_kani_version(
+            InvocationType::CargoKani(input_args),
+            args.verify_opts.common_args.verbose,
+        );
+        return Ok(());
+    }
+
     let mut session = match args.command {
         Some(CargoKaniSubcommand::Autoharness(autoharness_args)) => {
             return autoharness_cargo(*autoharness_args);
@@ -82,7 +91,7 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
     };
 
     if !session.args.common_args.quiet {
-        print_kani_version(InvocationType::CargoKani(input_args));
+        print_kani_version(InvocationType::CargoKani(input_args), session.args.common_args.verbose);
     }
 
     let project = project::cargo_project(&mut session, false)?;
@@ -94,6 +103,12 @@ fn standalone_main() -> Result<()> {
     let args = args::StandaloneArgs::parse();
     check_is_valid(&args);
 
+    // Handle version flag
+    if args.version {
+        print_kani_version(InvocationType::Standalone, args.verify_opts.common_args.verbose);
+        return Ok(());
+    }
+
     let (session, project) = match args.command {
         Some(StandaloneSubcommand::Autoharness(args)) => {
             return autoharness_standalone(*args);
@@ -105,7 +120,7 @@ fn standalone_main() -> Result<()> {
         Some(StandaloneSubcommand::VerifyStd(args)) => {
             let session = KaniSession::new(args.verify_opts)?;
             if !session.args.common_args.quiet {
-                print_kani_version(InvocationType::Standalone);
+                print_kani_version(InvocationType::Standalone, session.args.common_args.verbose);
             }
 
             let project = project::std_project(&args.std_path, &session)?;
@@ -114,7 +129,7 @@ fn standalone_main() -> Result<()> {
         None => {
             let session = KaniSession::new(args.verify_opts)?;
             if !session.args.common_args.quiet {
-                print_kani_version(InvocationType::Standalone);
+                print_kani_version(InvocationType::Standalone, session.args.common_args.verbose);
             }
 
             let project =

kani-driver/src/version.rs

@@ -2,30 +2,91 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::InvocationType;
+use anyhow::Result;
+use build_kani::built_info;
+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
 /// make sure it's enforced through CI:
 /// <https://github.com/model-checking/kani/issues/2626>
 pub(crate) const KANI_VERSION: &str = env!("CARGO_PKG_VERSION");
 
-/// Print Kani version. At present, this is only release version information.
-pub(crate) fn print_kani_version(invocation_type: InvocationType) {
-    let kani_version = kani_version_release(invocation_type);
-    // TODO: Print development version information.
-    // <https://github.com/model-checking/kani/issues/2617>
+/// Print Kani version. When verbose is true, also includes rustc version information.
+pub(crate) fn print_kani_version(invocation_type: InvocationType, verbose: bool) {
+    let kani_version = kani_version_release(invocation_type, verbose);
     println!("{kani_version}");
+
+    if verbose {
+        if let Ok(rustc_info) = get_rustc_version_info() {
+            println!("{rustc_info}");
+        } else {
+            println!("rustc version information unavailable");
+        }
+    }
 }
 
 /// Print Kani release version as `Kani Rust Verifier <version> (<invocation>)`
 /// where:
 ///  - `<version>` is the `kani-verifier` version
 ///  - `<invocation>` is `cargo plugin` if Kani was invoked with `cargo kani` or
 ///    `standalone` if it was invoked with `kani`.
-fn kani_version_release(invocation_type: InvocationType) -> String {
+fn kani_version_release(invocation_type: InvocationType, verbose: bool) -> String {
     let invocation_str = match invocation_type {
         InvocationType::CargoKani(_) => "cargo plugin",
         InvocationType::Standalone => "standalone",
     };
-    format!("{KANI_RUST_VERIFIER} {KANI_VERSION} ({invocation_str})")
+    let git_info_opt = if verbose && let Some(git_version) = built_info::GIT_VERSION {
+        if built_info::GIT_DIRTY == Some(true) {
+            format!(" ({git_version}-dirty)")
+        } else {
+            format!(" ({git_version})")
+        }
+    } else {
+        "".to_string()
+    };
+    format!("{KANI_RUST_VERIFIER} {KANI_VERSION}{git_info_opt} ({invocation_str})")
+}
+
+/// Get rustc version and commit information
+fn get_rustc_version_info() -> Result<String> {
+    let output = Command::new("rustc").arg("--version").arg("--verbose").output()?;
+
+    if !output.status.success() {
+        anyhow::bail!("Failed to get rustc version");
+    }
+
+    let version_output = String::from_utf8(output.stdout)?;
+    let lines: Vec<&str> = version_output.lines().collect();
+
+    // Parse the verbose output to extract relevant information
+    let mut rustc_version = None;
+    let mut commit_hash = None;
+    let mut commit_date = None;
+    let mut llvm_version = None;
+
+    for line in lines {
+        if line.starts_with("rustc ") {
+            rustc_version = Some(line.trim());
+        } else if line.starts_with("commit-hash: ") {
+            commit_hash = Some(line.trim_start_matches("commit-hash: ").trim());
+        } else if line.starts_with("commit-date: ") {
+            commit_date = Some(line.trim_start_matches("commit-date: ").trim());
+        } else if line.starts_with("LLVM version: ") {
+            llvm_version = Some(line.trim_start_matches("LLVM version: ").trim());
+        }
+    }
+
+    let mut result = String::new();
+    if let Some(version) = rustc_version {
+        result.push_str(&format!("using {}", version));
+    }
+    if let (Some(hash), Some(date)) = (commit_hash, commit_date) {
+        result.push_str(&format!(" (commit {} {})", &hash[..8.min(hash.len())], date));
+    }
+    if let Some(llvm) = llvm_version {
+        result.push_str(&format!(" with LLVM {}", llvm));
+    }
+
+    Ok(result)
 }

src/os_hacks.rs

@@ -9,6 +9,7 @@ use std::path::Path;
 use std::process::Command;
 
 use anyhow::{Context, Result, bail};
+use build_kani::built_info;
 use os_info::Info;
 
 use crate::cmd::AutoRun;
@@ -39,7 +40,7 @@ fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> {
     // support, we need to look for a different path.
     // Prevents clippy error.
     let target = "x86_64-unknown-linux-gnu";
-    assert!(env!("TARGET") == target);
+    assert!(built_info::TARGET == target);
     if let Ok(linker) = Path::new("/lib64/ld-linux-x86-64.so.2").canonicalize()
         && linker.exists()
         && !linker.to_string_lossy().contains("-stub-ld-")

src/setup.rs

@@ -9,14 +9,15 @@ use std::path::{Path, PathBuf};
 use std::process::Command;
 
 use anyhow::{Context, Result, bail};
+use build_kani::built_info;
 
 use crate::cmd::AutoRun;
 use crate::os_hacks;
 
 /// Comes from our Cargo.toml manifest file. Must correspond to our release verion.
 const VERSION: &str = env!("CARGO_PKG_VERSION");
 /// Set by our `build.rs`, reflects the Rust target triple we're building for
-const TARGET: &str = env!("TARGET");
+const TARGET: &str = built_info::TARGET;
 
 /// The directory where Kani is installed, either:
 ///  * (custom) `${KANI_HOME}/kani-<VERSION>` if the environment variable

tests/ui/version-verbose/expected

@@ -0,0 +1,2 @@
+Kani Rust Verifier \
+using rustc

tests/ui/version-verbose/version_test.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --version --verbose
+//
+// This test validates that the --version --verbose flag works correctly
+// and includes rustc version information.
+
+#[kani::proof]
+fn test_version_verbose() {
+    // This is a simple proof that should always pass
+    assert!(true);
+}

tools/build-kani/Cargo.toml

@@ -11,6 +11,10 @@ publish = false
 
 [dependencies]
 anyhow = "1"
+built = "0.8"
 cargo_metadata = "0.23"
 clap = { version = "4.4.11", features=["derive"] }
 which = "8"
+
+[build-dependencies]
+built = { version = "0.8", features = ["git2"] }

tools/build-kani/build.rs

@@ -1,11 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use std::env::var;
-
 fn main() {
-    // We want to know what target triple we were built with, so "repeat" this info
-    // from the build.rs environment into the normal build environment, so we can
-    // get it with `env!("TARGET")`
-    println!("cargo:rustc-env=TARGET={}", var("TARGET").unwrap());
+    // Collect build environment information
+    built::write_built_file().expect("Failed to acquire build-time information");
 }