Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 11 additions & 12 deletions kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<dyn Any> {
fn codegen_crate(&self, tcx: TyCtxt) -> Box<dyn Any> {
let ret_val = rustc_internal::run(tcx, || {
// Queries shouldn't change today once codegen starts.
let queries = self.queries.lock().unwrap().clone();
Expand Down Expand Up @@ -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()
}
Expand Down Expand Up @@ -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 <https://github.com/model-checking/kani/issues/2234> 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();
Expand Down Expand Up @@ -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<dyn Any> {
fn codegen_results(tcx: TyCtxt) -> Box<dyn Any> {
let work_products = FxIndexMap::<WorkProductId, WorkProduct>::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,
Expand Down
27 changes: 11 additions & 16 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -283,12 +283,7 @@ impl CodegenBackend for GotocCodegenBackend {
}
}

fn codegen_crate(
&self,
tcx: TyCtxt,
rustc_metadata: EncodedMetadata,
_need_metadata_module: bool,
) -> Box<dyn Any> {
fn codegen_crate(&self, tcx: TyCtxt) -> Box<dyn Any> {
let ret_val = rustc_internal::run(tcx, || {
super::utils::init();

Expand Down Expand Up @@ -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()
}
Expand All @@ -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 <https://github.com/model-checking/kani/issues/2234> 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.
Expand Down Expand Up @@ -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<dyn Any> {
fn codegen_results(tcx: TyCtxt, machine: &MachineModel) -> Box<dyn Any> {
let work_products = FxIndexMap::<WorkProductId, WorkProduct>::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,
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Loading