@@ -238,6 +238,14 @@ into the main commit for that patch, and then the *Update* line can be removed.
238238 This feature was using an ` AtomicPtr<()> ` with a cast from function
239239 pointer to ` *mut () ` that we don't support in its initializer.
240240
241+ * Avoid raw pointer comparisons in ` std::thread ` (last applied: January 22, 2026)
242+
243+ ` std::thread ` reserves raw pointers with the addresses 0-3 as sentinel
244+ values. Instead of checking if a thread's pointer is not a sentinel value by
245+ seeing if it is larger than the sentinel with the largest address, we instead
246+ check if the pointer is not equal to each of the individual sentinel values.
247+ See also the "Avoid raw pointer comparisons" note below.
248+
241249# Notes
242250
243251This section contains more detailed notes about why certain patches are written
@@ -260,3 +268,48 @@ this actually happened.)
260268
261269As a safeguard, we mark all custom hook functions as ` #[inline(never)] ` to
262270ensure that they persist when optimizations are applied.
271+
272+ ## Avoid raw pointer comparisons
273+
274+ We avoid using ` PartialOrd ` -based comparisons with raw pointers values, e.g.,
275+
276+ ``` rs
277+ fn f (p : * const ()) {
278+ if (p > ptr :: null ()) {
279+ ...
280+ }
281+ }
282+ ```
283+
284+ Instead, we prefer using ` PartialEq ` -based equality checks, e.g.,
285+
286+ ``` rs
287+ if (p != ptr :: null ()) {
288+ ...
289+ }
290+
291+ ```
292+
293+ The reason for this is because the ` PartialOrd ` impl for raw pointers compares
294+ their underlying addresses, but ` crucible-mir ` pointers do not always have
295+ addresses. ` MirReference_Integer ` pointers can treat their underlying integer
296+ as an address (e.g., ` ptr::null() ` has the address 0), but other forms of
297+ ` MirReference ` s (i.e., _ valid_ ` MirReference ` s) do not have a tangible address,
298+ so it is not currently possible to compare ` MirReference_Integer ` s against
299+ valid ` MirReference ` s. Attempting to do so will raise a simulation error.
300+
301+ Using the ` PartialEq ` impl for raw pointers is safer. Instead of raising a
302+ simulation error, ` crucible-mir ` will simply return ` False ` when checking if a
303+ ` MirReference_Integer ` is equal to a valid ` MirReference ` . This is slightly
304+ unsound, as it is theoretically possible (albeit very unlikely) for valid
305+ ` MirReference ` s to have very small addresses. For instance, the expression
306+ ` (0 .. usize::MAX).any(|addr| addr as *const T == ptr) ` will return ` true `
307+ (where ` ptr ` is a valid pointer) in normal execution of Rust code, as all
308+ pointers have an address that lies somewhere within the range of a ` usize `
309+ value. In ` crucible-mir ` , however, this will return ` false ` , since a valid
310+ pointer will never be equal to a pointer cast from an integer.
311+
312+ Again, it is worth emphasizing that this unsoundness poses a very small risk in
313+ practice, as the vast majority of pointers are valid ones. For instance, we use
314+ the ` PartialEq ` impl for raw pointers to great effect in the internals of
315+ ` std::thread ` , where most threads are backed by valid raw pointers.
0 commit comments