From 2c261d5c5616897a1dc878a22ef6550546fb9eb8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 10 Nov 2025 11:01:32 +0000 Subject: [PATCH] Upgrade Rust toolchain to 2025-11-10 Relevant upstream PR: - https://github.com/rust-lang/rust/pull/128666 (Add `overflow_checks` intrinsic) Resolves: #4458 --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../src/kani_middle/transform/internal_mir.rs | 21 ++++++++++++++----- rust-toolchain.toml | 2 +- 3 files changed, 18 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 6267b96bdbc..fc9e714cbde 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -842,7 +842,7 @@ impl GotocCtx<'_, '_> { .bytes(), Type::size_t(), ), - NullOp::ContractChecks | NullOp::UbChecks => Expr::c_false(), + NullOp::RuntimeChecks(_) => Expr::c_false(), } } Rvalue::ShallowInitBox(operand, content_ty) => { diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 9bcd545628e..45eca856f75 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -12,9 +12,9 @@ use rustc_middle::ty::{self as rustc_ty, TyCtxt}; use rustc_public::mir::{ AggregateKind, AssertMessage, Body, BorrowKind, CastKind, ConstOperand, CopyNonOverlapping, CoroutineDesugaring, CoroutineKind, CoroutineSource, FakeBorrowKind, FakeReadCause, LocalDecl, - MutBorrowKind, NonDivergingIntrinsic, NullOp, Operand, PointerCoercion, RetagKind, Rvalue, - Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, UnwindAction, - UserTypeProjection, Variance, + MutBorrowKind, NonDivergingIntrinsic, NullOp, Operand, PointerCoercion, RetagKind, + RuntimeChecks, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, + UnwindAction, UserTypeProjection, Variance, }; use rustc_public::rustc_internal::internal; @@ -209,8 +209,19 @@ impl RustcInternalMir for NullOp { .as_slice(), ), ), - NullOp::UbChecks => rustc_middle::mir::NullOp::UbChecks, - NullOp::ContractChecks => rustc_middle::mir::NullOp::ContractChecks, + NullOp::RuntimeChecks(RuntimeChecks::UbChecks) => { + rustc_middle::mir::NullOp::RuntimeChecks(rustc_middle::mir::RuntimeChecks::UbChecks) + } + NullOp::RuntimeChecks(RuntimeChecks::ContractChecks) => { + rustc_middle::mir::NullOp::RuntimeChecks( + rustc_middle::mir::RuntimeChecks::ContractChecks, + ) + } + NullOp::RuntimeChecks(RuntimeChecks::OverflowChecks) => { + rustc_middle::mir::NullOp::RuntimeChecks( + rustc_middle::mir::RuntimeChecks::OverflowChecks, + ) + } } } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c068681c525..42c7d2ee279 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-11-09" +channel = "nightly-2025-11-10" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]