Skip to content

Commit 302cfc4

Browse files
author
Carolyn Zech
committed
handle nullary intrinsics
backends no longer need to implement these intrinsics, see rust-lang/rust#142839
1 parent 5f211cf commit 302cfc4

File tree

11 files changed

+92
-94
lines changed

11 files changed

+92
-94
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -231,7 +231,7 @@ unchecked_shr | Yes | |
231231
unchecked_sub | Yes | |
232232
unlikely | Yes | |
233233
unreachable | Yes | |
234-
variant_count | No | |
234+
variant_count | Yes | |
235235
volatile_copy_memory | No | See [Notes - Concurrency](#concurrency) |
236236
volatile_copy_nonoverlapping_memory | No | See [Notes - Concurrency](#concurrency) |
237237
volatile_load | Partial | See [Notes - Concurrency](#concurrency) |

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -412,7 +412,6 @@ impl GotocCtx<'_> {
412412
Intrinsic::MulWithOverflow => {
413413
self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc)
414414
}
415-
Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
416415
Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
417416
Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
418417
Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif),
@@ -505,8 +504,6 @@ impl GotocCtx<'_> {
505504
Intrinsic::Transmute => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc),
506505
Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf),
507506
Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc),
508-
Intrinsic::TypeId => codegen_intrinsic_const!(),
509-
Intrinsic::TypeName => codegen_intrinsic_const!(),
510507
Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc),
511508
Intrinsic::UnalignedVolatileLoad => {
512509
unstable_codegen!(self.codegen_expr_to_place_stable(

‎kani-compiler/src/intrinsics.rs‎

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,6 @@ pub enum Intrinsic {
8686
MinNumF32,
8787
MinNumF64,
8888
MulWithOverflow,
89-
NeedsDrop,
9089
PowF32,
9190
PowF64,
9291
PowIF32,
@@ -132,8 +131,6 @@ pub enum Intrinsic {
132131
Transmute,
133132
TruncF32,
134133
TruncF64,
135-
TypeId,
136-
TypeName,
137134
TypedSwap,
138135
UnalignedVolatileLoad,
139136
UncheckedDiv,
@@ -321,10 +318,10 @@ impl Intrinsic {
321318
assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
322319
Self::MulWithOverflow
323320
}
324-
"needs_drop" => {
325-
assert_sig_matches!(sig, => RigidTy::Bool);
326-
Self::NeedsDrop
327-
}
321+
// For const eval of nullary intrinsics, see https://github.com/rust-lang/rust/pull/142839
322+
"needs_drop" => unreachable!(
323+
"Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
324+
),
328325
// As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
329326
"offset" => unreachable!(
330327
"Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
@@ -374,14 +371,12 @@ impl Intrinsic {
374371
assert_sig_matches!(sig, _ => _);
375372
Self::Transmute
376373
}
377-
"type_id" => {
378-
assert_sig_matches!(sig, => RigidTy::Uint(UintTy::U128));
379-
Self::TypeId
380-
}
381-
"type_name" => {
382-
assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not));
383-
Self::TypeName
384-
}
374+
"type_id" => unreachable!(
375+
"Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
376+
),
377+
"type_name" => unreachable!(
378+
"Expected nullary intrinsic `core::intrinsics::type_name` to be const-evaluated before codegen"
379+
),
385380
"typed_swap_nonoverlapping" => {
386381
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Mut) => RigidTy::Tuple(_));
387382
Self::TypedSwap
@@ -409,6 +404,9 @@ impl Intrinsic {
409404
"unreachable" => unreachable!(
410405
"Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
411406
),
407+
"variant_count" => unreachable!(
408+
"Expected nullary intrinsic `core::intrinsics::variant_count` to be const-evaluated before codegen"
409+
),
412410
"volatile_copy_memory" => {
413411
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
414412
Self::VolatileCopyMemory

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -664,7 +664,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
664664
| Intrinsic::MinNumF32
665665
| Intrinsic::MinNumF64
666666
| Intrinsic::MulWithOverflow
667-
| Intrinsic::NeedsDrop
668667
| Intrinsic::PowF32
669668
| Intrinsic::PowF64
670669
| Intrinsic::PowIF32
@@ -691,8 +690,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
691690
| Intrinsic::Transmute
692691
| Intrinsic::TruncF32
693692
| Intrinsic::TruncF64
694-
| Intrinsic::TypeId
695-
| Intrinsic::TypeName
696693
| Intrinsic::UncheckedDiv
697694
| Intrinsic::UncheckedRem
698695
| Intrinsic::Unlikely

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -624,7 +624,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
624624
| Intrinsic::MinNumF32
625625
| Intrinsic::MinNumF64
626626
| Intrinsic::MulWithOverflow
627-
| Intrinsic::NeedsDrop
628627
| Intrinsic::PowF32
629628
| Intrinsic::PowF64
630629
| Intrinsic::PowIF32
@@ -643,8 +642,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
643642
| Intrinsic::SubWithOverflow
644643
| Intrinsic::TruncF32
645644
| Intrinsic::TruncF64
646-
| Intrinsic::TypeId
647-
| Intrinsic::TypeName
648645
| Intrinsic::UncheckedDiv
649646
| Intrinsic::UncheckedRem
650647
| Intrinsic::Unlikely

‎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-06-30"
5+
channel = "nightly-2025-07-01"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

‎tests/kani/Intrinsics/Compiler/variant_count.rs‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,27 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// kani-verify-fail
43

5-
// Check that `variant_count` is not supported.
6-
// This test can be replaced with `variant_count_fixme.rs` once the intrinsic is
7-
// supported and works as expected.
4+
// Check that `variant_count` is supported and returns the expected result.
85

96
#![feature(variant_count)]
107
use std::mem;
118

129
enum Void {}
10+
enum MyError {
11+
Error1,
12+
Error2,
13+
Error3,
14+
}
1315

1416
#[kani::proof]
1517
fn main() {
16-
let _ = mem::variant_count::<Void>();
18+
const VOID_COUNT: usize = mem::variant_count::<Void>();
19+
const ERROR_COUNT: usize = mem::variant_count::<MyError>();
20+
const OPTION_COUNT: usize = mem::variant_count::<Option<u32>>();
21+
const RESULT_COUNT: usize = mem::variant_count::<Result<u32, MyError>>();
22+
23+
assert!(VOID_COUNT == 0);
24+
assert!(ERROR_COUNT == 3);
25+
assert!(OPTION_COUNT == 2);
26+
assert!(RESULT_COUNT == 2);
1727
}

‎tests/kani/Intrinsics/Compiler/variant_count_fixme.rs‎

Lines changed: 0 additions & 22 deletions
This file was deleted.

‎tests/kani/Intrinsics/ConstEval/needs_drop.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ pub struct Foo<T> {
1111

1212
impl<T> Foo<T> {
1313
fn call_needs_drop(&self) -> bool {
14-
return mem::needs_drop::<T>();
14+
return const { mem::needs_drop::<T>() };
1515
}
1616
}
1717

‎tests/kani/Intrinsics/ConstEval/type_id.rs‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -14,28 +14,28 @@ enum MyEnum {}
1414
fn main() {
1515
let type_ids = [
1616
// Scalar types
17-
type_id::<i8>(),
18-
type_id::<i16>(),
19-
type_id::<i32>(),
20-
type_id::<i64>(),
21-
type_id::<i128>(),
22-
type_id::<isize>(),
23-
type_id::<u8>(),
24-
type_id::<u16>(),
25-
type_id::<u32>(),
26-
type_id::<u64>(),
27-
type_id::<u128>(),
28-
type_id::<usize>(),
29-
type_id::<f32>(),
30-
type_id::<f64>(),
31-
type_id::<bool>(),
32-
type_id::<char>(),
17+
const { type_id::<i8>() },
18+
const { type_id::<i16>() },
19+
const { type_id::<i32>() },
20+
const { type_id::<i64>() },
21+
const { type_id::<i128>() },
22+
const { type_id::<isize>() },
23+
const { type_id::<u8>() },
24+
const { type_id::<u16>() },
25+
const { type_id::<u32>() },
26+
const { type_id::<u64>() },
27+
const { type_id::<u128>() },
28+
const { type_id::<usize>() },
29+
const { type_id::<f32>() },
30+
const { type_id::<f64>() },
31+
const { type_id::<bool>() },
32+
const { type_id::<char>() },
3333
// Compound types (tuple and array)
34-
type_id::<(i32, i32)>(),
35-
type_id::<[i32; 5]>(),
34+
const { type_id::<(i32, i32)>() },
35+
const { type_id::<[i32; 5]>() },
3636
// Custom data types (struct and enum)
37-
type_id::<MyStruct>(),
38-
type_id::<MyEnum>(),
37+
const { type_id::<MyStruct>() },
38+
const { type_id::<MyEnum>() },
3939
];
4040

4141
// Check that there are no duplicate type IDs

0 commit comments

Comments
 (0)