1module Runtime.NativeLaunchRecipeLoad
2
3import Model.Config
4import Model.Parameter
5import Model.Word64
6import Runtime.NativeLaunchRecipeRoutine
7import Runtime.NativePhysicalProgram
8import Std.Natural
9
10-- The host-program commands that bring one embedded launch-table recipe into
11-- a mapped arena: read the recipe from the executable into a staging area,
12-- expand it in place with the shared routine, and require the exact extent.
13-- Every system's host program loads its program, QMD, pushbuffer and GPFIFO
14-- components through this fragment; nothing here knows a system or a card.
15
16def nativeLaunchRecipeWord =
17 (lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value))
18
19def nativeLaunchRecipeImmediate =
20 (lambda unrestricted value : Nat .
21 (constructor NativePhysicalOperand NativePhysicalImmediate (nativeLaunchRecipeWord value)))
22
23def nativeLaunchRecipeSlot =
24 (lambda unrestricted index : Nat .
25 (constructor NativePhysicalSlot NativePhysicalSlotValue (nativeLaunchRecipeWord index)))
26
27def nativeLaunchRecipeSlotValue =
28 (lambda unrestricted index : Nat .
29 (constructor NativePhysicalOperand NativePhysicalResultValue (nativeLaunchRecipeSlot index)))
30
31def nativeLaunchRecipeStore =
32 (lambda unrestricted index : Nat .
33 (constructor NativePhysicalResultBinding NativePhysicalStoreResult (nativeLaunchRecipeSlot index)))
34
35def nativeLaunchRecipeArguments =
36 (lambda unrestricted a0 : (family NativePhysicalOperand) .
37 (lambda unrestricted a1 : (family NativePhysicalOperand) .
38 (lambda unrestricted a2 : (family NativePhysicalOperand) .
39 (lambda unrestricted a3 : (family NativePhysicalOperand) .
40 (constructor NativePhysicalArguments NativePhysicalArgumentsValue
41 a0 a1 a2 a3 (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0))))))
42
43def nativeLaunchRecipeCommand =
44 (lambda unrestricted operation : (family NativePhysicalOperation) .
45 (lambda unrestricted errorIdentity : Bytes .
46 (lambda unrestricted tail : (family NativePhysicalCommands) .
47 (constructor NativePhysicalCommands NativePhysicalCommandsNext
48 (constructor NativePhysicalCommand NativePhysicalCommandValue operation errorIdentity)
49 tail))))
50
51def nativeLaunchRecipeAssertEqual =
52 (lambda unrestricted left : (family NativePhysicalOperand) .
53 (lambda unrestricted right : (family NativePhysicalOperand) .
54 (lambda unrestricted errorIdentity : Bytes .
55 (lambda unrestricted tail : (family NativePhysicalCommands) .
56 (nativeLaunchRecipeCommand
57 (constructor NativePhysicalOperation NativePhysicalAssertEqual left right
58 (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed))
59 errorIdentity
60 tail)))))
61
62-- PROT_READ | PROT_WRITE and MAP_PRIVATE | MAP_FIXED | MAP_ANONYMOUS.
63def nativeLaunchRecipeMapProtection : Nat = 3
64def nativeLaunchRecipeMapFlags : Nat = 50
65def nativeLaunchRecipeNoDescriptor : Nat = 18446744073709551615
66
67-- Map the staging area once, at a fixed address the artifact reserves for it.
68-- Its extent must cover the longest recipe the host loads.
69def nativeLaunchRecipeStagingCommands =
70 (lambda unrestricted stagingAddress : Nat .
71 (lambda unrestricted stagingExtent : Nat .
72 (lambda unrestricted resultSlot : Nat .
73 (lambda unrestricted errorIdentity : Bytes .
74 (lambda unrestricted tail : (family NativePhysicalCommands) .
75 (nativeLaunchRecipeCommand
76 (constructor NativePhysicalOperation NativePhysicalSystemCall
77 (nativeLaunchRecipeImmediate 9)
78 (constructor NativePhysicalArguments NativePhysicalArgumentsValue
79 (nativeLaunchRecipeImmediate stagingAddress)
80 (nativeLaunchRecipeImmediate stagingExtent)
81 (nativeLaunchRecipeImmediate nativeLaunchRecipeMapProtection)
82 (nativeLaunchRecipeImmediate nativeLaunchRecipeMapFlags)
83 (nativeLaunchRecipeImmediate nativeLaunchRecipeNoDescriptor)
84 (nativeLaunchRecipeImmediate 0))
85 b""
86 (nativeLaunchRecipeStore resultSlot))
87 errorIdentity
88 (nativeLaunchRecipeAssertEqual
89 (nativeLaunchRecipeSlotValue resultSlot)
90 (nativeLaunchRecipeImmediate stagingAddress)
91 errorIdentity
92 tail)))))))
93
94-- Load one recipe: pread64 it from the executable at its component offset
95-- into the staging area, expand it into the destination, and require the
96-- routine to report exactly the table's extent. `executable` is the operand
97-- holding the /proc/self/exe descriptor.
98def nativeLaunchRecipeLoadCommands =
99 (lambda unrestricted executable : (family NativePhysicalOperand) .
100 (lambda unrestricted stagingAddress : Nat .
101 (lambda unrestricted recipeOffset : Nat .
102 (lambda unrestricted recipeExtent : Nat .
103 (lambda unrestricted destination : Nat .
104 (lambda unrestricted tableExtent : Nat .
105 (lambda unrestricted resultSlot : Nat .
106 (lambda unrestricted errorIdentity : Bytes .
107 (lambda unrestricted tail : (family NativePhysicalCommands) .
108 (nativeLaunchRecipeCommand
109 (constructor NativePhysicalOperation NativePhysicalSystemCall
110 (nativeLaunchRecipeImmediate 17)
111 (nativeLaunchRecipeArguments
112 executable
113 (nativeLaunchRecipeImmediate stagingAddress)
114 (nativeLaunchRecipeImmediate recipeExtent)
115 (nativeLaunchRecipeImmediate recipeOffset))
116 b""
117 (nativeLaunchRecipeStore resultSlot))
118 errorIdentity
119 (nativeLaunchRecipeAssertEqual
120 (nativeLaunchRecipeSlotValue resultSlot)
121 (nativeLaunchRecipeImmediate recipeExtent)
122 errorIdentity
123 (nativeLaunchRecipeCommand
124 (constructor NativePhysicalOperation NativePhysicalMachineRoutine
125 nativeLaunchRecipeRoutineBytes
126 (nativeLaunchRecipeArguments
127 (nativeLaunchRecipeImmediate stagingAddress)
128 (nativeLaunchRecipeImmediate recipeExtent)
129 (nativeLaunchRecipeImmediate destination)
130 (nativeLaunchRecipeImmediate tableExtent))
131 (nativeLaunchRecipeStore resultSlot))
132 errorIdentity
133 (nativeLaunchRecipeAssertEqual
134 (nativeLaunchRecipeSlotValue resultSlot)
135 (nativeLaunchRecipeImmediate tableExtent)
136 errorIdentity
137 tail)))))))))))))
138
139-- The same load with the offsets and extents already as machine words, for
140-- host programs that carry their layout as ModelWord64 values.
141def nativeLaunchRecipeWordImmediate =
142 (lambda unrestricted value : (family ModelWord64) .
143 (constructor NativePhysicalOperand NativePhysicalImmediate value))
144
145def nativeLaunchRecipeLoadWords =
146 (lambda unrestricted executable : (family NativePhysicalOperand) .
147 (lambda unrestricted stagingAddress : Nat .
148 (lambda unrestricted recipeOffset : (family ModelWord64) .
149 (lambda unrestricted recipeExtent : (family ModelWord64) .
150 (lambda unrestricted destination : Nat .
151 (lambda unrestricted tableExtent : (family ModelWord64) .
152 (lambda unrestricted resultSlot : Nat .
153 (lambda unrestricted errorIdentity : Bytes .
154 (lambda unrestricted tail : (family NativePhysicalCommands) .
155 (nativeLaunchRecipeCommand
156 (constructor NativePhysicalOperation NativePhysicalSystemCall
157 (nativeLaunchRecipeImmediate 17)
158 (nativeLaunchRecipeArguments
159 executable
160 (nativeLaunchRecipeImmediate stagingAddress)
161 (nativeLaunchRecipeWordImmediate recipeExtent)
162 (nativeLaunchRecipeWordImmediate recipeOffset))
163 b""
164 (nativeLaunchRecipeStore resultSlot))
165 errorIdentity
166 (nativeLaunchRecipeAssertEqual
167 (nativeLaunchRecipeSlotValue resultSlot)
168 (nativeLaunchRecipeWordImmediate recipeExtent)
169 errorIdentity
170 (nativeLaunchRecipeCommand
171 (constructor NativePhysicalOperation NativePhysicalMachineRoutine
172 nativeLaunchRecipeRoutineBytes
173 (nativeLaunchRecipeArguments
174 (nativeLaunchRecipeImmediate stagingAddress)
175 (nativeLaunchRecipeWordImmediate recipeExtent)
176 (nativeLaunchRecipeImmediate destination)
177 (nativeLaunchRecipeWordImmediate tableExtent))
178 (nativeLaunchRecipeStore resultSlot))
179 errorIdentity
180 (nativeLaunchRecipeAssertEqual
181 (nativeLaunchRecipeSlotValue resultSlot)
182 (nativeLaunchRecipeWordImmediate tableExtent)
183 errorIdentity
184 tail)))))))))))))
185
186-- The same load with the recipe's offset and extent as operands: the words a
187-- host read from its own manifest at run time, so the host program needs no
188-- build-time knowledge of where the linker put the recipe.
189def nativeLaunchRecipeLoadOperands =
190 (lambda unrestricted executable : (family NativePhysicalOperand) .
191 (lambda unrestricted stagingAddress : Nat .
192 (lambda unrestricted recipeOffset : (family NativePhysicalOperand) .
193 (lambda unrestricted recipeExtent : (family NativePhysicalOperand) .
194 (lambda unrestricted destination : Nat .
195 (lambda unrestricted tableExtent : Nat .
196 (lambda unrestricted resultSlot : Nat .
197 (lambda unrestricted errorIdentity : Bytes .
198 (lambda unrestricted tail : (family NativePhysicalCommands) .
199 (nativeLaunchRecipeCommand
200 (constructor NativePhysicalOperation NativePhysicalSystemCall
201 (nativeLaunchRecipeImmediate 17)
202 (nativeLaunchRecipeArguments
203 executable
204 (nativeLaunchRecipeImmediate stagingAddress)
205 recipeExtent
206 recipeOffset)
207 b""
208 (nativeLaunchRecipeStore resultSlot))
209 errorIdentity
210 (nativeLaunchRecipeAssertEqual
211 (nativeLaunchRecipeSlotValue resultSlot)
212 recipeExtent
213 errorIdentity
214 (nativeLaunchRecipeCommand
215 (constructor NativePhysicalOperation NativePhysicalMachineRoutine
216 nativeLaunchRecipeRoutineBytes
217 (nativeLaunchRecipeArguments
218 (nativeLaunchRecipeImmediate stagingAddress)
219 recipeExtent
220 (nativeLaunchRecipeImmediate destination)
221 (nativeLaunchRecipeImmediate tableExtent))
222 (nativeLaunchRecipeStore resultSlot))
223 errorIdentity
224 (nativeLaunchRecipeAssertEqual
225 (nativeLaunchRecipeSlotValue resultSlot)
226 (nativeLaunchRecipeImmediate tableExtent)
227 errorIdentity
228 tail)))))))))))))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.