|
|
|---|
|
|
|
|---|
VEX-encoded logical instructions.
(x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex
operation proc-mode
start-rip temp-rip prefixes rex-byte
vex-prefixes opcode modr/m sib x86)
→
x86VANDPD xmm1, xmm2, xmm3/m128 VANDPD ymm1, ymm2, ymm3/m256 VANDPS xmm1, xmm2, xmm3/m128 VANDPS ymm1, ymm2, ymm3/m256 VANDNPD xmm1, xmm2, xmm3/m128 VANDNPD ymm1, ymm2, ymm3/m256 VANDNPS xmm1, xmm2, xmm3/m128 VANDNPS ymm1, ymm2, ymm3/m256 VORPD xmm1, xmm2, xmm3/m128 VORPD ymm1, ymm2, ymm3/m256 VORPS xmm1, xmm2, xmm3/m128 VORPS ymm1, ymm2, ymm3/m256 VXORPD xmm1, xmm2, xmm3/m128 VXORPD ymm1, ymm2, ymm3/m256 VXORPS xmm1, xmm2, xmm3/m128 VXORPS ymm1, ymm2, ymm3/m256 VPAND xmm1, xmm2, xmm3/m128 VPAND ymm1, ymm2, ymm3/m256 VPANDN xmm1, xmm2, xmm3/m128 VPANDN ymm1, ymm2, ymm3/m256 VPOR xmm1, xmm2, xmm3/m128 VPOR ymm1, ymm2, ymm3/m256 VPXOR xmm1, xmm2, xmm3/m128 VPXOR ymm1, ymm2, ymm3/m256
Function:
(defun x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex (operation proc-mode start-rip temp-rip prefixes rex-byte vex-prefixes 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 24) vex-prefixes) (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) (vex-prefixes-byte0-p vex-prefixes)))) (let ((__function__ 'x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex)) (declare (ignorable __function__)) (b* ((?ctx 'x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex) (?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))) (seg-reg (select-segment-register proc-mode p2 p4? mod r/m sib x86)) (rex-byte (rex-byte-from-vex-prefixes vex-prefixes)) ((the (integer 16 32) operand-size) (if (equal (vex->l vex-prefixes) 1) 32 16)) ((the (unsigned-byte 4) src1-index) (vex-vvvv-reg-index (vex->vvvv vex-prefixes))) ((the (unsigned-byte 256) src1) (zmmi-size operand-size src1-index x86)) (inst-ac? nil) ((mv flg src2 (the (integer 0 4) increment-rip-by) (the (signed-byte 64) addr) x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode (if (= operand-size 16) 2 3) operand-size inst-ac? nil seg-reg p4? temp-rip rex-byte r/m mod sib 0 x86)) ((when flg) (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg)) ((the (unsigned-byte 4) dst-index) (reg-index reg rex-byte 2)) ((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)) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (result (case operation (3 (logand src1 src2)) (13 (logand (lognot src1) src2)) (1 (logior src1 src2)) (5 (logxor src1 src2)) (otherwise 0))) (result (if (= operand-size 16) (n128 result) (n256 result))) (x86 (!zmmi-size operand-size dst-index result x86 :regtype (if (= operand-size 16) 2 3))) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex (implies (x86p x86) (b* ((x86 (x86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex operation proc-mode start-rip temp-rip prefixes rex-byte vex-prefixes opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)