Wet
Evaluate a form and print subsequent error trace
The acronym ``wet'' stands for ``with-error-trace''. Wet
provides a convenient way to obtain a backtrace when evaluation causes a guard
violation or other error.
Summary Documentation
General Form:
(wet form ; an arbitrary form
:book bk-form ; optional, not evaluated; specify different wet book
;;; the rest are optional and evaluated:
:compile c ; :same, t, or nil; default :same (nil if :fns supplied)
:fullp h ; nil by default, else handle some raw Lisp errors
:evisc-tuple e ; an evisc-tuple
:fns fns ; :all, or a list of functions to show in a backtrace
Form is evaluated. If there is an error, a backtrace stack is printed
to the standard output (*standard-co*), containing (by default) the
user-defined function calls made before the error. Such printing is
controlled by the :evisc-tuple if supplied; otherwise, hiding of large
structures will occur.
Discussion
The basic idea is that (wet form) evaluates form and, if there is
an error, shows a backtrace of calls that led to that error. Note however
that by default only calls of user-defined (not built-in) functions
``supporting'' form in the following sense will show up in the backtrace:
those that occur in the macroexpansion of form or (recursively) support
any of those functions. So for example, since (make-event form)
macroexpands to (make-event-fn (quote form) ...), calls of functions
occurring in form will likely not show up in the backtrace by default.
The option :fns all overrides this default, with potential loss of speed;
more on this below.
The following example explains the use of wet. First, submit the
following three definitions:
(defun foo (x) (declare (xargs :guard (consp x))) (car x))
(defun bar (x) (foo (cdr x)))
(defun g (x) (bar (cdr x)))
Now imagine you have obtained the following guard violation:
ACL2 !>(g '(3 4))
ACL2 Error in TOP-LEVEL: The guard for the function call (FOO X),
which is (CONSP X), is violated by the arguments in the call (FOO NIL).
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See
:DOC set-guard-checking for information about suppressing this check
with (set-guard-checking :none), as recommended for new users.
ACL2 !>
With wet, you can get a backtrace of user-defined functions. The
package prefixes shown below, ACL2_*1*_, indicate that the
executable-counterparts of the corresponding submitted functions are being
called; see evaluation. Don't forget to start with (include-book
"misc/wet" :dir :system).
ACL2 !>(wet (g '(3 4)))
; Fast loading /projects/acl2/devel/books/misc/wet.fasl
TTAG NOTE: Adding ttag :TRACE! from the top level loop.
ACL2 Error in WET: The guard for the function call (FOO X), which
is (CONSP X), is violated by the arguments in the call (FOO NIL).
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See
:DOC set-guard-checking for information about suppressing this check
with (set-guard-checking :none), as recommended for new users.
Backtrace stack:
----------------
1. (ACL2_*1*_ACL2::FOO NIL)
2. (ACL2_*1*_ACL2::BAR (4))
3. (ACL2_*1*_ACL2::G (3 4))
ACL2 !>
By default, large structures are hidden during the printing of the
backtrace stack. (Technical detail: by default the global abbrev-evisc-tuple
is used, if bound; see set-evisc-tuple. But you can supply a value for
keyword argument :evisc-tuple to modify the printing: nil to avoid
hiding, else a suitable evisc-tuple, as shown below (see evisc-tuple).
ACL2 !>(wet (g '(3 4)) :evisc-tuple (evisc-tuple 1 1 nil nil))
; Fast loading /projects/acl2/devel/books/misc/wet.fasl
TTAG NOTE: Adding ttag :TRACE! from the top level loop.
ACL2 Error in WET: The guard for the function call (FOO X), which
is (CONSP X), is violated by the arguments in the call (FOO NIL).
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See
:DOC set-guard-checking for information about suppressing this check
with (set-guard-checking :none), as recommended for new users.
Backtrace stack:
----------------
1. (ACL2_*1*_ACL2::FOO ...)
2. (ACL2_*1*_ACL2::BAR ...)
3. (ACL2_*1*_ACL2::G ...)
ACL2 !>
For a backtrace as a data object, evaluate the form (@ wet-stack).
But note that this object may not be a legal ACL2 value, for example because
of the ``*1*'' symbols shown above.
Keyword Arguments
The :fullp option. Consider the following example.
(program)
(defun foo (x) (declare (xargs :guard (consp x))) (car x))
(defun bar (x) (foo (cdr x)))
(defun g (x) (bar (cdr x)))
; Raw Lisp error:
(g '(3 4 . 5))
We may be initially disappointed using wet on this example, as follows
— it didn't work!
ACL2 p!>(wet (g '(3 4 . 5)))
TTAG NOTE: Adding ttag :TRACE! from the top level loop.
***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error: Fault during read of memory address #x2D
While executing: FOO
***********************************************
The message above might explain the error. If not, and
if you didn't cause an explicit interrupt (Control-C),
then it may help to see :DOC raw-lisp-error.
To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)
ACL2 p!>
The fix is to use :fullp t.
ACL2 p!>(wet (g '(3 4 . 5)) :fullp t)
TTAG NOTE: Adding ttag :TRACE! from the top level loop.
ACL2 Error in WET: The guard for the :program function call (FOO X),
which is (CONSP X), is violated by the arguments in the call (FOO 5).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.
Backtrace stack:
----------------
1. (ACL2_*1*_ACL2::FOO 5)
2. (ACL2_*1*_ACL2::BAR (4 . 5))
3. (ACL2_*1*_ACL2::G (3 4 . 5))
ACL2 p!>
Why doesn't wet always do things this way? The answer pertains to
performance. When :fullp is non-nil, wet sets guard-checking to
:all before evaluating the given form; see set-guard-checking.
This may slow down evaluation substantially, which is why it is not the
default behavior.
The :fns option. As mentioned above, by default the wet
backtrace shows user-defined functions that syntactically ``support'' the form
being evaluated. This default can be overridden by supplying an explicit
list, fns, of functions, using option :fns fns; these will then be
the functions whose calls are eligible for inclusion in the backtrace. The
special value :fns :all will allow all user-defined function calls in the
backtrace. This value can be useful when using magic-ev-fncall, for
example, since the function being applied isn't typically included as a
syntactic supporter of the form being evaluated.
The :compile option. Wet uses the trace$ utility to
modify the definitions of affected functions so that they can record
information for the backtrace. As described above, these affected functions
are those that syntactically ``support'' the form unless specified by the
:fns option. As is the case for trace$ — see trace$
— the new definitions of these affected functions may or may not be
compiled. For trace$ and for wet, the default is to compile the new
definition if and only if the original definition was compiled, except: For
wet, if option :fns :all is provided, then the default is not to
compile the affected definitions. And for trace$ and wet, the
:compile option overrides the default, to specify what will be compiled:
value :same to compile each affected function if and only if its original
definition was compiled, value t to compile all affected functions, and
value nil to skip compilation.
The :book option. Wet actually works by temporarily including a
community book,
(include-book "misc/wet" :dir :system)
and then passing its arguments to macro wet!, defined in that book.
The keyword argument :book allows you to specify a different book that
defines a macro wet! to which to pass its arguments. If the value of
:book is a string, then the book named by that string is temporarily
included using include-book: (include-book "bk"). Otherwise
:book should be a list of arguments, to be provided (unevaluated) to
include-book, for example ("my-wet" :dir :my-utils). Thus you
can experiment by copying community book books/misc/wet.lisp to your own
directory and making modifications to the copy. If you make changes, we
invite you to share them with the ACL2 community (see books). Note
that you can also supply :book nil, in which case the definition of
wet! in your current session will be used without including a book.
Concluding Remark
Also see trace$ for a general tracing utility. As mentioned above,
wet is implemented using trace$. Wet actually first applies
untrace$; upon completion, wet then applies trace$ to
re-trace any functions that it had untraced, using their original trace
specs.
