amd64_contract.pl

Audited machine forms for the scalar stack cache. Unknown forms fail, selecting the unchanged implementation, rather than guessing effects. Reads name register families. write(Family,Bits) records partial writes: 32 bits zero-extend, 8/16 preserve the rest. Memory effects include addressing-register reads; flags and control/frame effects are separate. This describes selected instructions, not IR liveness or GC roots. Calls are unconditional cache boundaries; their ABI argument reads are not enumerated. Do not use this as a general call-liveness contract. Three compiler-local save stubs additionally preserve r10/r11 on normal return (docs/abi-findings.md); their original PLT calls do not.

moduleamd64_contract

exportsinstruction_effects/2 register/3 explicit_registers/2 operand_register/2 slow_call_stub/2 preserving_call/1

useslists

15:- discontiguousinstruction_effects/2

Name is the Bits-wide name of the general-purpose register Family (rax, ..., r15, rsp, rbp): register(eax, rax, 32). Concrete names index directly; family and width queries generate the name without searching every family for every operand in a large function.

register
23	rax	rax	64
23	eax	rax	32
24	ax	rax	16
24	al	rax	8
25	rcx	rcx	64
25	ecx	rcx	32
26	cx	rcx	16
26	cl	rcx	8
27	rdx	rdx	64
27	edx	rdx	32
28	dx	rdx	16
28	dl	rdx	8
29	rbx	rbx	64
29	ebx	rbx	32
30	bx	rbx	16
30	bl	rbx	8
31	rsi	rsi	64
31	esi	rsi	32
32	si	rsi	16
32	sil	rsi	8
33	rdi	rdi	64
33	edi	rdi	32
34	di	rdi	16
34	dil	rdi	8
35	rbp	rbp	64
35	ebp	rbp	32
36	bp	rbp	16
36	bpl	rbp	8
37	rsp	rsp	64
37	esp	rsp	32
38	sp	rsp	16
38	spl	rsp	8
39	r8	r8	64
39	r8d	r8	32
40	r8w	r8	16
40	r8b	r8	8
41	r9	r9	64
41	r9d	r9	32
42	r9w	r9	16
42	r9b	r9	8
43	r10	r10	64
43	r10d	r10	32
44	r10w	r10	16
44	r10b	r10	8
45	r11	r11	64
45	r11d	r11	32
46	r11w	r11	16
46	r11b	r11	8
47	r12	r12	64
47	r12d	r12	32
48	r12w	r12	16
48	r12b	r12	8
49	r13	r13	64
49	r13d	r13	32
50	r13w	r13	16
50	r13b	r13	8
51	r14	r14	64
51	r14d	r14	32
52	r14w	r14	16
52	r14b	r14	8
53	r15	r15	64
53	r15d	r15	32
54	r15w	r15	16
54	r15b	r15	8
55	xmm0	xmm0	128
55	xmm1	xmm1	128
56	xmm2	xmm2	128
56	xmm3	xmm3	128
57	xmm4	xmm4	128
57	xmm5	xmm5	128
58	xmm6	xmm6	128
58	xmm7	xmm7	128

width
60	b	8
60	w	16
60	l	32
60	q	64

61expressionE ←

integerE

62expressionE ←

atomE

63expressionA + B ←

expressionA

expressionB

64addressmemD, B, B ←

integerD

registerB, B, 64

65addressmemD, B, I, B, I ←

integerD

registerB, B, 64

registerI, I, 64

66addressripE, [] ←

expressionE

67addressgotpcrelS, [] ←

atomS

explicit_registers+Line, -Familiesdet

Families are the register families Line's operands name, addressing registers included, with repeats; [] for a label or directive.

73explicit_registersins_, _, Os, Rs ←

findallR,

memberO, Os

operand_registerO, R

, Rs

75explicit_registers_, []

operand_register+Operand, -Familynondet

Operand names the register Family: as a register, as a base or index of a memory operand, or under an indirection.

80operand_registerregN, F ←

registerN, F, _

81operand_registerO, R ←

addressO, Rs

memberR, Rs

82operand_registerindO, R ←

operand_registerO, R

84sourceregR, W, F, [] ←

registerR, F, W

85sourceimmE, _, [], [] ←

expressionE

86sourceM, W, Rs, readM, N ←

addressM, Rs

N is W//8

87destinationregR, W, [], writeF, W, [] ←

registerR, F, W

88destinationM, W, Rs, [], writeM, N ←

addressM, Rs

N is W//8

x86 does not admit a memory-to-memory two-operand instruction.

90not_two_memoryA, B ←

addressA, _

addressB, _

instruction_effects+Line, -Effectsemidet

Effect is effect(Reads, Writes, Flags, Memory, Flow) for the audited asm.pl line Line: the register families it reads (addressing registers included), its writes write(Family, Bits) (32 bits zero-extend, 8 and 16 preserve the rest), its effect on the flags (preserve among them), its memory reads and writes read(M, Bytes) and write(M, Bytes), and its control or frame effect (next for a line that falls through). Fails for a form not audited here, so a caller keeps the unchanged implementation rather than guessing its effects.

