		Search-engine friendly clone of the ACL2 documentation.

Unsound-eval

A somewhat robust evaluator.

Signature
(unsound-eval sexpr &key (state 'state)) → (mv errmsg values state)
Arguments: sexpr — An s-expression to evaluate, typically this should be a well-formed ACL2 form without guard violations, etc. It may mention stobjs.
Returns: errmsg — An error msg on failure, or nil on success. Note that this message is likely to be very terse/unhelpful when evaluating sexpr causes any ACL2 error.; values — The list of return values from evaluating sexpr, with stobjs elided with their names.; state — Type (state-p1 state), given (state-p1 state).

In the logic, this is implemented as oracle reads, so you can't prove anything about what it returns. Even so, it is generally unsound since it lets you to modify state and other stobjs without accounting for how they have been modified.

In the execution, we basically call ACL2's trans-eval function (technically: trans-eval-no-warning). But we wrap up the call in some error handlers so that, e.g., guard violations and er calls can be trapped and returned as error messages. Unfortunately these error messages are not very informative—they will just say something like ACL2 Halted instead of explaining the problem.

Definitions and Theorems

Function: unsound-eval-fn

(defun unsound-eval-fn (sexpr state)
  (declare (xargs :stobjs (state)))
  (declare (ignorable sexpr))
  (declare (xargs :guard t))
  (let ((__function__ 'unsound-eval))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw lisp definition not installed?"))
         ((mv err1 errmsg? state)
          (read-acl2-oracle state))
         ((mv err2 values state)
          (read-acl2-oracle state))
         ((when (or err1 err2))
          (mv (msg "Reading oracle failed.")
              nil state))
         ((when errmsg?) (mv errmsg? nil state)))
      (mv nil values state))))

Theorem: state-p1-of-unsound-eval.state

(defthm state-p1-of-unsound-eval.state
  (implies (state-p1 state)
           (b* (((mv ?errmsg common-lisp::?values ?state)
                 (unsound-eval-fn sexpr state)))
             (state-p1 state)))
  :rule-classes :rewrite)