From ea710b36c7ef81b038df4c1a9ef3c18d2f6ab0ef Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 8 Mar 2024 16:42:19 -0500 Subject: [PATCH] Add option to override `--crate-name` from `kani` (#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 #3046 for more details). Resolves #3046 --- kani-driver/src/args/mod.rs | 3 ++ kani-driver/src/main.rs | 2 +- kani-driver/src/project.rs | 27 +++++++--- kani-driver/src/util.rs | 20 ------- .../script-based-pre/crate-name/a/src/lib.rs | 6 +++ .../script-based-pre/crate-name/b/src/lib.rs | 7 +++ .../script-based-pre/crate-name/c/src/lib.rs | 8 +++ tests/script-based-pre/crate-name/config.yml | 4 ++ .../crate-name/crate-name.expected | 1 + .../script-based-pre/crate-name/crate-name.sh | 54 +++++++++++++++++++ tests/script-based-pre/crate-name/my-code.rs | 6 +++ 11 files changed, 111 insertions(+), 27 deletions(-) create mode 100644 tests/script-based-pre/crate-name/a/src/lib.rs create mode 100644 tests/script-based-pre/crate-name/b/src/lib.rs create mode 100644 tests/script-based-pre/crate-name/c/src/lib.rs create mode 100644 tests/script-based-pre/crate-name/config.yml create mode 100644 tests/script-based-pre/crate-name/crate-name.expected create mode 100755 tests/script-based-pre/crate-name/crate-name.sh create mode 100644 tests/script-based-pre/crate-name/my-code.rs diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 39b3c1fd025f7..aeda941688405 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -79,6 +79,9 @@ pub struct StandaloneArgs { #[command(subcommand)] pub command: Option, + + #[arg(long, hide = true)] + pub crate_name: Option, } /// Kani takes optional subcommands to request specialized behavior. diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 009f25b37b5aa..7986255609708 100644 --- a/kani-driver/src/main.rs +++ b/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) } } diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index b99a7e9aff073..fcf3805ab3dff 100644 --- a/kani-driver/src/project.rs +++ b/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 } /// Generate a project directly using `kani-compiler` on a single crate. -pub fn standalone_project(input: &Path, session: &KaniSession) -> Result { - StandaloneProjectBuilder::try_new(input, session)?.build() +pub fn standalone_project( + input: &Path, + crate_name: Option, + session: &KaniSession, +) -> Result { + StandaloneProjectBuilder::try_new(input, crate_name, session)?.build() } /// Builder for a standalone project. @@ -291,7 +295,7 @@ 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 { + fn try_new(input: &Path, krate_name: Option, session: &'a KaniSession) -> Result { // 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. @@ -299,7 +303,7 @@ impl<'a> StandaloneProjectBuilder<'a> { } 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 { // 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 diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index 1e0957dc77267..bfbf9e8d04e15 100644 --- a/kani-driver/src/util.rs +++ b/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 { @@ -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!( diff --git a/tests/script-based-pre/crate-name/a/src/lib.rs b/tests/script-based-pre/crate-name/a/src/lib.rs new file mode 100644 index 0000000000000..bff1d17f864a6 --- /dev/null +++ b/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 +} diff --git a/tests/script-based-pre/crate-name/b/src/lib.rs b/tests/script-based-pre/crate-name/b/src/lib.rs new file mode 100644 index 0000000000000..5a1a11687fcf0 --- /dev/null +++ b/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) +} diff --git a/tests/script-based-pre/crate-name/c/src/lib.rs b/tests/script-based-pre/crate-name/c/src/lib.rs new file mode 100644 index 0000000000000..b4dadd69e1be0 --- /dev/null +++ b/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) +} diff --git a/tests/script-based-pre/crate-name/config.yml b/tests/script-based-pre/crate-name/config.yml new file mode 100644 index 0000000000000..f022a9c037325 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/crate-name/crate-name.expected b/tests/script-based-pre/crate-name/crate-name.expected new file mode 100644 index 0000000000000..1a4e02d1ff62b --- /dev/null +++ b/tests/script-based-pre/crate-name/crate-name.expected @@ -0,0 +1 @@ +No proof harnesses (functions with #[kani::proof]) were found to verify. diff --git a/tests/script-based-pre/crate-name/crate-name.sh b/tests/script-based-pre/crate-name/crate-name.sh new file mode 100755 index 0000000000000..229cc36938f9d --- /dev/null +++ b/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=` 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=` 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=` 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 diff --git a/tests/script-based-pre/crate-name/my-code.rs b/tests/script-based-pre/crate-name/my-code.rs new file mode 100644 index 0000000000000..bff1d17f864a6 --- /dev/null +++ b/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 +}