• 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

• Decoding-and-spec-utils

Instruction-pointer-operations

Operations to manipulate instruction pointers.

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

Function: add-to-*ip$inline

(defun add-to-*ip$inline (proc-mode *ip delta x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (integer 0 4) proc-mode)
           (type (signed-byte 48) *ip)
           (type (signed-byte 48) delta))
  (b* ((*ip+delta (the (signed-byte 49) (+ *ip delta))))
    (case proc-mode
      (0 (if (mbe :logic (canonical-address-p *ip+delta)
                  :exec (and (<= -140737488355328 *ip+delta)
                             (< *ip+delta 140737488355328)))
             (mv nil *ip+delta)
           (mv (list :non-canonical-instruction-pointer *ip+delta)
               0)))
      (1 (b* (((the (unsigned-byte 32) cs.limit)
               (mbe :logic (loghead 32 (seg-hidden-limiti 1 x86))
                    :exec (seg-hidden-limiti 1 x86))))
           (if (and (<= 0 *ip+delta)
                    (<= *ip+delta cs.limit))
               (mv nil (the (unsigned-byte 32) *ip+delta))
             (mv (list :out-of-segment-instruction-pointer
                       cs.limit *ip+delta)
                 0))))
      (otherwise (mv (list :unimplemented-proc-mode proc-mode)
                     0)))))

Theorem: i48p-of-add-to-*ip.*ip+delta

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

Theorem: add-to-*ip-is-i48p

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

Theorem: add-to-*ip-is-i48p-rewrite-rule

(defthm add-to-*ip-is-i48p-rewrite-rule
 (implies
  (and (integerp *ip)
       (<= -140737488355328 *ip)
       (< *ip 140737488355328)
       (integerp delta))
  (and
    (integerp (mv-nth 1 (add-to-*ip proc-mode *ip delta x86)))
    (rationalp (mv-nth 1 (add-to-*ip proc-mode *ip delta x86)))
    (<= -140737488355328
        (mv-nth 1 (add-to-*ip proc-mode *ip delta x86)))
    (< (mv-nth 1 (add-to-*ip proc-mode *ip delta x86))
       140737488355328)
    (signed-byte-p 48
                   (mv-nth 1 (add-to-*ip proc-mode *ip delta x86)))
    (signed-byte-p 64
                   (mv-nth 1
                           (add-to-*ip proc-mode *ip delta x86))))))

Theorem: add-to-*ip-rationalp-type

(defthm add-to-*ip-rationalp-type
 (implies (and (rationalp *ip) (rationalp delta))
          (rationalp (mv-nth 1
                             (add-to-*ip proc-mode *ip delta x86))))
 :rule-classes :type-prescription)

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

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

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

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

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

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

Function: write-*ip$inline

(defun write-*ip$inline (proc-mode *ip x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 48) *ip))
 (declare (xargs :guard
                 (if (equal proc-mode 0)
                     t
                   (unsigned-byte-p 32 *ip))))
 (case proc-mode
  (0 (!rip *ip x86))
  (1
    (b* ((cs-attr (the (unsigned-byte 16)
                       (seg-hidden-attri 1 x86)))
         (cs.d (code-segment-descriptor-attributesbits->d cs-attr)))
      (if (= cs.d 1)
          (mbe :logic (!rip (n32 *ip) x86)
               :exec (!rip (the (unsigned-byte 32) *ip) x86))
        (b* ((rip (the (signed-byte 48) (rip x86)))
             ((the (signed-byte 48) rip-new)
              (mbe :logic (part-install (n16 *ip)
                                        rip
                                        :low 0
                                        :width 16)
                   :exec (logior (logand -65536 rip)
                                 (logand 65535 *ip)))))
          (!rip rip-new x86)))))
  (otherwise x86)))

Theorem: x86p-of-write-*ip

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

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

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

Subtopics

Write-*ip

Write an instruction pointer into the register RIP, EIP, or IP.

Add-to-*ip

Add a specified amount to an instruction pointer.

Read-*ip

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