		Search-engine friendly clone of the ACL2 documentation.

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