Operand Fetch and Execute for ADD, ADC, SUB, SBB, OR, AND, XOR, CMP, TEST: Addressing Mode = (E, I)
(x86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i operation proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
where
Function:
(defun x86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i (operation proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 38) operation) (type (integer 0 4) proc-mode) (type (signed-byte 48) start-rip) (type (signed-byte 48) temp-rip) (type (unsigned-byte 52) prefixes) (type (unsigned-byte 8) rex-byte) (type (unsigned-byte 8) opcode) (type (unsigned-byte 8) modr/m) (type (unsigned-byte 8) sib)) (declare (ignorable proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib)) (declare (xargs :guard (and (prefixes-p prefixes) (modr/m-p modr/m) (sib-p sib) (rip-guard-okp proc-mode temp-rip) (and (natp operation) (<= operation 8) (if (eql opcode 130) (not (equal proc-mode 0)) t))))) (let ((__function__ 'x86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i)) (declare (ignorable __function__)) (b* ((?ctx 'x86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i) (?r/m (the (unsigned-byte 3) (modr/m->r/m modr/m))) (?mod (the (unsigned-byte 2) (modr/m->mod modr/m))) (?reg (the (unsigned-byte 3) (modr/m->reg modr/m)))) (b* ((p2 (prefixes->seg prefixes)) (p4? (eql 103 (prefixes->adr prefixes))) (e-byte-operand? (or (eql opcode 128) (eql opcode 130) (eql opcode 246))) ((the (integer 1 8) e-size) (select-operand-size proc-mode e-byte-operand? rex-byte nil prefixes nil nil nil x86)) (imm-byte-operand? (or (eql opcode 128) (eql opcode 130) (eql opcode 131) (eql opcode 246))) ((the (integer 1 4) imm-size) (select-operand-size proc-mode imm-byte-operand? rex-byte t prefixes nil nil nil x86)) (seg-reg (select-segment-register proc-mode p2 p4? mod r/m sib x86)) (inst-ac? t) ((mv flg0 e increment-rip-by (the (signed-byte 64) e-addr) x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode 0 e-size inst-ac? nil seg-reg p4? temp-rip rex-byte r/m mod sib imm-size x86)) ((when flg0) (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg0)) ((mv flg (the (signed-byte 48) temp-rip)) (add-to-*ip proc-mode temp-rip increment-rip-by x86)) ((when flg) (!!ms-fresh :rip-increment-error flg)) ((mv ?flg1 (the (unsigned-byte 32) imm) x86) (rme-size-opt proc-mode imm-size temp-rip 1 :x nil x86)) ((when flg1) (!!ms-fresh :rme-size-error flg1)) (imm (mbe :logic (loghead (ash e-size 3) (logext (ash imm-size 3) imm)) :exec (logand (case e-size (1 255) (2 65535) (4 4294967295) (8 18446744073709551615) (t 0)) (case imm-size (1 (the (signed-byte 8) (n08-to-i08 (the (unsigned-byte 8) imm)))) (2 (the (signed-byte 16) (n16-to-i16 (the (unsigned-byte 16) imm)))) (4 (the (signed-byte 32) (n32-to-i32 (the (unsigned-byte 32) imm)))) (t 0))))) ((mv flg (the (signed-byte 49) temp-rip)) (add-to-*ip proc-mode temp-rip imm-size x86)) ((when flg) (!!ms-fresh :rip-increment-error flg)) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) ((the (unsigned-byte 32) input-rflags) (rflags x86)) ((mv result (the (unsigned-byte 32) output-rflags) (the (unsigned-byte 32) undefined-flags)) (gpr-arith/logic-spec e-size operation e imm input-rflags)) ((mv flg1 x86) (if (or (eql operation 8) (eql operation 7)) (mv nil x86) (x86-operand-to-reg/mem proc-mode e-size inst-ac? nil result seg-reg (the (signed-byte 64) e-addr) rex-byte r/m mod x86))) ((when flg1) (!!ms-fresh :x86-operand-to-reg/mem flg1)) (x86 (write-user-rflags output-rflags undefined-flags x86)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i (implies (x86p x86) (b* ((x86 (x86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i operation proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)