Search-engine friendly clone of the
ACL2 documentation
.
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
Booting-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
.