diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 208b43479185..b847d75f63e1 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/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) | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 921d9bd8c33e..6e896ee97288 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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 } => { diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 0ffc0cd8d5be..c49c1d3182f6 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/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 diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 363831c1db26..fa8521ec1499 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/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 diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 62161d28dee2..90bc7a78a3aa 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/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 diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 53b5d2e35166..1657f0867f65 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/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(), ); diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 524130a8a92e..6dcaa7e1d6fe 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/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] diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b88fc294f52a..42a4e2ec1383 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-06-30" +channel = "nightly-2025-07-02" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/Compiler/variant_count.rs b/tests/kani/Intrinsics/Compiler/variant_count.rs index a67dea0b8f0e..4bbdfd8c222e 100644 --- a/tests/kani/Intrinsics/Compiler/variant_count.rs +++ b/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::(); + const VOID_COUNT: usize = mem::variant_count::(); + const ERROR_COUNT: usize = mem::variant_count::(); + const OPTION_COUNT: usize = mem::variant_count::>(); + const RESULT_COUNT: usize = mem::variant_count::>(); + + assert!(VOID_COUNT == 0); + assert!(ERROR_COUNT == 3); + assert!(OPTION_COUNT == 2); + assert!(RESULT_COUNT == 2); } diff --git a/tests/kani/Intrinsics/Compiler/variant_count_fixme.rs b/tests/kani/Intrinsics/Compiler/variant_count_fixme.rs deleted file mode 100644 index 31ce1c7bc19a..000000000000 --- a/tests/kani/Intrinsics/Compiler/variant_count_fixme.rs +++ /dev/null @@ -1,22 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// 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() { - assert!(mem::variant_count::() == 0); - assert!(mem::variant_count::() == 3); - assert!(mem::variant_count::>() == 2); - assert!(mem::variant_count::>() == 2); -} diff --git a/tests/kani/Intrinsics/ConstEval/needs_drop.rs b/tests/kani/Intrinsics/ConstEval/needs_drop.rs index e2fdfa512995..12e8de0f12e0 100644 --- a/tests/kani/Intrinsics/ConstEval/needs_drop.rs +++ b/tests/kani/Intrinsics/ConstEval/needs_drop.rs @@ -11,7 +11,7 @@ pub struct Foo { impl Foo { fn call_needs_drop(&self) -> bool { - return mem::needs_drop::(); + return const { mem::needs_drop::() }; } } diff --git a/tests/kani/Intrinsics/ConstEval/type_id.rs b/tests/kani/Intrinsics/ConstEval/type_id.rs index 233292fcef45..9c2358997fd4 100644 --- a/tests/kani/Intrinsics/ConstEval/type_id.rs +++ b/tests/kani/Intrinsics/ConstEval/type_id.rs @@ -14,28 +14,28 @@ enum MyEnum {} fn main() { let type_ids = [ // Scalar types - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), - type_id::(), + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, + const { type_id::() }, // Compound types (tuple and array) - type_id::<(i32, i32)>(), - type_id::<[i32; 5]>(), + const { type_id::<(i32, i32)>() }, + const { type_id::<[i32; 5]>() }, // Custom data types (struct and enum) - type_id::(), - type_id::(), + const { type_id::() }, + const { type_id::() }, ]; // Check that there are no duplicate type IDs diff --git a/tests/kani/Intrinsics/ConstEval/type_name.rs b/tests/kani/Intrinsics/ConstEval/type_name.rs index 7c0a2cdd4af2..2742cbba34b8 100644 --- a/tests/kani/Intrinsics/ConstEval/type_name.rs +++ b/tests/kani/Intrinsics/ConstEval/type_name.rs @@ -13,26 +13,47 @@ enum MyEnum {} #[kani::proof] fn main() { // Scalar types - assert!(type_name::() == "i8"); - assert!(type_name::() == "i16"); - assert!(type_name::() == "i32"); - assert!(type_name::() == "i64"); - assert!(type_name::() == "i128"); - assert!(type_name::() == "isize"); - assert!(type_name::() == "u8"); - assert!(type_name::() == "u16"); - assert!(type_name::() == "u32"); - assert!(type_name::() == "u64"); - assert!(type_name::() == "u128"); - assert!(type_name::() == "usize"); - assert!(type_name::() == "f32"); - assert!(type_name::() == "f64"); - assert!(type_name::() == "bool"); - assert!(type_name::() == "char"); + const I8_NAME: &str = const { type_name::() }; + const I16_NAME: &str = const { type_name::() }; + const I32_NAME: &str = const { type_name::() }; + const I64_NAME: &str = const { type_name::() }; + const I128_NAME: &str = const { type_name::() }; + const ISIZE_NAME: &str = const { type_name::() }; + const U8_NAME: &str = const { type_name::() }; + const U16_NAME: &str = const { type_name::() }; + const U32_NAME: &str = const { type_name::() }; + const U64_NAME: &str = const { type_name::() }; + const U128_NAME: &str = const { type_name::() }; + const USIZE_NAME: &str = const { type_name::() }; + const F32_NAME: &str = const { type_name::() }; + const F64_NAME: &str = const { type_name::() }; + const BOOL_NAME: &str = const { type_name::() }; + const CHAR_NAME: &str = const { type_name::() }; // Compound types (tuple and array) - assert!(type_name::<(i32, i32)>() == "(i32, i32)"); - assert!(type_name::<[i32; 5]>() == "[i32; 5]"); + const TUPLE_NAME: &str = const { type_name::<(i32, i32)>() }; + const ARRAY_NAME: &str = const { type_name::<[i32; 5]>() }; // Custom data types (struct and enum) - assert!(type_name::() == "type_name::MyStruct"); - assert!(type_name::() == "type_name::MyEnum"); + const STRUCT_NAME: &str = const { type_name::() }; + const ENUM_NAME: &str = const { type_name::() }; + + assert_eq!(I8_NAME, "i8"); + assert_eq!(I16_NAME, "i16"); + assert_eq!(I32_NAME, "i32"); + assert_eq!(I64_NAME, "i64"); + assert_eq!(I128_NAME, "i128"); + assert_eq!(ISIZE_NAME, "isize"); + assert_eq!(U8_NAME, "u8"); + assert_eq!(U16_NAME, "u16"); + assert_eq!(U32_NAME, "u32"); + assert_eq!(U64_NAME, "u64"); + assert_eq!(U128_NAME, "u128"); + assert_eq!(USIZE_NAME, "usize"); + assert_eq!(F32_NAME, "f32"); + assert_eq!(F64_NAME, "f64"); + assert_eq!(BOOL_NAME, "bool"); + assert_eq!(CHAR_NAME, "char"); + assert_eq!(TUPLE_NAME, "(i32, i32)"); + assert_eq!(ARRAY_NAME, "[i32; 5]"); + assert_eq!(STRUCT_NAME, "type_name::MyStruct"); + assert_eq!(ENUM_NAME, "type_name::MyEnum"); }