1module Runtime.LaunchRecipe
2
3import Std.Foundation
4
5-- One bounded ALXR v1 expansion algorithm shared by host instruction emitters.
6-- The wire format and argument contract are documented by NativeLaunchRecipeRoutine.
7-- All pointers/extents are machine words; supplied input/output ranges must be
8-- valid, nonoverlapping and nonwrapping. Every read/write is checked against
9-- those ranges. This is a decoder for compiler-emitted bounded table recipes,
10-- not an OS mapping or pointer-validity checker.
11-- Immediates/displacements below are signed 32-bit bit patterns; loads are
12-- little-endian and permit unaligned access. Compare is unsigned left-right.
13-- Load8/32 zero-extend; Store8 truncates. Only explicit compares/tests supply
14-- branch flags, so other emitters need not reproduce unused arithmetic flags.
15-- SP denotes a private 64-byte scratch frame addressed by negative offsets.
16-- Each emitter supplies its ABI-compliant frame allocation and return sequence.
17-- A complete recipe consumes every input byte, fills the declared output and
18-- has a zero reserved header word. Accepting only its valid prefix would hide
19-- truncated operation counts or concatenated/corrupt tables.
20family LaunchRecipeCondition : Type 0
21constructor LaunchRecipeBelow
22constructor LaunchRecipeAbove
23constructor LaunchRecipeZero
24constructor LaunchRecipeNotZero
25end-family
26
27family LaunchRecipeBackend : Type 0
28parameter erased recipeAssembly : Type 0
29parameter erased recipeRegister : Type 0
30constructor LaunchRecipeBackendValue
31field unrestricted backendRecipeMove : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
32field unrestricted backendRecipeAdd : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
33field unrestricted backendRecipeSubtract : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
34field unrestricted backendRecipeAddImmediate : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
35field unrestricted backendRecipeCompare : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
36field unrestricted backendRecipeCompareImmediate : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
37field unrestricted backendRecipeTest : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeAssembly . recipeAssembly))
38field unrestricted backendRecipeLoad64 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : recipeAssembly . recipeAssembly))))
39field unrestricted backendRecipeLoad32 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : recipeAssembly . recipeAssembly))))
40field unrestricted backendRecipeLoad8 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
41field unrestricted backendRecipeStore64 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeRegister . (pi unrestricted a3 : recipeAssembly . recipeAssembly))))
42field unrestricted backendRecipeStore8 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
43field unrestricted backendRecipeClear : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeAssembly . recipeAssembly))
44field unrestricted backendRecipeMultiplyImmediate : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
45field unrestricted backendRecipeLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : recipeAssembly . recipeAssembly))
46field unrestricted backendRecipeJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : recipeAssembly . recipeAssembly))
47field unrestricted backendRecipeJumpIf : (pi unrestricted a0 : (family LaunchRecipeCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : recipeAssembly . recipeAssembly)))
48field unrestricted backendRecipeReturn : (pi unrestricted a0 : recipeAssembly . recipeAssembly)
49field unrestricted backendRecipeEnd : recipeAssembly
50field unrestricted backendRecipeRAX : recipeRegister
51field unrestricted backendRecipeRCX : recipeRegister
52field unrestricted backendRecipeRDX : recipeRegister
53field unrestricted backendRecipeRSI : recipeRegister
54field unrestricted backendRecipeRDI : recipeRegister
55field unrestricted backendRecipeRSP : recipeRegister
56field unrestricted backendRecipeR8 : recipeRegister
57field unrestricted backendRecipeR9 : recipeRegister
58field unrestricted backendRecipeR10 : recipeRegister
59field unrestricted backendRecipeR11 : recipeRegister
60end-family
61
62def lrLabelEntry : Bytes = b"alxr-entry"
63def lrLabelLoop : Bytes = b"alxr-loop"
64def lrLabelLiteral : Bytes = b"alxr-literal"
65def lrLabelLiteralLoop : Bytes = b"alxr-literal-loop"
66def lrLabelZero : Bytes = b"alxr-zero"
67def lrLabelZeroLoop : Bytes = b"alxr-zero-loop"
68def lrLabelRepeat : Bytes = b"alxr-repeat"
69def lrLabelUnitLoop : Bytes = b"alxr-unit-loop"
70def lrLabelNext : Bytes = b"alxr-next"
71def lrLabelCopyLoop : Bytes = b"alxr-copy-loop"
72def lrLabelPatchLoop : Bytes = b"alxr-patch-loop"
73def lrLabelPatchDone : Bytes = b"alxr-patch-done"
74def lrLabelRepeatDone : Bytes = b"alxr-repeat-done"
75def lrLabelDone : Bytes = b"alxr-done"
76def lrLabelFailed : Bytes = b"alxr-failed"
77
78def lrMagic : Nat = 0x52584c41
79def lrMinusEight : Nat = 0xfffffff8
80def lrSlotOutputStart : Nat = 0xfffffff8
81def lrSlotUnit : Nat = 0xfffffff0
82def lrSlotUnitLength : Nat = 0xffffffe8
83def lrSlotPatchCursor : Nat = 0xffffffe0
84def lrSlotPatchCount : Nat = 0xffffffd8
85def lrSlotRemaining : Nat = 0xffffffd0
86def lrSlotResume : Nat = 0xffffffc8
87def lrSlotPatchBase : Nat = 0xffffffc0
88
89def launchRecipeAssemblyFor =
90 (lambda erased A : Type 0 . (lambda erased R : Type 0 .
91 (lambda unrestricted backend : (family LaunchRecipeBackend A R) .
92 (eliminate LaunchRecipeBackend (lambda unrestricted current : (family LaunchRecipeBackend A R) . A) backend
93 (branch LaunchRecipeBackendValue
94 lrMove lrAdd lrSubtract lrAddImmediate lrCompare lrCompareImmediate lrTest lrLoad64 lrLoad32 lrLoad8 lrStore64 lrStore8 lrClear lrMultiplyImmediate lrLabel lrJump lrJumpIf lrReturn lrEnd
95 lrRAX lrRCX lrRDX lrRSI lrRDI lrRSP lrR8 lrR9 lrR10 lrR11 .
96 (let unrestricted lrBelow = (constructor LaunchRecipeCondition LaunchRecipeBelow) in
97 (let unrestricted lrAbove = (constructor LaunchRecipeCondition LaunchRecipeAbove) in
98 (let unrestricted lrZero = (constructor LaunchRecipeCondition LaunchRecipeZero) in
99 (let unrestricted lrNotZero = (constructor LaunchRecipeCondition LaunchRecipeNotZero) in
100 (let unrestricted lrEntryBlock =
101 (lambda unrestricted tail : A .
102 (lrLabel lrLabelEntry
103 (lrStore64 lrRSP lrSlotOutputStart lrRDX
104 (lrAdd lrRSI lrRDI
105 (lrAdd lrRCX lrRDX
106 (lrMove lrRAX lrRDI
107 (lrAddImmediate lrRAX 24
108 (lrCompare lrRAX lrRSI
109 (lrJumpIf lrAbove lrLabelFailed
110 (lrLoad32 lrR9 lrRDI 0
111 (lrCompareImmediate lrR9 lrMagic
112 (lrJumpIf lrNotZero lrLabelFailed
113 (lrLoad32 lrR9 lrRDI 4
114 (lrCompareImmediate lrR9 1
115 (lrJumpIf lrNotZero lrLabelFailed
116 (lrLoad64 lrR9 lrRDI 8
117 (lrAdd lrR9 lrRDX
118 (lrCompare lrR9 lrRCX
119 (lrJumpIf lrNotZero lrLabelFailed
120 (lrLoad32 lrR8 lrRDI 16
121 (lrLoad32 lrR9 lrRDI 20
122 (lrTest lrR9
123 (lrJumpIf lrNotZero lrLabelFailed
124 (lrAddImmediate lrRDI 24
125 (lrJump lrLabelLoop tail))))))))))))))))))))))))) in
126
127 -- Op dispatch: r8 ops remain; the op byte selects the block.
128
129 (let unrestricted lrLoopBlock =
130 (lambda unrestricted tail : A .
131 (lrLabel lrLabelLoop
132 (lrTest lrR8
133 (lrJumpIf lrZero lrLabelDone
134 (lrAddImmediate lrR8 0xffffffff
135 (lrCompare lrRDI lrRSI
136 (lrJumpIf lrAbove lrLabelFailed
137 (lrJumpIf lrZero lrLabelFailed
138 (lrLoad8 lrR9 lrRDI
139 (lrCompareImmediate lrR9 1
140 (lrJumpIf lrZero lrLabelLiteral
141 (lrCompareImmediate lrR9 2
142 (lrJumpIf lrZero lrLabelZero
143 (lrCompareImmediate lrR9 3
144 (lrJumpIf lrZero lrLabelRepeat
145 (lrJump lrLabelFailed tail)))))))))))))))) in
146
147 -- Reads the u32 length after the op byte into r10, advances rdi past it, and
148 -- checks the output has room; the caller checks the input.
149
150 (let unrestricted lrOperandLength =
151 (lambda unrestricted tail : A .
152 (lrMove lrRAX lrRDI
153 (lrAddImmediate lrRAX 5
154 (lrCompare lrRAX lrRSI
155 (lrJumpIf lrAbove lrLabelFailed
156 (lrLoad32 lrR10 lrRDI 1
157 (lrAddImmediate lrRDI 5
158 (lrMove lrRAX lrRDX
159 (lrAdd lrRAX lrR10
160 (lrCompare lrRAX lrRCX
161 (lrJumpIf lrAbove lrLabelFailed tail))))))))))) in
162
163 (let unrestricted lrLiteralBlock =
164 (lambda unrestricted tail : A .
165 (lrLabel lrLabelLiteral
166 (lrOperandLength
167 (lrMove lrRAX lrRDI
168 (lrAdd lrRAX lrR10
169 (lrCompare lrRAX lrRSI
170 (lrJumpIf lrAbove lrLabelFailed
171 (lrLabel lrLabelLiteralLoop
172 (lrTest lrR10
173 (lrJumpIf lrZero lrLabelLoop
174 (lrLoad8 lrR11 lrRDI
175 (lrStore8 lrRDX lrR11
176 (lrAddImmediate lrRDI 1
177 (lrAddImmediate lrRDX 1
178 (lrAddImmediate lrR10 0xffffffff
179 (lrJump lrLabelLiteralLoop tail)))))))))))))))) in
180
181 (let unrestricted lrZeroBlock =
182 (lambda unrestricted tail : A .
183 (lrLabel lrLabelZero
184 (lrOperandLength
185 (lrClear lrR11
186 (lrLabel lrLabelZeroLoop
187 (lrTest lrR10
188 (lrJumpIf lrZero lrLabelLoop
189 (lrStore8 lrRDX lrR11
190 (lrAddImmediate lrRDX 1
191 (lrAddImmediate lrR10 0xffffffff
192 (lrJump lrLabelZeroLoop tail))))))))))) in
193
194 -- REPEAT header: count (r9), unit length (r10), patch count (r11); the unit
195 -- and patch table must lie inside the recipe. The first copy is the unit
196 -- itself; the remaining count is saved for the copy loop.
197
198 (let unrestricted lrRepeatBlock =
199 (lambda unrestricted tail : A .
200 (lrLabel lrLabelRepeat
201 (lrMove lrRAX lrRDI
202 (lrAddImmediate lrRAX 13
203 (lrCompare lrRAX lrRSI
204 (lrJumpIf lrAbove lrLabelFailed
205 (lrLoad32 lrR9 lrRDI 1
206 (lrLoad32 lrR10 lrRDI 5
207 (lrLoad32 lrR11 lrRDI 9
208 (lrAddImmediate lrRDI 13
209 (lrTest lrR9
210 (lrJumpIf lrZero lrLabelFailed
211 (lrStore64 lrRSP lrSlotUnit lrRDI
212 (lrStore64 lrRSP lrSlotUnitLength lrR10
213 (lrStore64 lrRSP lrSlotPatchCount lrR11
214 (lrMove lrRAX lrRDI
215 (lrAdd lrRAX lrR10
216 (lrCompare lrRAX lrRSI
217 (lrJumpIf lrAbove lrLabelFailed
218 (lrStore64 lrRSP lrSlotPatchBase lrRAX
219 (lrMultiplyImmediate lrR11 12
220 (lrAdd lrRAX lrR11
221 (lrCompare lrRAX lrRSI
222 (lrJumpIf lrAbove lrLabelFailed
223 (lrStore64 lrRSP lrSlotResume lrRAX
224 (lrAddImmediate lrR9 0xffffffff
225 (lrStore64 lrRSP lrSlotRemaining lrR9
226 (lrMove lrRAX lrRDX
227 (lrAdd lrRAX lrR10
228 (lrCompare lrRAX lrRCX
229 (lrJumpIf lrAbove lrLabelFailed
230 (lrLabel lrLabelUnitLoop
231 (lrTest lrR10
232 (lrJumpIf lrZero lrLabelNext
233 (lrLoad8 lrR11 lrRDI
234 (lrStore8 lrRDX lrR11
235 (lrAddImmediate lrRDI 1
236 (lrAddImmediate lrRDX 1
237 (lrAddImmediate lrR10 0xffffffff
238 (lrJump lrLabelUnitLoop tail)))))))))))))))))))))))))))))))))))))))) in
239
240 -- Each further copy duplicates the previous copy (rax reads, rdx writes),
241 -- then adds the patch strides to the new copy at r11.
242
243 (let unrestricted lrNextBlock =
244 (lambda unrestricted tail : A .
245 (lrLabel lrLabelNext
246 (lrLoad64 lrR9 lrRSP lrSlotRemaining
247 (lrTest lrR9
248 (lrJumpIf lrZero lrLabelRepeatDone
249 (lrAddImmediate lrR9 0xffffffff
250 (lrStore64 lrRSP lrSlotRemaining lrR9
251 (lrLoad64 lrR10 lrRSP lrSlotUnitLength
252 (lrMove lrRAX lrRDX
253 (lrAdd lrRAX lrR10
254 (lrCompare lrRAX lrRCX
255 (lrJumpIf lrAbove lrLabelFailed
256 (lrMove lrR11 lrRDX
257 (lrMove lrRAX lrRDX
258 (lrSubtract lrRAX lrR10
259 (lrLabel lrLabelCopyLoop
260 (lrTest lrR10
261 (lrJumpIf lrZero lrLabelPatchLoop
262 (lrLoad8 lrR9 lrRAX
263 (lrStore8 lrRDX lrR9
264 (lrAddImmediate lrRAX 1
265 (lrAddImmediate lrRDX 1
266 (lrAddImmediate lrR10 0xffffffff
267 (lrJump lrLabelCopyLoop tail)))))))))))))))))))))))) in
268
269 -- Patches: r10 counts down, the cursor slot walks the table; r9 is the word
270 -- address, rdi (free inside a repeat) the word, rax the stride.
271
272 (let unrestricted lrPatchBlock =
273 (lambda unrestricted tail : A .
274 (lrLabel lrLabelPatchLoop
275 (lrLoad64 lrR9 lrRSP lrSlotPatchBase
276 (lrStore64 lrRSP lrSlotPatchCursor lrR9
277 (lrLoad64 lrR10 lrRSP lrSlotPatchCount
278 (lrLabel lrLabelPatchDone
279 (lrTest lrR10
280 (lrJumpIf lrZero lrLabelNext
281 (lrLoad64 lrR9 lrRSP lrSlotPatchCursor
282 (lrLoad32 lrRDI lrR9 0
283 (lrLoad64 lrRAX lrR9 4
284 (lrAddImmediate lrR9 12
285 (lrStore64 lrRSP lrSlotPatchCursor lrR9
286 (lrMove lrR9 lrRDI
287 (lrAddImmediate lrR9 8
288 (lrLoad64 lrRDI lrRSP lrSlotUnitLength
289 (lrCompare lrR9 lrRDI
290 (lrJumpIf lrAbove lrLabelFailed
291 (lrAddImmediate lrR9 lrMinusEight
292 (lrAdd lrR9 lrR11
293 (lrLoad64 lrRDI lrR9 0
294 (lrAdd lrRDI lrRAX
295 (lrStore64 lrR9 0 lrRDI
296 (lrAddImmediate lrR10 0xffffffff
297 (lrJump lrLabelPatchDone tail))))))))))))))))))))))))) in
298
299 (let unrestricted lrRepeatDoneBlock =
300 (lambda unrestricted tail : A .
301 (lrLabel lrLabelRepeatDone
302 (lrLoad64 lrRDI lrRSP lrSlotResume
303 (lrJump lrLabelLoop tail)))) in
304
305 (let unrestricted lrDoneBlock =
306 (lambda unrestricted tail : A .
307 (lrLabel lrLabelDone
308 (lrCompare lrRDX lrRCX
309 (lrJumpIf lrNotZero lrLabelFailed
310 (lrCompare lrRDI lrRSI
311 (lrJumpIf lrNotZero lrLabelFailed
312 (lrMove lrRAX lrRDX
313 (lrLoad64 lrR9 lrRSP lrSlotOutputStart
314 (lrSubtract lrRAX lrR9
315 (lrReturn tail)))))))))) in
316
317 (let unrestricted lrFailedBlock =
318 (lambda unrestricted tail : A .
319 (lrLabel lrLabelFailed
320 (lrClear lrRAX
321 (lrReturn tail)))) in
322
323 (lrEntryBlock
324 (lrLoopBlock
325 (lrLiteralBlock
326 (lrZeroBlock
327 (lrRepeatBlock
328 (lrNextBlock
329 (lrPatchBlock
330 (lrRepeatDoneBlock
331 (lrDoneBlock
332 (lrFailedBlock lrEnd))))))))))))))))))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.