• 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

Add-to-*ip

Add a specified amount to an instruction pointer.

Signature

(add-to-*ip proc-mode *ip delta x86) → (mv flg *ip+delta)

Returns

*ip+delta — Type (i48p *ip+delta), given (and (i48p *ip) (i48p delta)).

The amount may be positive (increment) or negative (decrement). This just calculates the new instruction pointer value, without storing it into the register RIP, EIP, or IP. The starting value is the result of read-*ip or a previous invocation of add-to-*ip.

In 64-bit mode, we check whether the result is a canonical address; in 32-bit mode, we check whether the result is within the segment limit. If these checks are not satisfied, this function returns an error flag (and 0 as incremented address), which causes the x86 model to stop execution with an error. It is not clear whether these checks should be performed when the instruction pointer is incremented or when an instruction byte is eventually accessed; the Intel and AMD manuals seem unclear in this respect. But since the failure of these checks stops execution with an error, and it is in a way always ``safe'' to stop execution with an error (in the sense that the model provides no guarantees when this happens), for now we choose to perform these checks here.

Note that a code segment is never expand-down, so the valid effective addresses are always between 0 and the segment limit (cf. segment-base-and-bounds).

Definitions and Theorems

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