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

The corpus a second time, under the sanitizers, behind @sanitize

Browse Source 
Twenty-eight programs built twice -- once plain, once sanitized -- and
compared on output and exit status, plus two positive controls that are
the only reason a clean result means anything: an out-of-bounds read
that must report, and a shift by the width of the type that must not,
because UBSan cannot see hand-written IR and this file would otherwise
be claiming coverage it does not have.

Its own alias rather than dune test. A sanitized program is a statically
linked 1.8MB binary and takes tens of seconds to link; the sweep is nine
minutes against the existing suite's seconds, and a test nobody will
wait for is a test nobody runs. dune build --root . @sanitize.

The checked sweep is clean. The unchecked variant -- ASan alone, with
Flan's own bounds checks off -- catches three of bounds.flan's six
deliberate out-of-bounds cases and is listed with why for the other
three: a global has a right redzone and nothing to its left, so arr[-1]
is invisible; a read past a string constant folds away entirely at -O2
and is caught only at -O0; and a reversed slice reads nothing at all.
ASan is not a substitute for the bounds checks, and now there is a table
saying which half it covers.
This commit is contained in:
Joseph Ferano 2026-09-12 09:25:43 +07:00
parent ac5c7e9c2b
commit c41c5812a9
2 changed files with 297 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
test/dune
View File

@ -1,5 +1,9 @@
(tests
(names test_flan test_acceptance test_reload test_agent test_session test_dev test_emacs test_repl test_cider)
; Explicit because test_sanitize lives in this directory and is not one of
; these: two stanzas in one directory have to say which modules are whose.
(modules test_flan test_acceptance test_reload test_agent test_session
test_dev test_emacs test_repl test_cider)
(libraries flan unix)
; The acceptance programs are part of the test corpus: if the reader, the
; parser or the checker regresses on them we want to know here, not at the CLI.
@ -28,3 +32,30 @@
; The WASI host the wasm32 case runs its module under, when no wasmtime or
; wasmer is installed.
(file wasm-run.mjs)))
; The corpus a second time under ASan and UBSan. Its own alias and not part of
; `dune test`: a sanitized build is a statically linked 1.8MB binary that takes
; tens of seconds to produce, so the sweep is minutes against the existing
; suite's seconds, and a test nobody will wait for is a test nobody runs.
;
; dune build --root . @sanitize
; An executable plus a rule rather than a (test ...): a test stanza attaches
; to the @runtest alias and offers no way to be attached to another one, which
; is the whole point here.
(executable
(name test_sanitize)
(modules test_sanitize)
(libraries flan unix))
(rule
(alias sanitize)
(deps
test_sanitize.exe
(file %{workspace_root}/calc-me.flan)
(file %{workspace_root}/sand.flan)
(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))
(action (run ./test_sanitize.exe)))

266
test/test_sanitize.ml Normal file
View File

