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
Physical-memory
Decoding-and-spec-utils
Instructions
Two-byte-opcodes
One-byte-opcodes
Fp-opcodes
Instruction-semantic-functions
Opcode-maps
Cpuid
Create-inst-doc
Opcode-maps-structures
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-illegal-instruction
Implemented-opcodes
X86-general-protection
X86-device-not-available
X86-step-unimplemented
Privileged-opcodes
Three-byte-opcodes
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
Instructions
X86-decoder
Opcode-maps
ACL2 representation of x86 Opcode Maps (see Intel Manuals, Vol. 2, Appendix A)
Subtopics
Cpuid
Determining which CPUID features are supported in
x86isa
Create-inst-doc
Opcode-maps-structures
Structures for representing Intel's x86 Opcode Maps in ACL2
Implemented-opcodes
Intel opcodes supported in
x86isa
.
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
Some Functions to operate on the ACL2 representation of Intel's Opcode Maps
Addressing-method-code-p
Codes for Operand Addressing Method; See Intel Vol. 2, Appendix A.2.1
Operand-type-code-p
Codes for Operand Type; See Intel Vol. 2, Appendix A.2.2
Eval-pre-map