diff options
| -rw-r--r-- | TODO.md | 1 | ||||
| -rw-r--r-- | docs/BOOTSTRAP-OWNERSHIP.md | 155 | ||||
| -rw-r--r-- | docs/BORROW.md | 2 | ||||
| -rwxr-xr-x | src/tools/bootstrap-check.sh | 20 |
4 files changed, 178 insertions, 0 deletions
@@ -142,3 +142,4 @@ - [ ] revise diagnostics, comments and learning/reference prose using professional compiler documentation guidance, preserving lowercase and adding message regressions. - [ ] implement and integrate `src/lib/icon.zc` with structured runtime syntax transformations, template matching, execution inspection and stepping, with explicit contracts and comprehensive tests. - [ ] change the producer of the genome header (`build/core/genome.h`) to emit a c translation unit that embeds the compiler, core and runtime zc sources with a `#embed` directive instead of concatenating them into a 1.5 mb generated header; keep the `.zc` sources as the single source of truth and extend the fixpoint check in `make genome` so it still verifies the emitted genome without materializing a header at all. +- [ ] close the two ownership completeness limits that stop the compiler compiling itself, so `make genome` completes from a clean checkout: allow an owned value held in a local to move into another local when the destination's previous owner is released in the same statement list, and allow a global to hold a bounded borrow of a local so an output stream can be redirected at a scratch buffer without a module-level variable. also give `rt.code_blocks = m*block;` a supported spelling and fix the `only a named owned object can be recast` diagnostic, which does not describe the real constraint. written up in `docs/BOOTSTRAP-OWNERSHIP.md`, which also records a verified partial fix that removes five of the eight current errors. diff --git a/docs/BOOTSTRAP-OWNERSHIP.md b/docs/BOOTSTRAP-OWNERSHIP.md new file mode 100644 index 0000000..509db2f --- /dev/null +++ b/docs/BOOTSTRAP-OWNERSHIP.md @@ -0,0 +1,155 @@ +# the bootstrap does not compile: owned values cannot be moved between locals + +status: open, blocks `make` +affects: `make genome`, the `fixpoint` check, the `genome.h is up to date` check +see also: `docs/BORROW.md` + +## summary + +`make` bootstraps the compiler with `zc0` compiling `src/runtime/rt.zc`, +`src/core/core.zc` and `src/compiler/compiler.zc` into a stage-0 image, stage-0 +becoming `build/zy0`, and `zy0` compiling the same three files again into the +genome. the second compilation runs with lifetime checking enabled and rejects +the compiler's own source. `bin/mkgenome` then reads the diagnostics as if they +were an image: + +``` +mkgenome: input is not a genome for this map +``` + +the real output of `zy0` is a diagnostic list, not an image. nothing after the +fixpoint can run, so a checkout with no prebuilt genome cannot be built. + +this is a completeness gap in the ownership rules, not a soundness failure. the +checker is refusing correct programs; it is not accepting unsafe ones. the +practical cost is that the compiler can no longer compile itself. + +## the affected code + +`methdef` in `src/compiler/compiler.zc` reassembles a typed generic method's +token list. it saves the output stream state, redirects the stream at a scratch +buffer, renders the return type into it, splits the result into tokens, builds a +replacement buffer that interleaves the new tokens with the old ones, and hands +the replacement back in place of the original. + +```zc +word output = rt.outbuf, grow = rt.outgrow, buffer = rt.new(4096), return_tokens, joined; +rt.outmode = 2; rt.outbuf = m*buffer; rt.outn = 0; rt.outcap = 4095; rt.outgrow = 0; +tprint(rty); if (rtag) rt.put_s(".u"); buffer[rt.outn] = 0; +rt.outmode = mode; rt.outbuf = output; rt.outn = length; rt.outcap = capacity; rt.outgrow = grow; +return_tokens = tokens(buffer); +... +joined = rt.new((r[0] + return_tokens[0]) * 3 + 1); +... +word previous = m*r; r = d*joined; rt.free(return_tokens); rt.free(buffer); rt.free(previous); +``` + +three separate moves are needed here, and each one hits a different limit: + +1. lend the local scratch buffer to the output stream, then keep using it +2. replace `r`, an owned local, with `joined`, another owned local +3. store the local block into the global code-block list + +## what the checker reports + +``` +zc: line 5571: buffer: used after it was given away; owner buffer was transferred on line 5570 (declared on line 5569) +zc: line 5573: buffer: used after it was given away; owner buffer was transferred on line 5570 (declared on line 5569) +zc: line 5589: r: is an owned object and can't be copied into another variable +zc: line 5589: r: still owns an object; overwriting it would leak it +zc: line 5589: buffer: used after it was given away; owner buffer was transferred on line 5570 (declared on line 5569) +zc: line 5590: joined: d object was never given away +zc: line 10572: only a named owned object can be recast +zc: line 10575: only a named owned object can be recast +zc: 8 errors +``` + +the line numbers are into the concatenation, not into `compiler.zc`. subtract +1401 lines: 5570 is `rt.outbuf = m*buffer;`, 5589 is the `previous` line, and +10572 and 10575 are `rt.code_blocks = m*block;` in `syntax_resident`. + +## what was tried + +| change | result | +|---|---| +| `rt.outbuf = buffer;` — drop the `m*` | still reported as a transfer; any owned value assigned into a global transfers, and a second diagnostic appeared at the following line | +| move the scratch buffer to a module global `rbuf`, assign it plainly, borrow it into `rt.outbuf` | accepted; removes five of the eight errors. this is the existing idiom, see `sgb` at `sig_attach` and `ltxt` in the literal pool | +| `word previous = m*r; r = d*joined; rt.free(previous);` unchanged | `initial declarations still cannot copy an owned local`, per BORROW.md line 30 | +| declare `previous` in the block's declaration list, then `previous = m*r;` | `r: is an owned object and can't be copied into another variable` | +| `rt.free(r); r = joined;` — the documented free-then-replace idiom | `joined: is an owned object and can't be copied into another variable`, and `r` is then reported as given away at its next use | + +## is this a borrow checker issue + +yes, and it is worth separating two kinds of gap. + +**a move between two locals has no syntax.** the accepted moves in the +compiler's own source all originate at a call: + +```zc +word p = m*rt.new(capacity); // src/compiler/compiler.zc:644 +buf = m*inc_open(full); // src/compiler/compiler.zc:4632 +dgbuf = chk_resize(dgbuf, dgpos, cap) // src/compiler/compiler.zc:401 +rt.free(d*buf); // src/compiler/compiler.zc:4447 +``` + +an owned value already held in a local can be disposed with `d*`, but it cannot +be handed to another local, and it cannot replace one. the free-then-replace rule +in BORROW.md line 30 covers `rt.free(buffer); buffer = replacement;` — but only +when `replacement` arrives from a call. with a local on the right-hand side the +same rule rejects the assignment and then reports the destination as given away. + +the replacement built here is a genuine local: it is written field by field and +then has to become `r`. no current spelling expresses that. the shortest +workaround is to route the swap through a call that takes both pointers and +returns the survivor, so the move originates at a call result. + +**a local cannot be lent to a global.** the output stream is global state. +redirecting it at a local scratch buffer is a borrow, not a transfer, but every +spelling is a transfer: + +- `rt.outbuf = m*buffer;` transfers, so every later use of `buffer` is a use + after transfer +- `rt.outbuf = buffer;` also transfers +- the three working redirects in the compiler all assign a global or a pointer + derived from one — `rt.outbuf = dgbuf + dgpos + 5;`, `rt.outbuf = sgb;`, + `rt.outbuf = ift + at;`, `rt.outbuf = ltxt;` + +so the scratch buffer has to live at module scope. that is workable here, and it +is what the module-global `rbuf` change adopts, but it costs something the +local version did not: the buffer is shared state for the duration of the call, +so any reentrancy through `methdef` would collide, and the checker cannot see +that the borrow ends at the restore. + +## proposal + +in rough order of value: + +1. allow a move into an existing local when the source is an owned local and the + destination's previous owner is released in the same statement list, generalizing + the free-then-replace rule beyond call results. this alone resolves the + `methdef` reassembly. +2. allow a global to hold a borrow of a local for a bounded region, so an output + stream can be pointed at a scratch buffer without a module-level variable. a + scoped-borrow rule on assignment into a global field would do it, and it removes + the reentrancy hazard that the module-global workaround introduces. +3. give `rt.code_blocks = m*block;` a supported spelling. the error, `only a named + owned object can be recast`, does not describe what is wrong: `block` is named and + owned. it is used again at `here = block + 3;` two lines later, which is the real + constraint, and the diagnostic should say so and point at the later use. + +none of these accept a program that is currently accepted unsafely. each widens +the set of programs the checker can describe. item 3 is also a message bug +independent of the rule change: a wrong diagnostic on a correct-looking transfer. + +## reproducing + +`src/tools/bootstrap-check.sh` rebuilds the two bootstrap stages and prints the +compiler's diagnostics on its own source instead of the word dump. it exits +through `mkgenome` when the image is malformed, which is the same failure `make` +reports. + +``` +bash src/tools/bootstrap-check.sh +``` + +a passing run prints `image ok: <n> bytes`.
\ No newline at end of file diff --git a/docs/BORROW.md b/docs/BORROW.md index 818eea4..10beb84 100644 --- a/docs/BORROW.md +++ b/docs/BORROW.md @@ -41,6 +41,8 @@ the compiler functions, standard library, and language server currently run with the analysis runs with the existing parser, ownership checker, and lifetime records; it does not have a separate source parser or a complete path-sensitive proof. snapshots conservatively join branches and loops. low-level and unknown boundaries can hide behavior, so a quiet diagnostic set is not a whole-program safety proof. zc is single-threaded; shared closure cells do not define concurrent mutation rules. +two completeness limits block the compiler from compiling itself, and are written up in `docs/BOOTSTRAP-OWNERSHIP.md`. an owned value already held in a local has no move into another local; every accepted move originates at a call, so the free-then-replace rule above applies only when the replacement comes from a call result. and a local cannot be lent to a global, so an output stream has to be redirected at a module-level buffer rather than a scratch local. neither limit accepts an unsafe program; both refuse correct ones. + the maintained regressions cover these cases: | case | behavior | diff --git a/src/tools/bootstrap-check.sh b/src/tools/bootstrap-check.sh new file mode 100755 index 0000000..a5de341 --- /dev/null +++ b/src/tools/bootstrap-check.sh @@ -0,0 +1,20 @@ +#!/bin/bash +# rebuild the bootstrap one stage and report what the compiler says about itself. +# zc0 (stage 0) compiles rt+core+compiler into build/s0, s0 becomes zy0, and zy0 +# runs build.zc over the same sources to produce the image. ownership diagnostics +# come back in the image, so print them instead of the word dump. +set -e +cd "$(dirname "$0")/../.." +mkdir -p bin build/s0 build/s1 build/core +cc -O1 -w -fwrapv src/tools/zc0.c -Isrc/core -o bin/zc0 +cc -O1 -w -fwrapv src/tools/mkgenome.c -Isrc/core -o bin/mkgenome +cp src/core/core.c src/core/io_linux.c src/core/memmap.h src/core/fops.h src/core/bops.h src/core/stack.h build/s0/ +cat src/runtime/rt.zc src/core/core.zc src/compiler/compiler.zc | bin/zc0 > build/s0/genome.h +cc -O2 -w -fwrapv -pthread -DJTYPE=int build/s0/core.c build/s0/io_linux.c -o build/zy0 +(cat src/tools/build.zc; printf '`'; cat src/runtime/rt.zc src/core/core.zc src/compiler/compiler.zc) | build/zy0 > build/g1.bin +if ! grep -q '^zc: ' build/g1.bin 2>/dev/null; then + echo "image ok: $(wc -c < build/g1.bin) bytes" +else + echo "--- compiler diagnostics on its own source ---" + cat -v build/g1.bin +fi
\ No newline at end of file |