|
|
|---|
|
|
|
|---|
Compare packed bytes for equal
(x86-pcmpeqb-op/en-rm proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Function:
(defun pcmpeqb32$inline (xmm xmm/mem) (declare (xargs :guard (and (n32p xmm) (n32p xmm/mem)))) (let* ((xmm0 (mbe :logic (part-select xmm :low 0 :high 7) :exec (the (unsigned-byte 8) (logand 255 xmm)))) (xmm/mem0 (mbe :logic (part-select xmm/mem :low 0 :high 7) :exec (the (unsigned-byte 8) (logand 255 xmm/mem)))) (xmm1 (mbe :logic (part-select xmm :low 8 :high 15) :exec (the (unsigned-byte 8) (logand 255 (ash xmm -8))))) (xmm/mem1 (mbe :logic (part-select xmm/mem :low 8 :high 15) :exec (the (unsigned-byte 8) (logand 255 (ash xmm/mem -8))))) (xmm2 (mbe :logic (part-select xmm :low 16 :high 23) :exec (the (unsigned-byte 8) (logand 255 (ash xmm -16))))) (xmm/mem2 (mbe :logic (part-select xmm/mem :low 16 :high 23) :exec (the (unsigned-byte 8) (logand 255 (ash xmm/mem -16))))) (xmm3 (mbe :logic (part-select xmm :low 24 :high 31) :exec (the (unsigned-byte 8) (logand 255 (ash xmm -24))))) (xmm/mem3 (mbe :logic (part-select xmm/mem :low 24 :high 31) :exec (the (unsigned-byte 8) (logand 255 (ash xmm/mem -24))))) (byte0 (the (unsigned-byte 8) (if (int= xmm0 xmm/mem0) 255 0))) (byte1 (the (unsigned-byte 8) (if (int= xmm1 xmm/mem1) 255 0))) (byte2 (the (unsigned-byte 8) (if (int= xmm2 xmm/mem2) 255 0))) (byte3 (the (unsigned-byte 8) (if (int= xmm3 xmm/mem3) 255 0))) (dword (merge-4-u8s byte3 byte2 byte1 byte0))) dword))
Theorem:
(defthm n32p-pcmpeqb32 (unsigned-byte-p 32 (pcmpeqb32 xmm xmm/mem)) :rule-classes (:rewrite (:type-prescription :corollary (natp (pcmpeqb32 xmm xmm/mem)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (pcmpeqb32 xmm xmm/mem)) (< (pcmpeqb32 xmm xmm/mem) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Function:
(defun x86-pcmpeqb-op/en-rm (proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) (declare (xargs :stobjs (x86))) (declare (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)))) (let ((__function__ 'x86-pcmpeqb-op/en-rm)) (declare (ignorable __function__)) (b* ((?ctx 'x86-pcmpeqb-op/en-rm) (?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* (((the (unsigned-byte 4) xmm-index) (reg-index reg rex-byte 2)) ((the (unsigned-byte 128) xmm) (xmmi-size 16 xmm-index x86)) (p2 (prefixes->seg prefixes)) (p4? (eql 103 (prefixes->adr prefixes))) (seg-reg (select-segment-register proc-mode p2 p4? mod r/m sib x86)) (inst-ac? t) ((mv flg0 (the (unsigned-byte 128) xmm/mem) (the (integer 0 4) increment-rip-by) (the (signed-byte 64) ?addr) x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode 1 16 inst-ac? nil seg-reg p4? temp-rip rex-byte r/m mod sib 0 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)) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (xmm0 (mbe :logic (part-select xmm :low 0 :high 31) :exec (the (unsigned-byte 32) (logand 4294967295 xmm)))) (xmm/mem0 (mbe :logic (part-select xmm/mem :low 0 :high 31) :exec (the (unsigned-byte 32) (logand 4294967295 xmm/mem)))) (xmm1 (mbe :logic (part-select xmm :low 32 :high 63) :exec (the (unsigned-byte 32) (logand 4294967295 (ash xmm -32))))) (xmm/mem1 (mbe :logic (part-select xmm/mem :low 32 :high 63) :exec (the (unsigned-byte 32) (logand 4294967295 (ash xmm/mem -32))))) (xmm2 (mbe :logic (part-select xmm :low 64 :high 95) :exec (the (unsigned-byte 32) (logand 4294967295 (ash xmm -64))))) (xmm/mem2 (mbe :logic (part-select xmm/mem :low 64 :high 95) :exec (the (unsigned-byte 32) (logand 4294967295 (ash xmm/mem -64))))) (xmm3 (mbe :logic (part-select xmm :low 96 :high 127) :exec (the (unsigned-byte 32) (logand 4294967295 (ash xmm -96))))) (xmm/mem3 (mbe :logic (part-select xmm/mem :low 96 :high 127) :exec (the (unsigned-byte 32) (logand 4294967295 (ash xmm/mem -96))))) (dword0 (the (unsigned-byte 32) (pcmpeqb32 xmm0 xmm/mem0))) (dword1 (the (unsigned-byte 32) (pcmpeqb32 xmm1 xmm/mem1))) (dword2 (the (unsigned-byte 32) (pcmpeqb32 xmm2 xmm/mem2))) (dword3 (the (unsigned-byte 32) (pcmpeqb32 xmm3 xmm/mem3))) (result (merge-4-u32s dword3 dword2 dword1 dword0)) (x86 (!xmmi-size 16 xmm-index result x86)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-pcmpeqb-op/en-rm (implies (x86p x86) (b* ((x86 (x86-pcmpeqb-op/en-rm proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)