module Compiler.MachineAArch64 import Data.Bytes import Model.Config import Model.Word32 import Std.Byte import Std.Natural -- The Alpha-side mirror of bootstrap/haskell/.../Alpha/Target/AArch64.hs: the -- same A64 subset, encoded to the same bytes. Every instruction is one -- little-endian 32-bit word; fields never overlap, so a word is the sum of -- its opcode base and its shifted fields, and the sum is serialised through -- the checked Model.Word32 owner. Registers are X0-X30 by construction: -- there is no constructor for code 31, so SP/XZR cannot be named. Every -- range-limited operand is checked and a violation is a result, never a -- truncated field. family AArch64Register : Type 0 constructor AArch64X0 constructor AArch64X1 constructor AArch64X2 constructor AArch64X3 constructor AArch64X4 constructor AArch64X5 constructor AArch64X6 constructor AArch64X7 constructor AArch64X8 constructor AArch64X9 constructor AArch64X10 constructor AArch64X11 constructor AArch64X12 constructor AArch64X13 constructor AArch64X14 constructor AArch64X15 constructor AArch64X16 constructor AArch64X17 constructor AArch64X18 constructor AArch64X19 constructor AArch64X20 constructor AArch64X21 constructor AArch64X22 constructor AArch64X23 constructor AArch64X24 constructor AArch64X25 constructor AArch64X26 constructor AArch64X27 constructor AArch64X28 constructor AArch64X29 constructor AArch64X30 end-family -- The halfword a wide move writes: lsl #0, #16, #32 or #48. family AArch64HalfwordShift : Type 0 constructor AArch64Shift0 constructor AArch64Shift16 constructor AArch64Shift32 constructor AArch64Shift48 end-family -- Condition codes in encoding order; AL and NV are deliberately absent. family AArch64Condition : Type 0 constructor AArch64Equal constructor AArch64NotEqual constructor AArch64CarrySet constructor AArch64CarryClear constructor AArch64Minus constructor AArch64Plus constructor AArch64OverflowSet constructor AArch64OverflowClear constructor AArch64UnsignedHigher constructor AArch64UnsignedLowerOrSame constructor AArch64GreaterOrEqual constructor AArch64LessThan constructor AArch64GreaterThan constructor AArch64LessOrEqual end-family -- A PC-relative distance is a direction and a magnitude in bytes, measured -- from the referencing instruction itself. family AArch64Direction : Type 0 constructor AArch64Forward constructor AArch64Backward end-family -- An add/sub immediate is taken as is or shifted left by 12. family AArch64ImmediateShift : Type 0 constructor AArch64Unshifted constructor AArch64ShiftedBy12 end-family -- The scalar single-precision register file (Arm A-profile, FP data-processing -- and FMOV between the general and vector files). Unlike the general -- registers, code 31 names a real register here rather than the stack pointer -- or the zero register, so this family carries all thirty-two. family AArch64FloatRegister : Type 0 constructor AArch64S0 constructor AArch64S1 constructor AArch64S2 constructor AArch64S3 constructor AArch64S4 constructor AArch64S5 constructor AArch64S6 constructor AArch64S7 constructor AArch64S8 constructor AArch64S9 constructor AArch64S10 constructor AArch64S11 constructor AArch64S12 constructor AArch64S13 constructor AArch64S14 constructor AArch64S15 constructor AArch64S16 constructor AArch64S17 constructor AArch64S18 constructor AArch64S19 constructor AArch64S20 constructor AArch64S21 constructor AArch64S22 constructor AArch64S23 constructor AArch64S24 constructor AArch64S25 constructor AArch64S26 constructor AArch64S27 constructor AArch64S28 constructor AArch64S29 constructor AArch64S30 constructor AArch64S31 end-family family AArch64Instruction : Type 0 constructor AArch64MoveWideZero field unrestricted aarch64MoveWideZeroDestination : (family AArch64Register) field unrestricted aarch64MoveWideZeroValue : Nat field unrestricted aarch64MoveWideZeroShift : (family AArch64HalfwordShift) constructor AArch64MoveWideKeep field unrestricted aarch64MoveWideKeepDestination : (family AArch64Register) field unrestricted aarch64MoveWideKeepValue : Nat field unrestricted aarch64MoveWideKeepShift : (family AArch64HalfwordShift) constructor AArch64MoveRegister field unrestricted aarch64MoveRegisterDestination : (family AArch64Register) field unrestricted aarch64MoveRegisterSource : (family AArch64Register) constructor AArch64AddImmediate field unrestricted aarch64AddImmediateDestination : (family AArch64Register) field unrestricted aarch64AddImmediateSource : (family AArch64Register) field unrestricted aarch64AddImmediateValue : Nat constructor AArch64SubtractImmediate field unrestricted aarch64SubtractImmediateDestination : (family AArch64Register) field unrestricted aarch64SubtractImmediateSource : (family AArch64Register) field unrestricted aarch64SubtractImmediateValue : Nat constructor AArch64AddRegister field unrestricted aarch64AddRegisterDestination : (family AArch64Register) field unrestricted aarch64AddRegisterLeft : (family AArch64Register) field unrestricted aarch64AddRegisterRight : (family AArch64Register) constructor AArch64SubtractRegister field unrestricted aarch64SubtractRegisterDestination : (family AArch64Register) field unrestricted aarch64SubtractRegisterLeft : (family AArch64Register) field unrestricted aarch64SubtractRegisterRight : (family AArch64Register) constructor AArch64AndRegister field unrestricted aarch64AndRegisterDestination : (family AArch64Register) field unrestricted aarch64AndRegisterLeft : (family AArch64Register) field unrestricted aarch64AndRegisterRight : (family AArch64Register) constructor AArch64OrRegister field unrestricted aarch64OrRegisterDestination : (family AArch64Register) field unrestricted aarch64OrRegisterLeft : (family AArch64Register) field unrestricted aarch64OrRegisterRight : (family AArch64Register) constructor AArch64ExclusiveOrRegister field unrestricted aarch64ExclusiveOrRegisterDestination : (family AArch64Register) field unrestricted aarch64ExclusiveOrRegisterLeft : (family AArch64Register) field unrestricted aarch64ExclusiveOrRegisterRight : (family AArch64Register) constructor AArch64ShiftLeftImmediate field unrestricted aarch64ShiftLeftImmediateDestination : (family AArch64Register) field unrestricted aarch64ShiftLeftImmediateSource : (family AArch64Register) field unrestricted aarch64ShiftLeftImmediateAmount : Nat constructor AArch64ShiftRightImmediate field unrestricted aarch64ShiftRightImmediateDestination : (family AArch64Register) field unrestricted aarch64ShiftRightImmediateSource : (family AArch64Register) field unrestricted aarch64ShiftRightImmediateAmount : Nat constructor AArch64MultiplyRegister field unrestricted aarch64MultiplyRegisterDestination : (family AArch64Register) field unrestricted aarch64MultiplyRegisterLeft : (family AArch64Register) field unrestricted aarch64MultiplyRegisterRight : (family AArch64Register) constructor AArch64DivideRegisterUnsigned field unrestricted aarch64DivideRegisterUnsignedDestination : (family AArch64Register) field unrestricted aarch64DivideRegisterUnsignedLeft : (family AArch64Register) field unrestricted aarch64DivideRegisterUnsignedRight : (family AArch64Register) constructor AArch64CompareImmediate field unrestricted aarch64CompareImmediateRegister : (family AArch64Register) field unrestricted aarch64CompareImmediateValue : Nat constructor AArch64CompareRegister field unrestricted aarch64CompareRegisterLeft : (family AArch64Register) field unrestricted aarch64CompareRegisterRight : (family AArch64Register) constructor AArch64LoadMemory64 field unrestricted aarch64LoadMemory64Destination : (family AArch64Register) field unrestricted aarch64LoadMemory64Base : (family AArch64Register) field unrestricted aarch64LoadMemory64Offset : Nat constructor AArch64StoreMemory64 field unrestricted aarch64StoreMemory64Base : (family AArch64Register) field unrestricted aarch64StoreMemory64Offset : Nat field unrestricted aarch64StoreMemory64Source : (family AArch64Register) constructor AArch64LoadMemory32ZeroExtend field unrestricted aarch64LoadMemory32Destination : (family AArch64Register) field unrestricted aarch64LoadMemory32Base : (family AArch64Register) field unrestricted aarch64LoadMemory32Offset : Nat constructor AArch64StoreMemory32 field unrestricted aarch64StoreMemory32Base : (family AArch64Register) field unrestricted aarch64StoreMemory32Offset : Nat field unrestricted aarch64StoreMemory32Source : (family AArch64Register) constructor AArch64LoadMemory8ZeroExtend field unrestricted aarch64LoadMemory8Destination : (family AArch64Register) field unrestricted aarch64LoadMemory8Base : (family AArch64Register) field unrestricted aarch64LoadMemory8Offset : Nat constructor AArch64StoreMemory8 field unrestricted aarch64StoreMemory8Base : (family AArch64Register) field unrestricted aarch64StoreMemory8Offset : Nat field unrestricted aarch64StoreMemory8Source : (family AArch64Register) constructor AArch64AddressRelative field unrestricted aarch64AddressRelativeDestination : (family AArch64Register) field unrestricted aarch64AddressRelativeDirection : (family AArch64Direction) field unrestricted aarch64AddressRelativeDistance : Nat constructor AArch64Branch field unrestricted aarch64BranchDirection : (family AArch64Direction) field unrestricted aarch64BranchDistance : Nat constructor AArch64BranchLink field unrestricted aarch64BranchLinkDirection : (family AArch64Direction) field unrestricted aarch64BranchLinkDistance : Nat constructor AArch64BranchLinkRegister field unrestricted aarch64BranchLinkRegisterTarget : (family AArch64Register) constructor AArch64BranchIf field unrestricted aarch64BranchIfCondition : (family AArch64Condition) field unrestricted aarch64BranchIfDirection : (family AArch64Direction) field unrestricted aarch64BranchIfDistance : Nat constructor AArch64CompareBranchIfZero field unrestricted aarch64CompareBranchIfZeroRegister : (family AArch64Register) field unrestricted aarch64CompareBranchIfZeroDirection : (family AArch64Direction) field unrestricted aarch64CompareBranchIfZeroDistance : Nat constructor AArch64CompareBranchIfNotZero field unrestricted aarch64CompareBranchIfNotZeroRegister : (family AArch64Register) field unrestricted aarch64CompareBranchIfNotZeroDirection : (family AArch64Direction) field unrestricted aarch64CompareBranchIfNotZeroDistance : Nat constructor AArch64AddImmediateFromStackPointer field unrestricted aarch64AddFromStackDestination : (family AArch64Register) field unrestricted aarch64AddFromStackValue : Nat constructor AArch64AddStackPointer field unrestricted aarch64AddStackPointerValue : Nat field unrestricted aarch64AddStackPointerShift : (family AArch64ImmediateShift) constructor AArch64SubtractStackPointer field unrestricted aarch64SubtractStackPointerValue : Nat field unrestricted aarch64SubtractStackPointerShift : (family AArch64ImmediateShift) constructor AArch64LoadMemory64FromStack field unrestricted aarch64LoadFromStackDestination : (family AArch64Register) field unrestricted aarch64LoadFromStackOffset : Nat constructor AArch64StoreMemory64ToStack field unrestricted aarch64StoreToStackOffset : Nat field unrestricted aarch64StoreToStackSource : (family AArch64Register) constructor AArch64LoadMemory8FromStack field unrestricted aarch64LoadByteFromStackDestination : (family AArch64Register) field unrestricted aarch64LoadByteFromStackOffset : Nat constructor AArch64StoreMemory8ToStack field unrestricted aarch64StoreByteToStackOffset : Nat field unrestricted aarch64StoreByteToStackSource : (family AArch64Register) constructor AArch64Return constructor AArch64SupervisorCall -- Full-system completion before a following device/MMIO store. This is -- stronger than a compiler fence and is required by the native submit path. constructor AArch64DataSynchronizationBarrierSystem constructor AArch64FloatAdd32 field unrestricted aarch64FloatAdd32Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatAdd32Left : (family AArch64FloatRegister) field unrestricted aarch64FloatAdd32Right : (family AArch64FloatRegister) constructor AArch64FloatSubtract32 field unrestricted aarch64FloatSubtract32Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatSubtract32Left : (family AArch64FloatRegister) field unrestricted aarch64FloatSubtract32Right : (family AArch64FloatRegister) constructor AArch64FloatMultiply32 field unrestricted aarch64FloatMultiply32Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatMultiply32Left : (family AArch64FloatRegister) field unrestricted aarch64FloatMultiply32Right : (family AArch64FloatRegister) constructor AArch64FloatDivide32 field unrestricted aarch64FloatDivide32Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatDivide32Left : (family AArch64FloatRegister) field unrestricted aarch64FloatDivide32Right : (family AArch64FloatRegister) constructor AArch64FloatCompare32 field unrestricted aarch64FloatCompare32Left : (family AArch64FloatRegister) field unrestricted aarch64FloatCompare32Right : (family AArch64FloatRegister) constructor AArch64FloatMoveFromGeneral32 field unrestricted aarch64FloatMoveFromGeneral32Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatMoveFromGeneral32Source : (family AArch64Register) constructor AArch64FloatMoveToGeneral32 field unrestricted aarch64FloatMoveToGeneral32Destination : (family AArch64Register) field unrestricted aarch64FloatMoveToGeneral32Source : (family AArch64FloatRegister) constructor AArch64ReadFloatControl field unrestricted aarch64ReadFloatControlDestination : (family AArch64Register) constructor AArch64WriteFloatControl field unrestricted aarch64WriteFloatControlSource : (family AArch64Register) -- Scalar double precision: the same register file read as D registers (a D -- register and the S register of the same number share their low 32 bits). constructor AArch64FloatAdd64 field unrestricted aarch64FloatAdd64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatAdd64Left : (family AArch64FloatRegister) field unrestricted aarch64FloatAdd64Right : (family AArch64FloatRegister) constructor AArch64FloatSubtract64 field unrestricted aarch64FloatSubtract64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatSubtract64Left : (family AArch64FloatRegister) field unrestricted aarch64FloatSubtract64Right : (family AArch64FloatRegister) constructor AArch64FloatMultiply64 field unrestricted aarch64FloatMultiply64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatMultiply64Left : (family AArch64FloatRegister) field unrestricted aarch64FloatMultiply64Right : (family AArch64FloatRegister) constructor AArch64FloatDivide64 field unrestricted aarch64FloatDivide64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatDivide64Left : (family AArch64FloatRegister) field unrestricted aarch64FloatDivide64Right : (family AArch64FloatRegister) constructor AArch64FloatSquareRoot64 field unrestricted aarch64FloatSquareRoot64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatSquareRoot64Source : (family AArch64FloatRegister) -- scvtf Dd, Xn: the signed 64-bit integer as the nearest double constructor AArch64FloatFromSigned64 field unrestricted aarch64FloatFromSigned64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatFromSigned64Source : (family AArch64Register) -- fcvt Sd, Dn and fcvt Dd, Sn constructor AArch64FloatNarrow64To32 field unrestricted aarch64FloatNarrow64To32Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatNarrow64To32Source : (family AArch64FloatRegister) constructor AArch64FloatWiden32To64 field unrestricted aarch64FloatWiden32To64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatWiden32To64Source : (family AArch64FloatRegister) -- fmov Dd, Xn and fmov Xd, Dn: the 64 bits unchanged constructor AArch64FloatMoveFromGeneral64 field unrestricted aarch64FloatMoveFromGeneral64Destination : (family AArch64FloatRegister) field unrestricted aarch64FloatMoveFromGeneral64Source : (family AArch64Register) constructor AArch64FloatMoveToGeneral64 field unrestricted aarch64FloatMoveToGeneral64Destination : (family AArch64Register) field unrestricted aarch64FloatMoveToGeneral64Source : (family AArch64FloatRegister) -- dsb sy: every memory access before completes before any after -- how a -- store to Normal memory is ordered before one to a Device mapping constructor AArch64DataSynchronizationBarrier end-family family AArch64Program : Type 0 constructor AArch64ProgramEnd constructor AArch64ProgramNext field unrestricted aarch64ProgramInstruction : (family AArch64Instruction) recursive unrestricted aarch64ProgramTail end-family -- Encoding either yields the exact bytes or names the operand it refused. family AArch64EncodeResult : Type 0 constructor AArch64Encoded field unrestricted aarch64EncodedBytes : Bytes constructor AArch64ImmediateOutOfRange field unrestricted aarch64ImmediateOutOfRangeValue : Nat constructor AArch64MisalignedOffset field unrestricted aarch64MisalignedOffsetValue : Nat constructor AArch64DisplacementOutOfRange field unrestricted aarch64DisplacementOutOfRangeValue : Nat end-family def aarch64RegisterCode : (pi unrestricted register : (family AArch64Register) . Nat) = (lambda unrestricted register : (family AArch64Register) . (eliminate AArch64Register (lambda unrestricted current : (family AArch64Register) . Nat) register (branch AArch64X0 . 0) (branch AArch64X1 . 1) (branch AArch64X2 . 2) (branch AArch64X3 . 3) (branch AArch64X4 . 4) (branch AArch64X5 . 5) (branch AArch64X6 . 6) (branch AArch64X7 . 7) (branch AArch64X8 . 8) (branch AArch64X9 . 9) (branch AArch64X10 . 10) (branch AArch64X11 . 11) (branch AArch64X12 . 12) (branch AArch64X13 . 13) (branch AArch64X14 . 14) (branch AArch64X15 . 15) (branch AArch64X16 . 16) (branch AArch64X17 . 17) (branch AArch64X18 . 18) (branch AArch64X19 . 19) (branch AArch64X20 . 20) (branch AArch64X21 . 21) (branch AArch64X22 . 22) (branch AArch64X23 . 23) (branch AArch64X24 . 24) (branch AArch64X25 . 25) (branch AArch64X26 . 26) (branch AArch64X27 . 27) (branch AArch64X28 . 28) (branch AArch64X29 . 29) (branch AArch64X30 . 30))) def aarch64FloatRegisterCode : (pi unrestricted register : (family AArch64FloatRegister) . Nat) = (lambda unrestricted register : (family AArch64FloatRegister) . (eliminate AArch64FloatRegister (lambda unrestricted current : (family AArch64FloatRegister) . Nat) register (branch AArch64S0 . 0) (branch AArch64S1 . 1) (branch AArch64S2 . 2) (branch AArch64S3 . 3) (branch AArch64S4 . 4) (branch AArch64S5 . 5) (branch AArch64S6 . 6) (branch AArch64S7 . 7) (branch AArch64S8 . 8) (branch AArch64S9 . 9) (branch AArch64S10 . 10) (branch AArch64S11 . 11) (branch AArch64S12 . 12) (branch AArch64S13 . 13) (branch AArch64S14 . 14) (branch AArch64S15 . 15) (branch AArch64S16 . 16) (branch AArch64S17 . 17) (branch AArch64S18 . 18) (branch AArch64S19 . 19) (branch AArch64S20 . 20) (branch AArch64S21 . 21) (branch AArch64S22 . 22) (branch AArch64S23 . 23) (branch AArch64S24 . 24) (branch AArch64S25 . 25) (branch AArch64S26 . 26) (branch AArch64S27 . 27) (branch AArch64S28 . 28) (branch AArch64S29 . 29) (branch AArch64S30 . 30) (branch AArch64S31 . 31) )) def aarch64HalfwordShiftCode : (pi unrestricted shift : (family AArch64HalfwordShift) . Nat) = (lambda unrestricted shift : (family AArch64HalfwordShift) . (eliminate AArch64HalfwordShift (lambda unrestricted current : (family AArch64HalfwordShift) . Nat) shift (branch AArch64Shift0 . 0) (branch AArch64Shift16 . 1) (branch AArch64Shift32 . 2) (branch AArch64Shift48 . 3))) def aarch64ConditionCode : (pi unrestricted condition : (family AArch64Condition) . Nat) = (lambda unrestricted condition : (family AArch64Condition) . (eliminate AArch64Condition (lambda unrestricted current : (family AArch64Condition) . Nat) condition (branch AArch64Equal . 0) (branch AArch64NotEqual . 1) (branch AArch64CarrySet . 2) (branch AArch64CarryClear . 3) (branch AArch64Minus . 4) (branch AArch64Plus . 5) (branch AArch64OverflowSet . 6) (branch AArch64OverflowClear . 7) (branch AArch64UnsignedHigher . 8) (branch AArch64UnsignedLowerOrSame . 9) (branch AArch64GreaterOrEqual . 10) (branch AArch64LessThan . 11) (branch AArch64GreaterThan . 12) (branch AArch64LessOrEqual . 13))) -- Field multipliers (the bit position of each field) and two's-complement moduli. def aarch64ImmediateShiftCode : (pi unrestricted shift : (family AArch64ImmediateShift) . Nat) = (lambda unrestricted shift : (family AArch64ImmediateShift) . (eliminate AArch64ImmediateShift (lambda unrestricted current : (family AArch64ImmediateShift) . Nat) shift (branch AArch64Unshifted . 0) (branch AArch64ShiftedBy12 . 1))) -- Encoding is BYTE-ORIENTED, like Compiler.MachineX86Native, and for the same -- reason: in the runtime machine a Nat literal costs steps linear in its -- value, so an opcode base near 3.6 billion is unrunnable even though the -- checker normalises it instantly. Every word is built as its four -- little-endian bytes from the base's bytes plus each field's contribution, -- and every intermediate stays below 256 except the operands themselves, -- which the smart constructors already bound. Powers of two are computed by -- doubling rather than written as literals for the same reason. def aarch64Two : Nat = 2 def aarch64Four : Nat = 4 def aarch64Eight : Nat = 8 def aarch64ThirtyTwo : Nat = 32 def aarch64SixtyFour : Nat = 64 def aarch64TwoHundredFiftySix : Nat = (naturalPowerOfTwo 8) def aarch64TwoThousandFortyEight : Nat = (naturalPowerOfTwo 11) -- Field limits. Anything at or above 256 is computed by doubling rather -- than written as a literal, because a literal costs steps equal to its value. def aarch64Immediate12Limit : Nat = (naturalPowerOfTwo 12) def aarch64Immediate16Limit : Nat = (naturalPowerOfTwo 16) def aarch64ShiftLimit : Nat = 64 -- The largest scaled 32-bit offset is 4095 * 4; the limit is one past it. -- Reusing the 64-bit limit here would let an offset up to 32767 through and -- overflow imm12, encoding a different instruction instead of refusing. def aarch64Scaled32OffsetLimit : Nat = (naturalAdd (naturalMultiply (naturalSaturatingSubtract aarch64Immediate12Limit 1) aarch64Four) 1) -- The largest scaled 64-bit offset is 4095 * 8; the limit is one past it. def aarch64ScaledOffsetLimit : Nat = (naturalAdd (naturalMultiply (naturalSaturatingSubtract aarch64Immediate12Limit 1) aarch64Eight) 1) def aarch64Modulus19 : Nat = (naturalPowerOfTwo 19) def aarch64Modulus21 : Nat = (naturalPowerOfTwo 21) def aarch64Modulus26 : Nat = (naturalPowerOfTwo 26) -- A word from its four little-endian bytes. Every argument is reduced mod -- 256 by nat-to-byte, so a field that overflows its byte cannot silently -- corrupt the next one: the smart constructors bound every operand first. def aarch64ByteWord = (lambda unrestricted byte0 : Nat . (lambda unrestricted byte1 : Nat . (lambda unrestricted byte2 : Nat . (lambda unrestricted byte3 : Nat . (constructor AArch64EncodeResult AArch64Encoded (bytes-cons (nat-to-byte byte0) (bytes-cons (nat-to-byte byte1) (bytes-cons (nat-to-byte byte2) (bytes-cons (nat-to-byte byte3) b""))))))))) -- Accept the word only when value < limit. def aarch64EncodeBounded = (lambda unrestricted value : Nat . (lambda unrestricted limit : Nat . (lambda unrestricted word : (family AArch64EncodeResult) . (nat-eliminate (lambda unrestricted accepted : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64ImmediateOutOfRange value) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . word)) (naturalLess value limit))))) -- Field contributions, by the byte they land in. -- Rd occupies bits 0-4, so it adds to byte 0. -- Rn occupies bits 5-9: its low three bits scale into byte 0, the rest into byte 1. def aarch64LowFive = (lambda unrestricted register : (family AArch64Register) . (aarch64RegisterCode register)) def aarch64RnByte0 = (lambda unrestricted register : (family AArch64Register) . (naturalMultiply (naturalModuloUnchecked (aarch64RegisterCode register) aarch64Eight) aarch64ThirtyTwo)) def aarch64RnByte1 = (lambda unrestricted register : (family AArch64Register) . (naturalDivideUnchecked (aarch64RegisterCode register) aarch64Eight)) -- The stack pointer is register code 31 in the encodings that admit it. def aarch64StackPointerByte0 : Nat = 224 def aarch64StackPointerByte1 : Nat = 3 def aarch64ZeroRegisterByte0 : Nat = 31 -- An imm12 occupies bits 10-21: byte 1 takes six bits scaled by four, byte 2 the rest. def aarch64Immediate12Byte1 = (lambda unrestricted value : Nat . (naturalMultiply (naturalModuloUnchecked value aarch64SixtyFour) aarch64Four)) def aarch64Immediate12Byte2 = (lambda unrestricted value : Nat . (naturalDivideUnchecked value aarch64SixtyFour)) -- An imm16 occupies bits 5-20, an imm19 bits 5-23: both start at bit 5. def aarch64FromBitFiveByte0 = (lambda unrestricted value : Nat . (naturalMultiply (naturalModuloUnchecked value aarch64Eight) aarch64ThirtyTwo)) def aarch64FromBitFiveByte1 = (lambda unrestricted value : Nat . (naturalModuloUnchecked (naturalDivideUnchecked value aarch64Eight) aarch64TwoHundredFiftySix)) def aarch64FromBitFiveByte2 = (lambda unrestricted value : Nat . (naturalModuloUnchecked (naturalDivideUnchecked value aarch64TwoThousandFortyEight) aarch64TwoHundredFiftySix)) -- A three-register data-processing word. def aarch64ThreeRegisterWord = (lambda unrestricted base1 : Nat . (lambda unrestricted base2 : Nat . (lambda unrestricted base3 : Nat . (lambda unrestricted destination : (family AArch64Register) . (lambda unrestricted left : (family AArch64Register) . (lambda unrestricted right : (family AArch64Register) . (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 left)) (naturalAdd base1 (aarch64RnByte1 left)) (naturalAdd base2 (aarch64RegisterCode right)) base3))))))) -- A wide move: imm16 at bit 5, the halfword selector at bits 21-22. def aarch64WideWord = (lambda unrestricted base3 : Nat . (lambda unrestricted destination : (family AArch64Register) . (lambda unrestricted value : Nat . (lambda unrestricted shift : (family AArch64HalfwordShift) . (aarch64EncodeBounded value aarch64Immediate16Limit (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64FromBitFiveByte0 value)) (aarch64FromBitFiveByte1 value) (naturalAdd (naturalAdd 128 (aarch64FromBitFiveByte2 value)) (naturalMultiply (aarch64HalfwordShiftCode shift) aarch64ThirtyTwo)) base3)))))) -- An add/subtract immediate over general registers. def aarch64ImmediateWord = (lambda unrestricted base3 : Nat . (lambda unrestricted destination : Nat . (lambda unrestricted source : (family AArch64Register) . (lambda unrestricted value : Nat . (aarch64EncodeBounded value aarch64Immediate12Limit (aarch64ByteWord (naturalAdd destination (aarch64RnByte0 source)) (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 value)) (aarch64Immediate12Byte2 value) base3)))))) -- A scaled 64-bit load or store: the offset must be a multiple of eight. def aarch64ScaledMemoryWord = (lambda unrestricted base2 : Nat . (lambda unrestricted base3 : Nat . (lambda unrestricted register : (family AArch64Register) . (lambda unrestricted address : (family AArch64Register) . (lambda unrestricted offset : Nat . (nat-eliminate (lambda unrestricted aligned : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64MisalignedOffset offset) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . (aarch64EncodeBounded offset aarch64ScaledOffsetLimit (aarch64ByteWord (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address)) (naturalAdd (aarch64RnByte1 address) (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Eight))) (naturalAdd base2 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Eight))) base3)))) (naturalIsZero (naturalModuloUnchecked offset aarch64Eight)))))))) -- A 32-bit load or store: like the 64-bit form, but the imm12 offset is -- scaled by 4 rather than 8, and the offset must be a multiple of 4. RM -- handles are NvU32, so placing one into a parameter struct needs this width: -- a 64-bit store would carry the neighbouring field along with it. def aarch64ScaledMemoryWord32 = (lambda unrestricted base2 : Nat . (lambda unrestricted base3 : Nat . (lambda unrestricted register : (family AArch64Register) . (lambda unrestricted address : (family AArch64Register) . (lambda unrestricted offset : Nat . (nat-eliminate (lambda unrestricted aligned : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64MisalignedOffset offset) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . (aarch64EncodeBounded offset aarch64Scaled32OffsetLimit (aarch64ByteWord (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address)) (naturalAdd (aarch64RnByte1 address) (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Four))) (naturalAdd base2 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Four))) base3)))) (naturalIsZero (naturalModuloUnchecked offset aarch64Four)))))))) -- A byte load or store: an unscaled imm12 offset. def aarch64ByteMemoryWord = (lambda unrestricted base2 : Nat . (lambda unrestricted base3 : Nat . (lambda unrestricted register : (family AArch64Register) . (lambda unrestricted address : (family AArch64Register) . (lambda unrestricted offset : Nat . (aarch64EncodeBounded offset aarch64Immediate12Limit (aarch64ByteWord (naturalAdd (aarch64LowFive register) (aarch64RnByte0 address)) (naturalAdd (aarch64RnByte1 address) (aarch64Immediate12Byte1 offset)) (naturalAdd base2 (aarch64Immediate12Byte2 offset)) base3))))))) -- The stack-pointer forms, where register code 31 means sp. def aarch64StackAdjustWord = (lambda unrestricted base3 : Nat . (lambda unrestricted value : Nat . (lambda unrestricted shift : (family AArch64ImmediateShift) . (aarch64EncodeBounded value aarch64Immediate12Limit (aarch64ByteWord (naturalAdd aarch64StackPointerByte0 aarch64ZeroRegisterByte0) (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 value)) (naturalAdd (aarch64Immediate12Byte2 value) (naturalMultiply (aarch64ImmediateShiftCode shift) aarch64SixtyFour)) base3))))) def aarch64StackScaledWord = (lambda unrestricted base2 : Nat . (lambda unrestricted base3 : Nat . (lambda unrestricted register : (family AArch64Register) . (lambda unrestricted offset : Nat . (nat-eliminate (lambda unrestricted aligned : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64MisalignedOffset offset) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . (aarch64EncodeBounded offset aarch64ScaledOffsetLimit (aarch64ByteWord (naturalAdd (aarch64LowFive register) aarch64StackPointerByte0) (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 (naturalDivideUnchecked offset aarch64Eight))) (naturalAdd base2 (aarch64Immediate12Byte2 (naturalDivideUnchecked offset aarch64Eight))) base3)))) (naturalIsZero (naturalModuloUnchecked offset aarch64Eight))))))) def aarch64StackByteWord = (lambda unrestricted base2 : Nat . (lambda unrestricted base3 : Nat . (lambda unrestricted register : (family AArch64Register) . (lambda unrestricted offset : Nat . (aarch64EncodeBounded offset aarch64Immediate12Limit (aarch64ByteWord (naturalAdd (aarch64LowFive register) aarch64StackPointerByte0) (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 offset)) (naturalAdd base2 (aarch64Immediate12Byte2 offset)) base3)))))) -- Two's-complement field for a signed distance whose magnitude is in `units`. def aarch64SignedField = (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted units : Nat . (lambda unrestricted modulus : Nat . (eliminate AArch64Direction (lambda unrestricted current : (family AArch64Direction) . Nat) direction (branch AArch64Forward . units) (branch AArch64Backward . (naturalModuloUnchecked (naturalSaturatingSubtract modulus units) modulus)))))) -- Forward distances reach modulus/2 - 1 units, backward ones modulus/2. def aarch64DistanceAccepted = (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted units : Nat . (lambda unrestricted half : Nat . (eliminate AArch64Direction (lambda unrestricted current : (family AArch64Direction) . Nat) direction (branch AArch64Forward . (naturalLess units half)) (branch AArch64Backward . (naturalLessOrEqual units half)))))) -- A 19-bit branch field at bit 5, with `extra` in byte 0 (a condition or a register). def aarch64Branch19Word = (lambda unrestricted base3 : Nat . (lambda unrestricted extra : Nat . (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (nat-eliminate (lambda unrestricted aligned : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64MisalignedOffset distance) (lambda unrestricted predecessorAligned : Nat . (lambda unrestricted inductionAligned : (family AArch64EncodeResult) . (nat-eliminate (lambda unrestricted accepted : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . (app (lambda unrestricted field : Nat . (aarch64ByteWord (naturalAdd extra (aarch64FromBitFiveByte0 field)) (aarch64FromBitFiveByte1 field) (aarch64FromBitFiveByte2 field) base3)) (aarch64SignedField direction (naturalDivideUnchecked distance aarch64Four) aarch64Modulus19)))) (aarch64DistanceAccepted direction (naturalDivideUnchecked distance aarch64Four) (naturalDivideUnchecked aarch64Modulus19 aarch64Two))))) (naturalIsZero (naturalModuloUnchecked distance aarch64Four))))))) -- A 26-bit branch field at bit 0. def aarch64Branch26Word = (lambda unrestricted base3 : Nat . (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (nat-eliminate (lambda unrestricted aligned : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64MisalignedOffset distance) (lambda unrestricted predecessorAligned : Nat . (lambda unrestricted inductionAligned : (family AArch64EncodeResult) . (nat-eliminate (lambda unrestricted accepted : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . (app (lambda unrestricted field : Nat . (aarch64ByteWord (naturalModuloUnchecked field aarch64TwoHundredFiftySix) (naturalModuloUnchecked (naturalDivideUnchecked field aarch64TwoHundredFiftySix) aarch64TwoHundredFiftySix) (naturalModuloUnchecked (naturalDivideUnchecked field (naturalMultiply aarch64TwoHundredFiftySix aarch64TwoHundredFiftySix)) aarch64TwoHundredFiftySix) (naturalAdd base3 (naturalModuloUnchecked (naturalDivideUnchecked field (naturalMultiply (naturalMultiply aarch64TwoHundredFiftySix aarch64TwoHundredFiftySix) aarch64TwoHundredFiftySix)) aarch64Four)))) (aarch64SignedField direction (naturalDivideUnchecked distance aarch64Four) aarch64Modulus26)))) (aarch64DistanceAccepted direction (naturalDivideUnchecked distance aarch64Four) (naturalDivideUnchecked aarch64Modulus26 aarch64Two))))) (naturalIsZero (naturalModuloUnchecked distance aarch64Four)))))) -- adr: a 21-bit BYTE distance, its low two bits at bits 29-30 and the rest at bit 5. def aarch64AddressWord = (lambda unrestricted destination : (family AArch64Register) . (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (nat-eliminate (lambda unrestricted accepted : Nat . (family AArch64EncodeResult)) (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64EncodeResult) . (app (lambda unrestricted field : Nat . (app (lambda unrestricted high : Nat . (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64FromBitFiveByte0 high)) (aarch64FromBitFiveByte1 high) (aarch64FromBitFiveByte2 high) (naturalAdd 16 (naturalMultiply (naturalModuloUnchecked field aarch64Four) aarch64ThirtyTwo)))) (naturalDivideUnchecked field aarch64Four))) (aarch64SignedField direction distance aarch64Modulus21)))) (aarch64DistanceAccepted direction distance (naturalDivideUnchecked aarch64Modulus21 aarch64Two)))))) -- lsl by amount is ubfm with immr = (64 - amount) mod 64 and imms = 63 - amount. def aarch64ShiftLeftWord = (lambda unrestricted destination : (family AArch64Register) . (lambda unrestricted source : (family AArch64Register) . (lambda unrestricted amount : Nat . (aarch64EncodeBounded amount aarch64ShiftLimit (app (lambda unrestricted immr : Nat . (app (lambda unrestricted imms : Nat . (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 source)) (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 imms)) (naturalAdd aarch64SixtyFour immr) 211)) (naturalSaturatingSubtract 63 amount))) (naturalModuloUnchecked (naturalSaturatingSubtract aarch64SixtyFour amount) aarch64SixtyFour)))))) -- lsr by amount is ubfm with immr = amount and imms = 63. def aarch64ShiftRightWord = (lambda unrestricted destination : (family AArch64Register) . (lambda unrestricted source : (family AArch64Register) . (lambda unrestricted amount : Nat . (aarch64EncodeBounded amount aarch64ShiftLimit (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64RnByte0 source)) (naturalAdd (aarch64RnByte1 source) (aarch64Immediate12Byte1 63)) (naturalAdd aarch64SixtyFour amount) 211))))) -- Scalar single-precision, the A64 counterpart of the x86-64 SSE scalar -- lowering (L13c). Every word below was assembled from the same mnemonic by -- GNU `as` on this host; the laws in Compiler.MachineAArch64Proof carry the -- bytes. -- -- FP data-processing, two sources: -- 0001 1110 0 01 Rm opcode 10 Rn Rd -- with opcode 0 FMUL, 1 FDIV, 2 FADD, 3 FSUB. The Rm field is bits 16-20, so -- byte 2 is 32 + Rm; the `10` in bits 10-11 is the 8 in byte 1. def aarch64FloatRdByte0 = (lambda unrestricted register : (family AArch64FloatRegister) . (aarch64FloatRegisterCode register)) def aarch64FloatRnByte0 = (lambda unrestricted register : (family AArch64FloatRegister) . (naturalMultiply (naturalModuloUnchecked (aarch64FloatRegisterCode register) aarch64Eight) aarch64ThirtyTwo)) def aarch64FloatRnByte1 = (lambda unrestricted register : (family AArch64FloatRegister) . (naturalDivideUnchecked (aarch64FloatRegisterCode register) aarch64Eight)) def aarch64FloatDataWord = (lambda unrestricted opcode : Nat . (lambda unrestricted destination : (family AArch64FloatRegister) . (lambda unrestricted left : (family AArch64FloatRegister) . (lambda unrestricted right : (family AArch64FloatRegister) . (aarch64ByteWord (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 left)) (naturalAdd (naturalMultiply opcode 16) (naturalAdd aarch64Eight (aarch64FloatRnByte1 left))) (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right)) 30))))) -- The same two-source form in double precision: the type field (bits 22-23) -- is 01, the 64 in byte 2. def aarch64FloatData64Word = (lambda unrestricted opcode : Nat . (lambda unrestricted destination : (family AArch64FloatRegister) . (lambda unrestricted left : (family AArch64FloatRegister) . (lambda unrestricted right : (family AArch64FloatRegister) . (aarch64ByteWord (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 left)) (naturalAdd (naturalMultiply opcode 16) (naturalAdd aarch64Eight (aarch64FloatRnByte1 left))) (naturalAdd aarch64SixtyFour (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right))) 30))))) -- One-source FP forms: Rd in bits 0-4 and Rn in bits 5-9, so byte 0 carries -- Rd and Rn's low three bits and byte 1 Rn's high two bits over the form's -- own byte-1 bits (fsqrt d: 1e61c000; fcvt s<-d: 1e624000; fcvt d<-s: -- 1e22c000). def aarch64FloatUnaryWord = (lambda unrestricted byte1 : Nat . (lambda unrestricted byte2 : Nat . (lambda unrestricted byte3 : Nat . (lambda unrestricted destination : (family AArch64FloatRegister) . (lambda unrestricted source : (family AArch64FloatRegister) . (aarch64ByteWord (naturalAdd (aarch64FloatRdByte0 destination) (aarch64FloatRnByte0 source)) (naturalAdd byte1 (aarch64FloatRnByte1 source)) byte2 byte3)))))) -- FCMP Sn, Sm: 0001 1110 0 01 Rm 001000 Rn 00000. The Rd field is zero -- the -- comparison writes NZCV, not a register -- and bits 10-15 are 001000, which -- is the 32 in byte 1. This is the QUIET compare, the counterpart of the -- SSE lowering's `ucomiss`: a quiet NaN does not raise Invalid, only a -- signalling one does. `fcmpe` would be the signalling form and is not what -- the x86 lane does. def aarch64FloatCompareWord = (lambda unrestricted left : (family AArch64FloatRegister) . (lambda unrestricted right : (family AArch64FloatRegister) . (aarch64ByteWord (aarch64FloatRnByte0 left) (naturalAdd aarch64ThirtyTwo (aarch64FloatRnByte1 left)) (naturalAdd aarch64ThirtyTwo (aarch64FloatRegisterCode right)) 30))) def aarch64EncodeInstruction : (pi unrestricted instruction : (family AArch64Instruction) . (family AArch64EncodeResult)) = (lambda unrestricted instruction : (family AArch64Instruction) . (eliminate AArch64Instruction (lambda unrestricted current : (family AArch64Instruction) . (family AArch64EncodeResult)) instruction (branch AArch64MoveWideZero destination value shift . (aarch64WideWord 210 destination value shift)) (branch AArch64MoveWideKeep destination value shift . (aarch64WideWord 242 destination value shift)) (branch AArch64MoveRegister destination source . (aarch64ByteWord (naturalAdd aarch64StackPointerByte0 (aarch64LowFive destination)) aarch64StackPointerByte1 (aarch64RegisterCode source) 170)) (branch AArch64AddImmediate destination source value . (aarch64ImmediateWord 145 (aarch64LowFive destination) source value)) (branch AArch64SubtractImmediate destination source value . (aarch64ImmediateWord 209 (aarch64LowFive destination) source value)) (branch AArch64AddRegister destination left right . (aarch64ThreeRegisterWord 0 0 139 destination left right)) (branch AArch64SubtractRegister destination left right . (aarch64ThreeRegisterWord 0 0 203 destination left right)) (branch AArch64AndRegister destination left right . (aarch64ThreeRegisterWord 0 0 138 destination left right)) (branch AArch64OrRegister destination left right . (aarch64ThreeRegisterWord 0 0 170 destination left right)) (branch AArch64ExclusiveOrRegister destination left right . (aarch64ThreeRegisterWord 0 0 202 destination left right)) (branch AArch64ShiftLeftImmediate destination source amount . (aarch64ShiftLeftWord destination source amount)) (branch AArch64ShiftRightImmediate destination source amount . (aarch64ShiftRightWord destination source amount)) (branch AArch64MultiplyRegister destination left right . (aarch64ThreeRegisterWord 124 0 155 destination left right)) (branch AArch64DivideRegisterUnsigned destination left right . (aarch64ThreeRegisterWord 8 192 154 destination left right)) (branch AArch64CompareImmediate register value . (aarch64ImmediateWord 241 aarch64ZeroRegisterByte0 register value)) (branch AArch64CompareRegister left right . (aarch64ByteWord (naturalAdd aarch64ZeroRegisterByte0 (aarch64RnByte0 left)) (aarch64RnByte1 left) (aarch64RegisterCode right) 235)) (branch AArch64LoadMemory64 destination base offset . (aarch64ScaledMemoryWord aarch64SixtyFour 249 destination base offset)) (branch AArch64StoreMemory64 base offset source . (aarch64ScaledMemoryWord 0 249 source base offset)) (branch AArch64LoadMemory32ZeroExtend destination base offset . (aarch64ScaledMemoryWord32 aarch64SixtyFour 185 destination base offset)) (branch AArch64StoreMemory32 base offset source . (aarch64ScaledMemoryWord32 0 185 source base offset)) (branch AArch64LoadMemory8ZeroExtend destination base offset . (aarch64ByteMemoryWord aarch64SixtyFour 57 destination base offset)) (branch AArch64StoreMemory8 base offset source . (aarch64ByteMemoryWord 0 57 source base offset)) (branch AArch64AddressRelative destination direction distance . (aarch64AddressWord destination direction distance)) (branch AArch64Branch direction distance . (aarch64Branch26Word 20 direction distance)) (branch AArch64BranchLink direction distance . (aarch64Branch26Word 148 direction distance)) (branch AArch64BranchLinkRegister target . (aarch64ByteWord (aarch64RnByte0 target) (aarch64RnByte1 target) 63 214)) (branch AArch64BranchIf condition direction distance . (aarch64Branch19Word 84 (aarch64ConditionCode condition) direction distance)) (branch AArch64CompareBranchIfZero register direction distance . (aarch64Branch19Word 180 (aarch64LowFive register) direction distance)) (branch AArch64CompareBranchIfNotZero register direction distance . (aarch64Branch19Word 181 (aarch64LowFive register) direction distance)) (branch AArch64AddImmediateFromStackPointer destination value . (aarch64EncodeBounded value aarch64Immediate12Limit (aarch64ByteWord (naturalAdd aarch64StackPointerByte0 (aarch64LowFive destination)) (naturalAdd aarch64StackPointerByte1 (aarch64Immediate12Byte1 value)) (aarch64Immediate12Byte2 value) 145))) (branch AArch64AddStackPointer value shift . (aarch64StackAdjustWord 145 value shift)) (branch AArch64SubtractStackPointer value shift . (aarch64StackAdjustWord 209 value shift)) (branch AArch64LoadMemory64FromStack destination offset . (aarch64StackScaledWord aarch64SixtyFour 249 destination offset)) (branch AArch64StoreMemory64ToStack offset source . (aarch64StackScaledWord 0 249 source offset)) (branch AArch64LoadMemory8FromStack destination offset . (aarch64StackByteWord aarch64SixtyFour 57 destination offset)) (branch AArch64StoreMemory8ToStack offset source . (aarch64StackByteWord 0 57 source offset)) (branch AArch64Return . (aarch64ByteWord 192 3 95 214)) (branch AArch64SupervisorCall . (aarch64ByteWord 1 0 0 212)) (branch AArch64DataSynchronizationBarrierSystem . (aarch64ByteWord 159 63 3 213)) (branch AArch64FloatAdd32 destination left right . (aarch64FloatDataWord aarch64Two destination left right)) (branch AArch64FloatSubtract32 destination left right . (aarch64FloatDataWord 3 destination left right)) (branch AArch64FloatMultiply32 destination left right . (aarch64FloatDataWord 0 destination left right)) (branch AArch64FloatDivide32 destination left right . (aarch64FloatDataWord 1 destination left right)) (branch AArch64FloatCompare32 left right . (aarch64FloatCompareWord left right)) (branch AArch64FloatMoveFromGeneral32 destination source . (aarch64ByteWord (naturalAdd (aarch64FloatRdByte0 destination) (aarch64RnByte0 source)) (aarch64RnByte1 source) 39 30)) (branch AArch64FloatMoveToGeneral32 destination source . (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64FloatRnByte0 source)) (aarch64FloatRnByte1 source) 38 30)) (branch AArch64ReadFloatControl destination . (aarch64ByteWord (aarch64LowFive destination) 68 59 213)) (branch AArch64WriteFloatControl source . (aarch64ByteWord (aarch64LowFive source) 68 27 213)) (branch AArch64FloatAdd64 destination left right . (aarch64FloatData64Word aarch64Two destination left right)) (branch AArch64FloatSubtract64 destination left right . (aarch64FloatData64Word 3 destination left right)) (branch AArch64FloatMultiply64 destination left right . (aarch64FloatData64Word 0 destination left right)) (branch AArch64FloatDivide64 destination left right . (aarch64FloatData64Word 1 destination left right)) (branch AArch64FloatSquareRoot64 destination source . (aarch64FloatUnaryWord 192 97 30 destination source)) (branch AArch64FloatFromSigned64 destination source . (aarch64ByteWord (naturalAdd (aarch64FloatRdByte0 destination) (aarch64RnByte0 source)) (aarch64RnByte1 source) 98 158)) (branch AArch64FloatNarrow64To32 destination source . (aarch64FloatUnaryWord aarch64SixtyFour 98 30 destination source)) (branch AArch64FloatWiden32To64 destination source . (aarch64FloatUnaryWord 192 34 30 destination source)) (branch AArch64FloatMoveFromGeneral64 destination source . (aarch64ByteWord (naturalAdd (aarch64FloatRdByte0 destination) (aarch64RnByte0 source)) (aarch64RnByte1 source) 103 158)) (branch AArch64FloatMoveToGeneral64 destination source . (aarch64ByteWord (naturalAdd (aarch64LowFive destination) (aarch64FloatRnByte0 source)) (aarch64FloatRnByte1 source) 102 158)) (branch AArch64DataSynchronizationBarrier . (aarch64ByteWord 159 63 3 213)))) def aarch64AppendResults = (lambda unrestricted head : (family AArch64EncodeResult) . (lambda unrestricted tail : (family AArch64EncodeResult) . (eliminate AArch64EncodeResult (lambda unrestricted current : (family AArch64EncodeResult) . (family AArch64EncodeResult)) head (branch AArch64Encoded headBytes . (eliminate AArch64EncodeResult (lambda unrestricted current : (family AArch64EncodeResult) . (family AArch64EncodeResult)) tail (branch AArch64Encoded tailBytes . (constructor AArch64EncodeResult AArch64Encoded (bytes-append headBytes tailBytes))) (branch AArch64ImmediateOutOfRange value . (constructor AArch64EncodeResult AArch64ImmediateOutOfRange value)) (branch AArch64MisalignedOffset value . (constructor AArch64EncodeResult AArch64MisalignedOffset value)) (branch AArch64DisplacementOutOfRange value . (constructor AArch64EncodeResult AArch64DisplacementOutOfRange value)))) (branch AArch64ImmediateOutOfRange value . (constructor AArch64EncodeResult AArch64ImmediateOutOfRange value)) (branch AArch64MisalignedOffset value . (constructor AArch64EncodeResult AArch64MisalignedOffset value)) (branch AArch64DisplacementOutOfRange value . (constructor AArch64EncodeResult AArch64DisplacementOutOfRange value))))) def aarch64EncodeProgram : (pi unrestricted program : (family AArch64Program) . (family AArch64EncodeResult)) = (lambda unrestricted program : (family AArch64Program) . (eliminate AArch64Program (lambda unrestricted current : (family AArch64Program) . (family AArch64EncodeResult)) program (branch AArch64ProgramEnd . (constructor AArch64EncodeResult AArch64Encoded b"")) (branch AArch64ProgramNext instruction tail encodedTail . (aarch64AppendResults (aarch64EncodeInstruction instruction) encodedTail))))