Skip to content

Commit f598ca7

Browse files
Samuelsillsclaude
andcommitted
Part 3: Add safety contracts to all atomic intrinsic declarations
Add #[requires] contracts to all 15 atomic intrinsic declarations encoding pointer validity and writability preconditions: atomic_cxchg, atomic_cxchgweak, atomic_load, atomic_store, atomic_xchg, atomic_xadd, atomic_xsub, atomic_and, atomic_nand, atomic_or, atomic_xor, atomic_max, atomic_min, atomic_umin, atomic_umax. Each generic declaration covers 3-15 monomorphizations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 933250b commit f598ca7

File tree

1 file changed

+15
-0
lines changed
  • library/core/src/intrinsics

1 file changed

+15
-0
lines changed

library/core/src/intrinsics/mod.rs

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,7 @@ pub enum AtomicOrdering {
9999
/// For example, [`AtomicBool::compare_exchange`].
100100
#[rustc_intrinsic]
101101
#[rustc_nounwind]
102+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
102103
pub unsafe fn atomic_cxchg<
103104
T: Copy,
104105
const ORD_SUCC: AtomicOrdering,
@@ -117,6 +118,7 @@ pub unsafe fn atomic_cxchg<
117118
/// For example, [`AtomicBool::compare_exchange_weak`].
118119
#[rustc_intrinsic]
119120
#[rustc_nounwind]
121+
#[requires(ub_checks::can_write(_dst) && ub_checks::can_dereference(_dst as *const T))]
120122
pub unsafe fn atomic_cxchgweak<
121123
T: Copy,
122124
const ORD_SUCC: AtomicOrdering,
@@ -134,6 +136,7 @@ pub unsafe fn atomic_cxchgweak<
134136
/// [`atomic`] types via the `load` method. For example, [`AtomicBool::load`].
135137
#[rustc_intrinsic]
136138
#[rustc_nounwind]
139+
#[requires(ub_checks::can_dereference(src))]
137140
pub unsafe fn atomic_load<T: Copy, const ORD: AtomicOrdering>(src: *const T) -> T;
138141

139142
/// Stores the value at the specified memory location.
@@ -143,6 +146,7 @@ pub unsafe fn atomic_load<T: Copy, const ORD: AtomicOrdering>(src: *const T) ->
143146
/// [`atomic`] types via the `store` method. For example, [`AtomicBool::store`].
144147
#[rustc_intrinsic]
145148
#[rustc_nounwind]
149+
#[requires(ub_checks::can_write(dst))]
146150
pub unsafe fn atomic_store<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, val: T);
147151

148152
/// Stores the value at the specified memory location, returning the old value.
@@ -152,6 +156,7 @@ pub unsafe fn atomic_store<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, val:
152156
/// [`atomic`] types via the `swap` method. For example, [`AtomicBool::swap`].
153157
#[rustc_intrinsic]
154158
#[rustc_nounwind]
159+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
155160
pub unsafe fn atomic_xchg<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T;
156161

157162
/// Adds to the current value, returning the previous value.
@@ -162,6 +167,7 @@ pub unsafe fn atomic_xchg<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src:
162167
/// [`atomic`] types via the `fetch_add` method. For example, [`AtomicIsize::fetch_add`].
163168
#[rustc_intrinsic]
164169
#[rustc_nounwind]
170+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
165171
pub unsafe fn atomic_xadd<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: U) -> T;
166172

167173
/// Subtract from the current value, returning the previous value.
@@ -172,6 +178,7 @@ pub unsafe fn atomic_xadd<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut
172178
/// [`atomic`] types via the `fetch_sub` method. For example, [`AtomicIsize::fetch_sub`].
173179
#[rustc_intrinsic]
174180
#[rustc_nounwind]
181+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
175182
pub unsafe fn atomic_xsub<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: U) -> T;
176183

177184
/// Bitwise and with the current value, returning the previous value.
@@ -182,6 +189,7 @@ pub unsafe fn atomic_xsub<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut
182189
/// [`atomic`] types via the `fetch_and` method. For example, [`AtomicBool::fetch_and`].
183190
#[rustc_intrinsic]
184191
#[rustc_nounwind]
192+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
185193
pub unsafe fn atomic_and<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: U) -> T;
186194

187195
/// Bitwise nand with the current value, returning the previous value.
@@ -192,6 +200,7 @@ pub unsafe fn atomic_and<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut
192200
/// [`AtomicBool`] type via the `fetch_nand` method. For example, [`AtomicBool::fetch_nand`].
193201
#[rustc_intrinsic]
194202
#[rustc_nounwind]
203+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
195204
pub unsafe fn atomic_nand<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: U) -> T;
196205

197206
/// Bitwise or with the current value, returning the previous value.
@@ -202,6 +211,7 @@ pub unsafe fn atomic_nand<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut
202211
/// [`atomic`] types via the `fetch_or` method. For example, [`AtomicBool::fetch_or`].
203212
#[rustc_intrinsic]
204213
#[rustc_nounwind]
214+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
205215
pub unsafe fn atomic_or<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: U) -> T;
206216

207217
/// Bitwise xor with the current value, returning the previous value.
@@ -212,6 +222,7 @@ pub unsafe fn atomic_or<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T
212222
/// [`atomic`] types via the `fetch_xor` method. For example, [`AtomicBool::fetch_xor`].
213223
#[rustc_intrinsic]
214224
#[rustc_nounwind]
225+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
215226
pub unsafe fn atomic_xor<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: U) -> T;
216227

217228
/// Maximum with the current value using a signed comparison.
@@ -221,6 +232,7 @@ pub unsafe fn atomic_xor<T: Copy, U: Copy, const ORD: AtomicOrdering>(dst: *mut
221232
/// [`atomic`] signed integer types via the `fetch_max` method. For example, [`AtomicI32::fetch_max`].
222233
#[rustc_intrinsic]
223234
#[rustc_nounwind]
235+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
224236
pub unsafe fn atomic_max<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T;
225237

226238
/// Minimum with the current value using a signed comparison.
@@ -230,6 +242,7 @@ pub unsafe fn atomic_max<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T
230242
/// [`atomic`] signed integer types via the `fetch_min` method. For example, [`AtomicI32::fetch_min`].
231243
#[rustc_intrinsic]
232244
#[rustc_nounwind]
245+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
233246
pub unsafe fn atomic_min<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T;
234247

235248
/// Minimum with the current value using an unsigned comparison.
@@ -239,6 +252,7 @@ pub unsafe fn atomic_min<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T
239252
/// [`atomic`] unsigned integer types via the `fetch_min` method. For example, [`AtomicU32::fetch_min`].
240253
#[rustc_intrinsic]
241254
#[rustc_nounwind]
255+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
242256
pub unsafe fn atomic_umin<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T;
243257

244258
/// Maximum with the current value using an unsigned comparison.
@@ -248,6 +262,7 @@ pub unsafe fn atomic_umin<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src:
248262
/// [`atomic`] unsigned integer types via the `fetch_max` method. For example, [`AtomicU32::fetch_max`].
249263
#[rustc_intrinsic]
250264
#[rustc_nounwind]
265+
#[requires(ub_checks::can_write(dst) && ub_checks::can_dereference(dst as *const T))]
251266
pub unsafe fn atomic_umax<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T;
252267

253268
/// An atomic fence.

0 commit comments

Comments
 (0)