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

• Stack-pointer-operations

Read-*sp

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

Signature

(read-*sp proc-mode x86) → *sp

Returns

*sp — Type (i64p *sp), given (x86p x86).

In 64-bit mode, a 64-bit stack pointer is read from the full RSP. Since, in the model, this is a 64-bit signed integer, this function returns a 64-bit signed integer.

In 32-bit mode, a 32-bit or 16-bit stack pointer is read from ESP (i.e. the low 32 bits of RSP) or SP (i.e. the low 16 bits of RSP), based on the SS.B bit, i.e. the B bit of the current stack segment register. Either way, this function returns an unsigned 32-bit or 16-bit integer, which is also a signed 64-bit integer.

See Intel manual, Mar'23, Vol. 1, Sec. 6.2.3 and Sec. 6.2.5, and AMD manual, Jun'23, Vol. 2, Sec 2.4.5 and Sec. 4.7.3. The actual size of the value returned by this function is StackAddrSize, introduced in Intel manual, Dec'23, Vol. 2, Sec. 3.1.1.9.

In 32-bit mode, the address-size override prefix (if present) should not affect the stack address size. It does not seem to make sense to change the stack address size on a per-instruction basis.

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