From 04cdbed53464d24969ede79ad61306546e40f9d7 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 17:35:57 +0530 Subject: [PATCH 1/3] Challenge 7: Kani contracts for atomic types and intrinsics Kani contracts and harnesses for verify-rust-std challenge. Fixes #83 --- library/core/src/intrinsics/mod.rs | 698 +++++++++++++++++++++++++++- library/core/src/intrinsics/simd.rs | 2 +- library/core/src/sync/atomic.rs | 389 +++++++++++++++- 3 files changed, 1061 insertions(+), 28 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index ddadeeb3c786a..9def017ec0c14 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -71,7 +71,11 @@ pub mod simd; // These imports are used for simplifying intra-doc links #[allow(unused_imports)] -#[cfg(all(target_has_atomic = "8", target_has_atomic = "32", target_has_atomic = "ptr"))] +#[cfg(all( + target_has_atomic = "8", + target_has_atomic = "32", + target_has_atomic = "ptr" +))] use crate::sync::atomic::{self, AtomicBool, AtomicI32, AtomicIsize, AtomicU32, Ordering}; /// A type for atomic ordering parameters for intrinsics. This is a separate type from @@ -492,7 +496,11 @@ pub const fn select_unpredictable(b: bool, true_val: T, false_val: T) -> T where T: [const] Destruct, { - if b { true_val } else { false_val } + if b { + true_val + } else { + false_val + } } /// A guard for unsafe functions that cannot ever be executed if `T` is uninhabited: @@ -3096,7 +3104,11 @@ pub const fn minimumf16(x: f16, y: f16) -> f16 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { x } else { y } + if x.is_sign_negative() && y.is_sign_positive() { + x + } else { + y + } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3117,7 +3129,11 @@ pub const fn minimumf32(x: f32, y: f32) -> f32 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { x } else { y } + if x.is_sign_negative() && y.is_sign_positive() { + x + } else { + y + } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3138,7 +3154,11 @@ pub const fn minimumf64(x: f64, y: f64) -> f64 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { x } else { y } + if x.is_sign_negative() && y.is_sign_positive() { + x + } else { + y + } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3159,7 +3179,11 @@ pub const fn minimumf128(x: f128, y: f128) -> f128 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { x } else { y } + if x.is_sign_negative() && y.is_sign_positive() { + x + } else { + y + } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3234,7 +3258,11 @@ pub const fn maximumf16(x: f16, y: f16) -> f16 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { x } else { y } + if x.is_sign_positive() && y.is_sign_negative() { + x + } else { + y + } } else { x + y } @@ -3254,7 +3282,11 @@ pub const fn maximumf32(x: f32, y: f32) -> f32 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { x } else { y } + if x.is_sign_positive() && y.is_sign_negative() { + x + } else { + y + } } else { x + y } @@ -3274,7 +3306,11 @@ pub const fn maximumf64(x: f64, y: f64) -> f64 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { x } else { y } + if x.is_sign_positive() && y.is_sign_negative() { + x + } else { + y + } } else { x + y } @@ -3294,7 +3330,11 @@ pub const fn maximumf128(x: f128, y: f128) -> f128 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { x } else { y } + if x.is_sign_positive() && y.is_sign_negative() { + x + } else { + y + } } else { x + y } @@ -3799,7 +3839,9 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); + kani::assume(ub_checks::can_dereference( + &src as *const $src as *const $dst, + )); let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; assert_eq!(src, src2); @@ -3815,7 +3857,9 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); + kani::assume(ub_checks::can_dereference( + &src as *const $src as *const $dst, + )); let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; if src.is_nan() { @@ -3871,7 +3915,10 @@ mod verify { let mut generator = PointerGenerator::<10000>::new(); let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ptr_2: *const u8 = unsafe { transmute_unchecked(arb_ptr) }; - assert_eq!(arb_ptr as *const bool, arb_ptr_2 as *const u8 as *const bool); + assert_eq!( + arb_ptr as *const bool, + arb_ptr_2 as *const u8 as *const bool + ); } //Tests that transmuting (unchecked) a ref does not mutate the stored address @@ -3881,7 +3928,10 @@ mod verify { let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ref: &bool = unsafe { &*(arb_ptr) }; let arb_ref_2: &u8 = unsafe { transmute_unchecked(arb_ref) }; - assert_eq!(arb_ref as *const bool, arb_ref_2 as *const u8 as *const bool); + assert_eq!( + arb_ref as *const bool, + arb_ref_2 as *const u8 as *const bool + ); } //Tests that transmuting (unchecked) a slice does not mutate the slice metadata (address and length) @@ -3907,7 +3957,9 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); + kani::assume(ub_checks::can_dereference( + &src as *const $src as *const $dst, + )); let dst: $dst = unsafe { transmute(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; assert_eq!(src, src2); @@ -3923,7 +3975,9 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); + kani::assume(ub_checks::can_dereference( + &src as *const $src as *const $dst, + )); let dst: $dst = unsafe { transmute(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; if src.is_nan() { @@ -3979,7 +4033,10 @@ mod verify { let mut generator = PointerGenerator::<10000>::new(); let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ptr_2: *const u8 = unsafe { transmute(arb_ptr) }; - assert_eq!(arb_ptr as *const bool, arb_ptr_2 as *const u8 as *const bool); + assert_eq!( + arb_ptr as *const bool, + arb_ptr_2 as *const u8 as *const bool + ); } //Tests that transmuting a ref does not mutate the stored address @@ -3989,7 +4046,10 @@ mod verify { let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ref: &bool = unsafe { &*(arb_ptr) }; let arb_ref_2: &u8 = unsafe { transmute(arb_ref) }; - assert_eq!(arb_ref as *const bool, arb_ref_2 as *const u8 as *const bool); + assert_eq!( + arb_ref as *const bool, + arb_ref_2 as *const u8 as *const bool + ); } //Tests that transmuting a slice does not mutate the slice metadata (address and length) @@ -4131,9 +4191,16 @@ mod verify { fn run_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { let mut generator1 = PointerGenerator::<100>::new(); let mut generator2 = PointerGenerator::<100>::new(); - let ArbitraryPointer { ptr: src, status: src_status, .. } = - generator1.any_alloc_status::(); - let ArbitraryPointer { ptr: dst, status: dst_status, .. } = if kani::any() { + let ArbitraryPointer { + ptr: src, + status: src_status, + .. + } = generator1.any_alloc_status::(); + let ArbitraryPointer { + ptr: dst, + status: dst_status, + .. + } = if kani::any() { generator1.any_alloc_status::() } else { generator2.any_alloc_status::() @@ -4150,4 +4217,593 @@ mod verify { fn supported_status(status: AllocationStatus) -> bool { status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject } + + // --- Challenge 7 Part 3: atomic intrinsic contracts --- + // + // `rustc_intrinsic` declarations have no body, so Kani cannot attach + // contracts to them (model-checking/kani#3345). These wrappers encode the + // documented pointer preconditions and invoke the const-generic intrinsics + // that replaced the older `atomic_*_{relaxed,acquire,...}` names. + + fn atomic_ptr_at_offset(buf: &mut [u8; 64]) -> *mut T { + let offset = kani::any_where(|o: &usize| *o < 64); + buf.as_mut_ptr().wrapping_add(offset).cast::() + } + + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_store_wrapper(dst: *mut T, val: T) { + // SAFETY: `requires` guarantees `dst` is aligned and writable. + unsafe { atomic_store::(dst, val) } + } + + #[requires(ub_checks::can_dereference(src))] + unsafe fn atomic_load_wrapper(src: *const T) -> T { + // SAFETY: `requires` guarantees `src` is aligned, allocated, and initialized. + unsafe { atomic_load::(src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_xchg_wrapper(dst: *mut T, src: T) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_xchg::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_xadd_wrapper( + dst: *mut T, + src: U, + ) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_xadd::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_xsub_wrapper( + dst: *mut T, + src: U, + ) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_xsub::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_and_wrapper( + dst: *mut T, + src: U, + ) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_and::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_nand_wrapper( + dst: *mut T, + src: U, + ) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_nand::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_or_wrapper( + dst: *mut T, + src: U, + ) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_or::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_xor_wrapper( + dst: *mut T, + src: U, + ) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_xor::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_max_wrapper(dst: *mut T, src: T) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_max::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_min_wrapper(dst: *mut T, src: T) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_min::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_umax_wrapper(dst: *mut T, src: T) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_umax::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_umin_wrapper(dst: *mut T, src: T) -> T { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_umin::(dst, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_cxchg_wrapper< + T: Copy, + const ORD_SUCC: AtomicOrdering, + const ORD_FAIL: AtomicOrdering, + >( + dst: *mut T, + old: T, + src: T, + ) -> (T, bool) { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_cxchg::(dst, old, src) } + } + + #[requires(ub_checks::can_dereference(dst as *const T))] + #[requires(ub_checks::can_write(dst))] + unsafe fn atomic_cxchgweak_wrapper< + T: Copy, + const ORD_SUCC: AtomicOrdering, + const ORD_FAIL: AtomicOrdering, + >( + dst: *mut T, + old: T, + src: T, + ) -> (T, bool) { + // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write. + unsafe { atomic_cxchgweak::(dst, old, src) } + } + + macro_rules! proof_atomic_store_ord { + ($name:ident, $ord:ident) => { + #[kani::proof_for_contract(atomic_store_wrapper)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = atomic_ptr_at_offset::(&mut buf); + unsafe { + atomic_store_wrapper::(ptr, kani::any()); + } + } + }; + } + + proof_atomic_store_ord!(check_atomic_store_relaxed, Relaxed); + proof_atomic_store_ord!(check_atomic_store_release, Release); + proof_atomic_store_ord!(check_atomic_store_seqcst, SeqCst); + + macro_rules! proof_atomic_load_ord { + ($name:ident, $ord:ident) => { + #[kani::proof_for_contract(atomic_load_wrapper)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = atomic_ptr_at_offset::(&mut buf); + unsafe { + let _ = atomic_load_wrapper::(ptr as *const u8); + } + } + }; + } + + proof_atomic_load_ord!(check_atomic_load_relaxed, Relaxed); + proof_atomic_load_ord!(check_atomic_load_acquire, Acquire); + proof_atomic_load_ord!(check_atomic_load_seqcst, SeqCst); + + macro_rules! proof_atomic_rmw_u8 { + ($wrapper:ident, $name:ident, $ord:ident) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = atomic_ptr_at_offset::(&mut buf); + unsafe { + let _ = $wrapper::(ptr, kani::any()); + } + } + }; + ($wrapper:ident, $name:ident, $ord:ident, two_ty) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = atomic_ptr_at_offset::(&mut buf); + unsafe { + let _ = $wrapper::(ptr, kani::any()); + } + } + }; + } + + proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_relaxed, Relaxed); + proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_acquire, Acquire); + proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_release, Release); + proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_acqrel, AcqRel); + proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_seqcst, SeqCst); + + proof_atomic_rmw_u8!( + atomic_xadd_wrapper, + check_atomic_xadd_relaxed, + Relaxed, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xadd_wrapper, + check_atomic_xadd_acquire, + Acquire, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xadd_wrapper, + check_atomic_xadd_release, + Release, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xadd_wrapper, + check_atomic_xadd_acqrel, + AcqRel, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xadd_wrapper, + check_atomic_xadd_seqcst, + SeqCst, + two_ty + ); + + proof_atomic_rmw_u8!( + atomic_xsub_wrapper, + check_atomic_xsub_relaxed, + Relaxed, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xsub_wrapper, + check_atomic_xsub_acquire, + Acquire, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xsub_wrapper, + check_atomic_xsub_release, + Release, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xsub_wrapper, + check_atomic_xsub_acqrel, + AcqRel, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xsub_wrapper, + check_atomic_xsub_seqcst, + SeqCst, + two_ty + ); + + proof_atomic_rmw_u8!( + atomic_and_wrapper, + check_atomic_and_relaxed, + Relaxed, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_and_wrapper, + check_atomic_and_acquire, + Acquire, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_and_wrapper, + check_atomic_and_release, + Release, + two_ty + ); + proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_acqrel, AcqRel, two_ty); + proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_seqcst, SeqCst, two_ty); + + proof_atomic_rmw_u8!( + atomic_nand_wrapper, + check_atomic_nand_relaxed, + Relaxed, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_nand_wrapper, + check_atomic_nand_acquire, + Acquire, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_nand_wrapper, + check_atomic_nand_release, + Release, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_nand_wrapper, + check_atomic_nand_acqrel, + AcqRel, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_nand_wrapper, + check_atomic_nand_seqcst, + SeqCst, + two_ty + ); + + proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_relaxed, Relaxed, two_ty); + proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_acquire, Acquire, two_ty); + proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_release, Release, two_ty); + proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_acqrel, AcqRel, two_ty); + proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_seqcst, SeqCst, two_ty); + + proof_atomic_rmw_u8!( + atomic_xor_wrapper, + check_atomic_xor_relaxed, + Relaxed, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xor_wrapper, + check_atomic_xor_acquire, + Acquire, + two_ty + ); + proof_atomic_rmw_u8!( + atomic_xor_wrapper, + check_atomic_xor_release, + Release, + two_ty + ); + proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_acqrel, AcqRel, two_ty); + proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_seqcst, SeqCst, two_ty); + + macro_rules! proof_atomic_minmax_ord { + ($wrapper:ident, $name:ident, $ty:ty, $ord:ident) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = atomic_ptr_at_offset::<$ty>(&mut buf); + unsafe { + let _ = $wrapper::<$ty, { AtomicOrdering::$ord }>(ptr, kani::any()); + } + } + }; + } + + proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_relaxed, i8, Relaxed); + proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_acquire, i8, Acquire); + proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_release, i8, Release); + proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_acqrel, i8, AcqRel); + proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_seqcst, i8, SeqCst); + + proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_relaxed, i8, Relaxed); + proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_acquire, i8, Acquire); + proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_release, i8, Release); + proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_acqrel, i8, AcqRel); + proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_seqcst, i8, SeqCst); + + proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_relaxed, u8, Relaxed); + proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_acquire, u8, Acquire); + proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_release, u8, Release); + proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_acqrel, u8, AcqRel); + proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_seqcst, u8, SeqCst); + + proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_relaxed, u8, Relaxed); + proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_acquire, u8, Acquire); + proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_release, u8, Release); + proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_acqrel, u8, AcqRel); + proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_seqcst, u8, SeqCst); + + macro_rules! proof_atomic_cxchg_ord { + ($wrapper:ident, $name:ident, $succ:ident, $fail:ident) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = atomic_ptr_at_offset::(&mut buf); + unsafe { + let _ = $wrapper::( + ptr, + kani::any(), + kani::any(), + ); + } + } + }; + } + + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_relaxed_relaxed, + Relaxed, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_relaxed_acquire, + Relaxed, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_relaxed_seqcst, + Relaxed, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_acquire_relaxed, + Acquire, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_acquire_acquire, + Acquire, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_acquire_seqcst, + Acquire, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_release_relaxed, + Release, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_release_acquire, + Release, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_release_seqcst, + Release, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_acqrel_relaxed, + AcqRel, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_acqrel_acquire, + AcqRel, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_acqrel_seqcst, + AcqRel, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_seqcst_relaxed, + SeqCst, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_seqcst_acquire, + SeqCst, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchg_wrapper, + check_atomic_cxchg_seqcst_seqcst, + SeqCst, + SeqCst + ); + + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_relaxed_relaxed, + Relaxed, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_relaxed_acquire, + Relaxed, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_relaxed_seqcst, + Relaxed, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_acquire_relaxed, + Acquire, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_acquire_acquire, + Acquire, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_acquire_seqcst, + Acquire, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_release_relaxed, + Release, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_release_acquire, + Release, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_release_seqcst, + Release, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_acqrel_relaxed, + AcqRel, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_acqrel_acquire, + AcqRel, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_acqrel_seqcst, + AcqRel, + SeqCst + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_seqcst_relaxed, + SeqCst, + Relaxed + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_seqcst_acquire, + SeqCst, + Acquire + ); + proof_atomic_cxchg_ord!( + atomic_cxchgweak_wrapper, + check_atomic_cxchgweak_seqcst_seqcst, + SeqCst, + SeqCst + ); } diff --git a/library/core/src/intrinsics/simd.rs b/library/core/src/intrinsics/simd.rs index 722a765cd01ee..10e69e7a0efa8 100644 --- a/library/core/src/intrinsics/simd.rs +++ b/library/core/src/intrinsics/simd.rs @@ -413,7 +413,7 @@ pub enum SimdAlign { #[rustc_intrinsic] #[rustc_nounwind] pub const unsafe fn simd_masked_load(mask: V, ptr: U, val: T) --> T; + -> T; /// Writes to a vector of pointers. /// diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index 0c5552a0b81cc..6c4f8c0df1537 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -242,10 +242,16 @@ // are just normal values that get loaded/stored, but not dereferenced. #![allow(clippy::not_unsafe_ptr_arg_deref)] +use safety::requires; + use self::Ordering::*; use crate::cell::UnsafeCell; use crate::hint::spin_loop; use crate::intrinsics::AtomicOrdering as AO; +#[cfg(kani)] +use crate::kani; +#[cfg(kani)] +use crate::ub_checks; use crate::{fmt, intrinsics}; trait Sealed {} @@ -526,7 +532,9 @@ impl AtomicBool { #[rustc_const_stable(feature = "const_atomic_new", since = "1.24.0")] #[must_use] pub const fn new(v: bool) -> AtomicBool { - AtomicBool { v: UnsafeCell::new(v as u8) } + AtomicBool { + v: UnsafeCell::new(v as u8), + } } /// Creates a new `AtomicBool` from a pointer. @@ -571,6 +579,9 @@ impl AtomicBool { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + // Cast to `AtomicBool` so the predicate uses this type's alignment (not `bool`'s). + #[requires(ub_checks::can_dereference(ptr as *const AtomicBool))] + #[requires(ub_checks::can_write(ptr as *mut AtomicBool))] pub const unsafe fn from_ptr<'a>(ptr: *mut bool) -> &'a AtomicBool { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -721,6 +732,7 @@ impl AtomicBool { #[inline] #[stable(feature = "rust1", since = "1.0.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(order == Relaxed || order == Acquire || order == SeqCst)] pub fn load(&self, order: Ordering) -> bool { // SAFETY: any data races are prevented by atomic intrinsics and the raw // pointer passed in is valid because we got it from a reference. @@ -750,6 +762,7 @@ impl AtomicBool { #[stable(feature = "rust1", since = "1.0.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(order == Relaxed || order == Release || order == SeqCst)] pub fn store(&self, val: bool, order: Ordering) { // SAFETY: any data races are prevented by atomic intrinsics and the raw // pointer passed in is valid because we got it from a reference. @@ -785,7 +798,11 @@ impl AtomicBool { #[rustc_should_not_be_called_on_const_items] pub fn swap(&self, val: bool, order: Ordering) -> bool { if EMULATE_ATOMIC_BOOL { - if val { self.fetch_or(true, order) } else { self.fetch_and(false, order) } + if val { + self.fetch_or(true, order) + } else { + self.fetch_and(false, order) + } } else { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_swap(self.v.get(), val as u8, order) != 0 } @@ -913,6 +930,7 @@ impl AtomicBool { #[cfg(target_has_atomic = "8")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange( &self, current: bool, @@ -944,7 +962,11 @@ impl AtomicBool { // This sets the value to the new one and returns the old one. self.swap(new, order) }; - if old == current { Ok(old) } else { Err(old) } + if old == current { + Ok(old) + } else { + Err(old) + } } else { // SAFETY: data races are prevented by atomic intrinsics. match unsafe { @@ -1009,6 +1031,7 @@ impl AtomicBool { #[cfg(target_has_atomic = "8")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange_weak( &self, current: bool, @@ -1498,7 +1521,9 @@ impl AtomicPtr { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_atomic_new", since = "1.24.0")] pub const fn new(p: *mut T) -> AtomicPtr { - AtomicPtr { p: UnsafeCell::new(p) } + AtomicPtr { + p: UnsafeCell::new(p), + } } /// Creates a new `AtomicPtr` from a pointer. @@ -1543,6 +1568,9 @@ impl AtomicPtr { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + // Cast to `AtomicPtr` so the predicate uses this type's alignment. + #[requires(ub_checks::can_dereference(ptr as *const AtomicPtr))] + #[requires(ub_checks::can_write(ptr as *mut AtomicPtr))] pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -1720,6 +1748,7 @@ impl AtomicPtr { #[inline] #[stable(feature = "rust1", since = "1.0.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(order == Relaxed || order == Acquire || order == SeqCst)] pub fn load(&self, order: Ordering) -> *mut T { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_load(self.p.get(), order) } @@ -1750,6 +1779,7 @@ impl AtomicPtr { #[stable(feature = "rust1", since = "1.0.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(order == Relaxed || order == Release || order == SeqCst)] pub fn store(&self, ptr: *mut T, order: Ordering) { // SAFETY: data races are prevented by atomic intrinsics. unsafe { @@ -1902,6 +1932,7 @@ impl AtomicPtr { #[cfg(target_has_atomic = "ptr")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange( &self, current: *mut T, @@ -1966,6 +1997,7 @@ impl AtomicPtr { #[cfg(target_has_atomic = "ptr")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange_weak( &self, current: *mut T, @@ -2738,6 +2770,10 @@ 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")] + // Cast to `$atomic_type` so alignment matches the atomic, which can + // be stricter than `$int_type` on some targets. + #[requires(ub_checks::can_dereference(ptr as *const $atomic_type))] + #[requires(ub_checks::can_write(ptr as *mut $atomic_type))] pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -2915,6 +2951,7 @@ macro_rules! atomic_int { #[inline] #[$stable] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(order == Relaxed || order == Acquire || order == SeqCst)] pub fn load(&self, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_load(self.v.get(), order) } @@ -2943,6 +2980,7 @@ macro_rules! atomic_int { #[$stable] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(order == Relaxed || order == Release || order == SeqCst)] pub fn store(&self, val: $int_type, order: Ordering) { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_store(self.v.get(), val, order); } @@ -3106,6 +3144,7 @@ macro_rules! atomic_int { #[$cfg_cas] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange(&self, current: $int_type, new: $int_type, @@ -3170,6 +3209,7 @@ macro_rules! atomic_int { #[$cfg_cas] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange_weak(&self, current: $int_type, new: $int_type, @@ -3985,6 +4025,8 @@ fn strongest_failure_ordering(order: Ordering) -> Ordering { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[requires(ub_checks::can_write(dst))] +#[requires(order == Relaxed || order == Release || order == SeqCst)] unsafe fn atomic_store(dst: *mut T, val: T, order: Ordering) { // SAFETY: the caller must uphold the safety contract for `atomic_store`. unsafe { @@ -4000,6 +4042,8 @@ 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 +#[requires(ub_checks::can_dereference(dst))] +#[requires(order == Relaxed || order == Acquire || order == SeqCst)] unsafe fn atomic_load(dst: *const T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_load`. unsafe { @@ -4016,6 +4060,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_swap(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_swap`. unsafe { @@ -4033,6 +4079,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_add(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_add`. unsafe { @@ -4050,6 +4098,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_sub(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_sub`. unsafe { @@ -4069,6 +4119,9 @@ 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)] +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] +#[requires(failure != Release && failure != AcqRel)] pub unsafe fn atomic_compare_exchange( dst: *mut T, old: T, @@ -4128,12 +4181,19 @@ pub unsafe fn atomic_compare_exchange( (_, Release) => panic!("there is no such thing as a release failure ordering"), } }; - if ok { Ok(val) } else { Err(val) } + if ok { + Ok(val) + } else { + Err(val) + } } #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] +#[requires(failure != Release && failure != AcqRel)] unsafe fn atomic_compare_exchange_weak( dst: *mut T, old: T, @@ -4193,12 +4253,18 @@ unsafe fn atomic_compare_exchange_weak( (_, Release) => panic!("there is no such thing as a release failure ordering"), } }; - if ok { Ok(val) } else { Err(val) } + if ok { + Ok(val) + } else { + Err(val) + } } #[inline] #[cfg(target_has_atomic)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_and(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_and` unsafe { @@ -4215,6 +4281,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_nand(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_nand` unsafe { @@ -4231,6 +4299,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_or(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_or` unsafe { @@ -4247,6 +4317,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_xor(dst: *mut T, val: U, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_xor` unsafe { @@ -4264,6 +4336,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_max(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_max` unsafe { @@ -4281,6 +4355,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_min(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_min` unsafe { @@ -4298,6 +4374,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_umax(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_umax` unsafe { @@ -4315,6 +4393,8 @@ 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 +#[requires(ub_checks::can_dereference(dst as *const T))] +#[requires(ub_checks::can_write(dst))] unsafe fn atomic_umin(dst: *mut T, val: T, order: Ordering) -> T { // SAFETY: the caller must uphold the safety contract for `atomic_umin` unsafe { @@ -4609,3 +4689,300 @@ 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; + + impl kani::Arbitrary for Ordering { + fn any() -> Self { + match kani::any::() { + 0 => Relaxed, + 1 => Release, + 2 => Acquire, + 3 => AcqRel, + _ => SeqCst, + } + } + } + + /// Pointer into `buf` at a nondeterministic byte offset. + /// + /// The offset may be misaligned for `T` or too close to the end of `buf` to + /// hold a `T`. `proof_for_contract` assumes the callee's `requires`, so only + /// pointers that satisfy alignment and validity are executed. + fn ptr_at_offset(buf: &mut [u8; 64]) -> *mut T { + let offset = kani::any_where(|o: &usize| *o < 64); + buf.as_mut_ptr().wrapping_add(offset).cast::() + } + + // SAFETY in every harness below: `proof_for_contract` assumes the function's + // `requires` (pointer validity / allowed `Ordering`) before executing the body. + + // --- Part 1: `from_ptr` --- + + #[kani::proof_for_contract(AtomicBool::from_ptr)] + fn check_atomic_bool_from_ptr() { + let mut buf: [bool; 16] = kani::any(); + let offset = kani::any_where(|o: &usize| *o < 16); + let ptr = buf.as_mut_ptr().wrapping_add(offset); + unsafe { + let _ = AtomicBool::from_ptr(ptr); + } + } + + macro_rules! from_ptr_proof { + ($name:ident, $atomic:ty, $int:ty) => { + #[kani::proof_for_contract(<$atomic>::from_ptr)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::<$int>(&mut buf); + unsafe { + let _ = <$atomic>::from_ptr(ptr); + } + } + }; + } + + #[cfg(target_has_atomic_load_store = "8")] + from_ptr_proof!(check_atomic_i8_from_ptr, AtomicI8, i8); + #[cfg(target_has_atomic_load_store = "8")] + from_ptr_proof!(check_atomic_u8_from_ptr, AtomicU8, u8); + #[cfg(target_has_atomic_load_store = "16")] + from_ptr_proof!(check_atomic_i16_from_ptr, AtomicI16, i16); + #[cfg(target_has_atomic_load_store = "16")] + from_ptr_proof!(check_atomic_u16_from_ptr, AtomicU16, u16); + #[cfg(target_has_atomic_load_store = "32")] + from_ptr_proof!(check_atomic_i32_from_ptr, AtomicI32, i32); + #[cfg(target_has_atomic_load_store = "32")] + from_ptr_proof!(check_atomic_u32_from_ptr, AtomicU32, u32); + #[cfg(target_has_atomic_load_store = "64")] + from_ptr_proof!(check_atomic_i64_from_ptr, AtomicI64, i64); + #[cfg(target_has_atomic_load_store = "64")] + from_ptr_proof!(check_atomic_u64_from_ptr, AtomicU64, u64); + #[cfg(target_has_atomic_load_store = "128")] + from_ptr_proof!(check_atomic_i128_from_ptr, AtomicI128, i128); + #[cfg(target_has_atomic_load_store = "128")] + from_ptr_proof!(check_atomic_u128_from_ptr, AtomicU128, u128); + #[cfg(target_has_atomic_load_store = "ptr")] + from_ptr_proof!(check_atomic_isize_from_ptr, AtomicIsize, isize); + #[cfg(target_has_atomic_load_store = "ptr")] + from_ptr_proof!(check_atomic_usize_from_ptr, AtomicUsize, usize); + + // `AtomicPtr`: T sizes 0, 1, 2, 4, and a non-power-of-two (3). + macro_rules! atomic_ptr_from_ptr_proof { + ($name:ident, $t:ty) => { + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(AtomicPtr::<$t>::from_ptr)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::<*mut $t>(&mut buf); + unsafe { + let _ = AtomicPtr::<$t>::from_ptr(ptr); + } + } + }; + } + + atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_zst, ()); + atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_u8, u8); + atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_u16, u16); + atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_u32, u32); + atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_odd, [u8; 3]); + + // --- Part 2: unsafe helpers --- + + #[kani::proof_for_contract(atomic_store)] + fn check_atomic_store_u8() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::(&mut buf); + unsafe { + atomic_store(ptr, kani::any(), kani::any()); + } + } + + #[kani::proof_for_contract(atomic_store)] + fn check_atomic_store_i32() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::(&mut buf); + unsafe { + atomic_store(ptr, kani::any(), kani::any()); + } + } + + #[kani::proof_for_contract(atomic_load)] + fn check_atomic_load_u8() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::(&mut buf); + unsafe { + let _ = atomic_load(ptr as *const u8, kani::any()); + } + } + + #[kani::proof_for_contract(atomic_load)] + fn check_atomic_load_i32() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::(&mut buf); + unsafe { + let _ = atomic_load(ptr as *const i32, kani::any()); + } + } + + macro_rules! rmw_proof { + ($contract:ident, $name:ident, $ty:ty) => { + #[cfg(target_has_atomic)] + #[kani::proof_for_contract($contract)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::<$ty>(&mut buf); + unsafe { + let _ = $contract::<$ty>(ptr, kani::any::<$ty>(), kani::any()); + } + } + }; + ($contract:ident, $name:ident, $ty:ty, $u:ty) => { + #[cfg(target_has_atomic)] + #[kani::proof_for_contract($contract)] + fn $name() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::<$ty>(&mut buf); + unsafe { + let _ = $contract::<$ty, $u>(ptr, kani::any::<$u>(), kani::any()); + } + } + }; + } + + rmw_proof!(atomic_swap, check_atomic_swap_u8, u8); + rmw_proof!(atomic_swap, check_atomic_swap_i32, i32); + rmw_proof!(atomic_add, check_atomic_add_u8, u8, u8); + rmw_proof!(atomic_add, check_atomic_add_i32, i32, i32); + rmw_proof!(atomic_sub, check_atomic_sub_u8, u8, u8); + rmw_proof!(atomic_sub, check_atomic_sub_i32, i32, i32); + rmw_proof!(atomic_and, check_atomic_and_u8, u8, u8); + rmw_proof!(atomic_nand, check_atomic_nand_u8, u8, u8); + rmw_proof!(atomic_or, check_atomic_or_u8, u8, u8); + rmw_proof!(atomic_xor, check_atomic_xor_u8, u8, u8); + rmw_proof!(atomic_max, check_atomic_max_i8, i8); + rmw_proof!(atomic_max, check_atomic_max_i32, i32); + rmw_proof!(atomic_min, check_atomic_min_i8, i8); + rmw_proof!(atomic_umax, check_atomic_umax_u8, u8); + rmw_proof!(atomic_umin, check_atomic_umin_u8, u8); + + #[cfg(target_has_atomic)] + #[kani::proof_for_contract(atomic_compare_exchange)] + fn check_atomic_compare_exchange_u8() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::(&mut buf); + unsafe { + let _ = + atomic_compare_exchange(ptr, kani::any(), kani::any(), kani::any(), kani::any()); + } + } + + #[cfg(target_has_atomic)] + #[kani::proof_for_contract(atomic_compare_exchange_weak)] + fn check_atomic_compare_exchange_weak_u8() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::(&mut buf); + unsafe { + let _ = atomic_compare_exchange_weak( + ptr, + kani::any(), + kani::any(), + kani::any(), + kani::any(), + ); + } + } + + #[cfg(target_has_atomic)] + #[kani::proof_for_contract(atomic_add)] + fn check_atomic_add_ptr() { + let mut buf: [u8; 64] = kani::any(); + let ptr = ptr_at_offset::<*mut u8>(&mut buf); + unsafe { + let _ = atomic_add::<*mut u8, usize>(ptr, kani::any::(), kani::any()); + } + } + + // --- Optional: panic-ordering contracts on safe methods --- + + #[kani::proof_for_contract(AtomicBool::store)] + fn check_atomic_bool_store() { + let atomic = AtomicBool::new(kani::any()); + atomic.store(kani::any(), kani::any()); + } + + #[kani::proof_for_contract(AtomicBool::load)] + fn check_atomic_bool_load() { + let atomic = AtomicBool::new(kani::any()); + let _ = atomic.load(kani::any()); + } + + #[cfg(target_has_atomic = "8")] + #[kani::proof_for_contract(AtomicBool::compare_exchange)] + fn check_atomic_bool_compare_exchange() { + let atomic = AtomicBool::new(kani::any()); + let _ = atomic.compare_exchange(kani::any(), kani::any(), kani::any(), kani::any()); + } + + #[cfg(target_has_atomic_load_store = "32")] + #[kani::proof_for_contract(AtomicI32::store)] + fn check_atomic_i32_store() { + let atomic = AtomicI32::new(kani::any()); + atomic.store(kani::any(), kani::any()); + } + + #[cfg(target_has_atomic_load_store = "32")] + #[kani::proof_for_contract(AtomicI32::load)] + fn check_atomic_i32_load() { + let atomic = AtomicI32::new(kani::any()); + let _ = atomic.load(kani::any()); + } + + #[cfg(all(target_has_atomic_load_store = "32", target_has_atomic = "32"))] + #[kani::proof_for_contract(AtomicI32::compare_exchange)] + fn check_atomic_i32_compare_exchange() { + let atomic = AtomicI32::new(kani::any()); + let _ = atomic.compare_exchange(kani::any(), kani::any(), kani::any(), kani::any()); + } + + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::store)] + fn check_atomic_ptr_store() { + let atomic = AtomicPtr::::new(kani::any::() as *mut u8); + atomic.store(kani::any::() as *mut u8, kani::any()); + } + + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::load)] + fn check_atomic_ptr_load() { + let atomic = AtomicPtr::::new(kani::any::() as *mut u8); + let _ = atomic.load(kani::any()); + } + + #[kani::proof] + #[kani::should_panic] + fn atomic_bool_store_panics_on_acquire() { + let atomic = AtomicBool::new(false); + atomic.store(true, Acquire); + } + + #[kani::proof] + #[kani::should_panic] + fn atomic_bool_load_panics_on_release() { + let atomic = AtomicBool::new(false); + let _ = atomic.load(Release); + } + + #[cfg(target_has_atomic = "8")] + #[kani::proof] + #[kani::should_panic] + fn atomic_bool_compare_exchange_panics_on_release_failure() { + let atomic = AtomicBool::new(false); + let _ = atomic.compare_exchange(false, true, Relaxed, Release); + } +} From 8d80a83a25098dc5a31841c4d308ba6817c00e67 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 18:11:49 +0530 Subject: [PATCH 2/3] fmt: rustfmt challenge 7 atomic contracts Apply rust-lang rustfmt.toml (style_edition 2024, use_small_heuristics=Max) so upstream_test format check passes. Same as ./scripts/check_rustc.sh --bless. --- library/core/src/intrinsics/mod.rs | 274 +++++----------------------- library/core/src/intrinsics/simd.rs | 2 +- library/core/src/sync/atomic.rs | 32 +--- 3 files changed, 53 insertions(+), 255 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 9def017ec0c14..a70214afc92a2 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -71,11 +71,7 @@ pub mod simd; // These imports are used for simplifying intra-doc links #[allow(unused_imports)] -#[cfg(all( - target_has_atomic = "8", - target_has_atomic = "32", - target_has_atomic = "ptr" -))] +#[cfg(all(target_has_atomic = "8", target_has_atomic = "32", target_has_atomic = "ptr"))] use crate::sync::atomic::{self, AtomicBool, AtomicI32, AtomicIsize, AtomicU32, Ordering}; /// A type for atomic ordering parameters for intrinsics. This is a separate type from @@ -496,11 +492,7 @@ pub const fn select_unpredictable(b: bool, true_val: T, false_val: T) -> T where T: [const] Destruct, { - if b { - true_val - } else { - false_val - } + if b { true_val } else { false_val } } /// A guard for unsafe functions that cannot ever be executed if `T` is uninhabited: @@ -3104,11 +3096,7 @@ pub const fn minimumf16(x: f16, y: f16) -> f16 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { - x - } else { - y - } + if x.is_sign_negative() && y.is_sign_positive() { x } else { y } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3129,11 +3117,7 @@ pub const fn minimumf32(x: f32, y: f32) -> f32 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { - x - } else { - y - } + if x.is_sign_negative() && y.is_sign_positive() { x } else { y } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3154,11 +3138,7 @@ pub const fn minimumf64(x: f64, y: f64) -> f64 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { - x - } else { - y - } + if x.is_sign_negative() && y.is_sign_positive() { x } else { y } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3179,11 +3159,7 @@ pub const fn minimumf128(x: f128, y: f128) -> f128 { } else if y < x { y } else if x == y { - if x.is_sign_negative() && y.is_sign_positive() { - x - } else { - y - } + if x.is_sign_negative() && y.is_sign_positive() { x } else { y } } else { // At least one input is NaN. Use `+` to perform NaN propagation and quieting. x + y @@ -3258,11 +3234,7 @@ pub const fn maximumf16(x: f16, y: f16) -> f16 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { - x - } else { - y - } + if x.is_sign_positive() && y.is_sign_negative() { x } else { y } } else { x + y } @@ -3282,11 +3254,7 @@ pub const fn maximumf32(x: f32, y: f32) -> f32 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { - x - } else { - y - } + if x.is_sign_positive() && y.is_sign_negative() { x } else { y } } else { x + y } @@ -3306,11 +3274,7 @@ pub const fn maximumf64(x: f64, y: f64) -> f64 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { - x - } else { - y - } + if x.is_sign_positive() && y.is_sign_negative() { x } else { y } } else { x + y } @@ -3330,11 +3294,7 @@ pub const fn maximumf128(x: f128, y: f128) -> f128 { } else if y > x { y } else if x == y { - if x.is_sign_positive() && y.is_sign_negative() { - x - } else { - y - } + if x.is_sign_positive() && y.is_sign_negative() { x } else { y } } else { x + y } @@ -3839,9 +3799,7 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference( - &src as *const $src as *const $dst, - )); + kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; assert_eq!(src, src2); @@ -3857,9 +3815,7 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference( - &src as *const $src as *const $dst, - )); + kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; if src.is_nan() { @@ -3915,10 +3871,7 @@ mod verify { let mut generator = PointerGenerator::<10000>::new(); let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ptr_2: *const u8 = unsafe { transmute_unchecked(arb_ptr) }; - assert_eq!( - arb_ptr as *const bool, - arb_ptr_2 as *const u8 as *const bool - ); + assert_eq!(arb_ptr as *const bool, arb_ptr_2 as *const u8 as *const bool); } //Tests that transmuting (unchecked) a ref does not mutate the stored address @@ -3928,10 +3881,7 @@ mod verify { let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ref: &bool = unsafe { &*(arb_ptr) }; let arb_ref_2: &u8 = unsafe { transmute_unchecked(arb_ref) }; - assert_eq!( - arb_ref as *const bool, - arb_ref_2 as *const u8 as *const bool - ); + assert_eq!(arb_ref as *const bool, arb_ref_2 as *const u8 as *const bool); } //Tests that transmuting (unchecked) a slice does not mutate the slice metadata (address and length) @@ -3957,9 +3907,7 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference( - &src as *const $src as *const $dst, - )); + kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); let dst: $dst = unsafe { transmute(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; assert_eq!(src, src2); @@ -3975,9 +3923,7 @@ mod verify { #[kani::proof] fn $harness() { let src: $src = kani::any(); - kani::assume(ub_checks::can_dereference( - &src as *const $src as *const $dst, - )); + kani::assume(ub_checks::can_dereference(&src as *const $src as *const $dst)); let dst: $dst = unsafe { transmute(src) }; let src2: $src = unsafe { *(&dst as *const $dst as *const $src) }; if src.is_nan() { @@ -4033,10 +3979,7 @@ mod verify { let mut generator = PointerGenerator::<10000>::new(); let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ptr_2: *const u8 = unsafe { transmute(arb_ptr) }; - assert_eq!( - arb_ptr as *const bool, - arb_ptr_2 as *const u8 as *const bool - ); + assert_eq!(arb_ptr as *const bool, arb_ptr_2 as *const u8 as *const bool); } //Tests that transmuting a ref does not mutate the stored address @@ -4046,10 +3989,7 @@ mod verify { let arb_ptr: *const bool = generator.any_in_bounds().ptr; let arb_ref: &bool = unsafe { &*(arb_ptr) }; let arb_ref_2: &u8 = unsafe { transmute(arb_ref) }; - assert_eq!( - arb_ref as *const bool, - arb_ref_2 as *const u8 as *const bool - ); + assert_eq!(arb_ref as *const bool, arb_ref_2 as *const u8 as *const bool); } //Tests that transmuting a slice does not mutate the slice metadata (address and length) @@ -4191,16 +4131,9 @@ mod verify { fn run_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { let mut generator1 = PointerGenerator::<100>::new(); let mut generator2 = PointerGenerator::<100>::new(); - let ArbitraryPointer { - ptr: src, - status: src_status, - .. - } = generator1.any_alloc_status::(); - let ArbitraryPointer { - ptr: dst, - status: dst_status, - .. - } = if kani::any() { + let ArbitraryPointer { ptr: src, status: src_status, .. } = + generator1.any_alloc_status::(); + let ArbitraryPointer { ptr: dst, status: dst_status, .. } = if kani::any() { generator1.any_alloc_status::() } else { generator2.any_alloc_status::() @@ -4430,119 +4363,29 @@ mod verify { proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_acqrel, AcqRel); proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_seqcst, SeqCst); - proof_atomic_rmw_u8!( - atomic_xadd_wrapper, - check_atomic_xadd_relaxed, - Relaxed, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xadd_wrapper, - check_atomic_xadd_acquire, - Acquire, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xadd_wrapper, - check_atomic_xadd_release, - Release, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xadd_wrapper, - check_atomic_xadd_acqrel, - AcqRel, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xadd_wrapper, - check_atomic_xadd_seqcst, - SeqCst, - two_ty - ); - - proof_atomic_rmw_u8!( - atomic_xsub_wrapper, - check_atomic_xsub_relaxed, - Relaxed, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xsub_wrapper, - check_atomic_xsub_acquire, - Acquire, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xsub_wrapper, - check_atomic_xsub_release, - Release, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xsub_wrapper, - check_atomic_xsub_acqrel, - AcqRel, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xsub_wrapper, - check_atomic_xsub_seqcst, - SeqCst, - two_ty - ); - - proof_atomic_rmw_u8!( - atomic_and_wrapper, - check_atomic_and_relaxed, - Relaxed, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_and_wrapper, - check_atomic_and_acquire, - Acquire, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_and_wrapper, - check_atomic_and_release, - Release, - two_ty - ); + proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_relaxed, Relaxed, two_ty); + proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_acquire, Acquire, two_ty); + proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_release, Release, two_ty); + proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_acqrel, AcqRel, two_ty); + proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_seqcst, SeqCst, two_ty); + + proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_relaxed, Relaxed, two_ty); + proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_acquire, Acquire, two_ty); + proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_release, Release, two_ty); + proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_acqrel, AcqRel, two_ty); + proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_seqcst, SeqCst, two_ty); + + proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_relaxed, Relaxed, two_ty); + proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_acquire, Acquire, two_ty); + proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_release, Release, two_ty); proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_acqrel, AcqRel, two_ty); proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_seqcst, SeqCst, two_ty); - proof_atomic_rmw_u8!( - atomic_nand_wrapper, - check_atomic_nand_relaxed, - Relaxed, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_nand_wrapper, - check_atomic_nand_acquire, - Acquire, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_nand_wrapper, - check_atomic_nand_release, - Release, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_nand_wrapper, - check_atomic_nand_acqrel, - AcqRel, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_nand_wrapper, - check_atomic_nand_seqcst, - SeqCst, - two_ty - ); + proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_relaxed, Relaxed, two_ty); + proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_acquire, Acquire, two_ty); + proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_release, Release, two_ty); + proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_acqrel, AcqRel, two_ty); + proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_seqcst, SeqCst, two_ty); proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_relaxed, Relaxed, two_ty); proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_acquire, Acquire, two_ty); @@ -4550,24 +4393,9 @@ mod verify { proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_acqrel, AcqRel, two_ty); proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_seqcst, SeqCst, two_ty); - proof_atomic_rmw_u8!( - atomic_xor_wrapper, - check_atomic_xor_relaxed, - Relaxed, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xor_wrapper, - check_atomic_xor_acquire, - Acquire, - two_ty - ); - proof_atomic_rmw_u8!( - atomic_xor_wrapper, - check_atomic_xor_release, - Release, - two_ty - ); + proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_relaxed, Relaxed, two_ty); + proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_acquire, Acquire, two_ty); + proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_release, Release, two_ty); proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_acqrel, AcqRel, two_ty); proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_seqcst, SeqCst, two_ty); @@ -4691,12 +4519,7 @@ mod verify { AcqRel, Acquire ); - proof_atomic_cxchg_ord!( - atomic_cxchg_wrapper, - check_atomic_cxchg_acqrel_seqcst, - AcqRel, - SeqCst - ); + proof_atomic_cxchg_ord!(atomic_cxchg_wrapper, check_atomic_cxchg_acqrel_seqcst, AcqRel, SeqCst); proof_atomic_cxchg_ord!( atomic_cxchg_wrapper, check_atomic_cxchg_seqcst_relaxed, @@ -4709,12 +4532,7 @@ mod verify { SeqCst, Acquire ); - proof_atomic_cxchg_ord!( - atomic_cxchg_wrapper, - check_atomic_cxchg_seqcst_seqcst, - SeqCst, - SeqCst - ); + proof_atomic_cxchg_ord!(atomic_cxchg_wrapper, check_atomic_cxchg_seqcst_seqcst, SeqCst, SeqCst); proof_atomic_cxchg_ord!( atomic_cxchgweak_wrapper, diff --git a/library/core/src/intrinsics/simd.rs b/library/core/src/intrinsics/simd.rs index 10e69e7a0efa8..722a765cd01ee 100644 --- a/library/core/src/intrinsics/simd.rs +++ b/library/core/src/intrinsics/simd.rs @@ -413,7 +413,7 @@ pub enum SimdAlign { #[rustc_intrinsic] #[rustc_nounwind] pub const unsafe fn simd_masked_load(mask: V, ptr: U, val: T) - -> T; +-> T; /// Writes to a vector of pointers. /// diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index 6c4f8c0df1537..eb4b8bfc73a3f 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -532,9 +532,7 @@ impl AtomicBool { #[rustc_const_stable(feature = "const_atomic_new", since = "1.24.0")] #[must_use] pub const fn new(v: bool) -> AtomicBool { - AtomicBool { - v: UnsafeCell::new(v as u8), - } + AtomicBool { v: UnsafeCell::new(v as u8) } } /// Creates a new `AtomicBool` from a pointer. @@ -798,11 +796,7 @@ impl AtomicBool { #[rustc_should_not_be_called_on_const_items] pub fn swap(&self, val: bool, order: Ordering) -> bool { if EMULATE_ATOMIC_BOOL { - if val { - self.fetch_or(true, order) - } else { - self.fetch_and(false, order) - } + if val { self.fetch_or(true, order) } else { self.fetch_and(false, order) } } else { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_swap(self.v.get(), val as u8, order) != 0 } @@ -962,11 +956,7 @@ impl AtomicBool { // This sets the value to the new one and returns the old one. self.swap(new, order) }; - if old == current { - Ok(old) - } else { - Err(old) - } + if old == current { Ok(old) } else { Err(old) } } else { // SAFETY: data races are prevented by atomic intrinsics. match unsafe { @@ -1521,9 +1511,7 @@ impl AtomicPtr { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_atomic_new", since = "1.24.0")] pub const fn new(p: *mut T) -> AtomicPtr { - AtomicPtr { - p: UnsafeCell::new(p), - } + AtomicPtr { p: UnsafeCell::new(p) } } /// Creates a new `AtomicPtr` from a pointer. @@ -4181,11 +4169,7 @@ pub unsafe fn atomic_compare_exchange( (_, Release) => panic!("there is no such thing as a release failure ordering"), } }; - if ok { - Ok(val) - } else { - Err(val) - } + if ok { Ok(val) } else { Err(val) } } #[inline] @@ -4253,11 +4237,7 @@ unsafe fn atomic_compare_exchange_weak( (_, Release) => panic!("there is no such thing as a release failure ordering"), } }; - if ok { - Ok(val) - } else { - Err(val) - } + if ok { Ok(val) } else { Err(val) } } #[inline] From f0c1b1c300a5b206c8290e6c84aba356797791a3 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 19:39:25 +0530 Subject: [PATCH 3/3] Challenge 7: fix Kani assignable failures on atomic writes Add kani::modifies on atomic store/RMW contracts and wrappers. Proofs use live stack objects instead of wrapping_add pointers, which lose provenance and fail CBMC's assignable check. Fixes #83 --- library/core/src/intrinsics/mod.rs | 61 +++++++++++++-------- library/core/src/sync/atomic.rs | 85 +++++++++++++++++++----------- 2 files changed, 94 insertions(+), 52 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index a70214afc92a2..6171fa004c31c 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4158,11 +4158,11 @@ mod verify { // documented pointer preconditions and invoke the const-generic intrinsics // that replaced the older `atomic_*_{relaxed,acquire,...}` names. - fn atomic_ptr_at_offset(buf: &mut [u8; 64]) -> *mut T { - let offset = kani::any_where(|o: &usize| *o < 64); - buf.as_mut_ptr().wrapping_add(offset).cast::() - } + // Write proofs use a live stack object. `wrapping_add` pointers lose + // provenance, so CBMC's assignable check fails even when `can_write` is + // assumed. + #[kani::modifies(dst)] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_store_wrapper(dst: *mut T, val: T) { // SAFETY: `requires` guarantees `dst` is aligned and writable. @@ -4175,6 +4175,7 @@ mod verify { unsafe { atomic_load::(src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_xchg_wrapper(dst: *mut T, src: T) -> T { @@ -4182,6 +4183,7 @@ mod verify { unsafe { atomic_xchg::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_xadd_wrapper( @@ -4192,6 +4194,7 @@ mod verify { unsafe { atomic_xadd::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_xsub_wrapper( @@ -4202,6 +4205,7 @@ mod verify { unsafe { atomic_xsub::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_and_wrapper( @@ -4212,6 +4216,7 @@ mod verify { unsafe { atomic_and::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_nand_wrapper( @@ -4222,6 +4227,7 @@ mod verify { unsafe { atomic_nand::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_or_wrapper( @@ -4232,6 +4238,7 @@ mod verify { unsafe { atomic_or::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_xor_wrapper( @@ -4242,6 +4249,7 @@ mod verify { unsafe { atomic_xor::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_max_wrapper(dst: *mut T, src: T) -> T { @@ -4249,6 +4257,7 @@ mod verify { unsafe { atomic_max::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_min_wrapper(dst: *mut T, src: T) -> T { @@ -4256,6 +4265,7 @@ mod verify { unsafe { atomic_min::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_umax_wrapper(dst: *mut T, src: T) -> T { @@ -4263,6 +4273,7 @@ mod verify { unsafe { atomic_umax::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_umin_wrapper(dst: *mut T, src: T) -> T { @@ -4270,6 +4281,7 @@ mod verify { unsafe { atomic_umin::(dst, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_cxchg_wrapper< @@ -4285,6 +4297,7 @@ mod verify { unsafe { atomic_cxchg::(dst, old, src) } } + #[kani::modifies(dst)] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_cxchgweak_wrapper< @@ -4304,10 +4317,12 @@ mod verify { ($name:ident, $ord:ident) => { #[kani::proof_for_contract(atomic_store_wrapper)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = atomic_ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { - atomic_store_wrapper::(ptr, kani::any()); + atomic_store_wrapper::( + &mut val as *mut u8, + kani::any(), + ); } } }; @@ -4321,10 +4336,9 @@ mod verify { ($name:ident, $ord:ident) => { #[kani::proof_for_contract(atomic_load_wrapper)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = atomic_ptr_at_offset::(&mut buf); + let val: u8 = kani::any(); unsafe { - let _ = atomic_load_wrapper::(ptr as *const u8); + let _ = atomic_load_wrapper::(&val as *const u8); } } }; @@ -4338,20 +4352,22 @@ mod verify { ($wrapper:ident, $name:ident, $ord:ident) => { #[kani::proof_for_contract($wrapper)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = atomic_ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { - let _ = $wrapper::(ptr, kani::any()); + let _ = + $wrapper::(&mut val as *mut u8, kani::any()); } } }; ($wrapper:ident, $name:ident, $ord:ident, two_ty) => { #[kani::proof_for_contract($wrapper)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = atomic_ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { - let _ = $wrapper::(ptr, kani::any()); + let _ = $wrapper::( + &mut val as *mut u8, + kani::any(), + ); } } }; @@ -4403,10 +4419,12 @@ mod verify { ($wrapper:ident, $name:ident, $ty:ty, $ord:ident) => { #[kani::proof_for_contract($wrapper)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = atomic_ptr_at_offset::<$ty>(&mut buf); + let mut val: $ty = kani::any(); unsafe { - let _ = $wrapper::<$ty, { AtomicOrdering::$ord }>(ptr, kani::any()); + let _ = $wrapper::<$ty, { AtomicOrdering::$ord }>( + &mut val as *mut $ty, + kani::any(), + ); } } }; @@ -4440,11 +4458,10 @@ mod verify { ($wrapper:ident, $name:ident, $succ:ident, $fail:ident) => { #[kani::proof_for_contract($wrapper)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = atomic_ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { let _ = $wrapper::( - ptr, + &mut val as *mut u8, kani::any(), kani::any(), ); diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index eb4b8bfc73a3f..70230dba847a9 100644 --- a/library/core/src/sync/atomic.rs +++ b/library/core/src/sync/atomic.rs @@ -760,6 +760,7 @@ impl AtomicBool { #[stable(feature = "rust1", since = "1.0.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.v.get()))] #[requires(order == Relaxed || order == Release || order == SeqCst)] pub fn store(&self, val: bool, order: Ordering) { // SAFETY: any data races are prevented by atomic intrinsics and the raw @@ -924,6 +925,7 @@ impl AtomicBool { #[cfg(target_has_atomic = "8")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.v.get()))] #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange( &self, @@ -1021,6 +1023,7 @@ impl AtomicBool { #[cfg(target_has_atomic = "8")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.v.get()))] #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange_weak( &self, @@ -1767,6 +1770,7 @@ impl AtomicPtr { #[stable(feature = "rust1", since = "1.0.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.p.get()))] #[requires(order == Relaxed || order == Release || order == SeqCst)] pub fn store(&self, ptr: *mut T, order: Ordering) { // SAFETY: data races are prevented by atomic intrinsics. @@ -1920,6 +1924,7 @@ impl AtomicPtr { #[cfg(target_has_atomic = "ptr")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.p.get()))] #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange( &self, @@ -1985,6 +1990,7 @@ impl AtomicPtr { #[cfg(target_has_atomic = "ptr")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.p.get()))] #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange_weak( &self, @@ -2968,6 +2974,7 @@ macro_rules! atomic_int { #[$stable] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.v.get()))] #[requires(order == Relaxed || order == Release || order == SeqCst)] pub fn store(&self, val: $int_type, order: Ordering) { // SAFETY: data races are prevented by atomic intrinsics. @@ -3132,6 +3139,7 @@ macro_rules! atomic_int { #[$cfg_cas] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.v.get()))] #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange(&self, current: $int_type, @@ -3197,6 +3205,7 @@ macro_rules! atomic_int { #[$cfg_cas] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_should_not_be_called_on_const_items] + #[cfg_attr(kani, kani::modifies(self.v.get()))] #[requires(failure != Release && failure != AcqRel)] pub fn compare_exchange_weak(&self, current: $int_type, @@ -4013,6 +4022,7 @@ fn strongest_failure_ordering(order: Ordering) -> Ordering { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_write(dst))] #[requires(order == Relaxed || order == Release || order == SeqCst)] unsafe fn atomic_store(dst: *mut T, val: T, order: Ordering) { @@ -4048,6 +4058,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_swap(dst: *mut T, val: T, order: Ordering) -> T { @@ -4067,6 +4078,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_add(dst: *mut T, val: U, order: Ordering) -> T { @@ -4086,6 +4098,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_sub(dst: *mut T, val: U, order: Ordering) -> T { @@ -4107,6 +4120,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)] +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] #[requires(failure != Release && failure != AcqRel)] @@ -4175,6 +4189,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] #[requires(failure != Release && failure != AcqRel)] @@ -4243,6 +4258,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_and(dst: *mut T, val: U, order: Ordering) -> T { @@ -4261,6 +4277,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_nand(dst: *mut T, val: U, order: Ordering) -> T { @@ -4279,6 +4296,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_or(dst: *mut T, val: U, order: Ordering) -> T { @@ -4297,6 +4315,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_xor(dst: *mut T, val: U, order: Ordering) -> T { @@ -4316,6 +4335,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_max(dst: *mut T, val: T, order: Ordering) -> T { @@ -4335,6 +4355,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_min(dst: *mut T, val: T, order: Ordering) -> T { @@ -4354,6 +4375,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_umax(dst: *mut T, val: T, order: Ordering) -> T { @@ -4373,6 +4395,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 +#[cfg_attr(kani, kani::modifies(dst))] #[requires(ub_checks::can_dereference(dst as *const T))] #[requires(ub_checks::can_write(dst))] unsafe fn atomic_umin(dst: *mut T, val: T, order: Ordering) -> T { @@ -4698,8 +4721,9 @@ mod verify { buf.as_mut_ptr().wrapping_add(offset).cast::() } - // SAFETY in every harness below: `proof_for_contract` assumes the function's - // `requires` (pointer validity / allowed `Ordering`) before executing the body. + // Write proofs use a live stack object. `wrapping_add` pointers lose + // provenance, so CBMC's assignable check fails even when `can_write` is + // assumed. `proof_for_contract` still assumes the callee's `requires`. // --- Part 1: `from_ptr` --- @@ -4776,37 +4800,33 @@ mod verify { #[kani::proof_for_contract(atomic_store)] fn check_atomic_store_u8() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { - atomic_store(ptr, kani::any(), kani::any()); + atomic_store(&mut val as *mut u8, kani::any(), kani::any()); } } #[kani::proof_for_contract(atomic_store)] fn check_atomic_store_i32() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::(&mut buf); + let mut val: i32 = kani::any(); unsafe { - atomic_store(ptr, kani::any(), kani::any()); + atomic_store(&mut val as *mut i32, kani::any(), kani::any()); } } #[kani::proof_for_contract(atomic_load)] fn check_atomic_load_u8() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::(&mut buf); + let val: u8 = kani::any(); unsafe { - let _ = atomic_load(ptr as *const u8, kani::any()); + let _ = atomic_load(&val as *const u8, kani::any()); } } #[kani::proof_for_contract(atomic_load)] fn check_atomic_load_i32() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::(&mut buf); + let val: i32 = kani::any(); unsafe { - let _ = atomic_load(ptr as *const i32, kani::any()); + let _ = atomic_load(&val as *const i32, kani::any()); } } @@ -4815,10 +4835,9 @@ mod verify { #[cfg(target_has_atomic)] #[kani::proof_for_contract($contract)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::<$ty>(&mut buf); + let mut val: $ty = kani::any(); unsafe { - let _ = $contract::<$ty>(ptr, kani::any::<$ty>(), kani::any()); + let _ = $contract::<$ty>(&mut val as *mut $ty, kani::any::<$ty>(), kani::any()); } } }; @@ -4826,10 +4845,10 @@ mod verify { #[cfg(target_has_atomic)] #[kani::proof_for_contract($contract)] fn $name() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::<$ty>(&mut buf); + let mut val: $ty = kani::any(); unsafe { - let _ = $contract::<$ty, $u>(ptr, kani::any::<$u>(), kani::any()); + let _ = + $contract::<$ty, $u>(&mut val as *mut $ty, kani::any::<$u>(), kani::any()); } } }; @@ -4854,22 +4873,25 @@ mod verify { #[cfg(target_has_atomic)] #[kani::proof_for_contract(atomic_compare_exchange)] fn check_atomic_compare_exchange_u8() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { - let _ = - atomic_compare_exchange(ptr, kani::any(), kani::any(), kani::any(), kani::any()); + let _ = atomic_compare_exchange( + &mut val as *mut u8, + kani::any(), + kani::any(), + kani::any(), + kani::any(), + ); } } #[cfg(target_has_atomic)] #[kani::proof_for_contract(atomic_compare_exchange_weak)] fn check_atomic_compare_exchange_weak_u8() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::(&mut buf); + let mut val: u8 = kani::any(); unsafe { let _ = atomic_compare_exchange_weak( - ptr, + &mut val as *mut u8, kani::any(), kani::any(), kani::any(), @@ -4881,10 +4903,13 @@ mod verify { #[cfg(target_has_atomic)] #[kani::proof_for_contract(atomic_add)] fn check_atomic_add_ptr() { - let mut buf: [u8; 64] = kani::any(); - let ptr = ptr_at_offset::<*mut u8>(&mut buf); + let mut val = kani::any::() as *mut u8; unsafe { - let _ = atomic_add::<*mut u8, usize>(ptr, kani::any::(), kani::any()); + let _ = atomic_add::<*mut u8, usize>( + &mut val as *mut *mut u8, + kani::any::(), + kani::any(), + ); } }