		Search-engine friendly clone of the ACL2 documentation.

Syscalls-logic

Syscall-read-logic

Signature
(syscall-read-logic fd *buf count x86) → (mv * x86)

From the read(2) man page (Linux):

read() attempts to read up to count bytes from file descriptor fd into the buffer starting at buf.

If count is zero, read() returns zero and has no other results. If count is greater than SSIZE_MAX, the result is unspecified.

RETURN VALUE

On success, the number of bytes read is returned (zero indicates end of file), and the file position is advanced by this number. It is not an error if this number is smaller than the number of bytes requested; this may happen for example because fewer bytes are actually available right now (maybe because we were close to end-of-file, or because we are reading from a pipe, or from a terminal), or because read() was interrupted by a signal. On error, -1 is returned, and errno is set appropriately. In this case it is left unspecified whether the file position (if any) changes.

Definitions and Theorems

Function: syscall-read-logic

(defun syscall-read-logic (fd *buf count x86)
 (declare (xargs :stobjs (x86)))
 (declare (ignorable fd *buf count x86))
 (declare (xargs :guard (and (integerp fd)
                             (integerp *buf)
                             (natp count))))
 (let ((__function__ 'syscall-read-logic))
  (declare (ignorable __function__))
  (b*
   ((obj-fd-field (read-x86-file-des fd x86))
    ((when (not (file-descriptor-fieldp obj-fd-field)))
     (b*
      ((-
        (cw
         "~%Error: File Descriptor Field ill-formed. Maybe these books were ~
not built with X86ISA_EXEC set to t? See :doc x86isa-build-instructions.~%~%"))
       (x86
        (!ms
         (list
          (rip x86)
          "File Descriptor Field ill-formed. Maybe these books were built
with X86ISA_EXEC set to nil? See :doc x86isa-build-instructions."
          (ms x86))
         x86)))
      (mv -1 x86)))
    (obj-name (cdr (assoc :name obj-fd-field)))
    (obj-offset (cdr (assoc :offset obj-fd-field)))
    (obj-mode (cdr (assoc :mode obj-fd-field)))
    ((when (and (not (equal (logand 3 obj-mode) *o_rdonly*))
                (not (equal (logand 3 obj-mode) *o_rdwr*))))
     (b*
      ((-
        (cw
         "~%Error: File has not been opened in the read access mode..~%~%")))
      (mv -1 x86)))
    (obj-contents-field (read-x86-file-contents obj-name x86))
    ((when (not (file-contents-fieldp obj-contents-field)))
     (b* ((- (cw "~%Error: File Contents Field ill-formed.~%~%"))
          (x86 (!ms (list (rip x86)
                          "File Contents Field ill-formed."
                          (ms x86))
                    x86)))
       (mv -1 x86)))
    (obj-contents (cdr (assoc :contents obj-contents-field)))
    (bytes-of-obj (string-to-bytes obj-contents))
    ((when (< (len bytes-of-obj) obj-offset))
     (b*
      ((-
        (cw
          "~%Error: Offset is beyond the size of the object.~%~%")))
      (mv -1 x86)))
    (bytes-of-obj-from-offset (nthcdr obj-offset bytes-of-obj))
    (count-bytes-of-obj-from-offset
         (if (eql bytes-of-obj-from-offset nil)
             nil
           (take count bytes-of-obj-from-offset)))
    (only-bytes-of-obj-from-offset
         (grab-bytes count-bytes-of-obj-from-offset))
    (n (if (eql only-bytes-of-obj-from-offset nil)
           0
         (len only-bytes-of-obj-from-offset)))
    ((mv flg x86)
     (if (equal only-bytes-of-obj-from-offset nil)
         (mv nil x86)
      (if
       (and
         (canonical-address-p *buf)
         (canonical-address-p (+ (len only-bytes-of-obj-from-offset)
                                 *buf)))
       (write-bytes-to-memory
            *buf only-bytes-of-obj-from-offset x86)
       (mv t x86))))
    ((when flg)
     (b* ((- (cw "~%Error: Buffer Memory Error.~%~%")))
       (mv -1 x86)))
    (x86 (write-x86-file-des fd
                             (put-assoc :offset (+ n obj-offset)
                                        obj-fd-field)
                             x86)))
   (mv n x86))))