• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • Register-readers-and-writers
          • Zmms-reads-and-writes
            • Xmms-reads-and-writes
            • !zmmi-size
            • Wz64
            • Wz32
            • Wz128
            • Wz256
            • Vector-access-type-p
            • Rz512
            • Zmmi-size
            • Wz512
            • Rz64
            • Rz32
            • Rz256
            • Rz128
          • Gprs-reads-and-writes
          • Mmx-registers-reads-and-writes
          • Xmms-reads-and-writes
          • Rflags-reads-and-writes
          • Gpr-indices
          • Vex-vvvv-reg-index
          • Msr-reads-and-writes
          • Ctr-reads-and-writes
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Register-readers-and-writers

Zmms-reads-and-writes

Functions to read/write 32/64/128/256/512 bits into the XMM/YMM/ZMM registers

Source: Intel Vol. 1, Section 15.5: ACCESSING XMM, YMM AND ZMM REGISTERS

The lower 128 bits of a YMM register is aliased to the corresponding XMM register. Legacy SSE instructions (i.e., SIMD instructions operating on XMM state but not using the VEX prefix, also referred to non-VEX encoded SIMD instructions) will not access the upper bits (MAXVL-1:128) of the YMM registers. AVX and FMA instructions with a VEX prefix and vector length of 128-bits zeroes the upper 128 bits of the YMM register.

Upper bits of YMM registers (255:128) can be read and written to by many instructions with a VEX.256 prefix. XSAVE and XRSTOR may be used to save and restore the upper bits of the YMM registers.

The lower 256 bits of a ZMM register are aliased to the corresponding YMM register. Legacy SSE instructions (i.e., SIMD instructions operating on XMM state but not using the VEX prefix, also referred to non-VEX encoded SIMD instructions) will not access the upper bits (MAXVL-1:128) of the ZMM registers, where MAXVL is maximum vector length (currently 512 bits). AVX and FMA instructions with a VEX prefix and vector length of 128-bits zero the upper 384 bits of the ZMM register, while the VEX prefix and vector length of 256-bits zeroes the upper 256 bits of the ZMM register. Upper bits of ZMM registers (511:256) can be read and written to by instructions with an EVEX.512 prefix.

rz32, rz64, rz128, rz256, and rz512 will read the contents of the ZMMs as natural numbers.

Similarly, wz32, wz64, wz128, wz256, and wz512 are used to write natural numbers into the ZMMs.

Definitions and Theorems

Function: rz32$inline

(defun rz32$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg))
  (n32 (the (unsigned-byte 512)
            (zmmi reg x86))))

Theorem: n32p-rz32

(defthm n32p-rz32
 (unsigned-byte-p 32 (rz32 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rz32 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rz32 reg x86))
                   (< (rz32 reg x86) 4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: rz64$inline

(defun rz64$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg))
  (n64 (the (unsigned-byte 512)
            (zmmi reg x86))))

Theorem: n64p-rz64

(defthm n64p-rz64
 (unsigned-byte-p 64 (rz64 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rz64 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rz64 reg x86))
                   (< (rz64 reg x86) 18446744073709551616))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: rz128$inline

(defun rz128$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg))
  (n128 (the (unsigned-byte 512)
             (zmmi reg x86))))

Theorem: n128p-rz128

(defthm n128p-rz128
 (unsigned-byte-p 128 (rz128 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rz128 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (rz128 reg x86))
                   (< (rz128 reg x86)
                      340282366920938463463374607431768211456))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: rz256$inline

(defun rz256$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg))
  (n256 (the (unsigned-byte 512)
             (zmmi reg x86))))

Theorem: n256p-rz256

(defthm n256p-rz256
 (unsigned-byte-p 256 (rz256 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rz256 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
    (<= 0 (rz256 reg x86))
    (<
     (rz256 reg x86)
     115792089237316195423570985008687907853269984665640564039457584007913129639936))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: rz512$inline

(defun rz512$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg))
  (n512 (the (unsigned-byte 512)
             (zmmi reg x86))))

Theorem: n512p-rz512

