From 885470820e9600099e44847c7ff34777aa3dd1c0 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 18 Sep 2026 07:37:14 +0700 Subject: [PATCH] A NaN has no sign to print (/ 0.0 0.0) printed nan through LLVM, which folds it at compile time to the positive quiet NaN, and -nan through x86, where divsd computes the negative one. Put the operands in globals so nothing folds and both say -nan, so the divergence is the folding path and not the arithmetic. The sign bit of a NaN is not a property of the number and IEEE 754 does not specify it, so the print site is where this is answered. flan_f64_to_bytes renders any NaN as nan, and the two dev emitters do the same. That is not a new rule: format-f64 in the prelude has always answered nan for this value, so a build where (print x) said -nan and (show x 2) said nan was contradicting itself inside one backend. An infinity still prints signed. format.flan prints the three non-finite values through print as well as through show. It is in the survey corpus, so the one program pins the printed form under dune test and the agreement between backends under the survey. --- docs/BUGS-2026-09-18.md | 7 +++++-- docs/BUILT.md | 24 ++++++++++++++++++++++++ runtime/flan_dev.c | 14 ++++++++++++-- runtime/flan_rt.c | 26 ++++++++++++++++++++++++-- test/programs/format.flan | 14 ++++++++++++++ test/test_acceptance.ml | 4 +++- 6 files changed, 82 insertions(+), 7 deletions(-) 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;