lowers_check.pl
The GC-root contract of a frame, checked: at every point of every reachable block, each live pointer temporary's lowers[] entry holds its current lower (docs/lowers.md). The collector marks the object of every lower in the frame record at each safepoint, so a live pointer whose entry held anything else could lose its object.
check_lowers/4 validates the frame filc_abi.pl built, whatever chose it: it does not ask which flights lower_roots.pl derived or how frame_slots.pl pooled the slots, only what each instruction writes.
Facts
| Fact | Holds at a point when |
|---|---|
holdsE, Ns | on every path here, entry E was last written with a lower that is the current lower of each name in Ns |
The state maps each entry to its Ns; an absent entry holds nothing known. Every name is only ever added to its own entry's Ns.
Transfer
| Event | Effect |
|---|---|
| entry | each p parameter N, in order: holds(E(N), [N]) |
a phi or an instruction defining p temporary N | holds(E(N), [N]) |
flighttmpN, _, _, lowertmpP, P ≠ N, E(P) = E(N) | emits no store (filc_amd64.pl); requires P in E's Ns, then adds N |
on the edge from B, a p phi N whose inputs are all temporaries with entry E(N) | copies no lower; requires the input V from B in E's Ns at B's end, then adds N |
Nothing else writes a temporary's entry: the runtime writes lowers[] only in zlongjmp, and a function with setjmp must give every pointer an entry of its own (today's discipline). Calls, polls and helpers only read it. Shadows, stack-aux, snapshot and jmpbuf roots are other entries.
Merge and check
A block's state is the meet of its reachable predecessors': per entry, the names in all of them. Then each live pointer (cfg.pl's liveness, refined per instruction) must be in its entry's Ns: before each instruction, after the last one (live out and the jump's uses, where an edge's poll would see them if it polled first) and before the first after the phis (where an edge's poll does see them). Unreachable blocks are not checked; they never run.
Frame = frame(Plain, Roots, Aliases), filc_abi.pl's, satisfies the contract above for function Fn with body parameters Params and the liveness view LiveBlocks. Throws nanofil_error otherwise.
A temporary's entry: the root its lower key names, through Aliases.
Outs maps each reachable block to its state after its last instruction, the greatest fixpoint from top (an unvisited predecessor is ignored by the meet).
the meet of the states its visited predecessors' edges leave, after L's phis, and the parameters' at the entry block.
Phi's write on the edge from From. A phi whose inputs all have its entry copies no lower (filc_amd64.pl), so its input from From must hold there.
Inst's writes of entries. Only a flight whose donor has its entry is no write (filc_amd64.pl emits none), and only when the donor's lower is there.
every live pointer holds at every point of Block.
the live set before each instruction, walking them backwards from the set After the last.
Every live name is defined somewhere, and a live pointer holds.