|
|
|---|
|
|
|
|---|
Setting up the x86 ISA model for a program run.
IMPORTANT: Note that if these books were built using any
other value of
First, obtain the x86 machine-code version of the program you want to execute on the model. Note that we support only ELF (created on Linux machines) and Mach-O binaries (created on Darwin/Apple machines).
Here is a sample popcount program in C that will be used for illustration throughout this section.
// FILENAME: popcount.c // From Sean Anderson's Bit Twiddling Hacks // See https://graphics.stanford.edu/~seander/bithacks.html #include<stdio.h> #include<stdlib.h> int popcount_32 (unsigned int v) { v = v - ((v>> 1)& 0x55555555); v = (v& 0x33333333) + ((v>> 2)& 0x33333333); v = ((v + (v>> 4)& 0xF0F0F0F) * 0x1010101)>> 24; return(v); } int main (int argc, char *argv[], char *env[]) { int v; printf ("\nEnter a 32-bit number: "); scanf ("%d",& v); v = v& 0xffffffff; printf ("\nPopcount of %d is: %d\n", v, popcount_32(v)); return 0; }
We can use the following command to obtain the x86 binary
corresponding to this program; we will call this binary
gcc popcount.c -o popcount.o
You can see the assembly and machine code corresponding to this
program using utilities like
On Linux machines:
objdump -d popcount.o
On Mac machines:
otool -tvj popcount.o
Note that the assembly and machine code can differ from machine to machine, program run to program run. All the concrete values of addresses, etc. used in this example can be different for you.
The following events describe the process of setting up the x86 ISA
model for the execution of
Include the top-level book (i.e., X86ISA/top.lisp) in a fresh ACL2 session.
(include-book "top" :ttags :all)
Alternatively, it can be faster to just include tools/execution/top.lisp.
(include-book "tools/execution/top" :ttags :all)
You should always be in the
(in-package "X86ISA")
(init-sys-view 0 x86)
Read and load
(binary-file-load "popcount.o" :elf t) ;; or :mach-o t
Use init-x86-state-64 to modify other components of the
x86 state, like the instruction pointer, registers, arguments in
memory, if necessary. This function only writes the specified values
into the x86 state while preserving any values previously written to
the x86 state. For example, the following form will not make
changes to any general-purpose registers except
(init-x86-state-64 ;; Status (MS and fault field) nil ;; Start Address --- set the RIP to this address #x100000f12 ;; Initial values of General-Purpose Registers '((#.*rdi* . #xff00ff00) (#.*rsp* . #.*2^45*)) ;; Control Registers: a value of nil will not nullify existing ;; values. nil ;; Model-Specific Registers: a value of nil will not nullify existing ;; values. nil ;; Segment Registers: a value of nil will not nullify existing values. nil ; visible portion nil nil nil ; hidden portion ;; Rflags Register 2 ;; Memory image: a value of nil will not nullify existing values. nil ;; x86 state x86)
Aside: Some other ways to initialize the x86 state are listed below. The list is not exhaustive.
The memory image argument of init-x86-state accepts
alists satisfying n64p-byte-alistp. This can be used to
provide a program binary in the form of a list of address-byte pairs
rather using
The function load-program-into-memory also accepts
programs that satisfy
Of course, wml08 (and its friends like write-bytes-to-memory) can also be used to write a program to the
memory. Initialization of other components of the x86 state can be
done by using the appropriate updater functions directly. For
example,
All the mechanisms to initialize the x86 state aside, how do we
know what values to put in the x86 state? This is an important and
interesting question. Its answer depends on the program (or snippet
of a program) we intend to execute and requires the user to be
familiar with x86 assembly and calling conventions. For this popcount
example, suppose all we wanted to execute was the
... 100000f10: 89 c7 mov %eax,%edi 100000f12: e8 49 ff ff ff callq 100000e60<_popcount_32> 100000f17: 48 8d 3d 66 00 00 00 lea 0x66(%rip),%rdi ...
We set the start address to be the address of the instruction that
calls the
Before entering
... 0000000100000e60<_popcount_32> : 100000e60: 55 push %rbp 100000e61: 48 89 e5 mov %rsp,%rbp 100000e64: 89 7d fc mov %edi,-0x4(%rbp) ...
It should be emphasized that it is the user's responsibility to
ensure that the state is initialized "correctly", i.e., the program
does not overlap with the page tables, the stack pointer is
initialized so that the stack does not run out of memory nor does it
overwrite the program during execution (in our example,
Run the program using x86-run or x86-run-steps or x86-run-halt. To run one instruction only, use x86-fetch-decode-execute. You can also see Dynamic-instrumentation for details about dynamically debugging the program by inserting breakpoints and logging the x86 state into a file, etc.
(x86-run-halt #x100000f17 ;; halt-address
10000 ;; limit on number of steps to be run
x86)
;; or
;; (x86-run-steps 10000 x86)
;; or
;; (x86-run 10000 x86)
How do know that the program ran to completion? After executing the above form, we can inspect the contents of the following fields:
(fault x86) (ms x86) (rip x86)
If the
Where did the number
This, again, is up to the user. Guessing the clock value is an
answer. In our example,
Inspect the output of the program. For this program, register
(rgfi *rax* x86) ;; Note that eax is the low 32 bits of rax.
For the value
If you wish to run this program again in the same ACL2 session, remember to initialize the x86 state appropriately.