• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
          • Syscalls-logic
          • X86-syscall-args-and-return-value-marshalling
            • X86-syscall-link
            • X86-syscall-truncate
            • X86-syscall-unlink
            • X86-syscall-stat
            • X86-syscall-open
            • X86-syscall-lstat
            • X86-syscall-write
            • X86-syscall-read
            • X86-syscall-lseek
            • X86-syscall-ftruncate
            • X86-syscall-fstat
            • X86-syscall-fcntl
            • X86-syscall-fadvise64
            • X86-syscall-dup3
            • X86-syscall-dup2
            • X86-syscall-dup
            • X86-syscall-close
          • 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
      • Proof-utilities
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Syscalls

X86-syscall-args-and-return-value-marshalling

Collecting arguments to system calls from the x86 state and retrieving the return value

Source: System V Application Binary Interface AMD64 Architecture Processor Supplement (Draft Version 0.99.6, July 2, 2012) --- also called x64 ABI informally. Edited by Michael Matz, Jan Hubic ka, Andreas Jaeger, Mark Mitchell

The Linux AMD64 kernel uses internally the same calling conventions as user-level applications... User-level applications that like to call system calls should use the functions from the C library. The interface between the C library and the Linux kernel is the same as for the user-level applications with the following differences:

1. User-level applications use as integer registers for passing the sequence %rdi, %rsi, %rdx, %rcx, %r8 and %r9. The kernel interface uses %rdi, %rsi, %rdx, %r10, %r8 and %r9.
2. A system-call is done via the syscall instruction. The kernel destroys registers %rcx and %r11.
3. The number of the syscall has to be passed in register %rax.
4. System-calls are limited to six arguments, no argument is passed directly on the stack.
5. Returning from the syscall, register %rax contains the result of the system-call. A value in the range between -4095 and -1 indicates an error, it is -errno.
6. Only values of class INTEGER or class MEMORY are passed to the kernel.

Definitions and Theorems

Function: x86-syscall-read

