Read-file-into-byte-array-stobj
Read the bytes from a file into a stobj array.
;; Returns (mv erp byte-array-stobj state) where either ERP is non-nil (meaning an error
;; occurred) or else the bytes field of BYTE-ARRAY-STOBJ contains the contents of FILENAME.
(defund read-file-into-byte-array-stobj (filename byte-array-stobj state)
(declare (xargs :guard (stringp filename)
:stobjs (byte-array-stobj state)))
;; Get the file length so we know how big to make the array (or I suppose we
;; could resize the array when needed):
(mv-let (file-length state)
(file-length$ filename state)
(if (not file-length)
(mv `(:failed-to-get-file-length ,filename) byte-array-stobj state)
(if (not (unsigned-byte-p 59 file-length)) ; we could weaken this check, but it lets the indexing use fixnums
(mv `(:file-too-long ,filename) byte-array-stobj state)
(mv-let (channel state)
(open-input-channel filename :byte state)
(if (not channel)
;; Error:
(mv `(:could-not-open-channel ,filename) byte-array-stobj state)
(let ( ;; make the array the right size:
(byte-array-stobj (resize-bytes file-length byte-array-stobj)))
(mv-let (byte-array-stobj state)
(read-bytes-into-byte-array-stobj 0 (bytes-length byte-array-stobj) channel byte-array-stobj state)
(let ((state (close-input-channel channel state)))
(mv nil ; no error
byte-array-stobj
state))))))))))
