Print Kani version

kani-driver/src/main.rs

@@ -14,6 +14,7 @@ use crate::args::StandaloneSubcommand;
 use crate::concrete_playback::playback::{playback_cargo, playback_standalone};
 use crate::project::Project;
 use crate::session::KaniSession;
+use crate::version::print_kani_version;
 use clap::Parser;
 use tracing::debug;
 
@@ -35,12 +36,15 @@ mod metadata;
 mod project;
 mod session;
 mod util;
+mod version;
 
 /// The main function for the `kani-driver`.
 /// The driver can be invoked via `cargo kani` and `kani` commands, which determines what kind of
 /// project should be verified.
 fn main() -> ExitCode {
-    let result = match determine_invocation_type(Vec::from_iter(std::env::args_os())) {
+    let invocation_type = determine_invocation_type(Vec::from_iter(std::env::args_os()));
+
+    let result = match invocation_type {
         InvocationType::CargoKani(args) => cargokani_main(args),
         InvocationType::Standalone => standalone_main(),
     };
@@ -59,10 +63,15 @@ 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 args = args::CargoKaniArgs::parse_from(input_args);
+    let args = args::CargoKaniArgs::parse_from(&input_args);
     check_is_valid(&args);
+
     let session = session::KaniSession::new(args.verify_opts)?;
 
+    if !session.args.common_args.quiet {
+        print_kani_version(InvocationType::CargoKani(input_args));
+    }
+
     match args.command {
         Some(CargoKaniSubcommand::Assess(args)) => {
             return assess::run_assess(session, *args);
@@ -91,6 +100,11 @@ fn standalone_main() -> Result<()> {
     }
 
     let session = session::KaniSession::new(args.verify_opts)?;
+
+    if !session.args.common_args.quiet {
+        print_kani_version(InvocationType::Standalone);
+    }
+
     let project = project::standalone_project(&args.input.unwrap(), &session)?;
     if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
 }

kani-driver/src/version.rs

@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::InvocationType;
+
+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>
+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>
+    println!("{kani_version}");
+}
+
+/// 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 {
+    let mut version_str = "Kani Rust Verifier ".to_string();
+    version_str.push_str(KANI_VERSION);
+
+    let invocation_str = match invocation_type {
+        InvocationType::CargoKani(_) => "cargo plugin",
+        InvocationType::Standalone => "standalone",
+    };
+    format!("{KANI_RUST_VERIFIER} {KANI_VERSION} ({invocation_str})")
+}

tests/script-based-pre/cargo-kani-version-flag-version/cargo-kani-version-flag-version.expected

@@ -0,0 +1,2 @@
+success: version printed agrees
+success: `(cargo plugin)` appears in version line

tests/script-based-pre/cargo-kani-version-flag-version/cargo-kani-version-flag-version.sh

@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+KANI_VERSION_CMD=`cargo kani --version`
+KANI_VERSION_CMD_VERSION=`echo ${KANI_VERSION_CMD} | awk '{print $2}'`
+
+# Check that the version printed is the same. Note: We use `sed -n '1p'` instead
+# of `head -n 1` to avoid https://github.com/model-checking/kani/issues/2618
+KANI_CARGO_OUTPUT_HEAD=`cd dummy-project; cargo kani | sed -n '1p'`
+KANI_CARGO_OUTPUT_HEAD_VERSION=`echo ${KANI_CARGO_OUTPUT_HEAD} | awk '{print $4}'`
+
+if [[ $KANI_VERSION_CMD_VERSION == $KANI_CARGO_OUTPUT_HEAD_VERSION ]]; then
+    echo "success: version printed agrees"
+else
+    echo "failed: version printed differs ($KANI_VERSION_CMD_VERSION - $KANI_CARGO_OUTPUT_HEAD_VERSION)"
+    exit 1
+fi
+
+KANI_CARGO_OUTPUT_HEAD_MODE=`echo ${KANI_CARGO_OUTPUT_HEAD} | awk '{print $5,$6}'`
+
+# Check that `(cargo plugin)` appears in the version line
+if [[ $KANI_CARGO_OUTPUT_HEAD_MODE == "(cargo plugin)" ]]; then
+    echo "success: \`(cargo plugin)\` appears in version line"
+else
+    echo "failed: expected \`(cargo plugin)\` in version line"
+    exit 1
+fi

tests/script-based-pre/cargo-kani-version-flag-version/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: cargo-kani-version-flag-version.sh
+expected: cargo-kani-version-flag-version.expected

tests/script-based-pre/cargo-kani-version-flag-version/dummy-project/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "dummy-project"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/script-based-pre/cargo-kani-version-flag-version/dummy-project/src/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is used to check that an invocation of `cargo kani` prints the version
+//! and invocation type as expected.
+
+fn main() {
+    println!("Hello, world!");
+}
+
+#[kani::proof]
+fn dummy() {
+    assert!(1 + 1 == 2);
+}

tests/script-based-pre/kani-version-flag-version/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: kani-version-flag-version.sh
+expected: kani-version-flag-version.expected

tests/script-based-pre/kani-version-flag-version/dummy-file.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is used to check that an invocation of `kani` or `cargo kani`
+//! prints the version and invocation type as expected.
+
+#[kani::proof]
+fn dummy() {
+    assert!(1 + 1 == 2);
+}

tests/script-based-pre/kani-version-flag-version/kani-version-flag-version.expected

@@ -0,0 +1,2 @@
+success: version printed agrees
+success: `(standalone)` appears in version line

tests/script-based-pre/kani-version-flag-version/kani-version-flag-version.sh

@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+KANI_VERSION_CMD=`kani --version`
+KANI_VERSION_CMD_VERSION=`echo ${KANI_VERSION_CMD} | awk '{print $2}'`
+
+# Check that the version printed is the same. Note: We use `sed -n '1p'` instead
+# of `head -n 1` to avoid https://github.com/model-checking/kani/issues/2618
+KANI_STANDALONE_OUTPUT_HEAD=`kani dummy-file.rs | sed -n '1p'`
+KANI_STANDALONE_OUTPUT_HEAD_VERSION=`echo ${KANI_STANDALONE_OUTPUT_HEAD} | awk '{print $4}'`
+
+if [[ $KANI_VERSION_CMD_VERSION == $KANI_STANDALONE_OUTPUT_HEAD_VERSION ]]; then
+    echo "success: version printed agrees"
+else
+    echo "failed: version printed differs ($KANI_VERSION_CMD_VERSION - $KANI_STANDALONE_OUTPUT_HEAD_VERSION)"
+    exit 1
+fi
+
+KANI_STANDALONE_OUTPUT_HEAD_MODE=`echo ${KANI_STANDALONE_OUTPUT_HEAD} | awk '{print $5}'`
+
+# Check that `(standalone)` appears in the version line
+if [[ $KANI_STANDALONE_OUTPUT_HEAD_MODE == "(standalone)" ]]; then
+    echo "success: \`(standalone)\` appears in version line"
+else
+    echo "failed: expected \`(standalone)\` in version line"
+    exit 1
+fi