• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
        • Two-byte-opcodes-map
        • One-byte-opcodes-map
        • 0f-38-three-byte-opcodes-map
        • 0f-3a-three-byte-opcodes-map
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Implemented-opcodes

Two-byte-opcodes-map

List of implemented instructions whose opcode is two bytes long, beginning with 0F; includes VEX/EVEX instructions too

Opcode	Mnemonic	Other Information	Semantic Function
00	LLDT	:REG 2	x86-lldt
00	LTR	:REG 3	x86-ltr
01	SGDT	:REG 0 :MOD :MEM	x86-sgdt
01	LGDT	:REG 2 :MOD :MEM	x86-lgdt
01	LIDT	:REG 3 :MOD :MEM	x86-lidt
01	INVLPG	:REG 7 :MOD :MEM	x86-invlpg
01	SWAPGS	:MODE :O64 :REG 7 :MOD 3 :R/M 0	x86-swapgs
05	SYSCALL	:MODE :O64	x86-syscall-both-views
07	SYSRET	:MODE :O64	x86-sysret
0B	UD2		x86-illegal-instruction -- ((message . "UD2 encountered!"))
10	MOVUPS	:PFX :NO-PREFIX :FEAT :SSE	x86-movups/movupd/movdqu-op/en-rm
10	MOVUPD	:PFX :66 :FEAT :SSE2	x86-movups/movupd/movdqu-op/en-rm
10	MOVSS	:PFX :F3 :FEAT :SSE	x86-movss/movsd-op/en-rm -- ((sp/dp . #x0))
10	MOVSD	:PFX :F2 :FEAT :SSE2	x86-movss/movsd-op/en-rm -- ((sp/dp . #x1))
10	VMOVUPS	:VEX :0F :128 :WIG :FEAT :AVX	x86-vmovups-vex-a
10	VMOVUPS	:VEX :0F :256 :WIG :FEAT :AVX	x86-vmovups-vex-a
11	MOVUPS	:PFX :NO-PREFIX :FEAT :SSE	x86-movups/movupd/movdqu-op/en-mr
11	MOVUPD	:PFX :66 :FEAT :SSE2	x86-movups/movupd/movdqu-op/en-mr
11	MOVSS	:PFX :F3 :FEAT :SSE	x86-movss/movsd-op/en-mr -- ((sp/dp . #x0))
11	MOVSD	:PFX :F2 :FEAT :SSE2	x86-movss/movsd-op/en-mr -- ((sp/dp . #x1))
11	VMOVUPS	:VEX :0F :128 :WIG :FEAT :AVX	x86-vmovups-vex-b
11	VMOVUPS	:VEX :0F :256 :WIG :FEAT :AVX	x86-vmovups-vex-b
12	MOVLPS	:PFX :NO-PREFIX :MOD :MEM :FEAT :SSE	x86-movlps/movlpd-op/en-rm
12	MOVHLPS	:PFX :NO-PREFIX :MOD 3 :FEAT :SSE	x86-movhlps-sse
12	MOVLPD	:PFX :66 :FEAT :SSE2	x86-movlps/movlpd-op/en-rm
13	MOVLPS	:PFX :NO-PREFIX :FEAT :SSE	x86-movlps/movlpd-op/en-mr
13	MOVLPD	:PFX :66 :FEAT :SSE2	x86-movlps/movlpd-op/en-mr
14	UNPCKLPS	:PFX :NO-PREFIX :FEAT :SSE	x86-unpck?ps-op/en-rm -- ((high/low . #x0))
14	UNPCKLPD	:PFX :66 :FEAT :SSE2	x86-unpck?pd-op/en-rm -- ((high/low . #x0))
15	UNPCKHPS	:PFX :NO-PREFIX :FEAT :SSE	x86-unpck?ps-op/en-rm -- ((high/low . #x1))
15	UNPCKHPD	:PFX :66 :FEAT :SSE2	x86-unpck?pd-op/en-rm -- ((high/low . #x1))
16	MOVHPS	:PFX :NO-PREFIX :MOD :MEM :FEAT :SSE	x86-movhps/movhpd-op/en-rm
16	MOVHPD	:PFX :66 :FEAT :SSE2	x86-movhps/movhpd-op/en-rm
17	MOVHPS	:PFX :NO-PREFIX :FEAT :SSE	x86-movhps/movhpd-op/en-mr
17	MOVHPD	:PFX :66 :FEAT :SSE2	x86-movhps/movhpd-op/en-mr
18	PREFETCHNTA	:REG 0 :MOD :MEM	x86-two-byte-nop
18	PREFETCHT0	:REG 1 :MOD :MEM	x86-two-byte-nop
18	PREFETCHT1	:REG 2 :MOD :MEM	x86-two-byte-nop
18	PREFETCHT2	:REG 3 :MOD :MEM	x86-two-byte-nop
19	RESERVEDNOP		x86-two-byte-nop
1E	ENDBR32/ENDBR64		x86-endbr32/endbr64
1F	NOP		x86-two-byte-nop
20	MOV		x86-mov-control-regs-op/en-mr
21	MOV		x86-two-byte-nop
22	MOV		x86-mov-control-regs-op/en-rm
23	MOV		x86-two-byte-nop
28	MOVAPS	:PFX :NO-PREFIX :FEAT :SSE	x86-movaps/movapd-op/en-rm
28	MOVAPD	:PFX :66 :FEAT :SSE2	x86-movaps/movapd-op/en-rm
29	MOVAPS	:PFX :NO-PREFIX :FEAT :SSE	x86-movaps/movapd-op/en-mr
29	MOVAPD	:PFX :66 :FEAT :SSE2	x86-movaps/movapd-op/en-mr
2A	CVTSI2SS	:PFX :F3 :FEAT :SSE	x86-cvtsi2s?-op/en-rm -- ((sp/dp . #x0))
2A	CVTSI2SD	:PFX :F2 :FEAT :SSE2	x86-cvtsi2s?-op/en-rm -- ((sp/dp . #x1))
2C	CVTTSS2SI	:PFX :F3 :FEAT :SSE	x86-cvts?2si/cvtts?2si-op/en-rm -- ((sp/dp . #x0) (trunc . t))
2C	CVTTSD2SI	:PFX :F2 :FEAT :SSE2	x86-cvts?2si/cvtts?2si-op/en-rm -- ((sp/dp . #x1) (trunc . t))
2D	CVTSS2SI	:PFX :F3 :FEAT :SSE	x86-cvts?2si/cvtts?2si-op/en-rm -- ((sp/dp . #x0) (trunc))
2D	CVTSD2SI	:PFX :F2 :FEAT :SSE2	x86-cvts?2si/cvtts?2si-op/en-rm -- ((sp/dp . #x1) (trunc))
2E	UCOMISS	:PFX :NO-PREFIX :FEAT :SSE	x86-comis?/ucomis?-op/en-rm -- ((operation . #x9) (sp/dp . #x0))
2E	UCOMISD	:PFX :66 :FEAT :SSE2	x86-comis?/ucomis?-op/en-rm -- ((operation . #x9) (sp/dp . #x1))
2F	COMISS	:PFX :NO-PREFIX :FEAT :SSE	x86-comis?/ucomis?-op/en-rm -- ((operation . #x9) (sp/dp . #x0))
2F	COMISD	:PFX :66 :FEAT :SSE2	x86-comis?/ucomis?-op/en-rm -- ((operation . #x9) (sp/dp . #x1))
30	WRMSR		x86-wrmsr
31	RDTSC		x86-rdtsc
32	RDMSR		x86-rdmsr
38	3-BYTE-ESCAPE		three-byte-opcode-decode-and-execute -- ((second-escape-byte . opcode))
3A	3-BYTE-ESCAPE		three-byte-opcode-decode-and-execute -- ((second-escape-byte . opcode))
40	CMOVO		x86-cmovcc
41	CMOVNO		x86-cmovcc
42	CMOVB/C/NAE		x86-cmovcc
43	CMOVAE/NB/NC		x86-cmovcc
44	CMOVE/Z		x86-cmovcc
45	CMOVNE/NZ		x86-cmovcc
46	CMOVBE/NA		x86-cmovcc
47	CMOVA/NBE		x86-cmovcc
48	CMOVS		x86-cmovcc
49	CMOVNS		x86-cmovcc
4A	CMOVP/PE		x86-cmovcc
4B	CMOVNP/PO		x86-cmovcc
4C	CMOVL/NGE		x86-cmovcc
4D	CMOVNL/GE		x86-cmovcc
4E	CMOVLE/NG		x86-cmovcc
4F	CMOVNLE/G		x86-cmovcc
51	SQRTPS	:PFX :NO-PREFIX :FEAT :SSE	x86-sqrtps-op/en-rm
51	SQRTPD	:PFX :66 :FEAT :SSE2	x86-sqrtpd-op/en-rm
51	SQRTSS	:PFX :F3 :FEAT :SSE	x86-sqrts?-op/en-rm -- ((sp/dp . #x0))
51	SQRTSD	:PFX :F2 :FEAT :SSE2	x86-sqrts?-op/en-rm -- ((sp/dp . #x1))
54	ANDPS	:PFX :NO-PREFIX :FEAT :SSE	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x3))
54	ANDPD	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x3))
54	VANDPD	:VEX :0F :NDS :128 :66 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x3))
54	VANDPD	:VEX :0F :NDS :256 :66 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x3))
54	VANDPS	:VEX :0F :NDS :128 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x3))
54	VANDPS	:VEX :0F :NDS :256 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
55	ANDNPS	:PFX :NO-PREFIX :FEAT :SSE	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #xD))
55	ANDNPD	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #xD))
55	VANDNPD	:VEX :0F :NDS :128 :66 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #xD))
55	VANDNPD	:VEX :0F :NDS :256 :66 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #xD))
55	VANDNPS	:VEX :0F :NDS :128 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #xD))
55	VANDNPS	:VEX :0F :NDS :256 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #xD))
56	ORPS	:PFX :NO-PREFIX :FEAT :SSE	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x1))
56	ORPD	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x1))
56	VORPD	:VEX :0F :NDS :128 :66 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x1))
56	VORPD	:VEX :0F :NDS :256 :66 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x1))
56	VORPS	:VEX :0F :NDS :128 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x1))
56	VORPS	:VEX :0F :NDS :256 :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x1))
57	XORPS	:PFX :NO-PREFIX :FEAT :SSE	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x5))
57	XORPD	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x5))
57	VXORPD	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
57	VXORPD	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
57	VXORPS	:VEX :0F :NDS :128 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
57	VXORPS	:VEX :0F :NDS :256 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
58	ADDPS	:PFX :NO-PREFIX :FEAT :SSE	x86-addps/subps/mulps/divps/maxps/minps-op/en-rm -- ((operation . #x0))
58	ADDPD	:PFX :66 :FEAT :SSE2	x86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm -- ((operation . #x0))
58	ADDSS	:PFX :F3 :FEAT :SSE	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x0) (sp/dp . #x0))
58	ADDSD	:PFX :F2 :FEAT :SSE2	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x0) (sp/dp . #x1))
59	MULPS	:PFX :NO-PREFIX :FEAT :SSE	x86-addps/subps/mulps/divps/maxps/minps-op/en-rm -- ((operation . #x1A))
59	MULPD	:PFX :66 :FEAT :SSE2	x86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm -- ((operation . #x1A))
59	MULSS	:PFX :F3 :FEAT :SSE	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x1A) (sp/dp . #x0))
59	MULSD	:PFX :F2 :FEAT :SSE2	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x1A) (sp/dp . #x1))
5A	CVTPS2PD	:PFX :NO-PREFIX :FEAT :SSE2	x86-cvtps2pd-op/en-rm
5A	CVTPD2PS	:PFX :66 :FEAT :SSE2	x86-cvtpd2ps-op/en-rm
5A	CVTSS2SD	:PFX :F3 :FEAT :SSE2	x86-cvts?2s?-op/en-rm -- ((dp-to-sp . #x0))
5A	CVTSD2SS	:PFX :F2 :FEAT :SSE2	x86-cvts?2s?-op/en-rm -- ((dp-to-sp . #x1))
5C	SUBPS	:PFX :NO-PREFIX :FEAT :SSE	x86-addps/subps/mulps/divps/maxps/minps-op/en-rm -- ((operation . #x4))
5C	SUBPD	:PFX :66 :FEAT :SSE2	x86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm -- ((operation . #x4))
5C	SUBSS	:PFX :F3 :FEAT :SSE	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x4) (sp/dp . #x0))
5C	SUBSD	:PFX :F2 :FEAT :SSE2	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x4) (sp/dp . #x1))
5D	MINPS	:PFX :NO-PREFIX :FEAT :SSE	x86-addps/subps/mulps/divps/maxps/minps-op/en-rm -- ((operation . #x24))
5D	MINPD	:PFX :66 :FEAT :SSE2	x86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm -- ((operation . #x24))
5D	MINSS	:PFX :F3 :FEAT :SSE	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x24) (sp/dp . #x0))
5D	MINSD	:PFX :F2 :FEAT :SSE2	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x24) (sp/dp . #x1))
5E	DIVPS	:PFX :NO-PREFIX :FEAT :SSE	x86-addps/subps/mulps/divps/maxps/minps-op/en-rm -- ((operation . #x1C))
5E	DIVPD	:PFX :66 :FEAT :SSE2	x86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm -- ((operation . #x1C))
5E	DIVSS	:PFX :F3 :FEAT :SSE	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x1C) (sp/dp . #x0))
5E	DIVSD	:PFX :F2 :FEAT :SSE2	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x1C) (sp/dp . #x1))
5F	MAXPS	:PFX :NO-PREFIX :FEAT :SSE	x86-addps/subps/mulps/divps/maxps/minps-op/en-rm -- ((operation . #x22))
5F	MAXPD	:PFX :66 :FEAT :SSE2	x86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm -- ((operation . #x22))
5F	MAXSS	:PFX :F3 :FEAT :SSE	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x22) (sp/dp . #x0))
5F	MAXSD	:PFX :F2 :FEAT :SSE2	x86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm -- ((operation . #x22) (sp/dp . #x1))
60	PUNPCKLBW	:PFX :66 :FEAT :SSE2	x86-punpckl-sse
61	PUNPCKLWD	:PFX :66 :FEAT :SSE2	x86-punpckl-sse
62	PUNPCKLDQ	:PFX :66 :FEAT :SSE2	x86-punpckl-sse
64	PCMPGTB	:PFX :66 :FEAT :SSE2	x86-pcmpgt-sse
65	PCMPGTW	:PFX :66 :FEAT :SSE2	x86-pcmpgt-sse
66	PCMPGTD	:PFX :66 :FEAT :SSE2	x86-pcmpgt-sse
67	PACKUSWB	:PFX :66 :FEAT :SSE2	x86-packuswb-sse
68	PUNPCKHBW	:PFX :66 :FEAT :SSE2	x86-punpckh-sse
69	PUNPCKHWD	:PFX :66 :FEAT :SSE2	x86-punpckh-sse
6A	PUNPCKHDQ	:PFX :66 :FEAT :SSE2	x86-punpckh-sse
6C	PUNPCKLQDQ	:PFX :66 :FEAT :SSE2	x86-punpckl-sse
6D	PUNPCKHQDQ	:PFX :66 :FEAT :SSE2	x86-punpckh-sse
6E	MOVD/Q	:PFX :66 :FEAT :SSE2	x86-movd/movq-to-xmm
6F	MOVDQA	:PFX :66 :FEAT :SSE2	x86-movdqa-to-xmm
6F	MOVDQU	:PFX :F3 :FEAT :SSE2	x86-movups/movupd/movdqu-op/en-rm
70	PSHUFD	:PFX :66 :FEAT :SSE2	x86-pshufd
70	PSHUFHW	:PFX :F3 :FEAT :SSE2	x86-pshufhw
70	PSHUFLW	:PFX :F2 :FEAT :SSE2	x86-pshuflw
71	PSRLW	:PFX :66 :REG 2 :MOD 3 :FEAT :SSE2	x86-psrl-imm-sse
71	PSRAW	:PFX :66 :REG 4 :MOD 3 :FEAT :SSE2	x86-psra-imm-sse
71	PSLLW	:PFX :66 :REG 6 :MOD 3 :FEAT :SSE2	x86-psll-imm-sse
72	PSRLD	:PFX :66 :REG 2 :MOD 3 :FEAT :SSE2	x86-psrl-imm-sse
72	PSRAD	:PFX :66 :REG 4 :MOD 3 :FEAT :SSE2	x86-psra-imm-sse
72	PSLLD	:PFX :66 :REG 6 :MOD 3 :FEAT :SSE2	x86-psll-imm-sse
73	PSRLQ	:PFX :66 :REG 2 :MOD 3 :FEAT :SSE2	x86-psrl-imm-sse
73	PSRLDQ	:PFX :66 :REG 3 :MOD 3 :FEAT :SSE2	x86-pslldq/psrldq
73	PSLLQ	:PFX :66 :REG 6 :MOD 3 :FEAT :SSE2	x86-psll-imm-sse
73	PSLLDQ	:PFX :66 :REG 7 :MOD 3 :FEAT :SSE2	x86-pslldq/psrldq
74	PCMPEQB	:PFX :66 :FEAT :SSE2	x86-pcmpeq-sse
75	PCMPEQW	:PFX :66 :FEAT :SSE2	x86-pcmpeq-sse
76	PCMPEQD	:PFX :66 :FEAT :SSE2	x86-pcmpeq-sse
77	VZEROUPPER	:VEX :0F :128 :WIG :FEAT :AVX	x86-vzeroupper
7E	MOVD/Q	:PFX :66 :FEAT :SSE2	x86-movd/movq-from-xmm
7E	MOVQ	:PFX :F3 :FEAT :SSE2	x86-movq-from-xmm/mem
7F	MOVDQA	:PFX :66 :FEAT :SSE2	x86-movdqa-from-xmm
7F	MOVDQU	:PFX :F3 :FEAT :SSE2	x86-movups/movupd/movdqu-op/en-mr
80	JO		x86-two-byte-jcc
81	JNO		x86-two-byte-jcc
82	JB/NAE/C		x86-two-byte-jcc
83	JNB/AE/NC		x86-two-byte-jcc
84	JZ/E		x86-two-byte-jcc
85	JNZ/NE		x86-two-byte-jcc
86	JBE/NA		x86-two-byte-jcc
87	JNBE/A		x86-two-byte-jcc
88	JS		x86-two-byte-jcc
89	JNS		x86-two-byte-jcc
8A	JP/PE		x86-two-byte-jcc
8B	JNP/PO		x86-two-byte-jcc
8C	JL/NGE		x86-two-byte-jcc
8D	JNL/GE		x86-two-byte-jcc
8E	JLE/NG		x86-two-byte-jcc
8F	JNLE/G		x86-two-byte-jcc
90	SETO		x86-setcc
91	SETNO		x86-setcc
92	SETB/NAE/C		x86-setcc
93	SETNB/AE/NC		x86-setcc
94	SETZ/E		x86-setcc
95	SETNZ/NE		x86-setcc
96	SETBE/NA		x86-setcc
97	SETNBE/A		x86-setcc
98	SETS		x86-setcc
99	SETNS		x86-setcc
9A	SETP/PE		x86-setcc
9B	SETNP/PO		x86-setcc
9C	SETL/NGE		x86-setcc
9D	SETNL/GE		x86-setcc
9E	SETLE/NG		x86-setcc
9F	SETNLE/G		x86-setcc
A0	PUSH FS		x86-push-segment-register
A2	CPUID		x86-cpuid
A3	BT		x86-bt-0f-a3
A4	SHLD		x86-shld/shrd
A5	SHLD		x86-shld/shrd
A8	PUSH GS		x86-push-segment-register
AB	BTS		x86-bt-0f-ab
AC	SHRD		x86-shld/shrd
AD	SHRD		x86-shld/shrd
AE	FXSAVE	:PFX :NO-PREFIX :REG 0 :MOD :MEM :FEAT :FXSR	x86-fxsave/fxsave64
AE	FXRSTOR	:PFX :NO-PREFIX :REG 1 :MOD :MEM :FEAT :FXSR	x86-fxrstor/fxrstor64
AE	LDMXCSR	:PFX :NO-PREFIX :REG 2 :MOD :MEM :FEAT :SSE	x86-ldmxcsr/stmxcsr-op/en-m
AE	STMXCSR	:PFX :NO-PREFIX :REG 3 :MOD :MEM :FEAT :SSE	x86-ldmxcsr/stmxcsr-op/en-m
AE	LFENCE	:PFX :NO-PREFIX :REG 5 :MOD 3 :FEAT :SSE2	x86-two-byte-nop
AF	IMUL		x86-imul-op/en-rm
B0	CMPXCHG		x86-cmpxchg
B1	CMPXCHG		x86-cmpxchg
B3	BTR		x86-btr-0f-b3
B6	MOVZX		x86-movzx
B7	MOVZX		x86-movzx
B8	POPCNT	:PFX :F3 :FEAT :POPCNT	x86-popcnt
B9	UD1		x86-illegal-instruction -- ((message . "UD1 encountered!"))
BA	BT	:REG 4	x86-bt-0f-ba
BA	BTS	:REG 5	x86-bt-0f-ba
BA	BTR	:REG 6	x86-bt-0f-ba
BA	BTC	:REG 7	x86-bt-0f-ba
BC	BSF	:PFX :NO-PREFIX	x86-bsf-op/en-rm
BC	TZCNT	:PFX :F3	x86-tzcnt
BD	BSR	:PFX :NO-PREFIX	x86-bsr
BE	MOVSX		x86-movsx
BF	MOVSX		x86-movsx
C0	XADD		x86-add/xadd/adc/sub/sbb/or/and/xor/cmp/test-e-g -- ((operation . #x26))
C1	XADD		x86-add/xadd/adc/sub/sbb/or/and/xor/cmp/test-e-g -- ((operation . #x26))
C2	CMPPS	:PFX :NO-PREFIX :FEAT :SSE	x86-cmpps-op/en-rmi
C2	CMPPD	:PFX :66 :FEAT :SSE2	x86-cmppd-op/en-rmi
C2	CMPSS	:PFX :F3 :FEAT :SSE	x86-cmpss/cmpsd-op/en-rmi -- ((sp/dp . #x0))
C2	CMPSD	:PFX :F2 :FEAT :SSE2	x86-cmpss/cmpsd-op/en-rmi -- ((sp/dp . #x1))
C6	SHUFPS	:PFX :NO-PREFIX :FEAT :SSE	x86-shufps-op/en-rmi
C6	SHUFPD	:PFX :66 :FEAT :SSE2	x86-shufpd-op/en-rmi
C7	CMPXCHG16B	:PFX :NO-PREFIX :REG 1 :MOD :MEM :REX :W :FEAT :CMPXCHG16B	x86-cmpxchg8b/16b
C7	CMPXCHG8B	:PFX :NO-PREFIX :REG 1 :MOD :MEM :REX :NOT-W :FEAT :CMPXCHG16B	x86-cmpxchg8b/16b
C7	RDRAND	:PFX :NO-PREFIX :REG 6 :MOD 3 :FEAT :RDRAND	x86-rdrand
C7	RDRAND	:PFX :66 :REG 6 :MOD 3 :FEAT :RDRAND	x86-rdrand
C8	BSWAP		x86-bswap
C9	BSWAP		x86-bswap
CA	BSWAP		x86-bswap
CB	BSWAP		x86-bswap
CC	BSWAP		x86-bswap
CD	BSWAP		x86-bswap
CE	BSWAP		x86-bswap
CF	BSWAP		x86-bswap
D1	PSRLW	:PFX :66 :FEAT :SSE2	x86-psrl-xmm-sse
D2	PSRLD	:PFX :66 :FEAT :SSE2	x86-psrl-xmm-sse
D3	PSRLQ	:PFX :66 :FEAT :SSE2	x86-psrl-xmm-sse
D4	PADDQ	:PFX :66 :FEAT :SSE2	x86-paddb/paddw/paddd/paddq-sse
D4	VPADDQ	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
D4	VPADDQ	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
D6	MOVQ	:PFX :66 :FEAT :SSE2	x86-movq-to-xmm/mem
D7	PMOVMSKB	:PFX :66 :FEAT :SSE2	x86-pmovmskb-op/en-rm
DB	PAND	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x3))
DB	VPAND	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x3))
DB	VPAND	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x3))
DF	PANDN	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #xD))
DF	VPANDN	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #xD))
DF	VPANDN	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #xD))
E1	PSRAW	:PFX :66 :FEAT :SSE2	x86-psra-xmm-sse
E2	PSRAD	:PFX :66 :FEAT :SSE2	x86-psra-xmm-sse
EB	POR	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x1))
EB	VPOR	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
EB	VPOR	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
EF	PXOR	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x5))
EF	VPXOR	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
EF	VPXOR	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex -- ((operation . #x5))
F1	PSLLW	:PFX :66 :FEAT :SSE2	x86-psll-xmm-sse
F2	PSLLD	:PFX :66 :FEAT :SSE2	x86-psll-xmm-sse
F3	PSLLQ	:PFX :66 :FEAT :SSE2	x86-psll-xmm-sse
F8	PSUBB	:PFX :66 :FEAT :SSE2	x86-psubb/psubw/psubd/psubq-sse
F8	VPSUBB	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
F8	VPSUBB	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
F9	PSUBW	:PFX :66 :FEAT :SSE2	x86-psubb/psubw/psubd/psubq-sse
F9	VPSUBW	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
F9	VPSUBW	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
FA	PSUBD	:PFX :66 :FEAT :SSE2	x86-psubb/psubw/psubd/psubq-sse
FA	VPSUBD	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
FA	VPSUBD	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
FB	PSUBQ	:PFX :66 :FEAT :SSE2	x86-psubb/psubw/psubd/psubq-sse
FB	VPSUBQ	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
FB	VPSUBQ	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpsubb/vpsubw/vpsubd/vpsubq-vex
FC	PADDB	:PFX :66 :FEAT :SSE2	x86-paddb/paddw/paddd/paddq-sse
FC	VPADDB	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
FC	VPADDB	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
FD	PADDW	:PFX :66 :FEAT :SSE2	x86-paddb/paddw/paddd/paddq-sse
FD	VPADDW	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
FD	VPADDW	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
FE	PADDD	:PFX :66 :FEAT :SSE2	x86-paddb/paddw/paddd/paddq-sse
FE	VPADDD	:VEX :0F :NDS :128 :66 :WIG :FEAT :AVX	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex
FE	VPADDD	:VEX :0F :NDS :256 :66 :WIG :FEAT :AVX2	x86-vpaddb/vpaddw/vpaddd/vpaddq-vex