diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index fc9e714cbde..57103a915cb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -19,7 +19,7 @@ use cbmc::goto_program::{ use cbmc::{InternString, InternedString, btree_string_map}; use num::bigint::BigInt; use rustc_abi::{FieldsShape, TagEncoding, Variants}; -use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry}; +use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_public::abi::{Primitive, Scalar, ValueAbi}; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ @@ -824,27 +824,7 @@ impl GotocCtx<'_, '_> { Rvalue::CheckedBinaryOp(op, e1, e2) => { self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty) } - Rvalue::NullaryOp(k, t) => { - let layout = self.layout_of_stable(*t); - match k { - NullOp::OffsetOf(fields) => Expr::int_constant( - self.tcx - .offset_of_subfield( - TypingEnv::fully_monomorphized(), - layout, - fields.iter().map(|(var_idx, field_idx)| { - ( - rustc_internal::internal(self.tcx, var_idx), - (*field_idx).into(), - ) - }), - ) - .bytes(), - Type::size_t(), - ), - NullOp::RuntimeChecks(_) => Expr::c_false(), - } - } + Rvalue::NullaryOp(NullOp::RuntimeChecks(_)) => Expr::c_false(), 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. diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 1720e043344..bccf143c09b 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -168,7 +168,7 @@ impl From<&Rvalue> for Key { Rvalue::Cast(_, _, _) => Key("Cast"), Rvalue::BinaryOp(..) => Key("BinaryOp"), Rvalue::CheckedBinaryOp(..) => Key("CheckedBinaryOp"), - Rvalue::NullaryOp(_, _) => Key("NullaryOp"), + Rvalue::NullaryOp(_) => Key("NullaryOp"), Rvalue::UnaryOp(_, _) => Key("UnaryOp"), Rvalue::Discriminant(_) => Key("Discriminant"), Rvalue::Aggregate(_, _) => Key("Aggregate"), diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 6334648fdd0..0abec3891f9 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -699,7 +699,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { | Rvalue::Ref(_, _, _) | Rvalue::Repeat(_, _) | Rvalue::ThreadLocalRef(_) - | Rvalue::NullaryOp(_, _) + | Rvalue::NullaryOp(_) | Rvalue::UnaryOp(_, _) | Rvalue::Use(_) => {} } diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 45eca856f75..edd016add17 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -191,24 +191,10 @@ impl RustcInternalMir for BorrowKind { } impl RustcInternalMir for NullOp { - type T<'tcx> = rustc_middle::mir::NullOp<'tcx>; + type T<'tcx> = rustc_middle::mir::NullOp; - fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { + fn internal_mir<'tcx>(&self, _tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - NullOp::OffsetOf(offsets) => rustc_middle::mir::NullOp::OffsetOf( - tcx.mk_offset_of( - offsets - .iter() - .map(|(variant_idx, field_idx)| { - ( - internal(tcx, variant_idx), - rustc_abi::FieldIdx::from_usize(*field_idx), - ) - }) - .collect::>() - .as_slice(), - ), - ), NullOp::RuntimeChecks(RuntimeChecks::UbChecks) => { rustc_middle::mir::NullOp::RuntimeChecks(rustc_middle::mir::RuntimeChecks::UbChecks) } @@ -278,8 +264,8 @@ impl RustcInternalMir for Rvalue { Rvalue::ThreadLocalRef(crate_item) => { rustc_middle::mir::Rvalue::ThreadLocalRef(internal(tcx, crate_item.0)) } - Rvalue::NullaryOp(null_op, ty) => { - rustc_middle::mir::Rvalue::NullaryOp(null_op.internal_mir(tcx), internal(tcx, ty)) + Rvalue::NullaryOp(null_op) => { + rustc_middle::mir::Rvalue::NullaryOp(null_op.internal_mir(tcx)) } Rvalue::UnaryOp(un_op, operand) => { rustc_middle::mir::Rvalue::UnaryOp(internal(tcx, un_op), operand.internal_mir(tcx)) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e210cc2931f..787d973b011 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-18" +channel = "nightly-2025-11-19" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]