module Runtime.NativeWordArithmetic

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad

-- System V: RDI destination, RSI left, RDX right. Unsigned addition returns
-- zero and stores the sum, or one on overflow without touching destination.
-- No pointer or counter is truncated to a signed immediate. The carry branch
-- must precede the store: recovery and frame versions cannot wrap into reuse.
def nativeCheckedWordAddAssembly : (family X86NativeAssembly) =
  (constructor
    X86NativeAssembly
    X86NativeAssemblyEmit
    (constructor
      X86NativeInstruction
      X86NativeAddRegister64
      (constructor X86NativeRegister64 X86NativeRDX)
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor
      X86NativeAssembly
      X86NativeAssemblyJumpCondition
      (constructor X86NativeCondition X86NativeConditionBelow)
      b"overflow"
      (constructor
        X86NativeAssembly
        X86NativeAssemblyEmit
        (constructor
          X86NativeInstruction
          X86NativeStoreMemory64
          (constructor X86NativeRegister64 X86NativeRDI)
          (x86NativeDisplacement32FromNatural 0)
          (constructor X86NativeRegister64 X86NativeRSI))
        (constructor
          X86NativeAssembly
          X86NativeAssemblyEmit
          (constructor
            X86NativeInstruction
            X86NativeClear32
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor
            X86NativeAssembly
            X86NativeAssemblyEmit
            (constructor X86NativeInstruction X86NativeReturn)
            (constructor
              X86NativeAssembly
              X86NativeAssemblyLabel
              b"overflow"
              (constructor
                X86NativeAssembly
                X86NativeAssemblyEmit
                (constructor
                  X86NativeInstruction
                  X86NativeMoveImmediate32
                  (constructor X86NativeRegister64 X86NativeRAX)
                  (x86NativeImmediate32FromNatural 1))
                (constructor
                  X86NativeAssembly
                  X86NativeAssemblyEmit
                  (constructor X86NativeInstruction X86NativeReturn)
                  (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))

def nativeCheckedWordAddCode : Bytes =
  (compiler-native-encode (family X86NativeAssembly) nativeCheckedWordAddAssembly)

def nativeCheckedWordAdd =
  (lambda unrestricted destination : (family NativePhysicalOperand) .
    (lambda unrestricted left : (family NativePhysicalOperand) .
      (lambda unrestricted right : (family NativePhysicalOperand) .
        (lambda unrestricted slot : Nat .
          (lambda unrestricted error : Bytes .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (constructor
                  NativePhysicalOperation
                  NativePhysicalMachineRoutine
                  nativeCheckedWordAddCode
                  (nativeLaunchRecipeArguments
                    destination
                    left
                    right
                    (nativeLaunchRecipeImmediate 0))
                  (nativeLaunchRecipeStore slot))
                error
                (nativeLaunchRecipeAssertEqual
                  (nativeLaunchRecipeSlotValue slot)
                  (nativeLaunchRecipeImmediate 0)
                  error
                  tail))))))))