module Runtime.NativeLaunchRecipeRoutine

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.NativePhysicalNative
import Runtime.LaunchRecipe

-- The shared host routine that expands a launch-table recipe into a mapped
-- arena at startup.  The compiler emits one recipe per NVIDIA component
-- (program, QMD, pushbuffer, GPFIFO) from the schedule's repeat structure and
-- has already checked that the recipe expands to the exact table; this
-- routine is the same expansion in x86-64, bounded and fail-closed.
--
-- Recipe (little-endian):
--   "ALXR" u32 version=1  u64 outputExtent  u32 opCount  u32 zero
--   0x01 LITERAL u32 length bytes[length]
--   0x02 ZERO    u32 length
--   0x03 REPEAT  u32 count u32 unitLength u32 patchCount unit[unitLength]
--                patches[patchCount]{u32 offset u64 stride}
-- REPEAT copies the unit, then for each further copy duplicates the previous
-- copy and adds every patch's stride to the 64-bit word at its offset.
--
-- ABI (System V): rdi = recipe, rsi = recipe extent, rdx = output,
-- rcx = expected output extent.  Returns rax = bytes written, or zero when the
-- recipe is malformed, exceeds a bound, or does not fill the expected extent
-- exactly.  Uses only caller-saved registers and the red zone below rsp.
--
-- Red zone slots (below rsp): -8 output start, -16 unit pointer,
-- -24 unit length, -32 patch cursor, -40 patch count, -48 remaining copies,
-- -56 recipe cursor after the repeat, -64 patch base.

def lrRAX : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRAX)
def lrRCX : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRCX)
def lrRDX : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRDX)
def lrRSI : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRSI)
def lrRDI : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRDI)
def lrRSP : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeRSP)
def lrR8 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR8)
def lrR9 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR9)
def lrR10 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR10)
def lrR11 : (family X86NativeRegister64) = (constructor X86NativeRegister64 X86NativeR11)

def lrBelow : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionBelow)
def lrAbove : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionAbove)
def lrZero : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionZero)
def lrNotZero : (family X86NativeCondition) = (constructor X86NativeCondition X86NativeConditionNotZero)

-- One instruction per line.  destination = source
def lrMove =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted source : (family X86NativeRegister64) .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeMove source destination) tail))))

-- destination += source
def lrAdd =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted source : (family X86NativeRegister64) .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeAdd source destination) tail))))

-- destination -= source
def lrSubtract =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted source : (family X86NativeRegister64) .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeSubtract source destination) tail))))

def lrAddImmediate =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted immediate : Nat .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeAddImmediate destination (x86NativeImmediate32FromNatural immediate)) tail))))

-- flags from left - right: Below means left < right, Above means left > right
def lrCompare =
  (lambda unrestricted left : (family X86NativeRegister64) .
    (lambda unrestricted right : (family X86NativeRegister64) .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeCompare right left) tail))))

def lrCompareImmediate =
  (lambda unrestricted left : (family X86NativeRegister64) .
    (lambda unrestricted immediate : Nat .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeCompareImmediate left (x86NativeImmediate32FromNatural immediate)) tail))))

def lrTest =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (nativePhysicalNativeEmit (nativePhysicalNativeTest register register) tail)))

def lrLoad64 =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted base : (family X86NativeRegister64) .
      (lambda unrestricted displacement : Nat .
        (lambda unrestricted tail : (family X86NativeAssembly) .
          (nativePhysicalNativeEmit (nativePhysicalNativeLoad64 destination base (x86NativeDisplacement32FromNatural displacement)) tail)))))

def lrLoad32 =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted base : (family X86NativeRegister64) .
      (lambda unrestricted displacement : Nat .
        (lambda unrestricted tail : (family X86NativeAssembly) .
          (nativePhysicalNativeEmit
            (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 destination base (x86NativeDisplacement32FromNatural displacement))
            tail)))))

def lrLoad8 =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted base : (family X86NativeRegister64) .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeLoad8 destination base nativePhysicalNativeD0) tail))))

def lrStore64 =
  (lambda unrestricted base : (family X86NativeRegister64) .
    (lambda unrestricted displacement : Nat .
      (lambda unrestricted source : (family X86NativeRegister64) .
        (lambda unrestricted tail : (family X86NativeAssembly) .
          (nativePhysicalNativeEmit (nativePhysicalNativeStore64 base (x86NativeDisplacement32FromNatural displacement) source) tail)))))

def lrStore8 =
  (lambda unrestricted base : (family X86NativeRegister64) .
    (lambda unrestricted source : (family X86NativeRegister64) .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit (nativePhysicalNativeStore8 base nativePhysicalNativeD0 source) tail))))

def lrClear =
  (lambda unrestricted register : (family X86NativeRegister64) .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (nativePhysicalNativeEmit (constructor X86NativeInstruction X86NativeClear32 register) tail)))

def lrMultiplyImmediate =
  (lambda unrestricted destination : (family X86NativeRegister64) .
    (lambda unrestricted immediate : Nat .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit
          (constructor X86NativeInstruction X86NativeMultiplyImmediate64 destination (x86NativeImmediate32FromNatural immediate))
          tail))))

def lrLabel = nativePhysicalNativeLabel
def lrJump = nativePhysicalNativeJump
def lrJumpIf = nativePhysicalNativeJumpCondition

def lrReturn =
  (lambda unrestricted tail : (family X86NativeAssembly) .
    (nativePhysicalNativeEmit nativePhysicalNativeReturnInstruction tail))

def lrBackendJumpIf = (lambda unrestricted condition : (family LaunchRecipeCondition) .
  (eliminate LaunchRecipeCondition
    (lambda unrestricted current : (family LaunchRecipeCondition) . (pi unrestricted name : Bytes . (pi unrestricted tail : (family X86NativeAssembly) . (family X86NativeAssembly)))) condition
    (branch LaunchRecipeBelow . (lrJumpIf lrBelow))
    (branch LaunchRecipeAbove . (lrJumpIf lrAbove))
    (branch LaunchRecipeZero . (lrJumpIf lrZero))
    (branch LaunchRecipeNotZero . (lrJumpIf lrNotZero))))

def lrX86Backend : (family LaunchRecipeBackend (family X86NativeAssembly) (family X86NativeRegister64)) =
  (constructor LaunchRecipeBackend LaunchRecipeBackendValue (family X86NativeAssembly) (family X86NativeRegister64)
    lrMove lrAdd lrSubtract lrAddImmediate lrCompare lrCompareImmediate lrTest
    lrLoad64 lrLoad32 lrLoad8 lrStore64 lrStore8 lrClear lrMultiplyImmediate
    lrLabel lrJump lrBackendJumpIf lrReturn (constructor X86NativeAssembly X86NativeAssemblyEnd)
    lrRAX lrRCX lrRDX lrRSI lrRDI lrRSP lrR8 lrR9 lrR10 lrR11)

def nativeLaunchRecipeAssembly : (family X86NativeAssembly) =
  (launchRecipeAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) lrX86Backend)

def nativeLaunchRecipeGenerateRoutine : (family X86NativeAssemblyResult) =
  (x86NativeAssemble nativeLaunchRecipeAssembly)

-- The routine's machine code, or empty bytes when assembly is refused.
def nativeLaunchRecipeRoutineBytes : Bytes =
  (eliminate
    X86NativeAssemblyResult
    (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
    nativeLaunchRecipeGenerateRoutine
    (branch X86NativeAssemblyEncoded code . code)
    (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
    (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
    (branch X86NativeAssemblyMissingLabel name . b"")
    (branch X86NativeAssemblyDisplacementOutOfRange ordinal . b""))