1module Runtime.NativePhysicalTrainingRoutine
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Model.Word64
6import Runtime.NativePhysicalNative
7import Runtime.NativeMemoryRoutine
8import Std.Natural
9import Model.Parameter
10
11family NativePhysicalTrainingBitPatchDestinationWidth : Type 0
12constructor NativePhysicalTrainingBitPatchDestination32
13constructor NativePhysicalTrainingBitPatchDestination64
14end-family
15
16family NativePhysicalTrainingCheckedBitPatchParameterError : Type 0
17constructor NativePhysicalTrainingCheckedBitPatchWidthZero
18constructor NativePhysicalTrainingCheckedBitPatchSourceBounds
19constructor NativePhysicalTrainingCheckedBitPatchDestinationBounds
20constructor NativePhysicalTrainingCheckedBitPatchAddressBits
21constructor NativePhysicalTrainingCheckedBitPatchAlignmentBits
22
23end-family
24
25family NativePhysicalTrainingCheckedBitPatchGeneration : Type 0
26constructor NativePhysicalTrainingCheckedBitPatchParametersRejected
27field unrestricted nativePhysicalTrainingCheckedBitPatchParameterError : (family NativePhysicalTrainingCheckedBitPatchParameterError)
28constructor NativePhysicalTrainingCheckedBitPatchAssemblyGenerated
29field unrestricted nativePhysicalTrainingCheckedBitPatchAssemblyResult : (family X86NativeAssemblyResult)
30
31end-family
32
33def nativePhysicalTrainingShiftLeftWord =
34 (lambda unrestricted value : (family ModelWord64) .
35 (lambda unrestricted count : Nat .
36 (nat-eliminate
37 (lambda unrestricted current : Nat . (family ModelWord64))
38 value
39 (lambda unrestricted predecessor : Nat .
40 (lambda unrestricted induction : (family ModelWord64) .
41 (app modelWord64ShiftLeftOne induction)))
42 count)))
43
44def nativePhysicalTrainingBitMask =
45 (lambda unrestricted width : Nat .
46 (app
47 (app modelWord64Subtract
48 (app
49 (app nativePhysicalTrainingShiftLeftWord modelWord64One)
50 width))
51 modelWord64One))
52
53def nativePhysicalTrainingImmediate64FromWord =
54 (lambda unrestricted value : (family ModelWord64) .
55 (eliminate ModelWord64
56 (lambda unrestricted current : (family ModelWord64) .
57 (family X86NativeImmediate64))
58 value
59 (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 .
60 (constructor X86NativeImmediate64 X86NativeImmediate64Value
61 b0 b1 b2 b3 b4 b5 b6 b7))))
62
63def nativePhysicalTrainingImmediate8FromNatural =
64 (lambda unrestricted value : Nat .
65 (constructor X86NativeImmediate8 X86NativeImmediate8Value
66 (nat-to-byte value)))
67
68-- The Linux ioctl return value only proves transport success. NVIDIA RM and
69-- UVM replies carry a second 32-bit status inside the mutable payload. This
70-- routine performs both checks as one result-producing operation: nonzero
71-- syscall returns pass through unchanged; successful syscalls return the
72-- embedded status word at payload + statusOffset.
73def nativePhysicalTrainingIoctlStatusFailureLabel =
74 b"ioctl-syscall-fail"
75
76def nativePhysicalTrainingIoctlStatusAssembly =
77 (constructor X86NativeAssembly X86NativeAssemblyEmit
78 (constructor X86NativeInstruction X86NativeAddRegister64
79 (constructor X86NativeRegister64 X86NativeRDX)
80 (constructor X86NativeRegister64 X86NativeR8))
81 (constructor X86NativeAssembly X86NativeAssemblyEmit
82 (constructor X86NativeInstruction X86NativeMoveImmediate32
83 (constructor X86NativeRegister64 X86NativeRAX)
84 (app nativePhysicalNativeI32Byte (byte 16)))
85 (constructor X86NativeAssembly X86NativeAssemblyEmit
86 (constructor X86NativeInstruction X86NativeSystemCall)
87 (constructor X86NativeAssembly X86NativeAssemblyEmit
88 (constructor X86NativeInstruction X86NativeTestRegister64
89 (constructor X86NativeRegister64 X86NativeRAX)
90 (constructor X86NativeRegister64 X86NativeRAX))
91 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
92 (constructor X86NativeCondition X86NativeConditionNotZero)
93 nativePhysicalTrainingIoctlStatusFailureLabel
94 (constructor X86NativeAssembly X86NativeAssemblyEmit
95 (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64
96 (constructor X86NativeRegister64 X86NativeRAX)
97 (constructor X86NativeRegister64 X86NativeR8)
98 nativePhysicalNativeD0)
99 (constructor X86NativeAssembly X86NativeAssemblyEmit
100 (constructor X86NativeInstruction X86NativeReturn)
101 (constructor X86NativeAssembly X86NativeAssemblyLabel
102 nativePhysicalTrainingIoctlStatusFailureLabel
103 (constructor X86NativeAssembly X86NativeAssemblyEmit
104 (constructor X86NativeInstruction X86NativeReturn)
105 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))
106
107def nativePhysicalTrainingGenerateIoctlStatusRoutine =
108 (app x86NativeAssemble nativePhysicalTrainingIoctlStatusAssembly)
109
110def nativePhysicalTrainingBitPatchAssemblyWithAccess =
111 (lambda unrestricted load : (family X86NativeInstruction) .
112 (lambda unrestricted store : (family X86NativeInstruction) .
113 (lambda unrestricted sourceShift : (family X86NativeImmediate8) .
114 (lambda unrestricted destinationShift : (family X86NativeImmediate8) .
115 (lambda unrestricted sourceMask : (family X86NativeImmediate64) .
116 (lambda unrestricted clearMask : (family X86NativeImmediate64) .
117 (constructor X86NativeAssembly X86NativeAssemblyEmit
118 load
119 (constructor X86NativeAssembly X86NativeAssemblyEmit
120 (constructor X86NativeInstruction X86NativeMoveRegister64
121 (constructor X86NativeRegister64 X86NativeRSI)
122 (constructor X86NativeRegister64 X86NativeRCX))
123 (constructor X86NativeAssembly X86NativeAssemblyEmit
124 (constructor X86NativeInstruction X86NativeShiftRightImmediate64
125 (constructor X86NativeRegister64 X86NativeRCX)
126 sourceShift)
127 (constructor X86NativeAssembly X86NativeAssemblyEmit
128 (constructor X86NativeInstruction X86NativeMoveImmediate64
129 (constructor X86NativeRegister64 X86NativeRDX)
130 sourceMask)
131 (constructor X86NativeAssembly X86NativeAssemblyEmit
132 (constructor X86NativeInstruction X86NativeAndRegister64
133 (constructor X86NativeRegister64 X86NativeRDX)
134 (constructor X86NativeRegister64 X86NativeRCX))
135 (constructor X86NativeAssembly X86NativeAssemblyEmit
136 (constructor X86NativeInstruction X86NativeShiftLeftImmediate64
137 (constructor X86NativeRegister64 X86NativeRCX)
138 destinationShift)
139 (constructor X86NativeAssembly X86NativeAssemblyEmit
140 (constructor X86NativeInstruction X86NativeMoveImmediate64
141 (constructor X86NativeRegister64 X86NativeRDX)
142 clearMask)
143 (constructor X86NativeAssembly X86NativeAssemblyEmit
144 (constructor X86NativeInstruction X86NativeAndRegister64
145 (constructor X86NativeRegister64 X86NativeRDX)
146 (constructor X86NativeRegister64 X86NativeRAX))
147 (constructor X86NativeAssembly X86NativeAssemblyEmit
148 (constructor X86NativeInstruction X86NativeOrRegister64
149 (constructor X86NativeRegister64 X86NativeRCX)
150 (constructor X86NativeRegister64 X86NativeRAX))
151 (constructor X86NativeAssembly X86NativeAssemblyEmit
152 store
153 (constructor X86NativeAssembly X86NativeAssemblyEmit
154 (constructor X86NativeInstruction X86NativeClear32
155 (constructor X86NativeRegister64 X86NativeRAX))
156 (constructor X86NativeAssembly X86NativeAssemblyEmit
157 (constructor X86NativeInstruction X86NativeReturn)
158 (constructor X86NativeAssembly
159 X86NativeAssemblyEnd)))))))))))))))))))
160
161def nativePhysicalTrainingBitPatchAssembly =
162 (lambda unrestricted destinationWidth :
163 (family NativePhysicalTrainingBitPatchDestinationWidth) .
164 (lambda unrestricted sourceShift : Nat .
165 (lambda unrestricted destinationShift : Nat .
166 (lambda unrestricted width : Nat .
167 (app
168 (lambda unrestricted sourceMaskWord : (family ModelWord64) .
169 (app
170 (lambda unrestricted shiftedMaskWord : (family ModelWord64) .
171 (app
172 (lambda unrestricted clearMaskWord : (family ModelWord64) .
173 (eliminate NativePhysicalTrainingBitPatchDestinationWidth
174 (lambda unrestricted current :
175 (family NativePhysicalTrainingBitPatchDestinationWidth) .
176 (family X86NativeAssembly))
177 destinationWidth
178 (branch NativePhysicalTrainingBitPatchDestination32 .
179 (app
180 (app
181 (app
182 (app
183 (app
184 (app nativePhysicalTrainingBitPatchAssemblyWithAccess
185 (constructor X86NativeInstruction
186 X86NativeLoadMemory32ZeroExtend64
187 (constructor X86NativeRegister64 X86NativeRAX)
188 (constructor X86NativeRegister64 X86NativeRDI)
189 nativePhysicalNativeD0))
190 (constructor X86NativeInstruction
191 X86NativeStoreMemory32
192 (constructor X86NativeRegister64 X86NativeRDI)
193 nativePhysicalNativeD0
194 (constructor X86NativeRegister64 X86NativeRAX)))
195 (app nativePhysicalTrainingImmediate8FromNatural
196 sourceShift))
197 (app nativePhysicalTrainingImmediate8FromNatural
198 destinationShift))
199 (app nativePhysicalTrainingImmediate64FromWord
200 sourceMaskWord))
201 (app nativePhysicalTrainingImmediate64FromWord
202 clearMaskWord)))
203 (branch NativePhysicalTrainingBitPatchDestination64 .
204 (app
205 (app
206 (app
207 (app
208 (app
209 (app nativePhysicalTrainingBitPatchAssemblyWithAccess
210 (constructor X86NativeInstruction
211 X86NativeLoadMemory64
212 (constructor X86NativeRegister64 X86NativeRAX)
213 (constructor X86NativeRegister64 X86NativeRDI)
214 nativePhysicalNativeD0))
215 (constructor X86NativeInstruction
216 X86NativeStoreMemory64
217 (constructor X86NativeRegister64 X86NativeRDI)
218 nativePhysicalNativeD0
219 (constructor X86NativeRegister64 X86NativeRAX)))
220 (app nativePhysicalTrainingImmediate8FromNatural
221 sourceShift))
222 (app nativePhysicalTrainingImmediate8FromNatural
223 destinationShift))
224 (app nativePhysicalTrainingImmediate64FromWord
225 sourceMaskWord))
226 (app nativePhysicalTrainingImmediate64FromWord
227 clearMaskWord)))))
228 (app modelWord64Complement shiftedMaskWord)))
229 (app
230 (app nativePhysicalTrainingShiftLeftWord sourceMaskWord)
231 destinationShift)))
232 (app nativePhysicalTrainingBitMask width))))))
233
234def nativePhysicalTrainingGenerateBitPatchRoutine =
235 (lambda unrestricted destinationWidth :
236 (family NativePhysicalTrainingBitPatchDestinationWidth) .
237 (lambda unrestricted sourceShift : Nat .
238 (lambda unrestricted destinationShift : Nat .
239 (lambda unrestricted width : Nat .
240 (app x86NativeAssemble
241 (app
242 (app
243 (app
244 (app nativePhysicalTrainingBitPatchAssembly destinationWidth)
245 sourceShift)
246 destinationShift)
247 width))))))
248
249def nativePhysicalTrainingPatch32Assembly =
250 (constructor X86NativeAssembly X86NativeAssemblyEmit
251 (constructor X86NativeInstruction X86NativeStoreMemory32
252 (constructor X86NativeRegister64 X86NativeRDI)
253 nativePhysicalNativeD0
254 (constructor X86NativeRegister64 X86NativeRSI))
255 (constructor X86NativeAssembly X86NativeAssemblyEmit
256 (constructor X86NativeInstruction X86NativeClear32
257 (constructor X86NativeRegister64 X86NativeRAX))
258 (constructor X86NativeAssembly X86NativeAssemblyEmit
259 (constructor X86NativeInstruction X86NativeReturn)
260 (constructor X86NativeAssembly X86NativeAssemblyEnd))))
261
262def nativePhysicalTrainingPatch64Assembly =
263 (constructor X86NativeAssembly X86NativeAssemblyEmit
264 (constructor X86NativeInstruction X86NativeStoreMemory64
265 (constructor X86NativeRegister64 X86NativeRDI)
266 nativePhysicalNativeD0
267 (constructor X86NativeRegister64 X86NativeRSI))
268 (constructor X86NativeAssembly X86NativeAssemblyEmit
269 (constructor X86NativeInstruction X86NativeClear32
270 (constructor X86NativeRegister64 X86NativeRAX))
271 (constructor X86NativeAssembly X86NativeAssemblyEmit
272 (constructor X86NativeInstruction X86NativeReturn)
273 (constructor X86NativeAssembly X86NativeAssemblyEnd))))
274
275def nativePhysicalTrainingPublish32Assembly =
276 (constructor X86NativeAssembly X86NativeAssemblyEmit
277 (constructor X86NativeInstruction X86NativeStoreMemory32
278 (constructor X86NativeRegister64 X86NativeRDI)
279 nativePhysicalNativeD0
280 (constructor X86NativeRegister64 X86NativeRSI))
281 (constructor X86NativeAssembly X86NativeAssemblyEmit
282 (constructor X86NativeInstruction X86NativeStoreFence)
283 (constructor X86NativeAssembly X86NativeAssemblyEmit
284 (constructor X86NativeInstruction X86NativeStoreMemory32
285 (constructor X86NativeRegister64 X86NativeRDX)
286 nativePhysicalNativeD0
287 (constructor X86NativeRegister64 X86NativeRCX))
288 (constructor X86NativeAssembly X86NativeAssemblyEmit
289 (constructor X86NativeInstruction X86NativeClear32
290 (constructor X86NativeRegister64 X86NativeRAX))
291 (constructor X86NativeAssembly X86NativeAssemblyEmit
292 (constructor X86NativeInstruction X86NativeReturn)
293 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))
294
295def nativePhysicalTrainingPublish64Assembly =
296 (constructor X86NativeAssembly X86NativeAssemblyEmit
297 (constructor X86NativeInstruction X86NativeStoreMemory64
298 (constructor X86NativeRegister64 X86NativeRDI)
299 nativePhysicalNativeD0
300 (constructor X86NativeRegister64 X86NativeRSI))
301 (constructor X86NativeAssembly X86NativeAssemblyEmit
302 (constructor X86NativeInstruction X86NativeStoreFence)
303 (constructor X86NativeAssembly X86NativeAssemblyEmit
304 (constructor X86NativeInstruction X86NativeStoreMemory64
305 (constructor X86NativeRegister64 X86NativeRDX)
306 nativePhysicalNativeD0
307 (constructor X86NativeRegister64 X86NativeRCX))
308 (constructor X86NativeAssembly X86NativeAssemblyEmit
309 (constructor X86NativeInstruction X86NativeClear32
310 (constructor X86NativeRegister64 X86NativeRAX))
311 (constructor X86NativeAssembly X86NativeAssemblyEmit
312 (constructor X86NativeInstruction X86NativeReturn)
313 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))
314
315def nativePhysicalTrainingPublish3264Assembly =
316 (constructor X86NativeAssembly X86NativeAssemblyEmit
317 (constructor X86NativeInstruction X86NativeStoreMemory32
318 (constructor X86NativeRegister64 X86NativeRDI)
319 nativePhysicalNativeD0
320 (constructor X86NativeRegister64 X86NativeRSI))
321 (constructor X86NativeAssembly X86NativeAssemblyEmit
322 (constructor X86NativeInstruction X86NativeStoreFence)
323 (constructor X86NativeAssembly X86NativeAssemblyEmit
324 (constructor X86NativeInstruction X86NativeStoreMemory64
325 (constructor X86NativeRegister64 X86NativeRDX)
326 nativePhysicalNativeD0
327 (constructor X86NativeRegister64 X86NativeRCX))
328 (constructor X86NativeAssembly X86NativeAssemblyEmit
329 (constructor X86NativeInstruction X86NativeClear32
330 (constructor X86NativeRegister64 X86NativeRAX))
331 (constructor X86NativeAssembly X86NativeAssemblyEmit
332 (constructor X86NativeInstruction X86NativeReturn)
333 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))
334
335def nativePhysicalTrainingPublish6432Assembly =
336 (constructor X86NativeAssembly X86NativeAssemblyEmit
337 (constructor X86NativeInstruction X86NativeStoreMemory64
338 (constructor X86NativeRegister64 X86NativeRDI)
339 nativePhysicalNativeD0
340 (constructor X86NativeRegister64 X86NativeRSI))
341 (constructor X86NativeAssembly X86NativeAssemblyEmit
342 (constructor X86NativeInstruction X86NativeStoreFence)
343 (constructor X86NativeAssembly X86NativeAssemblyEmit
344 (constructor X86NativeInstruction X86NativeStoreMemory32
345 (constructor X86NativeRegister64 X86NativeRDX)
346 nativePhysicalNativeD0
347 (constructor X86NativeRegister64 X86NativeRCX))
348 (constructor X86NativeAssembly X86NativeAssemblyEmit
349 (constructor X86NativeInstruction X86NativeClear32
350 (constructor X86NativeRegister64 X86NativeRAX))
351 (constructor X86NativeAssembly X86NativeAssemblyEmit
352 (constructor X86NativeInstruction X86NativeReturn)
353 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))
354
355def nativePhysicalTrainingGeneratePatch32Routine =
356 (app x86NativeAssemble nativePhysicalTrainingPatch32Assembly)
357
358def nativePhysicalTrainingGeneratePatch64Routine =
359 (app x86NativeAssemble nativePhysicalTrainingPatch64Assembly)
360
361def nativePhysicalTrainingGeneratePublish32Routine =
362 (app x86NativeAssemble nativePhysicalTrainingPublish32Assembly)
363
364def nativePhysicalTrainingGeneratePublish64Routine =
365 (app x86NativeAssemble nativePhysicalTrainingPublish64Assembly)
366
367def nativePhysicalTrainingGeneratePublish3264Routine =
368 (app x86NativeAssemble nativePhysicalTrainingPublish3264Assembly)
369
370def nativePhysicalTrainingGeneratePublish6432Routine =
371 (app x86NativeAssemble nativePhysicalTrainingPublish6432Assembly)
372
373def nativePhysicalTrainingGenerateCheckpointCopyRoutine =
374 nativeMemoryGenerateCopyRoutine
375
376def nativePhysicalTrainingFence32LoopLabel =
377 b"fence-32-loop"
378
379def nativePhysicalTrainingFence32SuccessLabel =
380 b"fence-32-success"
381
382def nativePhysicalTrainingFence32TimeoutLabel =
383 b"fence-32-timeout"
384
385def nativePhysicalTrainingFence64LoopLabel =
386 b"fence-64-loop"
387
388def nativePhysicalTrainingFence64SuccessLabel =
389 b"fence-64-success"
390
391def nativePhysicalTrainingFence64TimeoutLabel =
392 b"fence-64-timeout"
393
394def nativePhysicalTrainingFence32Assembly =
395 (constructor X86NativeAssembly X86NativeAssemblyLabel
396 nativePhysicalTrainingFence32LoopLabel
397 (constructor X86NativeAssembly X86NativeAssemblyEmit
398 (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64
399 (constructor X86NativeRegister64 X86NativeRAX)
400 (constructor X86NativeRegister64 X86NativeRDI)
401 nativePhysicalNativeD0)
402 (constructor X86NativeAssembly X86NativeAssemblyEmit
403 (constructor X86NativeInstruction X86NativeStoreMemory32
404 (constructor X86NativeRegister64 X86NativeRCX)
405 nativePhysicalNativeD0
406 (constructor X86NativeRegister64 X86NativeRAX))
407 (constructor X86NativeAssembly X86NativeAssemblyEmit
408 (constructor X86NativeInstruction X86NativeCompareRegister64
409 (constructor X86NativeRegister64 X86NativeRSI)
410 (constructor X86NativeRegister64 X86NativeRAX))
411 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
412 (constructor X86NativeCondition X86NativeConditionZero)
413 nativePhysicalTrainingFence32SuccessLabel
414 (constructor X86NativeAssembly X86NativeAssemblyEmit
415 (constructor X86NativeInstruction X86NativeTestRegister64
416 (constructor X86NativeRegister64 X86NativeRDX)
417 (constructor X86NativeRegister64 X86NativeRDX))
418 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
419 (constructor X86NativeCondition X86NativeConditionZero)
420 nativePhysicalTrainingFence32TimeoutLabel
421 (constructor X86NativeAssembly X86NativeAssemblyEmit
422 (constructor X86NativeInstruction X86NativeAddImmediate64
423 (constructor X86NativeRegister64 X86NativeRDX)
424 nativePhysicalNativeI32NegativeOne)
425 (constructor X86NativeAssembly X86NativeAssemblyJump
426 nativePhysicalTrainingFence32LoopLabel
427 (constructor X86NativeAssembly X86NativeAssemblyLabel
428 nativePhysicalTrainingFence32SuccessLabel
429 (constructor X86NativeAssembly X86NativeAssemblyEmit
430 (constructor X86NativeInstruction X86NativeClear32
431 (constructor X86NativeRegister64 X86NativeRAX))
432 (constructor X86NativeAssembly X86NativeAssemblyEmit
433 (constructor X86NativeInstruction X86NativeReturn)
434 (constructor X86NativeAssembly X86NativeAssemblyLabel
435 nativePhysicalTrainingFence32TimeoutLabel
436 (constructor X86NativeAssembly X86NativeAssemblyEmit
437 (constructor X86NativeInstruction X86NativeMoveImmediate32
438 (constructor X86NativeRegister64 X86NativeRAX)
439 nativePhysicalNativeI32NegativeOne)
440 (constructor X86NativeAssembly X86NativeAssemblyEmit
441 (constructor X86NativeInstruction X86NativeReturn)
442 (constructor X86NativeAssembly
443 X86NativeAssemblyEnd))))))))))))))))
444
445def nativePhysicalTrainingFence64Assembly =
446 (constructor X86NativeAssembly X86NativeAssemblyLabel
447 nativePhysicalTrainingFence64LoopLabel
448 (constructor X86NativeAssembly X86NativeAssemblyEmit
449 (constructor X86NativeInstruction X86NativeLoadMemory64
450 (constructor X86NativeRegister64 X86NativeRAX)
451 (constructor X86NativeRegister64 X86NativeRDI)
452 nativePhysicalNativeD0)
453 (constructor X86NativeAssembly X86NativeAssemblyEmit
454 (constructor X86NativeInstruction X86NativeStoreMemory64
455 (constructor X86NativeRegister64 X86NativeRCX)
456 nativePhysicalNativeD0
457 (constructor X86NativeRegister64 X86NativeRAX))
458 (constructor X86NativeAssembly X86NativeAssemblyEmit
459 (constructor X86NativeInstruction X86NativeCompareRegister64
460 (constructor X86NativeRegister64 X86NativeRSI)
461 (constructor X86NativeRegister64 X86NativeRAX))
462 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
463 (constructor X86NativeCondition X86NativeConditionZero)
464 nativePhysicalTrainingFence64SuccessLabel
465 (constructor X86NativeAssembly X86NativeAssemblyEmit
466 (constructor X86NativeInstruction X86NativeTestRegister64
467 (constructor X86NativeRegister64 X86NativeRDX)
468 (constructor X86NativeRegister64 X86NativeRDX))
469 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
470 (constructor X86NativeCondition X86NativeConditionZero)
471 nativePhysicalTrainingFence64TimeoutLabel
472 (constructor X86NativeAssembly X86NativeAssemblyEmit
473 (constructor X86NativeInstruction X86NativeAddImmediate64
474 (constructor X86NativeRegister64 X86NativeRDX)
475 nativePhysicalNativeI32NegativeOne)
476 (constructor X86NativeAssembly X86NativeAssemblyJump
477 nativePhysicalTrainingFence64LoopLabel
478 (constructor X86NativeAssembly X86NativeAssemblyLabel
479 nativePhysicalTrainingFence64SuccessLabel
480 (constructor X86NativeAssembly X86NativeAssemblyEmit
481 (constructor X86NativeInstruction X86NativeClear32
482 (constructor X86NativeRegister64 X86NativeRAX))
483 (constructor X86NativeAssembly X86NativeAssemblyEmit
484 (constructor X86NativeInstruction X86NativeReturn)
485 (constructor X86NativeAssembly X86NativeAssemblyLabel
486 nativePhysicalTrainingFence64TimeoutLabel
487 (constructor X86NativeAssembly X86NativeAssemblyEmit
488 (constructor X86NativeInstruction X86NativeMoveImmediate32
489 (constructor X86NativeRegister64 X86NativeRAX)
490 nativePhysicalNativeI32NegativeOne)
491 (constructor X86NativeAssembly X86NativeAssemblyEmit
492 (constructor X86NativeInstruction X86NativeReturn)
493 (constructor X86NativeAssembly
494 X86NativeAssemblyEnd))))))))))))))))
495
496def nativePhysicalTrainingGenerateFence32Routine =
497 (app x86NativeAssemble nativePhysicalTrainingFence32Assembly)
498
499def nativePhysicalTrainingGenerateFence64Routine =
500 (app x86NativeAssemble nativePhysicalTrainingFence64Assembly)
501
502def nativePhysicalTrainingRoutineHostFallbacks =
503 zero
504
505def nativePhysicalTrainingCheckedBitPatchCarryLabel =
506 b"addr-carry"
507
508def nativePhysicalTrainingCheckedBitPatchRangeLabel =
509 b"addr-range"
510
511def nativePhysicalTrainingCheckedBitPatchAlignmentLabel =
512 b"addr-align"
513
514def nativePhysicalTrainingCheckedBitPatchAssemblyAppend =
515 (lambda unrestricted assembly : (family X86NativeAssembly) .
516 (lambda unrestricted tail : (family X86NativeAssembly) .
517 (eliminate
518 X86NativeAssembly
519 (lambda unrestricted current : (family X86NativeAssembly) . (family X86NativeAssembly))
520 assembly
521 (branch X86NativeAssemblyEnd . tail)
522 (branch
523 X86NativeAssemblyEmit
524 instruction
525 rest
526 induction
527 .
528 (constructor X86NativeAssembly X86NativeAssemblyEmit instruction induction))
529 (branch
530 X86NativeAssemblyLabel
531 name
532 rest
533 induction
534 .
535 (constructor X86NativeAssembly X86NativeAssemblyLabel name induction))
536 (branch
537 X86NativeAssemblyJump
538 target
539 rest
540 induction
541 .
542 (constructor X86NativeAssembly X86NativeAssemblyJump target induction))
543 (branch
544 X86NativeAssemblyJumpCondition
545 condition
546 target
547 rest
548 induction
549 .
550 (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition target induction))
551 (branch
552 X86NativeAssemblyLoadEffectiveAddressRIPLabel
553 destination
554 target
555 rest
556 induction
557 .
558 (constructor
559 X86NativeAssembly
560 X86NativeAssemblyLoadEffectiveAddressRIPLabel
561 destination
562 target
563 induction)))))
564
565def nativePhysicalTrainingCheckedBitPatchAssemblyGuard =
566 (lambda unrestricted highMask : (family X86NativeImmediate64) .
567 (lambda unrestricted alignmentMask : (family X86NativeImmediate64) .
568 (lambda unrestricted body : (family X86NativeAssembly) .
569 (constructor
570 X86NativeAssembly
571 X86NativeAssemblyEmit
572 (constructor
573 X86NativeInstruction
574 X86NativeAddRegister64
575 (constructor X86NativeRegister64 X86NativeRDX)
576 (constructor X86NativeRegister64 X86NativeRSI))
577 (constructor
578 X86NativeAssembly
579 X86NativeAssemblyJumpCondition
580 (constructor X86NativeCondition X86NativeConditionBelow)
581 nativePhysicalTrainingCheckedBitPatchCarryLabel
582 (constructor
583 X86NativeAssembly
584 X86NativeAssemblyEmit
585 (constructor
586 X86NativeInstruction
587 X86NativeMoveRegister64
588 (constructor X86NativeRegister64 X86NativeRSI)
589 (constructor X86NativeRegister64 X86NativeRCX))
590 (constructor
591 X86NativeAssembly
592 X86NativeAssemblyEmit
593 (constructor
594 X86NativeInstruction
595 X86NativeMoveImmediate64
596 (constructor X86NativeRegister64 X86NativeRDX)
597 highMask)
598 (constructor
599 X86NativeAssembly
600 X86NativeAssemblyEmit
601 (constructor
602 X86NativeInstruction
603 X86NativeAndRegister64
604 (constructor X86NativeRegister64 X86NativeRDX)
605 (constructor X86NativeRegister64 X86NativeRCX))
606 (constructor
607 X86NativeAssembly
608 X86NativeAssemblyEmit
609 (constructor
610 X86NativeInstruction
611 X86NativeTestRegister64
612 (constructor X86NativeRegister64 X86NativeRCX)
613 (constructor X86NativeRegister64 X86NativeRCX))
614 (constructor
615 X86NativeAssembly
616 X86NativeAssemblyJumpCondition
617 (constructor X86NativeCondition X86NativeConditionNotZero)
618 nativePhysicalTrainingCheckedBitPatchRangeLabel
619 (constructor
620 X86NativeAssembly
621 X86NativeAssemblyEmit
622 (constructor
623 X86NativeInstruction
624 X86NativeMoveRegister64
625 (constructor X86NativeRegister64 X86NativeRSI)
626 (constructor X86NativeRegister64 X86NativeRCX))
627 (constructor
628 X86NativeAssembly
629 X86NativeAssemblyEmit
630 (constructor
631 X86NativeInstruction
632 X86NativeMoveImmediate64
633 (constructor X86NativeRegister64 X86NativeRDX)
634 alignmentMask)
635 (constructor
636 X86NativeAssembly
637 X86NativeAssemblyEmit
638 (constructor
639 X86NativeInstruction
640 X86NativeAndRegister64
641 (constructor X86NativeRegister64 X86NativeRDX)
642 (constructor X86NativeRegister64 X86NativeRCX))
643 (constructor
644 X86NativeAssembly
645 X86NativeAssemblyEmit
646 (constructor
647 X86NativeInstruction
648 X86NativeTestRegister64
649 (constructor X86NativeRegister64 X86NativeRCX)
650 (constructor X86NativeRegister64 X86NativeRCX))
651 (constructor
652 X86NativeAssembly
653 X86NativeAssemblyJumpCondition
654 (constructor X86NativeCondition X86NativeConditionNotZero)
655 nativePhysicalTrainingCheckedBitPatchAlignmentLabel
656 (app
657 nativePhysicalTrainingCheckedBitPatchAssemblyAppend
658 body
659 (constructor
660 X86NativeAssembly
661 X86NativeAssemblyLabel
662 nativePhysicalTrainingCheckedBitPatchCarryLabel
663 (constructor
664 X86NativeAssembly
665 X86NativeAssemblyEmit
666 (constructor
667 X86NativeInstruction
668 X86NativeMoveImmediate32
669 (constructor X86NativeRegister64 X86NativeRAX)
670 (app nativePhysicalNativeI32Byte (byte 1)))
671 (constructor
672 X86NativeAssembly
673 X86NativeAssemblyEmit
674 (constructor X86NativeInstruction X86NativeReturn)
675 (constructor
676 X86NativeAssembly
677 X86NativeAssemblyLabel
678 nativePhysicalTrainingCheckedBitPatchRangeLabel
679 (constructor
680 X86NativeAssembly
681 X86NativeAssemblyEmit
682 (constructor
683 X86NativeInstruction
684 X86NativeMoveImmediate32
685 (constructor X86NativeRegister64 X86NativeRAX)
686 (app nativePhysicalNativeI32Byte (byte 2)))
687 (constructor
688 X86NativeAssembly
689 X86NativeAssemblyEmit
690 (constructor X86NativeInstruction X86NativeReturn)
691 (constructor
692 X86NativeAssembly
693 X86NativeAssemblyLabel
694 nativePhysicalTrainingCheckedBitPatchAlignmentLabel
695 (constructor
696 X86NativeAssembly
697 X86NativeAssemblyEmit
698 (constructor
699 X86NativeInstruction
700 X86NativeMoveImmediate32
701 (constructor X86NativeRegister64 X86NativeRAX)
702 (app nativePhysicalNativeI32Byte (byte 3)))
703 (constructor
704 X86NativeAssembly
705 X86NativeAssemblyEmit
706 (constructor X86NativeInstruction X86NativeReturn)
707 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))))))))))
708
709def nativePhysicalTrainingCheckedBitPatchRequire =
710 (lambda unrestricted accepted : Nat .
711 (lambda unrestricted error : (family NativePhysicalTrainingCheckedBitPatchParameterError) .
712 (lambda unrestricted continuation : (pi unrestricted ignored : Nat . (family NativePhysicalTrainingCheckedBitPatchGeneration)) .
713 (app
714 (nat-eliminate
715 (lambda unrestricted current : Nat .
716 (pi unrestricted ignored : Nat .
717 (family NativePhysicalTrainingCheckedBitPatchGeneration)))
718 (lambda unrestricted ignored : Nat .
719 (constructor
720 NativePhysicalTrainingCheckedBitPatchGeneration
721 NativePhysicalTrainingCheckedBitPatchParametersRejected
722 error))
723 (lambda unrestricted predecessor : Nat .
724 (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family NativePhysicalTrainingCheckedBitPatchGeneration)) .
725 continuation))
726 accepted)
727 zero))))
728
729def nativePhysicalTrainingCheckedBitPatchFieldFits =
730 (lambda unrestricted shift : Nat .
731 (lambda unrestricted width : Nat .
732 (lambda unrestricted limit : Nat .
733 (app
734 (nat-eliminate
735 (lambda unrestricted current : Nat . (pi unrestricted ignored : Nat . Nat))
736 (lambda unrestricted ignored : Nat .
737 (app naturalIsZero (nat-less-than (app naturalSaturatingSubtract limit width) shift)))
738 (lambda unrestricted predecessor : Nat .
739 (lambda unrestricted induction : (pi unrestricted ignored : Nat . Nat) .
740 (lambda unrestricted ignored : Nat . zero)))
741 (nat-less-than limit width))
742 zero))))
743
744def nativePhysicalTrainingGenerateCheckedAddressBitPatchRoutine =
745 (lambda unrestricted destinationWidth : (family NativePhysicalTrainingBitPatchDestinationWidth) .
746 (lambda unrestricted sourceShift : Nat .
747 (lambda unrestricted destinationShift : Nat .
748 (lambda unrestricted width : Nat .
749 (lambda unrestricted addressBits : Nat .
750 (lambda unrestricted alignmentBits : Nat .
751 (app
752 (lambda unrestricted destinationBits : Nat .
753 (app
754 nativePhysicalTrainingCheckedBitPatchRequire
755 (app naturalNonzero width)
756 (constructor
757 NativePhysicalTrainingCheckedBitPatchParameterError
758 NativePhysicalTrainingCheckedBitPatchWidthZero)
759 (lambda unrestricted ignored : Nat .
760 (app
761 nativePhysicalTrainingCheckedBitPatchRequire
762 (app
763 nativePhysicalTrainingCheckedBitPatchFieldFits
764 sourceShift
765 width
766 (byte-to-nat (byte 64)))
767 (constructor
768 NativePhysicalTrainingCheckedBitPatchParameterError
769 NativePhysicalTrainingCheckedBitPatchSourceBounds)
770 (lambda unrestricted ignored : Nat .
771 (app
772 nativePhysicalTrainingCheckedBitPatchRequire
773 (app
774 nativePhysicalTrainingCheckedBitPatchFieldFits
775 destinationShift
776 width
777 destinationBits)
778 (constructor
779 NativePhysicalTrainingCheckedBitPatchParameterError
780 NativePhysicalTrainingCheckedBitPatchDestinationBounds)
781 (lambda unrestricted ignored : Nat .
782 (app
783 nativePhysicalTrainingCheckedBitPatchRequire
784 (app
785 naturalAnd
786 (app naturalNonzero addressBits)
787 (app naturalLessOrEqual addressBits (byte-to-nat (byte 64))))
788 (constructor
789 NativePhysicalTrainingCheckedBitPatchParameterError
790 NativePhysicalTrainingCheckedBitPatchAddressBits)
791 (lambda unrestricted ignored : Nat .
792 (app
793 nativePhysicalTrainingCheckedBitPatchRequire
794 (app
795 naturalAnd
796 (nat-less-than alignmentBits (byte-to-nat (byte 64)))
797 (app naturalLessOrEqual alignmentBits addressBits))
798 (constructor
799 NativePhysicalTrainingCheckedBitPatchParameterError
800 NativePhysicalTrainingCheckedBitPatchAlignmentBits)
801 (lambda unrestricted ignored : Nat .
802 (constructor
803 NativePhysicalTrainingCheckedBitPatchGeneration
804 NativePhysicalTrainingCheckedBitPatchAssemblyGenerated
805 (app
806 x86NativeAssemble
807 (app
808 nativePhysicalTrainingCheckedBitPatchAssemblyGuard
809 (app
810 nativePhysicalTrainingImmediate64FromWord
811 (app
812 modelWord64Complement
813 (app nativePhysicalTrainingBitMask addressBits)))
814 (app
815 nativePhysicalTrainingImmediate64FromWord
816 (app nativePhysicalTrainingBitMask alignmentBits))
817 (app
818 nativePhysicalTrainingBitPatchAssembly
819 destinationWidth
820 sourceShift
821 destinationShift
822 width)))))))))))))))
823 (eliminate
824 NativePhysicalTrainingBitPatchDestinationWidth
825 (lambda unrestricted current : (family NativePhysicalTrainingBitPatchDestinationWidth) .
826 Nat)
827 destinationWidth
828 (branch NativePhysicalTrainingBitPatchDestination32 . (byte-to-nat (byte 32)))
829 (branch NativePhysicalTrainingBitPatchDestination64 . (byte-to-nat (byte 64)))))))))))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.