102instruction_effectsinsmov, S, A, B, effectRs, Ws, preserve, Ms, next ←

widthS, W

sourceA, W, R₁, M₁

destinationB, W, R₂, Ws, M₂

not_two_memoryA, B

appendR₁, R₂, Rs

appendM₁, M₂, Ms

105instruction_effectsinsmovabs, q, immN, regR, effect[], writeF, 64, preserve, [], next ←

integerN

registerR, F, 64

108instruction_effectsinsOp, S, A, regR, effectRs, writeF, W, preserve, Ms, next ←

extensionOp, From

widthS, W

W > From

sourceA, From, Rs, Ms

A ≠ imm_

registerR, F, W

111instruction_effectsinslea, q, M, regR, effectRs, writeF, 64, preserve, [], next ←

addressM, Rs

registerR, F, 64

leal computes the 64-bit address and writes its low 32 bits, zero-extended, like any 32-bit write.

115instruction_effectsinslea, l, M, regR, effectRs, writeF, 32, preserve, [], next ←

addressM, Rs

registerR, F, 32

117instruction_effectsinsOp, S, A, B, effectRs, Ws, write, Ms, next ←

memberchkOp, add, sub, and, or, xor, imul, btc

widthS, W

memberchkOp, imul, btc

→

W ≥ 16

B = reg_

else

true

sourceA, W, R₁, M₁

sourceB, W, R₂, M₂

B ≠ imm_

destinationB, W, _, Ws, M₃

not_two_memoryA, B

appendR₁, R₂, Rs

appendM₁, M₂, M₃, Ms

123instruction_effectsinsOp, S, A, B, effectRs, [], write, Ms, next ←

memberchkOp, cmp, test

widthS, W

sourceA, W, R₁, M₁

sourceB, W, R₂, M₂

B ≠ imm_

not_two_memoryA, B

appendR₁, R₂, Rs

appendM₁, M₂, Ms

127instruction_effectsinsneg, S, A, effectRs, Ws, write, Ms, next ←

widthS, W

sourceA, W, Rs, M₁

destinationA, W, _, Ws, M₂

appendM₁, M₂, Ms

130instruction_effectsinsOp, S, Count, A, effectRs, Ws, read_write, Ms, next ←

memberchkOp, shl, shr, sar

widthS, W

shift_countCount, R₁

sourceA, W, R₂, M₁

destinationA, W, _, Ws, M₂

appendR₁, R₂, Rs

appendM₁, M₂, Ms

134instruction_effectsinsOp, none, regR, effectF, writeF, 8, read, [], next ←

atom_concatset, CC, Op

conditionCC

registerR, F, 8

136instruction_effectsinsOp, q, regA, regB, effectFA, FB, writeFB, 64, read, [], next ←

atom_concatcmov, CC, Op

conditionCC

registerA, FA, 64

registerB, FB, 64

138instruction_effectsinscltd, none, [], effectrax, writerdx, 32, preserve, [], next

139instruction_effectsinscqto, none, [], effectrax, writerdx, 64, preserve, [], next

140instruction_effectsinsOp, S, A, effectrax, rdx|Rs, Ws, write, Ms, next ←

memberchkOp, div, idiv

widthS, W

memberchkW, 32, 64

sourceA, W, Rs, Ms

A ≠ imm_

Ws = writerax, W, writerdx, W

extension
144	movzb	8
144	movsb	8
145	movzw	16
145	movsw	16
145	movsl	32

146shift_countregcl, rcx

147shift_countimmN, [] ←

integerN

N ≥ 0

N ≤ 255

148conditionCC ←

memberchkCC, e, ne, z, nz, b, be, a, ae, l, le, g, ge, s, ns, p, np

SSE forms use full-family symbolic outputs: the cache never changes one, so the validator need not emulate floating arithmetic or lanes.

152instruction_effectsinsOp, none, A, B, effectRs, Ws, preserve, Ms, next ←

sse_moveOp, W

sse_transferA, B, W, Rs, Ws, Ms

154instruction_effectsinsOp, S, regA, regB, effectA, B, writeB, 128, preserve, [], next ←

memberchkOp, add, sub, mul, div

memberchkS, ss, sd

registerA, A, 128

registerB, B, 128

158instruction_effectsinsOp, none, regA, regB, effectA, B, [], write, [], next ←

memberchkOp, ucomiss, ucomisd

registerA, A, 128

registerB, B, 128

160instruction_effectsinsOp, none, regA, regB, effectA, B, writeB, 128, preserve, [], next ←

memberchkOp, cvtss2sd, cvtsd2ss, sqrtss, sqrtsd

registerA, A, 128

registerB, B, 128

163instruction_effectsinsOp, S, regA, regB, effectA, writeF, W, preserve, [], next ←

memberchkOp, cvttss2si, cvttsd2si

widthS, W

memberchkW, 32, 64

registerA, A, 128

registerB, F, W

