Fil-C on Nix

Filnix wiki

the formal campaign

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.

From Stdlib Require Import String ZArith List Bool Ascii
From Nanofil Require Import Term Syntax Maps
From Backend Require Import Text Asm Plan Abi Layout EmitObject Emit
Import ListNotations
Open Scope string_scope
Open Scope Z_scope
Open Scope list_scope

Lines

type(S, Kind).

23Definition type_lines kind : string : line ≔

size(S, N).

26Definition size_lines : string n : Z : line ≔

section(S).

29Definition section_lines : section : line ≔

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.

34Definition data_linkage_globll : term s : string : listline ≔

Aux words

A flag of an object's aux word.

45Inductive object_flag_name: Type ≔
|FlGlobal
|FlReadonly
|FlGlobalAux
the aux array is static data
|FlFunction
special type 1, function
|FlSpecialType
the special type field, bits 7-10
53Definition object_flagf : object_flag_name : Z ≔
match f with

The bit at which an aux word's flags start: its low 48 bits are the aux pointer.

64Definition aux_flags_shift: Z ≔
48

As aux_bits/2: the flags in an aux word.

67Definition aux_bitsflags : listobject_flag_name : Z ≔
Z.shiftlfold_leftλsum f ⇒ Z.lorsum object_flagf flags 0 aux_flags_shift
Proof 1 step Qed
reflexivity

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.

77Definition linkage_flagslk : Syntax.linkage : optionterm × listobject_flag_name ≔
match lk with
⇒
Somel, FlReadonly
⇒
SomeTAtom"export", [ ]
⇒
SomeTAtom"local", [ ]
⇒
SomeTAtom"weak", [ ]
⇒
None

As memberchk(readonly, Flags).

87Definition has_readonlyflags : listobject_flag_name : bool ≔
existsb
λ f  ⇒
match f with
⇒
true
_
⇒
false
flags

The payload

As r(Offset, Symbol, Addend): the pointer at an offset of a payload is the symbol's plus the addend.

94Record reloc: Type ≔ mkReloc
r_off
 : Z
r_sym
 : name
r_addend
 : Z

The byte numbers of an x87 extended float, as numlist(0, 9, Is).

101Definition extended_bytes: listZ ≔
0; 1; 2; 3; 4; 5; 6; 7; 8; 9
103Definition byte_mask: Z ≔
255
104Definition byte_count: Z ≔
256

Whether a character code is a byte.

107Definition is_bytec : Z : bool ≔
0 ≤? c && c <? byte_count

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.

116Definition payload_itemit : data_item off : Z rs : listreloc : listline × Z × listreloc ≔
match it with
⇒
zeron, off + n, rs
Strcs
⇒
forallbis_byte cs
→
DirDAsciimapλc ⇒ ascii_of_natZ.to_natc cs
else
todo"string character is not a byte"
off + Zlengthcs
rs
Syms addend
⇒
off mod eight =? 0
→
else
todo"pointer data item is not 8-aligned"
off + eight
mkRelocoff s addend :: rs
⇒
match mapλi ⇒ LIntZ.landZ.shiftrn eight × i byte_mask extended_bytes with
b :: bs
⇒
[ ]
⇒
todo"extended float bytes"
off + 10
rs
Itemw n
⇒
let bytes ≔ width_bytesw in
let u ≔ n mod Z.shiftl1 eight × bytes in
bytes =? 1
→
bytes =? 2
→
bytes =? 4
→
bytes =? eight
→
else
todo"data item width"
off + bytes
rs
⇒
todo"data item", off, rs

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.

150Fixpoint payload_itemsits : listdata_item off : Z rs : listreloc : listline × Z × listreloc ≔
match its with
[ ]
⇒
[ ], off, rs
it :: its′
⇒
let 'l, off1, rs1 ≔ payload_itemit off rs in
let 'ls, off2, rs2 ≔ payload_itemsits′ off1 rs1 in
l ++ ls, off2, rs2

