		Search-engine friendly clone of the ACL2 documentation.

Print-gv

Print a form whose evaluation caused a guard violation

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 ; same as above
(print-gv ; same as above, showing all system defaults
 :conjunct nil
 :evisc-tuple (print-gv-evisc-tuple)
 :substitute nil)
(print-gv :substitute 20)
(print-gv :evisc-tuple (evisc-tuple 4 4 nil nil))
(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 :conjunct c
          :substitute s
          :evisc-tuple e)

where the keyword arguments are optional. These arguments have the following effects and system defaults, but note that the defaults can be changed by the user; see set-print-gv-defaults.

The :conjunct argument is nil by default, indicating that a form is to be displayed whose evaluation represents the guard evaluation that produced nil. A value of t indicates that ACL2 should parse the guard into conjuncts, and display the conjunct that actually evaluated to nil. It does this by evaluating each conjunct in turn until one produces a result of nil.
The :evisc-tuple argument should be an evisc-tuple. Its default is the value of the expression (print-gv-evisc-tuple), which specifies hiding only the ACL2 logical world, so that the symbol <world> is printed instead of the actual world. See evisc-tuple for a discussion of evisc-tuples.
The :substitute argument is nil by default, indicating that the displayed form uses flet, which avoids duplicate occurrences of actual parameters. A value of t indicates that ACL2 should instead substitute those actuals into the guard. Otherwise the value should be a natural number n, which behaves the same as nil except when large duplicated terms are to be avoided in the precise sense below, in which case the behavior is the same as t, that is, flet is used. The latter case (using flet) applies when some variable in the guard or (if :conjunct t is specified) conjunct has at least two occurrences, and corresponds to an actual parameter with at least n conses. Note that the number of conses is counted in the ``translated'' term (guard or conjunct); see term.

Again, the user can change these defaults; see set-print-gv-defaults. For example, one might wish to evaluate (set-print-gv-defaults :substitute 20) so that flet is used only when that avoids certain duplicated large terms, as discussed just above.

Remarks

(1) Print-gv starts by temporarily replacing the current installed ACL2 world with the world that was installed at the time the guard violation took place. The current world is re-installed when print-gv returns. We illustrate this point with an example at the end of this topic.
(2) The output from print-gv always goes to the terminal. (Specifically, the output goes to the value of the constant *standard-co*.)
(3) While print-gv is a utility for debugging guard violations, see guard-debug for a different sort of utility, which assists in debugging failed proofs arising from guard verification.

To see how one might use print-gv, consider the following definition.

(defun foo (x)
  (declare (xargs :guard (and (integerp x)
                              (posp (+ -2 x))
                              (posp (+ 3 x))
                              (posp (+ -4 x)))))
  x)

Now suppose we evaluate a call of foo and obtain a guard violation.

ACL2 !>(foo 1)


ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X),
which is (AND (INTEGERP X) (POSP (+ -2 X)) (POSP (+ 3 X)) (POSP (+ -4 X))),
is violated by the arguments in the call (FOO 1).
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.

Let us investigate this guard failure. First we use print-gv to obtain a form that represents our guard violation. Just for fun, we'll check that it indeed evaluates to nil.

ACL2 !>:print-gv

(FLET ((FOO{GUARD} (X)
                   (DECLARE (IGNORABLE X))
                   (AND (INTEGERP X)
                        (POSP (+ -2 X))
                        (POSP (+ 3 X))
                        (POSP (+ -4 X)))))
      (FOO{GUARD} 1))

ACL2 !>(FLET ((FOO{GUARD} (X)
                  (DECLARE (IGNORABLE X))
                  (AND (INTEGERP X)
                       (POSP (+ -2 X))
                       (POSP (+ 3 X))
                       (POSP (+ -4 X)))))
             (FOO{GUARD} 1))
NIL

This form doesn't tell us which of the four conjuncts actually evaluated to nil. We can fix that by using the :conjunct keyword argument.

ACL2 !>(print-gv :conjunct t)

Showing guard conjunct (#2 of 4) that evaluates to nil:

(FLET ((FOO{GUARD} (X) (POSP (+ -2 X)))) (FOO{GUARD} 1)).

ACL2 !>

But here's another way to analyze the guard failure. Let's change and to list in the result of :print-gv, to see which conjuncts are false. Of course, the user can massage the guard form in any way that might be helpful.

ACL2 !>(FLET ((FOO{GUARD} (X)
                  (DECLARE (IGNORABLE X))
                  (list (INTEGERP X)
                        (POSP (+ -2 X))
                        (POSP (+ 3 X))
                        (POSP (+ -4 X)))))
             (FOO{GUARD} 1))
(T NIL T NIL)
ACL2 !>

The NIL results show that the second and fourth conjuncts of the guard were false in our particular case.

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 !>

We conclude with an example that illustrates point (1) above, regarding the installation of the world that was in place at the time the guard violation took place. In the following, the progn call fails when the form (foo 3) causes a guard violation.

(progn (defn g (x) (consp x))
       (defun foo (x) (declare (xargs :guard (g x))) (car x))
       (value-triple (foo 3)))

We can then issue print-gv:

ACL2 !>:print-gv

(FLET ((FOO{GUARD} (X) (DECLARE (IGNORABLE X)) (G X))) (FOO{GUARD} 3))

ACL2 !>

However, if you try to evaluate this form, you will get an error because the function g is not currently defined. This problem can be solved by preceding :print-gv with :redo-flat, to re-run the events up to the one that failed; see redo-flat.

Subtopics

Set-print-gv-defaults: Set default keyword values for print-gv