rocq/backend/EmitData.v
# Data objects, thread-local data, table entries and aliases
The lines of a module item that is not a function, as filc_amd64.pl's item//2 gives them for data(Name, Linkage, Align, Items) (data_object//4, thread_local_object//4, init_entry//4, a weak declaration) and alias_getter//4 for alias(Name, Linkage, Target).
Emission is total: where the Prolog compiler's goal would fail or throw, the lines hold a todo line (Layout.v) in that place.
Lines
type(S, Kind).
size(S, N).
section(S).
As linkage_globl//2, of a linkage kept as its term. Emit.v's linkage_globl gives no line for a term the Prolog has no clause for; this one gives a todo.
Aux words
A flag of an object's aux word.
| | | FlGlobal | ||
| | | FlReadonly | ||
| | | FlGlobalAux | the aux array is static data | |
| | | FlFunction | special type 1, function | |
| | | FlSpecialType | the special type field, bits 7-10 |
As object_flag/2.
The bit at which an aux word's flags start: its low 48 bits are the aux pointer.
As aux_bits/2: the flags in an aux word.
Proof 1 step Qed
As linkage_flags/3: a data object's linkage, kept as its term, and the flag readonly if it is read-only. Nothing for a linkage that is not a data object's.
As memberchk(readonly, Flags).
The payload
As r(Offset, Symbol, Addend): the pointer at an offset of a payload is the symbol's plus the addend.
The byte numbers of an x87 extended float, as numlist(0, 9, Is).
Whether a character code is a byte.
As payload_item/4 and value_payload/5: the payload directive of the item at the offset off, the offset after it, and rs with a relocation added if the item is a pointer, whose slot stays 0 until the relocation fills it in. The directive is a todo where the Prolog fails (an item of no clause) or throws (a pointer that is not 8-aligned), and for a string with a character that is not a byte, which .ascii cannot hold.
As foldl(payload_item, Items, Payload, Off0-Rs0, Off-Rs): the payload directives of the items from the offset off, the offset after them, and their relocations in front of rs, the last first.
As template_needed/1: some byte of the items is not zero, so the fresh (zeroed) object needs a copy of them.
Relocations
As reloc_node/3: the label of the constexpr node of relocation i of the data object name.
As reloc_entries//3: the relocation table, each entry {u64 offset, u32 kind, pad, target}: kind 0 calls a getter, kind 1 a constexpr node. rs are the relocations from the ith.
As reloc_nodes//3: the constexpr node {u32 add-immediate = 0, u32 0, getter, u64 addend} of each relocation with an addend. rs are the relocations from the ith.
As relocations//2.
As relocs_aux_word/4: the aux word of a global data object with the relocations rs and the other flags: its flags, and its static aux array da if it holds pointers.
As aux_array//5: the aux array da of size bytes and the relocation table relocs, if there are relocations.
As relocations_call//3: the getter's call that runs the relocations, if there are any, of the data object dobj from the table relocs.
Data objects
As data_object//4, as clang lays out globals: the object {upper, aux} then the payload rounded up to 8 bytes, a 16-byte cache, an aux array if the payload holds pointers, and a getter whose slow path registers the object and runs the relocations that fill in its pointers. A payload aligned to more than 16 has align - 16 zero bytes before the object, so that its payload is aligned.
Thread-local data
As thread_local_object//4, as clang lays it out: a .tbss word holding this thread's payload address, null until the thread first asks, and a getter that returns it or calls the slow path. The slow path allocates the thread's object, copies the initializer's bytes from a template and runs its relocations, as a global's slow path does, then sets the word.
The Prolog fails on an item its payload has no directive for before it gives any line. Here the payload's todo lines stand where the template would be when no template is needed, so that they are never dropped.
Constructor and destructor table entries
As init_runtime/2: the runtime function a table entry of the kind hands its function object to, and whether the kind is ctor.
The priority of section(init(Kind, Prio)): none for the atom none, else the integer or atom; nothing for a term asm.pl has no text for.
As init_entry//4: a constructor or destructor table entry, as clang's Fil-C emits one: a native forwarder in the .init_array or .fini_array section, which hands f's function object to the runtime to call.
Items
As item//2 on data(Name, Linkage, Align, Items).
Whether the module defines the name target with a linkage that keeps its getter local: a local function, or local, ro(local) or tls(local) data.
As alias_getter//4, with sy the symbols of the module: an alias's getter returns its target's getter's result, so the alias's function or data object is the target's. It calls the target's getter, directly when the target is local, else through the PLT, with the stack kept 16-aligned.