		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-popa

POPA/POPD: 61

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

In 64-bit mode, this instruction is invalid; it throws a #UD exception.

We use some simple and repetitive code to read the registers from the stack. It may be possible to optimize it by popping all the registers in one shot.

Definitions and Theorems

Function: x86-popa

(defun x86-popa (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)
                             (not (equal proc-mode 0)))))
 (let ((__function__ 'x86-popa))
   (declare (ignorable __function__))
   (b* ((?ctx 'x86-popa))
     (b* (((the (integer 2 4) operand-size)
           (select-operand-size proc-mode
                                nil 0 nil prefixes nil nil nil x86))
          (rsp (read-*sp proc-mode x86))
          (check-alignment? (alignment-checking-enabled-p x86))
          ((mv flg edi/di x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (cond ((and (consp flg)
                       (eql (car flg) :non-canonical-address))
                  (!!fault-fresh :ss 0 :pop flg))
                 ((and (consp flg)
                       (eql (car flg)
                            :unaligned-linear-address))
                  (!!fault-fresh :ac 0 :pop flg))
                 (t (!!fault-fresh flg))))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          (check-alignment? nil)
          ((mv flg esi/si x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg ebp/bp x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg ebx/bx x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg edx/dx x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg ecx/cx x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg eax/ax x86)
           (rme-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp operand-size x86))
          ((when flg)
           (!!fault-fresh :ss 0 :pop flg))
          (x86 (!rgfi-size operand-size 7 edi/di 0 x86))
          (x86 (!rgfi-size operand-size 6 esi/si 0 x86))
          (x86 (!rgfi-size operand-size 5 ebp/bp 0 x86))
          (x86 (!rgfi-size operand-size 3 ebx/bx 0 x86))
          (x86 (!rgfi-size operand-size 2 edx/dx 0 x86))
          (x86 (!rgfi-size operand-size 1 ecx/cx 0 x86))
          (x86 (!rgfi-size operand-size 0 eax/ax 0 x86))
          (x86 (write-*sp proc-mode rsp x86))
          (x86 (write-*ip proc-mode temp-rip x86)))
       x86))))

Theorem: x86p-of-x86-popa

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