Initialize-x86-state
Initializing the x86 state for concrete program execution.
The utilities in this section are meant to be used to
initialize the x86 state when doing concrete execution or when
bit-blasting using GL. These are not intended for doing proofs using
rewriting. For utilities that help in code proofs, see the libraries
in directory x86isa/proofs/utilities.
Subtopics
- Init-x86-state-64
- A variant of init-x86-state that ensures 64-bit mode.
- Load-program-into-memory
- Loading a program into the model's memory.
- Init-x86-state
- A convenient function to populate the x86 state's
instruction pointer, registers, and memory.
- !seg-hidden-limiti-from-alist
- Update hidden portion of segment registers as dictated by
seg-hidden-alist, which is required to be a
seg-hidden-limiti-alistp.
- !seg-hidden-basei-from-alist
- Update hidden portion of segment registers as dictated by
seg-hidden-alist, which is required to be a
seg-hidden-basei-alistp.
- !seg-hidden-attri-from-alist
- Update hidden portion of segment registers as dictated by
seg-hidden-alist, which is required to be a
seg-hidden-attri-alistp.
- Seg-hidden-limiti-alistp
- Recognizer for pairs of segment register indices and values for the
hidden portions containing the limit value of the registers.
- Seg-hidden-basei-alistp
- Recognizer for pairs of segment register indices and values for the
hidden portions containing the base addresses of the registers.
- !seg-visiblei-from-alist
- Update visible portion of segment registers as dictated by
seg-visible-alist, which is required to be a seg-visiblei-alistp.
- Seg-visiblei-alistp
- Recognizer for pairs of segment register indices and
values for the visible portions of the registers.
- Seg-hidden-attri-alistp
- Recognizer for pairs of segment register indices and values for the
hidden portions containing the attr value of the registers.
- Rgfi-alistp
- Recognizer for pairs of general-purpose register indices and
values.
- N64p-byte-alistp
- Recognizer for a list of pairs of up to 64-bit wide linear address and byte.
- !rgfi-from-alist
- Update general-purpose registers as dictated by
rgf-alist, which is required to be a rgfi-alistp.
- !msri-from-alist
- Update model-specific registers as dictated by
msr-alist, which is required to be a msri-alistp.
- !ctri-from-alist
- Update control registers as dictated by ctr-alist,
which is required to be a ctri-alistp.
- Msri-alistp
- Recognizer for pairs of model-specific register indices and
values.
- Ctri-alistp
- Recognizer for pairs of control register indices and values.
