The extent of the record nativePhysicalImageEncodeCommand writes for a
command: the fixed 232 bytes, the (aligned) payload, the auxiliary bytes and
the error identity -- the same fields, measured instead of written. Where a
MachineRoutine's code lands follows from these (see
nativePhysicalImageRecordAlignment).
1021def nativePhysicalImageCommandExtent =
1022 (lambda unrestricted command : (family NativePhysicalCommand) .
1023 (eliminate
1024 NativePhysicalCommand
1025 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
1026 command
1027 (branch NativePhysicalCommandValue operation errorIdentity .
1028 (naturalAdd nativePhysicalImageCommandFixedBytes
1029 (naturalAdd (bytes-length errorIdentity)
1030 (eliminate
1031 NativePhysicalOperation
1032 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
1033 operation
1034 (branch NativePhysicalSystemCall number arguments payload result .
1035 (naturalAdd (bytes-length payload) (nativePhysicalImageSystemCallPayloadPadding (bytes-length payload))))
1036 (branch NativePhysicalCopyPayloadToState destination extent payload . (bytes-length payload))
1037 (branch NativePhysicalMachineRoutine code arguments result . (bytes-length code))
1038 (branch NativePhysicalFencePoll address expected polls . zero)
1039 (branch NativePhysicalTelemetryAppend path record . (naturalAdd (bytes-length path) (bytes-length record)))
1040 (branch NativePhysicalAssertEqual left right error . (bytes-length (nativePhysicalErrorCodeBytes error)))
1041 (branch NativePhysicalAssertOneOf observed first second error . (bytes-length (nativePhysicalErrorCodeBytes error)))
1042 (branch NativePhysicalHaltSuccess . zero)
1043 (branch NativePhysicalRepeatBegin count . zero)
1044 (branch NativePhysicalRepeatEnd . zero)
1045 (branch NativePhysicalStoreWord64 destination value . zero)
1046 (branch NativePhysicalFenceWait address expected polls interval . zero)
1047 (branch NativePhysicalRepeatBeginCounted count . zero)
1048 (branch NativePhysicalAddWord64 destination left right . zero)
1049 (branch NativePhysicalFloat64 kind destination left right . zero)))))))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.