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

Signature

(syscall-dup2-logic oldfd newfd x86) → (mv * x86)

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

int dup2(int oldfd, int newfd);

dup2() makes newfd be the copy of oldfd, closing newfd first if necessary, but note the following:

• If oldfd is not a valid file descriptor, then the call fails, and newfd is not closed.
• If oldfd is a valid file descriptor, and newfd has the same value as oldfd, then dup2() does nothing, and returns newfd.

After a successful return from one of these system calls, the old and new file descriptors may be used interchangeably. They refer to the same open file description (see open(2)) and thus share file offset and file status flags; for example, if the file offset is modified by using lseek(2) on one of the descriptors, the offset is also changed for the other.

The two descriptors do not share file descriptor flags (the close-on-exec flag). The close-on-exec flag (FD_CLOEXEC; see fcntl(2)) for the duplicate descriptor is off.

Definitions and Theorems

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