From 9ee398e8179b86295bd3723e68498f4f2f4e647f Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 13 Sep 2026 23:09:08 +0700 Subject: [PATCH] The two cases that would have passed while being wrong An i32 min / -1 and an f32 cast out of range. The first is where the two backends disagreed silently rather than both dying -- x86 divided in 64 bits and truncated on the store, answering -2147483648, where LLVM emitted poison -- and it is the only case that exercises the widening on the way into the condition, so a bug there would have left every other row passing. The second is the one place the two backends reach the same answer by deliberately different routes, f32 bounds here and widened doubles there, and the survey is what says the routes agree. --- HANDOFF-arith.md | 9 +++++++-- test/programs/arith.flan | 21 +++++++++++++++++++++ test/test_acceptance.ml | 16 ++++++++++++++++ 3 files changed, 44 insertions(+), 2 deletions(-) diff --git a/HANDOFF-arith.md b/HANDOFF-arith.md index 89039af..9ab5210 100644 --- a/HANDOFF-arith.md +++ b/HANDOFF-arith.md @@ -76,8 +76,13 @@ because `load_loc` has already widened both operands according to their own sign backends used to diverge silently rather than both dying: x86 divided in 64 bits and truncated on the store, producing `-2147483648` for an `i32`, where LLVM emitted poison. `arith.flan` has an `i32` case for exactly that reason. -`spike/x86/survey.sh` is 100 MATCH / 0 DIFFER / 0 REFUSED — the 98 that was the baseline plus the two programs this -change adds. +`spike/x86/survey.sh` is 101 MATCH / 0 DIFFER / 0 REFUSED, with the two programs this change adds among them. + +`arith.flan` carries an `i32` overflow case and an `f32` cast case on purpose, and neither is padding. The `i32` +overflow is where the two backends disagreed *silently* rather than both dying, and it is the only thing that +exercises the widening on the way into the condition — if that were wrong, the number in the message would be garbage +and every other case would still pass. The `f32` cast is the one place the two backends reach the same answer by +deliberately different routes, and the survey is what says the routes agree rather than the comment above them. ## What landed diff --git a/test/programs/arith.flan b/test/programs/arith.flan index 55b19e4..4601e64 100644 --- a/test/programs/arith.flan +++ b/test/programs/arith.flan @@ -20,6 +20,15 @@ (defvar ten i64 10) (defvar uz u32) (defvar huge f64 1e300) +;; The narrow versions of the same two failures. They are here because they are +;; the ones the two backends reach by different routes: the overflow test +;; compares against the *narrow* type's most negative value inside a 64-bit +;; register, and the f32 range test is compared in f32 on one backend and in a +;; double on the other. Both routes are supposed to give the same answer and +;; the survey is what says so. +(defvar i32big i32 2147483647) +(defvar m1-32 i32 -1) +(defvar wide f32 1e30) (defn main [args [string]] i32 (let [n (i32 (bytes->i64 (bytes (at args 1)))) @@ -55,6 +64,18 @@ ;; NaN, which fails the range test at both ends rather than passing it at ;; neither: the comparisons are ordered, deliberately. (= n 7) (print (i64 (/ (f64 0.0) (f64 0.0)))) + ;; The same overflow one width down, which is the case the two backends + ;; used to disagree about *silently* rather than both dying: this one + ;; loaded sign-extended into a 64-bit register, divided there and + ;; truncated on the store, answering -2147483648, where the other backend + ;; emitted poison. Neither was wrong about anything; they just were not + ;; the same program. + (= n 8) (print (/ (- (- (i32 0) i32big) 1) m1-32)) + ;; And an f32 source, whose range test the two backends reach by + ;; different routes on purpose — compared in f32 here and in a widened + ;; double there, which agree because every bound is a power of two and is + ;; exact in both. + (= n 9) (print (i32 wide)) :else (println "?")) 0)) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 01fbe25..5455c9e 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -1336,6 +1336,22 @@ let () = NaN as it is for 1e300. *) traps "NaN cast to an integer" "7" "does not fit the integer type it is cast to"; + (* One width down, and this is the case the two backends disagreed about + *silently* rather than both dying: x86 loaded the operands + sign-extended into 64-bit registers, divided there and truncated on + the store, answering -2147483648, where LLVM emitted poison. It is + also the only thing that exercises the widening on the way into the + condition — if that is wrong, the number in this sentence is + garbage. *) + traps "the i32 division that overflows" "8" + "(/ -2147483648 -1) overflows"; + (* An f32 source, whose range test the two backends reach by deliberately + different routes: emit.ml widens the value to a double and compares + against double bounds, x86.ml compares in f32 against an f32 constant. + They agree because every bound is a power of two and is exact in both, + and this is the row that says so rather than the comment. *) + traps "an f32 too large for an i32" "9" + "which holds [-2147483648 2147483647]"; (try Sys.remove exe with Sys_error _ -> ()) in arith ();