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.
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.
