		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-push-i

PUSH: 6A/68 ib/iw/id

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

6A ib: PUSH imm8

68 iw: PUSH imm16

68 id: PUSH imm32

From the description of the PUSH instruction (Intel Manual, Vol. 2, Section 4.2):

If the source operand is an immediate of size less than the operand size, a sign-extended value is pushed on the stack.

PUSH doesn't have a separate instruction semantic function, unlike other opcodes like ADD, SUB, etc. The decoding is coupled the decoding with the execution in this case.

Definitions and Theorems

Function: x86-push-i

(defun x86-push-i
       (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-i))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-push-i))
    (b*
     ((byte-imm? (eql opcode 106))
      ((the (integer 1 8) imm-size)
       (select-operand-size proc-mode byte-imm?
                            rex-byte t prefixes nil nil nil x86))
      ((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))
      ((mv flg0 (the (signed-byte 32) imm) x86)
       (rime-size-opt proc-mode
                      imm-size temp-rip 1 :x nil x86))
      ((when flg0)
       (!!ms-fresh :imm-rime-size-error flg0))
      ((mv flg (the (signed-byte 48) temp-rip))
       (add-to-*ip proc-mode temp-rip imm-size x86))
      ((when flg)
       (!!fault-fresh :gp 0
                      :temp-rip-not-canonical temp-rip))
      (badlength? (check-instruction-length start-rip temp-rip 0))
      ((when badlength?)
       (!!fault-fresh :gp 0
                      :instruction-length badlength?))
      ((mv flg1 x86)
       (wme-size-opt proc-mode operand-size new-rsp 2
                     (mbe :logic (loghead (ash operand-size 3) imm)
                          :exec (logand (case operand-size
                                          (2 65535)
                                          (4 4294967295)
                                          (8 18446744073709551615))
                                        (the (signed-byte 32) imm)))
                     (alignment-checking-enabled-p x86)
                     x86
                     :mem-ptr? nil))
      ((when flg1)
       (!!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-i

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