debug a rewriting loop or stack overflow
Major Section:  OTHER

Stack overflows are most often caused by looping rewrite rules. In some Lisps, especially GCL, stack overflows often manifest themselves as segmentation faults, causing the entire ACL2 image to crash. Finding looping rewrite rules can be tricky, especially if you are using books supplied by other people.

A wonderful trick is the following. When there is a stack overflow during a proof, abort and then try it again after turning on rewrite stack monitoring with :brr t. When the stack overflows again, exit to raw Lisp. How you exit to raw Lisp depends on which Lisp you are using. In Allegro Common Lisp, for example, the stack overflow will leave you in an interactive break. You must exit this break, e.g., with :continue 1. This will leave you in the top-level ACL2 command loop. You must exit this environment with :q. That will leave you in raw Allegro.

After getting into raw Lisp, execute

  (cw-gstack *deep-gstack* state)
The loop in the rewriter will probably be evident!

If you are in GCL the stack overflow will probably cause a segmentation fault and abort the Lisp job. This makes it harder to debug but here is what you do. First, re-create the situation just prior to submitting the form that will cause the stack overflow. You can do this without suffering through all the proofs by using the :ld-skip-proofsp option of ld to reload your scripts. Before you submit the form that causes the stack overflow, exit the ACL2 command loop with :q. In raw GCL type

 (si::use-fast-links nil)
This will slow GCL down but make it detect and signal stack overflows rather than overwrite the system memory. Now reenter the ACL2 command loop with (lp).

Now carry on as described above, turning on rewrite stack monitoring with :brr t and provoking the stack overflow. When it occurs, you will be in an interactive break. Exit to raw Lisp with two successive :q's, one to get out of the error break and the next to get out of the top-level ACL2 command loop. Then in raw GCL execute the cw-gstack above.

Suggestion: Once you have found the loop and fixed it, you should execute the ACL2 command :brr nil, so that you don't slow down subsequent proof attempts. If you are in GCL, you should also get into raw Lisp and execute (si::use-fast-links t).