rocq/backend/NfbTerm.v
NFB, the bytecode of a nanofil module (docs/nfb.md), read and written at the level of Prolog terms: the Gallina twin of src/nfb.pl, which must write the very same words.
As in nfb.pl, one table (forms) states every instruction: its opcode, its term as a pattern with numbered holes, and the fields its words hold, each naming a hole. The writer matches an instruction against the patterns and writes the fields of the hole values; the reader reads the fields of the opcode's form and fills the holes of its pattern. A list of the term, such as a call's arguments or a phi's pairs, is written element by element, each element by a smaller pattern and its own fields.
The words are integers below 2^32 (Z). The ids are as the document says: a temporary's is its place among first definitions, parameters first; a block's and a named local's their place in the stream. Without the NAMES section the reader names each by its id, an integer term.
Words
2^32, 2^64 and 2^96, hoisted so that extracted code does not rebuild them.
Whether n is a word, from 0 to 2^32 - 1.
Whether n is a signed 64-bit integer.
Whether n is a signed 96-bit integer, what CONSTANTS can hold.
The signed 64-bit n as two words, low first, in two's complement.
The signed 96-bit n as three words, low first.
The integer two words, low first, stand for as a signed 64-bit one.
The integer three words stand for as a signed 96-bit one.
2^29: a constant from -2^29 to 2^29 - 1 is written inside its operand word.
Whether the constant n is written inline.
Bytes
The bytes bs four to a word, low byte first, the last word padded with zero bytes.
The four bytes of each word, low first.
The length of bs, then bs packed: a string's or a str item's words.
The bytes of the string s.
The string of the bytes bs.
The one-character atom of the code b, below 256, as the term reader makes it: one byte below 128, else two of UTF-8.
Small helpers
The arguments of t when it is the compound f with n arguments.
Whether t is the atom a.
The value of the string key s in the association list xs.
The key of the value z in the association list xs.
Each element of xs through the partial f, or none if f fails on one.
The first n elements of xs and the rest, if xs has n.
Insert x into the sorted list xs, by the order le; an x equal to an element (by eqb) is dropped.
Merge two sorted lists without duplicates.
The runs of one element each, for sort_uniq.
Merge the runs rs in pairs.
Merge the runs until one is left, at most fuel rounds.
xs sorted by lt, each element once, as Prolog's sort/2 does with the order lt.
The byte order of strings.
The enumerations
The tables of codes a field can hold, each a list of atoms and their words (nfb.pl's nfb_code/3).
| | | EClass | ||
| | | EWidth | ||
| | | ELoad | ||
| | | EExt | ||
| | | ECas | ||
| | | ECond | ||
| | | ERights | ||
| | | EBound | ||
| | | ESetjmp | ||
| | | EEffect | ||
| | | EFlight | ||
| | | EMnemonic | ||
| | | ERegister |
The table of the enumeration e.
The word of the atom t in the enumeration e.
The atom of the word z in the enumeration e.
The table of instructions
A pattern of a term: a numbered hole, an atom, a compound, or a list of a fixed length.
The values of a pattern's holes.
The value of the hole i.
The holes' values that make the pattern p the term t, added to e.
The term of the pattern p with its holes filled from e.
A field of an instruction, holding the value of one hole:
| Field | Words |
|---|---|
FDef | none: the temporary takes the next id |
FClass, FEnum | one code |
FU32, FI64 | one word, or two, signed |
FOpnd | an operand word |
FLabel, FTarget | a block index; a target's shifted, bit 0 for poll |
FLocal, FLocalDef | a local's id; the definition writes none |
FStr | a STRINGS id |
FResult | a call's result word, defining its temporaries |
FLower | 0 for none, or 1 and the operand of lower(P) |
FFlightArg | 1 and the operand of address(P), or 0 and a value's |
FCount, FRest | a list: its length then its elements, or its elements to the end |
An element of a list is a smaller pattern with its own holes and fields.
| | | FDef | i : nat | |
| | | FClass | i : nat | |
| | | FEnum | e : enum i : nat | |
| | | FU32 | i : nat | |
| | | FI64 | i : nat | |
| | | FOpnd | i : nat | |
| | | FLabel | i : nat | |
| | | FTarget | i : nat | |
| | | FLocal | i : nat | |
| | | FLocalDef | i : nat | |
| | | FStr | i : nat | |
| | | FResult | i : nat | |
| | | FLower | i : nat | |
| | | FFlightArg | i : nat |
A field, or a list of elements.
| | | FOne | f : field | |
| | | FCount | ||
| | | FRest |
An instruction's form: its opcode, its pattern and its fields.
The pattern of a let(tmp(D), K, Op, Args), D hole 0 and K hole 1.
The fields of a let's definition and class, then fs.
The forms of the ops named ns, from the opcode c up, each made by mk.
The form of a let of a range op f: f(Lo, Hi, Rights, Align) on the operands of holes 6 on.
A call's or raw call's form.
Every form, in nfb.pl's order.
The opcode that prefixes an instruction defining a temporary again.
The group of an opcode: 0 a phi, 2 a jump, 1 any other.
The first form whose pattern t matches, with the holes' values.
The form of the opcode c.
What an instruction holds
The temporaries a call's result term r defines.
What a field holds besides words: the temporaries it defines, the symbols, constants and files it names.
The symbols and constants a value names.
What the field f holds, the holes' values e.
What the fields fs hold.
What the elements ts of a list hold, each the pattern el.
What an instruction of the form whose fields are fs holds.
What the instruction, phi or jump t holds.
Writing an instruction
The tables a function's instructions are written with: the ids of its temporaries, labels and locals, and of the module's symbols, strings and wide constants.
The words a field writes, the temporaries it defines, the ids of the temporaries it reads, and its targets' block indices with their poll bits.
The word of the constant n: inline, or a CONSTANTS index.
The operand word of the value v.
The word of a call's result term r, and what it defines.
The words of the field f, the holes' values e.
The words of the fields fs.
The words of the elements ts of a list, each the pattern el.
The words of an instruction's fields fs.
Reading an instruction
The tables a function's instructions are read with: names by id.
| r_syms | : ZMap.tterm | |
| r_strs | : ZMap.tterm | |
| r_consts | : ZMap.tZ | |
| r_temps | : ZMap.tterm | |
| r_labels | : ZMap.tterm | |
| r_locals | : ZMap.tterm |
The reader's state within an instruction: the words left, the rebind words left (none when there is no rebind prefix), the next temporary id and the next local id.
| s_words | : listZ | |
| s_rebinds | : optionlistZ | |
| s_next | : Z | |
| s_local | : Z |
The next word.
The constant of the word z, an inline or CONSTANTS one.
The value of the operand word z.
The name the next definition takes: the next id's, or the rebound id's.
The call result term of the word z, its temporaries named in turn.
Read the field f into the hole it names.
Read the fields fs.
Read n elements of the pattern el.
Read elements of the pattern el until no word is left, at most fuel of them.
Read an instruction's fields fs into its holes.
Instructions
The rebind words of the definitions ds, n temporaries defined before them: 0 for a first definition, which takes the id n, or the id plus one; and the count after them.
The words of the instruction t, which must be of the group g, in the block b, n temporaries defined before it; the count after it; and whether it keeps the stream ordered: no temporary read before its first definition, outside a phi, and no edge to an earlier or the same block without a poll.
The words of the instructions ts, all of the group g.
The parts of a block block(L, Phis, Insts, Jump).
The words of the blocks bs from the index b.
The names ns numbered from n in the map m, a name already there keeping its number; the names newly numbered, in order.
The temporary of a parameter param(K, tmp(D)), and K's code.
The word of a function's return type.
The names of a function: its temporaries', labels' and locals', in id order.
The words of a function's body, whether it is ordered, and its names; the module's tables are those of w.
Stage and mode
The names of the ops of the checked stage, with their arities; check_function is an atom.
Whether t is the compound f of n arguments.
As ir.pl's checked_inst/1: the instruction is of the checked stage's vocabulary.
As checked_jump/1: the jump has a poll edge.
The blocks of a function term, if it is one.
As module_stage/2: checked when a function uses the checked vocabulary.
Whether the class term k is one of the atoms ks.
As pointer_inst/1: the instruction produces, stores, passes or calls through a pointer, or converts one.
As pointer_item/1: the item has a pointer somewhere, or is of a linkage only the filc mode models.
As module_mode/2: filc when an item has a pointer, or a function calls one the module does not define.
The module's tables
The name a function, data object or alias defines, and its symbol kind: 0, 1 or 2.
What an item names: its instructions' parts, its data's symbols and constants, its alias's target.
The string of an atom.
A module's tables: its strings, wide constants and symbols (each a name, a kind, and the item that defines it, if any), and the ids of each.
The tables of the items.
The codes of the data linkages other than init(_, P) with an integer P.
The value of the term key t in the association list xs.
The key of the value z.
A data linkage's code and the word beside it, a priority's.
A symbol's three words.
The words of a data item.
The DATA words of a data item data(N, Lk, Align, Items), or none for another item.
The FUNCTIONS words of a function, whether it is ordered, and its names; nothing for another item.
Side sections
Every atom and functor of the term t.
The words of a string table: the count, then each string.
The words of the term t in a side section whose pool ids are ids: 0 and an integer, 1 and an atom, 2 and a compound's functor, arity and arguments, 3 and a list's length and elements.
The NAMES words of the functions' names: the pool, then each function's temporaries, labels and locals, each list its length and its terms.
A module's words
The words of the sections ss, each its id, length and payload.
The NFB of the module term module(Items) without context/2 items, with the NAMES section when names is true.
Reading a module
A reader of words: a value and the words after it, or none.
Read n of what r reads.
Read a count, then that many of what r reads; a count beyond the words left is refused before anything is read.
Read one word.
Read a byte string: its length, then its words.
Read a string table.
Read a signed 96-bit integer.
Read a signed 64-bit integer.
Read a side section's term, at most fuel deep.
The map from 0, 1, ... to the elements of xs.
Read the NAMES section: the pool, then each function's names, as many as the words hold.
The NAMES of the section's words.
The opcode of the next instruction, after its rebind prefix, if any.
Read one instruction of the group g, n temporaries and x locals defined before it; the counts after it.
Read the instructions of the group g that come next, at most fuel.
Read the blocks from the index i, k of them, fuel bounding each group.
The return type of its word.
The integers from 0 below n, as terms: the names without NAMES.
Read a function's body, of the symbol name n and linkage lk, its names from nm if NAMES has them.
Read a data item.
The linkage of a data symbol, from its code and extra word.
Read the items of the symbols syms, in order: a function's body from fws and its names from nms, a data object's from dws, an alias from the symbol itself.
Split the words into sections, each id with its payload.
Whether the section ids increase, each known: a core one from 1 to 5, NAMES, CONTEXT, or a tool's from 0x200.
The payload of the section id, or none.
The module term of the words ws, without its context items, and whether it had NAMES; the words are not yet checked against the module's own encoding (decode_term does that).
The words ws without their CONTEXT section and the sections of tools: those that do not say what the module is.
Equality of two lists of words.
The module term the NFB ws encode, provided ws are exactly its encoding, CONTEXT and tools' sections aside.