(defthm n512p-rz512
 (unsigned-byte-p 512 (rz512 reg x86))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (rz512 reg x86))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
    (<= 0 (rz512 reg x86))
    (<
     (rz512 reg x86)
     13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Function: vector-access-type-p

(defun vector-access-type-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vector-access-type-p))
    (declare (ignorable __function__))
    (or (equal x 1)
        (equal x 2)
        (equal x 3)
        (equal x 4))))

Theorem: booleanp-of-vector-access-type-p

(defthm booleanp-of-vector-access-type-p
  (b* ((ok? (vector-access-type-p x)))
    (booleanp ok?))
  :rule-classes :type-prescription)

Function: wz32$inline

(defun wz32$inline (reg val x86 regtype)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg)
           (type (unsigned-byte 32) val))
  (declare (xargs :guard (vector-access-type-p regtype)))
  (b* ((data (the (unsigned-byte 512)
                  (zmmi reg x86)))
       (regtype (the (unsigned-byte 3) regtype))
       (data (case regtype
               (2 (loghead 128 data))
               (3 (loghead 256 data))
               (otherwise data)))
       (val (n32 (the (unsigned-byte 32) val))))
    (!zmmi reg
           (part-install val data :low 0 :width 32)
           x86)))

Theorem: x86p-wz32

(defthm x86p-wz32
  (implies (x86p x86)
           (x86p (wz32 reg val x86 :regtype access))))

Theorem: rz32-wz32-same

(defthm rz32-wz32-same
  (equal (rz32 reg (wz32 reg val x86 :regtype access))
         (loghead 32 val)))

Theorem: rz32-wz32-different

(defthm rz32-wz32-different
  (implies (not (equal (nfix reg1) (nfix reg2)))
           (equal (rz32 reg1
                        (wz32 reg2 val x86 :regtype access))
                  (rz32 reg1 x86))))

Function: wz64$inline

(defun wz64$inline (reg val x86 regtype)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg)
           (type (unsigned-byte 64) val))
  (declare (xargs :guard (vector-access-type-p regtype)))
  (b* ((data (the (unsigned-byte 512)
                  (zmmi reg x86)))
       (regtype (the (unsigned-byte 3) regtype))
       (data (case regtype
               (2 (loghead 128 data))
               (3 (loghead 256 data))
               (otherwise data)))
       (val (the (unsigned-byte 64) (n64 val))))
    (!zmmi reg
           (part-install val data :low 0 :width 64)
           x86)))

Theorem: x86p-wz64

(defthm x86p-wz64
  (implies (x86p x86)
           (x86p (wz64 reg val x86 :regtype access))))

Theorem: rz64-wz64-same

(defthm rz64-wz64-same
  (equal (rz64 reg (wz64 reg val x86 :regtype access))
         (loghead 64 val)))

Theorem: rz64-wz64-different

(defthm rz64-wz64-different
  (implies (not (equal (nfix reg1) (nfix reg2)))
           (equal (rz64 reg1
                        (wz64 reg2 val x86 :regtype access))
                  (rz64 reg1 x86))))

Function: wz128$inline

(defun wz128$inline (reg val x86 regtype)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg)
           (type (unsigned-byte 128) val))
  (declare (xargs :guard (vector-access-type-p regtype)))
  (b* ((data (the (unsigned-byte 512)
                  (zmmi reg x86)))
       (regtype (the (unsigned-byte 3) regtype))
       (data (case regtype
               (2 (loghead 128 data))
               (3 (loghead 256 data))
               (otherwise data)))
       (val (the (unsigned-byte 128) (n128 val))))
    (!zmmi reg
           (part-install val data
                         :low 0
                         :width 128)
           x86)))

Theorem: x86p-wz128

(defthm x86p-wz128
  (implies (x86p x86)
           (x86p (wz128 reg val x86 :regtype access))))

Theorem: rz128-wz128-same

(defthm rz128-wz128-same
  (equal (rz128 reg (wz128 reg val x86 :regtype access))
         (loghead 128 val)))

Theorem: rz128-wz128-different

(defthm rz128-wz128-different
  (implies (not (equal (nfix reg1) (nfix reg2)))
           (equal (rz128 reg1
                         (wz128 reg2 val x86 :regtype access))
                  (rz128 reg1 x86))))

Function: wz256$inline

