		Search-engine friendly clone of the ACL2 documentation.

Trace

Trace!

Trace the indicated functions after creating an active trust tag

Example:
(trace! (fact :native t :entry *foo*))

General Form:
(trace! spec1 ... specn)

where the speci are suitable arguments to trace$.

See trace$ for a way to trace function calls. Some calls of trace$ are potentially dangerous and thus require a trust tag (see defttag). But it can be a nuisance to call defttag explicitly, so the trace! macro is provided in order to avoid the need to do that: trace! automatically defines a (temporary) trust tag.

See untrace$ for how to undo the effect of trace!.

The evaluation of a trace! form causes temporary creation of an active trust tag, :trace!, followed by the corresponding trace$ form. The trust tag will disappear when the call to trace! completes. Even though trace! will remove its temporary ttag, it will still print a ``TTAG NOTE'', which indicates that the session is suspect. See defttag and see ttags-seen for further remarks on this issue.

Because of the active trust tag, it is possible to do things with trace! that are useful but without logical justification. Below is an example of how to use trace! to cause a function call to change state, even though the function does not take state as a parameter. Note: It may be helpful to see evaluation in order to understand the package prefix "ACL2_*1*_ACL2" displayed below.

ACL2 !>(defun fact (n)
         (declare (xargs :guard (natp n) :verify-guards nil))
         (if (zp n)
             1
           (* n (fact (1- n)))))

The admission of FACT is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT N).  We observe that the type of FACT is described by the
theorem (AND (INTEGERP (FACT N)) (< 0 (FACT N))).  We used the :compound-
recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning.

Summary
Form:  ( DEFUN FACT ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 !>(defun update-foo (n value state)
         (declare (xargs :stobjs state :verify-guards nil))
         (assign foo (cons (cons n value) (@ foo))))

Since UPDATE-FOO is non-recursive, its admission is trivial.  We observe
that the type of UPDATE-FOO is described by the theorem
(AND (CONSP (UPDATE-FOO N VALUE STATE))
     (TRUE-LISTP (UPDATE-FOO N VALUE STATE))).
We used primitive type reasoning.

(UPDATE-FOO * * STATE) => (MV * * STATE).

Summary
Form:  ( DEFUN UPDATE-FOO ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 UPDATE-FOO
ACL2 !>(trace! (fact :exit (update-foo n value state)))

TTAG NOTE: Adding ttag :TRACE! from the top level loop.
 ((FACT :EXIT (UPDATE-FOO N VALUE STATE)))
ACL2 !>(assign foo nil)
 NIL
ACL2 !>(fact 7)
1> (ACL2_*1*_ACL2::FACT 7)
  2> (ACL2_*1*_ACL2::FACT 6)
    3> (ACL2_*1*_ACL2::FACT 5)
      4> (ACL2_*1*_ACL2::FACT 4)
        5> (ACL2_*1*_ACL2::FACT 3)
          6> (ACL2_*1*_ACL2::FACT 2)
            7> (ACL2_*1*_ACL2::FACT 1)
              8> (ACL2_*1*_ACL2::FACT 0)
              <8 NIL
            <7 NIL
          <6 NIL
        <5 NIL
      <4 NIL
    <3 NIL
  <2 NIL
<1 NIL
5040
ACL2 !>(@ foo)
((7 . 5040)
 (6 . 720)
 (5 . 120)
 (4 . 24)
 (3 . 6)
 (2 . 2)
 (1 . 1)
 (0 . 1))
ACL2 !>(verify-guards fact)

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound-
recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER,
primitive type reasoning and the :type-prescription rule FACT.  FACT
is compliant with Common Lisp.

Summary
Form:  ( VERIFY-GUARDS FACT)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION FACT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FACT
ACL2 !>(assign foo nil)
 NIL
ACL2 !>(fact 7)
1> (ACL2_*1*_ACL2::FACT 7)
  2> (FACT 7)
    3> (FACT 6)
      4> (FACT 5)
        5> (FACT 4)
          6> (FACT 3)
            7> (FACT 2)
              8> (FACT 1)
                9> (FACT 0)
                <9 NIL
              <8 NIL
            <7 NIL
          <6 NIL
        <5 NIL
      <4 NIL
    <3 NIL
  <2 NIL
<1 NIL
5040
ACL2 !>(@ foo)
((7 . 5040)
 (7 . 5040)
 (6 . 720)
 (5 . 120)
 (4 . 24)
 (3 . 6)
 (2 . 2)
 (1 . 1)
 (0 . 1))
ACL2 !>(trace! (fact :exit (progn (update-foo n value state)
                                  (cons traced-fn values))))

TTAG NOTE: Adding ttag :TRACE! from the top level loop.
 ((FACT :EXIT (PROGN (UPDATE-FOO N VALUE STATE)
                     (CONS TRACED-FN VALUES))))
ACL2 !>(assign foo nil)
 NIL
ACL2 !>(fact 7)
1> (ACL2_*1*_ACL2::FACT 7)
  2> (FACT 7)
    3> (FACT 6)
      4> (FACT 5)
        5> (FACT 4)
          6> (FACT 3)
            7> (FACT 2)
              8> (FACT 1)
                9> (FACT 0)
                <9 (FACT 1)
              <8 (FACT 1)
            <7 (FACT 2)
          <6 (FACT 6)
        <5 (FACT 24)
      <4 (FACT 120)
    <3 (FACT 720)
  <2 (FACT 5040)
<1 (ACL2_*1*_ACL2::FACT 5040)
5040
ACL2 !>(@ foo)
((7 . 5040)
 (7 . 5040)
 (6 . 720)
 (5 . 120)
 (4 . 24)
 (3 . 6)
 (2 . 2)
 (1 . 1)
 (0 . 1))
ACL2 !>

Finally, we remark that using trace! can cause errors in situations where tracing is automatically suspended and re-introduced. This is likely to be a rare occurrence, but consider the following example.

(trace! (lexorder :native t :multiplicity 1))
(certify-book "foo" 0 t)

If the certify-book causes compilation, you may see an error such as the following.

ACL2 Error in (CERTIFY-BOOK "foo" ...):  The keyword :NATIVE cannot
be used in a trace spec unless there is an active trust tag.  The trace
spec (LEXORDER :NATIVE T :MULTIPLICITY 1) is thus illegal.  Consider
using trace! instead.  The complete list of keywords that require a
trust tag for use in a trace spec is: (:NATIVE :DEF :MULTIPLICITY).

This error is harmless. The function will appear, when calling (trace$), to remain traced, but in fact there will be no tracing behavior, so you may want to call untrace$ on the function symbol in question.