Large source region · 2,191 lines
module Platform.AArch64.NativePhysicalRuntime
import Runtime.NativePhysicalImage
import Runtime.NativePhysicalMemory
import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Data.Bytes
import Model.Config
import Model.Word32
import Std.Byte
import Std.Natural
-- The AArch64 Linux twin of Runtime.NativePhysicalNative: one fixed program
-- that interprets an ALPXPHY3 command image appended after its code. The V3
-- layout aligns every record; see Runtime.NativePhysicalImagePlan. V2's packed
-- records can put an inline routine at an unaligned instruction address even
-- when syscall payloads are padded. This reader explicitly rejects that format.
-- Block for block it is the x86-64 runtime, under this register map:
--
-- x86-64 A64 role
-- RAX x6 accumulator, resolver result
-- RDI RSI RDX x0 x1 x2 system-call arguments 0-2
-- RCX/R10 R8 R9 x3 x4 x5 system-call arguments 3-5 (x86 moves RCX to R10; A64 needs no move)
-- R10 R11 x9 x10 temporaries
-- R12 R13 R14 R15 x12 x13 x14 x15 image end, remaining commands, command pointer, image base
-- RBX RBP x19 x20 result-slot base, mapped state base
-- - x21 the process entry stack pointer (argc, argv)
-- - x11 the resolver's address, for blr
-- [rsp-248/-240/-232] [sp,#8] [sp,#16] [sp,#24] in a derived aligned frame
--
-- The system-call number travels in x8 and the result returns in x0; the
-- runtime's own calls use the asm-generic numbers (mmap 222, openat 56,
-- write 64, fsync 82, close 57, munmap 215, exit_group 94, exit 93). The
-- numbers a program's commands carry are the program's data, so an A64
-- program supplies A64 numbers. Calls into the resolver and into machine
-- routines use blr/ret through x30; the runtime itself never returns.
def nprtX0 : (family AArch64Register) =
(constructor AArch64Register AArch64X0)
def nprtX1 : (family AArch64Register) =
(constructor AArch64Register AArch64X1)
def nprtX2 : (family AArch64Register) =
(constructor AArch64Register AArch64X2)
def nprtX3 : (family AArch64Register) =
(constructor AArch64Register AArch64X3)
def nprtX4 : (family AArch64Register) =
(constructor AArch64Register AArch64X4)
def nprtX5 : (family AArch64Register) =
(constructor AArch64Register AArch64X5)
def nprtX6 : (family AArch64Register) =
(constructor AArch64Register AArch64X6)
def nprtX7 : (family AArch64Register) =
(constructor AArch64Register AArch64X7)
def nprtX8 : (family AArch64Register) =
(constructor AArch64Register AArch64X8)
def nprtX9 : (family AArch64Register) =
(constructor AArch64Register AArch64X9)
def nprtX10 : (family AArch64Register) =
(constructor AArch64Register AArch64X10)
def nprtX11 : (family AArch64Register) =
(constructor AArch64Register AArch64X11)
def nprtX12 : (family AArch64Register) =
(constructor AArch64Register AArch64X12)
def nprtX13 : (family AArch64Register) =
(constructor AArch64Register AArch64X13)
def nprtX14 : (family AArch64Register) =
(constructor AArch64Register AArch64X14)
def nprtX15 : (family AArch64Register) =
(constructor AArch64Register AArch64X15)
def nprtX19 : (family AArch64Register) =
(constructor AArch64Register AArch64X19)
def nprtX20 : (family AArch64Register) =
(constructor AArch64Register AArch64X20)
def nprtX21 : (family AArch64Register) =
(constructor AArch64Register AArch64X21)
def nprtShift0 : (family AArch64HalfwordShift) =
(constructor AArch64HalfwordShift AArch64Shift0)
def nprtEqual : (family AArch64Condition) =
(constructor AArch64Condition AArch64Equal)
def nprtNotEqual : (family AArch64Condition) =
(constructor AArch64Condition AArch64NotEqual)
def nprtMinus : (family AArch64Condition) =
(constructor AArch64Condition AArch64Minus)
def nprtBelow : (family AArch64Condition) =
(constructor AArch64Condition AArch64CarryClear)
def nprtAbove : (family AArch64Condition) =
(constructor AArch64Condition AArch64UnsignedHigher)
-- Frame slots standing in for the x86 runtime's [rsp-248], [rsp-240], [rsp-232].
def nprtSlotA : Nat =
8
def nprtSlotB : Nat =
16
def nprtSlotC : Nat =
24
-- x12-x15 carry live VM state but are volatile in AAPCS64. Save them at
-- the caller boundary around every user routine. Depending on an incidental
-- routine register allocation corrupts the image cursor after a legal call.
-- These slots follow the existing temporary slots in the VM's private frame.
def nprtStackWordBytes =
(bytes-length (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))
def nprtSaveImageEnd =
(naturalAdd nprtSlotC nprtStackWordBytes)
def nprtSaveRemaining =
(naturalAdd nprtSaveImageEnd nprtStackWordBytes)
def nprtSaveCommand =
(naturalAdd nprtSaveRemaining nprtStackWordBytes)
def nprtSaveImage =
(naturalAdd nprtSaveCommand nprtStackWordBytes)
def nprtStackBytes =
(naturalMultiply
16
(naturalDivideUnchecked (naturalAdd 15 (naturalAdd nprtSaveImage nprtStackWordBytes)) 16))
-- Labels.
def nprtLabelEntry : Bytes =
b"np-entry"
def nprtLabelLoop : Bytes =
b"np-loop"
def nprtLabelDone : Bytes =
b"np-done"
def nprtLabelAdvance : Bytes =
b"np-advance"
def nprtLabelResolve : Bytes =
b"np-resolve"
def nprtLabelResolveImmediate : Bytes =
b"np-res-imm"
def nprtLabelResolveResult : Bytes =
b"np-res-res"
def nprtLabelResolveResultAddress : Bytes =
b"np-res-raddr"
def nprtLabelResolveStateAddress : Bytes =
b"np-res-saddr"
def nprtLabelResolveStateLoad : Bytes =
b"np-res-sload"
def nprtLabelResolvePayloadAddress : Bytes =
b"np-res-paddr"
def nprtLabelResolvePayloadLoad : Bytes =
b"np-res-pload"
def nprtLabelResolveProcessArgument : Bytes =
b"np-res-argv"
def nprtLabelResolveSlotValid : Bytes =
b"np-res-sv"
def nprtLabelResolveResultAddressSlotValid : Bytes =
b"np-res-rasv"
def nprtLabelResolveStateAddressValid : Bytes =
b"np-res-sav"
def nprtLabelResolveStateLoadValid : Bytes =
b"np-res-slv"
def nprtLabelResolvePayloadAddressValid : Bytes =
b"np-res-pav"
def nprtLabelResolvePayloadLoadValid : Bytes =
b"np-res-plv"
def nprtLabelDispatchSystemCall : Bytes =
b"np-syscall"
def nprtLabelDispatchCopy : Bytes =
b"np-copy"
def nprtLabelDispatchRoutine : Bytes =
b"np-routine"
def nprtLabelDispatchFence : Bytes =
b"np-fence"
def nprtLabelDispatchTelemetry : Bytes =
b"np-telemetry"
def nprtLabelDispatchAssert : Bytes =
b"np-assert"
def nprtLabelDispatchAssertOneOf : Bytes =
b"np-assert-one"
def nprtLabelDispatchHalt : Bytes =
b"np-halt"
def nprtLabelBindResult : Bytes =
b"np-bind"
def nprtLabelBindStore : Bytes =
b"np-bind-s"
def nprtLabelBindSlotValid : Bytes =
b"np-bind-sv"
def nprtLabelCopyLoop : Bytes =
b"np-copy-l"
def nprtLabelCopyDone : Bytes =
b"np-copy-d"
def nprtLabelFenceLoop : Bytes =
b"np-fence-l"
def nprtLabelFenceDone : Bytes =
b"np-fence-d"
def nprtLabelTelemetryCopyLoop : Bytes =
b"np-tel-cl"
def nprtLabelTelemetryWriteLoop : Bytes =
b"np-tel-wl"
def nprtLabelRecordExtentValid : Bytes =
b"np-rec-ev"
def nprtLabelRecordEndValid : Bytes =
b"np-rec-bv"
def nprtLabelFatalFormat : Bytes =
b"np-fatal-format"
def nprtLabelFatalBounds : Bytes =
b"np-fatal-bounds"
def nprtLabelFatalOperand : Bytes =
b"np-fatal-operand"
def nprtLabelFatalSystemCall : Bytes =
b"np-fatal-syscall"
def nprtLabelFatalAssertion : Bytes =
b"np-fatal-assert"
def nprtLabelFatalFence : Bytes =
b"np-fatal-fence"
def nprtLabelFatalTelemetry : Bytes =
b"np-fatal-tel"
def nprtLabelFatalRecord : Bytes =
b"np-fatal-record"
def nprtLabelCommandFailure : Bytes =
b"np-command-fail"
def nprtLabelExit : Bytes =
b"np-exit"
def nprtLabelImage : Bytes =
b"np-image"
-- Assembly item builders.
def nprtEmit =
(lambda unrestricted instruction : (family AArch64Instruction) .
(lambda unrestricted tail : (family AArch64Assembly) .
(constructor AArch64Assembly AArch64AssemblyEmit instruction tail)))
def nprtLabel =
(lambda unrestricted name : Bytes .
(lambda unrestricted tail : (family AArch64Assembly) .
(constructor AArch64Assembly AArch64AssemblyLabel name tail)))
def nprtB =
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family AArch64Assembly) .
(constructor AArch64Assembly AArch64AssemblyBranch target tail)))
def nprtBIf =
(lambda unrestricted condition : (family AArch64Condition) .
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family AArch64Assembly) .
(constructor AArch64Assembly AArch64AssemblyBranchIf condition target tail))))
def nprtAdr =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family AArch64Assembly) .
(constructor AArch64Assembly AArch64AssemblyAddressOf destination target tail))))
-- Instructions. `nprtCompare a b` is the x86 runtime's `Compare a b`, which
-- computes b - a: on A64 that is `cmp b, a`, so Below means b < a unsigned.
def nprtMovz =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted value : Nat .
(constructor AArch64Instruction AArch64MoveWideZero destination value nprtShift0)))
def nprtMov =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted source : (family AArch64Register) .
(constructor AArch64Instruction AArch64MoveRegister destination source)))
def nprtAdd =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted source : (family AArch64Register) .
(constructor AArch64Instruction AArch64AddRegister destination destination source)))
def nprtSub =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted source : (family AArch64Register) .
(constructor AArch64Instruction AArch64SubtractRegister destination destination source)))
def nprtAddImm =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted value : Nat .
(constructor AArch64Instruction AArch64AddImmediate destination destination value)))
def nprtSubImm =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted value : Nat .
(constructor AArch64Instruction AArch64SubtractImmediate destination destination value)))
def nprtCompare =
(lambda unrestricted a : (family AArch64Register) .
(lambda unrestricted b : (family AArch64Register) .
(constructor AArch64Instruction AArch64CompareRegister b a)))
def nprtCmpImm =
(lambda unrestricted register : (family AArch64Register) .
(lambda unrestricted value : Nat .
(constructor AArch64Instruction AArch64CompareImmediate register value)))
def nprtTest =
(lambda unrestricted register : (family AArch64Register) .
(constructor AArch64Instruction AArch64CompareImmediate register 0))
def nprtLsl =
(lambda unrestricted register : (family AArch64Register) .
(lambda unrestricted amount : Nat .
(constructor AArch64Instruction AArch64ShiftLeftImmediate register register amount)))
def nprtLdr =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted base : (family AArch64Register) .
(lambda unrestricted offset : Nat .
(constructor AArch64Instruction AArch64LoadMemory64 destination base offset))))
def nprtStr =
(lambda unrestricted base : (family AArch64Register) .
(lambda unrestricted offset : Nat .
(lambda unrestricted source : (family AArch64Register) .
(constructor AArch64Instruction AArch64StoreMemory64 base offset source))))
def nprtLdrb =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted base : (family AArch64Register) .
(constructor AArch64Instruction AArch64LoadMemory8ZeroExtend destination base 0)))
def nprtStrb =
(lambda unrestricted base : (family AArch64Register) .
(lambda unrestricted source : (family AArch64Register) .
(constructor AArch64Instruction AArch64StoreMemory8 base 0 source)))
def nprtLdrSlot =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted slot : Nat .
(constructor AArch64Instruction AArch64LoadMemory64FromStack destination slot)))
def nprtStrSlot =
(lambda unrestricted slot : Nat .
(lambda unrestricted source : (family AArch64Register) .
(constructor AArch64Instruction AArch64StoreMemory64ToStack slot source)))
def nprtSvc : (family AArch64Instruction) =
(constructor AArch64Instruction AArch64SupervisorCall)
def nprtRet : (family AArch64Instruction) =
(constructor AArch64Instruction AArch64Return)
def nprtBlr =
(lambda unrestricted target : (family AArch64Register) .
(constructor AArch64Instruction AArch64BranchLinkRegister target))
-- A 64-bit constant from eight little-endian bytes: movz then three movk.
def nprtHalf =
(lambda unrestricted low : Byte .
(lambda unrestricted high : Byte .
(naturalAdd (byte-to-nat low) (naturalMultiply 256 (byte-to-nat high)))))
def nprtMovImm64 =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted b0 : Byte .
(lambda unrestricted b1 : Byte .
(lambda unrestricted b2 : Byte .
(lambda unrestricted b3 : Byte .
(lambda unrestricted b4 : Byte .
(lambda unrestricted b5 : Byte .
(lambda unrestricted b6 : Byte .
(lambda unrestricted b7 : Byte .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
(constructor
AArch64Instruction
AArch64MoveWideZero
destination
(nprtHalf b0 b1)
nprtShift0)
(nprtEmit
(constructor
AArch64Instruction
AArch64MoveWideKeep
destination
(nprtHalf b2 b3)
(constructor AArch64HalfwordShift AArch64Shift16))
(nprtEmit
(constructor
AArch64Instruction
AArch64MoveWideKeep
destination
(nprtHalf b4 b5)
(constructor AArch64HalfwordShift AArch64Shift32))
(nprtEmit
(constructor
AArch64Instruction
AArch64MoveWideKeep
destination
(nprtHalf b6 b7)
(constructor AArch64HalfwordShift AArch64Shift48))
tail))))))))))))))
def nprtMovNegativeOne =
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtMovImm64
destination
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
tail)))
-- The system call with the given asm-generic number: movz x8, svc.
def nprtSyscall =
(lambda unrestricted number : Nat .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit (nprtMovz nprtX8 number) (nprtEmit nprtSvc tail))))
-- Resolve the operand descriptor at [x14 + offset] into a register:
-- x0 = x14 + offset ; adr x11, resolve ; blr x11 ; mov dest, x6.
def nprtResolveCall =
(lambda unrestricted descriptorOffset : Nat .
(lambda unrestricted destination : (family AArch64Register) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
(nprtMov nprtX0 nprtX14)
(nprtEmit
(nprtAddImm nprtX0 descriptorOffset)
(nprtAdr
nprtX11
nprtLabelResolve
(nprtEmit (nprtBlr nprtX11) (nprtEmit (nprtMov destination nprtX6) tail))))))))
-- Exit with the code in x0.
def nprtExitWith =
(lambda unrestricted code : Nat .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit (nprtMovz nprtX0 code) (nprtB nprtLabelExit tail))))
-- ---------------------------------------------------------------------------
-- The commands Runtime.NativePhysicalNative gained after this twin was
-- written (Repeat, StoreWord64, the LoopAffine operand, FenceWait, AddWord64
-- and the Float64 family), block for block under the same register map. The
-- resolver scratches x6, x9 and x10 and reads x0, and `svc` returns in x0, so
-- x1 .. x5 carry values across a resolve and a system call.
def nprtLabelDispatchSkip : Bytes =
b"np-skip"
def nprtLabelDispatchRepeatBegin : Bytes =
b"np-repeat-begin"
def nprtLabelDispatchRepeatEnd : Bytes =
b"np-repeat-end"
def nprtLabelDispatchStore : Bytes =
b"np-store"
def nprtLabelDispatchAdd : Bytes =
b"np-add"
def nprtLabelDispatchFloat64 : Bytes =
b"np-float64-"
def nprtLabelDispatchFenceWait : Bytes =
b"np-fence-wait"
def nprtLabelFenceWaitLoop : Bytes =
b"np-fence-wait-l"
def nprtLabelFenceWaitDone : Bytes =
b"np-fence-wait-d"
def nprtLabelRepeatScan : Bytes =
b"np-repeat-scan"
def nprtLabelRepeatScanNext : Bytes =
b"np-repeat-scan-n"
def nprtLabelRepeatFound : Bytes =
b"np-repeat-found"
def nprtLabelRepeatAgain : Bytes =
b"np-repeat-again"
def nprtLabelResolveLoopAffine : Bytes =
b"np-res-affine"
def nprtLabelResolveLoopAffineStep : Bytes =
b"np-res-affine-s"
def nprtLabelResolveLoopAffineDone : Bytes =
b"np-res-affine-d"
-- the scratch after the result slots: [+0] repeat iteration, [+8] count,
-- [+16] first body record, [+24] body record count, [+32] a timespec
-- (seconds, nanoseconds) for the fence wait's nanosleep
def nprtScratchBytes : Nat =
nativePhysicalMemoryScratchBytes
-- argv[0]'s offset from the entry stack pointer x21 holds ([sp] is argc).
-- The x86 runtime reads [rsp + 16] because its resolver runs one call deep,
-- with the return address on the stack; x21 is the entry value itself.
def nprtArgvOffset : Nat =
8
-- the asm-generic nanosleep
def nprtNanosleep : Nat =
101
def nprtD0 : (family AArch64FloatRegister) =
(constructor AArch64FloatRegister AArch64S0)
def nprtD1 : (family AArch64FloatRegister) =
(constructor AArch64FloatRegister AArch64S1)
-- in the command dispatch: `tag` to `target`
def nprtDispatchTag =
(lambda unrestricted tag : Nat .
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit (nprtCmpImm nprtX6 tag) (nprtBIf nprtEqual target tail)))))
-- in the resolver's dispatch: operand kind `kind` to `target`
def nprtDispatchKind =
(lambda unrestricted kind : Nat .
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit (nprtCmpImm nprtX9 kind) (nprtBIf nprtEqual target tail)))))
-- the scratch's address, x19 + 8 * resultSlots, into `register`
def nprtScratchInto =
(lambda unrestricted register : (family AArch64Register) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
(nprtLdr register nprtX15 32)
(nprtEmit (nprtLsl register 3) (nprtEmit (nprtAdd register nprtX19) tail)))))
-- RepeatBegin (tag 9): iteration 0, the count from operand 0, the first body
-- record, and the number of body records found by scanning forward to the
-- matching RepeatEnd (tag 10). A nested RepeatBegin or running off the image
-- is a malformed record. A count of zero skips the body.
-- Shared by repeat search and branch skipping. Extents are checked before
-- reading or advancing, including the V3 alignment/padding contract.
def nprtScanRecord =
(lambda unrestricted pointer : (family AArch64Register) .
(lambda unrestricted extent : (family AArch64Register) .
(lambda unrestricted scratch : (family AArch64Register) .
(lambda unrestricted field : (family AArch64Register) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
(nprtCompare pointer nprtX12)
(nprtBIf
nprtBelow
nprtLabelFatalBounds
(nprtEmit
(nprtMov scratch nprtX12)
(nprtEmit
(nprtSub scratch pointer)
(nprtEmit
(nprtCmpImm scratch nativePhysicalImageCommandFixedBytes)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtLdr extent pointer 8)
(nprtEmit
(nprtCmpImm extent nativePhysicalImageCommandFixedBytes)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtCompare extent scratch)
(nprtBIf
nprtBelow
nprtLabelFatalBounds
(nprtEmit
(nprtMovz
field
(naturalSaturatingSubtract
nativePhysicalImageRecordAlignment
1))
(nprtEmit
(constructor
AArch64Instruction
AArch64AndRegister
field
extent
field)
(nprtEmit
(nprtCmpImm field 0)
(nprtBIf
nprtNotEqual
nprtLabelFatalRecord
(nprtEmit
(nprtMov scratch extent)
(nprtEmit
(nprtSubImm scratch nativePhysicalImageCommandFixedBytes)
(nprtEmit
(nprtLdr field pointer 32)
(nprtEmit
(nprtCompare field scratch)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtSub scratch field)
(nprtEmit
(nprtLdr field pointer 40)
(nprtEmit
(nprtCompare field scratch)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtSub scratch field)
(nprtEmit
(nprtLdr field pointer 48)
(nprtEmit
(nprtCompare field scratch)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtSub scratch field)
(nprtEmit
(nprtCmpImm
scratch
(naturalSaturatingSubtract
nativePhysicalImageRecordAlignment
1))
(nprtBIf
nprtAbove
nprtLabelFatalRecord
(nprtEmit
(nprtLdr field pointer 0)
(nprtEmit
(nprtCmpImm field 1)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtCmpImm field 23)
(nprtBIf nprtAbove nprtLabelFatalRecord tail)))))))))))))))))))))))))))))))))))))))))
-- X9 owns the loop-frame address and X10 its record count throughout this
-- scan. The record validator uses X0/X4/X5 so those live values survive.
def nprtRepeatBeginBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchRepeatBegin
(nprtResolveCall
64
nprtX6
(nprtScratchInto
nprtX9
(nprtEmit
(nprtStr nprtX9 8 nprtX6)
(nprtEmit
(nprtMovz nprtX10 0)
(nprtEmit
(nprtStr nprtX9 0 nprtX10)
(nprtEmit
(nprtLdr nprtX6 nprtX14 8)
(nprtEmit
(nprtAdd nprtX6 nprtX14)
(nprtEmit
(nprtStr nprtX9 16 nprtX6)
(nprtLabel
nprtLabelRepeatScan
(nprtScanRecord
nprtX6
nprtX0
nprtX4
nprtX5
(nprtEmit
(nprtCompare nprtX12 nprtX6)
(nprtBIf
nprtBelow
nprtLabelRepeatScanNext
(nprtB
nprtLabelFatalRecord
(nprtLabel
nprtLabelRepeatScanNext
(nprtEmit
(nprtLdr nprtX0 nprtX6 0)
(nprtEmit
(nprtCmpImm nprtX0 10)
(nprtBIf
nprtEqual
nprtLabelRepeatFound
(nprtEmit
(nprtCmpImm nprtX0 9)
(nprtBIf
nprtEqual
nprtLabelFatalRecord
(nprtEmit
(nprtAddImm nprtX10 1)
(nprtEmit
(nprtLdr nprtX0 nprtX6 8)
(nprtEmit
(nprtAdd nprtX6 nprtX0)
(nprtB
nprtLabelRepeatScan
(nprtLabel
nprtLabelRepeatFound
(nprtEmit
(nprtStr nprtX9 24 nprtX10)
(nprtEmit
(nprtLdr nprtX0 nprtX9 8)
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtNotEqual
nprtLabelAdvance
(nprtEmit
(nprtSub nprtX13 nprtX10)
(nprtEmit
(nprtSubImm nprtX13 1)
(nprtEmit
(nprtMov nprtX14 nprtX6)
(nprtB nprtLabelAdvance tail))))))))))))))))))))))))))))))))))
-- RepeatEnd (tag 10): one more iteration done; while iterations remain,
-- continue at the first body record with the body's records still to count,
-- otherwise advance past the end.
def nprtRepeatEndBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchRepeatEnd
(nprtScratchInto
nprtX9
(nprtEmit
(nprtLdr nprtX10 nprtX9 0)
(nprtEmit
(nprtAddImm nprtX10 1)
(nprtEmit
(nprtStr nprtX9 0 nprtX10)
(nprtEmit
(nprtLdr nprtX6 nprtX9 8)
(nprtEmit
(nprtCompare nprtX6 nprtX10)
(nprtBIf
nprtBelow
nprtLabelRepeatAgain
(nprtB
nprtLabelAdvance
(nprtLabel
nprtLabelRepeatAgain
(nprtEmit
(nprtLdr nprtX14 nprtX9 16)
(nprtEmit
(nprtLdr nprtX6 nprtX9 24)
(nprtEmit (nprtAdd nprtX13 nprtX6) (nprtB nprtLabelLoop tail)))))))))))))))
-- StoreWord64 (tag 11): the value of operand 1 into the address operand 0
-- resolves to.
def nprtStoreBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchStore
(nprtResolveCall
64
nprtX1
(nprtResolveCall
88
nprtX2
(nprtEmit (nprtStr nprtX1 0 nprtX2) (nprtB nprtLabelAdvance tail))))))
-- AddWord64 (tag 13): operand 1 plus operand 2, modulo 2^64, into the
-- address operand 0 resolves to.
def nprtAddBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchAdd
(nprtResolveCall
64
nprtX1
(nprtResolveCall
88
nprtX2
(nprtResolveCall
112
nprtX3
(nprtEmit
(nprtAdd nprtX2 nprtX3)
(nprtEmit (nprtStr nprtX1 0 nprtX2) (nprtB nprtLabelAdvance tail))))))))
-- Float64 (tags 14 .. 21, Runtime.NativePhysicalImage.
-- nativePhysicalImageFloat64Tag): operand 1's and operand 2's words into d0
-- and d1, the operation, the result's word (binary32: the low word,
-- zero-extended) into the address operand 0 resolves to. Each operation
-- leaves its word in x6.
def nprtFloat64Word =
(lambda unrestricted instruction : (family AArch64Instruction) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
instruction
(nprtEmit (constructor AArch64Instruction AArch64FloatMoveToGeneral64 nprtX6 nprtD0) tail))))
def nprtFloat64Binary =
(lambda unrestricted operation : (pi unrestricted d : (family AArch64FloatRegister) . (pi unrestricted l : (family AArch64FloatRegister) . (pi unrestricted r : (family AArch64FloatRegister) . (family AArch64Instruction)))) .
(nprtFloat64Word (operation nprtD0 nprtD0 nprtD1)))
-- `each tag operation rest` for every tag, in order
def nprtFloat64Entries =
(lambda unrestricted each : (pi unrestricted tag : Nat . (pi unrestricted operation : (pi unrestricted after : (family AArch64Assembly) . (family AArch64Assembly)) . (pi unrestricted rest : (family AArch64Assembly) . (family AArch64Assembly)))) .
(lambda unrestricted tail : (family AArch64Assembly) .
(each
14
(nprtFloat64Binary
(lambda unrestricted d : (family AArch64FloatRegister) .
(lambda unrestricted l : (family AArch64FloatRegister) .
(lambda unrestricted r : (family AArch64FloatRegister) .
(constructor AArch64Instruction AArch64FloatAdd64 d l r)))))
(each
15
(nprtFloat64Binary
(lambda unrestricted d : (family AArch64FloatRegister) .
(lambda unrestricted l : (family AArch64FloatRegister) .
(lambda unrestricted r : (family AArch64FloatRegister) .
(constructor AArch64Instruction AArch64FloatSubtract64 d l r)))))
(each
16
(nprtFloat64Binary
(lambda unrestricted d : (family AArch64FloatRegister) .
(lambda unrestricted l : (family AArch64FloatRegister) .
(lambda unrestricted r : (family AArch64FloatRegister) .
(constructor AArch64Instruction AArch64FloatMultiply64 d l r)))))
(each
17
(nprtFloat64Binary
(lambda unrestricted d : (family AArch64FloatRegister) .
(lambda unrestricted l : (family AArch64FloatRegister) .
(lambda unrestricted r : (family AArch64FloatRegister) .
(constructor AArch64Instruction AArch64FloatDivide64 d l r)))))
-- the square root of operand 2, as the x86 lane's sqrtsd xmm0, xmm1
(each
18
(nprtFloat64Word
(constructor AArch64Instruction AArch64FloatSquareRoot64 nprtD0 nprtD1))
-- operand 1 as a signed 64-bit integer
(each
19
(nprtFloat64Word
(constructor AArch64Instruction AArch64FloatFromSigned64 nprtD0 nprtX2))
-- operand 1 rounded to binary32, its word zero-extended
(each
20
(lambda unrestricted after : (family AArch64Assembly) .
(nprtEmit
(constructor AArch64Instruction AArch64FloatNarrow64To32 nprtD0 nprtD0)
(nprtEmit
(constructor AArch64Instruction AArch64FloatMoveToGeneral32 nprtX6 nprtD0)
after)))
-- operand 1's low word read as binary32, widened
(each
21
(nprtFloat64Word
(constructor AArch64Instruction AArch64FloatWiden32To64 nprtD0 nprtD0))
tail))))))))))
def nprtFloat64Label =
(lambda unrestricted tag : Nat .
(bytes-append nprtLabelDispatchFloat64 (bytes (nat-to-byte tag))))
def nprtFloat64Dispatch =
(nprtFloat64Entries
(lambda unrestricted tag : Nat .
(lambda unrestricted operation : (pi unrestricted after : (family AArch64Assembly) . (family AArch64Assembly)) .
(lambda unrestricted rest : (family AArch64Assembly) .
(nprtDispatchTag tag (nprtFloat64Label tag) rest)))))
def nprtFloat64Block =
(nprtFloat64Entries
(lambda unrestricted tag : Nat .
(lambda unrestricted operation : (pi unrestricted after : (family AArch64Assembly) . (family AArch64Assembly)) .
(lambda unrestricted rest : (family AArch64Assembly) .
(nprtLabel
(nprtFloat64Label tag)
(nprtResolveCall
64
nprtX1
(nprtResolveCall
88
nprtX2
(nprtResolveCall
112
nprtX3
(nprtEmit
(constructor AArch64Instruction AArch64FloatMoveFromGeneral64 nprtD0 nprtX2)
(nprtEmit
(constructor AArch64Instruction AArch64FloatMoveFromGeneral64 nprtD1 nprtX3)
(operation (nprtEmit (nprtStr nprtX1 0 nprtX6) (nprtB nprtLabelAdvance rest)))))))))))))
-- LoopAffine (operand kind 8): base + iteration * stride, the product by
-- repeated addition. x0 holds the descriptor.
def nprtResolveLoopAffineBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelResolveLoopAffine
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtLdr nprtX10 nprtX0 16)
(nprtScratchInto
nprtX9
(nprtEmit
(nprtLdr nprtX9 nprtX9 0)
(nprtLabel
nprtLabelResolveLoopAffineStep
(nprtEmit
(nprtTest nprtX9)
(nprtBIf
nprtEqual
nprtLabelResolveLoopAffineDone
(nprtEmit
(nprtAdd nprtX6 nprtX10)
(nprtEmit
(nprtSubImm nprtX9 1)
(nprtB
nprtLabelResolveLoopAffineStep
(nprtLabel nprtLabelResolveLoopAffineDone (nprtEmit nprtRet tail))))))))))))))
-- FenceWait (tag 12): the address into x3, the expected value into x4, the
-- poll bound into x5 and the interval into the scratch timespec, then load,
-- compare, nanosleep, count down. A timeout is a command failure; only
-- equality advances.
def nprtFenceWaitBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchFenceWait
(nprtResolveCall
64
nprtX3
(nprtResolveCall
88
nprtX4
(nprtResolveCall
112
nprtX5
(nprtResolveCall
136
nprtX6
(nprtScratchInto
nprtX9
(nprtEmit
(nprtMovz nprtX10 0)
(nprtEmit
(nprtStr nprtX9 32 nprtX10)
(nprtEmit
(nprtStr nprtX9 40 nprtX6)
(nprtLabel
nprtLabelFenceWaitLoop
(nprtEmit
(nprtLdr nprtX6 nprtX3 0)
(nprtEmit
(nprtCompare nprtX4 nprtX6)
(nprtBIf
nprtEqual
nprtLabelFenceWaitDone
(nprtEmit
(nprtMov nprtX0 nprtX9)
(nprtEmit
(nprtAddImm nprtX0 32)
(nprtEmit
(nprtMovz nprtX1 0)
(nprtSyscall
nprtNanosleep
(nprtEmit
(nprtSubImm nprtX5 1)
(nprtEmit
(nprtTest nprtX5)
(nprtBIf
nprtNotEqual
nprtLabelFenceWaitLoop
(nprtB
nprtLabelCommandFailure
(nprtLabel
nprtLabelFenceWaitDone
(nprtB nprtLabelAdvance tail))))))))))))))))))))))))
-- entry: x21 = sp ; sp -= 256 ; x15 = &image ; check magic and version ;
-- x13 = command count ; x14 = x15 + 176 ; x12 = x14 + body extent ;
-- x1 = state extent (must be nonzero) ; result slots = count << 3 + extent ;
-- mmap(0, x1, 3, 0x22, -1, 0) -> x20 = state base ; x19 = x20 + state extent.
-- X1 is state extent, X6 result count. X10 holds the remaining word bound.
-- Check before shifting or adding so a damaged image cannot wrap mmap length.
def nprtMemoryGuard =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtMovNegativeOne
nprtX10
(nprtEmit
(nprtSubImm nprtX10 nativePhysicalMemoryScratchBytes)
(nprtEmit
(nprtCompare nprtX10 nprtX1)
(nprtBIf
nprtAbove
nprtLabelFatalFormat
(nprtEmit
(nprtSub nprtX10 nprtX1)
(nprtEmit
(constructor
AArch64Instruction
AArch64ShiftRightImmediate
nprtX10
nprtX10
nativePhysicalMemoryWordShift)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf nprtAbove nprtLabelFatalFormat tail)))))))))
def nprtMainBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelEntry
(nprtEmit
(constructor AArch64Instruction AArch64AddImmediateFromStackPointer nprtX21 0)
(nprtEmit
(constructor
AArch64Instruction
AArch64SubtractStackPointer
nprtStackBytes
(constructor AArch64ImmediateShift AArch64Unshifted))
(nprtAdr
nprtX15
nprtLabelImage
(nprtEmit
(nprtLdr nprtX6 nprtX15 0)
(nprtMovImm64
nprtX10
(byte 65)
(byte 76)
(byte 80)
(byte 88)
(byte 80)
(byte 72)
(byte 89)
(byte 51)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf
nprtNotEqual
nprtLabelFatalFormat
(nprtEmit
(nprtLdr nprtX6 nprtX15 8)
(nprtEmit
(nprtCmpImm nprtX6 3)
(nprtBIf
nprtNotEqual
nprtLabelFatalFormat
(nprtEmit
(nprtLdr nprtX13 nprtX15 16)
(nprtEmit
(nprtMov nprtX14 nprtX15)
(nprtEmit
(nprtAddImm nprtX14 176)
(nprtEmit
(nprtMov nprtX12 nprtX14)
(nprtEmit
(nprtLdr nprtX6 nprtX15 40)
(nprtEmit
(nprtAdd nprtX12 nprtX6)
(nprtEmit
(nprtLdr nprtX1 nprtX15 24)
(nprtEmit
(nprtTest nprtX1)
(nprtBIf
nprtEqual
nprtLabelFatalFormat
(nprtEmit
(nprtLdr nprtX6 nprtX15 32)
(nprtMemoryGuard
(nprtEmit
(nprtLsl nprtX6 nativePhysicalMemoryWordShift)
(nprtEmit
(nprtAdd nprtX1 nprtX6)
(nprtEmit
(nprtAddImm nprtX1 nprtScratchBytes)
(nprtEmit
(nprtMovz nprtX0 0)
(nprtEmit
(nprtMovz nprtX2 3)
(nprtEmit
(nprtMovz nprtX3 34)
(nprtMovNegativeOne
nprtX4
(nprtEmit
(nprtMovz nprtX5 0)
(nprtSyscall
222
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelFatalSystemCall
(nprtEmit
(nprtMov nprtX20 nprtX0)
(nprtEmit
(nprtMov nprtX19 nprtX20)
(nprtEmit
(nprtLdr nprtX6 nprtX15 24)
(nprtEmit
(nprtAdd nprtX19 nprtX6)
(nprtB nprtLabelLoop tail)))))))))))))))))))))))))))))))))))))))
-- V3's declared record extent includes only the minimum tail padding. Rounding
-- the sum of the content extents (rather than any individual field) keeps their
-- lengths and the diagnostic output intact. Every advance preserves alignment.
def nprtRoundRecordExtent =
(lambda unrestricted register : (family AArch64Register) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
(nprtAddImm register 3)
(nprtEmit
(constructor AArch64Instruction AArch64ShiftRightImmediate register register 2)
(nprtEmit (nprtLsl register 2) tail)))))
-- loop: while x13 != 0: bounds-check the record at x14, dispatch on kind.
def nprtLoopBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelLoop
(nprtEmit
(nprtTest nprtX13)
(nprtBIf
nprtEqual
nprtLabelDone
(nprtEmit
(nprtCompare nprtX12 nprtX14)
(nprtBIf
nprtBelow
nprtLabelRecordEndValid
(nprtB
nprtLabelFatalBounds
(nprtLabel
nprtLabelRecordEndValid
(nprtEmit
(nprtLdr nprtX6 nprtX14 8)
(nprtEmit
(nprtCmpImm nprtX6 232)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtLabel
nprtLabelRecordExtentValid
(nprtEmit
(nprtMov nprtX10 nprtX14)
(nprtEmit
(nprtAdd nprtX10 nprtX6)
(nprtEmit
(nprtCompare nprtX12 nprtX10)
(nprtBIf
nprtAbove
nprtLabelFatalBounds
(nprtEmit
(nprtLdr nprtX9 nprtX14 32)
(nprtEmit
(nprtLdr nprtX10 nprtX14 40)
(nprtEmit
(nprtAdd nprtX9 nprtX10)
(nprtEmit
(nprtLdr nprtX10 nprtX14 48)
(nprtEmit
(nprtAdd nprtX9 nprtX10)
(nprtEmit
(nprtAddImm nprtX9 232)
(nprtRoundRecordExtent
nprtX9
(nprtEmit
(nprtCompare nprtX6 nprtX9)
(nprtBIf
nprtNotEqual
nprtLabelFatalRecord
(nprtEmit
(nprtLdr nprtX9 nprtX14 48)
(nprtEmit
(nprtTest nprtX9)
(nprtBIf
nprtEqual
nprtLabelFatalRecord
(nprtEmit
(nprtLdr nprtX6 nprtX14 0)
(nprtEmit
(nprtCmpImm nprtX6 1)
(nprtBIf
nprtEqual
nprtLabelDispatchSystemCall
(nprtEmit
(nprtCmpImm nprtX6 2)
(nprtBIf
nprtEqual
nprtLabelDispatchCopy
(nprtEmit
(nprtCmpImm nprtX6 3)
(nprtBIf
nprtEqual
nprtLabelDispatchRoutine
(nprtEmit
(nprtCmpImm nprtX6 4)
(nprtBIf
nprtEqual
nprtLabelDispatchFence
(nprtEmit
(nprtCmpImm nprtX6 5)
(nprtBIf
nprtEqual
nprtLabelDispatchTelemetry
(nprtEmit
(nprtCmpImm nprtX6 6)
(nprtBIf
nprtEqual
nprtLabelDispatchAssert
(nprtEmit
(nprtCmpImm nprtX6 7)
(nprtBIf
nprtEqual
nprtLabelDispatchHalt
(nprtEmit
(nprtCmpImm nprtX6 8)
(nprtBIf
nprtEqual
nprtLabelDispatchAssertOneOf
(nprtDispatchTag
23
nprtLabelDispatchSkip
(nprtDispatchTag
9
nprtLabelDispatchRepeatBegin
(nprtDispatchTag
10
nprtLabelDispatchRepeatEnd
(nprtDispatchTag
11
nprtLabelDispatchStore
(nprtDispatchTag
12
nprtLabelDispatchFenceWait
(nprtDispatchTag
13
nprtLabelDispatchAdd
(nprtFloat64Dispatch (nprtB nprtLabelFatalRecord tail)))))))))))))))))))))))))))))))))))))))))))))))))))))
-- syscall: resolve number (slot B) and six arguments, svc, result to x2, bind.
def nprtSystemCallBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchSystemCall
(nprtResolveCall
64
nprtX6
(nprtEmit
(nprtStrSlot nprtSlotB nprtX6)
(nprtResolveCall
112
nprtX1
(nprtResolveCall
136
nprtX2
(nprtResolveCall
160
nprtX3
(nprtResolveCall
184
nprtX4
(nprtResolveCall
208
nprtX5
(nprtResolveCall
88
nprtX0
(nprtEmit
(nprtLdrSlot nprtX8 nprtSlotB)
(nprtEmit
nprtSvc
(nprtEmit (nprtMov nprtX2 nprtX0) (nprtB nprtLabelBindResult tail))))))))))))))
-- bind: binding kind at [x14+16]: 0 discard, 1 store x2 into result slot [x14+24].
def nprtBindBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelBindResult
(nprtEmit
(nprtLdr nprtX6 nprtX14 16)
(nprtEmit
(nprtCmpImm nprtX6 0)
(nprtBIf
nprtEqual
nprtLabelAdvance
(nprtEmit
(nprtCmpImm nprtX6 1)
(nprtBIf
nprtEqual
nprtLabelBindStore
(nprtB
nprtLabelFatalRecord
(nprtLabel
nprtLabelBindStore
(nprtEmit
(nprtLdr nprtX6 nprtX14 24)
(nprtEmit
(nprtLdr nprtX10 nprtX15 32)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf
nprtBelow
nprtLabelBindSlotValid
(nprtB
nprtLabelFatalOperand
(nprtLabel
nprtLabelBindSlotValid
(nprtEmit
(nprtLsl nprtX6 3)
(nprtEmit
(nprtAdd nprtX6 nprtX19)
(nprtEmit
(nprtStr nprtX6 0 nprtX2)
(nprtB nprtLabelAdvance tail)))))))))))))))))))
-- copy: payload [x14+232 ..) of extent (resolved 88, must equal [x14+32]) into
-- state at resolved destination (64), bounded by the state extent.
def nprtCopyBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchCopy
(nprtResolveCall
88
nprtX3
(nprtEmit
(nprtLdr nprtX10 nprtX14 32)
(nprtEmit
(nprtCompare nprtX10 nprtX3)
(nprtBIf
nprtNotEqual
nprtLabelCommandFailure
(nprtEmit
(nprtMov nprtX5 nprtX3)
(nprtResolveCall
64
nprtX6
(nprtEmit
(nprtMov nprtX9 nprtX6)
(nprtEmit
(nprtAdd nprtX9 nprtX5)
(nprtEmit
(nprtLdr nprtX10 nprtX15 24)
(nprtEmit
(nprtCompare nprtX10 nprtX9)
(nprtBIf
nprtAbove
nprtLabelCommandFailure
(nprtEmit
(nprtAdd nprtX6 nprtX20)
(nprtEmit
(nprtMov nprtX0 nprtX6)
(nprtEmit
(nprtMov nprtX1 nprtX14)
(nprtEmit
(nprtAddImm nprtX1 232)
(nprtEmit
(nprtTest nprtX3)
(nprtBIf
nprtEqual
nprtLabelCopyDone
(nprtLabel
nprtLabelCopyLoop
(nprtEmit
(nprtLdrb nprtX6 nprtX1)
(nprtEmit
(nprtStrb nprtX0 nprtX6)
(nprtEmit
(nprtAddImm nprtX1 1)
(nprtEmit
(nprtAddImm nprtX0 1)
(nprtEmit
(nprtSubImm nprtX3 1)
(nprtEmit
(nprtTest nprtX3)
(nprtBIf
nprtNotEqual
nprtLabelCopyLoop
(nprtLabel nprtLabelCopyDone (nprtB nprtLabelAdvance tail)))))))))))))))))))))))))))))
def nprtRoutineCall =
(lambda unrestricted target : (family AArch64Register) .
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtEmit
(nprtStrSlot nprtSaveImageEnd nprtX12)
(nprtEmit
(nprtStrSlot nprtSaveRemaining nprtX13)
(nprtEmit
(nprtStrSlot nprtSaveCommand nprtX14)
(nprtEmit
(nprtStrSlot nprtSaveImage nprtX15)
(nprtEmit
(nprtBlr target)
(nprtEmit
(nprtLdrSlot nprtX12 nprtSaveImageEnd)
(nprtEmit
(nprtLdrSlot nprtX13 nprtSaveRemaining)
(nprtEmit
(nprtLdrSlot nprtX14 nprtSaveCommand)
(nprtEmit (nprtLdrSlot nprtX15 nprtSaveImage) tail)))))))))))
-- routine: call the machine code at [x14+232] with six resolved arguments.
def nprtRoutineBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchRoutine
(nprtEmit
(nprtMov nprtX6 nprtX14)
(nprtEmit
(nprtAddImm nprtX6 232)
(nprtEmit
(nprtStrSlot nprtSlotB nprtX6)
(nprtResolveCall
88
nprtX1
(nprtResolveCall
112
nprtX2
(nprtResolveCall
136
nprtX3
(nprtResolveCall
160
nprtX4
(nprtResolveCall
184
nprtX5
(nprtResolveCall
64
nprtX0
(nprtEmit
(nprtLdrSlot nprtX10 nprtSlotB)
(nprtRoutineCall
nprtX10
(nprtEmit (nprtMov nprtX2 nprtX0) (nprtB nprtLabelBindResult tail)))))))))))))))
-- fence: poll [address] (64) for expected (88), at most maximumPolls (112) times.
def nprtFenceBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchFence
(nprtResolveCall
112
nprtX3
(nprtEmit
(nprtStrSlot nprtSlotB nprtX3)
(nprtResolveCall
88
nprtX1
(nprtEmit
(nprtStrSlot nprtSlotA nprtX1)
(nprtResolveCall
64
nprtX0
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotA)
(nprtEmit
(nprtLdrSlot nprtX3 nprtSlotB)
(nprtEmit
(nprtTest nprtX3)
(nprtBIf
nprtEqual
nprtLabelCommandFailure
(nprtLabel
nprtLabelFenceLoop
(nprtEmit
(nprtLdr nprtX6 nprtX0 0)
(nprtEmit
(nprtCompare nprtX1 nprtX6)
(nprtBIf
nprtEqual
nprtLabelFenceDone
(nprtEmit
(nprtSubImm nprtX3 1)
(nprtEmit
(nprtTest nprtX3)
(nprtBIf
nprtNotEqual
nprtLabelFenceLoop
(nprtB
nprtLabelCommandFailure
(nprtLabel nprtLabelFenceDone (nprtB nprtLabelAdvance tail)))))))))))))))))))))
-- assert: resolved (88) must equal resolved (64).
def nprtAssertBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchAssert
(nprtResolveCall
88
nprtX1
(nprtEmit
(nprtStrSlot nprtSlotB nprtX1)
(nprtResolveCall
64
nprtX6
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotB)
(nprtEmit
(nprtCompare nprtX1 nprtX6)
(nprtBIf nprtNotEqual nprtLabelCommandFailure (nprtB nprtLabelAdvance tail)))))))))
-- assert-one-of: resolved (64) must equal resolved (88) or resolved (112).
def nprtAssertOneOfBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchAssertOneOf
(nprtResolveCall
112
nprtX1
(nprtEmit
(nprtStrSlot nprtSlotC nprtX1)
(nprtResolveCall
88
nprtX1
(nprtEmit
(nprtStrSlot nprtSlotB nprtX1)
(nprtResolveCall
64
nprtX6
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotB)
(nprtEmit
(nprtCompare nprtX1 nprtX6)
(nprtBIf
nprtEqual
nprtLabelAdvance
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotC)
(nprtEmit
(nprtCompare nprtX1 nprtX6)
(nprtBIf
nprtNotEqual
nprtLabelCommandFailure
(nprtB nprtLabelAdvance tail))))))))))))))
-- telemetry: mmap a buffer of path length + 1, copy the path (payload) in,
-- openat(AT_FDCWD, path, O_WRONLY|O_CREAT|O_APPEND, 0644), write the record
-- (payload after the path) in a loop, fsync, close, munmap.
def nprtTelemetryBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchTelemetry
(nprtEmit
(nprtLdr nprtX3 nprtX14 32)
(nprtEmit
(nprtTest nprtX3)
(nprtBIf
nprtEqual
nprtLabelCommandFailure
(nprtEmit
(nprtMov nprtX1 nprtX3)
(nprtEmit
(nprtAddImm nprtX1 1)
(nprtEmit
(nprtStrSlot nprtSlotC nprtX1)
(nprtEmit
(nprtMovz nprtX0 0)
(nprtEmit
(nprtMovz nprtX2 3)
(nprtEmit
(nprtMovz nprtX3 34)
(nprtMovNegativeOne
nprtX4
(nprtEmit
(nprtMovz nprtX5 0)
(nprtSyscall
222
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelCommandFailure
(nprtEmit
(nprtStrSlot nprtSlotA nprtX0)
(nprtEmit
(nprtLdr nprtX3 nprtX14 32)
(nprtEmit
(nprtMov nprtX1 nprtX14)
(nprtEmit
(nprtAddImm nprtX1 232)
(nprtLabel
nprtLabelTelemetryCopyLoop
(nprtEmit
(nprtLdrb nprtX6 nprtX1)
(nprtEmit
(nprtStrb nprtX0 nprtX6)
(nprtEmit
(nprtAddImm nprtX1 1)
(nprtEmit
(nprtAddImm nprtX0 1)
(nprtEmit
(nprtSubImm nprtX3 1)
(nprtEmit
(nprtTest nprtX3)
(nprtBIf
nprtNotEqual
nprtLabelTelemetryCopyLoop
(nprtMovNegativeOne
nprtX0
(nprtEmit
(nprtAddImm nprtX0 0)
(nprtEmit
(nprtMovz nprtX9 99)
(nprtEmit
(nprtSub nprtX0 nprtX9)
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotA)
(nprtEmit
(nprtMovz nprtX2 1089)
(nprtEmit
(nprtMovz nprtX3 420)
(nprtSyscall
56
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelCommandFailure
(nprtEmit
(nprtStrSlot nprtSlotB nprtX0)
(nprtEmit
(nprtMov nprtX1 nprtX14)
(nprtEmit
(nprtAddImm nprtX1 232)
(nprtEmit
(nprtLdr nprtX3 nprtX14 32)
(nprtEmit
(nprtAdd nprtX1 nprtX3)
(nprtEmit
(nprtLdr nprtX2 nprtX14 40)
(nprtEmit
(nprtLdrSlot nprtX0 nprtSlotB)
(nprtLabel
nprtLabelTelemetryWriteLoop
(nprtSyscall
64
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelCommandFailure
(nprtBIf
nprtEqual
nprtLabelCommandFailure
(nprtEmit
(nprtAdd nprtX1 nprtX0)
(nprtEmit
(nprtSub nprtX2 nprtX0)
(nprtEmit
(nprtLdrSlot nprtX0 nprtSlotB)
(nprtEmit
(nprtTest nprtX2)
(nprtBIf
nprtNotEqual
nprtLabelTelemetryWriteLoop
(nprtSyscall
82
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelCommandFailure
(nprtEmit
(nprtLdrSlot nprtX0 nprtSlotB)
(nprtSyscall
57
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelCommandFailure
(nprtEmit
(nprtLdrSlot nprtX0 nprtSlotA)
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotC)
(nprtSyscall
215
(nprtEmit
(nprtTest nprtX0)
(nprtBIf
nprtMinus
nprtLabelCommandFailure
(nprtB nprtLabelAdvance tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-- advance: x14 += record extent ; x13 -= 1 ; loop.
def nprtAdvanceBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelAdvance
(nprtEmit
(nprtLdr nprtX6 nprtX14 8)
(nprtEmit
(nprtAdd nprtX14 nprtX6)
(nprtEmit (nprtSubImm nprtX13 1) (nprtB nprtLabelLoop tail))))))
-- done: the command pointer must have reached the image end exactly.
def nprtDoneBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDone
(nprtEmit
(nprtCompare nprtX12 nprtX14)
(nprtBIf nprtNotEqual nprtLabelFatalBounds (nprtExitWith 0 tail)))))
def nprtHaltBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel nprtLabelDispatchHalt (nprtExitWith 0 tail)))
-- command failure: write the command's error identity ([x14+48] bytes at
-- payload + [x14+32] + [x14+40]) to stderr, exit 120.
def nprtCommandFailureBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelCommandFailure
(nprtEmit
(nprtMov nprtX1 nprtX14)
(nprtEmit
(nprtAddImm nprtX1 232)
(nprtEmit
(nprtLdr nprtX6 nprtX14 32)
(nprtEmit
(nprtAdd nprtX1 nprtX6)
(nprtEmit
(nprtLdr nprtX6 nprtX14 40)
(nprtEmit
(nprtAdd nprtX1 nprtX6)
(nprtEmit
(nprtLdr nprtX2 nprtX14 48)
(nprtEmit (nprtMovz nprtX0 2) (nprtSyscall 64 (nprtExitWith 120 tail))))))))))))
-- The resolver: x0 points at an operand descriptor (kind at +0, value at +8,
-- extra at +16); the value lands in x6; ret.
def nprtResolveBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelResolve
(nprtEmit
(nprtLdr nprtX9 nprtX0 0)
(nprtEmit
(nprtCmpImm nprtX9 0)
(nprtBIf
nprtEqual
nprtLabelResolveImmediate
(nprtEmit
(nprtCmpImm nprtX9 1)
(nprtBIf
nprtEqual
nprtLabelResolveResult
(nprtEmit
(nprtCmpImm nprtX9 2)
(nprtBIf
nprtEqual
nprtLabelResolveResultAddress
(nprtEmit
(nprtCmpImm nprtX9 3)
(nprtBIf
nprtEqual
nprtLabelResolveStateAddress
(nprtEmit
(nprtCmpImm nprtX9 4)
(nprtBIf
nprtEqual
nprtLabelResolveStateLoad
(nprtEmit
(nprtCmpImm nprtX9 5)
(nprtBIf
nprtEqual
nprtLabelResolvePayloadAddress
(nprtEmit
(nprtCmpImm nprtX9 6)
(nprtBIf
nprtEqual
nprtLabelResolvePayloadLoad
(nprtEmit
(nprtCmpImm nprtX9 7)
(nprtBIf
nprtEqual
nprtLabelResolveProcessArgument
(nprtDispatchKind
8
nprtLabelResolveLoopAffine
(nprtB
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolveImmediate
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolveResult
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtLdr nprtX10 nprtX15 32)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf
nprtBelow
nprtLabelResolveSlotValid
(nprtB
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolveSlotValid
(nprtEmit
(nprtLsl nprtX6 3)
(nprtEmit
(nprtAdd nprtX6 nprtX19)
(nprtEmit
(nprtLdr nprtX6 nprtX6 0)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolveResultAddress
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtLdr nprtX10 nprtX15 32)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf
nprtBelow
nprtLabelResolveResultAddressSlotValid
(nprtB
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolveResultAddressSlotValid
(nprtEmit
(nprtLsl nprtX6 3)
(nprtEmit
(nprtAdd nprtX6 nprtX19)
(nprtEmit
(nprtLdr nprtX6 nprtX6 0)
(nprtEmit
(nprtLdr nprtX10 nprtX0 16)
(nprtEmit
(nprtAdd nprtX6 nprtX10)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolveStateAddress
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtLdr nprtX10 nprtX15 24)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf
nprtBelow
nprtLabelResolveStateAddressValid
(nprtB
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolveStateAddressValid
(nprtEmit
(nprtAdd nprtX6 nprtX20)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolveStateLoad
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtMov nprtX9 nprtX6)
(nprtEmit
(nprtAddImm nprtX9 8)
(nprtEmit
(nprtLdr nprtX10 nprtX15 24)
(nprtEmit
(nprtCompare nprtX10 nprtX9)
(nprtBIf
nprtAbove
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolveStateLoadValid
(nprtEmit
(nprtAdd nprtX6 nprtX20)
(nprtEmit
(nprtLdr nprtX6 nprtX6 0)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolvePayloadAddress
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtLdr nprtX10 nprtX14 32)
(nprtEmit
(nprtCompare nprtX10 nprtX6)
(nprtBIf
nprtBelow
nprtLabelResolvePayloadAddressValid
(nprtB
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolvePayloadAddressValid
(nprtEmit
(nprtAdd nprtX6 nprtX14)
(nprtEmit
(nprtAddImm nprtX6 232)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolvePayloadLoad
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtMov nprtX9 nprtX6)
(nprtEmit
(nprtAddImm nprtX9 8)
(nprtEmit
(nprtLdr nprtX10 nprtX14 32)
(nprtEmit
(nprtCompare nprtX10 nprtX9)
(nprtBIf
nprtAbove
nprtLabelFatalOperand
(nprtLabel
nprtLabelResolvePayloadLoadValid
(nprtEmit
(nprtAdd nprtX6 nprtX14)
(nprtEmit
(nprtAddImm nprtX6 232)
(nprtEmit
(nprtLdr nprtX6 nprtX6 0)
(nprtEmit
nprtRet
(nprtLabel
nprtLabelResolveProcessArgument
(nprtEmit
(nprtLdr nprtX6 nprtX0 8)
(nprtEmit
(nprtLsl nprtX6 3)
(nprtEmit
(nprtAdd nprtX6 nprtX21)
(nprtEmit
(nprtLdr nprtX6 nprtX6 nprtArgvOffset)
(nprtEmit nprtRet tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-- fatal exits, and the shared exit: exit_group(x0).
def nprtFatalBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelFatalFormat
(nprtExitWith
101
(nprtLabel
nprtLabelFatalBounds
(nprtExitWith
102
(nprtLabel
nprtLabelFatalOperand
(nprtExitWith
103
(nprtLabel
nprtLabelFatalSystemCall
(nprtExitWith
104
(nprtLabel
nprtLabelFatalAssertion
(nprtExitWith
105
(nprtLabel
nprtLabelFatalFence
(nprtExitWith
106
(nprtLabel
nprtLabelFatalTelemetry
(nprtExitWith
107
(nprtLabel
nprtLabelFatalRecord
(nprtExitWith 108 (nprtLabel nprtLabelExit (nprtSyscall 94 tail)))))))))))))))))))
-- Same record-count and repeat-frame contract as the x86-64 executor.
-- Skip traversal uses temporary registers, preserving the current loop frame.
def nprtSkipBlock =
(lambda unrestricted tail : (family AArch64Assembly) .
(nprtLabel
nprtLabelDispatchSkip
(nprtResolveCall
88
nprtX1
(nprtEmit
(nprtStrSlot nprtSlotB nprtX1)
(nprtResolveCall
64
nprtX6
(nprtEmit
(nprtLdrSlot nprtX1 nprtSlotB)
(nprtEmit
(nprtCompare nprtX1 nprtX6)
(nprtBIf
nprtEqual
nprtLabelAdvance
(nprtResolveCall
112
nprtX8
(nprtEmit
(nprtMov nprtX6 nprtX13)
(nprtEmit
(nprtSubImm nprtX6 1)
(nprtEmit
(nprtCompare nprtX8 nprtX6)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtMovz nprtX7 0)
(nprtLabel
b"np-skip-scan"
(nprtEmit
(nprtLdr nprtX6 nprtX14 8)
(nprtEmit
(nprtAdd nprtX14 nprtX6)
(nprtEmit
(nprtSubImm nprtX13 1)
(nprtEmit
(nprtCmpImm nprtX8 0)
(nprtBIf
nprtEqual
b"np-skip-done"
(nprtScanRecord
nprtX14
nprtX9
nprtX6
nprtX10
(nprtEmit
(nprtLdr nprtX6 nprtX14 0)
(nprtEmit
(nprtCmpImm nprtX6 1)
(nprtBIf
nprtBelow
nprtLabelFatalRecord
(nprtEmit
(nprtCmpImm nprtX6 23)
(nprtBIf
nprtAbove
nprtLabelFatalRecord
(nprtEmit
(nprtCmpImm nprtX6 9)
(nprtBIf
nprtEqual
b"np-skip-begin"
(nprtEmit
(nprtCmpImm nprtX6 10)
(nprtBIf
nprtEqual
b"np-skip-end"
(nprtEmit
(nprtCmpImm nprtX6 22)
(nprtBIf
nprtEqual
b"np-skip-end"
(nprtB
b"np-skip-next"
(nprtLabel
b"np-skip-begin"
(nprtEmit
(nprtCmpImm nprtX7 0)
(nprtBIf
nprtNotEqual
nprtLabelFatalRecord
(nprtEmit
(nprtMovz nprtX7 1)
(nprtB
b"np-skip-next"
(nprtLabel
b"np-skip-end"
(nprtEmit
(nprtCmpImm nprtX7 0)
(nprtBIf
nprtEqual
nprtLabelFatalRecord
(nprtEmit
(nprtMovz nprtX7 0)
(nprtLabel
b"np-skip-next"
(nprtEmit
(nprtSubImm nprtX8 1)
(nprtB
b"np-skip-scan"
(nprtLabel
b"np-skip-done"
(nprtEmit
(nprtCmpImm nprtX7 0)
(nprtBIf
nprtNotEqual
nprtLabelFatalRecord
(nprtB nprtLabelLoop tail)))))))))))))))))))))))))))))))))))))))))))))))))
def aarch64NativePhysicalRuntimeAssembly : (family AArch64Assembly) =
(nprtMainBlock
(nprtLoopBlock
(nprtSystemCallBlock
(nprtBindBlock
(nprtCopyBlock
(nprtRoutineBlock
(nprtFenceBlock
(nprtTelemetryBlock
(nprtAssertBlock
(nprtAssertOneOfBlock
(nprtAdvanceBlock
(nprtDoneBlock
(nprtHaltBlock
(nprtCommandFailureBlock
(nprtResolveBlock
(nprtSkipBlock
(nprtFatalBlock
(nprtRepeatBeginBlock
(nprtRepeatEndBlock
(nprtStoreBlock
(nprtAddBlock
(nprtFloat64Block
(nprtResolveLoopAffineBlock
(nprtFenceWaitBlock
(constructor
AArch64Assembly
AArch64AssemblyLabel
nprtLabelImage
(constructor AArch64Assembly AArch64AssemblyEnd))))))))))))))))))))))))))
def aarch64NativePhysicalRuntime : (family AArch64AssemblyResult) =
(aarch64Assemble aarch64NativePhysicalRuntimeAssembly)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.