What memcheck sees that a sanitizer cannot, and where it stops seeing
This commit is contained in:
parent
3a91c7ef06
commit
9ebee780e7
75
BUILT.md
75
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
|
||||
|
||||
22
NEXT.md
22
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
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user