rocq/backend/Plan.v
The ABI plan of a function, as filc_abi.pl's abi_function/10 states it before any register or frame offset is chosen: a frame of named slots, entry actions, blocks whose calls, getters and returns are lists of ABI actions, and the function's public object. It is what Fuse.v and Abi.v build and what instruction selection reads.
The instructions inside it are Syntax.v's, the model's own: the plan adds only the forms the checked IR has no term for, which are a check fused with its access, a reused proof, and abi(Actions). PlanTerm.v writes a plan as the term the Prolog compiler prints for it.
f of every element of xs, or nothing if any has none.
Fused instructions
Where a fused access is: at the pointer P its check proved, or at local(X, Off), the named local x plus off, which check_local proves.
| | | ALoad | let(tmp(D), K, raw_load(T, Off), [P]) | |
| | | AStore | raw_store(W, Off, V, P) | |
| | | ALoadPointer | let(tmp(D), p, raw_load_pointer(Off, Es), [P]) | |
| | | AStorePointer | raw_store_pointer(Off, V, P, Es) | |
| | | ATouch | p : place | touch(P): the check alone, with no access after it |
An instruction after fusion (filc_amd64.pl's fused_blocks/5).
| | | FPlain | i : inst | an instruction of the checked IR, unchanged |
| | | FFused | fused(Check, Access): a check and the access it proves, at one index | |
| | | FReused | a : access | reused(Access): an access under an earlier check's proof, with no check |
| | | FCall | fused(check_function, call(Res, P, Args)) |
The temporaries a place reads: its pointer, if a temporary.
The temporaries an access reads.
The temporary an access defines, with its class.
As cfg:inst_uses/2 of live_inst/2: the temporaries a fused instruction reads, as liveness and the frame layout see it: the bare access at its checked pointer, or the call of the checked pointer. The proof is not among them: it is a register value and has no slot.
As cfg:inst_def/2 of live_inst/2: the temporaries a fused instruction defines, each with its class.
Frames
A pool of the frame's slots (frame_slots.pl): PoolScalar holds the w, l, s and d temporaries, PoolPointer the p ones, each slot an address and its lower, and PoolWide the x ones.
| | | PoolScalar | ||
| | | PoolPointer | ||
| | | PoolWide |
The name of something a frame holds.
| | | KTmp | n : name | tmp(N): the payload of the temporary n |
| | | KShadow | n : name | shadow(N): the copy of the phi n that an edge's parallel moves read |
| | | KStorage | p : pool i : Z | storage(Pool, I): the slot i of a pool |
| | | KThread | thread: the saved thread pointer | |
| | | KAux | aux: a scratch word | |
| | | KRetbuf | retbuf: the caller's return buffer | |
| | | KLocal | x : name size : Z | local(X, Size): the bytes of a named local |
| | | KLower | k : key | lower(K): the capability beside the address K, a root |
| | | KStackAux | x : name | stack_aux(X): the aux of a named local, a root |
As frame(Plain, Roots, Aliases): the payload slots, the roots the collector scans, in order, and the slot each temporary's payload or lower is kept in.
Words, cells and results
How a function returns: registers, or buffer(N), through a buffer of n words when more than two integer words come back.
| | | Registers | ||
| | | Buffer | n : Z |
Where a fast word comes from or goes.
| | | SrcSlot | k : key | a parameter's slot, tmp(N) or lower(tmp(N)) |
| | | SrcAddr | v : value | addr(V): the address of the pointer v |
| | | SrcLower | v : value | lower(V): its capability |
| | | SrcVal | val(K, V): the value v at class k | |
| | | SrcData | i : Z | data(I): the data word of the generic cell i |
| | | SrcAux | i : Z | aux(I): its aux word |
| | | SrcSnapshot | snapshot: a variadic entry's promoted argument packet |
As wf(K, Source): one word of a fast call, at the class k (l for both words of a pointer).
What a generic cell holds: a value, or saved(W), the fast word w a thunk saved.
As cell(I, K, Source, Lower): the eightbyte i of a generic packet, with the capability beside it if it is a pointer.
| | | Cell |
The channels a fast call's results come back in.
| | | ChSlots | ks : listkey | slots([...]): integer words, to these slots |
| | | ChFloat | float(K, tmp(D)): one float | |
| | | ChTyped | typed([K-Slot, ...]): a tuple with a float in it |
A direct call's signature in its symbol: its number, or never(R-A) for a call of more than 16 words, which has no fast signature.
| | | SigNumber | n : Z | |
| | | SigNever | r a : Z |
What a direct call invokes.
| | | TImplementation | f : name sig : Z | implementation(F, Sig): the private body of a function of this module |
| | | TEntry | entry(F, Sig): the weak thunk of this symbol and signature |
The getter that gives a symbol's address.
| | | GetLocal | s : name | local_getter(S): this module defines s |
| | | GetWeak | s : name | weak_getter(S): declared weak; may be null |
| | | GetExternal | s : name | external_getter(S) |
Actions
One step of an abi(Actions) instruction. Each list of them occupies the one index of the instruction it lowers.
| | | AOrigin | origin(c): record the catching origin before a safepoint | |
| | | AReserveResult | r : protocol | reserve_result(R) |
| | | AInvoke | invoke(Target, R, Words) | |
| | | AResult | result(R, Channels) | |
| | | AReleaseResult | r : protocol | release_result(R) |
| | | ACopyFilter | copy_filter(D, S, N, Res): a small memcpy's inline filter | |
| | | ACopyJoin | copy_join | |
| | | ADispatch | ||
| |||
| | | AGetter | getter(G, c, D) | |
| | | ASnapshotCursor | off : Z d : name | snapshot_cursor(tmp(hidden(va_snapshot)), Off, D) |
| | | AConsumeVa | consume_va(K, P, Size, D) | |
| | | AInitializeLocal | x : name | initialize_local(X) |
An instruction of a plan: a fused instruction passed through, or abi(Actions).
The jump that ends a plan's block: a jump of the IR, or abi_return(Actions), the actions of a return.
| | | PJump | j : jump | goto, branch or unreachable, unchanged |
| | | PReturnValue | [return_value(Ret, V), pop_frame, success(P)] | |
| | | PReturnBuffer | ws : listword | [return_buffer(Words), success_buffer, pop_frame, native_return] |
| | | PReturnTyped | [return_typed(Ks, Vs), pop_frame, success(registers)] | |
| | | PReturnRegisters | vs : listvalue | [return_registers(Vs), pop_frame, success(registers)] |
| | | PReturnVoid | p : protocol | [pop_frame, success(P)] |
A block of a plan.
Public objects and thunks
The channel a generic adapter takes the fast result from.
As adapter_result(R, Channel, Size, packet(Copies, Zeros)): how an adapter turns a fast result into a generic packet of size bytes: the words it copies and those it zeroes.
A function's public object.
| | | FastAndGeneric | ||
| |||
| | | GenericOnly | ||
generic_only(promote_incoming(Need, Words, Result)): a variadic function
How a thunk refers to its callee.
| | | RefWeak | ||
| | | RefLocal | ||
| | | RefStrong |
As thunk(F, Ref, Sig, Words, Cells, ArgsSize, Result, Need): the weak thunk of a symbol and signature that the module calls directly and does not define.
| th_name | : name | |
| th_ref | ||
| th_sig | : sigref | |
| th_words | : listword | |
| th_cells | : listcell | |
| th_args_size | : Z | |
| th_result | ||
| th_need | : Z |
The plan
As abi_function(Name, Linkage, Ret, Sig, Frame, Entry, Blocks, Exit, Object, Origins). The entry actions, the exception exit and the origins have one shape each, so the plan keeps what they vary in: the return protocol, the words received, the payload slots a setjmp would snapshot, and the numbers of roots and named locals.