• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
      • Open-channel-lemmas
      • Std/io/read-char$
      • Std/io/read-object
      • Std/io/open-output-channel
      • Unsound-read
      • Read-string
      • Read-bytes$
      • File-measure
      • Read-bytes$-n
      • Std/io/read-byte$
      • Std/io/open-input-channel
      • Read-file-lines-no-newlines
      • Print-compressed
      • Nthcdr-bytes
      • Read-file-lines
      • Std/io/close-output-channel
      • Read-file-characters
      • Read-file-bytes
      • Print-legibly
      • Std/io/close-input-channel
      • Read-file-objects
      • Logical-story-of-io
      • Take-bytes
      • Std/io/peek-char$
      • Read-file-characters-rev
      • Read-file-as-string
      • Std/io/write-byte$
      • Std/io/set-serialize-character
      • Std/io/print-object$
      • Std/io/princ$
      • Std/io/read-file-into-string
      • *file-types*
    • Oslib
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/io

Read-string

Parse a string into s-expressions, by using Common Lisp's read under the hood. (requires a ttag)

Signature

(read-string str pkg &key (state 'state)) 
  → 
(mv errmsg objects state)

Arguments

str — The string to parse.
    Guard (stringp str).

pkg — The package in which to read the string, or NIL for the current-package.
    Guard (or (null pkg) (stringp pkg)).

Returns

errmsg — An error msg on failure, e.g., parse errors; or nil on success.

objects — The list of objects parsed from str.

state — Type (state-p1 state), given (state-p1 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 str and the resulting s-expressions that you get out.

In the execution, we turn the string into a Common Lisp input stream and try to parse it using read, so that full Common Lisp syntax is permitted. The read is done in the current-package if the pkg argument is nil; otherwise, the pkg argument should be a known package name and the read is done in that package. If we are able to successfully parse objects until EOF is reached, we return success and the list of objects we read.

Jared thinks this may be sound. (Matt K. has since added the pkg argument but thinks this is still sound, because of the continued use of the oracle.) See read-string-tests.lisp for some obvious attempts to cause unsoundness.

Definitions and Theorems

Function: read-string-fn

(defun read-string-fn (str pkg state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp str)
                              (or (null pkg) (stringp pkg)))))
  (declare (ignore pkg))
  (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))))

Theorem: state-p1-of-read-string.state

(defthm state-p1-of-read-string.state
  (implies (state-p1 state)
           (b* (((mv ?errmsg ?objects ?state)
                 (read-string-fn str pkg state)))
             (state-p1 state)))
  :rule-classes :rewrite)