X86isa
x86 ISA model and machine-code analysis framework developed
at UT Austin.
Subtopics
- Program-execution
- Setting up the x86 ISA model for a program run.
- Sdm-instruction-set-summary
- Summary of what instructions are implemented/unimplemented, as organized in the
Instruction Set Summary of the Intel Software Developer Manual (volume 1
chapter 5).
- Tlb
- A translation lookaside buffer for the x86isa model.
- Booting-linux
- Booting linux on the x86isa model.
- Introduction
- A formal and executable model of the x86 Instruction Set
Architecture.
- Asmtest
- A simple framework for testing execution of small programs against
the x86isa model.
- X86isa-build-instructions
- Building books related to the x86 ISA and the machine-code
analysis framework.
- Publications
- Technical publications related to these x86isa books.
- Contributors
- Authorship details and acknowledgments.
- Machine
- Core elements of the x86 ISA, like the x86 state,
decoder function, etc., and proofs about the x86 ISA
specification.
- Implemented-opcodes
- Intel opcodes supported in x86isa.
- To-do
- Known issues, planned activities, wishlists, etc.
- Proof-utilities
- Basic utilities for x86 machine-code proofs.
- Peripherals
- The various peripherals the x86isa model contains
- Model-validation
- How do we trust that our x86 ISA model is faithful to the
real machine?
- Modelcalls
- Modelcalls, like syscalls, but instead of calling into the OS, we call into the model.
- Concrete-simulation-examples
- Utils
- Utilities for rest of the X86ISA books.
- Debugging-code-proofs
