From 487e9631026f0d7e1c4c4101cb427f79d9044781 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 13 Nov 2024 17:32:29 -0600 Subject: [PATCH 1/4] Upgrade toolchain to nightly-2024-11-13 --- kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- rust-toolchain.toml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 9f4365b194b2..01f2c9351598 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -338,7 +338,7 @@ impl CodegenBackend for LlbcCodegenBackend { 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)? + link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs)? } else { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9da07e36bdf4..ee53987b412b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -412,7 +412,7 @@ impl CodegenBackend for GotocCodegenBackend { 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)?; + link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs)?; } // But override all the other outputs. diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2df39d2a3931..4b99432e755f 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-11-12" +channel = "nightly-2024-11-13" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 334022e0c3a1c26ed63ff4494c4b3c9ad8dac079 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 14 Nov 2024 00:32:18 -0600 Subject: [PATCH 2/4] Fix compilation error --- kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs | 5 +++-- .../src/codegen_cprover_gotoc/compiler_interface.rs | 6 ++++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 01f2c9351598..ae2865c4ccae 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -326,7 +326,8 @@ impl CodegenBackend for LlbcCodegenBackend { codegen_results: CodegenResults, outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { - let requested_crate_types = &codegen_results.crate_info.crate_types; + let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); + let mut link_result = link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); for crate_type in requested_crate_types { let out_fname = out_filename( sess, @@ -338,7 +339,7 @@ impl CodegenBackend for LlbcCodegenBackend { 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)? + link_result? } else { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index ee53987b412b..2e16b0030050 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -409,12 +409,14 @@ impl CodegenBackend for GotocCodegenBackend { codegen_results: CodegenResults, outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { - let requested_crate_types = &codegen_results.crate_info.crate_types; + let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); // 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)?; } + let local_crate_name = + codegen_results.crate_info.local_crate_name; // 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. @@ -423,7 +425,7 @@ impl CodegenBackend for GotocCodegenBackend { sess, *crate_type, outputs, - codegen_results.crate_info.local_crate_name, + local_crate_name, ); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); From b1f127cece835bb54afade19e7259de9c716eb8f Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 14 Nov 2024 01:28:43 -0600 Subject: [PATCH 3/4] Fix format --- .../src/codegen_aeneas_llbc/compiler_interface.rs | 5 +++-- .../src/codegen_cprover_gotoc/compiler_interface.rs | 10 ++-------- 2 files changed, 5 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index ae2865c4ccae..b5d5a7d83dd4 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -327,13 +327,14 @@ impl CodegenBackend for LlbcCodegenBackend { outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); - let mut link_result = link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); + let local_crate_name = codegen_results.crate_info.local_crate_name; + let link_result = link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); for crate_type in requested_crate_types { let out_fname = out_filename( sess, *crate_type, outputs, - codegen_results.crate_info.local_crate_name, + local_crate_name, ); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 2e16b0030050..3935be784311 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -410,23 +410,17 @@ impl CodegenBackend for GotocCodegenBackend { outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); + let local_crate_name = codegen_results.crate_info.local_crate_name; // 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)?; } - let local_crate_name = - codegen_results.crate_info.local_crate_name; // 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, - *crate_type, - outputs, - local_crate_name, - ); + let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); if *crate_type != CrateType::Rlib { From f50ff23126d38ddb1633a4618a499e4cfafec492 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 14 Nov 2024 01:34:50 -0600 Subject: [PATCH 4/4] Fix format --- .../src/codegen_aeneas_llbc/compiler_interface.rs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index b5d5a7d83dd4..0cccda92f3b7 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -330,12 +330,7 @@ impl CodegenBackend for LlbcCodegenBackend { let local_crate_name = codegen_results.crate_info.local_crate_name; let link_result = link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); for crate_type in requested_crate_types { - let out_fname = out_filename( - sess, - *crate_type, - outputs, - local_crate_name, - ); + let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); if *crate_type == CrateType::Rlib {