167instruction_effectsinsOp, S, regA, regB, effectF, B, writeB, 128, preserve, [], next ←

memberchkOp, cvtsi2ss, cvtsi2sd

widthS, W

memberchkW, 32, 64

registerA, F, W

registerB, B, 128

171sse_movemovd, 32

171sse_movemovq, 64

172sse_transferregA, regB, W, F, writeB, 128, [] ←

registerA, F, W

registerB, B, 128

174sse_transferregA, regB, W, A, writeF, W, [] ←

registerA, A, 128

registerB, F, W

177instruction_effectsinsjmp, none, T, effectRs, [], preserve, Ms, branch ←

targetT, Rs, Ms

179instruction_effectsinsOp, none, T, effect[], [], read, [], branch ←

atom_concatj, CC, Op

conditionCC

targetT, [], []

181instruction_effectsinscall, S, T, effectrsp|Rs, Ws, write, Ms, call ←

memberchkS, none, q

targetT, Rs, M

preserving_callinscall, S, T

→

Kept = r10, r11

else

Kept = []

findallwriteR, W,

caller_clobberR, W

¬memberchkR, Kept

, Ws

appendM, read_writeruntime, unknown, Ms

186instruction_effectsinspush, q, regR, effectF, rsp, writersp, 64, preserve, writestack, 8, frame ←

registerR, F, 64

189instruction_effectsinspop, q, regR, effectrsp, writeF, 64, writersp, 64, preserve, readstack, 8, frame ←

registerR, F, 64

192instruction_effectsinsleave, none, [], effectrbp, writerbp, 64, writersp, 64, preserve, readstack, 8, frame

194instruction_effectsinsret, none, [], effectrsp, writersp, 64, preserve, readstack, 8, terminal

196instruction_effectsinsud2, none, [], effect[], [], preserve, [], terminal

A fence orders memory; it reads and writes no register or frame slot.

198instruction_effectsinsmfence, none, [], effect[], [], preserve, [], next

lock cmpxchg R, M compares %rax's low W bits with M; equal, it writes R to M, else M to them. It reads rax, R and M's addressing registers, reads and writes M (the write happens either way), and defines the flags. At 32 bits a failure zero-extends rax and a success leaves it, so 32 and 64 record a whole write of an unknown value; 8 and 16 preserve the rest either way. A locked access is also a full fence.

205instruction_effectsins'lock cmpxchg', S, regR, M, effectrax, F|Rs, writerax, WA, write, readM, N, writeM, N, next ←

widthS, W

registerR, F, W

addressM, Rs

N is W//8

W ≥ 32

→

WA = 64

else

WA = W

A fixed-register asm line (docs/asm-fixed.md) is not an ins/3, so the register checker treats it as a region boundary. Its writes are 32 bits; cpuid's line saves rbx in rsi and brings its b result out in edi, so rbx is preserved. None of them changes the flags.

213instruction_effectsasm_fixedcpuid, effectrax, rcx, writerax, 32, writercx, 32, writerdx, 32, writersi, 64, writerdi, 32, preserve, [], next

216instruction_effectsasm_fixedxgetbv, effectrcx, writerax, 32, writerdx, 32, preserve, [], next

217instruction_effectsasm_fixedrdtsc, effect[], writerax, 32, writerdx, 32, preserve, [], next

218instruction_effectsasm_fixedrdtscp, effect[], writerax, 32, writercx, 32, writerdx, 32, preserve, [], next

220instruction_effectsasm_fixedM, effect[], [], preserve, [], next ←

memberchkM, lfence, sfence, pause

222instruction_effectslabelS, effect[], [], preserve, [], label ←

atomS

223instruction_effectsD, effect[], [], preserve, [], directive ←

directiveD

225targetsymS, [], [] ←

atomS

226targetpltS, [], [] ←

atomS

227targetindO, Rs, Ms ←

sourceO, 64, Rs, Ms

O ≠ imm_

slow_call_stub?Helper, ?Labelnondet

Label is the compiler-local r10/r11 save stub for exactly Helper. Its emitter template is trusted; the native ABI fixture checks it.

slow_call_stub
233	filc_pollcheck_slow	'.Lnanofil_save_filc_pollcheck_slow'
234	filc_store_barrier_for_lower_slow	'.Lnanofil_save_filc_store_barrier_for_lower_slow'
235	filc_object_ensure_aux_ptr_outline	'.Lnanofil_save_filc_object_ensure_aux_ptr_outline'

preserving_call+Linesemidet

Line calls an authenticated local stub preserving full r10/r11 on normal return. No PLT or indirect target inherits this guarantee.

241preserving_callinscall, none, symLabel ←

slow_call_stub_, Label

243caller_clobberR, 64 ←

memberR, rax, rcx, rdx, rsi, rdi, r8, r9, r10, r11, rsp

244caller_clobberR, 128 ←

registerR, R, 128

245directivesectiontext

246directivep2alignN ←

integerN

247directivegloblS ←

atomS

248directivetypeS, function ←

atomS

249directivesizeS ←

atomS