The spike counted nodes it could do. This counts nodes a real input
actually contains, after Reach prunes, which is the question that decides
whether whole-program coverage is reachable.
The answer is worse than the spike's four buckets suggested: enum-compare
needs Str, Make, Field and Call before it prints anything, because the
prelude builds a slice to print one. And loops.flan carries Handled,
RestartCase and Signal one each -- conditions are not an advanced feature
to defer, they are in the reachable set of a program that only loops.
The same three shapes written in C and as first-class IR aggregates,
compiled by the same clang. { i8, i64 } agrees. { i8, float } does not: C
packs both halves into rax, the IR form answers in al and xmm0. And a
24-byte struct does not agree at all -- C spills through an sret pointer,
the IR form returns it in rax, rdx and rcx, and rcx is a register SysV never
uses for a return value.
That resolves the ret-big anomaly the first pass noted and moved past, and
it makes the finding stronger than it was written: the internal convention
is not the C ABI, not only undocumented in the emitted IR.
spike_call0 deleted with it -- declared, never bound, and the two unused
probes were removed for the same reason.
The verdict, as DISCUSS.md item 15. One function goes from Tast to machine
code and answers correctly, so the question is not whether it can be done.
Three findings decide the shape. Layout is already owned -- emit.ml computes
C struct layout for DWARF and is tested against LLVM's own answer -- so the
silent-drift risk item 10 feared most does not arise. The C boundary is the
easy half, because check.ml already rejects aggregates in a declare and the
shim flattens them. And the hard half was not on anyone's list: Flan calling
Flan passes aggregates by value, and LLVM's lowering of a first-class struct
is per-field rather than the C psABI -- { i8, float } comes back in al and
xmm0 where C would pack it into rax, and a %vec return takes a hidden sret
pointer that does not appear in the define line. The internal convention is
an implementation, not a document.
The audit stands on its own: overflow, shifts and evaluation order are
defined; division by zero, INT64_MIN/-1, the float cast, Uninit and
unreachable are not. Uninit is the one that bites, because poison is where
the two backends are supposed to differ.
Unloading: the shadow stack answers the running half and every dev-build
function is on it -- only the slot table is gated, not the frame. It cannot
answer the pointed-into half, which BUILT.md says is the actual reason
nothing is dlclose'd. Escaped function values need a rule the language does
not have.
SPIKE_DISASM=1 objdumps the exact buffers that ran. Kept behind a flag and
kept out of the pass/fail path: a disassembly that reads correctly beside a
function answering the wrong number is the normal outcome of hand-encoding.
Every stack movement now goes through pushv/popv and increments a depth
word on the function context. A call pads to 16 from wherever the expression
evaluator has left rsp, and asserts the parity before it emits the call.
The nested probe passes.
The stack-argument path is folded into the same counter rather than keeping
its own, because two independent notions of parity is how the bug comes back.
Three synthetic Tast functions calling C: eight integers so two go on the
stack, and a callee that does a 16-byte aligned spill and answers -1 if it
was entered with rsp misaligned. The third calls it from inside a binary
operator.
The third fails. Alignment at a call site is not a property of the prologue
-- it is a property of how much the expression evaluator has pushed, and
the evaluator spills the left operand across the right one's evaluation. A
call in that right operand runs 8 bytes off. Nothing in the arithmetic tests
could see it, because they call nothing that spills a vector register.
This is the raylib failure mode exactly, and it is left red for one commit
so the record shows the probe found it rather than agreeing with the code.
x86.ml is an instruction selector for the part of Tast that fits in one
integer register: literals, slots, let, if, arithmetic, comparison, and a
call. Everything else raises with the node that defeated it, because an
honest refusal is the measurement and a silently wrong answer would waste
the exercise.
The frontend is the real one -- Reader, Parse, Load, Check -- so what is
lowered is the same Tast.fn the LLVM backend gets. Seven arithmetic results
are compared against what the language says they should be; the disassembly
proves nothing and is not the evidence.
Nothing is wired into the build. No dune file under spike/, driven by hand
with ocamlfind and clang as spike/embed already does.
The first six probes each proved a piece. merged.sh puts them together: the
program's @main is renamed out of the way, a C main takes the main thread and
runs it there, caml_startup happens on a thread beside it, and clang links the
lot -- the emitted program object, flan_rt.c, flan_dev.c, flan_agent.c and the
whole compiler as one -output-complete-obj. It runs, and the compiler inside it
compiles the very source the program was built from.
Nothing is wired up. The two halves share an address space and do not speak.
That is the point: the question was whether they can, not what they would say.
sig.sh and symbols.sh answer the two questions the first pass got wrong or
skipped. The SIGSEGV reading in harness5.c was taken at the wrong moment --
OCaml 5 starts domains after caml_startup returns, so the disposition had to be
read from inside the runtime, and against a plain ocamlopt executable as a
control. symbols.sh is the hazard nobody looks for until the link fails: four
.c files that are compiled into two different processes today, and the OCaml
runtime, all landing in one link.
Item 12 asks five questions and says to answer them with a spike rather than a
rewrite. spike/embed/ is that spike: one script, six binaries, each one built to
fail loudly at the thing it is asking about. It is deliberately not a dune
target -- the root dune only excludes old-ocaml/, so a dune file here would land
in @default and make the spike part of the build. It drives ocamlfind and clang
by hand against the flan.cmxa dune already produces.
The probes, in the order they would kill the idea: the smallest possible link, a
C main() reaching one OCaml function; the whole compiler linked in and doing
real work; the same again with lib/dynload_stubs.c from the unmerged dlopen
branch, because that is the only C the compiler itself is built from; the game
keeping the main thread while caml_startup happens on a pthread beside it; the
SIGSEGV disposition read on both sides of caml_startup; and an 8 MiB arena
checked byte for byte across a compaction.
No result is written down yet. This is the apparatus.
