		Search-engine friendly clone of the ACL2 documentation.

Two-byte-opcodes

X86-vmovddup-vex

VMOVDDUP: replicate double precision floating-point values.

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

This instruction is listed under MOVDDUP in Intel Manual Volume 2 (Jun 2025).

When 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 bits and ignoring the 64 high ones can make a difference if the additional memory accesses cause some kind of exception.

When the operand size is 256 bits, the use of m256 in ymm2/m256 in the Intel manual suggests that all 256 bits are read from the source operand, even though the ones at positions 64-127 and 192-255 are ignored. In principle it could suffice to read the ones at positions 0-63 and 128-191, or perhaps the low 192 bits. But we read all 256, because of the m256. If the access is to memory, reading fewer bytes could make a difference if the additional ignored ones cause some kind of exception.

Definitions and Theorems

Function: x86-vmovddup-vex

(defun x86-vmovddup-vex
       (proc-mode start-rip temp-rip prefixes rex-byte
                  vex-prefixes 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 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-vmovddup-vex))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-vmovddup-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 (unsigned-byte 4) xmm/ymm-index)
      (reg-index reg rex-byte 2))
     ((the (integer 16 32) operand-size)
      (if (equal (vex->l vex-prefixes) 1)
          32
        16))
     (inst-ac? t)
     ((mv flg (the (unsigned-byte 256) val)
          (the (integer 0 4) increment-rip-by)
          & x86)
      (x86-operand-from-modr/m-and-sib-bytes
           proc-mode (if (= operand-size 16) 2 3)
           (if (= operand-size 16) 8 32)
           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))
     ((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 (if (= operand-size 16)
                  (logior (ash val 64) val)
                (b* ((x0 (part-select val :low 0 :high 63))
                     (x2 (part-select val :low 128 :high 191))
                     (x0x0 (logior (ash x0 64) x0))
                     (x2x2 (logior (ash x2 64) x2)))
                  (logior (ash x2x2 128) x0x0))))
     (x86 (!zmmi-size operand-size xmm/ymm-index dup-val x86
                      :regtype (if (= operand-size 16) 2 3)))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-vmovddup-vex

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