Merge branch 'worktree-agent-ae9bc74da338fa214' into dev-loop
This commit is contained in:
commit
45c5b43021
18
bin/main.ml
18
bin/main.ml
@ -123,9 +123,16 @@ let two_process_flag = "--two-process"
|
||||
compiled. *)
|
||||
let x86_flag = "--x86"
|
||||
|
||||
(* [flan emit --x86] annotates, because it exists to be read. This turns that
|
||||
off, and the only caller who wants it is the test that assembles the listing
|
||||
both ways and compares the object's sections byte for byte -- a claim that
|
||||
comments and the splitting of a [.byte] directive are invisible to the
|
||||
assembler is worth measuring rather than asserting. *)
|
||||
let no_annotate_flag = "--no-annotate"
|
||||
|
||||
let flags =
|
||||
[ no_checks_flag; dev_flag; debug_flag; sanitize_flag; two_process_flag;
|
||||
x86_flag ]
|
||||
x86_flag; no_annotate_flag ]
|
||||
|
||||
(* [--target=wasm32-wasi] and [--target=web], the two cross targets. Unlike
|
||||
the flags above, a target
|
||||
@ -441,13 +448,20 @@ let () =
|
||||
let checks = not (List.mem no_checks_flag args) in
|
||||
let dev = List.mem dev_flag args in
|
||||
let debug = List.mem debug_flag args in
|
||||
(* The listing is annotated because a listing is what this command is for:
|
||||
a person asked to see what their program compiles to, and a wall of
|
||||
[.byte] with nothing saying which form produced which run answers the
|
||||
letter of that and not the question. --no-annotate is here for the one
|
||||
consumer that wants the bare spelling, which is the check that says
|
||||
annotation changed no byte of the object. *)
|
||||
let annotate = not (List.mem no_annotate_flag args) in
|
||||
let files = List.filter (fun a -> not (is_flag a)) args in
|
||||
List.iter
|
||||
(fun path ->
|
||||
with_errors path (fun () ->
|
||||
load path |> fun l ->
|
||||
Flan.Check.program_all l.decls
|
||||
|> Flan.X86.program ~checks ~dev ~debug
|
||||
|> Flan.X86.program ~checks ~dev ~debug ~annotate
|
||||
|> print_string))
|
||||
files
|
||||
| _ :: "emit" :: args when List.exists (fun a -> not (is_flag a)) args ->
|
||||
|
||||
233
docs/handoffs/HANDOFF-x86-annotate.md
Normal file
233
docs/handoffs/HANDOFF-x86-annotate.md
Normal file
@ -0,0 +1,233 @@
|
||||
# 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.
|
||||
44
lib/loc.ml
44
lib/loc.ml
@ -284,6 +284,50 @@ let squiggle ?(mark = '^') (t : t) =
|
||||
(Printf.sprintf " %*d | %s\n %*s | %s%s" g t.line text g ""
|
||||
(Buffer.contents pad) bar)
|
||||
|
||||
(** The text of the span itself, on one line, or [None] when there is no source
|
||||
to show it from.
|
||||
|
||||
This is the squiggle's other half: the squiggle points at a form in its own
|
||||
file, and this quotes the form somewhere the file is not — the x86
|
||||
backend's listing, where a comment has to say which form a run of bytes
|
||||
came from and the reader is looking at an assembly file rather than at the
|
||||
Flan. A form written across several lines is cut at the end of its first
|
||||
line with an ellipsis rather than wrapped, because the consumer is a
|
||||
one-line comment; runs of whitespace collapse for the same reason, which is
|
||||
what keeps an indented form from arriving as a column of blanks.
|
||||
|
||||
A zero-width span — a location the checker invented a form for, or one an
|
||||
older reader never widened — has no end to slice to, so the rest of the
|
||||
line is quoted. That is the best answer available and it is usually the
|
||||
right one: the form the location names generally runs to the end of it. *)
|
||||
let snippet ?(lim = 64) (t : t) =
|
||||
match source_line t with
|
||||
| None -> None
|
||||
| Some text ->
|
||||
let n = String.length text in
|
||||
let start = max 0 (min (t.col - 1) n) in
|
||||
let stop =
|
||||
if t.eline > t.line || t.ecol <= t.col then n else min n (t.ecol - 1)
|
||||
in
|
||||
let raw = if stop > start then String.sub text start (stop - start) else "" in
|
||||
(* One space for any run of blanks, and nothing on either end. *)
|
||||
let b = Buffer.create (String.length raw) in
|
||||
let sp = ref false in
|
||||
String.iter
|
||||
(fun c ->
|
||||
if c = ' ' || c = '\t' || c = '\r' then sp := true
|
||||
else begin
|
||||
if !sp && Buffer.length b > 0 then Buffer.add_char b ' ';
|
||||
sp := false;
|
||||
Buffer.add_char b c
|
||||
end)
|
||||
raw;
|
||||
let s = Buffer.contents b in
|
||||
if s = "" then None
|
||||
else if String.length s > lim then Some (String.sub s 0 (max 1 (lim - 1)) ^ "…")
|
||||
else if t.eline > t.line then Some (s ^ " …")
|
||||
else Some s
|
||||
|
||||
let entry ?(mark = '^') ?(label = "") (t : t) msg =
|
||||
let head = Printf.sprintf "%s: %s%s" (to_string t) label msg in
|
||||
match squiggle ~mark t with
|
||||
|
||||
532
lib/x86.ml
532
lib/x86.ml
@ -93,20 +93,65 @@ let unsupported fmt = Printf.ksprintf (fun s -> raise (Unsupported s)) fmt
|
||||
(* Raw bytes accumulate in [pend] and are flushed as one [.byte] directive;
|
||||
anything the assembler has to resolve goes out as a directive with a known
|
||||
size, so [n] is the exact offset of the next byte either way. *)
|
||||
type buf = { out : Buffer.t; mutable pend : int list; mutable n : int }
|
||||
type buf = {
|
||||
out : Buffer.t;
|
||||
mutable pend : int list;
|
||||
mutable n : int;
|
||||
(* ── Annotation ──
|
||||
A comment waiting for the bytes it is about, newest last, each with the
|
||||
serial that says who queued it. Nothing here reaches the object: the
|
||||
assembler discards a comment, and splitting one [.byte] directive into
|
||||
two is the same bytes in the same order. What it buys is a listing whose
|
||||
runs of machine code are each headed by the Flan form that produced them.
|
||||
|
||||
let create () = { out = Buffer.create 4096; pend = []; n = 0 }
|
||||
Queued rather than written, because the point of the comment is to sit
|
||||
above bytes and a form that emits none must not leave its heading on the
|
||||
next form's. So [annote] queues, the first byte written afterwards flushes
|
||||
the queue, and [unannote] withdraws whatever its own form queued and never
|
||||
spent. *)
|
||||
mutable ann : (int * string) list;
|
||||
(* How far to indent a run of bytes, which is the nesting depth of the form
|
||||
that is emitting it. An argument's bytes step in and the call's step back
|
||||
out, so the shape of the expression is visible in the left margin without
|
||||
reading a single comment. *)
|
||||
mutable ind : string;
|
||||
}
|
||||
|
||||
let create () =
|
||||
{ out = Buffer.create 4096; pend = []; n = 0; ann = []; ind = "" }
|
||||
|
||||
let flush b =
|
||||
if b.pend <> [] then begin
|
||||
Buffer.add_string b.out "\t.byte ";
|
||||
Buffer.add_string b.out ("\t" ^ b.ind ^ ".byte ");
|
||||
Buffer.add_string b.out
|
||||
(String.concat "," (List.rev_map (Printf.sprintf "0x%02x") b.pend));
|
||||
Buffer.add_char b.out '\n';
|
||||
b.pend <- []
|
||||
end
|
||||
|
||||
(* The serial of the highest-numbered comment that has actually been written.
|
||||
[unannote] compares against it to tell "my heading is still waiting and
|
||||
should be withdrawn" from "my heading was spent on bytes I emitted". Module
|
||||
scope because the serials are, and they are because a function's prologue
|
||||
and its body are two buffers. *)
|
||||
let annser = ref 0
|
||||
let annmax = ref 0
|
||||
|
||||
(* Bytes are about to be written, so anything queued is about them. *)
|
||||
let ann_due b =
|
||||
if b.ann <> [] then begin
|
||||
flush b;
|
||||
List.iter
|
||||
(fun (s, line) ->
|
||||
Buffer.add_string b.out line;
|
||||
Buffer.add_char b.out '\n';
|
||||
if s > !annmax then annmax := s)
|
||||
b.ann;
|
||||
b.ann <- []
|
||||
end
|
||||
|
||||
let u8 b x =
|
||||
if b.ann <> [] then ann_due b;
|
||||
b.pend <- (x land 0xff) :: b.pend;
|
||||
b.n <- b.n + 1
|
||||
|
||||
@ -122,13 +167,38 @@ let u64 b (n : int64) =
|
||||
(Int64.to_int (Int64.logand (Int64.shift_right_logical n (i * 8)) 0xffL))
|
||||
done
|
||||
|
||||
(* A relocation, a label and raw text all count as "bytes about to be written"
|
||||
for the queue's purpose: each is part of the run its form produced, and a
|
||||
heading has to arrive before the label its form's code begins at. *)
|
||||
let dir b s size =
|
||||
ann_due b;
|
||||
flush b;
|
||||
Buffer.add_string b.out ("\t" ^ s ^ "\n");
|
||||
Buffer.add_string b.out ("\t" ^ b.ind ^ s ^ "\n");
|
||||
b.n <- b.n + size
|
||||
|
||||
let text b s = flush b; Buffer.add_string b.out s
|
||||
let lbl b l = flush b; Buffer.add_string b.out (l ^ ":\n")
|
||||
let text b s = ann_due b; flush b; Buffer.add_string b.out s
|
||||
let lbl b l = ann_due b; flush b; Buffer.add_string b.out (l ^ ":\n")
|
||||
|
||||
(* The margin a run of bytes is written at. Changing it flushes, because
|
||||
[flush] writes the margin as it stands when the line is written and the
|
||||
bytes pending at that moment were accumulated under the old one — without
|
||||
this, the tail of an outer form comes out at the indentation its last
|
||||
argument had. *)
|
||||
let set_ind b s = if b.ind <> s then begin flush b; b.ind <- s end
|
||||
|
||||
(* Queue one comment line. [pre] is written as given — the callers below spell
|
||||
their own leading tab and hash — and the serial comes back so that the form
|
||||
that queued it can withdraw it if it turns out to have emitted nothing. *)
|
||||
let annote b line =
|
||||
incr annser;
|
||||
b.ann <- b.ann @ [ (!annser, line) ];
|
||||
!annser
|
||||
|
||||
(* Drop every heading queued at or after [s] and still unspent. Answers whether
|
||||
[s] itself was spent, which is the only thing a caller wants to know. *)
|
||||
let unannote b s =
|
||||
if b.ann <> [] then b.ann <- List.filter (fun (k, _) -> k < s) b.ann;
|
||||
!annmax >= s
|
||||
|
||||
(* ── Registers ───────────────────────────────────────────────────────── *)
|
||||
|
||||
@ -144,6 +214,14 @@ let int_args = [| rdi; rsi; rdx; rcx; r8; r9 |]
|
||||
let n_int_args = 6
|
||||
let n_sse_args = 8
|
||||
|
||||
(* For the listing only — nothing encodes through this. In the same order the
|
||||
numbering above is in, which is the modrm one and not the alphabetical one a
|
||||
reader might expect. *)
|
||||
let rname = [| "rax"; "rcx"; "rdx"; "rbx"; "rsp"; "rbp"; "rsi"; "rdi";
|
||||
"r8"; "r9"; "r10"; "r11"; "r12"; "r13"; "r14"; "r15" |]
|
||||
|
||||
let regname r = if r >= 0 && r < 16 then rname.(r) else Printf.sprintf "r?%d" r
|
||||
|
||||
(* REX. [force] is for the 8-bit forms, where without a REX byte registers 4-7
|
||||
name ah/ch/dh/bh rather than spl/bpl/sil/dil — a store of a bool from rsi
|
||||
would otherwise write the wrong half of rdx. *)
|
||||
@ -573,6 +651,18 @@ type fnctx = {
|
||||
and does nothing — so a release build's output is byte-identical to what
|
||||
it was before debug information existed. *)
|
||||
dw : dwarf option;
|
||||
(* True when this listing is meant to be read by a person rather than handed
|
||||
to clang — see [program]'s [annotate]. Every annotation in this file is
|
||||
behind it, so that a build's assembly is character-for-character what it
|
||||
was before any of this existed and [survey.sh] goes on comparing the same
|
||||
text it always compared. *)
|
||||
ann : bool;
|
||||
(* How deeply nested the form being lowered is, which is what the left margin
|
||||
of the listing shows. *)
|
||||
mutable adepth : int;
|
||||
(* The last heading written, so that a macro that expands to forty forms at
|
||||
one call site does not print that call site forty times. *)
|
||||
mutable alast : string;
|
||||
}
|
||||
|
||||
(* Module-wide rather than per-function. Two functions each holding an [if]
|
||||
@ -614,6 +704,113 @@ let dwline f (loc : Loc.t) =
|
||||
{ rlbl = l; rfile = file; rline = line; rcol = col } :: s.srows
|
||||
end)
|
||||
|
||||
(* ── Annotation ──────────────────────────────────────────────────────── *)
|
||||
|
||||
(* Everything below writes comments and nothing else, and all of it is behind
|
||||
[f.ann]. The reason it is worth the code is the one the frame model makes
|
||||
unavoidable: every intermediate value in this backend lives in a frame
|
||||
temporary, so a listing is a wall of [-0x48(%rbp)] and there is no way to
|
||||
tell which of those is the loop counter and which is where the left operand
|
||||
of an [imul] was parked. LLVM's output names its values and this file's
|
||||
cannot, so the names have to be written down beside it instead.
|
||||
|
||||
A comment costs nothing in the object — the assembler discards it — so what
|
||||
it buys is paid for entirely in the size of the [.s], which nothing but a
|
||||
reader ever looks at. *)
|
||||
|
||||
(* One bookkeeping line: something the compiler put there that no form in the
|
||||
source asked for, named once so that a reader who meets it again recognises
|
||||
it. The post-call guard and the bounds-check triple are the two that matter
|
||||
most, because they are the two a reader counts instructions in and wonders
|
||||
about. *)
|
||||
(* Wrapped rather than written as given, and whitespace collapsed on the way:
|
||||
the callers below spell their text across several source lines, and an
|
||||
assembly comment that runs to two hundred columns is one nobody reads. *)
|
||||
let wrap ~pre ~width s =
|
||||
let words =
|
||||
List.filter (fun w -> w <> "")
|
||||
(String.split_on_char ' '
|
||||
(String.map (fun c -> if c = '\n' || c = '\t' then ' ' else c) s))
|
||||
in
|
||||
let lines = ref [] and cur = Buffer.create 80 in
|
||||
let emit () =
|
||||
if Buffer.length cur > 0 then begin
|
||||
lines := (pre ^ Buffer.contents cur) :: !lines;
|
||||
Buffer.clear cur
|
||||
end
|
||||
in
|
||||
List.iter
|
||||
(fun w ->
|
||||
if Buffer.length cur > 0
|
||||
&& String.length pre + Buffer.length cur + 1 + String.length w > width
|
||||
then emit ();
|
||||
if Buffer.length cur > 0 then Buffer.add_char cur ' ';
|
||||
Buffer.add_string cur w)
|
||||
words;
|
||||
emit ();
|
||||
List.rev !lines
|
||||
|
||||
let note f s =
|
||||
if f.ann then
|
||||
List.iter
|
||||
(fun l -> ignore (annote f.b l))
|
||||
(wrap ~pre:(Printf.sprintf "\t%s# " f.b.ind) ~width:78 s)
|
||||
|
||||
(* The same, on a buffer rather than a function context: the prologue is built
|
||||
into its own buffer before [f.b] is finished with. *)
|
||||
let bnote ann b s =
|
||||
if ann then
|
||||
List.iter (fun l -> ignore (annote b l)) (wrap ~pre:"\t# " ~width:78 s)
|
||||
|
||||
(* The heading for one Flan form, queued against whatever bytes it goes on to
|
||||
emit. Three things are deliberately not annotated.
|
||||
|
||||
A form the checker invented carries [Loc.unknown], and there is no source
|
||||
text to quote for it; it inherits the heading of the form that contains it,
|
||||
which is where it came from and therefore the true answer.
|
||||
|
||||
An atom — a literal, a local, a global — is skipped because annotating it
|
||||
would steal its parent's heading. A multiply of a local by a literal lowers
|
||||
as a load, a load and an [imul]: if the two operands each queued a heading
|
||||
of their own, the heading standing above the [imul] would name the literal,
|
||||
and the one line a reader of this file most wants to be right would be
|
||||
wrong. Skipping the atoms leaves the multiply queued until the first byte
|
||||
and spanning the whole run, which is the answer.
|
||||
|
||||
And a form at the same source position as the last heading written is
|
||||
skipped, which is what keeps a macro from printing its call site once per
|
||||
form of its expansion. *)
|
||||
let atomic (e : Tast.expr) =
|
||||
match e.Tast.e with
|
||||
| Tast.Int _ | Tast.Bool _ | Tast.Float _ | Tast.Str _ | Tast.Unit
|
||||
| Tast.Zero _ | Tast.None_ | Tast.Uninit _ | Tast.Local _ | Tast.Global _
|
||||
| Tast.FnAddr _ -> true
|
||||
| _ -> false
|
||||
|
||||
let annot f (e : Tast.expr) =
|
||||
if (not f.ann) || atomic e || e.Tast.loc.Loc.line = 0 then None
|
||||
else
|
||||
let loc = e.Tast.loc in
|
||||
let where = Printf.sprintf "%s:%d:%d" (Filename.basename loc.Loc.file)
|
||||
loc.Loc.line loc.Loc.col in
|
||||
match Loc.snippet loc with
|
||||
| None -> None
|
||||
| Some src ->
|
||||
let src =
|
||||
match loc.Loc.macro with
|
||||
| Some m -> Printf.sprintf "%s [from the macro %s]" src m
|
||||
| None -> src
|
||||
in
|
||||
let key = where ^ " " ^ src in
|
||||
if key = f.alast then None
|
||||
else begin
|
||||
f.alast <- key;
|
||||
set_ind f.b (String.make (2 * min 12 f.adepth) ' ');
|
||||
let head = Printf.sprintf "\t%s# %s" f.b.ind src in
|
||||
let pad = max 1 (62 - String.length head) in
|
||||
Some (annote f.b (head ^ String.make pad ' ' ^ where))
|
||||
end
|
||||
|
||||
(* Bump-allocate a frame temporary and answer its rbp-relative offset. The
|
||||
offset is negative, so the running total is rounded *up* to the alignment;
|
||||
rbp is 16-aligned, so that is the alignment the value actually gets. *)
|
||||
@ -668,6 +865,9 @@ let store_scalar_at f ~reg ~base ~disp (t : Types.t) =
|
||||
(* n bytes from the address in rsi to the address in rdi. *)
|
||||
let blockcopy f n =
|
||||
if n > 0 then begin
|
||||
note f (Printf.sprintf
|
||||
"rep movsb: %d bytes from rsi to rdi. An aggregate is copied rather than \
|
||||
aliased — spec-memory.md's assignment rule" n);
|
||||
movabs f.b ~dst:rcx (Int64.of_int n);
|
||||
rep_movsb f.b
|
||||
end
|
||||
@ -681,6 +881,8 @@ let copy_frames f ~dst ~src n =
|
||||
|
||||
let zero_frame f ~dst n =
|
||||
if n > 0 then begin
|
||||
note f (Printf.sprintf "rep stosb: %d bytes of zero, which is what this backend \
|
||||
spells a zero value as" n);
|
||||
lea f.b ~dst:rdi ~mm:(Frame dst);
|
||||
xor_rr f.b ~dst:rax ~src:rax;
|
||||
movabs f.b ~dst:rcx (Int64.of_int n);
|
||||
@ -1016,6 +1218,10 @@ let current_pad f =
|
||||
nothing a guard there could find. The exceptions are the runtime entry
|
||||
points that take the channel themselves and signal through it. *)
|
||||
let guard f =
|
||||
note f
|
||||
"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.";
|
||||
xfer_load f ~reg:r11;
|
||||
test_rr f.b ~a:r11 ~c:r11;
|
||||
jcc_lbl f.b ~cc:cc_ne (current_pad f)
|
||||
@ -1158,7 +1364,27 @@ let rec lower f (e : Tast.expr) (dst : loc) : unit =
|
||||
scoped f (fun () ->
|
||||
let o = tmp f e.Tast.ty in
|
||||
lower f e (Lf o))
|
||||
else lower_at f e dst
|
||||
else if not f.ann then lower_at f e dst
|
||||
else begin
|
||||
(* The second hook, and it hangs off the same recursion for the same
|
||||
reason: a heading queued here spans exactly the bytes this form and
|
||||
everything inside it emit, so the listing nests the way the source
|
||||
does. Withdrawn again if the form emitted nothing — a [defer] that is
|
||||
hoisted, a [Unit] in statement position — because a heading left
|
||||
standing would be read as belonging to whatever came next. *)
|
||||
let prev = f.alast in
|
||||
(* Captured before [annot], which moves the margin as a side effect of
|
||||
queueing a heading: restoring what it moved is the point. *)
|
||||
let d = f.adepth and ind = f.b.ind in
|
||||
let s = annot f e in
|
||||
f.adepth <- d + 1;
|
||||
lower_at f e dst;
|
||||
f.adepth <- d;
|
||||
set_ind f.b ind;
|
||||
match s with
|
||||
| Some s -> if not (unannote f.b s) then f.alast <- prev
|
||||
| None -> ()
|
||||
end
|
||||
|
||||
and lower_at f (e : Tast.expr) (dst : loc) : unit =
|
||||
let t = e.Tast.ty in
|
||||
@ -1866,6 +2092,9 @@ and elements f (base : loc) (ty : Types.t) (is : Tast.expr list) : loc =
|
||||
does, because it leaves through the innermost pad; an unanswered one still
|
||||
does not, because it is a die inside C. Identical on both backends. *)
|
||||
and bounds_call f sym (loc : Loc.t) (extra : int list) =
|
||||
note f (Printf.sprintf
|
||||
"Out of bounds: the location string, the operands, and this frame's channel, \
|
||||
then %s, which signals" sym);
|
||||
let s = Loc.to_string loc in
|
||||
str_args f ~preg:rdi ~nreg:rsi s;
|
||||
let regs = [| rdx; rcx; r8; r9 |] in
|
||||
@ -1877,6 +2106,9 @@ and bounds_call f sym (loc : Loc.t) (extra : int list) =
|
||||
xor_rr f.b ~dst:rax ~src:rax;
|
||||
call_sym f.b sym;
|
||||
guard f;
|
||||
note f
|
||||
"ud2, where emit.ml writes unreachable. Nothing answered the signal, so the runtime \
|
||||
already died inside that call and nothing falls through to here.";
|
||||
ud2 f.b
|
||||
|
||||
(* The length an index is checked against, or [None] for the forms [emit.ml]
|
||||
@ -1900,6 +2132,9 @@ and check_at f (base : loc) (ty : Types.t) (i : Tast.expr) (iv : loc) =
|
||||
| None -> ()
|
||||
| Some len ->
|
||||
scoped f (fun () ->
|
||||
note f
|
||||
"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.";
|
||||
let a = ptmp f and b = ptmp f in
|
||||
load_loc f ~reg:rax iv i.Tast.ty;
|
||||
store_int f.b ~src:rax ~mm:(Frame a) ~size:8;
|
||||
@ -1992,6 +2227,13 @@ and check_div f (loc : Loc.t) ~is_rem (k : Types.ikind) ~lit =
|
||||
in
|
||||
if need_zero || need_ovf then
|
||||
scoped f (fun () ->
|
||||
note f
|
||||
(Printf.sprintf
|
||||
"The arithmetic guard: %s%s%s, and the failure path signals through \
|
||||
flan_arith_fail"
|
||||
(if need_zero then "a zero divisor" else "")
|
||||
(if need_zero && need_ovf then " and " else "")
|
||||
(if need_ovf then "the one overflowing division" else ""));
|
||||
let so = ptmp f and sa = ptmp f and sb = ptmp f in
|
||||
store_int f.b ~src:rax ~mm:(Frame sa) ~size:8;
|
||||
store_int f.b ~src:rcx ~mm:(Frame sb) ~size:8;
|
||||
@ -2044,6 +2286,9 @@ and check_div f (loc : Loc.t) ~is_rem (k : Types.ikind) ~lit =
|
||||
undefined as 1e300 is and has no business walking through the guard. *)
|
||||
and check_cast f (loc : Loc.t) (src : Types.fkind) (k : Types.ikind) =
|
||||
if f.md.Emit.checks then begin
|
||||
note f
|
||||
"The range check on a float-to-integer cast. Two compares, written in the \
|
||||
directions that make a NaN fail both of them.";
|
||||
let f64 = (src = Types.F64) in
|
||||
let n = Types.bits k in
|
||||
let signed = Types.signed k in
|
||||
@ -2154,6 +2399,10 @@ and call_flan f ~target ~args ~rty dst =
|
||||
(match callee with
|
||||
| `Sym s -> call_sym f.b s
|
||||
| `Cell s ->
|
||||
note f
|
||||
"The indirection cell. A dev build calls through it rather than to the symbol, so \
|
||||
that a redefinition installed while the process runs is reached by the next \
|
||||
call.";
|
||||
load_sym f ~dst:r11 s;
|
||||
call_r f.b r11
|
||||
| `Loc o ->
|
||||
@ -2586,8 +2835,157 @@ let incoming_of ~sret (params : Types.t list) =
|
||||
in
|
||||
sret_at, ps, next_int ()
|
||||
|
||||
(* ── The frame map ───────────────────────────────────────────────────── *)
|
||||
|
||||
(* What a listing out of this backend needs most, and the one thing no amount
|
||||
of disassembly recovers. LLVM's output names its values; this file's names
|
||||
nothing, because every value it has lives in a frame temporary and a
|
||||
temporary has no name to print. So the key goes above the function: which
|
||||
displacement is which parameter, which is which named local, where the
|
||||
compiler's own three live, and where the nameless temporaries begin.
|
||||
|
||||
Everything here is read out of state [emit_fn] already keeps. Nothing is
|
||||
recomputed and nothing is guessed, which is why this cannot drift from the
|
||||
code it describes: [f.slots] *is* what the prologue stores through.
|
||||
|
||||
The one thing deliberately not described is any individual temporary.
|
||||
[scoped] reclaims them and a later statement reuses the bytes, so naming an
|
||||
offset that holds something else half the time is worse than saying where
|
||||
the region starts — which is the same call the DWARF above makes about
|
||||
locals, and for the same reason. *)
|
||||
let where_from = function
|
||||
| Ireg r -> Printf.sprintf "from %s" (regname r)
|
||||
| Isse i -> Printf.sprintf "from xmm%d" i
|
||||
| Istk d -> Printf.sprintf "from the caller's stack, at rbp+0x%x" d
|
||||
|
||||
let frame_map (md : Emit.m) (fn : Tast.fn) ~slots ~fixed ~total ~outgoing
|
||||
~xfer_off ~sret_off ~retval ~sret ~sret_at ~param_at ~xfer_at =
|
||||
let b = Buffer.create 1024 in
|
||||
let line s = Buffer.add_string b (if s = "" then "#\n" else "# " ^ s ^ "\n") in
|
||||
(* The prose paragraphs wrap; the table below does not, because its columns
|
||||
are the point of it. *)
|
||||
let para s = List.iter (fun l -> Buffer.add_string b (l ^ "\n"))
|
||||
(wrap ~pre:"# " ~width:76 s) in
|
||||
let bar = "# " ^ String.concat "" (List.init 68 (fun _ -> "\xe2\x94\x80")) in
|
||||
Buffer.add_string b (bar ^ "\n");
|
||||
(* The [defn] as it was written, which is the whole line and not the span:
|
||||
[floc] points at the name, and a reader wants the parameter list too. A
|
||||
function the checker lifted out of a [handler-bind] clause has no line of
|
||||
its own to show and says so. *)
|
||||
let decl =
|
||||
match Loc.source_line fn.Tast.floc with
|
||||
| Some l -> Some (String.trim l)
|
||||
| None -> None
|
||||
in
|
||||
line
|
||||
(Printf.sprintf "%s%s" (fsym fn.Tast.name)
|
||||
(match decl with
|
||||
| Some d when String.length d > 0 ->
|
||||
Printf.sprintf " %s %s"
|
||||
(if String.length d > 56 then String.sub d 0 55 ^ "…" else d)
|
||||
(Loc.to_string fn.Tast.floc)
|
||||
| _ ->
|
||||
(match fn.Tast.fparent with
|
||||
| Some parent ->
|
||||
Printf.sprintf
|
||||
" a clause lifted out of %s, which no one wrote as a \
|
||||
function" parent
|
||||
| None -> " " ^ Loc.to_string fn.Tast.floc)));
|
||||
(* A function out of the prelude, or out of any file this process cannot open
|
||||
again, gets a frame map and no form headings at all: [Loc.snippet] has
|
||||
nothing to quote and says so rather than printing a column of bare
|
||||
positions. Worth saying once per function, because the absence is
|
||||
otherwise read as a bug in the annotation. *)
|
||||
if decl = None then
|
||||
para
|
||||
"The source this was compiled from is not readable from here, so the \
|
||||
byte runs below carry no form headings — only this map.";
|
||||
line "";
|
||||
(* The convention, stated where the function is rather than only in this
|
||||
file's header, because the header is not what a reader of a listing has
|
||||
in front of them. *)
|
||||
let nparams = List.length fn.Tast.params in
|
||||
let args =
|
||||
List.mapi
|
||||
(fun i at ->
|
||||
let nm = match fn.Tast.snames.(i) with Some n -> n | None -> "_" in
|
||||
Printf.sprintf "%s %s" nm (where_from at))
|
||||
param_at
|
||||
in
|
||||
para
|
||||
(if nparams = 0 then "Takes nothing."
|
||||
else "Arguments: " ^ String.concat ", " args ^ ".");
|
||||
(match sret_at with
|
||||
| Some at ->
|
||||
para (Printf.sprintf
|
||||
"The result is an aggregate, so it comes back through a hidden sret pointer \
|
||||
the caller allocated (%s) and hands that same pointer back in rax. Every \
|
||||
aggregate goes by pointer here; nothing is classified and there is no \
|
||||
eightbyte rule."
|
||||
(where_from at))
|
||||
| None ->
|
||||
if is_void fn.Tast.ret then line "Returns nothing."
|
||||
else
|
||||
line (Printf.sprintf "Returns %s in %s."
|
||||
(Types.to_string fn.Tast.ret)
|
||||
(if is_float fn.Tast.ret then "xmm0" else "rax")));
|
||||
para (Printf.sprintf
|
||||
"The transfer channel arrives last of all, %s. It is a pointer to the cell a \
|
||||
callee writes its target into, and reading it is what every guard below \
|
||||
does."
|
||||
(where_from xfer_at));
|
||||
line "";
|
||||
para (Printf.sprintf
|
||||
"The frame is 0x%x bytes below rbp. %s" total
|
||||
(if outgoing > 0 then
|
||||
Printf.sprintf
|
||||
"The lowest 0x%x of them are the outgoing argument area, reserved once \
|
||||
here and written by whichever call in this function passes the most on \
|
||||
the stack." outgoing
|
||||
else "No call in it passes an argument on the stack."));
|
||||
line "";
|
||||
let row off name ty what =
|
||||
line (Printf.sprintf " %-8s %-14s %-10s %s"
|
||||
(Printf.sprintf "-0x%x" (-off)) name ty what)
|
||||
in
|
||||
Array.iteri
|
||||
(fun i ty ->
|
||||
if not (is_void ty) then begin
|
||||
let name =
|
||||
match fn.Tast.snames.(i) with Some n -> n | None -> "<anon>"
|
||||
in
|
||||
let what =
|
||||
if i < nparams then
|
||||
Printf.sprintf "parameter %d, %s" (i + 1)
|
||||
(where_from (List.nth param_at i))
|
||||
else if fn.Tast.snames.(i) = None then
|
||||
"a slot the compiler made, not one anyone named"
|
||||
else "a local"
|
||||
in
|
||||
let what =
|
||||
if is_agg ty then
|
||||
what ^ Printf.sprintf " — %d bytes, copied in" (sizeof md ty)
|
||||
else what
|
||||
in
|
||||
row slots.(i) name (Types.to_string ty) what
|
||||
end)
|
||||
fn.Tast.slots;
|
||||
row xfer_off "<chan>" "ptr" "the transfer channel this frame passes on";
|
||||
if sret then
|
||||
row sret_off "<sret>" "ptr"
|
||||
"the caller's sret pointer, kept for the epilogue";
|
||||
if (not sret) && not (is_void fn.Tast.ret) then
|
||||
row retval "<ret>" (Types.to_string fn.Tast.ret)
|
||||
"the return value the epilogue loads";
|
||||
para (Printf.sprintf
|
||||
"Everything below -0x%x 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." fixed);
|
||||
Buffer.add_string b (bar ^ "\n");
|
||||
Buffer.contents b
|
||||
|
||||
let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
?(slot = fun _ -> None) ?(hidden = false) ?dw (fn : Tast.fn)
|
||||
?(slot = fun _ -> None) ?(hidden = false) ?(ann = false) ?dw (fn : Tast.fn)
|
||||
: string * string =
|
||||
let b = create () in
|
||||
let nslots = Array.length fn.Tast.slots in
|
||||
@ -2597,7 +2995,8 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
xfer_off = 0; sret_off = 0; retval = 0;
|
||||
frame = 0; maxframe = 0; outgoing = 0;
|
||||
loops = []; pads = []; xfer_lbl = ""; unwound = false;
|
||||
rodata = Buffer.create 64; externs; fns; ext; slot; dw }
|
||||
rodata = Buffer.create 64; externs; fns; ext; slot; dw;
|
||||
ann; adepth = 0; alast = "" }
|
||||
in
|
||||
(* The subprogram this function's rows hang off. Its first row is the
|
||||
function symbol itself, at the line the [defn] was written on, so the
|
||||
@ -2638,6 +3037,11 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
if (not sret) && not (is_void fn.Tast.ret) then f.retval <- tmp f fn.Tast.ret;
|
||||
f.retlbl <- new_label f "ret";
|
||||
f.xfer_lbl <- new_label f "xfer";
|
||||
(* Where the named part of the frame ends and the nameless part begins. Read
|
||||
here rather than from [maxframe] afterwards, because [maxframe] is the
|
||||
high-water mark of the temporaries and this is the boundary below which
|
||||
they start. It is the frame map's last line. *)
|
||||
let fixed = f.frame in
|
||||
let sret_at, param_at, xfer_at = incoming_of ~sret fn.Tast.params in
|
||||
(* An aggregate parameter arrives as a pointer to the caller's copy and has
|
||||
to be copied into its slot before anything else runs — and [rep movsb]
|
||||
@ -2685,6 +3089,10 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
the transfer exit and the defers run a second time. [emit.ml] cannot
|
||||
have this bug — its [ret] terminates the block. *)
|
||||
jmp_lbl f.b f.retlbl;
|
||||
if ann then set_ind f.b "";
|
||||
note f
|
||||
"The transfer exit — spec-conditions.md §5. A transfer that found no restart-case \
|
||||
in this frame leaves the way a return does, which is what runs the defers.";
|
||||
lbl f.b f.xfer_lbl;
|
||||
(* [emit.ml] leaves here with [ret zeroinitializer]. The value is
|
||||
meaningless to a caller — its guard sees the channel set and never looks
|
||||
@ -2739,6 +3147,11 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
|
||||
(* The prologue, now that the frame size is known. *)
|
||||
let pb = create () in
|
||||
bnote ann pb
|
||||
"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.";
|
||||
push_r pb rbp;
|
||||
if cfi then cfi_after_push pb;
|
||||
mov_rr pb ~dst:rbp ~src:rsp;
|
||||
@ -2798,6 +3211,10 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
fn.Tast.params;
|
||||
|
||||
(* The epilogue, in exactly one place. *)
|
||||
if ann then set_ind f.b "";
|
||||
note f
|
||||
"The epilogue, and every return and every transfer out of this frame arrives here, \
|
||||
so the frame is torn down once.";
|
||||
lbl f.b f.retlbl;
|
||||
if sret then load_int f.b ~dst:rax ~mm:(Frame f.sret_off) ~size:8 ~signed:false
|
||||
else if not (is_void fn.Tast.ret) then
|
||||
@ -2810,6 +3227,11 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
flush f.b;
|
||||
let sym = fsym fn.Tast.name in
|
||||
let out = Buffer.create 1024 in
|
||||
if ann then
|
||||
Buffer.add_string out
|
||||
(frame_map md fn ~slots:f.slots ~fixed ~total:(frame_bytes f)
|
||||
~outgoing:f.outgoing ~xfer_off:f.xfer_off ~sret_off:f.sret_off
|
||||
~retval:f.retval ~sret ~sret_at ~param_at ~xfer_at);
|
||||
Buffer.add_string out (Printf.sprintf "\t.globl\t%s\n" sym);
|
||||
(* [emit.ml:2072] says this is load-bearing and it is: default visibility in
|
||||
a shared object is interposable, and that applies to taking the address
|
||||
@ -2842,8 +3264,16 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
|
||||
the loader put them in, the program's own end of the transfer channel is a
|
||||
null cell on this frame, and the exit goes through [flan_exit] because
|
||||
stdout is a FILE* and something has to flush it. *)
|
||||
let emit_main ?(cfi = false) (md : Emit.m) (fn : Tast.fn) =
|
||||
let emit_main ?(cfi = false) ?(ann = false) (md : Emit.m) (fn : Tast.fn) =
|
||||
let b = create () in
|
||||
bnote ann b
|
||||
"C's main, which is the whole of the adapter between the loader and a Flan program. \
|
||||
The runtime is initialised while argc and argv are still in the registers the \
|
||||
loader put them in; the program's own end of the transfer channel is a null cell \
|
||||
on this frame, so flan.main is called exactly the way every other Flan function \
|
||||
is; and the exit goes through flan_exit rather than ret, because stdout is a FILE* \
|
||||
and something has to flush it. The ud2 at the end is unreachable — flan_exit does \
|
||||
not return.";
|
||||
push_r b rbp;
|
||||
if cfi then cfi_after_push b;
|
||||
mov_rr b ~dst:rbp ~src:rsp;
|
||||
@ -2911,7 +3341,7 @@ let emit_globals_data (md : Emit.m) (globals : Tast.global list) =
|
||||
|
||||
let init_sym = "\"flan..init-globals\""
|
||||
|
||||
let emit_globals_init ?(cfi = false) (md : Emit.m) ~externs ~fns
|
||||
let emit_globals_init ?(cfi = false) ?(ann = false) (md : Emit.m) ~externs ~fns
|
||||
(globals : Tast.global list) =
|
||||
let b = create () in
|
||||
let f =
|
||||
@ -2920,7 +3350,7 @@ let emit_globals_init ?(cfi = false) (md : Emit.m) ~externs ~fns
|
||||
frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = [];
|
||||
xfer_lbl = ""; unwound = false;
|
||||
rodata = Buffer.create 64; externs; fns; ext = (fun _ -> false);
|
||||
slot = (fun _ -> None); dw = None }
|
||||
slot = (fun _ -> None); dw = None; ann; adepth = 0; alast = "" }
|
||||
in
|
||||
(* Two slots, not one: [xfer_off] holds the *pointer* every call passes on,
|
||||
and [cell] is what it points at. Storing a null into [xfer_off] itself —
|
||||
@ -3256,7 +3686,8 @@ let emit_dwarf (dw : dwarf) ~cufile ~tbeg ~tend =
|
||||
Buffer.contents out
|
||||
|
||||
(* A whole program as one assembly file. *)
|
||||
let program ~checks ?(dev = false) ?(debug = false) (p : Tast.program) : string =
|
||||
let program ~checks ?(dev = false) ?(debug = false) ?(annotate = false)
|
||||
(p : Tast.program) : string =
|
||||
check_no_transfer p;
|
||||
let md = layout_ctx ~checks ~dev p in
|
||||
let externs = Hashtbl.create 16 in
|
||||
@ -3282,6 +3713,69 @@ let program ~checks ?(dev = false) ?(debug = false) (p : Tast.program) : string
|
||||
"# Generated by flan's x86-64 backend (the dev one). The instructions are\n\
|
||||
# .byte blobs so that every byte offset stays exactly known; the few\n\
|
||||
# fields that need a relocation are assembler expressions.\n";
|
||||
(* The legend, and the reason it is here rather than repeated: four of the
|
||||
five things below are emitted at hundreds of sites, and a comment that
|
||||
explains the transfer guard at every call site is noise by the third one.
|
||||
Each is named where it appears and explained once, here. *)
|
||||
if annotate then
|
||||
Buffer.add_string text
|
||||
"#\n\
|
||||
# Annotated, because `flan emit --x86` exists to be read. Every comment\n\
|
||||
# here is discarded by the assembler; the bytes are what a build emits,\n\
|
||||
# unchanged and in the same order.\n\
|
||||
#\n\
|
||||
# How to read it\n\
|
||||
#\n\
|
||||
# Above each function is a frame map. Every value in this backend\n\
|
||||
# lives in a frame slot, so -0x20(%rbp) is the whole vocabulary of the\n\
|
||||
# listing and the map is its key: which displacement is which\n\
|
||||
# parameter, which is which named local, where the compiler's own\n\
|
||||
# three sit, and below which offset everything is an unnamed\n\
|
||||
# temporary that later forms reuse.\n\
|
||||
#\n\
|
||||
# Inside a function, each run of bytes is headed by the Flan form that\n\
|
||||
# produced it, with the file:line:col it was written at. Headings and\n\
|
||||
# byte runs are indented by how deeply the form nests, so an\n\
|
||||
# argument's code steps in and the call's steps back out.\n\
|
||||
#\n\
|
||||
# Literals, locals and globals are not headed: they would steal the\n\
|
||||
# heading of the form that contains them, and the operand loads\n\
|
||||
# belong under the operator.\n\
|
||||
#\n\
|
||||
# The five things the compiler adds that no form asked for\n\
|
||||
#\n\
|
||||
# The transfer guard. After every call to Flan code: load this\n\
|
||||
# frame's channel pointer, load through it, test, and branch if it is\n\
|
||||
# set. A callee that transferred wrote a frame address there and the\n\
|
||||
# value in rax means nothing, so the branch goes to the innermost\n\
|
||||
# restart-case, handler-bind or with-allocator landing pad, or to the\n\
|
||||
# function's own transfer exit. Four instructions, touching only r11,\n\
|
||||
# which is why it fits between the call and the store of the result.\n\
|
||||
# spec-conditions.md §6.\n\
|
||||
#\n\
|
||||
# The bounds check. A compare and a not-taken branch on the fast\n\
|
||||
# path; the slow path passes a location string, the index and the\n\
|
||||
# length, and this frame's channel, to a runtime entry point that\n\
|
||||
# signals. Because it signals rather than aborting, it is an ordinary\n\
|
||||
# call with a guard after it, and the ud2 past the guard is where\n\
|
||||
# nothing answered.\n\
|
||||
#\n\
|
||||
# The arithmetic guard, the same shape: a zero divisor, the one\n\
|
||||
# overflowing division, and the range check on a float-to-integer\n\
|
||||
# cast.\n\
|
||||
#\n\
|
||||
# rep movsb. An aggregate is copied and never aliased, so a struct\n\
|
||||
# argument, a struct return and a struct assignment are each a block\n\
|
||||
# copy. spec-memory.md's assignment rule.\n\
|
||||
#\n\
|
||||
# The indirection cell, in a --dev build only. A call by name loads\n\
|
||||
# the cell first and calls through it, so that a redefinition\n\
|
||||
# installed while the process runs is reached by the next call.\n\
|
||||
#\n\
|
||||
# What is not here are mnemonics. The bytes are a blob so that every\n\
|
||||
# offset stays exactly known, and spike/x86/dump.sh puts objdump's\n\
|
||||
# disassembly of this same object beside this file: that one says what,\n\
|
||||
# and this one says why.\n";
|
||||
(* A numbered [.file] is what stops clang's integrated assembler from
|
||||
generating a compile unit of its *own* over this file -- one that names
|
||||
the .s, and whose rows land at the [call] mnemonics, which are the only
|
||||
@ -3299,15 +3793,18 @@ let program ~checks ?(dev = false) ?(debug = false) (p : Tast.program) : string
|
||||
(if debug then "\t.text\n.Ldwtext:\n\n" else "\t.text\n\n");
|
||||
List.iter
|
||||
(fun (fn : Tast.fn) ->
|
||||
let t, r = emit_fn md ~externs ~fns ?dw fn in
|
||||
let t, r = emit_fn md ~externs ~fns ~ann:annotate ?dw fn in
|
||||
Buffer.add_string text t;
|
||||
Buffer.add_string rodata r)
|
||||
p.Tast.fns;
|
||||
let ginit, gr = emit_globals_init ~cfi:debug md ~externs ~fns p.Tast.globals in
|
||||
let ginit, gr =
|
||||
emit_globals_init ~cfi:debug ~ann:annotate md ~externs ~fns p.Tast.globals
|
||||
in
|
||||
Buffer.add_string text ginit;
|
||||
Buffer.add_string rodata gr;
|
||||
(match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = "main") p.Tast.fns with
|
||||
| Some fn -> Buffer.add_string text (emit_main ~cfi:debug md fn)
|
||||
| Some fn ->
|
||||
Buffer.add_string text (emit_main ~cfi:debug ~ann:annotate md fn)
|
||||
(* No [main] is not an error, and [emit.ml] treats it the same way: a
|
||||
program can be linked against a C host that brings its own entry point,
|
||||
which is what [reload_host.c] is. Refusing here made a --x86 host for the
|
||||
@ -3517,7 +4014,8 @@ let redefinition ~checks ?(dev = true) ?(known = fun _ -> true)
|
||||
fret = Types.Unit; slots = [||]; xfer_off = 0; sret_off = 0; retval = 0;
|
||||
frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = [];
|
||||
xfer_lbl = ""; unwound = false;
|
||||
rodata = Buffer.create 256; externs; fns = fnstbl; ext; slot; dw = None }
|
||||
rodata = Buffer.create 256; externs; fns = fnstbl; ext; slot; dw = None;
|
||||
ann = false; adepth = 0; alast = "" }
|
||||
in
|
||||
let chan = ptmp f in
|
||||
f.xfer_off <- ptmp f;
|
||||
|
||||
101
spike/x86/annot.sh
Executable file
101
spike/x86/annot.sh
Executable file
@ -0,0 +1,101 @@
|
||||
#!/usr/bin/env bash
|
||||
# Does annotation change a single byte of what the backend emits?
|
||||
#
|
||||
# `flan emit --x86` annotates: a comment per Flan form, a frame map per
|
||||
# function, and a name for each piece of bookkeeping the compiler adds. All of
|
||||
# that is comments, plus the splitting of one long `.byte` directive into
|
||||
# several. Both are supposed to be invisible to the assembler -- and "supposed
|
||||
# to be" is exactly the kind of claim this repo measures rather than asserts,
|
||||
# because the whole licence for annotating at all is that the bytes are the
|
||||
# bytes.
|
||||
#
|
||||
# So: emit every program in the corpus both ways, assemble both, and compare
|
||||
# each section of the two objects byte for byte. No linking and no running --
|
||||
# survey.sh is what says the programs still behave, and this says nothing they
|
||||
# are built from moved.
|
||||
#
|
||||
# Three settings, because they are three different emitters. The default; --dev,
|
||||
# which adds the indirection cells and the ABI marker; and --debug, which adds
|
||||
# the line table, the labels its rows hang off, and the CFI directives. The
|
||||
# debug case is the sharp one: a `.debug_line` row is an address expressed as a
|
||||
# label, and annotation emits no labels precisely so that those cannot move.
|
||||
#
|
||||
# Usage: spike/x86/annot.sh [name-substring ...]
|
||||
set -u
|
||||
orig=$(pwd)
|
||||
here=$(cd "$(dirname "$0")" && pwd)
|
||||
root=$(cd "$here/../.." && pwd)
|
||||
cd "$root" || exit 1
|
||||
|
||||
if [ -n "${FLAN:-}" ]; then
|
||||
case $FLAN in /*) flan=$FLAN;; *) flan=$orig/$FLAN;; esac
|
||||
else
|
||||
dune build --root . bin/main.exe 2>&1 | head -30
|
||||
flan=$root/_build/default/bin/main.exe
|
||||
fi
|
||||
test -x "$flan" || { echo "build failed"; exit 1; }
|
||||
|
||||
corpus=${SURVEY_CORPUS:-$root}
|
||||
tmp=$(mktemp -d "${TMPDIR:-/tmp}/flan-annot.XXXXXX")
|
||||
trap 'rm -rf "$tmp"' EXIT
|
||||
|
||||
same=0; differ=0; skip=0
|
||||
|
||||
# Every section either object has, not a fixed list: a section that exists on
|
||||
# one side and not the other is itself a difference, and comparing a named list
|
||||
# would miss one that annotation invented.
|
||||
sections () {
|
||||
objdump -h "$1" | awk '$1 ~ /^[0-9]+$/ { print $2 }'
|
||||
}
|
||||
|
||||
check () {
|
||||
src=$1; shift
|
||||
name=$(basename "$src" .flan)
|
||||
tag="$name${*:+ $*}"
|
||||
a=$tmp/a.s; b=$tmp/b.s
|
||||
|
||||
if ! "$flan" emit --x86 "$@" "$src" > "$a" 2>"$tmp/err"; then
|
||||
skip=$((skip + 1)); echo "SKIP $tag"; return
|
||||
fi
|
||||
if ! "$flan" emit --x86 --no-annotate "$@" "$src" > "$b" 2>/dev/null; then
|
||||
skip=$((skip + 1)); echo "SKIP $tag"; return
|
||||
fi
|
||||
if ! as --64 -o "$tmp/a.o" "$a" 2>"$tmp/err"; then
|
||||
differ=$((differ + 1))
|
||||
echo "BADASM $tag -- the annotated listing does not assemble"
|
||||
head -3 "$tmp/err"; return
|
||||
fi
|
||||
if ! as --64 -o "$tmp/b.o" "$b" 2>/dev/null; then
|
||||
skip=$((skip + 1)); echo "SKIP $tag"; return
|
||||
fi
|
||||
|
||||
bad=
|
||||
for sec in $(sections "$tmp/a.o"; sections "$tmp/b.o"); do
|
||||
case " $bad " in *" $sec "*) continue;; esac
|
||||
objcopy -O binary --only-section="$sec" "$tmp/a.o" "$tmp/a.bin" 2>/dev/null
|
||||
objcopy -O binary --only-section="$sec" "$tmp/b.o" "$tmp/b.bin" 2>/dev/null
|
||||
cmp -s "$tmp/a.bin" "$tmp/b.bin" || bad="$bad $sec"
|
||||
done
|
||||
|
||||
if [ -z "$bad" ]; then
|
||||
same=$((same + 1)); echo "SAME $tag"
|
||||
else
|
||||
differ=$((differ + 1)); echo "DIFFER $tag --$bad"
|
||||
fi
|
||||
}
|
||||
|
||||
for src in "$corpus"/test/programs/*.flan "$corpus"/spike/x86/*.flan; do
|
||||
[ -f "$src" ] || continue
|
||||
if [ $# -gt 0 ]; then
|
||||
hit=
|
||||
for pat in "$@"; do case $src in *"$pat"*) hit=1;; esac; done
|
||||
[ -n "$hit" ] || continue
|
||||
fi
|
||||
check "$src"
|
||||
check "$src" --dev
|
||||
check "$src" --debug
|
||||
done
|
||||
|
||||
echo
|
||||
echo "$same SAME / $differ DIFFER / $skip SKIP"
|
||||
[ "$differ" -eq 0 ]
|
||||
@ -1,8 +1,10 @@
|
||||
#!/bin/sh
|
||||
# Every lowering of one program, side by side: the LLVM IR the frontend emits,
|
||||
# what LLVM makes of it at -O0 and at -O2, and what the hand-written backend
|
||||
# emits. Reading one against another is the only way to check a lowering by eye,
|
||||
# and the whole reason the second backend is trustworthy is that the two agree.
|
||||
# emits -- the last of those twice, as the annotated listing it writes and as
|
||||
# the disassembly of the object that listing assembles to. Reading one against
|
||||
# another is the only way to check a lowering by eye, and the whole reason the
|
||||
# second backend is trustworthy is that the two agree.
|
||||
#
|
||||
# $ spike/x86/dump.sh file.flan [name]
|
||||
#
|
||||
@ -16,8 +18,8 @@
|
||||
#
|
||||
# FLAN overrides the compiler; the default is the one dune just built. Flags
|
||||
# after the name are passed to every stage that understands them, so
|
||||
# `dump.sh f.flan twice --dev` compares the four dev lowerings rather than the
|
||||
# four release ones.
|
||||
# `dump.sh f.flan twice --dev` compares the dev lowerings rather than the
|
||||
# release ones.
|
||||
set -e
|
||||
here=$(cd "$(dirname "$0")" && pwd)
|
||||
root=$(cd "$here/../.." && pwd)
|
||||
@ -34,9 +36,20 @@ base=$(basename "$src" .flan)
|
||||
"$FLAN" emit "$src" "$@" > "$out/$base.ll"
|
||||
llc -O0 "$out/$base.ll" -o "$out/$base.O0.s"
|
||||
llc -O2 "$out/$base.ll" -o "$out/$base.O2.s"
|
||||
# The backend writes machine code, not mnemonics, so its .s is .byte blobs.
|
||||
# Assembling and disassembling is what makes it readable -- and it is also a
|
||||
# check that the bytes are well formed, which reading them never would be.
|
||||
# Two files out of the backend, and they answer different questions.
|
||||
#
|
||||
# The .s is what it emits, and it is annotated: a frame map above each
|
||||
# function saying which rbp displacement is which parameter and which is which
|
||||
# named local, the Flan form above each run of bytes that produced it, and a
|
||||
# name for each piece of bookkeeping the compiler added. That is the *why*, and
|
||||
# it is the file to read when the question is where eleven instructions came
|
||||
# from.
|
||||
#
|
||||
# The disassembly is the *what*. The backend writes machine code rather than
|
||||
# mnemonics -- .byte blobs, so that every offset stays exactly known -- so
|
||||
# assembling and disassembling is the only way to see the instructions, and it
|
||||
# is also a check that the bytes are well formed, which reading them never
|
||||
# would be.
|
||||
"$FLAN" emit --x86 "$src" "$@" > "$out/$base.x86.s"
|
||||
as --64 -o "$out/$base.x86.o" "$out/$base.x86.s"
|
||||
objdump -d --no-show-raw-insn "$out/$base.x86.o" > "$out/$base.x86.dis"
|
||||
@ -54,8 +67,21 @@ if [ -n "$fn" ]; then
|
||||
done
|
||||
awk -v f="<flan.$fn>:" '$0 ~ f {p=1} p; p && /^$/ {p=0}' \
|
||||
"$out/$base.x86.dis" > "$out/$base.fn.x86" || true
|
||||
# The annotated listing for the same function, which is the half of the four
|
||||
# that says *why*. It has to carry the frame map with it -- the map sits above
|
||||
# the .globl, and without it every displacement in the body is anonymous -- so
|
||||
# this keeps the most recent run of comment lines in hand and prints it when
|
||||
# the function's label arrives.
|
||||
awk -v f="flan.$fn" '
|
||||
/^#/ { if (!inc) buf = ""; inc = 1; buf = buf $0 "\n"; next }
|
||||
{ inc = 0 }
|
||||
$0 ~ "^\"?" f "\"?:" { printf "%s", buf; p = 1 }
|
||||
p
|
||||
p && /\.size/ { p = 0 }' \
|
||||
"$out/$base.x86.s" > "$out/$base.fn.x86.s" || true
|
||||
|
||||
for f in "$out/$base.fn.ll" "$out/$base.fn.O0.s" "$out/$base.fn.O2.s" "$out/$base.fn.x86"; do
|
||||
for f in "$out/$base.fn.ll" "$out/$base.fn.O0.s" "$out/$base.fn.O2.s" \
|
||||
"$out/$base.fn.x86.s" "$out/$base.fn.x86"; do
|
||||
[ -s "$f" ] || { echo "nothing for '$fn' in $(basename "$f")" >&2; continue; }
|
||||
echo "=== $(basename "$f") ==="
|
||||
cat "$f"
|
||||
@ -63,4 +89,4 @@ if [ -n "$fn" ]; then
|
||||
done
|
||||
fi
|
||||
|
||||
echo "all four in $out"
|
||||
echo "all of them in $out"
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user