|
|
|---|
|
|
|
|---|
Effective address calculation with 32-bit and 64-bit addressing.
(x86-effective-addr-32/64 proc-mode p4 temp-rip
rex-byte r/m mod sib num-imm-bytes x86)
→
(mv flg i64p-memory-address increment-rip-by x86)Note that we do not add segment bases (such as the FS and GS bases, if FS and GS overrides are present) to the effective address computed in this function. Addition of those segment base addresses is a part of the segmentation process --- we handle that in the function ea-to-la that performs the segment address translation.
Quoting from Intel Vol 1, Sec 3.3.7:
In 64-bit mode, the effective address components are added and the effective address is truncated (See for example the instruction LEA) before adding the full 64-bit segment base. The base is never truncated, regardless of addressing mode in 64-bit mode.
Quoting Intel Vol. 1 Sec. 3.3.7 (Address Calculations in 64-Bit Mode):
All 16-bit and 32-bit address calculations are zero-extended in IA-32e mode to form 64-bit addresses. Address calculations are first truncated to the effective address size of the current mode (64-bit mode or compatibility mode), as overridden by any address-size prefix. The result is then zero-extended to the full 64-bit address width. Because of this, 16-bit and 32-bit applications running in compatibility mode can access only the low 4 GBytes of the 64-bit mode effective addresses. Likewise, a 32-bit address generated in 64-bit mode can access only the low 4 GBytes of the 64-bit mode effective addresses.
Also: Intel Vol 1, Section 3.3.7 says that we need sign-extended displacements in effective address calculations. In Lisp, sign-extension is implicit.
In 64-bit mode, instructions such as LEA use this function to compute the effective address. LEA, at least, does not check whether the generated address is canonical or not, which is why we don't make the canonical-address-p check in this function.
In 64-bit mode,
we use
Function:
(defun x86-effective-addr-32/64 (proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 4) proc-mode) (type (signed-byte 48) temp-rip) (type (unsigned-byte 8) rex-byte) (type (unsigned-byte 3) r/m) (type (unsigned-byte 2) mod) (type (unsigned-byte 8) sib) (type (unsigned-byte 3) num-imm-bytes)) (declare (xargs :guard (and (2bits-p mod) (3bits-p r/m) (sib-p sib)))) (let ((__function__ 'x86-effective-addr-32/64)) (declare (ignorable __function__)) (b* (((mv flg addr displacement increment-rip-by x86) (case mod (0 (case r/m (4 (x86-effective-addr-from-sib proc-mode temp-rip rex-byte mod sib x86)) (5 (if (equal proc-mode 0) (b* (((mv ?flg0 dword x86) (rime-size-opt 0 4 temp-rip 1 :x nil x86 :mem-ptr? nil)) ((mv flg next-rip) (add-to-*ip 0 temp-rip (+ 4 num-imm-bytes) x86)) ((when flg) (mv flg 0 0 0 x86))) (mv flg0 next-rip dword 4 x86)) (b* (((mv flg dword x86) (rime-size-opt proc-mode 4 temp-rip 1 :x nil x86 :mem-ptr? nil)) ((when flg) (mv flg 0 0 0 x86))) (mv nil 0 dword 4 x86)))) (otherwise (mv nil (if (equal proc-mode 0) (rgfi (reg-index r/m rex-byte 0) x86) (rr32 r/m x86)) 0 0 x86)))) (1 (case r/m (4 (x86-effective-addr-from-sib proc-mode temp-rip rex-byte mod sib x86)) (otherwise (b* (((mv ?flg2 byte2 x86) (rime-size-opt proc-mode 1 temp-rip 1 :x nil x86 :mem-ptr? nil)) (reg (if (equal proc-mode 0) (rgfi (reg-index r/m rex-byte 0) x86) (rr32 r/m x86)))) (mv flg2 reg byte2 1 x86))))) (2 (case r/m (4 (x86-effective-addr-from-sib proc-mode temp-rip rex-byte mod sib x86)) (otherwise (b* (((mv ?flg1 dword x86) (rime-size-opt proc-mode 4 temp-rip 1 :x nil x86 :mem-ptr? nil)) (reg (if (equal proc-mode 0) (rgfi (reg-index r/m rex-byte 0) x86) (rr32 r/m x86)))) (mv flg1 reg dword 4 x86))))) (otherwise (mv 'mod-value-wrong 0 0 0 x86)))) (dst-base (+ addr displacement)) (dst-base (if (equal proc-mode 0) (if p4 (n32 dst-base) (n64-to-i64 (n64 dst-base))) (n32 dst-base)))) (mv flg dst-base increment-rip-by x86))))
Theorem:
(defthm x86p-of-x86-effective-addr-32/64.x86 (implies (force (x86p x86)) (b* (((mv ?flg ?i64p-memory-address ?increment-rip-by ?x86) (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (x86p x86))) :rule-classes :rewrite)
Theorem:
(defthm i64p-mv-nth-1-x86-effective-addr-32/64 (signed-byte-p 64 (mv-nth 1 (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) :rule-classes (:rewrite (:type-prescription :corollary (integerp (mv-nth 1 (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) :hints (("Goal" :in-theory '(signed-byte-p integer-range-p)))) (:linear :corollary (and (<= -9223372036854775808 (mv-nth 1 (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (< (mv-nth 1 (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)) 9223372036854775808)) :hints (("Goal" :in-theory '(signed-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm natp-mv-nth-2-x86-effective-addr-32/64 (natp (mv-nth 2 (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) :rule-classes :type-prescription)
Theorem:
(defthm mv-nth-2-x86-effective-addr-32/64-<=-4 (<= (mv-nth 2 (x86-effective-addr-32/64 proc-mode p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)) 4) :rule-classes :linear)