rocq/backend/EmitThunk.v
# Weak thunks
The lines of a weak thunk from its plan (Plan.v's thunk), as filc_amd64.pl's thunk//1 gives them. The thunk resolves its symbol through the getter and calls the fast entry when the callee's signature is the call's, else it transports its words as generic cells and the generic result back.
Every incoming word is saved below %rbp before the getter can clobber it: word i at -32-8i(%rbp). %rbx holds the thread, %r12 the return buffer of a buffered return, and -24(%rbp) the callee's function object.
Where the Prolog compiler has no clause for a form, the lines hold a todo (Layout.v) in that place.
The words a thunk saves
As never_signature/1: the signature no function object has, which a call of more than 16 words is compared with, so that it always goes generic.
The offsets, below %rbp, of the first saved word and of the callee's function object.
As saved_operand/2: the fast word saved(I) is at -32-8I(%rbp). A cell of a thunk holds nothing else.
As saved_words/3: each word's class and where it is saved, the first at the index i.
As mixed_thunk_thread//1: the thread into %rbx. A buffered return has its buffer in %rdi, kept in %r12, and the thread in %rsi, which the getter takes in %rdi.
As incoming_bits//2: the word at a location of the fast convention into %rax; a stack word is at 16+8I(%rbp).
As save_mixed_words//3: each incoming word to where it is saved. An integer stack word is copied whole, as a register one is: w and l share a signature digit, so a thunk emitted for a 32-bit call also serves another object's 64-bit calls.
The callee
The getter's call, as thunk_getter(strong, Getter, G): the callee's function object in %rax and %rcx.
As thunk_getter//3. The getter of a weak declaration may be null, and then so is the object: the function check fails, as clang's thunk does.
As mixed_thunk_call//1: the call of the fast entry of the object at -24(%rbp), with the thread, and before it the buffer of a buffered return.
The generic call
As outline_ensure_rdi//2: with the thread in %rdi, a packet of more than the inline bytes needs the thread's outline buffers to hold the rest.
As thunk_outline_ensure//2.
As operand_thread_store//2: the operand into the thread at an offset, through %rax if it is in memory.
One cell of saved_generic//1: an inline cell goes straight to the thread at %rbx, a later one through cell_stores//2 into the outline buffers. A cell with no lower gets a zero one.
As saved_generic//1: the saved words into the cells of the generic packet.
The generic return
As rets_check//2: the check that the generic return's size in %rdx is at least need, with a call of filc_cc_rets_check_failure if it is not.
As thunk_typed_loads//2: each word of a returned tuple from its thread offset into its register, a float through %rax.
As thunk_reg_loads//2: each generic return word, at its thread offset, into its register.
As thunk_generic_reg_words//4: the result words, if the channel has any, in %rdx and %rcx, or %xmm0 and %xmm1.
As thunk_buffer_copies//2: each generic return word, at its thread offset, into the return buffer at off(%r12).
As thunk_generic_return//7: after the generic entry's call and the test of its exception flag, the return of its result words, at the thread offsets srcs, then a jump to out. A buffered return's flag is the buffer's first byte.
The thunk
The value a thunk compares the callee's signature with.
As thunk//1.
The third word is saved at -48(%rbp).