Parse a string into s-expressions, by using Common Lisp's
(read-string str &key (state 'state)) → (mv errmsg objects state)
In the logic we just read the oracle to decide if parsing will
succeed or fail. So you can never prove any relationship between the input
In the execution, we turn the string into a Common Lisp input stream and try
to parse it using
Jared thinks this may be sound. See read-string-tests.lisp for some obvious attempts to cause unsoundness.
(defun read-string-fn (str state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp str))) (declare (ignorable str)) (let ((__function__ 'read-string)) (declare (ignorable __function__)) (b* ((- (raise "Raw lisp definition not installed?")) ((mv err1 errmsg? state) (read-acl2-oracle state)) ((mv err2 objects state) (read-acl2-oracle state)) ((when (or err1 err2)) (mv (msg "Reading oracle failed.") nil state)) ((when errmsg?) (mv errmsg? nil state))) (mv nil objects state))))