• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
          • Syscalls-logic
            • Syscall-write-logic
            • Syscall-lseek-logic
            • Syscall-read-logic
            • Syscall-open-logic
            • Syscall-dup2-logic
            • Syscall-close-logic
            • Syscall-dup-logic
            • Syscall-write
            • Syscall-read
            • Syscall-open
            • Syscall-lseek
            • Syscall-close
            • Syscall-dup
            • Syscall-unlink
            • Syscall-truncate
            • Syscall-stat
            • Syscall-lstat
            • Syscall-link
            • Syscall-ftruncate
            • Syscall-fstat
            • Syscall-fcntl
            • Syscall-fadvise64
            • Syscall-dup2
            • Syscall-unlink-logic
            • Syscall-truncate-logic
            • Syscall-stat-logic
            • Syscall-lstat-logic
            • Syscall-link-logic
            • Syscall-ftruncate-logic
            • Syscall-fstat-logic
            • Syscall-fcntl-logic
            • Syscall-fadvise64-logic
            • Syscall-dup3-logic
            • Syscall-dup3
          • X86-syscall-args-and-return-value-marshalling
          • Syscall-numbers
          • Syscalls-exec
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Syscalls

Syscalls-logic

Logical definitions for syscalls to be used in the application-level view for reasoning

All the *-logic functions (like syscall-read-logic) should be untouchable (push-untouchable) --- we want to disallow the use of these functions during evaluation as well as proof since they aren't the top-level interface functions (like syscall-read).

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))))

Function: syscall-read$notinline

(defun syscall-read$notinline (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))
    (declare (ignorable __function__))
    (syscall-read-logic fd *buf count x86)))

Theorem: integerp-mv-nth-0-syscall-read

(defthm integerp-mv-nth-0-syscall-read
  (integerp (mv-nth 0 (syscall-read fd *buf count x86)))
  :rule-classes :type-prescription)

Theorem: x86p-mv-nth-1-syscall-read

(defthm x86p-mv-nth-1-syscall-read
  (implies (and (x86p x86) (integerp fd))
           (x86p (mv-nth 1 (syscall-read fd *buf count x86)))))

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))))

Function: syscall-write$notinline

(defun syscall-write$notinline (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))
    (declare (ignorable __function__))
    (syscall-write-logic fd *buf count x86)))

Theorem: integerp-mv-nth-0-syscall-write

(defthm integerp-mv-nth-0-syscall-write
  (implies (natp count)
           (integerp (mv-nth 0 (syscall-write fd *buf count x86))))
  :rule-classes :type-prescription)

Theorem: x86p-mv-nth-1-syscall-write

(defthm x86p-mv-nth-1-syscall-write
  (implies (and (x86p x86) (integerp fd))
           (x86p (mv-nth 1 (syscall-write fd *buf count x86)))))

Function: syscall-open-logic

