Skip to content

Commit e197baf

Browse files
authored
Upgrade toolchain to 07/02 (#4195)
Culprit PRs: - rust-lang/rust#142839 - rust-lang/rust#143262 Resolves #4192 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 5f211cf commit e197baf

File tree

13 files changed

+119
-137
lines changed

13 files changed

+119
-137
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: 4 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -200,19 +200,6 @@ impl GotocCtx<'_> {
200200
}};
201201
}
202202

203-
// Intrinsics which encode a value known during compilation
204-
macro_rules! codegen_intrinsic_const {
205-
() => {{
206-
let place_ty = self.place_ty_stable(&place);
207-
let stable_instance = instance;
208-
let alloc = stable_instance.try_const_eval(place_ty).unwrap();
209-
// We assume that the intrinsic has type checked at this point, so
210-
// we can use the place type as the expression type.
211-
let expr = self.codegen_allocation(&alloc, place_ty, loc);
212-
self.codegen_expr_to_place_stable(&place, expr, loc)
213-
}};
214-
}
215-
216203
// Most atomic intrinsics do:
217204
// 1. Perform an operation on a primary argument (e.g., addition)
218205
// 2. Return the previous value of the primary argument
@@ -406,13 +393,11 @@ impl GotocCtx<'_> {
406393
Intrinsic::LogF64 => codegen_simple_intrinsic!(Log),
407394
Intrinsic::MaxNumF32 => codegen_simple_intrinsic!(Fmaxf),
408395
Intrinsic::MaxNumF64 => codegen_simple_intrinsic!(Fmax),
409-
Intrinsic::MinAlignOf => codegen_intrinsic_const!(),
410396
Intrinsic::MinNumF32 => codegen_simple_intrinsic!(Fminf),
411397
Intrinsic::MinNumF64 => codegen_simple_intrinsic!(Fmin),
412398
Intrinsic::MulWithOverflow => {
413399
self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc)
414400
}
415-
Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
416401
Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
417402
Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
418403
Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif),
@@ -505,8 +490,6 @@ impl GotocCtx<'_> {
505490
Intrinsic::Transmute => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc),
506491
Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf),
507492
Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc),
508-
Intrinsic::TypeId => codegen_intrinsic_const!(),
509-
Intrinsic::TypeName => codegen_intrinsic_const!(),
510493
Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc),
511494
Intrinsic::UnalignedVolatileLoad => {
512495
unstable_codegen!(self.codegen_expr_to_place_stable(
@@ -536,11 +519,11 @@ impl GotocCtx<'_> {
536519
assert!(self.place_ty_stable(place).kind().is_unit());
537520
self.codegen_write_bytes(fargs, farg_types, loc)
538521
}
539-
Intrinsic::PtrOffsetFrom
522+
Intrinsic::AlignOfVal
523+
| Intrinsic::PtrOffsetFrom
540524
| Intrinsic::PtrOffsetFromUnsigned
541-
| Intrinsic::SizeOfVal
542-
| Intrinsic::MinAlignOfVal => {
543-
unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str)
525+
| Intrinsic::SizeOfVal => {
526+
unreachable!("Kani models the intrinsic `{}` before codegen", intrinsic_str)
544527
}
545528
// Unimplemented
546529
Intrinsic::Unimplemented { name, issue_link } => {

kani-compiler/src/intrinsics.rs

Lines changed: 24 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ use stable_mir::{
1414
#[derive(Clone, Debug)]
1515
pub enum Intrinsic {
1616
AddWithOverflow,
17+
AlignOfVal,
1718
ArithOffset,
1819
AssertInhabited,
1920
AssertMemUninitializedValid,
@@ -81,12 +82,9 @@ pub enum Intrinsic {
8182
LogF64,
8283
MaxNumF32,
8384
MaxNumF64,
84-
MinAlignOf,
85-
MinAlignOfVal,
8685
MinNumF32,
8786
MinNumF64,
8887
MulWithOverflow,
89-
NeedsDrop,
9088
PowF32,
9189
PowF64,
9290
PowIF32,
@@ -132,8 +130,6 @@ pub enum Intrinsic {
132130
Transmute,
133131
TruncF32,
134132
TruncF64,
135-
TypeId,
136-
TypeName,
137133
TypedSwap,
138134
UnalignedVolatileLoad,
139135
UncheckedDiv,
@@ -181,6 +177,13 @@ impl Intrinsic {
181177
assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
182178
Self::AddWithOverflow
183179
}
180+
"align_of" => unreachable!(
181+
"Expected `core::intrinsics::align_of` to be handled by NullOp::SizeOf"
182+
),
183+
"align_of_val" => {
184+
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
185+
Self::AlignOfVal
186+
}
184187
"arith_offset" => {
185188
assert_sig_matches!(sig,
186189
RigidTy::RawPtr(_, Mutability::Not),
@@ -309,22 +312,14 @@ impl Intrinsic {
309312
assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool);
310313
Self::Likely
311314
}
312-
"align_of" => {
313-
assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize));
314-
Self::MinAlignOf
315-
}
316-
"align_of_val" => {
317-
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
318-
Self::MinAlignOfVal
319-
}
320315
"mul_with_overflow" => {
321316
assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
322317
Self::MulWithOverflow
323318
}
324-
"needs_drop" => {
325-
assert_sig_matches!(sig, => RigidTy::Bool);
326-
Self::NeedsDrop
327-
}
319+
// For const eval of nullary intrinsics, see https://github.com/rust-lang/rust/pull/142839
320+
"needs_drop" => unreachable!(
321+
"Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
322+
),
328323
// As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
329324
"offset" => unreachable!(
330325
"Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
@@ -361,7 +356,9 @@ impl Intrinsic {
361356
assert_sig_matches!(sig, _, _ => _);
362357
Self::SaturatingSub
363358
}
364-
"size_of" => unreachable!(),
359+
"size_of" => {
360+
unreachable!("Expected `core::intrinsics::size_of` to be handled by NullOp::SizeOf")
361+
}
365362
"size_of_val" => {
366363
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
367364
Self::SizeOfVal
@@ -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: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -611,6 +611,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> {
611611
fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
612612
match intrinsic {
613613
Intrinsic::AddWithOverflow
614+
| Intrinsic::AlignOfVal
614615
| Intrinsic::ArithOffset
615616
| Intrinsic::AssertInhabited
616617
| Intrinsic::AssertMemUninitializedValid
@@ -659,12 +660,9 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
659660
| Intrinsic::LogF64
660661
| Intrinsic::MaxNumF32
661662
| Intrinsic::MaxNumF64
662-
| Intrinsic::MinAlignOf
663-
| Intrinsic::MinAlignOfVal
664663
| Intrinsic::MinNumF32
665664
| Intrinsic::MinNumF64
666665
| Intrinsic::MulWithOverflow
667-
| Intrinsic::NeedsDrop
668666
| Intrinsic::PowF32
669667
| Intrinsic::PowF64
670668
| Intrinsic::PowIF32
@@ -691,8 +689,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
691689
| Intrinsic::Transmute
692690
| Intrinsic::TruncF32
693691
| Intrinsic::TruncF64
694-
| Intrinsic::TypeId
695-
| Intrinsic::TypeName
696692
| Intrinsic::UncheckedDiv
697693
| Intrinsic::UncheckedRem
698694
| Intrinsic::Unlikely

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

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -572,6 +572,7 @@ impl MirVisitor for CheckUninitVisitor {
572572
fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
573573
match intrinsic {
574574
Intrinsic::AddWithOverflow
575+
| Intrinsic::AlignOfVal
575576
| Intrinsic::ArithOffset
576577
| Intrinsic::AssertInhabited
577578
| Intrinsic::AssertMemUninitializedValid
@@ -619,12 +620,9 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
619620
| Intrinsic::LogF64
620621
| Intrinsic::MaxNumF32
621622
| Intrinsic::MaxNumF64
622-
| Intrinsic::MinAlignOf
623-
| Intrinsic::MinAlignOfVal
624623
| Intrinsic::MinNumF32
625624
| Intrinsic::MinNumF64
626625
| Intrinsic::MulWithOverflow
627-
| Intrinsic::NeedsDrop
628626
| Intrinsic::PowF32
629627
| Intrinsic::PowF64
630628
| Intrinsic::PowIF32
@@ -643,8 +641,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
643641
| Intrinsic::SubWithOverflow
644642
| Intrinsic::TruncF32
645643
| Intrinsic::TruncF64
646-
| Intrinsic::TypeId
647-
| Intrinsic::TypeName
648644
| Intrinsic::UncheckedDiv
649645
| Intrinsic::UncheckedRem
650646
| Intrinsic::Unlikely

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -424,10 +424,9 @@ impl RustcInternalMir for Statement {
424424
type T<'tcx> = rustc_middle::mir::Statement<'tcx>;
425425

426426
fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
427-
rustc_middle::mir::Statement {
428-
source_info: rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span)),
429-
kind: self.kind.internal_mir(tcx),
430-
}
427+
let source_info = rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span));
428+
let kind = self.kind.internal_mir(tcx);
429+
rustc_middle::mir::Statement::new(source_info, kind)
431430
}
432431
}
433432

@@ -654,14 +653,15 @@ impl RustcInternalMir for Body {
654653
let internal_basic_blocks = rustc_index::IndexVec::from_raw(
655654
self.blocks
656655
.iter()
657-
.map(|stable_basic_block| rustc_middle::mir::BasicBlockData {
658-
statements: stable_basic_block
656+
.map(|stable_basic_block| {
657+
let statements = stable_basic_block
659658
.statements
660659
.iter()
661660
.map(|statement| statement.internal_mir(tcx))
662-
.collect(),
663-
terminator: Some(stable_basic_block.terminator.internal_mir(tcx)),
664-
is_cleanup: false,
661+
.collect();
662+
let terminator = Some(stable_basic_block.terminator.internal_mir(tcx));
663+
let is_cleanup = false;
664+
rustc_middle::mir::BasicBlockData::new_stmts(statements, terminator, is_cleanup)
665665
})
666666
.collect(),
667667
);

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,8 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_, '_> {
180180
let intrinsic = Intrinsic::from_instance(&instance);
181181
debug!(?intrinsic, "handle_terminator");
182182
match intrinsic {
183+
Intrinsic::AlignOfVal => self.models[&KaniModel::AlignOfVal],
183184
Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal],
184-
Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal],
185185
Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom],
186186
Intrinsic::PtrOffsetFromUnsigned => {
187187
self.models[&KaniModel::PtrOffsetFromUnsigned]

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-02"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
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.

0 commit comments

Comments
 (0)