		Search-engine friendly clone of the ACL2 documentation.

Debugging

Sneaky

A debugging tool for ACL2 programs. The sneaky functions allow you to save and mutate global variables, even without access to state.

Introductory example

ACL2 !> (defun my-function (x y)           ;; note: no state
          (b* ((sum     (+ x y))
               (product (* x y)))
            (sneaky-save :sum sum)         ; save the latest sum
            (sneaky-save :product product) ; save the latest product
            (sneaky-incf :calls 1)         ; count how many calls there were
            (list sum product)))

ACL2 !> (my-function 1 2)
(3 2)

ACL2 !> (my-function 3 4)
(7 12)

ACL2 !> (defconsts (*sum* state)           ;; *sum* is 7
          (sneaky-load :sum state))        ;; (its most recent value)

ACL2 !> (defconsts (*product* state)       ;; *product* is 7
          (sneaky-load :product state))    ;; (its most recent value)

ACL2 !> (defconsts (*calls* state)         ;; *calls* is 2
          (sneaky-load :product state))    ;; (we called my-function twice)

Motivation

When you are debugging a large program, you may want to get a hold of internal values from some function that is somehow "deep" inside your computation. Here are some ways you might do this:

Printing. You could, perhaps via redef, add cw statements to print out the desired values. This is easy and works well when your values are small enough to print, and your function is called infrequently enough that the printing is not unmanageable.
Tracing. If the values you want to see are inputs or outputs of a function, you could perhaps use trace$. This may avoid needing to rebuild or use redef. Like printing, this is likely to work well for inspecting small values and infrequently called functions.
Globals. If your functions involves state, you might be able to just assign the values of interest to some new state globals. You could then extract and inspect them using @. This approach may work well even for large values or frequently called functions, but requires access to state.

Unfortunately, if your program is made up of ordinary, pure ACL2 functions that do not involve state, then using globals might require adding state all throughout the call tree. This could be really difficult, especially for a one-off investigation.

The sneaky mechanism allows you to work around this limitation: it is very similar to using globals, but allows you to avoid state.

Implementation

The sneaky book requires a trust tag. In raw Lisp, we add a Common Lisp variable, the *sneaky-state*, which is a hash table associating names with values.

The main sneaky operations, like sneaky-save, sneaky-push, and sneaky-incf, allow you to manipulate the values in this hash table, but only indirectly. This keeps the *sneaky-state* as a purely Common Lisp variable that exists outside of ACL2, so the effects of manipulating this state are logically invisible. That is, in the logic, all of these functions just return nil.

Meanwhile, to be able to retrieve values, the special operations sneaky-load and sneaky-alist allow you to access the *sneaky-state*. However, in the logic these functions just read from the ACL2 oracle. So, even though a sequence like:

(sneaky-save :foo 5)
(sneaky-load :foo state)   ;; should always return (mv '5 state)

There is no logical connection between the sneaky save/load, so you should never be able to prove theorems such as

(defthm unprovable
  (progn$ (sneaky-save :foo 5)
          (equal (mv-nth 0 (sneaky-load :foo state)) 5)))

Subtopics

Sneaky-mutate: Low-level way to modify the sneaky store.
Sneaky-push: Extend a value in the sneaky store.
Sneaky-incf: Increment a value in the sneaky store.
Sneaky-save: Assign a value into the sneaky store.
Sneaky-load: Load a value that was previously saved into the sneaky store.
Sneaky-load-list: Load a list of values that were previously saved into the sneaky store.
Sneaky-alist: Load an alist containing all values previously saved into the sneaky store.
Sneaky-pop: Pop the car off a list in the sneaky store.
Sneaky-cw: Print a value from the sneaky store.
Sneaky-delete: Delete the data stored under a key from the sneaky store.
Sneaky-clear: Clear all data stored in the sneaky store.