Trace$
Trace function evaluations
Examples:
(trace$ foo bar) ; trace foo and bar
(trace$) ; return current trace info (no new tracing specified)
(trace$ (foo :entry ; trace foo, printing first actual parameter upon entry
(car arglist)))
(trace$ (foo :exit ; trace foo, using fmt to print upon exit
(:fmt (msg "Exiting FOO with ~x0"
value))))
(trace$ (foo :native t))
General Forms:
(trace$ spec1 spec2 ... specn) ; n >= 1
(trace$)
where the speci are trace specs, as described below.
Trace$ installs alternate code for the indicated functions that prints
information upon entry to, and exit from, calls of the functions. For an
alternate tracing utility used for educational purposes in ACL2s, see community book
books/misc/trace-star.lisp.
From a logical perspective all trace printing is a fiction. (But see trace! for a way to get around this and modify state.) For a related
fiction, see cw. (Trace$) returns the list of currently-active
trace specs, while the application of trace$ to at least one argument
returns the list of its arguments that are successfully acted on.
Output from trace$ normally goes to the screen, i.e., to standard-co. But it can be redirected to a file; see trace-co.
See untrace$ for how to undo the effect of trace$. Also see
trace for mention of modifications made to raw Lisp trace, which is
accessible (as described below) using the :native keyword.
Note that when trace$ is applied to a function without option
:native, that function's declarations and documentation are
discarded.
Next, we introduce tracing with some examples. After that, we provide
reference documentation for individual trace options allowed in a trace spec.
Note that although our example focuses on user-defined functions, trace$
can also be applied to built-in functions, though perhaps only system hackers
should take advantage of this observation.
We begin by illustrating the simplest sort of trace spec: a function
symbol. For example, the form (trace$ foo bar) directs the tracing of
functions foo and bar by virtue of the two trace specs foo and
bar. We can see tracing in action by first defining:
(defun f (x)
(cons x x))
(defun g (x)
(list (f x) 3))
The following log then illustrates tracing of these two functions. Notice
that before guards have been verified, the ``executable-counterpart
functions'' are called but the corresponding submitted functions are
not (see evaluation for relevant background); but after guard
verification of f, the submitted function for f is indeed called.
(See guard and see guard-evaluation-examples-log.)
ACL2 !>(trace$ f g)
((F) (G))
ACL2 !>(g 7)
1> (ACL2_*1*_ACL2::G 7)
2> (ACL2_*1*_ACL2::F 7)
<2 (ACL2_*1*_ACL2::F (7 . 7))
<1 (ACL2_*1*_ACL2::G ((7 . 7) 3))
((7 . 7) 3)
ACL2 !>(verify-guards f)
Computing the guard conjecture for F....
The guard conjecture for F is trivial to prove. F is compliant with
Common Lisp.
Summary
Form: ( VERIFY-GUARDS F)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
F
ACL2 !>(g 7)
1> (ACL2_*1*_ACL2::G 7)
2> (ACL2_*1*_ACL2::F 7)
3> (F 7)
<3 (F (7 . 7))
<2 (ACL2_*1*_ACL2::F (7 . 7))
<1 (ACL2_*1*_ACL2::G ((7 . 7) 3))
((7 . 7) 3)
ACL2 !>
The following example introduces trace specs other than function symbols.
Consider the following definition.
(defun fact (n)
(declare (xargs :guard (natp n)))
(if (zp n)
1
(* n (fact (1- n)))))
The following log illustrates the use of trace options :cond
(condition for entering trace), :entry (what to print on entry), and
:exit (what to print on exit). The reason for two calls on argument 4 is
that we are seeing such calls for the executable-counterpart of fact and
also its raw Lisp function.
ACL2 !>(trace$ (fact :cond (evenp (car arglist))
:entry (cons 'factorial-call arglist)
:exit (car values)))
((FACT :COND (EVENP (CAR ARGLIST))
:ENTRY (CONS 'FACTORIAL-CALL ARGLIST)
:EXIT (CAR VALUES)))
ACL2 !>(fact 4)
1> (FACTORIAL-CALL 4)
2> (FACTORIAL-CALL 4)
3> (FACTORIAL-CALL 2)
4> (FACTORIAL-CALL 0)
<4 1
<3 2
<2 24
<1 24
24
ACL2 !>
Notice that VALUES above is the list of all values returned, which is
a one-element list unless mv return is used, as illustrated in the
following example, after defining: (defun two-vals (x) (mv x 7)).
ACL2 !>(trace$ two-vals)
((TWO-VALS))
ACL2 !>(two-vals 3)
1> (ACL2_*1*_ACL2::TWO-VALS 3)
<1 (ACL2_*1*_ACL2::TWO-VALS 3 7)
(3 7)
ACL2 !>(verify-guards two-vals)
Computing the guard conjecture for TWO-VALS....
The guard conjecture for TWO-VALS is trivial to prove, given the :executable-
counterpart of CONS. TWO-VALS is compliant with Common Lisp.
Summary
Form: ( VERIFY-GUARDS TWO-VALS)
Rules: ((:EXECUTABLE-COUNTERPART CONS))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TWO-VALS
ACL2 !>(two-vals 3)
1> (ACL2_*1*_ACL2::TWO-VALS 3)
2> (TWO-VALS 3)
<2 (TWO-VALS 3 7)
<1 (ACL2_*1*_ACL2::TWO-VALS 3 7)
(3 7)
ACL2 !>
We now document all of the options that may appear in a trace spec. A
trace spec with options is of the form
(fn :kwd1 val1 :kwd2 val2 ... :kwdn valn)
and here we document each legal keyword :kwdi and corresponding
expected value vali. Note that trace$ is intended primarily for
functions defined in the ACL2 command loop (see lp). If you want to
trace a function that is defined in raw Lisp, then you can use option
:native (see below), but then many other trace$ options will not be
available to you: all of them except :multiplicity and :native
itself will be passed directly to the trace utility of the underlying
Common Lisp.
:COND, :ENTRY, and :EXIT
Introduction
For each of these three options, the value is a
(user-level) term, except that for :entry and :exit the value can be
of the form (:fmt u) or (:fmt! u), where u is a user-level
term. We skip these two latter cases for now and return to them later. Then
the indicated term is evaluated as indicated in the next paragraph, and if the
:cond term is omitted or evaluates to non-nil, then the value of the
:entry term is printed on entry and the value of the :exit term is
printed on exit. By default, where :entry is omitted or is specified as
nil, the value printed for :entry is the list obtained by consing
the calling function symbol onto the list of actual parameters: in the
notation described below, this is (cons TRACED-FN ARGLIST). Similarly,
the default for printing at the exit of the function call, i.e. where
:exit is omitted or is specified as nil, is (cons TRACED-FN
VALUES) where VALUES is the list of values returned as described
below.
Available Variables
NOTE. The symbols mentioned below, for example ARGLIST, are
all in the "ACL2" package. If you are in another package you may need
an "ACL2::" package prefix, e.g., ACL2::ARGLIST.
In the evaluations of the term described below upon a call of fn, each
formal parameter of the definition of fn will be bound to the
corresponding actual of the call, the variable ARGLIST will be bound to
the list of actuals, and the variable TRACED-FN will be bound to the
function being called (either fn or its executable-counterpart function;
see above). Additionally in the case of :exit, the variable VALUES
will be bound to the multiple values returned (thus, a one-element list if
mv is not used in the return). Also for :exit, we bind
VALUE to the logical value returned, i.e., to the suitable list of values
returned in the mv case and otherwise to the single value returned.
So in the mv case, VALUE is the same as VALUES, and otherwise
VALUE is (car VALUES). Finally, the variable TRACE-LEVEL will
be bound to the level, or depth, of tracing; that is, the number printed at
entry and exit (e.g., 3 in `3>' and `<3'). Other than these
variables and state, no other variable may occur in the term, whose
value must be a single non-stobj value, unless there is an active
trust tag (see defttag).
Basic Options
Now suppose fn is called. First: If :cond is supplied and the
result of evaluating the :cond term is nil, then no tracing is done.
Otherwise tracing proceeds as follows. First the :entry form is
evaluated, and the result is printed. Then the call of fn is evaluated.
Finally the :exit term is evaluated and the result is printed. As
indicated above, the default for the :entry term if omitted or explicitly
nil is (cons TRACED-FN ARGLIST), and the default for the :exit
term if omitted or explicitly nil is (cons TRACED-FN VALUES).
Note that if the function has a formal named ARGLIST, then
ARGLIST will nevertheless refer to the entire list of formals, not the
single formal named ARGLIST; similarly for TRACED-FN, and
additionally for VALUE and VALUES in the case of :exit.
As mentioned above, for each of :entry and :exit, a value of
nil specifies the default behavior. If you really want a value of
nil, use a non-nil form that evaluates to nil, for example
(car nil) or 'nil. However, for :cond a value of nil
means what it says: do not evaluate the :entry or :exit forms.
Finally we discuss the case that the :entry or :exit term is of
the form (:fmt u) or (:fmt! u). In these cases, the term u is
evaluated as described above to produce a value, say msg, but instead of
printing msg directly, ACL2 calls fmt1 using the string "~@0"
and the alist that binds just character #\0 to msg. The following
example illustrates this point, where fact is defined as above. Also see
fmt. Note that (msg string . vals) produces a value suitable for
a "~@" directive to the fmt family of print functions.
ACL2 !>(trace$
(fact
:entry (:fmt (msg "Tracing ~x0 on ~x1" traced-fn arglist))
:exit (car values)))
((FACT :ENTRY (:FMT (MSG "Tracing ~x0 on ~x1" TRACED-FN ARGLIST))
:EXIT (CAR VALUES)))
ACL2 !>(fact 3)
1> Tracing ACL2_*1*_ACL2::FACT on (3)
2> Tracing FACT on (3)
3> Tracing FACT on (2)
4> Tracing FACT on (1)
5> Tracing FACT on (0)
<5 1
<4 1
<3 2
<2 6
<1 6
6
ACL2 !>
If :fmt! is used instead of :fmt, then indentation as is the
prefix string, "n> " or "<n ". The following example
illustrates the use of :fmt!.
ACL2 !>(trace$
(fact
:entry (:fmt! (msg "Tracing ~x0 on ~x1" traced-fn arglist))
:exit (:fmt! (msg "From input ~x0: ~x1"
(car arglist) (car values)))))
((FACT :ENTRY (:FMT! (MSG "Tracing ~x0 on ~x1" TRACED-FN ARGLIST))
:EXIT (:FMT! (MSG "From input ~x0: ~x1" (CAR ARGLIST)
(CAR VALUES)))))
ACL2 !>(fact 3)
Tracing ACL2_*1*_ACL2::FACT on (3)
Tracing FACT on (3)
Tracing FACT on (2)
Tracing FACT on (1)
Tracing FACT on (0)
From input 0: 1
From input 1: 1
From input 2: 2
From input 3: 6
From input 3: 6
6
ACL2 !>
Here is the same example, with user-managed indentation.
ACL2 !>(trace$
(fact
:entry (:fmt! (msg "~t0Tracing ~x1 on ~x2"
(+ 3 (* 2 trace-level))
traced-fn arglist))
:exit (:fmt! (msg "~t0From input ~x1: ~x2"
(1+ (* 2 trace-level))
(car arglist) (car values)))))
((FACT :ENTRY (:FMT! (MSG "~t0Tracing ~x1 on ~x2"
(+ 3 (* 2 TRACE-LEVEL))
TRACED-FN ARGLIST))
:EXIT (:FMT! (MSG "~t0From input ~x1: ~x2"
(1+ (* 2 TRACE-LEVEL))
(CAR ARGLIST)
(CAR VALUES)))))
ACL2 !>(fact 3)
Tracing ACL2_*1*_ACL2::FACT on (3)
Tracing FACT on (3)
Tracing FACT on (2)
Tracing FACT on (1)
Tracing FACT on (0)
From input 0: 1
From input 1: 1
From input 2: 2
From input 3: 6
From input 3: 6
6
ACL2 !>
Advanced Options (alphabetical list)
:COMPILE
The tracing of fn installs a substitute definition of fn that
prints trace information. If the :compile option is omitted or has value
:same, then the new definition will be compiled if and only if the
existing definition is already compiled. Otherwise, the new definition will
be compiled exactly when the value of :compile is not nil.
:DEF, :MULTIPLICITY
ACL2's trace$ mechanism often needs to know the number of outputs of a
traced function, in the sense of mv. If you trace a function that was
not defined inside the ACL2 loop (hence you are using the :native
option), or if you provide an alternative definition using option :def
(see below) and the new definition changes the number of values returned, then
a natural number value for :multiplicity informs the trace utility of the
number of expected outputs of the function being traced. In the case that
:native is supplied, the effect of a non-nil :multiplicity
value depends on the host Lisp. In the case of Lisps for which ACL2 uses the
built-in Lisp mechanism for returning multiple values (see mv), which
are CCL and threaded SBCL as of June, 2010, :multiplicity is not needed
and is ignored with :native t. For GCL and Allegro CL,
:multiplicity is used to generate a suitable :exit form if the
:exit keyword was not already supplied. For the other Lisps, the
:multiplicity value is treated essentially as 1 whether it is supplied or
not, because we do not know how to pass suitable information based on this
value to the host Lisp's built-in tracing mechanism.
Note that even supplying a :multiplicity option does not change the
meaning of the variable values. See the discussion of :native
below.
A useful option can be to supply a definition as the value of :def.
(Again, note that if :native is used, then all options other than
:multiplicity are passed directly to the underlying Lisp; in particular,
:def will have no effect with :native except in the unlikely case
that the raw Lisp provides some sort of support for :def.) Note that
this definition should be like a defun form, but without the leading
defun symbol; and it should define the function symbol being traced, with
the same formal parameter list. However, tracing of the
``executable-counterpart'' of a function (see evaluation is not
sensitive to the :def option; rather, if a function has an
executable-counterpart then that executable-counterpart is traced.
:EVISC-TUPLE
The printing described above is, by default, done using the current default
trace evisc-tuple, which can be set using set-trace-evisc-tuple (for
the shape of this tuple, see evisc-tuple); see set-trace-evisc-tuple. This tuple is based by default on the raw Lisp
variables *print-level* and *print-length*, and will hide the ACL2
world and handle stobjs appropriately. You may override this
default by supplying an evisc tuple with the :evisc-tuple argument in
your trace spec. Be careful to supply a valid evisc-tuple, or you may get a
raw Lisp error!
A special value, :print, is useful if you are doing system hacking
that can produce objects that are not valid ACL2 objects, such as raw Lisp
arrays or objects in supporting packages not visible in the ACL2
read-eval-print loop. If you supply :evisc-tuple :print, then the
printing described above will be done with raw Lisp printing rather than ACL2
printing. Note that stobjs will be printed as vectors (rather than
their usual hiding with symbols such as <st>) when using
:evisc-tuple :print, but other structures will still be hidden unless
:hide nil is supplied.
A second special value for :evisc-tuple, :no-print, avoids
printing the values of the :entry and :exit forms (or their
defaults, if not specified). This option is of use for side effects; for an
example see community book books/misc/wet.lisp.
Note that if :evisc-tuple X is supplied, then the form X will be
evaluated before the function body is entered. You can thus pull some tricks
to print extra information before the :entry form is evaluated, for
example as follows for a factorial function, fact.
ACL2 !>(trace$ (fact :evisc-tuple
(prog2$ (cw "~|**** HERE IS CW ****~|")
nil)))
((FACT :EVISC-TUPLE (PROG2$ (CW "~|**** HERE IS CW ****~|")
NIL)))
ACL2 !>(fact 3)
**** HERE IS CW ****
1> (ACL2_*1*_ACL2::FACT 3)
**** HERE IS CW ****
2> (ACL2_*1*_ACL2::FACT 2)
**** HERE IS CW ****
3> (ACL2_*1*_ACL2::FACT 1)
**** HERE IS CW ****
4> (ACL2_*1*_ACL2::FACT 0)
<4 (ACL2_*1*_ACL2::FACT 1)
<3 (ACL2_*1*_ACL2::FACT 1)
<2 (ACL2_*1*_ACL2::FACT 2)
<1 (ACL2_*1*_ACL2::FACT 6)
6
ACL2 !>
:FORMALS
Normally ACL2 can figure out the formals for a given function. This is
always the case for functions defined in the ACL2 command loop and when option
:def is supplied. If neither of these cases applies then you can still
trace a function (even without using the :native option) by supplying
option :notinline :fncall, but you will still need to supply the list of
formal parameters. The value of the :formals option should be the list
of formals in this case.
:HIDE
The default value for this advanced option is t, which causes stobjs and the logical world to be printed as single symbols, along
with certain large structures of interest to developers (rewrite constants,
enabled structures, and event and command index structures).
(For an exception regarding stobjs, see the discussion of :evisc-tuple
:print above.) If however the value nil is supplied, then this default
behavior is defeated. In that case, you can still arrange to print the
logical world as a symbol and to print stobjs without breaking the
trace printing: see set-trace-evisc-tuple for how to do this globally,
or similarly use the :evisc-tuple option to trace$ to do this with a
single trace spec. Note however that with value nil specified for
:hide, such use of an evisc-tuple will not deal properly with local
stobjs (see with-local-stobj) or stobjs bound by stobj-let, or
with the aforementioned large structures other than the logical world.
:NATIVE
If :native is supplied with a non-nil value, then the trace spec
is passed to the native Lisp trace (after removing the :native option).
A trust tag (see defttag) is required in order to use this option,
because no syntactic check is made on the :cond, :entry, or
:exit forms — arbitrary raw Lisp may occur in them!
Note that by ``native Lisp trace'' we mean the currently installed
trace. As discussed briefly elsewhere (see trace), ACL2 has
modified that trace to be more useful if the underlying host Lisp is GCL,
Allegro CL, or CCL (OpenMCL). If you need the original trace utility supplied
for those Lisps, quit the ACL2 loop with :q and call old-trace and
old-untrace in raw Lisp where you would otherwise call trace and
untrace. Note that the original trace utility supplied with a given Lisp
will not hide the ACL2 logical world or give special treatment to stobjs.
It is important to understand that if :native t is specified, then all
other options are interpreted by the native Lisp trace. For example, that
trace probably has no understanding of the use of :fmt described above
for :entry or :exit. Indeed, the native trace may not even accept
any of :cond, :entry or :exit, let alone any of the advanced
options! Moreover, if :native t is specified, then even a
:multiplicity option does not provide the meaning of the variable
values that one might desire. In GCL for example, in the case of an
mv return of a function defined only in raw Lisp (not in ACL2), this
variable will be bound to a list containing only the first result.
:NOTINLINE
By default, a new definition installed by trace$ will include a
notinline declaration so that recursive calls will always be traced.
(But see Remark (0) below for an exception involving invariant-risk.)
To avoid this declaration, supply value nil.
A special value for :notinline, :fncall, will cause the traced
function to call its original definition. Without this special value, the new
installed definition for the traced function will include the body of the
original definition. This :fncall behavior is the default only in the
following cases:
- for functions whose definitions are built into ACL2;
- for functions that have been added (using a trust tag, an advanced
feature, so most users can probably ignore this case) to either of the state global variables program-fns-with-raw-code or
logic-fns-with-raw-code;
- for memoized functions.
The legal values for :notinline are t (the default for other than
the cases displayed above), nil, and :fncall.
Remarks
(0) For a :program mode function with invariant-risk,
recursive calls are never traced. To see these recursive calls, use one of
the two methods to defeat invariant-risk checking; see invariant-risk. (Implementation note: This behavior on recursive calls is a
consequence of how ACL2 defines the executable-counterpart — also known
as the ``*1* function'' (see evaluation) — to call a local
function to do the computation.)
(1) If some of the given trace specs have errors, then trace$ will
generally print error messages for those but will still process those that do
not have errors. The value returned will indicate the trace specs that were
processed successfully.
(2) If you certify or include a book that redundantly defines a function
that is currently traced, then tracing behavior may disappear if a compiled
definition is installed for the submitted function or its
executable-counterpart (see evaluation for relevant background).
(3) Some predefined functions are called during tracing. In order to avoid
infinite loops, such calls of traced predefined functions will be made using
the original predefined functions, not using their code installed by
trace$.
(4) For a wormhole such as the break-rewrite loop, all calls
of trace$ and untrace$ inside that wormhole are undone upon exit
from the wormhole. In particular, if you trace or untrace a function during a
brr break, then effects of that trace or untrace will disappear when
you proceed using a keyword such as :eval or :go.
Subtopics
- Trace*
- Trace* is a beginner-friendly variant of trace$, the ACL2
tracing utility.
