		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-pusha

PUSHA/PUSHAD: 60

Signature
(x86-pusha 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.

Note that the stack pointer is read twice: via read-*sp and via rgfi-size. The former is used as the address to write into the stack, while the latter is used as (part of) the data to write into the stack. In principle, the sizes of these two stack pointers may differ: the former's size is determined solely by CS.D, while the latter's size is also influenced by the operand size override prefix. It seems odd that the two sizes would differ, though.

We use some simple and repetitive code to write the registers into the stack. It may be possible to optimize it by pushing all the registers in one shot.

Definitions and Theorems

Function: x86-pusha

(defun x86-pusha (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-pusha))
   (declare (ignorable __function__))
   (b* ((?ctx 'x86-pusha))
     (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))
          (eax/ax (rgfi-size operand-size 0 0 x86))
          (ecx/cx (rgfi-size operand-size 1 0 x86))
          (edx/dx (rgfi-size operand-size 2 0 x86))
          (ebx/bx (rgfi-size operand-size 3 0 x86))
          (esp/sp (rgfi-size operand-size 4 0 x86))
          (ebp/bp (rgfi-size operand-size 5 0 x86))
          (esi/si (rgfi-size operand-size 6 0 x86))
          (edi/di (rgfi-size operand-size 7 0 x86))
          (check-alignment? (alignment-checking-enabled-p x86))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 eax/ax check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!ms-fresh :wme-size-opt flg))
          (check-alignment? nil)
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 ecx/cx check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 edx/dx check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 ebx/bx check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 esp/sp check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 ebp/bp check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 esi/si check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg rsp)
           (add-to-*sp proc-mode rsp (- operand-size)
                       x86))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          ((mv flg x86)
           (wme-size-opt proc-mode operand-size
                         rsp 2 edi/di check-alignment? x86
                         :mem-ptr? nil))
          ((when flg)
           (!!fault-fresh :ss 0 :push flg))
          (x86 (write-*sp proc-mode rsp x86))
          (x86 (write-*ip proc-mode temp-rip x86)))
       x86))))

Theorem: x86p-of-x86-pusha

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