		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-push-ev

PUSH: FF /6 r/m

Signature
(x86-push-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

FF /6 r/m16/32/64

Note that FF/6 r/m32 is N.E. in 64-bit mode and that FF/6 r/m64 is N.E. in 32-bit mode.

PUSH 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 5, and it has an opcode extension (ModR/m.reg = 6).

Definitions and Theorems

Function: x86-push-ev

(defun x86-push-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-push-ev))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-push-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? (eql 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 :push flg))
     (seg-reg
         (select-segment-register proc-mode p2 p4? mod r/m sib x86))
     ((mv flg0 e
          (the (unsigned-byte 3) increment-rip-by)
          ?e-addr x86)
      (x86-operand-from-modr/m-and-sib-bytes
           proc-mode
           0 operand-size t nil seg-reg p4?
           temp-rip rex-byte r/m mod sib 0 x86))
     ((when flg0)
      (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg0))
     ((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))
     (badlength? (check-instruction-length start-rip temp-rip 0))
     ((when badlength?)
      (!!fault-fresh :gp 0
                     :instruction-length badlength?))
     ((mv flg x86)
      (wme-size-opt proc-mode operand-size
                    (the (signed-byte 48) new-rsp)
                    2 e (alignment-checking-enabled-p x86)
                    x86
                    :mem-ptr? nil))
     ((when flg)
      (!!ms-fresh :wme-size-opt flg))
     (x86 (write-*sp proc-mode new-rsp x86))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-push-ev

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