module Platform.AArch64.NativePhysicalELF

import Compiler.ELF
import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Data.Bytes
import Model.Config
import Model.Parameter
import Model.Word32
import Model.Word64
import Platform.AArch64.NativePhysicalRuntime
import Runtime.NativePhysicalImage
import Runtime.NativePhysicalNativeELF
import Runtime.NativePhysicalProgram
import Std.Byte
import Std.Natural

-- The AArch64 twin of Runtime.NativePhysicalNativeELF's fast path: the same
-- aligned V3 command image (Runtime.NativePhysicalImage owns the format), the
-- AArch64 runtime in front of it, and the same static ELF64 container with
-- e_machine 183.  Everything else in the header -- entry 0x400078, one
-- PT_LOAD at 0x400000 with a 4 MiB memory extent, 4 KiB alignment -- is the
-- x86-64 header's, byte for byte.  The result reuses the x86 module's
-- artifact and telemetry families so a caller can handle either target's
-- artifact with one eliminator.
-- The container is Compiler.ELF's, with e_machine 183 and its memory extent
-- its file extent (Compiler.ELF.wrapMachineCodeExactFor).
def aarch64WrapMachineCodeSparseLarge = (wrapMachineCodeExactFor elfMachineAArch64)

def aarch64NativePhysicalGenerateELFFast =
  (lambda unrestricted program : (family NativePhysicalProgram) .
    (eliminate
      NativePhysicalImageResult
      (lambda unrestricted current : (family NativePhysicalImageResult) .
        (family NativePhysicalNativeELFResult))
      (nativePhysicalGenerateImageAlignedFast program)
      (branch
        NativePhysicalImageGenerated
        image
        imageTelemetry
        .
        (eliminate
          NativePhysicalImage
          (lambda unrestricted current : (family NativePhysicalImage) .
            (family NativePhysicalNativeELFResult))
          image
          (branch
            NativePhysicalImageValue
            imageBytes
            bodyDigest
            identity
            commandCount
            stateExtent
            resultSlots
            telemetry
            .
            (eliminate
              AArch64AssemblyResult
              (lambda unrestricted current : (family AArch64AssemblyResult) .
                (family NativePhysicalNativeELFResult))
              aarch64NativePhysicalRuntime
              (branch
                AArch64AssemblyEncoded
                codeBytes
                .
                (app
                  (lambda unrestricted machineBytes : Bytes .
                    (app
                      (lambda unrestricted elfBytes : Bytes .
                        (constructor
                          NativePhysicalNativeELFResult
                          NativePhysicalNativeELFGenerated
                          (constructor
                            NativePhysicalNativeELFArtifact
                            NativePhysicalNativeELFArtifactValue
                            elfBytes
                            codeBytes
                            imageBytes
                            machineBytes
                            identity
                            b""
                            b""
                            b""
                            b""
                            commandCount
                            (nativePhysicalNativeELFTelemetryFor
                              codeBytes
                              imageBytes
                              machineBytes
                              elfBytes
                              identity
                              b""
                              b""
                              b""
                              b""))
                          (nativePhysicalNativeELFTelemetryFor
                            codeBytes
                            imageBytes
                            machineBytes
                            elfBytes
                            identity
                            b""
                            b""
                            b""
                            b"")))
                      (aarch64WrapMachineCodeSparseLarge machineBytes)))
                  (bytes-append codeBytes imageBytes)))
              (branch
                AArch64AssemblyEncodeDuplicateLabel
                duplicateName
                .
                (nativePhysicalNativeELFFail
                  nativePhysicalNativeELFAssemblyFailurePhase
                  (constructor
                    NativePhysicalNativeELFErrorCode
                    NativePhysicalNativeELFDuplicateLabel
                    duplicateName)
                  b""
                  duplicateName))
              (branch
                AArch64AssemblyMissingLabel
                missingName
                .
                (nativePhysicalNativeELFFail
                  nativePhysicalNativeELFAssemblyFailurePhase
                  (constructor
                    NativePhysicalNativeELFErrorCode
                    NativePhysicalNativeELFMissingLabel
                    missingName)
                  b""
                  missingName))
              (branch
                AArch64AssemblyDisplacementOutOfRange
                distantName
                .
                (nativePhysicalNativeELFFail
                  nativePhysicalNativeELFAssemblyFailurePhase
                  (constructor
                    NativePhysicalNativeELFErrorCode
                    NativePhysicalNativeELFDisplacementOutOfRange
                    distantName)
                  b""
                  distantName))
              (branch
                AArch64AssemblyOperandRefused
                value
                .
                (nativePhysicalNativeELFFail
                  nativePhysicalNativeELFAssemblyFailurePhase
                  (constructor
                    NativePhysicalNativeELFErrorCode
                    NativePhysicalNativeELFAssemblyOffsetOverflow)
                  b""
                  b""))))))
      (branch
        NativePhysicalImageGenerationFailed
        imageError
        failureTelemetry
        .
        (nativePhysicalNativeELFFail
          nativePhysicalNativeELFImageFailurePhase
          (constructor
            NativePhysicalNativeELFErrorCode
            NativePhysicalNativeELFImageGenerationFailed
            imageError)
          (nativePhysicalNativeELFEncodeImageFailureTelemetry failureTelemetry)
          b""))))