flan dev --sanitize builds the host under ASan and UBSan on LLVM, refuses --x86 by name, and the sanitize sweep drives a real session through reloads and breaks
This commit is contained in:
parent
f67498c789
commit
d0fc036bba
7
TODO.org
7
TODO.org
@ -1771,13 +1771,6 @@ nothing orders the two. The read raised on a closed socket and the test binary
|
|||||||
exited 1 with no failure line, which is the worst shape a failure can have when
|
exited 1 with no failure line, which is the worst shape a failure can have when
|
||||||
a lane is judged on the exit status.
|
a lane is judged on the exit status.
|
||||||
|
|
||||||
** NEXT A program driven by a real flan dev daemon under a sanitizer
|
|
||||||
Decided 2026-09-25: =flan dev --sanitize= builds the host under ASan/UBSan on the LLVM backend (refused by name with =--x86=), and the @sanitize alias gains a case driving a real session through reloads and a break.
|
|
||||||
The daemon builds its host through its own path and the CLI has no way to pass a
|
|
||||||
sanitizer flag to it. Named as the check worth adding next; a day rather than an
|
|
||||||
hour. The x86 backend is not a gap here — that pair is refused by name, because
|
|
||||||
there is no sanitizer pass over hand-written assembly.
|
|
||||||
|
|
||||||
** DONE A transient signal 11 on a globals daemon
|
** DONE A transient signal 11 on a globals daemon
|
||||||
CLOSED: [2026-09-25]
|
CLOSED: [2026-09-25]
|
||||||
Not a segfault. The report was OCaml's signal number, and in OCaml's numbering
|
Not a segfault. The report was OCaml's signal number, and in OCaml's numbering
|
||||||
|
|||||||
12
bin/main.ml
12
bin/main.ml
@ -782,7 +782,11 @@ let () =
|
|||||||
which is the point of leaving it readable here — the combination stays
|
which is the point of leaving it readable here — the combination stays
|
||||||
refused by name, it is just no longer somewhere you arrive by typing one
|
refused by name, it is just no longer somewhere you arrive by typing one
|
||||||
flag. *)
|
flag. *)
|
||||||
let x86 = backend_x86 ~default:(not debug) rest in
|
(* --sanitize takes [--llvm]'s side for the reason [--debug] does: the
|
||||||
|
sanitizers are LLVM passes. [--x86] written as well is refused by name
|
||||||
|
in [Dev.start]. *)
|
||||||
|
let sanitize = List.mem sanitize_flag rest in
|
||||||
|
let x86 = backend_x86 ~default:(not (debug || sanitize)) rest in
|
||||||
let asked_x86 = List.mem x86_flag rest in
|
let asked_x86 = List.mem x86_flag rest in
|
||||||
let merged = not (List.mem two_process_flag rest) in
|
let merged = not (List.mem two_process_flag rest) in
|
||||||
let rest = List.filter (fun a -> not (is_flag a)) rest in
|
let rest = List.filter (fun a -> not (is_flag a)) rest in
|
||||||
@ -792,8 +796,8 @@ let () =
|
|||||||
| [] -> Filename.concat (Filename.dirname path) ".flan-dev.sock"
|
| [] -> Filename.concat (Filename.dirname path) ".flan-dev.sock"
|
||||||
| _ ->
|
| _ ->
|
||||||
prerr_endline
|
prerr_endline
|
||||||
"usage: flan dev <program.flan> [-s socket] [--debug] [--llvm] \
|
"usage: flan dev <program.flan> [-s socket] [--debug] [--sanitize] \
|
||||||
[--two-process]";
|
[--llvm] [--two-process]";
|
||||||
exit 2
|
exit 2
|
||||||
in
|
in
|
||||||
(* Only this command hands one over, and only when it chose the backend
|
(* Only this command hands one over, and only when it chose the backend
|
||||||
@ -809,7 +813,7 @@ let () =
|
|||||||
else None
|
else None
|
||||||
in
|
in
|
||||||
with_errors ?x86_hint path (fun () ->
|
with_errors ?x86_hint path (fun () ->
|
||||||
Flan.Dev.start ~debug ~merged ~x86 ~file:path ~sock ())
|
Flan.Dev.start ~debug ~sanitize ~merged ~x86 ~file:path ~sock ())
|
||||||
|
|
||||||
(* One redefinition, built the way an editor will ask for it: a session over
|
(* One redefinition, built the way an editor will ask for it: a session over
|
||||||
the program the process was built from, and a file of the forms that
|
the program the process was built from, and a file of the forms that
|
||||||
|
|||||||
@ -1045,8 +1045,9 @@ the two builds are *supposed* to differ, since `flan_dev_crash_enable` checks a
|
|||||||
install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's
|
install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's
|
||||||
line, built at `-O0` because at `-O2` a store through a zeroed `(Ptr u8)` is undefined and need not fault. That yield had
|
line, built at `-O0` because at `-O2` a store through a zeroed `(Ptr u8)` is undefined and need not fault. That yield had
|
||||||
never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm.
|
never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm.
|
||||||
What it still does not reach is a program driven by a real daemon under ASan: `flan dev` builds its host through its own
|
`dev_session` drives a real `flan dev --sanitize` session — merged, LLVM, the compiler's OCaml in the same process as
|
||||||
path and has no `--sanitize` to pass it.
|
the sanitized host — through a break, three reloads and a second break; the modules it sends are still not
|
||||||
|
instrumented.
|
||||||
|
|
||||||
**Two aliases were green only because `dune test` runs first, and that is the same disease in a different place.**
|
**Two aliases were green only because `dune test` runs first, and that is the same disease in a different place.**
|
||||||
`@sanitize` never listed the package directories `pkg-diamond.flan` imports and `@page` never listed `sand.flan`, which
|
`@sanitize` never listed the package directories `pkg-diamond.flan` imports and `@page` never listed `sand.flan`, which
|
||||||
@ -1821,7 +1822,9 @@ shape TODO.org's "The compiler is a thread inside the program" landed on: **the
|
|||||||
program's process. It is SLIME's model — you start the image, it serves, the editor connects.
|
program's process. It is SLIME's model — you start the image, it serves, the editor connects.
|
||||||
|
|
||||||
`--two-process` is the escape hatch, for a machine where the compiler object cannot be built (no `ocamlfind`, no
|
`--two-process` is the escape hatch, for a machine where the compiler object cannot be built (no `ocamlfind`, no
|
||||||
`flan.cmxa` beside the binary). It has its own test and it stays.
|
`flan.cmxa` beside the binary). It has its own test and it stays. A re-run there is a new child built from the session
|
||||||
|
as it stands, so the redefinitions are in it and the globals start over; the daemon outlives a finished child to take
|
||||||
|
that request.
|
||||||
|
|
||||||
**The editor socket and its wire protocol did not move.** Emacs cannot tell the difference, which is what made the merge
|
**The editor socket and its wire protocol did not move.** Emacs cannot tell the difference, which is what made the merge
|
||||||
testable: the whole existing suite is the check.
|
testable: the whole existing suite is the check.
|
||||||
|
|||||||
25
lib/dev.ml
25
lib/dev.ml
@ -5281,7 +5281,7 @@ let report_dropped ~file = function
|
|||||||
deletes it — and silently making every reloaded body -O0 would change the
|
deletes it — and silently making every reloaded body -O0 would change the
|
||||||
frame time of the one function you are iterating on, in the loop whose whole
|
frame time of the one function you are iterating on, in the loop whose whole
|
||||||
point is watching that number. *)
|
point is watching that number. *)
|
||||||
let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
|
let two_process ?(debug = false) ?(sanitize = false) ?(x86 = true) ~file ~sock () =
|
||||||
let t0 = Unix.gettimeofday () in
|
let t0 = Unix.gettimeofday () in
|
||||||
(* Absolute, because every location this daemon ever reports is derived from
|
(* Absolute, because every location this daemon ever reports is derived from
|
||||||
it and an editor is not in this process's working directory. [flan dev
|
it and an editor is not in this process's working directory. [flan dev
|
||||||
@ -5316,7 +5316,7 @@ let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
|
|||||||
let _, kept =
|
let _, kept =
|
||||||
Build.executable
|
Build.executable
|
||||||
~opts:{ Build.default with Build.dev = true; Build.keep = true;
|
~opts:{ Build.default with Build.dev = true; Build.keep = true;
|
||||||
Build.debug; Build.x86 }
|
Build.debug; Build.sanitize; Build.x86 }
|
||||||
~csrcs ~lflags session.Session.host ~out:exe
|
~csrcs ~lflags session.Session.host ~out:exe
|
||||||
in
|
in
|
||||||
match kept with
|
match kept with
|
||||||
@ -6336,7 +6336,7 @@ let merged_serve () =
|
|||||||
(* The merged build is made here and then [exec]'d, so what an editor talks to
|
(* The merged build is made here and then [exec]'d, so what an editor talks to
|
||||||
is the program itself rather than something that launched it. The launcher
|
is the program itself rather than something that launched it. The launcher
|
||||||
does not survive: there is one process from the first reply onwards. *)
|
does not survive: there is one process from the first reply onwards. *)
|
||||||
let start_merged ?(debug = false) ?(x86 = true) ~file ~sock () =
|
let start_merged ?(debug = false) ?(sanitize = false) ?(x86 = true) ~file ~sock () =
|
||||||
let t0 = Unix.gettimeofday () in
|
let t0 = Unix.gettimeofday () in
|
||||||
let dir = session_dir ~file ~sock in
|
let dir = session_dir ~file ~sock in
|
||||||
let given = file in
|
let given = file in
|
||||||
@ -6354,7 +6354,8 @@ let start_merged ?(debug = false) ?(x86 = true) ~file ~sock () =
|
|||||||
let host_ll = Filename.concat dir (if x86 then "host.s" else "host.ll") in
|
let host_ll = Filename.concat dir (if x86 then "host.s" else "host.ll") in
|
||||||
ignore
|
ignore
|
||||||
(merged_executable
|
(merged_executable
|
||||||
~opts:{ Build.default with Build.dev = true; Build.debug; Build.x86 }
|
~opts:{ Build.default with Build.dev = true; Build.debug;
|
||||||
|
Build.sanitize; Build.x86 }
|
||||||
~csrcs ~lflags ~pnames:[]
|
~csrcs ~lflags ~pnames:[]
|
||||||
session.Session.host ~out:exe ~ll:host_ll);
|
session.Session.host ~out:exe ~ll:host_ll);
|
||||||
(* Read by the park, so the first one says the session is waiting rather
|
(* Read by the park, so the first one says the session is waiting rather
|
||||||
@ -6395,7 +6396,17 @@ let start_merged ?(debug = false) ?(x86 = true) ~file ~sock () =
|
|||||||
flan.cmxa beside the binary — and it is what every behaviour in this file
|
flan.cmxa beside the binary — and it is what every behaviour in this file
|
||||||
was written against, so it stays until the transport it exists to drive is
|
was written against, so it stays until the transport it exists to drive is
|
||||||
actually deleted. *)
|
actually deleted. *)
|
||||||
let start ?(debug = false) ?(merged = true) ?(x86 = true) ~file ~sock () =
|
let start ?(debug = false) ?(sanitize = false) ?(merged = true) ?(x86 = true)
|
||||||
|
~file ~sock () =
|
||||||
|
(* The sanitizers are LLVM passes, and the x86 backend's host is written
|
||||||
|
by hand with no pass run over it. The modules a session sends are not
|
||||||
|
instrumented on either backend; what is checked is the host and the
|
||||||
|
runtime, which is where a dev session's own bookkeeping lives. *)
|
||||||
|
if x86 && sanitize then
|
||||||
|
failwith
|
||||||
|
"flan dev --x86 --sanitize: the sanitizers instrument LLVM's output, and \
|
||||||
|
the x86 backend writes its code by hand, so the program's own code \
|
||||||
|
would not be checked. Drop --x86 to build this session with LLVM.";
|
||||||
(* x86 unless told otherwise, and the default is here rather than only in
|
(* x86 unless told otherwise, and the default is here rather than only in
|
||||||
[bin/main.ml] so that there is one answer to "what backend is a dev
|
[bin/main.ml] so that there is one answer to "what backend is a dev
|
||||||
session". A library caller that starts a daemon starts the same daemon the
|
session". A library caller that starts a daemon starts the same daemon the
|
||||||
@ -6445,5 +6456,5 @@ let start ?(debug = false) ?(merged = true) ?(x86 = true) ~file ~sock () =
|
|||||||
|
|
||||||
[--x86 --debug] above is still refused, and for a reason that has nothing
|
[--x86 --debug] above is still refused, and for a reason that has nothing
|
||||||
to do with this one. *)
|
to do with this one. *)
|
||||||
if merged then start_merged ~debug ~x86 ~file ~sock ()
|
if merged then start_merged ~debug ~sanitize ~x86 ~file ~sock ()
|
||||||
else two_process ~debug ~x86 ~file ~sock ()
|
else two_process ~debug ~sanitize ~x86 ~file ~sock ()
|
||||||
|
|||||||
@ -129,7 +129,9 @@
|
|||||||
; a Flan program: flan_dyn.c has no Flan spelling yet. It is also the one
|
; a Flan program: flan_dyn.c has no Flan spelling yet. It is also the one
|
||||||
; translation unit here that frees the most, which is what makes it worth a
|
; translation unit here that frees the most, which is what makes it worth a
|
||||||
; sanitized run at all. See [dyn_sweep].
|
; sanitized run at all. See [dyn_sweep].
|
||||||
(file dyn_ops.c))
|
(file dyn_ops.c)
|
||||||
|
; [dev_session] drives a real flan dev --sanitize.
|
||||||
|
(file %{workspace_root}/bin/main.exe))
|
||||||
(action (run ./test_sanitize.exe)))
|
(action (run ./test_sanitize.exe)))
|
||||||
|
|
||||||
; The corpus a third time, under Valgrind's memcheck. Its own alias for the
|
; The corpus a third time, under Valgrind's memcheck. Its own alias for the
|
||||||
|
|||||||
@ -376,13 +376,8 @@ let dyn_sweep () =
|
|||||||
part that carries the weight; the run is what says the constructor the fix
|
part that carries the weight; the run is what says the constructor the fix
|
||||||
introduced actually calls both of the things it replaced.
|
introduced actually calls both of the things it replaced.
|
||||||
|
|
||||||
Not covered, and worth naming rather than leaving to be discovered the way
|
A program driven by a real [flan dev] session is [dev_session] below, and
|
||||||
this bug was: a program driven by [flan dev] under ASan. The daemon builds
|
the faulting dev build is [dev_segv]. *)
|
||||||
its host through its own path and the CLI has no [--sanitize] to pass it,
|
|
||||||
so that one wants a flag and a way through [Dev.serve]. See TODO.org, "A
|
|
||||||
program driven by a real flan dev daemon under a sanitizer". The faulting
|
|
||||||
dev build, which was on that list too, is covered now — see
|
|
||||||
[dev_segv] below. *)
|
|
||||||
let dev_corpus =
|
let dev_corpus =
|
||||||
[ (* The only [dev-*] program with no agent import: it prints and returns.
|
[ (* The only [dev-*] program with no agent import: it prints and returns.
|
||||||
Here because it is the one program in the tree written for a dev
|
Here because it is the one program in the tree written for a dev
|
||||||
@ -474,6 +469,93 @@ let dev_segv () =
|
|||||||
prevent\n%s" text;
|
prevent\n%s" text;
|
||||||
(try Sys.remove exe with Sys_error _ -> ())
|
(try Sys.remove exe with Sys_error _ -> ())
|
||||||
|
|
||||||
|
(* A program driven by a real [flan dev --sanitize] session: the host and the
|
||||||
|
runtime under ASan and UBSan, the modules the session sends built as
|
||||||
|
always (llc and ld, not instrumented). dev-break stops on its first frame,
|
||||||
|
so the session starts at a break; it is resumed, [step] is redefined three
|
||||||
|
times with an expression evaluated after each, an expression is evaluated
|
||||||
|
into a second break and resumed out of it, and the session is closed. The
|
||||||
|
daemon's own output is the program's stderr, so a report anywhere in the
|
||||||
|
session lands in it. *)
|
||||||
|
let dev_session () =
|
||||||
|
let flan = "../bin/main.exe" in
|
||||||
|
let sock = Filename.concat scratch "flan-san-dev.sock" in
|
||||||
|
let log = Filename.concat scratch "flan-san-dev.log" in
|
||||||
|
let src = "programs/dev-break.flan" in
|
||||||
|
(try Sys.remove sock with Sys_error _ -> ());
|
||||||
|
let fd = Unix.openfile log [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600 in
|
||||||
|
let env =
|
||||||
|
Array.append (Unix.environment ())
|
||||||
|
[| "ASAN_OPTIONS=detect_leaks=0"; "UBSAN_OPTIONS=print_stacktrace=1" |]
|
||||||
|
in
|
||||||
|
let pid =
|
||||||
|
Unix.create_process_env flan
|
||||||
|
[| flan; "dev"; src; "-s"; sock; "--sanitize" |]
|
||||||
|
env Unix.stdin fd fd
|
||||||
|
in
|
||||||
|
Unix.close fd;
|
||||||
|
let said () = In_channel.with_open_bin log In_channel.input_all in
|
||||||
|
if not (Test_support.listening ~ms:180000 ~pid sock) then begin
|
||||||
|
fail "dev session: flan dev --sanitize %s\n%s" !Test_support.listen_why
|
||||||
|
(said ());
|
||||||
|
(try Unix.kill pid Sys.sigkill with Unix.Unix_error _ -> ())
|
||||||
|
end
|
||||||
|
else begin
|
||||||
|
let c = Test_support.connect sock in
|
||||||
|
let ask q = Wire.parse (Wire.send c q; Wire.recv c) in
|
||||||
|
let field r k = Option.value ~default:"" (Wire.string_field r k) in
|
||||||
|
let stopped () =
|
||||||
|
match Wire.field (ask "(:op \"describe\")") "stopped" with
|
||||||
|
| Some { Form.v = Form.Sym "t"; _ } -> true
|
||||||
|
| _ -> false
|
||||||
|
in
|
||||||
|
let expect what r =
|
||||||
|
if field r "status" <> "ok" then
|
||||||
|
fail "dev session: %s: %s" what (field r "message")
|
||||||
|
in
|
||||||
|
let f = Printf.sprintf ":file %S" src in
|
||||||
|
if not (Test_support.await ~ms:30000 stopped) then
|
||||||
|
fail "dev session: the program never reached its first break"
|
||||||
|
else begin
|
||||||
|
expect "retry" (ask "(:op \"restart\" :name \"retry\")");
|
||||||
|
if not (Test_support.await ~ms:10000 (fun () -> not (stopped ()))) then
|
||||||
|
fail "dev session: the program did not resume";
|
||||||
|
for i = 1 to 3 do
|
||||||
|
expect "a redefinition"
|
||||||
|
(ask
|
||||||
|
(Printf.sprintf
|
||||||
|
"(:op \"eval\" :code \"(defn step [] i64 (set ticks (+ ticks \
|
||||||
|
%d)) ticks)\" %s)" (100 * i) f));
|
||||||
|
expect "an expression"
|
||||||
|
(ask (Printf.sprintf "(:op \"eval-expr\" :code \"(+ ticks 1)\" %s)" f))
|
||||||
|
done;
|
||||||
|
let r = ask (Printf.sprintf "(:op \"eval-expr\" :code \"(divide 1 0)\" %s)" f) in
|
||||||
|
if not (contains (field r "condition") "ArithError") then
|
||||||
|
fail "dev session: (divide 1 0) did not stop on ArithError: %s"
|
||||||
|
(field r "message");
|
||||||
|
expect "use-zero" (ask "(:op \"restart\" :name \"use-zero\")");
|
||||||
|
if not (Test_support.await ~ms:10000 (fun () -> not (stopped ()))) then
|
||||||
|
fail "dev session: the program did not resume from the second break";
|
||||||
|
expect "an expression after both breaks"
|
||||||
|
(ask (Printf.sprintf "(:op \"eval-expr\" :code \"(+ 1 2)\" %s)" f))
|
||||||
|
end;
|
||||||
|
(try ignore (ask "(:op \"close\")") with _ -> ());
|
||||||
|
(try Unix.close c with Unix.Unix_error _ -> ());
|
||||||
|
if not
|
||||||
|
(Test_support.await ~ms:30000 (fun () ->
|
||||||
|
match Unix.waitpid [ Unix.WNOHANG ] pid with
|
||||||
|
| 0, _ -> false
|
||||||
|
| _ -> true))
|
||||||
|
then begin
|
||||||
|
fail "dev session: the daemon did not end on close";
|
||||||
|
(try Unix.kill pid Sys.sigkill with Unix.Unix_error _ -> ());
|
||||||
|
(try ignore (Unix.waitpid [] pid) with Unix.Unix_error _ -> ())
|
||||||
|
end;
|
||||||
|
if reported (said ()) then
|
||||||
|
fail "dev session: sanitizer report\n%s" (said ())
|
||||||
|
end;
|
||||||
|
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) [ sock; log ]
|
||||||
|
|
||||||
(* The positive controls, which are the only evidence that a clean sweep means
|
(* 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
|
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
|
neither is a program anybody should build: one reads off the end of an
|
||||||
@ -600,6 +682,7 @@ let () =
|
|||||||
dyn_sweep ();
|
dyn_sweep ();
|
||||||
dev_sweep ();
|
dev_sweep ();
|
||||||
dev_segv ();
|
dev_segv ();
|
||||||
|
dev_session ();
|
||||||
unchecked_controls ();
|
unchecked_controls ();
|
||||||
if !failures = 0 then print_endline "sanitizer sweep: clean"
|
if !failures = 0 then print_endline "sanitizer sweep: clean"
|
||||||
else Printf.printf "%d sanitizer failure(s)\n" !failures;
|
else Printf.printf "%d sanitizer failure(s)\n" !failures;
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user