From 401fbbedd61c6fac7c2a88cca7dcf00ba3afbac8 Mon Sep 17 00:00:00 2001 From: v3risec Date: Tue, 8 Sep 2026 23:55:50 +0800 Subject: [PATCH] Add Kani verification method for Challenge 7 --- library/Cargo.lock | 90 ++ library/core/src/intrinsics/mod.rs | 594 ++++++++++++ library/core/src/sync/atomic.rs | 1404 ++++++++++++++++++++++++++++ 3 files changed, 2088 insertions(+) diff --git a/library/Cargo.lock b/library/Cargo.lock index 8f60cea459c7d..213c7200e8a4a 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -28,6 +28,7 @@ version = "0.0.0" dependencies = [ "compiler_builtins", "core", + "safety", ] [[package]] @@ -67,6 +68,9 @@ dependencies = [ [[package]] name = "core" version = "0.0.0" +dependencies = [ + "safety", +] [[package]] name = "coretests" @@ -213,6 +217,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -229,6 +266,15 @@ dependencies = [ "cc", ] +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "5.3.0" @@ -313,6 +359,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "shlex" version = "1.3.0" @@ -342,6 +398,7 @@ dependencies = [ "rand", "rand_xorshift", "rustc-demangle", + "safety", "std_detect", "unwind", "vex-sdk", @@ -359,6 +416,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -379,6 +457,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + [[package]] name = "unwind" version = "0.0.0" @@ -398,6 +482,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "vex-sdk" version = "0.27.1" diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index ddadeeb3c786a..04a0fc9797c8d 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4150,4 +4150,598 @@ mod verify { fn supported_status(status: AllocationStatus) -> bool { status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject } + + // Challenge 7, Part 3: atomic intrinsic contracts. + // + // Kani cannot currently attach contracts directly to bodyless + // `rustc_intrinsic` declarations (model-checking/kani#3345). These wrappers + // are the Kani-facing specifications for the const-generic intrinsics above. + // The harness instantiations follow the integer and pointer restrictions in + // the intrinsic documentation, while the contracts encode only the local + // memory obligations required by the intrinsic calls. + // + // `can_dereference` and `can_write` cover allocation bounds, initialization, + // and alignment for `T`. Kani function contracts do not currently expose a predicate for cross-thread + // access histories, so the atomic model remains responsible for detecting + // data races and mixed-size overlapping atomic accesses in concurrent proofs. + + #[allow(dead_code)] + #[kani::modifies(dst)] + #[requires(crate::ub_checks::can_write(dst))] + unsafe fn atomic_store_wrapper(dst: *mut T, val: T) { + unsafe { atomic_store::(dst, val) } + } + + #[allow(dead_code)] + #[requires(crate::ub_checks::can_dereference(src))] + unsafe fn atomic_load_wrapper(src: *const T) -> T { + unsafe { atomic_load::(src) } + } + + #[allow(dead_code)] + #[kani::modifies(dst)] + #[requires(crate::ub_checks::can_dereference(dst as *const T))] + #[requires(crate::ub_checks::can_write(dst))] + unsafe fn atomic_xchg_wrapper(dst: *mut T, val: T) -> T { + unsafe { atomic_xchg::(dst, val) } + } + + macro_rules! define_atomic_binary_rmw_wrapper { + ($wrapper:ident, $intrinsic:ident) => { + #[allow(dead_code)] + #[kani::modifies(dst)] + #[requires(crate::ub_checks::can_dereference(dst as *const T))] + #[requires(crate::ub_checks::can_write(dst))] + unsafe fn $wrapper( + dst: *mut T, + val: U, + ) -> T { + unsafe { $intrinsic::(dst, val) } + } + }; + } + + define_atomic_binary_rmw_wrapper!(atomic_xadd_wrapper, atomic_xadd); + define_atomic_binary_rmw_wrapper!(atomic_xsub_wrapper, atomic_xsub); + define_atomic_binary_rmw_wrapper!(atomic_and_wrapper, atomic_and); + define_atomic_binary_rmw_wrapper!(atomic_nand_wrapper, atomic_nand); + define_atomic_binary_rmw_wrapper!(atomic_or_wrapper, atomic_or); + define_atomic_binary_rmw_wrapper!(atomic_xor_wrapper, atomic_xor); + + macro_rules! define_atomic_extremum_wrapper { + ($wrapper:ident, $intrinsic:ident) => { + #[allow(dead_code)] + #[kani::modifies(dst)] + #[requires(crate::ub_checks::can_dereference(dst as *const T))] + #[requires(crate::ub_checks::can_write(dst))] + unsafe fn $wrapper(dst: *mut T, val: T) -> T { + unsafe { $intrinsic::(dst, val) } + } + }; + } + + define_atomic_extremum_wrapper!(atomic_max_wrapper, atomic_max); + define_atomic_extremum_wrapper!(atomic_min_wrapper, atomic_min); + define_atomic_extremum_wrapper!(atomic_umax_wrapper, atomic_umax); + define_atomic_extremum_wrapper!(atomic_umin_wrapper, atomic_umin); + + macro_rules! define_atomic_compare_exchange_wrapper { + ($wrapper:ident, $intrinsic:ident) => { + #[allow(dead_code)] + #[kani::modifies(dst)] + #[requires(crate::ub_checks::can_dereference(dst as *const T))] + #[requires(crate::ub_checks::can_write(dst))] + unsafe fn $wrapper< + T: Copy, + const ORD_SUCC: AtomicOrdering, + const ORD_FAIL: AtomicOrdering, + >( + dst: *mut T, + old: T, + new: T, + ) -> (T, bool) { + unsafe { $intrinsic::(dst, old, new) } + } + }; + } + + define_atomic_compare_exchange_wrapper!(atomic_cxchg_wrapper, atomic_cxchg); + define_atomic_compare_exchange_wrapper!(atomic_cxchgweak_wrapper, atomic_cxchgweak); + + // Every ordering-specific harness below expands to every legal integer + // width and to the pointer form. Storage is a local object, so the raw + // pointer passed to the intrinsic has concrete provenance without a + // separate wrapper type. Pointer *values* remain arbitrary addresses. + macro_rules! atomic_integer_load_store_types { + ($call:ident, $($args:tt)*) => { + #[cfg(target_has_atomic_load_store = "8")] { $call!(i8, $($args)*); $call!(u8, $($args)*); } + #[cfg(target_has_atomic_load_store = "16")] { $call!(i16, $($args)*); $call!(u16, $($args)*); } + #[cfg(target_has_atomic_load_store = "32")] { $call!(i32, $($args)*); $call!(u32, $($args)*); } + #[cfg(target_has_atomic_load_store = "64")] { $call!(i64, $($args)*); $call!(u64, $($args)*); } + #[cfg(target_has_atomic_load_store = "128")] { $call!(i128, $($args)*); $call!(u128, $($args)*); } + #[cfg(target_has_atomic_load_store = "ptr")] { $call!(isize, $($args)*); $call!(usize, $($args)*); } + }; + } + + macro_rules! atomic_integer_types { + ($call:ident, $($args:tt)*) => { + #[cfg(target_has_atomic = "8")] { $call!(i8, $($args)*); $call!(u8, $($args)*); } + #[cfg(target_has_atomic = "16")] { $call!(i16, $($args)*); $call!(u16, $($args)*); } + #[cfg(target_has_atomic = "32")] { $call!(i32, $($args)*); $call!(u32, $($args)*); } + #[cfg(target_has_atomic = "64")] { $call!(i64, $($args)*); $call!(u64, $($args)*); } + #[cfg(target_has_atomic = "128")] { $call!(i128, $($args)*); $call!(u128, $($args)*); } + #[cfg(target_has_atomic = "ptr")] { $call!(isize, $($args)*); $call!(usize, $($args)*); } + }; + } + + macro_rules! atomic_signed_types { + ($call:ident, $($args:tt)*) => { + #[cfg(target_has_atomic = "8")] { $call!(i8, $($args)*); } + #[cfg(target_has_atomic = "16")] { $call!(i16, $($args)*); } + #[cfg(target_has_atomic = "32")] { $call!(i32, $($args)*); } + #[cfg(target_has_atomic = "64")] { $call!(i64, $($args)*); } + #[cfg(target_has_atomic = "128")] { $call!(i128, $($args)*); } + #[cfg(target_has_atomic = "ptr")] { $call!(isize, $($args)*); } + }; + } + + macro_rules! atomic_unsigned_types { + ($call:ident, $($args:tt)*) => { + #[cfg(target_has_atomic = "8")] { $call!(u8, $($args)*); } + #[cfg(target_has_atomic = "16")] { $call!(u16, $($args)*); } + #[cfg(target_has_atomic = "32")] { $call!(u32, $($args)*); } + #[cfg(target_has_atomic = "64")] { $call!(u64, $($args)*); } + #[cfg(target_has_atomic = "128")] { $call!(u128, $($args)*); } + #[cfg(target_has_atomic = "ptr")] { $call!(usize, $($args)*); } + }; + } + + // Store: integer and pointer T, with the three orderings accepted by the + // intrinsic's stabilized atomic counterpart. + macro_rules! atomic_store_call { + ($ty:ty, $ord:path) => {{ + let mut dst: $ty = kani::any(); + let val: $ty = kani::any(); + unsafe { atomic_store_wrapper::<$ty, { $ord }>(&mut dst, val) }; + }}; + } + macro_rules! atomic_store_harness { + ($name:ident, $ord:path) => { + #[kani::proof_for_contract(atomic_store_wrapper)] + fn $name() { + atomic_integer_load_store_types!(atomic_store_call, $ord); + #[cfg(target_has_atomic_load_store = "ptr")] + { + let mut dst: *mut u8 = kani::any::() as *mut u8; + let val: *mut u8 = kani::any::() as *mut u8; + unsafe { atomic_store_wrapper::<*mut u8, { $ord }>(&mut dst, val) }; + } + kani::cover(true, "atomic intrinsic store: reached after call"); + } + }; + } + atomic_store_harness!(harness_intrinsic_atomic_store_relaxed, AtomicOrdering::Relaxed); + atomic_store_harness!(harness_intrinsic_atomic_store_release, AtomicOrdering::Release); + atomic_store_harness!(harness_intrinsic_atomic_store_seqcst, AtomicOrdering::SeqCst); + + // Load: the same complete T matrix as store. + macro_rules! atomic_load_call { + ($ty:ty, $ord:path) => {{ + let src: $ty = kani::any(); + let _ = unsafe { atomic_load_wrapper::<$ty, { $ord }>(&src) }; + }}; + } + macro_rules! atomic_load_harness { + ($name:ident, $ord:path) => { + #[kani::proof_for_contract(atomic_load_wrapper)] + fn $name() { + atomic_integer_load_store_types!(atomic_load_call, $ord); + #[cfg(target_has_atomic_load_store = "ptr")] + { + let src: *mut u8 = kani::any::() as *mut u8; + let _ = unsafe { atomic_load_wrapper::<*mut u8, { $ord }>(&src) }; + } + kani::cover(true, "atomic intrinsic load: reached after call"); + } + }; + } + atomic_load_harness!(harness_intrinsic_atomic_load_relaxed, AtomicOrdering::Relaxed); + atomic_load_harness!(harness_intrinsic_atomic_load_acquire, AtomicOrdering::Acquire); + atomic_load_harness!(harness_intrinsic_atomic_load_seqcst, AtomicOrdering::SeqCst); + + // Unary RMW operations (swap, xchg): integer and pointer T. + macro_rules! atomic_rmw_call { + ($ty:ty, $wrapper:ident, $ord:path) => {{ + let mut dst: $ty = kani::any(); + let val: $ty = kani::any(); + let _ = unsafe { $wrapper::<$ty, { $ord }>(&mut dst, val) }; + }}; + } + macro_rules! atomic_rmw_harness { + ($name:ident, $wrapper:ident, $ord:path) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + atomic_integer_types!(atomic_rmw_call, $wrapper, $ord); + #[cfg(target_has_atomic = "ptr")] + { + let mut dst: *mut u8 = kani::any::() as *mut u8; + let val: *mut u8 = kani::any::() as *mut u8; + let _ = unsafe { $wrapper::<*mut u8, { $ord }>(&mut dst, val) }; + } + kani::cover(true, "atomic intrinsic exchange: reached after call"); + } + }; + } + macro_rules! atomic_rmw_orders { + ($wrapper:ident, $relaxed:ident, $acquire:ident, $release:ident, $acqrel:ident, $seqcst:ident) => { + atomic_rmw_harness!($relaxed, $wrapper, AtomicOrdering::Relaxed); + atomic_rmw_harness!($acquire, $wrapper, AtomicOrdering::Acquire); + atomic_rmw_harness!($release, $wrapper, AtomicOrdering::Release); + atomic_rmw_harness!($acqrel, $wrapper, AtomicOrdering::AcqRel); + atomic_rmw_harness!($seqcst, $wrapper, AtomicOrdering::SeqCst); + }; + } + atomic_rmw_orders!( + atomic_xchg_wrapper, + harness_intrinsic_atomic_xchg_relaxed, + harness_intrinsic_atomic_xchg_acquire, + harness_intrinsic_atomic_xchg_release, + harness_intrinsic_atomic_xchg_acqrel, + harness_intrinsic_atomic_xchg_seqcst + ); + + // Binary RMW operations: U == T for integer T, and U == usize for pointer T. + macro_rules! atomic_binary_call { + ($ty:ty, $wrapper:ident, $ord:path) => {{ + let mut dst: $ty = kani::any(); + let val: $ty = kani::any(); + let _ = unsafe { $wrapper::<$ty, $ty, { $ord }>(&mut dst, val) }; + }}; + } + macro_rules! atomic_binary_harness { + ($name:ident, $wrapper:ident, $ord:path) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + atomic_integer_types!(atomic_binary_call, $wrapper, $ord); + #[cfg(target_has_atomic = "ptr")] + { + let mut dst: *mut u8 = kani::any::() as *mut u8; + let val: usize = kani::any(); + let _ = unsafe { $wrapper::<*mut u8, usize, { $ord }>(&mut dst, val) }; + } + kani::cover(true, "atomic intrinsic binary RMW: reached after call"); + } + }; + } + macro_rules! atomic_binary_orders { + ($wrapper:ident, $relaxed:ident, $acquire:ident, $release:ident, $acqrel:ident, $seqcst:ident) => { + atomic_binary_harness!($relaxed, $wrapper, AtomicOrdering::Relaxed); + atomic_binary_harness!($acquire, $wrapper, AtomicOrdering::Acquire); + atomic_binary_harness!($release, $wrapper, AtomicOrdering::Release); + atomic_binary_harness!($acqrel, $wrapper, AtomicOrdering::AcqRel); + atomic_binary_harness!($seqcst, $wrapper, AtomicOrdering::SeqCst); + }; + } + atomic_binary_orders!( + atomic_xadd_wrapper, + harness_intrinsic_atomic_xadd_relaxed, + harness_intrinsic_atomic_xadd_acquire, + harness_intrinsic_atomic_xadd_release, + harness_intrinsic_atomic_xadd_acqrel, + harness_intrinsic_atomic_xadd_seqcst + ); + atomic_binary_orders!( + atomic_xsub_wrapper, + harness_intrinsic_atomic_xsub_relaxed, + harness_intrinsic_atomic_xsub_acquire, + harness_intrinsic_atomic_xsub_release, + harness_intrinsic_atomic_xsub_acqrel, + harness_intrinsic_atomic_xsub_seqcst + ); + atomic_binary_orders!( + atomic_and_wrapper, + harness_intrinsic_atomic_and_relaxed, + harness_intrinsic_atomic_and_acquire, + harness_intrinsic_atomic_and_release, + harness_intrinsic_atomic_and_acqrel, + harness_intrinsic_atomic_and_seqcst + ); + atomic_binary_orders!( + atomic_nand_wrapper, + harness_intrinsic_atomic_nand_relaxed, + harness_intrinsic_atomic_nand_acquire, + harness_intrinsic_atomic_nand_release, + harness_intrinsic_atomic_nand_acqrel, + harness_intrinsic_atomic_nand_seqcst + ); + atomic_binary_orders!( + atomic_or_wrapper, + harness_intrinsic_atomic_or_relaxed, + harness_intrinsic_atomic_or_acquire, + harness_intrinsic_atomic_or_release, + harness_intrinsic_atomic_or_acqrel, + harness_intrinsic_atomic_or_seqcst + ); + atomic_binary_orders!( + atomic_xor_wrapper, + harness_intrinsic_atomic_xor_relaxed, + harness_intrinsic_atomic_xor_acquire, + harness_intrinsic_atomic_xor_release, + harness_intrinsic_atomic_xor_acqrel, + harness_intrinsic_atomic_xor_seqcst + ); + + // Signed and unsigned extrema have the restricted T matrices documented by + // atomic_max/min and atomic_umax/umin respectively. + macro_rules! atomic_extremum_call { + ($ty:ty, $wrapper:ident, $ord:path) => {{ + let mut dst: $ty = kani::any(); + let val: $ty = kani::any(); + let _ = unsafe { $wrapper::<$ty, { $ord }>(&mut dst, val) }; + }}; + } + macro_rules! atomic_extremum_harness { + ($name:ident, $wrapper:ident, $types:ident, $ord:path) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + $types!(atomic_extremum_call, $wrapper, $ord); + kani::cover(true, "atomic intrinsic extremum: reached after call"); + } + }; + } + macro_rules! atomic_extremum_orders { + ($wrapper:ident, $types:ident, $relaxed:ident, $acquire:ident, $release:ident, $acqrel:ident, $seqcst:ident) => { + atomic_extremum_harness!($relaxed, $wrapper, $types, AtomicOrdering::Relaxed); + atomic_extremum_harness!($acquire, $wrapper, $types, AtomicOrdering::Acquire); + atomic_extremum_harness!($release, $wrapper, $types, AtomicOrdering::Release); + atomic_extremum_harness!($acqrel, $wrapper, $types, AtomicOrdering::AcqRel); + atomic_extremum_harness!($seqcst, $wrapper, $types, AtomicOrdering::SeqCst); + }; + } + atomic_extremum_orders!( + atomic_max_wrapper, + atomic_signed_types, + harness_intrinsic_atomic_max_relaxed, + harness_intrinsic_atomic_max_acquire, + harness_intrinsic_atomic_max_release, + harness_intrinsic_atomic_max_acqrel, + harness_intrinsic_atomic_max_seqcst + ); + atomic_extremum_orders!( + atomic_min_wrapper, + atomic_signed_types, + harness_intrinsic_atomic_min_relaxed, + harness_intrinsic_atomic_min_acquire, + harness_intrinsic_atomic_min_release, + harness_intrinsic_atomic_min_acqrel, + harness_intrinsic_atomic_min_seqcst + ); + atomic_extremum_orders!( + atomic_umax_wrapper, + atomic_unsigned_types, + harness_intrinsic_atomic_umax_relaxed, + harness_intrinsic_atomic_umax_acquire, + harness_intrinsic_atomic_umax_release, + harness_intrinsic_atomic_umax_acqrel, + harness_intrinsic_atomic_umax_seqcst + ); + atomic_extremum_orders!( + atomic_umin_wrapper, + atomic_unsigned_types, + harness_intrinsic_atomic_umin_relaxed, + harness_intrinsic_atomic_umin_acquire, + harness_intrinsic_atomic_umin_release, + harness_intrinsic_atomic_umin_acqrel, + harness_intrinsic_atomic_umin_seqcst + ); + + // Compare exchange uses all integer/pointer T types for every legal + // success/failure ordering pair. Failure orderings are exactly the three + // values listed in the intrinsic documentation. + macro_rules! atomic_cxchg_call { + ($ty:ty, $wrapper:ident, $succ:path, $fail:path) => {{ + let mut dst: $ty = kani::any(); + let old: $ty = kani::any(); + let new: $ty = kani::any(); + let _ = unsafe { $wrapper::<$ty, { $succ }, { $fail }>(&mut dst, old, new) }; + }}; + } + macro_rules! atomic_cxchg_harness { + ($name:ident, $wrapper:ident, $succ:path, $fail:path) => { + #[kani::proof_for_contract($wrapper)] + fn $name() { + atomic_integer_types!(atomic_cxchg_call, $wrapper, $succ, $fail); + #[cfg(target_has_atomic = "ptr")] + { + let mut dst: *mut u8 = kani::any::() as *mut u8; + let old: *mut u8 = kani::any::() as *mut u8; + let new: *mut u8 = kani::any::() as *mut u8; + let _ = + unsafe { $wrapper::<*mut u8, { $succ }, { $fail }>(&mut dst, old, new) }; + } + kani::cover(true, "atomic intrinsic compare-exchange: reached after call"); + } + }; + } + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_relaxed_relaxed, + atomic_cxchg_wrapper, + AtomicOrdering::Relaxed, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_relaxed_acquire, + atomic_cxchg_wrapper, + AtomicOrdering::Relaxed, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_relaxed_seqcst, + atomic_cxchg_wrapper, + AtomicOrdering::Relaxed, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_acquire_relaxed, + atomic_cxchg_wrapper, + AtomicOrdering::Acquire, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_acquire_acquire, + atomic_cxchg_wrapper, + AtomicOrdering::Acquire, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_acquire_seqcst, + atomic_cxchg_wrapper, + AtomicOrdering::Acquire, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_release_relaxed, + atomic_cxchg_wrapper, + AtomicOrdering::Release, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_release_acquire, + atomic_cxchg_wrapper, + AtomicOrdering::Release, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_release_seqcst, + atomic_cxchg_wrapper, + AtomicOrdering::Release, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_acqrel_relaxed, + atomic_cxchg_wrapper, + AtomicOrdering::AcqRel, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_acqrel_acquire, + atomic_cxchg_wrapper, + AtomicOrdering::AcqRel, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_acqrel_seqcst, + atomic_cxchg_wrapper, + AtomicOrdering::AcqRel, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_seqcst_relaxed, + atomic_cxchg_wrapper, + AtomicOrdering::SeqCst, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_seqcst_acquire, + atomic_cxchg_wrapper, + AtomicOrdering::SeqCst, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchg_seqcst_seqcst, + atomic_cxchg_wrapper, + AtomicOrdering::SeqCst, + AtomicOrdering::SeqCst + ); + + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_relaxed_relaxed, + atomic_cxchgweak_wrapper, + AtomicOrdering::Relaxed, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_relaxed_acquire, + atomic_cxchgweak_wrapper, + AtomicOrdering::Relaxed, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_relaxed_seqcst, + atomic_cxchgweak_wrapper, + AtomicOrdering::Relaxed, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_acquire_relaxed, + atomic_cxchgweak_wrapper, + AtomicOrdering::Acquire, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_acquire_acquire, + atomic_cxchgweak_wrapper, + AtomicOrdering::Acquire, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_acquire_seqcst, + atomic_cxchgweak_wrapper, + AtomicOrdering::Acquire, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_release_relaxed, + atomic_cxchgweak_wrapper, + AtomicOrdering::Release, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_release_acquire, + atomic_cxchgweak_wrapper, + AtomicOrdering::Release, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_release_seqcst, + atomic_cxchgweak_wrapper, + AtomicOrdering::Release, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_acqrel_relaxed, + atomic_cxchgweak_wrapper, + AtomicOrdering::AcqRel, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_acqrel_acquire, + atomic_cxchgweak_wrapper, + AtomicOrdering::AcqRel, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_acqrel_seqcst, + atomic_cxchgweak_wrapper, + AtomicOrdering::AcqRel, + AtomicOrdering::SeqCst + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_seqcst_relaxed, + atomic_cxchgweak_wrapper, + AtomicOrdering::SeqCst, + AtomicOrdering::Relaxed + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_seqcst_acquire, + atomic_cxchgweak_wrapper, + AtomicOrdering::SeqCst, + AtomicOrdering::Acquire + ); + atomic_cxchg_harness!( + harness_intrinsic_atomic_cxchgweak_seqcst_seqcst, + atomic_cxchgweak_wrapper, + AtomicOrdering::SeqCst, + AtomicOrdering::SeqCst + ); } diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs index 0c5552a0b81cc..4f54cfc3efcf2 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::{ensures, 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 {} @@ -571,6 +577,12 @@ impl AtomicBool { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + #[requires(ptr.cast::().is_aligned())] + #[requires(ub_checks::can_dereference(ptr))] + #[requires(ub_checks::can_write(ptr))] + #[ensures(|result: &&AtomicBool| { + core::ptr::eq(*result, ptr.cast::()) + })] pub const unsafe fn from_ptr<'a>(ptr: *mut bool) -> &'a AtomicBool { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -721,6 +733,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 +763,8 @@ 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)] + #[cfg_attr(kani, kani::modifies(self))] 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. @@ -783,6 +798,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))] 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) } @@ -851,6 +867,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))] pub fn compare_and_swap(&self, current: bool, new: bool, order: Ordering) -> bool { match self.compare_exchange(current, new, order, strongest_failure_ordering(order)) { Ok(x) => x, @@ -913,6 +930,8 @@ 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 == Relaxed || failure == Acquire || failure == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn compare_exchange( &self, current: bool, @@ -1009,6 +1028,8 @@ 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 == Relaxed || failure == Acquire || failure == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn compare_exchange_weak( &self, current: bool, @@ -1066,6 +1087,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))] pub fn fetch_and(&self, val: bool, order: Ordering) -> bool { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_and(self.v.get(), val as u8, order) != 0 } @@ -1109,6 +1131,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))] pub fn fetch_nand(&self, val: bool, order: Ordering) -> bool { // We can't use atomic_nand here because it can result in a bool with // an invalid value. This happens because the atomic operation is done @@ -1162,6 +1185,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))] pub fn fetch_or(&self, val: bool, order: Ordering) -> bool { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_or(self.v.get(), val as u8, order) != 0 } @@ -1204,6 +1228,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))] pub fn fetch_xor(&self, val: bool, order: Ordering) -> bool { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_xor(self.v.get(), val as u8, order) != 0 } @@ -1242,6 +1267,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))] pub fn fetch_not(&self, order: Ordering) -> bool { self.fetch_xor(true, order) } @@ -1335,6 +1361,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn fetch_update( &self, set_order: Ordering, @@ -1407,6 +1435,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn try_update( &self, set_order: Ordering, @@ -1466,6 +1496,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn update( &self, set_order: Ordering, @@ -1543,6 +1575,12 @@ impl AtomicPtr { #[inline] #[stable(feature = "atomic_from_ptr", since = "1.75.0")] #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")] + #[requires(ptr.cast::>().is_aligned())] + #[requires(ub_checks::can_dereference(ptr))] + #[requires(ub_checks::can_write(ptr))] + #[ensures(|result: &&AtomicPtr| { + core::ptr::eq(*result, ptr.cast::>()) + })] pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -1720,6 +1758,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 +1789,8 @@ 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)] + #[cfg_attr(kani, kani::modifies(self))] pub fn store(&self, ptr: *mut T, order: Ordering) { // SAFETY: data races are prevented by atomic intrinsics. unsafe { @@ -1784,6 +1825,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))] pub fn swap(&self, ptr: *mut T, order: Ordering) -> *mut T { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_swap(self.p.get(), ptr, order) } @@ -1847,6 +1889,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))] pub fn compare_and_swap(&self, current: *mut T, new: *mut T, order: Ordering) -> *mut T { match self.compare_exchange(current, new, order, strongest_failure_ordering(order)) { Ok(x) => x, @@ -1902,6 +1945,8 @@ 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 == Relaxed || failure == Acquire || failure == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn compare_exchange( &self, current: *mut T, @@ -1966,6 +2011,8 @@ 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 == Relaxed || failure == Acquire || failure == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn compare_exchange_weak( &self, current: *mut T, @@ -2040,6 +2087,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn fetch_update( &self, set_order: Ordering, @@ -2121,6 +2170,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn try_update( &self, set_order: Ordering, @@ -2185,6 +2236,8 @@ impl AtomicPtr { #[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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn update( &self, set_order: Ordering, @@ -2404,6 +2457,7 @@ impl AtomicPtr { #[stable(feature = "strict_provenance_atomic_ptr", since = "1.91.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))] pub fn fetch_or(&self, val: usize, order: Ordering) -> *mut T { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_or(self.p.get(), val, order).cast() } @@ -2454,6 +2508,7 @@ impl AtomicPtr { #[stable(feature = "strict_provenance_atomic_ptr", since = "1.91.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))] pub fn fetch_and(&self, val: usize, order: Ordering) -> *mut T { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_and(self.p.get(), val, order).cast() } @@ -2502,6 +2557,7 @@ impl AtomicPtr { #[stable(feature = "strict_provenance_atomic_ptr", since = "1.91.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))] pub fn fetch_xor(&self, val: usize, order: Ordering) -> *mut T { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_xor(self.p.get(), val, order).cast() } @@ -2738,6 +2794,19 @@ 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")] + #[requires(ptr.cast::<$atomic_type>().is_aligned())] + #[requires(!ptr.is_null())] + #[requires(ub_checks::can_dereference(ptr))] + #[requires(ub_checks::can_write(ptr))] + #[ensures(|result: &&$atomic_type| { + core::ptr::eq(*result, ptr.cast::<$atomic_type>()) + })] + #[ensures(|result: &&$atomic_type| { + ub_checks::can_dereference(*result as *const $atomic_type) + })] + #[ensures(|result: &&$atomic_type| { + ub_checks::can_write((*result).as_ptr()) + })] pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type { // SAFETY: guaranteed by the caller unsafe { &*ptr.cast() } @@ -2915,6 +2984,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 +3013,8 @@ 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)] + #[cfg_attr(kani, kani::modifies(self))] 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); } @@ -2972,6 +3044,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))] pub fn swap(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_swap(self.v.get(), val, order) } @@ -3037,6 +3110,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))] pub fn compare_and_swap(&self, current: $int_type, new: $int_type, @@ -3106,6 +3180,8 @@ 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 == Relaxed || failure == Acquire || failure == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn compare_exchange(&self, current: $int_type, new: $int_type, @@ -3170,6 +3246,8 @@ 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 == Relaxed || failure == Acquire || failure == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn compare_exchange_weak(&self, current: $int_type, new: $int_type, @@ -3207,6 +3285,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))] pub fn fetch_add(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_add(self.v.get(), val, order) } @@ -3238,6 +3317,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))] pub fn fetch_sub(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_sub(self.v.get(), val, order) } @@ -3272,6 +3352,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))] pub fn fetch_and(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_and(self.v.get(), val, order) } @@ -3306,6 +3387,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))] pub fn fetch_nand(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_nand(self.v.get(), val, order) } @@ -3340,6 +3422,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))] pub fn fetch_or(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_or(self.v.get(), val, order) } @@ -3374,6 +3457,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))] pub fn fetch_xor(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { atomic_xor(self.v.get(), val, order) } @@ -3429,6 +3513,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn fetch_update(&self, set_order: Ordering, fetch_order: Ordering, @@ -3497,6 +3583,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn try_update( &self, set_order: Ordering, @@ -3559,6 +3647,8 @@ 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(fetch_order == Relaxed || fetch_order == Acquire || fetch_order == SeqCst)] + #[cfg_attr(kani, kani::modifies(self))] pub fn update( &self, set_order: Ordering, @@ -3614,6 +3704,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))] pub fn fetch_max(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { $max_fn(self.v.get(), val, order) } @@ -3661,6 +3752,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))] pub fn fetch_min(&self, val: $int_type, order: Ordering) -> $int_type { // SAFETY: data races are prevented by atomic intrinsics. unsafe { $min_fn(self.v.get(), val, order) } @@ -3985,6 +4077,11 @@ 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)] +#[ensures(|_| ub_checks::can_dereference(dst as *const T))] +#[ensures(|_| 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 { @@ -4000,6 +4097,9 @@ 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)] +#[ensures(|_| 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 { @@ -4016,6 +4116,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4139,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4162,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4187,13 @@ 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)] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst) +})] pub unsafe fn atomic_compare_exchange( dst: *mut T, old: T, @@ -4134,6 +4259,13 @@ 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)] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst) +})] unsafe fn atomic_compare_exchange_weak( dst: *mut T, old: T, @@ -4199,6 +4331,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4353,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4375,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4397,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4420,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 { @@ -4298,6 +4460,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4483,12 @@ 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))] +#[ensures(|_| { + ub_checks::can_dereference(dst as *const T) && 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 +4783,1233 @@ impl fmt::Pointer for AtomicPtr { pub fn spin_loop_hint() { spin_loop() } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Generate candidates across the allocation. Contract proofs assume the callee's + // preconditions, retaining only initialized, aligned, readable, and writable offsets. + fn ptr_at_offset(buf: &mut [u8; 100]) -> *mut T { + let offset = kani::any_where(|offset: &usize| *offset < 100); + buf.as_mut_ptr().wrapping_add(offset).cast::() + } + + fn any_ordering() -> Ordering { + match kani::any::() { + 0 => Relaxed, + 1 => Release, + 2 => Acquire, + 3 => AcqRel, + _ => SeqCst, + } + } + + // Part 1: from_ptr. + #[cfg(target_has_atomic_load_store = "8")] + #[kani::proof_for_contract(AtomicBool::from_ptr)] + pub fn harness_atomic_bool_from_ptr() { + let mut buf: [bool; 100] = kani::any(); + let offset = kani::any_where(|offset: &usize| *offset < 100); + let ptr = buf.as_mut_ptr().wrapping_add(offset); + + let _ = unsafe { AtomicBool::from_ptr(ptr) }; + kani::cover(true, "AtomicBool::from_ptr: reached after call"); + } + + // Harnesses for integer Atomic*::from_ptr functions. + macro_rules! from_ptr_harness { + ($name:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract(<$atomic>::from_ptr)] + pub fn $name() { + let mut buf: [u8; 100] = kani::any(); + let ptr = ptr_at_offset::<$value>(&mut buf); + + let _ = unsafe { <$atomic>::from_ptr(ptr) }; + kani::cover(true, "integer from_ptr: reached after call"); + } + }; + } + + #[cfg(target_has_atomic_load_store = "8")] + from_ptr_harness!(harness_atomic_i8_from_ptr, AtomicI8, i8); + #[cfg(target_has_atomic_load_store = "8")] + from_ptr_harness!(harness_atomic_u8_from_ptr, AtomicU8, u8); + #[cfg(target_has_atomic_load_store = "16")] + from_ptr_harness!(harness_atomic_i16_from_ptr, AtomicI16, i16); + #[cfg(target_has_atomic_load_store = "16")] + from_ptr_harness!(harness_atomic_u16_from_ptr, AtomicU16, u16); + #[cfg(target_has_atomic_load_store = "32")] + from_ptr_harness!(harness_atomic_i32_from_ptr, AtomicI32, i32); + #[cfg(target_has_atomic_load_store = "32")] + from_ptr_harness!(harness_atomic_u32_from_ptr, AtomicU32, u32); + #[cfg(target_has_atomic_load_store = "64")] + from_ptr_harness!(harness_atomic_i64_from_ptr, AtomicI64, i64); + #[cfg(target_has_atomic_load_store = "64")] + from_ptr_harness!(harness_atomic_u64_from_ptr, AtomicU64, u64); + #[cfg(target_has_atomic_load_store = "128")] + from_ptr_harness!(harness_atomic_i128_from_ptr, AtomicI128, i128); + #[cfg(target_has_atomic_load_store = "128")] + from_ptr_harness!(harness_atomic_u128_from_ptr, AtomicU128, u128); + + // Harnesses for AtomicPtr::from_ptr. + macro_rules! atomic_ptr_from_ptr_harness { + ($name:ident, $pointee:ty) => { + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(AtomicPtr::<$pointee>::from_ptr)] + pub fn $name() { + // The stored pointer is arbitrary; the outer pointer targets valid local storage. + let mut value = kani::any::() as *mut $pointee; + let ptr = &mut value as *mut *mut $pointee; + + let _ = unsafe { AtomicPtr::<$pointee>::from_ptr(ptr) }; + kani::cover(true, "AtomicPtr::from_ptr: reached after call"); + } + }; + } + + // Cover pointee sizes 0, 1, 2, 4, and the non-power-of-two size 3. + atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_unit, ()); + atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u8, u8); + atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u16, u16); + atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u32, u32); + atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u8_3, [u8; 3]); + + // Part 2: unsafe atomic helpers. + // Harnesses for atomic_store. + macro_rules! store_harness { + ($name:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract(atomic_store::<$value>)] + pub fn $name() { + let initial: $value = kani::any(); + let storage = <$atomic>::new(initial); + let val: $value = kani::any(); + + unsafe { atomic_store(storage.as_ptr(), val, any_ordering()) }; + kani::cover(true, "atomic_store: reached after call"); + } + }; + } + + #[cfg(target_has_atomic_load_store = "8")] + store_harness!(harness_atomic_store_i8, AtomicI8, i8); + #[cfg(target_has_atomic_load_store = "8")] + store_harness!(harness_atomic_store_u8, AtomicU8, u8); + #[cfg(target_has_atomic_load_store = "16")] + store_harness!(harness_atomic_store_i16, AtomicI16, i16); + #[cfg(target_has_atomic_load_store = "16")] + store_harness!(harness_atomic_store_u16, AtomicU16, u16); + #[cfg(target_has_atomic_load_store = "32")] + store_harness!(harness_atomic_store_i32, AtomicI32, i32); + #[cfg(target_has_atomic_load_store = "32")] + store_harness!(harness_atomic_store_u32, AtomicU32, u32); + #[cfg(target_has_atomic_load_store = "64")] + store_harness!(harness_atomic_store_i64, AtomicI64, i64); + #[cfg(target_has_atomic_load_store = "64")] + store_harness!(harness_atomic_store_u64, AtomicU64, u64); + #[cfg(target_has_atomic_load_store = "128")] + store_harness!(harness_atomic_store_i128, AtomicI128, i128); + #[cfg(target_has_atomic_load_store = "128")] + store_harness!(harness_atomic_store_u128, AtomicU128, u128); + #[cfg(target_has_atomic_load_store = "ptr")] + store_harness!(harness_atomic_store_isize, AtomicIsize, isize); + #[cfg(target_has_atomic_load_store = "ptr")] + store_harness!(harness_atomic_store_usize, AtomicUsize, usize); + + // Pointer harnesses for atomic_store. + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(atomic_store::<*mut u8>)] + pub fn harness_atomic_store_ptr() { + let initial = kani::any::() as *mut u8; + let storage = AtomicPtr::::new(initial); + let val = kani::any::() as *mut u8; + + unsafe { atomic_store(storage.as_ptr(), val, any_ordering()) }; + kani::cover(true, "atomic_store: reached after call"); + } + + // Harnesses for atomic_load. + macro_rules! load_harness { + ($name:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract(atomic_load::<$value>)] + pub fn $name() { + let initial: $value = kani::any(); + let storage = <$atomic>::new(initial); + + let _ = unsafe { atomic_load(storage.as_ptr().cast_const(), any_ordering()) }; + kani::cover(true, "atomic_load: reached after call"); + } + }; + } + + // Load helpers. + #[cfg(target_has_atomic_load_store = "8")] + load_harness!(harness_atomic_load_i8, AtomicI8, i8); + #[cfg(target_has_atomic_load_store = "8")] + load_harness!(harness_atomic_load_u8, AtomicU8, u8); + #[cfg(target_has_atomic_load_store = "16")] + load_harness!(harness_atomic_load_i16, AtomicI16, i16); + #[cfg(target_has_atomic_load_store = "16")] + load_harness!(harness_atomic_load_u16, AtomicU16, u16); + #[cfg(target_has_atomic_load_store = "32")] + load_harness!(harness_atomic_load_i32, AtomicI32, i32); + #[cfg(target_has_atomic_load_store = "32")] + load_harness!(harness_atomic_load_u32, AtomicU32, u32); + #[cfg(target_has_atomic_load_store = "64")] + load_harness!(harness_atomic_load_i64, AtomicI64, i64); + #[cfg(target_has_atomic_load_store = "64")] + load_harness!(harness_atomic_load_u64, AtomicU64, u64); + #[cfg(target_has_atomic_load_store = "128")] + load_harness!(harness_atomic_load_i128, AtomicI128, i128); + #[cfg(target_has_atomic_load_store = "128")] + load_harness!(harness_atomic_load_u128, AtomicU128, u128); + #[cfg(target_has_atomic_load_store = "ptr")] + load_harness!(harness_atomic_load_isize, AtomicIsize, isize); + #[cfg(target_has_atomic_load_store = "ptr")] + load_harness!(harness_atomic_load_usize, AtomicUsize, usize); + + // Pointer harness for atomic_load. + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(atomic_load::<*mut u8>)] + pub fn harness_atomic_load_ptr_u8() { + let initial = kani::any::() as *mut u8; + let storage = AtomicPtr::::new(initial); + + let _ = unsafe { atomic_load(storage.as_ptr().cast_const(), any_ordering()) }; + kani::cover(true, "atomic_load: reached after call"); + } + + // Harnesses for atomic_swap, atomic_max, atomic_umax, and atomic_umin. + macro_rules! rmw_harness { + ($name:ident, $operation:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract($operation::<$value>)] + pub fn $name() { + let initial: $value = kani::any(); + let storage = <$atomic>::new(initial); + let val: $value = kani::any(); + + let _ = unsafe { $operation(storage.as_ptr(), val, any_ordering()) }; + kani::cover(true, "atomic_swap/max/umax/umin: reached after call"); + } + }; + } + + // Exchange helpers. + #[cfg(target_has_atomic = "8")] + rmw_harness!(harness_atomic_swap_i8, atomic_swap, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + rmw_harness!(harness_atomic_swap_u8, atomic_swap, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + rmw_harness!(harness_atomic_swap_i16, atomic_swap, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + rmw_harness!(harness_atomic_swap_u16, atomic_swap, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + rmw_harness!(harness_atomic_swap_i32, atomic_swap, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + rmw_harness!(harness_atomic_swap_u32, atomic_swap, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + rmw_harness!(harness_atomic_swap_i64, atomic_swap, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + rmw_harness!(harness_atomic_swap_u64, atomic_swap, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + rmw_harness!(harness_atomic_swap_i128, atomic_swap, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + rmw_harness!(harness_atomic_swap_u128, atomic_swap, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + rmw_harness!(harness_atomic_swap_isize, atomic_swap, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + rmw_harness!(harness_atomic_swap_usize, atomic_swap, AtomicUsize, usize); + + // Signed maximum helpers. + #[cfg(target_has_atomic = "8")] + rmw_harness!(harness_atomic_max_i8, atomic_max, AtomicI8, i8); + #[cfg(target_has_atomic = "16")] + rmw_harness!(harness_atomic_max_i16, atomic_max, AtomicI16, i16); + #[cfg(target_has_atomic = "32")] + rmw_harness!(harness_atomic_max_i32, atomic_max, AtomicI32, i32); + #[cfg(target_has_atomic = "64")] + rmw_harness!(harness_atomic_max_i64, atomic_max, AtomicI64, i64); + #[cfg(target_has_atomic = "128")] + rmw_harness!(harness_atomic_max_i128, atomic_max, AtomicI128, i128); + #[cfg(target_has_atomic = "ptr")] + rmw_harness!(harness_atomic_max_isize, atomic_max, AtomicIsize, isize); + + // Unsigned maximum helpers. + #[cfg(target_has_atomic = "8")] + rmw_harness!(harness_atomic_umax_u8, atomic_umax, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + rmw_harness!(harness_atomic_umax_u16, atomic_umax, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + rmw_harness!(harness_atomic_umax_u32, atomic_umax, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + rmw_harness!(harness_atomic_umax_u64, atomic_umax, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + rmw_harness!(harness_atomic_umax_u128, atomic_umax, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + rmw_harness!(harness_atomic_umax_usize, atomic_umax, AtomicUsize, usize); + + // Unsigned minimum helpers. + #[cfg(target_has_atomic = "8")] + rmw_harness!(harness_atomic_umin_u8, atomic_umin, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + rmw_harness!(harness_atomic_umin_u16, atomic_umin, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + rmw_harness!(harness_atomic_umin_u32, atomic_umin, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + rmw_harness!(harness_atomic_umin_u64, atomic_umin, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + rmw_harness!(harness_atomic_umin_u128, atomic_umin, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + rmw_harness!(harness_atomic_umin_usize, atomic_umin, AtomicUsize, usize); + + // Pointer harnesses for atomic_swap. + #[cfg(target_has_atomic = "ptr")] + #[kani::proof_for_contract(atomic_swap::<*mut u8>)] + pub fn harness_atomic_swap_ptr() { + let initial = kani::any::() as *mut u8; + let storage = AtomicPtr::::new(initial); + let val = kani::any::() as *mut u8; + + let _ = unsafe { atomic_swap(storage.as_ptr(), val, any_ordering()) }; + kani::cover(true, "atomic_swap: reached after call"); + } + + // Harnesses for atomic_add, atomic_sub, atomic_and, atomic_nand, atomic_or, and atomic_xor. + macro_rules! binary_rmw_harness { + ($name:ident, $operation:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract($operation::<$value, $value>)] + pub fn $name() { + let initial: $value = kani::any(); + let storage = <$atomic>::new(initial); + let val: $value = kani::any(); + + let _ = unsafe { $operation(storage.as_ptr(), val, any_ordering()) }; + kani::cover(true, "atomic_add/sub/and/nand/or/xor: reached after call"); + } + }; + } + + // Pointer versions use a usize operand; raw pointers do not implement kani::Arbitrary. + macro_rules! binary_rmw_ptr_harness { + ($name:ident, $operation:ident, $pointee:ty) => { + #[kani::proof_for_contract($operation::<*mut $pointee, usize>)] + pub fn $name() { + let initial = kani::any::() as *mut $pointee; + let storage = AtomicPtr::<$pointee>::new(initial); + let val: usize = kani::any(); + + let _ = unsafe { $operation(storage.as_ptr(), val, any_ordering()) }; + kani::cover(true, "atomic pointer binary RMW: reached after call"); + } + }; + } + + // Add helpers. + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_add_i8, atomic_add, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_add_u8, atomic_add, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_add_i16, atomic_add, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_add_u16, atomic_add, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_add_i32, atomic_add, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_add_u32, atomic_add, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_add_i64, atomic_add, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_add_u64, atomic_add, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_add_i128, atomic_add, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_add_u128, atomic_add, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_add_isize, atomic_add, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_add_usize, atomic_add, AtomicUsize, usize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_ptr_harness!(harness_atomic_add_ptr, atomic_add, u8); + + // Subtract helpers. + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_sub_i8, atomic_sub, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_sub_u8, atomic_sub, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_sub_i16, atomic_sub, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_sub_u16, atomic_sub, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_sub_i32, atomic_sub, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_sub_u32, atomic_sub, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_sub_i64, atomic_sub, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_sub_u64, atomic_sub, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_sub_i128, atomic_sub, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_sub_u128, atomic_sub, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_sub_isize, atomic_sub, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_sub_usize, atomic_sub, AtomicUsize, usize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_ptr_harness!(harness_atomic_sub_ptr, atomic_sub, u8); + + // Bitwise AND helpers. + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_and_i8, atomic_and, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_and_u8, atomic_and, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_and_i16, atomic_and, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_and_u16, atomic_and, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_and_i32, atomic_and, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_and_u32, atomic_and, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_and_i64, atomic_and, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_and_u64, atomic_and, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_and_i128, atomic_and, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_and_u128, atomic_and, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_and_isize, atomic_and, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_and_usize, atomic_and, AtomicUsize, usize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_ptr_harness!(harness_atomic_and_ptr, atomic_and, u8); + + // Bitwise NAND helpers. + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_nand_i8, atomic_nand, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_nand_u8, atomic_nand, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_nand_i16, atomic_nand, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_nand_u16, atomic_nand, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_nand_i32, atomic_nand, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_nand_u32, atomic_nand, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_nand_i64, atomic_nand, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_nand_u64, atomic_nand, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_nand_i128, atomic_nand, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_nand_u128, atomic_nand, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_nand_isize, atomic_nand, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_nand_usize, atomic_nand, AtomicUsize, usize); + + // Bitwise OR helpers. + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_or_i8, atomic_or, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_or_u8, atomic_or, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_or_i16, atomic_or, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_or_u16, atomic_or, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_or_i32, atomic_or, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_or_u32, atomic_or, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_or_i64, atomic_or, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_or_u64, atomic_or, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_or_i128, atomic_or, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_or_u128, atomic_or, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_or_isize, atomic_or, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_or_usize, atomic_or, AtomicUsize, usize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_ptr_harness!(harness_atomic_or_ptr, atomic_or, u8); + + // Bitwise XOR helpers. + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_xor_i8, atomic_xor, AtomicI8, i8); + #[cfg(target_has_atomic = "8")] + binary_rmw_harness!(harness_atomic_xor_u8, atomic_xor, AtomicU8, u8); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_xor_i16, atomic_xor, AtomicI16, i16); + #[cfg(target_has_atomic = "16")] + binary_rmw_harness!(harness_atomic_xor_u16, atomic_xor, AtomicU16, u16); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_xor_i32, atomic_xor, AtomicI32, i32); + #[cfg(target_has_atomic = "32")] + binary_rmw_harness!(harness_atomic_xor_u32, atomic_xor, AtomicU32, u32); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_xor_i64, atomic_xor, AtomicI64, i64); + #[cfg(target_has_atomic = "64")] + binary_rmw_harness!(harness_atomic_xor_u64, atomic_xor, AtomicU64, u64); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_xor_i128, atomic_xor, AtomicI128, i128); + #[cfg(target_has_atomic = "128")] + binary_rmw_harness!(harness_atomic_xor_u128, atomic_xor, AtomicU128, u128); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_xor_isize, atomic_xor, AtomicIsize, isize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_harness!(harness_atomic_xor_usize, atomic_xor, AtomicUsize, usize); + #[cfg(target_has_atomic = "ptr")] + binary_rmw_ptr_harness!(harness_atomic_xor_ptr, atomic_xor, u8); + + // Harnesses for atomic_compare_exchange and atomic_compare_exchange_weak. + macro_rules! compare_exchange_harness { + ($name:ident, $operation:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract($operation::<$value>)] + pub fn $name() { + let initial: $value = kani::any(); + let storage = <$atomic>::new(initial); + let old: $value = kani::any(); + let new: $value = kani::any(); + + let _ = unsafe { + $operation(storage.as_ptr(), old, new, any_ordering(), any_ordering()) + }; + kani::cover(true, "atomic_compare_exchange/weak: reached after call"); + } + }; + } + + // Strong compare-exchange helpers. + #[cfg(target_has_atomic = "8")] + compare_exchange_harness!( + harness_atomic_compare_exchange_i8, + atomic_compare_exchange, + AtomicI8, + i8 + ); + #[cfg(target_has_atomic = "8")] + compare_exchange_harness!( + harness_atomic_compare_exchange_u8, + atomic_compare_exchange, + AtomicU8, + u8 + ); + #[cfg(target_has_atomic = "16")] + compare_exchange_harness!( + harness_atomic_compare_exchange_i16, + atomic_compare_exchange, + AtomicI16, + i16 + ); + #[cfg(target_has_atomic = "16")] + compare_exchange_harness!( + harness_atomic_compare_exchange_u16, + atomic_compare_exchange, + AtomicU16, + u16 + ); + #[cfg(target_has_atomic = "32")] + compare_exchange_harness!( + harness_atomic_compare_exchange_i32, + atomic_compare_exchange, + AtomicI32, + i32 + ); + #[cfg(target_has_atomic = "32")] + compare_exchange_harness!( + harness_atomic_compare_exchange_u32, + atomic_compare_exchange, + AtomicU32, + u32 + ); + #[cfg(target_has_atomic = "64")] + compare_exchange_harness!( + harness_atomic_compare_exchange_i64, + atomic_compare_exchange, + AtomicI64, + i64 + ); + #[cfg(target_has_atomic = "64")] + compare_exchange_harness!( + harness_atomic_compare_exchange_u64, + atomic_compare_exchange, + AtomicU64, + u64 + ); + #[cfg(target_has_atomic = "128")] + compare_exchange_harness!( + harness_atomic_compare_exchange_i128, + atomic_compare_exchange, + AtomicI128, + i128 + ); + #[cfg(target_has_atomic = "128")] + compare_exchange_harness!( + harness_atomic_compare_exchange_u128, + atomic_compare_exchange, + AtomicU128, + u128 + ); + #[cfg(target_has_atomic = "ptr")] + compare_exchange_harness!( + harness_atomic_compare_exchange_isize, + atomic_compare_exchange, + AtomicIsize, + isize + ); + #[cfg(target_has_atomic = "ptr")] + compare_exchange_harness!( + harness_atomic_compare_exchange_usize, + atomic_compare_exchange, + AtomicUsize, + usize + ); + + // Weak compare-exchange helpers. + #[cfg(target_has_atomic = "8")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_i8, + atomic_compare_exchange_weak, + AtomicI8, + i8 + ); + #[cfg(target_has_atomic = "8")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_u8, + atomic_compare_exchange_weak, + AtomicU8, + u8 + ); + #[cfg(target_has_atomic = "16")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_i16, + atomic_compare_exchange_weak, + AtomicI16, + i16 + ); + #[cfg(target_has_atomic = "16")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_u16, + atomic_compare_exchange_weak, + AtomicU16, + u16 + ); + #[cfg(target_has_atomic = "32")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_i32, + atomic_compare_exchange_weak, + AtomicI32, + i32 + ); + #[cfg(target_has_atomic = "32")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_u32, + atomic_compare_exchange_weak, + AtomicU32, + u32 + ); + #[cfg(target_has_atomic = "64")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_i64, + atomic_compare_exchange_weak, + AtomicI64, + i64 + ); + #[cfg(target_has_atomic = "64")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_u64, + atomic_compare_exchange_weak, + AtomicU64, + u64 + ); + #[cfg(target_has_atomic = "128")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_i128, + atomic_compare_exchange_weak, + AtomicI128, + i128 + ); + #[cfg(target_has_atomic = "128")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_u128, + atomic_compare_exchange_weak, + AtomicU128, + u128 + ); + #[cfg(target_has_atomic = "ptr")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_isize, + atomic_compare_exchange_weak, + AtomicIsize, + isize + ); + #[cfg(target_has_atomic = "ptr")] + compare_exchange_harness!( + harness_atomic_compare_exchange_weak_usize, + atomic_compare_exchange_weak, + AtomicUsize, + usize + ); + + // Pointer harnesses for atomic_compare_exchange and atomic_compare_exchange_weak. + macro_rules! compare_exchange_ptr_harness { + ($name:ident, $operation:ident, $pointee:ty) => { + #[kani::proof_for_contract($operation::<*mut $pointee>)] + pub fn $name() { + let initial = kani::any::() as *mut $pointee; + let storage = AtomicPtr::<$pointee>::new(initial); + let old = kani::any::() as *mut $pointee; + let new = kani::any::() as *mut $pointee; + + let _ = unsafe { + $operation(storage.as_ptr(), old, new, any_ordering(), any_ordering()) + }; + kani::cover(true, "atomic_compare_exchange/weak: reached after call"); + } + }; + } + + #[cfg(target_has_atomic = "ptr")] + compare_exchange_ptr_harness!(harness_atomic_compare_exchange_ptr, atomic_compare_exchange, u8); + #[cfg(target_has_atomic = "ptr")] + compare_exchange_ptr_harness!( + harness_atomic_compare_exchange_weak_ptr, + atomic_compare_exchange_weak, + u8 + ); + + // Part 2 (optional): safe atomic abstractions and ordering contracts. + fn any_load_order() -> Ordering { + match kani::any::() % 3 { + 0 => Relaxed, + 1 => Acquire, + _ => SeqCst, + } + } + + fn any_store_order() -> Ordering { + match kani::any::() % 3 { + 0 => Relaxed, + 1 => Release, + _ => SeqCst, + } + } + + fn any_failure_order() -> Ordering { + any_load_order() + } + + // Harnesses for load and store methods of atomic types, with safe abstractions. + macro_rules! safe_load_store_harness { + ($load_name:ident, $store_name:ident, $atomic:ty, $value:ty) => { + #[kani::proof_for_contract(<$atomic>::load)] + pub fn $load_name() { + let storage = <$atomic>::new(kani::any::<$value>()); + let _ = storage.load(any_load_order()); + kani::cover(true, "safe atomic load: reached after call"); + } + + #[kani::proof_for_contract(<$atomic>::store)] + pub fn $store_name() { + let storage = <$atomic>::new(kani::any::<$value>()); + storage.store(kani::any::<$value>(), any_store_order()); + kani::cover(true, "safe atomic store: reached after call"); + } + }; + } + + #[cfg(target_has_atomic_load_store = "8")] + safe_load_store_harness!(harness_safe_load_bool, harness_safe_store_bool, AtomicBool, bool); + #[cfg(target_has_atomic_load_store = "8")] + safe_load_store_harness!(harness_safe_load_i8, harness_safe_store_i8, AtomicI8, i8); + #[cfg(target_has_atomic_load_store = "8")] + safe_load_store_harness!(harness_safe_load_u8, harness_safe_store_u8, AtomicU8, u8); + #[cfg(target_has_atomic_load_store = "16")] + safe_load_store_harness!(harness_safe_load_i16, harness_safe_store_i16, AtomicI16, i16); + #[cfg(target_has_atomic_load_store = "16")] + safe_load_store_harness!(harness_safe_load_u16, harness_safe_store_u16, AtomicU16, u16); + #[cfg(target_has_atomic_load_store = "32")] + safe_load_store_harness!(harness_safe_load_i32, harness_safe_store_i32, AtomicI32, i32); + #[cfg(target_has_atomic_load_store = "32")] + safe_load_store_harness!(harness_safe_load_u32, harness_safe_store_u32, AtomicU32, u32); + #[cfg(target_has_atomic_load_store = "64")] + safe_load_store_harness!(harness_safe_load_i64, harness_safe_store_i64, AtomicI64, i64); + #[cfg(target_has_atomic_load_store = "64")] + safe_load_store_harness!(harness_safe_load_u64, harness_safe_store_u64, AtomicU64, u64); + #[cfg(target_has_atomic_load_store = "128")] + safe_load_store_harness!(harness_safe_load_i128, harness_safe_store_i128, AtomicI128, i128); + #[cfg(target_has_atomic_load_store = "128")] + safe_load_store_harness!(harness_safe_load_u128, harness_safe_store_u128, AtomicU128, u128); + #[cfg(target_has_atomic_load_store = "ptr")] + safe_load_store_harness!(harness_safe_load_isize, harness_safe_store_isize, AtomicIsize, isize); + #[cfg(target_has_atomic_load_store = "ptr")] + safe_load_store_harness!(harness_safe_load_usize, harness_safe_store_usize, AtomicUsize, usize); + + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::load)] + pub fn harness_safe_load_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + let _ = storage.load(any_load_order()); + kani::cover(true, "safe atomic pointer load: reached after call"); + } + + #[cfg(target_has_atomic_load_store = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::store)] + pub fn harness_safe_store_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + storage.store(kani::any::() as *mut u8, any_store_order()); + kani::cover(true, "safe atomic pointer store: reached after call"); + } + + macro_rules! safe_compare_exchange_harness { + ($name:ident, $atomic:ty, $value:ty, $method:ident) => { + #[kani::proof_for_contract(<$atomic>::$method)] + pub fn $name() { + let storage = <$atomic>::new(kani::any::<$value>()); + let _ = storage.$method( + kani::any::<$value>(), + kani::any::<$value>(), + any_ordering(), + any_failure_order(), + ); + kani::cover(true, "safe atomic compare-exchange: reached after call"); + } + }; + } + + #[cfg(target_has_atomic = "8")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_bool, + AtomicBool, + bool, + compare_exchange + ); + #[cfg(target_has_atomic = "8")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_bool, + AtomicBool, + bool, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::compare_exchange)] + pub fn harness_safe_compare_exchange_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + let _ = storage.compare_exchange( + kani::any::() as *mut u8, + kani::any::() as *mut u8, + any_ordering(), + any_failure_order(), + ); + kani::cover(true, "safe atomic pointer compare-exchange: reached after call"); + } + #[cfg(target_has_atomic = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::compare_exchange_weak)] + pub fn harness_safe_compare_exchange_weak_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + let _ = storage.compare_exchange_weak( + kani::any::() as *mut u8, + kani::any::() as *mut u8, + any_ordering(), + any_failure_order(), + ); + kani::cover(true, "safe atomic pointer weak compare-exchange: reached after call"); + } + #[cfg(target_has_atomic = "8")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_u8, + AtomicU8, + u8, + compare_exchange + ); + #[cfg(target_has_atomic = "8")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_u8, + AtomicU8, + u8, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "8")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_i8, + AtomicI8, + i8, + compare_exchange + ); + #[cfg(target_has_atomic = "8")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_i8, + AtomicI8, + i8, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "16")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_i16, + AtomicI16, + i16, + compare_exchange + ); + #[cfg(target_has_atomic = "16")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_i16, + AtomicI16, + i16, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "16")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_u16, + AtomicU16, + u16, + compare_exchange + ); + #[cfg(target_has_atomic = "16")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_u16, + AtomicU16, + u16, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "32")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_i32, + AtomicI32, + i32, + compare_exchange + ); + #[cfg(target_has_atomic = "32")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_i32, + AtomicI32, + i32, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "32")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_u32, + AtomicU32, + u32, + compare_exchange + ); + #[cfg(target_has_atomic = "32")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_u32, + AtomicU32, + u32, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "64")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_i64, + AtomicI64, + i64, + compare_exchange + ); + #[cfg(target_has_atomic = "64")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_i64, + AtomicI64, + i64, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "64")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_u64, + AtomicU64, + u64, + compare_exchange + ); + #[cfg(target_has_atomic = "64")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_u64, + AtomicU64, + u64, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "128")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_i128, + AtomicI128, + i128, + compare_exchange + ); + #[cfg(target_has_atomic = "128")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_i128, + AtomicI128, + i128, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "128")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_u128, + AtomicU128, + u128, + compare_exchange + ); + #[cfg(target_has_atomic = "128")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_u128, + AtomicU128, + u128, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "ptr")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_isize, + AtomicIsize, + isize, + compare_exchange + ); + #[cfg(target_has_atomic = "ptr")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_isize, + AtomicIsize, + isize, + compare_exchange_weak + ); + #[cfg(target_has_atomic = "ptr")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_usize, + AtomicUsize, + usize, + compare_exchange + ); + #[cfg(target_has_atomic = "ptr")] + safe_compare_exchange_harness!( + harness_safe_compare_exchange_weak_usize, + AtomicUsize, + usize, + compare_exchange_weak + ); + + macro_rules! safe_update_harness { + ($name:ident, $atomic:ty, $value:ty, $method:ident, $closure:expr) => { + #[kani::proof_for_contract(<$atomic>::$method)] + pub fn $name() { + let storage = <$atomic>::new(kani::any::<$value>()); + let _ = storage.$method(Relaxed, any_failure_order(), $closure); + kani::cover(true, "safe atomic update: reached after call"); + } + }; + } + + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_fetch_update_bool, AtomicBool, bool, fetch_update, |_| None); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_try_update_bool, AtomicBool, bool, try_update, |_| None); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_update_bool, AtomicBool, bool, update, |x| x); + #[cfg(target_has_atomic = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::fetch_update)] + pub fn harness_safe_fetch_update_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + let _ = storage.fetch_update(Relaxed, any_failure_order(), |_| None); + kani::cover(true, "safe atomic pointer fetch-update: reached after call"); + } + #[cfg(target_has_atomic = "ptr")] + #[kani::proof_for_contract(AtomicPtr::::try_update)] + pub fn harness_safe_try_update_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + let _ = storage.try_update(Relaxed, any_failure_order(), |_| None); + kani::cover(true, "safe atomic pointer try-update: reached after call"); + } + #[cfg(all(target_has_atomic_load_store = "ptr", target_has_atomic = "8"))] + #[kani::proof_for_contract(AtomicPtr::::update)] + pub fn harness_safe_update_ptr() { + let storage = AtomicPtr::::new(kani::any::() as *mut u8); + let value = kani::any::() as *mut u8; + let _ = storage.update(Relaxed, any_failure_order(), |_| value); + kani::cover(true, "safe atomic pointer update: reached after call"); + } + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_fetch_update_i8, AtomicI8, i8, fetch_update, |_| None); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_try_update_i8, AtomicI8, i8, try_update, |_| None); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_update_i8, AtomicI8, i8, update, |x| x); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_fetch_update_u8, AtomicU8, u8, fetch_update, |_| None); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_try_update_u8, AtomicU8, u8, try_update, |_| None); + #[cfg(target_has_atomic = "8")] + safe_update_harness!(harness_safe_update_u8, AtomicU8, u8, update, |x| x); + #[cfg(target_has_atomic = "16")] + safe_update_harness!(harness_safe_fetch_update_i16, AtomicI16, i16, fetch_update, |_| None); + #[cfg(target_has_atomic = "16")] + safe_update_harness!(harness_safe_try_update_i16, AtomicI16, i16, try_update, |_| None); + #[cfg(target_has_atomic = "16")] + safe_update_harness!(harness_safe_update_i16, AtomicI16, i16, update, |x| x); + #[cfg(target_has_atomic = "16")] + safe_update_harness!(harness_safe_fetch_update_u16, AtomicU16, u16, fetch_update, |_| None); + #[cfg(target_has_atomic = "16")] + safe_update_harness!(harness_safe_try_update_u16, AtomicU16, u16, try_update, |_| None); + #[cfg(target_has_atomic = "16")] + safe_update_harness!(harness_safe_update_u16, AtomicU16, u16, update, |x| x); + #[cfg(target_has_atomic = "32")] + safe_update_harness!(harness_safe_fetch_update_i32, AtomicI32, i32, fetch_update, |_| None); + #[cfg(target_has_atomic = "32")] + safe_update_harness!(harness_safe_try_update_i32, AtomicI32, i32, try_update, |_| None); + #[cfg(target_has_atomic = "32")] + safe_update_harness!(harness_safe_update_i32, AtomicI32, i32, update, |x| x); + #[cfg(target_has_atomic = "32")] + safe_update_harness!(harness_safe_fetch_update_u32, AtomicU32, u32, fetch_update, |_| None); + #[cfg(target_has_atomic = "32")] + safe_update_harness!(harness_safe_try_update_u32, AtomicU32, u32, try_update, |_| None); + #[cfg(target_has_atomic = "32")] + safe_update_harness!(harness_safe_update_u32, AtomicU32, u32, update, |x| x); + #[cfg(target_has_atomic = "64")] + safe_update_harness!(harness_safe_fetch_update_i64, AtomicI64, i64, fetch_update, |_| None); + #[cfg(target_has_atomic = "64")] + safe_update_harness!(harness_safe_try_update_i64, AtomicI64, i64, try_update, |_| None); + #[cfg(target_has_atomic = "64")] + safe_update_harness!(harness_safe_update_i64, AtomicI64, i64, update, |x| x); + #[cfg(target_has_atomic = "64")] + safe_update_harness!(harness_safe_fetch_update_u64, AtomicU64, u64, fetch_update, |_| None); + #[cfg(target_has_atomic = "64")] + safe_update_harness!(harness_safe_try_update_u64, AtomicU64, u64, try_update, |_| None); + #[cfg(target_has_atomic = "64")] + safe_update_harness!(harness_safe_update_u64, AtomicU64, u64, update, |x| x); + #[cfg(target_has_atomic = "128")] + safe_update_harness!(harness_safe_fetch_update_i128, AtomicI128, i128, fetch_update, |_| None); + #[cfg(target_has_atomic = "128")] + safe_update_harness!(harness_safe_try_update_i128, AtomicI128, i128, try_update, |_| None); + #[cfg(target_has_atomic = "128")] + safe_update_harness!(harness_safe_update_i128, AtomicI128, i128, update, |x| x); + #[cfg(target_has_atomic = "128")] + safe_update_harness!(harness_safe_fetch_update_u128, AtomicU128, u128, fetch_update, |_| None); + #[cfg(target_has_atomic = "128")] + safe_update_harness!(harness_safe_try_update_u128, AtomicU128, u128, try_update, |_| None); + #[cfg(target_has_atomic = "128")] + safe_update_harness!(harness_safe_update_u128, AtomicU128, u128, update, |x| x); + #[cfg(target_has_atomic = "ptr")] + safe_update_harness!(harness_safe_fetch_update_isize, AtomicIsize, isize, fetch_update, |_| { + None + }); + #[cfg(target_has_atomic = "ptr")] + safe_update_harness!(harness_safe_try_update_isize, AtomicIsize, isize, try_update, |_| None); + #[cfg(target_has_atomic = "ptr")] + safe_update_harness!(harness_safe_update_isize, AtomicIsize, isize, update, |x| x); + #[cfg(target_has_atomic = "ptr")] + safe_update_harness!(harness_safe_fetch_update_usize, AtomicUsize, usize, fetch_update, |_| { + None + }); + #[cfg(target_has_atomic = "ptr")] + safe_update_harness!(harness_safe_try_update_usize, AtomicUsize, usize, try_update, |_| None); + #[cfg(target_has_atomic = "ptr")] + safe_update_harness!(harness_safe_update_usize, AtomicUsize, usize, update, |x| x); + #[cfg(target_has_atomic_load_store = "8")] + #[kani::proof] + #[kani::should_panic] + pub fn harness_safe_load_panics_on_release() { + let storage = AtomicBool::new(false); + let _ = storage.load(Release); + } + + #[cfg(target_has_atomic_load_store = "8")] + #[kani::proof] + #[kani::should_panic] + pub fn harness_safe_load_panics_on_acqrel() { + let storage = AtomicBool::new(false); + let _ = storage.load(AcqRel); + } + + #[cfg(target_has_atomic_load_store = "8")] + #[kani::proof] + #[kani::should_panic] + pub fn harness_safe_store_panics_on_acquire() { + let storage = AtomicBool::new(false); + storage.store(true, Acquire); + } + + #[cfg(target_has_atomic_load_store = "8")] + #[kani::proof] + #[kani::should_panic] + pub fn harness_safe_store_panics_on_acqrel() { + let storage = AtomicBool::new(false); + storage.store(true, AcqRel); + } + + macro_rules! safe_compare_exchange_panics_harness { + ($name:ident, $method:ident, $failure:expr) => { + #[cfg(target_has_atomic = "8")] + #[kani::proof] + #[kani::should_panic] + pub fn $name() { + let storage = AtomicBool::new(false); + let _ = storage.$method(false, true, Relaxed, $failure); + } + }; + } + + safe_compare_exchange_panics_harness!( + harness_safe_compare_exchange_panics_on_release, + compare_exchange, + Release + ); + safe_compare_exchange_panics_harness!( + harness_safe_compare_exchange_panics_on_acqrel, + compare_exchange, + AcqRel + ); + safe_compare_exchange_panics_harness!( + harness_safe_compare_exchange_weak_panics_on_release, + compare_exchange_weak, + Release + ); + safe_compare_exchange_panics_harness!( + harness_safe_compare_exchange_weak_panics_on_acqrel, + compare_exchange_weak, + AcqRel + ); + + macro_rules! safe_update_panics_harness { + ($name:ident, $method:ident, $failure:expr, $closure:expr) => { + #[cfg(target_has_atomic = "8")] + #[kani::proof] + #[kani::should_panic] + pub fn $name() { + let storage = AtomicBool::new(false); + let _ = storage.$method(Relaxed, $failure, $closure); + } + }; + } + + safe_update_panics_harness!( + harness_safe_fetch_update_panics_on_release, + fetch_update, + Release, + |_| None + ); + safe_update_panics_harness!( + harness_safe_fetch_update_panics_on_acqrel, + fetch_update, + AcqRel, + |_| None + ); + safe_update_panics_harness!( + harness_safe_try_update_panics_on_release, + try_update, + Release, + |_| None + ); + safe_update_panics_harness!( + harness_safe_try_update_panics_on_acqrel, + try_update, + AcqRel, + |_| None + ); + safe_update_panics_harness!(harness_safe_update_panics_on_release, update, Release, |x| x); + safe_update_panics_harness!(harness_safe_update_panics_on_acqrel, update, AcqRel, |x| x); +}