		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-syscall-app-view

Signature
(x86-syscall-app-view proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Returns: x86 — Type (x86p x86), given (and (x86p x86) (app-view x86)).

Definitions and Theorems

Function: x86-syscall-app-view

(defun x86-syscall-app-view
       (proc-mode start-rip temp-rip
                  prefixes rex-byte opcode modr/m sib x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 48) start-rip)
          (type (signed-byte 48) temp-rip)
          (type (unsigned-byte 52) prefixes)
          (type (unsigned-byte 8) rex-byte)
          (type (unsigned-byte 8) opcode)
          (type (unsigned-byte 8) modr/m)
          (type (unsigned-byte 8) sib))
 (declare (ignorable proc-mode start-rip temp-rip
                     prefixes rex-byte opcode modr/m sib))
 (declare (xargs :guard (and (prefixes-p prefixes)
                             (modr/m-p modr/m)
                             (sib-p sib)
                             (rip-guard-okp proc-mode temp-rip))))
 (let ((__function__ 'x86-syscall-app-view))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-syscall-app-view))
   (b*
    ((ia32-efer (n12 (msri *ia32_efer-idx* x86)))
     ((the (unsigned-byte 1) ia32-efer-sce)
      (ia32_eferbits->sce ia32-efer))
     ((when (mbe :logic (zp ia32-efer-sce)
                 :exec (equal 0 ia32-efer-sce)))
      (!!fault-fresh :ud nil
                     :ia32-efer-sce=0 (cons 'ia32_efer ia32-efer)))
     (x86 (!rgfi *rcx* temp-rip x86))
     ((the (unsigned-byte 32) eflags)
      (rflags x86))
     (x86 (wr64 *r11* (!rflagsbits->tf 1 eflags)
                x86))
     (rax (rr64 *rax* x86))
     ((the (unsigned-byte 32) eax) (n32 rax))
     (x86
        (cond ((equal eax (sys_read-idx x86))
               (x86-syscall-read x86))
              ((equal eax (sys_write-idx x86))
               (x86-syscall-write x86))
              ((equal eax (sys_open-idx x86))
               (x86-syscall-open x86))
              ((equal eax (sys_close-idx x86))
               (x86-syscall-close x86))
              ((equal eax (sys_stat-idx x86))
               (x86-syscall-stat x86))
              ((equal eax (sys_lstat-idx x86))
               (x86-syscall-lstat x86))
              ((equal eax (sys_fstat-idx x86))
               (x86-syscall-fstat x86))
              ((equal eax (sys_lseek-idx x86))
               (x86-syscall-lseek x86))
              ((equal eax (sys_dup-idx x86))
               (x86-syscall-dup x86))
              ((equal eax (sys_dup2-idx x86))
               (x86-syscall-dup2 x86))
              ((equal eax (sys_fcntl-idx x86))
               (x86-syscall-fcntl x86))
              ((equal eax (sys_truncate-idx x86))
               (x86-syscall-truncate x86))
              ((equal eax (sys_ftruncate-idx x86))
               (x86-syscall-ftruncate x86))
              ((equal eax (sys_link-idx x86))
               (x86-syscall-link x86))
              ((equal eax (sys_unlink-idx x86))
               (x86-syscall-unlink x86))
              ((equal eax (sys_fadvise64-idx x86))
               (x86-syscall-fadvise64 x86))
              ((equal eax (sys_dup3-idx x86))
               (x86-syscall-dup3 x86))
              (t (let* ((x86 (!ms (list "Unimplemented syscall" 'rax
                                        rax 'rip
                                        (rip x86))
                                  x86)))
                   x86))))
     ((when (ms x86))
      (!!ms-fresh :x86-syscall (ms x86)))
     (eflags (!rflagsbits->rf 0 eflags))
     (eflags (!rflagsbits->vm 0 eflags))
     (eflags (!rflagsbits->pf 1 eflags))
     (x86 (!rflags eflags x86))
     (x86 (!rip temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-syscall-app-view

(defthm x86p-of-x86-syscall-app-view
 (implies
  (and (x86p x86) (app-view x86))
  (b*
   ((x86 (x86-syscall-app-view proc-mode start-rip temp-rip prefixes
                               rex-byte opcode modr/m sib x86)))
   (x86p x86)))
 :rule-classes :rewrite)