Compiler.MachineX86Native

818def x86NativeLoadEffectiveAddressRIPHead :
819  (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
820  (lambda unrestricted destination : (family X86NativeRegister64) .
821    (eliminate
822      X86NativeRegister64
823      (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
824      destination
825      (branch X86NativeRAX . (bytes 72 141 5))
826      (branch X86NativeRCX . (bytes 72 141 13))
827      (branch X86NativeRDX . (bytes 72 141 21))
828      (branch X86NativeRBX . (bytes 72 141 29))
829      (branch X86NativeRSP . (bytes 72 141 37))
830      (branch X86NativeRBP . (bytes 72 141 45))
831      (branch X86NativeRSI . (bytes 72 141 53))
832      (branch X86NativeRDI . (bytes 72 141 61))
833      (branch X86NativeR8 . (bytes 76 141 5))
834      (branch X86NativeR9 . (bytes 76 141 13))
835      (branch X86NativeR10 . (bytes 76 141 21))
836      (branch X86NativeR11 . (bytes 76 141 29))
837      (branch X86NativeR12 . (bytes 76 141 37))
838      (branch X86NativeR13 . (bytes 76 141 45))
839      (branch X86NativeR14 . (bytes 76 141 53))
840      (branch X86NativeR15 . (bytes 76 141 61))))