diff --git a/docs/BUGS-2026-09-18.md b/docs/BUGS-2026-09-18.md index 827942e..fb24cc4 100644 --- a/docs/BUGS-2026-09-18.md +++ b/docs/BUGS-2026-09-18.md @@ -102,8 +102,11 @@ territory; fix or record, the lane's call. - **defenum values never range-checked to i32** (`parse.ml:994`, `check.ml:1666`): the collision rule compares i64s, so `[A 0 B 4294967296]` passes and both are 0 at runtime; autoincrement can overflow silently on --x86. -- **NaN sign**: LLVM constant-folds `0.0/0.0` to `nan`, x86 computes `-nan` — a stdout - DIFFER on a two-line program. Runtime paths agree (`-nan` both). +- **NaN sign** — **fixed**. LLVM constant-folded `0.0/0.0` to `nan`, x86 computed `-nan` + — a stdout DIFFER on a two-line program. Resolved by canonicalizing the *printed* form + rather than the arithmetic: `flan_f64_to_bytes` and the two dev emitters render any NaN + as unsigned `nan`, which is what `format-f64` in the prelude always did. Pinned in + `test/programs/format.flan`. See docs/BUILT.md. - **`emit.ml:3369` transient test ignores `new_globals`**: on the `retains=false` path a module first to intern a global gets dlclosed; zero-init makes it moot today, a literal init would dangle. diff --git a/docs/BUILT.md b/docs/BUILT.md index 5919e59..de23c5a 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -5742,3 +5742,27 @@ off the end of a slice. `check_slice` no longer lets the value out of Flan, but `slice-from-ptr` promise all reach it. A function correct on its own arguments does not become incorrect because its callers improved. +## A NaN prints without a sign + +`(/ 0.0 0.0)` printed `nan` through LLVM and `-nan` through the x86 backend. Neither is +wrong about the arithmetic: IEEE 754 does not specify the sign of a NaN any operation +produces, LLVM's constant folder answers with the positive quiet NaN at compile time, and +`divsd` answers with the negative one at run time. Putting the operands in `defvar` +globals so nothing folds makes both say `-nan`, which is what confirms the divergence is +the folding path and not a disagreement about float arithmetic. + +The fix is at the **print site**, not in the arithmetic, and the reason to prefer it is +not cross-backend agreement — that is a side effect. `format-f64` in the prelude has +always rendered this value as `nan`: it reaches the case through `(not (= x x))` and has +no sign bit in its hands at all. So a build where `(print x)` said `-nan` and +`(show x 2)` said `nan` was already contradicting itself about one value inside one +backend. `flan_f64_to_bytes` now renders any NaN as `nan`, and `flan_dev_emit_f64` and +`flan_dev_watch_emit_f64` do the same, because the REPL and `println` are held to +agreeing about what a value looks like — the same rule the escape tables beside them +already follow. `print` agrees with `show` first; the two backends agree second. + +The test is `x != x` rather than `isnan`, which keeps `math.h` out of the runtime and is +the same comparison the prelude uses. An infinity still prints signed: there the sign is +the value, and the backends were always agreed about it. Pinned in +`test/programs/format.flan`, which is in the x86 survey corpus, so one program holds both +the printed form under `dune test` and the agreement under the survey. diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c index 28d0b49..a811cdf 100644 --- a/runtime/flan_dev.c +++ b/runtime/flan_dev.c @@ -217,9 +217,16 @@ void flan_dev_emit_i64(int64_t x) { emit_cstr(buf); } +/* Unsigned NaN, for flan_f64_to_bytes's reason and one of its own: the REPL + * and println must not disagree about what a value looks like, which is the + * rule the escape table below is already held to. A NaN's sign bit is decided + * by whether the value was folded or computed, so showing it makes the printed + * form depend on the backend and the optimisation level rather than on the + * number. */ void flan_dev_emit_f64(double x) { char buf[64]; - snprintf(buf, sizeof buf, "%g", x); + if (x != x) snprintf(buf, sizeof buf, "nan"); + else snprintf(buf, sizeof buf, "%g", x); emit_cstr(buf); } @@ -528,9 +535,12 @@ void flan_dev_watch_emit_u64(uint64_t x) { watch_cstr(buf); } +/* Unsigned NaN, the same rule [flan_dev_emit_f64] states: a watch row and a + * REPL answer for one value must read the same. */ void flan_dev_watch_emit_f64(double x) { char buf[64]; - snprintf(buf, sizeof buf, "%g", x); + if (x != x) snprintf(buf, sizeof buf, "nan"); + else snprintf(buf, sizeof buf, "%g", x); watch_cstr(buf); } diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index e53c6fe..c66c579 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -305,9 +305,31 @@ int64_t flan_bytes_to_i64(const uint8_t *p, int64_t n) { } /* %g so that 3.5 prints as "3.5" and not "3.500000" — calc-me's expected - * output is a table of exact strings. */ + * output is a table of exact strings. + * + * NaN is rendered by hand, and the reason is that %g renders the *sign bit* of + * something that does not have a sign. glibc prints "-nan" when the bit is set + * and "nan" when it is not, and which one a program gets is decided by things + * no source line chose: LLVM's constant folder answers (/ 0.0 0.0) with a + * positive quiet NaN at compile time, divsd on this machine answers the same + * expression with the negative one at run time, so the same two-line program + * printed "nan" through one backend and "-nan" through the other. Neither is + * wrong about the arithmetic — IEEE 754 does not specify the sign of a NaN any + * operation produces — which is exactly what makes it the wrong thing to show. + * + * Reporting it unsigned is not a new rule here either: format-f64 in the + * prelude has always answered "nan" for the same value, because it reaches the + * case with (not (= x x)) and has no sign bit in its hands at all. So a build + * where (print x) said "-nan" and (show x 2) said "nan" was already disagreeing + * with itself about one value inside one backend. This makes print agree with + * show first and the two backends agree second. + * + * The test is x != x rather than isnan, which keeps math.h out of this file + * and is the same comparison the prelude uses. An infinity still prints signed: + * there the sign is the value. */ void flan_f64_to_bytes(double x, uint8_t *buf, flan_slice *out) { - int n = snprintf((char *)buf, FLAN_NUM_BYTES, "%g", x); + int n = (x != x) ? snprintf((char *)buf, FLAN_NUM_BYTES, "nan") + : snprintf((char *)buf, FLAN_NUM_BYTES, "%g", x); out->ptr = buf; out->len = fit(n); } diff --git a/test/programs/format.flan b/test/programs/format.flan index cfe4f53..4fac218 100644 --- a/test/programs/format.flan +++ b/test/programs/format.flan @@ -61,6 +61,20 @@ (show (/ 1.0 0.0) 2) ; inf (show (/ -1.0 0.0) 2) ; -inf + ;; The same three through print, which goes to the runtime's %g rather than + ;; to format-f64, and the first of them is here for a reason the other two + ;; are not. A NaN carries a sign bit that no arithmetic chose: LLVM folds + ;; (/ 0.0 0.0) at compile time and answers the positive one, divsd answers + ;; the negative one at run time, and "%g" prints the difference. So this + ;; line printed "nan" through one backend and "-nan" through the other for + ;; the same source, and disagreed with the (show ...) above it inside either + ;; one. flan_f64_to_bytes now renders any NaN unsigned, which is what + ;; format-f64 always did. An infinity still prints signed: there the sign is + ;; the value, and both backends were always agreed about it. + (print (/ 0.0 0.0)) (println "") ; nan + (print (/ 1.0 0.0)) (println "") ; inf + (print (/ -1.0 0.0)) (println "") ; -inf + ;; Past 9e18 an f64 has no fractional bits and the integer part does not fit ;; in an i64, so this falls back to %g rather than approximating. (show 1e20 2) ; 1e+20 diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index be4901c..d06c1e4 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -719,7 +719,9 @@ let () = 1.005\n1.0001\n7.000000\n\ -0.50\n-0.00\n0.00\n0.00\n\ 2\n1.500000000\n\ - nan\ninf\n-inf\n1e+20\n1234567890123.00\n\ + nan\ninf\n-inf\n\ + nan\ninf\n-inf\n\ + 1e+20\n1234567890123.00\n\ fps 59.9 / frame 0.0167\n" in outputs "a number with a precision" "programs/format.flan" format_out;