Backtraces
Accessing a backtrace during FGL rewriting
The following utilities allow FGL to retrieve backtrace data while
rewriting. These can be used to help debug code proofs or FGL rewriter
problems.
Specifying backtrace data to collect
- backtrace-spec is the data structure specifying an FGL rule to
include in the backtrace and which variables of that rule to include. A list
of these (a backtrace-speclist) are given to the backtrace collection
functions to get data from multiple rules.
- function-rules-to-backtrace-spec collects backtrace specs for all
FGL rewrite rules targeting a particular function.
Collecting a backtrace of symbolic values
Evaluating a backtrace under a satisfying assignment
A backtrace is a data structure with symbolic objects in it. Sometimes it is
useful to evaluate this object to get concrete values for all of the symbolic
objects.
- backtrace-to-obj and backtrace-frame-to-obj construct proper
symbolic objects from (respectively) a backtrace or backtrace-frame. It's
likely that one of these already is a proper symbolic object, but these functions
make sure of it.
- fgl-counterexamples for utilities that can be used to derive a
counterexample and evaluate the backtrace under it.
Subtopics
- Interp-st-stack-backtrace
- Collect a backtrace object from the FGL rewriter stack, given a list of rule specifications
- Function-rules-to-backtrace-spec
- Get a set of FGL backtrace specifiers for all FGL rules targeting a function symbol
