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

• 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
01	LGDT	:REG 2 :MOD :MEM	x86-lgdt
01	LIDT	:REG 3 :MOD :MEM	x86-lidt
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))
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))
12	MOVLPS	:PFX :NO-PREFIX :MOD :MEM	x86-movlps/movlpd-op/en-rm
12	MOVLPD	:PFX :66 :FEAT :SSE2	x86-movlps/movlpd-op/en-rm
12	MOVSLDUP	:PFX :F3 :FEAT :SSE3	x86-movlps/movlpd-op/en-rm
12	MOVDDUP	:PFX :F2 :FEAT :SSE3	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	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
1F	NOP		x86-two-byte-nop
20	MOV		x86-mov-control-regs-op/en-mr
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))
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))
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))
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))
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))
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))
6E	MOVD/Q	:PFX :66 :FEAT :SSE2	x86-movd/movq-to-xmm
6F	MOVDQU	:PFX :F3 :FEAT :SSE2	x86-movups/movupd/movdqu-op/en-rm
74	PCMPEQB	:PFX :66 :FEAT :SSE2	x86-pcmpeqb-op/en-rm
7E	MOVD/Q	:PFX :66 :FEAT :SSE2	x86-movd/movq-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
A3	BT		x86-bt-0f-a3
A4	SHLD		x86-shld/shrd
A5	SHLD		x86-shld/shrd
A8	PUSH GS		x86-push-segment-register
AC	SHRD		x86-shld/shrd
AD	SHRD		x86-shld/shrd
AE	LDMXCSR	:PFX :NO-PREFIX :REG 2 :MOD :MEM	x86-ldmxcsr/stmxcsr-op/en-m
AE	STMXCSR	:PFX :NO-PREFIX :REG 3 :MOD :MEM	x86-ldmxcsr/stmxcsr-op/en-m
AF	IMUL		x86-imul-op/en-rm
B0	CMPXCHG		x86-cmpxchg
B1	CMPXCHG		x86-cmpxchg
B6	MOVZX		x86-movzx
B7	MOVZX		x86-movzx
B9	UD1		x86-illegal-instruction -- ((message . "UD1 encountered!"))
BA	BT	:REG 4	x86-bt-0f-ba
BC	BSF	:PFX :NO-PREFIX	x86-bsf-op/en-rm
BE	MOVSX		x86-movsxd
BF	MOVSX		x86-movsxd
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	RDRAND	:PFX :NO-PREFIX :REG 6 :MOD 3 :FEAT :RDRAND	x86-rdrand
C7	RDRAND	:PFX :66 :REG 6 :MOD 3 :FEAT :RDRAND	x86-rdrand
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))
DF	PANDN	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #xD))
EB	POR	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x1))
EF	PXOR	:PFX :66 :FEAT :SSE2	x86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm -- ((operation . #x5))