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.

moduleamd64_contract

exportsinstruction_effects/2 register/3 explicit_registers/2 operand_register/2

useslists

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

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

58expressionE ←

integerE

59expressionE ←

atomE

60expressionA + B ←

expressionA

expressionB

61addressmemD, B, B ←

integerD

registerB, B, 64

62addressmemD, B, I, B, I ←

integerD

registerB, B, 64

registerI, I, 64

63addressripE, [] ←

expressionE

64addressgotpcrelS, [] ←

atomS

explicit_registers+Line, -Familiesdet

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

70explicit_registersins_, _, Os, Rs ←

findallR,

memberO, Os

operand_registerO, R

, Rs

72explicit_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.

77operand_registerregN, F ←

registerN, F, _

78operand_registerO, R ←

addressO, Rs

memberR, Rs

79operand_registerindO, R ←

operand_registerO, R

81sourceregR, W, F, [] ←

registerR, F, W

82sourceimmE, _, [], [] ←

expressionE

83sourceM, W, Rs, readM, N ←

addressM, Rs

N is W//8

84destinationregR, W, [], writeF, W, [] ←

registerR, F, W

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

addressM, Rs

N is W//8

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

87not_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.

99instruction_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

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

integerN

registerR, F, 64

105instruction_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

108instruction_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.

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

addressM, Rs

registerR, F, 32

114instruction_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

120instruction_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

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

widthS, W

sourceA, W, Rs, M₁

destinationA, W, _, Ws, M₂

appendM₁, M₂, Ms

127instruction_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

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

atom_concatset, CC, Op

conditionCC

registerR, F, 8

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

atom_concatcmov, CC, Op

conditionCC

registerA, FA, 64

registerB, FB, 64

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

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

137instruction_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
141	movzb	8
141	movsb	8
142	movzw	16
142	movsw	16
142	movsl	32

143shift_countregcl, rcx

144shift_countimmN, [] ←

integerN

N ≥ 0

N ≤ 255

145conditionCC ←

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.

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

sse_moveOp, W

sse_transferA, B, W, Rs, Ws, Ms

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

memberchkOp, add, sub, mul, div

memberchkS, ss, sd

registerA, A, 128

registerB, B, 128

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

memberchkOp, ucomiss, ucomisd

registerA, A, 128

registerB, B, 128

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

memberchkOp, cvtss2sd, cvtsd2ss

registerA, A, 128

registerB, B, 128

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

memberchkOp, cvttss2si, cvttsd2si

widthS, W

memberchkW, 32, 64

registerA, A, 128

registerB, F, W

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

memberchkOp, cvtsi2ss, cvtsi2sd

widthS, W

memberchkW, 32, 64

registerA, F, W

registerB, B, 128

168sse_movemovd, 32

168sse_movemovq, 64

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

registerA, F, W

registerB, B, 128

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

registerA, A, 128

registerB, F, W

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

targetT, Rs, Ms

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

atom_concatj, CC, Op

conditionCC

targetT, [], []

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

memberchkS, none, q

targetT, Rs, M

findallwriteR, W, caller_clobberR, W, Ws

appendM, read_writeruntime, unknown, Ms

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

registerR, F, 64

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

registerR, F, 64

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

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

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

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

194instruction_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.

201instruction_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.

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

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

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

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

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

memberchkM, lfence, sfence, pause

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

atomS

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

directiveD

221targetsymS, [], [] ←

atomS

222targetpltS, [], [] ←

atomS

223targetindO, Rs, Ms ←

sourceO, 64, Rs, Ms

O ≠ imm_

224caller_clobberR, 64 ←

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

225caller_clobberR, 128 ←

registerR, R, 128

226directivesectiontext

227directivep2alignN ←

integerN

228directivegloblS ←

atomS

229directivetypeS, function ←

atomS

230directivesizeS ←

atomS