		Search-engine friendly clone of the ACL2 documentation.

Read-file-into-string

The contents of a file (or part of it) as a string

When this macro is passed a valid filename and the ACL2 state, it generally returns the contents of the file (or a specified part of the file) as a string. Otherwise, it returns nil or causes an error. Unlike other ACL2 functions for reading a file, this one does not return the ACL2 state, and it is generally much faster.

Example Forms:

(read-file-into-string "foo.lisp")
(read-file-into-string "foo.lisp" :start 0 :bytes nil) ; same as above
(read-file-into-string "foo.lisp" :start 20000 :bytes 10000)
(read-file-into-string "foo.lisp" :start 20000 :bytes 10000 :close t)

General Form:

(read-file-into-string filename ; a filename relative to the current directory
                       :start s ; default 0
                       :bytes b ; default nil
                       :close c ; default :default
                       )

where filename is a string, which is typically the name of a file, and the keyword argument are optional and evaluated, as follows: s has default 0 and its value is a natural number (except, an error occurs if that number exceeds the length of the given file), b has default nil and its value is either a natural number or nil, and c has default :default and its value is otherwise considered to be false (when nil) or true (when not nil).

For examples, see community-books file books/system/tests/read-file-into-string.lisp.

The result, when not nil or an error, is a string representing the specified file contents. For the default of :start 0 and :bytes nil, or equivalently, when no keyword arguments are specified, the entire file contents are returned as a string. In general, :start s specifies the part of the file starting at byte position s of the file, and :bytes b specifies that only the first b bytes are to be read starting at that position — however, stopping at the end of the file if b+s exceeds the length L of the file. Below we call this case that b+s>L the ``truncation case''.

Note that ACL2 characters always fit into a single byte, which is why we can talk about ``bytes'' here.

The :close argument affects handling of the Lisp stream that is created for the specified file. When the value of :close is the default, :default, this stream is closed immediately after the read exactly when either :bytes has value nil (the default) or we are in the truncation case b+s>L described above. But otherwise the stream remains open, which could cause a problem since operating systems can complain when too many streams are open at the same time. If the value of :bytes is non-nil (hence, a natural number), then you may want to specify :close t to prevent that problem, unless you plan to read more bytes from the same file. If you decide to close the file later, this can be accomplished efficiently by evaluating the following form for your file, "<file>".

(time$ (read-file-into-string "<file>" :start 0 :bytes 0 :close t))

Compared with the usual io routines provided by ACL2, read-file-into-string is generally much more efficient, and also it does not return state. Note that the expansion of a call of this macro takes state as an argument; so if you call it in the body of a function definition, then — as usual for functions that take state — either (set-state-ok t) must have been evaluated or else a suitable :stobjs declaration, typically :stobjs state, must be provided (see xargs).

The constant *read-file-into-string-bound* (see the definition below) establishes a strict upper bound on the size of the string returned. If the file (or specified portion thereof) contains more bytes than this, then nil is returned.

There are two checks to guarantee that read-file-into-string is truly a function — that is, it returns the same value for two calls with the same inputs. The primary check ensures that the write date of the file has not changed in the interval between two such calls unless the file-clock component of the ACL2 state has been updated within that interval. That update takes place when an input or output channel is opened or closed in the usual way (that is, using open-input-channel, open-output-channel, close-input-channel, or close-output-channel; see io). However, it suffices to evaluate the following form, which returns the state obtained by incrementing its file-clock.

(increment-file-clock state)

If however you make illegal successive reads as described above, a Lisp error will occur with a message of the following form.

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  Illegal consecutive reads from file
"<some_filename>",
which appears to have been written between the two reads.
Execute (INCREMENT-FILE-CLOCK STATE) to avoid this error.
See :DOC read-file-into-string.
While executing: READ-FILE-INTO-STRING2
***********************************************

A similar error may occur when a call of read-file-into-string is followed by a call of open-input-channel on the same filename when that file is modified between the two calls. For low-level details about logical issues being addressed by such errors, see the comment in the definition of *read-file-into-string-alist* in the ACL2 sources.

The other check ensures that the write date of the file has not changed while a call is in progress. When that check fails the corresponding Lisp error is of the following form.

************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  Illegal attempt to call READ-FILE-INTO-STRING concurrently
with some write to that file!  See :DOC read-file-into-string.
***********************************************

We close by showing the relevant ACL2 definitions in the logic, that is, not including the special raw Lisp (under the hood) code in the definition of read-file-into-string2.

Function: read-file-into-string1

(defun
 read-file-into-string1
 (channel state ans bound)
 (declare (xargs :stobjs state
                 :guard (and (symbolp channel)
                             (open-input-channel-p channel
                                                   :character state)
                             (character-listp ans)
                             (natp bound))))
 (cond
  ((zp bound) (mv nil state))
  (t
   (mv-let
       (val state)
       (read-char$ channel state)
       (cond ((not (characterp val))
              (mv (coerce (reverse ans) 'string)
                  state))
             (t (read-file-into-string1 channel state (cons val ans)
                                        (1- bound))))))))

Definition: *read-file-into-string-bound*

(defconst *read-file-into-string-bound*
          (1- (ash 1 60)))

Function: read-file-into-string2-logical

(defun
 read-file-into-string2-logical
 (filename start bytes state)
 (declare (xargs :stobjs state
                 :guard (and (stringp filename)
                             (natp start)
                             (or (null bytes) (natp bytes)))))
 (non-exec
  (mv-let
   (erp val state)
   (mv-let
    (chan state)
    (open-input-channel filename
                        :character state)
    (cond
       ((or (null chan) (not (state-p state)))
        (mv nil nil state))
       (t (mv-let (val state)
                  (read-file-into-string1
                       chan
                       state nil *read-file-into-string-bound*)
                  (pprogn (ec-call (close-input-channel chan state))
                          (mv nil val state))))))
   (declare (ignore erp state))
   (and (stringp val)
        (<= start (length val))
        (subseq val start
                (if bytes (min (+ start bytes) (length val))
                    (length val)))))))

Function: read-file-into-string2

(defun read-file-into-string2
       (filename start bytes close state)
       (declare (xargs :stobjs state
                       :guard (and (stringp filename)
                                   (natp start)
                                   (or (null bytes) (natp bytes)))))
       (declare (ignore close))
       (read-file-into-string2-logical filename start bytes state))

Macro: read-file-into-string

(defmacro read-file-into-string
          (filename &key (start '0)
                    bytes (close ':default))
          (cons 'read-file-into-string2
                (cons filename
                      (cons start
                            (cons bytes (cons close '(state)))))))

Subtopics

Std/io/read-file-into-string