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.
