module Compiler.MachineAArch64Assembly import Compiler.MachineAArch64 import Data.Bytes import Model.Config import Model.Word32 import Std.Byte import Std.Natural -- The AArch64 twin of Compiler.MachineX86NativeAssembly: a program with -- named labels, laid out in one pass and encoded in a second. Every item -- occupies exactly one 32-bit word except a label, which occupies none, so -- layout is arithmetic rather than encoding. A branch's displacement is -- measured from the branch itself (A64), where x86-64 measures from the end -- of the instruction; that is the one place the two assemblers differ. family AArch64Assembly : Type 0 constructor AArch64AssemblyEnd constructor AArch64AssemblyEmit field unrestricted aarch64AssemblyInstruction : (family AArch64Instruction) recursive unrestricted aarch64AssemblyAfterInstruction constructor AArch64AssemblyLabel field unrestricted aarch64AssemblyLabelName : Bytes recursive unrestricted aarch64AssemblyAfterLabel constructor AArch64AssemblyBranch field unrestricted aarch64AssemblyBranchTarget : Bytes recursive unrestricted aarch64AssemblyAfterBranch constructor AArch64AssemblyBranchLink field unrestricted aarch64AssemblyBranchLinkTarget : Bytes recursive unrestricted aarch64AssemblyAfterBranchLink constructor AArch64AssemblyBranchIf field unrestricted aarch64AssemblyBranchIfCondition : (family AArch64Condition) field unrestricted aarch64AssemblyBranchIfTarget : Bytes recursive unrestricted aarch64AssemblyAfterBranchIf constructor AArch64AssemblyCompareBranchIfZero field unrestricted aarch64AssemblyCompareBranchIfZeroRegister : (family AArch64Register) field unrestricted aarch64AssemblyCompareBranchIfZeroTarget : Bytes recursive unrestricted aarch64AssemblyAfterCompareBranchIfZero constructor AArch64AssemblyCompareBranchIfNotZero field unrestricted aarch64AssemblyCompareBranchIfNotZeroRegister : (family AArch64Register) field unrestricted aarch64AssemblyCompareBranchIfNotZeroTarget : Bytes recursive unrestricted aarch64AssemblyAfterCompareBranchIfNotZero constructor AArch64AssemblyAddressOf field unrestricted aarch64AssemblyAddressOfDestination : (family AArch64Register) field unrestricted aarch64AssemblyAddressOfTarget : Bytes recursive unrestricted aarch64AssemblyAfterAddressOf end-family family AArch64LabelTable : Type 0 constructor AArch64LabelTableEmpty constructor AArch64LabelTableEntry field unrestricted aarch64LabelName : Bytes field unrestricted aarch64LabelOffset : Nat recursive unrestricted aarch64RemainingLabels end-family family AArch64LabelLookupResult : Type 0 constructor AArch64LabelFound field unrestricted aarch64FoundLabelOffset : Nat constructor AArch64LabelMissing end-family family AArch64AssemblyLayoutResult : Type 0 constructor AArch64AssemblyLayoutSuccess field unrestricted aarch64AssemblyLabels : (family AArch64LabelTable) field unrestricted aarch64AssemblySize : Nat constructor AArch64AssemblyDuplicateLabel field unrestricted aarch64DuplicateLabelName : Bytes end-family family AArch64AssemblyResult : Type 0 constructor AArch64AssemblyEncoded field unrestricted aarch64AssemblyEncodedBytes : Bytes constructor AArch64AssemblyEncodeDuplicateLabel field unrestricted aarch64AssemblyEncodeDuplicateName : Bytes constructor AArch64AssemblyMissingLabel field unrestricted aarch64AssemblyMissingLabelName : Bytes constructor AArch64AssemblyDisplacementOutOfRange field unrestricted aarch64AssemblyDisplacementLabelName : Bytes constructor AArch64AssemblyOperandRefused field unrestricted aarch64AssemblyOperandRefusedValue : Nat end-family def aarch64LookupLabel : (pi unrestricted name : Bytes . (pi unrestricted labels : (family AArch64LabelTable) . (family AArch64LabelLookupResult))) = (lambda unrestricted name : Bytes . (lambda unrestricted labels : (family AArch64LabelTable) . (eliminate AArch64LabelTable (lambda unrestricted current : (family AArch64LabelTable) . (family AArch64LabelLookupResult)) labels (branch AArch64LabelTableEmpty . (constructor AArch64LabelLookupResult AArch64LabelMissing)) (branch AArch64LabelTableEntry entryName entryOffset remaining lookupRemaining . (nat-eliminate (lambda unrestricted matches : Nat . (family AArch64LabelLookupResult)) lookupRemaining (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64LabelLookupResult) . (constructor AArch64LabelLookupResult AArch64LabelFound entryOffset))) (bytes-equal entryName name)))))) -- Layout: every item but a label is one word. Labels are recorded at the -- offset of the word that follows them; a duplicate name is refused. def aarch64LayoutAssemblyFrom : (pi unrestricted assembly : (family AArch64Assembly) . (pi unrestricted offset : Nat . (family AArch64AssemblyLayoutResult))) = (lambda unrestricted assembly : (family AArch64Assembly) . (eliminate AArch64Assembly (lambda unrestricted current : (family AArch64Assembly) . (pi unrestricted offset : Nat . (family AArch64AssemblyLayoutResult))) assembly (branch AArch64AssemblyEnd . (lambda unrestricted offset : Nat . (constructor AArch64AssemblyLayoutResult AArch64AssemblyLayoutSuccess (constructor AArch64LabelTable AArch64LabelTableEmpty) offset))) (branch AArch64AssemblyEmit instruction tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))) (branch AArch64AssemblyLabel name tail layoutTail . (lambda unrestricted offset : Nat . (eliminate AArch64AssemblyLayoutResult (lambda unrestricted current : (family AArch64AssemblyLayoutResult) . (family AArch64AssemblyLayoutResult)) (layoutTail offset) (branch AArch64AssemblyLayoutSuccess labels finalSize . (eliminate AArch64LabelLookupResult (lambda unrestricted lookup : (family AArch64LabelLookupResult) . (family AArch64AssemblyLayoutResult)) (aarch64LookupLabel name labels) (branch AArch64LabelFound existing . (constructor AArch64AssemblyLayoutResult AArch64AssemblyDuplicateLabel name)) (branch AArch64LabelMissing . (constructor AArch64AssemblyLayoutResult AArch64AssemblyLayoutSuccess (constructor AArch64LabelTable AArch64LabelTableEntry name offset labels) finalSize)))) (branch AArch64AssemblyDuplicateLabel duplicate . (constructor AArch64AssemblyLayoutResult AArch64AssemblyDuplicateLabel duplicate))))) (branch AArch64AssemblyBranch target tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))) (branch AArch64AssemblyBranchLink target tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))) (branch AArch64AssemblyBranchIf condition target tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))) (branch AArch64AssemblyCompareBranchIfZero register target tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))) (branch AArch64AssemblyCompareBranchIfNotZero register target tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))) (branch AArch64AssemblyAddressOf destination target tail layoutTail . (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4)))))) def aarch64LayoutAssembly : (pi unrestricted assembly : (family AArch64Assembly) . (family AArch64AssemblyLayoutResult)) = (lambda unrestricted assembly : (family AArch64Assembly) . (aarch64LayoutAssemblyFrom assembly 0)) -- The direction and byte distance from the referencing word to a target. def aarch64DirectionTo = (lambda unrestricted source : Nat . (lambda unrestricted target : Nat . (nat-eliminate (lambda unrestricted backward : Nat . (family AArch64Direction)) (constructor AArch64Direction AArch64Forward) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family AArch64Direction) . (constructor AArch64Direction AArch64Backward))) (naturalLess target source)))) def aarch64DistanceTo = (lambda unrestricted source : Nat . (lambda unrestricted target : Nat . (nat-eliminate (lambda unrestricted backward : Nat . Nat) (naturalSaturatingSubtract target source) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (naturalSaturatingSubtract source target))) (naturalLess target source)))) -- One encoded word in front of the tail's result; the first refusal wins. def aarch64PrependWord = (lambda unrestricted name : Bytes . (lambda unrestricted word : (family AArch64EncodeResult) . (lambda unrestricted tailResult : (family AArch64AssemblyResult) . (eliminate AArch64EncodeResult (lambda unrestricted current : (family AArch64EncodeResult) . (family AArch64AssemblyResult)) word (branch AArch64Encoded encoded . (eliminate AArch64AssemblyResult (lambda unrestricted current : (family AArch64AssemblyResult) . (family AArch64AssemblyResult)) tailResult (branch AArch64AssemblyEncoded tailBytes . (constructor AArch64AssemblyResult AArch64AssemblyEncoded (bytes-append encoded tailBytes))) (branch AArch64AssemblyEncodeDuplicateLabel duplicate . (constructor AArch64AssemblyResult AArch64AssemblyEncodeDuplicateLabel duplicate)) (branch AArch64AssemblyMissingLabel missing . (constructor AArch64AssemblyResult AArch64AssemblyMissingLabel missing)) (branch AArch64AssemblyDisplacementOutOfRange label . (constructor AArch64AssemblyResult AArch64AssemblyDisplacementOutOfRange label)) (branch AArch64AssemblyOperandRefused value . (constructor AArch64AssemblyResult AArch64AssemblyOperandRefused value)))) (branch AArch64ImmediateOutOfRange value . (constructor AArch64AssemblyResult AArch64AssemblyOperandRefused value)) (branch AArch64MisalignedOffset value . (constructor AArch64AssemblyResult AArch64AssemblyDisplacementOutOfRange name)) (branch AArch64DisplacementOutOfRange value . (constructor AArch64AssemblyResult AArch64AssemblyDisplacementOutOfRange name)))))) -- Encode a label-relative word: look the target up, then build the -- instruction with the direction and distance from this word. def aarch64EncodeToLabel = (lambda unrestricted name : Bytes . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted source : Nat . (lambda unrestricted build : (pi unrestricted direction : (family AArch64Direction) . (pi unrestricted distance : Nat . (family AArch64Instruction))) . (lambda unrestricted tailResult : (family AArch64AssemblyResult) . (eliminate AArch64LabelLookupResult (lambda unrestricted lookup : (family AArch64LabelLookupResult) . (family AArch64AssemblyResult)) (aarch64LookupLabel name labels) (branch AArch64LabelFound target . (aarch64PrependWord name (aarch64EncodeInstruction (build (aarch64DirectionTo source target) (aarch64DistanceTo source target))) tailResult)) (branch AArch64LabelMissing . (constructor AArch64AssemblyResult AArch64AssemblyMissingLabel name)))))))) def aarch64EncodeAssemblyFrom : (pi unrestricted assembly : (family AArch64Assembly) . (pi unrestricted labels : (family AArch64LabelTable) . (pi unrestricted offset : Nat . (family AArch64AssemblyResult)))) = (lambda unrestricted assembly : (family AArch64Assembly) . (eliminate AArch64Assembly (lambda unrestricted current : (family AArch64Assembly) . (pi unrestricted labels : (family AArch64LabelTable) . (pi unrestricted offset : Nat . (family AArch64AssemblyResult)))) assembly (branch AArch64AssemblyEnd . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (constructor AArch64AssemblyResult AArch64AssemblyEncoded b"")))) (branch AArch64AssemblyEmit instruction tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64PrependWord b"" (aarch64EncodeInstruction instruction) (encodeTail labels (naturalAdd offset 4)))))) (branch AArch64AssemblyLabel name tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (encodeTail labels offset)))) (branch AArch64AssemblyBranch target tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64EncodeToLabel target labels offset (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (constructor AArch64Instruction AArch64Branch direction distance))) (encodeTail labels (naturalAdd offset 4)))))) (branch AArch64AssemblyBranchLink target tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64EncodeToLabel target labels offset (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (constructor AArch64Instruction AArch64BranchLink direction distance))) (encodeTail labels (naturalAdd offset 4)))))) (branch AArch64AssemblyBranchIf condition target tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64EncodeToLabel target labels offset (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (constructor AArch64Instruction AArch64BranchIf condition direction distance))) (encodeTail labels (naturalAdd offset 4)))))) (branch AArch64AssemblyCompareBranchIfZero register target tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64EncodeToLabel target labels offset (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (constructor AArch64Instruction AArch64CompareBranchIfZero register direction distance))) (encodeTail labels (naturalAdd offset 4)))))) (branch AArch64AssemblyCompareBranchIfNotZero register target tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64EncodeToLabel target labels offset (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (constructor AArch64Instruction AArch64CompareBranchIfNotZero register direction distance))) (encodeTail labels (naturalAdd offset 4)))))) (branch AArch64AssemblyAddressOf destination target tail encodeTail . (lambda unrestricted labels : (family AArch64LabelTable) . (lambda unrestricted offset : Nat . (aarch64EncodeToLabel target labels offset (lambda unrestricted direction : (family AArch64Direction) . (lambda unrestricted distance : Nat . (constructor AArch64Instruction AArch64AddressRelative destination direction distance))) (encodeTail labels (naturalAdd offset 4)))))))) def aarch64Assemble : (pi unrestricted assembly : (family AArch64Assembly) . (family AArch64AssemblyResult)) = (lambda unrestricted assembly : (family AArch64Assembly) . (eliminate AArch64AssemblyLayoutResult (lambda unrestricted layout : (family AArch64AssemblyLayoutResult) . (family AArch64AssemblyResult)) (aarch64LayoutAssembly assembly) (branch AArch64AssemblyLayoutSuccess labels size . (aarch64EncodeAssemblyFrom assembly labels 0)) (branch AArch64AssemblyDuplicateLabel duplicate . (constructor AArch64AssemblyResult AArch64AssemblyEncodeDuplicateLabel duplicate))))