As template_needed/1: some byte of the items is not zero, so the fresh (zeroed) object needs a copy of them.

162Definition template_neededitems : listdata_item : bool ≔
existsb
λ it  ⇒
match it with
Item_ n
⇒
negbn =? 0
Strcs
⇒
existsbλc ⇒ negbc =? 0 cs
_
⇒
false
items

Relocations

As reloc_node/3: the label of the constexpr node of relocation i of the data object name.

173Definition reloc_nodename : string i : Z : string ≔
".Lpizlonated_" ++ name ++ "..node" ++ decimali

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.

179Fixpoint reloc_entriesrs : listreloc i : Z name : string : listline ≔
match rs with
[ ]
⇒
[ ]

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.

192Fixpoint reloc_nodesrs : listreloc i : Z name : string : listline ≔
match rs with
[ ]
⇒
[ ]
r :: rs′
⇒

As relocations//2.

205Definition relocationsrs : listreloc name : string : listline ≔
reloc_entriesrs 0 name ++ reloc_nodesrs 0 name

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.

211Definition relocs_aux_wordrs : listreloc flags : listobject_flag_name da : string : expr ≔
match rs with

As aux_array//5: the aux array da of size bytes and the relocation table relocs, if there are relocations.

220Definition aux_arrayrs : listreloc da : string size : Z relocs name : string : listline ≔
match rs with
[ ]
⇒
[ ]
_ :: _
⇒

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.

233Definition relocations_callrs : listreloc dobj relocs : string : listline ≔
match rs with
[ ]
⇒
[ ]
_ :: _
⇒
ins"mov" "q" reg"rbx"; reg"rdi"; ins"lea" "q" ripdobj; reg"rsi"; ins"lea" "q" riprelocs; reg"rdx"; ins"mov" "l" immZlengthrs; reg"ecx"; ins0"call" plt"filc_execute_constant_relocations"

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.

253Definition data_objectn : name lk : Syntax.linkage align : Z items : listdata_item : listline ≔
match linkage_flagslk with
None
⇒
todo"data linkage"
Somelinkage, flags
⇒
let name ≔ name_textn in
let dobj ≔ data_object_symbolname in
let da ≔ data_aux_symbolname in
let gp ≔ ".LpizlonatedGP_" ++ name%string in
let getter ≔ getter_symbolname in
let relocs ≔ ".Lpizlonated_" ++ name ++ "..relocs"%string in
let slow ≔ ".Lpizlonated_" ++ name ++ "..slow"%string in
let inited ≔ ".Lpizlonated_" ++ name ++ "..inited"%string in
let 'payload, size0, rs0 ≔ payload_itemsitems 0 [ ] in
let rs ≔ rev'rs0 in
let size ≔ Z.quotsize0 + 7 eight × eight in
let pad ≔ size − size0 in
let aux_word ≔ relocs_aux_wordrs flags da in
let total ≔ sixteen + size in
let payload_align ≔ Z.maxalign sixteen in
let front ≔ payload_align − sixteen in
let log ≔ Z.log2payload_align in
let sec ≔
&&
match rs with
[ ]
⇒
true
_
⇒
false
→
else
in
++
front >? 0
→
zerofront
else
[ ]
++
type_linedobj "object"; labeldobj; DirDQuadEAddpayload_ofdobj ELitLIntsize; DirDQuadaux_word
++
payload
++
pad >? 0
→
zeropad
else
[ ]
++
size_linedobj total ++ section_lineSBss; p2align4; labelgp; zerosixteen ++ aux_arrayrs da size relocs name ++ section_lineSText; p2align4 ++ data_linkage_globllinkage getter ++ type_linegetter "function"; labelgetter; ins"mov" "q" ripgp; reg"rax"; ins"mov" "q" rip_plusgp eight; reg"rdx"; ins"test" "q" reg"rax"; reg"rax"; ins0"jz" symslow; ins"test" "q" reg"rdx"; reg"rdx"; ins0"jz" symslow; ins0"ret" [ ]; labelslow; ins"push" "q" reg"rbx"; ins"mov" "q" reg"rdi"; reg"rbx"; ins"lea" "q" ripgp; reg"rdx"; ins"lea" "q" ripdobj; reg"rcx"; ins0"call" plt"filc_global_initialization_start"; ins"test" "b" imm1; reg"al"; ins0"jz" syminited ++ relocations_callrs dobj relocs ++ ins"mov" "q" reg"rbx"; reg"rdi"; ins0"call" plt"filc_global_initialization_end"; labelinited; ins"pop" "q" reg"rbx"; ins"lea" "q" ORippayload_ofdobj; reg"rax"; ins"mov" "q" reg"rax"; reg"rdx"; ins0"ret" [ ]

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.

