Major Section: OTHER
By default, ACL2 checks input constraints on functions, known as
guards. When guards are violated, an informative message is printed;
but sometimes it is useful to investigate why the guard check fails. The
utility print-gv is provided for that purpose. (Alternatively, you may
prefer to avoid guards entirely with (set-guard-checking :none);
see set-guard-checking.)
Example Forms:
(print-gv)
(print-gv :evisc-tuple (evisc-tuple 4 4 nil nil))
(print-gv :evisc-tuple (evisc-tuple 4 ; print-level
5 ; print-length
(world-evisceration-alist state nil)
nil ; hiding-cars
))
General Form: (print-gv :evisc-tuple x)where the
:evisc-tuple argument is optional and defaults to one that
hides only the ACL2 logical world, by printing <world> instead of a
very large structure. See evisc-tuple for a discussion of evisc-tuples.To see how one might use print-gv, consider the following definition.
(defun foo (x)
(declare (xargs :guard (and (my-first-predicate x)
(my-second-predicate x))))
(cdr x))
Now suppose we evaluate a call of foo and obtain a guard violation.
ACL2 !>(foo 3) ACL2 Error in TOP-LEVEL: The guard for the function call (FOO X), which is (AND (MY-FIRST-PREDICATE X) (MY-SECOND-PREDICATE X)), is violated by the arguments in the call (FOO 3). 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 !>We can obtain (in essence) the guard form that was false, as follows.
ACL2 !>(print-gv)
(LET ((X '3))
(DECLARE (IGNORABLE X))
(AND (MY-FIRST-PREDICATE X)
(MY-SECOND-PREDICATE X)))
ACL2 !>
But which conjunct is to blame? With a bit of editing we can try each
conjunct in turn.
ACL2 !>(LET ((X '3))
(DECLARE (IGNORABLE X))
(MY-FIRST-PREDICATE X))
T
ACL2 !>(LET ((X '3))
(DECLARE (IGNORABLE X))
(MY-SECOND-PREDICATE X))
NIL
ACL2 !>
Aha! Now we can investigate why the second predicate fails for 3.The following hack will give you access in raw Lisp to the form printed by
(print-gv). After a guard violation, just submit this form to raw Lisp:
(print-gv1 (wormhole-data (cdr (assoc 'ev-fncall-guard-er-wormhole
*wormhole-status-alist*)))
state)
If you use local stobjs (see with-local-stobj), you my need to edit the
output of print-gv in order to evaluate it. Consider the following
example.
(defstobj st fld)
(defun g (x st)
(declare (xargs :guard (consp x) :stobjs st)
(ignore x))
(fld st))
(defun test ()
(with-local-stobj
st
(mv-let (result st)
(mv (g 3 st) st)
result)))
(test)
Then :print-gv yields the result shown below.
(FLET ((G{GUARD} (X ST)
(DECLARE (IGNORABLE X ST))
(AND (STP ST) (CONSP X))))
(G{GUARD} '3 |<some-local-stobj>|))
In this example you could replace ``|<some-local-stobj>|'' by ``st''
to obtain a result of nil. But similar cases may require the use of a
local stobj that is no longer available, in which case you may need to be
creative in order to take advantage of :print-gv. Here is such an
example.
(defstobj st2 fld2)
(defun g2 (st2)
(declare (xargs :guard (null (fld2 st2)) :stobjs st2))
(mv 0 st2))
(defun test2 ()
(with-local-stobj
st2
(mv-let (result st2)
(let ((st2 (update-fld2 17 st2)))
(g2 st2))
result)))
(test2)
In this case, :print-gv yields the following.
(FLET ((G2{GUARD} (ST2)
(DECLARE (IGNORABLE ST2))
(AND (ST2P ST2) (NULL (FLD2 ST2)))))
(G2{GUARD} |<some-local-stobj>|))
But if you replace ``|<some-local-stobj>|'' by ``st'', the guard
holds; it is only the local stobj, which is no longer available, that
produced a guard violation (because its field had been updated to a cons).
ACL2 !>(FLET ((G2{GUARD} (ST2)
(DECLARE (IGNORABLE ST2))
(AND (ST2P ST2) (NULL (FLD2 ST2)))))
(G2{GUARD} st2))
T
ACL2 !>
Finally, we note that while print-gv is a utility for debugging guard
violations, in contrast, see guard-debug for a utility to assist in
debugging failed proofs arising from guard verification.
