Platform.AArch64.RoutineEmitter

1module Platform.AArch64.RoutineEmitter
2
3import Compiler.MachineAArch64
4import Compiler.MachineAArch64Assembly
5import Std.Natural
6
7-- Shared instruction builders for small inline host routines. Logical registers
8-- are supplied by each caller. x16 and x17 are reserved scratch registers: no
9-- input, output or live value may use them. Signed imm32 conversion is explicit
10-- so decrements and private-frame offsets mean the same on both host ISAs.
11-- These builders do not provide a calling convention or preserve registers;
12-- the routine's entry/return and its caller contract own that responsibility.
13def ahrX0 = (constructor AArch64Register AArch64X0)
14def ahrX1 = (constructor AArch64Register AArch64X1)
15def ahrX2 = (constructor AArch64Register AArch64X2)
16def ahrX3 = (constructor AArch64Register AArch64X3)
17def ahrX4 = (constructor AArch64Register AArch64X4)
18def ahrX5 = (constructor AArch64Register AArch64X5)
19def ahrX6 = (constructor AArch64Register AArch64X6)
20def ahrX7 = (constructor AArch64Register AArch64X7)
21def ahrX8 = (constructor AArch64Register AArch64X8)
22def ahrX9 = (constructor AArch64Register AArch64X9)
23def ahrX10 = (constructor AArch64Register AArch64X10)
24def ahrX11 = (constructor AArch64Register AArch64X11)
25def ahrX12 = (constructor AArch64Register AArch64X12)
26def ahrX13 = (constructor AArch64Register AArch64X13)
27def ahrX14 = (constructor AArch64Register AArch64X14)
28def ahrX15 = (constructor AArch64Register AArch64X15)
29def ahrX16 = (constructor AArch64Register AArch64X16)
30def ahrX17 = (constructor AArch64Register AArch64X17)
31
32def ahrEmit = (lambda unrestricted instruction : (family AArch64Instruction) .
33  (lambda unrestricted rest : (family AArch64Assembly) .
34    (constructor AArch64Assembly AArch64AssemblyEmit instruction rest)))
35def ahrAddress = (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
36  (ahrEmit (constructor AArch64Instruction AArch64AddImmediate ahrX16 base at))))
37def ahrLoad32 = (lambda unrestricted destination : (family AArch64Register) .
38  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
39    (lambda unrestricted rest : (family AArch64Assembly) .
40      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64LoadMemory32ZeroExtend destination ahrX16 0) rest))))))
41def ahrLoad64 = (lambda unrestricted destination : (family AArch64Register) .
42  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
43    (lambda unrestricted rest : (family AArch64Assembly) .
44      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64LoadMemory64 destination ahrX16 0) rest))))))
45def ahrLoad8 = (lambda unrestricted destination : (family AArch64Register) .
46  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted at : Nat .
47    (lambda unrestricted rest : (family AArch64Assembly) .
48      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64LoadMemory8ZeroExtend destination ahrX16 0) rest))))))
49def ahrStore32 = (lambda unrestricted base : (family AArch64Register) .
50  (lambda unrestricted at : Nat . (lambda unrestricted source : (family AArch64Register) .
51    (lambda unrestricted rest : (family AArch64Assembly) .
52      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64StoreMemory32 ahrX16 0 source) rest))))))
53def ahrStore64 = (lambda unrestricted base : (family AArch64Register) .
54  (lambda unrestricted at : Nat . (lambda unrestricted source : (family AArch64Register) .
55    (lambda unrestricted rest : (family AArch64Assembly) .
56      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64 ahrX16 0 source) rest))))))
57def ahrStore8 = (lambda unrestricted base : (family AArch64Register) .
58  (lambda unrestricted at : Nat . (lambda unrestricted source : (family AArch64Register) .
59    (lambda unrestricted rest : (family AArch64Assembly) .
60      (ahrAddress base at (ahrEmit (constructor AArch64Instruction AArch64StoreMemory8 ahrX16 0 source) rest))))))
61
62def ahrMov = (lambda unrestricted destination : (family AArch64Register) .
63  (lambda unrestricted source : (family AArch64Register) .
64    (ahrEmit (constructor AArch64Instruction AArch64MoveRegister destination source))))
65def ahrAdd = (lambda unrestricted destination : (family AArch64Register) .
66  (lambda unrestricted source : (family AArch64Register) .
67    (ahrEmit (constructor AArch64Instruction AArch64AddRegister destination destination source))))
68def ahrAnd = (lambda unrestricted destination : (family AArch64Register) .
69  (lambda unrestricted source : (family AArch64Register) .
70    (ahrEmit (constructor AArch64Instruction AArch64AndRegister destination destination source))))
71def ahrOr = (lambda unrestricted destination : (family AArch64Register) .
72  (lambda unrestricted source : (family AArch64Register) .
73    (ahrEmit (constructor AArch64Instruction AArch64OrRegister destination destination source))))
74def ahrXor = (lambda unrestricted destination : (family AArch64Register) .
75  (lambda unrestricted source : (family AArch64Register) .
76    (ahrEmit (constructor AArch64Instruction AArch64ExclusiveOrRegister destination destination source))))
77def ahrShl = (lambda unrestricted destination : (family AArch64Register) .
78  (lambda unrestricted amount : Nat .
79    (ahrEmit (constructor AArch64Instruction AArch64ShiftLeftImmediate destination destination amount))))
80def ahrShr = (lambda unrestricted destination : (family AArch64Register) .
81  (lambda unrestricted amount : Nat .
82    (ahrEmit (constructor AArch64Instruction AArch64ShiftRightImmediate destination destination amount))))
83
84-- MOV imm32 zero-extends, while arithmetic imm32 sign-extends. In particular
85-- the shared loop decrement is 0xffffffff, which must become -1, not +2^32-1.
86def ahrMovImm = (lambda unrestricted destination : (family AArch64Register) .
87  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
88    (ahrEmit (constructor AArch64Instruction AArch64MoveWideZero destination
89      (naturalModuloUnchecked value 65536) (constructor AArch64HalfwordShift AArch64Shift0))
90      (ahrEmit (constructor AArch64Instruction AArch64MoveWideKeep destination
91        (naturalModuloUnchecked (naturalDivideUnchecked value 65536) 65536)
92        (constructor AArch64HalfwordShift AArch64Shift16)) rest)))))
93
94def ahrSignedImm = (lambda unrestricted destination : (family AArch64Register) .
95  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
96    (ahrMovImm destination value
97      (nat-eliminate (lambda unrestricted sign : Nat . (family AArch64Assembly)) rest
98        (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family AArch64Assembly) .
99          (ahrEmit (constructor AArch64Instruction AArch64MoveWideKeep destination 65535
100            (constructor AArch64HalfwordShift AArch64Shift32))
101            (ahrEmit (constructor AArch64Instruction AArch64MoveWideKeep destination 65535
102              (constructor AArch64HalfwordShift AArch64Shift48)) rest))))
103        (naturalModuloUnchecked (naturalDivideUnchecked value 2147483648) 2))))))
104
105def ahrAddImm = (lambda unrestricted destination : (family AArch64Register) .
106  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
107    (ahrSignedImm ahrX17 value (ahrAdd destination ahrX17
108      (ahrEmit (constructor AArch64Instruction AArch64CompareImmediate destination 0) rest))))))
109def ahrAndImm = (lambda unrestricted destination : (family AArch64Register) .
110  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
111    (ahrSignedImm ahrX17 value (ahrAnd destination ahrX17 rest)))))
112def ahrCmpImm = (lambda unrestricted destination : (family AArch64Register) .
113  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
114    (ahrSignedImm ahrX17 value
115      (ahrEmit (constructor AArch64Instruction AArch64CompareRegister destination ahrX17) rest)))))
116def ahrMulImm = (lambda unrestricted destination : (family AArch64Register) .
117  (lambda unrestricted value : Nat . (lambda unrestricted rest : (family AArch64Assembly) .
118    (ahrSignedImm ahrX17 value
119      (ahrEmit (constructor AArch64Instruction AArch64MultiplyRegister destination destination ahrX17) rest)))))
120
121def ahrLabel = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family AArch64Assembly) .
122  (constructor AArch64Assembly AArch64AssemblyLabel name rest)))
123def ahrBranch = (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family AArch64Assembly) .
124  (constructor AArch64Assembly AArch64AssemblyBranch name rest)))
125def ahrBranchIf = (lambda unrestricted condition : (family AArch64Condition) .
126  (lambda unrestricted name : Bytes . (lambda unrestricted rest : (family AArch64Assembly) .
127    (constructor AArch64Assembly AArch64AssemblyBranchIf condition name rest))))
128def ahrReturn = (ahrEmit (constructor AArch64Instruction AArch64Return))
129def ahrEnd = (constructor AArch64Assembly AArch64AssemblyEnd)
130
131-- Typed AArch64 assembly is decided by its maintained Alpha assembler. An
132-- unresolved label or refused operand remains an empty artifact for the
133-- enclosing checked ELF emitter to refuse; no host assembler is consulted.
134def aarch64RoutineBytes =
135  (lambda unrestricted assembly : (family AArch64Assembly) .
136    (eliminate AArch64AssemblyResult
137      (lambda unrestricted result : (family AArch64AssemblyResult) . Bytes)
138      (aarch64Assemble assembly)
139      (branch AArch64AssemblyEncoded code . code)
140      (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
141      (branch AArch64AssemblyMissingLabel name . b"")
142      (branch AArch64AssemblyDisplacementOutOfRange name . b"")
143      (branch AArch64AssemblyOperandRefused value . b"")))