Add option to override --crate-name from kani

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
+}