Skip to content

Commit 9b2abba

Browse files
Upgrade Rust toolchain to 2025-10-24 (#4426)
Relevant upstream PR: - rust-lang/rust#147793 (Replace NullOp::SizeOf and NullOp::AlignOf by lang items.) Resolves: #4425 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: thanhnguyen-aws <[email protected]>
1 parent 8ec44d0 commit 9b2abba

File tree

6 files changed

+25
-12
lines changed

6 files changed

+25
-12
lines changed

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -272,6 +272,14 @@ impl GotocCtx<'_, '_> {
272272
Intrinsic::AddWithOverflow => {
273273
self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, place, loc)
274274
}
275+
Intrinsic::AlignOf => {
276+
let genarg = instance.args();
277+
let tys = genarg.0.clone();
278+
let t = tys.first().unwrap().ty().unwrap();
279+
let layout = self.layout_of_stable(*t);
280+
let expr = Expr::int_constant(layout.align.abi.bytes(), Type::size_t());
281+
self.codegen_expr_to_place_stable(place, expr, loc)
282+
}
275283
Intrinsic::ArithOffset => self.codegen_arith_offset(fargs, place, loc),
276284
Intrinsic::AssertInhabited => {
277285
self.codegen_assert_intrinsic(instance, intrinsic_str, span)
@@ -481,6 +489,15 @@ impl GotocCtx<'_, '_> {
481489
loc,
482490
),
483491
Intrinsic::SimdXor => codegen_intrinsic_binop!(bitxor),
492+
Intrinsic::SizeOf => {
493+
let genarg = instance.args();
494+
let tys = genarg.0.clone();
495+
let t = tys.first().unwrap().ty().unwrap();
496+
let layout = self.layout_of_stable(*t);
497+
let expr = Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
498+
.with_size_of_annotation(self.codegen_ty_stable(*t));
499+
self.codegen_expr_to_place_stable(place, expr, loc)
500+
}
484501
Intrinsic::SqrtF32 => codegen_simple_intrinsic!(Sqrtf),
485502
Intrinsic::SqrtF64 => codegen_simple_intrinsic!(Sqrt),
486503
Intrinsic::SubWithOverflow => self.codegen_op_with_overflow(

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -827,9 +827,6 @@ impl GotocCtx<'_, '_> {
827827
Rvalue::NullaryOp(k, t) => {
828828
let layout = self.layout_of_stable(*t);
829829
match k {
830-
NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
831-
.with_size_of_annotation(self.codegen_ty_stable(*t)),
832-
NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
833830
NullOp::OffsetOf(fields) => Expr::int_constant(
834831
self.tcx
835832
.offset_of_subfield(

kani-compiler/src/intrinsics.rs

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ use rustc_public::{
1414
#[derive(Clone, Debug)]
1515
pub enum Intrinsic {
1616
AddWithOverflow,
17+
AlignOf,
1718
AlignOfVal,
1819
ArithOffset,
1920
AssertInhabited,
@@ -123,6 +124,7 @@ pub enum Intrinsic {
123124
SimdShuffle(String),
124125
SimdSub,
125126
SimdXor,
127+
SizeOf,
126128
SizeOfVal,
127129
SqrtF32,
128130
SqrtF64,
@@ -177,9 +179,10 @@ impl Intrinsic {
177179
assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
178180
Self::AddWithOverflow
179181
}
180-
"align_of" => unreachable!(
181-
"Expected `core::intrinsics::align_of` to be handled by NullOp::SizeOf"
182-
),
182+
"align_of" => {
183+
Self::AlignOf
184+
//"Expected `core::intrinsics::align_of` to be handled by NullOp::SizeOf"
185+
}
183186
"align_of_val" => {
184187
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
185188
Self::AlignOfVal
@@ -356,9 +359,7 @@ impl Intrinsic {
356359
assert_sig_matches!(sig, _, _ => _);
357360
Self::SaturatingSub
358361
}
359-
"size_of" => {
360-
unreachable!("Expected `core::intrinsics::size_of` to be handled by NullOp::SizeOf")
361-
}
362+
"size_of" => Self::SizeOf,
362363
"size_of_val" => {
363364
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
364365
Self::SizeOfVal

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -195,8 +195,6 @@ impl RustcInternalMir for NullOp {
195195

196196
fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
197197
match self {
198-
NullOp::SizeOf => rustc_middle::mir::NullOp::SizeOf,
199-
NullOp::AlignOf => rustc_middle::mir::NullOp::AlignOf,
200198
NullOp::OffsetOf(offsets) => rustc_middle::mir::NullOp::OffsetOf(
201199
tcx.mk_offset_of(
202200
offsets

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

0 commit comments

Comments
 (0)