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)))
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
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
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))