A debugging tool for ACL2 programs. The sneaky functions allow you to save and mutate global variables, even without access to state.
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)
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:
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.
The sneaky book requires a trust tag. In raw Lisp, we add a Common Lisp
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
Meanwhile, to be able to retrieve values, the special operations sneaky-load and sneaky-alist allow you to access the
(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)))