fix: constant folding for Nat.ble and Nat.blt

leanprover · Nov 15, 2024 · a2d37c6 · a2d37c6
1 parent a074bd9
commit a2d37c6
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 5 deletions.
diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean
@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
     return mkConst ``Bool.false
 
 def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
-def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
-def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
+def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
+def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
 
 def natFoldFns : List (Name × BinFoldFn) :=
   [(``Nat.add, foldNatAdd),

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -1259,7 +1259,8 @@ 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))) {
-        return a1 == a2;
+        // Avoid UB due to pointer comparison
+        return lean_unbox(a1) == lean_unbox(a2);
     } else {
         return lean_nat_big_eq(a1, a2);
     }
@@ -1275,7 +1276,8 @@ 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))) {
-        return a1 <= a2;
+        // Avoid UB due to pointer comparison
+        return lean_unbox(a1) <= lean_unbox(a2);
     } else {
         return lean_nat_big_le(a1, a2);
     }
@@ -1287,7 +1289,8 @@ 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))) {
-        return a1 < a2;
+        // Avoid UB due to pointer comparison
+        return lean_unbox(a1) < lean_unbox(a2);
     } else {
         return lean_nat_big_lt(a1, a2);
     }

diff --git a/tests/lean/run/6086.lean b/tests/lean/run/6086.lean
@@ -0,0 +1,3 @@
+/-- info: [true, true, false, true, false, false, true, true, false, true, false, false] -/
+#guard_msgs in
+#eval [Nat.ble 36 37, Nat.ble 37 37, Nat.ble 38 37, Nat.blt 36 37, Nat.blt 37 37, Nat.blt 38 37, 36 ≤ 37, 37 ≤ 37, 38 ≤ 37 ,36 < 37, 37 < 37, 38 < 37]