From 3b7aa7b234842e4a63dfd7323bf59f3f1c79de41 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Thu, 7 Aug 2025 18:55:14 -0700 Subject: [PATCH 01/10] A bunch of LLM-generated contracts --- library/core/src/hint.rs | 8 ++++ library/core/src/iter/adapters/step_by.rs | 7 +++ library/core/src/ops/index_range.rs | 42 ++++++++++++++++++ library/std/src/sync/mpmc/context.rs | 10 +++++ .../stdarch/crates/core_arch/src/x86/sse3.rs | 44 +++++++++++++++++++ .../stdarch/crates/core_arch/src/x86/sse41.rs | 34 ++++++++++++++ 6 files changed, 145 insertions(+) diff --git a/library/core/src/hint.rs b/library/core/src/hint.rs index c72eeb9a9c976..663c8d894d6b3 100644 --- a/library/core/src/hint.rs +++ b/library/core/src/hint.rs @@ -4,6 +4,12 @@ //! //! Hints may be compile time or runtime. +use safety::{ensures,requires}; +#[cfg(kani)] +use crate::kani; +#[allow(unused_imports)] +use crate::ub_checks::*; + use crate::mem::MaybeUninit; use crate::{intrinsics, ub_checks}; @@ -99,6 +105,7 @@ use crate::{intrinsics, ub_checks}; #[stable(feature = "unreachable", since = "1.27.0")] #[rustc_const_stable(feature = "const_unreachable_unchecked", since = "1.57.0")] #[track_caller] +#[requires(false)] pub const unsafe fn unreachable_unchecked() -> ! { ub_checks::assert_unsafe_precondition!( check_language_ub, @@ -198,6 +205,7 @@ pub const unsafe fn unreachable_unchecked() -> ! { #[doc(alias = "assume")] #[stable(feature = "hint_assert_unchecked", since = "1.81.0")] #[rustc_const_stable(feature = "hint_assert_unchecked", since = "1.81.0")] +#[requires(cond == true)] pub const unsafe fn assert_unchecked(cond: bool) { // SAFETY: The caller promised `cond` is true. unsafe { diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index 2d0f210420317..b1e19f6e055f1 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -1,3 +1,9 @@ +use safety::{ensures,requires}; +#[cfg(kani)] +use crate::kani; +#[allow(unused_imports)] +use crate::ub_checks::*; + use crate::intrinsics; use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn}; use crate::num::NonZero; @@ -40,6 +46,7 @@ impl StepBy { /// The `step` that was originally passed to `Iterator::step_by(step)`, /// aka `self.step_minus_one + 1`. #[inline] + #[requires(self.step_minus_one != usize::MAX)] fn original_step(&self) -> NonZero { // SAFETY: By type invariant, `step_minus_one` cannot be `MAX`, which // means the addition cannot overflow and the result cannot be zero. diff --git a/library/core/src/ops/index_range.rs b/library/core/src/ops/index_range.rs index 507fa9460bea6..b390b56406aa3 100644 --- a/library/core/src/ops/index_range.rs +++ b/library/core/src/ops/index_range.rs @@ -1,3 +1,9 @@ +use safety::{ensures,requires}; +#[cfg(kani)] +use crate::kani; +#[allow(unused_imports)] +use crate::ub_checks::*; + use crate::iter::{FusedIterator, TrustedLen}; use crate::num::NonZero; use crate::ops::{NeverShortCircuit, Try}; @@ -20,6 +26,7 @@ impl IndexRange { /// - `start <= end` #[inline] #[track_caller] + #[requires(start <= end)] pub(crate) const unsafe fn new_unchecked(start: usize, end: usize) -> Self { ub_checks::assert_unsafe_precondition!( check_library_ub, @@ -54,6 +61,8 @@ impl IndexRange { /// # Safety /// - Can only be called when `start < end`, aka when `len > 0`. #[inline] + #[requires(self.start < self.end)] + #[cfg_attr(kani, kani::modifies(self))] unsafe fn next_unchecked(&mut self) -> usize { debug_assert!(self.start < self.end); @@ -66,6 +75,8 @@ impl IndexRange { /// # Safety /// - Can only be called when `start < end`, aka when `len > 0`. #[inline] + #[requires(self.start < self.end)] + #[cfg_attr(kani, kani::modifies(self))] unsafe fn next_back_unchecked(&mut self) -> usize { debug_assert!(self.start < self.end); @@ -225,3 +236,34 @@ impl ExactSizeIterator for IndexRange { unsafe impl TrustedLen for IndexRange {} impl FusedIterator for IndexRange {} +#[cfg(kani)] +mod verify { + use super::*; + #[kani::proof_for_contract(IndexRange::new_unchecked)] + fn proof_for_index_range_new_unchecked() { + let start = kani::any::(); + let end = kani::any::(); + + unsafe { IndexRange::new_unchecked(start, end) }; + } + + #[kani::proof_for_contract(IndexRange::next_unchecked)] + fn proof_for_index_range_next_unchecked() { + let start = kani::any::(); + let end = kani::any::(); + + let mut range = unsafe { IndexRange::new_unchecked(start, end) }; + + unsafe { range.next_unchecked() }; + } + + #[kani::proof_for_contract(IndexRange::next_back_unchecked)] + fn proof_for_index_range_next_back_unchecked() { + let start = kani::any::(); + let end = kani::any::(); + + let mut range = unsafe { IndexRange::new_unchecked(start, end) }; + + unsafe { range.next_back_unchecked() }; + } +} diff --git a/library/std/src/sync/mpmc/context.rs b/library/std/src/sync/mpmc/context.rs index 6b2f4cb6ffd29..8114db7d98370 100644 --- a/library/std/src/sync/mpmc/context.rs +++ b/library/std/src/sync/mpmc/context.rs @@ -1,5 +1,14 @@ //! Thread-local channel context. +#![feature(ub_checks)] +use safety::{ensures,requires}; +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +use core::kani; +#[allow(unused_imports)] +#[unstable(feature = "ub_checks", issue = "none")] +use core::ub_checks::*; + use super::select::Selected; use super::waker::current_thread_id; use crate::cell::Cell; @@ -116,6 +125,7 @@ impl Context { /// # Safety /// This may only be called from the thread this `Context` belongs to. #[inline] + #[requires(self.thread_id() == current_thread_id())] pub unsafe fn wait_until(&self, deadline: Option) -> Selected { loop { // Check whether an operation has been selected. diff --git a/library/stdarch/crates/core_arch/src/x86/sse3.rs b/library/stdarch/crates/core_arch/src/x86/sse3.rs index 7a32cfe472d43..06d6f9e367ac2 100644 --- a/library/stdarch/crates/core_arch/src/x86/sse3.rs +++ b/library/stdarch/crates/core_arch/src/x86/sse3.rs @@ -1,5 +1,14 @@ //! Streaming SIMD Extensions 3 (SSE3) +#![feature(ub_checks)] +use safety::{ensures,requires}; +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +use core::kani; +#[allow(unused_imports)] +#[unstable(feature = "ub_checks", issue = "none")] +use core::ub_checks::*; + use crate::core_arch::{simd::*, x86::*}; use crate::intrinsics::simd::*; @@ -99,6 +108,7 @@ pub fn _mm_hsub_ps(a: __m128, b: __m128) -> __m128 { #[target_feature(enable = "sse3")] #[cfg_attr(test, assert_instr(lddqu))] #[stable(feature = "simd_x86", since = "1.27.0")] +#[requires(can_dereference(mem_addr))] pub unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i { transmute(lddqu(mem_addr as *const _)) } @@ -260,3 +270,37 @@ mod tests { assert_eq_m128d(r, _mm_setr_pd(d, d)); } } +#[cfg(kani)] +mod verify { + use super::*; + + #[cfg(kani)] + #[kani::proof_for_contract(unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i)] + fn proof_mm_lddqu_si128() { + // Create a valid __m128i value + let mut value = [0i32; 4]; + + // Get a pointer to the value + let ptr: *const __m128i = value.as_ptr() as *const __m128i; + + // Call the function with the valid pointer + unsafe { + let _result = _mm_lddqu_si128(ptr); + } + } + + #[cfg(kani)] + #[kani::proof_for_contract(unsafe fn _mm_loadddup_pd(mem_addr: *const f64) -> __m128d)] + fn proof_mm_loadddup_pd() { + // Create a valid f64 value + let value: f64 = 0.0; + + // Get a pointer to the value + let ptr: *const f64 = &value; + + // Call the function with the valid pointer + unsafe { + let _result = _mm_loadddup_pd(ptr); + } + } +} diff --git a/library/stdarch/crates/core_arch/src/x86/sse41.rs b/library/stdarch/crates/core_arch/src/x86/sse41.rs index 9aa200dfc07ab..e3ac2e5094cc4 100644 --- a/library/stdarch/crates/core_arch/src/x86/sse41.rs +++ b/library/stdarch/crates/core_arch/src/x86/sse41.rs @@ -1,5 +1,14 @@ //! Streaming SIMD Extensions 4.1 (SSE4.1) +#![feature(ub_checks)] +use safety::{ensures,requires}; +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +use core::kani; +#[allow(unused_imports)] +#[unstable(feature = "ub_checks", issue = "none")] +use core::ub_checks::*; + use crate::core_arch::{simd::*, x86::*}; use crate::intrinsics::simd::*; @@ -1132,6 +1141,8 @@ pub fn _mm_test_mix_ones_zeros(a: __m128i, mask: __m128i) -> i32 { #[target_feature(enable = "sse4.1")] #[cfg_attr(test, assert_instr(movntdqa))] #[stable(feature = "simd_x86_updates", since = "1.82.0")] +#[requires(can_dereference(mem_addr))] +#[requires(mem_addr as usize % 16 == 0)] pub unsafe fn _mm_stream_load_si128(mem_addr: *const __m128i) -> __m128i { let dst: __m128i; crate::arch::asm!( @@ -1939,3 +1950,26 @@ mod tests { assert_eq_m128i(a, r); } } +#[cfg(kani)] +mod verify { + use super::*; + #[cfg(kani)] + #[repr(align(16))] + struct Aligned16Bytes { + data: [u8; 16], + } + + #[cfg(kani)] + #[kani::proof_for_contract(_mm_stream_load_si128)] + fn verify_mm_stream_load_si128() { + // Allocate memory for __m128i (16 bytes) with proper alignment + let mut aligned_data = Aligned16Bytes { data: [0u8; 16] }; + let ptr = &aligned_data.data as *const _ as *const __m128i; + + // Call the function with our properly aligned pointer + unsafe { + let _result = _mm_stream_load_si128(ptr); + // No postconditions to verify + } + } +} From 59cdd4c92b64715b96196dc9ab6d817d81c9cd99 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Fri, 8 Aug 2025 07:52:53 -0700 Subject: [PATCH 02/10] Undo changes to stdarch --- .../stdarch/crates/core_arch/src/x86/sse3.rs | 44 ------------------- .../stdarch/crates/core_arch/src/x86/sse41.rs | 34 -------------- 2 files changed, 78 deletions(-) diff --git a/library/stdarch/crates/core_arch/src/x86/sse3.rs b/library/stdarch/crates/core_arch/src/x86/sse3.rs index 06d6f9e367ac2..7a32cfe472d43 100644 --- a/library/stdarch/crates/core_arch/src/x86/sse3.rs +++ b/library/stdarch/crates/core_arch/src/x86/sse3.rs @@ -1,14 +1,5 @@ //! Streaming SIMD Extensions 3 (SSE3) -#![feature(ub_checks)] -use safety::{ensures,requires}; -#[cfg(kani)] -#[unstable(feature="kani", issue="none")] -use core::kani; -#[allow(unused_imports)] -#[unstable(feature = "ub_checks", issue = "none")] -use core::ub_checks::*; - use crate::core_arch::{simd::*, x86::*}; use crate::intrinsics::simd::*; @@ -108,7 +99,6 @@ pub fn _mm_hsub_ps(a: __m128, b: __m128) -> __m128 { #[target_feature(enable = "sse3")] #[cfg_attr(test, assert_instr(lddqu))] #[stable(feature = "simd_x86", since = "1.27.0")] -#[requires(can_dereference(mem_addr))] pub unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i { transmute(lddqu(mem_addr as *const _)) } @@ -270,37 +260,3 @@ mod tests { assert_eq_m128d(r, _mm_setr_pd(d, d)); } } -#[cfg(kani)] -mod verify { - use super::*; - - #[cfg(kani)] - #[kani::proof_for_contract(unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i)] - fn proof_mm_lddqu_si128() { - // Create a valid __m128i value - let mut value = [0i32; 4]; - - // Get a pointer to the value - let ptr: *const __m128i = value.as_ptr() as *const __m128i; - - // Call the function with the valid pointer - unsafe { - let _result = _mm_lddqu_si128(ptr); - } - } - - #[cfg(kani)] - #[kani::proof_for_contract(unsafe fn _mm_loadddup_pd(mem_addr: *const f64) -> __m128d)] - fn proof_mm_loadddup_pd() { - // Create a valid f64 value - let value: f64 = 0.0; - - // Get a pointer to the value - let ptr: *const f64 = &value; - - // Call the function with the valid pointer - unsafe { - let _result = _mm_loadddup_pd(ptr); - } - } -} diff --git a/library/stdarch/crates/core_arch/src/x86/sse41.rs b/library/stdarch/crates/core_arch/src/x86/sse41.rs index e3ac2e5094cc4..9aa200dfc07ab 100644 --- a/library/stdarch/crates/core_arch/src/x86/sse41.rs +++ b/library/stdarch/crates/core_arch/src/x86/sse41.rs @@ -1,14 +1,5 @@ //! Streaming SIMD Extensions 4.1 (SSE4.1) -#![feature(ub_checks)] -use safety::{ensures,requires}; -#[cfg(kani)] -#[unstable(feature="kani", issue="none")] -use core::kani; -#[allow(unused_imports)] -#[unstable(feature = "ub_checks", issue = "none")] -use core::ub_checks::*; - use crate::core_arch::{simd::*, x86::*}; use crate::intrinsics::simd::*; @@ -1141,8 +1132,6 @@ pub fn _mm_test_mix_ones_zeros(a: __m128i, mask: __m128i) -> i32 { #[target_feature(enable = "sse4.1")] #[cfg_attr(test, assert_instr(movntdqa))] #[stable(feature = "simd_x86_updates", since = "1.82.0")] -#[requires(can_dereference(mem_addr))] -#[requires(mem_addr as usize % 16 == 0)] pub unsafe fn _mm_stream_load_si128(mem_addr: *const __m128i) -> __m128i { let dst: __m128i; crate::arch::asm!( @@ -1950,26 +1939,3 @@ mod tests { assert_eq_m128i(a, r); } } -#[cfg(kani)] -mod verify { - use super::*; - #[cfg(kani)] - #[repr(align(16))] - struct Aligned16Bytes { - data: [u8; 16], - } - - #[cfg(kani)] - #[kani::proof_for_contract(_mm_stream_load_si128)] - fn verify_mm_stream_load_si128() { - // Allocate memory for __m128i (16 bytes) with proper alignment - let mut aligned_data = Aligned16Bytes { data: [0u8; 16] }; - let ptr = &aligned_data.data as *const _ as *const __m128i; - - // Call the function with our properly aligned pointer - unsafe { - let _result = _mm_stream_load_si128(ptr); - // No postconditions to verify - } - } -} From 743e5e432bf5aad8eb7a75ad3607a32ffc697e20 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Fri, 8 Aug 2025 08:16:21 -0700 Subject: [PATCH 03/10] Fix imports --- library/core/src/hint.rs | 4 +--- library/core/src/iter/adapters/step_by.rs | 4 +--- library/core/src/ops/index_range.rs | 4 +--- library/std/src/sync/mpmc/context.rs | 6 +----- 4 files changed, 4 insertions(+), 14 deletions(-) diff --git a/library/core/src/hint.rs b/library/core/src/hint.rs index 663c8d894d6b3..b181a7f96b01d 100644 --- a/library/core/src/hint.rs +++ b/library/core/src/hint.rs @@ -4,11 +4,9 @@ //! //! Hints may be compile time or runtime. -use safety::{ensures,requires}; +use safety::requires; #[cfg(kani)] use crate::kani; -#[allow(unused_imports)] -use crate::ub_checks::*; use crate::mem::MaybeUninit; use crate::{intrinsics, ub_checks}; diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index b1e19f6e055f1..8195ba7dd5f4d 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -1,8 +1,6 @@ -use safety::{ensures,requires}; +use safety::requires; #[cfg(kani)] use crate::kani; -#[allow(unused_imports)] -use crate::ub_checks::*; use crate::intrinsics; use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn}; diff --git a/library/core/src/ops/index_range.rs b/library/core/src/ops/index_range.rs index b390b56406aa3..cd6c6098ac3b0 100644 --- a/library/core/src/ops/index_range.rs +++ b/library/core/src/ops/index_range.rs @@ -1,8 +1,6 @@ -use safety::{ensures,requires}; +use safety::requires; #[cfg(kani)] use crate::kani; -#[allow(unused_imports)] -use crate::ub_checks::*; use crate::iter::{FusedIterator, TrustedLen}; use crate::num::NonZero; diff --git a/library/std/src/sync/mpmc/context.rs b/library/std/src/sync/mpmc/context.rs index 8114db7d98370..12b39890f56ac 100644 --- a/library/std/src/sync/mpmc/context.rs +++ b/library/std/src/sync/mpmc/context.rs @@ -1,13 +1,9 @@ //! Thread-local channel context. -#![feature(ub_checks)] -use safety::{ensures,requires}; #[cfg(kani)] #[unstable(feature="kani", issue="none")] use core::kani; -#[allow(unused_imports)] -#[unstable(feature = "ub_checks", issue = "none")] -use core::ub_checks::*; +use safety::requires; use super::select::Selected; use super::waker::current_thread_id; From 44ab559502a3d32423df023c5d6b3eeaebcb7042 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Fri, 8 Aug 2025 08:27:41 -0700 Subject: [PATCH 04/10] Fix imports --- library/core/src/hint.rs | 4 ++-- library/core/src/iter/adapters/step_by.rs | 8 ++++---- library/core/src/ops/index_range.rs | 6 +++--- library/std/src/sync/mpmc/context.rs | 5 +++-- 4 files changed, 12 insertions(+), 11 deletions(-) diff --git a/library/core/src/hint.rs b/library/core/src/hint.rs index b181a7f96b01d..0365ad612122c 100644 --- a/library/core/src/hint.rs +++ b/library/core/src/hint.rs @@ -4,13 +4,13 @@ //! //! Hints may be compile time or runtime. -use safety::requires; #[cfg(kani)] use crate::kani; - use crate::mem::MaybeUninit; use crate::{intrinsics, ub_checks}; +use safety::requires; + /// Informs the compiler that the site which is calling this function is not /// reachable, possibly enabling further optimizations. /// diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index 8195ba7dd5f4d..c09bb22986c55 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -1,12 +1,12 @@ -use safety::requires; -#[cfg(kani)] -use crate::kani; - use crate::intrinsics; use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn}; +#[cfg(kani)] +use crate::kani; use crate::num::NonZero; use crate::ops::{Range, Try}; +use safety::requires; + /// An iterator for stepping iterators by a custom amount. /// /// This `struct` is created by the [`step_by`] method on [`Iterator`]. See diff --git a/library/core/src/ops/index_range.rs b/library/core/src/ops/index_range.rs index cd6c6098ac3b0..d6bfac547e5ee 100644 --- a/library/core/src/ops/index_range.rs +++ b/library/core/src/ops/index_range.rs @@ -1,12 +1,12 @@ -use safety::requires; +use crate::iter::{FusedIterator, TrustedLen}; #[cfg(kani)] use crate::kani; - -use crate::iter::{FusedIterator, TrustedLen}; use crate::num::NonZero; use crate::ops::{NeverShortCircuit, Try}; use crate::ub_checks; +use safety::requires; + /// Like a `Range`, but with a safety invariant that `start <= end`. /// /// This means that `end - start` cannot overflow, allowing some μoptimizations. diff --git a/library/std/src/sync/mpmc/context.rs b/library/std/src/sync/mpmc/context.rs index 12b39890f56ac..6b21ef3e888eb 100644 --- a/library/std/src/sync/mpmc/context.rs +++ b/library/std/src/sync/mpmc/context.rs @@ -1,9 +1,8 @@ //! Thread-local channel context. #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue="none")] use core::kani; -use safety::requires; use super::select::Selected; use super::waker::current_thread_id; @@ -14,6 +13,8 @@ use crate::sync::atomic::{Atomic, AtomicPtr, AtomicUsize, Ordering}; use crate::thread::{self, Thread}; use crate::time::Instant; +use safety::requires; + /// Thread-local context. #[derive(Debug, Clone)] pub struct Context { From c0927a755232116426753e3e1ebbc344ed26dd1c Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Fri, 8 Aug 2025 08:43:31 -0700 Subject: [PATCH 05/10] Fix imports --- library/core/src/hint.rs | 4 ++-- library/core/src/iter/adapters/step_by.rs | 4 ++-- library/core/src/ops/index_range.rs | 4 ++-- library/std/src/sync/mpmc/context.rs | 6 +++--- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/library/core/src/hint.rs b/library/core/src/hint.rs index 0365ad612122c..e7a19e2d8000a 100644 --- a/library/core/src/hint.rs +++ b/library/core/src/hint.rs @@ -4,13 +4,13 @@ //! //! Hints may be compile time or runtime. +use safety::requires; + #[cfg(kani)] use crate::kani; use crate::mem::MaybeUninit; use crate::{intrinsics, ub_checks}; -use safety::requires; - /// Informs the compiler that the site which is calling this function is not /// reachable, possibly enabling further optimizations. /// diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index c09bb22986c55..f43d0f6206a56 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -1,3 +1,5 @@ +use safety::requires; + use crate::intrinsics; use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn}; #[cfg(kani)] @@ -5,8 +7,6 @@ use crate::kani; use crate::num::NonZero; use crate::ops::{Range, Try}; -use safety::requires; - /// An iterator for stepping iterators by a custom amount. /// /// This `struct` is created by the [`step_by`] method on [`Iterator`]. See diff --git a/library/core/src/ops/index_range.rs b/library/core/src/ops/index_range.rs index d6bfac547e5ee..2a347ded448f0 100644 --- a/library/core/src/ops/index_range.rs +++ b/library/core/src/ops/index_range.rs @@ -1,3 +1,5 @@ +use safety::requires; + use crate::iter::{FusedIterator, TrustedLen}; #[cfg(kani)] use crate::kani; @@ -5,8 +7,6 @@ use crate::num::NonZero; use crate::ops::{NeverShortCircuit, Try}; use crate::ub_checks; -use safety::requires; - /// Like a `Range`, but with a safety invariant that `start <= end`. /// /// This means that `end - start` cannot overflow, allowing some μoptimizations. diff --git a/library/std/src/sync/mpmc/context.rs b/library/std/src/sync/mpmc/context.rs index 6b21ef3e888eb..e6eb6b9cace03 100644 --- a/library/std/src/sync/mpmc/context.rs +++ b/library/std/src/sync/mpmc/context.rs @@ -1,9 +1,11 @@ //! Thread-local channel context. #[cfg(kani)] -#[unstable(feature = "kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] use core::kani; +use safety::requires; + use super::select::Selected; use super::waker::current_thread_id; use crate::cell::Cell; @@ -13,8 +15,6 @@ use crate::sync::atomic::{Atomic, AtomicPtr, AtomicUsize, Ordering}; use crate::thread::{self, Thread}; use crate::time::Instant; -use safety::requires; - /// Thread-local context. #[derive(Debug, Clone)] pub struct Context { From d41de3fb1af6bd400f09e79918e0d5d389a8655f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Aug 2025 11:43:18 +0200 Subject: [PATCH 06/10] Add type invariant --- library/core/src/iter/adapters/step_by.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index f43d0f6206a56..ee043caab861f 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -1,11 +1,10 @@ -use safety::requires; - use crate::intrinsics; use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn}; #[cfg(kani)] use crate::kani; use crate::num::NonZero; use crate::ops::{Range, Try}; +use crate::ub_checks::Invariant; /// An iterator for stepping iterators by a custom amount. /// @@ -33,6 +32,12 @@ pub struct StepBy { first_take: bool, } +impl Invariant for StepBy { + fn is_safe(&self) -> bool { + step_minus_one < usize::MAX + } +} + impl StepBy { #[inline] pub(in crate::iter) fn new(iter: I, step: usize) -> StepBy { From 583e475666d79f02dede27862ae13c02a1059ccf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Aug 2025 11:43:43 +0200 Subject: [PATCH 07/10] Update library/core/src/iter/adapters/step_by.rs --- library/core/src/iter/adapters/step_by.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index ee043caab861f..5fab3a326642e 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -49,7 +49,6 @@ impl StepBy { /// The `step` that was originally passed to `Iterator::step_by(step)`, /// aka `self.step_minus_one + 1`. #[inline] - #[requires(self.step_minus_one != usize::MAX)] fn original_step(&self) -> NonZero { // SAFETY: By type invariant, `step_minus_one` cannot be `MAX`, which // means the addition cannot overflow and the result cannot be zero. From f8afdfeca6a9f1f7d1dd91cdb7de385130d357b6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Aug 2025 11:43:49 +0200 Subject: [PATCH 08/10] Update library/core/src/hint.rs --- library/core/src/hint.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/hint.rs b/library/core/src/hint.rs index e7a19e2d8000a..a06ffde6ed9b2 100644 --- a/library/core/src/hint.rs +++ b/library/core/src/hint.rs @@ -203,7 +203,7 @@ pub const unsafe fn unreachable_unchecked() -> ! { #[doc(alias = "assume")] #[stable(feature = "hint_assert_unchecked", since = "1.81.0")] #[rustc_const_stable(feature = "hint_assert_unchecked", since = "1.81.0")] -#[requires(cond == true)] +#[requires(cond)] pub const unsafe fn assert_unchecked(cond: bool) { // SAFETY: The caller promised `cond` is true. unsafe { From 9ef3aa94e323be494213a015103dc99a6147b0b6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Aug 2025 11:49:49 +0200 Subject: [PATCH 09/10] Fix syntax --- library/core/src/iter/adapters/step_by.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index 5fab3a326642e..e65e4b3514086 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -34,7 +34,7 @@ pub struct StepBy { impl Invariant for StepBy { fn is_safe(&self) -> bool { - step_minus_one < usize::MAX + self.step_minus_one < usize::MAX } } From 1242e65fc711c1d70815cdf82e4fd94bff6daf68 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Aug 2025 11:56:14 +0200 Subject: [PATCH 10/10] Stability attribute --- library/core/src/iter/adapters/step_by.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index e65e4b3514086..32604a07ca40c 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -32,6 +32,7 @@ pub struct StepBy { first_take: bool, } +#[unstable(feature = "ub_checks", issue = "none")] impl Invariant for StepBy { fn is_safe(&self) -> bool { self.step_minus_one < usize::MAX