1module Compiler.MachineAArch64
2
3import Data.Bytes
4import Model.Config
5import Model.Word32
6import Std.Byte
7import Std.Natural
8
9-- The Alpha-side mirror of bootstrap/haskell/.../Alpha/Target/AArch64.hs: the
10-- same A64 subset, encoded to the same bytes. Every instruction is one
11-- little-endian 32-bit word; fields never overlap, so a word is the sum of
12-- its opcode base and its shifted fields, and the sum is serialised through
13-- the checked Model.Word32 owner. Registers are X0-X30 by construction:
14-- there is no constructor for code 31, so SP/XZR cannot be named. Every
15-- range-limited operand is checked and a violation is a result, never a
16-- truncated field.
17family AArch64Register : Type 0
18constructor AArch64X0
19constructor AArch64X1
20constructor AArch64X2
21constructor AArch64X3
22constructor AArch64X4
23constructor AArch64X5
24constructor AArch64X6
25constructor AArch64X7
26constructor AArch64X8
27constructor AArch64X9
28constructor AArch64X10
29constructor AArch64X11
30constructor AArch64X12
31constructor AArch64X13
32constructor AArch64X14
33constructor AArch64X15
34constructor AArch64X16
35constructor AArch64X17
36constructor AArch64X18
37constructor AArch64X19
38constructor AArch64X20
39constructor AArch64X21
40constructor AArch64X22
41constructor AArch64X23
42constructor AArch64X24
43constructor AArch64X25
44constructor AArch64X26
45constructor AArch64X27
46constructor AArch64X28
47constructor AArch64X29
48constructor AArch64X30
49
50end-family
51
52-- The halfword a wide move writes: lsl #0, #16, #32 or #48.
53family AArch64HalfwordShift : Type 0
54constructor AArch64Shift0
55constructor AArch64Shift16
56constructor AArch64Shift32
57constructor AArch64Shift48
58
59end-family
60
61-- Condition codes in encoding order; AL and NV are deliberately absent.
62family AArch64Condition : Type 0
63constructor AArch64Equal
64constructor AArch64NotEqual
65constructor AArch64CarrySet
66constructor AArch64CarryClear
67constructor AArch64Minus
68constructor AArch64Plus
69constructor AArch64OverflowSet
70constructor AArch64OverflowClear
71constructor AArch64UnsignedHigher
72constructor AArch64UnsignedLowerOrSame
73constructor AArch64GreaterOrEqual
74constructor AArch64LessThan
75constructor AArch64GreaterThan
76constructor AArch64LessOrEqual
77
78end-family
79
80-- A PC-relative distance is a direction and a magnitude in bytes, measured
81-- from the referencing instruction itself.
82family AArch64Direction : Type 0
83constructor AArch64Forward
84constructor AArch64Backward
85
86end-family
87
88-- An add/sub immediate is taken as is or shifted left by 12.
89family AArch64ImmediateShift : Type 0
90constructor AArch64Unshifted
91constructor AArch64ShiftedBy12
92
93end-family
94
95
96
97-- The scalar single-precision register file (Arm A-profile, FP data-processing
98-- and FMOV between the general and vector files). Unlike the general
99-- registers, code 31 names a real register here rather than the stack pointer
100-- or the zero register, so this family carries all thirty-two.
101family AArch64FloatRegister : Type 0
102constructor AArch64S0
103constructor AArch64S1
104constructor AArch64S2
105constructor AArch64S3
106constructor AArch64S4
107constructor AArch64S5
108constructor AArch64S6
109constructor AArch64S7
110constructor AArch64S8
111constructor AArch64S9
112constructor AArch64S10
113constructor AArch64S11
114constructor AArch64S12
115constructor AArch64S13
116constructor AArch64S14
117constructor AArch64S15
118constructor AArch64S16
119constructor AArch64S17
120constructor AArch64S18
121constructor AArch64S19
122constructor AArch64S20
123constructor AArch64S21
124constructor AArch64S22
125constructor AArch64S23
126constructor AArch64S24
127constructor AArch64S25
128constructor AArch64S26
129constructor AArch64S27
130constructor AArch64S28
131constructor AArch64S29
132constructor AArch64S30
133constructor AArch64S31
134end-family
135
136family AArch64Instruction : Type 0
137constructor AArch64MoveWideZero
138field unrestricted aarch64MoveWideZeroDestination : (family AArch64Register)
139field unrestricted aarch64MoveWideZeroValue : Nat
140field unrestricted aarch64MoveWideZeroShift : (family AArch64HalfwordShift)
141constructor AArch64MoveWideKeep
142field unrestricted aarch64MoveWideKeepDestination : (family AArch64Register)
143field unrestricted aarch64MoveWideKeepValue : Nat
144field unrestricted aarch64MoveWideKeepShift : (family AArch64HalfwordShift)
145constructor AArch64MoveRegister
146field unrestricted aarch64MoveRegisterDestination : (family AArch64Register)
147field unrestricted aarch64MoveRegisterSource : (family AArch64Register)
148constructor AArch64AddImmediate
149field unrestricted aarch64AddImmediateDestination : (family AArch64Register)
150field unrestricted aarch64AddImmediateSource : (family AArch64Register)
151field unrestricted aarch64AddImmediateValue : Nat
152constructor AArch64SubtractImmediate
153field unrestricted aarch64SubtractImmediateDestination : (family AArch64Register)
154field unrestricted aarch64SubtractImmediateSource : (family AArch64Register)
155field unrestricted aarch64SubtractImmediateValue : Nat
156constructor AArch64AddRegister
157field unrestricted aarch64AddRegisterDestination : (family AArch64Register)
158field unrestricted aarch64AddRegisterLeft : (family AArch64Register)
159field unrestricted aarch64AddRegisterRight : (family AArch64Register)
160constructor AArch64SubtractRegister
161field unrestricted aarch64SubtractRegisterDestination : (family AArch64Register)
162field unrestricted aarch64SubtractRegisterLeft : (family AArch64Register)
163field unrestricted aarch64SubtractRegisterRight : (family AArch64Register)
164constructor AArch64AndRegister
165field unrestricted aarch64AndRegisterDestination : (family AArch64Register)
166field unrestricted aarch64AndRegisterLeft : (family AArch64Register)
167field unrestricted aarch64AndRegisterRight : (family AArch64Register)
168constructor AArch64OrRegister
169field unrestricted aarch64OrRegisterDestination : (family AArch64Register)
170field unrestricted aarch64OrRegisterLeft : (family AArch64Register)
171field unrestricted aarch64OrRegisterRight : (family AArch64Register)
172constructor AArch64ExclusiveOrRegister
173field unrestricted aarch64ExclusiveOrRegisterDestination : (family AArch64Register)
174field unrestricted aarch64ExclusiveOrRegisterLeft : (family AArch64Register)
175field unrestricted aarch64ExclusiveOrRegisterRight : (family AArch64Register)
176constructor AArch64ShiftLeftImmediate
177field unrestricted aarch64ShiftLeftImmediateDestination : (family AArch64Register)
178field unrestricted aarch64ShiftLeftImmediateSource : (family AArch64Register)
179field unrestricted aarch64ShiftLeftImmediateAmount : Nat
180constructor AArch64ShiftRightImmediate
181field unrestricted aarch64ShiftRightImmediateDestination : (family AArch64Register)
182field unrestricted aarch64ShiftRightImmediateSource : (family AArch64Register)
183field unrestricted aarch64ShiftRightImmediateAmount : Nat
184constructor AArch64MultiplyRegister
185field unrestricted aarch64MultiplyRegisterDestination : (family AArch64Register)
186field unrestricted aarch64MultiplyRegisterLeft : (family AArch64Register)
187field unrestricted aarch64MultiplyRegisterRight : (family AArch64Register)
188constructor AArch64DivideRegisterUnsigned
189field unrestricted aarch64DivideRegisterUnsignedDestination : (family AArch64Register)
190field unrestricted aarch64DivideRegisterUnsignedLeft : (family AArch64Register)
191field unrestricted aarch64DivideRegisterUnsignedRight : (family AArch64Register)
192constructor AArch64CompareImmediate
193field unrestricted aarch64CompareImmediateRegister : (family AArch64Register)
194field unrestricted aarch64CompareImmediateValue : Nat
195constructor AArch64CompareRegister
196field unrestricted aarch64CompareRegisterLeft : (family AArch64Register)
197field unrestricted aarch64CompareRegisterRight : (family AArch64Register)
198constructor AArch64LoadMemory64
199field unrestricted aarch64LoadMemory64Destination : (family AArch64Register)
200field unrestricted aarch64LoadMemory64Base : (family AArch64Register)
201field unrestricted aarch64LoadMemory64Offset : Nat
202constructor AArch64StoreMemory64
203field unrestricted aarch64StoreMemory64Base : (family AArch64Register)
204field unrestricted aarch64StoreMemory64Offset : Nat
205field unrestricted aarch64StoreMemory64Source : (family AArch64Register)
206constructor AArch64LoadMemory32ZeroExtend
207field unrestricted aarch64LoadMemory32Destination : (family AArch64Register)
208field unrestricted aarch64LoadMemory32Base : (family AArch64Register)
209field unrestricted aarch64LoadMemory32Offset : Nat
210constructor AArch64StoreMemory32
211field unrestricted aarch64StoreMemory32Base : (family AArch64Register)
212field unrestricted aarch64StoreMemory32Offset : Nat
213field unrestricted aarch64StoreMemory32Source : (family AArch64Register)
214constructor AArch64LoadMemory8ZeroExtend
215field unrestricted aarch64LoadMemory8Destination : (family AArch64Register)
216field unrestricted aarch64LoadMemory8Base : (family AArch64Register)
217field unrestricted aarch64LoadMemory8Offset : Nat
218constructor AArch64StoreMemory8
219field unrestricted aarch64StoreMemory8Base : (family AArch64Register)
220field unrestricted aarch64StoreMemory8Offset : Nat
221field unrestricted aarch64StoreMemory8Source : (family AArch64Register)
222constructor AArch64AddressRelative
223field unrestricted aarch64AddressRelativeDestination : (family AArch64Register)
224field unrestricted aarch64AddressRelativeDirection : (family AArch64Direction)
225field unrestricted aarch64AddressRelativeDistance : Nat
226constructor AArch64Branch
227field unrestricted aarch64BranchDirection : (family AArch64Direction)
228field unrestricted aarch64BranchDistance : Nat
229constructor AArch64BranchLink
230field unrestricted aarch64BranchLinkDirection : (family AArch64Direction)
231field unrestricted aarch64BranchLinkDistance : Nat
232constructor AArch64BranchLinkRegister
233field unrestricted aarch64BranchLinkRegisterTarget : (family AArch64Register)
234constructor AArch64BranchIf
235field unrestricted aarch64BranchIfCondition : (family AArch64Condition)
236field unrestricted aarch64BranchIfDirection : (family AArch64Direction)
237field unrestricted aarch64BranchIfDistance : Nat
238constructor AArch64CompareBranchIfZero
239field unrestricted aarch64CompareBranchIfZeroRegister : (family AArch64Register)
240field unrestricted aarch64CompareBranchIfZeroDirection : (family AArch64Direction)
241field unrestricted aarch64CompareBranchIfZeroDistance : Nat
242constructor AArch64CompareBranchIfNotZero
243field unrestricted aarch64CompareBranchIfNotZeroRegister : (family AArch64Register)
244field unrestricted aarch64CompareBranchIfNotZeroDirection : (family AArch64Direction)
245field unrestricted aarch64CompareBranchIfNotZeroDistance : Nat
246constructor AArch64AddImmediateFromStackPointer
247field unrestricted aarch64AddFromStackDestination : (family AArch64Register)
248field unrestricted aarch64AddFromStackValue : Nat
249constructor AArch64AddStackPointer
250field unrestricted aarch64AddStackPointerValue : Nat
251field unrestricted aarch64AddStackPointerShift : (family AArch64ImmediateShift)
252constructor AArch64SubtractStackPointer
253field unrestricted aarch64SubtractStackPointerValue : Nat
254field unrestricted aarch64SubtractStackPointerShift : (family AArch64ImmediateShift)
255constructor AArch64LoadMemory64FromStack
256field unrestricted aarch64LoadFromStackDestination : (family AArch64Register)
257field unrestricted aarch64LoadFromStackOffset : Nat
258constructor AArch64StoreMemory64ToStack
259field unrestricted aarch64StoreToStackOffset : Nat
260field unrestricted aarch64StoreToStackSource : (family AArch64Register)
261constructor AArch64LoadMemory8FromStack
262field unrestricted aarch64LoadByteFromStackDestination : (family AArch64Register)
263field unrestricted aarch64LoadByteFromStackOffset : Nat
264constructor AArch64StoreMemory8ToStack
265field unrestricted aarch64StoreByteToStackOffset : Nat
266field unrestricted aarch64StoreByteToStackSource : (family AArch64Register)
267constructor AArch64Return
268constructor AArch64SupervisorCall
269-- Full-system completion before a following device/MMIO store. This is
270-- stronger than a compiler fence and is required by the native submit path.
271constructor AArch64DataSynchronizationBarrierSystem
272
273constructor AArch64FloatAdd32
274field unrestricted aarch64FloatAdd32Destination : (family AArch64FloatRegister)
275field unrestricted aarch64FloatAdd32Left : (family AArch64FloatRegister)
276field unrestricted aarch64FloatAdd32Right : (family AArch64FloatRegister)
277constructor AArch64FloatSubtract32
278field unrestricted aarch64FloatSubtract32Destination : (family AArch64FloatRegister)
279field unrestricted aarch64FloatSubtract32Left : (family AArch64FloatRegister)
280field unrestricted aarch64FloatSubtract32Right : (family AArch64FloatRegister)
281constructor AArch64FloatMultiply32
282field unrestricted aarch64FloatMultiply32Destination : (family AArch64FloatRegister)
283field unrestricted aarch64FloatMultiply32Left : (family AArch64FloatRegister)
284field unrestricted aarch64FloatMultiply32Right : (family AArch64FloatRegister)
285constructor AArch64FloatDivide32
286field unrestricted aarch64FloatDivide32Destination : (family AArch64FloatRegister)
287field unrestricted aarch64FloatDivide32Left : (family AArch64FloatRegister)
288field unrestricted aarch64FloatDivide32Right : (family AArch64FloatRegister)
289constructor AArch64FloatCompare32
290field unrestricted aarch64FloatCompare32Left : (family AArch64FloatRegister)
291field unrestricted aarch64FloatCompare32Right : (family AArch64FloatRegister)
292constructor AArch64FloatMoveFromGeneral32
293field unrestricted aarch64FloatMoveFromGeneral32Destination : (family AArch64FloatRegister)
294field unrestricted aarch64FloatMoveFromGeneral32Source : (family AArch64Register)
295constructor AArch64FloatMoveToGeneral32
296field unrestricted aarch64FloatMoveToGeneral32Destination : (family AArch64Register)
297field unrestricted aarch64FloatMoveToGeneral32Source : (family AArch64FloatRegister)
298constructor AArch64ReadFloatControl
299field unrestricted aarch64ReadFloatControlDestination : (family AArch64Register)
300constructor AArch64WriteFloatControl
301field unrestricted aarch64WriteFloatControlSource : (family AArch64Register)
302-- Scalar double precision: the same register file read as D registers (a D
303-- register and the S register of the same number share their low 32 bits).
304constructor AArch64FloatAdd64
305field unrestricted aarch64FloatAdd64Destination : (family AArch64FloatRegister)
306field unrestricted aarch64FloatAdd64Left : (family AArch64FloatRegister)
307field unrestricted aarch64FloatAdd64Right : (family AArch64FloatRegister)
308constructor AArch64FloatSubtract64
309field unrestricted aarch64FloatSubtract64Destination : (family AArch64FloatRegister)
310field unrestricted aarch64FloatSubtract64Left : (family AArch64FloatRegister)
311field unrestricted aarch64FloatSubtract64Right : (family AArch64FloatRegister)
312constructor AArch64FloatMultiply64
313field unrestricted aarch64FloatMultiply64Destination : (family AArch64FloatRegister)
314field unrestricted aarch64FloatMultiply64Left : (family AArch64FloatRegister)
315field unrestricted aarch64FloatMultiply64Right : (family AArch64FloatRegister)
316constructor AArch64FloatDivide64
317field unrestricted aarch64FloatDivide64Destination : (family AArch64FloatRegister)
318field unrestricted aarch64FloatDivide64Left : (family AArch64FloatRegister)
319field unrestricted aarch64FloatDivide64Right : (family AArch64FloatRegister)
320constructor AArch64FloatSquareRoot64
321field unrestricted aarch64FloatSquareRoot64Destination : (family AArch64FloatRegister)
322field unrestricted aarch64FloatSquareRoot64Source : (family AArch64FloatRegister)
323-- scvtf Dd, Xn: the signed 64-bit integer as the nearest double
324constructor AArch64FloatFromSigned64
325field unrestricted aarch64FloatFromSigned64Destination : (family AArch64FloatRegister)
326field unrestricted aarch64FloatFromSigned64Source : (family AArch64Register)
327-- fcvt Sd, Dn and fcvt Dd, Sn
328constructor AArch64FloatNarrow64To32
329field unrestricted aarch64FloatNarrow64To32Destination : (family AArch64FloatRegister)
330field unrestricted aarch64FloatNarrow64To32Source : (family AArch64FloatRegister)
331constructor AArch64FloatWiden32To64
332field unrestricted aarch64FloatWiden32To64Destination : (family AArch64FloatRegister)
333field unrestricted aarch64FloatWiden32To64Source : (family AArch64FloatRegister)
334-- fmov Dd, Xn and fmov Xd, Dn: the 64 bits unchanged
335constructor AArch64FloatMoveFromGeneral64
336field unrestricted aarch64FloatMoveFromGeneral64Destination : (family AArch64FloatRegister)
337field unrestricted aarch64FloatMoveFromGeneral64Source : (family AArch64Register)
338constructor AArch64FloatMoveToGeneral64
339field unrestricted aarch64FloatMoveToGeneral64Destination : (family AArch64Register)
340field unrestricted aarch64FloatMoveToGeneral64Source : (family AArch64FloatRegister)
341-- dsb sy: every memory access before completes before any after -- how a
342-- store to Normal memory is ordered before one to a Device mapping
343constructor AArch64DataSynchronizationBarrier
344end-family
345
346family AArch64Program : Type 0
347constructor AArch64ProgramEnd
348constructor AArch64ProgramNext
349field unrestricted aarch64ProgramInstruction : (family AArch64Instruction)
350recursive unrestricted aarch64ProgramTail
351
352end-family
353
354-- Encoding either yields the exact bytes or names the operand it refused.
355family AArch64EncodeResult : Type 0
356constructor AArch64Encoded
357field unrestricted aarch64EncodedBytes : Bytes
358constructor AArch64ImmediateOutOfRange
359field unrestricted aarch64ImmediateOutOfRangeValue : Nat
360constructor AArch64MisalignedOffset
361field unrestricted aarch64MisalignedOffsetValue : Nat
362constructor AArch64DisplacementOutOfRange
363field unrestricted aarch64DisplacementOutOfRangeValue : Nat
364
365end-family
366
367def aarch64RegisterCode : (pi unrestricted register : (family AArch64Register) . Nat) =
368 (lambda unrestricted register : (family AArch64Register) .
369 (eliminate
370 AArch64Register
371 (lambda unrestricted current : (family AArch64Register) . Nat)
372 register
373 (branch AArch64X0 . 0)
374 (branch AArch64X1 . 1)
375 (branch AArch64X2 . 2)
376 (branch AArch64X3 . 3)
377 (branch AArch64X4 . 4)
378 (branch AArch64X5 . 5)
379 (branch AArch64X6 . 6)
380 (branch AArch64X7 . 7)
381 (branch AArch64X8 . 8)
382 (branch AArch64X9 . 9)
383 (branch AArch64X10 . 10)
384 (branch AArch64X11 . 11)
385 (branch AArch64X12 . 12)
386 (branch AArch64X13 . 13)
387 (branch AArch64X14 . 14)
388 (branch AArch64X15 . 15)
389 (branch AArch64X16 . 16)
390 (branch AArch64X17 . 17)
391 (branch AArch64X18 . 18)
392 (branch AArch64X19 . 19)
393 (branch AArch64X20 . 20)
394 (branch AArch64X21 . 21)
395 (branch AArch64X22 . 22)
396 (branch AArch64X23 . 23)
397 (branch AArch64X24 . 24)
398 (branch AArch64X25 . 25)
399 (branch AArch64X26 . 26)
400 (branch AArch64X27 . 27)
401 (branch AArch64X28 . 28)
402 (branch AArch64X29 . 29)
403 (branch AArch64X30 . 30)))
404
405
406def aarch64FloatRegisterCode :
407 (pi unrestricted register : (family AArch64FloatRegister) . Nat) =
408 (lambda unrestricted register : (family AArch64FloatRegister) .
409 (eliminate
410 AArch64FloatRegister
411 (lambda unrestricted current : (family AArch64FloatRegister) . Nat)
412 register
413 (branch AArch64S0 . 0)
414 (branch AArch64S1 . 1)
415 (branch AArch64S2 . 2)
416 (branch AArch64S3 . 3)
417 (branch AArch64S4 . 4)
418 (branch AArch64S5 . 5)
419 (branch AArch64S6 . 6)
420 (branch AArch64S7 . 7)
421 (branch AArch64S8 . 8)
422 (branch AArch64S9 . 9)
423 (branch AArch64S10 . 10)
424 (branch AArch64S11 . 11)
425 (branch AArch64S12 . 12)
426 (branch AArch64S13 . 13)
427 (branch AArch64S14 . 14)
428 (branch AArch64S15 . 15)
429 (branch AArch64S16 . 16)
430 (branch AArch64S17 . 17)
431 (branch AArch64S18 . 18)
432 (branch AArch64S19 . 19)
433 (branch AArch64S20 . 20)
434 (branch AArch64S21 . 21)
435 (branch AArch64S22 . 22)
436 (branch AArch64S23 . 23)
437 (branch AArch64S24 . 24)
438 (branch AArch64S25 . 25)
439 (branch AArch64S26 . 26)
440 (branch AArch64S27 . 27)
441 (branch AArch64S28 . 28)
442 (branch AArch64S29 . 29)
443 (branch AArch64S30 . 30)
444 (branch AArch64S31 . 31)
445 ))
446
447def aarch64HalfwordShiftCode : (pi unrestricted shift : (family AArch64HalfwordShift) . Nat) =
448 (lambda unrestricted shift : (family AArch64HalfwordShift) .
449 (eliminate
450 AArch64HalfwordShift
451 (lambda unrestricted current : (family AArch64HalfwordShift) . Nat)
452 shift
453 (branch AArch64Shift0 . 0)
454 (branch AArch64Shift16 . 1)
455 (branch AArch64Shift32 . 2)
456 (branch AArch64Shift48 . 3)))
457
458def aarch64ConditionCode : (pi unrestricted condition : (family AArch64Condition) . Nat) =
459 (lambda unrestricted condition : (family AArch64Condition) .
460 (eliminate
461 AArch64Condition
462 (lambda unrestricted current : (family AArch64Condition) . Nat)
463 condition
464 (branch AArch64Equal . 0)
465 (branch AArch64NotEqual . 1)
466 (branch AArch64CarrySet . 2)
467 (branch AArch64CarryClear . 3)
468 (branch AArch64Minus . 4)
469 (branch AArch64Plus . 5)
470 (branch AArch64OverflowSet . 6)
471 (branch AArch64OverflowClear . 7)
472 (branch AArch64UnsignedHigher . 8)
473 (branch AArch64UnsignedLowerOrSame . 9)
474 (branch AArch64GreaterOrEqual . 10)
475 (branch AArch64LessThan . 11)
476 (branch AArch64GreaterThan . 12)
477 (branch AArch64LessOrEqual . 13)))
478
479-- Field multipliers (the bit position of each field) and two's-complement moduli.
480def aarch64ImmediateShiftCode : (pi unrestricted shift : (family AArch64ImmediateShift) . Nat) =
481 (lambda unrestricted shift : (family AArch64ImmediateShift) .
482 (eliminate
483 AArch64ImmediateShift
484 (lambda unrestricted current : (family AArch64ImmediateShift) . Nat)
485 shift
486 (branch AArch64Unshifted . 0)
487 (branch AArch64ShiftedBy12 . 1)))
488
489-- Encoding is BYTE-ORIENTED, like Compiler.MachineX86Native, and for the same
490-- reason: in the runtime machine a Nat literal costs steps linear in its
491-- value, so an opcode base near 3.6 billion is unrunnable even though the
492-- checker normalises it instantly. Every word is built as its four
493-- little-endian bytes from the base's bytes plus each field's contribution,
494-- and every intermediate stays below 256 except the operands themselves,
495-- which the smart constructors already bound. Powers of two are computed by
496-- doubling rather than written as literals for the same reason.
497def aarch64Two : Nat =
498 2
499
500def aarch64Four : Nat =
501 4
502
503def aarch64Eight : Nat =
504 8
505
506def aarch64ThirtyTwo : Nat =
507 32
508
509def aarch64SixtyFour : Nat =
510 64
511
512def aarch64TwoHundredFiftySix : Nat =
513 (naturalPowerOfTwo 8)
514
515def aarch64TwoThousandFortyEight : Nat =
516 (naturalPowerOfTwo 11)
517
518-- Field limits. Anything at or above 256 is computed by doubling rather
519-- than written as a literal, because a literal costs steps equal to its value.
520def aarch64Immediate12Limit : Nat =
521 (naturalPowerOfTwo 12)
522
523def aarch64Immediate16Limit : Nat =
524 (naturalPowerOfTwo 16)
525
526def aarch64ShiftLimit : Nat =
527 64
528
529-- The largest scaled 32-bit offset is 4095 * 4; the limit is one past it.
530-- Reusing the 64-bit limit here would let an offset up to 32767 through and
531-- overflow imm12, encoding a different instruction instead of refusing.
532def aarch64Scaled32OffsetLimit : Nat =
533 (naturalAdd
534 (naturalMultiply (naturalSaturatingSubtract aarch64Immediate12Limit 1) aarch64Four)
535 1)
536
537-- The largest scaled 64-bit offset is 4095 * 8; the limit is one past it.
538def aarch64ScaledOffsetLimit : Nat =
539 (naturalAdd
540 (naturalMultiply (naturalSaturatingSubtract aarch64Immediate12Limit 1) aarch64Eight)
541 1)
542
543def aarch64Modulus19 : Nat =
544 (naturalPowerOfTwo 19)
545
546def aarch64Modulus21 : Nat =
547 (naturalPowerOfTwo 21)
548
549def aarch64Modulus26 : Nat =
550 (naturalPowerOfTwo 26)
551
552-- A word from its four little-endian bytes. Every argument is reduced mod
553-- 256 by nat-to-byte, so a field that overflows its byte cannot silently
554-- corrupt the next one: the smart constructors bound every operand first.
555def aarch64ByteWord =
556 (lambda unrestricted byte0 : Nat .
557 (lambda unrestricted byte1 : Nat .
558 (lambda unrestricted byte2 : Nat .
559 (lambda unrestricted byte3 : Nat .
560 (constructor
561 AArch64EncodeResult
562 AArch64Encoded
563 (bytes-cons
564 (nat-to-byte byte0)
565 (bytes-cons
566 (nat-to-byte byte1)
567 (bytes-cons (nat-to-byte byte2) (bytes-cons (nat-to-byte byte3) b"")))))))))
568
569-- Accept the word only when value < limit.
570def aarch64EncodeBounded =
571 (lambda unrestricted value : Nat .
572 (lambda unrestricted limit : Nat .
573 (lambda unrestricted word : (family AArch64EncodeResult) .
574 (nat-eliminate
575 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
576 (constructor AArch64EncodeResult AArch64ImmediateOutOfRange value)
577 (lambda unrestricted predecessor : Nat .
578 (lambda unrestricted induction : (family AArch64EncodeResult) . word))
579 (naturalLess value limit)))))
580
581-- Field contributions, by the byte they land in.
582-- Rd occupies bits 0-4, so it adds to byte 0.
583-- Rn occupies bits 5-9: its low three bits scale into byte 0, the rest into byte 1.
584def aarch64LowFive =
585 (lambda unrestricted register : (family AArch64Register) . (aarch64RegisterCode register))
586
587def aarch64RnByte0 =
588 (lambda unrestricted register : (family AArch64Register) .
589 (naturalMultiply
590 (naturalModuloUnchecked (aarch64RegisterCode register) aarch64Eight)
591 aarch64ThirtyTwo))
592
593def aarch64RnByte1 =
594 (lambda unrestricted register : (family AArch64Register) .
595 (naturalDivideUnchecked (aarch64RegisterCode register) aarch64Eight))
596
597-- The stack pointer is register code 31 in the encodings that admit it.
598def aarch64StackPointerByte0 : Nat =
599 224
600
601def aarch64StackPointerByte1 : Nat =
602 3
603
604def aarch64ZeroRegisterByte0 : Nat =
605 31
606
607-- An imm12 occupies bits 10-21: byte 1 takes six bits scaled by four, byte 2 the rest.
608def aarch64Immediate12Byte1 =
609 (lambda unrestricted value : Nat .
610 (naturalMultiply (naturalModuloUnchecked value aarch64SixtyFour) aarch64Four))
611
612def aarch64Immediate12Byte2 =
613 (lambda unrestricted value : Nat . (naturalDivideUnchecked value aarch64SixtyFour))
614
615-- An imm16 occupies bits 5-20, an imm19 bits 5-23: both start at bit 5.
616def aarch64FromBitFiveByte0 =
617 (lambda unrestricted value : Nat .
618 (naturalMultiply (naturalModuloUnchecked value aarch64Eight) aarch64ThirtyTwo))
619
620def aarch64FromBitFiveByte1 =
621 (lambda unrestricted value : Nat .
622 (naturalModuloUnchecked (naturalDivideUnchecked value aarch64Eight) aarch64TwoHundredFiftySix))
623
624def aarch64FromBitFiveByte2 =
625 (lambda unrestricted value : Nat .
626 (naturalModuloUnchecked
627 (naturalDivideUnchecked value aarch64TwoThousandFortyEight)
628 aarch64TwoHundredFiftySix))
629
630-- A three-register data-processing word.
631def aarch64ThreeRegisterWord =
632 (lambda unrestricted base1 : Nat .
633 (lambda unrestricted base2 : Nat .
634 (lambda unrestricted base3 : Nat .
635 (lambda unrestricted destination : (family AArch64Register) .
636 (lambda unrestricted left : (family AArch64Register) .
637 (lambda unrestricted right : (family AArch64Register) .
638 (aarch64ByteWord
639 (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 left))
640 (naturalAdd base1 (aarch64RnByte1 left))
641 (naturalAdd base2 (aarch64RegisterCode right))
642 base3)))))))
643
644-- A wide move: imm16 at bit 5, the halfword selector at bits 21-22.
645def aarch64WideWord =
646 (lambda unrestricted base3 : Nat .
647 (lambda unrestricted destination : (family AArch64Register) .
648 (lambda unrestricted value : Nat .
649 (lambda unrestricted shift : (family AArch64HalfwordShift) .
650 (aarch64EncodeBounded
651 value
652 aarch64Immediate16Limit
653 (aarch64ByteWord
654 (naturalAdd (aarch64LowFive destination) (aarch64FromBitFiveByte0 value))
655 (aarch64FromBitFiveByte1 value)
656 (naturalAdd
657 (naturalAdd 128 (aarch64FromBitFiveByte2 value))
658 (naturalMultiply (aarch64HalfwordShiftCode shift) aarch64ThirtyTwo))
659 base3))))))
660
661-- An add/subtract immediate over general registers.
662def aarch64ImmediateWord =
663 (lambda unrestricted base3 : Nat .
664 (lambda unrestricted destination : Nat .
665 (lambda unrestricted source : (family AArch64Register) .
666 (lambda unrestricted value : Nat .
667 (aarch64EncodeBounded
668 value
669 aarch64Immediate12Limit
670 (aarch64ByteWord
671 (naturalAdd destination (aarch64RnByte0 source))
672 (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 value))
673 (aarch64Immediate12Byte2 value)
674 base3))))))
675
676-- A scaled 64-bit load or store: the offset must be a multiple of eight.
677def aarch64ScaledMemoryWord =
678 (lambda unrestricted base2 : Nat .
679 (lambda unrestricted base3 : Nat .
680 (lambda unrestricted register : (family AArch64Register) .
681 (lambda unrestricted address : (family AArch64Register) .
682 (lambda unrestricted offset : Nat .
683 (nat-eliminate
684 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
685 (constructor AArch64EncodeResult AArch64MisalignedOffset offset)
686 (lambda unrestricted predecessor : Nat .
687 (lambda unrestricted induction : (family AArch64EncodeResult) .
688 (aarch64EncodeBounded
689 offset
690 aarch64ScaledOffsetLimit
691 (aarch64ByteWord
692 (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address))
693 (naturalAdd
694 (aarch64RnByte1 address)
695 (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Eight)))
696 (naturalAdd
697 base2
698 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Eight)))
699 base3))))
700 (naturalIsZero (naturalModuloUnchecked offset aarch64Eight))))))))
701
702-- A 32-bit load or store: like the 64-bit form, but the imm12 offset is
703-- scaled by 4 rather than 8, and the offset must be a multiple of 4. RM
704-- handles are NvU32, so placing one into a parameter struct needs this width:
705-- a 64-bit store would carry the neighbouring field along with it.
706def aarch64ScaledMemoryWord32 =
707 (lambda unrestricted base2 : Nat .
708 (lambda unrestricted base3 : Nat .
709 (lambda unrestricted register : (family AArch64Register) .
710 (lambda unrestricted address : (family AArch64Register) .
711 (lambda unrestricted offset : Nat .
712 (nat-eliminate
713 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
714 (constructor AArch64EncodeResult AArch64MisalignedOffset offset)
715 (lambda unrestricted predecessor : Nat .
716 (lambda unrestricted induction : (family AArch64EncodeResult) .
717 (aarch64EncodeBounded
718 offset
719 aarch64Scaled32OffsetLimit
720 (aarch64ByteWord
721 (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address))
722 (naturalAdd
723 (aarch64RnByte1 address)
724 (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Four)))
725 (naturalAdd
726 base2
727 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Four)))
728 base3))))
729 (naturalIsZero (naturalModuloUnchecked offset aarch64Four))))))))
730
731-- A byte load or store: an unscaled imm12 offset.
732def aarch64ByteMemoryWord =
733 (lambda unrestricted base2 : Nat .
734 (lambda unrestricted base3 : Nat .
735 (lambda unrestricted register : (family AArch64Register) .
736 (lambda unrestricted address : (family AArch64Register) .
737 (lambda unrestricted offset : Nat .
738 (aarch64EncodeBounded
739 offset
740 aarch64Immediate12Limit
741 (aarch64ByteWord
742 (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address))
743 (naturalAdd (aarch64RnByte1 address) (aarch64Immediate12Byte1 offset))
744 (naturalAdd base2 (aarch64Immediate12Byte2 offset))
745 base3)))))))
746
747-- The stack-pointer forms, where register code 31 means sp.
748def aarch64StackAdjustWord =
749 (lambda unrestricted base3 : Nat .
750 (lambda unrestricted value : Nat .
751 (lambda unrestricted shift : (family AArch64ImmediateShift) .
752 (aarch64EncodeBounded
753 value
754 aarch64Immediate12Limit
755 (aarch64ByteWord
756 (naturalAdd aarch64StackPointerByte0 aarch64ZeroRegisterByte0)
757 (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 value))
758 (naturalAdd
759 (aarch64Immediate12Byte2 value)
760 (naturalMultiply (aarch64ImmediateShiftCode shift) aarch64SixtyFour))
761 base3)))))
762
763def aarch64StackScaledWord =
764 (lambda unrestricted base2 : Nat .
765 (lambda unrestricted base3 : Nat .
766 (lambda unrestricted register : (family AArch64Register) .
767 (lambda unrestricted offset : Nat .
768 (nat-eliminate
769 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
770 (constructor AArch64EncodeResult AArch64MisalignedOffset offset)
771 (lambda unrestricted predecessor : Nat .
772 (lambda unrestricted induction : (family AArch64EncodeResult) .
773 (aarch64EncodeBounded
774 offset
775 aarch64ScaledOffsetLimit
776 (aarch64ByteWord
777 (naturalAdd (aarch64LowFive register) aarch64StackPointerByte0)
778 (naturalAdd
779 aarch64StackPointerByte1
780 (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Eight)))
781 (naturalAdd
782 base2
783 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Eight)))
784 base3))))
785 (naturalIsZero (naturalModuloUnchecked offset aarch64Eight)))))))
786
787def aarch64StackByteWord =
788 (lambda unrestricted base2 : Nat .
789 (lambda unrestricted base3 : Nat .
790 (lambda unrestricted register : (family AArch64Register) .
791 (lambda unrestricted offset : Nat .
792 (aarch64EncodeBounded
793 offset
794 aarch64Immediate12Limit
795 (aarch64ByteWord
796 (naturalAdd (aarch64LowFive register) aarch64StackPointerByte0)
797 (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 offset))
798 (naturalAdd base2 (aarch64Immediate12Byte2 offset))
799 base3))))))
800
801-- Two's-complement field for a signed distance whose magnitude is in `units`.
802def aarch64SignedField =
803 (lambda unrestricted direction : (family AArch64Direction) .
804 (lambda unrestricted units : Nat .
805 (lambda unrestricted modulus : Nat .
806 (eliminate
807 AArch64Direction
808 (lambda unrestricted current : (family AArch64Direction) . Nat)
809 direction
810 (branch AArch64Forward . units)
811 (branch
812 AArch64Backward
813 .
814 (naturalModuloUnchecked (naturalSaturatingSubtract modulus units) modulus))))))
815
816-- Forward distances reach modulus/2 - 1 units, backward ones modulus/2.
817def aarch64DistanceAccepted =
818 (lambda unrestricted direction : (family AArch64Direction) .
819 (lambda unrestricted units : Nat .
820 (lambda unrestricted half : Nat .
821 (eliminate
822 AArch64Direction
823 (lambda unrestricted current : (family AArch64Direction) . Nat)
824 direction
825 (branch AArch64Forward . (naturalLess units half))
826 (branch AArch64Backward . (naturalLessOrEqual units half))))))
827
828-- A 19-bit branch field at bit 5, with `extra` in byte 0 (a condition or a register).
829def aarch64Branch19Word =
830 (lambda unrestricted base3 : Nat .
831 (lambda unrestricted extra : Nat .
832 (lambda unrestricted direction : (family AArch64Direction) .
833 (lambda unrestricted distance : Nat .
834 (nat-eliminate
835 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
836 (constructor AArch64EncodeResult AArch64MisalignedOffset distance)
837 (lambda unrestricted predecessorAligned : Nat .
838 (lambda unrestricted inductionAligned : (family AArch64EncodeResult) .
839 (nat-eliminate
840 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
841 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance)
842 (lambda unrestricted predecessor : Nat .
843 (lambda unrestricted induction : (family AArch64EncodeResult) .
844 (app
845 (lambda unrestricted field : Nat .
846 (aarch64ByteWord
847 (naturalAdd extra (aarch64FromBitFiveByte0 field))
848 (aarch64FromBitFiveByte1 field)
849 (aarch64FromBitFiveByte2 field)
850 base3))
851 (aarch64SignedField
852 direction
853 (naturalDivideUnchecked distance aarch64Four)
854 aarch64Modulus19))))
855 (aarch64DistanceAccepted
856 direction
857 (naturalDivideUnchecked distance aarch64Four)
858 (naturalDivideUnchecked aarch64Modulus19 aarch64Two)))))
859 (naturalIsZero (naturalModuloUnchecked distance aarch64Four)))))))
860
861-- A 26-bit branch field at bit 0.
862def aarch64Branch26Word =
863 (lambda unrestricted base3 : Nat .
864 (lambda unrestricted direction : (family AArch64Direction) .
865 (lambda unrestricted distance : Nat .
866 (nat-eliminate
867 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
868 (constructor AArch64EncodeResult AArch64MisalignedOffset distance)
869 (lambda unrestricted predecessorAligned : Nat .
870 (lambda unrestricted inductionAligned : (family AArch64EncodeResult) .
871 (nat-eliminate
872 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
873 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance)
874 (lambda unrestricted predecessor : Nat .
875 (lambda unrestricted induction : (family AArch64EncodeResult) .
876 (app
877 (lambda unrestricted field : Nat .
878 (aarch64ByteWord
879 (naturalModuloUnchecked field aarch64TwoHundredFiftySix)
880 (naturalModuloUnchecked
881 (naturalDivideUnchecked field aarch64TwoHundredFiftySix)
882 aarch64TwoHundredFiftySix)
883 (naturalModuloUnchecked
884 (naturalDivideUnchecked
885 field
886 (naturalMultiply aarch64TwoHundredFiftySix aarch64TwoHundredFiftySix))
887 aarch64TwoHundredFiftySix)
888 (naturalAdd
889 base3
890 (naturalModuloUnchecked
891 (naturalDivideUnchecked
892 field
893 (naturalMultiply
894 (naturalMultiply
895 aarch64TwoHundredFiftySix
896 aarch64TwoHundredFiftySix)
897 aarch64TwoHundredFiftySix))
898 aarch64Four))))
899 (aarch64SignedField
900 direction
901 (naturalDivideUnchecked distance aarch64Four)
902 aarch64Modulus26))))
903 (aarch64DistanceAccepted
904 direction
905 (naturalDivideUnchecked distance aarch64Four)
906 (naturalDivideUnchecked aarch64Modulus26 aarch64Two)))))
907 (naturalIsZero (naturalModuloUnchecked distance aarch64Four))))))
908
909-- adr: a 21-bit BYTE distance, its low two bits at bits 29-30 and the rest at bit 5.
910def aarch64AddressWord =
911 (lambda unrestricted destination : (family AArch64Register) .
912 (lambda unrestricted direction : (family AArch64Direction) .
913 (lambda unrestricted distance : Nat .
914 (nat-eliminate
915 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
916 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance)
917 (lambda unrestricted predecessor : Nat .
918 (lambda unrestricted induction : (family AArch64EncodeResult) .
919 (app
920 (lambda unrestricted field : Nat .
921 (app
922 (lambda unrestricted high : Nat .
923 (aarch64ByteWord
924 (naturalAdd (aarch64LowFive destination) (aarch64FromBitFiveByte0 high))
925 (aarch64FromBitFiveByte1 high)
926 (aarch64FromBitFiveByte2 high)
927 (naturalAdd
928 16
929 (naturalMultiply
930 (naturalModuloUnchecked field aarch64Four)
931 aarch64ThirtyTwo))))
932 (naturalDivideUnchecked field aarch64Four)))
933 (aarch64SignedField direction distance aarch64Modulus21))))
934 (aarch64DistanceAccepted
935 direction
936 distance
937 (naturalDivideUnchecked aarch64Modulus21 aarch64Two))))))
938
939-- lsl by amount is ubfm with immr = (64 - amount) mod 64 and imms = 63 - amount.
940def aarch64ShiftLeftWord =
941 (lambda unrestricted destination : (family AArch64Register) .
942 (lambda unrestricted source : (family AArch64Register) .
943 (lambda unrestricted amount : Nat .
944 (aarch64EncodeBounded
945 amount
946 aarch64ShiftLimit
947 (app
948 (lambda unrestricted immr : Nat .
949 (app
950 (lambda unrestricted imms : Nat .
951 (aarch64ByteWord
952 (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 source))
953 (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 imms))
954 (naturalAdd aarch64SixtyFour immr)
955 211))
956 (naturalSaturatingSubtract 63 amount)))
957 (naturalModuloUnchecked
958 (naturalSaturatingSubtract aarch64SixtyFour amount)
959 aarch64SixtyFour))))))
960
961-- lsr by amount is ubfm with immr = amount and imms = 63.
962def aarch64ShiftRightWord =
963 (lambda unrestricted destination : (family AArch64Register) .
964 (lambda unrestricted source : (family AArch64Register) .
965 (lambda unrestricted amount : Nat .
966 (aarch64EncodeBounded
967 amount
968 aarch64ShiftLimit
969 (aarch64ByteWord
970 (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 source))
971 (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 63))
972 (naturalAdd aarch64SixtyFour amount)
973 211)))))
974
975-- Scalar single-precision, the A64 counterpart of the x86-64 SSE scalar
976-- lowering (L13c). Every word below was assembled from the same mnemonic by
977-- GNU `as` on this host; the laws in Compiler.MachineAArch64Proof carry the
978-- bytes.
979--
980-- FP data-processing, two sources:
981-- 0001 1110 0 01 Rm opcode 10 Rn Rd
982-- with opcode 0 FMUL, 1 FDIV, 2 FADD, 3 FSUB. The Rm field is bits 16-20, so
983-- byte 2 is 32 + Rm; the `10` in bits 10-11 is the 8 in byte 1.
984def aarch64FloatRdByte0 =
985 (lambda unrestricted register : (family AArch64FloatRegister) .
986 (aarch64FloatRegisterCode register))
987
988def aarch64FloatRnByte0 =
989 (lambda unrestricted register : (family AArch64FloatRegister) .
990 (naturalMultiply
991 (naturalModuloUnchecked (aarch64FloatRegisterCode register) aarch64Eight)
992 aarch64ThirtyTwo))
993
994def aarch64FloatRnByte1 =
995 (lambda unrestricted register : (family AArch64FloatRegister) .
996 (naturalDivideUnchecked (aarch64FloatRegisterCode register) aarch64Eight))
997
998def aarch64FloatDataWord =
999 (lambda unrestricted opcode : Nat .
1000 (lambda unrestricted destination : (family AArch64FloatRegister) .
1001 (lambda unrestricted left : (family AArch64FloatRegister) .
1002 (lambda unrestricted right : (family AArch64FloatRegister) .
1003 (aarch64ByteWord
1004 (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 left))
1005 (naturalAdd
1006 (naturalMultiply opcode 16)
1007 (naturalAdd aarch64Eight (aarch64FloatRnByte1 left)))
1008 (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right))
1009 30)))))
1010
1011-- The same two-source form in double precision: the type field (bits 22-23)
1012-- is 01, the 64 in byte 2.
1013def aarch64FloatData64Word =
1014 (lambda unrestricted opcode : Nat .
1015 (lambda unrestricted destination : (family AArch64FloatRegister) .
1016 (lambda unrestricted left : (family AArch64FloatRegister) .
1017 (lambda unrestricted right : (family AArch64FloatRegister) .
1018 (aarch64ByteWord
1019 (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 left))
1020 (naturalAdd
1021 (naturalMultiply opcode 16)
1022 (naturalAdd aarch64Eight (aarch64FloatRnByte1 left)))
1023 (naturalAdd aarch64SixtyFour (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right)))
1024 30)))))
1025
1026-- One-source FP forms: Rd in bits 0-4 and Rn in bits 5-9, so byte 0 carries
1027-- Rd and Rn's low three bits and byte 1 Rn's high two bits over the form's
1028-- own byte-1 bits (fsqrt d: 1e61c000; fcvt s<-d: 1e624000; fcvt d<-s:
1029-- 1e22c000).
1030def aarch64FloatUnaryWord =
1031 (lambda unrestricted byte1 : Nat .
1032 (lambda unrestricted byte2 : Nat .
1033 (lambda unrestricted byte3 : Nat .
1034 (lambda unrestricted destination : (family AArch64FloatRegister) .
1035 (lambda unrestricted source : (family AArch64FloatRegister) .
1036 (aarch64ByteWord
1037 (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 source))
1038 (naturalAdd byte1 (aarch64FloatRnByte1 source))
1039 byte2
1040 byte3))))))
1041
1042-- FCMP Sn, Sm: 0001 1110 0 01 Rm 001000 Rn 00000. The Rd field is zero -- the
1043-- comparison writes NZCV, not a register -- and bits 10-15 are 001000, which
1044-- is the 32 in byte 1. This is the QUIET compare, the counterpart of the
1045-- SSE lowering's `ucomiss`: a quiet NaN does not raise Invalid, only a
1046-- signalling one does. `fcmpe` would be the signalling form and is not what
1047-- the x86 lane does.
1048def aarch64FloatCompareWord =
1049 (lambda unrestricted left : (family AArch64FloatRegister) .
1050 (lambda unrestricted right : (family AArch64FloatRegister) .
1051 (aarch64ByteWord
1052 (aarch64FloatRnByte0 left)
1053 (naturalAdd aarch64ThirtyTwo (aarch64FloatRnByte1 left))
1054 (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right))
1055 30)))
1056
1057
1058def aarch64EncodeInstruction :
1059 (pi unrestricted instruction : (family AArch64Instruction) . (family AArch64EncodeResult)) =
1060 (lambda unrestricted instruction : (family AArch64Instruction) .
1061 (eliminate
1062 AArch64Instruction
1063 (lambda unrestricted current : (family AArch64Instruction) . (family AArch64EncodeResult))
1064 instruction
1065 (branch
1066 AArch64MoveWideZero
1067 destination
1068 value
1069 shift
1070 .
1071 (aarch64WideWord 210 destination value shift))
1072 (branch
1073 AArch64MoveWideKeep
1074 destination
1075 value
1076 shift
1077 .
1078 (aarch64WideWord 242 destination value shift))
1079 (branch
1080 AArch64MoveRegister
1081 destination
1082 source
1083 .
1084 (aarch64ByteWord
1085 (naturalAdd aarch64StackPointerByte0 (aarch64LowFive destination))
1086 aarch64StackPointerByte1
1087 (aarch64RegisterCode source)
1088 170))
1089 (branch
1090 AArch64AddImmediate
1091 destination
1092 source
1093 value
1094 .
1095 (aarch64ImmediateWord 145 (aarch64LowFive destination) source value))
1096 (branch
1097 AArch64SubtractImmediate
1098 destination
1099 source
1100 value
1101 .
1102 (aarch64ImmediateWord 209 (aarch64LowFive destination) source value))
1103 (branch
1104 AArch64AddRegister
1105 destination
1106 left
1107 right
1108 .
1109 (aarch64ThreeRegisterWord 0 0 139 destination left right))
1110 (branch
1111 AArch64SubtractRegister
1112 destination
1113 left
1114 right
1115 .
1116 (aarch64ThreeRegisterWord 0 0 203 destination left right))
1117 (branch
1118 AArch64AndRegister
1119 destination
1120 left
1121 right
1122 .
1123 (aarch64ThreeRegisterWord 0 0 138 destination left right))
1124 (branch
1125 AArch64OrRegister
1126 destination
1127 left
1128 right
1129 .
1130 (aarch64ThreeRegisterWord 0 0 170 destination left right))
1131 (branch
1132 AArch64ExclusiveOrRegister
1133 destination
1134 left
1135 right
1136 .
1137 (aarch64ThreeRegisterWord 0 0 202 destination left right))
1138 (branch
1139 AArch64ShiftLeftImmediate
1140 destination
1141 source
1142 amount
1143 .
1144 (aarch64ShiftLeftWord destination source amount))
1145 (branch
1146 AArch64ShiftRightImmediate
1147 destination
1148 source
1149 amount
1150 .
1151 (aarch64ShiftRightWord destination source amount))
1152 (branch
1153 AArch64MultiplyRegister
1154 destination
1155 left
1156 right
1157 .
1158 (aarch64ThreeRegisterWord 124 0 155 destination left right))
1159 (branch
1160 AArch64DivideRegisterUnsigned
1161 destination
1162 left
1163 right
1164 .
1165 (aarch64ThreeRegisterWord 8 192 154 destination left right))
1166 (branch
1167 AArch64CompareImmediate
1168 register
1169 value
1170 .
1171 (aarch64ImmediateWord 241 aarch64ZeroRegisterByte0 register value))
1172 (branch
1173 AArch64CompareRegister
1174 left
1175 right
1176 .
1177 (aarch64ByteWord
1178 (naturalAdd aarch64ZeroRegisterByte0 (aarch64RnByte0 left))
1179 (aarch64RnByte1 left)
1180 (aarch64RegisterCode right)
1181 235))
1182 (branch
1183 AArch64LoadMemory64
1184 destination
1185 base
1186 offset
1187 .
1188 (aarch64ScaledMemoryWord aarch64SixtyFour 249 destination base offset))
1189 (branch
1190 AArch64StoreMemory64
1191 base
1192 offset
1193 source
1194 .
1195 (aarch64ScaledMemoryWord 0 249 source base offset))
1196 (branch
1197 AArch64LoadMemory32ZeroExtend
1198 destination
1199 base
1200 offset
1201 .
1202 (aarch64ScaledMemoryWord32 aarch64SixtyFour 185 destination base offset))
1203 (branch
1204 AArch64StoreMemory32
1205 base
1206 offset
1207 source
1208 .
1209 (aarch64ScaledMemoryWord32 0 185 source base offset))
1210 (branch
1211 AArch64LoadMemory8ZeroExtend
1212 destination
1213 base
1214 offset
1215 .
1216 (aarch64ByteMemoryWord aarch64SixtyFour 57 destination base offset))
1217 (branch
1218 AArch64StoreMemory8
1219 base
1220 offset
1221 source
1222 .
1223 (aarch64ByteMemoryWord 0 57 source base offset))
1224 (branch
1225 AArch64AddressRelative
1226 destination
1227 direction
1228 distance
1229 .
1230 (aarch64AddressWord destination direction distance))
1231 (branch AArch64Branch direction distance . (aarch64Branch26Word 20 direction distance))
1232 (branch AArch64BranchLink direction distance . (aarch64Branch26Word 148 direction distance))
1233 (branch
1234 AArch64BranchLinkRegister
1235 target
1236 .
1237 (aarch64ByteWord (aarch64RnByte0 target) (aarch64RnByte1 target) 63 214))
1238 (branch
1239 AArch64BranchIf
1240 condition
1241 direction
1242 distance
1243 .
1244 (aarch64Branch19Word 84 (aarch64ConditionCode condition) direction distance))
1245 (branch
1246 AArch64CompareBranchIfZero
1247 register
1248 direction
1249 distance
1250 .
1251 (aarch64Branch19Word 180 (aarch64LowFive register) direction distance))
1252 (branch
1253 AArch64CompareBranchIfNotZero
1254 register
1255 direction
1256 distance
1257 .
1258 (aarch64Branch19Word 181 (aarch64LowFive register) direction distance))
1259 (branch
1260 AArch64AddImmediateFromStackPointer
1261 destination
1262 value
1263 .
1264 (aarch64EncodeBounded
1265 value
1266 aarch64Immediate12Limit
1267 (aarch64ByteWord
1268 (naturalAdd aarch64StackPointerByte0 (aarch64LowFive destination))
1269 (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 value))
1270 (aarch64Immediate12Byte2 value)
1271 145)))
1272 (branch AArch64AddStackPointer value shift . (aarch64StackAdjustWord 145 value shift))
1273 (branch AArch64SubtractStackPointer value shift . (aarch64StackAdjustWord 209 value shift))
1274 (branch
1275 AArch64LoadMemory64FromStack
1276 destination
1277 offset
1278 .
1279 (aarch64StackScaledWord aarch64SixtyFour 249 destination offset))
1280 (branch
1281 AArch64StoreMemory64ToStack
1282 offset
1283 source
1284 .
1285 (aarch64StackScaledWord 0 249 source offset))
1286 (branch
1287 AArch64LoadMemory8FromStack
1288 destination
1289 offset
1290 .
1291 (aarch64StackByteWord aarch64SixtyFour 57 destination offset))
1292 (branch AArch64StoreMemory8ToStack offset source . (aarch64StackByteWord 0 57 source offset))
1293 (branch AArch64Return . (aarch64ByteWord 192 3 95 214))
1294 (branch AArch64SupervisorCall . (aarch64ByteWord 1 0 0 212))
1295 (branch AArch64DataSynchronizationBarrierSystem . (aarch64ByteWord 159 63 3 213))
1296 (branch
1297 AArch64FloatAdd32
1298 destination
1299 left
1300 right
1301 .
1302 (aarch64FloatDataWord aarch64Two destination left right))
1303 (branch
1304 AArch64FloatSubtract32
1305 destination
1306 left
1307 right
1308 .
1309 (aarch64FloatDataWord 3 destination left right))
1310 (branch
1311 AArch64FloatMultiply32
1312 destination
1313 left
1314 right
1315 .
1316 (aarch64FloatDataWord 0 destination left right))
1317 (branch
1318 AArch64FloatDivide32
1319 destination
1320 left
1321 right
1322 .
1323 (aarch64FloatDataWord 1 destination left right))
1324 (branch
1325 AArch64FloatCompare32
1326 left
1327 right
1328 .
1329 (aarch64FloatCompareWord left right))
1330 (branch
1331 AArch64FloatMoveFromGeneral32
1332 destination
1333 source
1334 .
1335 (aarch64ByteWord
1336 (naturalAdd (aarch64FloatRdByte0 destination) (aarch64RnByte0 source))
1337 (aarch64RnByte1 source)
1338 39
1339 30))
1340 (branch
1341 AArch64FloatMoveToGeneral32
1342 destination
1343 source
1344 .
1345 (aarch64ByteWord
1346 (naturalAdd (aarch64LowFive destination) (aarch64FloatRnByte0 source))
1347 (aarch64FloatRnByte1 source)
1348 38
1349 30))
1350 (branch
1351 AArch64ReadFloatControl
1352 destination
1353 .
1354 (aarch64ByteWord (aarch64LowFive destination) 68 59 213))
1355 (branch
1356 AArch64WriteFloatControl
1357 source
1358 .
1359 (aarch64ByteWord (aarch64LowFive source) 68 27 213))
1360 (branch AArch64FloatAdd64 destination left right . (aarch64FloatData64Word aarch64Two destination left right))
1361 (branch AArch64FloatSubtract64 destination left right . (aarch64FloatData64Word 3 destination left right))
1362 (branch AArch64FloatMultiply64 destination left right . (aarch64FloatData64Word 0 destination left right))
1363 (branch AArch64FloatDivide64 destination left right . (aarch64FloatData64Word 1 destination left right))
1364 (branch
1365 AArch64FloatSquareRoot64
1366 destination
1367 source
1368 .
1369 (aarch64FloatUnaryWord 192 97 30 destination source))
1370 (branch
1371 AArch64FloatFromSigned64
1372 destination
1373 source
1374 .
1375 (aarch64ByteWord
1376 (naturalAdd (aarch64FloatRdByte0 destination) (aarch64RnByte0 source))
1377 (aarch64RnByte1 source)
1378 98
1379 158))
1380 (branch
1381 AArch64FloatNarrow64To32
1382 destination
1383 source
1384 .
1385 (aarch64FloatUnaryWord aarch64SixtyFour 98 30 destination source))
1386 (branch
1387 AArch64FloatWiden32To64
1388 destination
1389 source
1390 .
1391 (aarch64FloatUnaryWord 192 34 30 destination source))
1392 (branch
1393 AArch64FloatMoveFromGeneral64
1394 destination
1395 source
1396 .
1397 (aarch64ByteWord
1398 (naturalAdd (aarch64FloatRdByte0 destination) (aarch64RnByte0 source))
1399 (aarch64RnByte1 source)
1400 103
1401 158))
1402 (branch
1403 AArch64FloatMoveToGeneral64
1404 destination
1405 source
1406 .
1407 (aarch64ByteWord
1408 (naturalAdd (aarch64LowFive destination) (aarch64FloatRnByte0 source))
1409 (aarch64FloatRnByte1 source)
1410 102
1411 158))
1412 (branch AArch64DataSynchronizationBarrier . (aarch64ByteWord 159 63 3 213))))
1413
1414def aarch64AppendResults =
1415 (lambda unrestricted head : (family AArch64EncodeResult) .
1416 (lambda unrestricted tail : (family AArch64EncodeResult) .
1417 (eliminate
1418 AArch64EncodeResult
1419 (lambda unrestricted current : (family AArch64EncodeResult) . (family AArch64EncodeResult))
1420 head
1421 (branch
1422 AArch64Encoded
1423 headBytes
1424 .
1425 (eliminate
1426 AArch64EncodeResult
1427 (lambda unrestricted current : (family AArch64EncodeResult) .
1428 (family AArch64EncodeResult))
1429 tail
1430 (branch
1431 AArch64Encoded
1432 tailBytes
1433 .
1434 (constructor AArch64EncodeResult AArch64Encoded (bytes-append headBytes tailBytes)))
1435 (branch
1436 AArch64ImmediateOutOfRange
1437 value
1438 .
1439 (constructor AArch64EncodeResult AArch64ImmediateOutOfRange value))
1440 (branch
1441 AArch64MisalignedOffset
1442 value
1443 .
1444 (constructor AArch64EncodeResult AArch64MisalignedOffset value))
1445 (branch
1446 AArch64DisplacementOutOfRange
1447 value
1448 .
1449 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange value))))
1450 (branch
1451 AArch64ImmediateOutOfRange
1452 value
1453 .
1454 (constructor AArch64EncodeResult AArch64ImmediateOutOfRange value))
1455 (branch
1456 AArch64MisalignedOffset
1457 value
1458 .
1459 (constructor AArch64EncodeResult AArch64MisalignedOffset value))
1460 (branch
1461 AArch64DisplacementOutOfRange
1462 value
1463 .
1464 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange value)))))
1465
1466def aarch64EncodeProgram :
1467 (pi unrestricted program : (family AArch64Program) . (family AArch64EncodeResult)) =
1468 (lambda unrestricted program : (family AArch64Program) .
1469 (eliminate
1470 AArch64Program
1471 (lambda unrestricted current : (family AArch64Program) . (family AArch64EncodeResult))
1472 program
1473 (branch AArch64ProgramEnd . (constructor AArch64EncodeResult AArch64Encoded b""))
1474 (branch
1475 AArch64ProgramNext
1476 instruction
1477 tail
1478 encodedTail
1479 .
1480 (aarch64AppendResults (aarch64EncodeInstruction instruction) encodedTail))))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.