@ -0,0 +1,266 @@
(* The corpus a second time, under AddressSanitizer and
UndefinedBehaviorSanitizer.
Not part of [dune test] and deliberately so: a sanitized build of one
program is a 1.8MB statically linked binary and takes ten to twenty seconds
to produce, so the sweep is minutes where the whole existing suite is
seconds. It has its own alias.
dune build --root . @sanitize
What this can and cannot see is written down in [Build.opts] and in
[Emit]'s [sanitize] comment, and it is not symmetric:
- ASan reaches Flan code, but only because [Emit] puts [sanitize_address]
on every function it defines; the attribute is what the pass selects on
and hand-written IR has none by default. The positive control for that is
[oob], below, which must report.
- UBSan reaches the runtime's C and nothing else. Its checks are branches
clang's *frontend* emits, and no attribute asks an LLVM pass to produce
them, so the shift-past-the-width and float-cast questions this sweep was
partly meant to answer are not answerable this way. [shift] records that
as a test rather than as a paragraph: it is a program with unambiguous
shift UB in it, and it is expected *not* to be caught.
The check is two-sided. A marker in the sanitized run's output is a
failure, and so is any divergence from the unsanitized run — same output,
same exit status. The second half is not redundant: UBSan recovers by
default, so a program can trip a check, carry on with a different value and
still exit 0, and several of these programs exit nonzero by design, so
"exit status 0" is not available as a pass condition. *)
open Flan
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 ()
(* Leaks are off. Every allocation in the runtime is allocate-once-never-free
by design — [rt_args] says so in its own comment — so LeakSanitizer here
produces a suppression list and no information. Set in the environment
rather than baked in, so a session asking the leak question can ask it.
[print_stacktrace] is what turns a UBSan report from a source line into
something with a caller in it, and it is off by default. *)
let env =
"ASAN_OPTIONS=${ASAN_OPTIONS:-detect_leaks=0} \
UBSAN_OPTIONS=${UBSAN_OPTIONS:-print_stacktrace=1} "
let run exe args =
let out = Filename.concat scratch "flan-sanitize.out" in
let cmd =
Printf.sprintf "%s%s %s > %s 2>&1" env (Filename.quote exe)
(String.concat " " (List.map Filename.quote args))
(Filename.quote out)
in
let code = Sys.command cmd in
let text = In_channel.with_open_bin out In_channel.input_all in
(try Sys.remove out with Sys_error _ -> ());
(code, text)
let compile ~sanitize ~checks path =
let exe =
Filename.concat scratch
(Printf.sprintf "flan-san-%s-%s"
(if sanitize then "s" else "p")
(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; sanitize } ~csrcs ~lflags p ~out:exe);
exe
let contains hay needle =
let n = String.length needle and h = String.length hay in
let rec go i = i + n <= h && (String.sub hay i n = needle || go (i + 1)) in
go 0
(* What a report looks like, whichever sanitizer wrote it. *)
let markers =
[ "ERROR: AddressSanitizer"; "runtime error:"; "ERROR: LeakSanitizer";
"SUMMARY: UndefinedBehaviorSanitizer" ]
let reported text = List.exists (contains text) markers
(* The corpus. Excluded, with the reason, rather than quietly absent:
- raylib-*, and the windowed examples, because raylib and libm are not
instrumented and every report through them would be about somebody
else's code.
- break.flan and agent.flan, which stop in the break loop and wait for an
editor to connect. They are covered by test_agent against a real daemon.
- the dev-* and reload-* programs, which need a host process or a dlopen
harness. The reload path is half-covered at best in any case: a
redefinition module is built by llc and ld, not by clang, so nothing
instruments it — one more thing this sweep does not prove.
- nth-gone, pkg-hidden-main, pkg-two-aliases, pkg-two-mains, which are
negative cases and are expected not to compile.
calc-me is here and is not in test/programs: it is the one string parser in
the corpus, which makes it the likeliest to push [scratch] or [escaped]
anywhere near their bounds. *)
let corpus =
[ (* bounds.flan selects its case from argv, and every case but 0 is one
that traps. Argument 0 is the in-bounds path — the last index of a
fixed array, a slice ending exactly at len, an empty slice at len —
which is the one the sweep has something to say about. The trapping
cases are where the ASan-without-bounds-checks question lives and they
are run separately; see [unchecked_controls]. Running this program with
*no* argument reads args[1] of a one-element argv, which is a bug in
the harness rather than in anything under test. *)
"programs/bounds.flan", [ "0" ];
"programs/bytes2.flan", [];
"programs/cleanup.flan", [];
"programs/conditions.flan", [];
"programs/debug.flan", [];
"programs/debug-permuted.flan", [];
"programs/destructure.flan", [];
"programs/edn.flan", [];
"programs/enum-compare.flan", [];
"programs/error.flan", [];
"programs/machine.flan", [];
"programs/math.flan", [];
"programs/pkg-return.flan", [];
"programs/pkg-shared.flan", [];
"programs/pkg-unused.flan", [];
"programs/printers.flan", [];
"programs/println.flan", [];
"programs/restarts.flan", [];
"programs/sand-headless.flan", [];
"programs/signedness.flan", [];
"programs/slices.flan", [];
"programs/string-of-bytes.flan", [];
"programs/text.flan", [];
"programs/unit-main.flan", [];
"programs/utf8.flan", [];
"programs/values.flan", [];
"programs/virtual-controls-headless.flan", [];
"../calc-me.flan", [ "1 + 2 * (3 - 0.5) / 2" ] ]
let sweep ~checks label =
List.iter
(fun (path, args) ->
match compile ~sanitize:false ~checks path with
| exception Failure m -> fail "%s %s: unsanitized build: %s" label path m
| plain ->
(match compile ~sanitize:true ~checks path with
| exception Failure m -> fail "%s %s: sanitized build: %s" label path m
| san ->
let c1, t1 = run plain args in
let c2, t2 = run san args in
if reported t2 then
fail "%s %s: sanitizer report\n%s" label path t2
else if c1 <> c2 || t1 <> t2 then
fail "%s %s: diverged from the unsanitized run\n \
plain (exit %d): %S\n sanitized (exit %d): %S"
label path c1 t1 c2 t2;
(try Sys.remove plain with Sys_error _ -> ());
(try Sys.remove san with Sys_error _ -> ())))
corpus
(* The positive controls, which are the only evidence that a clean sweep means
anything. Both are written here rather than kept in test/programs because
neither is a program anybody should build: one reads off the end of an
array and the other shifts an i32 by 32. *)
let control ~expect_report name src =
let path = Filename.concat scratch (name ^ ".flan") in
Out_channel.with_open_bin path (fun ch -> Out_channel.output_string ch src);
let exe = compile ~sanitize:true ~checks:false path in
let _, text = run exe [] in
(match expect_report, reported text with
| true, false ->
fail "control %s: nothing reported, so this sweep is not instrumenting \
Flan code at all — check that Emit still writes the \
sanitize_address attribute group" name
| false, true ->
fail "control %s: reported, which contradicts what this file says UBSan \
reaches. Good news; rewrite the comment." name
| _ -> ());
(try Sys.remove exe with Sys_error _ -> ());
(try Sys.remove path with Sys_error _ -> ())
(* The variant the checked build cannot ask for: with Flan's own bounds checks
off, is ASan enough on its own? bounds.flan is the program to ask it with —
every one of its selectors is a deliberate out-of-bounds access, and in a
checked build every one of them traps.
The answer is no, and it is worth having the shape of the no. [reports]
holds the cases ASan catches; the rest are listed with why it does not, and
they are printed rather than asserted, because a future LLVM that folds
differently would change them and that is information, not a regression.
[9] is the one that is not about ASan at all: at -O2 the access never
happens. The index is out of bounds on an [inbounds] getelementptr into a
string constant, so the whole load folds to zero and the program prints a
wrong answer instead of touching a redzone. At -O0, with the load still in
the program, ASan reports it. That divergence is why [--sanitize] does not
force -O0 the way [--debug] does — the optimiser is half of what is being
measured. *)
let unchecked_controls () =
let reports = [ "3"; "7"; "4" ] in
let silent =
[ "-1", "a negative index into a global: ASan gives a global a right \
redzone and nothing on the left, so arr[-1] lands in whatever \
is in front of it";
"9", "at -O2 the load is folded away — an out-of-bounds inbounds GEP \
into a string constant is poison, so nothing is read and a wrong \
value is printed. Reported at -O0.";
"2", "a reversed slice (lo 2, hi 1), whose length comes out negative; \
nothing is read, and flan_write_stdout ignores a negative count. \
No access, so nothing for ASan to see — the hazard is a slice \
with a negative length reaching user code, which is a checker \
question" ]
in
match compile ~sanitize:true ~checks:false "programs/bounds.flan" with
| exception Failure m -> fail "unchecked bounds.flan: build: %s" m
| exe ->
List.iter
(fun a ->
let _, t = run exe [ a ] in
if not (reported t) then
fail "unchecked bounds.flan %s: nothing reported, and this is the \
case that says ASan sees an unchecked build at all\n%s" a t)
reports;
List.iter
(fun (a, why) ->
let _, t = run exe [ a ] in
if reported t then
Printf.printf
"note unchecked bounds.flan %s now reports; it did not, on the \
grounds that %s\n" a why
else
Printf.printf "note unchecked bounds.flan %s: silent — %s\n" a why)
silent;
(try Sys.remove exe with Sys_error _ -> ())
let () =
match Sys.command "command -v clang > /dev/null 2>&1" with
| 0 ->
(* A read five past the end of a four-element global. Five and not ten:
ASan's redzone on a global this small is 16 bytes, so an index far
enough past the end lands beyond the redzone and is not seen — which is
itself worth knowing about what this tool can do. *)
control ~expect_report:true "flan-san-ctl-oob"
"(defvar arr [4 i32])\n\
(defn main [] i32\n\
\ (set (at arr 0) 1)\n\
\ (let [i 5] (print (at arr i)) (println \"\"))\n\
\ 0)\n";
(* Shift by the full width of the type: undefined in C, poison in LLVM,
and invisible to UBSan here because nothing emitted a check for it. If
this ever starts reporting, the note above is stale. *)
control ~expect_report:false "flan-san-ctl-shift"
"(defn main [] i32\n\
\ (let [x 1] (let [n 32] (print (<< x n)) (println \"\")))\n\
\ 0)\n";
sweep ~checks:true "checked";
unchecked_controls ();
if !failures = 0 then print_endline "sanitizer sweep: clean"
else Printf.printf "%d sanitizer failure(s)\n" !failures;
exit (if !failures = 0 then 0 else 1)
| _ ->
print_endline "no clang on PATH; sanitizer sweep skipped"