(defun x86-syscall-read (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-read))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-read)
         (fd (rr64 *rdi* x86))
         (*buf (rgfi *rsi* x86))
         (count (rr64 *rdx* x86))
         ((mv ret x86)
          (syscall-read fd *buf count x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-read

(defthm x86p-of-x86-syscall-read
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-read x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-write

(defun x86-syscall-write (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-write))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-write)
         (fd (rr64 *rdi* x86))
         (*buf (rgfi *rsi* x86))
         (count (rr64 *rdx* x86))
         ((mv ret x86)
          (syscall-write fd *buf count x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-write

(defthm x86p-of-x86-syscall-write
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-write x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-open

(defun x86-syscall-open (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-open))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-open)
         (path-ptr (rgfi *rdi* x86))
         (flags (rr64 *rsi* x86))
         (mode (rr64 *rdx* x86))
         ((when (not (canonical-address-p path-ptr)))
          (!ms :syscall-open-path-ptr-not-canonical x86))
         ((mv flg path x86)
          (read-string-zero-terminated path-ptr x86))
         ((when flg)
          (!ms (list ctx :path flg) x86))
         ((mv ret x86)
          (syscall-open path flags mode x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-open

(defthm x86p-of-x86-syscall-open
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-open x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-close

(defun x86-syscall-close (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-close))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-close)
         (fd (rr64 *rdi* x86))
         ((mv ret x86) (syscall-close fd x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-close

(defthm x86p-of-x86-syscall-close
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-close x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-lseek

(defun x86-syscall-lseek (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-lseek))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-lseek)
         (fd (rr64 *rdi* x86))
         (offset (rgfi *rsi* x86))
         (whence (rr64 *rdx* x86))
         ((mv ret x86)
          (syscall-lseek fd offset whence x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-lseek

(defthm x86p-of-x86-syscall-lseek
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-lseek x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-fadvise64

(defun x86-syscall-fadvise64 (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-fadvise64))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-fadvise64)
         (fd (rr64 *rdi* x86))
         (offset (rgfi *rsi* x86))
         (len (rgfi *rdx* x86))
         (advice (rgfi *r10* x86))
         ((mv ret x86)
          (syscall-fadvise64 fd offset len advice x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-fadvise64

(defthm x86p-of-x86-syscall-fadvise64
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-fadvise64 x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-link

(defun x86-syscall-link (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-link))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-link)
         (old-path-ptr (rgfi *rdi* x86))
         (new-path-ptr (rgfi *rsi* x86))
         ((when (not (canonical-address-p old-path-ptr)))
          (!ms (list ctx :syscall-link-oldpath-ptr-overflow)
               x86))
         ((mv flg old-path x86)
          (read-string-zero-terminated old-path-ptr x86))
         ((when flg)
          (!ms (list ctx :old-path flg) x86))
         ((when (not (canonical-address-p new-path-ptr)))
          (!ms (list ctx :syscall-link-newpath-ptr-overflow)
               x86))
         ((mv flg new-path x86)
          (read-string-zero-terminated new-path-ptr x86))
         ((when flg)
          (!ms (list ctx :new-path flg) x86))
         ((mv ret x86)
          (syscall-link old-path new-path x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-link

(defthm x86p-of-x86-syscall-link
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-link x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-unlink

(defun x86-syscall-unlink (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-unlink))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-unlink)
         (path-ptr (rgfi *rdi* x86))
         ((when (not (canonical-address-p path-ptr)))
          (!ms (list ctx :syscall-link-path-ptr-overflow)
               x86))
         ((mv flg path x86)
          (read-string-zero-terminated path-ptr x86))
         ((when flg)
          (!ms (list ctx :path flg) x86))
         ((mv ret x86) (syscall-unlink path x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :oracle-val-for-syscall-unlink ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-unlink

(defthm x86p-of-x86-syscall-unlink
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-unlink x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-dup

(defun x86-syscall-dup (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-dup))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-dup)
         (oldfd (rgfi *rdi* x86))
         ((mv ret x86) (syscall-dup oldfd x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :oracle-val-for-syscall-dup ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-dup

(defthm x86p-of-x86-syscall-dup
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-dup x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-dup2

(defun x86-syscall-dup2 (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-dup2))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-dup2)
         (oldfd (rgfi *rdi* x86))
         (newfd (rgfi *rsi* x86))
         ((mv ret x86)
          (syscall-dup2 oldfd newfd x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-dup2

(defthm x86p-of-x86-syscall-dup2
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-dup2 x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-dup3

(defun x86-syscall-dup3 (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-dup3))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-dup3)
         (oldfd (rgfi *rdi* x86))
         (newfd (rgfi *rsi* x86))
         (flags (rgfi *rdx* x86))
         ((mv ret x86)
          (syscall-dup3 oldfd newfd flags x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-dup3

(defthm x86p-of-x86-syscall-dup3
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-dup3 x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-stat

(defun x86-syscall-stat (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-stat))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-stat)
         (path (rgfi *rdi* x86))
         (statbuf (rgfi *rsi* x86))
         ((when (not (canonical-address-p path)))
          (!ms (list ctx
                     :syscall-stat-path-ptr-not-canonical)
               x86))
         ((mv flg pathname x86)
          (read-string-zero-terminated path x86))
         ((when flg)
          (!ms (list ctx :path flg) x86))
         ((mv ret x86)
          (syscall-stat pathname statbuf x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :oracle-val-for-syscall-stat ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-stat

(defthm x86p-of-x86-syscall-stat
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-stat x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-lstat

(defun x86-syscall-lstat (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-lstat))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-lstat)
         (path (rgfi *rdi* x86))
         (statbuf (rgfi *rsi* x86))
         ((when (not (canonical-address-p path)))
          (!ms (list ctx
                     :syscall-lstat-path-ptr-not-canonical)
               x86))
         ((mv flg pathname x86)
          (read-string-zero-terminated path x86))
         ((when flg)
          (!ms (list ctx :path flg) x86))
         ((mv ret x86)
          (syscall-lstat pathname statbuf x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :oracle-val-for-syscall-lstat ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-lstat

(defthm x86p-of-x86-syscall-lstat
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-lstat x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-fstat

(defun x86-syscall-fstat (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-fstat))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-fstat)
         (fd (rgfi *rdi* x86))
         (statbuf (rgfi *rsi* x86))
         ((mv ret x86)
          (syscall-fstat fd statbuf x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-fstat

(defthm x86p-of-x86-syscall-fstat
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-fstat x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-fcntl

(defun x86-syscall-fcntl (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-fcntl))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-fcntl)
         (fd (rgfi *rdi* x86))
         (cmd (rgfi *rsi* x86))
         (arg (rgfi *rdx* x86))
         ((mv ret x86)
          (syscall-fcntl fd cmd arg x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-fcntl

(defthm x86p-of-x86-syscall-fcntl
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-fcntl x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-truncate

(defun x86-syscall-truncate (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-truncate))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-truncate)
         (path (rgfi *rdi* x86))
         (length (rgfi *rsi* x86))
         ((when (not (canonical-address-p path)))
          (!ms (list ctx
                     :syscall-truncate-path-ptr-not-canonical)
               x86))
         ((mv flg pathname x86)
          (read-string-zero-terminated path x86))
         ((when flg)
          (!ms (list ctx :path flg) x86))
         ((mv ret x86)
          (syscall-truncate pathname length x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :oracle-val-for-syscall-truncate ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-truncate

(defthm x86p-of-x86-syscall-truncate
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-truncate x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Function: x86-syscall-ftruncate

(defun x86-syscall-ftruncate (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-ftruncate))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-ftruncate)
         (fd (rgfi *rdi* x86))
         (length (rgfi *rsi* x86))
         ((mv ret x86)
          (syscall-ftruncate fd length x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :ret-val-or-ms-for-syscall-write ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-ftruncate

(defthm x86p-of-x86-syscall-ftruncate
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-ftruncate x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Subtopics

X86-syscall-link

X86-syscall-truncate

X86-syscall-unlink

X86-syscall-stat

X86-syscall-open

X86-syscall-lstat

X86-syscall-write

X86-syscall-read

X86-syscall-lseek

X86-syscall-ftruncate

X86-syscall-fstat

X86-syscall-fcntl

X86-syscall-fadvise64

X86-syscall-dup3

X86-syscall-dup2

X86-syscall-dup

X86-syscall-close