1module Platform.AArch64.HostLowering
2
3import Compiler.ELF
4import Data.Bytes
5import Model.Config
6import Model.Parameter
7import Model.Word64
8import Platform.AArch64.MemoryRoutine
9import Platform.AArch64.WordArithmetic
10import Platform.AArch64.SocketRoutine
11import Runtime.NativeMemoryRoutine
12import Runtime.NativeWordArithmetic
13import Runtime.NativeFloatPlan
14import Platform.AArch64.FloatRoutine
15import Runtime.NativeSocketRoutine
16import Runtime.NativeSocketEndpoint
17import Platform.AArch64.Descriptor
18import Platform.AArch64.CardInfo
19import Platform.Linux.Nvidia.DeviceBinding
20import Runtime.NativeDescriptor
21import Platform.AArch64.CyclicRecordOffset
22import Platform.AArch64.LaunchRecipeRoutine
23import Platform.AArch64.NativePhysicalELF
24import Platform.AArch64.NativePhysicalRuntime
25import Platform.Linux.Nvidia.PlanHost
26import Platform.AArch64.PublicationRoutine
27import Platform.AArch64.TelemetrySeal
28import Platform.AArch64.WordDigest
29import Runtime.NativeCyclicRecordOffset
30import Runtime.NativeTelemetrySeal
31import Runtime.NativeWordDigest
32import Compiler.MachineAArch64Assembly
33import Runtime.NativeLaunchRecipeRoutine
34import Runtime.NativePhysicalImage
35import Runtime.NativePhysicalImagePlan
36import Runtime.NativePhysicalProgram
37import Std.Natural
38
39-- A host program for Linux x86-64 lowered to Linux AArch64.
40--
41-- The physical command language is the same on both machines and the
42-- runtimes interpret it block for block (Platform.AArch64.
43-- NativePhysicalRuntime). What differs is the Linux ABI the program's own
44-- commands speak and the machine code its routines carry, and this module is
45-- the one place both are translated:
46--
47-- * a system call's number, from the x86-64 table to the asm-generic one
48-- AArch64 uses;
49-- * the three x86-64 calls AArch64 has only in their general form -- dup2,
50-- unlink and rename become dup3(old, new, 0), unlinkat(AT_FDCWD, path,
51-- 0) and renameat2(AT_FDCWD, old, AT_FDCWD, new, 0), the same calls on
52-- both kernels;
53-- * openat's flags, whose O_DIRECT, O_LARGEFILE, O_DIRECTORY and
54-- O_NOFOLLOW bits sit at different positions (see ahlOpenFlags);
55-- * a machine routine, by its exact x86-64 code, to its AArch64 twin --
56-- including the endpoint routines (connect, accept), so a learner's
57-- participant establishes its own sessions on either host.
58--
59-- Anything else -- a call this table does not know, a number or an openat
60-- flag word not given as an immediate, a routine without a twin -- is
61-- refused by name, never passed through.
62family AArch64SystemCallForm : Type 0
63constructor AArch64SystemCallAbsent
64-- the same arguments under another number
65constructor AArch64SystemCallSame
66field unrestricted aarch64SystemCallSameNumber : Nat
67constructor AArch64SystemCallDup3
68field unrestricted aarch64SystemCallDup3Number : Nat
69constructor AArch64SystemCallUnlinkat
70field unrestricted aarch64SystemCallUnlinkatNumber : Nat
71constructor AArch64SystemCallRenameat2
72field unrestricted aarch64SystemCallRenameat2Number : Nat
73constructor AArch64SystemCallOpenat
74field unrestricted aarch64SystemCallOpenatNumber : Nat
75
76end-family
77
78family AArch64SystemCallTable : Type 0
79constructor AArch64SystemCallTableEnd
80constructor AArch64SystemCallTableNext
81field unrestricted aarch64SystemCallTableX86 : Nat
82field unrestricted aarch64SystemCallTableForm : (family AArch64SystemCallForm)
83recursive unrestricted aarch64SystemCallTableRest
84
85end-family
86
87family AArch64HostOperation : Type 0
88constructor AArch64HostOperationLowered
89field unrestricted aarch64HostOperationValue : (family NativePhysicalOperation)
90constructor AArch64HostOperationRefused
91field unrestricted aarch64HostOperationReason : Bytes
92-- two commands in place of one
93constructor AArch64HostOperationLoweredPair
94field unrestricted aarch64HostOperationFirst : (family NativePhysicalOperation)
95field unrestricted aarch64HostOperationSecond : (family NativePhysicalOperation)
96
97end-family
98
99family AArch64HostLowering : Type 0
100constructor AArch64HostLowered
101field unrestricted aarch64HostLoweredProgram : (family NativePhysicalProgram)
102constructor AArch64HostRefused
103-- why, and the command (from 0) that was refused
104field unrestricted aarch64HostRefusedReason : Bytes
105field unrestricted aarch64HostRefusedCommand : Nat
106
107end-family
108
109family AArch64HostRoutines : Type 0
110constructor AArch64HostRoutinesEnd
111constructor AArch64HostRoutinesNext
112field unrestricted aarch64HostRoutineX86 : Bytes
113field unrestricted aarch64HostRoutineAArch64 : Bytes
114recursive unrestricted aarch64HostRoutinesRest
115
116end-family
117
118family AArch64HostCommands : Type 0
119constructor AArch64HostCommandsLowered
120field unrestricted aarch64HostCommandsValue : (family NativePhysicalCommands)
121constructor AArch64HostCommandsRefused
122field unrestricted aarch64HostCommandsReason : Bytes
123field unrestricted aarch64HostCommandsIndex : Nat
124
125end-family
126
127-- the asm-generic AT_FDCWD, the same -100 as x86-64's
128def ahlAtFdCwd : Nat =
129 18446744073709551516
130
131def ahlEntry =
132 (lambda unrestricted x86 : Nat .
133 (lambda unrestricted form : (family AArch64SystemCallForm) .
134 (lambda unrestricted rest : (family AArch64SystemCallTable) .
135 (constructor AArch64SystemCallTable AArch64SystemCallTableNext x86 form rest))))
136
137def ahlSame =
138 (lambda unrestricted number : Nat .
139 (constructor AArch64SystemCallForm AArch64SystemCallSame number))
140
141-- Every call the plan hosts and the host-runtime contracts make: x86-64
142-- (arch/x86/entry/syscalls/syscall_64.tbl) against asm-generic
143-- (include/uapi/asm-generic/unistd.h).
144def aarch64SystemCallTable : (family AArch64SystemCallTable) =
145 (ahlEntry
146 0
147 (ahlSame 63) -- read
148 (ahlEntry
149 1
150 (ahlSame 64) -- write
151 (ahlEntry
152 3
153 (ahlSame 57) -- close
154 (ahlEntry
155 5
156 (ahlSame 80) -- fstat (st_size at 48 in both layouts)
157 (ahlEntry
158 8
159 (ahlSame 62) -- lseek
160 (ahlEntry
161 9
162 (ahlSame 222) -- mmap
163 (ahlEntry
164 11
165 (ahlSame 215) -- munmap
166 (ahlEntry
167 16
168 (ahlSame 29) -- ioctl
169 (ahlEntry
170 17
171 (ahlSame 67) -- pread64
172 (ahlEntry
173 18
174 (ahlSame 68) -- pwrite64
175 (ahlEntry
176 33
177 (constructor AArch64SystemCallForm AArch64SystemCallDup3 24)
178 (ahlEntry
179 35
180 (ahlSame 101) -- nanosleep
181 (ahlEntry
182 40
183 (ahlSame 71) -- sendfile
184 (ahlEntry
185 41
186 (ahlSame 198) -- socket
187 (ahlEntry
188 43
189 (ahlSame 202) -- accept
190 (ahlEntry
191 49
192 (ahlSame 200) -- bind
193 (ahlEntry
194 50
195 (ahlSame 201) -- listen
196 (ahlEntry
197 51
198 (ahlSame 204) -- getsockname
199 (ahlEntry
200 54
201 (ahlSame 208) -- setsockopt (level/option values shared, see Runtime.NativeSocketPlan)
202 (ahlEntry
203 60
204 (ahlSame 93) -- exit
205 (ahlEntry
206 74
207 (ahlSame 82) -- fsync
208 (ahlEntry
209 75
210 (ahlSame 83) -- fdatasync
211 (ahlEntry
212 82
213 (constructor
214 AArch64SystemCallForm
215 AArch64SystemCallRenameat2
216 276)
217 (ahlEntry
218 87
219 (constructor
220 AArch64SystemCallForm
221 AArch64SystemCallUnlinkat
222 35)
223 (ahlEntry
224 228
225 (ahlSame 113) -- clock_gettime
226 (ahlEntry
227 231
228 (ahlSame 94) -- exit_group
229 (ahlEntry
230 257
231 (constructor
232 AArch64SystemCallForm
233 AArch64SystemCallOpenat
234 56)
235 (ahlEntry
236 293
237 (ahlSame 59) -- pipe2
238 (ahlEntry
239 316
240 (ahlSame 276) -- renameat2 (RENAME_* flags are asm-generic on both)
241 (ahlEntry
242 324
243 (ahlSame 283) -- membarrier
244 (constructor
245 AArch64SystemCallTable
246 AArch64SystemCallTableEnd)))))))))))))))))))))))))))))))
247
248def aarch64SystemCallFor =
249 (lambda unrestricted x86 : Nat .
250 (eliminate
251 AArch64SystemCallTable
252 (lambda unrestricted current : (family AArch64SystemCallTable) .
253 (family AArch64SystemCallForm))
254 aarch64SystemCallTable
255 (branch
256 AArch64SystemCallTableEnd
257 .
258 (constructor AArch64SystemCallForm AArch64SystemCallAbsent))
259 (branch
260 AArch64SystemCallTableNext
261 key
262 form
263 rest
264 induction
265 .
266 (nat-eliminate
267 (lambda unrestricted current : Nat . (family AArch64SystemCallForm))
268 induction
269 (lambda unrestricted predecessor : Nat .
270 (lambda unrestricted ignored : (family AArch64SystemCallForm) . form))
271 (naturalEqual key x86)))))
272
273-- open(2) flag bits that sit at different positions in the two ABIs:
274-- include/uapi/asm-generic/fcntl.h (x86-64 uses it unchanged) against
275-- arch/arm64/include/uapi/asm/fcntl.h.
276-- O_DIRECT x86-64 0x4000 AArch64 0x10000
277-- O_LARGEFILE x86-64 0x8000 AArch64 0x20000
278-- O_DIRECTORY x86-64 0x10000 AArch64 0x4000
279-- O_NOFOLLOW x86-64 0x20000 AArch64 0x8000
280-- Every other flag bit has one value on both. The four positions are
281-- exchanged among themselves, so each is tested on the caller's x86-64 word,
282-- never on a partly translated one. Checkpoint restore and publication open
283-- with O_NOFOLLOW; moving it (not refusing it) is what lets an AArch64
284-- participant restore the shards an x86-64 participant published.
285def ahlX86Direct : Nat =
286 0x4000
287
288def ahlX86LargeFile : Nat =
289 0x8000
290
291def ahlX86Directory : Nat =
292 0x10000
293
294def ahlX86NoFollow : Nat =
295 0x20000
296
297def ahlAArch64Direct : Nat =
298 0x10000
299
300def ahlAArch64LargeFile : Nat =
301 0x20000
302
303def ahlAArch64Directory : Nat =
304 0x4000
305
306def ahlAArch64NoFollow : Nat =
307 0x8000
308
309def ahlBit =
310 (lambda unrestricted flags : Nat .
311 (lambda unrestricted bit : Nat . (naturalModuloUnchecked (naturalDivideUnchecked flags bit) 2)))
312
313-- `bit` when the x86-64 word sets x86, else zero
314def ahlMovedBit =
315 (lambda unrestricted flags : Nat .
316 (lambda unrestricted x86 : Nat .
317 (lambda unrestricted bit : Nat . (naturalMultiply (ahlBit flags x86) bit))))
318
319-- ---- results ----
320def ahlImm =
321 (lambda unrestricted value : Nat .
322 (constructor
323 NativePhysicalOperand
324 NativePhysicalImmediate
325 (modelWord64FromNaturalTruncated value)))
326
327def ahlLowered =
328 (lambda unrestricted operation : (family NativePhysicalOperation) .
329 (constructor AArch64HostOperation AArch64HostOperationLowered operation))
330
331def ahlRefuse =
332 (lambda unrestricted reason : Bytes .
333 (constructor AArch64HostOperation AArch64HostOperationRefused reason))
334
335-- the natural an operand holds when it is an immediate, else `otherwise`
336def ahlImmediateOr =
337 (lambda unrestricted operand : (family NativePhysicalOperand) .
338 (lambda unrestricted continue : (pi unrestricted value : Nat . (family AArch64HostOperation)) .
339 (lambda unrestricted otherwise : (family AArch64HostOperation) .
340 (eliminate
341 NativePhysicalOperand
342 (lambda unrestricted current : (family NativePhysicalOperand) .
343 (family AArch64HostOperation))
344 operand
345 (branch NativePhysicalImmediate value . (continue (modelWord64Natural value)))
346 (branch NativePhysicalResultValue slot . otherwise)
347 (branch NativePhysicalResultAddress slot offset . otherwise)
348 (branch NativePhysicalStateAddress offset . otherwise)
349 (branch NativePhysicalStateLoad64 offset . otherwise)
350 (branch NativePhysicalPayloadAddress offset . otherwise)
351 (branch NativePhysicalPayloadLoad64 offset . otherwise)
352 (branch NativePhysicalProcessArgument index . otherwise)
353 (branch NativePhysicalLoopAffine base stride . otherwise)))))
354
355-- ... else refuse
356def ahlWithImmediate =
357 (lambda unrestricted operand : (family NativePhysicalOperand) .
358 (lambda unrestricted reason : Bytes .
359 (lambda unrestricted continue : (pi unrestricted value : Nat . (family AArch64HostOperation)) .
360 (ahlImmediateOr operand continue (ahlRefuse reason)))))
361
362-- openat's flags on AArch64: the four relocated bits moved, every other bit
363-- the same
364def ahlOpenFlags =
365 (lambda unrestricted flags : Nat .
366 (naturalAdd
367 (naturalSaturatingSubtract
368 flags
369 (naturalAdd
370 (ahlMovedBit flags ahlX86Direct ahlX86Direct)
371 (naturalAdd
372 (ahlMovedBit flags ahlX86LargeFile ahlX86LargeFile)
373 (naturalAdd
374 (ahlMovedBit flags ahlX86Directory ahlX86Directory)
375 (ahlMovedBit flags ahlX86NoFollow ahlX86NoFollow)))))
376 (naturalAdd
377 (ahlMovedBit flags ahlX86Direct ahlAArch64Direct)
378 (naturalAdd
379 (ahlMovedBit flags ahlX86LargeFile ahlAArch64LargeFile)
380 (naturalAdd
381 (ahlMovedBit flags ahlX86Directory ahlAArch64Directory)
382 (ahlMovedBit flags ahlX86NoFollow ahlAArch64NoFollow))))))
383
384def ahlSystemCall =
385 (lambda unrestricted number : Nat .
386 (lambda unrestricted arguments : (family NativePhysicalArguments) .
387 (lambda unrestricted payload : Bytes .
388 (lambda unrestricted result : (family NativePhysicalResultBinding) .
389 (eliminate
390 NativePhysicalArguments
391 (lambda unrestricted current : (family NativePhysicalArguments) .
392 (family AArch64HostOperation))
393 arguments
394 (branch
395 NativePhysicalArgumentsValue
396 a0
397 a1
398 a2
399 a3
400 a4
401 a5
402 .
403 (let unrestricted call =
404 (lambda unrestricted target : Nat .
405 (lambda unrestricted argv : (family NativePhysicalArguments) .
406 (ahlLowered
407 (constructor
408 NativePhysicalOperation
409 NativePhysicalSystemCall
410 (ahlImm target)
411 argv
412 payload
413 result))))
414 in
415 (eliminate
416 AArch64SystemCallForm
417 (lambda unrestricted current : (family AArch64SystemCallForm) .
418 (family AArch64HostOperation))
419 (aarch64SystemCallFor number)
420 (branch AArch64SystemCallAbsent . (ahlRefuse b"aarch64-host-system-call-unknown"))
421 (branch AArch64SystemCallSame target . (call target arguments))
422 (branch
423 AArch64SystemCallDup3
424 target
425 .
426 (call
427 target
428 (constructor
429 NativePhysicalArguments
430 NativePhysicalArgumentsValue
431 a0
432 a1
433 (ahlImm 0)
434 a3
435 a4
436 a5)))
437 (branch
438 AArch64SystemCallUnlinkat
439 target
440 .
441 (call
442 target
443 (constructor
444 NativePhysicalArguments
445 NativePhysicalArgumentsValue
446 (ahlImm ahlAtFdCwd)
447 a0
448 (ahlImm 0)
449 (ahlImm 0)
450 (ahlImm 0)
451 (ahlImm 0))))
452 (branch
453 AArch64SystemCallRenameat2
454 target
455 .
456 (call
457 target
458 (constructor
459 NativePhysicalArguments
460 NativePhysicalArgumentsValue
461 (ahlImm ahlAtFdCwd)
462 a0
463 (ahlImm ahlAtFdCwd)
464 a1
465 (ahlImm 0)
466 (ahlImm 0))))
467 (branch
468 AArch64SystemCallOpenat
469 target
470 .
471 (ahlWithImmediate
472 a2
473 b"aarch64-host-openat-flags-not-immediate"
474 (lambda unrestricted flags : Nat .
475 (call
476 target
477 (constructor
478 NativePhysicalArguments
479 NativePhysicalArgumentsValue
480 a0
481 a1
482 (ahlImm (ahlOpenFlags flags))
483 a3
484 a4
485 a5)))))))))))))
486
487-- ---- a number read at run time ----
488-- A system call whose number the program reads at run time (the text
489-- request's operation word is one: 39 continues, 231 stops) cannot be
490-- translated here. It is translated there, by a routine generated from the
491-- table above: x0 in, the AArch64 number of an entry of the same form out,
492-- and -1 -- a call the kernel refuses -- for any other. Its result is kept
493-- in one result slot this lowering adds after the program's own.
494def ahlTranslateLabel =
495 (lambda unrestricted x86 : Nat .
496 (bytes-append
497 b"ahl-translate-"
498 (bytes
499 (nat-to-byte (naturalDivideUnchecked x86 256))
500 (nat-to-byte (naturalModuloUnchecked x86 256)))))
501
502def aarch64SystemCallTranslateAssembly : (family AArch64Assembly) =
503 (eliminate
504 AArch64SystemCallTable
505 (lambda unrestricted current : (family AArch64SystemCallTable) . (family AArch64Assembly))
506 aarch64SystemCallTable
507 (branch
508 AArch64SystemCallTableEnd
509 .
510 (nprtMovNegativeOne
511 nprtX0
512 (nprtEmit nprtRet (constructor AArch64Assembly AArch64AssemblyEnd))))
513 (branch
514 AArch64SystemCallTableNext
515 key
516 form
517 rest
518 induction
519 .
520 (eliminate
521 AArch64SystemCallForm
522 (lambda unrestricted current : (family AArch64SystemCallForm) . (family AArch64Assembly))
523 form
524 (branch AArch64SystemCallAbsent . induction)
525 (branch
526 AArch64SystemCallSame
527 target
528 .
529 (nprtEmit
530 (nprtCmpImm nprtX0 key)
531 (nprtBIf
532 nprtNotEqual
533 (ahlTranslateLabel key)
534 (nprtEmit
535 (nprtMovz nprtX0 target)
536 (nprtEmit nprtRet (nprtLabel (ahlTranslateLabel key) induction))))))
537 (branch AArch64SystemCallDup3 target . induction)
538 (branch AArch64SystemCallUnlinkat target . induction)
539 (branch AArch64SystemCallRenameat2 target . induction)
540 (branch AArch64SystemCallOpenat target . induction))))
541
542def aarch64SystemCallTranslateRoutine : Bytes =
543 (eliminate
544 AArch64AssemblyResult
545 (lambda unrestricted current : (family AArch64AssemblyResult) . Bytes)
546 (aarch64Assemble aarch64SystemCallTranslateAssembly)
547 (branch AArch64AssemblyEncoded code . code)
548 (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
549 (branch AArch64AssemblyMissingLabel name . b"")
550 (branch AArch64AssemblyDisplacementOutOfRange name . b"")
551 (branch AArch64AssemblyOperandRefused value . b""))
552
553-- translate the number into `slot`, then call through it
554def ahlTranslatedSystemCall =
555 (lambda unrestricted slot : Nat .
556 (lambda unrestricted number : (family NativePhysicalOperand) .
557 (lambda unrestricted arguments : (family NativePhysicalArguments) .
558 (lambda unrestricted payload : Bytes .
559 (lambda unrestricted result : (family NativePhysicalResultBinding) .
560 (let unrestricted slotOf =
561 (constructor
562 NativePhysicalSlot
563 NativePhysicalSlotValue
564 (modelWord64FromNaturalTruncated slot))
565 in
566 (constructor
567 AArch64HostOperation
568 AArch64HostOperationLoweredPair
569 (constructor
570 NativePhysicalOperation
571 NativePhysicalMachineRoutine
572 aarch64SystemCallTranslateRoutine
573 (constructor
574 NativePhysicalArguments
575 NativePhysicalArgumentsValue
576 number
577 (ahlImm 0)
578 (ahlImm 0)
579 (ahlImm 0)
580 (ahlImm 0)
581 (ahlImm 0))
582 (constructor NativePhysicalResultBinding NativePhysicalStoreResult slotOf))
583 (constructor
584 NativePhysicalOperation
585 NativePhysicalSystemCall
586 (constructor NativePhysicalOperand NativePhysicalResultValue slotOf)
587 arguments
588 payload
589 result))))))))
590
591-- ---- routines ----
592-- Each x86-64 routine a plan host carries, with its AArch64 twin.
593-- Each twin realizes the same admitted semantic/ABI contract. Shared algorithms
594-- use Platform.AArch64.RoutineEmitter; memory, arithmetic and connected stream
595-- routines implement their target-local contracts with typed AArch64 assembly.
596def aarch64HostRoutines : (family AArch64HostRoutines) =
597 (constructor
598 AArch64HostRoutines
599 AArch64HostRoutinesNext
600 phPublishCode
601 aarch64Publish32Routine
602 (constructor
603 AArch64HostRoutines
604 AArch64HostRoutinesNext
605 nativeTelemetrySealRoutine
606 aarch64TelemetrySealRoutine
607 (constructor
608 AArch64HostRoutines
609 AArch64HostRoutinesNext
610 nativeLaunchRecipeRoutineBytes
611 aarch64LaunchRecipeRoutine
612 (constructor
613 AArch64HostRoutines
614 AArch64HostRoutinesNext
615 nativeCyclicRecordOffsetRoutine
616 aarch64CyclicRecordOffsetRoutine
617 (constructor
618 AArch64HostRoutines
619 AArch64HostRoutinesNext
620 nativeWordDigestRoutine
621 aarch64WordDigestRoutine
622 (constructor
623 AArch64HostRoutines
624 AArch64HostRoutinesNext
625 nativeByteDigestRoutine
626 aarch64ByteDigestRoutine
627 (constructor
628 AArch64HostRoutines
629 AArch64HostRoutinesNext
630 nvidiaCardInfoGPUIdCode
631 aarch64CardInfoCode
632 (constructor
633 AArch64HostRoutines
634 AArch64HostRoutinesNext
635 nativeDescriptorStatusCode
636 aarch64DescriptorCode
637 (constructor
638 AArch64HostRoutines
639 AArch64HostRoutinesNext
640 nativeFloat64FiniteCode
641 aarch64Float64FiniteCode
642 (constructor
643 AArch64HostRoutines
644 AArch64HostRoutinesNext
645 nativeMemoryCopyCode
646 aarch64MemoryCopyCode
647 (constructor
648 AArch64HostRoutines
649 AArch64HostRoutinesNext
650 nativeMemoryEqualCode
651 aarch64MemoryEqualCode
652 (constructor
653 AArch64HostRoutines
654 AArch64HostRoutinesNext
655 nativeCheckedWordAddCode
656 aarch64CheckedWordAddCode
657 (constructor
658 AArch64HostRoutines
659 AArch64HostRoutinesNext
660 nativeSocketReadCode
661 aarch64SocketReadCode
662 (constructor
663 AArch64HostRoutines
664 AArch64HostRoutinesNext
665 nativeSocketWriteCode
666 aarch64SocketWriteCode
667 (constructor
668 AArch64HostRoutines
669 AArch64HostRoutinesNext
670 nativeSocketConnectCode
671 aarch64SocketConnectCode
672 (constructor
673 AArch64HostRoutines
674 AArch64HostRoutinesNext
675 nativeSocketAcceptCode
676 aarch64SocketAcceptCode
677 (constructor
678 AArch64HostRoutines
679 AArch64HostRoutinesNext
680 nativeWordDigestContinueRoutine
681 aarch64WordDigestContinueRoutine
682 (constructor
683 AArch64HostRoutines
684 AArch64HostRoutinesNext
685 nativeByteDigestStreamStartRoutine
686 aarch64ByteDigestStreamStartRoutine
687 (constructor
688 AArch64HostRoutines
689 AArch64HostRoutinesNext
690 nativeByteDigestStreamFinishRoutine
691 aarch64ByteDigestStreamFinishRoutine
692 (constructor AArch64HostRoutines AArch64HostRoutinesEnd))))))))))))))))))))
693
694def ahlRoutine =
695 (lambda unrestricted code : Bytes .
696 (lambda unrestricted arguments : (family NativePhysicalArguments) .
697 (lambda unrestricted result : (family NativePhysicalResultBinding) .
698 (eliminate
699 AArch64HostRoutines
700 (lambda unrestricted current : (family AArch64HostRoutines) .
701 (family AArch64HostOperation))
702 aarch64HostRoutines
703 (branch AArch64HostRoutinesEnd . (ahlRefuse b"aarch64-host-routine-without-twin"))
704 (branch
705 AArch64HostRoutinesNext
706 x86
707 twin
708 rest
709 induction
710 .
711 (nat-eliminate
712 (lambda unrestricted current : Nat . (family AArch64HostOperation))
713 induction
714 (lambda unrestricted predecessor : Nat .
715 (lambda unrestricted ignored : (family AArch64HostOperation) .
716 (ahlLowered
717 (constructor
718 NativePhysicalOperation
719 NativePhysicalMachineRoutine
720 twin
721 arguments
722 result))))
723 (bytes-equal x86 code)))))))
724
725def aarch64LowerOperation =
726 (lambda unrestricted translateSlot : Nat .
727 (lambda unrestricted operation : (family NativePhysicalOperation) .
728 (eliminate
729 NativePhysicalOperation
730 (lambda unrestricted current : (family NativePhysicalOperation) .
731 (family AArch64HostOperation))
732 operation
733 (branch
734 NativePhysicalSystemCall
735 number
736 arguments
737 payload
738 result
739 .
740 (ahlImmediateOr
741 number
742 (lambda unrestricted value : Nat . (ahlSystemCall value arguments payload result))
743 (ahlTranslatedSystemCall translateSlot number arguments payload result)))
744 (branch
745 NativePhysicalCopyPayloadToState
746 destination
747 extent
748 payload
749 .
750 (ahlLowered operation))
751 (branch
752 NativePhysicalMachineRoutine
753 code
754 arguments
755 result
756 .
757 (ahlRoutine code arguments result))
758 (branch NativePhysicalFencePoll address expected polls . (ahlLowered operation))
759 (branch NativePhysicalTelemetryAppend path record . (ahlLowered operation))
760 (branch NativePhysicalAssertEqual left right error . (ahlLowered operation))
761 (branch NativePhysicalAssertOneOf observed first second error . (ahlLowered operation))
762 (branch NativePhysicalHaltSuccess . (ahlLowered operation))
763 (branch NativePhysicalRepeatBegin count . (ahlLowered operation))
764 (branch NativePhysicalSkipUnlessEqual left right count . (ahlLowered operation))
765 (branch NativePhysicalRepeatEnd . (ahlLowered operation))
766 (branch
767 NativePhysicalRepeatEndWhen
768 observed
769 expected
770 .
771 (ahlRefuse b"aarch64-repeat-end-when-unavailable"))
772 (branch NativePhysicalStoreWord64 destination value . (ahlLowered operation))
773 (branch NativePhysicalFenceWait address expected polls interval . (ahlLowered operation))
774 (branch NativePhysicalRepeatBeginCounted count . (ahlLowered operation))
775 (branch NativePhysicalAddWord64 destination left right . (ahlLowered operation))
776 (branch NativePhysicalFloat64 kind destination left right . (ahlLowered operation)))))
777
778-- Lowering may expand one source operation into two commands (a dynamic
779-- syscall number is translated before the syscall). Relative branches refer
780-- to source records, so their distances must be derived again from the emitted
781-- prefix. Validate the source window first: truncating an invalid source skip
782-- to the available suffix would silently admit a malformed source program.
783def aarch64LoweredWindowCount =
784 (lambda unrestricted translateSlot : Nat .
785 (lambda unrestricted commands : (family NativePhysicalCommands) .
786 (eliminate
787 NativePhysicalCommands
788 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
789 commands
790 (branch NativePhysicalCommandsEnd . 0)
791 (branch
792 NativePhysicalCommandsNext
793 head
794 rest
795 induction
796 .
797 (naturalAdd
798 (eliminate
799 NativePhysicalCommand
800 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
801 head
802 (branch
803 NativePhysicalCommandValue
804 operation
805 identity
806 .
807 (eliminate
808 AArch64HostOperation
809 (lambda unrestricted current : (family AArch64HostOperation) . Nat)
810 (aarch64LowerOperation translateSlot operation)
811 (branch AArch64HostOperationLowered value . 1)
812 (branch AArch64HostOperationRefused reason . 0)
813 (branch AArch64HostOperationLoweredPair first second . 2))))
814 induction)))))
815
816def aarch64LowerCommandOperation =
817 (lambda unrestricted translateSlot : Nat .
818 (lambda unrestricted remaining : (family NativePhysicalCommands) .
819 (lambda unrestricted operation : (family NativePhysicalOperation) .
820 (let unrestricted lowered =
821 (aarch64LowerOperation translateSlot operation)
822 in
823 (eliminate
824 NativePhysicalOperation
825 (lambda unrestricted current : (family NativePhysicalOperation) .
826 (family AArch64HostOperation))
827 operation
828 (branch NativePhysicalSystemCall field0 field1 field2 field3 . lowered)
829 (branch NativePhysicalCopyPayloadToState field0 field1 field2 . lowered)
830 (branch NativePhysicalMachineRoutine field0 field1 field2 . lowered)
831 (branch NativePhysicalFencePoll field0 field1 field2 . lowered)
832 (branch NativePhysicalTelemetryAppend field0 field1 . lowered)
833 (branch NativePhysicalAssertEqual field0 field1 field2 . lowered)
834 (branch NativePhysicalAssertOneOf field0 field1 field2 field3 . lowered)
835 (branch NativePhysicalHaltSuccess . lowered)
836 (branch NativePhysicalRepeatBegin field0 . lowered)
837 (branch
838 NativePhysicalSkipUnlessEqual
839 field0
840 field1
841 field2
842 .
843 (nat-eliminate
844 (lambda unrestricted flag : Nat . (family AArch64HostOperation))
845 (ahlRefuse b"aarch64-host-branch-target-invalid")
846 (lambda unrestricted prior : Nat .
847 (lambda unrestricted ignored : (family AArch64HostOperation) .
848 (ahlLowered
849 (constructor
850 NativePhysicalOperation
851 NativePhysicalSkipUnlessEqual
852 field0
853 field1
854 (modelWord64FromNaturalTruncated
855 (aarch64LoweredWindowCount
856 translateSlot
857 (nativePhysicalCommandsTake remaining (modelWord64Natural field2))))))))
858 (nativePhysicalBranchWindowValid field2 remaining)))
859 (branch NativePhysicalRepeatEnd . lowered)
860 (branch NativePhysicalRepeatEndWhen field0 field1 . lowered)
861 (branch NativePhysicalStoreWord64 field0 field1 . lowered)
862 (branch NativePhysicalFenceWait field0 field1 field2 field3 . lowered)
863 (branch NativePhysicalRepeatBeginCounted field0 . lowered)
864 (branch NativePhysicalAddWord64 field0 field1 field2 . lowered)
865 (branch NativePhysicalFloat64 field0 field1 field2 field3 . lowered))))))
866
867-- the commands lowered in order; a refusal names the first refused command
868def aarch64LowerCommands =
869 (lambda unrestricted translateSlot : Nat .
870 (lambda unrestricted commands : (family NativePhysicalCommands) .
871 (app
872 (eliminate
873 NativePhysicalCommands
874 (lambda unrestricted current : (family NativePhysicalCommands) .
875 (pi unrestricted index : Nat . (family AArch64HostCommands)))
876 commands
877 (branch
878 NativePhysicalCommandsEnd
879 .
880 (lambda unrestricted index : Nat .
881 (constructor
882 AArch64HostCommands
883 AArch64HostCommandsLowered
884 (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
885 (branch
886 NativePhysicalCommandsNext
887 head
888 tail
889 induction
890 .
891 (lambda unrestricted index : Nat .
892 (eliminate
893 NativePhysicalCommand
894 (lambda unrestricted current : (family NativePhysicalCommand) .
895 (family AArch64HostCommands))
896 head
897 (branch
898 NativePhysicalCommandValue
899 operation
900 identity
901 .
902 (eliminate
903 AArch64HostOperation
904 (lambda unrestricted current : (family AArch64HostOperation) .
905 (family AArch64HostCommands))
906 (aarch64LowerCommandOperation translateSlot tail operation)
907 (branch
908 AArch64HostOperationLowered
909 lowered
910 .
911 (eliminate
912 AArch64HostCommands
913 (lambda unrestricted current : (family AArch64HostCommands) .
914 (family AArch64HostCommands))
915 (induction (succ index))
916 (branch
917 AArch64HostCommandsLowered
918 rest
919 .
920 (constructor
921 AArch64HostCommands
922 AArch64HostCommandsLowered
923 (constructor
924 NativePhysicalCommands
925 NativePhysicalCommandsNext
926 (constructor
927 NativePhysicalCommand
928 NativePhysicalCommandValue
929 lowered
930 identity)
931 rest)))
932 (branch
933 AArch64HostCommandsRefused
934 reason
935 at
936 .
937 (constructor AArch64HostCommands AArch64HostCommandsRefused reason at))))
938 (branch
939 AArch64HostOperationRefused
940 reason
941 .
942 (constructor AArch64HostCommands AArch64HostCommandsRefused reason index))
943 (branch
944 AArch64HostOperationLoweredPair
945 first
946 second
947 .
948 (eliminate
949 AArch64HostCommands
950 (lambda unrestricted current : (family AArch64HostCommands) .
951 (family AArch64HostCommands))
952 (induction (succ index))
953 (branch
954 AArch64HostCommandsLowered
955 rest
956 .
957 (constructor
958 AArch64HostCommands
959 AArch64HostCommandsLowered
960 (constructor
961 NativePhysicalCommands
962 NativePhysicalCommandsNext
963 (constructor
964 NativePhysicalCommand
965 NativePhysicalCommandValue
966 first
967 identity)
968 (constructor
969 NativePhysicalCommands
970 NativePhysicalCommandsNext
971 (constructor
972 NativePhysicalCommand
973 NativePhysicalCommandValue
974 second
975 identity)
976 rest))))
977 (branch
978 AArch64HostCommandsRefused
979 reason
980 at
981 .
982 (constructor AArch64HostCommands AArch64HostCommandsRefused reason at))))))))))
983 zero)))
984
985-- ---- routine alignment ----
986--
987-- A MachineRoutine's code runs in place, at its record + 232, and A64
988-- fetches instructions only from 4-byte aligned addresses; a copy's payload,
989-- an assertion's error code and a telemetry record have observable lengths
990-- that need not be words. The image format this host is encoded in,
991-- NativePhysicalImageAlignedV3 (Runtime.NativePhysicalImagePlan), places
992-- every record on an aligned boundary, and the runtime refuses any other
993-- format (exit 101).
994def ahlCommandCount =
995 (lambda unrestricted commands : (family NativePhysicalCommands) .
996 (eliminate
997 NativePhysicalCommands
998 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
999 commands
1000 (branch NativePhysicalCommandsEnd . zero)
1001 (branch NativePhysicalCommandsNext head tail induction . (succ induction))))
1002
1003def aarch64LowerHostProgram =
1004 (lambda unrestricted program : (family NativePhysicalProgram) .
1005 (eliminate
1006 NativePhysicalProgram
1007 (lambda unrestricted current : (family NativePhysicalProgram) . (family AArch64HostLowering))
1008 program
1009 (branch
1010 NativePhysicalProgramValue
1011 stateExtent
1012 slots
1013 commands
1014 expected
1015 identity
1016 fallbacks
1017 .
1018 (eliminate
1019 AArch64HostCommands
1020 (lambda unrestricted current : (family AArch64HostCommands) .
1021 (family AArch64HostLowering))
1022 (aarch64LowerCommands (modelWord64Natural slots) commands)
1023 -- the program's slots plus the one a translated system call's number
1024 -- is written to; a translated call is two commands, so the count is
1025 -- the lowered program's. Routine code is placed on instruction
1026 -- boundaries by the image format (NativePhysicalImageAlignedV3),
1027 -- which the AArch64 runtime requires.
1028 (branch
1029 AArch64HostCommandsLowered
1030 lowered
1031 .
1032 (constructor
1033 AArch64HostLowering
1034 AArch64HostLowered
1035 (constructor
1036 NativePhysicalProgram
1037 NativePhysicalProgramValue
1038 stateExtent
1039 (modelWord64FromNaturalTruncated (succ (modelWord64Natural slots)))
1040 lowered
1041 (ahlCommandCount lowered)
1042 identity
1043 fallbacks)))
1044 (branch
1045 AArch64HostCommandsRefused
1046 reason
1047 index
1048 .
1049 (constructor AArch64HostLowering AArch64HostRefused reason index))))))
1050
1051-- The AArch64 runtime's machine code, assembled once.
1052def aarch64HostRuntimeBytes : Bytes =
1053 (eliminate
1054 AArch64AssemblyResult
1055 (lambda unrestricted current : (family AArch64AssemblyResult) . Bytes)
1056 aarch64NativePhysicalRuntime
1057 (branch AArch64AssemblyEncoded code . code)
1058 (branch AArch64AssemblyEncodeDuplicateLabel name . b"")
1059 (branch AArch64AssemblyMissingLabel name . b"")
1060 (branch AArch64AssemblyDisplacementOutOfRange name . b"")
1061 (branch AArch64AssemblyOperandRefused value . b""))
1062
1063-- The x86-64 host program as an AArch64 executable: the program lowered, its
1064-- image after the AArch64 runtime, in Compiler.ELF's container. A refusal is
1065-- the empty value, which the direct artifact writer rejects as a non-ELF --
1066-- fail-closed, as Runtime.NativePhysicalNativeELF's direct path is.
1067def aarch64HostELFBytes =
1068 (lambda unrestricted program : (family NativePhysicalProgram) .
1069 (eliminate
1070 AArch64HostLowering
1071 (lambda unrestricted current : (family AArch64HostLowering) . Bytes)
1072 (aarch64LowerHostProgram program)
1073 (branch
1074 AArch64HostLowered
1075 lowered
1076 .
1077 (aarch64WrapMachineCodeSparseLarge
1078 (bytes-append
1079 aarch64HostRuntimeBytes
1080 (compiler-native-encode
1081 (family NativePhysicalImagePlan)
1082 (constructor
1083 NativePhysicalImagePlan
1084 NativePhysicalImagePlanValue
1085 (constructor NativePhysicalImageFormat NativePhysicalImageAlignedV3)
1086 lowered)))))
1087 (branch AArch64HostRefused reason index . b"")))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.