JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Valgrind over the corpus, in 88 seconds, with no suppressions to write

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-12 21:49:50 +07:00
commit b71b7a7981
5 changed files with 620 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

75
BUILT.md
View File

@ -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
View File

@ -225,8 +225,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
@ -1255,7 +1270,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

42
test/dune
View File

@ -119,3 +119,45 @@
(glob_files programs/*.flan)
(glob_files programs/assets/*))
(action (run ./test_sanitize.exe)))
; The corpus a third time, under Valgrind's memcheck. Its own alias for the
; same reason @sanitize has one, only more so: memcheck runs the program on a
; synthetic CPU, so the corpus is tens of minutes rather than seconds.
;
; dune build --root . @valgrind
;
; Why a third sweep when @sanitize exists: ASan answers "is this address
; mine", and cannot answer "were these bytes ever written". That second
; question is MSan's, MSan needs every dependency instrumented and raylib
; settles it, and memcheck answers both while needing no instrumentation at
; all. NEXT.md asked for exactly this.
(executable
(name test_valgrind)
(modules test_valgrind watchdog)
(libraries flan unix str))
(rule
(alias valgrind)
(deps
test_valgrind.exe
; The suppression file, which is all reasons and no suppressions; its own
; header says why that is the finding rather than an oversight.
(file valgrind.supp)
(file %{workspace_root}/calc-me.flan)
(file %{workspace_root}/sand.flan)
(file %{workspace_root}/brush.png)
(glob_files %{workspace_root}/vendor/raylib/*)
(glob_files %{workspace_root}/vendor/agent/*)
(glob_files %{workspace_root}/vendor/edn/*)
(glob_files %{workspace_root}/examples/*)
(glob_files programs/*.flan)
(glob_files programs/assets/*)
; The package tree the multi-level cases import, as in the test stanza
; above: a glob per directory, because dune's glob does not descend.
(glob_files programs/pkgs/shape/*)
(glob_files programs/pkgs/area/*)
(glob_files programs/pkgs/draw/*)
(glob_files programs/pkgs/ring-a/*)
(glob_files programs/pkgs/ring-b/*)
(glob_files programs/pkgs/ring-c/*))
(action (run ./test_valgrind.exe)))

442
test/test_valgrind.ml Normal file
View File

@ -0,0 +1,442 @@
(* The corpus a third time, under Valgrind's memcheck.
*
* Not part of [dune test] and for the same reason [test_sanitize.ml] is not:
* memcheck runs a program on a synthetic CPU and the corpus takes minutes
* rather than seconds. It has its own alias, beside @sanitize.
*
* dune build --root . @valgrind
*
* Why a third tool, when @sanitize already exists. ASan answers "is this
* address mine?" and has nothing at all to say about "were these bytes ever
* written?" — that second question is MemorySanitizer's, and MSan is not
* available here because it needs every dependency instrumented and raylib
* settles it. Memcheck answers both, and needs no instrumentation whatever:
* it works on the binary, so hand-written IR, clang-compiled C and libc all
* arrive on the same footing. Nothing in [Emit] has to cooperate, which is
* the exact opposite of the sanitize_address attribute story in BUILT.md.
*
* The two tools are not ordered, they are complementary, and the measurement
* that shows it is bounds.flan: ASan catches three of its six deliberate
* out-of-bounds cases and memcheck catches *none* of them, because every one
* is a global or a stack array and memcheck guards neither. What memcheck
* sees that ASan does not is in [heap_uninit] below. Believe neither sweep on
* its own.
*
* The check is three-sided, and the third side is the one that matters:
* - any error memcheck reports is a failure;
* - any divergence from the un-instrumented run — output or exit status —
* is a failure, because a program that behaves differently under the tool
* has not been tested by it;
* - and the controls below must report, because a clean sweep from a tool
* that turns out to be looking at nothing is worth nothing. *)
open Flan
(* A hang reports nothing at all, and memcheck makes every program 20-50x
slower, so the clock is looser than the sanitize sweep's. See watchdog.ml. *)
let () = Watchdog.arm ~seconds:5400 "test_valgrind"
let failures = ref 0
let fail fmt =
Printf.ksprintf (fun s -> incr failures; print_endline ("FAIL " ^ s)) fmt
let scratch = Filename.get_temp_dir_name ()
let supp = "valgrind.supp"
(* Leak checking is off, and the reason is [test_sanitize.ml]'s reason for
detect_leaks=0 unchanged: allocate-once-never-free is this runtime's design,
not an accident — rt_args says so in its own comment, an arena hands back
nothing before arena-destroy, and the context temp arena is made on first
use and never released. LeakSanitizer produced a suppression list and no
information; memcheck would produce the same list. The question is worth
asking on purpose one day, and this is not that run. *)
let vg_flags =
[ "--leak-check=no"; "--error-exitcode=0"; "--track-origins=yes";
(* Origins are what turn "uninitialised value" into a line naming the
allocation it came from. They cost roughly 2x on top of memcheck and
are worth every bit of it: without them an uninitialised-read report
says where the value was *used*, which for a runtime this small is
almost always snprintf inside libc and tells you nothing. *)
"--num-callers=30" ]
let quoted l = String.concat " " (List.map Filename.quote l)
(* Run [exe], with and without memcheck under it. The log is a file rather
than stderr so that the program's own output stays byte-comparable against
the plain run — memcheck's ==pid== preamble on stderr would otherwise be a
difference in every single case. *)
let run ?(vg = false) exe args =
let out = Filename.concat scratch "flan-vg.out" in
let log = Filename.concat scratch "flan-vg.log" in
let prefix =
if not vg then ""
else
Printf.sprintf "valgrind %s --log-file=%s %s "
(String.concat " " vg_flags) (Filename.quote log)
(if Sys.file_exists supp then "--suppressions=" ^ Filename.quote supp
else "")
in
let cmd =
Printf.sprintf "%s%s %s > %s 2>&1" prefix (Filename.quote exe)
(quoted args) (Filename.quote out)
in
let code = Sys.command cmd in
let text = In_channel.with_open_bin out In_channel.input_all in
let report =
if vg && Sys.file_exists log then
In_channel.with_open_bin log In_channel.input_all
else ""
in
(try Sys.remove out with Sys_error _ -> ());
(try Sys.remove log with Sys_error _ -> ());
(code, text, report)
let compile ~checks path =
let exe =
Filename.concat scratch
(Printf.sprintf "flan-vg-%s-%s"
(if checks then "c" else "u")
(Filename.remove_extension (Filename.basename path)))
in
let l = Load.program ~file:path (Parse.program (Reader.read_file path)) in
let p = Check.program l.Load.decls in
let p, csrcs, lflags = Reach.link ~dev:false l p in
ignore
(Build.executable
~opts:{ Build.default with checks } ~csrcs ~lflags p ~out:exe);
exe
(* "ERROR SUMMARY: 3 errors from 2 contexts (suppressed: 1 from 1)".
Both numbers are read, and the suppressed count is *printed* rather than
ignored: a suppression that has quietly started absorbing new reports is
exactly the failure mode a suppression file introduces, and a count nobody
looks at is how it stays hidden. *)
let summary text =
let re = Str.regexp
"ERROR SUMMARY: \\([0-9]+\\) errors? from [0-9]+ contexts? (suppressed: \\([0-9]+\\)" in
try
let _ = Str.search_backward re text (String.length text) in
Some (int_of_string (Str.matched_group 1 text),
int_of_string (Str.matched_group 2 text))
with Not_found | Failure _ -> None
let suppressed_total = ref 0
(* Files a corpus program leaves in the working directory, cleared before
*every* run of it.
Not housekeeping: two of these programs are not idempotent, and running one
twice — which is precisely what this harness does, once plain and once
under memcheck — makes the second run print something different from the
first. slurp.flan is the case that found it. Its last section sets up a
missing file, expects the handler to fire, and has the handler barf the
file into existence and invoke retry; on a second run the file is already
there, slurp succeeds first time, and the handler count prints 0 where the
first run printed 1. That looks exactly like "the program behaves
differently under memcheck" and is nothing of the kind — measured by
running it twice with no valgrind anywhere near it, which reproduces the 0.
test_acceptance.ml removes the same two names for the same reason; this is
that list, not a new fact about the corpus. It matters here and not in
test_sanitize.ml only because slurp.flan is in this sweep's corpus and not
in that one's. *)
let artifacts =
[ "slurp-out.txt"; "slurp-made.txt"; "web-files-out.txt" ]
let clean () =
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) artifacts
(* One program, both ways. *)
let check label path args ~checks =
match compile ~checks path with
| exception Failure m -> fail "%s %s: build: %s" label path m
| exe ->
clean ();
let c1, t1, _ = run exe args in
clean ();
let c2, t2, log = run ~vg:true exe args in
(match summary log with
| None ->
fail "%s %s: no ERROR SUMMARY in the memcheck log — valgrind did not \
run the program to completion\n%s" label path log
| Some (errors, sup) ->
suppressed_total := !suppressed_total + sup;
if errors > 0 then fail "%s %s: %d memcheck error(s)\n%s" label path errors log);
if c1 <> c2 || t1 <> t2 then
fail "%s %s: diverged under memcheck\n \
plain (exit %d): %S\n memcheck (exit %d): %S"
label path c1 t1 c2 t2;
clean ();
(try Sys.remove exe with Sys_error _ -> ())
(* The corpus. This list is *larger* than @sanitize's, deliberately: that one
was written before maps.flan, vec.flan, unions.flan and allocators.flan
existed and was never extended, and those four are most of what this sweep
was pointed at. The exclusions are the same classes test_sanitize.ml names,
for the same reasons:
- raylib-* and the windowed examples: raylib and libm are not instrumented,
and under memcheck that is worse than under ASan rather than better —
memcheck reports on uninstrumented code too, so every one of them would
be a page of somebody else's stack traces.
- break.flan and agent.flan, which wait for an editor to connect.
- dev-* and reload-*, which need a host process or a dlopen harness.
- the compile-time refusals: nth-gone, pkg-hidden-main, pkg-two-aliases,
pkg-two-mains, pkg-cycle, pkg-alias-clash, user-allocator, and the whole
vec-moved / vec-double-free / vec-in-struct / vec-global / vec-of-vec /
vec-to-c / vec-untyped family. These never produce a binary at all: the
checker refuses them, which is the point of them. There is nothing for
memcheck to run.
- shadow-pkg.flan, which is a package fragment with no main and does not
link on its own.
The six programs here that abort by design — error, exhausted-unhandled,
free-all-refused, map-stale-region, slurp-unhandled, stale-region — are
kept. A trap is a controlled abort after an fprintf, and "the trap still
fires, in the same place, with the same message, under memcheck" is worth
asserting: the region and epoch traps are the runtime's own answer to the
bugs this tool hunts, and a trap that stopped firing would be silent. *)
let corpus =
[ "programs/allocators.flan", [];
"programs/bounds.flan", [ "0" ];
"programs/bytes2.flan", [];
"programs/cleanup.flan", [];
"programs/conditions.flan", [];
"programs/debug.flan", [];
"programs/debug-permuted.flan", [];
"programs/defer-let.flan", [];
"programs/destructure.flan", [];
"programs/edn.flan", [];
"programs/embed.flan", [];
"programs/enum-compare.flan", [];
"programs/enum-convert.flan", [];
"programs/error.flan", [];
"programs/exhausted.flan", [];
"programs/exhausted-unhandled.flan", [];
"programs/free-all-refused.flan", [];
"programs/machine.flan", [];
"programs/map-exhausted.flan", [];
"programs/map-stale-region.flan", [];
"programs/maps.flan", [];
"programs/math.flan", [];
"programs/pkg-diamond.flan", [];
"programs/pkg-return.flan", [];
"programs/pkg-shadow.flan", [];
"programs/pkg-shared.flan", [];
"programs/pkg-unused.flan", [];
"programs/printers.flan", [];
"programs/println.flan", [];
"programs/reach-walk.flan", [];
"programs/restarts.flan", [];
"programs/sand-headless.flan", [];
"programs/signedness.flan", [];
"programs/slices.flan", [];
"programs/slurp.flan", [];
"programs/slurp-unhandled.flan", [];
"programs/stale-region.flan", [];
"programs/string-of-bytes.flan", [];
"programs/text.flan", [];
"programs/unions.flan", [];
"programs/unit-main.flan", [];
"programs/utf8.flan", [];
"programs/values.flan", [];
"programs/vec.flan", [];
"programs/virtual-controls-headless.flan", [];
"programs/web-files.flan", [];
"../calc-me.flan", [ "1 + 2 * (3 - 0.5) / 2" ] ]
(* The subset run a second time with Flan's own bounds checks off.
[test_sanitize.ml] has [unchecked_controls] for the same reason: in a
checked build the language traps before the bad access and the tool below
never sees anything, so a checked-only sweep measures the checks and not
the runtime.
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. *)
let unchecked_subset =
[ "programs/allocators.flan", [];
"programs/edn.flan", [];
"programs/maps.flan", [];
"programs/map-exhausted.flan", [];
"programs/sand-headless.flan", [];
"programs/slices.flan", [];
"programs/slurp.flan", [];
"programs/text.flan", [];
"programs/unions.flan", [];
"programs/utf8.flan", [];
"programs/vec.flan", [];
"../calc-me.flan", [ "1 + 2 * (3 - 0.5) / 2" ] ]
(* A control is a program written here rather than kept in test/programs,
because none of these is a program anybody should build. [expect] says
whether memcheck must report on it. *)
let control ~expect ?(args = []) ~why name src =
let path = Filename.concat scratch (name ^ ".flan") in
Out_channel.with_open_bin path (fun ch -> Out_channel.output_string ch src);
match compile ~checks:false path with
| exception Failure m -> fail "control %s: build: %s" name m
| exe ->
let _, _, log = run ~vg:true exe args in
(match summary log with
| None -> fail "control %s: no ERROR SUMMARY\n%s" name log
| Some (errors, _) ->
(match expect, errors > 0 with
| true, false ->
fail "control %s: memcheck reported nothing. %s\n%s" name why log
| false, true ->
fail "control %s: memcheck reported. %s\n%s" name why log
| _ -> ()));
(try Sys.remove exe with Sys_error _ -> ());
(try Sys.remove path with Sys_error _ -> ())
(* A read far past the end of a Vec's heap block, through a slice so that the
compiler-emitted check is the one in play and --no-bounds-checks removes
it. This is the only shape in the language that reaches unmapped-to-me heap
through Flan code, and it is what says memcheck sees Flan code at all.
Nothing had to be added to Emit for this to work, which is the whole
difference from the ASan story. *)
let heap_oob =
"(defn main [] i32\n\
\ (let [v (vec-new i32)]\n\
\ (push v 1)\n\
\ (push v 2)\n\
\ (let [s (as-slice v)] (print (at s 4000)) (println \"\"))\n\
\ (free v))\n\
\ 0)\n"
(* The control this whole file exists for. Index 3 of a Vec with len 2 and cap
4 is *inside* the allocation — every addressability check in the world says
it is fine, and ASan is one of those checks — but nothing ever wrote it.
Memcheck reports it, and --track-origins names flan_vec_push's
aligned_alloc as where the undefined bytes came from.
If this control ever stops reporting, the argument for running memcheck at
all has gone with it, and NEXT.md's "ASan does not see uninitialised reads,
which is where zeroed and struct padding live" needs rewriting. *)
let heap_uninit =
"(defn main [] i32\n\
\ (let [v (vec-new i32)]\n\
\ (push v 1)\n\
\ (push v 2)\n\
\ (let [s (as-slice v)] (print (at s 3)) (println \"\"))\n\
\ (free v))\n\
\ 0)\n"
(* A negative control aimed straight at the Map's emitted hash and equality
pair. The key has two holes in it — seven bytes after the i8 at offset 0
and seven more after the i8 at offset 16 — and the flat hasher in
flan_rt.c, which is what a key type without an emitted pair falls back to,
hashes and memcmps the object whole. If a struct key ever reached that
path, the padding would be uninitialised stack and this would report.
That it does not report is the evidence for maps.flan's comment (2), which
claims the pair walks field by field and never reads the holes; maps.flan
can only show the *consequence*, entries that are still findable, and a
padded key that happened to be zeroed would pass it. This shows the cause. *)
let padded_key =
"(defstruct Padded [a i8 b i64 c i8])\n\
(defn main [] i32\n\
\ (let [m (map-new Padded i32)]\n\
\ (dotimes [i 40] (put m (Padded {.a (i8 i) .b (i64 i) .c 7}) i))\n\
\ (print (len m)) (println \"\")\n\
\ (match (get m (Padded {.a (i8 9) .b (i64 9) .c 7}))\n\
\ (Some v) (do (print v) (println \"\"))\n\
\ None (println \"missing\"))\n\
\ (free m))\n\
\ 0)\n"
(* Not a control but a measurement, and the ceiling on everything above.
Round one writes four elements into arena storage; free-all resets the
offset and keeps the pages; round two allocates the same bytes back and
reads one it never wrote. The value printed is round one's — and memcheck
says nothing, because the definedness bits round one set are still on those
bytes. Nothing told memcheck the storage died, because from malloc's point
of view it did not: an arena is one allocation and free-all is an integer
going to zero inside it.
So the uninitialised-read coverage this file's headline control
demonstrates holds for the heap allocator and *not* for arena storage
reused after a free-all, which is the per-frame pattern the arena exists
for. Closing it means VALGRIND_MAKE_MEM_UNDEFINED in flan_arena_proc, which
is a runtime change and a different lane's. It is printed rather than
asserted because it is a fact about the tool, not a regression. *)
let arena_reuse =
"(defvar frame Allocator)\n\
(defn main [] i32\n\
\ (set frame (arena-new 65536))\n\
\ (with-allocator frame\n\
\ (let [v (vec-new i32)]\n\
\ (push v 11) (push v 22) (push v 33) (push v 44)\n\
\ (print (at v 3)) (println \"\")))\n\
\ (free-all frame)\n\
\ (with-allocator frame\n\
\ (let [w (vec-new i32)]\n\
\ (push w 5) (push w 6)\n\
\ (let [t (as-slice w)] (print (at t 3)) (println \"\"))))\n\
\ 0)\n"
let note_arena_reuse () =
let path = Filename.concat scratch "flan-vg-arena.flan" in
Out_channel.with_open_bin path (fun ch ->
Out_channel.output_string ch arena_reuse);
(match compile ~checks:false path with
| exception Failure m -> fail "arena reuse note: build: %s" m
| exe ->
let _, text, log = run ~vg:true exe [] in
(match summary log with
| Some (0, _) ->
Printf.printf
"note arena storage reused after free-all is not re-poisoned: the \
second round read a byte it never wrote, printed %S, and memcheck \
was silent. This is the ceiling on the uninitialised-read coverage \
below — it holds for the heap allocator and not for an arena.\n"
(String.trim text)
| Some (n, _) ->
Printf.printf
"note arena storage reused after free-all now reports (%d): \
something started telling memcheck the region died. Good news; \
this file and BUILT.md both say it does not.\n" n
| None -> fail "arena reuse note: no ERROR SUMMARY\n%s" log);
(try Sys.remove exe with Sys_error _ -> ()));
(try Sys.remove path with Sys_error _ -> ())
let () =
match Sys.command "command -v valgrind > /dev/null 2>&1" with
| 0 when Sys.command "command -v clang > /dev/null 2>&1" = 0 ->
let t0 = Unix.gettimeofday () in
control ~expect:true "flan-vg-ctl-oob" heap_oob
~why:"Memcheck is not seeing Flan code. Unlike ASan this needs no \
attribute and no cooperation from Emit, so the likely cause is \
the harness rather than the compiler — check that valgrind is \
actually running the binary.";
control ~expect:true "flan-vg-ctl-uninit" heap_uninit
~why:"The uninitialised-read check is not working, which is the single \
reason this sweep exists beside @sanitize. Without it this file \
covers strictly less than test_sanitize.ml does.";
control ~expect:false "flan-vg-ctl-padded-key" padded_key
~why:"A padded struct key is being hashed or compared whole rather than \
field by field, so the holes in it are being read. See maps.flan \
comment (2) and flan_key_hash_flat in flan_rt.c: the flat path is \
bytewise and a struct key must not reach it.";
note_arena_reuse ();
List.iter (fun (p, a) -> check "checked" p a ~checks:true) corpus;
List.iter (fun (p, a) -> check "unchecked" p a ~checks:false)
unchecked_subset;
Printf.printf "memcheck: %d programs checked, %d unchecked, %.0fs\n"
(List.length corpus) (List.length unchecked_subset)
(Unix.gettimeofday () -. t0);
if !suppressed_total > 0 then
Printf.printf
"note %d report(s) suppressed by %s. Every entry there has a written \
reason; if this number is growing, one of them is absorbing \
something new.\n" !suppressed_total supp;
if !failures = 0 then print_endline "valgrind sweep: clean"
else Printf.printf "%d valgrind failure(s)\n" !failures;
exit (if !failures = 0 then 0 else 1)
| 0 -> print_endline "no clang on PATH; valgrind sweep skipped"
| _ -> print_endline "no valgrind on PATH; valgrind sweep skipped"

42
test/valgrind.supp Normal file
View File

@ -0,0 +1,42 @@
# Memcheck suppressions for the Flan corpus. See test/test_valgrind.ml.
#
# This file is empty of suppressions, and that is a finding rather than an
# oversight. The sweep was run over forty-seven programs with
# --gen-suppressions=all before this file existed, checked and again with
# --no-bounds-checks, and memcheck produced nothing to suppress: no false
# positives, and no true ones either. Every entry below the line would have
# been written from valgrind's own --gen-suppressions output plus a reason;
# none was needed.
#
# The four complaints that were expected, and why none of them appeared:
#
# 1. The arena's alignment padding, and the gap between its offset and its
# capacity. Expected to show as uninitialised reads. It cannot, and the
# reason is structural rather than lucky: the arena is a single
# malloc(cap), so every byte in it — handed out, padding, or still past
# the offset — is one allocation to memcheck. It never learns that a
# sub-object ended, so it has nothing to complain about and equally
# nothing to catch. Recorded as a coverage ceiling in BUILT.md, not as a
# clean bill of health. A read of arena bytes never written *is* caught,
# by definedness rather than addressability; a read of bytes a previous
# round wrote before a free-all is not.
#
# 2. Hand-written LLVM IR. Expected to confuse the tool. It does not, and it
# could not: memcheck instruments the binary, so it never sees IR, never
# sees a frontend attribute, and cannot tell Emit's output from clang's.
# This is the whole reason it was reachable here when MSan was not.
#
# 3. `zeroed` storage. A zeroed defvar is in .bss, which memcheck treats as
# defined because it is — the kernel supplies zeroes. No complaint, and
# correctly so.
#
# 4. Struct padding in a Map key. The compiler emits a per-key-type hash and
# equality pair that walks fields rather than bytes, so the holes are
# never read. test_valgrind.ml asserts this directly with a key carrying
# two seven-byte holes: it must not report, and a suppression here would
# have destroyed the one control that proves the pair is correct.
#
# The rule for adding to this file: paste valgrind's own --gen-suppressions
# text, and write above it why the report is not a bug. A suppression without
# a reason is how a real defect gets silenced later, and an empty file is a
# better outcome than a speculative one.