Merge branch 'sanitize' into dev-loop
ASan was instrumenting none of the Flan half: it is an LLVM pass that only touches functions carrying sanitize_address, which clang's C frontend adds and hand-written IR does not. Globals get redzones either way, which is why it looked right. emit.ml puts the attribute on every define now, and a control asserts the report. UBSan reaches no Flan code and no flag changes that -- its checks are frontend-emitted branches, not a pass -- so shift UB and the NaN cast are not answerable this way. Left as a compiler question, pinned by a control that must not report.
This commit is contained in:
commit
50ed2cbef0
42
BUILT.md
42
BUILT.md
@ -269,6 +269,48 @@ that split them would break the write check silently. The test covers both.
|
||||
Cost, measured: a 50M-iteration dependency chain over a 1024-element array runs at 0.11–0.12s checked against 0.12–0.13s
|
||||
unchecked. Indistinguishable.
|
||||
|
||||
## Sanitizers, and why hand-written IR does not get them for free
|
||||
|
||||
`--sanitize` builds the whole program under ASan and UBSan — the runtime's C, the generated shim, and the Flan. The last
|
||||
of those is not what passing `-fsanitize=address` to the clang run over the `.ll` gets you, and the gap is silent.
|
||||
|
||||
**AddressSanitizer is an LLVM pass, but it instruments only functions carrying the `sanitize_address` attribute.** That
|
||||
attribute is put there by clang's C frontend. `Emit` writes `.ll` by hand, so it wrote none, so the pass walked past
|
||||
every Flan function and instrumented `flan_rt.c`. The measurement that settled it: an out-of-bounds read of a `defvar`
|
||||
array in a `--no-bounds-checks` build printed its garbage and exited 0; with an `attributes #0 = { sanitize_address }`
|
||||
group named on every `define`, the same program reports `global-buffer-overflow in flan.main`. Globals are the exception
|
||||
— the module pass redzones them whether or not any function is attributed — which is why the *shape* of a sanitized
|
||||
build looked right long before it worked.
|
||||
|
||||
**UndefinedBehaviorSanitizer has no equivalent lever.** Its checks are not a pass: the C frontend emits branches to
|
||||
`__ubsan_handle_*` inline, and no attribute asks anything to produce them. So UBSan covers the C and nothing else, and
|
||||
`(<< 1 32)` is still unremarked under `-fsanitize=undefined`. Shift UB, alignment and the f32→i32 cast on NaN are
|
||||
therefore a compiler feature if they are wanted — checks emitted from `Emit` behind the flag, the same shape the bounds
|
||||
checks already have — and not a flag away. `test_sanitize` pins both halves with controls: one program that must report
|
||||
and one that must not, so either fact changing is a test failure rather than a discovery.
|
||||
|
||||
`-fno-sanitize=signed-integer-overflow` is the only exclusion, because wrapping is what this language's arithmetic
|
||||
means and without it every program trips on its first `+`.
|
||||
|
||||
**The flag deliberately does not force `-O0`,** unlike `--debug`, whose reason (mem2reg deletes the alloca a
|
||||
`llvm.dbg.declare` describes) does not apply. The optimiser is half of what is being measured, and `bounds.flan` proves
|
||||
it: with checks off, its read past the end of a string constant is reported at `-O0` and silent at `-O2`, because an
|
||||
out-of-bounds `inbounds` getelementptr into a constant is poison and LLVM folds the load away. The program then prints a
|
||||
wrong answer instead of touching memory. Same family as `(<< 1 32)` compiling to a bare `retq`.
|
||||
|
||||
**What ASan covers of the bounds checks' job, since `--sanitize --no-bounds-checks` is the run that asks.** Three of
|
||||
`bounds.flan`'s six deliberate out-of-bounds cases are caught. A negative index into a global is not, and the reason is
|
||||
layout rather than anything about the access: ASan lays a global out as `{data, redzone}`, so reading before one lands
|
||||
in whatever precedes it, which is a redzone if something instrumented is there and ordinary memory if nothing is.
|
||||
Measured both ways — silent in `bounds.flan`, reported as soon as another `defvar` is declared in front of `arr`. A
|
||||
reversed slice is not caught either, having computed a negative length and read nothing at all. And ASan sees
|
||||
out-of-*object* access, not out-of-subobject, so a slice into the middle of a larger array can overrun its logical
|
||||
bounds without crossing a redzone. Three of six is a ceiling on what it covers, not a measurement of the risk. It is a
|
||||
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.
|
||||
|
||||
## Why there is no interpreter
|
||||
|
||||
Open decision #7 is settled: **the compiled path is the only backend.** Both arguments for a permanent interpreter had
|
||||
|
||||
54
NEXT.md
54
NEXT.md
@ -62,39 +62,37 @@ the commit that made it.
|
||||
`-2851001042534928384` — the same 64 bits, printed unsigned now that `hash-grid`'s `u64` no longer goes through an
|
||||
`(i64 …)` cast — and a trap column shifted because the call it names got shorter.
|
||||
|
||||
### Queued — the runtime under a sanitizer
|
||||
### Landed — the runtime under a sanitizer
|
||||
|
||||
Nothing has ever run under ASan or UBSan on the test path. `grep -i 'sanitize\|asan\|valgrind'` over `lib/ bin/ test/
|
||||
runtime/ vendor/` returns nothing at all. This is not a big project — the whole C surface is about 1,260 lines
|
||||
(`flan_rt.c` 394, `flan_dev.c` 219, `flan_agent.c` 647) plus what `shim.ml` generates.
|
||||
`--sanitize` is a build flag beside `--debug`; `dune build --root . @sanitize` builds twenty-eight programs twice, plain
|
||||
and sanitized, and compares output and exit status. Its own alias and not `dune test`, because the sweep is about nine
|
||||
minutes. The checked sweep is **clean**. How ASan and UBSan reach a language whose IR is written by hand, and why the
|
||||
flag does not force `-O0` when `--debug` does, is in [`BUILT.md`](BUILT.md).
|
||||
|
||||
**The bugs are not in allocation.** There are four `malloc`/`calloc`/`strdup` sites in the entire runtime and every one
|
||||
is allocate-once-never-free by design — `rt_args` says so in its own comment — so LeakSanitizer would mostly produce
|
||||
suppressions. The risk is **fixed static buffers with bounds arithmetic**, and the ones with no coverage are already
|
||||
written down: `scratch[SCRATCH]` and `escaped[ESCAPE_MAX]` in `flan_rt.c`, the 4K result cap, the registry overflow
|
||||
guard, and `SNAP_MAX`/`SNAP_NAMES` from the restart snapshot.
|
||||
Two defects came out of it, both found by reading rather than by the tools, both fixed with a regression case:
|
||||
`flan_bytes_to_i64`/`flan_bytes_to_f64` clamped a slice length with `(size_t)n` and so read 63 or 511 bytes off the end
|
||||
of a negative-length slice; and the three `snprintf` shims published snprintf's return as a slice length, which is what
|
||||
it *would* have written.
|
||||
|
||||
There is evidence the sweep pays. Checking `flan_escape_bytes` by hand against lengths 0–1300 under ASan with a red
|
||||
zone found the guard correct but its comment understating its own reserve by four bytes — worst output 1021 into 1024.
|
||||
That was one buffer, found by looking.
|
||||
**What is left, and it is most of what the sweep was meant to settle:**
|
||||
|
||||
The shape:
|
||||
1. **UBSan sees no Flan code and no flag changes that.** Its checks are branches clang's C frontend emits inline, not a
|
||||
pass, so shift UB (`(<< 1 32)`, see Sharp edges), alignment, and the f32→i32 cast on NaN or an infinity — the things
|
||||
`floor-f32` guards by hand and nothing else does — are unreached. Either `Emit` grows those checks behind the flag,
|
||||
which is a compiler feature of the same shape the bounds checks already have, or they belong to the checker. Not
|
||||
decided. `test_sanitize` pins the current answer with a control that must *not* report, so a future clang changing
|
||||
this is a test failure rather than a discovery.
|
||||
2. **Four named buffers got no evidence at all.** The 4K result cap, the dev registry overflow guard,
|
||||
`SNAP_MAX`/`SNAP_NAMES` and `condition_name[128]` are on the daemon and agent paths, which need a socket and are not
|
||||
in the corpus. Their guards were read and are correct; that is reading, not testing. `escaped[ESCAPE_MAX]` is the one
|
||||
that *is* 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.
|
||||
|
||||
1. A `--sanitize` flag beside `--debug` in `lib/build.ml`, reaching both the clang run over the `.ll` and the runtime's
|
||||
own C.
|
||||
2. Run the existing corpus under it. `test/programs/` is about forty programs with pinned output — a second pass over
|
||||
them is the cheapest coverage available here, and needs no new test written.
|
||||
3. **UBSan is worth more than ASan**, with one exclusion that is not optional: arithmetic wraps by design, so
|
||||
`-fno-sanitize=signed-integer-overflow` or every program trips on the first `+`. What is left is real — shift UB
|
||||
(`(<< 1 32)` compiled to a bare `retq` at -O2, see Sharp edges), alignment, and the f32→i32 cast on NaN or an
|
||||
infinity that `floor-f32` guards by hand and nothing else does.
|
||||
4. The variant worth its own run: **ASan with `--no-bounds-checks`**. That asks whether the bounds checks are the only
|
||||
thing between the language and corruption, which the checked build cannot ask.
|
||||
|
||||
Two limits, so nobody is surprised. raylib and libm are not instrumented, so the windowed examples are noise and the
|
||||
headless corpus is the target — `sand-headless`, `values`, `machine`, `virtual-controls-headless`. And ASan does not
|
||||
see uninitialised reads, which is where `zeroed` and struct padding live; that wants Valgrind as a slower second pass,
|
||||
because MSan needs every dependency instrumented and raylib settles that.
|
||||
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
|
||||
whatever the flag says.
|
||||
|
||||
### Managed classes are planned. Do not start them.
|
||||
|
||||
|
||||
23
bin/main.ml
23
bin/main.ml
@ -72,7 +72,14 @@ let dev_flag = "--dev"
|
||||
stop it and read it". See [Build.opts]. *)
|
||||
let debug_flag = "--debug"
|
||||
|
||||
let flags = [ no_checks_flag; dev_flag; debug_flag ]
|
||||
(* ASan and UBSan over the whole program, the runtime's C and the Flan alike.
|
||||
Its own flag for the same reason --debug is: it answers "is this program
|
||||
touching memory it does not own", which is neither of the other two
|
||||
questions. It does not imply -O0 — see [Build.opts], which also records
|
||||
what each of the two sanitizers actually reaches. *)
|
||||
let sanitize_flag = "--sanitize"
|
||||
|
||||
let flags = [ no_checks_flag; dev_flag; debug_flag; sanitize_flag ]
|
||||
|
||||
(* [--target=wasm32-wasi], the one cross target. Unlike the flags above it
|
||||
carries a value, so it is matched by prefix and stripped from the residual
|
||||
@ -153,6 +160,10 @@ let () =
|
||||
let checks = not (List.mem no_checks_flag args) in
|
||||
let dev = List.mem dev_flag args in
|
||||
let debug = List.mem debug_flag args in
|
||||
(* --sanitize changes the IR — every [define] names the attribute group
|
||||
ASan's pass selects on — so [emit] has to honour it or what this prints
|
||||
is not what a sanitized build compiles. *)
|
||||
let sanitize = List.mem sanitize_flag args in
|
||||
let files = List.filter (fun a -> not (is_flag a)) args in
|
||||
List.iter
|
||||
(fun path ->
|
||||
@ -160,13 +171,14 @@ let () =
|
||||
let l = load path in
|
||||
let pnames = if debug then param_names l else [] in
|
||||
Flan.Check.program l.decls
|
||||
|> Flan.Emit.program ~checks ~dev ~debug ~pnames
|
||||
|> Flan.Emit.program ~checks ~dev ~debug ~pnames ~sanitize
|
||||
|> print_string))
|
||||
files
|
||||
| _ :: "build" :: path :: rest ->
|
||||
let checks = not (List.mem no_checks_flag rest) in
|
||||
let dev = List.mem dev_flag rest in
|
||||
let debug = List.mem debug_flag rest in
|
||||
let sanitize = List.mem sanitize_flag rest in
|
||||
let target = target_of rest in
|
||||
let out =
|
||||
match List.filter (fun a -> not (is_flag a)) rest with
|
||||
@ -181,7 +193,7 @@ let () =
|
||||
| _ ->
|
||||
prerr_endline
|
||||
"usage: flan build <file.flan> [-o out] [--no-bounds-checks] \
|
||||
[--dev] [--debug] [--target=wasm32-wasi]";
|
||||
[--dev] [--debug] [--sanitize] [--target=wasm32-wasi]";
|
||||
exit 2
|
||||
in
|
||||
with_errors path (fun () ->
|
||||
@ -193,7 +205,8 @@ let () =
|
||||
raylib and still be buildable for wasm32. *)
|
||||
let p, csrcs, lflags = Flan.Reach.link ~dev l p in
|
||||
ignore (Flan.Build.executable
|
||||
~opts:{ Flan.Build.default with checks; dev; debug; target }
|
||||
~opts:{ Flan.Build.default with checks; dev; debug; sanitize;
|
||||
target }
|
||||
~csrcs ~lflags ~pnames:(if debug then param_names l else [])
|
||||
p ~out))
|
||||
(* The daemon an editor talks to: one session, the program it belongs to
|
||||
@ -272,7 +285,7 @@ let () =
|
||||
prerr_endline
|
||||
"usage: flan (read|parse|check|emit|shim) <file.flan>...\n\
|
||||
\ flan build <file.flan> [-o out] [--no-bounds-checks] [--dev] \
|
||||
[--debug] [--target=wasm32-wasi]\n\
|
||||
[--debug] [--sanitize] [--target=wasm32-wasi]\n\
|
||||
\ flan run <file.flan> [args...]\n\
|
||||
\ flan reload <program.flan> <forms.flan> [-o out.so]\n\
|
||||
\ flan dev <program.flan> [-s socket]";
|
||||
|
||||
66
lib/build.ml
66
lib/build.ml
@ -72,6 +72,28 @@ type opts = {
|
||||
mechanism is a [llvm.dbg.declare] on an alloca and mem2reg deletes the
|
||||
alloca. *)
|
||||
debug : bool;
|
||||
(* AddressSanitizer and UndefinedBehaviorSanitizer over the whole program:
|
||||
the runtime's C, the generated shim, and — via [Emit]'s
|
||||
[sanitize_address] attribute — the Flan code itself.
|
||||
|
||||
Its own axis and not a mode of [debug]. It deliberately does *not* force
|
||||
-O0: the UB worth finding (a shift past the width folding to nothing, a
|
||||
float cast that only traps once it is a real cvttss2si) is what the
|
||||
optimiser does with it, so the sweep is worth running at -O2 and at -O0
|
||||
and any divergence between the two is itself the finding. It does pull in
|
||||
-g, because a report without a line number costs more to read than the
|
||||
build costs to make.
|
||||
|
||||
What reaches what, measured rather than assumed:
|
||||
- ASan instruments Flan functions only because [Emit] attributes them;
|
||||
globals get their redzone from the module pass either way.
|
||||
- UBSan instruments the C only. Its checks come out of clang's C
|
||||
frontend, and there is no attribute that asks a pass for them, so
|
||||
hand-written IR gets none. See [Emit]'s [sanitize] comment.
|
||||
- signed-integer-overflow is excluded because wrapping is what this
|
||||
language's arithmetic means; without the exclusion every program
|
||||
trips on its first [+]. Nothing else is excluded. *)
|
||||
sanitize : bool;
|
||||
}
|
||||
|
||||
(* Checks are deliberately independent of [opt]: the acceptance table runs the
|
||||
@ -80,7 +102,24 @@ type opts = {
|
||||
checks. Dropping them is a release decision, not an optimisation one. *)
|
||||
let default =
|
||||
{ target = None; opt = "-O2"; keep = false; checks = true; dev = false;
|
||||
debug = false }
|
||||
debug = false; sanitize = false }
|
||||
|
||||
(* The flags that are neither [opt] nor the target, spelled once so that the
|
||||
compile command and the object-cache key cannot disagree. They did before:
|
||||
-g was written out at the command and again at the key, and a flag that
|
||||
appears in one and not the other is the silent failure — an unsanitized
|
||||
[flan_rt.o] served out of the cache to a sanitized build links fine and
|
||||
reports nothing. *)
|
||||
let cflags opts =
|
||||
(if opts.debug then [ "-g" ] else [])
|
||||
@ (if opts.sanitize then
|
||||
(* -g here and not via [debug]: a sanitizer report with no file and no
|
||||
line is most of the work still to do. *)
|
||||
[ "-fsanitize=address,undefined";
|
||||
"-fno-sanitize=signed-integer-overflow";
|
||||
"-fno-omit-frame-pointer" ]
|
||||
@ (if opts.debug then [] else [ "-g" ])
|
||||
else [])
|
||||
|
||||
(* ── wasm32, which needs more than a triple ──────────────────────────
|
||||
The native target is whatever clang was built for, so [--target=] alone is
|
||||
@ -278,7 +317,7 @@ let compile_c ~opts ?tflags ~src ~name () =
|
||||
(Digest.string
|
||||
(String.concat "\000"
|
||||
[ name; src; Lazy.force clang_stamp; opts.opt;
|
||||
(if opts.debug then "-g" else "");
|
||||
String.concat " " (cflags opts);
|
||||
String.concat " " tflags ]))
|
||||
in
|
||||
let obj = Filename.concat (cachedir ()) (key ^ ".o") in
|
||||
@ -292,7 +331,7 @@ let compile_c ~opts ?tflags ~src ~name () =
|
||||
let cmd =
|
||||
String.concat " "
|
||||
([ Filename.quote clang; opts.opt ]
|
||||
@ (if opts.debug then [ "-g" ] else [])
|
||||
@ cflags opts
|
||||
@ [ "-c" ] @ tflags
|
||||
@ [ Filename.quote c; "-o"; Filename.quote tmp ])
|
||||
in
|
||||
@ -327,14 +366,23 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
|
||||
"wasm32: --debug is native only — the DWARF member offsets are computed \
|
||||
for the host's layout, and wasm32's 32-bit pointer moves every one of \
|
||||
them";
|
||||
(* There is no wasm32 sanitizer runtime to link against: clang accepts
|
||||
-fsanitize=address for the triple and the link fails on
|
||||
__asan_report_load4. Refused by name rather than met at the linker. *)
|
||||
if wasm_target opts && opts.sanitize then
|
||||
failwith
|
||||
"wasm32: --sanitize is native only — there is no libclang_rt.asan for \
|
||||
wasm32-wasi to link against";
|
||||
(* -O0 is not a choice a debug build offers: [llvm.dbg.declare] describes an
|
||||
alloca, and at -O2 mem2reg deletes the alloca. *)
|
||||
alloca, and at -O2 mem2reg deletes the alloca. [sanitize] deliberately
|
||||
does not do this: see [opts]. *)
|
||||
let opts = if opts.debug then { opts with opt = "-O0" } else opts in
|
||||
let tflags = target_flags opts in
|
||||
let dir = workdir () in
|
||||
let ll = Filename.concat dir (Filename.basename out ^ ".ll") in
|
||||
write ll
|
||||
(Emit.program ~checks:opts.checks ~dev:opts.dev ~debug:opts.debug ~pnames p);
|
||||
(Emit.program ~checks:opts.checks ~dev:opts.dev ~debug:opts.debug ~pnames
|
||||
~sanitize:opts.sanitize p);
|
||||
(* [flan_dev.c] is compiled into every build, not only a dev one. Nothing in
|
||||
a release build calls into it — the compiler only emits a registry lookup
|
||||
for a name the host was not built with, which cannot arise without cells —
|
||||
@ -368,8 +416,12 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
|
||||
String.concat " "
|
||||
([ Filename.quote clang; opts.opt; "-Wno-override-module" ]
|
||||
(* -g at the link so clang does not strip, and keeps the object files'
|
||||
debug sections; the .ll carries its own. *)
|
||||
@ (if opts.debug then [ "-g" ] else [])
|
||||
debug sections; the .ll carries its own. The sanitizer flags have to
|
||||
be here too — they are what pulls in libclang_rt.asan and the UBSan
|
||||
runtime, and they are also what makes clang run the ASan pass over
|
||||
the .ll, which is the only place the Flan half of the program gets
|
||||
instrumented at all. *)
|
||||
@ cflags opts
|
||||
@ (if opts.dev then [ "-rdynamic" ] else [])
|
||||
@ tflags
|
||||
@ [ Filename.quote ll ]
|
||||
|
||||
35
lib/emit.ml
35
lib/emit.ml
@ -193,9 +193,26 @@ type m = {
|
||||
down because every emitter that can produce an instruction has to be able
|
||||
to hang a location on it. *)
|
||||
dbg : dbg option;
|
||||
(* True in a sanitized build, and the whole of what ASan needs from us.
|
||||
AddressSanitizer is an LLVM *pass*, but it instruments only functions
|
||||
carrying the [sanitize_address] attribute — which clang's C frontend adds
|
||||
and nothing adds to IR written by hand. Passing -fsanitize=address to the
|
||||
clang run over this .ll therefore instruments the runtime's C and not one
|
||||
instruction of Flan; measured, not assumed (see NEXT.md). So every
|
||||
[define] here names attribute group #0 and [finish] writes it out.
|
||||
|
||||
There is no equivalent for UndefinedBehaviorSanitizer: its checks are
|
||||
emitted by the C frontend as branches to __ubsan_handle_*, and no
|
||||
attribute asks a pass to produce them. UBSan over this .ll covers the C
|
||||
and nothing else. *)
|
||||
sanitize : bool;
|
||||
mutable nstr : int;
|
||||
}
|
||||
|
||||
(* The attribute group every emitted function names, empty unless sanitizing.
|
||||
Spelled once so the [define] sites and [finish] cannot disagree. *)
|
||||
let attrs m = if m.sanitize then " #0" else ""
|
||||
|
||||
let field_ty m sn i =
|
||||
let s = Hashtbl.find m.structs sn in
|
||||
(List.nth s.Tast.fields i).Tast.fty
|
||||
@ -1472,8 +1489,8 @@ let emit_fn m ?(hidden = false) ?(pnames = []) (fn : Tast.fn) =
|
||||
end
|
||||
end;
|
||||
Buffer.add_string m.out
|
||||
(Printf.sprintf "\ndefine %s%s%s {\nentry:\n%s%s}\n"
|
||||
(if hidden then "hidden " else "") (signature ~named:true fn)
|
||||
(Printf.sprintf "\ndefine %s%s%s%s {\nentry:\n%s%s}\n"
|
||||
(if hidden then "hidden " else "") (signature ~named:true fn) (attrs m)
|
||||
(match dsub with None -> "" | Some n -> Printf.sprintf " !dbg !%d" n)
|
||||
(Buffer.contents f.allocas) (Buffer.contents f.b))
|
||||
|
||||
@ -1557,7 +1574,9 @@ declare void @flan_slice_fail(ptr, i64, i64, i64, i64) noreturn cold
|
||||
the i32 status are each optional (plan.org, Milestone-2 primitives). *)
|
||||
let emit_main m (fn : Tast.fn) =
|
||||
let b = Buffer.create 256 in
|
||||
Buffer.add_string b "\ndefine i32 @main(i32 %argc, ptr %argv) {\nentry:\n";
|
||||
Buffer.add_string b
|
||||
(Printf.sprintf "\ndefine i32 @main(i32 %%argc, ptr %%argv)%s {\nentry:\n"
|
||||
(attrs m));
|
||||
Buffer.add_string b " call void @flan_rt_init(i32 %argc, ptr %argv)\n";
|
||||
(* The program's own end of the transfer channel. Nothing can be transferring
|
||||
when [main] returns: a restart is found by name on the restart stack, and
|
||||
@ -1616,12 +1635,13 @@ let new_dbg (p : Tast.program) =
|
||||
file);
|
||||
d
|
||||
|
||||
let new_module ~checks ~dev ~known ?(debug = false) (p : Tast.program) =
|
||||
let new_module ~checks ~dev ~known ?(debug = false) ?(sanitize = false)
|
||||
(p : Tast.program) =
|
||||
let m = {
|
||||
out = Buffer.create 8192; strs = Buffer.create 512;
|
||||
structs = Hashtbl.create 16; globals = Hashtbl.create 16;
|
||||
externs = Hashtbl.create 32;
|
||||
checks; dev; known; nstr = 0;
|
||||
checks; dev; known; nstr = 0; sanitize;
|
||||
dbg = (if debug then Some (new_dbg p) else None);
|
||||
} in
|
||||
List.iter (fun (s : Tast.structure) -> Hashtbl.replace m.structs s.Tast.sname s)
|
||||
@ -1676,13 +1696,14 @@ let dmodule d =
|
||||
|
||||
let finish m =
|
||||
header ^ Buffer.contents m.strs ^ "\n" ^ Buffer.contents m.out
|
||||
^ (if m.sanitize then "\nattributes #0 = { sanitize_address }\n" else "")
|
||||
^ (match m.dbg with None -> "" | Some d -> dmodule d)
|
||||
|
||||
(* [checks] is on by default: a dev build traps on an out-of-bounds [at] or
|
||||
[slice], a release build is told to drop them. *)
|
||||
let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = [])
|
||||
(p : Tast.program) : string =
|
||||
let m = new_module ~checks ~dev ~known:(fun _ -> true) ~debug p in
|
||||
?(sanitize = false) (p : Tast.program) : string =
|
||||
let m = new_module ~checks ~dev ~known:(fun _ -> true) ~debug ~sanitize p in
|
||||
(* One cell per function, initialised to the function this build compiled.
|
||||
Nothing has been redefined yet, so a dev build starts out behaving exactly
|
||||
like a release one — the indirection is the only difference. *)
|
||||
|
||||
@ -184,9 +184,37 @@ void flan_exit(int32_t status) {
|
||||
#define SCRATCH 64
|
||||
static char scratch[SCRATCH]; /* rendered text lives here until the next call */
|
||||
|
||||
/* snprintf returns what it *would* have written, not what it did. The three
|
||||
* shims below hand the result back as a slice, so taking that number at face
|
||||
* value would publish a length past the end of the buffer and every reader of
|
||||
* that slice would run off it. No format here can reach 64 — %g is at most 13
|
||||
* characters and %lld at most 20 — so this clamp cannot fire today; it is here
|
||||
* because the distance between "cannot fire" and "reads off the end of a
|
||||
* static buffer" is one format string, and nothing else in the file says so.
|
||||
* Found by reading, under a sanitizer sweep that could not have found it:
|
||||
* nothing in the corpus prints a number long enough. */
|
||||
static int64_t fit(int n) {
|
||||
if (n < 0) return 0;
|
||||
return n < SCRATCH ? (int64_t)n : (int64_t)(SCRATCH - 1);
|
||||
}
|
||||
|
||||
/* The length is clamped below *and* above. Above is obvious and was always
|
||||
* here. Below was not, and it was the real one: a slice's length is a signed
|
||||
* 64-bit count, (slice s 2 1) computes 2 - 1 - 2 = -1, and `(size_t)n` on a
|
||||
* negative n is 18446744073709551615, which is not less than 511, so k became
|
||||
* 511 and the memcpy read 511 bytes from wherever the slice pointed. A checked
|
||||
* build traps on the reversed slice before it gets here; an unchecked one does
|
||||
* not, and every other (ptr, len) entry point in this file — flan_write_stdout,
|
||||
* flan_escape_bytes, flan_dev_emit — already guards the negative case. These
|
||||
* two were the exceptions. */
|
||||
static size_t clamp_len(int64_t n, size_t cap) {
|
||||
if (n <= 0) return 0;
|
||||
return (uint64_t)n < (uint64_t)cap ? (size_t)n : cap;
|
||||
}
|
||||
|
||||
double flan_bytes_to_f64(const uint8_t *p, int64_t n) {
|
||||
char buf[512];
|
||||
size_t k = (size_t)n < sizeof buf - 1 ? (size_t)n : sizeof buf - 1;
|
||||
size_t k = clamp_len(n, sizeof buf - 1);
|
||||
memcpy(buf, p, k);
|
||||
buf[k] = '\0';
|
||||
return strtod(buf, NULL);
|
||||
@ -194,7 +222,7 @@ double flan_bytes_to_f64(const uint8_t *p, int64_t n) {
|
||||
|
||||
int64_t flan_bytes_to_i64(const uint8_t *p, int64_t n) {
|
||||
char buf[64];
|
||||
size_t k = (size_t)n < sizeof buf - 1 ? (size_t)n : sizeof buf - 1;
|
||||
size_t k = clamp_len(n, sizeof buf - 1);
|
||||
memcpy(buf, p, k);
|
||||
buf[k] = '\0';
|
||||
return (int64_t)strtoll(buf, NULL, 10);
|
||||
@ -205,13 +233,13 @@ int64_t flan_bytes_to_i64(const uint8_t *p, int64_t n) {
|
||||
void flan_f64_to_bytes(double x, flan_slice *out) {
|
||||
int n = snprintf(scratch, SCRATCH, "%g", x);
|
||||
out->ptr = (const uint8_t *)scratch;
|
||||
out->len = n < 0 ? 0 : (int64_t)n;
|
||||
out->len = fit(n);
|
||||
}
|
||||
|
||||
void flan_i64_to_bytes(int64_t x, flan_slice *out) {
|
||||
int n = snprintf(scratch, SCRATCH, "%lld", (long long)x);
|
||||
out->ptr = (const uint8_t *)scratch;
|
||||
out->len = n < 0 ? 0 : (int64_t)n;
|
||||
out->len = fit(n);
|
||||
}
|
||||
|
||||
/* u64 is not i64 with a flag: 0xFFFFFFFFFFFFFFFF is 18446744073709551615 and
|
||||
@ -221,7 +249,7 @@ void flan_i64_to_bytes(int64_t x, flan_slice *out) {
|
||||
void flan_u64_to_bytes(uint64_t x, flan_slice *out) {
|
||||
int n = snprintf(scratch, SCRATCH, "%llu", (unsigned long long)x);
|
||||
out->ptr = (const uint8_t *)scratch;
|
||||
out->len = n < 0 ? 0 : (int64_t)n;
|
||||
out->len = fit(n);
|
||||
}
|
||||
|
||||
/* A string *inside* a printed structure, quoted and escaped, so that the run
|
||||
|
||||
31
test/dune
31
test/dune
@ -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)))
|
||||
|
||||
288
test/test_sanitize.ml
Normal file
288
test/test_sanitize.ml
Normal file
@ -0,0 +1,288 @@
|
||||
(* 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 ?(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);
|
||||
let exe = compile ~sanitize:true ~checks:false path in
|
||||
let _, text = run exe args in
|
||||
(match expect_report, reported text with
|
||||
| true, false -> fail "control %s: nothing reported. %s\n%s" name why text
|
||||
| false, true -> fail "control %s: reported. %s\n%s" name why text
|
||||
| _ -> ());
|
||||
(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. Not a property of the access: \
|
||||
ASan lays a global out as {data, redzone}, so an underflow is \
|
||||
caught when something redzoned precedes it and not when nothing \
|
||||
does — measured both ways, and here nothing does. Whether \
|
||||
reading before an array is seen at all is therefore up to what \
|
||||
the linker put 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 one past the end of a four-element global. Index 5 and not 9,
|
||||
and the difference is worth knowing: ASan registers this array as
|
||||
"16 bytes in a 32-byte slot", so the poisoned redzone is bytes 16..31.
|
||||
Index 5 is byte 20 and is caught; index 9 is byte 36, past the
|
||||
registration entirely, and is silent. Overrunning a small object by
|
||||
enough lands back in ordinary memory. *)
|
||||
control ~expect_report:true "flan-san-ctl-oob"
|
||||
~why:"This sweep is not instrumenting Flan code at all — check that \
|
||||
Emit still puts every define in the sanitize_address attribute \
|
||||
group, without which -fsanitize=address covers the runtime's C \
|
||||
and nothing else."
|
||||
"(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"
|
||||
~why:"UBSan has started seeing Flan code, which contradicts what this \
|
||||
file and Build.opts both say it reaches. Good news; rewrite them."
|
||||
"(defn main [] i32\n\
|
||||
\ (let [x 1] (let [n 32] (print (<< x n)) (println \"\")))\n\
|
||||
\ 0)\n";
|
||||
(* A regression case, and the one defect this exercise found: a slice's
|
||||
length is signed, (slice s 2 1) is -1, and flan_bytes_to_i64 cast that
|
||||
to size_t before comparing it against its buffer — so the memcpy copied
|
||||
63 bytes out of whatever the slice pointed at. Every other (ptr, len)
|
||||
entry point in the runtime already guarded the negative case; these two
|
||||
were the exceptions. A checked build traps on the reversed slice long
|
||||
before this, which is why it needs an unchecked build to show. *)
|
||||
control ~expect_report:false ~args:[ "2" ] "flan-san-ctl-negslice"
|
||||
~why:"flan_bytes_to_i64 or flan_bytes_to_f64 is reading off the end of \
|
||||
a negative-length slice again — see clamp_len in flan_rt.c."
|
||||
"(defn main [args [string]] i32\n\
|
||||
\ (let [s (bytes \"42\")\n\
|
||||
\ n (i32 (bytes->i64 (bytes (at args 1))))]\n\
|
||||
\ (print (bytes->i64 (slice s n 1)))\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"
|
||||
Loading…
x
Reference in New Issue
Block a user