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
Introduction
X86isa-build-instructions
Publications
Contributors
Machine
Implemented-opcodes
Proof-utilities
To-do
Concrete-simulation-examples
Model-validation
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
Inst
Op/en-p
Operands
Operands-fix
Make-operands
Operands-equiv
Change-operands
Operands->op4
Operands->op3
Operands->op2
Operands->op1
Operands-p
Operand-type-p
Strict-opcode-p
Opcode-extension-group-p
Superscripts-p
Maybe-operands-p
Inst-list-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
4bits
2bits
16bits
Paging-bitstructs
3bits
11bits
40bits
5bits
32bits
19bits
10bits
7bits
64bits
54bits
45bits
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
Operands
This is a product type introduced by
defprod
.
Fields
op1 —
operand-type
op2 —
operand-type
op3 —
operand-type
op4 —
operand-type
Subtopics
Operands-fix
Fixing function for
operands
structures.
Make-operands
Basic constructor macro for
operands
structures.
Operands-equiv
Basic equivalence relation for
operands
structures.
Change-operands
Modifying constructor for
operands
structures.
Operands->op4
Get the
op4
field from a
operands
.
Operands->op3
Get the
op3
field from a
operands
.
Operands->op2
Get the
op2
field from a
operands
.
Operands->op1
Get the
op1
field from a
operands
.
Operands-p
Recognizer for
operands
structures.