module Runtime.NativeDescriptor

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.NativePhysicalNative
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Std.Natural

-- Admit a Linux descriptor-returning syscall result: [0, INT_MAX] succeeds;
-- negative kernel errors survive unchanged, oversized positive words fail.
-- This does not test whether an arbitrary integer names an open descriptor.
def nativeDescriptorStatusAssembly =
  (nativePhysicalNativeEmit
    (nativePhysicalNativeMove
      (constructor X86NativeRegister64 X86NativeRDI)
      (constructor X86NativeRegister64 X86NativeRAX))
    (nativePhysicalNativeEmit
      (nativePhysicalNativeTest
        (constructor X86NativeRegister64 X86NativeRAX)
        (constructor X86NativeRegister64 X86NativeRAX))
      (nativePhysicalNativeJumpCondition
        (constructor X86NativeCondition X86NativeConditionSign)
        b"descriptor-return"
        (nativePhysicalNativeEmit
          (nativePhysicalNativeCompareImmediate
            (constructor X86NativeRegister64 X86NativeRAX)
            (x86NativeImmediate32FromNatural 2147483647))
          (nativePhysicalNativeJumpCondition
            (constructor X86NativeCondition X86NativeConditionAbove)
            b"descriptor-invalid"
            (nativePhysicalNativeEmit
              (constructor
                X86NativeInstruction
                X86NativeClear32
                (constructor X86NativeRegister64 X86NativeRAX))
              (nativePhysicalNativeJump
                b"descriptor-return"
                (nativePhysicalNativeLabel
                  b"descriptor-invalid"
                  (nativePhysicalNativeEmit
                    (constructor
                      X86NativeInstruction
                      X86NativeClear32
                      (constructor X86NativeRegister64 X86NativeRAX))
                    (nativePhysicalNativeEmit
                      (nativePhysicalNativeAddImmediate
                        (constructor X86NativeRegister64 X86NativeRAX)
                        (x86NativeImmediate32FromNatural (naturalSaturatingSubtract 4294967296 22)))
                      (nativePhysicalNativeLabel
                        b"descriptor-return"
                        (nativePhysicalNativeEmit
                          nativePhysicalNativeReturnInstruction
                          (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))))

def nativeDescriptorStatusCode =
  (compiler-native-encode (family X86NativeAssembly) nativeDescriptorStatusAssembly)

def nativeDescriptorRequire =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted error : Bytes .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeLaunchRecipeCommand
            (constructor
              NativePhysicalOperation
              NativePhysicalMachineRoutine
              nativeDescriptorStatusCode
              (nativeLaunchRecipeArguments
                descriptor
                (nativeLaunchRecipeImmediate 0)
                (nativeLaunchRecipeImmediate 0)
                (nativeLaunchRecipeImmediate 0))
              (nativeLaunchRecipeStore slot))
            error
            (nativeLaunchRecipeAssertEqual
              (nativeLaunchRecipeSlotValue slot)
              (nativeLaunchRecipeImmediate 0)
              error
              tail))))))