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)))))We can prove that

`double`

is compliant with Common Lisp (see guard) and
that it always computes `(* 2 x)`

.
(verify-guards double) (thm (equal (double x) (* 2 x)))We can evaluate double on the specified arguments. But a call of

`non-exec`

results in an error message that reports the form that was
supplied to `non-exec`

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