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.
This commit is contained in:
Joseph Ferano 2026-09-13 23:09:08 +07:00
parent b0f4fb73e1
commit 9ee398e817
3 changed files with 44 additions and 2 deletions

View File

@ -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

View File

@ -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))

View File

@ -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 ();