		Search-engine friendly clone of the ACL2 documentation.

Stack-pointer-operations

Write-*sp

Write a stack pointer into the register RSP, ESP, or SP.

Signature
(write-*sp proc-mode *sp x86) → x86-new
Returns: x86-new — Type (x86p x86-new), given (x86p x86).

In 64-bit mode, a 64-bit stack pointer is written into the full RSP. Since, in the model, this is a 64-bit signed integer, this function consumes a 64-bit signed integer.

In 32-bit mode, the stack pointer is 32 or 16 bits based on the SS.B bit, i.e. the B bit of the current stack segment descriptor. In these cases, the argument to this function should be a 32-bit or 16-bit unsigned integer, which is also a 64-bit signed integer.

See Intel manual, Mar'17, Vol. 1, Sec. 6.2.3 and Sec. 6.2.5, and AMD manual, Apr'16, Vol. 2, Sec 2.4.5 and Sec. 4.7.3. The actual size of the value consumed by this function should be StackAddrSize, introduced in Intel manual, Mar'17, Vol. 2, Sec. 3.1.1.9.

The pseudocode of stack instructions like PUSH in Intel manual, Mar'17, Vol. 2 show assignments of the form RSP <- ..., ESP <- ..., and SP <- ... based on the stack address size. This may suggests that when the stack address size is 32 the assignment to ESP leaves the high 32 bits of RSP unchanged, and when the stack address size is 16 the assignment to SP leaves the high 48 bits of RSP unchanged. However, as explained in the documentation of wr32 and wr16, normally writing to the low 32 bits of a general-purpose register (which RSP/ESP/SP is) zeros the high 32 bits, while writing the low 16 bits leaves the high 48 bits unchanged. Thus, we follow this requirement also when writing RSP/ESP/SP implicitly, via stack manipulation instructions like PUSH that use this write-*sp function to update the stack pointer register.

This function should be always called with a stack pointer of the right type (64-bit signed, 32-bit unsigned, or 16-bit unsigned) based on the stack address size. We may add a guard to ensure that in the future, but for now in the code below we coerce the stack pointer to 32 and 16 bits as appropriate, to verify guards; these coercions are expected not to change the argument stack pointer.

Definitions and Theorems

Function: write-*sp$inline

(defun write-*sp$inline (proc-mode *sp x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 64) *sp))
 (declare (xargs :guard
                 (if (equal proc-mode 0)
                     t
                   (unsigned-byte-p 32 *sp))))
 (case proc-mode
  (0 (!rgfi 4 *sp x86))
  (1
    (b*
      (((the (unsigned-byte 16) ss-attr)
        (seg-hidden-attri 2 x86))
       (ss.b (data-segment-descriptor-attributesbits->d/b ss-attr)))
      (if (= ss.b 1)
          (mbe :logic (!rgfi 4 (n32 *sp) x86)
               :exec (!rgfi 4 (the (unsigned-byte 32) *sp)
                            x86))
        (b* (((the (signed-byte 64) rsp)
              (rgfi 4 x86))
             ((the (signed-byte 64) rsp-new)
              (mbe :logic (part-install (n16 *sp)
                                        rsp
                                        :low 0
                                        :width 16)
                   :exec (logior (logand -65536 rsp)
                                 (logand 65535 *sp)))))
          (!rgfi 4 rsp-new x86)))))
  (otherwise x86)))

Theorem: x86p-of-write-*sp

(defthm x86p-of-write-*sp
  (implies (x86p x86)
           (b* ((x86-new (write-*sp$inline proc-mode *sp x86)))
             (x86p x86-new)))
  :rule-classes :rewrite)

Theorem: write-*sp-when-64-bit-modep

(defthm write-*sp-when-64-bit-modep
  (equal (write-*sp 0 *sp x86)
         (!rgfi 4 *sp x86)))