• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
          • Effective-address-computations
          • Read-operands-and-write-results
          • Instruction-pointer-operations
          • Select-operand-size
          • Stack-pointer-operations
            • Add-to-*sp
            • Write-*sp
            • Read-*sp
          • Select-segment-register
          • Prefix-modrm-sib-decoding
          • Select-address-size
          • Check-instruction-length
          • Error-objects
          • Rip-guard-okp
          • Sib-decoding
        • Instructions
        • X86-modes
        • Segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Decoding-and-spec-utils

Stack-pointer-operations

Operations to manipulate stack pointers.

Definitions and Theorems

Function: read-*sp$inline

(defun
 read-*sp$inline (proc-mode x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode))
 (b*
  ((*sp (the (signed-byte 64) (rgfi 4 x86))))
  (case
   proc-mode (0 *sp)
   (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) (n32 *sp) (n16 *sp))))
   (otherwise 0))))

Theorem: i64p-of-read-*sp

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

Theorem: read-*sp-is-i64p

(defthm
 read-*sp-is-i64p
 (implies (x86p x86)
          (signed-byte-p 64 (read-*sp proc-mode x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (x86p x86)
                          (integerp (read-*sp proc-mode x86)))
      :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
    :corollary (implies (x86p x86)
                        (and (<= -9223372036854775808
                                 (read-*sp proc-mode x86))
                             (< (read-*sp proc-mode x86)
                                9223372036854775808)))
    :hints
    (("Goal"
          :in-theory '(signed-byte-p integer-range-p (:e expt)))))))

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

(defthm read-*sp-when-64-bit-modep
        (equal (read-*sp 0 x86)
               (rgfi *rsp* x86)))

Theorem: read-*sp-when-not-64-bit-modep

(defthm
 read-*sp-when-not-64-bit-modep
 (implies (not (equal proc-mode 0))
          (unsigned-byte-p 32 (read-*sp proc-mode x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (not (equal proc-mode 0))
                          (natp (read-*sp proc-mode x86)))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (implies (not (equal proc-mode 0))
                       (and (<= 0 (read-*sp proc-mode x86))
                            (< (read-*sp proc-mode x86)
                               4294967296)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

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)))))))

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)))

Subtopics

Add-to-*sp

Add a specified amount to a stack pointer.

Write-*sp

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

Read-*sp

Read the stack pointer from the register RSP, ESP, or SP.