Skip to content

Commit ed84b1c

Browse files
committed
libs: Avoid raw pointer comparisons in std::thread
Fixes #225.
1 parent 5553e60 commit ed84b1c

File tree

2 files changed

+46
-4
lines changed

2 files changed

+46
-4
lines changed

libs/Patches.md

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -261,6 +261,14 @@ into the main commit for that patch, and then the *Update* line can be removed.
261261
intrinsic. To prevent this function from throwing translation errors, we have
262262
it return a constant dummy location.
263263

264+
* Avoid raw pointer comparisons in `std::thread` (last applied: January 22, 2026)
265+
266+
`std::thread` reserves raw pointers with the addresses 0-2 as sentinel
267+
values. Instead of checking if a thread's pointer is not a sentinel value by
268+
seeing if it is larger than the sentinel with the largest address, we instead
269+
check if the pointer is not equal to each of the individual sentinel values.
270+
See also the "Avoid raw pointer comparisons" note below.
271+
264272
# Notes
265273

266274
This section contains more detailed notes about why certain patches are written
@@ -283,3 +291,37 @@ this actually happened.)
283291

284292
As a safeguard, we mark all custom hook functions as `#[inline(never)]` to
285293
ensure that they persist when optimizations are applied.
294+
295+
## Avoid raw pointer comparisons
296+
297+
We avoid using `PartialOrd`-based comparisons with raw pointers values, e.g.,
298+
299+
```rs
300+
fn f(p: *const ()) {
301+
if (p > ptr::null()) {
302+
...
303+
}
304+
}
305+
```
306+
307+
Instead, we prefer using `PartialEq`-based equality checks, e.g.,
308+
309+
```rs
310+
if (p != ptr::null()) {
311+
...
312+
}
313+
314+
```
315+
316+
The reason for this is because the `PartialOrd` impl for raw pointers compares
317+
their underlying addresses, but `crucible-mir` pointers do not always have
318+
addresses. `MirReference_Integer` pointers can treat their underlying integer
319+
as an address (e.g., `ptr::null()` has the address 0), but other forms of
320+
`MirReference`s (i.e., _valid_ `MirReference`s) do not have a tangible address,
321+
so it is not currently possible to compare `MirReference_Integer`s against
322+
valid `MirReference`s. Attempting to do so will raise a simulation error.
323+
324+
Using the `PartialEq` impl for raw pointers works better in a `crucible-mir`
325+
context. Instead of raising a simulation error, `crucible-mir` will simply
326+
return `False` when checking if a `MirReference_Integer` is equal to a valid
327+
`MirReference`.

libs/std/src/thread/current.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ where
169169
F: FnOnce(Option<&Thread>) -> R,
170170
{
171171
let current = CURRENT.get();
172-
if current > DESTROYED {
172+
if current != NONE && current != BUSY && current != DESTROYED {
173173
// SAFETY: `Arc` does not contain interior mutability, so it does not
174174
// matter that the address of the handle might be different depending
175175
// on where this is called.
@@ -187,7 +187,7 @@ where
187187
/// handle to allow thread parking in nearly all situations.
188188
pub(crate) fn current_or_unnamed() -> Thread {
189189
let current = CURRENT.get();
190-
if current > DESTROYED {
190+
if current != NONE && current != BUSY && current != DESTROYED {
191191
unsafe {
192192
let current = ManuallyDrop::new(Thread::from_raw(current));
193193
(*current).clone()
@@ -222,7 +222,7 @@ pub(crate) fn current_or_unnamed() -> Thread {
222222
#[stable(feature = "rust1", since = "1.0.0")]
223223
pub fn current() -> Thread {
224224
let current = CURRENT.get();
225-
if current > DESTROYED {
225+
if current != NONE && current != BUSY && current != DESTROYED {
226226
unsafe {
227227
let current = ManuallyDrop::new(Thread::from_raw(current));
228228
(*current).clone()
@@ -279,7 +279,7 @@ fn init_current(current: *mut ()) -> Thread {
279279
/// handle.
280280
pub(crate) fn drop_current() {
281281
let current = CURRENT.get();
282-
if current > DESTROYED {
282+
if current != NONE && current != BUSY && current != DESTROYED {
283283
unsafe {
284284
CURRENT.set(DESTROYED);
285285
drop(Thread::from_raw(current));

0 commit comments

Comments
 (0)