327Definition thread_local_objectn : name linkage : term align : Z items : listdata_item : listline ≔
let name ≔ name_textn in
let getter ≔ getter_symbolname in
let tp ≔ "pizlonatedTP_" ++ name%string in
let slow ≔ ".LpizlonatedGS_" ++ name%string in
let template ≔ ".LpizlonatedTI_" ++ name%string in
let relocs ≔ ".Lpizlonated_" ++ name ++ "..relocs"%string in
let ensure ≔ ".Lpizlonated_" ++ name ++ "..ensure"%string in
let 'payload, size, rs0 ≔ payload_itemsitems 0 [ ] in
let rs ≔ rev'rs0 in
let allocate ≔
match rs with
[ ]
⇒
"filc_allocate_thread_local"
_ :: _
⇒
"filc_allocate_thread_local_with_ptrs"
in
let needed ≔ template_neededitems in
let copy ≔
needed
→
ins"lea" "q" memsixteen "r12"; reg"rdi"; ins"lea" "q" riptemplate; reg"rsi"; ins"mov" "q" immsize; reg"rcx"; ins0"rep movsb" [ ]
else
[ ]
in
let relocs_call ≔
match rs with
[ ]
⇒
[ ]
_ :: _
⇒
ins"mov" "q" reg"rbx"; reg"rdi"; ins"mov" "q" reg"r12"; reg"rsi"; ins"lea" "q" riprelocs; reg"rdx"; ins"mov" "l" immZlengthrs; reg"ecx"; ins0"call" plt"filc_execute_constant_relocations"
in
++
++
++
needed
→
section_lineSRodata; p2align4; labeltemplate ++ payload
else
filteris_todo payload
++
match rs with
[ ]
⇒
[ ]
_ :: _
⇒
++
section_lineSText; p2align4 ++ data_linkage_globllinkage getter ++ type_linegetter "function"; labelgetter; ins"mov" "q" OGottpoffLSymtp; reg"rax"; ins"mov" "q" OFsmem0 "rax"; reg"rax"; ins"test" "q" reg"rax"; reg"rax"; ins0"jz" symensure; ins"mov" "q" reg"rax"; reg"rdx"; ins0"ret" [ ]; labelensure; ins"sub" "q" immeight; reg"rsp"; ins0"call" symslow; ins"add" "q" immeight; reg"rsp"; ins"mov" "q" reg"rax"; reg"rdx"; ins0"ret" [ ]; p2align4; type_lineslow "function"; labelslow; ins"push" "q" reg"rbx"; ins"push" "q" reg"r12"; ins"sub" "q" immeight; reg"rsp"; ins"mov" "q" reg"rdi"; reg"rbx"; ins"mov" "q" immsize; reg"rsi"; ins"mov" "q" immalign; reg"rdx"; ins0"call" pltallocate; ins"mov" "q" reg"rax"; reg"r12" ++ copy ++ relocs_call ++ ins"lea" "q" memsixteen "r12"; reg"rax"; ins"mov" "q" OGottpoffLSymtp; reg"rcx"; ins"mov" "q" reg"rax"; OFsmem0 "rcx"; ins"add" "q" immeight; reg"rsp"; ins"pop" "q" reg"r12"; ins"pop" "q" reg"rbx"; ins0"ret" [ ]

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.