(defun syscall-open-logic (pathname oflags mode x86)
 (declare (xargs :stobjs (x86)))
 (declare (ignorable pathname oflags mode x86))
 (declare (xargs :guard (and (stringp pathname)
                             (natp oflags)
                             (natp mode))))
 (let ((__function__ 'syscall-open-logic))
  (declare (ignorable __function__))
  (b*
   (((mv new-fd x86) (pop-x86-oracle x86))
    ((when (not (natp new-fd)))
     (b*
      ((-
        (cw
         "~%Error: File Descriptor 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 ill-formed. Maybe these books were
not built with X86ISA_EXEC set to t? See :doc x86sa-build-instructions."
          (ms x86))
         x86)))
      (mv -1 x86)))
    ((when (and (not (equal (logand 3 mode) *o_rdonly*))
                (not (equal (logand 3 mode) *o_wronly*))
                (not (equal (logand 3 mode) *o_rdwr*))))
     (b*
      ((-
        (cw
         "~%Error: File mode is not an appropriate access mode.~%~%")))
      (mv -1 x86)))
    (obj-fd-field (read-x86-file-des new-fd x86))
    (obj-contents-field (read-x86-file-contents pathname x86))
    ((mv flg obj-contents-field x86)
     (if
      (equal (logand *o_creat* mode)
             *o_creat*)
      (if (and (file-descriptor-fieldp obj-fd-field)
               (file-contents-fieldp obj-contents-field))
          (if (equal (logand *o_excl* mode) *o_excl*)
              (mv t obj-contents-field x86)
            (mv nil obj-contents-field x86))
       (b*
        ((x86
          (write-x86-file-contents pathname (acons :contents "" nil)
                                   x86))
         (- (cw "here 0")))
        (mv nil (acons :contents "" nil) x86)))
      (mv nil obj-contents-field x86)))
    ((when flg)
     (b*
      ((-
        (cw
         "~%Error: [O_EXCL Mode] O_CREAT used but file already exists.~%~%")))
      (mv -1 x86)))
    (x86
      (if (and (equal (logand *o_trunc* mode)
                      *o_trunc*)
               (file-descriptor-fieldp obj-fd-field)
               (file-contents-fieldp obj-contents-field))
          (write-x86-file-contents pathname (acons :contents "" nil)
                                   x86)
        x86))
    (x86
      (if (equal obj-contents-field nil)
          (write-x86-file-contents pathname (acons :contents "" nil)
                                   x86)
        x86))
    (fd-field
     (put-assoc
         :name pathname
         (put-assoc :offset 0
                    (put-assoc :mode oflags
                               (put-assoc :permissions mode nil)))))
    (x86 (write-x86-file-des new-fd fd-field x86)))
   (mv new-fd x86))))

Function: syscall-open$notinline

(defun syscall-open$notinline (pathname oflags mode x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable pathname oflags mode x86))
  (declare (xargs :guard (and (stringp pathname)
                              (natp oflags)
                              (natp mode))))
  (let ((__function__ 'syscall-open))
    (declare (ignorable __function__))
    (syscall-open-logic pathname oflags mode x86)))

Theorem: integerp-mv-nth-0-syscall-open

(defthm integerp-mv-nth-0-syscall-open
  (implies
       (and (x86p x86) (stringp pathname))
       (integerp (mv-nth 0
                         (syscall-open pathname oflags mode x86))))
  :rule-classes :type-prescription)

Theorem: x86p-mv-nth-1-syscall-open

(defthm x86p-mv-nth-1-syscall-open
  (implies (and (x86p x86) (stringp pathname))
           (x86p (mv-nth 1
                         (syscall-open pathname oflags mode x86)))))

Function: syscall-close-logic

(defun syscall-close-logic (fd x86)
 (declare (xargs :stobjs (x86)))
 (declare (ignorable fd x86))
 (declare (xargs :guard (integerp fd)))
 (let ((__function__ 'syscall-close-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
not built with X86ISA_EXEC set to t? See :doc x86isa-build-instructions."
          (ms x86))
         x86)))
      (mv -1 x86)))
    (x86 (delete-x86-file-des fd x86)))
   (mv 0 x86))))

Function: syscall-close$notinline

(defun syscall-close$notinline (fd x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd x86))
  (declare (xargs :guard (integerp fd)))
  (let ((__function__ 'syscall-close))
    (declare (ignorable __function__))
    (syscall-close-logic fd x86)))

Theorem: integerp-mv-nth-0-syscall-close

(defthm integerp-mv-nth-0-syscall-close
  (integerp (mv-nth 0 (syscall-close fd x86)))
  :rule-classes :type-prescription)

Theorem: x86p-mv-nth-1-syscall-close

(defthm x86p-mv-nth-1-syscall-close
  (implies (and (x86p x86) (integerp fd))
           (x86p (mv-nth 1 (syscall-close fd x86)))))

Function: syscall-lseek-logic

(defun syscall-lseek-logic (fd offset whence x86)
 (declare (xargs :stobjs (x86)))
 (declare (ignorable fd offset whence x86))
 (declare (xargs :guard (and (natp fd)
                             (integerp offset)
                             (natp whence))))
 (let ((__function__ 'syscall-lseek-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
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)))
    ((mv new-offset x86)
     (case whence
      (0
       (b*
        (((when (not (natp offset)))
          (b*
           ((-
             (cw
              "~%Error: SEEK_SET: New file offset not a Natp.~%~%")))
           (mv -1 x86)))
         (x86 (write-x86-file-des
                   fd
                   (put-assoc :offset offset obj-fd-field)
                   x86)))
        (mv offset x86)))
      (1
       (b*
        (((when (not (natp (+ obj-offset offset))))
          (b*
           ((-
             (cw
              "~%Error: SEEK_CUR: New file offset not a natp.~%~%")))
           (mv -1 x86)))
         (x86 (write-x86-file-des
                   fd
                   (put-assoc :offset (+ obj-offset offset)
                              obj-fd-field)
                   x86)))
        (mv (+ obj-offset offset) x86)))
      (2
       (b*
        ((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-len (len bytes-of-obj))
         ((when (not (natp (+ obj-len offset))))
          (b*
           ((-
             (cw
              "~%Error: SEEK_END: New file offset not a natp.~%~%")))
           (mv -1 x86)))
         (x86
           (write-x86-file-des fd
                               (put-assoc :offset (+ obj-len offset)
                                          obj-fd-field)
                               x86)))
        (mv (+ obj-len offset) x86)))
      (t (b* ((- (cw "~%Error: Unsupported whence value.~%~%"))
              (x86 (!ms (list (rip x86)
                              "Unsupported whence value." (ms x86))
                        x86)))
           (mv -1 x86))))))
   (mv new-offset x86))))

