		Search-engine friendly clone of the ACL2 documentation.

Instruction-pointer-operations

Write-*ip

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

Signature
(write-*ip proc-mode *ip x86) → x86-new
Returns: x86-new — Type (x86p x86-new), given (x86p x86).

In 64-bit mode, a 64-bit instruction pointer is written into the full RIP. Since, in the model, this is a 48-bit signed integer, this function consumes a 48-bit signed integer.

In 32-bit mode, the instruction pointer is 32 or 16 bits based on the CS.D bit, i.e. the D bit of the current code segment descriptor. In these cases, the argument to this function should be a 32-bit or 16-bit unsigned integer, which is also a 48-bit signed 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.

According to Intel manual, Mar'17, Vol. 1, Table 3-1, it seems that when writing a 32-bit instruction pointer (EIP) the high 32 bits of RIP should be set to 0, and when writing a 16-bit instruction pointer (IP) the high 48 bits of RIP should be left unmodified; since in our model the RIP is 48 bits, the above applies to the high 16 and 32 bits, respectively. The pseudocode for the JMP instruction in Intel manual, Mar'17, Vol. 2 shows an assignment EIP <- tempEIP AND 0000FFFFh for the 16-bit case, which seems to imply that the high 32 (or 16, in our model) bits are left unmodified and the high 16 bits of EIP are set to 0, which would contradict Table 3-1; the pseudocode for some other instructions that directly write the instruction pointer (e.g. RET and Jcc) show similar assignments. However, it is possible that this assignment has a typo and should be IP <- tempEIP AND 0000FFFFh instead, which would be consistent with Table 3-1. But we also note that the pseudocode for the JMP instruction shows an assignment EIP <- tempEIP for the 32-bit case, which seems to imply that the high 32 (or 16, in our model) bits are left unmodified, which would contradict Table 3-1. The AMD manuals do not show pseudocode for these instructions, and AMD manual, Oct'13, Vol. 1, Fig. 2-10 (which is somewhat analogous to Intel's Table 3-1) shows the high bits simply grayed out; so the AMD manuals do not provide disambiguation help. It is also possible that Table 3-1 has a typo and should say that a 16-bit instruction pointer is zero-extended, but that is not quite consistent with the pseudocode assignments to EIP, which seem to imply that the high bits are untouched. Table 3-1 is under a section titled `Address Calculation in 64-Bit Mode', which may suggest that the table may not apply to 32-bit mode, but then it is not clear how it would just apply to 64-bit mode. For now, we decide to have this function follow Intel's Table 3-1, but we may revise that if we manage to resolve these ambiguities. We also note that Intel's Table 3-1 is consistent with the way in which 32-bit and 16-bit values are written to general-purpose registers (even though RIP/EIP/IP is not a general-purpose register); see wr32 and wr16.

This function should be always called with an instruction pointer of the right type (48-bit signed, 32-bit unsigned, or 16-bit unsigned) based on the mode and code segment. We may add a guard to ensure that in the future, but for now in the code below we coerce the instruction pointer to 32 and 16 bits as appropriate, to verify guards; these coercions are expected not to change the argument instruction pointer.

Definitions and Theorems

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