Runtime.NativeLaunchRecipeRoutine

1module Runtime.NativeLaunchRecipeRoutine
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Runtime.NativePhysicalNative
6import Runtime.LaunchRecipe
7
8-- The shared host routine that expands a launch-table recipe into a mapped
9-- arena at startup.  The compiler emits one recipe per NVIDIA component
10-- (program, QMD, pushbuffer, GPFIFO) from the schedule's repeat structure and
11-- has already checked that the recipe expands to the exact table; this
12-- routine is the same expansion in x86-64, bounded and fail-closed.
13--
14-- Recipe (little-endian):
15--   "ALXR" u32 version=1  u64 outputExtent  u32 opCount  u32 zero
16--   0x01 LITERAL u32 length bytes[length]
17--   0x02 ZERO    u32 length
18--   0x03 REPEAT  u32 count u32 unitLength u32 patchCount unit[unitLength]
19--                patches[patchCount]{u32 offset u64 stride}
20-- REPEAT copies the unit, then for each further copy duplicates the previous
21-- copy and adds every patch's stride to the 64-bit word at its offset.
22--
23-- ABI (System V): rdi = recipe, rsi = recipe extent, rdx = output,
24-- rcx = expected output extent.  Returns rax = bytes written, or zero when the
25-- recipe is malformed, exceeds a bound, or does not fill the expected extent
26-- exactly.  Uses only caller-saved registers and the red zone below rsp.
27--
28-- Red zone slots (below rsp): -8 output start, -16 unit pointer,
29-- -24 unit length, -32 patch cursor, -40 patch count, -48 remaining copies,
30-- -56 recipe cursor after the repeat, -64 patch base.
31
32def lrRAX : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRAX)
33def lrRCX : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRCX)
34def lrRDX : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRDX)
35def lrRSI : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRSI)
36def lrRDI : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRDI)
37def lrRSP : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRSP)
38def lrR8 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR8)
39def lrR9 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR9)
40def lrR10 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR10)
41def lrR11 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR11)
42
43def lrBelow : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionBelow)
44def lrAbove : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionAbove)
45def lrZero : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionZero)
46def lrNotZero : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionNotZero)
47
48-- One instruction per line.  destination = source
49def lrMove =
50  (lambda unrestricted destination : (family X86NativeRegister64) .
51    (lambda unrestricted source : (family X86NativeRegister64) .
52      (lambda unrestricted tail : (family X86NativeAssembly) .
53        (nativePhysicalNativeEmit (nativePhysicalNativeMove source destination) tail))))
54
55-- destination += source
56def lrAdd =
57  (lambda unrestricted destination : (family X86NativeRegister64) .
58    (lambda unrestricted source : (family X86NativeRegister64) .
59      (lambda unrestricted tail : (family X86NativeAssembly) .
60        (nativePhysicalNativeEmit (nativePhysicalNativeAdd source destination) tail))))
61
62-- destination -= source
63def lrSubtract =
64  (lambda unrestricted destination : (family X86NativeRegister64) .
65    (lambda unrestricted source : (family X86NativeRegister64) .
66      (lambda unrestricted tail : (family X86NativeAssembly) .
67        (nativePhysicalNativeEmit (nativePhysicalNativeSubtract source destination) tail))))
68
69def lrAddImmediate =
70  (lambda unrestricted destination : (family X86NativeRegister64) .
71    (lambda unrestricted immediate : Nat .
72      (lambda unrestricted tail : (family X86NativeAssembly) .
73        (nativePhysicalNativeEmit (nativePhysicalNativeAddImmediate destination (x86NativeImmediate32FromNatural immediate)) tail))))
74
75-- flags from left - right: Below means left < right, Above means left > right
76def lrCompare =
77  (lambda unrestricted left : (family X86NativeRegister64) .
78    (lambda unrestricted right : (family X86NativeRegister64) .
79      (lambda unrestricted tail : (family X86NativeAssembly) .
80        (nativePhysicalNativeEmit (nativePhysicalNativeCompare right left) tail))))
81
82def lrCompareImmediate =
83  (lambda unrestricted left : (family X86NativeRegister64) .
84    (lambda unrestricted immediate : Nat .
85      (lambda unrestricted tail : (family X86NativeAssembly) .
86        (nativePhysicalNativeEmit (nativePhysicalNativeCompareImmediate left (x86NativeImmediate32FromNatural immediate)) tail))))
87
88def lrTest =
89  (lambda unrestricted register : (family X86NativeRegister64) .
90    (lambda unrestricted tail : (family X86NativeAssembly) .
91      (nativePhysicalNativeEmit (nativePhysicalNativeTest register register) tail)))
92
93def lrLoad64 =
94  (lambda unrestricted destination : (family X86NativeRegister64) .
95    (lambda unrestricted base : (family X86NativeRegister64) .
96      (lambda unrestricted displacement : Nat .
97        (lambda unrestricted tail : (family X86NativeAssembly) .
98          (nativePhysicalNativeEmit (nativePhysicalNativeLoad64 destination base (x86NativeDisplacement32FromNatural displacement)) tail)))))
99
100def lrLoad32 =
101  (lambda unrestricted destination : (family X86NativeRegister64) .
102    (lambda unrestricted base : (family X86NativeRegister64) .
103      (lambda unrestricted displacement : Nat .
104        (lambda unrestricted tail : (family X86NativeAssembly) .
105          (nativePhysicalNativeEmit
106            (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 destination base (x86NativeDisplacement32FromNatural displacement))
107            tail)))))
108
109def lrLoad8 =
110  (lambda unrestricted destination : (family X86NativeRegister64) .
111    (lambda unrestricted base : (family X86NativeRegister64) .
112      (lambda unrestricted tail : (family X86NativeAssembly) .
113        (nativePhysicalNativeEmit (nativePhysicalNativeLoad8 destination base nativePhysicalNativeD0) tail))))
114
115def lrStore64 =
116  (lambda unrestricted base : (family X86NativeRegister64) .
117    (lambda unrestricted displacement : Nat .
118      (lambda unrestricted source : (family X86NativeRegister64) .
119        (lambda unrestricted tail : (family X86NativeAssembly) .
120          (nativePhysicalNativeEmit (nativePhysicalNativeStore64 base (x86NativeDisplacement32FromNatural displacement) source) tail)))))
121
122def lrStore8 =
123  (lambda unrestricted base : (family X86NativeRegister64) .
124    (lambda unrestricted source : (family X86NativeRegister64) .
125      (lambda unrestricted tail : (family X86NativeAssembly) .
126        (nativePhysicalNativeEmit (nativePhysicalNativeStore8 base nativePhysicalNativeD0 source) tail))))
127
128def lrClear =
129  (lambda unrestricted register : (family X86NativeRegister64) .
130    (lambda unrestricted tail : (family X86NativeAssembly) .
131      (nativePhysicalNativeEmit (constructor X86NativeInstruction X86NativeClear32 register) tail)))
132
133def lrMultiplyImmediate =
134  (lambda unrestricted destination : (family X86NativeRegister64) .
135    (lambda unrestricted immediate : Nat .
136      (lambda unrestricted tail : (family X86NativeAssembly) .
137        (nativePhysicalNativeEmit
138          (constructor X86NativeInstruction X86NativeMultiplyImmediate64 destination (x86NativeImmediate32FromNatural immediate))
139          tail))))
140
141def lrLabel = nativePhysicalNativeLabel
142def lrJump = nativePhysicalNativeJump
143def lrJumpIf = nativePhysicalNativeJumpCondition
144
145def lrReturn =
146  (lambda unrestricted tail : (family X86NativeAssembly) .
147    (nativePhysicalNativeEmit nativePhysicalNativeReturnInstruction tail))
148
149def lrBackendJumpIf = (lambda unrestricted condition : (family LaunchRecipeCondition) .
150  (eliminate LaunchRecipeCondition
151    (lambda unrestricted current : (family LaunchRecipeCondition) . (pi unrestricted name : Bytes . (pi unrestricted tail : (family X86NativeAssembly) . (family X86NativeAssembly)))) condition
152    (branch LaunchRecipeBelow . (lrJumpIf lrBelow))
153    (branch LaunchRecipeAbove . (lrJumpIf lrAbove))
154    (branch LaunchRecipeZero . (lrJumpIf lrZero))
155    (branch LaunchRecipeNotZero . (lrJumpIf lrNotZero))))
156
157def lrX86Backend : (family LaunchRecipeBackend (family X86NativeAssembly) (family X86NativeRegister64)) =
158  (constructor LaunchRecipeBackend LaunchRecipeBackendValue (family X86NativeAssembly) (family X86NativeRegister64)
159    lrMove lrAdd lrSubtract lrAddImmediate lrCompare lrCompareImmediate lrTest
160    lrLoad64 lrLoad32 lrLoad8 lrStore64 lrStore8 lrClear lrMultiplyImmediate
161    lrLabel lrJump lrBackendJumpIf lrReturn (constructor X86NativeAssembly X86NativeAssemblyEnd)
162    lrRAX lrRCX lrRDX lrRSI lrRDI lrRSP lrR8 lrR9 lrR10 lrR11)
163
164def nativeLaunchRecipeAssembly : (family X86NativeAssembly) =
165  (launchRecipeAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) lrX86Backend)
166
167def nativeLaunchRecipeGenerateRoutine : (family X86NativeAssemblyResult) =
168  (x86NativeAssemble nativeLaunchRecipeAssembly)
169
170-- The routine's machine code, or empty bytes when assembly is refused.
171def nativeLaunchRecipeRoutineBytes : Bytes =
172  (eliminate
173    X86NativeAssemblyResult
174    (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
175    nativeLaunchRecipeGenerateRoutine
176    (branch X86NativeAssemblyEncoded code . code)
177    (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
178    (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
179    (branch X86NativeAssemblyMissingLabel name . b"")
180    (branch X86NativeAssemblyDisplacementOutOfRange ordinal . b""))