		Search-engine friendly clone of the ACL2 documentation.

Fgl-debugging

Tools for debugging FGL failures

In this topic we list some techniques for debugging FGL failures.

Examining the Stack

FGL keeps almost all of the state of its interpreter inside its interpreter state stobj interp-st. In particular, it keeps a stack containing variable bindings, scratch objects, and debugging information inside this stobj. Examining this stack to see where FGL ran into an error or where it's spending time is one of the best tools for debugging FGL problems.

The stack is contained in a nested stobj inside the interpreter state, but it can be dumped into a regular ACL2 object using the function (fgl::interp-st-extract-stack fgl::interp-st). Usually when FGL encounters an error it will also save the stack into a state global (@ :fgl-interp-error-debug-stack). The FGL clause processor is typically run on the live interp-st stobj, so if the clause processor is interrupted during a proof the stack can be retrieved from that stobj, either afterward from the ACL2 loop or within the raw Lisp break:

;; From within the ACL2 loop, save the stack into a constant (using std/util/defconsts.lisp):
(defconsts *my-stack* (fgl::interp-st-extract-stack fgl::interp-st))
;; Or put it in a state global, accessed as (@ :my-stack):
(f-put-global ':my-stack (fgl::interp-st-extract-stack fgl::interp-st) state)

;; From within a raw Lisp break, save the stack as a defparameter:
(defparameter *my-stack* (fgl::interp-st-extract-stack (cdr (assoc 'fgl::interp-st *user-stobj-alist*)))

Note: be sure NOT to do the latter when in a raw Lisp break resulting from a stack overflow! It may cause your Lisp to crash completely.

The stack object's type is major-stack, which is documented under fgl-stack. Essentially it is a nonempty list of major-frame objects representing scopes such as function calls and rewrite rules. Each frame contains some variable bindings and debug info identifying what rule application that frame represents, as well as a minor stack representing a nesting of lambdas.

A useful tool for examining a stack object is (fgl::major-stack->debugframes my-stack), which returns the debug info from each of the major frames paired with its index. Often you can find the frames you're most interested in by looking at the debug info, and then examine those frames closer by indexing into the stack with nth etc.

It may be useful to set a lower recursion limit for the FGL interpreter. The default is 10000, but it may help to catch runaway rule applications to limit it to 1000 or less. This can be adjusted by setting the state global :fgl-reclimit.

Tracing Rewrite Rules

Most of the work of FGL is done by rewrite rules -- even the expansion of function definitions is just treated as an application of a rewrite rule. Tracing rewrites can help debug problems due to rule applications unexpectedly failing or recurring out of control, etc. See fgl-rewrite-tracing.

Profiling

FGL provides accumulated persistence-style profiling of rewrite rules, concrete executions, and FGL primitive executions. These may help debug performance problems by showing which rules are invoked many times and which rules cause other rules to be invoked many times. As with ACL2's accumulated persistence, we count two numbers for each rule: tries, which simply measures the number of times the rule is attempted, and frames, which measures how many tries total, including other rules, happen during a top-level attempted application of the rule.

Subtopics

Fgl-support-vars: Display the list of objects corresponding to the Boolean variables used in the symbolic representation of an object
Fgl-gatecount: Display how many AIG gates are used in the symbolic representation of an object