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.
This commit is contained in:
parent
ce3e879e83
commit
b93b6120d1
@ -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.
|
||||
|
||||
@ -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.
|
||||
|
||||
|
||||
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
@ -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;
|
||||
|
||||
@ -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;
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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