(defun wz256$inline (reg val x86 regtype)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg)
           (type (unsigned-byte 256) val))
  (declare (xargs :guard (vector-access-type-p regtype)))
  (b* ((data (the (unsigned-byte 512)
                  (zmmi reg x86)))
       (regtype (the (unsigned-byte 3) regtype))
       (data (case regtype
               (3 (loghead 256 data))
               (otherwise data)))
       (val (the (unsigned-byte 256) (n256 val))))
    (!zmmi reg
           (part-install val data
                         :low 0
                         :width 256)
           x86)))

Theorem: x86p-wz256

(defthm x86p-wz256
  (implies (x86p x86)
           (x86p (wz256 reg val x86 :regtype access))))

Theorem: rz256-wz256-same

(defthm rz256-wz256-same
  (equal (rz256 reg (wz256 reg val x86 :regtype access))
         (loghead 256 val)))

Theorem: rz256-wz256-different

(defthm rz256-wz256-different
  (implies (not (equal (nfix reg1) (nfix reg2)))
           (equal (rz256 reg1
                         (wz256 reg2 val x86 :regtype access))
                  (rz256 reg1 x86))))

Function: wz512$inline

(defun wz512$inline (reg val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) reg)
           (type (unsigned-byte 512) val))
  (let ((val (the (unsigned-byte 512) (n512 val))))
    (!zmmi reg val x86)))

Theorem: x86p-wz512

(defthm x86p-wz512
  (implies (x86p x86)
           (x86p (wz512 reg val x86))))

Theorem: rz512-wz512-same

(defthm rz512-wz512-same
  (equal (rz512 reg (wz512 reg val x86))
         (loghead 512 val)))

Theorem: rz512-wz512-different

(defthm rz512-wz512-different
  (implies (not (equal (nfix reg1) (nfix reg2)))
           (equal (rz512 reg1 (wz512 reg2 val x86))
                  (rz512 reg1 x86))))

Function: zmmi-size$inline

(defun zmmi-size$inline (nbytes index x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 7) nbytes)
           (type (unsigned-byte 5) index))
  (declare (xargs :guard (member nbytes '(4 8 16 32 64))))
  (case nbytes
    (4 (rz32 index x86))
    (8 (rz64 index x86))
    (16 (rz128 index x86))
    (32 (rz256 index x86))
    (64 (rz512 index x86))
    (otherwise 0)))

Theorem: natp-of-zmmi-size

(defthm natp-of-zmmi-size
  (b* ((val (zmmi-size$inline nbytes index x86)))
    (natp val))
  :rule-classes :type-prescription)

Function: !zmmi-size$inline

(defun !zmmi-size$inline (nbytes index val x86 regtype)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 7) nbytes)
          (type (unsigned-byte 5) index)
          (type integer val))
 (declare (xargs :guard (vector-access-type-p regtype)))
 (declare (xargs :guard (and (member nbytes '(4 8 16 32 64))
                             (unsigned-byte-p (ash nbytes 3) val))))
 (case nbytes
   (4 (wz32 index val x86 :regtype regtype))
   (8 (wz64 index val x86 :regtype regtype))
   (16 (wz128 index val x86 :regtype regtype))
   (32 (wz256 index val x86 :regtype regtype))
   (64 (wz512 index val x86))
   (otherwise x86)))

Theorem: x86p-of-!zmmi-size

(defthm x86p-of-!zmmi-size
  (implies
       (x86p x86)
       (b* ((x86 (!zmmi-size$inline nbytes index val x86 regtype)))
         (x86p x86)))
  :rule-classes :rewrite)

Subtopics

Xmms-reads-and-writes

Functions to read/write 32/64/128 bits into the XMM registers (to be used by non-VEX encoded 128-bit SIMD instructions)

!zmmi-size

Write val to low nbytes of a ZMM register

Wz64

Write val to low 64 bits of a ZMM register

Wz32

Write val to low 32 bits of a ZMM register

Wz128

Write val to low 128 bits of a ZMM register

Wz256

Write val to low 256 bits of a ZMM register.

Vector-access-type-p

Rz512

Zmmi-size

Wz512

Write val to 512 bits of a ZMM register.

Rz64

Rz32

Rz256

Rz128