1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
|
# the bootstrap did not compile: owned values could not be moved between locals
status: resolved. the analyzer gained the two rules proposed below and a clearer
recast diagnostic, and `make genome` reaches its fixpoint from a clean checkout.
see "resolution" at the end; the rest of this note is the record of the problem.
affects: `make genome` and the `fixpoint` 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. `mkgenome` then read 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`.
## resolution
the analyzer (`src/compiler/compiler.zc`) now accepts the three spellings:
1. **moves into a released owner.** `rt.free(r); r = joined;` moves `joined` into `r`
when `r` was released first and `joined` is an owner of the same block or a deeper
one. `joined` is retired by the move. a destination that still owns something is
still rejected (`still owns an object; overwriting it would leak it`), and so is a
copy of an owner into a fresh declaration.
2. **bounded lends to globals.** `g = m*x;` with `x` an owned local lends `x` to `g`:
`x` keeps ownership and stays usable, and the lend ends when the same block assigns
`g` again. giving `x` away, returning, breaking or leaving the block while the lend
is open is an error (`is lent to global g; assign the global again before ...`). the
lend list is per function and per block depth (`lend_add`, `lend_clear`,
`lend_exit`), so a restore inside a nested branch does not end a lend made outside it.
3. **recasts of plain locals.** `rt.code_blocks = m*block;` failed because `block` came
from `chk_resize`, which returns collector-managed storage, so `block` never owned
anything. the compiler now writes `rt.code_blocks = block;`, and a recast of a plain
local reports `block: isn't an owned object, so there is no ownership to recast`
instead of the old message.
`methdef` uses the lend for its scratch buffer and the move for the joined token list.
the regressions are `tests/programs/ownmove.zc` and `tests/errors/lend_*.zc`,
`recast_plain.zc` and `move_live_owner.zc`.
|
