		Search-engine friendly clone of the ACL2 documentation.

X86-vzeroupper

VZEROUPPER: Zero Upper Bits of YMM and ZMM Registers

Signature
(x86-vzeroupper 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).

Definitions and Theorems

Function: x86-vzeroupper

(defun x86-vzeroupper
       (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-vzeroupper))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-vzeroupper))
    (b*
      (((unless (equal (vex->l vex-prefixes) 0))
        (!!fault-fresh :ud nil :vzeroupper 'vex.l
                       1))
       (|2^128-1| (1- (expt 2 128)))
       (zmm0 (zmmi-size 64 0 x86))
       (zmm1 (zmmi-size 64 1 x86))
       (zmm2 (zmmi-size 64 2 x86))
       (zmm3 (zmmi-size 64 3 x86))
       (zmm4 (zmmi-size 64 4 x86))
       (zmm5 (zmmi-size 64 5 x86))
       (zmm6 (zmmi-size 64 6 x86))
       (zmm7 (zmmi-size 64 7 x86))
       (x86 (!zmmi-size 64 0 (logand zmm0 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 1 (logand zmm1 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 2 (logand zmm2 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 3 (logand zmm3 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 4 (logand zmm4 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 5 (logand zmm5 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 6 (logand zmm6 |2^128-1|)
                        x86))
       (x86 (!zmmi-size 64 7 (logand zmm7 |2^128-1|)
                        x86))
       (x86 (if (equal proc-mode 0)
                (b* ((zmm8 (zmmi-size 64 8 x86))
                     (zmm9 (zmmi-size 64 9 x86))
                     (zmm10 (zmmi-size 64 10 x86))
                     (zmm11 (zmmi-size 64 11 x86))
                     (zmm12 (zmmi-size 64 12 x86))
                     (zmm13 (zmmi-size 64 13 x86))
                     (zmm14 (zmmi-size 64 14 x86))
                     (zmm15 (zmmi-size 64 15 x86))
                     (x86 (!zmmi-size 64 8 (logand zmm8 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 9 (logand zmm9 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 10 (logand zmm10 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 11 (logand zmm11 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 12 (logand zmm12 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 13 (logand zmm13 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 14 (logand zmm14 |2^128-1|)
                                      x86))
                     (x86 (!zmmi-size 64 15 (logand zmm15 |2^128-1|)
                                      x86)))
                  x86)
              x86))
       (x86 (write-*ip proc-mode temp-rip x86)))
      x86))))

Theorem: x86p-of-x86-vzeroupper

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