Utilities to instrument a program run on the model
Utilities to save the x86 state to a log file:
(printing-x86-components 16 x86 state) ;; 16 is the print-base.
The current state of the general-purpose registers, instruction
pointer, and the flags will be stored in a log file, which is called
Utilities to print the x86 state in the ACL2 session (and not log it into a file):
The current state of the general-purpose registers, instruction pointer, and the flags can be printed on screen by the following:
(printing-x86-to-terminal 16 x86 state) ;; 16 is the print-base.
The following will print the current values of CF, PF, AF, ZF, SF,
and OF flags (i.e., from the
(printing-flgs x86 state)
The following will interpret its first argument (100 in this
example) as an
(printing-flg-val 100 state)
To trace memory reads and writes, you can use the following:
;; Trace rml08 and rml16. (trace-read-memory (rml08 rml16)) ;; The following is the same as ;; (trace-read-memory (rml08 riml08 rml16 riml16 rml32 riml32 rml64 riml64)) (trace-all-reads) ;; Trace wml32 and wml64. (trace-write-memory (wml32 wml64)) ;; The following is the same as ;; (trace-write-memory (wml08 wiml08 wml16 wiml16 wml32 wiml32 wml64 wiml64)) (trace-all-writes)
You can send the output of these memory traces to file using the ACL2 utility open-trace-file. Note that doing so will also send the output of any other functions that you have traced to the same file.
To step the interpreter once (like
To step the interpreter till a halt instruction (#xF4) is encountered or an error occurs or (2^60 - 1) instructions (you will probably never want to execute these many instructions all at once) have been executed (whatever comes first):
To set a breakpoint:
(x86-break '(equal (rip x86) 10)) (x86-break '(equal (rgfi *rax* x86) 42)) (x86-break '(and (equal (rgfi *rsp* x86) 0) (equal (rip x86) 12)))
Any well-formed ACL2 expression that evaluates to a boolean is a
valid breakpoint. Multiple breakpoints can be set using
See all active breakpoints:
To delete all breakpoints:
To delete some breakpoints:
(delete-breakpoints '(0 2))
Run the program when breakpoints are set:
Like GDB, the first breakpoint encountered will stop the execution of the program. Of course, execution can also come to a stop if an error is encountered or if (2^60 - 1) instructions (again, you probably never want to execute these many instructions!) have been executed (whatever comes first).
To continue execution, see
To continue execution of the program past a breakpoint:
To record the x86 state at a breakpoint and then continue: