NON-EXEC

Major Section:  ACL2-BUILT-INS

Non-exec is a macro such that logically, (non-exec x) is equal to x. However, the argument to a call of non-exec need not obey the usual syntactic restrictions for executable code, and indeed, evaluation of a call of non-exec will result in an error. Moreover, for any form occurring in the body of a function (see defun) that is a call of non-exec, no guard proof obligations are generated for that form.

The following example, although rather contrived, illustrates the use of non-exec. One can imagine a less contrived example that efficiently computes return values for a small number of fixed inputs and, for other inputs, returns something logically ``consistent'' with those return values.

(defun double (x)
  (case x
    (1 2)
    (2 4)
    (3 6)
    (otherwise (non-exec (* 2 x)))))

(verify-guards double)
(thm (equal (double x) (* 2 x)))

ACL2 !>(double 3)
6
ACL2 !>(double 10)


ACL2 Error in TOP-LEVEL:  ACL2 has been instructed to cause an error
because of an attempt to evaluate the following form (see :DOC non-
exec):

  (* 2 X).

To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

ACL2 !>

During proofs, the error is silent; it is ``caught'' by the proof mechanism and generally results in the introduction of a call of hide during a proof.

Also see defun-nx for a utility that makes every call of a function non-executable, rather than a specified form. The following examples contrast non-exec with defun-nx, in particular illustratating the role of non-exec in avoiding guard proof obligations.

; Guard verification fails:
(defun-nx f1 (x)
  (declare (xargs :guard t))
  (car x))

; Guard verification succeeds after changing the guard above:
(defun-nx f1 (x)
  (declare (xargs :guard (consp x)))
  (car x))

; Guard verification succeeds:
(defun f2 (x)
  (declare (xargs :guard t))
  (non-exec (car x)))

; Evaluating (g1) prints "Hello" before signaling an error.
(defun g1 ()
  (f1 (cw "Hello")))

; Evaluating (g2) does not print before signaling an error.
(defun g2 ()
  (non-exec (cw "Hello")))

; Evaluating (h1) gives a guard violation for taking reciprocal of 0.
(defun h1 ()
  (f1 (/ 1 0)))

; Evaluating (h2) does not take a reciprocal, hence there is no guard
; violation for that; we just get the error expected from using non-exec.
(defun h2 ()
  (non-exec (/ 0)))