AlphaGitHub
Source/Packages

Compiler.MachineX86Native

packages/compiler/src/Compiler/MachineX86Native.alpha

1,314 lines242 declarations56.6 KiBSHA-256 b3ccf0f17d32
Download exact fileView at revisionf5034773ad4bb52133

def · lines 854–867

x86NativeRegisterInstructionBytes

Full file
854def x86NativeRegisterInstructionBytes :
855  (pi unrestricted opcode : Byte .
856    (pi unrestricted source : (family X86NativeRegister64) .
857      (pi unrestricted destination : (family X86NativeRegister64) . Bytes))) =
858  (lambda unrestricted opcode : Byte .
859    (lambda unrestricted source : (family X86NativeRegister64) .
860      (lambda unrestricted destination : (family X86NativeRegister64) .
861        (bytes-append
862          (x86NativeRexWRegisterPair source destination)
863          (bytes-append
864            (bytes opcode)
865            (x86NativeModRMRegister
866              (x86NativeRegisterLow3 source)
867              (x86NativeRegisterLow3 destination)))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.