rocq/backend/Asm.v
x86-64 assembly as the backend builds it, and its printer as GNU as (AT&T) text: asm.pl's line terms as inductives, and asm.pl's grammar as functions. The text is asm.pl's byte for byte, which the backend's gate checks on every line the Prolog compiler emits for the corpus (asm.sh).
Mnemonics, suffixes and register names are strings, as they are atoms in asm.pl: the set is whatever instruction selection uses, and this file only prints.
What asm.pl prints with literal//1: an integer or an atom.
An expression: a literal or a sum.
An operand. Registers are named concretely (eax, cl, r9d), so mixed widths need no bookkeeping.
| | | OImm | e : expr | $E |
| | | OReg | r : string | %R |
| | | OMem | D(%B), D omitted when it is 0 | |
| | | OMemIndex | D(%B,%I), D omitted when it is 0 | |
| | | ORip | e : expr | E(%rip) |
| | | OGotpcrel | s : lit | S@GOTPCREL(%rip) |
| | | OPlt | s : lit | S@PLT |
| | | OGottpoff | s : lit | S@GOTTPOFF(%rip) |
| | | OFs | o : operand | %fs:O |
| | | OSym | e : expr | E, a jump or call target |
| | | OInd | o : operand | *O |
A section.
| | | SText | ||
| | | SData | ||
| | | SRodata | ||
| | | SBss | ||
| | | STbss | thread-local, zeroed | |
| | | SDataRelRo | ||
| | | SNoteGnuStack | ||
| | | SInit | ctor : bool prio : optionlit | .init_array or .fini_array, with .Prio if any |
A directive.
| | | DSection | s : section | |
| | | DP2align | n : lit | |
| | | DBalign | n : lit | |
| | | DGlobl | s : lit | |
| | | DWeak | s : lit | |
| | | DHidden | s : lit | |
| | | DType | s t : lit | .type S, @T |
| | | DSize | s : lit | .size S, .-S |
| | | DSizeOf | s n : lit | .size S, N |
| | | DSet | ||
| | | DQuad | e : expr | |
| | | DLong | n : lit | |
| | | DInt | n : lit | |
| | | DShort | n : lit | |
| | | DByte | .byte and a non-empty list | |
| | | DZero | n : lit | |
| | | DAscii | cs : listascii | .ascii and the bytes, escaped |
| | | DAsciz | a : lit | .asciz and the atom, as it is |
A fixed-register instruction from the emitter's own table (docs/asm-fixed.md).
| | | Cpuid | ||
| | | Xgetbv | ||
| | | Rdtsc | ||
| | | Rdtscp | ||
| | | Lfence | ||
| | | Sfence | ||
| | | Pause |
A line.
| | | Label | s : lit | S: |
| | | Fixed | m : fixed_op | |
| | | Ins | ||
Op, then the suffix if any, then the operands in AT&T order | |||
| | | Dir | d : directive | |
The printer
The text of a literal.
A displacement; 0 is omitted.
The operands after a mnemonic: a space, then the operands with commas between them, or nothing.
A byte in three octal digits.
One byte inside an .ascii string: printable ASCII as itself except quote and backslash, which are escaped, newline and tab as \n and \t, any other byte as a backslash and three octal digits.
cpuid writes rbx, which may hold a register home: it is kept in rsi, and cpuid's b result is brought out in edi.
The parts of the lines in rev, which is the lines in reverse, in front of k. A loop, so a module of any length prints in constant stack.
The text of ls.