Skip to content

Commit b64e59d

Browse files
Upgrade Rust toolchain to 2025-06-17 (#4163)
Relevant upstream PR: - rust-lang/rust#141769 (Move metadata object generation for dylibs to the linker code) Resolves: #4162 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
1 parent 583c3d3 commit b64e59d

File tree

3 files changed

+23
-29
lines changed

3 files changed

+23
-29
lines changed

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -202,12 +202,7 @@ impl CodegenBackend for LlbcCodegenBackend {
202202
DEFAULT_LOCALE_RESOURCE
203203
}
204204

205-
fn codegen_crate(
206-
&self,
207-
tcx: TyCtxt,
208-
rustc_metadata: EncodedMetadata,
209-
_need_metadata_module: bool,
210-
) -> Box<dyn Any> {
205+
fn codegen_crate(&self, tcx: TyCtxt) -> Box<dyn Any> {
211206
let ret_val = rustc_internal::run(tcx, || {
212207
// Queries shouldn't change today once codegen starts.
213208
let queries = self.queries.lock().unwrap().clone();
@@ -286,7 +281,7 @@ impl CodegenBackend for LlbcCodegenBackend {
286281
// To avoid overriding the metadata for its verification, we skip this step when
287282
// reachability is None, even because there is nothing to record.
288283
}
289-
codegen_results(tcx, rustc_metadata)
284+
codegen_results(tcx)
290285
});
291286
ret_val.unwrap()
292287
}
@@ -318,10 +313,16 @@ impl CodegenBackend for LlbcCodegenBackend {
318313
/// For cases where no metadata file was requested, we stub the file requested by writing the
319314
/// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata.
320315
/// See <https://github.com/model-checking/kani/issues/2234> for more details.
321-
fn link(&self, sess: &Session, codegen_results: CodegenResults, outputs: &OutputFilenames) {
316+
fn link(
317+
&self,
318+
sess: &Session,
319+
codegen_results: CodegenResults,
320+
rustc_metadata: EncodedMetadata,
321+
outputs: &OutputFilenames,
322+
) {
322323
let requested_crate_types = &codegen_results.crate_info.crate_types.clone();
323324
let local_crate_name = codegen_results.crate_info.local_crate_name;
324-
link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs);
325+
link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, rustc_metadata, outputs);
325326
for crate_type in requested_crate_types {
326327
let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name);
327328
let out_path = out_fname.as_path();
@@ -356,14 +357,12 @@ fn contract_metadata_for_harness(
356357
}
357358

358359
/// Return a struct that contains information about the codegen results as expected by `rustc`.
359-
fn codegen_results(tcx: TyCtxt, rustc_metadata: EncodedMetadata) -> Box<dyn Any> {
360+
fn codegen_results(tcx: TyCtxt) -> Box<dyn Any> {
360361
let work_products = FxIndexMap::<WorkProductId, WorkProduct>::default();
361362
Box::new((
362363
CodegenResults {
363364
modules: vec![],
364365
allocator_module: None,
365-
metadata_module: None,
366-
metadata: rustc_metadata,
367366
crate_info: CrateInfo::new(tcx, tcx.sess.target.arch.clone().to_string()),
368367
},
369368
work_products,

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 11 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -283,12 +283,7 @@ impl CodegenBackend for GotocCodegenBackend {
283283
}
284284
}
285285

286-
fn codegen_crate(
287-
&self,
288-
tcx: TyCtxt,
289-
rustc_metadata: EncodedMetadata,
290-
_need_metadata_module: bool,
291-
) -> Box<dyn Any> {
286+
fn codegen_crate(&self, tcx: TyCtxt) -> Box<dyn Any> {
292287
let ret_val = rustc_internal::run(tcx, || {
293288
super::utils::init();
294289

@@ -414,7 +409,7 @@ impl CodegenBackend for GotocCodegenBackend {
414409
);
415410
}
416411
}
417-
codegen_results(tcx, rustc_metadata, &results.machine_model)
412+
codegen_results(tcx, &results.machine_model)
418413
});
419414
ret_val.unwrap()
420415
}
@@ -440,12 +435,18 @@ impl CodegenBackend for GotocCodegenBackend {
440435
/// For other crate types, we stub the file requested by writing the
441436
/// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata.
442437
/// See <https://github.com/model-checking/kani/issues/2234> for more details.
443-
fn link(&self, sess: &Session, codegen_results: CodegenResults, outputs: &OutputFilenames) {
438+
fn link(
439+
&self,
440+
sess: &Session,
441+
codegen_results: CodegenResults,
442+
rustc_metadata: EncodedMetadata,
443+
outputs: &OutputFilenames,
444+
) {
444445
let requested_crate_types = &codegen_results.crate_info.crate_types.clone();
445446
let local_crate_name = codegen_results.crate_info.local_crate_name;
446447
// Create the rlib if one was requested.
447448
if requested_crate_types.contains(&CrateType::Rlib) {
448-
link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs);
449+
link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, rustc_metadata, outputs);
449450
}
450451

451452
// But override all the other outputs.
@@ -541,18 +542,12 @@ fn check_options(session: &Session) {
541542
}
542543

543544
/// Return a struct that contains information about the codegen results as expected by `rustc`.
544-
fn codegen_results(
545-
tcx: TyCtxt,
546-
rustc_metadata: EncodedMetadata,
547-
machine: &MachineModel,
548-
) -> Box<dyn Any> {
545+
fn codegen_results(tcx: TyCtxt, machine: &MachineModel) -> Box<dyn Any> {
549546
let work_products = FxIndexMap::<WorkProductId, WorkProduct>::default();
550547
Box::new((
551548
CodegenResults {
552549
modules: vec![],
553550
allocator_module: None,
554-
metadata_module: None,
555-
metadata: rustc_metadata,
556551
crate_info: CrateInfo::new(tcx, machine.architecture.clone()),
557552
},
558553
work_products,

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-06-16"
5+
channel = "nightly-2025-06-17"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)