		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-syscall

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

Definitions and Theorems

Function: x86-syscall

(defun x86-syscall
       (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))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-syscall))
   (b*
    ((ia32-efer (n12 (msri 0 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)))
     ((the (unsigned-byte 16) cs-attr)
      (seg-hidden-attri 1 x86))
     (x86 (!rgfi 1 temp-rip x86))
     (lstar (msri 5 x86))
     (lstar-addr (n64-to-i64 lstar))
     ((when (not (canonical-address-p lstar-addr)))
      (!!ms-fresh :lstar-not-canonical lstar))
     (x86 (!rip lstar-addr x86))
     ((the (unsigned-byte 32) eflags)
      (rflags x86))
     (x86 (wr64 11 eflags x86))
     (fmask (msri 6 x86))
     (not-fmask (lognot fmask))
     (new-eflags (the (unsigned-byte 32)
                      (logand eflags not-fmask)))
     (x86 (!rflags new-eflags x86))
     (star (msri 4 x86))
     (new-cs-selector
          (the (unsigned-byte 16)
               (logand (part-select star :low 32 :high 47)
                       65532)))
     (x86 (!seg-visiblei 1 new-cs-selector x86))
     (cs-hidden-base-addr 0)
     (cs-hidden-limit 4294967295)
     (cs-attr
       (change-code-segment-descriptor-attributesbits cs-attr
                                                      :a 1
                                                      :r 1
                                                      :c 0
                                                      :msb-of-type 1
                                                      :s 1
                                                      :dpl 0
                                                      :p 1
                                                      :l 1
                                                      :d 0
                                                      :g 1))
     (x86 (!seg-hidden-basei 1 cs-hidden-base-addr x86))
     (x86 (!seg-hidden-limiti 1 cs-hidden-limit x86))
     (x86 (!seg-hidden-attri 1 cs-attr x86))
     (new-ss-selector (+ (part-select star :low 32 :high 47)
                         8))
     ((when (not (n16p new-ss-selector)))
      (!!ms-fresh :new-ss-selector-too-large new-ss-selector))
     (x86 (!seg-visiblei 2 new-ss-selector x86))
     (ss-hidden-base-addr 0)
     (ss-hidden-limit 4294967295)
     ((the (unsigned-byte 16) ss-attr)
      (seg-hidden-attri 2 x86))
     (ss-attr
       (change-data-segment-descriptor-attributesbits ss-attr
                                                      :a 1
                                                      :w 1
                                                      :e 0
                                                      :msb-of-type 0
                                                      :s 1
                                                      :dpl 0
                                                      :p 1
                                                      :d/b 1
                                                      :g 1))
     (x86 (!seg-hidden-basei 2 ss-hidden-base-addr x86))
     (x86 (!seg-hidden-limiti 2 ss-hidden-limit x86))
     (x86 (!seg-hidden-attri 2 ss-attr x86)))
    x86))))

Theorem: x86p-of-x86-syscall

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