Do not unbox nat comparisons

leanprover · Nov 15, 2024 · e6ca7b5 · e6ca7b5
1 parent a2d37c6
commit e6ca7b5
Showing 1 changed file with 9 additions and 6 deletions.
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -1259,8 +1259,9 @@ static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
-        // Avoid UB due to pointer comparison
-        return lean_unbox(a1) == lean_unbox(a2);
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
+        return a1 == a2;
     } else {
         return lean_nat_big_eq(a1, a2);
     }
@@ -1276,8 +1277,9 @@ static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
-        // Avoid UB due to pointer comparison
-        return lean_unbox(a1) <= lean_unbox(a2);
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
+        return a1 <= a2;
     } else {
         return lean_nat_big_le(a1, a2);
     }
@@ -1289,8 +1291,9 @@ static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
-        // Avoid UB due to pointer comparison
-        return lean_unbox(a1) < lean_unbox(a2);
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
+        return a1 < a2;
     } else {
         return lean_nat_big_lt(a1, a2);
     }