		Search-engine friendly clone of the ACL2 documentation.

Dynamic-instrumentation

Utilities to instrument a program run on the model

Command Reference

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 acl2-instrument.log by default. The log file's name can be changed by the following:
```
 (!log-file-name "my-very-own-log-file") 
```
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 rflags field in the x86 state):
```
(printing-flgs x86 state) 
```
The following will interpret its first argument (100 in this example) as an rflags value and print the values of CF, PF, AF, ZF, SF, and OF flags.
```
(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 stepi command of GDB):
```
 (one_step) 
```
one_step logs the resulting state in the log file, which is called acl2-instrument.log by default, and can be changed via !log-file-name.
To execute <n> steps of a program (or less if it halts or an error occurs):
```
 (big_step <n>) 
```
big_step logs the final state in the log file, which is called acl2-instrument.log by default, and can be changed via !log-file-name.
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):
```
 (log_instr) 
```
log_instr logs the x86 state after every instruction in the log file, which is called acl2-instrument.log by default, and can be changed via !log-file-name. Note that if you are executing a large number of instructions, log_instr might be really slow because of all the file output.

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 x86-break repeatedly.

See all active breakpoints:
```
 (show-breakpoints) 
```
To delete all breakpoints:
```
(delete-all-breakpoints)
```
To delete some breakpoints:
```
 (delete-breakpoints '(0 2)) 
```
delete-breakpoints takes a list of the identifiers of the breakpoints, where the identifiers are reported by show-breakpoints.
Run the program when breakpoints are set:
```
 (x86-debug) 
```
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 continue-debug below. Note that x86-debug works only when at least one breakpoint is set.

x86-debug logs the x86 state after every breakpoint in the log file, which is called acl2-instrument.log by default, and can be changed via !log-file-name.

When x86-debug stops when a breakpoint is reached, the ms field contains BREAKPOINT-REACHED. This can be used to differentiate between executions that stop because of an error or those that stop when a breakpoint is reached.
To continue execution of the program past a breakpoint:
```
 (continue-debug) 
```
Note that continue-debug will set the contents of MS to nil only if MS contained breakpoint-reached, then it will step one instruction, and then carry on with x86-debug.

Since continue-debug essentially calls x86-debug, it logs the x86 state after every breakpoint in the log file, which is called acl2-instrument.log by default, and can be changed via !log-file-name.

continue-debug also sets ms to BREAKPOINT-REACHED if it stops at a breakpoint. ms will be set to a legal halt message when (if) continue-debug finally leads the program to completion.
To record the x86 state at a breakpoint and then continue:
```
(x86-debug!)
```
x86-debug! logs the x86 state after every breakpoint in the log file and continues execution till a halt or error is encountered or if (2^60 - 1) instructions (Do we need to say again that you might never want to execute these many instructions?) have been executed (whatever comes first).

Subtopics

Printing-x86-components: Functions to print some components of the x86 state, either to file (printing-x86-components) or to terminal (printing-x86-to-terminal)
!log-file-name: Assign a log file where the instrumentation output from printing-x86-components will be stored