TRACE$.html -- ACL2 Version 6.2

TRACE$

trace function evaluations

Major Section:  TRACE

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 (http://acl2s.ccs.neu.edu/acl2s/doc/), 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 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 :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 so-called ``*1*'' functions (sometimes called ``executable counterpart functions'' or ``logic functions'') are called but the corresponding raw Lisp functions are not; but after guard verification of f, the raw Lisp counterpart of 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 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.

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). 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).

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 so-called ``executable counterpart'' of a function (sometimes referred to as the ``*1* function'', for evaluation in the ACL2 loop; see guards for related discussion) 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: specifically, with (format *trace-output* "s%" x), where x is the value to be printed.

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 contants, enabled structures, and event and command index structures). 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. 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:

o for functions whose definitions are built into ACL2;
o 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;
o (`HONS' extension only; see hons-and-memoization) for memoized functions.

The legal values for :notinline are t (the default for other than the cases displayed above), nil, and :fncall. (Except: For the 'HONS' extension, only :fncall is legal.)

Remarks.

(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 function or its in-the-logic (so-called `*1*') counterpart.

(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$.