module Compiler.MachineX86Native import Std.Natural family X86NativeRegister64 : Type 0 constructor X86NativeRAX constructor X86NativeRCX constructor X86NativeRDX constructor X86NativeRBX constructor X86NativeRSP constructor X86NativeRBP constructor X86NativeRSI constructor X86NativeRDI constructor X86NativeR8 constructor X86NativeR9 constructor X86NativeR10 constructor X86NativeR11 constructor X86NativeR12 constructor X86NativeR13 constructor X86NativeR14 constructor X86NativeR15 end-family family X86NativeImmediate32 : Type 0 constructor X86NativeImmediate32Value field unrestricted x86NativeImmediate32Byte0 : Byte field unrestricted x86NativeImmediate32Byte1 : Byte field unrestricted x86NativeImmediate32Byte2 : Byte field unrestricted x86NativeImmediate32Byte3 : Byte end-family family X86NativeImmediate8 : Type 0 constructor X86NativeImmediate8Value field unrestricted x86NativeImmediate8Byte0 : Byte end-family family X86NativeImmediate64 : Type 0 constructor X86NativeImmediate64Value field unrestricted x86NativeImmediate64Byte0 : Byte field unrestricted x86NativeImmediate64Byte1 : Byte field unrestricted x86NativeImmediate64Byte2 : Byte field unrestricted x86NativeImmediate64Byte3 : Byte field unrestricted x86NativeImmediate64Byte4 : Byte field unrestricted x86NativeImmediate64Byte5 : Byte field unrestricted x86NativeImmediate64Byte6 : Byte field unrestricted x86NativeImmediate64Byte7 : Byte end-family family X86NativeDisplacement32 : Type 0 constructor X86NativeDisplacement32Value field unrestricted x86NativeDisplacement32Byte0 : Byte field unrestricted x86NativeDisplacement32Byte1 : Byte field unrestricted x86NativeDisplacement32Byte2 : Byte field unrestricted x86NativeDisplacement32Byte3 : Byte end-family family X86NativeRegisterLow3 : Type 0 constructor X86NativeLow0 constructor X86NativeLow1 constructor X86NativeLow2 constructor X86NativeLow3 constructor X86NativeLow4 constructor X86NativeLow5 constructor X86NativeLow6 constructor X86NativeLow7 end-family family X86NativeRegisterBank : Type 0 constructor X86NativeLowBank constructor X86NativeHighBank end-family -- the SSE registers the encoder names (xmm0 .. xmm7: no REX bit) family X86NativeRegisterXMM : Type 0 constructor X86NativeXMM0 constructor X86NativeXMM1 constructor X86NativeXMM2 constructor X86NativeXMM3 constructor X86NativeXMM4 constructor X86NativeXMM5 constructor X86NativeXMM6 constructor X86NativeXMM7 end-family -- the SSE2 scalar-double operations on two XMM registers (F2 0F op): -- destination op= source, the square root of the source, and the source -- rounded to binary32 (CVTSD2SS) -- in the MXCSR rounding mode family X86NativeScalarDoubleOperation : Type 0 constructor X86NativeScalarDoubleAdd constructor X86NativeScalarDoubleSubtract constructor X86NativeScalarDoubleMultiply constructor X86NativeScalarDoubleDivide constructor X86NativeScalarDoubleSquareRoot constructor X86NativeScalarDoubleToSingle end-family family X86NativeCondition : Type 0 constructor X86NativeConditionZero constructor X86NativeConditionNotZero constructor X86NativeConditionBelow constructor X86NativeConditionAbove constructor X86NativeConditionSign end-family family X86NativeInstruction : Type 0 constructor X86NativeMoveImmediate32 field unrestricted x86NativeMoveImmediate32Destination : (family X86NativeRegister64) field unrestricted x86NativeMoveImmediate32Value : (family X86NativeImmediate32) constructor X86NativeMoveImmediate64 field unrestricted x86NativeMoveImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeMoveImmediate64Value : (family X86NativeImmediate64) constructor X86NativeClear32 field unrestricted x86NativeClear32Destination : (family X86NativeRegister64) constructor X86NativeMoveRegister64 field unrestricted x86NativeMoveRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeMoveRegister64Destination : (family X86NativeRegister64) constructor X86NativeAddRegister64 field unrestricted x86NativeAddRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeAddRegister64Destination : (family X86NativeRegister64) constructor X86NativeSubtractRegister64 field unrestricted x86NativeSubtractRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeSubtractRegister64Destination : (family X86NativeRegister64) constructor X86NativeAndRegister64 field unrestricted x86NativeAndRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeAndRegister64Destination : (family X86NativeRegister64) constructor X86NativeOrRegister64 field unrestricted x86NativeOrRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeOrRegister64Destination : (family X86NativeRegister64) constructor X86NativeXorRegister64 field unrestricted x86NativeXorRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeXorRegister64Destination : (family X86NativeRegister64) constructor X86NativeCompareRegister64 field unrestricted x86NativeCompareRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeCompareRegister64Destination : (family X86NativeRegister64) constructor X86NativeTestRegister64 field unrestricted x86NativeTestRegister64Source : (family X86NativeRegister64) field unrestricted x86NativeTestRegister64Destination : (family X86NativeRegister64) constructor X86NativeAddImmediate64 field unrestricted x86NativeAddImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeAddImmediate64Value : (family X86NativeImmediate32) constructor X86NativeAndImmediate64 field unrestricted x86NativeAndImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeAndImmediate64Value : (family X86NativeImmediate32) constructor X86NativeCompareImmediate64 field unrestricted x86NativeCompareImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeCompareImmediate64Value : (family X86NativeImmediate32) constructor X86NativeMultiplyImmediate64 field unrestricted x86NativeMultiplyImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeMultiplyImmediate64Value : (family X86NativeImmediate32) -- Unsigned implicit-accumulator forms: multiply writes RDX:RAX; divide -- consumes RDX:RAX and writes quotient RAX and remainder RDX. The caller -- must establish a nonzero divisor and a quotient that fits in 64 bits. constructor X86NativeMultiplyRegister64Unsigned field unrestricted x86NativeMultiplyRegister64UnsignedSource : (family X86NativeRegister64) constructor X86NativeDivideRegister64Unsigned field unrestricted x86NativeDivideRegister64UnsignedDivisor : (family X86NativeRegister64) constructor X86NativeShiftLeftImmediate64 field unrestricted x86NativeShiftLeftImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeShiftLeftImmediate64Value : (family X86NativeImmediate8) constructor X86NativeShiftRightImmediate64 field unrestricted x86NativeShiftRightImmediate64Destination : (family X86NativeRegister64) field unrestricted x86NativeShiftRightImmediate64Value : (family X86NativeImmediate8) constructor X86NativeLoadMemory64 field unrestricted x86NativeLoadMemory64Destination : (family X86NativeRegister64) field unrestricted x86NativeLoadMemory64Base : (family X86NativeRegister64) field unrestricted x86NativeLoadMemory64Displacement : (family X86NativeDisplacement32) constructor X86NativeLoadMemory8ZeroExtend64 field unrestricted x86NativeLoadMemory8Destination : (family X86NativeRegister64) field unrestricted x86NativeLoadMemory8Base : (family X86NativeRegister64) field unrestricted x86NativeLoadMemory8Displacement : (family X86NativeDisplacement32) constructor X86NativeLoadMemory32ZeroExtend64 field unrestricted x86NativeLoadMemory32Destination : (family X86NativeRegister64) field unrestricted x86NativeLoadMemory32Base : (family X86NativeRegister64) field unrestricted x86NativeLoadMemory32Displacement : (family X86NativeDisplacement32) constructor X86NativeStoreMemory32 field unrestricted x86NativeStoreMemory32Base : (family X86NativeRegister64) field unrestricted x86NativeStoreMemory32Displacement : (family X86NativeDisplacement32) field unrestricted x86NativeStoreMemory32Source : (family X86NativeRegister64) constructor X86NativeStoreMemory64 field unrestricted x86NativeStoreMemory64Base : (family X86NativeRegister64) field unrestricted x86NativeStoreMemory64Displacement : (family X86NativeDisplacement32) field unrestricted x86NativeStoreMemory64Source : (family X86NativeRegister64) constructor X86NativeStoreMemory8 field unrestricted x86NativeStoreMemory8Base : (family X86NativeRegister64) field unrestricted x86NativeStoreMemory8Displacement : (family X86NativeDisplacement32) field unrestricted x86NativeStoreMemory8Source : (family X86NativeRegister64) constructor X86NativeStoreFence constructor X86NativeLoadEffectiveAddressRIP field unrestricted x86NativeLEADestination : (family X86NativeRegister64) field unrestricted x86NativeLEADisplacement : (family X86NativeDisplacement32) constructor X86NativeJumpRelative32 field unrestricted x86NativeJumpDisplacement : (family X86NativeDisplacement32) constructor X86NativeJumpConditionRelative32 field unrestricted x86NativeJumpCondition : (family X86NativeCondition) field unrestricted x86NativeJumpConditionDisplacement : (family X86NativeDisplacement32) constructor X86NativeCallRegister64 field unrestricted x86NativeCallRegister64Target : (family X86NativeRegister64) constructor X86NativeReturn constructor X86NativeSystemCall -- MOVQ xmm, r64 constructor X86NativeMoveToXMM64 field unrestricted x86NativeMoveToXMM64Destination : (family X86NativeRegisterXMM) field unrestricted x86NativeMoveToXMM64Source : (family X86NativeRegister64) -- MOVQ r64, xmm constructor X86NativeMoveFromXMM64 field unrestricted x86NativeMoveFromXMM64Destination : (family X86NativeRegister64) field unrestricted x86NativeMoveFromXMM64Source : (family X86NativeRegisterXMM) -- MOVD r32, xmm (zero-extended into the 64-bit register) constructor X86NativeMoveFromXMM32 field unrestricted x86NativeMoveFromXMM32Destination : (family X86NativeRegister64) field unrestricted x86NativeMoveFromXMM32Source : (family X86NativeRegisterXMM) constructor X86NativeScalarDouble field unrestricted x86NativeScalarDoubleOperation : (family X86NativeScalarDoubleOperation) field unrestricted x86NativeScalarDoubleDestination : (family X86NativeRegisterXMM) field unrestricted x86NativeScalarDoubleSource : (family X86NativeRegisterXMM) -- CVTSS2SD xmm, xmm: the source's binary32 as a binary64 constructor X86NativeScalarSingleToDouble field unrestricted x86NativeScalarSingleToDoubleDestination : (family X86NativeRegisterXMM) field unrestricted x86NativeScalarSingleToDoubleSource : (family X86NativeRegisterXMM) -- CVTSI2SD xmm, r64: the signed 64-bit integer as the nearest binary64 constructor X86NativeScalarDoubleFromInteger64 field unrestricted x86NativeScalarDoubleFromIntegerDestination : (family X86NativeRegisterXMM) field unrestricted x86NativeScalarDoubleFromIntegerSource : (family X86NativeRegister64) end-family family X86NativeProgram : Type 0 constructor X86NativeProgramEnd constructor X86NativeProgramNext field unrestricted x86NativeProgramInstruction : (family X86NativeInstruction) recursive unrestricted x86NativeProgramTail end-family def x86NativeImmediate32Bytes : (pi unrestricted immediate : (family X86NativeImmediate32) . Bytes) = (lambda unrestricted immediate : (family X86NativeImmediate32) . (eliminate X86NativeImmediate32 (lambda unrestricted value : (family X86NativeImmediate32) . Bytes) immediate (branch X86NativeImmediate32Value byte0 byte1 byte2 byte3 . (bytes byte0 byte1 byte2 byte3)))) def x86NativeImmediate8Bytes : (pi unrestricted immediate : (family X86NativeImmediate8) . Bytes) = (lambda unrestricted immediate : (family X86NativeImmediate8) . (eliminate X86NativeImmediate8 (lambda unrestricted value : (family X86NativeImmediate8) . Bytes) immediate (branch X86NativeImmediate8Value byte0 . (bytes byte0)))) def x86NativeImmediate64Bytes : (pi unrestricted immediate : (family X86NativeImmediate64) . Bytes) = (lambda unrestricted immediate : (family X86NativeImmediate64) . (eliminate X86NativeImmediate64 (lambda unrestricted value : (family X86NativeImmediate64) . Bytes) immediate (branch X86NativeImmediate64Value byte0 byte1 byte2 byte3 byte4 byte5 byte6 byte7 . (bytes byte0 byte1 byte2 byte3 byte4 byte5 byte6 byte7)))) def x86NativeDisplacement32Bytes : (pi unrestricted displacement : (family X86NativeDisplacement32) . Bytes) = (lambda unrestricted displacement : (family X86NativeDisplacement32) . (eliminate X86NativeDisplacement32 (lambda unrestricted value : (family X86NativeDisplacement32) . Bytes) displacement (branch X86NativeDisplacement32Value byte0 byte1 byte2 byte3 . (bytes byte0 byte1 byte2 byte3)))) def x86NativeMoveImmediate32Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 184)) (branch X86NativeRCX . (bytes 185)) (branch X86NativeRDX . (bytes 186)) (branch X86NativeRBX . (bytes 187)) (branch X86NativeRSP . (bytes 188)) (branch X86NativeRBP . (bytes 189)) (branch X86NativeRSI . (bytes 190)) (branch X86NativeRDI . (bytes 191)) (branch X86NativeR8 . (bytes 65 184)) (branch X86NativeR9 . (bytes 65 185)) (branch X86NativeR10 . (bytes 65 186)) (branch X86NativeR11 . (bytes 65 187)) (branch X86NativeR12 . (bytes 65 188)) (branch X86NativeR13 . (bytes 65 189)) (branch X86NativeR14 . (bytes 65 190)) (branch X86NativeR15 . (bytes 65 191)))) def x86NativeMoveImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 184)) (branch X86NativeRCX . (bytes 72 185)) (branch X86NativeRDX . (bytes 72 186)) (branch X86NativeRBX . (bytes 72 187)) (branch X86NativeRSP . (bytes 72 188)) (branch X86NativeRBP . (bytes 72 189)) (branch X86NativeRSI . (bytes 72 190)) (branch X86NativeRDI . (bytes 72 191)) (branch X86NativeR8 . (bytes 73 184)) (branch X86NativeR9 . (bytes 73 185)) (branch X86NativeR10 . (bytes 73 186)) (branch X86NativeR11 . (bytes 73 187)) (branch X86NativeR12 . (bytes 73 188)) (branch X86NativeR13 . (bytes 73 189)) (branch X86NativeR14 . (bytes 73 190)) (branch X86NativeR15 . (bytes 73 191)))) def x86NativeClear32Bytes : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 49 192)) (branch X86NativeRCX . (bytes 49 201)) (branch X86NativeRDX . (bytes 49 210)) (branch X86NativeRBX . (bytes 49 219)) (branch X86NativeRSP . (bytes 49 228)) (branch X86NativeRBP . (bytes 49 237)) (branch X86NativeRSI . (bytes 49 246)) (branch X86NativeRDI . (bytes 49 255)) (branch X86NativeR8 . (bytes 69 49 192)) (branch X86NativeR9 . (bytes 69 49 201)) (branch X86NativeR10 . (bytes 69 49 210)) (branch X86NativeR11 . (bytes 69 49 219)) (branch X86NativeR12 . (bytes 69 49 228)) (branch X86NativeR13 . (bytes 69 49 237)) (branch X86NativeR14 . (bytes 69 49 246)) (branch X86NativeR15 . (bytes 69 49 255)))) def x86NativeRegisterLow3 : (pi unrestricted register : (family X86NativeRegister64) . (family X86NativeRegisterLow3)) = (lambda unrestricted register : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . (family X86NativeRegisterLow3)) register (branch X86NativeRAX . (constructor X86NativeRegisterLow3 X86NativeLow0)) (branch X86NativeRCX . (constructor X86NativeRegisterLow3 X86NativeLow1)) (branch X86NativeRDX . (constructor X86NativeRegisterLow3 X86NativeLow2)) (branch X86NativeRBX . (constructor X86NativeRegisterLow3 X86NativeLow3)) (branch X86NativeRSP . (constructor X86NativeRegisterLow3 X86NativeLow4)) (branch X86NativeRBP . (constructor X86NativeRegisterLow3 X86NativeLow5)) (branch X86NativeRSI . (constructor X86NativeRegisterLow3 X86NativeLow6)) (branch X86NativeRDI . (constructor X86NativeRegisterLow3 X86NativeLow7)) (branch X86NativeR8 . (constructor X86NativeRegisterLow3 X86NativeLow0)) (branch X86NativeR9 . (constructor X86NativeRegisterLow3 X86NativeLow1)) (branch X86NativeR10 . (constructor X86NativeRegisterLow3 X86NativeLow2)) (branch X86NativeR11 . (constructor X86NativeRegisterLow3 X86NativeLow3)) (branch X86NativeR12 . (constructor X86NativeRegisterLow3 X86NativeLow4)) (branch X86NativeR13 . (constructor X86NativeRegisterLow3 X86NativeLow5)) (branch X86NativeR14 . (constructor X86NativeRegisterLow3 X86NativeLow6)) (branch X86NativeR15 . (constructor X86NativeRegisterLow3 X86NativeLow7)))) def x86NativeRegisterBank : (pi unrestricted register : (family X86NativeRegister64) . (family X86NativeRegisterBank)) = (lambda unrestricted register : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . (family X86NativeRegisterBank)) register (branch X86NativeRAX . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRCX . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRDX . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRBX . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRSP . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRBP . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRSI . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeRDI . (constructor X86NativeRegisterBank X86NativeLowBank)) (branch X86NativeR8 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR9 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR10 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR11 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR12 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR13 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR14 . (constructor X86NativeRegisterBank X86NativeHighBank)) (branch X86NativeR15 . (constructor X86NativeRegisterBank X86NativeHighBank)))) def x86NativeRexWRegisterPair : (pi unrestricted source : (family X86NativeRegister64) . (pi unrestricted destination : (family X86NativeRegister64) . Bytes)) = (lambda unrestricted source : (family X86NativeRegister64) . (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegisterBank (lambda unrestricted sourceBank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank source) (branch X86NativeLowBank . (eliminate X86NativeRegisterBank (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank destination) (branch X86NativeLowBank . b"H") (branch X86NativeHighBank . b"I"))) (branch X86NativeHighBank . (eliminate X86NativeRegisterBank (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank destination) (branch X86NativeLowBank . b"L") (branch X86NativeHighBank . b"M")))))) def x86NativeRexRegisterPair : (pi unrestricted source : (family X86NativeRegister64) . (pi unrestricted destination : (family X86NativeRegister64) . Bytes)) = (lambda unrestricted source : (family X86NativeRegister64) . (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegisterBank (lambda unrestricted sourceBank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank source) (branch X86NativeLowBank . (eliminate X86NativeRegisterBank (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank destination) (branch X86NativeLowBank . b"") (branch X86NativeHighBank . b"A"))) (branch X86NativeHighBank . (eliminate X86NativeRegisterBank (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank destination) (branch X86NativeLowBank . b"D") (branch X86NativeHighBank . b"E")))))) def x86NativeModRMRegisterRow0 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 192)) (branch X86NativeLow1 . (bytes 193)) (branch X86NativeLow2 . (bytes 194)) (branch X86NativeLow3 . (bytes 195)) (branch X86NativeLow4 . (bytes 196)) (branch X86NativeLow5 . (bytes 197)) (branch X86NativeLow6 . (bytes 198)) (branch X86NativeLow7 . (bytes 199)))) def x86NativeModRMRegisterRow1 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 200)) (branch X86NativeLow1 . (bytes 201)) (branch X86NativeLow2 . (bytes 202)) (branch X86NativeLow3 . (bytes 203)) (branch X86NativeLow4 . (bytes 204)) (branch X86NativeLow5 . (bytes 205)) (branch X86NativeLow6 . (bytes 206)) (branch X86NativeLow7 . (bytes 207)))) def x86NativeModRMRegisterRow2 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 208)) (branch X86NativeLow1 . (bytes 209)) (branch X86NativeLow2 . (bytes 210)) (branch X86NativeLow3 . (bytes 211)) (branch X86NativeLow4 . (bytes 212)) (branch X86NativeLow5 . (bytes 213)) (branch X86NativeLow6 . (bytes 214)) (branch X86NativeLow7 . (bytes 215)))) def x86NativeModRMRegisterRow3 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 216)) (branch X86NativeLow1 . (bytes 217)) (branch X86NativeLow2 . (bytes 218)) (branch X86NativeLow3 . (bytes 219)) (branch X86NativeLow4 . (bytes 220)) (branch X86NativeLow5 . (bytes 221)) (branch X86NativeLow6 . (bytes 222)) (branch X86NativeLow7 . (bytes 223)))) def x86NativeModRMRegisterRow4 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 224)) (branch X86NativeLow1 . (bytes 225)) (branch X86NativeLow2 . (bytes 226)) (branch X86NativeLow3 . (bytes 227)) (branch X86NativeLow4 . (bytes 228)) (branch X86NativeLow5 . (bytes 229)) (branch X86NativeLow6 . (bytes 230)) (branch X86NativeLow7 . (bytes 231)))) def x86NativeModRMRegisterRow5 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 232)) (branch X86NativeLow1 . (bytes 233)) (branch X86NativeLow2 . (bytes 234)) (branch X86NativeLow3 . (bytes 235)) (branch X86NativeLow4 . (bytes 236)) (branch X86NativeLow5 . (bytes 237)) (branch X86NativeLow6 . (bytes 238)) (branch X86NativeLow7 . (bytes 239)))) def x86NativeModRMRegisterRow6 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 240)) (branch X86NativeLow1 . (bytes 241)) (branch X86NativeLow2 . (bytes 242)) (branch X86NativeLow3 . (bytes 243)) (branch X86NativeLow4 . (bytes 244)) (branch X86NativeLow5 . (bytes 245)) (branch X86NativeLow6 . (bytes 246)) (branch X86NativeLow7 . (bytes 247)))) def x86NativeModRMRegisterRow7 : (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) destination (branch X86NativeLow0 . (bytes 248)) (branch X86NativeLow1 . (bytes 249)) (branch X86NativeLow2 . (bytes 250)) (branch X86NativeLow3 . (bytes 251)) (branch X86NativeLow4 . (bytes 252)) (branch X86NativeLow5 . (bytes 253)) (branch X86NativeLow6 . (bytes 254)) (branch X86NativeLow7 . (bytes 255)))) def x86NativeModRMRegister : (pi unrestricted source : (family X86NativeRegisterLow3) . (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes)) = (lambda unrestricted source : (family X86NativeRegisterLow3) . (lambda unrestricted destination : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) source (branch X86NativeLow0 . (x86NativeModRMRegisterRow0 destination)) (branch X86NativeLow1 . (x86NativeModRMRegisterRow1 destination)) (branch X86NativeLow2 . (x86NativeModRMRegisterRow2 destination)) (branch X86NativeLow3 . (x86NativeModRMRegisterRow3 destination)) (branch X86NativeLow4 . (x86NativeModRMRegisterRow4 destination)) (branch X86NativeLow5 . (x86NativeModRMRegisterRow5 destination)) (branch X86NativeLow6 . (x86NativeModRMRegisterRow6 destination)) (branch X86NativeLow7 . (x86NativeModRMRegisterRow7 destination))))) def x86NativeModRMMemoryRow0 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 128)) (branch X86NativeLow1 . (bytes 129)) (branch X86NativeLow2 . (bytes 130)) (branch X86NativeLow3 . (bytes 131)) (branch X86NativeLow4 . (bytes 132)) (branch X86NativeLow5 . (bytes 133)) (branch X86NativeLow6 . (bytes 134)) (branch X86NativeLow7 . (bytes 135)))) def x86NativeModRMMemoryRow1 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 136)) (branch X86NativeLow1 . (bytes 137)) (branch X86NativeLow2 . (bytes 138)) (branch X86NativeLow3 . (bytes 139)) (branch X86NativeLow4 . (bytes 140)) (branch X86NativeLow5 . (bytes 141)) (branch X86NativeLow6 . (bytes 142)) (branch X86NativeLow7 . (bytes 143)))) def x86NativeModRMMemoryRow2 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 144)) (branch X86NativeLow1 . (bytes 145)) (branch X86NativeLow2 . (bytes 146)) (branch X86NativeLow3 . (bytes 147)) (branch X86NativeLow4 . (bytes 148)) (branch X86NativeLow5 . (bytes 149)) (branch X86NativeLow6 . (bytes 150)) (branch X86NativeLow7 . (bytes 151)))) def x86NativeModRMMemoryRow3 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 152)) (branch X86NativeLow1 . (bytes 153)) (branch X86NativeLow2 . (bytes 154)) (branch X86NativeLow3 . (bytes 155)) (branch X86NativeLow4 . (bytes 156)) (branch X86NativeLow5 . (bytes 157)) (branch X86NativeLow6 . (bytes 158)) (branch X86NativeLow7 . (bytes 159)))) def x86NativeModRMMemoryRow4 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 160)) (branch X86NativeLow1 . (bytes 161)) (branch X86NativeLow2 . (bytes 162)) (branch X86NativeLow3 . (bytes 163)) (branch X86NativeLow4 . (bytes 164)) (branch X86NativeLow5 . (bytes 165)) (branch X86NativeLow6 . (bytes 166)) (branch X86NativeLow7 . (bytes 167)))) def x86NativeModRMMemoryRow5 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 168)) (branch X86NativeLow1 . (bytes 169)) (branch X86NativeLow2 . (bytes 170)) (branch X86NativeLow3 . (bytes 171)) (branch X86NativeLow4 . (bytes 172)) (branch X86NativeLow5 . (bytes 173)) (branch X86NativeLow6 . (bytes 174)) (branch X86NativeLow7 . (bytes 175)))) def x86NativeModRMMemoryRow6 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 176)) (branch X86NativeLow1 . (bytes 177)) (branch X86NativeLow2 . (bytes 178)) (branch X86NativeLow3 . (bytes 179)) (branch X86NativeLow4 . (bytes 180)) (branch X86NativeLow5 . (bytes 181)) (branch X86NativeLow6 . (bytes 182)) (branch X86NativeLow7 . (bytes 183)))) def x86NativeModRMMemoryRow7 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . (bytes 184)) (branch X86NativeLow1 . (bytes 185)) (branch X86NativeLow2 . (bytes 186)) (branch X86NativeLow3 . (bytes 187)) (branch X86NativeLow4 . (bytes 188)) (branch X86NativeLow5 . (bytes 189)) (branch X86NativeLow6 . (bytes 190)) (branch X86NativeLow7 . (bytes 191)))) def x86NativeModRMMemory : (pi unrestricted register : (family X86NativeRegisterLow3) . (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes)) = (lambda unrestricted register : (family X86NativeRegisterLow3) . (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) register (branch X86NativeLow0 . (x86NativeModRMMemoryRow0 base)) (branch X86NativeLow1 . (x86NativeModRMMemoryRow1 base)) (branch X86NativeLow2 . (x86NativeModRMMemoryRow2 base)) (branch X86NativeLow3 . (x86NativeModRMMemoryRow3 base)) (branch X86NativeLow4 . (x86NativeModRMMemoryRow4 base)) (branch X86NativeLow5 . (x86NativeModRMMemoryRow5 base)) (branch X86NativeLow6 . (x86NativeModRMMemoryRow6 base)) (branch X86NativeLow7 . (x86NativeModRMMemoryRow7 base))))) def x86NativeMemorySIB : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) = (lambda unrestricted base : (family X86NativeRegisterLow3) . (eliminate X86NativeRegisterLow3 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes) base (branch X86NativeLow0 . b"") (branch X86NativeLow1 . b"") (branch X86NativeLow2 . b"") (branch X86NativeLow3 . b"") (branch X86NativeLow4 . b"$") (branch X86NativeLow5 . b"") (branch X86NativeLow6 . b"") (branch X86NativeLow7 . b""))) def x86NativeMemoryInstructionBytes : (pi unrestricted opcode : Bytes . (pi unrestricted register : (family X86NativeRegister64) . (pi unrestricted base : (family X86NativeRegister64) . (pi unrestricted displacement : (family X86NativeDisplacement32) . Bytes)))) = (lambda unrestricted opcode : Bytes . (lambda unrestricted register : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted displacement : (family X86NativeDisplacement32) . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk (x86NativeRexWRegisterPair register base)) (bytes-builder-append (bytes-builder-chunk opcode) (bytes-builder-append (bytes-builder-chunk (x86NativeModRMMemory (x86NativeRegisterLow3 register) (x86NativeRegisterLow3 base))) (bytes-builder-append (bytes-builder-chunk (x86NativeMemorySIB (x86NativeRegisterLow3 base))) (bytes-builder-chunk (x86NativeDisplacement32Bytes displacement))))))))))) def x86NativeMemoryInstruction32Bytes : (pi unrestricted opcode : Bytes . (pi unrestricted register : (family X86NativeRegister64) . (pi unrestricted base : (family X86NativeRegister64) . (pi unrestricted displacement : (family X86NativeDisplacement32) . Bytes)))) = (lambda unrestricted opcode : Bytes . (lambda unrestricted register : (family X86NativeRegister64) . (lambda unrestricted base : (family X86NativeRegister64) . (lambda unrestricted displacement : (family X86NativeDisplacement32) . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk (x86NativeRexRegisterPair register base)) (bytes-builder-append (bytes-builder-chunk opcode) (bytes-builder-append (bytes-builder-chunk (x86NativeModRMMemory (x86NativeRegisterLow3 register) (x86NativeRegisterLow3 base))) (bytes-builder-append (bytes-builder-chunk (x86NativeMemorySIB (x86NativeRegisterLow3 base))) (bytes-builder-chunk (x86NativeDisplacement32Bytes displacement))))))))))) def x86NativeLoadEffectiveAddressRIPHead : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 141 5)) (branch X86NativeRCX . (bytes 72 141 13)) (branch X86NativeRDX . (bytes 72 141 21)) (branch X86NativeRBX . (bytes 72 141 29)) (branch X86NativeRSP . (bytes 72 141 37)) (branch X86NativeRBP . (bytes 72 141 45)) (branch X86NativeRSI . (bytes 72 141 53)) (branch X86NativeRDI . (bytes 72 141 61)) (branch X86NativeR8 . (bytes 76 141 5)) (branch X86NativeR9 . (bytes 76 141 13)) (branch X86NativeR10 . (bytes 76 141 21)) (branch X86NativeR11 . (bytes 76 141 29)) (branch X86NativeR12 . (bytes 76 141 37)) (branch X86NativeR13 . (bytes 76 141 45)) (branch X86NativeR14 . (bytes 76 141 53)) (branch X86NativeR15 . (bytes 76 141 61)))) def x86NativeConditionOpcode : (pi unrestricted condition : (family X86NativeCondition) . Byte) = (lambda unrestricted condition : (family X86NativeCondition) . (eliminate X86NativeCondition (lambda unrestricted value : (family X86NativeCondition) . Byte) condition (branch X86NativeConditionZero . (byte 132)) (branch X86NativeConditionNotZero . (byte 133)) (branch X86NativeConditionBelow . (byte 130)) (branch X86NativeConditionAbove . (byte 135)) (branch X86NativeConditionSign . (byte 136)))) def x86NativeRegisterInstructionBytes : (pi unrestricted opcode : Byte . (pi unrestricted source : (family X86NativeRegister64) . (pi unrestricted destination : (family X86NativeRegister64) . Bytes))) = (lambda unrestricted opcode : Byte . (lambda unrestricted source : (family X86NativeRegister64) . (lambda unrestricted destination : (family X86NativeRegister64) . (bytes-append (x86NativeRexWRegisterPair source destination) (bytes-append (bytes opcode) (x86NativeModRMRegister (x86NativeRegisterLow3 source) (x86NativeRegisterLow3 destination))))))) def x86NativeAddImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 129 192)) (branch X86NativeRCX . (bytes 72 129 193)) (branch X86NativeRDX . (bytes 72 129 194)) (branch X86NativeRBX . (bytes 72 129 195)) (branch X86NativeRSP . (bytes 72 129 196)) (branch X86NativeRBP . (bytes 72 129 197)) (branch X86NativeRSI . (bytes 72 129 198)) (branch X86NativeRDI . (bytes 72 129 199)) (branch X86NativeR8 . (bytes 73 129 192)) (branch X86NativeR9 . (bytes 73 129 193)) (branch X86NativeR10 . (bytes 73 129 194)) (branch X86NativeR11 . (bytes 73 129 195)) (branch X86NativeR12 . (bytes 73 129 196)) (branch X86NativeR13 . (bytes 73 129 197)) (branch X86NativeR14 . (bytes 73 129 198)) (branch X86NativeR15 . (bytes 73 129 199)))) def x86NativeAndImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 129 224)) (branch X86NativeRCX . (bytes 72 129 225)) (branch X86NativeRDX . (bytes 72 129 226)) (branch X86NativeRBX . (bytes 72 129 227)) (branch X86NativeRSP . (bytes 72 129 228)) (branch X86NativeRBP . (bytes 72 129 229)) (branch X86NativeRSI . (bytes 72 129 230)) (branch X86NativeRDI . (bytes 72 129 231)) (branch X86NativeR8 . (bytes 73 129 224)) (branch X86NativeR9 . (bytes 73 129 225)) (branch X86NativeR10 . (bytes 73 129 226)) (branch X86NativeR11 . (bytes 73 129 227)) (branch X86NativeR12 . (bytes 73 129 228)) (branch X86NativeR13 . (bytes 73 129 229)) (branch X86NativeR14 . (bytes 73 129 230)) (branch X86NativeR15 . (bytes 73 129 231)))) def x86NativeCompareImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 129 248)) (branch X86NativeRCX . (bytes 72 129 249)) (branch X86NativeRDX . (bytes 72 129 250)) (branch X86NativeRBX . (bytes 72 129 251)) (branch X86NativeRSP . (bytes 72 129 252)) (branch X86NativeRBP . (bytes 72 129 253)) (branch X86NativeRSI . (bytes 72 129 254)) (branch X86NativeRDI . (bytes 72 129 255)) (branch X86NativeR8 . (bytes 73 129 248)) (branch X86NativeR9 . (bytes 73 129 249)) (branch X86NativeR10 . (bytes 73 129 250)) (branch X86NativeR11 . (bytes 73 129 251)) (branch X86NativeR12 . (bytes 73 129 252)) (branch X86NativeR13 . (bytes 73 129 253)) (branch X86NativeR14 . (bytes 73 129 254)) (branch X86NativeR15 . (bytes 73 129 255)))) def x86NativeMultiplyImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (x86NativeRegisterInstructionBytes (byte 105) destination destination)) def x86NativeShiftLeftImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 193 224)) (branch X86NativeRCX . (bytes 72 193 225)) (branch X86NativeRDX . (bytes 72 193 226)) (branch X86NativeRBX . (bytes 72 193 227)) (branch X86NativeRSP . (bytes 72 193 228)) (branch X86NativeRBP . (bytes 72 193 229)) (branch X86NativeRSI . (bytes 72 193 230)) (branch X86NativeRDI . (bytes 72 193 231)) (branch X86NativeR8 . (bytes 73 193 224)) (branch X86NativeR9 . (bytes 73 193 225)) (branch X86NativeR10 . (bytes 73 193 226)) (branch X86NativeR11 . (bytes 73 193 227)) (branch X86NativeR12 . (bytes 73 193 228)) (branch X86NativeR13 . (bytes 73 193 229)) (branch X86NativeR14 . (bytes 73 193 230)) (branch X86NativeR15 . (bytes 73 193 231)))) def x86NativeShiftRightImmediate64Head : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) = (lambda unrestricted destination : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) destination (branch X86NativeRAX . (bytes 72 193 232)) (branch X86NativeRCX . (bytes 72 193 233)) (branch X86NativeRDX . (bytes 72 193 234)) (branch X86NativeRBX . (bytes 72 193 235)) (branch X86NativeRSP . (bytes 72 193 236)) (branch X86NativeRBP . (bytes 72 193 237)) (branch X86NativeRSI . (bytes 72 193 238)) (branch X86NativeRDI . (bytes 72 193 239)) (branch X86NativeR8 . (bytes 73 193 232)) (branch X86NativeR9 . (bytes 73 193 233)) (branch X86NativeR10 . (bytes 73 193 234)) (branch X86NativeR11 . (bytes 73 193 235)) (branch X86NativeR12 . (bytes 73 193 236)) (branch X86NativeR13 . (bytes 73 193 237)) (branch X86NativeR14 . (bytes 73 193 238)) (branch X86NativeR15 . (bytes 73 193 239)))) def x86NativeCallRegister64Bytes : (pi unrestricted target : (family X86NativeRegister64) . Bytes) = (lambda unrestricted target : (family X86NativeRegister64) . (eliminate X86NativeRegister64 (lambda unrestricted value : (family X86NativeRegister64) . Bytes) target (branch X86NativeRAX . (bytes 255 208)) (branch X86NativeRCX . (bytes 255 209)) (branch X86NativeRDX . (bytes 255 210)) (branch X86NativeRBX . (bytes 255 211)) (branch X86NativeRSP . (bytes 255 212)) (branch X86NativeRBP . (bytes 255 213)) (branch X86NativeRSI . (bytes 255 214)) (branch X86NativeRDI . (bytes 255 215)) (branch X86NativeR8 . (bytes 65 255 208)) (branch X86NativeR9 . (bytes 65 255 209)) (branch X86NativeR10 . (bytes 65 255 210)) (branch X86NativeR11 . (bytes 65 255 211)) (branch X86NativeR12 . (bytes 65 255 212)) (branch X86NativeR13 . (bytes 65 255 213)) (branch X86NativeR14 . (bytes 65 255 214)) (branch X86NativeR15 . (bytes 65 255 215)))) def x86NativeRegisterXMMLow3 : (pi unrestricted register : (family X86NativeRegisterXMM) . (family X86NativeRegisterLow3)) = (lambda unrestricted register : (family X86NativeRegisterXMM) . (eliminate X86NativeRegisterXMM (lambda unrestricted value : (family X86NativeRegisterXMM) . (family X86NativeRegisterLow3)) register (branch X86NativeXMM0 . (constructor X86NativeRegisterLow3 X86NativeLow0)) (branch X86NativeXMM1 . (constructor X86NativeRegisterLow3 X86NativeLow1)) (branch X86NativeXMM2 . (constructor X86NativeRegisterLow3 X86NativeLow2)) (branch X86NativeXMM3 . (constructor X86NativeRegisterLow3 X86NativeLow3)) (branch X86NativeXMM4 . (constructor X86NativeRegisterLow3 X86NativeLow4)) (branch X86NativeXMM5 . (constructor X86NativeRegisterLow3 X86NativeLow5)) (branch X86NativeXMM6 . (constructor X86NativeRegisterLow3 X86NativeLow6)) (branch X86NativeXMM7 . (constructor X86NativeRegisterLow3 X86NativeLow7)))) def x86NativeScalarDoubleOpcode : (pi unrestricted operation : (family X86NativeScalarDoubleOperation) . Byte) = (lambda unrestricted operation : (family X86NativeScalarDoubleOperation) . (eliminate X86NativeScalarDoubleOperation (lambda unrestricted value : (family X86NativeScalarDoubleOperation) . Byte) operation (branch X86NativeScalarDoubleAdd . (byte 88)) (branch X86NativeScalarDoubleSubtract . (byte 92)) (branch X86NativeScalarDoubleMultiply . (byte 89)) (branch X86NativeScalarDoubleDivide . (byte 94)) (branch X86NativeScalarDoubleSquareRoot . (byte 81)) (branch X86NativeScalarDoubleToSingle . (byte 90)))) -- 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 def x86NativeXMMGeneralBytes : (pi unrestricted prefix : Byte . (pi unrestricted wide : Nat . (pi unrestricted opcode : Byte . (pi unrestricted xmm : (family X86NativeRegisterXMM) . (pi unrestricted general : (family X86NativeRegister64) . Bytes))))) = (lambda unrestricted prefix : Byte . (lambda unrestricted wide : Nat . (lambda unrestricted opcode : Byte . (lambda unrestricted xmm : (family X86NativeRegisterXMM) . (lambda unrestricted general : (family X86NativeRegister64) . (bytes-append (bytes prefix) (bytes-append (eliminate X86NativeRegisterBank (lambda unrestricted bank : (family X86NativeRegisterBank) . Bytes) (x86NativeRegisterBank general) (branch X86NativeLowBank . (nat-eliminate (lambda unrestricted w : Nat . Bytes) b"" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"H")) wide)) (branch X86NativeHighBank . (nat-eliminate (lambda unrestricted w : Nat . Bytes) b"A" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"I")) wide))) (bytes-append (bytes 15 opcode) (x86NativeModRMRegister (x86NativeRegisterXMMLow3 xmm) (x86NativeRegisterLow3 general)))))))))) def x86EncodeNativeInstruction : (pi unrestricted instruction : (family X86NativeInstruction) . Bytes) = (lambda unrestricted instruction : (family X86NativeInstruction) . (eliminate X86NativeInstruction (lambda unrestricted value : (family X86NativeInstruction) . Bytes) instruction (branch X86NativeMoveImmediate32 destination immediate . (bytes-append (x86NativeMoveImmediate32Head destination) (x86NativeImmediate32Bytes immediate))) (branch X86NativeMoveImmediate64 destination immediate . (bytes-append (x86NativeMoveImmediate64Head destination) (x86NativeImmediate64Bytes immediate))) (branch X86NativeClear32 destination . (x86NativeClear32Bytes destination)) (branch X86NativeMoveRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 137) source destination)) (branch X86NativeAddRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 1) source destination)) (branch X86NativeSubtractRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 41) source destination)) (branch X86NativeAndRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 33) source destination)) (branch X86NativeOrRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 9) source destination)) (branch X86NativeXorRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 49) source destination)) (branch X86NativeCompareRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 57) source destination)) (branch X86NativeTestRegister64 source destination . (x86NativeRegisterInstructionBytes (byte 133) source destination)) (branch X86NativeAddImmediate64 destination immediate . (bytes-append (x86NativeAddImmediate64Head destination) (x86NativeImmediate32Bytes immediate))) (branch X86NativeAndImmediate64 destination immediate . (bytes-append (x86NativeAndImmediate64Head destination) (x86NativeImmediate32Bytes immediate))) (branch X86NativeCompareImmediate64 destination immediate . (bytes-append (x86NativeCompareImmediate64Head destination) (x86NativeImmediate32Bytes immediate))) (branch X86NativeMultiplyImmediate64 destination immediate . (bytes-append (x86NativeMultiplyImmediate64Head destination) (x86NativeImmediate32Bytes immediate))) (branch X86NativeMultiplyRegister64Unsigned source . (x86NativeRegisterInstructionBytes (byte 247) (constructor X86NativeRegister64 X86NativeRSP) source)) (branch X86NativeDivideRegister64Unsigned divisor . (x86NativeRegisterInstructionBytes (byte 247) (constructor X86NativeRegister64 X86NativeRSI) divisor)) (branch X86NativeShiftLeftImmediate64 destination immediate . (bytes-append (x86NativeShiftLeftImmediate64Head destination) (x86NativeImmediate8Bytes immediate))) (branch X86NativeShiftRightImmediate64 destination immediate . (bytes-append (x86NativeShiftRightImmediate64Head destination) (x86NativeImmediate8Bytes immediate))) (branch X86NativeLoadMemory64 destination base displacement . (x86NativeMemoryInstructionBytes (bytes 139) destination base displacement)) (branch X86NativeLoadMemory8ZeroExtend64 destination base displacement . (x86NativeMemoryInstructionBytes (bytes 15 182) destination base displacement)) (branch X86NativeLoadMemory32ZeroExtend64 destination base displacement . (x86NativeMemoryInstruction32Bytes (bytes 139) destination base displacement)) (branch X86NativeStoreMemory32 base displacement source . (x86NativeMemoryInstruction32Bytes (bytes 137) source base displacement)) (branch X86NativeStoreMemory64 base displacement source . (x86NativeMemoryInstructionBytes (bytes 137) source base displacement)) (branch X86NativeStoreMemory8 base displacement source . (x86NativeMemoryInstructionBytes (bytes 136) source base displacement)) (branch X86NativeStoreFence . (bytes 15 174 248)) (branch X86NativeLoadEffectiveAddressRIP destination displacement . (bytes-append (x86NativeLoadEffectiveAddressRIPHead destination) (x86NativeDisplacement32Bytes displacement))) (branch X86NativeJumpRelative32 displacement . (bytes-append (bytes 233) (x86NativeDisplacement32Bytes displacement))) (branch X86NativeJumpConditionRelative32 condition displacement . (bytes-append (bytes 15 (x86NativeConditionOpcode condition)) (x86NativeDisplacement32Bytes displacement))) (branch X86NativeCallRegister64 target . (x86NativeCallRegister64Bytes target)) (branch X86NativeReturn . (bytes 195)) (branch X86NativeSystemCall . (bytes 15 5)) (branch X86NativeMoveToXMM64 destination source . (x86NativeXMMGeneralBytes (byte 102) 1 (byte 110) destination source)) (branch X86NativeMoveFromXMM64 destination source . (x86NativeXMMGeneralBytes (byte 102) 1 (byte 126) source destination)) (branch X86NativeMoveFromXMM32 destination source . (x86NativeXMMGeneralBytes (byte 102) 0 (byte 126) source destination)) (branch X86NativeScalarDouble operation destination source . (bytes-append (bytes 242 15 (x86NativeScalarDoubleOpcode operation)) (x86NativeModRMRegister (x86NativeRegisterXMMLow3 destination) (x86NativeRegisterXMMLow3 source)))) (branch X86NativeScalarSingleToDouble destination source . (bytes-append (bytes 243 15 90) (x86NativeModRMRegister (x86NativeRegisterXMMLow3 destination) (x86NativeRegisterXMMLow3 source)))) (branch X86NativeScalarDoubleFromInteger64 destination source . (x86NativeXMMGeneralBytes (byte 242) 1 (byte 42) destination source)))) def x86EncodeNativeProgram : (pi unrestricted program : (family X86NativeProgram) . Bytes) = (lambda unrestricted program : (family X86NativeProgram) . (eliminate X86NativeProgram (lambda unrestricted value : (family X86NativeProgram) . Bytes) program (branch X86NativeProgramEnd . b"") (branch X86NativeProgramNext instruction tail encodedTail . (bytes-append (x86EncodeNativeInstruction instruction) encodedTail)))) -- Truncating low-word constructors; sign interpretation is the instruction's -- contract. This keeps signed offsets and unsigned constants out of handwritten -- per-routine byte decompositions. def x86NativeByteOfNatural = (lambda unrestricted value : Nat . (lambda unrestricted scale : Nat . (nat-to-byte (naturalModuloUnchecked (naturalDivideUnchecked value scale) 256)))) def x86NativeImmediate32FromNatural = (lambda unrestricted value : Nat . (constructor X86NativeImmediate32 X86NativeImmediate32Value (x86NativeByteOfNatural value 1) (x86NativeByteOfNatural value 256) (x86NativeByteOfNatural value 65536) (x86NativeByteOfNatural value 16777216))) def x86NativeDisplacement32FromNatural = (lambda unrestricted value : Nat . (constructor X86NativeDisplacement32 X86NativeDisplacement32Value (x86NativeByteOfNatural value 1) (x86NativeByteOfNatural value 256) (x86NativeByteOfNatural value 65536) (x86NativeByteOfNatural value 16777216)))