		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-pop-ev

POP: 8F/0 r/m

Signature
(x86-pop-ev 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: M

8F/0 r/m16/32/64

Note that 8F/0 r/m32 is N.E. in 64-bit mode and that 8F/0 r/m64 is N.E. in 32-bit mode.

POP does not have a separate instruction semantic function, unlike other opcodes like ADD, SUB, etc. The decoding is coupled with the execution in this case.

This opcode belongs to Group 1A, and it has an opcode extension (ModR/m.reg = 0).

Definitions and Theorems

Function: x86-pop-ev

(defun x86-pop-ev
       (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-pop-ev))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-pop-ev)
       (?r/m (the (unsigned-byte 3)
                  (modr/m->r/m modr/m)))
       (?mod (the (unsigned-byte 2)
                  (modr/m->mod modr/m)))
       (?reg (the (unsigned-byte 3)
                  (modr/m->reg modr/m))))
   (b*
    ((p2 (prefixes->seg prefixes))
     (p4? (equal 103 (prefixes->adr prefixes)))
     ((the (integer 1 8) operand-size)
      (select-operand-size proc-mode
                           nil rex-byte nil prefixes t t nil x86))
     (rsp (read-*sp proc-mode x86))
     ((mv flg new-rsp)
      (add-to-*sp proc-mode rsp operand-size x86))
     ((when flg)
      (!!fault-fresh :ss 0 :pop flg))
     (check-alignment? (alignment-checking-enabled-p x86))
     ((mv flg0 val x86)
      (rme-size-opt proc-mode operand-size
                    rsp 2 :r check-alignment? x86
                    :mem-ptr? nil
                    :check-canonicity t))
     ((when flg0)
      (!!ms-fresh :rme-size-opt flg))
     ((mv flg1 (the (signed-byte 64) addr)
          (the (unsigned-byte 3) increment-rip-by)
          x86)
      (if (equal mod 3)
          (mv nil 0 0 x86)
        (x86-effective-addr proc-mode p4?
                            temp-rip rex-byte r/m mod sib 0 x86)))
     ((when flg1)
      (!!ms-fresh :x86-effective-addr-error flg1))
     (seg-reg
         (select-segment-register proc-mode p2 p4? mod r/m sib x86))
     (badlength? (check-instruction-length start-rip temp-rip 0))
     ((when badlength?)
      (!!fault-fresh :gp 0
                     :instruction-length badlength?))
     (x86 (write-*sp proc-mode new-rsp x86))
     ((mv flg1 (the (signed-byte 64) addr)
          (the (unsigned-byte 3) increment-rip-by)
          x86)
      (if (equal mod 3)
          (mv nil 0 0 x86)
        (x86-effective-addr proc-mode p4?
                            temp-rip rex-byte r/m mod sib 0 x86)))
     ((when flg1)
      (!!ms-fresh :x86-effective-addr-error flg1))
     ((mv flg temp-rip)
      (add-to-*ip proc-mode
                  temp-rip increment-rip-by x86))
     ((when flg)
      (!!fault-fresh :gp 0
                     :increment-ip-error flg))
     ((mv flg3 x86)
      (x86-operand-to-reg/mem
           proc-mode
           operand-size check-alignment? nil
           val seg-reg addr rex-byte r/m mod x86))
     ((when flg3)
      (!!ms-fresh :x86-operand-to-reg/mem flg3))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-pop-ev

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