Skip to content

Commit e388117

Browse files
authored
Upgrade Rust toolchain to 2025-11-19 (#4482)
Relevant upstream PR: - rust-lang/rust#148151 (Replace OffsetOf by an actual sum of calls to intrinsic.) Resolves: #4481 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 6fb80aa commit e388117

File tree

5 files changed

+9
-43
lines changed

5 files changed

+9
-43
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 2 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ use cbmc::goto_program::{
1919
use cbmc::{InternString, InternedString, btree_string_map};
2020
use num::bigint::BigInt;
2121
use rustc_abi::{FieldsShape, TagEncoding, Variants};
22-
use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry};
22+
use rustc_middle::ty::{TyCtxt, VtblEntry};
2323
use rustc_public::abi::{Primitive, Scalar, ValueAbi};
2424
use rustc_public::mir::mono::Instance;
2525
use rustc_public::mir::{
@@ -824,27 +824,7 @@ impl GotocCtx<'_, '_> {
824824
Rvalue::CheckedBinaryOp(op, e1, e2) => {
825825
self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty)
826826
}
827-
Rvalue::NullaryOp(k, t) => {
828-
let layout = self.layout_of_stable(*t);
829-
match k {
830-
NullOp::OffsetOf(fields) => Expr::int_constant(
831-
self.tcx
832-
.offset_of_subfield(
833-
TypingEnv::fully_monomorphized(),
834-
layout,
835-
fields.iter().map(|(var_idx, field_idx)| {
836-
(
837-
rustc_internal::internal(self.tcx, var_idx),
838-
(*field_idx).into(),
839-
)
840-
}),
841-
)
842-
.bytes(),
843-
Type::size_t(),
844-
),
845-
NullOp::RuntimeChecks(_) => Expr::c_false(),
846-
}
847-
}
827+
Rvalue::NullaryOp(NullOp::RuntimeChecks(_)) => Expr::c_false(),
848828
Rvalue::ShallowInitBox(operand, content_ty) => {
849829
// The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.
850830
// See https://github.com/rust-lang/compiler-team/issues/460 for more details.

kani-compiler/src/kani_middle/analysis.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,7 @@ impl From<&Rvalue> for Key {
168168
Rvalue::Cast(_, _, _) => Key("Cast"),
169169
Rvalue::BinaryOp(..) => Key("BinaryOp"),
170170
Rvalue::CheckedBinaryOp(..) => Key("CheckedBinaryOp"),
171-
Rvalue::NullaryOp(_, _) => Key("NullaryOp"),
171+
Rvalue::NullaryOp(_) => Key("NullaryOp"),
172172
Rvalue::UnaryOp(_, _) => Key("UnaryOp"),
173173
Rvalue::Discriminant(_) => Key("Discriminant"),
174174
Rvalue::Aggregate(_, _) => Key("Aggregate"),

kani-compiler/src/kani_middle/transform/check_values.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -699,7 +699,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
699699
| Rvalue::Ref(_, _, _)
700700
| Rvalue::Repeat(_, _)
701701
| Rvalue::ThreadLocalRef(_)
702-
| Rvalue::NullaryOp(_, _)
702+
| Rvalue::NullaryOp(_)
703703
| Rvalue::UnaryOp(_, _)
704704
| Rvalue::Use(_) => {}
705705
}

kani-compiler/src/kani_middle/transform/internal_mir.rs

Lines changed: 4 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -191,24 +191,10 @@ impl RustcInternalMir for BorrowKind {
191191
}
192192

193193
impl RustcInternalMir for NullOp {
194-
type T<'tcx> = rustc_middle::mir::NullOp<'tcx>;
194+
type T<'tcx> = rustc_middle::mir::NullOp;
195195

196-
fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
196+
fn internal_mir<'tcx>(&self, _tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
197197
match self {
198-
NullOp::OffsetOf(offsets) => rustc_middle::mir::NullOp::OffsetOf(
199-
tcx.mk_offset_of(
200-
offsets
201-
.iter()
202-
.map(|(variant_idx, field_idx)| {
203-
(
204-
internal(tcx, variant_idx),
205-
rustc_abi::FieldIdx::from_usize(*field_idx),
206-
)
207-
})
208-
.collect::<Vec<_>>()
209-
.as_slice(),
210-
),
211-
),
212198
NullOp::RuntimeChecks(RuntimeChecks::UbChecks) => {
213199
rustc_middle::mir::NullOp::RuntimeChecks(rustc_middle::mir::RuntimeChecks::UbChecks)
214200
}
@@ -278,8 +264,8 @@ impl RustcInternalMir for Rvalue {
278264
Rvalue::ThreadLocalRef(crate_item) => {
279265
rustc_middle::mir::Rvalue::ThreadLocalRef(internal(tcx, crate_item.0))
280266
}
281-
Rvalue::NullaryOp(null_op, ty) => {
282-
rustc_middle::mir::Rvalue::NullaryOp(null_op.internal_mir(tcx), internal(tcx, ty))
267+
Rvalue::NullaryOp(null_op) => {
268+
rustc_middle::mir::Rvalue::NullaryOp(null_op.internal_mir(tcx))
283269
}
284270
Rvalue::UnaryOp(un_op, operand) => {
285271
rustc_middle::mir::Rvalue::UnaryOp(internal(tcx, un_op), operand.internal_mir(tcx))

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-11-18"
5+
channel = "nightly-2025-11-19"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)