From 244acd9add8ef6fb8b8f4d363e607cb92b28ecac Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 11 Nov 2025 12:13:31 +0000 Subject: [PATCH 1/2] Add git revision and rustc version info to verbose version output Enhances the `cargo kani --version --verbose` command to display comprehensive information about the underlying Rust compiler that Kani is using, including the rustc version, git commit hash, commit date, and LLVM version. While at it, also adds git build revision output to said verbose version output. The output of `kani --version --verbose` now looks like this: ``` Kani Rust Verifier 0.66.0 (kani-0.66.0-10-g21a9b31-dirty) (standalone) using rustc 1.93.0-nightly (29a69716f 2025-11-10) (commit 29a69716 2025-11-10) with LLVM 21.1.5 ``` Resolves: #2617 Resolves: #2872 --- Cargo.lock | 344 +++++++++++++++++++++++ Cargo.toml | 1 + kani-driver/Cargo.toml | 1 + kani-driver/src/args/mod.rs | 18 +- kani-driver/src/autoharness/mod.rs | 4 +- kani-driver/src/call_cargo.rs | 5 +- kani-driver/src/coverage/cov_session.rs | 5 +- kani-driver/src/list/collect_metadata.rs | 6 +- kani-driver/src/main.rs | 21 +- kani-driver/src/version.rs | 75 ++++- src/os_hacks.rs | 3 +- src/setup.rs | 3 +- tests/ui/version-verbose/expected | 2 + tests/ui/version-verbose/version_test.rs | 13 + tools/build-kani/Cargo.toml | 4 + tools/build-kani/build.rs | 8 +- tools/build-kani/src/main.rs | 3 +- tools/build-kani/src/sysroot.rs | 3 +- 18 files changed, 486 insertions(+), 33 deletions(-) create mode 100644 tests/ui/version-verbose/expected create mode 100644 tests/ui/version-verbose/version_test.rs diff --git a/Cargo.lock b/Cargo.lock index 786f6056a360..c43a4e20ecaf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -181,11 +181,21 @@ name = "build-kani" version = "0.66.0" dependencies = [ "anyhow", + "built", "cargo_metadata", "clap", "which 8.0.0", ] +[[package]] +name = "built" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f4ad8f11f288f48ca24471bbd51ac257aaeaaa07adae295591266b792902ae64" +dependencies = [ + "git2", +] + [[package]] name = "bumpalo" version = "3.19.0" @@ -237,6 +247,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "35900b6c8d709fb1d854671ae27aeaa9eec2f8b01b364e1619a40da3e6fe2afe" dependencies = [ "find-msvc-tools", + "jobserver", + "libc", "shlex", ] @@ -610,6 +622,17 @@ dependencies = [ "crypto-common", ] +[[package]] +name = "displaydoc" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "document-features" version = "0.2.12" @@ -712,6 +735,15 @@ version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" +[[package]] +name = "form_urlencoded" +version = "1.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb4cb245038516f5f85277875cdaa4f7d2c9a0fa0468de06ed190163b1581fcf" +dependencies = [ + "percent-encoding", +] + [[package]] name = "generic-array" version = "0.14.9" @@ -743,6 +775,19 @@ dependencies = [ "wasip2", ] +[[package]] +name = "git2" +version = "0.20.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2deb07a133b1520dc1a5690e9bd08950108873d7ed5de38dcc74d3b5ebffa110" +dependencies = [ + "bitflags", + "libc", + "libgit2-sys", + "log", + "url", +] + [[package]] name = "glob" version = "0.3.3" @@ -813,12 +858,114 @@ dependencies = [ "cc", ] +[[package]] +name = "icu_collections" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c6b649701667bbe825c3b7e6388cb521c23d88644678e83c0c4d0a621a34b43" +dependencies = [ + "displaydoc", + "potential_utf", + "yoke", + "zerofrom", + "zerovec", +] + +[[package]] +name = "icu_locale_core" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "edba7861004dd3714265b4db54a3c390e880ab658fec5f7db895fae2046b5bb6" +dependencies = [ + "displaydoc", + "litemap", + "tinystr", + "writeable", + "zerovec", +] + +[[package]] +name = "icu_normalizer" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5f6c8828b67bf8908d82127b2054ea1b4427ff0230ee9141c54251934ab1b599" +dependencies = [ + "icu_collections", + "icu_normalizer_data", + "icu_properties", + "icu_provider", + "smallvec", + "zerovec", +] + +[[package]] +name = "icu_normalizer_data" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7aedcccd01fc5fe81e6b489c15b247b8b0690feb23304303a9e560f37efc560a" + +[[package]] +name = "icu_properties" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e93fcd3157766c0c8da2f8cff6ce651a31f0810eaa1c51ec363ef790bbb5fb99" +dependencies = [ + "icu_collections", + "icu_locale_core", + "icu_properties_data", + "icu_provider", + "zerotrie", + "zerovec", +] + +[[package]] +name = "icu_properties_data" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "02845b3647bb045f1100ecd6480ff52f34c35f82d9880e029d329c21d1054899" + +[[package]] +name = "icu_provider" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85962cf0ce02e1e0a629cc34e7ca3e373ce20dda4c4d7294bbd0bf1fdb59e614" +dependencies = [ + "displaydoc", + "icu_locale_core", + "writeable", + "yoke", + "zerofrom", + "zerotrie", + "zerovec", +] + [[package]] name = "ident_case" version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" +[[package]] +name = "idna" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3b0875f23caa03898994f6ddc501886a45c7d3d62d04d2d90788d47be1b1e4de" +dependencies = [ + "idna_adapter", + "smallvec", + "utf8_iter", +] + +[[package]] +name = "idna_adapter" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3acae9609540aa318d1bc588455225fb2085b9ed0c4f6bd0d9d5bcd86f1a0344" +dependencies = [ + "icu_normalizer", + "icu_properties", +] + [[package]] name = "indent_write" version = "2.2.0" @@ -909,6 +1056,16 @@ dependencies = [ "syn", ] +[[package]] +name = "jobserver" +version = "0.1.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9afb3de4395d6b3e67a780b6de64b51c978ecf11cb9a462c66be7d4ca9039d33" +dependencies = [ + "getrandom", + "libc", +] + [[package]] name = "joinery" version = "2.1.0" @@ -976,6 +1133,7 @@ name = "kani-driver" version = "0.66.0" dependencies = [ "anyhow", + "build-kani", "cargo_metadata", "chrono", "clap", @@ -1006,6 +1164,7 @@ name = "kani-verifier" version = "0.66.0" dependencies = [ "anyhow", + "build-kani", "home", "os_info", ] @@ -1053,6 +1212,30 @@ version = "0.2.177" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2874a2af47a2325c2001a6e6fad9b16a53b802102b528163885171cf92b15976" +[[package]] +name = "libgit2-sys" +version = "0.18.2+1.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1c42fe03df2bd3c53a3a9c7317ad91d80c81cd1fb0caec8d7cc4cd2bfa10c222" +dependencies = [ + "cc", + "libc", + "libz-sys", + "pkg-config", +] + +[[package]] +name = "libz-sys" +version = "1.1.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8b70e7a7df205e92a1a4cd9aaae7898dac0aa555503cc0a649494d0d60e7651d" +dependencies = [ + "cc", + "libc", + "pkg-config", + "vcpkg", +] + [[package]] name = "linear-map" version = "1.2.0" @@ -1069,6 +1252,12 @@ version = "0.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "df1d3c3b53da64cf5760482273a98e575c651a67eec7f77df96b5b642de8f039" +[[package]] +name = "litemap" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77" + [[package]] name = "litrs" version = "1.0.0" @@ -1318,6 +1507,12 @@ version = "0.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "df94ce210e5bc13cb6651479fa48d14f601d9858cfe0467f43ae157023b938d3" +[[package]] +name = "percent-encoding" +version = "2.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220" + [[package]] name = "petgraph" version = "0.6.5" @@ -1346,6 +1541,12 @@ version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3b3cff922bd51709b605d9ead9aa71031d81447142d828eb4a6eba76fe619f9b" +[[package]] +name = "pkg-config" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7edddbd0b52d732b21ad9a5fab5c704c14cd949e5e9a1ec5929a24fded1b904c" + [[package]] name = "plist" version = "1.8.0" @@ -1374,6 +1575,15 @@ dependencies = [ "portable-atomic", ] +[[package]] +name = "potential_utf" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b73949432f5e2a09657003c25bca5e19a0e9c84f8058ca374f49e0ebe605af77" +dependencies = [ + "zerovec", +] + [[package]] name = "powerfmt" version = "0.2.0" @@ -1768,6 +1978,12 @@ version = "1.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" +[[package]] +name = "stable_deref_trait" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" + [[package]] name = "stacker" version = "0.1.22" @@ -1839,6 +2055,17 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "synstructure" +version = "0.13.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "take_mut" version = "0.2.2" @@ -1946,6 +2173,16 @@ dependencies = [ "time-core", ] +[[package]] +name = "tinystr" +version = "0.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42d3e9c45c09de15d06dd8acf5f4e0e399e85927b7f00711024eb7ae10fa4869" +dependencies = [ + "displaydoc", + "zerovec", +] + [[package]] name = "to_markdown_table" version = "0.1.5" @@ -2208,6 +2445,24 @@ version = "0.2.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "673aac59facbab8a9007c7f6108d11f63b603f7cabff99fabf650fea5c32b861" +[[package]] +name = "url" +version = "2.5.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08bc136a29a3d1758e07a9cca267be308aeebf5cfd5a10f3f67ab2097683ef5b" +dependencies = [ + "form_urlencoded", + "idna", + "percent-encoding", + "serde", +] + +[[package]] +name = "utf8_iter" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6c140620e7ffbb22c2dee59cafe6084a59b5ffc27a8859a5f0d494b5d52b6be" + [[package]] name = "utf8parse" version = "0.2.2" @@ -2220,6 +2475,12 @@ version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ba73ea9cf16a25df0c8caa16c51acb937d5712a8429db78a3ee29d5dcacd3a65" +[[package]] +name = "vcpkg" +version = "0.2.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426" + [[package]] name = "version_check" version = "0.9.5" @@ -2604,6 +2865,35 @@ version = "0.46.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f17a85883d4e6d00e8a97c586de764dabcc06133f7f1d55dce5cdc070ad7fe59" +[[package]] +name = "writeable" +version = "0.6.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9edde0db4769d2dc68579893f2306b26c6ecfbe0ef499b013d731b7b9247e0b9" + +[[package]] +name = "yoke" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72d6e5c6afb84d73944e5cedb052c4680d5657337201555f9f2a16b7406d4954" +dependencies = [ + "stable_deref_trait", + "yoke-derive", + "zerofrom", +] + +[[package]] +name = "yoke-derive" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b659052874eb698efe5b9e8cf382204678a0086ebf46982b79d6ca3182927e5d" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "synstructure", +] + [[package]] name = "zerocopy" version = "0.8.27" @@ -2623,3 +2913,57 @@ dependencies = [ "quote", "syn", ] + +[[package]] +name = "zerofrom" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "50cc42e0333e05660c3587f3bf9d0478688e15d870fab3346451ce7f8c9fbea5" +dependencies = [ + "zerofrom-derive", +] + +[[package]] +name = "zerofrom-derive" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d71e5d6e06ab090c67b5e44993ec16b72dcbaabc526db883a360057678b48502" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "synstructure", +] + +[[package]] +name = "zerotrie" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2a59c17a5562d507e4b54960e8569ebee33bee890c70aa3fe7b97e85a9fd7851" +dependencies = [ + "displaydoc", + "yoke", + "zerofrom", +] + +[[package]] +name = "zerovec" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c28719294829477f525be0186d13efa9a3c602f7ec202ca9e353d310fb9a002" +dependencies = [ + "yoke", + "zerofrom", + "zerovec-derive", +] + +[[package]] +name = "zerovec-derive" +version = "0.11.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eadce39539ca5cb3985590102671f2567e659fca9666581ad3411d59207951f3" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] diff --git a/Cargo.toml b/Cargo.toml index 2d82261b3ec1..5e54cf7c68d5 100644 --- a/Cargo.toml +++ b/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 } diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 7953044c054b..0718dc5b99f5 100644 --- a/kani-driver/Cargo.toml +++ b/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" diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 2481d2477554..d1d872bca871 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -140,17 +140,17 @@ impl From 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, #[command(flatten)] @@ -161,6 +161,10 @@ pub struct StandaloneArgs { #[arg(long, hide = true)] pub crate_name: Option, + + /// Print version information + #[arg(long, short = 'V')] + pub version: bool, } /// Kani takes optional subcommands to request specialized behavior. @@ -179,10 +183,10 @@ 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)] @@ -190,6 +194,10 @@ pub struct CargoKaniArgs { #[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 diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 01904bb786d6..2e339a588f0a 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/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 { diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index fbcd09c4c835..8f147f6766e2 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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 { - 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 { [ "--target", - env!("TARGET"), + built_info::TARGET, // Propagate `--cfg=kani_host` to build scripts. "-Zhost-config", "-Ztarget-applies-to-host", diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs index 60fa2f1c242f..6ef0ee886b0f 100644 --- a/kani-driver/src/coverage/cov_session.rs +++ b/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, 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 diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index c0d452ee6051..66befa895e97 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -72,10 +72,11 @@ pub fn process_metadata(metadata: Vec) -> BTreeSet { 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 { diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 21b74e8672c7..d644ca133194 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -68,6 +68,15 @@ fn cargokani_main(input_args: Vec) -> 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) -> 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 = diff --git a/kani-driver/src/version.rs b/kani-driver/src/version.rs index e1b995c3cd53..24f8ed311e8d 100644 --- a/kani-driver/src/version.rs +++ b/kani-driver/src/version.rs @@ -2,6 +2,9 @@ // 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 @@ -9,12 +12,18 @@ const KANI_RUST_VERIFIER: &str = "Kani Rust Verifier"; /// 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. - // +/// 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 ()` @@ -22,10 +31,62 @@ pub(crate) fn print_kani_version(invocation_type: InvocationType) { /// - `` is the `kani-verifier` version /// - `` 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 { + 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) } diff --git a/src/os_hacks.rs b/src/os_hacks.rs index 0a149a005934..38a371e04fc5 100644 --- a/src/os_hacks.rs +++ b/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 Path::new("/lib64/ld-linux-x86-64.so.2").exists() { // if the expected path exists, I guess things are fine? return Ok(()); diff --git a/src/setup.rs b/src/setup.rs index b33e69b15ec9..a48aa15d9e0b 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -9,6 +9,7 @@ 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; @@ -16,7 +17,7 @@ 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-` if the environment variable diff --git a/tests/ui/version-verbose/expected b/tests/ui/version-verbose/expected new file mode 100644 index 000000000000..13abbd32c876 --- /dev/null +++ b/tests/ui/version-verbose/expected @@ -0,0 +1,2 @@ +Kani Rust Verifier \ +using rustc diff --git a/tests/ui/version-verbose/version_test.rs b/tests/ui/version-verbose/version_test.rs new file mode 100644 index 000000000000..0012b0484a7e --- /dev/null +++ b/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); +} diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 9ab61c04929d..709e994b3b2c 100644 --- a/tools/build-kani/Cargo.toml +++ b/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"] } diff --git a/tools/build-kani/build.rs b/tools/build-kani/build.rs index c01b82b23c44..fce0201a9a52 100644 --- a/tools/build-kani/build.rs +++ b/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"); } diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 1e37cba165a0..9791b828b917 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -14,6 +14,7 @@ use crate::sysroot::{ build_bin, build_lib, build_tools, kani_no_core_lib, kani_playback_lib, kani_sysroot_lib, }; use anyhow::{Result, bail}; +use build_kani::built_info; use clap::Parser; use std::{ffi::OsString, path::Path, process::Command}; @@ -31,7 +32,7 @@ fn main() -> Result<()> { parser::Commands::Bundle(bundle_parser) => { let version_string = bundle_parser.version; let kani_string = format!("kani-{version_string}"); - let bundle_name = format!("{kani_string}-{}.tar.gz", env!("TARGET")); + let bundle_name = format!("{kani_string}-{}.tar.gz", built_info::TARGET); let dir = Path::new(&kani_string); // Check everything is ready before we start copying files diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index bb8708a14f68..01e73c92e247 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -13,6 +13,7 @@ use crate::{AutoRun, cp}; use anyhow::{Result, bail, format_err}; +use build_kani::built_info; use cargo_metadata::{Artifact, Message, TargetKind}; use std::ffi::OsStr; use std::fs; @@ -67,7 +68,7 @@ fn kani_sysroot_bin() -> PathBuf { /// Returns the build target fn build_target() -> &'static str { - env!("TARGET") + built_info::TARGET } /// Build the `lib/` folder and `lib-playback/` for the new sysroot. From f00c07c86aded031f98d491c2333870b9f4889a3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Nov 2025 11:18:23 +0000 Subject: [PATCH 2/2] Add missing file --- tools/build-kani/src/lib.rs | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 tools/build-kani/src/lib.rs diff --git a/tools/build-kani/src/lib.rs b/tools/build-kani/src/lib.rs new file mode 100644 index 000000000000..59bafdd28b2d --- /dev/null +++ b/tools/build-kani/src/lib.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub mod built_info { + // The file has been placed there by the build script. + include!(concat!(env!("OUT_DIR"), "/built.rs")); +}