Upgrade toolchain to 07/02

docs/src/rust-feature-support/intrinsics.md

@@ -231,7 +231,7 @@ unchecked_shr | Yes | |
 unchecked_sub | Yes | |
 unlikely | Yes | |
 unreachable | Yes | |
-variant_count | No | |
+variant_count | Yes | |
 volatile_copy_memory | No | See [Notes - Concurrency](#concurrency) |
 volatile_copy_nonoverlapping_memory | No | See [Notes - Concurrency](#concurrency) |
 volatile_load | Partial | See [Notes - Concurrency](#concurrency) |

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

@@ -200,19 +200,6 @@ impl GotocCtx<'_> {
             }};
         }
 
-        // Intrinsics which encode a value known during compilation
-        macro_rules! codegen_intrinsic_const {
-            () => {{
-                let place_ty = self.place_ty_stable(&place);
-                let stable_instance = instance;
-                let alloc = stable_instance.try_const_eval(place_ty).unwrap();
-                // We assume that the intrinsic has type checked at this point, so
-                // we can use the place type as the expression type.
-                let expr = self.codegen_allocation(&alloc, place_ty, loc);
-                self.codegen_expr_to_place_stable(&place, expr, loc)
-            }};
-        }
-
         // Most atomic intrinsics do:
         //   1. Perform an operation on a primary argument (e.g., addition)
         //   2. Return the previous value of the primary argument
@@ -406,13 +393,11 @@ impl GotocCtx<'_> {
             Intrinsic::LogF64 => codegen_simple_intrinsic!(Log),
             Intrinsic::MaxNumF32 => codegen_simple_intrinsic!(Fmaxf),
             Intrinsic::MaxNumF64 => codegen_simple_intrinsic!(Fmax),
-            Intrinsic::MinAlignOf => codegen_intrinsic_const!(),
             Intrinsic::MinNumF32 => codegen_simple_intrinsic!(Fminf),
             Intrinsic::MinNumF64 => codegen_simple_intrinsic!(Fmin),
             Intrinsic::MulWithOverflow => {
                 self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc)
             }
-            Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
             Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
             Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
             Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif),
@@ -505,8 +490,6 @@ impl GotocCtx<'_> {
             Intrinsic::Transmute => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc),
             Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf),
             Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc),
