rocq/backend/EmitInst.v
# Instructions
The code of one instruction of a plan, as filc_amd64.pl's inst//4 and abi_action//4 give it in the reference emission: every temporary in its stack slot, the split bounds check, no inline copies. A form that is not ported yet is a todo line (Layout).
Heap checks
As aux_pointer_mask/1: the low 48 bits of an aux word are the aux pointer; the high 16 are the object's flags.
As aux_bits/2 of special_type and of function.
As write_check//2: a write needs an object that is neither read-only nor free.
As align_check//2.
As access_check//2 with the split bounds: with the pointer in %rax and its lower in %rcx, a jump to the kind's failure block unless the lower is not null, lower <= pointer and pointer + size <= upper, and the flags and alignment permit.
Raw accesses
After its check, an access has its address in %rax and the lower of the pointer in %rcx.
As raw_load//6: a scalar load of the type t at the class k into the temporary d.
As width_value_class/2: the class a store of the width w reads its value at.
As raw_store//6.
As aux_of_lower//0: the aux pointer of the object at the lower in %rcx into %rdx, setting ZF if it has none.
As pointer_load_effect//4: one step of a pointer load's protocol, at the instruction index of the block b.
As pointer_store_effect//6: one step of the protocol of a store of the pointer v at the pointer a. Ensuring the aux may exit, so rooted_reload reads both again from their roots before the lower and then the address are written.
As raw_access//4: the access a at a heap pointer.
Named locals
As local_address//5: the address of the access's aux word into %rdx and of its payload into %rax. The check has passed, so an offset in range and aligned is a constant displacement.
As local_check//6: the exact bounds of the named local x, with no heap lower. The offset and the size are the stack reporter's arguments; the address is formed only after the check.
As local_raw_access//4: the access a at a named local, with the payload address in %rax and the aux word's in %rdx. Only what a pointer load reads or a pointer store writes has a heap lower.
Values
As integer_inst//5: the op's value in %rax, then into the temporary d.
As span_end//2: the pointer in %rax plus off, modulo 2^64, into the register r.
As the span_test clause of kind_inst//8: 1 when the lower of p is not null and lower <= p + lo < p + hi <= upper, unsigned; else 0. It reads only what a full check reads and never traps.
As kind_inst//8: the temporary d, of class k, is o of args, at the instruction index of the block b.
As flight_address_load//3: an address operand of a flight into the short register r.
As shared_lower/3: the flight d's lower is the root of its donor, which already holds it.
As the flight clause of inst//4: every input is read before the destination is written. The second address goes by %rdx; %rcx holds the lower.
Calls
As word_reg_load//4: a word of a call into the short register r.
As typed_stack_args//4: the words that travel on the stack, through %rax.
As typed_register_args//4.
As entry_call//4: the entry registers and the call of a fast entry: of the operand callee, or without one of the function object whose lower is in the aux slot. A buffered return's buffer sits above the pop bytes of stack words.
As fast_call//4: the arguments, the entry registers and the call, in the fast convention.
As reg_slot_stores//3.
As buffer_slot_copies//3: each word of a returned buffer into its slot.
As typed_result_gprs//3 and typed_result_xmms//3, over the registers result_registers/2 gives a returned tuple's words. The integer registers are stored first, since a float goes to its slot through %rax.
As typed_result_stores//3, with result_registers/2.
As fast_result//3: the exception flag, then the results from their registers or the buffer into their slots.
As function_check//1: with a pointer in %rax and %rcx, a jump to fail unless it is the address of a function object.
The generic packet: 32 cells are inline in the thread.
As cell_stores//2: the argument cell i from %rax and its lower from %rcx, with the thread in the register t: in the inline buffers, or past them in the outline ones, by %rsi.
As generic_call_args//3: each argument into the thread's generic argument area.
As outline_ensure//3: a packet of more than the inline bytes needs the thread's outline buffers to hold the rest, before any cell is set.
As generic_slot_copies//2: a generic return's words, from the thread at %rsi, into their slots.
As generic_results//3, with rets_check//2: the check that the generic return's size in %rdx is at least need, then the result cells.
As indirect_call//10: a call through a checked function, whose lower is in the aux slot and in %rcx: the fast entry if its signature is the call site's, else the generic entry, with each argument a cell of the thread's packet.
Actions
As target_operand/2.
As the plain getter clause of abi_action//4: the call of a symbol's getter, which gives its address in %rax and %rdx.
As va_arg_load//5: the helper has left the address of the argument's payload in %rax and of its aux word in %rdx; both are read with no safepoint between.
As zero_words//2: n zero words from off(%rbp) up.
As abi_action//4, for the actions of an instruction. The reference emission copies nothing inline, so a copy's filter and join are empty.
Instructions
The pointer an access is at.
As inst//4: the code of the instruction at index i of the block b.