		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-movddup-sse

MOVDDUP: replicate double precision floating-point values.

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

This is the SSE variant.

Although the operand size is 128 bits, the use of m64 in xmm2/m64 in the Intel manual suggests that only 64 bits are read from the source operand. If the access is to memory, reading 128 and ignoring the 64 high ones can make a difference if the additional memory accesses cause some kind of exception.

Definitions and Theorems

Function: x86-movddup-sse

(defun x86-movddup-sse
       (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-movddup-sse))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-movddup-sse)
       (?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))
     ((the (unsigned-byte 4) xmm-index)
      (reg-index reg rex-byte 2))
     (inst-ac? t)
     ((mv flg0 (the (unsigned-byte 64) val)
          (the (integer 0 4) increment-rip-by)
          & x86)
      (x86-operand-from-modr/m-and-sib-bytes
           proc-mode 1 8 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?))
     (dup-val (logior (ash val 64) val))
     (x86 (!xmmi-size 16 xmm-index dup-val x86))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-movddup-sse

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