diff --git a/FIX.org b/FIX.org index 1a0f890..0621920 100644 --- a/FIX.org +++ b/FIX.org @@ -5430,3 +5430,41 @@ with a *new* def rather than one the fixture declares — see below. rule for diagnostics, but it is [session.ml]'s stale-caller tripwire, which is documented as unreachable and is not this lane's to loosen. A brand-new def is unaffected, which is what the test uses. + +* 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. diff --git a/lib/emit.ml b/lib/emit.ml index fc1c06d..2f48dac 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -4404,18 +4404,42 @@ let program ?(checks = true) ?(dev = false) ?(debug = false) ?(pnames = []) handler has to be installed before any program code can fault. Only in a dev build — the constructor is emitted here and nowhere else — so a release build dies exactly the way it always did. *) - Buffer.add_string m.out - "@llvm.global_ctors = appending global [2 x { i32, ptr, ptr }] \ - [{ i32, ptr, ptr } { i32 65535, ptr @flan_dev_reg_enable, ptr null }, \ - { i32, ptr, ptr } { i32 65535, ptr @flan_dev_crash_enable, ptr null }]\n"; + (* Both of them behind one constructor defined here, rather than named + directly in the table, and that shape is load-bearing rather than + tidiness. [llvm.global_ctors] naming a *declaration* — which both of + these are, they are C in the runtime — crashes clang 20's + AddressSanitizer module pass outright, so `--dev --sanitize` could not + compile any program at all; the whole combination was unreachable, and + that includes the [__asan_init] yield in [flan_dev_crash_enable] that + is the one thing keeping the crash handler out of ASan's way. Reduced + to five lines of IR here; it is an upstream crash and nobody has filed + it. A local definition in the table is what clang itself emits for its + own constructors, and it costs a call before main. + The ordering the wrapper now fixes was unspecified before — two entries + at one priority — and arming the registry before the handler is the + 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 - declare is worth gating: this lane then adds no dev-only text at all to - a release module, and the only line it does add there — + 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 — [flan_bytes_dup] — is a function release builds really call, since (bytes s) allocates in every build. The neighbouring - [flan_dev_reg_enable] stays in the preamble ungated; it predates this - and moving it is not this lane's to make. *) + [flan_dev_reg_enable] stays in the preamble ungated; it predates that + lane and moving it was not its to make. *) Buffer.add_string m.out "declare void @flan_dev_crash_enable()\n"; + let ctor = "@" ^ quoted Mangle.dev_ctor in + Buffer.add_string m.out + (Printf.sprintf + "define internal void %s() {\n\ + \ call void @flan_dev_reg_enable()\n\ + \ call void @flan_dev_crash_enable()\n\ + \ ret void\n\ + }\n" + ctor); + Buffer.add_string m.out + (Printf.sprintf + "@llvm.global_ctors = appending global [1 x { i32, ptr, ptr }] \ + [{ i32, ptr, ptr } { i32 65535, ptr %s, ptr null }]\n" ctor); Buffer.add_char m.out '\n' end; List.iter (emit_global m ~hidden) p.Tast.globals; diff --git a/lib/mangle.ml b/lib/mangle.ml index 81390aa..834f1a9 100644 --- a/lib/mangle.ml +++ b/lib/mangle.ml @@ -30,6 +30,16 @@ let prefix = "flan." and [.init-data] start with a dot no reader token can produce. *) 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 function that is currently this name's body. *) let cell n = prefix ^ "cell." ^ n diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh index 8a245f5..63e15cf 100755 --- a/spike/x86/survey.sh +++ b/spike/x86/survey.sh @@ -92,6 +92,31 @@ forever="dev-loop dev-watch dev-chatty agent-auto" # in the epilogue that every exit already went through. The five are in the # sweep now and they are five of the MATCHes. +# The ones whose whole point is a fault, and which therefore cannot be compared +# at this sweep's optimisation level. Both write through a bytes-view of a +# string literal, which is a store into .rodata: measured here, LLVM exits 0 +# having printed the unmodified literal and this backend exits 139, because the +# store is undefined and the optimiser deleted it on one side and there is no +# optimiser on the other. That is not a lowering disagreement. At -O0 the two +# agree exactly -- 139, no output, both backends -- and test_acceptance.ml's +# dies_segv rows pin precisely that, on both backends, which is the coverage +# 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. +# +# Excluded by name rather than by building these two at -O0 here, and the +# 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. +# +# One more thing about dev-segv, which is a reason to keep it out of the +# comparison rather than a reason for this list: it calls agent/start, so it +# leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks +# 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" + TIMEOUT=${TIMEOUT:-20} # Extra flags, given to *both* sides. SURVEY_FLAGS=--dev is the one that has a @@ -115,6 +140,7 @@ for src in "$corpus"/test/programs/*.flan "$corpus"/spike/x86/*.flan \ [ $want = 1 ] || continue fi case " $forever " in *" $name "*) skip+=("$name:runs-forever"); continue;; esac + case " $faults " in *" $name "*) skip+=("$name:faults-by-design"); continue;; esac # LLVM first. A program that does not compile at all, or has no main, is not # this backend's business -- the frontend refused it either way. diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml index b43cd72..2a4e481 100644 --- a/test/test_sanitize.ml +++ b/test/test_sanitize.ml @@ -118,6 +118,14 @@ let corpus = an output comparison does not. *) "programs/two-numbers.flan", []; "programs/bytes2.flan", []; + (* (bytes s) allocates a copy now rather than reinterpreting the string, + which is the one change in that lane this tool can see: the copy is a + block from an allocator, it is written through immediately, and the + last case takes its block from an arena that is then freed and + destroyed. A copy one byte short, or a write landing after the block, + is a heap overflow here and a correct-looking program everywhere + else. *) + "programs/bytes-copy.flan", []; "programs/cleanup.flan", []; "programs/conditions.flan", []; "programs/debug.flan", []; diff --git a/test/test_valgrind.ml b/test/test_valgrind.ml index 007c79c..724b879 100644 --- a/test/test_valgrind.ml +++ b/test/test_valgrind.ml @@ -198,6 +198,11 @@ let corpus = "programs/arena-value.flan", []; "programs/bounds.flan", [ "0" ]; "programs/bytes2.flan", []; + (* The same program [test_sanitize.ml] added, and here for the half that + one cannot answer: a copy whose tail was never written reads as a + perfectly addressable block to ASan and as an uninitialised value to + memcheck. *) + "programs/bytes-copy.flan", []; "programs/cleanup.flan", []; "programs/conditions.flan", []; "programs/debug.flan", [];