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

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.

Output from `trace$` normally goes to the screen, i.e., to `standard-co`. But it can be redirected to a file; see open-trace-file.

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

Note that when

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,

We begin by illustrating the simplest sort of trace spec: a function
symbol. For example, the form

(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

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

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 `mv` return is used, as illustrated in the
following example, after defining:

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

For each of these three options, the value is a
(user-level) term, except that for

NOTE. The symbols mentioned below, for exampleARGLIST , 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 `mv` is not used in the return). Also for `mv` case and otherwise to the single value returned.
So in the `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).

Now suppose

Note that if the function has a formal named

As mentioned above, for each of

Finally we discuss the case that the

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

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

The tracing of

ACL2's `mv`. If you trace a function that was
not defined inside the ACL2 loop (hence you are using the

Note that even supplying a

A useful option can be to supply a definition as the value of `defun` form, but without the leading

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

A special value,

A second special value for

Note that if

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

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

The default value for this advanced option is `stobj-let`, or
with the aforementioned large structures other than the logical world.

If

Note that by ``native Lisp trace'' we mean the currently installed

It is important to understand that if `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.

By default, a new definition installed by

A special value for

- 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 variablesprogram-fns-with-raw-code orlogic-fns-with-raw-code ; - for
`memoize`d functions.

The legal values for

(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

(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

(4) For a wormhole such as the break-rewrite loop, all calls
of `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