From 9091c52d3c9f04a3cc2ea90a29682da715eb6883 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 1 Mar 2024 22:28:23 +0000 Subject: [PATCH 1/7] Add `--crate-name` option to `StandaloneArgs` --- kani-driver/src/args/mod.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 39b3c1fd025f..48858f2c7f85 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, requires("enable_unstable"))] + pub crate_name: Option, } /// Kani takes optional subcommands to request specialized behavior. From f85da7312c5e501b8e6ae1cd5e8c00ce56d616b1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 1 Mar 2024 22:28:49 +0000 Subject: [PATCH 2/7] Pass crate name argument to standalone project --- kani-driver/src/main.rs | 2 +- kani-driver/src/project.rs | 12 ++++++++---- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 009f25b37b5a..798625560970 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 b99a7e9aff07..75c1026b8fe9 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -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, From 1e9531b6f1a4e56cef02a5e10432f9fc8f67b788 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 7 Mar 2024 16:42:11 +0000 Subject: [PATCH 3/7] Convert rlib name getter into method --- kani-driver/src/project.rs | 15 +++++++++++++-- kani-driver/src/util.rs | 20 -------------------- 2 files changed, 13 insertions(+), 22 deletions(-) diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 75c1026b8fe9..fcf3805ab3df 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, @@ -317,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); @@ -343,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 1e0957dc7726..bfbf9e8d04e1 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!( From 6f47efbf897e2518e6eb0d9becf5ae9d1608f8a2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 7 Mar 2024 16:44:06 +0000 Subject: [PATCH 4/7] Don't require `--enable-unstable` --- kani-driver/src/args/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 48858f2c7f85..aeda94168840 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -80,7 +80,7 @@ pub struct StandaloneArgs { #[command(subcommand)] pub command: Option, - #[arg(long, hide = true, requires("enable_unstable"))] + #[arg(long, hide = true)] pub crate_name: Option, } From faceae87a6196258e6687c331810c8800bafc68a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Mar 2024 15:22:15 +0000 Subject: [PATCH 5/7] Add script-based test --- .../crate-name-default/a/src/lib.rs | 6 +++ .../crate-name-default/b/src/lib.rs | 7 ++++ .../crate-name-default/c/src/lib.rs | 7 ++++ .../crate-name-default/config.yml | 3 ++ .../crate-name-default/crate-name-default.sh | 39 +++++++++++++++++++ .../crate-name-default/my-code.rs | 6 +++ 6 files changed, 68 insertions(+) create mode 100644 tests/script-based-pre/crate-name-default/a/src/lib.rs create mode 100644 tests/script-based-pre/crate-name-default/b/src/lib.rs create mode 100644 tests/script-based-pre/crate-name-default/c/src/lib.rs create mode 100644 tests/script-based-pre/crate-name-default/config.yml create mode 100755 tests/script-based-pre/crate-name-default/crate-name-default.sh create mode 100644 tests/script-based-pre/crate-name-default/my-code.rs diff --git a/tests/script-based-pre/crate-name-default/a/src/lib.rs b/tests/script-based-pre/crate-name-default/a/src/lib.rs new file mode 100644 index 000000000000..bff1d17f864a --- /dev/null +++ b/tests/script-based-pre/crate-name-default/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-default/b/src/lib.rs b/tests/script-based-pre/crate-name-default/b/src/lib.rs new file mode 100644 index 000000000000..5a1a11687fcf --- /dev/null +++ b/tests/script-based-pre/crate-name-default/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-default/c/src/lib.rs b/tests/script-based-pre/crate-name-default/c/src/lib.rs new file mode 100644 index 000000000000..4031c04a9775 --- /dev/null +++ b/tests/script-based-pre/crate-name-default/c/src/lib.rs @@ -0,0 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +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-default/config.yml b/tests/script-based-pre/crate-name-default/config.yml new file mode 100644 index 000000000000..d72240852e2f --- /dev/null +++ b/tests/script-based-pre/crate-name-default/config.yml @@ -0,0 +1,3 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: crate-name-default.sh diff --git a/tests/script-based-pre/crate-name-default/crate-name-default.sh b/tests/script-based-pre/crate-name-default/crate-name-default.sh new file mode 100755 index 000000000000..a9e94744b5c6 --- /dev/null +++ b/tests/script-based-pre/crate-name-default/crate-name-default.sh @@ -0,0 +1,39 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +check_file_exists() { + local file=$1 + if ! [ -e "${file}" ] + then + echo "error: expected \`${file}\` to have been generated" + exit 1 + fi +} + +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 + +kani --only-codegen --keep-temps my-code.rs +check_file_exists libmy_code.rlib +check_file_exists my_code.kani-metadata.json + +RUSTFLAGS="--edition 2021" 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="--edition 2021 --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="--edition 2021 --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-default/my-code.rs b/tests/script-based-pre/crate-name-default/my-code.rs new file mode 100644 index 000000000000..bff1d17f864a --- /dev/null +++ b/tests/script-based-pre/crate-name-default/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 +} From 21c9168710e045e699779a92e712e6197989c032 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Mar 2024 15:55:58 +0000 Subject: [PATCH 6/7] Add `extern crate a;` to `c` --- tests/script-based-pre/crate-name-default/c/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/script-based-pre/crate-name-default/c/src/lib.rs b/tests/script-based-pre/crate-name-default/c/src/lib.rs index 4031c04a9775..b4dadd69e1be 100644 --- a/tests/script-based-pre/crate-name-default/c/src/lib.rs +++ b/tests/script-based-pre/crate-name-default/c/src/lib.rs @@ -1,5 +1,6 @@ // 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 { From b2e765f3a0f909fe29b5ac06a13c00b0fc38a53c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Mar 2024 16:28:59 +0000 Subject: [PATCH 7/7] Rename and add comments to script --- .../crate-name-default/crate-name-default.sh | 39 -------------- .../a/src/lib.rs | 0 .../b/src/lib.rs | 0 .../c/src/lib.rs | 0 .../config.yml | 3 +- .../crate-name/crate-name.expected | 1 + .../script-based-pre/crate-name/crate-name.sh | 54 +++++++++++++++++++ .../my-code.rs | 0 8 files changed, 57 insertions(+), 40 deletions(-) delete mode 100755 tests/script-based-pre/crate-name-default/crate-name-default.sh rename tests/script-based-pre/{crate-name-default => crate-name}/a/src/lib.rs (100%) rename tests/script-based-pre/{crate-name-default => crate-name}/b/src/lib.rs (100%) rename tests/script-based-pre/{crate-name-default => crate-name}/c/src/lib.rs (100%) rename tests/script-based-pre/{crate-name-default => crate-name}/config.yml (59%) create mode 100644 tests/script-based-pre/crate-name/crate-name.expected create mode 100755 tests/script-based-pre/crate-name/crate-name.sh rename tests/script-based-pre/{crate-name-default => crate-name}/my-code.rs (100%) diff --git a/tests/script-based-pre/crate-name-default/crate-name-default.sh b/tests/script-based-pre/crate-name-default/crate-name-default.sh deleted file mode 100755 index a9e94744b5c6..000000000000 --- a/tests/script-based-pre/crate-name-default/crate-name-default.sh +++ /dev/null @@ -1,39 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -check_file_exists() { - local file=$1 - if ! [ -e "${file}" ] - then - echo "error: expected \`${file}\` to have been generated" - exit 1 - fi -} - -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 - -kani --only-codegen --keep-temps my-code.rs -check_file_exists libmy_code.rlib -check_file_exists my_code.kani-metadata.json - -RUSTFLAGS="--edition 2021" 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="--edition 2021 --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="--edition 2021 --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-default/a/src/lib.rs b/tests/script-based-pre/crate-name/a/src/lib.rs similarity index 100% rename from tests/script-based-pre/crate-name-default/a/src/lib.rs rename to tests/script-based-pre/crate-name/a/src/lib.rs diff --git a/tests/script-based-pre/crate-name-default/b/src/lib.rs b/tests/script-based-pre/crate-name/b/src/lib.rs similarity index 100% rename from tests/script-based-pre/crate-name-default/b/src/lib.rs rename to tests/script-based-pre/crate-name/b/src/lib.rs diff --git a/tests/script-based-pre/crate-name-default/c/src/lib.rs b/tests/script-based-pre/crate-name/c/src/lib.rs similarity index 100% rename from tests/script-based-pre/crate-name-default/c/src/lib.rs rename to tests/script-based-pre/crate-name/c/src/lib.rs diff --git a/tests/script-based-pre/crate-name-default/config.yml b/tests/script-based-pre/crate-name/config.yml similarity index 59% rename from tests/script-based-pre/crate-name-default/config.yml rename to tests/script-based-pre/crate-name/config.yml index d72240852e2f..f022a9c03732 100644 --- a/tests/script-based-pre/crate-name-default/config.yml +++ b/tests/script-based-pre/crate-name/config.yml @@ -1,3 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -script: crate-name-default.sh +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 000000000000..1a4e02d1ff62 --- /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 000000000000..229cc36938f9 --- /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-default/my-code.rs b/tests/script-based-pre/crate-name/my-code.rs similarity index 100% rename from tests/script-based-pre/crate-name-default/my-code.rs rename to tests/script-based-pre/crate-name/my-code.rs