Platform.AArch64.LaunchRecipeRoutine

1module Platform.AArch64.LaunchRecipeRoutine
2
3import Compiler.MachineAArch64
4import Compiler.MachineAArch64Assembly
5import Platform.AArch64.RoutineEmitter
6import Runtime.LaunchRecipe
7
8-- AAPCS64 realization of the shared recipe algorithm. Its four arguments are
9-- x0..x3 and its result is x0. Logical temporaries occupy x4..x8; x9 is the
10-- private frame base. x12..x15 (the interpreter's persistent image state), x18
11-- and every callee-saved register remain untouched. No call changes x30.
12-- AArch64 has no red zone, so allocate 64 aligned stack bytes explicitly and
13-- release them on BOTH returns, including malformed-input rejection.
14def arAddress = (lambda unrestricted base : (family AArch64Register) .
15  (lambda unrestricted displacement : Nat . (lambda unrestricted tail : (family AArch64Assembly) .
16    (ahrSignedImm ahrX17 displacement
17      (ahrEmit (constructor AArch64Instruction AArch64AddRegister ahrX16 base ahrX17) tail)))))
18def arLoad64 = (lambda unrestricted destination : (family AArch64Register) .
19  (lambda unrestricted base : (family AArch64Register) . (lambda unrestricted displacement : Nat .
20    (lambda unrestricted tail : (family AArch64Assembly) .
21      (arAddress base displacement
22        (ahrEmit (constructor AArch64Instruction AArch64LoadMemory64 destination ahrX16 0) tail))))))
23def arStore64 = (lambda unrestricted base : (family AArch64Register) .
24  (lambda unrestricted displacement : Nat . (lambda unrestricted source : (family AArch64Register) .
25    (lambda unrestricted tail : (family AArch64Assembly) .
26      (arAddress base displacement
27        (ahrEmit (constructor AArch64Instruction AArch64StoreMemory64 ahrX16 0 source) tail))))))
28def arLoad8 = (lambda unrestricted destination : (family AArch64Register) .
29  (lambda unrestricted base : (family AArch64Register) . (ahrLoad8 destination base 0)))
30def arStore8 = (lambda unrestricted base : (family AArch64Register) .
31  (lambda unrestricted source : (family AArch64Register) . (ahrStore8 base 0 source)))
32def arSubtract = (lambda unrestricted destination : (family AArch64Register) .
33  (lambda unrestricted source : (family AArch64Register) .
34    (ahrEmit (constructor AArch64Instruction AArch64SubtractRegister destination destination source))))
35def arCompare = (lambda unrestricted left : (family AArch64Register) .
36  (lambda unrestricted right : (family AArch64Register) .
37    (ahrEmit (constructor AArch64Instruction AArch64CompareRegister left right))))
38def arTest = (lambda unrestricted register : (family AArch64Register) .
39  (ahrEmit (constructor AArch64Instruction AArch64CompareImmediate register 0)))
40def arClear = (lambda unrestricted register : (family AArch64Register) . (ahrMovImm register 0))
41def arJump = (lambda unrestricted label : Bytes . (lambda unrestricted tail : (family AArch64Assembly) .
42  (constructor AArch64Assembly AArch64AssemblyBranch label tail)))
43def arJumpIf = (lambda unrestricted condition : (family LaunchRecipeCondition) .
44  (lambda unrestricted label : Bytes . (lambda unrestricted tail : (family AArch64Assembly) .
45    (constructor AArch64Assembly AArch64AssemblyBranchIf
46      (eliminate LaunchRecipeCondition (lambda unrestricted current : (family LaunchRecipeCondition) . (family AArch64Condition)) condition
47        (branch LaunchRecipeBelow . (constructor AArch64Condition AArch64CarryClear))
48        (branch LaunchRecipeAbove . (constructor AArch64Condition AArch64UnsignedHigher))
49        (branch LaunchRecipeZero . (constructor AArch64Condition AArch64Equal))
50        (branch LaunchRecipeNotZero . (constructor AArch64Condition AArch64NotEqual))) label tail))))
51def arReturn = (lambda unrestricted tail : (family AArch64Assembly) .
52  (ahrMov ahrX0 ahrX6
53    (ahrEmit (constructor AArch64Instruction AArch64AddStackPointer 64
54      (constructor AArch64ImmediateShift AArch64Unshifted)) (ahrReturn tail))))
55
56def aarch64LaunchRecipeBackend : (family LaunchRecipeBackend (family AArch64Assembly) (family AArch64Register)) =
57  (constructor LaunchRecipeBackend LaunchRecipeBackendValue (family AArch64Assembly) (family AArch64Register)
58    ahrMov ahrAdd arSubtract ahrAddImm arCompare ahrCmpImm arTest
59    arLoad64 ahrLoad32 arLoad8 arStore64 arStore8 arClear ahrMulImm
60    ahrLabel arJump arJumpIf arReturn ahrEnd
61    ahrX6 ahrX3 ahrX2 ahrX1 ahrX0 ahrX9 ahrX4 ahrX5 ahrX7 ahrX8)
62def aarch64LaunchRecipeAssembly =
63  (ahrEmit (constructor AArch64Instruction AArch64SubtractStackPointer 64
64    (constructor AArch64ImmediateShift AArch64Unshifted))
65    (ahrEmit (constructor AArch64Instruction AArch64AddImmediateFromStackPointer ahrX9 64)
66      (launchRecipeAssemblyFor (family AArch64Assembly) (family AArch64Register) aarch64LaunchRecipeBackend)))
67def aarch64LaunchRecipeRoutine : Bytes =
68  (eliminate AArch64AssemblyResult (lambda unrestricted result : (family AArch64AssemblyResult) . Bytes)
69    (aarch64Assemble aarch64LaunchRecipeAssembly)
70    (branch AArch64AssemblyEncoded code . code)
71    (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
72    (branch AArch64AssemblyMissingLabel name . b"")
73    (branch AArch64AssemblyDisplacementOutOfRange name . b"")
74    (branch AArch64AssemblyOperandRefused value . b""))