• 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.22 Virtual-Machine Extensions

    • VMPTRST (0x0F_C7 /7) is missing from the opcode map
    • VMREAD and VMWRITE (0x0F_78 and 0x0F_79) are listed with mnemonics MREAD and MWRITE

    Unimplemented Instructions

    Opcode Mnemonic Other Information Semantic Function
    0F 01 VMCALL
    :REG 0
    :MOD 3
    :R/M 1
    0F 01 VMLAUNCH
    :REG 0
    :MOD 3
    :R/M 2
    0F 01 VMRESUME
    :REG 0
    :MOD 3
    :R/M 3
    0F 01 VMXOFF
    :REG 0
    :MOD 3
    :R/M 4
    0F 01 VMFUNC
    :REG 3
    :MOD 3
    :R/M 4
    0F 78 MREAD
    0F 79 MWRITE
    NP 0F C7 VMPTRLD
    :PFX :NO-PREFIX
    :REG 6
    :MOD :MEM
    66 0F C7 VMCLEAR
    :PFX :66
    :REG 6
    :MOD :MEM
    F3 0F C7 VMXON
    :PFX :F3
    :REG 6
    :MOD :MEM
    NP 0F C7 VMPTRLD
    :PFX :NO-PREFIX
    :REG 7
    :MOD :MEM
    66 0F 38 80 INVEPT
    :PFX :66
    66 0F 38 81 INVVPID
    :PFX :66