Add option to override --crate-name from kani (rust-lang#3054)

Adds a hidden `--crate-name` option to standalone Kani (i.e., `kani`)
only. This option allows users to override the crate name used during
the compilation of single-file Rust programs, making it easier to apply
Kani to non-Cargo projects (see rust-lang#3046 for more details).

Resolves rust-lang#3046

Author: adpaco-aws

kani-driver/src/args/mod.rs

@@ -79,6 +79,9 @@ pub struct StandaloneArgs {
 
     #[command(subcommand)]
     pub command: Option<StandaloneSubcommand>,
+
+    #[arg(long, hide = true)]
+    pub crate_name: Option<String>,
 }
 
 /// Kani takes optional subcommands to request specialized behavior.

kani-driver/src/main.rs

@@ -104,7 +104,7 @@ fn standalone_main() -> Result<()> {
         print_kani_version(InvocationType::Standalone);
     }
 
-    let project = project::standalone_project(&args.input.unwrap(), &session)?;
+    let project = project::standalone_project(&args.input.unwrap(), args.crate_name, &session)?;
     if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
 }
 

kani-driver/src/project.rs

@@ -18,7 +18,7 @@
 
 use crate::metadata::{from_json, merge_kani_metadata, mock_proof_harness};
 use crate::session::KaniSession;
-use crate::util::{crate_name, guess_rlib_name};
+use crate::util::crate_name;
 use anyhow::{Context, Result};
 use kani_metadata::{
     artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata,
@@ -270,8 +270,12 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result<Project>
 }
 
 /// Generate a project directly using `kani-compiler` on a single crate.
-pub fn standalone_project(input: &Path, session: &KaniSession) -> Result<Project> {
-    StandaloneProjectBuilder::try_new(input, session)?.build()
+pub fn standalone_project(
+    input: &Path,
+    crate_name: Option<String>,
+    session: &KaniSession,
+) -> Result<Project> {
+    StandaloneProjectBuilder::try_new(input, crate_name, session)?.build()
 }
 
 /// Builder for a standalone project.
@@ -291,15 +295,15 @@ struct StandaloneProjectBuilder<'a> {
 impl<'a> StandaloneProjectBuilder<'a> {
     /// Create a `StandaloneProjectBuilder` from the given input and session.
     /// This will perform a few validations before the build.
-    fn try_new(input: &Path, session: &'a KaniSession) -> Result<Self> {
+    fn try_new(input: &Path, krate_name: Option<String>, session: &'a KaniSession) -> Result<Self> {
         // Ensure the directory exist and it's in its canonical form.
         let outdir = if let Some(target_dir) = &session.args.target_dir {
             std::fs::create_dir_all(target_dir)?; // This is a no-op if directory exists.
             target_dir.canonicalize()?
         } else {
             input.canonicalize().unwrap().parent().unwrap().to_path_buf()
         };
-        let crate_name = crate_name(&input);
+        let crate_name = if let Some(name) = krate_name { name } else { crate_name(&input) };
         let metadata = standalone_artifact(&outdir, &crate_name, Metadata);
         Ok(StandaloneProjectBuilder {
             outdir,
@@ -313,7 +317,7 @@ impl<'a> StandaloneProjectBuilder<'a> {
     /// Build a project by compiling `self.input` file.
     fn build(self) -> Result<Project> {
         // Register artifacts that may be generated by the compiler / linker for future deletion.
-        let rlib_path = guess_rlib_name(&self.outdir.join(self.input.file_name().unwrap()));
+        let rlib_path = self.rlib_name();
         self.session.record_temporary_file(&rlib_path);
         self.session.record_temporary_file(&self.metadata.path);
 
@@ -339,6 +343,17 @@ impl<'a> StandaloneProjectBuilder<'a> {
         }
         result
     }
+
+    /// Build the rlib name from the crate name.
+    /// This is only used by 'kani', never 'cargo-kani', so we hopefully don't have too many corner
+    /// cases to deal with.
+    fn rlib_name(&self) -> PathBuf {
+        let path = &self.outdir.join(self.input.file_name().unwrap());
+        let basedir = path.parent().unwrap_or(Path::new("."));
+        let rlib_name = format!("lib{}.rlib", self.crate_name);
+
+        basedir.join(rlib_name)
+    }
 }
 
 /// Generate a `KaniMetadata` by extending the original metadata to contain the function under

kani-driver/src/util.rs

@@ -26,18 +26,6 @@ pub fn crate_name(path: &Path) -> String {
     stem.replace(['-', '.'], "_")
 }
 
-/// Attempt to guess the rlib name for rust source file.
-/// This is only used by 'kani', never 'cargo-kani', so we hopefully don't have too many corner
-/// cases to deal with.
-/// In rustc, you can find some code dealing this this naming in:
-///      compiler/rustc_codegen_ssa/src/back/link.rs
-pub fn guess_rlib_name(path: &Path) -> PathBuf {
-    let basedir = path.parent().unwrap_or(Path::new("."));
-    let rlib_name = format!("lib{}.rlib", crate_name(path));
-
-    basedir.join(rlib_name)
-}
-
 /// Given a path of some sort (usually from argv0), this attempts to extract the basename / stem
 /// of the executable. e.g. "/path/foo -> foo" "./foo.exe -> foo" "foo -> foo"
 pub fn executable_basename(argv0: &Option<&OsString>) -> Option<OsString> {
@@ -117,14 +105,6 @@ mod tests {
         assert_eq!(alter_extension(&q, "symtab.json"), PathBuf::from("file.more.symtab.json"));
     }
 
-    #[test]
-    fn check_guess_rlib_name() {
-        assert_eq!(guess_rlib_name(Path::new("mycrate.rs")), PathBuf::from("libmycrate.rlib"));
-        assert_eq!(guess_rlib_name(Path::new("my-crate.rs")), PathBuf::from("libmy_crate.rlib"));
-        assert_eq!(guess_rlib_name(Path::new("./foo.rs")), PathBuf::from("./libfoo.rlib"));
-        assert_eq!(guess_rlib_name(Path::new("a/b/foo.rs")), PathBuf::from("a/b/libfoo.rlib"));
-    }
-
     #[test]
     fn check_exe_basename() {
         assert_eq!(

tests/script-based-pre/crate-name/a/src/lib.rs

@@ -0,0 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn add_a(left: usize, right: usize) -> usize {
+    left + right
+}

tests/script-based-pre/crate-name/b/src/lib.rs

@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+extern crate a;
+
+pub fn add_b(left: usize, right: usize) -> usize {
+    a::add_a(left, right)
+}

tests/script-based-pre/crate-name/c/src/lib.rs

@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+extern crate a;
+extern crate b;
+
+pub fn add_c(left: usize, right: usize) -> usize {
+    b::add_b(left, right)
+}

tests/script-based-pre/crate-name/config.yml

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

tests/script-based-pre/crate-name/crate-name.expected

@@ -0,0 +1 @@
+No proof harnesses (functions with #[kani::proof]) were found to verify.

tests/script-based-pre/crate-name/crate-name.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This test performs multiple checks focused on crate names. The first steps
+# check expected results with the default naming scheme. The remaining ones
+# check expected results with the `--crate-name=<name>` feature which allows
+# users to specify the crate name used for compilation with standalone `kani`.
+set -eu
+
+check_file_exists() {
+    local file=$1
+    if ! [ -e "${file}" ]
+    then
+        echo "error: expected \`${file}\` to have been generated"
+        exit 1
+    fi
+}
+
+# 1. Check expected results with the default naming scheme.
+# Note: The assumed crate name is `lib`, so we generate `liblib.rlib`.
+kani --only-codegen --keep-temps a/src/lib.rs
+check_file_exists a/src/liblib.rlib
+check_file_exists a/src/lib.kani-metadata.json
+rm a/src/liblib.rlib
+rm a/src/lib.kani-metadata.json
+
+# 2. Check expected results with the default naming scheme, which replaces
+#    some characters.
+# Note: The assumed crate name is `my-code`, so we generate `libmy_code.rlib`.
+kani --only-codegen --keep-temps my-code.rs
+check_file_exists libmy_code.rlib
+check_file_exists my_code.kani-metadata.json
+
+# 3. Check expected results with the `--crate-name=<name>` feature. This feature
+#    allows users to specify the crate name used for compilation with standalone
+#    `kani`, enabling the compilation of multiple dependencies with similar
+#    names.
+# Note: In the example below, compiling without `--crate-name=<name>` would
+# result in files named `liblib.rlib` for each dependency.
+kani --only-codegen --keep-temps a/src/lib.rs --crate-name="a"
+check_file_exists a/src/liba.rlib
+check_file_exists a/src/a.kani-metadata.json
+
+RUSTFLAGS="--extern a=a/src/liba.rlib" kani --only-codegen --keep-temps b/src/lib.rs --crate-name="b"
+check_file_exists b/src/libb.rlib
+check_file_exists b/src/b.kani-metadata.json
+
+RUSTFLAGS="--extern b=b/src/libb.rlib --extern a=a/src/liba.rlib" kani c/src/lib.rs
+
+rm a/src/liba.rlib
+rm a/src/a.kani-metadata.json
+rm b/src/libb.rlib
+rm b/src/b.kani-metadata.json

tests/script-based-pre/crate-name/my-code.rs

@@ -0,0 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn add_a(left: usize, right: usize) -> usize {
+    left + right
+}