From 688ee4c88722ca191981246f7732f25caed81cac Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 15 Nov 2024 13:09:52 +0100 Subject: [PATCH] fix: constant folding for Nat.ble and Nat.blt (#6087) This PR fixes a bug in the constant folding for the `Nat.ble` and `Nat.blt` function in the old code generator, leading to a miscompilation. Closes #6086 --- src/Lean/Compiler/ConstFolding.lean | 4 ++-- src/include/lean/lean.h | 6 ++++++ tests/lean/run/6086.lean | 3 +++ 3 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/6086.lean diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean index ee99319fd2da..320648111376 100644 --- 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 index 5ac680164cc7..90b4b8439ea6 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1259,6 +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))) { + // 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); @@ -1275,6 +1277,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))) { + // 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); @@ -1287,6 +1291,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))) { + // 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); diff --git a/tests/lean/run/6086.lean b/tests/lean/run/6086.lean new file mode 100644 index 000000000000..84dedc6e375b --- /dev/null +++ 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]