Joseph Ferano
6363635bae
Item 17 left two correctness items and a loose end. The loose end is the answer to the first item: flan_vec_as_slice's Flan-level return type is Unit, so is_void answers before is_agg is ever tested, and that is the convention rather than one symbol's accident. So there was no sret-for-Rt to build, and building one would have been untestable and wrong. The second item is built and tested by the only thing that can test it, a preloaded dlsym, because a dev build with nothing yet redefined prints what a release build prints whether or not anything reads a cell. Survey: 93 MATCH / 0 DIFFER / 2 refused before, 97 / 0 / 0 after; 97 / 0 / 0 again with --dev on both sides.
166 lines
11 KiB
Markdown
166 lines
11 KiB
Markdown
# Handoff — the x86 backend's last two correctness items
|
|
|
|
Branch: `dev-loop`, worktree `agent-af9064091c0602dc8`. Three commits plus this one; nothing is half-written and
|
|
nothing is reverted. The long-form report is **DISCUSS.md item 18**; this file is the operational version.
|
|
|
|
## 1. The `flan_vec_as_slice` answer — got it, and it is complete
|
|
|
|
**`flan_vec_as_slice` never reaches the aggregate-return refusal because its Flan-level return type is `Unit`.**
|
|
|
|
Primary sources, all three agreeing:
|
|
|
|
- `lib/check.ml:3721` — `rt loc Types.Unit "flan_vec_as_slice"`
|
|
- `runtime/flan_rt.c:1165` — `void flan_vec_as_slice(flan_vec *v, void *out, int32_t lo, int32_t hi, ...)`
|
|
- `lib/emit.ml:2464` — `declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64, ptr)`
|
|
|
|
In `lib/x86.ml`'s `call_native` the two tests are in this order:
|
|
|
|
```
|
|
if not (is_void rty) then begin
|
|
if is_agg rty then unsupported ...
|
|
```
|
|
|
|
`rty` is the *node's* type, which is `Unit`, so `is_void` answers first and `is_agg` is never evaluated. The slice
|
|
leaves through the `void *out` pointer the checker allocated with `fresh_slot`.
|
|
|
|
**So the refusal is narrower than it reads — the first of the two possibilities the brief named. Nothing is going
|
|
right by accident.** It is not one symbol's quirk either; two rules in `check.ml` make the line unreachable for
|
|
*every* caller of that code path:
|
|
|
|
1. **The `rt` out-pointer convention.** Every `rt loc <ty> ...` builder in `check.ml` answers `Unit`, an `Int`, a
|
|
`Ptr`, an `Alloc`, a `Handle` or `Int U64`. Enumerated exhaustively by grepping `Tast.Rt` construction sites —
|
|
there are 26 and none is aggregate-typed. `flan_pool_resolve` answers `Ptr elem` and the `Option` is built in Flan;
|
|
`Argv` is its own `Tast` node with its own out-pointer and does not come through `call_native` at all.
|
|
2. **`crossable`** (`lib/check.ml`, the `Ast.Declare` arm, ~line 5228), the other user of `call_native`, admits
|
|
`String`/`Slice _` only when `what = "a parameter"` and refuses an aggregate return from a `declare` outright.
|
|
|
|
**Conclusion, and it changed the work: do not build sret-for-`Rt`.** That path is the *C* boundary, where the header
|
|
says the backend must match SysV rather than pick its own. A 16-byte slice comes back in `rax:rdx`, not through this
|
|
backend's internal hidden-pointer convention, and there is no classifier in the file. Building one would have been
|
|
untestable (nothing in the language can produce a call that needs it) *and* wrong (wrong convention). The refusal
|
|
stays as a guard against those two rules changing, with the reasoning in a comment and a message that now names SysV
|
|
classification instead of reading like a missing feature.
|
|
|
|
**Consequence:** item 16's "`Vec`, `Map` and `Pool` have not been exercised at all" was already stale when item 17
|
|
repeated it. Verified with the survey: `Vec`/`Map` via `vec.flan`, `vec-of-vec.flan`, `vec-in-struct.flan`,
|
|
`maps.flan`, `map-iter.flan`; **`Pool` — which neither report checked** — via `registry.flan`, `handles.flan`,
|
|
`generics.flan`, `pool-stale-region.flan`. All MATCH.
|
|
|
|
## 2. Survey counts, measured
|
|
|
|
`spike/x86/survey.sh`, unchanged in what it compares (stdout + stderr + exit status, same bounds-check setting both
|
|
sides).
|
|
|
|
| | brief said | measured before | after |
|
|
|---|---|---|---|
|
|
| MATCH | 89 | **93** | **97** |
|
|
| DIFFER | 0 | 0 | **0** |
|
|
| refused by name | 0 | **2** | **0** |
|
|
| skip: does not compile / no main / forever | 25 / 6 / 2 | 28 / 6 / 2 | 28 / 6 / 2 |
|
|
|
|
**The brief's 89/0/0 baseline was stale.** Another lane landed `(slice-from-ptr p n)` after item 17, and it arrived as
|
|
two refusals — `slice-from-ptr.flan` and `bounds.flan` — both reported as `x86: primitive with 2 arguments`. Fixing
|
|
that is commit 1 and is reported separately so the "after" number is not misread as this lane's work.
|
|
|
|
Also measured, opt-in and new: `SURVEY_FLAGS=--dev spike/x86/survey.sh` → **97 MATCH / 0 DIFFER**.
|
|
|
|
## 3. What was built, file by file
|
|
|
|
All **working and verified**; nothing in this list is unverified or reverted.
|
|
|
|
| file | state | what |
|
|
|---|---|---|
|
|
| `lib/x86.ml` — `prim`, `Tast.SliceFromPtr` case | working | new. Two stores; the length check is **signed** (`cc_ge`), not `check_slice`'s unsigned compare |
|
|
| `lib/x86.ml` — `call_native` | working | refusal reworded + the two `check.ml` invariants written down. No behaviour change |
|
|
| `lib/x86.ml` — `csym` | working | new, `"flan.cell." ^ n` quoted; must stay byte-identical to `Emit.cellname` |
|
|
| `lib/x86.ml` — `lower`, `FnAddr (Fnval _)` | working | splits from `Flanfn`; loads the cell when `md.dev` |
|
|
| `lib/x86.ml` — `lower`, `Tast.Call` | working | passes `` `Cell `` instead of `` `Sym `` when `md.dev` |
|
|
| `lib/x86.ml` — `call_flan` | working | new `` `Cell `` target: `mov r11, [rip+cell]; call r11`, **after** `emit_args` |
|
|
| `lib/x86.ml` — `emit_cells` | working | new. `.data`, `.globl`, `.quad <body>`, one per `p.Tast.fns` |
|
|
| `lib/x86.ml` — `program` | working | now `~checks ?dev`; emits cells and the `flan_dev_reg_enable` ctor when `dev` |
|
|
| `lib/x86.ml` — `layout_ctx` | working | now `~checks ~dev`; `Emit.m.dev` is no longer hardcoded `false` |
|
|
| `lib/build.ml` | working | `--dev` removed from the `--x86` refusal list; `~dev:opts.dev` threaded to `X86.program` |
|
|
| `spike/x86/survey.sh` | working | `SURVEY_FLAGS`, given to **both** sides. Default unchanged |
|
|
| `spike/x86/p7-slice-from-ptr.flan` | working, MATCH | negative length through a parameter and a `restart-case` |
|
|
| `spike/x86/p8-cell.flan` | working, MATCH | direct call + function value, for `cells.sh` |
|
|
| `spike/x86/cell-override.c` | working | `dlsym("flan.cell.twice")` + store, in a constructor |
|
|
| `spike/x86/cells.sh` | working, 4/4 ok | the only test of the cell that can exist |
|
|
|
|
`lib/emit.ml` was **not** modified. No change to it was needed.
|
|
|
|
## 4. What did not work, with the errors
|
|
|
|
Nothing fought for an hour. Four short false starts, all mine and all one-line:
|
|
|
|
- `handler-bind` clause syntax guessed as an `fn` literal:
|
|
`spike/x86/p7-slice-from-ptr.flan:30:18: a handler-bind clause is (Type [name] body ...)`.
|
|
The form is `(BoundsError [c] body ...)`; `test/programs/bounds-condition.flan:112` is the model.
|
|
- `(defn show [name [u8] ...])` for a literal argument:
|
|
`spike/x86/p7-slice-from-ptr.flan:37:14: expected [u8], found string`. A string literal wants `string`, not `[u8]`,
|
|
even though they are the same two words at the machine level.
|
|
- `cmp_imm` takes `~dst` and an `int`, not `~reg` and an `Int64`.
|
|
- `cell-override.c`: `error: 'NULL' undeclared` — needs `<stddef.h>` beside `<dlfcn.h>`.
|
|
|
|
One environment note for the next lane, not a failure of this work: `dune test --root .` prints
|
|
`/usr/bin/ld: cannot open output file /tmp/build_*_dune/flan-devtest-robust.cache/flan-macros-*.so.*: Permission
|
|
denied` and `clang: error: linker command failed with exit code 1` twice. That is **inside the `dev-robust` fixture**,
|
|
which exists to prove a failed build leaves the session standing; the run still exits 0. Item 17's four raylib
|
|
fixtures did **not** fail here — `/tmp` had room throughout (6% used at start and at finish).
|
|
|
|
## 5. Was `Fnval`'s cell reached, and the `--dev` call
|
|
|
|
**Yes, reached and tested.** And the test is the interesting part, because *the corpus cannot do it*: a dev build
|
|
starts with every cell pointing at the body that build compiled, so it prints exactly what a release build prints
|
|
whether or not anything reads the cell. `spike/x86/cells.sh` preloads a `.so` whose constructor `dlsym`s
|
|
`flan.cell.twice` (the cells are in `.dynsym` — a dev build is `-rdynamic`) and stores a different body there. Four
|
|
builds; the two release rows are the control that says the effect is the indirection and not symbol interposition:
|
|
|
|
```
|
|
ok llvm --dev: 22 22
|
|
ok x86 --dev: 22 22
|
|
ok llvm : 42 42
|
|
ok x86 : 42 42
|
|
```
|
|
|
|
Also checked: `nm -D` over an LLVM `--dev` build and an x86 `--dev` build of the same program gives **identical sets of
|
|
68 `flan.cell.*` symbols**. That is the property the later lane depends on.
|
|
|
|
**My call: yes, relax `--x86` with `--dev`, and it is relaxed.** The argument is narrow and verified: `--x86` is read
|
|
in exactly one place, `flan build`'s argument list in `bin/main.ml`. `flan dev` and `flan reload` build host and
|
|
module through `Build.executable` / `Build.shared` with no `x86` field set, and there is no spelling that hands them
|
|
one. So the daemon is unchanged and cannot reach the new path. What `--x86 --dev` gives is **a host whose call sites
|
|
are redefinable**; what it does not give is anything in the toolchain that can write a cell, because
|
|
`Emit.redefinition` has no counterpart here.
|
|
|
|
**The one thing the next lane must read before it writes that counterpart** (now in `x86.ml`'s header and
|
|
`build.ml`'s refusal comment too): `x86.ml` licenses its own calling convention on the grounds that a dev build is
|
|
compiled entirely here and a release build entirely by LLVM, *so the two never meet in one process*. A cell an
|
|
LLVM-built module can store into is the first thing that can make that false. The two conventions agree on scalars and
|
|
disagree on **every aggregate** — here each goes by pointer with a hidden `sret`; LLVM classifies. An
|
|
`Emit.redefinition` module dlopened into an `--x86` host would be correct until the first redefined function took or
|
|
returned a struct. `cells.sh` does not reach it: the body it installs is `(i64, void *) -> i64`.
|
|
**The answer is a redefinition emitter here, not a classifier.**
|
|
|
|
## 6. What remains, in the order to do it
|
|
|
|
1. **A redefinition emitter in `lib/x86.ml`** — the counterpart to `Emit.redefinition`, producing a `.so`: cells as
|
|
`.globl` externs rather than definitions, bodies hidden, `Emit.cellptr`'s deeper spelling for names the host lacks,
|
|
the `flan_dev_cell` / `flan_dev_global` lookups, and a publish function. This is the only item that unblocks the
|
|
dev loop, and question 5 above is why it cannot be skipped by leaning on LLVM for modules.
|
|
2. **`flan_dev_reg_note` dropped in a release build** — in `prim`'s `Tast.Rt` dispatch, matching `emit.ml:1918`'s
|
|
`when (not f.md.dev) && ...` arm. Today `x86.ml` emits real calls into a disabled registry: correct, no-ops, one
|
|
call each. Cheap; a code-size item, not a correctness one.
|
|
3. **`f64` → `i64` out of range**, and **`INT64_MIN / -1`**, in `prim`'s `Tast.Cast` and `Div`/`Rem` arms. `idiv`
|
|
raises `SIGFPE` where LLVM says undefined. Blocked on a *language* decision, unchanged across items 15, 16, 17.
|
|
4. **The `flan_transfer_fail` branch** — a defer starting a second transfer while the first unwinds. Emitted in
|
|
`transfer_exit`, refused loudly, reached by no program. Needs a probe in `spike/x86`.
|
|
5. **`"defers on a transfer path nothing reaches"`** — the refusal in `emit_fn`. Same: exists so that if the reasoning
|
|
is wrong it says so, and no program reaches it.
|
|
6. **Debug information.** None; `--x86 --debug` still refused in `build.ml`.
|
|
7. **Code size and speed.** Still unmeasured, and the list grew: a guard after every call, three frame temporaries per
|
|
bounds check, every intermediate in memory, `rep movsb` block copies, and now an extra load per call site in a dev
|
|
build — which is the one item `emit.ml` pays too.
|
|
|
|
**Also worth doing and not a backend item: run `spike/x86/survey.sh` in CI.** The 2 refusals this lane found were a
|
|
month-old lane's new prim, and nothing noticed. A backend that refuses by name does not rot quietly, but it does rot.
|