		Search-engine friendly clone of the ACL2 documentation.

Syscalls-logic

Syscall-write-logic

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

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

write() writes up to count bytes from the buffer pointed buf to the file referred to by the file descriptor fd.

The number of bytes written may be less than count if, for example, there is insufficient space on the underlying physical medium, or the RLIMIT_FSIZE resource limit is encountered (see setrlimit(2)), or the call was interrupted by a signal handler after having written less than count bytes. (See also pipe(7).)

For a seekable file (i.e., one to which lseek(2) may be applied, for example, a regular file) writing takes place at the current file offset, and the file offset is incremented by the number of bytes actually written. If the file was open(2)ed with O_APPEND, the file offset is first set to the end of the file before writing. The adjustment of the file offset and the write operation are performed as an atomic step.

RETURN VALUE

On success, the number of bytes written is returned (zero indicates nothing was written). On error, -1 is returned, and errno is set appropriately.

If count is zero and fd refers to a regular file, then write() may return a failure status if one of the errors below is detected. If no errors are detected, 0 will be returned without causing any other effect. If count is zero and fd refers to a file other than a regular file, the results are not specified.

Definitions and Theorems

Function: syscall-write-logic

(defun syscall-write-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-write-logic))
  (declare (ignorable __function__))
  (b*
   (((mv flg count-bytes-from-buffer x86)
     (if (and (canonical-address-p *buf)
              (canonical-address-p (+ count *buf)))
         (read-bytes-from-memory *buf count x86 nil)
       (mv t 0 x86)))
    ((when flg)
     (b* ((- (cw "~%Error: Buffer Memory Error.~%~%")))
       (mv -1 x86)))
    (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
not built with X86ISA_EXEC set to t? 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_wronly*))
                (not (equal (logand 3 obj-mode) *o_rdwr*))))
     (b*
      ((-
        (cw
         "~%Error: File has not been opened in the write 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))
    (obj-offset (if (equal (logand *o_append* obj-mode)
                           *o_append*)
                    (len bytes-of-obj)
                  obj-offset))
    (bytes-of-obj-till-offset
         (coerce-bytes (take obj-offset bytes-of-obj)))
    (new-byte-contents (append bytes-of-obj-till-offset
                               count-bytes-from-buffer))
    (new-string-contents
         (coerce (bytes-to-charlist new-byte-contents)
                 'string))
    (x86 (write-x86-file-contents
              obj-name
              (put-assoc :contents
                         new-string-contents obj-contents-field)
              x86))
    (x86 (write-x86-file-des fd
                             (put-assoc :offset (+ count obj-offset)
                                        obj-fd-field)
                             x86)))
   (mv count x86))))