diff --git a/Cargo.lock b/Cargo.lock index 34aa59db806..4ed0754589a 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" @@ -977,6 +1134,7 @@ name = "kani-driver" version = "0.66.0" dependencies = [ "anyhow", + "build-kani", "cargo_metadata", "chrono", "clap", @@ -1007,6 +1165,7 @@ name = "kani-verifier" version = "0.66.0" dependencies = [ "anyhow", + "build-kani", "home", "os_info", ] @@ -1054,6 +1213,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" @@ -1070,6 +1253,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" @@ -1319,6 +1508,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" @@ -1347,6 +1542,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" @@ -1375,6 +1576,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" @@ -1769,6 +1979,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" @@ -1840,6 +2056,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" @@ -1947,6 +2174,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" @@ -2209,6 +2446,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" @@ -2221,6 +2476,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" @@ -2605,6 +2866,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" @@ -2624,3 +2914,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 2d82261b3ec..5e54cf7c68d 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 7953044c054..0718dc5b99f 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 2481d247755..d1d872bca87 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 01904bb786d..2e339a588f0 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 fbcd09c4c83..8f147f6766e 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 60fa2f1c242..6ef0ee886b0 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 c0d452ee605..66befa895e9 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 21b74e8672c..d644ca13319 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 e1b995c3cd5..24f8ed311e8 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 15bd1153887..f8faf9fea10 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 let Ok(linker) = Path::new("/lib64/ld-linux-x86-64.so.2").canonicalize() && linker.exists() && !linker.to_string_lossy().contains("-stub-ld-") diff --git a/src/setup.rs b/src/setup.rs index b33e69b15ec..a48aa15d9e0 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 00000000000..13abbd32c87 --- /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 00000000000..0012b0484a7 --- /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 9ab61c04929..709e994b3b2 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 c01b82b23c4..fce0201a9a5 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/lib.rs b/tools/build-kani/src/lib.rs new file mode 100644 index 00000000000..59bafdd28b2 --- /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")); +} diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 1e37cba165a..9791b828b91 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 bb8708a14f6..01e73c92e24 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.