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

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

X86-syscall-truncate

X86-syscall-stat

X86-syscall-open

X86-syscall-lstat

X86-syscall-write

X86-syscall-lseek

X86-syscall-ftruncate

X86-syscall-fadvise64

X86-syscall-read

X86-syscall-fstat

X86-syscall-fcntl

X86-syscall-dup3

X86-syscall-dup2

X86-syscall-dup

X86-syscall-close