Function: syscall-lseek$notinline

(defun syscall-lseek$notinline (fd offset whence x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd offset whence x86))
  (declare (xargs :guard (and (natp fd)
                              (integerp offset)
                              (natp whence))))
  (let ((__function__ 'syscall-lseek))
    (declare (ignorable __function__))
    (syscall-lseek-logic fd offset whence x86)))

Theorem: integerp-mv-nth-0-syscall-lseek

(defthm integerp-mv-nth-0-syscall-lseek
  (integerp (mv-nth 0 (syscall-lseek fd offset whence x86)))
  :rule-classes :type-prescription)

Theorem: x86p-mv-nth-1-syscall-lseek

(defthm x86p-mv-nth-1-syscall-lseek
  (implies (and (x86p x86) (natp fd))
           (x86p (mv-nth 1
                         (syscall-lseek fd offset whence x86)))))

Function: syscall-fadvise64-logic

(defun syscall-fadvise64-logic (fd offset len advice x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd offset len advice x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-fadvise64-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-fadvise64$notinline

(defun syscall-fadvise64$notinline (fd offset len advice x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd offset len advice x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-fadvise64))
    (declare (ignorable __function__))
    (syscall-fadvise64-logic fd offset len advice x86)))

Function: syscall-link-logic

(defun syscall-link-logic (oldpath newpath x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldpath newpath x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-link-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-link$notinline

(defun syscall-link$notinline (oldpath newpath x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldpath newpath x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-link))
    (declare (ignorable __function__))
    (syscall-link-logic oldpath newpath x86)))

Function: syscall-unlink-logic

(defun syscall-unlink-logic (path x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-unlink-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-unlink$notinline

(defun syscall-unlink$notinline (path x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-unlink))
    (declare (ignorable __function__))
    (syscall-unlink-logic path x86)))

Function: syscall-dup-logic

(defun syscall-dup-logic (oldfd x86)
 (declare (xargs :stobjs (x86)))
 (declare (ignorable oldfd x86))
 (declare (xargs :guard (integerp oldfd)))
 (let ((__function__ 'syscall-dup-logic))
  (declare (ignorable __function__))
  (b*
   ((obj-fd-field (read-x86-file-des oldfd 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)))
    ((mv newfd x86) (pop-x86-oracle x86))
    ((when (not (integerp newfd)))
     (b*
       ((- (cw "~%Error: New file descriptor not an integer.~%~%"))
        (x86 (!ms (list (rip x86)
                        "New file descriptor not an integer"
                        newfd (ms x86))
                  x86)))
       (mv -1 x86))))
   (mv newfd x86))))

Function: syscall-dup$notinline

(defun syscall-dup$notinline (oldfd x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldfd x86))
  (declare (xargs :guard (integerp oldfd)))
  (let ((__function__ 'syscall-dup))
    (declare (ignorable __function__))
    (syscall-dup-logic oldfd x86)))

Theorem: integerp-mv-nth-0-syscall-dup

(defthm integerp-mv-nth-0-syscall-dup
  (integerp (mv-nth 0 (syscall-dup oldfd x86)))
  :rule-classes :type-prescription)

Theorem: x86p-mv-nth-1-syscall-dup

(defthm x86p-mv-nth-1-syscall-dup
  (implies (x86p x86)
           (x86p (mv-nth 1 (syscall-dup oldfd x86)))))

Function: syscall-dup2-logic

(defun syscall-dup2-logic (oldfd newfd x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldfd newfd x86))
  (declare (xargs :guard (and (integerp oldfd)
                              (integerp newfd))))
  (let ((__function__ 'syscall-dup2-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-dup2$notinline

(defun syscall-dup2$notinline (oldfd newfd x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldfd newfd x86))
  (declare (xargs :guard (and (integerp oldfd)
                              (integerp newfd))))
  (let ((__function__ 'syscall-dup2))
    (declare (ignorable __function__))
    (syscall-dup2-logic oldfd newfd x86)))

Function: syscall-dup3-logic

(defun syscall-dup3-logic (oldfd newfd flags x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldfd newfd flags x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-dup3-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-dup3$notinline

(defun syscall-dup3$notinline (oldfd newfd flags x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable oldfd newfd flags x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-dup3))
    (declare (ignorable __function__))
    (syscall-dup3-logic oldfd newfd flags x86)))

Function: syscall-stat-logic

(defun syscall-stat-logic (path buf x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path buf x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-stat-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-stat$notinline

(defun syscall-stat$notinline (path buf x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path buf x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-stat))
    (declare (ignorable __function__))
    (syscall-stat-logic path buf x86)))

Function: syscall-lstat-logic

(defun syscall-lstat-logic (path buf x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path buf x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-lstat-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-lstat$notinline

(defun syscall-lstat$notinline (path buf x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path buf x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-lstat))
    (declare (ignorable __function__))
    (syscall-lstat-logic path buf x86)))

Function: syscall-fstat-logic

(defun syscall-fstat-logic (fd buf x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd buf x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-fstat-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-fstat$notinline

(defun syscall-fstat$notinline (fd buf x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd buf x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-fstat))
    (declare (ignorable __function__))
    (syscall-fstat-logic fd buf x86)))

Function: syscall-fcntl-logic

(defun syscall-fcntl-logic (fd cmd arg x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd cmd arg x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-fcntl-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-fcntl$notinline

(defun syscall-fcntl$notinline (fd cmd arg x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd cmd arg x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-fcntl))
    (declare (ignorable __function__))
    (syscall-fcntl-logic fd cmd arg x86)))

Function: syscall-truncate-logic

(defun syscall-truncate-logic (path length x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path length x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-truncate-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-truncate$notinline

(defun syscall-truncate$notinline (path length x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable path length x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-truncate))
    (declare (ignorable __function__))
    (syscall-truncate-logic path length x86)))

Function: syscall-ftruncate-logic

(defun syscall-ftruncate-logic (fd length x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd length x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-ftruncate-logic))
    (declare (ignorable __function__))
    (pop-x86-oracle x86)))

Function: syscall-ftruncate$notinline

(defun syscall-ftruncate$notinline (fd length x86)
  (declare (xargs :stobjs (x86)))
  (declare (ignorable fd length x86))
  (declare (xargs :guard t))
  (let ((__function__ 'syscall-ftruncate))
    (declare (ignorable __function__))
    (syscall-ftruncate-logic fd length x86)))

Subtopics

Syscall-write-logic

Syscall-lseek-logic

Syscall-read-logic

Syscall-open-logic

Syscall-dup2-logic

Syscall-close-logic

Syscall-dup-logic

Syscall-write

Syscall-read

Syscall-open

Syscall-lseek

Syscall-close

Syscall-dup

Syscall-unlink

Syscall-truncate

Syscall-stat

Syscall-lstat

Syscall-link

Syscall-ftruncate

Syscall-fstat

Syscall-fcntl

Syscall-fadvise64

Syscall-dup2

Syscall-unlink-logic

Syscall-truncate-logic

Syscall-stat-logic

Syscall-lstat-logic

Syscall-link-logic

Syscall-ftruncate-logic

Syscall-fstat-logic

Syscall-fcntl-logic

Syscall-fadvise64-logic

Syscall-dup3-logic

Syscall-dup3