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

Signature

(syscall-lseek-logic fd offset whence x86) → (mv * x86)

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

The lseek() function repositions the offset of the open file associated with the file descriptor fd to the argument offset according to the directive whence as follows:

SEEK_SET The offset is set to offset bytes.

SEEK_CUR The offset is set to its current location plus offset bytes.

SEEK_END The offset is set to the size of the file plus offset bytes.

The lseek() function allows the file offset to be set beyond the end of the file (but this does not change the size of the file). If data is later written at this point, subsequent reads of the data in the gap (a "hole") return null bytes ('0') until data is actually written into the gap.

RETURN VALUE

Upon successful completion, lseek() returns the resulting offset location as measured in bytes from the beginning of the file. On error, the value (off_t) -1 is returned and errno is set to indicate the error.

NOTES

When converting old code, substitute values for whence with the follow ing macros:

old new

0 SEEK_SET

1 SEEK_CUR

2 SEEK_END

TO-DO: I have not modeled SEEK_HOLE and SEEK_DATA (available on Linux systems).

Definitions and Theorems

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