		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.

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)

General Form:

(read-file-into-string filename :start s :bytes b)

where filename is a string, which is typically the name of a file; and where :start s and :bytes b are optional, where s has default 0 and b has default nil, s is a natural number, and b is either a natural number or 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, then the entire file contents are returned as a string. In general, :start s specifies the part of the file starting at the s-th byte, and :bytes b specifies that only the first b bytes are to be read starting at that position, stopping at end of file in what we call the ``truncation case'': where b+s exceeds the length of the file.

If :start s is specified where s > 0, then the next read must start where the previous read left off. More precisely: in this case ACL2 expects that there was an earlier call of read-file-into-string on the same file, where the most recent such call must not have been the ``truncation case'' (see above) and must have have specified :bytes such that the first unread byte position is s. Otherwise, an error occurs. Note that if s is 0 then there is no such restriction; the read is viewed as a new ``first'' read of the file.

WARNING: A Lisp stream is created for the specified file, and is left open until a call of read-file-into-string is either made with :bytes having value nil (the default) or is in the ``truncation case'' described above. Operating systems can complain when too many streams are open at the same time. In particular, consider the case that :start s and :bytes b are specified where s > 0, and where s+b is exactly the length of the file. Thus we are barely not in the ``truncation case'' described above, so one more read will be necessary in order to close that stream. Your code might thus include code such as the following (for example) after a call of read-file-into-string with non-nil :bytes:

(prog2$
 (and (= (+ position bytes) file-length)

; Then close the stream:

      (read-file-into-string
       filename
       :start file-length
       :bytes 1))
 <more_code>)

End of warning.

This macro provides functionality that can be obtained through the usual io routines provided by ACL2, as shown by the sequence of definitions below. However, under-the-hood raw Lisp code provides an implementation that not only is efficient, but also does not return state. Note that the expansion of a call of this macro does take state as an argument, which (as usual for functions that take state) necessitates either that (set-state-ok t) has already been evaluated, or else that a suitable :stobjs declaration, typically :stobjs state, is provided (see xargs).

The value of the constant *read-file-into-string-bound* (see the definition below) is a strict upper bound on the size of the string returned. If the file (or 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. One check ensures that the write date of the file has not changed between two such calls; otherwise ACL2 will cause a raw Lisp error of the following form.

************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  Illegal consecutive reads from file "MY-FILE".
See :DOC read-file-into-string.
***********************************************

The other check ensures that the write date of the file has not changed while the second call is in progress. For simplicity, ACL2 actually makes this check even for the first call. When the check fails the corresponding raw 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.
***********************************************

The first of these errors can actually occur when the second read is performed by open-input-channel of type :character. But we expect all such errors to be rare, since they only occur when there are two reads to the same file with an intervening external write, in the case that the two ACL2 states have the same file-clock field (see state). That field is updated any time a channel is opened or closed.

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 state)
       (declare (xargs :stobjs state
                       :guard (and (stringp filename)
                                   (natp start)
                                   (or (null bytes) (natp bytes)))))
       (read-file-into-string2-logical filename start bytes state))

Macro: read-file-into-string

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

Subtopics

Std/io/read-file-into-string