407Definition init_runtimekind : term : optionbool × string ≔
is_atom"ctor" kind
→
Sometrue, "filc_defer_or_run_global_ctor"
is_atom"dtor" kind
→
Somefalse, "filc_run_global_dtor"
else
None

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.

415Definition init_priorityprio : term : optionoptionlit ≔
match prio with
⇒
SomeSomeLIntp
⇒
String.eqba "none"
→
SomeNone
else
SomeSomeLSyma
_
⇒
None

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.

426Definition init_entryn : name kind prio : term f : name : listline ≔
let forwarder ≔ ".L" ++ name_textn ++ "..forwarder"%string in
match init_runtimekind with
None
⇒
todo"init kind"
Somector, run
⇒
section_lineSText; p2align4; type_lineforwarder "function"; labelforwarder; ins"lea" "q" ORippayload_offo; reg"rdi"; ins"mov" "q" reg"rdi"; reg"rsi"; ins0"jmp" pltrun
++
match init_priorityprio with
Somep
⇒
None
⇒
todo"init priority"
++
p2align3; quad_symforwarder

Items

As item//2 on data(Name, Linkage, Align, Items).

446Definition data_linesn : name lk : Syntax.linkage align : Z items : listdata_item : listline ≔
match lk, items with
LTlsl, _
⇒
thread_local_objectn l align items
LInitkind prio, Symf 0
⇒
init_entryn kind prio f
_, _
⇒
data_objectn lk 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.

458Definition alias_target_localsy : symbols target : name : bool ≔
match nm_findtarget sy_funcssy with
Somefe
⇒
None
⇒
false
||
match nm_findtarget sy_datasy with
SomeLLocal
⇒
true
SomeLRol | SomeLTlsl
⇒
is_atom"local" l
_
⇒
false

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.

474Definition alias_linessy : symbols n : name lk : term target : name : listline ≔
let getter ≔ getter_symbolname_textn in
let tg ≔ getter_symbolname_texttarget in
let op ≔
→
symtg
else
plttg
in
section_lineSText ++ data_linkage_globllk getter ++ type_linegetter "function"; labelgetter; ins"push" "q" reg"rax"; ins0"call" op; ins"pop" "q" reg"rcx"; ins0"ret" [ ]

Examples

488Example weak_declaration: data_linesTAtom"f" LExternWeak 1 [ ] = DirDWeakLSym"pizlonated_f"
Proof 1 step Qed
reflexivity
492Example payload_pointer_after_bytes: payload_itemsItemWw −1; Zero4; SymTAtom"g" 8; ItemWb 300 0 [ ] = long4294967295; zero4; quad_int0; DirDByteLInt44 [ ], 17, mkReloc8 TAtom"g" 8
Proof 1 step Qed
reflexivity
498Example payload_unaligned_pointer: first_todofstfstpayload_itemsItemWb 1; SymTAtom"g" 0 0 [ ] = Some"pointer data item is not 8-aligned"
Proof 1 step Qed
reflexivity
503Example payload_other_linkage: data_linesTAtom"d" LOtherTAtom"common" 8 Zero8 = todo"data linkage"
Proof 1 step Qed
reflexivity
507Example thread_local_other_item: first_tododata_linesTAtom"d" LTlsTAtom"local" 8 ItemOtherTAtom"x" = Some"data item"
Proof 1 step Qed
reflexivity
512Example relocation_table: relocationsmkReloc0 TAtom"g" 0; mkReloc8 TAtom"h" −1 "d" = quad_int0; long0; zero4; quad_sym"pizlonated_g"; quad_int8; long1; zero4; quad_sym".Lpizlonated_d..node1"; label".Lpizlonated_d..node1"; long0; long0; quad_sym"pizlonated_h"; quad_int18446744073709551615
Proof 1 step Qed
reflexivity