diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 6d3db1666407..96f757e22aeb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -272,6 +272,14 @@ impl GotocCtx<'_, '_> { Intrinsic::AddWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, place, loc) } + Intrinsic::AlignOf => { + let genarg = instance.args(); + let tys = genarg.0.clone(); + let t = tys.first().unwrap().ty().unwrap(); + let layout = self.layout_of_stable(*t); + let expr = Expr::int_constant(layout.align.abi.bytes(), Type::size_t()); + self.codegen_expr_to_place_stable(place, expr, loc) + } Intrinsic::ArithOffset => self.codegen_arith_offset(fargs, place, loc), Intrinsic::AssertInhabited => { self.codegen_assert_intrinsic(instance, intrinsic_str, span) @@ -481,6 +489,15 @@ impl GotocCtx<'_, '_> { loc, ), Intrinsic::SimdXor => codegen_intrinsic_binop!(bitxor), + Intrinsic::SizeOf => { + let genarg = instance.args(); + let tys = genarg.0.clone(); + let t = tys.first().unwrap().ty().unwrap(); + let layout = self.layout_of_stable(*t); + let expr = Expr::int_constant(layout.size.bytes_usize(), Type::size_t()) + .with_size_of_annotation(self.codegen_ty_stable(*t)); + self.codegen_expr_to_place_stable(place, expr, loc) + } Intrinsic::SqrtF32 => codegen_simple_intrinsic!(Sqrtf), Intrinsic::SqrtF64 => codegen_simple_intrinsic!(Sqrt), Intrinsic::SubWithOverflow => self.codegen_op_with_overflow( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 93ee106188b4..6267b96bdbca 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -827,9 +827,6 @@ impl GotocCtx<'_, '_> { Rvalue::NullaryOp(k, t) => { let layout = self.layout_of_stable(*t); match k { - NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t()) - .with_size_of_annotation(self.codegen_ty_stable(*t)), - NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()), NullOp::OffsetOf(fields) => Expr::int_constant( self.tcx .offset_of_subfield( diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index bf832aa91a2f..1784d25269c7 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -14,6 +14,7 @@ use rustc_public::{ #[derive(Clone, Debug)] pub enum Intrinsic { AddWithOverflow, + AlignOf, AlignOfVal, ArithOffset, AssertInhabited, @@ -123,6 +124,7 @@ pub enum Intrinsic { SimdShuffle(String), SimdSub, SimdXor, + SizeOf, SizeOfVal, SqrtF32, SqrtF64, @@ -177,9 +179,10 @@ impl Intrinsic { assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_)); Self::AddWithOverflow } - "align_of" => unreachable!( - "Expected `core::intrinsics::align_of` to be handled by NullOp::SizeOf" - ), + "align_of" => { + Self::AlignOf + //"Expected `core::intrinsics::align_of` to be handled by NullOp::SizeOf" + } "align_of_val" => { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); Self::AlignOfVal @@ -356,9 +359,7 @@ impl Intrinsic { assert_sig_matches!(sig, _, _ => _); Self::SaturatingSub } - "size_of" => { - unreachable!("Expected `core::intrinsics::size_of` to be handled by NullOp::SizeOf") - } + "size_of" => Self::SizeOf, "size_of_val" => { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); Self::SizeOfVal diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 4db9d4cca4c3..9bcd545628ee 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -195,8 +195,6 @@ impl RustcInternalMir for NullOp { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - NullOp::SizeOf => rustc_middle::mir::NullOp::SizeOf, - NullOp::AlignOf => rustc_middle::mir::NullOp::AlignOf, NullOp::OffsetOf(offsets) => rustc_middle::mir::NullOp::OffsetOf( tcx.mk_offset_of( offsets diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 38c9708c1f41..af6307fd8c47 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-10-23" +channel = "nightly-2025-10-24" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Drop/drop_after_moving_across_channel.rs b/tests/slow/tokio-proofs/src/drop_after_moving_across_channel.rs similarity index 100% rename from tests/kani/Drop/drop_after_moving_across_channel.rs rename to tests/slow/tokio-proofs/src/drop_after_moving_across_channel.rs