443 lines
20 KiB
OCaml
443 lines
20 KiB
OCaml
(* 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"
|