• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
          • 5.50 Uncategorized "Instructions"
            • 5.15 Fused-Multiply-Add (FMA)
            • 5.20 System Instructions
            • 5.19 Intel(R) Advanced Vector Extensions 512 (Intel(R) AVX-512)
            • 5.1 General-Purpose Instructions
            • 5.10 Intel(R) SSE4.1 Instructions
            • 5.13 Intel(R) Advanced Vector Extensions (Intel(R) AVX)
            • 5.7 Intel(R) SSE3 Instructions
            • 5.8 Supplemental Streaming Simd Extensions 3 (SSSE3) Instructions
            • 5.4 MMX Instructions
            • 5.22 Virtual-Machine Extensions
            • 5.6 Intel(R) SSE2 Instructions
            • 5.21 64-Bit Mode Instructions
            • 5.2 X87 FPU Instructions
            • 5.24 Intel(R) Memory Protection Extensions
            • 5.5 Intel(R) SSE Instructions
            • 5.16 Intel(R) Advanced Vector Extensions 2 (Intel(R) AVX2)
            • 5.12 Intel(R) AES-NI And PCLMULQDQ
            • 5.17 Intel(R) Transactional Synchronization Extensions (Intel(R) Tsx)
            • 5.14 16-Bit Floating-Point Conversion
            • 5.18 Intel(R) SHA Extensions
            • 5.11 Intel(R) SSE4.2 Instruction Set
            • 5.3 X87 FPU and SIMD State Management Instructions
            • 5.40 Other ISA Extensions
            • 5.25 Intel(R) Software Guard Extensions
            • 5.27 Control Transfer Terminating Instructions
            • 5.23 Safer Mode Extensions
            • 5.30 Enqueue Store Instructions
            • 5.29 User Interrupt Instructions
            • 5.28 Intel(R) AMX Instructions
            • 5.26 Shadow Stack Management Instructions
            • 5.31 Intel(R) Advanced Vector Extensions 10 Version 1 Instructions
          • Tlb
          • Running-linux
          • Introduction
          • Asmtest
          • X86isa-build-instructions
          • Publications
          • Contributors
          • Machine
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Sdm-instruction-set-summary

    5.50 Uncategorized "Instructions"

    Unimplemented Instructions

    Opcode Mnemonic Other Information Semantic Function
    NP 0F B8 JMPE
    :PFX :NO-PREFIX
    0F 18 RESERVEDNOP
    :MOD 3
    0F 18 RESERVEDNOP
    :REG 4
    0F 18 RESERVEDNOP
    :REG 5
    0F 18 RESERVEDNOP
    :REG 6
    0F 18 RESERVEDNOP
    :REG 7
    NP 0F 1A RESERVEDNOP
    :PFX :NO-PREFIX
    :MOD 3
    :FEAT :MPX
    F3 0F 1B RESERVEDNOP
    :PFX :F3
    :MOD 3
    :FEAT :MPX
    NP 0F 1B RESERVEDNOP
    :PFX :NO-PREFIX
    :MOD 3
    :FEAT :MPX
    0F 1C RESERVEDNOP
    0F 1D RESERVEDNOP
    FF far CALL
    :REG 3

    Implemented Instructions

    Opcode Mnemonic Other Information Semantic Function
    06 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "PUSH ES is illegal in the 64-bit mode!"))
    07 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "POP ES is illegal in the 64-bit mode!"))
    0E #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "PUSH CS is illegal in the 64-bit mode!"))
    16 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "PUSH SS is illegal in the 64-bit mode!"))
    17 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "POP SS is illegal in the 64-bit mode!"))
    1E #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "PUSH DS is illegal in the 64-bit mode!"))
    1F #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "POP DS is illegal in the 64-bit mode!"))
    27 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "DAA is illegal in the 64-bit mode!"))
    2F #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "DAS is illegal in the 64-bit mode!"))
    37 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "AAA is illegal in the 64-bit mode!"))
    3F #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "AAS is illegal in the 64-bit mode!"))
    60 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "PUSHA is illegal in the 64-bit mode!"))
    61 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "POPA is illegal in the 64-bit mode!"))
    82 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "Opcode 0x82 is illegal in the 64-bit mode!"))
    9A #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "far CALL is illegal in the 64-bit mode!"))
    CE #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "INTO is illegal in the 64-bit mode!"))
    D4 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "AAM is illegal in the 64-bit mode!"))
    D5 #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "AAD is illegal in the 64-bit mode!"))
    EA #UD
    :MODE :O64
    		x86-illegal-instruction --
    ((message . "JMP is illegal in the 64-bit mode!"))
    0F 19 RESERVEDNOP
    		x86-two-byte-nop
    FF far JMP
    :REG 5
    :MOD :MEM
    		x86-far-jmp-op/en-d
    FF near CALL
    :REG 2
    		x86-call-ff/2-op/en-m
    FF near JMP
    :REG 4
    		x86-near-jmp-op/en-m
    0F 2-BYTE-ESCAPE
    		two-byte-opcode-decode-and-execute --
    ((escape-byte . opcode))
    0F 38 3-BYTE-ESCAPE
    		three-byte-opcode-decode-and-execute --
    ((second-escape-byte . opcode))
    0F 3A 3-BYTE-ESCAPE
    		three-byte-opcode-decode-and-execute --
    ((second-escape-byte . opcode))
    62 EVEX-BYTE0
    :MODE :O64
    		NO INSTRUCTION
    67 PREFIX-ADDRSIZE
    		NO INSTRUCTION
    2E PREFIX-CS
    		NO INSTRUCTION
    3E PREFIX-DS
    		NO INSTRUCTION
    26 PREFIX-ES
    		NO INSTRUCTION
    64 PREFIX-FS
    		NO INSTRUCTION
    65 PREFIX-GS
    		NO INSTRUCTION
    F0 PREFIX-LOCK
    		NO INSTRUCTION
    66 PREFIX-OPSIZE
    		NO INSTRUCTION
    F3 PREFIX-REP/REPE
    		NO INSTRUCTION
    F2 PREFIX-REPNE
    		NO INSTRUCTION
    36 PREFIX-SS
    		NO INSTRUCTION
    40 REX
    :MODE :O64
    		NO INSTRUCTION
    41 REX-B
    :MODE :O64
    		NO INSTRUCTION
    44 REX-R
    :MODE :O64
    		NO INSTRUCTION
    45 REX-RB
    :MODE :O64
    		NO INSTRUCTION
    46 REX-RX
    :MODE :O64
    		NO INSTRUCTION
    47 REX-RXB
    :MODE :O64
    		NO INSTRUCTION
    48 REX-W
    :MODE :O64
    		NO INSTRUCTION
    49 REX-WB
    :MODE :O64
    		NO INSTRUCTION
    4C REX-WR
    :MODE :O64
    		NO INSTRUCTION
    4D REX-WRB
    :MODE :O64
    		NO INSTRUCTION
    4E REX-WRX
    :MODE :O64
    		NO INSTRUCTION
    4F REX-WRXB
    :MODE :O64
    		NO INSTRUCTION
    4A REX-WX
    :MODE :O64
    		NO INSTRUCTION
    4B REX-WXB
    :MODE :O64
    		NO INSTRUCTION
    42 REX-X
    :MODE :O64
    		NO INSTRUCTION
    43 REX-XB
    :MODE :O64
    		NO INSTRUCTION
    C5 VEX2-BYTE0
    :MODE :O64
    		NO INSTRUCTION
    C4 VEX3-BYTE0
    :MODE :O64
    		NO INSTRUCTION