Merge: a reversed slice traps in every build, and a NaN has no sign to print
# Conflicts: # docs/BUGS-2026-09-18.md
This commit is contained in:
commit
9d73900f3e
@ -78,10 +78,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**~~ — **fixed**. Compaction now also asks
|
||||
whether there is an eighth of a table's worth of dead to reclaim, so a table full of
|
||||
live blocks stops thrashing the epoch; `flan_dev_reg_by_type` returns −1 with an unread
|
||||
@ -108,8 +111,20 @@ territory; fix or record, the lane's call.
|
||||
explicit or autoincremented, is range-checked against i32 in the parser before the collision scan,
|
||||
so the scan compares the numbers the program will actually have. Out of range is refused
|
||||
by name (`parse/enum-value-out-of-range`); explicit-duplicate aliasing stays legal.
|
||||
- **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.
|
||||
- **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.
|
||||
|
||||
@ -5723,3 +5723,74 @@ 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.
|
||||
|
||||
## 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.
|
||||
|
||||
78
lib/emit.ml
78
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
|
||||
|
||||
114
lib/x86.ml
114
lib/x86.ml
@ -2165,37 +2165,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
|
||||
@ -2666,23 +2692,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;
|
||||
|
||||
@ -221,9 +221,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);
|
||||
}
|
||||
|
||||
@ -532,9 +539,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);
|
||||
}
|
||||
|
||||
|
||||
@ -281,11 +281,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;
|
||||
@ -308,9 +318,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);
|
||||
}
|
||||
|
||||
26
spike/x86/p11-reversed-slice.flan
Normal file
26
spike/x86/p11-reversed-slice.flan
Normal file
@ -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)
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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;
|
||||
@ -1531,10 +1533,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 +1552,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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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", [];
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user