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