A somewhat robust evaluator.
(unsound-eval sexpr &key (state 'state))
(mv errmsg values state)
- sexpr — An s-expression to evaluate, typically this should be a well-formed
ACL2 form without guard violations, etc. It may mention stobjs.
- 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
(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)
((mv err2 values state)
((when (or err1 err2))
(mv (msg "Reading oracle failed.")
((when errmsg?) (mv errmsg? nil state)))
(mv nil values state))))
(implies (state-p1 state)
(b* (((mv ?errmsg common-lisp::?values ?state)
(unsound-eval-fn sexpr state)))