• 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-logic

Syscall-open-logic

Signature

(syscall-open-logic pathname oflags mode x86) → (mv * x86)

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

Given a pathname for a file, open() returns a file descriptor, a small, nonnegative integer for use in subsequent system calls (read(2), write(2), lseek(2), fcntl(2), etc.). The file descriptor returned by a successful call will be the lowest-numbered file descriptor not currently open for the process.

The file offset is set to the beginning of the file (see lseek(2)).

The argument flags must include one of the following access modes: O_RDONLY, O_WRONLY, or O_RDWR. These request opening the file read- only, write-only, or read/write, respectively.

In addition, zero or more file creation flags and file status flags can be bitwise-or'd in flags. The file creation flags are O_CREAT, O_EXCL, O_NOCTTY, and O_TRUNC.

Definitions and Theorems

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