Large source region · 3,650 lines
module Runtime.NativePhysicalNative
import Runtime.NativePhysicalImage
import Runtime.NativePhysicalMemory
import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.NativePhysicalProgram
import Std.Natural
def nativePhysicalNativeLabelEntry : Bytes =
b"np-entry"
def nativePhysicalNativeLabelLoop : Bytes =
b"np-loop"
def nativePhysicalNativeLabelDone : Bytes =
b"np-done"
def nativePhysicalNativeLabelAdvance : Bytes =
b"np-advance"
def nativePhysicalNativeLabelResolve : Bytes =
b"np-resolve"
def nativePhysicalNativeLabelUnpack : Bytes =
b"np-unpack"
def nativePhysicalNativeLabelImageReady : Bytes =
b"np-image-ready"
def nativePhysicalNativeLabelFatalUnpack : Bytes =
b"np-fatal-unpack"
def nativePhysicalNativeLabelUnpackSequence : Bytes =
b"np-unpack-sequence"
def nativePhysicalNativeLabelUnpackToken : Bytes =
b"np-unpack-token"
def nativePhysicalNativeLabelUnpackEnd : Bytes =
b"np-unpack-end"
def nativePhysicalNativeLabelUnpackLiterals : Bytes =
b"np-unpack-literals"
def nativePhysicalNativeLabelUnpackLiteralLength : Bytes =
b"np-unpack-literal-length"
def nativePhysicalNativeLabelUnpackLiteralByte : Bytes =
b"np-unpack-literal-byte"
def nativePhysicalNativeLabelUnpackLiteralCopy : Bytes =
b"np-unpack-literal-copy"
def nativePhysicalNativeLabelUnpackLiteralsDone : Bytes =
b"np-unpack-literals-done"
def nativePhysicalNativeLabelUnpackMatch : Bytes =
b"np-unpack-match"
def nativePhysicalNativeLabelUnpackMatchLength : Bytes =
b"np-unpack-match-length"
def nativePhysicalNativeLabelUnpackMatchByte : Bytes =
b"np-unpack-match-byte"
def nativePhysicalNativeLabelUnpackMatchCopy : Bytes =
b"np-unpack-match-copy"
def nativePhysicalNativeLabelResolveSlot : Bytes =
b"np-resolve-slot"
def nativePhysicalNativeLabelResolveImmediate : Bytes =
b"np-res-imm"
def nativePhysicalNativeLabelResolveResult : Bytes =
b"np-res-res"
def nativePhysicalNativeLabelResolveResultAddress : Bytes =
b"np-res-raddr"
def nativePhysicalNativeLabelResolveStateAddress : Bytes =
b"np-res-saddr"
def nativePhysicalNativeLabelResolveStateLoad : Bytes =
b"np-res-sload"
def nativePhysicalNativeLabelResolvePayloadAddress : Bytes =
b"np-res-paddr"
def nativePhysicalNativeLabelResolvePayloadLoad : Bytes =
b"np-res-pload"
def nativePhysicalNativeLabelResolveProcessArgument : Bytes =
b"np-res-argv"
def nativePhysicalNativeLabelResolveSlotValid : Bytes =
b"np-res-sv"
def nativePhysicalNativeLabelResolveResultAddressSlotValid : Bytes =
b"np-res-rasv"
def nativePhysicalNativeLabelResolveStateAddressValid : Bytes =
b"np-res-sav"
def nativePhysicalNativeLabelResolveStateLoadValid : Bytes =
b"np-res-slv"
def nativePhysicalNativeLabelResolvePayloadAddressValid : Bytes =
b"np-res-pav"
def nativePhysicalNativeLabelResolvePayloadLoadValid : Bytes =
b"np-res-plv"
def nativePhysicalNativeLabelDispatchSystemCall : Bytes =
b"np-syscall"
def nativePhysicalNativeLabelDispatchCopy : Bytes =
b"np-copy"
def nativePhysicalNativeLabelDispatchRoutine : Bytes =
b"np-routine"
def nativePhysicalNativeLabelDispatchFence : Bytes =
b"np-fence"
def nativePhysicalNativeLabelDispatchTelemetry : Bytes =
b"np-telemetry"
def nativePhysicalNativeLabelDispatchAssert : Bytes =
b"np-assert"
def nativePhysicalNativeLabelDispatchSkip : Bytes =
b"np-skip"
def nativePhysicalNativeLabelDispatchRepeatBegin : Bytes =
b"dispatch-repeat-begin"
def nativePhysicalNativeLabelDispatchRepeatEnd : Bytes =
b"dispatch-repeat-end"
def nativePhysicalNativeLabelDispatchRepeatEndWhen : Bytes =
b"dispatch-repeat-end-when"
def nativePhysicalNativeLabelDispatchStore : Bytes =
b"dispatch-store"
def nativePhysicalNativeLabelDispatchAdd : Bytes =
b"dispatch-add"
def nativePhysicalNativeLabelDispatchFloat64 : Bytes =
b"dispatch-float64"
def nativePhysicalNativeLabelRepeatScan : Bytes =
b"repeat-scan"
def nativePhysicalNativeLabelRepeatScanNext : Bytes =
b"repeat-scan-next"
def nativePhysicalNativeLabelRepeatFound : Bytes =
b"repeat-found"
def nativePhysicalNativeLabelRepeatAgain : Bytes =
b"repeat-again"
def nativePhysicalNativeLabelResolveLoopAffine : Bytes =
b"resolve-loop-affine"
def nativePhysicalNativeLabelResolveLoopAffineStep : Bytes =
b"resolve-loop-affine-step"
def nativePhysicalNativeLabelResolveLoopAffineDone : Bytes =
b"resolve-loop-affine-done"
def nativePhysicalNativeLabelDispatchFenceWait : Bytes =
b"dispatch-fence-wait"
def nativePhysicalNativeLabelFenceWaitLoop : Bytes =
b"fence-wait-loop"
def nativePhysicalNativeLabelFenceWaitDone : Bytes =
b"fence-wait-done"
def nativePhysicalNativeLabelDispatchAssertOneOf : Bytes =
b"np-assert-one"
def nativePhysicalNativeLabelDispatchHalt : Bytes =
b"np-halt"
def nativePhysicalNativeLabelBindResult : Bytes =
b"np-bind"
def nativePhysicalNativeLabelBindDiscard : Bytes =
b"np-bind-d"
def nativePhysicalNativeLabelBindStore : Bytes =
b"np-bind-s"
def nativePhysicalNativeLabelBindSlotValid : Bytes =
b"np-bind-sv"
def nativePhysicalNativeLabelCopyBoundsValid : Bytes =
b"np-copy-bv"
def nativePhysicalNativeLabelCopyLoop : Bytes =
b"np-copy-l"
def nativePhysicalNativeLabelCopyDone : Bytes =
b"np-copy-d"
def nativePhysicalNativeLabelFenceLoop : Bytes =
b"np-fence-l"
def nativePhysicalNativeLabelFenceDone : Bytes =
b"np-fence-d"
def nativePhysicalNativeLabelTelemetryCopyLoop : Bytes =
b"np-tel-cl"
def nativePhysicalNativeLabelTelemetryCopyDone : Bytes =
b"np-tel-cd"
def nativePhysicalNativeLabelTelemetryWriteLoop : Bytes =
b"np-tel-wl"
def nativePhysicalNativeLabelTelemetryWriteDone : Bytes =
b"np-tel-wd"
def nativePhysicalNativeLabelRecordExtentValid : Bytes =
b"np-rec-ev"
def nativePhysicalNativeLabelRecordEndValid : Bytes =
b"np-rec-bv"
def nativePhysicalNativeLabelRecordTotalValid : Bytes =
b"np-rec-tv"
def nativePhysicalNativeLabelRecordErrorValid : Bytes =
b"np-rec-iv"
def nativePhysicalNativeLabelFatalFormat : Bytes =
b"np-fatal-format"
def nativePhysicalNativeLabelFatalBounds : Bytes =
b"np-fatal-bounds"
def nativePhysicalNativeLabelFatalOperand : Bytes =
b"np-fatal-operand"
def nativePhysicalNativeLabelFatalSystemCall : Bytes =
b"np-fatal-syscall"
def nativePhysicalNativeLabelFatalAssertion : Bytes =
b"np-fatal-assert"
def nativePhysicalNativeLabelFatalFence : Bytes =
b"np-fatal-fence"
def nativePhysicalNativeLabelFatalTelemetry : Bytes =
b"np-fatal-tel"
def nativePhysicalNativeLabelFatalRecord : Bytes =
b"np-fatal-record"
def nativePhysicalNativeLabelCommandFailure : Bytes =
b"np-command-fail"
def nativePhysicalNativeLabelExit : Bytes =
b"np-exit"
def nativePhysicalNativeLabelImage : Bytes =
b"np-image"
def nativePhysicalNativeDisplacement =
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(lambda unrestricted byte3 : Byte .
(constructor X86NativeDisplacement32 X86NativeDisplacement32Value byte0 byte1 byte2 byte3)))))
def nativePhysicalNativeImmediate32 =
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(lambda unrestricted byte3 : Byte .
(constructor X86NativeImmediate32 X86NativeImmediate32Value byte0 byte1 byte2 byte3)))))
def nativePhysicalNativeImmediate8 =
(lambda unrestricted byte0 : Byte .
(constructor X86NativeImmediate8 X86NativeImmediate8Value byte0))
def nativePhysicalNativeImmediate64 =
(lambda unrestricted byte0 : Byte .
(lambda unrestricted byte1 : Byte .
(lambda unrestricted byte2 : Byte .
(lambda unrestricted byte3 : Byte .
(lambda unrestricted byte4 : Byte .
(lambda unrestricted byte5 : Byte .
(lambda unrestricted byte6 : Byte .
(lambda unrestricted byte7 : Byte .
(constructor
X86NativeImmediate64
X86NativeImmediate64Value
byte0
byte1
byte2
byte3
byte4
byte5
byte6
byte7)))))))))
def nativePhysicalNativeD0 : (family X86NativeDisplacement32) =
(nativePhysicalNativeDisplacement (byte 0) (byte 0) (byte 0) (byte 0))
def nativePhysicalNativeD8 : (family X86NativeDisplacement32) =
(nativePhysicalNativeDisplacement (byte 8) (byte 0) (byte 0) (byte 0))
def nativePhysicalNativeDisplacementByte =
(lambda unrestricted value : Byte .
(nativePhysicalNativeDisplacement value (byte 0) (byte 0) (byte 0)))
def nativePhysicalNativeNegativeDisplacementByte =
(lambda unrestricted value : Byte .
(nativePhysicalNativeDisplacement value (byte 255) (byte 255) (byte 255)))
def nativePhysicalNativeI32Byte =
(lambda unrestricted value : Byte .
(nativePhysicalNativeImmediate32 value (byte 0) (byte 0) (byte 0)))
def nativePhysicalNativeI32NegativeOne : (family X86NativeImmediate32) =
(nativePhysicalNativeImmediate32 (byte 255) (byte 255) (byte 255) (byte 255))
def nativePhysicalNativeI64Byte =
(lambda unrestricted value : Byte .
(nativePhysicalNativeImmediate64
value
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)))
def nativePhysicalNativeI64NegativeOne : (family X86NativeImmediate64) =
(nativePhysicalNativeImmediate64
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255))
def nativePhysicalNativeEmit =
(lambda unrestricted instruction : (family X86NativeInstruction) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(constructor X86NativeAssembly X86NativeAssemblyEmit instruction tail)))
def nativePhysicalNativeLabel =
(lambda unrestricted name : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(constructor X86NativeAssembly X86NativeAssemblyLabel name tail)))
def nativePhysicalNativeJump =
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(constructor X86NativeAssembly X86NativeAssemblyJump target tail)))
def nativePhysicalNativeJumpCondition =
(lambda unrestricted condition : (family X86NativeCondition) .
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition target tail))))
def nativePhysicalNativeLEA =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted target : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(constructor
X86NativeAssembly
X86NativeAssemblyLoadEffectiveAddressRIPLabel
destination
target
tail))))
def nativePhysicalNativeMoveImmediate32 =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate32) .
(constructor X86NativeInstruction X86NativeMoveImmediate32 destination immediate)))
def nativePhysicalNativeMoveImmediate64 =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate64) .
(constructor X86NativeInstruction X86NativeMoveImmediate64 destination immediate)))
def nativePhysicalNativeMove =
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted destination : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeMoveRegister64 source destination)))
def nativePhysicalNativeAdd =
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted destination : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeAddRegister64 source destination)))
def nativePhysicalNativeSubtract =
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted destination : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeSubtractRegister64 source destination)))
def nativePhysicalNativeCompare =
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted destination : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeCompareRegister64 source destination)))
def nativePhysicalNativeTest =
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted destination : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeTestRegister64 source destination)))
def nativePhysicalNativeAddImmediate =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate32) .
(constructor X86NativeInstruction X86NativeAddImmediate64 destination immediate)))
def nativePhysicalNativeCompareImmediate =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate32) .
(constructor X86NativeInstruction X86NativeCompareImmediate64 destination immediate)))
def nativePhysicalNativeShiftLeft =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate8) .
(constructor X86NativeInstruction X86NativeShiftLeftImmediate64 destination immediate)))
def nativePhysicalNativeLoad64 =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : (family X86NativeDisplacement32) .
(constructor X86NativeInstruction X86NativeLoadMemory64 destination base displacement))))
def nativePhysicalNativeLoad8 =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : (family X86NativeDisplacement32) .
(constructor
X86NativeInstruction
X86NativeLoadMemory8ZeroExtend64
destination
base
displacement))))
def nativePhysicalNativeStore64 =
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : (family X86NativeDisplacement32) .
(lambda unrestricted source : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeStoreMemory64 base displacement source))))
def nativePhysicalNativeStore8 =
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : (family X86NativeDisplacement32) .
(lambda unrestricted source : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeStoreMemory8 base displacement source))))
def nativePhysicalNativeCall =
(lambda unrestricted target : (family X86NativeRegister64) .
(constructor X86NativeInstruction X86NativeCallRegister64 target))
def nativePhysicalNativeReturnInstruction : (family X86NativeInstruction) =
(constructor X86NativeInstruction X86NativeReturn)
def nativePhysicalNativeSystemCallInstruction : (family X86NativeInstruction) =
(constructor X86NativeInstruction X86NativeSystemCall)
def nativePhysicalNativeResolveCall =
(lambda unrestricted descriptorOffset : Byte .
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRDI))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte descriptorOffset))
(nativePhysicalNativeLEA
(constructor X86NativeRegister64 X86NativeRAX)
nativePhysicalNativeLabelResolveSlot
(nativePhysicalNativeEmit
(nativePhysicalNativeCall (constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
destination)
tail))))))))
-- Record layout (Runtime.NativePhysicalImagePlan, V4): a record stores its
-- operand slots up to the last one that is not the zero immediate; header
-- word 7 ([record+56]) holds the operand bytes it omits (at most 168), and
-- its payload begins at 232 minus that. These helpers keep the record
-- pointer in R14 and use one scratch register that is dead at the call site.
-- destination := destination + 232 - [r14+56]
def nativePhysicalNativePayloadBase =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted scratch : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
destination
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandFixedBytes)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
scratch
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 56)))
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract scratch destination)
tail))))))
-- The validated extent: content + 232 - omitted, refusing omitted > 168.
def nativePhysicalNativeRecordFixedPart =
(lambda unrestricted total : (family X86NativeRegister64) .
(lambda unrestricted scratch : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
total
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandFixedBytes)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
scratch
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 56)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
scratch
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandOperandBytes)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract scratch total)
tail))))))))
-- Resolve the operand slot at rdi of the record at r14. A slot at or past
-- 232 - [r14+56] is not stored and reads as the zero immediate. Scratches
-- rax, r10 and r11, like the resolver it falls into.
def nativePhysicalNativeResolveSlot =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveSlot
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRDI)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandFixedBytes)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 56)))
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR11))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelResolve
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
tail)))))))))))
-- A scanned record (pointer, extent in scratch): scratch := extent + omitted
-- - 232, the bytes after its operand slots, refusing omitted > 168 or a
-- record shorter than its fixed part. field is dead afterwards.
def nativePhysicalNativeScanFixedPart =
(lambda unrestricted pointer : (family X86NativeRegister64) .
(lambda unrestricted scratch : (family X86NativeRegister64) .
(lambda unrestricted field : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64 field pointer (nativePhysicalNativeDisplacementByte (byte 56)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
field
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandOperandBytes)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd field scratch)
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
field
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandFixedBytes)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare field scratch)
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract field scratch)
tail))))))))))))
def nativePhysicalNativeResolveBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeResolveSlot
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolve
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR10)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveImmediate
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveResult
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 2)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveResultAddress
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 3)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveStateAddress
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 4)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveStateLoad
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 5)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolvePayloadAddress
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 6)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolvePayloadLoad
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 7)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveProcessArgument
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 8)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelResolveLoopAffine
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveImmediate
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveResult
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelResolveSlotValid
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveSlotValid
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeImmediate8 (byte 3)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRBX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveResultAddress
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelResolveResultAddressSlotValid
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveResultAddressSlotValid
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeImmediate8 (byte 3)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRBX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeDisplacementByte (byte 16)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveStateAddress
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 24)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelResolveStateAddressValid
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveStateAddressValid
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRBP)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveStateLoad
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 8)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 24)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveStateLoadValid
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRBP)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolvePayloadAddress
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelResolvePayloadAddressValid
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolvePayloadAddressValid
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolvePayloadLoad
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 8)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolvePayloadLoadValid
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveProcessArgument
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeImmediate8 (byte 3)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRSP)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeDisplacementByte (byte 16)))
(nativePhysicalNativeEmit
nativePhysicalNativeReturnInstruction
tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-- RSI is state extent and RAX is the result count. Compare with the remaining
-- capacity BEFORE shifting or adding; wrapped allocation lengths are never
-- passed to mmap. RDX/R10 are scratch until the following syscall setup.
-- scratchBytes is the interpreter scratch the caller derives (repeat frames
-- included), so the guard and the allocation reserve the same extent.
def nativePhysicalNativeMemoryGuard =
(lambda unrestricted scratchBytes : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate64
(constructor X86NativeRegister64 X86NativeRDX)
nativePhysicalNativeI64NegativeOne)
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR10)
(x86NativeImmediate32FromNatural scratchBytes))
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract
(constructor X86NativeRegister64 X86NativeR10)
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRDX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalFormat
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeShiftRightImmediate64
(constructor X86NativeRegister64 X86NativeRDX)
(nativePhysicalNativeImmediate8 (nat-to-byte nativePhysicalMemoryWordShift)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRDX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalFormat
tail)))))))))))
def nativePhysicalNativeMainBlockForDepth =
(lambda unrestricted maximumDepth : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelEntry
(nativePhysicalNativeLEA
(constructor X86NativeRegister64 X86NativeR15)
nativePhysicalNativeLabelImage
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR15)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate64
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeImmediate64 (byte 65) (byte 76) (byte 80) (byte 88) (byte 76) (byte 90) (byte 48) (byte 49)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelUnpack
(nativePhysicalNativeLabel
nativePhysicalNativeLabelImageReady
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR15)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate64
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeImmediate64
(byte 65)
(byte 76)
(byte 80)
(byte 88)
(byte 80) (byte 72) (byte 89) (byte 52)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelFatalFormat
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR15)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 4)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelFatalFormat
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR13)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 16)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR15)
(constructor X86NativeRegister64 X86NativeR14))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeI32Byte (byte 176)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeR12))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 40)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR12))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 24)))
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelFatalFormat
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeMemoryGuard
(nativePhysicalRepeatScratchBytes maximumDepth)
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeImmediate8
(nat-to-byte nativePhysicalMemoryWordShift)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRSI)
(x86NativeImmediate32FromNatural
(nativePhysicalRepeatScratchBytes maximumDepth)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 9)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDX)
(nativePhysicalNativeI32Byte (byte 3)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 34)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate64
(constructor X86NativeRegister64 X86NativeR8)
nativePhysicalNativeI64NegativeOne)
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR9)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelFatalSystemCall
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRBP))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRBP)
(constructor X86NativeRegister64 X86NativeRBX))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 24)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRBX))
(nativePhysicalNativeJump
nativePhysicalNativeLabelLoop
tail))))))))))))))))))))))))))))))))))))))))))))
-- Float64 (tags 14 .. 21, Runtime.NativePhysicalImage.
-- nativePhysicalImageFloat64Tag): operand 1's and operand 2's words into
-- xmm0 and xmm1 (the resolver touches no XMM register, so the left word
-- waits there while the right one resolves: either may read the
-- destination), the operation, the result's word (binary32: the low word,
-- zero-extended) into the address operand 0 resolves to (in rsi, which the
-- resolver leaves). Each tag has its own entry, all alike but for the
-- operation's instructions.
def npXMM0 : (family X86NativeRegisterXMM) =
(constructor X86NativeRegisterXMM X86NativeXMM0)
def npXMM1 : (family X86NativeRegisterXMM) =
(constructor X86NativeRegisterXMM X86NativeXMM1)
-- an operation on xmm0 and xmm1, its result's word left in rax
def npScalarDouble =
(lambda unrestricted operation : (family X86NativeScalarDoubleOperation) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeScalarDouble operation npXMM0 npXMM1)
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMoveFromXMM64
(constructor X86NativeRegister64 X86NativeRAX)
npXMM0)
tail))))
def npFromNatural =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMoveFromXMM64
(constructor X86NativeRegister64 X86NativeRAX)
npXMM0)
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeScalarDoubleFromInteger64
npXMM0
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMoveFromXMM64
(constructor X86NativeRegister64 X86NativeRAX)
npXMM0)
tail))))
def npToBinary32 =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeScalarDouble
(constructor X86NativeScalarDoubleOperation X86NativeScalarDoubleToSingle)
npXMM0
npXMM0)
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMoveFromXMM32
(constructor X86NativeRegister64 X86NativeRAX)
npXMM0)
tail)))
def npFromBinary32 =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeScalarSingleToDouble npXMM0 npXMM0)
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMoveFromXMM64
(constructor X86NativeRegister64 X86NativeRAX)
npXMM0)
tail)))
-- `each tag operation rest` for every tag, in order
def nativePhysicalNativeFloat64Entries =
(lambda unrestricted each : (pi unrestricted tag : Byte . (pi unrestricted operation : (pi unrestricted after : (family X86NativeAssembly) . (family X86NativeAssembly)) . (pi unrestricted rest : (family X86NativeAssembly) . (family X86NativeAssembly)))) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(each
(byte 14)
(npScalarDouble (constructor X86NativeScalarDoubleOperation X86NativeScalarDoubleAdd))
(each
(byte 15)
(npScalarDouble
(constructor X86NativeScalarDoubleOperation X86NativeScalarDoubleSubtract))
(each
(byte 16)
(npScalarDouble
(constructor X86NativeScalarDoubleOperation X86NativeScalarDoubleMultiply))
(each
(byte 17)
(npScalarDouble
(constructor X86NativeScalarDoubleOperation X86NativeScalarDoubleDivide))
(each
(byte 18)
(npScalarDouble
(constructor X86NativeScalarDoubleOperation X86NativeScalarDoubleSquareRoot))
(each
(byte 19)
npFromNatural
(each (byte 20) npToBinary32 (each (byte 21) npFromBinary32 tail))))))))))
def nativePhysicalNativeFloat64Label =
(lambda unrestricted tag : Byte .
(bytes-append nativePhysicalNativeLabelDispatchFloat64 (bytes tag)))
-- in the dispatch: each tag to its entry
def nativePhysicalNativeFloat64Dispatch =
(nativePhysicalNativeFloat64Entries
(lambda unrestricted tag : Byte .
(lambda unrestricted operation : (pi unrestricted after : (family X86NativeAssembly) . (family X86NativeAssembly)) .
(lambda unrestricted rest : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte tag))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
(nativePhysicalNativeFloat64Label tag)
rest))))))
def nativePhysicalNativeRepeatEndWhenDispatch =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 22)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchRepeatEndWhen
tail)))
def nativePhysicalNativeRepeatEndWhenScan =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 22)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelRepeatFound
tail)))
def nativePhysicalNativeSkipDispatch =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 23)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchSkip
tail)))
def nativePhysicalNativeLoopBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeR13)
(constructor X86NativeRegister64 X86NativeR13))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDone
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR12)
(constructor X86NativeRegister64 X86NativeR14))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelRecordEndValid
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalBounds
(nativePhysicalNativeLabel
nativePhysicalNativeLabelRecordEndValid
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (nat-to-byte nativePhysicalImageCommandHeaderBytes)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeLabel
nativePhysicalNativeLabelRecordExtentValid
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeR11))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR11))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR12)
(constructor X86NativeRegister64 X86NativeR11))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalBounds
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR10)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 40)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 48)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeRecordFixedPart
(constructor X86NativeRegister64 X86NativeR10)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR10)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 48)))
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeR10)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchSystemCall
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 2)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchCopy
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 3)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchRoutine
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 4)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchFence
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 5)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchTelemetry
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 6)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchAssert
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 7)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchHalt
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 8)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchAssertOneOf
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 9)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchRepeatBegin
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 10)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchRepeatEnd
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 11)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchStore
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 12)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchFenceWait
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 13)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelDispatchAdd
(nativePhysicalNativeSkipDispatch
(nativePhysicalNativeRepeatEndWhenDispatch
(nativePhysicalNativeFloat64Dispatch
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalRecord
tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
def nativePhysicalNativeSystemCallBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchSystemCall
(nativePhysicalNativeResolveCall
(byte 64)
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240))
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeResolveCall
(byte 112)
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeResolveCall
(byte 136)
(constructor X86NativeRegister64 X86NativeRDX)
(nativePhysicalNativeResolveCall
(byte 160)
(constructor X86NativeRegister64 X86NativeRCX)
(nativePhysicalNativeResolveCall
(byte 184)
(constructor X86NativeRegister64 X86NativeR8)
(nativePhysicalNativeResolveCall
(byte 208)
(constructor X86NativeRegister64 X86NativeR9)
(nativePhysicalNativeResolveCall
(byte 88)
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeJump nativePhysicalNativeLabelBindResult tail)))))))))))))))
def nativePhysicalNativeBindBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelBindResult
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 16)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelAdvance
(nativePhysicalNativeEmit
(nativePhysicalNativeCompareImmediate
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelBindStore
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeLabel
nativePhysicalNativeLabelBindStore
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 24)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionBelow)
nativePhysicalNativeLabelBindSlotValid
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeLabel
nativePhysicalNativeLabelBindSlotValid
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeImmediate8 (byte 3)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRBX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRAX)
nativePhysicalNativeD0
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
tail)))))))))))))))))))
def nativePhysicalNativeCopyBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchCopy
(nativePhysicalNativeResolveCall
(byte 88)
(constructor X86NativeRegister64 X86NativeRCX)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeR9))
(nativePhysicalNativeResolveCall
(byte 64)
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeR9)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR15)
(nativePhysicalNativeDisplacementByte (byte 24)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeR10))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRBP)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelCopyDone
(nativePhysicalNativeLabel
nativePhysicalNativeLabelCopyLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad8
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSI)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore8
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD0
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRCX)
nativePhysicalNativeI32NegativeOne)
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelCopyLoop
(nativePhysicalNativeLabel
nativePhysicalNativeLabelCopyDone
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
tail)))))))))))))))))))))))))))))
def nativePhysicalNativeRoutineBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchRoutine
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
-- Keep the routine address below the return-address slot used
-- by the resolver calls. byte 240 encodes -16; byte 248 was
-- -8 and was overwritten by each call instruction.
(nativePhysicalNativeNegativeDisplacementByte (byte 240))
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeResolveCall
(byte 88)
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeResolveCall
(byte 112)
(constructor X86NativeRegister64 X86NativeRDX)
(nativePhysicalNativeResolveCall
(byte 136)
(constructor X86NativeRegister64 X86NativeRCX)
(nativePhysicalNativeResolveCall
(byte 160)
(constructor X86NativeRegister64 X86NativeR8)
(nativePhysicalNativeResolveCall
(byte 184)
(constructor X86NativeRegister64 X86NativeR9)
(nativePhysicalNativeResolveCall
(byte 64)
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeR11)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCall
(constructor X86NativeRegister64 X86NativeR11))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeJump nativePhysicalNativeLabelBindResult tail)))))))))))))))
def nativePhysicalNativeFenceBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchFence
(nativePhysicalNativeResolveCall
(byte 112)
(constructor X86NativeRegister64 X86NativeRCX)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240))
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeResolveCall
(byte 88)
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 248))
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeResolveCall
(byte 64)
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 248)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240)))
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFenceLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelFenceDone
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRCX)
nativePhysicalNativeI32NegativeOne)
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelFenceLoop
(nativePhysicalNativeJump
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFenceDone
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
tail)))))))))))))))))))))
def nativePhysicalNativeAssertBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchAssert
(nativePhysicalNativeResolveCall
(byte 88)
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240))
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeResolveCall
(byte 64)
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeJump nativePhysicalNativeLabelAdvance tail)))))))))
def nativePhysicalNativeAssertOneOfBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchAssertOneOf
(nativePhysicalNativeResolveCall
(byte 112)
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 232))
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeResolveCall
(byte 88)
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240))
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeResolveCall
(byte 64)
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelAdvance
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 232)))
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeJump nativePhysicalNativeLabelAdvance tail))))))))))))))
def nativePhysicalNativeTelemetryBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchTelemetry
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 232))
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 9)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDX)
(nativePhysicalNativeI32Byte (byte 3)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeI32Byte (byte 34)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate64
(constructor X86NativeRegister64 X86NativeR8)
nativePhysicalNativeI64NegativeOne)
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR9)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 248))
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDI))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeLabel
nativePhysicalNativeLabelTelemetryCopyLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad8
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSI)
nativePhysicalNativeD0)
(nativePhysicalNativeEmit
(nativePhysicalNativeStore8
(constructor X86NativeRegister64 X86NativeRDI)
nativePhysicalNativeD0
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRSI)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeRCX)
nativePhysicalNativeI32NegativeOne)
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRCX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelTelemetryCopyLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeImmediate32
(byte 1)
(byte 1)
(byte 0)
(byte 0)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate64
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeImmediate64
(byte 156)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 248)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDX)
(nativePhysicalNativeImmediate32
(byte 65)
(byte 4)
(byte 0)
(byte 0)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeR10)
(nativePhysicalNativeImmediate32
(byte 164)
(byte 1)
(byte 0)
(byte 0)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeStore64
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240))
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRCX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRDX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 40)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRDI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 240)))
(nativePhysicalNativeLabel
nativePhysicalNativeLabelTelemetryWriteLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionZero)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRDX)
(constructor X86NativeRegister64 X86NativeRDX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelTelemetryWriteLoop
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 75)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 3)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 11)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRDI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 248)))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeRSP)
(nativePhysicalNativeNegativeDisplacementByte (byte 232)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeTest
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRAX))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionSign)
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
tail)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
def nativePhysicalNativeAdvanceBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelAdvance
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
nativePhysicalNativeD8)
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14))
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate
(constructor X86NativeRegister64 X86NativeR13)
nativePhysicalNativeI32NegativeOne)
(nativePhysicalNativeJump nativePhysicalNativeLabelLoop tail))))))
def nativePhysicalNativeDoneBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDone
(nativePhysicalNativeEmit
(nativePhysicalNativeCompare
(constructor X86NativeRegister64 X86NativeR12)
(constructor X86NativeRegister64 X86NativeR14))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionNotZero)
nativePhysicalNativeLabelFatalBounds
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeJump nativePhysicalNativeLabelExit tail))))))
def nativePhysicalNativeHaltBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchHalt
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 0)))
(nativePhysicalNativeJump nativePhysicalNativeLabelExit tail))))
def nativePhysicalNativeCommandFailureBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeEmit
(nativePhysicalNativeMove
(constructor X86NativeRegister64 X86NativeR14)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativePayloadBase
(constructor X86NativeRegister64 X86NativeRSI)
(constructor X86NativeRegister64 X86NativeR11)
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 32)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 40)))
(nativePhysicalNativeEmit
(nativePhysicalNativeAdd
(constructor X86NativeRegister64 X86NativeRAX)
(constructor X86NativeRegister64 X86NativeRSI))
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad64
(constructor X86NativeRegister64 X86NativeRDX)
(constructor X86NativeRegister64 X86NativeR14)
(nativePhysicalNativeDisplacementByte (byte 48)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 1)))
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 2)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 120)))
(nativePhysicalNativeJump nativePhysicalNativeLabelExit tail))))))))))))))
def nativePhysicalNativeFatalBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalFormat
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 101)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalBounds
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 102)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalOperand
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 103)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalSystemCall
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 104)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalAssertion
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 105)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalFence
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 106)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalTelemetry
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 107)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 108)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFatalUnpack
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRDI)
(nativePhysicalNativeI32Byte (byte 109)))
(nativePhysicalNativeJump
nativePhysicalNativeLabelExit
(nativePhysicalNativeLabel
nativePhysicalNativeLabelExit
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
(constructor X86NativeRegister64 X86NativeRAX)
(nativePhysicalNativeI32Byte (byte 60)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
tail)))))))))))))))))))))))))))))))
-- One instruction per line for the repeat machinery.
def npRAX : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeRAX)
def npR10 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR10)
def npR11 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR11)
def npR12 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR12)
def npR13 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR13)
def npR14 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR14)
def npR15 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR15)
def npRBX : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeRBX)
def npRDI : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeRDI)
def npRSI : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeRSI)
def npRDX : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeRDX)
def npZero : (family X86NativeCondition) =
(constructor X86NativeCondition X86NativeConditionZero)
def npNotZero : (family X86NativeCondition) =
(constructor X86NativeCondition X86NativeConditionNotZero)
def npBelow : (family X86NativeCondition) =
(constructor X86NativeCondition X86NativeConditionBelow)
def npD =
(lambda unrestricted value : Byte . (nativePhysicalNativeDisplacementByte value))
def npMove =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeMove source destination) tail))))
def npAdd =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeAdd source destination) tail))))
def npAddImmediate =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate32) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeAddImmediate destination immediate) tail))))
-- flags from left - right
def npCompare =
(lambda unrestricted left : (family X86NativeRegister64) .
(lambda unrestricted right : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeCompare right left) tail))))
def npCompareImmediate =
(lambda unrestricted left : (family X86NativeRegister64) .
(lambda unrestricted immediate : (family X86NativeImmediate32) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeCompareImmediate left immediate) tail))))
def npTest =
(lambda unrestricted register : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeTest register register) tail)))
def npLoad64 =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : (family X86NativeDisplacement32) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeLoad64 destination base displacement) tail)))))
def npStore64 =
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : (family X86NativeDisplacement32) .
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeStore64 base displacement source) tail)))))
def npClear =
(lambda unrestricted register : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (constructor X86NativeInstruction X86NativeClear32 register) tail)))
-- The scratch follows 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. Nested programs add
-- a depth word and the exact command-tree maximum number of saved frames.
-- The scratch address is rbx + 8 * resultSlots, computed into the register.
def npScratchInto =
(lambda unrestricted register : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(npLoad64
register
npR15
(npD (byte 32))
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft register (nativePhysicalNativeImmediate8 (byte 3)))
(npAdd register npRBX tail)))))
-- RepeatBegin: push the enclosing frame, then 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) or RepeatEndWhen (tag
-- 22); a nested RepeatBegin (tag 9) deepens the scan. Running off the image
-- is a malformed record. A count of zero skips the body, nested bodies
-- included: the records left lose the body's and this one, the frame is
-- popped, and the advance steps past the end -- so a count read from the
-- state makes a block conditional.
-- Both forward branches and repeat-boundary search traverse unexecuted
-- records. Validate before every load/advance: malformed extents must fail,
-- never wrap the cursor or leave a zero-length scan spinning indefinitely.
-- Registers are distinct; pointer and extent survive, scratch/field are dead.
def nativePhysicalNativeScanRecord =
(lambda unrestricted pointer : (family X86NativeRegister64) .
(lambda unrestricted extent : (family X86NativeRegister64) .
(lambda unrestricted scratch : (family X86NativeRegister64) .
(lambda unrestricted field : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(npCompare
npR12
pointer
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalBounds
(npMove
scratch
npR12
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract pointer scratch)
(npCompareImmediate
scratch
(nativePhysicalNativeI32Byte
(nat-to-byte nativePhysicalImageCommandHeaderBytes))
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(npLoad64
extent
pointer
nativePhysicalNativeD8
(npCompareImmediate
extent
(nativePhysicalNativeI32Byte
(nat-to-byte nativePhysicalImageCommandHeaderBytes))
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(npCompare
scratch
extent
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalBounds
(npMove
scratch
extent
(nativePhysicalNativeScanFixedPart
pointer
scratch
field
(npLoad64
field
pointer
(npD (byte 32))
(npCompare
scratch
field
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract field scratch)
(npLoad64
field
pointer
(npD (byte 40))
(npCompare
scratch
field
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract field scratch)
(npLoad64
field
pointer
(npD (byte 48))
(npCompare
scratch
field
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract field scratch)
(npTest
scratch
(nativePhysicalNativeJumpCondition
npNotZero
nativePhysicalNativeLabelFatalRecord
(npLoad64
field
pointer
nativePhysicalNativeD0
(npCompareImmediate
field
(nativePhysicalNativeI32Byte (byte 1))
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(npCompareImmediate
field
(nativePhysicalNativeI32Byte (byte 23))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalRecord
tail)))))))))))))))))))))))))))))))))))))
-- Frame zero is the inactive context. Push saves the parent iteration,
-- count, first-body address and body-record count in private mapped scratch;
-- pop restores it. Consequently loop-affine operands always use the innermost
-- active iteration, and read zero again after the outermost repeat finishes.
-- The frame bound comes from the command tree, not a fixed nesting capacity.
def npRepeatPush =
(lambda unrestricted maximumDepth : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nat-eliminate
(lambda unrestricted current : Nat . (family X86NativeAssembly))
(nativePhysicalNativeJump nativePhysicalNativeLabelFatalRecord tail)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : (family X86NativeAssembly) .
(npScratchInto
npR10
(npLoad64
npR11
npR10
(x86NativeDisplacement32FromNatural nativePhysicalRepeatDepthAt)
(npCompareImmediate
npR11
(x86NativeImmediate32FromNatural maximumDepth)
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelFatalRecord
(npMove
npRDI
npR11
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMultiplyImmediate64
npRDI
(x86NativeImmediate32FromNatural nativePhysicalRepeatFrameBytes))
(npAdd
npRDI
npR10
(npAddImmediate
npRDI
(x86NativeImmediate32FromNatural nativePhysicalRepeatFramesAt)
(npLoad64
npRAX
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 0 8))
(npStore64
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 0 8))
npRAX
(npLoad64
npRAX
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 1 8))
(npStore64
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 1 8))
npRAX
(npLoad64
npRAX
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 2 8))
(npStore64
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 2 8))
npRAX
(npLoad64
npRAX
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 3 8))
(npStore64
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 3 8))
npRAX
(npAddImmediate
npR11
(x86NativeImmediate32FromNatural 1)
(npStore64
npR10
(x86NativeDisplacement32FromNatural
nativePhysicalRepeatDepthAt)
npR11
tail)))))))))))))))))))))
maximumDepth)))
def npRepeatPop =
(lambda unrestricted tail : (family X86NativeAssembly) .
(npScratchInto
npR10
(npLoad64
npR11
npR10
(x86NativeDisplacement32FromNatural nativePhysicalRepeatDepthAt)
(npTest
npR11
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelFatalRecord
(npAddImmediate
npR11
nativePhysicalNativeI32NegativeOne
(npStore64
npR10
(x86NativeDisplacement32FromNatural nativePhysicalRepeatDepthAt)
npR11
(npMove
npRDI
npR11
(nativePhysicalNativeEmit
(constructor
X86NativeInstruction
X86NativeMultiplyImmediate64
npRDI
(x86NativeImmediate32FromNatural nativePhysicalRepeatFrameBytes))
(npAdd
npRDI
npR10
(npAddImmediate
npRDI
(x86NativeImmediate32FromNatural nativePhysicalRepeatFramesAt)
(npLoad64
npRAX
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 0 8))
(npStore64
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 0 8))
npRAX
(npLoad64
npRAX
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 1 8))
(npStore64
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 1 8))
npRAX
(npLoad64
npRAX
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 2 8))
(npStore64
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 2 8))
npRAX
(npLoad64
npRAX
npRDI
(x86NativeDisplacement32FromNatural (naturalMultiply 3 8))
(npStore64
npR10
(x86NativeDisplacement32FromNatural (naturalMultiply 3 8))
npRAX
tail)))))))))))))))))))
-- Count the body records from RAX up to the matching end into R11. RDX is the
-- nesting depth inside the body: a begin deepens it, an end at depth zero is
-- the match. Every record is validated by nativePhysicalNativeScanRecord before
-- its tag or extent is used (RDI holds the extent, R8/R9 are its scratch), and
-- the count stays below the records left in R13.
def npRepeatScan =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelRepeatScan
(nativePhysicalNativeScanRecord
npRAX
npRDI
(constructor X86NativeRegister64 X86NativeR8)
(constructor X86NativeRegister64 X86NativeR9)
(npCompare
npRAX
npR12
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelRepeatScanNext
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeLabel
nativePhysicalNativeLabelRepeatScanNext
(npCompare
npR11
npR13
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelFatalRecord
(npLoad64
npRSI
npRAX
nativePhysicalNativeD0
(npCompareImmediate
npRSI
(nativePhysicalNativeI32Byte (byte 9))
(nativePhysicalNativeJumpCondition
npZero
b"repeat-scan-enter"
(npCompareImmediate
npRSI
(nativePhysicalNativeI32Byte (byte 10))
(nativePhysicalNativeJumpCondition
npZero
b"repeat-scan-end"
(npCompareImmediate
npRSI
(nativePhysicalNativeI32Byte (byte 22))
(nativePhysicalNativeJumpCondition
npZero
b"repeat-scan-end"
(nativePhysicalNativeJump
b"repeat-scan-advance"
(nativePhysicalNativeLabel
b"repeat-scan-enter"
(npAddImmediate
npRDX
(nativePhysicalNativeI32Byte (byte 1))
(nativePhysicalNativeJump
b"repeat-scan-advance"
(nativePhysicalNativeLabel
b"repeat-scan-end"
(npTest
npRDX
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelRepeatFound
(npAddImmediate
npRDX
nativePhysicalNativeI32NegativeOne
(nativePhysicalNativeLabel
b"repeat-scan-advance"
(npAddImmediate
npR11
(nativePhysicalNativeI32Byte (byte 1))
(npAdd
npRAX
npRDI
(nativePhysicalNativeJump
nativePhysicalNativeLabelRepeatScan
tail)))))))))))))))))))))))))))))
-- A zero count skips through the matching end, including nested bodies.
def nativePhysicalNativeRepeatBeginBlockForDepth =
(lambda unrestricted maximumDepth : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchRepeatBegin
(npRepeatPush
maximumDepth
(nativePhysicalNativeResolveCall
(byte 64)
npRAX
(npScratchInto
npR10
(npStore64
npR10
(x86NativeDisplacement32FromNatural 8)
npRAX
(npClear
npR11
(npStore64
npR10
(x86NativeDisplacement32FromNatural 0)
npR11
(npLoad64
npRAX
npR14
nativePhysicalNativeD8
(npAdd
npRAX
npR14
(npStore64
npR10
(x86NativeDisplacement32FromNatural 16)
npRAX
(npClear
npRDX
(npRepeatScan
(nativePhysicalNativeLabel
nativePhysicalNativeLabelRepeatFound
(npStore64
npR10
(x86NativeDisplacement32FromNatural 24)
npR11
(npLoad64
npRDI
npR10
(x86NativeDisplacement32FromNatural 8)
(npTest
npRDI
(nativePhysicalNativeJumpCondition
npNotZero
nativePhysicalNativeLabelAdvance
(nativePhysicalNativeEmit
(nativePhysicalNativeSubtract npR11 npR13)
(npAddImmediate
npR13
nativePhysicalNativeI32NegativeOne
(npMove
npR14
npRAX
(npRepeatPop
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
tail))))))))))))))))))))))))
-- RepeatEnd: one more iteration done; while iterations remain, continue at
-- the first body record with the body's records (plus this end) still to
-- count, otherwise advance past the end.
-- Resolution scratches RAX/R10/R11; XMM0 preserves the first word while
-- resolving the second. Equality exits the bounded loop through the end's
-- frame pop; otherwise the existing end operation advances its counter and
-- enforces the original cap.
def nativePhysicalNativeRepeatEndWhenBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchRepeatEndWhen
(nativePhysicalNativeResolveCall
(byte 64)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveToXMM64 npXMM0 npR11)
(nativePhysicalNativeResolveCall
(byte 88)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveFromXMM64 npRAX npXMM0)
(npCompare
npRAX
npR11
(nativePhysicalNativeJumpCondition
npZero
b"repeat-leave"
(nativePhysicalNativeJump nativePhysicalNativeLabelDispatchRepeatEnd tail)))))))))
def nativePhysicalNativeRepeatEndBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchRepeatEnd
(npScratchInto
npR10
(npLoad64
npR11
npR10
(x86NativeDisplacement32FromNatural nativePhysicalRepeatDepthAt)
(npTest
npR11
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelFatalRecord
(npLoad64
npR11
npR10
(x86NativeDisplacement32FromNatural 0)
(npAddImmediate
npR11
(x86NativeImmediate32FromNatural 1)
(npStore64
npR10
(x86NativeDisplacement32FromNatural 0)
npR11
(npLoad64
npRAX
npR10
(x86NativeDisplacement32FromNatural 8)
(npCompare
npR11
npRAX
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelRepeatAgain
(nativePhysicalNativeLabel
b"repeat-leave"
(npRepeatPop
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
(nativePhysicalNativeLabel
nativePhysicalNativeLabelRepeatAgain
(npLoad64
npR14
npR10
(x86NativeDisplacement32FromNatural 16)
(npLoad64
npRAX
npR10
(x86NativeDisplacement32FromNatural 24)
(npAdd
npR13
npRAX
(nativePhysicalNativeJump
nativePhysicalNativeLabelLoop
tail))))))))))))))))))))
-- StoreWord64: the value of operand 1 into the address operand 0 resolves to.
-- The resolver scratches rax, r10 and r11, so the address is parked in rsi
-- (untouched by the resolver, dead between commands) while the value resolves.
def nativePhysicalNativeStoreBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchStore
(nativePhysicalNativeResolveCall
(byte 64)
npRSI
(nativePhysicalNativeResolveCall
(byte 88)
npR11
(npStore64
npRSI
nativePhysicalNativeD0
npR11
(nativePhysicalNativeJump nativePhysicalNativeLabelAdvance tail))))))
-- AddWord64: operand 1 plus operand 2 (modulo 2^64) into the address operand
-- 0 resolves to (in rsi, which the resolver leaves). The left value waits
-- in xmm0 while the right one resolves (the resolver touches no XMM
-- register), so either may read the destination.
def nativePhysicalNativeAddBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchAdd
(nativePhysicalNativeResolveCall
(byte 64)
npRSI
(nativePhysicalNativeResolveCall
(byte 88)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveToXMM64 npXMM0 npR11)
(nativePhysicalNativeResolveCall
(byte 112)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveFromXMM64 npRAX npXMM0)
(npAdd
npRAX
npR11
(npStore64
npRSI
nativePhysicalNativeD0
npRAX
(nativePhysicalNativeJump nativePhysicalNativeLabelAdvance tail))))))))))
def nativePhysicalNativeFloat64Block =
(nativePhysicalNativeFloat64Entries
(lambda unrestricted tag : Byte .
(lambda unrestricted operation : (pi unrestricted after : (family X86NativeAssembly) . (family X86NativeAssembly)) .
(lambda unrestricted rest : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
(nativePhysicalNativeFloat64Label tag)
(nativePhysicalNativeResolveCall
(byte 64)
npRSI
(nativePhysicalNativeResolveCall
(byte 88)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveToXMM64 npXMM0 npR11)
(nativePhysicalNativeResolveCall
(byte 112)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveToXMM64 npXMM1 npR11)
(operation
(npStore64
npRSI
nativePhysicalNativeD0
npRAX
(nativePhysicalNativeJump nativePhysicalNativeLabelAdvance rest)))))))))))))
-- LoopAffine: base + iteration * stride, the product by repeated addition.
-- rdi holds the descriptor; rax, r10 and r11 are the resolver's scratch
def nativePhysicalNativeResolveLoopAffineBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveLoopAffine
(npLoad64
npRAX
npRDI
nativePhysicalNativeD8
(npLoad64
npR11
npRDI
(npD (byte 16))
(npScratchInto
npR10
(npLoad64
npR10
npR10
nativePhysicalNativeD0
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveLoopAffineStep
(npTest
npR10
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelResolveLoopAffineDone
(npAdd
npRAX
npR11
(npAddImmediate
npR10
nativePhysicalNativeI32NegativeOne
(nativePhysicalNativeJump
nativePhysicalNativeLabelResolveLoopAffineStep
(nativePhysicalNativeLabel
nativePhysicalNativeLabelResolveLoopAffineDone
(nativePhysicalNativeEmit nativePhysicalNativeReturnInstruction tail))))))))))))))
-- FenceWait: resolve the address into r9, the expected value into rdx, the
-- poll bound into r8 and the interval into the scratch timespec, then load,
-- compare, nanosleep, count down. The resolver scratches rax, r10, r11 and
-- rdi; the system call scratches rax, rcx and r11; r8, r9 and rdx survive
-- both. A timeout is a command failure; only equality advances.
def npR8 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR8)
def npR9 : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeR9)
def nativePhysicalNativeFenceWaitBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchFenceWait
(nativePhysicalNativeResolveCall
(byte 64)
npR9
(nativePhysicalNativeResolveCall
(byte 88)
npRDX
(nativePhysicalNativeResolveCall
(byte 112)
npR8
(nativePhysicalNativeResolveCall
(byte 136)
npRAX
(npScratchInto
npR10
(npClear
npR11
(npStore64
npR10
(npD (byte 32))
npR11
(npStore64
npR10
(npD (byte 40))
npRAX
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFenceWaitLoop
(npLoad64
npRAX
npR9
nativePhysicalNativeD0
(npCompare
npRAX
npRDX
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelFenceWaitDone
(npMove
npRDI
npR10
(npAddImmediate
npRDI
(nativePhysicalNativeI32Byte (byte 32))
(npClear
npRSI
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32
npRAX
(nativePhysicalNativeI32Byte (byte 35)))
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(npAddImmediate
npR8
nativePhysicalNativeI32NegativeOne
(npTest
npR8
(nativePhysicalNativeJumpCondition
npNotZero
nativePhysicalNativeLabelFenceWaitLoop
(nativePhysicalNativeJump
nativePhysicalNativeLabelCommandFailure
(nativePhysicalNativeLabel
nativePhysicalNativeLabelFenceWaitDone
(nativePhysicalNativeJump
nativePhysicalNativeLabelAdvance
tail)))))))))))))))))))))))))
-- A forward branch consumes record boundaries without evaluating skipped
-- operands or touching the active repeat frame. Recheck count, extents and
-- isolated repeat balance before advancing; malformed images cannot turn a
-- skip into an out-of-image load or cross a loop boundary. R9 is the nesting
-- depth inside the window: complete (possibly nested) loops may be skipped.
def nativePhysicalNativeSkipBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelDispatchSkip
(nativePhysicalNativeResolveCall
(byte 64)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveToXMM64 npXMM0 npR11)
(nativePhysicalNativeResolveCall
(byte 88)
npR11
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeMoveFromXMM64 npRAX npXMM0)
(npCompare
npRAX
npR11
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelAdvance
(nativePhysicalNativeResolveCall
(byte 112)
npR8
(npMove
npRAX
npR13
(npAddImmediate
npRAX
nativePhysicalNativeI32NegativeOne
(npCompare
npRAX
npR8
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(npClear
npR9
(nativePhysicalNativeLabel
b"np-skip-scan"
(npLoad64
npRAX
npR14
nativePhysicalNativeD8
(npAdd
npR14
npRAX
(npAddImmediate
npR13
nativePhysicalNativeI32NegativeOne
(npTest
npR8
(nativePhysicalNativeJumpCondition
npZero
b"np-skip-done"
(nativePhysicalNativeScanRecord
npR14
npR11
npRAX
npR10
(npLoad64
npRAX
npR14
nativePhysicalNativeD0
(npCompareImmediate
npRAX
(nativePhysicalNativeI32Byte (byte 1))
(nativePhysicalNativeJumpCondition
npBelow
nativePhysicalNativeLabelFatalRecord
(npCompareImmediate
npRAX
(nativePhysicalNativeI32Byte (byte 23))
(nativePhysicalNativeJumpCondition
(constructor X86NativeCondition X86NativeConditionAbove)
nativePhysicalNativeLabelFatalRecord
(npCompareImmediate
npRAX
(nativePhysicalNativeI32Byte (byte 9))
(nativePhysicalNativeJumpCondition
npZero
b"np-skip-begin"
(npCompareImmediate
npRAX
(nativePhysicalNativeI32Byte (byte 10))
(nativePhysicalNativeJumpCondition
npZero
b"np-skip-end"
(npCompareImmediate
npRAX
(nativePhysicalNativeI32Byte (byte 22))
(nativePhysicalNativeJumpCondition
npZero
b"np-skip-end"
(nativePhysicalNativeJump
b"np-skip-next"
(nativePhysicalNativeLabel
b"np-skip-begin"
(npAddImmediate
npR9
(nativePhysicalNativeI32Byte (byte 1))
(nativePhysicalNativeJump
b"np-skip-next"
(nativePhysicalNativeLabel
b"np-skip-end"
(npTest
npR9
(nativePhysicalNativeJumpCondition
npZero
nativePhysicalNativeLabelFatalRecord
(npAddImmediate
npR9
nativePhysicalNativeI32NegativeOne
(nativePhysicalNativeLabel
b"np-skip-next"
(npAddImmediate
npR8
nativePhysicalNativeI32NegativeOne
(nativePhysicalNativeJump
b"np-skip-scan"
(nativePhysicalNativeLabel
b"np-skip-done"
(npTest
npR9
(nativePhysicalNativeJumpCondition
npNotZero
nativePhysicalNativeLabelFatalRecord
(nativePhysicalNativeJump
nativePhysicalNativeLabelLoop
tail)))))))))))))))))))))))))))))))))))))))))))))))
-- ---- packed image ----
-- An executable whose image is packed (Runtime.NativePhysicalImagePlan:
-- ALPXLZ01, version 1, unpacked length U, packed length P, then P bytes of LZ
-- sequences) unpacks it once, before anything else runs, into the pages after
-- the file's last page: the load segment reserves them (Compiler.ELF). They
-- are writable while they are written and read+execute afterwards, never
-- both. Every literal and match is bounded by the stream and by U; a match's
-- distance reaches at most back to the first unpacked byte; the output must
-- be exactly U. Then R15 addresses the unpacked image and execution continues
-- exactly as for an image stored in place. RSP is untouched (process arguments
-- are read relative to it). Registers: RBX source, R8 source end, R14 output
-- start, RDI output, R9 output end, R10 mapped length, RCX token, RDX a
-- length, RAX/RSI/R11 scratch.
def npRCX : (family X86NativeRegister64) =
(constructor X86NativeRegister64 X86NativeRCX)
def npSubtract =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit (nativePhysicalNativeSubtract source destination) tail))))
def npLoad8 =
(lambda unrestricted destination : (family X86NativeRegister64) .
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted displacement : Byte .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeLoad8 destination base (nativePhysicalNativeDisplacementByte displacement))
tail)))))
def npStore8 =
(lambda unrestricted base : (family X86NativeRegister64) .
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeStore8 base (nativePhysicalNativeDisplacementByte (byte 0)) source)
tail))))
def npImmediate =
(lambda unrestricted register : (family X86NativeRegister64) .
(lambda unrestricted value : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeMoveImmediate32 register (x86NativeImmediate32FromNatural value))
tail))))
def npStep =
(lambda unrestricted register : (family X86NativeRegister64) .
(lambda unrestricted value : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeEmit
(nativePhysicalNativeAddImmediate register (x86NativeImmediate32FromNatural value))
tail))))
-- register := (register + 4095) & -4096
def npPageRound =
(lambda unrestricted register : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(npStep
register
4095
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeAndImmediate64 register (x86NativeImmediate32FromNatural 4294963200))
tail))))
def npJumpIf =
(lambda unrestricted condition : (family X86NativeCondition) .
(lambda unrestricted label : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeJumpCondition condition label tail))))
-- mprotect(R14, R10, protection); any error refuses
def npProtectUnpacked =
(lambda unrestricted protection : Nat .
(lambda unrestricted tail : (family X86NativeAssembly) .
(npImmediate npRAX 10
(npMove npRDI npR14
(npMove npRSI npR10
(npImmediate npRDX protection
(nativePhysicalNativeEmit
nativePhysicalNativeSystemCallInstruction
(npTest npRAX
(npJumpIf npNotZero nativePhysicalNativeLabelFatalUnpack tail)))))))))
-- A length continued in bytes of 255 and a final remainder, added to RDX.
-- `next` is this loop's label, `done` where it continues; RAX is scratch.
def npUnpackLength =
(lambda unrestricted next : Bytes .
(lambda unrestricted byteLabel : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
next
(npCompare npRBX npR8
(npJumpIf npBelow byteLabel
(nativePhysicalNativeJump
nativePhysicalNativeLabelFatalUnpack
(nativePhysicalNativeLabel
byteLabel
(npLoad8 npR11 npRBX (byte 0)
(npStep npRBX 1
(npAdd npRDX npR11
(npCompareImmediate npR11 (nativePhysicalNativeI32Byte (byte 255))
(npJumpIf npZero next tail)))))))))))))
-- Copy RDX bytes from `source` to RDI, advancing both; then continue at `done`.
def npUnpackCopy =
(lambda unrestricted source : (family X86NativeRegister64) .
(lambda unrestricted loop : Bytes .
(lambda unrestricted done : Bytes .
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
loop
(npTest npRDX
(npJumpIf npZero done
(npLoad8 npR11 source (byte 0)
(npStore8 npRDI npR11
(npStep source 1
(npStep npRDI 1
(npStep npRDX 4294967295
(nativePhysicalNativeJump loop tail)))))))))))))
-- RSI := `limit` - `position`; refuse when it is below RDX
def npUnpackRoom =
(lambda unrestricted limit : (family X86NativeRegister64) .
(lambda unrestricted position : (family X86NativeRegister64) .
(lambda unrestricted tail : (family X86NativeAssembly) .
(npMove npRSI limit
(npSubtract npRSI position
(npCompare npRSI npRDX
(npJumpIf npBelow nativePhysicalNativeLabelFatalUnpack tail)))))))
def nativePhysicalNativeUnpackBlock =
(lambda unrestricted tail : (family X86NativeAssembly) .
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpack
(npLoad64 npRAX npR15 nativePhysicalNativeD8
(npCompareImmediate npRAX (nativePhysicalNativeI32Byte (byte 1))
(npJumpIf npNotZero nativePhysicalNativeLabelFatalUnpack
(npLoad64 npR13 npR15 (npD (byte 16))
(npLoad64 npR12 npR15 (npD (byte 24))
(npTest npR13
(npJumpIf npZero nativePhysicalNativeLabelFatalUnpack
-- source and its end; a packed length that wraps refuses
(npMove npRBX npR15
(npStep npRBX 32
(npMove npR8 npRBX
(npAdd npR8 npR12
(npCompare npR8 npRBX
(npJumpIf npBelow nativePhysicalNativeLabelFatalUnpack
-- output: the page after the file's last page, U page-rounded
(npMove npR14 npR8
(npPageRound npR14
(npMove npR10 npR13
(npPageRound npR10
(npCompare npR10 npR13
(npJumpIf npBelow nativePhysicalNativeLabelFatalUnpack
(npProtectUnpacked 3
(npMove npRDI npR14
(npMove npR9 npR14
(npAdd npR9 npR13
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpackSequence
(npCompare npRBX npR8
(npJumpIf npBelow nativePhysicalNativeLabelUnpackToken
(nativePhysicalNativeJump
nativePhysicalNativeLabelUnpackEnd
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpackToken
(npLoad8 npRCX npRBX (byte 0)
(npStep npRBX 1
-- literals: the token's high nibble, continued at 15
(npMove npRDX npRCX
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeShiftRightImmediate64 npRDX (nativePhysicalNativeImmediate8 (byte 4)))
(npCompareImmediate npRDX (nativePhysicalNativeI32Byte (byte 15))
(npJumpIf npNotZero nativePhysicalNativeLabelUnpackLiterals
(npUnpackLength
nativePhysicalNativeLabelUnpackLiteralLength
nativePhysicalNativeLabelUnpackLiteralByte
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpackLiterals
(npUnpackRoom npR8 npRBX
(npUnpackRoom npR9 npRDI
(npUnpackCopy
npRBX
nativePhysicalNativeLabelUnpackLiteralCopy
nativePhysicalNativeLabelUnpackLiteralsDone
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpackLiteralsDone
-- the last sequence ends with its literals
(npCompare npRBX npR8
(npJumpIf npZero nativePhysicalNativeLabelUnpackEnd
-- distance: two bytes, little-endian, 1 .. produced
(npImmediate npRDX 2
(npUnpackRoom npR8 npRBX
(npLoad8 npRAX npRBX (byte 0)
(npLoad8 npRSI npRBX (byte 1)
(nativePhysicalNativeEmit
(nativePhysicalNativeShiftLeft npRSI (nativePhysicalNativeImmediate8 (byte 8)))
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeOrRegister64 npRSI npRAX)
(npStep npRBX 2
(npTest npRAX
(npJumpIf npZero nativePhysicalNativeLabelFatalUnpack
(npMove npRSI npRDI
(npSubtract npRSI npR14
(npCompare npRSI npRAX
(npJumpIf npBelow nativePhysicalNativeLabelFatalUnpack
-- match length: the low nibble plus 4, continued at 15
(npMove npRDX npRCX
(nativePhysicalNativeEmit
(constructor X86NativeInstruction X86NativeAndImmediate64 npRDX (x86NativeImmediate32FromNatural 15))
(npCompareImmediate npRDX (nativePhysicalNativeI32Byte (byte 15))
(npJumpIf npNotZero nativePhysicalNativeLabelUnpackMatch
(npUnpackLength
nativePhysicalNativeLabelUnpackMatchLength
nativePhysicalNativeLabelUnpackMatchByte
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpackMatch
(npStep npRDX 4
(npUnpackRoom npR9 npRDI
(npMove npRSI npRDI
(npSubtract npRSI npRAX
(npUnpackCopy
npRSI
nativePhysicalNativeLabelUnpackMatchCopy
nativePhysicalNativeLabelUnpackSequence
(nativePhysicalNativeLabel
nativePhysicalNativeLabelUnpackEnd
(npCompare npRDI npR9
(npJumpIf npNotZero nativePhysicalNativeLabelFatalUnpack
(npProtectUnpacked 5
(npMove npR15 npR14
(nativePhysicalNativeJump
nativePhysicalNativeLabelImageReady
tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-- Low-level assembly construction. Artifact owners must admit the derived
-- scratch extent before encoding its signed immediate (see NativeELF).
def nativePhysicalNativeAssemblyForDepth =
(lambda unrestricted maximumDepth : Nat .
(nativePhysicalNativeMainBlockForDepth
maximumDepth
(nativePhysicalNativeUnpackBlock
(nativePhysicalNativeLoopBlock
(nativePhysicalNativeSystemCallBlock
(nativePhysicalNativeBindBlock
(nativePhysicalNativeCopyBlock
(nativePhysicalNativeRoutineBlock
(nativePhysicalNativeFenceBlock
(nativePhysicalNativeTelemetryBlock
(nativePhysicalNativeAssertBlock
(nativePhysicalNativeAssertOneOfBlock
(nativePhysicalNativeRepeatBeginBlockForDepth
maximumDepth
(nativePhysicalNativeRepeatEndWhenBlock
(nativePhysicalNativeRepeatEndBlock
(nativePhysicalNativeStoreBlock
(nativePhysicalNativeAddBlock
(nativePhysicalNativeFloat64Block
(nativePhysicalNativeResolveLoopAffineBlock
(nativePhysicalNativeFenceWaitBlock
(nativePhysicalNativeAdvanceBlock
(nativePhysicalNativeDoneBlock
(nativePhysicalNativeHaltBlock
(nativePhysicalNativeCommandFailureBlock
(nativePhysicalNativeResolveBlock
(nativePhysicalNativeSkipBlock
(nativePhysicalNativeFatalBlock
(constructor
X86NativeAssembly
X86NativeAssemblyLabel
nativePhysicalNativeLabelImage
(constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))))))))))))))))))))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.