		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-sysret

Return from fast system call to user code at privilege level 3

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

Op/En: NP
0F 07: SYSRET
REX.W + 0F 07: SYSRET

SYSRET when REX.W is not set is not supported yet because 0F 07 (as opposed to REX.W + 0F 07) switches the machine to compatibility mode, not 64-bit mode.

Definitions and Theorems

Function: x86-sysret

(defun x86-sysret
       (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-sysret))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-sysret))
   (b*
    (((when (not (logbitp 3 rex-byte)))
      (!!ms-fresh :unsupported-sysret-because-rex.w!=1 rex-byte))
     (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)))
     (current-cs-register (the (unsigned-byte 16)
                               (seg-visiblei 1 x86)))
     (cpl (segment-selectorbits->rpl current-cs-register))
     ((when (not (equal 0 cpl)))
      (!!fault-fresh :gp 0
                     :cpl!=0 (cons 'cs-register
                                   current-cs-register)))
     (rcx (rgfi *rcx* x86))
     ((when (not (canonical-address-p rcx)))
      (!!ms-fresh :rcx-non-canonical rcx))
     (x86 (!rip rcx x86))
     (r11 (n32 (rgfi *r11* x86)))
     (x86 (!rflags (logior (logand r11 3964887) 2)
                   x86))
     (star (msri *ia32_star-idx* x86))
     (new-cs-selector (+ (part-select star :low 48 :high 63)
                         16))
     ((when (not (n16p new-cs-selector)))
      (!!ms-fresh :new-cs-selector-too-large new-cs-selector))
     (new-cs-selector
          (!segment-selectorbits->rpl 3 new-cs-selector))
     (x86 (!seg-visiblei 1 new-cs-selector x86))
     (cs-base-addr 0)
     (cs-limit 4294967295)
     ((the (unsigned-byte 16) cs-attr)
      (seg-hidden-attri 1 x86))
     (cs-attr
       (change-code-segment-descriptor-attributesbits cs-attr
                                                      :a 1
                                                      :r 1
                                                      :c 0
                                                      :msb-of-type 1
                                                      :s 1
                                                      :dpl 3
                                                      :p 1
                                                      :l 1
                                                      :d 0
                                                      :g 1))
     (x86 (!seg-hidden-basei 1 cs-base-addr x86))
     (x86 (!seg-hidden-limiti 1 cs-limit x86))
     (x86 (!seg-hidden-attri 1 cs-attr x86))
     (new-ss-selector (+ (part-select star :low 48 :high 63)
                         8))
     ((when (not (n16p new-ss-selector)))
      (!!ms-fresh :new-ss-selector-too-large new-ss-selector))
     (new-ss-selector
          (!segment-selectorbits->rpl 3 new-ss-selector))
     (x86 (!seg-visiblei 2 new-ss-selector x86))
     (ss-base-addr 0)
     (ss-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 3
                                                      :p 1
                                                      :d/b 1
                                                      :g 1))
     (x86 (!seg-hidden-basei 2 ss-base-addr x86))
     (x86 (!seg-hidden-limiti 2 ss-limit x86))
     (x86 (!seg-hidden-attri 2 ss-attr x86)))
    x86))))

Theorem: x86p-of-x86-sysret

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