From 552754640c7ce50e78b12eb9c9b0cac22da45921 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Sat, 28 Mar 2026 23:05:55 +0100 Subject: [PATCH 1/6] Challenge 7: Verify safety of Atomic from_ptr methods Add Kani proof harnesses for all Atomic from_ptr functions specified in Challenge #7 Part 1: AtomicBool, AtomicI8, AtomicU8, AtomicI16, AtomicU16, AtomicI32, AtomicU32, AtomicI64, AtomicU64, AtomicPtr. Each harness verifies pointer validity and alignment for the unsafe from_ptr conversion. Resolves #83 Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/sync/atomic.rs | 88 +++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index 30a42d4eb5e64..0cbe5823b4c18 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -4480,3 +4480,91 @@ impl fmt::Pointer for AtomicPtr { pub fn spin_loop_hint() { spin_loop() } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + #[kani::proof] + fn verify_atomic_bool_from_ptr() { + let mut val: bool = kani::any(); + let ptr = &mut val as *mut bool; + let atomic = unsafe { AtomicBool::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_i8_from_ptr() { + let mut val: i8 = kani::any(); + let ptr = &mut val as *mut i8; + let atomic = unsafe { AtomicI8::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_u8_from_ptr() { + let mut val: u8 = kani::any(); + let ptr = &mut val as *mut u8; + let atomic = unsafe { AtomicU8::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_i16_from_ptr() { + let mut val: i16 = kani::any(); + let ptr = &mut val as *mut i16; + let atomic = unsafe { AtomicI16::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_u16_from_ptr() { + let mut val: u16 = kani::any(); + let ptr = &mut val as *mut u16; + let atomic = unsafe { AtomicU16::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_i32_from_ptr() { + let mut val: i32 = kani::any(); + let ptr = &mut val as *mut i32; + let atomic = unsafe { AtomicI32::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_u32_from_ptr() { + let mut val: u32 = kani::any(); + let ptr = &mut val as *mut u32; + let atomic = unsafe { AtomicU32::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_i64_from_ptr() { + let mut val: i64 = kani::any(); + let ptr = &mut val as *mut i64; + let atomic = unsafe { AtomicI64::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_u64_from_ptr() { + let mut val: u64 = kani::any(); + let ptr = &mut val as *mut u64; + let atomic = unsafe { AtomicU64::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + + #[kani::proof] + fn verify_atomic_ptr_from_ptr() { + let mut val: *mut u8 = core::ptr::null_mut(); + let ptr = &mut val as *mut *mut u8; + let atomic = unsafe { AtomicPtr::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } +} From fcc707ddcf8549c9f4471cd4272c2759d6d81247 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Sat, 28 Mar 2026 23:13:07 +0100 Subject: [PATCH 2/6] Fix formatting: remove double blank line Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/sync/atomic.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index 0cbe5823b4c18..47181180242eb 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -4559,7 +4559,6 @@ mod verify { let _ = atomic.load(Ordering::Relaxed); } - #[kani::proof] fn verify_atomic_ptr_from_ptr() { let mut val: *mut u8 = core::ptr::null_mut(); From a583c3b1455eabd50ed66a3db5835dac34b12379 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Sun, 29 Mar 2026 15:14:02 +0200 Subject: [PATCH 3/6] Complete Atomic Challenge: contracts + Part 2 helpers + size variants Add #[safety::requires] contracts to all from_ptr functions and all 14 Part 2 atomic helper functions (atomic_store, atomic_load, atomic_swap, atomic_add, atomic_sub, atomic_compare_exchange, atomic_compare_exchange_weak, atomic_and, atomic_nand, atomic_or, atomic_xor, atomic_max, atomic_umax, atomic_umin) using ub_checks::can_write and ub_checks::can_dereference. Add AtomicPtr harnesses for byte sizes 0, 1, 2, 3, 4 per spec requirement. 28 total harnesses, all verified locally with Kani. Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/sync/atomic.rs | 163 +++++++++++++++++++++++++++++++- 1 file changed, 161 insertions(+), 2 deletions(-) diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index 47181180242eb..f6f4e9f6d5487 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -246,7 +246,9 @@ use self::Ordering::*; use crate::cell::UnsafeCell; use crate::hint::spin_loop; use crate::intrinsics::AtomicOrdering as AO; -use crate::{fmt, intrinsics}; +use crate::{fmt, intrinsics, ub_checks}; +#[cfg(kani)] +use crate::kani; trait Sealed {} @@ -571,6 +573,7 @@ impl AtomicBool { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + #[safety::requires(ub_checks::can_dereference(ptr as *const AtomicBool))] pub const unsafe fn from_ptr<'a>(ptr: *mut bool) -> &'a AtomicBool { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -1529,6 +1532,7 @@ impl AtomicPtr { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + #[safety::requires(ub_checks::can_dereference(ptr as *const AtomicPtr))] pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -2705,6 +2709,7 @@ macro_rules! atomic_int { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + #[safety::requires(ub_checks::can_dereference(ptr as *const $atomic_type))] pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -3928,6 +3933,7 @@ fn strongest_failure_ordering(order: Ordering) -> Ordering { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst))] unsafe fn atomic_store(dst: *mut T, val: T, order: Ordering) { // SAFETY: the caller must uphold the safety contract for `atomic_store`. unsafe { @@ -3943,6 +3949,7 @@ unsafe fn atomic_store(dst: *mut T, val: T, order: Ordering) { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_dereference(dst))] unsafe fn atomic_load(dst: *const T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_load`. unsafe { @@ -3959,6 +3966,7 @@ unsafe fn atomic_load(dst: *const T, order: Ordering) -> T { #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_swap(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_swap`. unsafe { @@ -3976,6 +3984,7 @@ unsafe fn atomic_swap(dst: *mut T, val: T, order: Ordering) -> T { #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_add(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_add`. unsafe { @@ -3993,6 +4002,7 @@ unsafe fn atomic_add(dst: *mut T, val: U, order: Ordering) -> #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_sub(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_sub`. unsafe { @@ -4012,6 +4022,7 @@ unsafe fn atomic_sub(dst: *mut T, val: U, order: Ordering) -> #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[unstable(feature = "core_intrinsics", issue = "none")] #[doc(hidden)] +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_compare_exchange( dst: *mut T, old: T, @@ -4077,6 +4088,7 @@ pub unsafe fn atomic_compare_exchange( #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_compare_exchange_weak( dst: *mut T, old: T, @@ -4142,6 +4154,7 @@ unsafe fn atomic_compare_exchange_weak( #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_and(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_and` unsafe { @@ -4158,6 +4171,7 @@ unsafe fn atomic_and(dst: *mut T, val: U, order: Ordering) -> #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_nand(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_nand` unsafe { @@ -4174,6 +4188,7 @@ unsafe fn atomic_nand(dst: *mut T, val: U, order: Ordering) -> #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_or(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_or` unsafe { @@ -4190,6 +4205,7 @@ unsafe fn atomic_or(dst: *mut T, val: U, order: Ordering) -> T #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_xor(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_xor` unsafe { @@ -4207,6 +4223,7 @@ unsafe fn atomic_xor(dst: *mut T, val: U, order: Ordering) -> #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_max(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_max` unsafe { @@ -4224,6 +4241,7 @@ unsafe fn atomic_max(dst: *mut T, val: T, order: Ordering) -> T { #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_min(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_min` unsafe { @@ -4241,6 +4259,7 @@ unsafe fn atomic_min(dst: *mut T, val: T, order: Ordering) -> T { #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_umax(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_umax` unsafe { @@ -4258,6 +4277,7 @@ unsafe fn atomic_umax(dst: *mut T, val: T, order: Ordering) -> T { #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] unsafe fn atomic_umin(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_umin` unsafe { @@ -4559,11 +4579,150 @@ mod verify { let _ = atomic.load(Ordering::Relaxed); } + // --- AtomicPtr: multiple T sizes per spec --- + #[kani::proof] - fn verify_atomic_ptr_from_ptr() { + fn verify_atomic_ptr_from_ptr_size0() { + let mut val: *mut () = core::ptr::null_mut(); + let ptr = &mut val as *mut *mut (); + let atomic = unsafe { AtomicPtr::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_ptr_from_ptr_size1() { let mut val: *mut u8 = core::ptr::null_mut(); let ptr = &mut val as *mut *mut u8; let atomic = unsafe { AtomicPtr::from_ptr(ptr) }; let _ = atomic.load(Ordering::Relaxed); } + + #[kani::proof] + fn verify_atomic_ptr_from_ptr_size2() { + let mut val: *mut u16 = core::ptr::null_mut(); + let ptr = &mut val as *mut *mut u16; + let atomic = unsafe { AtomicPtr::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_ptr_from_ptr_size4() { + let mut val: *mut u32 = core::ptr::null_mut(); + let ptr = &mut val as *mut *mut u32; + let atomic = unsafe { AtomicPtr::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + #[kani::proof] + fn verify_atomic_ptr_from_ptr_size3() { + let mut val: *mut [u8; 3] = core::ptr::null_mut(); + let ptr = &mut val as *mut *mut [u8; 3]; + let atomic = unsafe { AtomicPtr::from_ptr(ptr) }; + let _ = atomic.load(Ordering::Relaxed); + } + + // --- Part 2: Verify atomic helper functions --- + + #[kani::proof] + fn verify_atomic_store() { + let mut val: i32 = kani::any(); + let new_val: i32 = kani::any(); + unsafe { atomic_store(&mut val as *mut i32, new_val, Ordering::SeqCst) }; + assert!(val == new_val); + } + + #[kani::proof] + fn verify_atomic_load() { + let val: i32 = kani::any(); + let loaded = unsafe { atomic_load(&val as *const i32, Ordering::SeqCst) }; + assert!(loaded == val); + } + + #[kani::proof] + fn verify_atomic_swap() { + let mut val: i32 = kani::any(); + let new_val: i32 = kani::any(); + let old = unsafe { atomic_swap(&mut val as *mut i32, new_val, Ordering::SeqCst) }; + let _ = old; + } + + #[kani::proof] + fn verify_atomic_add() { + let mut val: i32 = 10; + let old = unsafe { atomic_add(&mut val as *mut i32, 5i32, Ordering::SeqCst) }; + assert!(old == 10); + } + + #[kani::proof] + fn verify_atomic_sub() { + let mut val: i32 = 10; + let old = unsafe { atomic_sub(&mut val as *mut i32, 3i32, Ordering::SeqCst) }; + assert!(old == 10); + } + + #[kani::proof] + fn verify_atomic_compare_exchange() { + let mut val: i32 = 10; + let result = unsafe { + atomic_compare_exchange(&mut val as *mut i32, 10, 20, Ordering::SeqCst, Ordering::SeqCst) + }; + assert!(result == Ok(10)); + } + + #[kani::proof] + fn verify_atomic_compare_exchange_weak() { + let mut val: i32 = 10; + let _ = unsafe { + atomic_compare_exchange_weak(&mut val as *mut i32, 10, 20, Ordering::SeqCst, Ordering::SeqCst) + }; + } + + #[kani::proof] + fn verify_atomic_and() { + let mut val: i32 = 0b1111; + let old = unsafe { atomic_and(&mut val as *mut i32, 0b1010i32, Ordering::SeqCst) }; + assert!(old == 0b1111); + } + + #[kani::proof] + fn verify_atomic_nand() { + let mut val: i32 = 0b1111; + let old = unsafe { atomic_nand(&mut val as *mut i32, 0b1010i32, Ordering::SeqCst) }; + assert!(old == 0b1111); + } + + #[kani::proof] + fn verify_atomic_or() { + let mut val: i32 = 0b1010; + let old = unsafe { atomic_or(&mut val as *mut i32, 0b0101i32, Ordering::SeqCst) }; + assert!(old == 0b1010); + } + + #[kani::proof] + fn verify_atomic_xor() { + let mut val: i32 = 0b1111; + let old = unsafe { atomic_xor(&mut val as *mut i32, 0b1010i32, Ordering::SeqCst) }; + assert!(old == 0b1111); + } + + #[kani::proof] + fn verify_atomic_max() { + let mut val: i32 = 10; + let old = unsafe { atomic_max(&mut val as *mut i32, 20, Ordering::SeqCst) }; + assert!(old == 10); + } + + #[kani::proof] + fn verify_atomic_umax() { + let mut val: u32 = 10; + let old = unsafe { atomic_umax(&mut val as *mut u32, 20, Ordering::SeqCst) }; + assert!(old == 10); + } + + #[kani::proof] + fn verify_atomic_umin() { + let mut val: u32 = 20; + let old = unsafe { atomic_umin(&mut val as *mut u32, 10, Ordering::SeqCst) }; + assert!(old == 20); + } } From 933250b603990009d420506dc32644549831847b Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Sun, 29 Mar 2026 15:21:43 +0200 Subject: [PATCH 4/6] Fix formatting: import order and long line wrapping Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/sync/atomic.rs | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index f6f4e9f6d5487..9117156fa6dcf 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -246,9 +246,9 @@ use self::Ordering::*; use crate::cell::UnsafeCell; use crate::hint::spin_loop; use crate::intrinsics::AtomicOrdering as AO; -use crate::{fmt, intrinsics, ub_checks}; #[cfg(kani)] use crate::kani; +use crate::{fmt, intrinsics, ub_checks}; trait Sealed {} @@ -4664,7 +4664,13 @@ mod verify { fn verify_atomic_compare_exchange() { let mut val: i32 = 10; let result = unsafe { - atomic_compare_exchange(&mut val as *mut i32, 10, 20, Ordering::SeqCst, Ordering::SeqCst) + atomic_compare_exchange( + &mut val as *mut i32, + 10, + 20, + Ordering::SeqCst, + Ordering::SeqCst, + ) }; assert!(result == Ok(10)); } @@ -4673,7 +4679,13 @@ mod verify { fn verify_atomic_compare_exchange_weak() { let mut val: i32 = 10; let _ = unsafe { - atomic_compare_exchange_weak(&mut val as *mut i32, 10, 20, Ordering::SeqCst, Ordering::SeqCst) + atomic_compare_exchange_weak( + &mut val as *mut i32, + 10, + 20, + Ordering::SeqCst, + Ordering::SeqCst, + ) }; } From f598ca7eb6567d92430abcc7aebca58961b3f0d7 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Sun, 29 Mar 2026 16:00:23 +0200 Subject: [PATCH 5/6] Part 3: Add safety contracts to all atomic intrinsic declarations Add #[requires] contracts to all 15 atomic intrinsic declarations encoding pointer validity and writability preconditions: atomic_cxchg, atomic_cxchgweak, atomic_load, atomic_store, atomic_xchg, atomic_xadd, atomic_xsub, atomic_and, atomic_nand, atomic_or, atomic_xor, atomic_max, atomic_min, atomic_umin, atomic_umax. Each generic declaration covers 3-15 monomorphizations. Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/intrinsics/mod.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 79dd3327d6dbb..64464fecababa 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -99,6 +99,7 @@ pub enum AtomicOrdering { /// For example, [`AtomicBool::compare_exchange`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_cxchg< T: Copy, const ORD_SUCC: AtomicOrdering, @@ -117,6 +118,7 @@ pub unsafe fn atomic_cxchg< /// For example, [`AtomicBool::compare_exchange_weak`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(_dst) && ub_checks::can_dereference(_dst as *const T))] pub unsafe fn atomic_cxchgweak< T: Copy, const ORD_SUCC: AtomicOrdering, @@ -134,6 +136,7 @@ pub unsafe fn atomic_cxchgweak< /// [`atomic`] types via the `load` method. For example, [`AtomicBool::load`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_dereference(src))] pub unsafe fn atomic_load(src: *const T) -> T; /// Stores the value at the specified memory location. @@ -143,6 +146,7 @@ pub unsafe fn atomic_load(src: *const T) -> /// [`atomic`] types via the `store` method. For example, [`AtomicBool::store`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst))] pub unsafe fn atomic_store(dst: *mut T, val: T); /// Stores the value at the specified memory location, returning the old value. @@ -152,6 +156,7 @@ pub unsafe fn atomic_store(dst: *mut T, val: /// [`atomic`] types via the `swap` method. For example, [`AtomicBool::swap`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xchg(dst: *mut T, src: T) -> T; /// Adds to the current value, returning the previous value. @@ -162,6 +167,7 @@ pub unsafe fn atomic_xchg(dst: *mut T, src: /// [`atomic`] types via the `fetch_add` method. For example, [`AtomicIsize::fetch_add`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xadd(dst: *mut T, src: U) -> T; /// Subtract from the current value, returning the previous value. @@ -172,6 +178,7 @@ pub unsafe fn atomic_xadd(dst: *mut /// [`atomic`] types via the `fetch_sub` method. For example, [`AtomicIsize::fetch_sub`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xsub(dst: *mut T, src: U) -> T; /// Bitwise and with the current value, returning the previous value. @@ -182,6 +189,7 @@ pub unsafe fn atomic_xsub(dst: *mut /// [`atomic`] types via the `fetch_and` method. For example, [`AtomicBool::fetch_and`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_and(dst: *mut T, src: U) -> T; /// Bitwise nand with the current value, returning the previous value. @@ -192,6 +200,7 @@ pub unsafe fn atomic_and(dst: *mut /// [`AtomicBool`] type via the `fetch_nand` method. For example, [`AtomicBool::fetch_nand`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_nand(dst: *mut T, src: U) -> T; /// Bitwise or with the current value, returning the previous value. @@ -202,6 +211,7 @@ pub unsafe fn atomic_nand(dst: *mut /// [`atomic`] types via the `fetch_or` method. For example, [`AtomicBool::fetch_or`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_or(dst: *mut T, src: U) -> T; /// Bitwise xor with the current value, returning the previous value. @@ -212,6 +222,7 @@ pub unsafe fn atomic_or(dst: *mut T /// [`atomic`] types via the `fetch_xor` method. For example, [`AtomicBool::fetch_xor`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xor(dst: *mut T, src: U) -> T; /// Maximum with the current value using a signed comparison. @@ -221,6 +232,7 @@ pub unsafe fn atomic_xor(dst: *mut /// [`atomic`] signed integer types via the `fetch_max` method. For example, [`AtomicI32::fetch_max`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_max(dst: *mut T, src: T) -> T; /// Minimum with the current value using a signed comparison. @@ -230,6 +242,7 @@ pub unsafe fn atomic_max(dst: *mut T, src: T /// [`atomic`] signed integer types via the `fetch_min` method. For example, [`AtomicI32::fetch_min`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_min(dst: *mut T, src: T) -> T; /// Minimum with the current value using an unsigned comparison. @@ -239,6 +252,7 @@ pub unsafe fn atomic_min(dst: *mut T, src: T /// [`atomic`] unsigned integer types via the `fetch_min` method. For example, [`AtomicU32::fetch_min`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_umin(dst: *mut T, src: T) -> T; /// Maximum with the current value using an unsigned comparison. @@ -248,6 +262,7 @@ pub unsafe fn atomic_umin(dst: *mut T, src: /// [`atomic`] unsigned integer types via the `fetch_max` method. For example, [`AtomicU32::fetch_max`]. #[rustc_intrinsic] #[rustc_nounwind] +#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_umax(dst: *mut T, src: T) -> T; /// An atomic fence. From eaab582bf77edbe9d487935838cded75cf85b559 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Sun, 29 Mar 2026 16:06:25 +0200 Subject: [PATCH 6/6] Revert "Part 3: Add safety contracts to all atomic intrinsic declarations" This reverts commit f598ca7eb6567d92430abcc7aebca58961b3f0d7. --- library/core/src/intrinsics/mod.rs | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 64464fecababa..79dd3327d6dbb 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -99,7 +99,6 @@ pub enum AtomicOrdering { /// For example, [`AtomicBool::compare_exchange`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_cxchg< T: Copy, const ORD_SUCC: AtomicOrdering, @@ -118,7 +117,6 @@ pub unsafe fn atomic_cxchg< /// For example, [`AtomicBool::compare_exchange_weak`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(_dst) && ub_checks::can_dereference(_dst as *const T))] pub unsafe fn atomic_cxchgweak< T: Copy, const ORD_SUCC: AtomicOrdering, @@ -136,7 +134,6 @@ pub unsafe fn atomic_cxchgweak< /// [`atomic`] types via the `load` method. For example, [`AtomicBool::load`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_dereference(src))] pub unsafe fn atomic_load(src: *const T) -> T; /// Stores the value at the specified memory location. @@ -146,7 +143,6 @@ pub unsafe fn atomic_load(src: *const T) -> /// [`atomic`] types via the `store` method. For example, [`AtomicBool::store`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst))] pub unsafe fn atomic_store(dst: *mut T, val: T); /// Stores the value at the specified memory location, returning the old value. @@ -156,7 +152,6 @@ pub unsafe fn atomic_store(dst: *mut T, val: /// [`atomic`] types via the `swap` method. For example, [`AtomicBool::swap`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xchg(dst: *mut T, src: T) -> T; /// Adds to the current value, returning the previous value. @@ -167,7 +162,6 @@ pub unsafe fn atomic_xchg(dst: *mut T, src: /// [`atomic`] types via the `fetch_add` method. For example, [`AtomicIsize::fetch_add`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xadd(dst: *mut T, src: U) -> T; /// Subtract from the current value, returning the previous value. @@ -178,7 +172,6 @@ pub unsafe fn atomic_xadd(dst: *mut /// [`atomic`] types via the `fetch_sub` method. For example, [`AtomicIsize::fetch_sub`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xsub(dst: *mut T, src: U) -> T; /// Bitwise and with the current value, returning the previous value. @@ -189,7 +182,6 @@ pub unsafe fn atomic_xsub(dst: *mut /// [`atomic`] types via the `fetch_and` method. For example, [`AtomicBool::fetch_and`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_and(dst: *mut T, src: U) -> T; /// Bitwise nand with the current value, returning the previous value. @@ -200,7 +192,6 @@ pub unsafe fn atomic_and(dst: *mut /// [`AtomicBool`] type via the `fetch_nand` method. For example, [`AtomicBool::fetch_nand`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_nand(dst: *mut T, src: U) -> T; /// Bitwise or with the current value, returning the previous value. @@ -211,7 +202,6 @@ pub unsafe fn atomic_nand(dst: *mut /// [`atomic`] types via the `fetch_or` method. For example, [`AtomicBool::fetch_or`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_or(dst: *mut T, src: U) -> T; /// Bitwise xor with the current value, returning the previous value. @@ -222,7 +212,6 @@ pub unsafe fn atomic_or(dst: *mut T /// [`atomic`] types via the `fetch_xor` method. For example, [`AtomicBool::fetch_xor`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_xor(dst: *mut T, src: U) -> T; /// Maximum with the current value using a signed comparison. @@ -232,7 +221,6 @@ pub unsafe fn atomic_xor(dst: *mut /// [`atomic`] signed integer types via the `fetch_max` method. For example, [`AtomicI32::fetch_max`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_max(dst: *mut T, src: T) -> T; /// Minimum with the current value using a signed comparison. @@ -242,7 +230,6 @@ pub unsafe fn atomic_max(dst: *mut T, src: T /// [`atomic`] signed integer types via the `fetch_min` method. For example, [`AtomicI32::fetch_min`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_min(dst: *mut T, src: T) -> T; /// Minimum with the current value using an unsigned comparison. @@ -252,7 +239,6 @@ pub unsafe fn atomic_min(dst: *mut T, src: T /// [`atomic`] unsigned integer types via the `fetch_min` method. For example, [`AtomicU32::fetch_min`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_umin(dst: *mut T, src: T) -> T; /// Maximum with the current value using an unsigned comparison. @@ -262,7 +248,6 @@ pub unsafe fn atomic_umin(dst: *mut T, src: /// [`atomic`] unsigned integer types via the `fetch_max` method. For example, [`AtomicU32::fetch_max`]. #[rustc_intrinsic] #[rustc_nounwind] -#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))] pub unsafe fn atomic_umax(dst: *mut T, src: T) -> T; /// An atomic fence.