Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Zfc
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
C
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
Java
Taspi
Bitcoin
Riscv
Des
Ethereum
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
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
X86-run
Implemented-opcodes
Three-byte-opcode-decode-and-execute
X86-run-halt-count
Two-byte-opcode-decode-and-execute
X86-run-steps
Opcode-maps
X86-run-halt
X86-fetch-decode-execute-halt
X86-run-steps1
Physical-memory
Decoding-and-spec-utils
Instructions
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
Sha-2
Yul
Zcash
Proof-checker-itp13
Regex
ACL2-programming-language
Json
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Axe
Bigmems
Builtins
Execloader
Aleo
Solidity
Paco
Concurrent-programs
Bls12-377-curves
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Machine
X86-decoder
Definitions of the x86 fetch, decode, and execute function and the top-level run function
Subtopics
Get-prefixes
Fetch and store legacy and REX prefixes, if any, of an instruction
Vex-0f3a-execute
Dispatch function for VEX-encoded instructions in the second three-byte opcode map
Vex-0f38-execute
Dispatch function for VEX-encoded instructions in the first three-byte opcode map
Vex-0f-execute
Dispatch function for VEX-encoded instructions in the two-byte opcode map
Two-byte-opcode-execute
Two-byte opcode dispatch function.
Second-three-byte-opcode-execute
Second three-byte opcode dispatch function.
One-byte-opcode-execute
Top-level dispatch function.
First-three-byte-opcode-execute
First three-byte opcode dispatch function.
Evex-0f3a-execute
Dispatch function for EVEX-encoded instructions in the second three-byte opcode map
Evex-0f38-execute
Dispatch function for EVEX-encoded instructions in the first three-byte opcode map
Evex-0f-execute
Dispatch function for EVEX-encoded instructions in the two-byte opcode map
X86-fetch-decode-execute
Top-level step function
Vex-decode-and-execute
Evex-decode-and-execute
X86-run
Top-level specification function for the x86 ISA model
Implemented-opcodes
Intel opcodes supported in
x86isa
.
Three-byte-opcode-decode-and-execute
Decoder and dispatch function for three-byte opcodes, where
0x0F 0x38
are the first two opcode bytes
X86-run-halt-count
A combination in functionality of
x86-run-steps
and
x86-run-halt
Two-byte-opcode-decode-and-execute
Decoder and dispatch function for two-byte opcodes
X86-run-steps
An alternative to
x86-run
Opcode-maps
ACL2 representation of x86 Opcode Maps (see Intel Manuals, Vol. 2, Appendix A)
X86-run-halt
Alternative version of
x86-run
that uses
x86-fetch-decode-execute-halt
instead of
x86-fetch-decode-execute
X86-fetch-decode-execute-halt
Alternative version of
x86-fetch-decode-execute
that sets the
MS
field if
rip
is equal to
halt-address
X86-run-steps1
