an SSE instruction with an XMM register in ModRM.reg and a general
register in ModRM.rm: the mandatory prefix, REX (W when `wide`; B for
r8 .. r15; none when neither), 0F, the opcode
1050def x86NativeXMMGeneralBytes :
1051 (pi unrestricted prefix : Byte .
1052 (pi unrestricted wide : Nat .
1053 (pi unrestricted opcode : Byte .
1054 (pi unrestricted xmm : (family X86NativeRegisterXMM) .
1055 (pi unrestricted general : (family X86NativeRegister64) . Bytes))))) =
1056 (lambda unrestricted prefix : Byte .
1057 (lambda unrestricted wide : Nat .
1058 (lambda unrestricted opcode : Byte .
1059 (lambda unrestricted xmm : (family X86NativeRegisterXMM) .
1060 (lambda unrestricted general : (family X86NativeRegister64) .
1061 (bytes-append
1062 (bytes prefix)
1063 (bytes-append
1064 (eliminate
1065 X86NativeRegisterBank
1066 (lambda unrestricted bank : (family X86NativeRegisterBank) . Bytes)
1067 (x86NativeRegisterBank general)
1068 (branch X86NativeLowBank . (nat-eliminate (lambda unrestricted w : Nat . Bytes) b"" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"H")) wide))
1069 (branch X86NativeHighBank . (nat-eliminate (lambda unrestricted w : Nat . Bytes) b"A" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"I")) wide)))
1070 (bytes-append
1071 (bytes 15 opcode)
1072 (x86NativeModRMRegister (x86NativeRegisterXMMLow3 xmm) (x86NativeRegisterLow3 general))))))))))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.