		Search-engine friendly clone of the ACL2 documentation.

Reference

Gl-aside

A debugging facility that is typically used for printing messages during GL symbolic execution.

Signature
(gl-aside form) → *

In the logic and during ordinary execution, (gl-aside form) is just an ordinary function that ignores its argument and returns nil. However, during GL symbolic execution it has a special meaning which is useful for printing debugging messages and doing other kinds of low-level hacking.

Note: gl-aside is fairly flexible but it can be tricky to use correctly. You should probably read this documentation carefully and also see the ``Tricks and Pitfalls'' section below!

Basic Example

Here is a typical usage of gl-aside:

(defun spec1 (x y)
  (b* ((sum (+ x y))
       (?msg (gl-aside (cw "Note: X is ~x0 and Y is ~x1.~%" x y))))
    sum))

During the normal execution of spec1, this Note will (of course) be printed: gl-aside is just an ordinary function, so ACL2 will (eagerly) evaluate the cw call before even invoking gl-aside.

What happens during symbolic execution? If we try to prove the following, simple GL theorem, e.g.,:

(def-gl-thm spec1-correct
  :hyp (and (unsigned-byte-p 3 x)
            (unsigned-byte-p 3 y))
  :concl (equal (spec1 x y)
                (+ x y))
  :g-bindings
  (auto-bindings (:nat x 3) (:nat y 3)))

then our Note will still be printed even though X and Y are symbolic-objects when spec1 is being executed! In particular, we will see, in gl-satlink-mode:

Note: X is (:G-INTEGER 0 1 2 NIL) and Y is
(:G-NUMBER 4 5 6 NIL).

The numbers 0-6 here are AIG variables. If we were instead in gl-bdd-mode, we would see large BDD variables (trees of T and NIL) here instead of these numbers.

The technical explanation of how this works is: when GL's symbolic interpreter encounters a call of (gl-aside form), it executes form inside a wormhole, with the variables bound to their symbolic versions.

Why do we even need this?

Couldn't we just write our spec without gl-aside? If we just wrote:

(defun spec2 (x y)
  (b* ((sum (+ x y))
       (?msg (cw "Note: X is ~x0 and Y is ~x1.~%" x y)))
    sum))

Then our Note would still get printed during normal execution. It would also get printed during some symbolic executions. In particular, if we know that X and Y are particular concrete values, then we will still see our note. For example, if we heavily constrain X and Y so to be constants:

(def-gl-thm spec2-correct-for-3-and-4
  :hyp (and (equal x 3)
            (equal y 4))
  :concl (equal (spec2 x y)
                (+ x y))
  :g-bindings
  (auto-bindings (:nat x 3) (:nat y 3)))

then we will indeed see our Note printed:

Note: X is 3 and Y is 4.

here, the cw form is being applied to all-constant arguments, so GL can simply evaluate it, causing the message to be printed. However, if we instead submit something more like our original theorem:

(def-gl-thm spec2-correct
  :hyp (and (unsigned-byte-p 3 x)
            (unsigned-byte-p 3 y))
  :concl (equal (spec2 x y)
                (+ x y))
  :g-bindings
  (auto-bindings (:nat x 3) (:nat y 3)))

then the Note is not printed. Why not? In this case, when GL's interpreter reaches the cw form, x and y are still symbolic objects, so it cannot simply concretely execute cw. Instead, GL symbolically executes the logical definition of cw—really fmt-to-comment-window. But in the logic, this function (of course) does not print anything, but instead just returns nil. At any rate, GL ends up binding msg to nil and nothing gets printed.

Tricks and Pitfalls

Pitfall: progn$ and its ilk

You probably never want to use prog2$ or progn$ to invoke a gl-aside. For instance, you do NOT want to do this:

(progn$ (gl-aside ...)      ;; WRONG
        sum)

Why not? During symbolic execution, GL just completely skips directly to the last form in the progn$, so it will never even see your gl-aside!

For similar reasons, you should also generally not use b* binders like -, &, and ?!, or the implicit progn$ forms that b* permits. For example:

(b* ((ans   (f x y ...))
     (?msg  (gl-aside ...))  ;; GOOD, bind to an ignored variable
     (?!msg (gl-aside ...))  ;; BAD, won't get evaluated
     (-     (gl-aside ...))  ;; BAD, won't get evaluated

     ((when condition)
      ;; implicit b* progn$:
      (gl-aside ...)         ;; BAD, won't get evaluated
      ans))

   ;; implicit b* progn$:
   (gl-aside ...)            ;; BAD, won't get evaluated
   ans)

Trick: print only during symbolic execution

The above spec1 function will print its Note during both regular execution and symbolic execution. It is also possible to use mbe to get a message that only prints during symbolic execution.

(defmacro gl-aside-symbolic (form)
  `(mbe :logic (gl-aside ,form)
        :exec nil))

(defun spec3 (x y)
  (declare (xargs :guard (and (natp x) (natp y))))
  (b* ((sum (+ x y))
       (?msg (gl-aside-symbolic (cw "Note: X is ~x0 and Y is ~x1.~%" x y))))
    sum))

(spec3 3 4)      ;; No Note is printed
7

(def-gl-thm spec3-correct ...) ;; Note is printed

Of course, this only works for guard-verified functions.

Definitions and Theorems

Function: gl-aside

(defun gl-aside (form)
  (declare (ignore form))
  (declare (xargs :guard t))
  (let ((__function__ 'gl-aside))
    (declare (ignorable __function__))
    nil))

Subtopics

Gl-aside-symbolic: Alternative to gl-aside that is only evaluated during GL symbolic execution.