• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • 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
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
            • Get-prefixes
            • Vex-0f3a-execute
            • Vex-0f38-execute
            • Vex-0f-execute
            • Two-byte-opcode-execute
            • Second-three-byte-opcode-execute
            • One-byte-opcode-execute
            • First-three-byte-opcode-execute
            • Evex-0f3a-execute
            • Evex-0f38-execute
            • Evex-0f-execute
            • X86-fetch-decode-execute
            • Vex-decode-and-execute
            • Evex-decode-and-execute
            • X86-run
            • Implemented-opcodes
              • Two-byte-opcodes-map
              • One-byte-opcodes-map
              • 0f-38-three-byte-opcodes-map
              • 0f-3a-three-byte-opcodes-map
            • Three-byte-opcode-decode-and-execute
            • X86-run-halt-count
            • Two-byte-opcode-decode-and-execute
            • X86-run-steps
            • Opcode-maps
            • X86-run-halt
            • X86-fetch-decode-execute-halt
            • X86-run-steps1
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • 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
  • X86isa
  • Instructions
  • X86-decoder
  • Opcode-maps

Implemented-opcodes

Intel opcodes supported in x86isa.

We support decoding of all the x86 instructions in the one-, two-, and three-byte opcode maps, including the AVX/AVX2/AVX512 extensions. However, a fraction of those are actually implemented in this model --- when we say implemented instructions, we mean instructions that have a semantic function that models its effects on the machine's state.

For a listing of all such supported instructions, see one-byte-opcodes-map, two-byte-opcodes-map, 0f-38-three-byte-opcodes-map, and 0f-3a-three-byte-opcodes-map.

For a readable version of all the opcode maps, see constants like *pre-one-byte-opcode-map* in the book inst-listing.lisp. These are the constants to edit in order to add new instructions, etc. in the future. The dispatch, modr/m and prefixes computation, and generation of documentation is done automatically from these constants.

Subtopics

Two-byte-opcodes-map
List of implemented instructions whose opcode is two bytes long, beginning with 0F; includes VEX/EVEX instructions too
One-byte-opcodes-map
List of implemented instructions whose opcode is one byte long
0f-38-three-byte-opcodes-map
List of implemented instructions whose opcode is three bytes long, beginning with 0F_38; includes VEX/EVEX instructions too
0f-3a-three-byte-opcodes-map
List of implemented instructions whose opcode is three bytes long, beginning with 0F_3A; includes VEX/EVEX instructions too