From 21f4af94201eaf412ed7802892721ebcbd539558 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 7 Oct 2024 17:46:25 -0400 Subject: [PATCH 1/2] Fix issue when linking rlib + another library type (#3576) Invoking the native linker was overriding the `json` we create in Kani's compiler. Thus, invoke the native linker first, then create the `json` files. Resolves #3569 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../compiler_interface.rs | 21 +++++++++---------- .../cdylib-rlib/Cargo.toml | 13 ++++++++++++ .../supported-lib-types/cdylib-rlib/expected | 2 ++ 3 files changed, 25 insertions(+), 11 deletions(-) create mode 100644 tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml create mode 100644 tests/cargo-ui/supported-lib-types/cdylib-rlib/expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 85117b6a2974..da211c58946c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -403,13 +403,7 @@ impl CodegenBackend for GotocCodegenBackend { /// We need to emit `rlib` files normally if requested. Cargo expects these in some /// circumstances and sends them to subsequent builds with `-L`. /// - /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects. - /// What determines whether the native linker is invoked or not is the set of `crate_types`. - /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. - /// - /// Thus, we manually build the rlib file including only the `rmeta` file. - /// - /// For cases where no metadata file was requested, we stub the file requested by writing the + /// For other crate types, we stub the file requested by writing the /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. /// See for more details. fn link( @@ -419,6 +413,14 @@ impl CodegenBackend for GotocCodegenBackend { outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = &codegen_results.crate_info.crate_types; + // Create the rlib if one was requested. + if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) { + link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?; + } + + // But override all the other outputs. + // Note: Do this after `link_binary` call, since it may write to the object files + // and override the json we are creating. for crate_type in requested_crate_types { let out_fname = out_filename( sess, @@ -428,10 +430,7 @@ impl CodegenBackend for GotocCodegenBackend { ); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); - if *crate_type == CrateType::Rlib { - // Emit the `rlib` that contains just one file: `.rmeta` - link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)? - } else { + if *crate_type != CrateType::Rlib { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); let base_filename = base_filepath.as_path(); diff --git a/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml b/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml new file mode 100644 index 000000000000..fcf91e061e57 --- /dev/null +++ b/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "supported-lib" +version = "0.1.0" +edition = "2021" +description = "Test that Kani correctly handle supported crate types" + +[lib] +name = "lib" +crate-type = ["cdylib", "rlib"] +path = "../src/lib.rs" + diff --git a/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected b/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected new file mode 100644 index 000000000000..426470e8702c --- /dev/null +++ b/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected @@ -0,0 +1,2 @@ +Checking harness check_ok... +VERIFICATION:- SUCCESSFUL From 91044db940d11193a75bef8414f65f1fd5832503 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 8 Oct 2024 07:16:12 -0700 Subject: [PATCH 2/2] Running `verify-std` no longer changes Cargo files (#3577) In order to create a dummy crate we were using `cargo init` command. However, this command will interact with any existing workspace. Instead, explicitly create a dummy `Cargo.toml` and `src/lib.rs`. Resolves #3574 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-driver/src/call_cargo.rs | 35 +++++++++++++++-- .../verify_std_cmd/verify_std.expected | 4 ++ .../verify_std_cmd/verify_std.sh | 39 ++++++++++++++++--- 3 files changed, 69 insertions(+), 9 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 191b104a8c1c..bc0e9d8361d7 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -46,10 +46,39 @@ pub struct CargoOutputs { impl KaniSession { /// Create a new cargo library in the given path. + /// + /// Since we cannot create a new workspace with `cargo init --lib`, we create the dummy + /// crate manually. =( See . + /// + /// Without setting up a new workspace, cargo init will modify the workspace where this is + /// running. See for details. pub fn cargo_init_lib(&self, path: &Path) -> Result<()> { - let mut cmd = setup_cargo_command()?; - cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]); - self.run_terminal(cmd) + let toml_path = path.join("Cargo.toml"); + if toml_path.exists() { + bail!("Cargo.toml already exists in {}", path.display()); + } + + // Create folder for library + fs::create_dir_all(path.join("src"))?; + + // Create dummy crate and write dummy body + let lib_path = path.join("src/lib.rs"); + fs::write(&lib_path, "pub fn dummy() {}")?; + + // Create Cargo.toml + fs::write( + &toml_path, + r#"[package] +name = "dummy" +version = "0.1.0" + +[lib] +crate-type = ["lib"] + +[workspace] +"#, + )?; + Ok(()) } pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result> { diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index 157adb94ba16..3c1f474af0e7 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -1,3 +1,7 @@ +[TEST] Only codegen inside library folder +No kani crate inside Cargo.toml as expected + + [TEST] Run kani verify-std Checking harness verify::dummy_proof... diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 022e7b79de4a..e7276867a2a5 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -50,17 +50,44 @@ cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs +# Test that the command works inside the library folder and does not change +# the existing workspace +# See https://github.com/model-checking/kani/issues/3574 +echo "[TEST] Only codegen inside library folder" +pushd "${TMP_DIR}/library" >& /dev/null +RUSTFLAGS="--cfg=uninit_checks" kani verify-std \ + -Z unstable-options \ + . \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates \ + --only-codegen +popd +# Grep should not find anything and exit status is 1. +grep -c kani ${TMP_DIR}/library/Cargo.toml \ + && echo "Unexpected kani crate inside Cargo.toml" \ + || echo "No kani crate inside Cargo.toml as expected" + echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" \ - --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \ +kani verify-std \ + -Z unstable-options \ + "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" \ + -Z function-contracts \ + -Z stubbing \ -Z mem-predicates +# Test that uninit-checks basic setup works on a no-core library echo "[TEST] Run kani verify-std -Z uninit-checks" -export RUSTFLAGS="--cfg=uninit_checks" -kani verify-std -Z unstable-options "${TMP_DIR}/library" \ - --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \ - -Z mem-predicates -Z uninit-checks +RUSTFLAGS="--cfg=uninit_checks" kani verify-std \ + -Z unstable-options \ + "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates \ + -Z uninit-checks # Cleanup rm -r ${TMP_DIR}