rocq/backend/Abi.v
Fil-C ABI lowering (filc_abi.pl's lower_function/4 and lower_thunks/2): the plan of a checked function, before any register or frame offset is chosen. Its frame names payload slots, ordered roots and aliases; a call, a getter or a return becomes a list of ABI actions in the place of the instruction it lowers; and the function's public object says how a generic caller reaches it.
Fast words split a pointer into its address and its lower; generic cells are one eightbyte a value. registers or buffer(N) is the return protocol. Nothing here knows a native location.
The first version shares the frame's pools and gives every temporary and phi a slot of its own kind, as the Prolog compiler does without −O; it has no setjmp sites.
Signatures
As class_digit/2: the digit of a word of the class k in a signature: 0 for an integer, 7 for a pointer, 1 and 2 for the floats. Other classes have none.
As bijective_value/2: the digits ds, the first the least, as a number in bijective base 11.
As never_signature/1: the signature no function object has, for more than 16 argument words. A call with it always goes generic.
As ret_kinds/2: the classes a function of the return type r returns.
As word_codes/3: the bijective values of the return digits and of the argument digits of a function returning r on parameters of the classes ks.
As signature/3: Fil-C's fast-call signature number, 1 + R + 133 * A, or the never_signature for more than 16 arguments. It names private bodies.
As return_protocol/2: how a function of the return type r returns: through a buffer if more than two integer words come back, a pointer being two. Float words return in registers of their own.
As result_ret/2: the return type a call reading the result r expects.
Symbols
What a call needs of a function the module defines: its linkage, its own signature if it has one, and whether it is variadic.
As module_symbols/2: a module's functions and data by name, the first of a name, and the names it declares weak.
The fentry of a function outside the core subset, read off its term t.
As module_symbols/2.
Whether the term t is the atom a.
As weak_defined/2: the module defines the name n with linkage weak or ro(weak), so another object's definition may replace it.
As direct_target/4: what a direct call of f at the call-site signature sig invokes: the private body, under the callee's own signature, if the module defines f, not variadic and not weak; else the weak thunk of f and sig.
As getter_target/3: the getter of the symbol s: this module's if it defines s and not weakly, a weak one, which may give null, if it declares s weak, else an external one.
Frames
The standard order of two N − K pairs, a temporary and its class.
The destination of a phi and its class.
As storage_keys/3: storage(Pool, I) for i from 0 up to n.
As body_params/3: the parameters of the private body of f: a variadic function's has the hidden pointer to the promoted packet last.
As frame/6: the frame of a body with the parameters ps and the fused blocks bs, returning by ret; with it, the payload keys a setjmp would snapshot and the number of named locals.
The plain keys are the slots of the pools, a shadow for each phi, thread, aux, the return buffer if there is one, and the named locals. The roots are the lowers of the pointer slots and of the pointer phis' shadows, then the stack auxes of the locals, the last root group, as the collector's origin says.
Words and cells
As fast_params/2: the words a body receives for the parameters ps: a pointer is its address and its lower, both at l.
As fast_args/2: the words of a fast call's arguments.
As payload_class/2: the class of a value's data word in a generic packet.
The elements of xs, each with its index from i.
As generic_args/2: the cells of a generic call's arguments, one a value, a pointer's with its lower.
As generic_params/2: the words a generic packet holds for parameters of the classes ks: a pointer's data and aux, another value's data.
As result_tos/2: the results a call reads.
Whether k is a float class a register returns: s or d.
As fast_result/2: the return protocol and the channels of a fast call's result r. One float has a channel of its own; a tuple with a float names each slot's class; anything else is integer words, a pointer two.
As generic_result/2: the bytes a generic call's result r needs and the cells it comes back in.
Instructions
As call_signature/3: the signature of a call reading r on the arguments args.
As call_symbol_signature/4: the signature in the name of the weak thunk a direct call goes through. Every call of more than 16 words has the never signature, so its thunk is named by the whole word list.
As small_copy/5: the inline filter of a call of f that is a memcpy or memmove of a constant 1 to 16 bytes, if the module defines neither: the emitter may test for the common case in front of the unchanged call.
As lower_inst/4: the fused instruction i lowered. A direct call invokes its target's fast entry; a call of a checked function pointer dispatches on the signature, fast or generic; a symbol's address comes from its getter; va_args and va_arg read the promoted packet; a local's declaration initializes it. Every other instruction passes through.
As lower_jump/4: the jump j of a function returning r by the protocol ret. A return's values are in place before the roots are popped, and no safepoint comes between.
As lower_block/6.
Public objects
As adapter_return/2: how an adapter turns the fast result of a function returning r into a generic packet. The void result is one zero word.
The words zeroed are the aux of each cell that holds no pointer, whatever else comes back: tuple([l, s]) zeroes aux(0) and aux(1), so no stale aux word of the caller's reaches a result read as a pointer.
As public_object/3: the public object of the function f: a fast entry under its signature and a generic adapter, or, for a variadic function, a generic entry that promotes the incoming packet.
The plan of a function
As lower_function/4 of the function f after fused_blocks/5: its plan, with sy the symbols of its module. Nothing if the function is outside what the first version lowers, as one that calls setjmp is: its frame keeps a snapshot and a hidden buffer for each site, which nothing here builds.
Thunks
A direct call that goes through a weak thunk: the callee, the signature in the thunk's name, and the call's return type and argument classes.
A signature in a symbol as its term: the number, or never(R-A).
As t(F, Sig, Ret, Ks), the term lower_thunks/2 sorts thunk calls by.
The thunk call of a direct call of f returning r on arguments of the classes ks, if its target is a thunk and it has a signature.
The return type the term t of a call's result expects: void, result(_, K) or tuple([result(_, K), ...]).
The thunk calls among the instruction terms of a function outside the core subset, whose term is t: its direct calls, call(Res, global(F), Args), as lower_thunks/2 reads them.
The thunk calls of a module: those of every direct call in it.
As one_per_symbol/2: of the sorted calls cs, the first of each symbol and signature.
As thunk_cells/4: the generic cells of a thunk for parameters of the classes ks, the value i from the fast word w the thunk saved; a pointer takes two words.
As lower_thunk/3: the plan of the weak thunk for the call c. It is weak if the callee is declared weak, since its getter may be null; local if this module defines the callee with local linkage, so that the thunk never merges with another object's; else strong.
As lower_thunks/2: the plans of the weak thunks the module md needs, one for each symbol and signature of a direct call to a function it does not implement, in the standard order of t(F, Sig, Ret, Ks).