From 62ec1ab34bcb3ee5b709031f5f2e32fb4ff49369 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 15 Jul 2026 11:22:07 +0000 Subject: [PATCH] Upgrade Rust toolchain to nightly-2026-02-20 Advance from nightly-2026-02-18 to nightly-2026-02-20. One set of source changes is required (first needed at nightly-2026-02-19); 02-20 then passes with no further changes. Three rustc changes needed handling: 1. `Rvalue::ShallowInitBox` was removed (rust-lang/rust "Remove ShallowInitBox"). Box construction no longer produces this rvalue: `Box::new` now allocates, `write_via_move`s the value, and transmutes the pointer, while `vec!` uses the new `write_box_via_move` intrinsic. Remove Kani's now-dead `ShallowInitBox` match arms across codegen, analysis, points-to, check-values, the MIR visitor, internal-MIR conversion, and the LLBC backend. 2. The `rustc_allow_const_fn_unstable` feature/attribute was removed. Drop it from the vendored `VecDeque` sources used by the `vecdeque-cve` test. 3. The `E0433` diagnostic was reworded ("failed to resolve: could not find" -> "cannot find"); update the `unsupported-annotation` UI test's expected output. Co-authored-by: Kiro --- .../src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 1 - .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 10 ---------- kani-compiler/src/kani_middle/analysis.rs | 1 - .../src/kani_middle/points_to/points_to_analysis.rs | 1 - kani-compiler/src/kani_middle/transform/body.rs | 1 - .../src/kani_middle/transform/check_values.rs | 4 ---- .../src/kani_middle/transform/internal_mir.rs | 4 ---- rust-toolchain.toml | 2 +- tests/cargo-kani/vecdeque-cve/src/harness.rs | 1 - tests/cargo-kani/vecdeque-cve/src/raw_vec.rs | 1 - tests/ui/unsupported-annotation/expected | 2 +- 11 files changed, 2 insertions(+), 26 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 56bf64bffa54..3ae8be991e96 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -1714,7 +1714,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } - Rvalue::ShallowInitBox(_, _) => todo!(), Rvalue::CopyForDeref(_) => todo!(), Rvalue::ThreadLocalRef(_) => todo!(), _ => todo!(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 668e8b6c11ea..6c522d354a66 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -824,16 +824,6 @@ impl GotocCtx<'_, '_> { Rvalue::CheckedBinaryOp(op, e1, e2) => { self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty) } - Rvalue::ShallowInitBox(operand, content_ty) => { - // The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box. - // See https://github.com/rust-lang/compiler-team/issues/460 for more details. - let operand = self.codegen_operand_stable(operand); - let box_ty = Ty::new_box(*content_ty); - let box_ty = self.codegen_ty_stable(box_ty); - let cbmc_t = self.codegen_ty_stable(*content_ty); - let box_contents = operand.cast_to(cbmc_t.to_pointer()); - self.box_value(box_contents, box_ty) - } Rvalue::UnaryOp(op, e) => match op { UnOp::Not => { if self.operand_ty_stable(e).kind().is_bool() { diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 6fc1326e33e2..4b2c0b93dd41 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -171,7 +171,6 @@ impl From<&Rvalue> for Key { Rvalue::UnaryOp(_, _) => Key("UnaryOp"), Rvalue::Discriminant(_) => Key("Discriminant"), Rvalue::Aggregate(_, _) => Key("Aggregate"), - Rvalue::ShallowInitBox(_, _) => Key("ShallowInitBox"), Rvalue::CopyForDeref(_) => Key("CopyForDeref"), } } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 34cc38cd8b7c..4ee27ecc9a1e 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -527,7 +527,6 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { // Using the operand unchanged requires determining where it could point, which // `successors_for_operand` does. Rvalue::Use(operand) - | Rvalue::ShallowInitBox(operand, _) | Rvalue::Cast(_, operand, _) | Rvalue::Repeat(operand, ..) | Rvalue::WrapUnsafeBinder(operand, _) => self.successors_for_operand(state, operand), diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 9d36caadcd73..5e770ed266e6 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -624,7 +624,6 @@ pub trait MutMirVisitor { Rvalue::Repeat(op, _) => { self.visit_operand(op); } - Rvalue::ShallowInitBox(op, _) => self.visit_operand(op), Rvalue::UnaryOp(_, op) | Rvalue::Use(op) => { self.visit_operand(op); } diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 840354125d61..cfaf56b30022 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -657,10 +657,6 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { | CastKind::IntToFloat | CastKind::FnPtrToPtr => {} }, - Rvalue::ShallowInitBox(_, _) => { - // The contents of the box is considered uninitialized. - // This should already be covered by the Assign detection. - } Rvalue::Aggregate(kind, operands) => match kind { // If the aggregated structure has invalid value, this could generate invalid value. // But only if the operands don't have the exact same restrictions. diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 416fccdf2f3e..e943746db671 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -250,10 +250,6 @@ impl RustcInternalMir for Rvalue { operand.internal_mir(tcx), internal(tcx, ty_const), ), - Rvalue::ShallowInitBox(operand, ty) => rustc_middle::mir::Rvalue::ShallowInitBox( - operand.internal_mir(tcx), - internal(tcx, ty), - ), Rvalue::ThreadLocalRef(crate_item) => { rustc_middle::mir::Rvalue::ThreadLocalRef(internal(tcx, crate_item.0)) } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 8932a8ee0670..a16496d53b37 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2026-02-18" +channel = "nightly-2026-02-20" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/vecdeque-cve/src/harness.rs b/tests/cargo-kani/vecdeque-cve/src/harness.rs index f8ec8f5fdbde..4bac2204cfe3 100644 --- a/tests/cargo-kani/vecdeque-cve/src/harness.rs +++ b/tests/cargo-kani/vecdeque-cve/src/harness.rs @@ -9,7 +9,6 @@ #![feature(rustc_attrs)] #![feature(core_intrinsics)] #![feature(ptr_internals)] -#![feature(rustc_allow_const_fn_unstable)] #![allow(internal_features)] #[cfg(disable_debug_asserts)] diff --git a/tests/cargo-kani/vecdeque-cve/src/raw_vec.rs b/tests/cargo-kani/vecdeque-cve/src/raw_vec.rs index aac8a586fa24..b943ac76b67e 100644 --- a/tests/cargo-kani/vecdeque-cve/src/raw_vec.rs +++ b/tests/cargo-kani/vecdeque-cve/src/raw_vec.rs @@ -120,7 +120,6 @@ impl RawVec { /// Like `new`, but parameterized over the choice of allocator for /// the returned `RawVec`. - #[rustc_allow_const_fn_unstable(const_fn)] pub const fn new_in(alloc: A) -> Self { // `cap: 0` means "unallocated". zero-sized types are ignored. Self { ptr: Unique::dangling(), cap: 0, alloc } diff --git a/tests/ui/unsupported-annotation/expected b/tests/ui/unsupported-annotation/expected index 8427f1e9102b..7205902bc585 100644 --- a/tests/ui/unsupported-annotation/expected +++ b/tests/ui/unsupported-annotation/expected @@ -1 +1 @@ -error[E0433]: failed to resolve: could not find `test_annotation` in `kani` +error[E0433]: cannot find `test_annotation` in `kani`