Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Program-execution
Introduction
X86isa-build-instructions
Publications
Contributors
Machine
Syscalls
Cpuid
X86isa-state
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
Opcode-maps
Cpuid
Create-inst-doc
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
Implemented-opcodes
Create-insts-doc
Create-insts-doc-aux
Chk-exc-fn
Gen-operand-type-code-doc
Gen-addressing-method-code-doc
Create-arg-doc
Create-extra-info-doc
Create-extra-info-doc-string
Create-args-doc
Symbol-list-to-string
Get-operand-type-code-doc
Get-addressing-method-doc
Filtering-instructions
Addressing-method-code-p
Operand-type-code-p
Eval-pre-map
X86-run
Implemented-opcodes
Three-byte-opcode-decode-and-execute
X86-run-halt-count
Two-byte-opcode-decode-and-execute
X86-run-steps
X86-run-halt
X86-fetch-decode-execute-halt
X86-run-steps1
Physical-memory
Decoding-and-spec-utils
Instructions
X86-modes
Register-readers-and-writers
Segmentation
Other-non-deterministic-computations
Environment
Paging
Implemented-opcodes
Proof-utilities
To-do
Concrete-simulation-examples
Model-validation
Utils
Debugging-code-proofs
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
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.