amd64_regs_check.pl
Translation validation for whole-function scalar register homes (docs/perf.md item 3, run by --registers=temps). The allocator proposes a fixed map from frame homes to registers; nothing about how it chose the map is trusted here.
The allocated stream is determined by the reference stream, the map and the save slots: every access to a mapped home is the same move with the home's register in place of its slot (substitute/3), the callee-saved registers the map uses are stored to their save slots right after the stack check and reloaded before every leave, and nothing else changes. The checker rebuilds that stream and requires the proposal to equal it, so flags, failure arguments, control flow and every unmapped location are unchanged by construction.
What remains to prove is that each mapped register holds its home's value wherever the reference could read it. The invariant: at every point, every live half (low or high 32 bits) of a mapped home equals the same half of its register. Liveness is computed here, per half, on the reference stream's control-flow graph, which must be complete: every jump names a label of the function or the stack-overflow exit, and no instruction falls off the end. The obligations:
| Event | Obligation |
|---|---|
| function entry | no mapped half is live |
| a write to home H in register R | every other home in R is dead after it |
| a 32-bit write to H | H's high half is dead after it (a register write zero-extends) |
a call | homes in r10/r11 are dead after it, except at the three authenticated save stubs |
a leave | no mapped half is live (the restores replace the registers) |
Byte and word writes preserve the rest of a register as they do of memory; liveness treats them as reads. Callee-saved registers keep their values across calls by the SysV ABI, which every callee obeys: C runtime functions, clang code and nanofil functions, which save what they use here. The reference stream must not name an allocatable register or %rbp outside the prologue, must not take the address of a mapped home or save slot, and must not touch a save slot.
Trusted, as in M6's retired cache checker: the emitter's home classes and root ranges (the frame record and local objects, from the layout that places them), and that only %rbp-relative operands reach a home (homes and save slots never escape). Checked: no mapped home overlaps a root range, so every GC root keeps the reference's stores, and a pointer's address word (class a) may be a home but its lower never is (docs/perf.md 5b-2).
Metadata is regs_metadata(Setjmp, Impl, Homes, Saves): Homes lists home(Offset, Classes) as for the scalar cache, with class a for a pointer's address word (docs/perf.md 5b-2), and root(Offset, Bytes) for each frame range holding GC roots, which no mapped home may overlap: the frame record and local objects. Saves lists save(R, Offset) for each callee-saved register in Map, in callee_saved/1 order. Map lists Offset-Register. An empty map or a setjmp function admits only identity.
As check_regs/4, with the effects, CFG and home liveness of Before's implementation body already computed by body_analysis/3 (the driver computes it once and shares it with the allocator). The analysis must be of that very body and cover every mapped home; liveness bits are independent per home, so extra homes change nothing.
R is a SysV callee-saved register a home live across a call may take: rbx or r12 to r15. The emitter reserves a save slot for each.
Mapped homes are disjoint 8-byte homes, every description of each one a scalar (w, l) or a pointer's address word (a), never a pointer (p); no mapped home overlaps a GC root range; save slots match the callee-saved registers used, in order, and lie outside every home.
Body follows label(Impl) in Lines; Pre is everything before it.
Every line has audited effects; no allocatable register is named; %rbp appears as a register only in the prologue; no indexed %rbp operand; no lea of a mapped home or save slot; no access to a save slot; an access that touches a mapped home is a substitutable move of that exact home.
As preflight_regs/3, with Effects the lines' audited effects.
the operand O names an allocatable register (as amd64_contract's explicit_registers/2 reads operands), or %rbp other than as the base of a mem(D, rbp) operand.
Line reads or writes Bytes at D(%rbp).
One of the memory effects Memory (instruction_effects/2) reads or writes Bytes at D(%rbp).
New is the move Line with its mapped home operand replaced by the home's register at the same width. Only moves are substituted.
A q immediate must fit a sign-extended imm32, as the memory form must; the register form would otherwise assemble as movabs.
After is the implementation body Body with the map applied: mapped moves substituted, saves after the stack check, restores before every leave. Fails if Body has no stack check, if anything before it is a label, a transfer or an access to a mapped home (the saves must run once, on every path, before any mapped register changes), or if a leave is not followed by ret.
Control flow and liveness
Succs are the successors of each line of Body by index. Fails when a transfer is unknown or the last line falls through: the checker's liveness needs the complete control-flow graph.
Effect is instruction_effects/2's first answer for Line.
As successors/2, given each line's line_effect/2.
T is the index of the label Name jumped to from line I. GNU as numeric labels: 1f is the next 1, 1b the previous one.
Homes is a list of home offsets. LiveOut lists, per line of Body, the set of live halves after it as a bitset: bit 2K is home K's low half, 2K+1 its high half (body_analysis/3's sets shifted down by the eight scratch and flags bits). LiveIn0 is the set live at Body's first line. Dataflow runs on basic blocks: a block ends at a line whose only successor is not the next line, and starts at a label.
Home K's low half is bit S of the analysis's sets, its high half S+1. Bits 0-7 are the scratch families and the flags, below the homes, so a set is only as wide as the highest home live in it: with them on top, every line's set was as wide as all the function's homes.
Analysis = analysis(Body, Effects, Homes, Index, LiveOut, LiveIn0, UDs): each line's audited effects, the home offsets and their bit numbers (Index), the live sets after each line (LiveOut) and at the first, and each line's ud(Use, Def). Bits 0-6 are the scratch families (scratch_family/2) and bit 7 the flags, which only the operand checker reads (docs/perf.md, step 3b); home K's halves are the two bits from home_shift/2. Fails when a line has no audited effects or the CFG is incomplete. The one whole-function analysis the allocator and both checkers share.
As body_analysis/3, with Effects the lines' audited effects.
block(Start, Lines, Succs) with the successor line indices of its last line.
A block's gen and kill sets, composed backward over its lines. Set difference is xor(A, A /\ B), not A /\ \ B: pinned Trealla truncates a bigint intersected with a negative machine integer.
Uses and definitions of home halves by one line. A write covering a whole half defines it; a partial write reads it too.
Use and Def are the scratch families and flags Line uses and defines, as 8-bit sets. A read at any width uses a family, a 32- or 64-bit write defines it, a narrower one uses and defines it. A flags read uses bit 7 and a flags write defines it. A call, the stack-overflow jump and an asm_fixed line use every scratch family (their arity is not known here); ret uses rax, rcx and rdx, the return registers.
the homes' offset-to-number pairs bucketed by 8-byte word, so halves/5 looks up the two or three words an access can overlap rather than each of its byte offsets.
bitsets of the home halves that bytes [D, D+N) cover entirely and touch at all.
The obligations
Each register's mask: both halves of every home mapped to it.
The operand checker (docs/perf.md, step 3b)
Lives lists live(In, Out, Effect) for each line of A: the scratch and flags bits before and after it, and its audited effects (line_effect/2, shared with the analysis when the line is the reference's). A is the 3a stream of the reference body the shared Analysis is of. A is that body with mapped moves substituted, which changes no scratch or flags use, and with the save and restore moves of Saves inserted (check_regs/5 proved it is exactly that stream); an inserted line touches neither, so it takes the set live before the next reference line.
As operand_lives/4, with the home registers' liveness in bits 8-14 of each set (home_register_bit/2) from the map 3a's checker validated (docs/perf.md item 19). A home register is live where a half of a home mapped to it is live in the reference. A callee-saved register is also live wherever it holds the caller's value: always when Saves does not save it, and, when it does, from the body's start through the saves and at every leave and ret (the restores write it just before). Map is Offset-Register pairs, or all(Registers) to keep those registers live everywhere (operand_lives/4).
Each line of A gets live(In, Out, Effect): a line equal to its reference line shares its effects; a substituted or inserted one gets its own. Phase is pre until the saves are done (the callee-saved registers hold the caller's values and are live), then post.
B, the operand rewrite of the implementation body A, makes the same paired lines in the same order on equal values (docs/perf.md, step 3b's contract). Lives lists live(In, Out, Effect) for each line of A: the scratch families and flags (8 bits, scratch_family/2) live before and after it, from the shared analysis of the reference (operand_lives/4), and its audited effects. The walk takes A's boundaries from those effects, and B's from its own unless the line is identical to A's. Moves (operand_move/2) execute in their own stream only; boundary lines must be identical, and at each boundary A and B agree on every register compared there.
As check_operands/3, with frame cells (docs/perf.md, 5a-loads). Cells is cells(Ds, Others): the rbp displacements of the 8-byte frame words the emitter lists as cells, and the Disp-Bytes ranges of the other frame storage (locals, wide and save slots) they must stay apart from. Stores to cells stay paired lines, so frame memory is the same in A and B at every instruction; a whole 32- or 64-bit load of a cell into a general register is a move in its own stream, reading the cell's symbolic value. The value is shared by A and B, set by paired stores and reset at every region start. A word whose address a lea computes is not a cell.
The cells of Cells0, cells(Ds, Others), are distinct, 8-aligned frame words outside every other range in Others; Cells maps those no lea in the stream A addresses, which the operand rewrite may then use.
Lines after a ret, ud2 or jmp and before the next boundary are unreachable (state none): they must pair, but nothing is compared. CS is the cells' values (cell_value/3), shared by A and B.
line_effect/2 is a function.Line is a move (operand_move/2)
or a whole load of a cell into a general register other than rsp or rbp, as a move of the cell's value.
the cell's halves, v(Lo, Hi); a cell not written in this region holds its shared start value.
The paired
line J writes the same memory in A and B. A whole store of a register or immediate sets the cell from A's source (equal to B's): 64 bits both halves, 32 bits the low half, keeping the high half. Any other write overlapping a cell gives it a fresh shared value.
Facts, so a bound query is deterministic and an unbound one enumerates.
S is the symbolic state S0 after Move (operand_move/2, stream_move/4). The state is st(GPRs, XMMs, Flags); a GPR is v(Low, High).
Line ends a straight-line run: it transfers control, writes rsp or rbp, or is not an instruction (a label or directive).
The registers of a state are the arguments of r/16 and x/8, in gpr/1's and xmm/1's order. put_slot/4 (r/16) and put_xslot/4 (x/8) are separate so that a bound index leaves no choicepoint.
| 897 | 1 | x_, A2, A3, A4, A5, A6, A7, A8 | V | xV, A2, A3, A4, A5, A6, A7, A8 |
| 898 | 2 | xA1, _, A3, A4, A5, A6, A7, A8 | V | xA1, V, A3, A4, A5, A6, A7, A8 |
| 899 | 3 | xA1, A2, _, A4, A5, A6, A7, A8 | V | xA1, A2, V, A4, A5, A6, A7, A8 |
| 900 | 4 | xA1, A2, A3, _, A5, A6, A7, A8 | V | xA1, A2, A3, V, A5, A6, A7, A8 |
| 901 | 5 | xA1, A2, A3, A4, _, A6, A7, A8 | V | xA1, A2, A3, A4, V, A6, A7, A8 |
| 902 | 6 | xA1, A2, A3, A4, A5, _, A7, A8 | V | xA1, A2, A3, A4, A5, V, A7, A8 |
| 903 | 7 | xA1, A2, A3, A4, A5, A6, _, A8 | V | xA1, A2, A3, A4, A5, A6, V, A8 |
| 904 | 8 | xA1, A2, A3, A4, A5, A6, A7, _ | V | xA1, A2, A3, A4, A5, A6, A7, V |
After a boundary, live scratch
families, live home registers (bits 8-14, home_register_bit/2) and live flags are shared, dead ones distinct per stream; the rest is shared.
at a boundary, A and B agree on both halves of rsp and rbp, every XMM register, each live scratch family and home register, and the flags if live.
The role of each explicit operand of an audited non-boundary form: src(W), dst(W), srcdst(W) (a two-address destination) or addr (a memory operand not accessed). W is the operand's width in bits, or unbound when its register gives it (SSE forms).
Facts, indexed on the mnemonic.
| 960 | mov | b | src8, dst8 |
| 961 | mov | w | src16, dst16 |
| 962 | mov | l | src32, dst32 |
| 963 | mov | q | src64, dst64 |
| 964 | movabs | q | src64, dst64 |
| 965 | movzb | b | src8, dst8 |
| 966 | movzb | w | src8, dst16 |
| 967 | movzb | l | src8, dst32 |
| 968 | movzb | q | src8, dst64 |
| 969 | movsb | b | src8, dst8 |
| 970 | movsb | w | src8, dst16 |
| 971 | movsb | l | src8, dst32 |
| 972 | movsb | q | src8, dst64 |
| 973 | movzw | b | src16, dst8 |
| 974 | movzw | w | src16, dst16 |
| 975 | movzw | l | src16, dst32 |
| 976 | movzw | q | src16, dst64 |
| 977 | movsw | b | src16, dst8 |
| 978 | movsw | w | src16, dst16 |
| 979 | movsw | l | src16, dst32 |
| 980 | movsw | q | src16, dst64 |
| 981 | movsl | b | src32, dst8 |
| 982 | movsl | w | src32, dst16 |
| 983 | movsl | l | src32, dst32 |
| 984 | movsl | q | src32, dst64 |
| 985 | lea | q | addr, dst64 |
| 986 | lea | l | addr, dst32 |
| 987 | add | b | src8, srcdst8 |
| 988 | add | w | src16, srcdst16 |
| 989 | add | l | src32, srcdst32 |
| 990 | add | q | src64, srcdst64 |
| 991 | sub | b | src8, srcdst8 |
| 992 | sub | w | src16, srcdst16 |
| 993 | sub | l | src32, srcdst32 |
| 994 | sub | q | src64, srcdst64 |
| 995 | and | b | src8, srcdst8 |
| 996 | and | w | src16, srcdst16 |
| 997 | and | l | src32, srcdst32 |
| 998 | and | q | src64, srcdst64 |
| 999 | or | b | src8, srcdst8 |
| 1000 | or | w | src16, srcdst16 |
| 1001 | or | l | src32, srcdst32 |
| 1002 | or | q | src64, srcdst64 |
| 1003 | xor | b | src8, srcdst8 |
| 1004 | xor | w | src16, srcdst16 |
| 1005 | xor | l | src32, srcdst32 |
| 1006 | xor | q | src64, srcdst64 |
| 1007 | imul | b | src8, srcdst8 |
| 1008 | imul | w | src16, srcdst16 |
| 1009 | imul | l | src32, srcdst32 |
| 1010 | imul | q | src64, srcdst64 |
| 1011 | btc | b | src8, srcdst8 |
| 1012 | btc | w | src16, srcdst16 |
| 1013 | btc | l | src32, srcdst32 |
| 1014 | btc | q | src64, srcdst64 |
| 1015 | cmp | b | src8, src8 |
| 1016 | cmp | w | src16, src16 |
| 1017 | cmp | l | src32, src32 |
| 1018 | cmp | q | src64, src64 |
| 1019 | test | b | src8, src8 |
| 1020 | test | w | src16, src16 |
| 1021 | test | l | src32, src32 |
| 1022 | test | q | src64, src64 |
| 1023 | neg | b | srcdst8 |
| 1024 | neg | w | srcdst16 |
| 1025 | neg | l | srcdst32 |
| 1026 | neg | q | srcdst64 |
| 1027 | shl | b | src8, srcdst8 |
| 1028 | shl | w | src8, srcdst16 |
| 1029 | shl | l | src8, srcdst32 |
| 1030 | shl | q | src8, srcdst64 |
| 1031 | shr | b | src8, srcdst8 |
| 1032 | shr | w | src8, srcdst16 |
| 1033 | shr | l | src8, srcdst32 |
| 1034 | shr | q | src8, srcdst64 |
| 1035 | sar | b | src8, srcdst8 |
| 1036 | sar | w | src8, srcdst16 |
| 1037 | sar | l | src8, srcdst32 |
| 1038 | sar | q | src8, srcdst64 |
| 1039 | sete | none | dst8 |
| 1040 | setne | none | dst8 |
| 1041 | setz | none | dst8 |
| 1042 | setnz | none | dst8 |
| 1043 | setb | none | dst8 |
| 1044 | cmovb | q | src64, srcdst64 |
| 1045 | setbe | none | dst8 |
| 1046 | seta | none | dst8 |
| 1047 | setae | none | dst8 |
| 1048 | setl | none | dst8 |
| 1049 | setle | none | dst8 |
| 1050 | setg | none | dst8 |
| 1051 | setge | none | dst8 |
| 1052 | sets | none | dst8 |
| 1053 | setns | none | dst8 |
| 1054 | setp | none | dst8 |
| 1055 | setnp | none | dst8 |
| 1056 | cltd | none | [] |
| 1057 | cqto | none | [] |
A fence pairs with itself, in its place among the memory accesses. | |||
| 1059 | mfence | none | [] |
| 1060 | div | b | src8 |
| 1061 | div | w | src16 |
| 1062 | div | l | src32 |
| 1063 | div | q | src64 |
| 1064 | idiv | b | src8 |
| 1065 | idiv | w | src16 |
| 1066 | idiv | l | src32 |
| 1067 | idiv | q | src64 |
lock cmpxchg: New, then the memory it compares and writes. | |||
| 1069 | 'lock cmpxchg' | b | src8, srcdst8 |
| 1070 | 'lock cmpxchg' | w | src16, srcdst16 |
| 1071 | 'lock cmpxchg' | l | src32, srcdst32 |
| 1072 | 'lock cmpxchg' | q | src64, srcdst64 |
| 1073 | movd | none | src_, dst_ |
| 1074 | movq | none | src_, dst_ |
| 1075 | add | ss | src128, srcdst128 |
| 1076 | add | sd | src128, srcdst128 |
| 1077 | sub | ss | src128, srcdst128 |
| 1078 | sub | sd | src128, srcdst128 |
| 1079 | mul | ss | src128, srcdst128 |
| 1080 | mul | sd | src128, srcdst128 |
| 1081 | div | ss | src128, srcdst128 |
| 1082 | div | sd | src128, srcdst128 |
| 1083 | ucomiss | none | src128, src128 |
| 1084 | ucomisd | none | src128, src128 |
| 1085 | cvtss2sd | none | src128, srcdst128 |
| 1086 | cvtsd2ss | none | src128, srcdst128 |
| 1087 | sqrtss | none | src128, srcdst128 |
| 1088 | sqrtsd | none | src128, srcdst128 |
| 1089 | cvttss2si | b | src128, dst8 |
| 1090 | cvttss2si | w | src128, dst16 |
| 1091 | cvttss2si | l | src128, dst32 |
| 1092 | cvttss2si | q | src128, dst64 |
| 1093 | cvttsd2si | b | src128, dst8 |
| 1094 | cvttsd2si | w | src128, dst16 |
| 1095 | cvttsd2si | l | src128, dst32 |
| 1096 | cvttsd2si | q | src128, dst64 |
| 1097 | cvtsi2ss | b | src8, srcdst128 |
| 1098 | cvtsi2ss | w | src16, srcdst128 |
| 1099 | cvtsi2ss | l | src32, srcdst128 |
| 1100 | cvtsi2ss | q | src64, srcdst128 |
| 1101 | cvtsi2sd | b | src8, srcdst128 |
| 1102 | cvtsi2sd | w | src16, srcdst128 |
| 1103 | cvtsi2sd | l | src32, srcdst128 |
| 1104 | cvtsi2sd | q | src64, srcdst128 |
Implicit operands, read and written at a width, by mnemonic.
| 1107 | cltd | _ | rax−32 | rdx−32 |
| 1108 | cqto | _ | rax−64 | rdx−64 |
| 1109 | div | b | rax−8, rdx−8 | rax−8, rdx−8 |
| 1110 | div | w | rax−16, rdx−16 | rax−16, rdx−16 |
| 1111 | div | l | rax−32, rdx−32 | rax−32, rdx−32 |
| 1112 | div | q | rax−64, rdx−64 | rax−64, rdx−64 |
| 1113 | idiv | b | rax−8, rdx−8 | rax−8, rdx−8 |
| 1114 | idiv | w | rax−16, rdx−16 | rax−16, rdx−16 |
| 1115 | idiv | l | rax−32, rdx−32 | rax−32, rdx−32 |
| 1116 | idiv | q | rax−64, rdx−64 | rax−64, rdx−64 |
lock cmpxchg reads %rax at its width and writes it: wholly at 32 and 64 bits (amd64_contract.pl), the width's part at 8 and 16. | ||||
| 1119 | 'lock cmpxchg' | b | rax−8 | rax−8 |
| 1120 | 'lock cmpxchg' | w | rax−16 | rax−16 |
| 1121 | 'lock cmpxchg' | l | rax−32 | rax−64 |
| 1122 | 'lock cmpxchg' | q | rax−64 | rax−64 |
The flags a form defines from its inputs (res), or leaves partly undefined or preserved (distinct per stream). The SSE arithmetic forms (add, sub, mul, div with ss/sd) preserve them. Facts, indexed on the mnemonic.
| 1128 | add | b | defined |
| 1129 | add | w | defined |
| 1130 | add | l | defined |
| 1131 | add | q | defined |
| 1132 | sub | b | defined |
| 1133 | sub | w | defined |
| 1134 | sub | l | defined |
| 1135 | sub | q | defined |
| 1136 | and | b | defined |
| 1137 | and | w | defined |
| 1138 | and | l | defined |
| 1139 | and | q | defined |
| 1140 | or | b | defined |
| 1141 | or | w | defined |
| 1142 | or | l | defined |
| 1143 | or | q | defined |
| 1144 | xor | b | defined |
| 1145 | xor | w | defined |
| 1146 | xor | l | defined |
| 1147 | xor | q | defined |
| 1148 | cmp | b | defined |
| 1149 | cmp | w | defined |
| 1150 | cmp | l | defined |
| 1151 | cmp | q | defined |
| 1152 | test | b | defined |
| 1153 | test | w | defined |
| 1154 | test | l | defined |
| 1155 | test | q | defined |
| 1156 | neg | b | defined |
| 1157 | neg | w | defined |
| 1158 | neg | l | defined |
| 1159 | neg | q | defined |
| 1160 | ucomiss | none | defined |
| 1161 | ucomisd | none | defined |
| 1162 | shl | b | shift |
| 1163 | shl | w | shift |
| 1164 | shl | l | shift |
| 1165 | shl | q | shift |
| 1166 | shr | b | shift |
| 1167 | shr | w | shift |
| 1168 | shr | l | shift |
| 1169 | shr | q | shift |
| 1170 | sar | b | shift |
| 1171 | sar | w | shift |
| 1172 | sar | l | shift |
| 1173 | sar | q | shift |
| 1174 | imul | b | undefined |
| 1175 | imul | w | undefined |
| 1176 | imul | l | undefined |
| 1177 | imul | q | undefined |
| 1178 | btc | b | undefined |
| 1179 | btc | w | undefined |
| 1180 | btc | l | undefined |
| 1181 | btc | q | undefined |
| 1182 | div | b | undefined |
| 1183 | div | w | undefined |
| 1184 | div | l | undefined |
| 1185 | div | q | undefined |
| 1186 | idiv | b | undefined |
| 1187 | idiv | w | undefined |
| 1188 | idiv | l | undefined |
| 1189 | idiv | q | undefined |
| 1190 | 'lock cmpxchg' | b | defined |
| 1191 | 'lock cmpxchg' | w | defined |
| 1192 | 'lock cmpxchg' | l | defined |
| 1193 | 'lock cmpxchg' | q | defined |
A's line LA and B's line LB, the J-th paired line, compute the same outputs from the pre-states SA0 and SB0; SA and SB are the post-states. Besides the same form on equal operand values (docs/perf.md, step 3b), three pairings are accepted (item 19):
- a zero idiom,
xororsubof a register with itself at 32 or 64 bits, in any register: both write 0 and the same flags, whatever the register held; add,and,or,xororimulof two registers with B's operands swapped: the result and the flags are symmetric;addof a register or an immediate, orsubof an immediate, as aleaof the same width into any register (a register addend that holds a constant may be the displacement): the same result, but B's flags keep their old value, so A's differ from them after it.
lea_pair: A's add or sub writes res(J,2) to its destination and defines the flags; B's lea writes res(J,2) to its own and keeps them.
lea's base and index registers, read at the operation's width, are A's two addends in either order; a displacement is A's immediate (negated for sub) within disp32.
A register addend holding a constant (in A) may be the displacement.
one role per operand of both lines, and each operand pair matches in the pre-states.
register destinations at positions P.. get res(J,P).
setcc and cmovcc read the flags; a shift's flags output depends on its input (flags_after/9), jcc is a boundary.
Sources: equal values at the role's width; memory operands of the same form on equal addressing registers; other operands identical.
A destination: registers of the same width (any register), or the same memory operand.
V is register family F read at W bits in state S.
the same memory operand on equal addressing registers, or the same non-register, non-immediate operand.