PRINT-GV

print a form whose evaluation caused a guard violation
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) or stobj fields of stobjs, you may 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-stobj>|))
In this example you could replace ``|<some-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-stobj>|))
But if you replace ``|<some-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.