		Search-engine friendly clone of the ACL2 documentation.

Stack-pointer-operations

Add-to-*sp

Add a specified amount to a stack pointer.

Signature
(add-to-*sp proc-mode *sp delta x86) → (mv flg *sp+delta)
Returns: *sp+delta — Type (i64p *sp+delta).

The amount may be positive (increment) or negative (decrement). This just calculates the new stack pointer value, without storing it into the register RSP, ESP, or SP. The starting value is the result of read-*sp or a previous invocation of add-to-*sp.

The increment or decrement is modular: 64 bits in 64-bit mode, and either 32 or 16 bits in 32-bit mode (depending on the SS.B bit). Since our model uses signed 64-bit addresses, we use i64 for them, while we use n32 or n16 for 32-bit and 16-bit addresses.

In 64-bit mode, we check whether the result is a canonical address; in 32-bit mode, we check whether the result is within the segment limit. If these checks are not satisfied, this function returns an error flag (and 0 as new pointer), which causes the x86 model to stop execution with an error. It is not clear whether these checks should be performed when the stack pointer is updated, or when the stack is eventually accessed through the updated pointer; the Intel and AMD manuals seem unclear in this respect. But since the failure of these checks stops execution with an error, and it is in a way always ``safe'' to stop execution with an error (in the sense that the model provides no guarantees when this happens), for now we choose to perform these checks here.

Note that a stack segment may be expand-down or expand-up (see Intel manual, Mar'17, Vol. 3, Sec. 3.4.5.1), so the checks need to cover these two cases. See segment-base-and-bounds and ea-to-la.

Definitions and Theorems

Function: add-to-*sp$inline

(defun add-to-*sp$inline (proc-mode *sp delta x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 64) *sp)
          (type (signed-byte 64) delta))
 (b* ((*sp+delta (the (signed-byte 65) (+ *sp delta))))
  (case proc-mode
   (0 (let ((*sp+delta (i64 *sp+delta)))
        (if (mbe :logic (canonical-address-p *sp+delta)
                 :exec (and (<= -140737488355328 *sp+delta)
                            (< *sp+delta 140737488355328)))
            (mv nil *sp+delta)
          (mv (list :non-canonical-stack-address *sp+delta)
              0))))
   (1
     (b*
       (((the (unsigned-byte 32) ss.limit)
         (seg-hidden-limiti 2 x86))
        ((the (unsigned-byte 16) ss-attr)
         (seg-hidden-attri 2 x86))
        (ss.b (data-segment-descriptor-attributesbits->d/b ss-attr))
        (ss.e (data-segment-descriptor-attributesbits->e ss-attr))
        (ss-lower (if (= ss.e 1) (1+ ss.limit) 0))
        (ss-upper (if (= ss.e 1)
                      (if (= ss.b 1) 4294967295 65535)
                    ss.limit))
        (*sp+delta (if (= ss.b 1)
                       (n32 *sp+delta)
                     (n16 *sp+delta)))
        ((unless (and (<= ss-lower *sp+delta)
                      (<= *sp+delta ss-upper)))
         (mv (list :out-of-segment-stack-address
                   *sp+delta ss-lower ss-upper)
             0)))
       (mv nil *sp+delta)))
   (otherwise (mv (list :unimplemented-proc-mode proc-mode)
                  0)))))

Theorem: i64p-of-add-to-*sp.*sp+delta

(defthm i64p-of-add-to-*sp.*sp+delta
  (b* (((mv ?flg ?*sp+delta)
        (add-to-*sp$inline proc-mode *sp delta x86)))
    (i64p *sp+delta))
  :rule-classes :rewrite)

Theorem: add-to-*sp-is-i64p

(defthm add-to-*sp-is-i64p
 (signed-byte-p 48
                (mv-nth 1 (add-to-*sp proc-mode *sp delta x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (integerp (mv-nth 1 (add-to-*sp proc-mode *sp delta x86)))
      :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
    :corollary
    (and (<= -140737488355328
             (mv-nth 1 (add-to-*sp proc-mode *sp delta x86)))
         (< (mv-nth 1 (add-to-*sp proc-mode *sp delta x86))
            140737488355328))
    :hints
    (("Goal"
          :in-theory '(signed-byte-p integer-range-p (:e expt)))))))

Theorem: mv-nth-0-of-add-to-*sp-when-64-bit-modep

(defthm mv-nth-0-of-add-to-*sp-when-64-bit-modep
 (equal (mv-nth 0 (add-to-*sp 0 *sp delta x86))
        (if (canonical-address-p (i64 (+ *sp delta)))
            nil
          (list :non-canonical-stack-address (i64 (+ *sp delta))))))

Theorem: mv-nth-1-of-add-to-*sp-when-64-bit-modep

(defthm mv-nth-1-of-add-to-*sp-when-64-bit-modep
  (equal (mv-nth 1 (add-to-*sp 0 *sp delta x86))
         (if (canonical-address-p (i64 (+ *sp delta)))
             (i64 (+ *sp delta))
           0)))

Theorem: mv-nth-1-of-add-to-*sp-when-compatibility-modep

(defthm mv-nth-1-of-add-to-*sp-when-compatibility-modep
 (implies
    (and (not (equal proc-mode 0))
         (integerp (+ *sp delta))
         (not (mv-nth 0
                      (add-to-*sp proc-mode *sp delta x86))))
    (unsigned-byte-p 32
                     (mv-nth 1
                             (add-to-*sp proc-mode *sp delta x86))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies
           (and (not (equal proc-mode 0))
                (integerp (+ *sp delta))
                (not (mv-nth 0
                             (add-to-*sp proc-mode *sp delta x86))))
           (natp (mv-nth 1
                         (add-to-*sp proc-mode *sp delta x86))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies
        (and (not (equal proc-mode 0))
             (integerp (+ *sp delta))
             (not (mv-nth 0
                          (add-to-*sp proc-mode *sp delta x86))))
        (and (<= 0
                 (mv-nth 1 (add-to-*sp proc-mode *sp delta x86)))
             (< (mv-nth 1 (add-to-*sp proc-mode *sp delta x86))
                4294967296)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))