A debugging facility that is typically used for printing messages during GL symbolic execution.
(gl-aside form) → *
In the logic and during ordinary execution, (gl-aside form) is
just an ordinary function that ignores its argument and returns
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
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
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
Couldn't we just write our spec without
(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
(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
You probably never want to use prog2$ or progn$ to
(progn$ (gl-aside ...) ;; WRONG sum)
Why not? During symbolic execution, GL just completely skips directly to
the last form in the
For similar reasons, you should also generally not use b* binders
(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)
(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.
(defun gl-aside (form) (declare (ignore form)) (declare (xargs :guard t)) (let ((__function__ 'gl-aside)) (declare (ignorable __function__)) nil))