• 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
      • Running-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
            • Write-*ip
            • Add-to-*ip
            • Read-*ip
          • Stack-pointer-operations
          • 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

• Instruction-pointer-operations

Read-*ip

Read the instruction pointer from the register RIP, EIP, or IP.

Signature

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

Returns

*ip — Type (i48p *ip), given (x86p x86).

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

In 32-bit mode, a 32-bit or 16-bit instruction pointer is read from EIP (i.e. the low 32 bits of RIP) or IP (i.e. the low 16 bits of RIP), based on the CS.D bit, i.e. the D bit of the current code segment descriptor. Either way, this function returns an unsigned 32-bit or 16-bit integer, which is also a signed 48-bit integer.

See AMD manual, Oct'13, Vol. 1, Sec. 2.2.4 and Sec. 2.5. AMD manual, Apr'16, Vol. 2, Sec 4.7.2., and Intel manual, Mar'17, Vol. 1, Sec. 3.6.

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

Definitions and Theorems

Function: read-*ip$inline

(defun read-*ip$inline (proc-mode x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode))
 (b* ((*ip (the (signed-byte 48) (rip x86))))
  (case proc-mode
   (0 *ip)
   (1
    (b* (((the (unsigned-byte 16) cs-attr)
          (seg-hidden-attri 1 x86))
         (cs.d (code-segment-descriptor-attributesbits->d cs-attr)))
      (if (= cs.d 1) (n32 *ip) (n16 *ip))))
   (otherwise 0))))

Theorem: i48p-of-read-*ip

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

Theorem: read-*ip-is-i48p

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

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

(defthm read-*ip-when-64-bit-modep
  (equal (read-*ip 0 x86) (rip x86)))

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

(defthm read-*ip-when-not-64-bit-modep
 (implies (not (equal proc-mode 0))
          (unsigned-byte-p 32 (read-*ip proc-mode x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (not (equal proc-mode 0))
                          (natp (read-*ip 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-*ip proc-mode x86))
                            (< (read-*ip proc-mode x86)
                               4294967296)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))