`flan emit --x86` printed a three-line header and then nothing but .byte blobs. The information was all there and none of it was written down. Each run of bytes is now headed by the Flan form that produced it, with the position it was written at, indented by how deeply the form nests. The headings are queued rather than written, so a form that emits nothing does not leave its heading on the next form's bytes; atoms queue none at all, because a literal operand would otherwise steal the heading standing above the imul that consumes it. Above each function is a frame map, which is the half no disassembly recovers: every value in this backend lives in a frame temporary, so -0x20(%rbp) is the whole vocabulary of the listing and nothing says what it means. It is read out of what emit_fn already keeps, so it cannot drift. Beside it, where the arguments arrived and whether there is a hidden sret. And the bookkeeping is named where it appears -- the transfer guard, the bounds triple, the arithmetic guards, rep movsb, the dev indirection cell -- with each explained once in a legend at the top rather than at every site. Always on for `emit --x86`, which exists to be read, and never for a build, whose .s is a temp file handed to clang. spike/x86/annot.sh is the check that this costs no byte: emit both ways, assemble both, compare every section. 342 SAME / 0 DIFFER over the corpus in default, --dev and --debug. dump.sh now shows the annotated listing beside objdump's disassembly -- why beside what, which is the pairing that answers the mnemonics question. survey.sh has not been run on this; see the handoff.
234 lines
14 KiB
Markdown
234 lines
14 KiB
Markdown
# Handoff — `flan emit --x86` annotated, so its output can be read
|
|
|
|
Branch `dev-loop`, from `f772162`.
|
|
|
|
The x86 backend exists so that a dev build is ours end to end and so that a reader can be told *why* each
|
|
instruction is there. Until now `flan emit --x86` printed a three-line file header and then nothing but
|
|
`.byte` blobs: no source form, no frame key, no statement of the calling convention, nothing naming the
|
|
bookkeeping. Reading it meant `as` plus `objdump`, and even that answers only *what*.
|
|
|
|
**It is annotated now.** Every run of bytes is headed by the Flan form that produced it; every function
|
|
carries a frame map and a statement of how its arguments arrived; and every piece of bookkeeping the
|
|
compiler adds has a name where it appears and an explanation once, in a legend at the top of the file.
|
|
|
|
## What was built
|
|
|
|
| file | what |
|
|
|---|---|
|
|
| `lib/loc.ml` | `Loc.snippet` — the text of a span, on one line, whitespace collapsed, or `None` where there is no readable source. The squiggle's other half: the squiggle points at a form in its own file, this quotes it somewhere the file is not |
|
|
| `lib/x86.ml` | the annotation machinery: a queue of pending comments on `buf`, the per-form hook in `lower`, `frame_map`, the bookkeeping `note`s, and the legend |
|
|
| `bin/main.ml` | `emit --x86` annotates; `--no-annotate` is the bare spelling |
|
|
| `spike/x86/annot.sh` | **new** — emits every program in the corpus both ways, assembles both, and compares every section of the two objects byte for byte, in all three of default, `--dev` and `--debug` |
|
|
| `spike/x86/dump.sh` | its x86 section now shows the annotated listing *and* the disassembly of the object that listing assembles to — why beside what |
|
|
|
|
`lib/build.ml` was not touched. A `--x86` build emits exactly the assembly it emitted before.
|
|
|
|
## The two decisions
|
|
|
|
**Annotation is always on for `flan emit --x86` and always off for a `--x86` build.** `flan emit` exists to
|
|
be read by a person, and there is no reason to make a reader ask for the thing the command is for. A build's
|
|
`.s` is a temporary file handed straight to clang and read by nobody, so leaving it untouched costs nothing
|
|
and buys something: `survey.sh`'s 103 MATCH stays a statement about the same text it has always been about,
|
|
rather than about text this lane rewrote. `--no-annotate` exists for exactly one consumer, `annot.sh`.
|
|
|
|
**None of this belongs to the LLVM path.** `flan emit` already prints IR that names its values, carries
|
|
`!dbg` on every instruction and a `!DILocalVariable` per slot. The problem being fixed here is one this
|
|
backend has and LLVM does not.
|
|
|
|
## Mnemonics: not done, deliberately
|
|
|
|
The brief allowed a trailing mnemonic per line as a bonus and said not to write a disassembler for it. No
|
|
disassembler was written — but the honest reason is not that one would be needed. The encoder knows the
|
|
mnemonic at the moment it emits the bytes; threading a text trace through every one of its entry points,
|
|
with memory-operand formatting to match, is a larger change than the request and would touch every encoding
|
|
function in the file, which is the part of it the survey is a structural check on.
|
|
|
|
What replaces it is cheaper and arguably better: `dump.sh` now prints the annotated `.s` and `objdump`'s
|
|
disassembly of the same object side by side. The disassembly says what the instructions are; the listing
|
|
says why they exist. Neither answers the other's question, and having both is what the four-way comparison
|
|
was for.
|
|
|
|
## How the annotation is attached, and why that shape
|
|
|
|
The bytes accumulate in `buf.pend` and flush as one `.byte` directive. A comment therefore cannot simply be
|
|
written when a form starts lowering — the form may emit nothing, and a heading left standing would be read
|
|
as belonging to whatever came next.
|
|
|
|
So headings are **queued, not written**. `annote` puts one on `buf.ann` with a serial; the next byte written
|
|
flushes the pending directive and then the queue, so the comment lands immediately above the bytes it is
|
|
about; and `unannote` withdraws whatever a form queued and never spent. The serials are monotonic, so
|
|
"was mine written?" is one integer comparison against the highest serial ever written.
|
|
|
|
The hook is in `lower`, beside `dwline`, and for the same reason `dwline` is there: the recursion that
|
|
lowers a nested call also lowers its arguments, so a heading queued in `lower` spans exactly the bytes that
|
|
form and everything inside it emit. The margin moves with the nesting, so an argument's code steps in and
|
|
the call's steps back out and the shape of the expression is visible without reading a word.
|
|
|
|
**Atoms are not annotated**, and this is the single detail the acceptance test turns on. A literal, a local
|
|
or a global would steal its parent's heading: `(* n 2)` lowers as a load, a load and an `imul`, and if the
|
|
two operands each queued a heading of their own then the line standing above the `imul` would name the
|
|
literal `2`. Skipping them leaves `(* n 2)` queued until the first byte and spanning the whole run. Read the
|
|
sample below: the line above the `imul` is the one that had to be right.
|
|
|
|
A form the checker invented carries `Loc.unknown` and is not annotated either — there is no source text to
|
|
quote, and it inherits the heading of the form that contains it, which is where it really came from. A form
|
|
at the same position as the last heading written is skipped, which is what stops a macro from printing its
|
|
call site once per form of its expansion. A function whose source is not readable from here — the prelude —
|
|
gets its frame map, no form headings, and one line saying so, rather than a column of bare positions.
|
|
|
|
## The frame map
|
|
|
|
This is the half that matters most and the one no amount of disassembly recovers. LLVM's output names its
|
|
values; this backend's cannot, because every value it has is a bump-allocated frame temporary and a
|
|
temporary has no name. So `-0x20(%rbp)` is the whole vocabulary of the listing and the map is its key.
|
|
|
|
Everything in it is read out of state `emit_fn` already keeps — `f.slots` *is* what the prologue stores
|
|
through, `fn.snames` is what the source called each slot — so it cannot drift from the code it describes.
|
|
The boundary between named slots and temporaries is captured as `fixed` right after the fixed allocations
|
|
and before the body is lowered; `maxframe` would be the wrong number, because that is the high-water mark of
|
|
the temporaries rather than where they start.
|
|
|
|
What is deliberately *not* described is any individual temporary. `scoped` reclaims them and a later form
|
|
reuses the bytes, so naming an offset that holds something else half the time is worse than saying where the
|
|
region begins — the same call the DWARF above it makes about locals, and for the same reason.
|
|
|
|
## The bookkeeping, named
|
|
|
|
Five things the compiler adds that no form asked for, each named where it appears and explained once in the
|
|
file legend rather than at every site: the transfer guard after every call to Flan code, the bounds check and
|
|
its signalling slow path, the arithmetic guard and the float-to-integer range check, `rep movsb` for every
|
|
aggregate copy, and the indirection cell a `--dev` build calls through. The prologue, the epilogue, the
|
|
transfer exit and C's `main` carry a prose block each.
|
|
|
|
## A worked sample
|
|
|
|
`spike/x86/dump.sh small.flan twice`, on
|
|
|
|
```
|
|
(defn twice [n i64] i64
|
|
(* n 2))
|
|
```
|
|
|
|
LLVM at `-O2`:
|
|
|
|
```
|
|
flan.twice:
|
|
movq %rdi, -8(%rsp)
|
|
leaq (%rdi,%rdi), %rax
|
|
retq
|
|
```
|
|
|
|
and the same function out of this backend:
|
|
|
|
```
|
|
# ────────────────────────────────────────────────────────────────────
|
|
# "flan.twice" (defn twice [n i64] i64 small.flan:1:7
|
|
#
|
|
# Arguments: n from rdi.
|
|
# Returns i64 in rax.
|
|
# The transfer channel arrives last of all, from rsi. It is a pointer to the
|
|
# cell a callee writes its target into, and reading it is what every guard
|
|
# below does.
|
|
#
|
|
# The frame is 0x30 bytes below rbp. No call in it passes an argument on the
|
|
# stack.
|
|
#
|
|
# -0x8 n i64 parameter 1, from rdi
|
|
# -0x10 <chan> ptr the transfer channel this frame passes on
|
|
# -0x18 <ret> i64 the return value the epilogue loads
|
|
# Everything below -0x18 is a temporary. They are bump-allocated and
|
|
# reclaimed at the end of the form that made them, so a later form reuses
|
|
# the bytes and no one offset down there means one thing for long.
|
|
# ────────────────────────────────────────────────────────────────────
|
|
.globl "flan.twice"
|
|
.type "flan.twice", @function
|
|
"flan.twice":
|
|
# The prologue: save rbp, take the frame in one sub, and spill every incoming
|
|
# register into its slot. rsp is written here and by leave and nowhere else,
|
|
# so rsp % 16 == 0 at every call site below is a property of that one rounded
|
|
# sub rather than an invariant each case has to keep.
|
|
.byte 0x55,0x48,0x89,0xe5,0x48,0x81,0xec,0x30,...
|
|
# (* n 2) small.flan:2:3
|
|
.byte 0x48,0x8b,0x85,0xf8,0xff,0xff,0xff,0x48,0x89,0x85,0xe0,...
|
|
# The epilogue, and every return and every transfer out of this frame arrives
|
|
# here, so the frame is torn down once.
|
|
.Lret1048:
|
|
.byte 0x48,0x8b,0x85,0xe8,0xff,0xff,0xff,0xc9,0xc3
|
|
.size "flan.twice", . - "flan.twice"
|
|
```
|
|
|
|
Three LLVM instructions against thirteen, and the listing now says where the difference went: a real frame
|
|
rather than a red zone, because rsp is written twice per function and never at a call site; a transfer
|
|
channel parameter that LLVM's `-O2` dropped as dead and this backend spills because a dev build does not
|
|
optimise; and both operands of the multiply through frame temporaries at `-0x20` and `-0x28`, because every
|
|
intermediate in this backend is a frame temporary. None of that is visible in the disassembly and all of it
|
|
is visible here.
|
|
|
|
A denser one, from `bounds.flan` — the four instructions after every call, and the bounds triple:
|
|
|
|
```
|
|
# (at args 1) bounds.flan:11:35
|
|
.byte 0x48,0xb8,0x01,...
|
|
# The bounds check. One unsigned compare catches a negative index as
|
|
# well as an oversized one, and the not-taken branch is the whole of
|
|
# the fast path.
|
|
.byte 0x48,0x63,0x85,0xa4,...,0x48,0x39,0xc8,0x0f,0x82
|
|
.long .Linb1078 - . - 4
|
|
# Out of bounds: the location string, the operands, and this frame's
|
|
# channel, then flan_bounds_error, which signals
|
|
.byte 0x48,0x8d,0x3d
|
|
.long .Lk1079 - . - 4
|
|
...
|
|
call flan_bounds_error
|
|
# The transfer guard, after every call to Flan code: load this
|
|
# frame's channel, load through it, test, and branch if it is set —
|
|
# a callee that transferred left a target there and the value in rax
|
|
# means nothing.
|
|
.byte 0x4c,0x8b,0x9d,0xd0,...,0x0f,0x85
|
|
.long .Lxfer1077 - . - 4
|
|
# ud2, where emit.ml writes unreachable. Nothing answered the signal,
|
|
# so the runtime already died inside that call and nothing falls
|
|
# through to here.
|
|
.byte 0x0f,0x0b
|
|
```
|
|
|
|
## Verification
|
|
|
|
**Byte identity — `spike/x86/annot.sh`, 342 SAME / 0 DIFFER, measured on this code.** Every program in `test/programs` and in
|
|
`spike/x86`, emitted both ways, assembled both ways, and every section of the two objects compared byte for
|
|
byte — in the default build, in `--dev`, and in `--debug`. The `--debug` case is the sharp one: a
|
|
`.debug_line` row is an address expressed as a label, and annotation issues no labels and consumes no
|
|
`uniq`, precisely so that those cannot move. The 84 SKIPs are programs that do not compile at all — the
|
|
reject corpus and the generic-milestone ones — and are the same set the survey skips.
|
|
|
|
**`dune test --root .` — 232 checks, 0 failures**, run against this code. `dune build @page` and
|
|
`dune build @cells` both exit 0; `@cells` reports `x86 --dev: 22 22` and `x86 : 42 42`, which is the check
|
|
that the indirection cells and the ABI marker still come out where they were.
|
|
|
|
**`spike/x86/survey.sh` has NOT been run on this work.** Two runs were started and both were invalidated by
|
|
racing with a `dune build` that replaced `bin/main.exe` underneath them; a third was killed on instruction
|
|
before it finished. **Whoever picks this up must not assume the 103 MATCH / 0 DIFFER / 0 REFUSED baseline
|
|
still holds — it is the one check that matters and it is outstanding.** Run it detached and with the
|
|
compiler pinned, so it cannot race a rebuild:
|
|
|
|
```
|
|
FLAN=_build/default/bin/main.exe setsid timeout 2400 spike/x86/survey.sh > log 2>&1 </dev/null
|
|
```
|
|
|
|
What makes an unwelcome result unlikely rather than impossible: the survey builds through `flan build --x86`,
|
|
which passes `annotate = false`, so the assembly it compiles is produced by the same code path as before with
|
|
one field added to a record and two branches that are never taken. The edits that *could* reach it are the
|
|
ones to `buf` — `flush` now writes `b.ind`, which is `""` in a build, and `u8`/`dir`/`text`/`lbl` now test
|
|
`b.ann`, which is empty in a build. `annot.sh` proves those are inert for the object at 342 SAME across the
|
|
corpus in all three of default, `--dev` and `--debug`, but it proves it about the *assembly*, and only the
|
|
survey proves it about the programs.
|
|
|
|
## What is not here
|
|
|
|
- No mnemonics, for the reason above.
|
|
- No annotation of an individual temporary, for the reason above.
|
|
- The redefinition emitter (`X86.redefinition`) builds its install stub with annotation off. It is generated
|
|
code with no Flan form behind it and a frame map of two slots; the legend would be longer than the
|
|
function. If the reload path ever wants a readable listing, the `ann` field on its context is the one
|
|
line to change.
|