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.
This commit is contained in:
Joseph Ferano 2026-09-18 07:37:14 +07:00
parent b93b6120d1
commit 885470820e
6 changed files with 82 additions and 7 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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