Machine
Core elements of the x86 ISA, like the x86 state,
decoder function, etc., and proofs about the x86 ISA
specification.
Subtopics
- Syscalls
- Extending the x86 ISA with the system call model in the
application-level view
- Cpuid
- Determining which CPUID features are supported in x86isa
- X86isa-state
- The state of the x86isa model
- Linear-memory
- Linear Memory Accessor and Updater Functions
- Rflag-specifications
- Specifications of rflags
- Characterizing-undefined-behavior
- An undef field in the x86 state feeds unknown
values to processor components that are undefined
- Top-level-memory
- Top-level Memory Accessor and Updater Functions
- App-view
- Application-level view of the x86 model
- X86-decoder
- Definitions of the x86 fetch, decode, and execute function
and the top-level run function
- Physical-memory
- Physical memory read and write functions
- Decoding-and-spec-utils
- Miscellaneous utilities for instruction decoding and for writing
instruction specification functions
- Instructions
- Umbrella topic for specification of Intel's x86 instructions
- X86-modes
- Modes of operation of the processor.
- Segmentation
- Specification of x86 segmentation.
- Register-readers-and-writers
- Top-level utilities for reading and writing into various
registers
- Other-non-deterministic-computations
- Definitions of other non-deterministic computations
- Environment
- Defining the environment field for reasoning about
non-deterministic computations
- Paging
- Specification of x86 Paging
