1module Compiler.MachineAArch64Assembly
2
3import Compiler.MachineAArch64
4import Data.Bytes
5import Model.Config
6import Model.Word32
7import Std.Byte
8import Std.Natural
9
10-- The AArch64 twin of Compiler.MachineX86NativeAssembly: a program with
11-- named labels, laid out in one pass and encoded in a second. Every item
12-- occupies exactly one 32-bit word except a label, which occupies none, so
13-- layout is arithmetic rather than encoding. A branch's displacement is
14-- measured from the branch itself (A64), where x86-64 measures from the end
15-- of the instruction; that is the one place the two assemblers differ.
16family AArch64Assembly : Type 0
17constructor AArch64AssemblyEnd
18constructor AArch64AssemblyEmit
19field unrestricted aarch64AssemblyInstruction : (family AArch64Instruction)
20recursive unrestricted aarch64AssemblyAfterInstruction
21constructor AArch64AssemblyLabel
22field unrestricted aarch64AssemblyLabelName : Bytes
23recursive unrestricted aarch64AssemblyAfterLabel
24constructor AArch64AssemblyBranch
25field unrestricted aarch64AssemblyBranchTarget : Bytes
26recursive unrestricted aarch64AssemblyAfterBranch
27constructor AArch64AssemblyBranchLink
28field unrestricted aarch64AssemblyBranchLinkTarget : Bytes
29recursive unrestricted aarch64AssemblyAfterBranchLink
30constructor AArch64AssemblyBranchIf
31field unrestricted aarch64AssemblyBranchIfCondition : (family AArch64Condition)
32field unrestricted aarch64AssemblyBranchIfTarget : Bytes
33recursive unrestricted aarch64AssemblyAfterBranchIf
34constructor AArch64AssemblyCompareBranchIfZero
35field unrestricted aarch64AssemblyCompareBranchIfZeroRegister : (family AArch64Register)
36field unrestricted aarch64AssemblyCompareBranchIfZeroTarget : Bytes
37recursive unrestricted aarch64AssemblyAfterCompareBranchIfZero
38constructor AArch64AssemblyCompareBranchIfNotZero
39field unrestricted aarch64AssemblyCompareBranchIfNotZeroRegister : (family AArch64Register)
40field unrestricted aarch64AssemblyCompareBranchIfNotZeroTarget : Bytes
41recursive unrestricted aarch64AssemblyAfterCompareBranchIfNotZero
42constructor AArch64AssemblyAddressOf
43field unrestricted aarch64AssemblyAddressOfDestination : (family AArch64Register)
44field unrestricted aarch64AssemblyAddressOfTarget : Bytes
45recursive unrestricted aarch64AssemblyAfterAddressOf
46
47end-family
48
49family AArch64LabelTable : Type 0
50constructor AArch64LabelTableEmpty
51constructor AArch64LabelTableEntry
52field unrestricted aarch64LabelName : Bytes
53field unrestricted aarch64LabelOffset : Nat
54recursive unrestricted aarch64RemainingLabels
55
56end-family
57
58family AArch64LabelLookupResult : Type 0
59constructor AArch64LabelFound
60field unrestricted aarch64FoundLabelOffset : Nat
61constructor AArch64LabelMissing
62
63end-family
64
65family AArch64AssemblyLayoutResult : Type 0
66constructor AArch64AssemblyLayoutSuccess
67field unrestricted aarch64AssemblyLabels : (family AArch64LabelTable)
68field unrestricted aarch64AssemblySize : Nat
69constructor AArch64AssemblyDuplicateLabel
70field unrestricted aarch64DuplicateLabelName : Bytes
71
72end-family
73
74family AArch64AssemblyResult : Type 0
75constructor AArch64AssemblyEncoded
76field unrestricted aarch64AssemblyEncodedBytes : Bytes
77constructor AArch64AssemblyEncodeDuplicateLabel
78field unrestricted aarch64AssemblyEncodeDuplicateName : Bytes
79constructor AArch64AssemblyMissingLabel
80field unrestricted aarch64AssemblyMissingLabelName : Bytes
81constructor AArch64AssemblyDisplacementOutOfRange
82field unrestricted aarch64AssemblyDisplacementLabelName : Bytes
83constructor AArch64AssemblyOperandRefused
84field unrestricted aarch64AssemblyOperandRefusedValue : Nat
85
86end-family
87
88def aarch64LookupLabel :
89 (pi unrestricted name : Bytes .
90 (pi unrestricted labels : (family AArch64LabelTable) . (family AArch64LabelLookupResult))) =
91 (lambda unrestricted name : Bytes .
92 (lambda unrestricted labels : (family AArch64LabelTable) .
93 (eliminate
94 AArch64LabelTable
95 (lambda unrestricted current : (family AArch64LabelTable) .
96 (family AArch64LabelLookupResult))
97 labels
98 (branch AArch64LabelTableEmpty . (constructor AArch64LabelLookupResult AArch64LabelMissing))
99 (branch
100 AArch64LabelTableEntry
101 entryName
102 entryOffset
103 remaining
104 lookupRemaining
105 .
106 (nat-eliminate
107 (lambda unrestricted matches : Nat . (family AArch64LabelLookupResult))
108 lookupRemaining
109 (lambda unrestricted predecessor : Nat .
110 (lambda unrestricted induction : (family AArch64LabelLookupResult) .
111 (constructor AArch64LabelLookupResult AArch64LabelFound entryOffset)))
112 (bytes-equal entryName name))))))
113
114-- Layout: every item but a label is one word. Labels are recorded at the
115-- offset of the word that follows them; a duplicate name is refused.
116def aarch64LayoutAssemblyFrom :
117 (pi unrestricted assembly : (family AArch64Assembly) .
118 (pi unrestricted offset : Nat . (family AArch64AssemblyLayoutResult))) =
119 (lambda unrestricted assembly : (family AArch64Assembly) .
120 (eliminate
121 AArch64Assembly
122 (lambda unrestricted current : (family AArch64Assembly) .
123 (pi unrestricted offset : Nat . (family AArch64AssemblyLayoutResult)))
124 assembly
125 (branch
126 AArch64AssemblyEnd
127 .
128 (lambda unrestricted offset : Nat .
129 (constructor
130 AArch64AssemblyLayoutResult
131 AArch64AssemblyLayoutSuccess
132 (constructor AArch64LabelTable AArch64LabelTableEmpty)
133 offset)))
134 (branch
135 AArch64AssemblyEmit
136 instruction
137 tail
138 layoutTail
139 .
140 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
141 (branch
142 AArch64AssemblyLabel
143 name
144 tail
145 layoutTail
146 .
147 (lambda unrestricted offset : Nat .
148 (eliminate
149 AArch64AssemblyLayoutResult
150 (lambda unrestricted current : (family AArch64AssemblyLayoutResult) .
151 (family AArch64AssemblyLayoutResult))
152 (layoutTail offset)
153 (branch
154 AArch64AssemblyLayoutSuccess
155 labels
156 finalSize
157 .
158 (eliminate
159 AArch64LabelLookupResult
160 (lambda unrestricted lookup : (family AArch64LabelLookupResult) .
161 (family AArch64AssemblyLayoutResult))
162 (aarch64LookupLabel name labels)
163 (branch
164 AArch64LabelFound
165 existing
166 .
167 (constructor AArch64AssemblyLayoutResult AArch64AssemblyDuplicateLabel name))
168 (branch
169 AArch64LabelMissing
170 .
171 (constructor
172 AArch64AssemblyLayoutResult
173 AArch64AssemblyLayoutSuccess
174 (constructor AArch64LabelTable AArch64LabelTableEntry name offset labels)
175 finalSize))))
176 (branch
177 AArch64AssemblyDuplicateLabel
178 duplicate
179 .
180 (constructor AArch64AssemblyLayoutResult AArch64AssemblyDuplicateLabel duplicate)))))
181 (branch
182 AArch64AssemblyBranch
183 target
184 tail
185 layoutTail
186 .
187 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
188 (branch
189 AArch64AssemblyBranchLink
190 target
191 tail
192 layoutTail
193 .
194 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
195 (branch
196 AArch64AssemblyBranchIf
197 condition
198 target
199 tail
200 layoutTail
201 .
202 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
203 (branch
204 AArch64AssemblyCompareBranchIfZero
205 register
206 target
207 tail
208 layoutTail
209 .
210 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
211 (branch
212 AArch64AssemblyCompareBranchIfNotZero
213 register
214 target
215 tail
216 layoutTail
217 .
218 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
219 (branch
220 AArch64AssemblyAddressOf
221 destination
222 target
223 tail
224 layoutTail
225 .
226 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))))
227
228def aarch64LayoutAssembly :
229 (pi unrestricted assembly : (family AArch64Assembly) . (family AArch64AssemblyLayoutResult)) =
230 (lambda unrestricted assembly : (family AArch64Assembly) . (aarch64LayoutAssemblyFrom assembly 0))
231
232-- The direction and byte distance from the referencing word to a target.
233def aarch64DirectionTo =
234 (lambda unrestricted source : Nat .
235 (lambda unrestricted target : Nat .
236 (nat-eliminate
237 (lambda unrestricted backward : Nat . (family AArch64Direction))
238 (constructor AArch64Direction AArch64Forward)
239 (lambda unrestricted predecessor : Nat .
240 (lambda unrestricted induction : (family AArch64Direction) .
241 (constructor AArch64Direction AArch64Backward)))
242 (naturalLess target source))))
243
244def aarch64DistanceTo =
245 (lambda unrestricted source : Nat .
246 (lambda unrestricted target : Nat .
247 (nat-eliminate
248 (lambda unrestricted backward : Nat . Nat)
249 (naturalSaturatingSubtract target source)
250 (lambda unrestricted predecessor : Nat .
251 (lambda unrestricted induction : Nat . (naturalSaturatingSubtract source target)))
252 (naturalLess target source))))
253
254-- One encoded word in front of the tail's result; the first refusal wins.
255def aarch64PrependWord =
256 (lambda unrestricted name : Bytes .
257 (lambda unrestricted word : (family AArch64EncodeResult) .
258 (lambda unrestricted tailResult : (family AArch64AssemblyResult) .
259 (eliminate
260 AArch64EncodeResult
261 (lambda unrestricted current : (family AArch64EncodeResult) .
262 (family AArch64AssemblyResult))
263 word
264 (branch
265 AArch64Encoded
266 encoded
267 .
268 (eliminate
269 AArch64AssemblyResult
270 (lambda unrestricted current : (family AArch64AssemblyResult) .
271 (family AArch64AssemblyResult))
272 tailResult
273 (branch
274 AArch64AssemblyEncoded
275 tailBytes
276 .
277 (constructor
278 AArch64AssemblyResult
279 AArch64AssemblyEncoded
280 (bytes-append encoded tailBytes)))
281 (branch
282 AArch64AssemblyEncodeDuplicateLabel
283 duplicate
284 .
285 (constructor AArch64AssemblyResult AArch64AssemblyEncodeDuplicateLabel duplicate))
286 (branch
287 AArch64AssemblyMissingLabel
288 missing
289 .
290 (constructor AArch64AssemblyResult AArch64AssemblyMissingLabel missing))
291 (branch
292 AArch64AssemblyDisplacementOutOfRange
293 label
294 .
295 (constructor AArch64AssemblyResult AArch64AssemblyDisplacementOutOfRange label))
296 (branch
297 AArch64AssemblyOperandRefused
298 value
299 .
300 (constructor AArch64AssemblyResult AArch64AssemblyOperandRefused value))))
301 (branch
302 AArch64ImmediateOutOfRange
303 value
304 .
305 (constructor AArch64AssemblyResult AArch64AssemblyOperandRefused value))
306 (branch
307 AArch64MisalignedOffset
308 value
309 .
310 (constructor AArch64AssemblyResult AArch64AssemblyDisplacementOutOfRange name))
311 (branch
312 AArch64DisplacementOutOfRange
313 value
314 .
315 (constructor AArch64AssemblyResult AArch64AssemblyDisplacementOutOfRange name))))))
316
317-- Encode a label-relative word: look the target up, then build the
318-- instruction with the direction and distance from this word.
319def aarch64EncodeToLabel =
320 (lambda unrestricted name : Bytes .
321 (lambda unrestricted labels : (family AArch64LabelTable) .
322 (lambda unrestricted source : Nat .
323 (lambda unrestricted build : (pi unrestricted direction : (family AArch64Direction) . (pi unrestricted distance : Nat . (family AArch64Instruction))) .
324 (lambda unrestricted tailResult : (family AArch64AssemblyResult) .
325 (eliminate
326 AArch64LabelLookupResult
327 (lambda unrestricted lookup : (family AArch64LabelLookupResult) .
328 (family AArch64AssemblyResult))
329 (aarch64LookupLabel name labels)
330 (branch
331 AArch64LabelFound
332 target
333 .
334 (aarch64PrependWord
335 name
336 (aarch64EncodeInstruction
337 (build (aarch64DirectionTo source target) (aarch64DistanceTo source target)))
338 tailResult))
339 (branch
340 AArch64LabelMissing
341 .
342 (constructor AArch64AssemblyResult AArch64AssemblyMissingLabel name))))))))
343
344def aarch64EncodeAssemblyFrom :
345 (pi unrestricted assembly : (family AArch64Assembly) .
346 (pi unrestricted labels : (family AArch64LabelTable) .
347 (pi unrestricted offset : Nat . (family AArch64AssemblyResult)))) =
348 (lambda unrestricted assembly : (family AArch64Assembly) .
349 (eliminate
350 AArch64Assembly
351 (lambda unrestricted current : (family AArch64Assembly) .
352 (pi unrestricted labels : (family AArch64LabelTable) .
353 (pi unrestricted offset : Nat . (family AArch64AssemblyResult))))
354 assembly
355 (branch
356 AArch64AssemblyEnd
357 .
358 (lambda unrestricted labels : (family AArch64LabelTable) .
359 (lambda unrestricted offset : Nat .
360 (constructor AArch64AssemblyResult AArch64AssemblyEncoded b""))))
361 (branch
362 AArch64AssemblyEmit
363 instruction
364 tail
365 encodeTail
366 .
367 (lambda unrestricted labels : (family AArch64LabelTable) .
368 (lambda unrestricted offset : Nat .
369 (aarch64PrependWord
370 b""
371 (aarch64EncodeInstruction instruction)
372 (encodeTail labels (naturalAdd offset 4))))))
373 (branch
374 AArch64AssemblyLabel
375 name
376 tail
377 encodeTail
378 .
379 (lambda unrestricted labels : (family AArch64LabelTable) .
380 (lambda unrestricted offset : Nat . (encodeTail labels offset))))
381 (branch
382 AArch64AssemblyBranch
383 target
384 tail
385 encodeTail
386 .
387 (lambda unrestricted labels : (family AArch64LabelTable) .
388 (lambda unrestricted offset : Nat .
389 (aarch64EncodeToLabel
390 target
391 labels
392 offset
393 (lambda unrestricted direction : (family AArch64Direction) .
394 (lambda unrestricted distance : Nat .
395 (constructor AArch64Instruction AArch64Branch direction distance)))
396 (encodeTail labels (naturalAdd offset 4))))))
397 (branch
398 AArch64AssemblyBranchLink
399 target
400 tail
401 encodeTail
402 .
403 (lambda unrestricted labels : (family AArch64LabelTable) .
404 (lambda unrestricted offset : Nat .
405 (aarch64EncodeToLabel
406 target
407 labels
408 offset
409 (lambda unrestricted direction : (family AArch64Direction) .
410 (lambda unrestricted distance : Nat .
411 (constructor AArch64Instruction AArch64BranchLink direction distance)))
412 (encodeTail labels (naturalAdd offset 4))))))
413 (branch
414 AArch64AssemblyBranchIf
415 condition
416 target
417 tail
418 encodeTail
419 .
420 (lambda unrestricted labels : (family AArch64LabelTable) .
421 (lambda unrestricted offset : Nat .
422 (aarch64EncodeToLabel
423 target
424 labels
425 offset
426 (lambda unrestricted direction : (family AArch64Direction) .
427 (lambda unrestricted distance : Nat .
428 (constructor AArch64Instruction AArch64BranchIf condition direction distance)))
429 (encodeTail labels (naturalAdd offset 4))))))
430 (branch
431 AArch64AssemblyCompareBranchIfZero
432 register
433 target
434 tail
435 encodeTail
436 .
437 (lambda unrestricted labels : (family AArch64LabelTable) .
438 (lambda unrestricted offset : Nat .
439 (aarch64EncodeToLabel
440 target
441 labels
442 offset
443 (lambda unrestricted direction : (family AArch64Direction) .
444 (lambda unrestricted distance : Nat .
445 (constructor
446 AArch64Instruction
447 AArch64CompareBranchIfZero
448 register
449 direction
450 distance)))
451 (encodeTail labels (naturalAdd offset 4))))))
452 (branch
453 AArch64AssemblyCompareBranchIfNotZero
454 register
455 target
456 tail
457 encodeTail
458 .
459 (lambda unrestricted labels : (family AArch64LabelTable) .
460 (lambda unrestricted offset : Nat .
461 (aarch64EncodeToLabel
462 target
463 labels
464 offset
465 (lambda unrestricted direction : (family AArch64Direction) .
466 (lambda unrestricted distance : Nat .
467 (constructor
468 AArch64Instruction
469 AArch64CompareBranchIfNotZero
470 register
471 direction
472 distance)))
473 (encodeTail labels (naturalAdd offset 4))))))
474 (branch
475 AArch64AssemblyAddressOf
476 destination
477 target
478 tail
479 encodeTail
480 .
481 (lambda unrestricted labels : (family AArch64LabelTable) .
482 (lambda unrestricted offset : Nat .
483 (aarch64EncodeToLabel
484 target
485 labels
486 offset
487 (lambda unrestricted direction : (family AArch64Direction) .
488 (lambda unrestricted distance : Nat .
489 (constructor
490 AArch64Instruction
491 AArch64AddressRelative
492 destination
493 direction
494 distance)))
495 (encodeTail labels (naturalAdd offset 4))))))))
496
497def aarch64Assemble :
498 (pi unrestricted assembly : (family AArch64Assembly) . (family AArch64AssemblyResult)) =
499 (lambda unrestricted assembly : (family AArch64Assembly) .
500 (eliminate
501 AArch64AssemblyLayoutResult
502 (lambda unrestricted layout : (family AArch64AssemblyLayoutResult) .
503 (family AArch64AssemblyResult))
504 (aarch64LayoutAssembly assembly)
505 (branch
506 AArch64AssemblyLayoutSuccess
507 labels
508 size
509 .
510 (aarch64EncodeAssemblyFrom assembly labels 0))
511 (branch
512 AArch64AssemblyDuplicateLabel
513 duplicate
514 .
515 (constructor AArch64AssemblyResult AArch64AssemblyEncodeDuplicateLabel duplicate))))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.