-            Intrinsic::TypeId => codegen_intrinsic_const!(),
-            Intrinsic::TypeName => codegen_intrinsic_const!(),
             Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc),
             Intrinsic::UnalignedVolatileLoad => {
                 unstable_codegen!(self.codegen_expr_to_place_stable(
@@ -536,11 +519,11 @@ impl GotocCtx<'_> {
                 assert!(self.place_ty_stable(place).kind().is_unit());
                 self.codegen_write_bytes(fargs, farg_types, loc)
             }
-            Intrinsic::PtrOffsetFrom
+            Intrinsic::AlignOfVal
+            | Intrinsic::PtrOffsetFrom
             | Intrinsic::PtrOffsetFromUnsigned
-            | Intrinsic::SizeOfVal
-            | Intrinsic::MinAlignOfVal => {
-                unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str)
+            | Intrinsic::SizeOfVal => {
+                unreachable!("Kani models the intrinsic `{}` before codegen", intrinsic_str)
             }
             // Unimplemented
             Intrinsic::Unimplemented { name, issue_link } => {

kani-compiler/src/intrinsics.rs

@@ -14,6 +14,7 @@ use stable_mir::{
 #[derive(Clone, Debug)]
 pub enum Intrinsic {
     AddWithOverflow,
+    AlignOfVal,
     ArithOffset,
     AssertInhabited,
     AssertMemUninitializedValid,
@@ -81,12 +82,9 @@ pub enum Intrinsic {
     LogF64,
     MaxNumF32,
     MaxNumF64,
-    MinAlignOf,
-    MinAlignOfVal,
     MinNumF32,
     MinNumF64,
     MulWithOverflow,
-    NeedsDrop,
     PowF32,
     PowF64,
     PowIF32,
@@ -132,8 +130,6 @@ pub enum Intrinsic {
     Transmute,
     TruncF32,
     TruncF64,
-    TypeId,
-    TypeName,
     TypedSwap,
     UnalignedVolatileLoad,
     UncheckedDiv,
@@ -181,6 +177,13 @@ 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_val" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
+                Self::AlignOfVal
+            }
             "arith_offset" => {
                 assert_sig_matches!(sig,
                     RigidTy::RawPtr(_, Mutability::Not),
@@ -309,22 +312,14 @@ impl Intrinsic {
                 assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool);
                 Self::Likely
             }
-            "align_of" => {
-                assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize));
-                Self::MinAlignOf
-            }
-            "align_of_val" => {
-                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
-                Self::MinAlignOfVal
-            }
             "mul_with_overflow" => {
                 assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
                 Self::MulWithOverflow
             }
-            "needs_drop" => {
-                assert_sig_matches!(sig, => RigidTy::Bool);
-                Self::NeedsDrop
-            }
+            // For const eval of nullary intrinsics, see https://github.com/rust-lang/rust/pull/142839
+            "needs_drop" => unreachable!(
+                "Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
+            ),
             // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
             "offset" => unreachable!(
                 "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
@@ -361,7 +356,9 @@ impl Intrinsic {
                 assert_sig_matches!(sig, _, _ => _);
                 Self::SaturatingSub
             }
-            "size_of" => unreachable!(),
+            "size_of" => {
+                unreachable!("Expected `core::intrinsics::size_of` to be handled by NullOp::SizeOf")
+            }
             "size_of_val" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
                 Self::SizeOfVal
@@ -374,14 +371,12 @@ impl Intrinsic {
                 assert_sig_matches!(sig, _ => _);
                 Self::Transmute
             }
-            "type_id" => {
-                assert_sig_matches!(sig, => RigidTy::Uint(UintTy::U128));
-                Self::TypeId
-            }
-            "type_name" => {
-                assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not));
-                Self::TypeName
-            }
+            "type_id" => unreachable!(
+                "Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
+            ),
+            "type_name" => unreachable!(
+                "Expected nullary intrinsic `core::intrinsics::type_name` to be const-evaluated before codegen"
+            ),
             "typed_swap_nonoverlapping" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Mut) => RigidTy::Tuple(_));
                 Self::TypedSwap
@@ -409,6 +404,9 @@ impl Intrinsic {
             "unreachable" => unreachable!(
                 "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
             ),
+            "variant_count" => unreachable!(
+                "Expected nullary intrinsic `core::intrinsics::variant_count` to be const-evaluated before codegen"
+            ),
             "volatile_copy_memory" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
                 Self::VolatileCopyMemory

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -611,6 +611,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> {
 fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
     match intrinsic {
         Intrinsic::AddWithOverflow
+        | Intrinsic::AlignOfVal
         | Intrinsic::ArithOffset
         | Intrinsic::AssertInhabited
         | Intrinsic::AssertMemUninitializedValid
@@ -659,12 +660,9 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::LogF64
         | Intrinsic::MaxNumF32
         | Intrinsic::MaxNumF64
-        | Intrinsic::MinAlignOf
-        | Intrinsic::MinAlignOfVal
         | Intrinsic::MinNumF32
         | Intrinsic::MinNumF64
         | Intrinsic::MulWithOverflow
-        | Intrinsic::NeedsDrop
         | Intrinsic::PowF32
         | Intrinsic::PowF64
         | Intrinsic::PowIF32
@@ -691,8 +689,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::Transmute
         | Intrinsic::TruncF32
         | Intrinsic::TruncF64
-        | Intrinsic::TypeId
-        | Intrinsic::TypeName
         | Intrinsic::UncheckedDiv
         | Intrinsic::UncheckedRem
         | Intrinsic::Unlikely

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -572,6 +572,7 @@ impl MirVisitor for CheckUninitVisitor {
 fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
     match intrinsic {
         Intrinsic::AddWithOverflow
+        | Intrinsic::AlignOfVal
         | Intrinsic::ArithOffset
         | Intrinsic::AssertInhabited
         | Intrinsic::AssertMemUninitializedValid
@@ -619,12 +620,9 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::LogF64
         | Intrinsic::MaxNumF32
         | Intrinsic::MaxNumF64
-        | Intrinsic::MinAlignOf
-        | Intrinsic::MinAlignOfVal
         | Intrinsic::MinNumF32
         | Intrinsic::MinNumF64
         | Intrinsic::MulWithOverflow
-        | Intrinsic::NeedsDrop
         | Intrinsic::PowF32
         | Intrinsic::PowF64
         | Intrinsic::PowIF32
@@ -643,8 +641,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::SubWithOverflow
         | Intrinsic::TruncF32
         | Intrinsic::TruncF64
-        | Intrinsic::TypeId
-        | Intrinsic::TypeName
         | Intrinsic::UncheckedDiv
         | Intrinsic::UncheckedRem
         | Intrinsic::Unlikely

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

@@ -424,10 +424,9 @@ impl RustcInternalMir for Statement {
     type T<'tcx> = rustc_middle::mir::Statement<'tcx>;
 
     fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
-        rustc_middle::mir::Statement {
-            source_info: rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span)),
-            kind: self.kind.internal_mir(tcx),
-        }
+        let source_info = rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span));
+        let kind = self.kind.internal_mir(tcx);
+        rustc_middle::mir::Statement::new(source_info, kind)
     }
 }
 
@@ -654,14 +653,15 @@ impl RustcInternalMir for Body {
         let internal_basic_blocks = rustc_index::IndexVec::from_raw(
             self.blocks
                 .iter()
-                .map(|stable_basic_block| rustc_middle::mir::BasicBlockData {
-                    statements: stable_basic_block
+                .map(|stable_basic_block| {
+                    let statements = stable_basic_block
                         .statements
                         .iter()
                         .map(|statement| statement.internal_mir(tcx))
-                        .collect(),
-                    terminator: Some(stable_basic_block.terminator.internal_mir(tcx)),
-                    is_cleanup: false,
+                        .collect();
+                    let terminator = Some(stable_basic_block.terminator.internal_mir(tcx));
+                    let is_cleanup = false;
+                    rustc_middle::mir::BasicBlockData::new_stmts(statements, terminator, is_cleanup)
                 })
                 .collect(),
         );

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

@@ -180,8 +180,8 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_, '_> {
                 let intrinsic = Intrinsic::from_instance(&instance);
                 debug!(?intrinsic, "handle_terminator");
                 match intrinsic {
+                    Intrinsic::AlignOfVal => self.models[&KaniModel::AlignOfVal],
                     Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal],
-                    Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal],
                     Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom],
                     Intrinsic::PtrOffsetFromUnsigned => {
                         self.models[&KaniModel::PtrOffsetFromUnsigned]

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-06-30"
+channel = "nightly-2025-07-02"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/Intrinsics/Compiler/variant_count.rs

@@ -1,17 +1,27 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
-// Check that `variant_count` is not supported.
-// This test can be replaced with `variant_count_fixme.rs` once the intrinsic is
-// supported and works as expected.
+// Check that `variant_count` is supported and returns the expected result.
 
 #![feature(variant_count)]
 use std::mem;
 
 enum Void {}
+enum MyError {
+    Error1,
+    Error2,
+    Error3,
+}
 
 #[kani::proof]
 fn main() {
-    let _ = mem::variant_count::<Void>();
+    const VOID_COUNT: usize = mem::variant_count::<Void>();
+    const ERROR_COUNT: usize = mem::variant_count::<MyError>();
+    const OPTION_COUNT: usize = mem::variant_count::<Option<u32>>();
+    const RESULT_COUNT: usize = mem::variant_count::<Result<u32, MyError>>();
+
+    assert!(VOID_COUNT == 0);
+    assert!(ERROR_COUNT == 3);
+    assert!(OPTION_COUNT == 2);
+    assert!(RESULT_COUNT == 2);
 }

tests/kani/Intrinsics/ConstEval/needs_drop.rs

@@ -11,7 +11,7 @@ pub struct Foo<T> {
 
 impl<T> Foo<T> {
     fn call_needs_drop(&self) -> bool {
-        return mem::needs_drop::<T>();
+        return const { mem::needs_drop::<T>() };
     }
 }