• 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
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
          • Structures
            • Rflagsbits
            • Cr4bits
            • Xcr0bits
            • Cr0bits
            • Prefixes
            • Ia32_eferbits
            • Evex-byte1
            • Cr3bits
            • Evex-byte3
            • Vex3-byte2
            • Vex3-byte1
            • Vex2-byte1
            • Evex-prefixes
            • Evex-byte2
            • Vex-prefixes
            • Sib
            • Modr/m-structures
            • Vex-prefixes-layout-structures
            • Sib-structures
            • Legacy-prefixes-layout-structure
            • Evex-prefixes-layout-structures
            • Cr8bits
            • Opcode-maps-structures
              • Opcode
                • Opcode-fix
                • Make-opcode
                • Opcode-p
                • Opcode-equiv
                • Change-opcode
                • Opcode->superscripts
                • Opcode->group
                • Opcode->vex
                • Opcode->r/m
                • Opcode->reg
                • Opcode->pfx
                • Opcode->mode
                • Opcode->feat
                • Opcode->evex
                • Opcode->rex
                • Opcode->op
                • Opcode->mod
              • Inst
              • Op/en-p
              • Operands
              • Inst-list-p
              • Operand-type-p
              • Strict-opcode-p
              • Opcode-extension-group-p
              • Superscripts-p
              • Maybe-operands-p
              • Exception-desc-p
              • Count-avx-pfx-cases
              • Mnemonic-p
              • Maybe-3bits-p
              • Op-pfx-p
              • Maybe-vex-p
              • Maybe-evex-p
              • Fn-desc-p
              • Op-mode-p
              • Rex-p
              • Mod-p
              • Avx-pfx-well-formed-p
              • Any-present-in
              • Superscripts-fix
              • Strict-opcode-fix
              • Operand-type-fix
              • Opcode-extension-group-fix
              • Maybe-operands-fix
              • Maybe-evex-fix
              • Maybe-3bits-fix
              • Keyword-list-fix
              • Exception-desc-fix
              • Rex-fix
              • Op-pfx-fix
              • Op-mode-fix
              • Mod-fix
              • Mnemonic-fix
              • Maybe-vex-fix
              • Fn-desc-fix
              • Vex-p
              • Evex-p
            • Segmentation-bitstructs
            • 8bits
            • 2bits
            • 4bits
            • 16bits
            • Paging-bitstructs
            • 3bits
            • 11bits
            • 40bits
            • 5bits
            • 32bits
            • 19bits
            • 10bits
            • 7bits
            • 64bits
            • 54bits
            • 45bits
            • 36bits
            • 31bits
            • 24bits
            • 22bits
            • 17bits
            • 13bits
            • 12bits
            • 6bits
            • Vex->x
            • Vex->b
            • Vex-prefixes-map-p
            • Vex-prefixes-byte0-p
            • Vex->w
            • Vex->vvvv
            • Vex->r
            • Fp-bitstructs
            • Cr4bits-debug
            • Vex->pp
            • Vex->l
            • Rflagsbits-debug
            • Evex->v-prime
            • Evex->z
            • Evex->w
            • Evex->vvvv
            • Evex->vl/rc
            • Evex->pp
            • Evex->aaa
            • Xcr0bits-debug
            • Vex3-byte1-equiv-under-mask
            • Vex3-byte2-equiv-under-mask
            • Vex2-byte1-equiv-under-mask
            • Vex-prefixes-equiv-under-mask
            • Rflagsbits-equiv-under-mask
            • Ia32_eferbits-equiv-under-mask
            • Evex-prefixes-equiv-under-mask
            • Evex-byte3-equiv-under-mask
            • Evex-byte2-equiv-under-mask
            • Evex-byte1-equiv-under-mask
            • Cr0bits-debug
            • Xcr0bits-equiv-under-mask
            • Sib-equiv-under-mask
            • Prefixes-equiv-under-mask
            • Cr8bits-equiv-under-mask
            • Cr4bits-equiv-under-mask
            • Cr3bits-equiv-under-mask
            • Cr0bits-equiv-under-mask
            • Vex3-byte1-debug
            • Prefixes-debug
            • Ia32_eferbits-debug
            • Evex-byte1-debug
            • Vex3-byte2-debug
            • Vex2-byte1-debug
            • Vex-prefixes-debug
            • Evex-prefixes-debug
            • Evex-byte3-debug
            • Evex-byte2-debug
            • Cr3bits-debug
            • Sib-debug
            • Cr8bits-debug
          • Utilities
        • Debugging-code-proofs
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Quote
  • Opcode-maps-structures

Opcode

This is a product type introduced by defprod.

Fields
op — 24bits
Includes escape bytes of two- and three-byte opcodes as well
mode — op-mode
reg — maybe-3bits
ModR/M.reg descriptor
mod — mod
ModR/M.mod descriptor
r/m — maybe-3bits
ModR/M.r/m descriptor
pfx — op-pfx
rex — rex
REX descriptor
vex — maybe-vex
evex — maybe-evex
feat — ACL2::symbol-list
superscripts — superscripts
group — opcode-extension-group

Subtopics

Opcode-fix
Fixing function for opcode structures.
Make-opcode
Basic constructor macro for opcode structures.
Opcode-p
Recognizer for opcode structures.
Opcode-equiv
Basic equivalence relation for opcode structures.
Change-opcode
Modifying constructor for opcode structures.
Opcode->superscripts
Get the superscripts field from a opcode.
Opcode->group
Get the group field from a opcode.
Opcode->vex
Get the vex field from a opcode.
Opcode->r/m
Get the r/m field from a opcode.
Opcode->reg
Get the reg field from a opcode.
Opcode->pfx
Get the pfx field from a opcode.
Opcode->mode
Get the mode field from a opcode.
Opcode->feat
Get the feat field from a opcode.
Opcode->evex
Get the evex field from a opcode.
Opcode->rex
Get the rex field from a opcode.
Opcode->op
Get the op field from a opcode.
Opcode->mod
Get the mod field from a opcode.