From 33e671583f4b30eaecf2a6bc87952ddea5c3fec7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Jul 2025 19:28:29 +0000 Subject: [PATCH] Upgrade Rust toolchain to 2025-07-25 Relevant upstream PRs: - https://github.com/rust-lang/rust/pull/144389 (MIR-build: No longer emit assumes in enum-as casting) - https://github.com/rust-lang/rust/pull/144392 (rustc_public: Remove movability from `RigidTy/AggregateKind::Coroutine`) - https://github.com/rust-lang/rust/pull/144377 (Rename impl_of_method and trait_of_item) Resolves: #4246 --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- kani-compiler/src/kani_middle/stubbing/mod.rs | 2 +- .../src/kani_middle/transform/check_uninit/ty_layout.rs | 2 +- kani-compiler/src/kani_middle/transform/check_values.rs | 4 ++-- kani-compiler/src/kani_middle/transform/internal_mir.rs | 2 +- rust-toolchain.toml | 2 +- .../cargo_autoharness_contracts/contracts.expected | 4 ---- 7 files changed, 7 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 93fb86bcae1b..54bdf1b819dd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -734,7 +734,7 @@ impl GotocCtx<'_> { } } } - AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(operands, res_ty), + AggregateKind::Coroutine(_, _) => self.codegen_rvalue_coroutine(operands, res_ty), AggregateKind::CoroutineClosure(_, _) => { let ty = self.codegen_ty_stable(res_ty); self.codegen_unimplemented_expr( diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 9adb1c96826a..aee12d7abd71 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -183,7 +183,7 @@ impl MirVisitor for StubConstChecker<'_> { [one] => one.as_type().unwrap(), _ => unreachable!(), }; - let trait_ = tcx.trait_of_item(mono_const.def).unwrap(); + let trait_ = tcx.trait_of_assoc(mono_const.def).unwrap(); let msg = format!( "Type `{implementor}` does not implement trait `{}`. \ This is likely because `{}` is used as a stub but its \ diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index af9699fa4629..ee219114f714 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -394,7 +394,7 @@ fn data_bytes_for_ty( RigidTy::FnDef(_, _) | RigidTy::FnPtr(_) | RigidTy::Closure(_, _) - | RigidTy::Coroutine(_, _, _) + | RigidTy::Coroutine(_, _) | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 71cd11e3ba1f..0ec394d2cddc 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -687,7 +687,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { // Only aggregate value. AggregateKind::Array(_) | AggregateKind::Closure(_, _) - | AggregateKind::Coroutine(_, _, _) + | AggregateKind::Coroutine(_, _) | AggregateKind::CoroutineClosure(_, _) | AggregateKind::RawPtr(_, _) | AggregateKind::Tuple => {} @@ -1057,7 +1057,7 @@ pub fn ty_validity_per_offset( RigidTy::FnDef(_, _) | RigidTy::FnPtr(_) | RigidTy::Closure(_, _) - | RigidTy::Coroutine(_, _, _) + | RigidTy::Coroutine(_, _) | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index de18b780ef92..b20718b7bd11 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -50,7 +50,7 @@ impl RustcInternalMir for AggregateKind { internal(tcx, generic_args), ) } - AggregateKind::Coroutine(coroutine_def, generic_args, _) => { + AggregateKind::Coroutine(coroutine_def, generic_args) => { rustc_middle::mir::AggregateKind::Coroutine( internal(tcx, coroutine_def.0), internal(tcx, generic_args), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index af3af69e4885..ea14bc9515ab 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-07-24" +channel = "nightly-2025-07-29" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected index b963f7d6a912..66fffb277786 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -40,10 +40,6 @@ arithmetic_overflow\ Autoharness: Checking function should_pass::alignment::Alignment::as_usize's contract against all possible inputs... -should_pass::alignment::Alignment::as_usize\ - - Status: SUCCESS\ - - Description: "Rust intrinsic assumption failed" - should_pass::alignment::Alignment::as_usize\ - Status: SUCCESS\ - Description: "|result| result.is_power_of_two()"