diff --git a/BUILT.md b/BUILT.md index c47e10b..385c283 100644 --- a/BUILT.md +++ b/BUILT.md @@ -557,6 +557,81 @@ 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. +## Valgrind, and the two questions a sanitizer cannot be asked + +`dune build --root . @valgrind` runs the headless corpus under memcheck: forty-seven programs checked, twelve of them a +second time with `--no-bounds-checks`, in **88 seconds** against `@sanitize`'s nine minutes — and that figure includes +the compiles, because the programs are built once here rather than twice. Memcheck is 20–50x on execution and the +corpus is small; the sanitized build's static link was always the expensive half. + +**It needs nothing from `Emit`, and that is the entire reason it was reachable.** The `sanitize_address` attribute +story above is a story about an LLVM pass that only instruments what the C frontend marked. Memcheck instruments the +*binary*: it never sees IR, never sees an attribute, and cannot tell `Emit`'s output from clang's. Hand-written IR, +the runtime's C and libc arrive on the same footing. This is also why MSan was ruled out and memcheck was not — +MSan needs every dependency instrumented and raylib settles it, and memcheck needs none. + +**The two tools are complementary and neither is a superset.** Measured on `bounds.flan`'s six deliberate +out-of-bounds cases: ASan catches three, memcheck catches **zero**. Every one of them is a global or a stack array, +and memcheck's *addressability* checking covers heap blocks only — it has no redzone concept for anything else. What +memcheck has instead is *definedness*, per byte, which ASan does not have at all. Believe neither sweep alone. + +**The control that justifies the sweep.** Index 3 of a `Vec` with len 2 and cap 4 is inside the allocation — every +addressability check in existence says it is fine, ASan among them — and was never written. Memcheck reports it, and +`--track-origins=yes` names `flan_vec_push`'s `aligned_alloc` as where the undefined bytes came from. That is +NEXT.md's "ASan does not see uninitialised reads" turned into a test. `test_valgrind.ml` also asserts a heap overrun +that must report, and a `Map` key with two seven-byte holes that must *not* — the last being direct evidence for the +emitted per-key hash and equality pair walking fields rather than bytes, where `maps.flan` could only show the +consequence. + +**What `--no-bounds-checks` actually removes, which is less than its name suggests.** `check_at` and `check_slice` in +`emit.ml` are behind the flag. 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 ordinary C, and run in every build. So the flag lowers the guard on fixed arrays and +slices only, and the single way to reach unguarded heap storage from Flan is a slice taken over a `Vec` — which is +what both positive controls do. This retro-explains why `unchecked_controls` in `test_sanitize.ml` only ever found +anything through fixed arrays. + +### What a clean run does not prove + +The sweep is clean. Enumerated, in the spirit of "three of six is a ceiling, not a measurement of the risk": + +- **Globals and stack are outside it.** Measured: 0 of 6 against ASan's 3 of 6. +- **Arena storage reused after `free-all` is not re-poisoned.** Measured, and it is the sharpest hole. Round one + writes four elements; `free-all` resets the offset and keeps the pages; round two allocates the same bytes back and + reads one it never wrote — and prints round one's `44`, with memcheck silent. Nothing told memcheck the storage + died, because from `malloc`'s point of view it did not: an arena is one `malloc(cap)` and `free-all` is an integer + going to zero inside it. So the uninitialised-read coverage the control demonstrates holds for the **heap** + allocator and not for the per-frame pattern the arena exists for. Closing it means `VALGRIND_MAKE_MEM_UNDEFINED` + in `flan_arena_proc`, which is a `runtime/` change. +- **Interior overruns inside a single allocation are invisible by construction.** The arena's alignment padding and + the gap between its offset and its capacity are one block to memcheck, so a read across a sub-object boundary + crosses nothing. The same holds for the `Map`, whose `data` is *one* allocation laid out `keys | values | hashes | + scratch`: a probe walking off the end of the hashes array into the values region is not an error memcheck can see. + "Probe overrun at high load" is therefore not clean — it is **not observable by this tool**. +- **The union aliasing case is not exercised.** `unions.flan` reassigns a payload across cases and copies a union + through a struct field, but `match` is tag-dispatched and the checker enforces it, so reading case A's bytes after + writing case B cannot be written in the language. The sweep says nothing about that `getelementptr` because no + program can reach it. +- **raylib and the windowed examples are excluded**, so nothing is claimed about them. Under memcheck this matters + more than under ASan, not less: memcheck reports on uninstrumented code too, so including them would bury the + signal rather than lose it. +- **Both positive controls had to be synthesized.** No program in the corpus reaches a state where an uninitialised + read is observable. That is what a corpus passing its own acceptance table should look like, but it means the + sweep's value is as a regression net from here on, not as evidence that the current runtime was audited and found + sound. + +`test/valgrind.supp` exists and contains **no suppressions**, which is a finding rather than an oversight: the sweep +was run with `--gen-suppressions=all` before the file existed and memcheck produced nothing to suppress — no false +positives from the hand-written IR, the arena or `zeroed`, and no true ones either. The file is the four expected +complaints with the reason each failed to appear, and the rule for adding to it: paste valgrind's own generated text, +and write above it why the report is not a bug. + +One thing the sweep found that is not a memory defect: **`slurp.flan` is not idempotent.** Its last section expects a +missing file, and its handler `barf`s that file into existence and invokes `retry`; run twice, the second run finds +the file already there and prints a handler count of 0 where the first printed 1. Running each program plain and then +under memcheck is exactly two runs, so this presented as "diverges under memcheck" and was nothing of the kind — +reproduced with no valgrind anywhere near it. `test_acceptance.ml` already cleared the same two filenames for the same +reason; `test_valgrind.ml` now does too. + ## Why there is no interpreter Open decision #7 is settled: **the compiled path is the only backend.** Both arguments for a permanent interpreter had diff --git a/NEXT.md b/NEXT.md index 46396c2..78a6c61 100644 --- a/NEXT.md +++ b/NEXT.md @@ -197,8 +197,23 @@ it *would* have written. of program for a clamp. `escaped[ESCAPE_MAX]` was already covered, because `println.flan` drives a 1100-character string through it on purpose — 1019 bytes out against a worst case of 1021 into 1024. `scratch[SCRATCH]` never sees more than 20 characters of 64. -3. **Valgrind over the headless corpus, not done.** ASan does not see uninitialised reads, which is where `zeroed` and - struct padding live. MSan is out: it needs every dependency instrumented and raylib settles that. +3. **Valgrind over the headless corpus, done.** `dune build --root . @valgrind` runs forty-seven programs under + memcheck, twelve of them again with `--no-bounds-checks`, in 88 seconds including the compiles. Clean. It needs no + instrumentation at all — memcheck works on the binary, so `Emit`'s hand-written IR arrives on the same footing as + clang's C, which is why it was reachable where MSan was not. The uninitialised read ASan is blind to is now a + control that must report: index 3 of a `Vec` with len 2 and cap 4, with `--track-origins` naming the + `aligned_alloc` in `flan_vec_push`. Two more controls pin a heap overrun and a padded `Map` key. `test/valgrind.supp` + holds **no suppressions** — nothing false came up to suppress. Details, and the measured fact that memcheck catches + 0 of `bounds.flan`'s 6 cases where ASan catches 3, in [`BUILT.md`](BUILT.md). + + **The hole it leaves, and it is the arena.** `free-all` is retain-capacity, so the pages stay and memcheck is never + told the storage died: round two of a reset arena reads a byte it never wrote, prints round one's value, and + nothing reports. Interior overruns are invisible for the same structural reason — an arena is one `malloc`, and the + `Map`'s `keys | values | hashes | scratch` is one allocation too, so "probe overrun at high load" is not clean, it + is not observable. Closing the arena half means `VALGRIND_MAKE_MEM_UNDEFINED` in `flan_arena_proc`, a `runtime/` + change nobody has made. And both positive controls had to be written by hand: no corpus program reaches an + observable uninitialised read, so the sweep is a regression net from here rather than an audit that found the + runtime sound. Two things the sweep structurally cannot cover: raylib and libm are uninstrumented, so the windowed examples are noise; and a redefinition module is built by `llc` and `ld` rather than clang, so the reload path carries no instrumentation @@ -1201,7 +1216,8 @@ watched fail against the new test before the mutation was reverted — a test no looping reader costs five seconds and names the row instead of never finishing. What is still open here: the mutation pass has not been re-run since, so the count of nineteen is the old one. The -sanitized sweep (`@sanitize`) is under the same watchdog but has never been observed to fire it. +sanitized sweep (`@sanitize`) is under the same watchdog but has never been observed to fire it, and so is the +memcheck sweep (`@valgrind`), whose alarm is looser at 5400s because memcheck is 20-50x on execution. ### Asked for by the editor lanes