From b93b6120d17868d526dea5044eadd96aa20f37f2 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 18 Sep 2026 07:36:21 +0700 Subject: [PATCH 1/3] A reversed slice is not a slice, in every build The lo <= hi test in check_slice and slice-from-ptr's n >= 0 sat behind --no-bounds-checks in both backends, while the comment beside each said they could not be dropped. They are not bounds checks: hi <= len asks whether a range fits inside a length, and lo <= hi asks whether the word about to be written into a %slice's length field is a count at all. The first stays behind the flag, the second is now emitted everywhere, the way flan_vec_as_slice has always validated its own l > h in plain C. emit.ml emits two signal blocks rather than one and i1, so an unchecked build carries one compare. x86.ml keeps all three frame temporaries stored outside the flag and gates only the second compare, because the third is the length the message prints. The IR assertion in test_acceptance now says the two slice calls are present under --no-bounds-checks rather than absent, and the same build is run: case 2 and case -2 of bounds.flan must still die. --- docs/BUGS-2026-09-18.md | 11 ++-- docs/BUILT.md | 47 ++++++++++++++++ lib/emit.ml | 78 ++++++++++++++++++-------- lib/x86.ml | 114 +++++++++++++++++++++++++------------- runtime/flan_rt.c | 20 +++++-- test/programs/bounds.flan | 10 +++- test/test_acceptance.ml | 65 +++++++++++++++++++--- test/test_sanitize.ml | 15 +++-- test/test_valgrind.ml | 13 +++-- 9 files changed, 283 insertions(+), 90 deletions(-) diff --git a/docs/BUGS-2026-09-18.md b/docs/BUGS-2026-09-18.md index 1a3b14c..827942e 100644 --- a/docs/BUGS-2026-09-18.md +++ b/docs/BUGS-2026-09-18.md @@ -72,10 +72,13 @@ territory; fix or record, the lane's call. (printed garbage). Breaks the premise stated in the clone note at check.ml:4152. Candidate fixes: refuse `free` of a non-binding target, or region-check the element at `push`/`put`. Sixth on the list; needs a deliberate mixed-allocator construction. -- **Reversed slice under `--no-bounds-checks`**: the `lo <= hi` test is a representation - invariant, not a bounds check, but sits behind `if f.md.checks` in both backends - (`emit.ml:1037`, `x86.ml:2164`; same for SliceFromPtr's `n >= 0`). A negative-length - slice reaches user code. `flan_vec_as_slice` checks unconditionally — the model. +- **Reversed slice under `--no-bounds-checks`** — **fixed**. The `lo <= hi` test is a + representation invariant, not a bounds check, but sat behind `if f.md.checks` in both + backends (`emit.ml:1037`, `x86.ml:2164`; same for SliceFromPtr's `n >= 0`), so a + negative-length slice reached user code. Split in both backends: `hi <= len` stays + behind the flag, `lo <= hi` and `n >= 0` are now emitted in every build, through the + same slice-failure path. `flan_vec_as_slice` was the model. See "A slice's length word + is a count" in docs/BUILT.md. - **`reg leaks` lies at >3072 live blocks** (`runtime/flan_dev.c:1521`): compaction then fires on every allocation, the epoch stays odd, all 8 scan retries fail, and `flan_dev_reg_by_type` returns 0 — measured 198/200 wrong answers on a full table. diff --git a/docs/BUILT.md b/docs/BUILT.md index 5f33f1a..5919e59 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -5695,3 +5695,50 @@ position, and requires the error overlay to start at exactly that position. The in-buffer `m` sends its text *un*padded, which is the honest shape there: the expansion is in no file, so there is no line or column for a refusal to be drawn at. The `:file` still goes on the wire, because that is what says which session's macros to expand against. + +## A slice's length word is a count + +`--no-bounds-checks` used to drop two different claims because they were written as one +`and`. Splitting them is the whole of the change in `check_slice`, in both backends. + +`hi <= len` is a **bounds check**. It asks whether the range a caller wrote fits inside +the thing being sliced, and the answer depends on a length that has nothing to do with +the result's shape. Dropping it is what the flag is for: a release decision, taken by +someone who has decided their indices are right and will accept undefined behaviour if +they are not. It stays behind `f.md.checks`. + +`lo <= hi` is **not a bounds check**, and the old comment beside it said as much while the +code did the opposite. A slice is `{ptr, i64}` and the `i64` is a count: the emitted +`sub` computes it as `hi - lo`, and the `len` primitive, a re-slice, `flan_write_stdout` +and any C the value is handed to all read it as a non-negative number of elements. +`(slice s 2 1)` does not build an out-of-range slice, it builds a value that is not a +slice — the length word holds -1, which as a count is 18446744073709551615. No build +wants that, so no flag turns the test off. `flan_vec_as_slice` in the runtime has always +validated its own `l > h` unconditionally, in plain C, on the same grounds; this is that +rule arriving on the emitted path. + +`slice-from-ptr`'s `n >= 0` is the same claim spelled the other way, and it moved out +from behind the flag with it. The argument for gating it read well — dropping bounds +checks is a release decision, so this goes off with the rest — and was a category error: +a bounds check compares an index against a length the compiler knows, and this form has +no length to compare against, which is the first thing its own comment says. What it +tests is that the word about to become the slice's count is a count. + +Mechanically: `emit.ml` emits two `signal_block`s rather than one `and i1`, so an +unchecked build carries exactly one compare and a checked one carries the two it always +did. `x86.ml` keeps all three frame temporaries stored outside the flag and gates only +the second compare — the third temporary is the length the message prints, and gating its +store with its compare would trap correctly with a garbage number in the text, which is +the kind of wrong answer that builds, links, and passes any test that reads the IR. + +Both still report through `flan_slice_error` (`flan_slice_promise_error` for the promise), +because from a handler's point of view there is one condition here — a range that was +refused — and which half was violated is in the sentence, not in the type. + +The runtime's `clamp_len` stays. It was written *because* this hole existed: a release +build handed it a length of -1 and it was the last thing between that and a 511-byte read +off the end of a slice. `check_slice` no longer lets the value out of Flan, but +`clamp_len` takes a raw `(ptr, len)` pair, and the FFI, a C caller and a caller's own +`slice-from-ptr` promise all reach it. A function correct on its own arguments does not +become incorrect because its callers improved. + diff --git a/lib/emit.ml b/lib/emit.ml index a76ec7a..94cfa21 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -1031,22 +1031,49 @@ let check_at f ~guard loc idx len = end (* [slice] is not: a slice ending at len — or an empty one at lo = len — is - legal, and its one-past-the-end gep is defined. [lo <= hi] is not redundant - with it, because a reversed range would otherwise yield hi - lo as a huge - unsigned length, which is a worse hole than the missing check. *) + legal, and its one-past-the-end gep is defined. + + Two tests, and they are not the same kind of test, which is the whole of + what this function has to get right. [hi <= len] is a bounds check: it asks + whether the range the caller wrote fits inside the thing being sliced, and + the answer depends entirely on a length that is nothing to do with the + result's representation. Dropping it is what [--no-bounds-checks] is for — + a release decision, taken by someone who has decided their indices are + right and will accept undefined behaviour if they are not. + + [lo <= hi] is not that. The value this expression builds is a [%slice], + which is {ptr, i64}, and the i64 is a *count*: the sub below computes it as + hi - lo, and every consumer in the language and in the runtime reads it as + a non-negative number of elements. A reversed range does not produce an + out-of-range slice, it produces a slice that is not a slice — (slice s 2 1) + writes -1 into the length word, and -1 as an unsigned count is + 18446744073709551615. That value is not a bounds error anyone can opt out + of; it is a malformed value of the type, and it goes on to be passed, + stored, re-sliced and handed to C. So the test rides ahead of the flag: it + is emitted in every build, at -O0, at -O2, with checks on and with checks + off, exactly the way flan_vec_as_slice in the runtime validates [l > h] + unconditionally and for the same reason. + + Two [signal_block]s and not one [and], so that the unchecked build emits + exactly one compare and the checked build emits the two it always did. Both + report through @flan_slice_error with the same three numbers, because from + a handler's point of view there is still one condition here — a range that + was refused — and which half of it was violated is in the text. *) let check_slice f ~guard loc lo hi len = - if f.md.checks then begin - let a = fresh f in - ins f "%s = icmp ule i64 %s, %s" a lo hi; - let b = fresh f in - ins f "%s = icmp ule i64 %s, %s" b hi len; - let ok = fresh f in - ins f "%s = and i1 %s, %s" ok a b; + let fail ok = signal_block f loc ~guard ok (fun id n -> ins f "call void @flan_slice_error(ptr %s, i64 %d, i64 %s, i64 %s, i64 %s, \ ptr %s)" id n lo hi len xfer_param) + in + let a = fresh f in + ins f "%s = icmp ule i64 %s, %s" a lo hi; + fail a; + if f.md.checks then begin + let b = fresh f in + ins f "%s = icmp ule i64 %s, %s" b hi len; + fail b end (* ── Expressions ───────────────────────────────────────────────────── *) @@ -2129,10 +2156,19 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) = to i64 is a huge unsigned value that [ule] waves straight through. It goes through [signal_block] for the reason the other two bounds checks - do — a bad length signals BoundsError and is answerable — and behind - [f.md.checks] for the reason they are: dropping bounds checks is a release - decision, not an optimisation one, so this is on at -O0 and -O2 alike and - off only when checks as a whole were asked off. + do — a bad length signals BoundsError and is answerable. It is *not* + behind [f.md.checks], and the argument that it should be was the argument + this paragraph used to make: that dropping bounds checks is a release + decision, so this goes off with the rest of them. That reads well and is + a category error. A bounds check compares a caller's index against a + length the compiler knows; this has no length to compare against — the + paragraph above says so in its first sentence — so there is nothing here + for [--no-bounds-checks] to be dropping. What it tests is that the word + about to be written into the [%slice]'s length field is a count and not a + negative number reinterpreted as an enormous one. That is [check_slice]'s + [lo <= hi], spelled the other way round, and it holds in every build for + the same reason: a slice with a negative length is not an unchecked slice, + it is not a slice. It has its own runtime function, @flan_slice_promise_error, and that is the whole of what it needed. It used to borrow @flan_slice_error — the @@ -2148,14 +2184,12 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) = let nv = value f n in let n64 = fresh f in ins f "%s = sext i32 %s to i64" n64 nv; - if f.md.checks then begin - let ok = fresh f in - ins f "%s = icmp sge i64 %s, 0" ok n64; - signal_block f e.Tast.loc ~guard:(fun () -> guard f) ok (fun id len -> - ins f - "call void @flan_slice_promise_error(ptr %s, i64 %d, i64 %s, ptr %s)" - id len n64 xfer_param) - end; + let ok = fresh f in + ins f "%s = icmp sge i64 %s, 0" ok n64; + signal_block f e.Tast.loc ~guard:(fun () -> guard f) ok (fun id len -> + ins f + "call void @flan_slice_promise_error(ptr %s, i64 %d, i64 %s, ptr %s)" + id len n64 xfer_param); let a = fresh f in ins f "%s = insertvalue %%slice zeroinitializer, ptr %s, 0" a pv; let b = fresh f in diff --git a/lib/x86.ml b/lib/x86.ml index 0c7249a..a2e74f9 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -2158,37 +2158,63 @@ and check_at f (base : loc) (ty : Types.t) (i : Tast.expr) (iv : loc) = lbl f.b ok) (* [slice] is not strict: a slice ending at len — or an empty one at lo = len — - is legal. [lo <= hi] is not redundant with [hi <= len], because a reversed - range would otherwise yield hi - lo as a huge unsigned length, which is a - worse hole than the missing check. *) + is legal. Two compares, and only one of them is a bounds check. + + [hi <= len] is the bounds check. It asks whether the caller's range fits + inside the thing being sliced, which is a question about a length this + backend has to go and load, and [--no-bounds-checks] exists to stop asking + it — the release decision, taken by someone who accepts undefined behaviour + if their indices are wrong. + + [lo <= hi] is a different claim and survives the flag. The two words stored + at the bottom of this case are a slice, and the second is a *count*: the + `sub` in the caller computes hi - lo, and everything downstream — the len + primitive, a re-slice, flan_write_stdout, any C this is handed to — reads + it as a non-negative number of elements. A reversed range does not build an + out-of-range slice, it builds a value that is not a slice: (slice s 2 1) + stores -1, and -1 read as a count is 18446744073709551615. There is no + build in which that is the intended behaviour, so there is no flag that + turns the compare off. flan_vec_as_slice validates its own [l > h] + unconditionally in plain C and always has; this is the same rule, arriving + late on the emitted path. + + Hence the shape below. All three frame temporaries are stored before either + compare and outside the flag, because [bounds_call] reads all three and the + third is the length the message prints — gate the store along with the + compare and an unchecked build traps with the right range beside a garbage + length, which is a wrong answer that builds, links and passes every test + that reads the IR rather than the text. *) and check_slice f (base : loc) (ty : Types.t) (loc : Loc.t) (lo : Tast.expr) (llo : loc) (hi : Tast.expr) (lhi : loc) = - if f.md.Emit.checks then - let len = - match ty with - | Types.Array (n, _) -> Some (`Const n) - | Types.Slice _ | Types.String -> Some (`At (shift base 8)) - | _ -> None - in - match len with - | None -> () - | Some len -> - scoped f (fun () -> - let a = ptmp f and b = ptmp f and c = ptmp f in - load_loc f ~reg:rax llo lo.Tast.ty; - store_int f.b ~src:rax ~mm:(Frame a) ~size:8; - load_loc f ~reg:rdx lhi hi.Tast.ty; - store_int f.b ~src:rdx ~mm:(Frame b) ~size:8; - load_len f len; - store_int f.b ~src:rcx ~mm:(Frame c) ~size:8; - let ok = new_label f "inb" and bad = new_label f "oob" in - cmp_rr f.b ~a:rax ~c:rdx; + let len = + match ty with + | Types.Array (n, _) -> Some (`Const n) + | Types.Slice _ | Types.String -> Some (`At (shift base 8)) + | _ -> None + in + match len with + | None -> () + | Some len -> + scoped f (fun () -> + let a = ptmp f and b = ptmp f and c = ptmp f in + load_loc f ~reg:rax llo lo.Tast.ty; + store_int f.b ~src:rax ~mm:(Frame a) ~size:8; + load_loc f ~reg:rdx lhi hi.Tast.ty; + store_int f.b ~src:rdx ~mm:(Frame b) ~size:8; + load_len f len; + store_int f.b ~src:rcx ~mm:(Frame c) ~size:8; + let ok = new_label f "inb" in + cmp_rr f.b ~a:rax ~c:rdx; + if f.md.Emit.checks then begin + let bad = new_label f "oob" in jcc_lbl f.b ~cc:cc_a bad; cmp_rr f.b ~a:rdx ~c:rcx; jcc_lbl f.b ~cc:cc_be ok; - lbl f.b bad; - bounds_call f "flan_slice_error" loc [ a; b; c ]; - lbl f.b ok) + lbl f.b bad + end else + jcc_lbl f.b ~cc:cc_be ok; + bounds_call f "flan_slice_error" loc [ a; b; c ]; + lbl f.b ok) (* [emit.ml]'s [check_div] and [check_cast], item 3 of docs/handoffs/HANDOFF-x86-rt.md's list, and the one item on it that was blocked on a language decision rather @@ -2644,23 +2670,31 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst = It reuses [flan_slice_error] for [emit.ml]'s reason: the violated condition is 0 <= n, which has the shape of a reversed slice, so the range - is reported as [0 n) against a length of 0. *) + is reported as [0 n) against a length of 0. + + It is not behind [f.md.Emit.checks], and the reason is the one + [check_slice] above spells out at length. [--no-bounds-checks] drops a + comparison against a known length; this comparison has no length to be + against — the paragraph above says as much — so the flag has nothing here + to drop. The word being stored into the second half of [dst] is the + slice's count, and a count that is negative is not a slice with the + bounds check taken off, it is not a slice. So the test runs in every + build, exactly as [lo <= hi] does. *) | Tast.SliceFromPtr, [ p; n ] -> let lp = eval f p in let ln = eval f n in - if f.md.Emit.checks then - scoped f (fun () -> - let a = ptmp f and b = ptmp f and c = ptmp f in - xor_rr f.b ~dst:rax ~src:rax; - store_int f.b ~src:rax ~mm:(Frame a) ~size:8; - store_int f.b ~src:rax ~mm:(Frame c) ~size:8; - load_loc f ~reg:rax ln n.Tast.ty; - store_int f.b ~src:rax ~mm:(Frame b) ~size:8; - cmp_imm f.b ~dst:rax 0; - let ok = new_label f "inb" in - jcc_lbl f.b ~cc:cc_ge ok; - bounds_call f "flan_slice_error" e.Tast.loc [ a; b; c ]; - lbl f.b ok); + scoped f (fun () -> + let a = ptmp f and b = ptmp f and c = ptmp f in + xor_rr f.b ~dst:rax ~src:rax; + store_int f.b ~src:rax ~mm:(Frame a) ~size:8; + store_int f.b ~src:rax ~mm:(Frame c) ~size:8; + load_loc f ~reg:rax ln n.Tast.ty; + store_int f.b ~src:rax ~mm:(Frame b) ~size:8; + cmp_imm f.b ~dst:rax 0; + let ok = new_label f "inb" in + jcc_lbl f.b ~cc:cc_ge ok; + bounds_call f "flan_slice_error" e.Tast.loc [ a; b; c ]; + lbl f.b ok); load_loc f ~reg:rax lp p.Tast.ty; store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:8; load_loc f ~reg:rax ln n.Tast.ty; diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index 3105bad..e53c6fe 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -268,11 +268,21 @@ static int64_t fit(int n) { * here. Below was not, and it was the real one: a slice's length is a signed * 64-bit count, (slice s 2 1) computes 2 - 1 - 2 = -1, and `(size_t)n` on a * negative n is 18446744073709551615, which is not less than 511, so k became - * 511 and the memcpy read 511 bytes from wherever the slice pointed. A checked - * build traps on the reversed slice before it gets here; an unchecked one does - * not, and every other (ptr, len) entry point in this file — flan_write_stdout, - * flan_escape_bytes, flan_dev_emit — already guards the negative case. These - * two were the exceptions. */ + * 511 and the memcpy read 511 bytes from wherever the slice pointed. Every + * other (ptr, len) entry point in this file — flan_write_stdout, + * flan_escape_bytes, flan_dev_emit — already guarded the negative case. These + * two were the exceptions. + * + * It is worth saying why this stays now that (slice s 2 1) traps in every + * build and not only in a checked one. This clamp was written when it did not: + * lo <= hi sat behind --no-bounds-checks in both backends, so a release build + * handed a length of -1 straight to these functions, and the clamp was the + * last thing between that and a 511-byte read. check_slice no longer lets the + * value out, which makes the negative case unreachable *from Flan* — and not + * from here, because these take a raw (ptr, len) pair and the FFI, a C caller + * and slice-from-ptr's promise all reach them too. A function that is correct + * on its own arguments does not become incorrect because its callers improved, + * and two branches are not the price to argue about. */ static size_t clamp_len(int64_t n, size_t cap) { if (n <= 0) return 0; return (uint64_t)n < (uint64_t)cap ? (size_t)n : cap; diff --git a/test/programs/bounds.flan b/test/programs/bounds.flan index def7bdd..228c519 100644 --- a/test/programs/bounds.flan +++ b/test/programs/bounds.flan @@ -1,6 +1,14 @@ ;;;; Bounds checks, NEXT.md item 2. One program, one case per argument, so a ;;;; trap is observable: the checked build exits 134 with the source location -;;;; on stderr, the unchecked one runs off the end and is not asserted on. +;;;; on stderr. +;;;; +;;;; The unchecked build is not uniform, and the split is the point. An index +;;;; past the end runs off the end there and is not asserted on — that is what +;;;; --no-bounds-checks buys. Two of the cases below still trap: the reversed +;;;; range at n = 2 and the negative promise at n = -2, because neither is a +;;;; bounds check. Both are the claim that a slice's length word is a count, +;;;; and a build that drops them does not produce an unchecked slice, it +;;;; produces a value that is not one. See check_slice in lib/emit.ml. ;;;; ;;;; The selector is also the index wherever it can be, which is what keeps the ;;;; index dynamic — a literal would let the checker reject it outright one day diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 6451bb8..be4901c 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -1531,10 +1531,17 @@ let () = bounds (); bounds ~opt:"-O0" (); - (* The release build drops them — the calls, that is; the two declarations - stay in the header and LLVM discards the unused ones. Asserted on the IR - rather than by running an unchecked out-of-bounds program, which has no - defined behaviour to assert on. *) + (* What the release build drops, and what it does not. Asserted on the IR + for the first half, because an index past the end has no defined + behaviour to run and assert on; the second half is asserted by running + the program, below, because it does. + + The line: @flan_bounds_error is the bounds check and goes. The two slice + calls stay, because what survives behind them is not a bounds check — + check_slice's lo <= hi and slice-from-ptr's n >= 0 are the claim that a + %slice's length word holds a count. This assertion is written as + "present" and not merely as "no longer looked at", so that re-gating + either one on f.md.checks fails here rather than passing quietly. *) let p = Reader.read_file "programs/bounds.flan" |> Parse.program |> Check.program in @@ -1543,12 +1550,54 @@ let () = print_endline "FAIL checks on: no bounds call emitted" end; let off = Emit.program ~checks:false p in - if contains off "call void @flan_bounds_error(" - || contains off "call void @flan_slice_error(" - || contains off "call void @flan_slice_promise_error(" then begin + if contains off "call void @flan_bounds_error(" then begin incr failures; - print_endline "FAIL --no-bounds-checks: a check survived" + print_endline "FAIL --no-bounds-checks: a bounds check survived" end; + if not (contains off "call void @flan_slice_error(") then begin + incr failures; + print_endline "FAIL --no-bounds-checks: the lo <= hi invariant went too" + end; + if not (contains off "call void @flan_slice_promise_error(") then begin + incr failures; + print_endline "FAIL --no-bounds-checks: the n >= 0 invariant went too" + end; + + (* And the same thing as behaviour rather than as text. A slice built + backwards writes hi - lo into a length word that every reader takes for + a count, so the value it produces is not a slice with its bounds check + removed — it is not a slice. The same for a promise of -2 elements. + Both must still die, with the same sentence, in a build that asked for + no bounds checks at all. + + The in-bounds selector is run too, and it is the other half of the + claim: the flag still buys something, and a program that slices + correctly does not start paying for a check it was promised was gone. + + This is the one place the two halves can be told apart, and it is worth + one compile. *) + let unchecked = compile ~checks:false "programs/bounds.flan" in + let still_traps name arg reason = + let code, text = run unchecked (Some arg) in + if code <> 134 || not (contains text reason) then begin + incr failures; + Printf.printf + "FAIL %s under --no-bounds-checks\n got: %S (exit %d)\n\ + \ wanted: %S (exit 134)\n" + name text code reason + end + in + still_traps "reversed slice" "2" "slice [2 1) is out of bounds for length 5"; + still_traps "slice-from-ptr with a negative length" "-2" + "slice-from-ptr was promised -2 elements behind the pointer"; + let code, text = run unchecked (Some "0") in + if text <> "0ello\n" || code <> 0 then begin + incr failures; + Printf.printf + "FAIL in-bounds edges under --no-bounds-checks\n got: %S (exit %d)\n" + text code + end; + (try Sys.remove unchecked with Sys_error _ -> ()); (* The other half of the same change: a bad index that something *answers*. bounds.flan above is still the unhandled case and still exits 134 with diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml index 3405f17..a3f2dfc 100644 --- a/test/test_sanitize.ml +++ b/test/test_sanitize.ml @@ -230,11 +230,16 @@ let unchecked_controls () = "9", "at -O2 the load is folded away — an out-of-bounds inbounds GEP \ into a string constant is poison, so nothing is read and a wrong \ value is printed. Reported at -O0."; - "2", "a reversed slice (lo 2, hi 1), whose length comes out negative; \ - nothing is read, and flan_write_stdout ignores a negative count. \ - No access, so nothing for ASan to see — the hazard is a slice \ - with a negative length reaching user code, which is a checker \ - question" ] + "2", "a reversed slice (lo 2, hi 1), which this build traps on before \ + anything is read. It is in this list rather than out of it \ + because it used to be here for the opposite reason: the length \ + came out negative, nothing was read, and ASan had nothing to \ + see, which made a slice with a negative length reaching user \ + code a checker question and not a sanitizer one. The checker \ + answered it — lo <= hi is a representation invariant and no \ + longer sits behind --no-bounds-checks — so ASan is still silent \ + here and now for a better reason. The trap itself is asserted in \ + test_acceptance.ml" ] in match compile ~sanitize:true ~checks:false "programs/bounds.flan" with | exception Failure m -> fail "unchecked bounds.flan: build: %s" m diff --git a/test/test_valgrind.ml b/test/test_valgrind.ml index 3577948..2d646ef 100644 --- a/test/test_valgrind.ml +++ b/test/test_valgrind.ml @@ -261,11 +261,14 @@ let corpus = It is a subset and not the whole corpus because --no-bounds-checks turns out to remove much less than its name suggests, and that is worth writing - down: [check_at] and [check_slice] in emit.ml are behind the flag, but a - Vec's and a Map's bounds checks are not — they live inside flan_vec_at and - the map probe in flan_rt.c, are plain C, and run in every build. So the - flag lowers the guard on fixed arrays and slices only. These are the - programs where that distinction reaches heap storage. *) + down: [check_at] is behind the flag and so is *half* of [check_slice] — the + [hi <= len] compare — while its [lo <= hi] stays, because that one is the + claim that a slice's length word is a count and not a bounds check at all. + A Vec's and a Map's bounds checks are not behind it either: they live inside + flan_vec_at and the map probe in flan_rt.c, are plain C, and run in every + build. So the flag lowers the guard on indexing a fixed array or a slice, + and on nothing else. These are the programs where that distinction reaches + heap storage. *) let unchecked_subset = [ "programs/allocators.flan", []; "programs/edn.flan", []; From 885470820e9600099e44847c7ff34777aa3dd1c0 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 18 Sep 2026 07:37:14 +0700 Subject: [PATCH 2/3] 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; From d11dfd8a443b48e140797fa666d5b56e79e281e7 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 18 Sep 2026 07:59:41 +0700 Subject: [PATCH 3/3] The reversed slice the survey can reach bounds.flan covers this already and the x86 survey cannot see it: the program picks its case out of (at args 1) and survey.sh runs everything with no arguments, so re-gating x86's lo <= hi would have failed nothing. This probe reaches the reversed slice on its own, through (len args) so that neither optimiser can fold the branch and the checker has no literal to object to. It matches under the default sweep and under SURVEY_FLAGS=--no-bounds-checks, which is the claim. Also records what the same reading turned up and did not fix: x86 still reports a negative slice-from-ptr promise through flan_slice_error, so the two backends print different sentences for it, and no corpus program reaches that case without arguments. --- docs/BUGS-2026-09-18.md | 9 +++++++++ spike/x86/p11-reversed-slice.flan | 26 ++++++++++++++++++++++++++ 2 files changed, 35 insertions(+) create mode 100644 spike/x86/p11-reversed-slice.flan diff --git a/docs/BUGS-2026-09-18.md b/docs/BUGS-2026-09-18.md index fb24cc4..ed21ee6 100644 --- a/docs/BUGS-2026-09-18.md +++ b/docs/BUGS-2026-09-18.md @@ -107,6 +107,15 @@ territory; fix or record, the lane's call. 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. +- **x86's slice-from-ptr refusal is the wrong sentence**: `x86.ml` still reports a + negative promise through `flan_slice_error` — "slice [0 -2) is out of bounds for + length 0", naming a range and a length the caller never wrote — where `emit.ml` has + its own `flan_slice_promise_error`. Same condition and same exit on both sides, only + the text differs. The survey cannot see it: `bounds.flan` picks its case out of + `(at args 1)` and `survey.sh` runs every program with no arguments, so nothing in the + corpus reaches the `n = -2` case on the x86 path. Noticed while making the check + unconditional (which did not change what it prints); the fix is one `bounds_call` with + one extra instead of three. - **`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/spike/x86/p11-reversed-slice.flan b/spike/x86/p11-reversed-slice.flan new file mode 100644 index 0000000..d276d4e --- /dev/null +++ b/spike/x86/p11-reversed-slice.flan @@ -0,0 +1,26 @@ +;;;; A slice built backwards, for the survey rather than for a person. +;;;; +;;;; test/programs/bounds.flan already covers this, and cannot cover it here: +;;;; it picks its case out of (at args 1) and survey.sh runs every program +;;;; with no arguments at all. So the one backend comparison that would catch +;;;; check_slice's lo <= hi being re-gated on --no-bounds-checks is a program +;;;; that reaches the reversed slice on its own. +;;;; +;;;; What it pins is that both backends die here in *every* build. lo <= hi is +;;;; not a bounds check — it is the claim that the length word of the %slice +;;;; this expression builds is a count, and hi - lo is -1 — so +;;;; --no-bounds-checks has nothing here to drop, and running this sweep with +;;;; SURVEY_FLAGS=--no-bounds-checks must report the same MATCH as without it. +;;;; A backend that quietly builds the slice exits 0 while the other exits 134 +;;;; and the survey says DIFFER. +;;;; +;;;; The two ends come from (len args), which is 1 for a program run with no +;;;; arguments and is not a number either optimiser can see, so the branch +;;;; cannot be folded away and the checker has no literal to object to. +(defn main [args [string]] i32 + (let [s (bytes "hello") + hi (i32 (len args)) + lo (+ hi 1)] + (print (slice s lo hi)) + (println "")) + 0)