module Platform.AArch64.MemoryRoutine

import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Platform.AArch64.RoutineEmitter

-- AAPCS64 realizations of Runtime.NativeMemoryRoutine's admitted views:
-- x0 destination/left, x1 source/right, x2 extent. Copy requires disjoint or
-- identical regions and returns zero; comparison returns one iff every byte
-- matches. Empty views access no memory. No x19-x29 or stack state is changed.
-- This is a bounded integrity comparison, not a constant-time secret compare.
def aarch64MemoryCopyAssembly =
  (ahrCmpImm
    (constructor AArch64Register AArch64X2)
    0
    (app
      (lambda unrestricted tail : (family AArch64Assembly) .
        (constructor
          AArch64Assembly
          AArch64AssemblyBranchIf
          (constructor AArch64Condition AArch64Equal)
          b"done"
          tail))
      (ahrLabel
        b"copy"
        (ahrEmit
          (constructor
            AArch64Instruction
            AArch64LoadMemory8ZeroExtend
            (constructor AArch64Register AArch64X3)
            (constructor AArch64Register AArch64X1)
            0)
          (ahrEmit
            (constructor
              AArch64Instruction
              AArch64StoreMemory8
              (constructor AArch64Register AArch64X0)
              0
              (constructor AArch64Register AArch64X3))
            (ahrEmit
              (constructor
                AArch64Instruction
                AArch64AddImmediate
                (constructor AArch64Register AArch64X0)
                (constructor AArch64Register AArch64X0)
                1)
              (ahrEmit
                (constructor
                  AArch64Instruction
                  AArch64AddImmediate
                  (constructor AArch64Register AArch64X1)
                  (constructor AArch64Register AArch64X1)
                  1)
                (ahrEmit
                  (constructor
                    AArch64Instruction
                    AArch64SubtractImmediate
                    (constructor AArch64Register AArch64X2)
                    (constructor AArch64Register AArch64X2)
                    1)
                  (ahrCmpImm
                    (constructor AArch64Register AArch64X2)
                    0
                    (app
                      (lambda unrestricted tail : (family AArch64Assembly) .
                        (constructor
                          AArch64Assembly
                          AArch64AssemblyBranchIf
                          (constructor AArch64Condition AArch64NotEqual)
                          b"copy"
                          tail))
                      (ahrLabel
                        b"done"
                        (ahrMovImm (constructor AArch64Register AArch64X0) 0 (ahrReturn ahrEnd)))))))))))))

def aarch64MemoryCopyCode =
  (aarch64RoutineBytes aarch64MemoryCopyAssembly)

def aarch64MemoryEqualAssembly =
  (ahrCmpImm
    (constructor AArch64Register AArch64X2)
    0
    (app
      (lambda unrestricted tail : (family AArch64Assembly) .
        (constructor
          AArch64Assembly
          AArch64AssemblyBranchIf
          (constructor AArch64Condition AArch64Equal)
          b"equal"
          tail))
      (ahrLabel
        b"compare"
        (ahrEmit
          (constructor
            AArch64Instruction
            AArch64LoadMemory8ZeroExtend
            (constructor AArch64Register AArch64X3)
            (constructor AArch64Register AArch64X0)
            0)
          (ahrEmit
            (constructor
              AArch64Instruction
              AArch64LoadMemory8ZeroExtend
              (constructor AArch64Register AArch64X4)
              (constructor AArch64Register AArch64X1)
              0)
            (ahrEmit
              (constructor
                AArch64Instruction
                AArch64CompareRegister
                (constructor AArch64Register AArch64X3)
                (constructor AArch64Register AArch64X4))
              (app
                (lambda unrestricted tail : (family AArch64Assembly) .
                  (constructor
                    AArch64Assembly
                    AArch64AssemblyBranchIf
                    (constructor AArch64Condition AArch64NotEqual)
                    b"different"
                    tail))
                (ahrEmit
                  (constructor
                    AArch64Instruction
                    AArch64AddImmediate
                    (constructor AArch64Register AArch64X0)
                    (constructor AArch64Register AArch64X0)
                    1)
                  (ahrEmit
                    (constructor
                      AArch64Instruction
                      AArch64AddImmediate
                      (constructor AArch64Register AArch64X1)
                      (constructor AArch64Register AArch64X1)
                      1)
                    (ahrEmit
                      (constructor
                        AArch64Instruction
                        AArch64SubtractImmediate
                        (constructor AArch64Register AArch64X2)
                        (constructor AArch64Register AArch64X2)
                        1)
                      (ahrCmpImm
                        (constructor AArch64Register AArch64X2)
                        0
                        (app
                          (lambda unrestricted tail : (family AArch64Assembly) .
                            (constructor
                              AArch64Assembly
                              AArch64AssemblyBranchIf
                              (constructor AArch64Condition AArch64NotEqual)
                              b"compare"
                              tail))
                          (ahrLabel
                            b"equal"
                            (ahrMovImm
                              (constructor AArch64Register AArch64X0)
                              1
                              (ahrReturn
                                (ahrLabel
                                  b"different"
                                  (ahrMovImm
                                    (constructor AArch64Register AArch64X0)
                                    0
                                    (ahrReturn ahrEnd))))))))))))))))))

def aarch64MemoryEqualCode =
  (aarch64RoutineBytes aarch64MemoryEqualAssembly)