• 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
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
            • Two-byte-opcodes
            • One-byte-opcodes
            • Fp-opcodes
            • Instruction-semantic-functions
            • X86-illegal-instruction
            • Implemented-opcodes
            • Opcode-maps
              • Cpuid
              • 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
              • Implemented-opcodes
              • Chk-exc-fn
              • Filtering-instructions
              • Addressing-method-code-p
              • Operand-type-code-p
              • Eval-pre-map
            • X86-general-protection
            • X86-device-not-available
            • X86-step-unimplemented
            • Privileged-opcodes
            • Three-byte-opcodes
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • 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.