Fil-C on Nix

Filnix wiki

mbrock/filnix/nanofil

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

useslists

12:- discontiguousinstruction_effects/2

Concrete names index directly; family/width queries generate the name without searching every family for every operand in a large function.

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

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

54expressionE ←

integerE

!

55expressionE ←

atomE

!

56expressionA + B ←

57addressmemD, B, B ←

integerD

registerB, B, 64

58addressmemD, B, I, B, I ←

integerD

registerB, B, 64

registerI, I, 64

59addressripE, [] ←

60addressgotpcrelS, [] ←

atomS

62explicit_registersins_, _, Os, Rs ←

!

findallR,

memberO, Os

operand_registerO, R

, Rs

64explicit_registers_, []

65operand_registerregN, F ←

registerN, F, _

66operand_registerO, R ←

memberR, Rs

67operand_registerindO, R ←

operand_registerO, R

69sourceregR, W, F, [] ←

registerR, F, W

70sourceimmE, _, [], [] ←

71sourceM, W, Rs, readM, N ←

N is W//8

72destinationregR, W, [], writeF, W, [] ←

registerR, F, W

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

N is W//8

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

75not_two_memoryA, B ←

¬

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

sourceA, W, R₁, M₁

destinationB, W, R₂, Ws, M₂

not_two_memoryA, B

appendR₁, R₂, Rs

appendM₁, M₂, Ms

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

integerN

registerR, F, 64

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

extensionOp, From

W > From

sourceA, From, Rs, Ms

A ≠ imm_

registerR, F, W

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

registerR, F, 64

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

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

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

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

memberchkOp, cmp, test

sourceA, W, R₁, M₁

sourceB, W, R₂, M₂

B ≠ imm_

not_two_memoryA, B

appendR₁, R₂, Rs

appendM₁, M₂, Ms

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

sourceA, W, Rs, M₁

destinationA, W, _, Ws, M₂

appendM₁, M₂, Ms

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

memberchkOp, shl, shr, sar

shift_countCount, R₁

sourceA, W, R₂, M₁

destinationA, W, _, Ws, M₂

appendR₁, R₂, Rs

appendM₁, M₂, Ms

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

atom_concatset, CC, Op

registerR, F, 8

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

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

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

memberchkOp, div, idiv

memberchkW, 32, 64

sourceA, W, Rs, Ms

A ≠ imm_

Ws = writerax, W, writerdx, W

extension
113	movzb	8
113	movsb	8
114	movzw	16
114	movsw	16
114	movsl	32

115shift_countregcl, rcx

116shift_countimmN, [] ←

integerN

N ≥ 0

N ≤ 255

117conditionCC ←

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.

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

sse_transferA, B, W, Rs, Ws, Ms

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

memberchkOp, add, sub, mul, div

memberchkS, ss, sd

registerA, A, 128

registerB, B, 128

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

memberchkOp, ucomiss, ucomisd

registerA, A, 128

registerB, B, 128

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

memberchkOp, cvtss2sd, cvtsd2ss

registerA, A, 128

registerB, B, 128

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

memberchkOp, cvttss2si, cvttsd2si

memberchkW, 32, 64

registerA, A, 128

registerB, F, W

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

memberchkOp, cvtsi2ss, cvtsi2sd

memberchkW, 32, 64

registerA, F, W

registerB, B, 128

140sse_movemovd, 32

140sse_movemovq, 64

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

registerA, F, W

registerB, B, 128

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

registerA, A, 128

registerB, F, W

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

targetT, Rs, Ms

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

atom_concatj, CC, Op

targetT, [], []

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

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

registerR, F, 64

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

registerR, F, 64

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

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

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

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

atomS

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

168targetsymS, [], [] ←

atomS

169targetpltS, [], [] ←

atomS

170targetindO, Rs, Ms ←

sourceO, 64, Rs, Ms

O ≠ imm_

171caller_clobberR, 64 ←

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

172caller_clobberR, 128 ←

registerR, R, 128

173directivesectiontext

174directivep2alignN ←

integerN

175directivegloblS ←

atomS

176directivetypeS, function ←

atomS

177directivesizeS ←

atomS