From ed84b1cc494a22695bebe9f59e9b19d60a2fd792 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 22 Jan 2026 07:55:26 -0500
Subject: [PATCH] libs: Avoid raw pointer comparisons in std::thread

Fixes #225.
---
 libs/Patches.md                | 42 ++++++++++++++++++++++++++++++++++
 libs/std/src/thread/current.rs |  8 +++----
 2 files changed, 46 insertions(+), 4 deletions(-)

diff --git a/libs/Patches.md b/libs/Patches.md
index 7360d803..a0b6d405 100644
--- a/libs/Patches.md
+++ b/libs/Patches.md
@@ -261,6 +261,14 @@ into the main commit for that patch, and then the *Update* line can be removed.
   intrinsic. To prevent this function from throwing translation errors, we have
   it return a constant dummy location.
 
+* Avoid raw pointer comparisons in `std::thread` (last applied: January 22, 2026)
+
+  `std::thread` reserves raw pointers with the addresses 0-2 as sentinel
+  values. Instead of checking if a thread's pointer is not a sentinel value by
+  seeing if it is larger than the sentinel with the largest address, we instead
+  check if the pointer is not equal to each of the individual sentinel values.
+  See also the "Avoid raw pointer comparisons" note below.
+
 # Notes
 
 This section contains more detailed notes about why certain patches are written
@@ -283,3 +291,37 @@ this actually happened.)
 
 As a safeguard, we mark all custom hook functions as `#[inline(never)]` to
 ensure that they persist when optimizations are applied.
+
+## Avoid raw pointer comparisons
+
+We avoid using `PartialOrd`-based comparisons with raw pointers values, e.g.,
+
+```rs
+fn f(p: *const ()) {
+    if (p > ptr::null()) {
+        ...
+    }
+}
+```
+
+Instead, we prefer using `PartialEq`-based equality checks, e.g.,
+
+```rs
+    if (p != ptr::null()) {
+        ...
+    }
+
+```
+
+The reason for this is because the `PartialOrd` impl for raw pointers compares
+their underlying addresses, but `crucible-mir` pointers do not always have
+addresses. `MirReference_Integer` pointers can treat their underlying integer
+as an address (e.g., `ptr::null()` has the address 0), but other forms of
+`MirReference`s (i.e., _valid_ `MirReference`s) do not have a tangible address,
+so it is not currently possible to compare `MirReference_Integer`s against
+valid `MirReference`s. Attempting to do so will raise a simulation error.
+
+Using the `PartialEq` impl for raw pointers works better in a `crucible-mir`
+context. Instead of raising a simulation error, `crucible-mir` will simply
+return `False` when checking if a `MirReference_Integer` is equal to a valid
+`MirReference`.
diff --git a/libs/std/src/thread/current.rs b/libs/std/src/thread/current.rs
index 7da1621d..24f473fd 100644
--- a/libs/std/src/thread/current.rs
+++ b/libs/std/src/thread/current.rs
@@ -169,7 +169,7 @@ where
     F: FnOnce(Option<&Thread>) -> R,
 {
     let current = CURRENT.get();
-    if current > DESTROYED {
+    if current != NONE && current != BUSY && current != DESTROYED {
         // SAFETY: `Arc` does not contain interior mutability, so it does not
         // matter that the address of the handle might be different depending
         // on where this is called.
@@ -187,7 +187,7 @@ where
 /// handle to allow thread parking in nearly all situations.
 pub(crate) fn current_or_unnamed() -> Thread {
     let current = CURRENT.get();
-    if current > DESTROYED {
+    if current != NONE && current != BUSY && current != DESTROYED {
         unsafe {
             let current = ManuallyDrop::new(Thread::from_raw(current));
             (*current).clone()
@@ -222,7 +222,7 @@ pub(crate) fn current_or_unnamed() -> Thread {
 #[stable(feature = "rust1", since = "1.0.0")]
 pub fn current() -> Thread {
     let current = CURRENT.get();
-    if current > DESTROYED {
+    if current != NONE && current != BUSY && current != DESTROYED {
         unsafe {
             let current = ManuallyDrop::new(Thread::from_raw(current));
             (*current).clone()
@@ -279,7 +279,7 @@ fn init_current(current: *mut ()) -> Thread {
 /// handle.
 pub(crate) fn drop_current() {
     let current = CURRENT.get();
-    if current > DESTROYED {
+    if current != NONE && current != BUSY && current != DESTROYED {
         unsafe {
             CURRENT.set(DESTROYED);
             drop(Thread::from_raw(current));