Review follow-ups: the constructor took a name a program can write
The wrapper was called flan.dev.ctor, and that is a name Flan can reach: (defn dev.ctor [] i32 7) mangles onto exactly it. The program compiles and runs as a release build and fails a dev build with a redefinition clang refuses -- loud, and only under LLVM with --dev, but mangle.ml's own comment exists to make it impossible rather than loud. The name is [Mangle.dev_ctor] now and starts with the dot no reader token can produce, beside .init-globals and .init-data. The colliding program builds and prints 7. Two comments in survey.sh, both of them reasoning rather than behaviour. The counts argument against a per-name -O0 list was no argument: excluding moves the counts just as much. What actually carries it is that dies_segv builds both programs at -O0 on both backends and asserts more than this sweep would. And dev-segv's park under --dev is a forever-list reason that happens to land on a program this list already covers, not a second reason for this list. FIX.org takes the sweep, and one thing the sweep cannot say: the two heap cases of bytes-copy.flan leak 24 bytes through flan_bytes_dup, measured with --leak-check=full, and both corpora are blind to it by policy -- detect_leaks=0 on one side and --leak-check=no on the other. The row proves the copy is in bounds and written. It says nothing about who frees it, and a green sweep should not be read as though it did.
This commit is contained in:
parent
892366e86d
commit
75177a5a18
38
FIX.org
38
FIX.org
@ -4495,3 +4495,41 @@ two walks — the Ast rename and the Form-level one at load.ml:503 — learn to
|
|||||||
walk more than one bound. The Form walk matched Vec [n; count] exactly, so
|
walk more than one bound. The Form walk matched Vec [n; count] exactly, so
|
||||||
it had to grow; before this, a three-bound dotimes was a parse error long
|
it had to grow; before this, a three-bound dotimes was a parse error long
|
||||||
before that walk could see it, so nothing was ever miscompiled by it.
|
before that walk could see it, so nothing was ever miscompiled by it.
|
||||||
|
|
||||||
|
* The heavy sweep, 2026-09-21 — and the leak question bytes-copy cannot answer
|
||||||
|
@x86, @sanitize and @valgrind, batched over the four lanes since the last
|
||||||
|
sweep, all three green at the end. What they found, and what they could not:
|
||||||
|
|
||||||
|
One x86 failure, two rows of it: bytes-view-write and dev-segv, both from the
|
||||||
|
bytes/bytes-view lane. Not a miscompile — both store through a bytes-view of a
|
||||||
|
string literal, which is .rodata, and the survey compares at its own -O2 where
|
||||||
|
LLVM deletes the undefined store and exits 0 while the hand-written backend
|
||||||
|
executes it and takes 139. At -O0 the two agree exactly, and test_acceptance's
|
||||||
|
dies_segv rows already pin that on both backends. Excluded by name in
|
||||||
|
survey.sh, with the reason.
|
||||||
|
|
||||||
|
One real bug, pre-existing and found by hand rather than by an alias:
|
||||||
|
--dev --sanitize did not compile at all. See the commit; the short of it is
|
||||||
|
that clang 20's ASan module pass segfaults on an llvm.global_ctors naming a
|
||||||
|
declaration, so the weak __asan_init yield that keeps the dev build's SIGSEGV
|
||||||
|
handler out of ASan's way had never once run.
|
||||||
|
|
||||||
|
** What neither corpus can answer about the new (bytes s)
|
||||||
|
bytes-copy.flan is in both sweeps now, and it is worth writing down what that
|
||||||
|
does not buy. Its first two cases leak 24 bytes through flan_bytes_dup —
|
||||||
|
measured, with valgrind --leak-check=full — and both sweeps miss it on
|
||||||
|
purpose: @sanitize runs with detect_leaks=0 and @valgrind with
|
||||||
|
--leak-check=no, each for the reason its own file gives, which is that
|
||||||
|
allocate-once-never-free is this runtime's design and a leak check produces a
|
||||||
|
suppression list rather than information.
|
||||||
|
|
||||||
|
So the row proves the copy is in bounds and its bytes are written. It does not
|
||||||
|
prove anything about who frees it, and nobody should read a green sweep as
|
||||||
|
saying the new allocating bytes has an owner. The leak question is worth
|
||||||
|
asking on purpose one day, across the whole corpus and not one program, and
|
||||||
|
that is a session of its own.
|
||||||
|
|
||||||
|
** Certified against 190fdad
|
||||||
|
The four-green result is measured against that base. dev-loop has moved since
|
||||||
|
— runtime/flan_rt.c, vendor/agent/flan_agent.c and lib/dev.ml among others —
|
||||||
|
and those belong to the next batch, not to this one.
|
||||||
|
|||||||
13
lib/emit.ml
13
lib/emit.ml
@ -4417,7 +4417,8 @@ let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = [])
|
|||||||
own constructors, and it costs a call before main.
|
own constructors, and it costs a call before main.
|
||||||
The ordering the wrapper now fixes was unspecified before — two entries
|
The ordering the wrapper now fixes was unspecified before — two entries
|
||||||
at one priority — and arming the registry before the handler is the
|
at one priority — and arming the registry before the handler is the
|
||||||
order that was wanted anyway. *)
|
order that was wanted anyway. Its name is [Mangle.dev_ctor] and the
|
||||||
|
leading dot there is load-bearing too; that comment says why. *)
|
||||||
(* Declared here rather than in the preamble, which is the one place a
|
(* Declared here rather than in the preamble, which is the one place a
|
||||||
declare is worth gating: the crash-handler lane then adds no dev-only
|
declare is worth gating: the crash-handler lane then adds no dev-only
|
||||||
text at all to a release module, and the only line it does add there —
|
text at all to a release module, and the only line it does add there —
|
||||||
@ -4426,15 +4427,19 @@ let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = [])
|
|||||||
[flan_dev_reg_enable] stays in the preamble ungated; it predates that
|
[flan_dev_reg_enable] stays in the preamble ungated; it predates that
|
||||||
lane and moving it was not its to make. *)
|
lane and moving it was not its to make. *)
|
||||||
Buffer.add_string m.out "declare void @flan_dev_crash_enable()\n";
|
Buffer.add_string m.out "declare void @flan_dev_crash_enable()\n";
|
||||||
|
let ctor = "@" ^ quoted Mangle.dev_ctor in
|
||||||
Buffer.add_string m.out
|
Buffer.add_string m.out
|
||||||
"define internal void @\"flan.dev.ctor\"() {\n\
|
(Printf.sprintf
|
||||||
|
"define internal void %s() {\n\
|
||||||
\ call void @flan_dev_reg_enable()\n\
|
\ call void @flan_dev_reg_enable()\n\
|
||||||
\ call void @flan_dev_crash_enable()\n\
|
\ call void @flan_dev_crash_enable()\n\
|
||||||
\ ret void\n\
|
\ ret void\n\
|
||||||
}\n";
|
}\n"
|
||||||
|
ctor);
|
||||||
Buffer.add_string m.out
|
Buffer.add_string m.out
|
||||||
|
(Printf.sprintf
|
||||||
"@llvm.global_ctors = appending global [1 x { i32, ptr, ptr }] \
|
"@llvm.global_ctors = appending global [1 x { i32, ptr, ptr }] \
|
||||||
[{ i32, ptr, ptr } { i32 65535, ptr @\"flan.dev.ctor\", ptr null }]\n";
|
[{ i32, ptr, ptr } { i32 65535, ptr %s, ptr null }]\n" ctor);
|
||||||
Buffer.add_char m.out '\n'
|
Buffer.add_char m.out '\n'
|
||||||
end;
|
end;
|
||||||
List.iter (emit_global m ~hidden) p.Tast.globals;
|
List.iter (emit_global m ~hidden) p.Tast.globals;
|
||||||
|
|||||||
@ -30,6 +30,16 @@ let prefix = "flan."
|
|||||||
and [.init-data] start with a dot no reader token can produce. *)
|
and [.init-data] start with a dot no reader token can produce. *)
|
||||||
let sym n = prefix ^ n
|
let sym n = prefix ^ n
|
||||||
|
|
||||||
|
(* The single constructor a dev build emits, which calls the runtime's two
|
||||||
|
enable entry points — the allocation registry and the crash handler — in
|
||||||
|
that order. It goes through [sym] with a leading dot for exactly the reason
|
||||||
|
that comment gives, and the reason is not decoration: the first spelling of
|
||||||
|
this was a plain [flan.dev.ctor], which is what [(defn dev.ctor [] i32 7)]
|
||||||
|
mangles to. That program compiles and runs as a release build and fails a
|
||||||
|
dev build with a redefinition clang refuses. A dot is what no reader token
|
||||||
|
can produce, so there is no Flan name that reaches this one. *)
|
||||||
|
let dev_ctor = prefix ^ ".dev-ctor"
|
||||||
|
|
||||||
(* A dev build's indirection cell: a mutable global holding the address of the
|
(* A dev build's indirection cell: a mutable global holding the address of the
|
||||||
function that is currently this name's body. *)
|
function that is currently this name's body. *)
|
||||||
let cell n = prefix ^ "cell." ^ n
|
let cell n = prefix ^ "cell." ^ n
|
||||||
|
|||||||
@ -103,13 +103,18 @@ forever="dev-loop dev-watch dev-chatty agent-auto"
|
|||||||
# this sweep would otherwise be duplicating at the one level where, as that
|
# this sweep would otherwise be duplicating at the one level where, as that
|
||||||
# file's own comment puts it, there is nothing left to pin but the UB.
|
# file's own comment puts it, there is nothing left to pin but the UB.
|
||||||
#
|
#
|
||||||
# Excluded by name rather than by building the whole corpus at -O0: the counts
|
# Excluded by name rather than by building these two at -O0 here, and the
|
||||||
# below are one measurement and every handoff's baseline was taken against it.
|
# reason is the coverage and not the counts: a per-name -O0 list would move the
|
||||||
|
# counts exactly as much as this does, so that is no argument at all. The
|
||||||
|
# argument is that dies_segv already builds both of them at -O0, on both
|
||||||
|
# backends, and asserts the exit status and the empty output -- everything this
|
||||||
|
# sweep would check, in the file where the ruling is written down.
|
||||||
#
|
#
|
||||||
# dev-segv would not belong here even if the store survived. It calls
|
# One more thing about dev-segv, which is a reason to keep it out of the
|
||||||
# agent/start, so it leaves a socket in /tmp on both runs, and under
|
# comparison rather than a reason for this list: it calls agent/start, so it
|
||||||
# SURVEY_FLAGS=--dev it parks in the break loop instead of dying -- two
|
# leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks
|
||||||
# truncations at the timeout, which is the dev-chatty failure by another road.
|
# in the break loop instead of dying -- which is a forever-list problem, met
|
||||||
|
# here by a program that was never going to be compared anyway.
|
||||||
faults="bytes-view-write dev-segv"
|
faults="bytes-view-write dev-segv"
|
||||||
|
|
||||||
TIMEOUT=${TIMEOUT:-20}
|
TIMEOUT=${TIMEOUT:-20}
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user