What the sanitizer sweep found, and what a clean run does not prove
NEXT.md's queued section becomes a landed one. The headline is not the flag: ASan reaches Flan code only because Emit now attributes every define, and UBSan reaches none of it and has no lever that would, so the shift-UB and float-cast items that section listed are still open and are a compiler feature rather than a flag. The clean result is written with its reach. println.flan pushes a 1100-character string through escaped[1024] on purpose, so that buffer is genuinely covered; scratch[64] never sees more than 20 characters; and the 4K result cap, the dev registry guard, SNAP_MAX/SNAP_NAMES and condition_name[128] are on the daemon path and not in the corpus at all -- read, not tested. Two defects fixed, both found by reading. Three of bounds.flan's six out-of-bounds cases caught with the checks off, with the other three tabulated and explained, and the caveat that ASan sees out-of-object and not out-of-subobject access, so three of six is a ceiling and not a measurement. BUILT.md gets the durable half: the attribute, the absent UBSan lever, why --sanitize does not force -O0 when --debug does, and the -O0/-O2 divergence that earned it.
This commit is contained in:
parent
5810fa286f
commit
c806125742
38
BUILT.md
38
BUILT.md
@ -269,6 +269,44 @@ that split them would break the write check silently. The test covers both.
|
||||
Cost, measured: a 50M-iteration dependency chain over a 1024-element array runs at 0.11–0.12s checked against 0.12–0.13s
|
||||
unchecked. Indistinguishable.
|
||||
|
||||
## Sanitizers, and why hand-written IR does not get them for free
|
||||
|
||||
`--sanitize` builds the whole program under ASan and UBSan — the runtime's C, the generated shim, and the Flan. The last
|
||||
of those is not what passing `-fsanitize=address` to the clang run over the `.ll` gets you, and the gap is silent.
|
||||
|
||||
**AddressSanitizer is an LLVM pass, but it instruments only functions carrying the `sanitize_address` attribute.** That
|
||||
attribute is put there by clang's C frontend. `Emit` writes `.ll` by hand, so it wrote none, so the pass walked past
|
||||
every Flan function and instrumented `flan_rt.c`. The measurement that settled it: an out-of-bounds read of a `defvar`
|
||||
array in a `--no-bounds-checks` build printed its garbage and exited 0; with an `attributes #0 = { sanitize_address }`
|
||||
group named on every `define`, the same program reports `global-buffer-overflow in flan.main`. Globals are the exception
|
||||
— the module pass redzones them whether or not any function is attributed — which is why the *shape* of a sanitized
|
||||
build looked right long before it worked.
|
||||
|
||||
**UndefinedBehaviorSanitizer has no equivalent lever.** Its checks are not a pass: the C frontend emits branches to
|
||||
`__ubsan_handle_*` inline, and no attribute asks anything to produce them. So UBSan covers the C and nothing else, and
|
||||
`(<< 1 32)` is still unremarked under `-fsanitize=undefined`. Shift UB, alignment and the f32→i32 cast on NaN are
|
||||
therefore a compiler feature if they are wanted — checks emitted from `Emit` behind the flag, the same shape the bounds
|
||||
checks already have — and not a flag away. `test_sanitize` pins both halves with controls: one program that must report
|
||||
and one that must not, so either fact changing is a test failure rather than a discovery.
|
||||
|
||||
`-fno-sanitize=signed-integer-overflow` is the only exclusion, because wrapping is what this language's arithmetic
|
||||
means and without it every program trips on its first `+`.
|
||||
|
||||
**The flag deliberately does not force `-O0`,** unlike `--debug`, whose reason (mem2reg deletes the alloca a
|
||||
`llvm.dbg.declare` describes) does not apply. The optimiser is half of what is being measured, and `bounds.flan` proves
|
||||
it: with checks off, its read past the end of a string constant is reported at `-O0` and silent at `-O2`, because an
|
||||
out-of-bounds `inbounds` getelementptr into a constant is poison and LLVM folds the load away. The program then prints a
|
||||
wrong answer instead of touching memory. Same family as `(<< 1 32)` compiling to a bare `retq`.
|
||||
|
||||
**What ASan covers of the bounds checks' job, since `--sanitize --no-bounds-checks` is the run that asks.** Three of
|
||||
`bounds.flan`'s six deliberate out-of-bounds cases are caught. A negative index into a global is not — a global gets a
|
||||
right redzone and nothing to its left. Neither is a reversed slice, which computes a negative length and then reads
|
||||
nothing at all. ASan sees out-of-*object* access, not out-of-subobject, so a slice into the middle of a larger array can
|
||||
overrun its logical bounds without crossing a redzone at all. It is a second net, not a replacement.
|
||||
|
||||
The sweep lives on its own dune alias rather than on `dune test`: a sanitized program links to a statically linked 1.8MB
|
||||
binary, and twenty-eight of them twice over is minutes against the suite's seconds.
|
||||
|
||||
## Why there is no interpreter
|
||||
|
||||
Open decision #7 is settled: **the compiled path is the only backend.** Both arguments for a permanent interpreter had
|
||||
|
||||
99
NEXT.md
99
NEXT.md
@ -62,39 +62,84 @@ the commit that made it.
|
||||
`-2851001042534928384` — the same 64 bits, printed unsigned now that `hash-grid`'s `u64` no longer goes through an
|
||||
`(i64 …)` cast — and a trap column shifted because the call it names got shorter.
|
||||
|
||||
### Queued — the runtime under a sanitizer
|
||||
### Landed — the runtime under a sanitizer
|
||||
|
||||
Nothing has ever run under ASan or UBSan on the test path. `grep -i 'sanitize\|asan\|valgrind'` over `lib/ bin/ test/
|
||||
runtime/ vendor/` returns nothing at all. This is not a big project — the whole C surface is about 1,260 lines
|
||||
(`flan_rt.c` 394, `flan_dev.c` 219, `flan_agent.c` 647) plus what `shim.ml` generates.
|
||||
`--sanitize` is a build flag beside `--debug`, and `dune build --root . @sanitize` is the sweep: twenty-eight programs
|
||||
built twice, plain and sanitized, compared on output and exit status. It is not on `dune test` — a sanitized program is
|
||||
a statically linked 1.8MB binary and the sweep is about nine minutes against the suite's seconds.
|
||||
|
||||
**The bugs are not in allocation.** There are four `malloc`/`calloc`/`strdup` sites in the entire runtime and every one
|
||||
is allocate-once-never-free by design — `rt_args` says so in its own comment — so LeakSanitizer would mostly produce
|
||||
suppressions. The risk is **fixed static buffers with bounds arithmetic**, and the ones with no coverage are already
|
||||
written down: `scratch[SCRATCH]` and `escaped[ESCAPE_MAX]` in `flan_rt.c`, the 4K result cap, the registry overflow
|
||||
guard, and `SNAP_MAX`/`SNAP_NAMES` from the restart snapshot.
|
||||
**The flag was the easy half. What the sanitizers reach is not symmetric, and this is the thing to remember:**
|
||||
|
||||
There is evidence the sweep pays. Checking `flan_escape_bytes` by hand against lengths 0–1300 under ASan with a red
|
||||
zone found the guard correct but its comment understating its own reserve by four bytes — worst output 1021 into 1024.
|
||||
That was one buffer, found by looking.
|
||||
- **ASan reaches Flan code only because `Emit` now says so.** AddressSanitizer is an LLVM pass but it instruments only
|
||||
functions carrying the `sanitize_address` attribute, which clang's *C frontend* adds and which nothing adds to IR
|
||||
written by hand. Before that attribute, `clang -fsanitize=address` over the `.ll` instrumented `flan_rt.c` and not one
|
||||
instruction of Flan: a read off the end of a `defvar` array in a `--no-bounds-checks` build printed its garbage and
|
||||
exited 0. With it, the same program reports `global-buffer-overflow in flan.main`. Globals get their redzone from the
|
||||
module pass either way. `test_sanitize`'s first control is that exact program, so the day the attribute stops being
|
||||
emitted the sweep fails loudly instead of going quietly green.
|
||||
- **UBSan reaches the runtime's C and nothing else, and there is no lever for it.** Its checks are branches to
|
||||
`__ubsan_handle_*` that clang's C frontend emits; no attribute asks a pass to produce them. `(<< 1 32)` under
|
||||
`-fsanitize=undefined` is still unremarked. **Item 3 of the old plan — shift UB, alignment, the f32→i32 cast on NaN —
|
||||
is therefore not answerable this way, and is still open.** The choices are to emit the checks from `Emit` behind the
|
||||
flag (a compiler feature, and the same shape the bounds checks already have) or to leave those to the checker. The
|
||||
second control in `test_sanitize` is a program with unambiguous shift UB that is expected *not* to be caught, so if a
|
||||
future clang changes this, the sweep says so.
|
||||
|
||||
The shape:
|
||||
`-fno-sanitize=signed-integer-overflow` is the one exclusion, because wrapping is what this language's arithmetic means.
|
||||
Nothing else is excluded. The flag does **not** force `-O0` the way `--debug` does; see below for why that earned its
|
||||
keep. `--sanitize --debug` together works and gives `-O0` plus source lines in the report.
|
||||
|
||||
1. A `--sanitize` flag beside `--debug` in `lib/build.ml`, reaching both the clang run over the `.ll` and the runtime's
|
||||
own C.
|
||||
2. Run the existing corpus under it. `test/programs/` is about forty programs with pinned output — a second pass over
|
||||
them is the cheapest coverage available here, and needs no new test written.
|
||||
3. **UBSan is worth more than ASan**, with one exclusion that is not optional: arithmetic wraps by design, so
|
||||
`-fno-sanitize=signed-integer-overflow` or every program trips on the first `+`. What is left is real — shift UB
|
||||
(`(<< 1 32)` compiled to a bare `retq` at -O2, see Sharp edges), alignment, and the f32→i32 cast on NaN or an
|
||||
infinity that `floor-f32` guards by hand and nothing else does.
|
||||
4. The variant worth its own run: **ASan with `--no-bounds-checks`**. That asks whether the bounds checks are the only
|
||||
thing between the language and corruption, which the checked build cannot ask.
|
||||
**The checked sweep is clean: 28 programs, no ASan report, no UBSan report, no divergence from the unsanitized run.**
|
||||
What that does and does not prove:
|
||||
|
||||
Two limits, so nobody is surprised. raylib and libm are not instrumented, so the windowed examples are noise and the
|
||||
headless corpus is the target — `sand-headless`, `values`, `machine`, `virtual-controls-headless`. And ASan does not
|
||||
see uninitialised reads, which is where `zeroed` and struct padding live; that wants Valgrind as a slower second pass,
|
||||
because MSan needs every dependency instrumented and raylib settles that.
|
||||
- It **does** cover `escaped[ESCAPE_MAX]` at its boundary. `println.flan` prints a 1100-character string inside a struct
|
||||
on purpose; the escaped output is 1019 bytes against a hand-verified worst case of 1021 into 1024. That buffer is
|
||||
genuinely exercised.
|
||||
- It says **nothing** about `scratch[SCRATCH]`, whose longest reachable output is 20 characters (`%lld`) into 64.
|
||||
- It says **nothing at all** about the 4K result cap, the dev registry overflow guard, `SNAP_MAX`/`SNAP_NAMES` or
|
||||
`condition_name[128]`. Those are on the dev and agent paths, which need a daemon and a socket and are not in the
|
||||
sweep's corpus. They were read and the guards are correct; that is reading, not evidence.
|
||||
|
||||
**Two defects, both found by reading under the sanitizer rather than by the sanitizer, both fixed.**
|
||||
|
||||
- `flan_bytes_to_i64` and `flan_bytes_to_f64` clamped with `(size_t)n < sizeof buf - 1`, and a slice's length is signed:
|
||||
`(slice s 2 1)` is −1, `(size_t)(-1)` is not less than 511, so the `memcpy` read 63 or 511 bytes out of a five-byte
|
||||
string constant. Every other `(ptr, len)` entry point in the runtime already folded a negative length to zero, so this
|
||||
was two exceptions and not a missing convention. A checked build traps on the reversed slice first, which is why it
|
||||
took `--no-bounds-checks` to show. Regression case in `test_sanitize`.
|
||||
- The three `snprintf` shims published `scratch` as a slice using snprintf's return, which is what it *would* have
|
||||
written. No format here can reach 64, so it could not fire; it is clamped anyway, because the distance between "cannot
|
||||
fire" and "hands out a length past the end of a static buffer" is one format string.
|
||||
|
||||
**Left, deliberately.** `break_loop` prints the condition name with `"%.*s"` and a negative `namelen` would drop the
|
||||
precision and read to a NUL that a Flan string does not have — compiler-emitted and not reachable from source, so it is
|
||||
recorded rather than fixed. `flan_bytes_to_f64` silently parses only the first 511 bytes, which changes a value rather
|
||||
than corrupting memory.
|
||||
|
||||
**ASan with `--no-bounds-checks`, the variant that asks whether the checks are the only thing holding the line. They
|
||||
mostly are.** Of `bounds.flan`'s six deliberate out-of-bounds cases ASan catches three:
|
||||
|
||||
| case | what it does | ASan |
|
||||
|---|---|---|
|
||||
| `3`, `7` | read and write past a 3-element global | caught |
|
||||
| `4` | slice `hi` past the end of a string constant | caught |
|
||||
| `-1` | negative index into a global | **silent** — a global gets a right redzone and nothing on its left |
|
||||
| `9` | read past the end of a string constant | **silent at -O2, caught at -O0** |
|
||||
| `2` | reversed slice, negative length | silent — nothing is read at all |
|
||||
|
||||
Three of six is an upper bound on ASan's cover, not a measured fraction of the risk: ASan sees out-of-*object* access,
|
||||
not out-of-subobject, so a slice into the middle of a larger array can overrun its logical bounds without crossing a
|
||||
redzone, and the `-1` case is one instance of that class. **ASan is not a substitute for the bounds checks.**
|
||||
|
||||
Case `9` is why `--sanitize` does not force `-O0`. At `-O2` the access does not happen: an out-of-bounds `inbounds`
|
||||
getelementptr into a constant is poison, LLVM folds the load away, and the program prints a wrong answer instead of
|
||||
touching anything. Same family as `(<< 1 32)` compiling to a bare `retq` under Sharp edges. Running the sweep at both
|
||||
levels is cheap and a divergence between them is itself the finding.
|
||||
|
||||
**Still not done.** Valgrind over the headless corpus, for the uninitialised reads ASan cannot see — where `zeroed` and
|
||||
struct padding live. MSan is out because it needs every dependency instrumented and raylib settles that. The reload path
|
||||
is uninstrumented whatever the flag says: a redefinition module is built by `llc` and `ld`, not by clang, so nothing
|
||||
puts a pass over it.
|
||||
|
||||
### Managed classes are planned. Do not start them.
|
||||
|
||||
|
||||
@ -235,10 +235,12 @@ let unchecked_controls () =
|
||||
let () =
|
||||
match Sys.command "command -v clang > /dev/null 2>&1" with
|
||||
| 0 ->
|
||||
(* A read five past the end of a four-element global. Five and not ten:
|
||||
ASan's redzone on a global this small is 16 bytes, so an index far
|
||||
enough past the end lands beyond the redzone and is not seen — which is
|
||||
itself worth knowing about what this tool can do. *)
|
||||
(* A read one past the end of a four-element global. Index 5 and not 9,
|
||||
and the difference is worth knowing: ASan registers this array as
|
||||
"16 bytes in a 32-byte slot", so the poisoned redzone is bytes 16..31.
|
||||
Index 5 is byte 20 and is caught; index 9 is byte 36, past the
|
||||
registration entirely, and is silent. Overrunning a small object by
|
||||
enough lands back in ordinary memory. *)
|
||||
control ~expect_report:true "flan-san-ctl-oob"
|
||||
~why:"This sweep is not instrumenting Flan code at all — check that \
|
||||
Emit still puts every define in the sanitize_address attribute \
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user