		Search-engine friendly clone of the ACL2 documentation.

X86-cmpps-op/en-rmi

Compare packed single-precision floating-point values

Signature
(x86-cmpps-op/en-rmi proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Op/En = RMI: [OP XMM, XMM/M, IMM]

0F C2: CMPPS xmm1, xmm2/m128, imm8

Definitions and Theorems

Function: x86-cmpps-op/en-rmi

(defun x86-cmpps-op/en-rmi
       (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-cmpps-op/en-rmi))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-cmpps-op/en-rmi)
       (?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? nil)
     ((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 1 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 8) imm)
          x86)
      (rme-size-opt proc-mode
                    1 (the (signed-byte 48) temp-rip)
                    1 :x nil x86
                    :mem-ptr? nil))
     ((when flg1)
      (!!ms-fresh :imm-rme-size-error flg1))
     ((mv flg (the (signed-byte 48) temp-rip))
      (add-to-*ip proc-mode temp-rip 1 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?))
     ((when (not (eql (mod addr 16) 0)))
      (!!ms-fresh :memory-address-is-not-16-byte-aligned addr))
     (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)))))
     (mxcsr (the (unsigned-byte 32) (mxcsr x86)))
     (operation (the (unsigned-byte 3) (n02 imm)))
     ((mv flg2 (the (unsigned-byte 32) result0)
          (the (unsigned-byte 32) mxcsr0))
      (sp-sse-cmp operation xmm0 xmm/mem0 mxcsr))
     ((when flg2)
      (!!ms-fresh :sp-sse-cmp flg2))
     ((mv flg3 (the (unsigned-byte 32) result1)
          (the (unsigned-byte 32) mxcsr1))
      (sp-sse-cmp operation xmm1 xmm/mem1 mxcsr))
     ((when flg3)
      (!!ms-fresh :sp-sse-cmp flg3))
     ((mv flg4 (the (unsigned-byte 32) result2)
          (the (unsigned-byte 32) mxcsr2))
      (sp-sse-cmp operation xmm2 xmm/mem2 mxcsr))
     ((when flg4)
      (!!ms-fresh :sp-sse-cmp flg4))
     ((mv flg5 (the (unsigned-byte 32) result3)
          (the (unsigned-byte 32) mxcsr3))
      (sp-sse-cmp operation xmm3 xmm/mem3 mxcsr))
     ((when flg5)
      (!!ms-fresh :sp-sse-cmp flg5))
     (result (merge-4-u32s result3 result2 result1 result0))
     (mxcsr (the (unsigned-byte 32)
                 (logior mxcsr0 mxcsr1 mxcsr2 mxcsr3)))
     (x86 (!mxcsr mxcsr x86))
     (x86 (!xmmi-size 16 xmm-index result x86))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-cmpps-op/en-rmi

(defthm x86p-of-x86-cmpps-op/en-rmi
 (implies
   (x86p x86)
   (b*
    ((x86 (x86-cmpps-op/en-rmi proc-mode start-rip temp-rip prefixes
                               rex-byte opcode modr/m sib x86)))
    (x86p x86)))
 :rule-classes :rewrite)