Read an operand from memory or a register.
(x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86) → (mv flg operand increment-rip-by addr x86)
Based on the ModR/M byte, the operand is read from either a register or memory. In the latter case, we calculate the effective address and then we read the operand from it. Besides returning the operand, we also return the calculated effective address. This is useful for instructions that modify the operand after reading it (e.g. the source/destination operand of ADD), which pass the effective address calculated by this function to x86-operand-to-reg/mem (which writes the result to memory).
Function:
(defun x86-operand-from-modr/m-and-sib-bytes (proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg 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 (member 0 1 2 3) reg-type) (type (member 1 2 4 6 8 10 16 32) operand-size) (type (or t nil) p4?) (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 (booleanp inst-ac?) (booleanp memory-ptr?) (integer-range-p 0 *segment-register-names-len* seg-reg)))) (declare (xargs :guard (if (equal mod 3) (case reg-type (0 (member operand-size '(1 2 4 8))) (1 (member operand-size '(4 8 16))) (2 (member operand-size '(4 8 16))) (3 (member operand-size '(4 8 16 32))) (t t)) (member operand-size '(member 1 2 4 6 8 10 16 32))))) (let ((__function__ 'x86-operand-from-modr/m-and-sib-bytes)) (declare (ignorable __function__)) (b* (((mv ?flg0 (the (signed-byte 64) addr) (the (integer 0 4) increment-rip-by) x86) (if (equal mod 3) (mv nil 0 0 x86) (x86-effective-addr proc-mode p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86))) ((when flg0) (mv (cons 'x86-effective-addr-error flg0) 0 0 0 x86)) ((mv ?flg2 operand x86) (if (equal mod 3) (case reg-type (0 (mv nil (rgfi-size operand-size (reg-index r/m rex-byte 0) rex-byte x86) x86)) (1 (mv nil (xmmi-size operand-size (reg-index r/m rex-byte 0) x86) x86)) (t (mv nil (zmmi-size operand-size (reg-index r/m rex-byte 0) x86) x86))) (b* ((check-alignment? (and inst-ac? (alignment-checking-enabled-p x86)))) (rme-size-opt proc-mode operand-size addr seg-reg :r check-alignment? x86 :mem-ptr? memory-ptr? :check-canonicity t)))) ((when flg2) (mv (cons 'rm-size-error flg2) 0 0 0 x86))) (mv nil operand increment-rip-by addr x86))))
Theorem:
(defthm natp-of-x86-operand-from-modr/m-and-sib-bytes.operand (b* (((mv ?flg ?operand ?increment-rip-by ?addr ?x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (natp operand)) :rule-classes :type-prescription)
Theorem:
(defthm x86p-of-x86-operand-from-modr/m-and-sib-bytes.x86 (implies (force (x86p x86)) (b* (((mv ?flg ?operand ?increment-rip-by ?addr ?x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (x86p x86))) :rule-classes :rewrite)
Theorem:
(defthm bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand (implies (and (equal bound (ash operand-size 3)) (member operand-size '(1 2 4 8 16 32)) (x86p x86)) (unsigned-byte-p bound (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :rule-classes (:rewrite (:type-prescription :corollary (implies (and (equal bound (ash operand-size 3)) (member operand-size '(1 2 4 8 16 32)) (x86p x86)) (natp (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (implies (and (equal bound (ash operand-size 3)) (member operand-size '(1 2 4 8 16 32)) (x86p x86)) (and (<= 0 (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (< (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)) (expt 2 bound)))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm bigger-bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand (implies (and (<= (ash operand-size 3) bound) (member operand-size '(1 2 4 8 16 32)) (integerp bound) (x86p x86)) (unsigned-byte-p bound (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :rule-classes (:rewrite))
Theorem:
(defthm bound-of-mv-nth-1-x86-operand-from-modr/m-and-sib-bytes-operand-6-and-10-bytes-read (implies (and (equal bound (ash operand-size 3)) (member operand-size '(6 10)) (not (equal mod 3)) (x86p x86)) (unsigned-byte-p bound (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :rule-classes (:rewrite (:type-prescription :corollary (implies (and (equal bound (ash operand-size 3)) (member operand-size '(6 10)) (not (equal mod 3)) (x86p x86)) (natp (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (implies (and (equal bound (ash operand-size 3)) (member operand-size '(6 10)) (not (equal mod 3)) (x86p x86)) (and (<= 0 (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (< (mv-nth 1 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4? temp-rip rex-byte r/m mod sib num-imm-bytes x86)) (expt 2 bound)))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm integerp-x86-operand-from-modr/m-and-sib-bytes-increment-rip-by-type-prescription (implies (force (x86p x86)) (natp (mv-nth 2 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :rule-classes :type-prescription)
Theorem:
(defthm mv-nth-2-x86-operand-from-modr/m-and-sib-bytes-increment-rip-by-linear<=4 (implies (x86p x86) (<= (mv-nth 2 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)) 4)) :rule-classes :linear)
Theorem:
(defthm i48p-x86-operand-from-modr/m-and-sib-bytes (implies (forced-and (x86p x86)) (signed-byte-p 48 (mv-nth 2 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :rule-classes (:rewrite (:type-prescription :corollary (implies (forced-and (x86p x86)) (integerp (mv-nth 2 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg 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 (implies (forced-and (x86p x86)) (and (<= -140737488355328 (mv-nth 2 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (< (mv-nth 2 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)) 140737488355328))) :hints (("Goal" :in-theory '(signed-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm i64p-x86-operand-from-modr/m-and-sib-bytes (implies (forced-and (x86p x86)) (signed-byte-p 64 (mv-nth 3 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86)))) :rule-classes (:rewrite (:type-prescription :corollary (implies (forced-and (x86p x86)) (integerp (mv-nth 3 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg 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 (implies (forced-and (x86p x86)) (and (<= -9223372036854775808 (mv-nth 3 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg p4 temp-rip rex-byte r/m mod sib num-imm-bytes x86))) (< (mv-nth 3 (x86-operand-from-modr/m-and-sib-bytes proc-mode reg-type operand-size inst-ac? memory-ptr? seg-reg 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)))))))