The corpus under memcheck, because ASan cannot see an unwritten byte
This commit is contained in:
parent
f61bda2bef
commit
c2df38e139
42
test/dune
42
test/dune
@ -117,3 +117,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)))
|
||||
|
||||
415
test/test_valgrind.ml
Normal file
415
test/test_valgrind.ml
Normal file
@ -0,0 +1,415 @@
|
||||
(* 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
|
||||
|
||||
(* 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 ->
|
||||
let c1, t1, _ = run exe args in
|
||||
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;
|
||||
(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
42
test/valgrind.supp
Normal 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.
|
||||
Loading…
x
Reference in New Issue
Block a user