rocq/backend/Layout.v
Where a function's plan lives below %rbp, and the names its code uses: filc_amd64.pl's layout/4, its function context, its labels and abi_symbol/3, with the short ways to write a line that the emission (Emit.v and the files it calls) is built from.
Emission is total: where the Prolog compiler would fail or reach a form this port does not have yet, the code holds a todo line, which is not an instruction. The driver emits no function that has one.
Lines
The mnemonic of a todo line.
A place in the code for what, which this port does not emit: a form not ported yet, or one the Prolog compiler has no code for (a slot the frame lacks, a class an operation does not take).
Whether a line is a todo.
The first thing lines leave undone, if any.
Names
The text of a name as format's ¬w writes it: an atom or an integer as it is, anything else in canonical form.
As abi_symbol/3: the names under which code finds a function f or a global: its implementation for the signature sig and the public alias of it, its getter, its function object, its data object and aux array.
As struct_field/3: the offsets of the thread's fields and of a function object's.
The frame
n rounded up to a multiple of 16.
Where a named local is: its payload at -payload(%rbp), 16 aligned, and its aux, a count and then a lower for each word, at -aux(%rbp).
| ls_payload | : Z | |
| ls_aux | : Z | |
| ls_size | : Z | |
| ls_padded | : Z |
As ctx(f(Name, Ret, Slots, Blocks), Size, FrameBase, Labels, _): what the code of a function reads of it. A slot's number n means -n(%rbp). The frame record the collector walks is at -base(%rbp): its parent, its origin, then lowers[ ].
| cx_name | : string | the function's name, the stem of its labels |
| cx_slots | : nmapZ | each key's slot, by key_term |
| cx_locals | each named local, by its name | |
| cx_size | : Z | the bytes subtracted from %rsp |
| cx_base | : Z | |
| cx_phis | each block's phis, by its label |
As plain_slot/3: place one payload key after off bytes.
As lower_slot/4: the root k is lowersi.
As layout/4 and function_ctx/8: the context of a plan. An alias whose key has no slot gets none.
As ctx_slot/3.
The lines f gives for k's slot.
As reg_slot_store//3: the store of the register r into k's slot.
As slot_reg_load//3: the load of k's slot into the register r.
Labels
As special_label/3: a label shared by the whole function.
As block_label/3.
As local_label/5: a label inside the code of the instruction index of a block, or of its jump.
As origin_label/3: the frame's origin, which is c at calls and n at pollchecks and checks.
Registers and values
As reg_name/3: the name of the short register r at a class, as integers have it; a float's bits travel in the same registers.
Whether a class is 32 bits wide in a register, or 64; nothing for the classes with no register form.
As att_suffix/2 at a class.
As amd64.pl's load//4: the code that puts the value v, read at the class k, in the short register r. A global's address is the same at every class.
As lower_reg_load//3: the lower of a p value into the register r: its root's, or 0 for a constant.
As flight_load//2: a p value's address into %rax and its lower into %rcx.
As flight_store//2: the pointer in %rax and %rcx into the temporary d and its root.
As origin_store//2: the store of the c or n origin into the frame record.
As to_xmm//3 and from_xmm//3: a float's bits between the short register r and an xmm register.
As target_form/2: the bytes of stack a buffered return of n words takes around a call.
More operands
D(%B,%I).
S+N(%rip).
*O, the target of an indirect call.
The fast convention
As form_short_regs/2: the integer registers that carry a call's words, by the return's protocol. A buffered return's buffer takes %rdx's place.
Where a word of a call travels.
| | | LocReg | r : string | the short register r |
| | | LocXmm | x : string | an xmm register |
| | | LocStack | i : Z | the stack word i, at 8i(%rsp) at the call |
As amd64.pl's float_class/1.
The register of a word of a returned tuple: gpr(G) or xmm(K, X).
As result_registers/4: integer words in the registers gs in order, float words in xs. A float word with no xmm register left takes an integer one, as the second clause gives it; nothing if the integer ones run out.
A tuple's third float word has no xmm register and takes an integer one.
Proof 1 step Qed
As bank_locations/7: each class's location, then the count of stack words and of xmm registers.
As stack_bytes/2: n stack words keep %rsp 16 aligned.
Check kinds
As k(Size, Write, Align): what an access check tests, which names its failure block and its origin.
| ck_size | : Z | |
| ck_write | : bool | |
| ck_align | : Z |