From 19207088f3aa7b39050833e2d4448c384e8c0f18 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 17 Jun 2025 06:41:47 +0000 Subject: [PATCH 1/2] Upgrade Rust toolchain to 2025-06-17 Relevant upstream PR: - https://github.com/rust-lang/rust/pull/141769 (Move metadata object generation for dylibs to the linker code) Resolves: #4162 --- .../compiler_interface.rs | 27 ++++++++----------- rust-toolchain.toml | 2 +- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index ae245ddca8f2..de082cb1c903 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -283,12 +283,7 @@ impl CodegenBackend for GotocCodegenBackend { } } - fn codegen_crate( - &self, - tcx: TyCtxt, - rustc_metadata: EncodedMetadata, - _need_metadata_module: bool, - ) -> Box { + fn codegen_crate(&self, tcx: TyCtxt) -> Box { let ret_val = rustc_internal::run(tcx, || { super::utils::init(); @@ -414,7 +409,7 @@ impl CodegenBackend for GotocCodegenBackend { ); } } - codegen_results(tcx, rustc_metadata, &results.machine_model) + codegen_results(tcx, &results.machine_model) }); ret_val.unwrap() } @@ -440,12 +435,18 @@ impl CodegenBackend for GotocCodegenBackend { /// 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(&self, sess: &Session, codegen_results: CodegenResults, outputs: &OutputFilenames) { + fn link( + &self, + sess: &Session, + codegen_results: CodegenResults, + rustc_metadata: EncodedMetadata, + outputs: &OutputFilenames, + ) { 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.contains(&CrateType::Rlib) { - link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); + link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, rustc_metadata, outputs); } // But override all the other outputs. @@ -541,18 +542,12 @@ fn check_options(session: &Session) { } /// Return a struct that contains information about the codegen results as expected by `rustc`. -fn codegen_results( - tcx: TyCtxt, - rustc_metadata: EncodedMetadata, - machine: &MachineModel, -) -> Box { +fn codegen_results(tcx: TyCtxt, machine: &MachineModel) -> Box { let work_products = FxIndexMap::::default(); Box::new(( CodegenResults { modules: vec![], allocator_module: None, - metadata_module: None, - metadata: rustc_metadata, crate_info: CrateInfo::new(tcx, machine.architecture.clone()), }, work_products, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index cc5085af0b9a..a7a32f1f5cb6 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-16" +channel = "nightly-2025-06-17" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 37ced13e3709ae0a64186214e5fe5dc998299d6e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 17 Jun 2025 20:38:34 +0000 Subject: [PATCH 2/2] Update LLBC back-end --- .../codegen_aeneas_llbc/compiler_interface.rs | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index fb1666526cf1..0ee1e00ba6f1 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -202,12 +202,7 @@ impl CodegenBackend for LlbcCodegenBackend { DEFAULT_LOCALE_RESOURCE } - fn codegen_crate( - &self, - tcx: TyCtxt, - rustc_metadata: EncodedMetadata, - _need_metadata_module: bool, - ) -> Box { + fn codegen_crate(&self, tcx: TyCtxt) -> Box { let ret_val = rustc_internal::run(tcx, || { // Queries shouldn't change today once codegen starts. let queries = self.queries.lock().unwrap().clone(); @@ -286,7 +281,7 @@ impl CodegenBackend for LlbcCodegenBackend { // To avoid overriding the metadata for its verification, we skip this step when // reachability is None, even because there is nothing to record. } - codegen_results(tcx, rustc_metadata) + codegen_results(tcx) }); ret_val.unwrap() } @@ -318,10 +313,16 @@ impl CodegenBackend for LlbcCodegenBackend { /// For cases where no metadata file was requested, 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(&self, sess: &Session, codegen_results: CodegenResults, outputs: &OutputFilenames) { + fn link( + &self, + sess: &Session, + codegen_results: CodegenResults, + rustc_metadata: EncodedMetadata, + outputs: &OutputFilenames, + ) { let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); let local_crate_name = codegen_results.crate_info.local_crate_name; - link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); + link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, rustc_metadata, outputs); for crate_type in requested_crate_types { let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name); let out_path = out_fname.as_path(); @@ -356,14 +357,12 @@ fn contract_metadata_for_harness( } /// Return a struct that contains information about the codegen results as expected by `rustc`. -fn codegen_results(tcx: TyCtxt, rustc_metadata: EncodedMetadata) -> Box { +fn codegen_results(tcx: TyCtxt) -> Box { let work_products = FxIndexMap::::default(); Box::new(( CodegenResults { modules: vec![], allocator_module: None, - metadata_module: None, - metadata: rustc_metadata, crate_info: CrateInfo::new(tcx, tcx.sess.target.arch.clone().to_string()), }, work_products,