• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
              • !xmmi-size
              • Xmmi-size
              • Wx64
              • Wx32
              • Wx128
              • Rx64
              • Rx32
              • Rx128
            • !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
            • !xmmi-size
            • Xmmi-size
            • Wx64
            • Wx32
            • Wx128
            • Rx64
            • Rx32
            • Rx128
          • 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

• Zmms-reads-and-writes
• Register-readers-and-writers

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)

These functions are meant to be used by instructions that do not use a VEX or EVEX prefix --- these functions preserve the upper bits of ZMM registers. For instructions that use these prefixes and zero out these bits instead, see ZMMs-Reads-and-Writes.

Note that the index for accessing the XMM registers is 4-bits wide (as opposed to the 5-bit index for ZMM registers --- see ZMMs-Reads-and-Writes) because only 16 XMM registers were supported initially in the 64-bit mode (and 8 in the 32-bit mode).

Source: Intel Vol. 2, Section 2.3.10 --- AVX Instructions and Upper 128-bits of YMM registers:

If an instruction with a destination XMM register is encoded with a VEX prefix, the processor zeroes the upper bits (above bit 128) of the equivalent YMM register. Legacy SSE instructions without VEX preserve the upper bits.

Functions rx32, rx64, and rx128 will read the contents of the XMMs (i.e., low 128 bits of ZMMs) as natural numbers.

Similarly, functions wx32, wx64, and wx128 are used to write natural numbers into the XMMs (and preserve the upper bits of ZMMs).

Definitions and Theorems

Function: rx32$inline

(defun rx32$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 4) reg))
  (rz32 reg x86))

Function: rx64$inline

(defun rx64$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 4) reg))
  (rz64 reg x86))

Function: rx128$inline

(defun rx128$inline (reg x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 4) reg))
  (rz128 reg x86))

Function: wx32$inline

(defun wx32$inline (reg val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 4) reg)
           (type (unsigned-byte 32) val))
  (wz32 reg val x86 :regtype 1))

Function: wx64$inline

(defun wx64$inline (reg val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 4) reg)
           (type (unsigned-byte 64) val))
  (wz64 reg val x86 :regtype 1))

Function: wx128$inline

(defun wx128$inline (reg val x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 4) reg)
           (type (unsigned-byte 128) val))
  (wz128 reg val x86 :regtype 1))

Function: xmmi-size$inline

(defun xmmi-size$inline (nbytes index x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 5) nbytes)
           (type (unsigned-byte 4) index))
  (declare (xargs :guard (member nbytes '(4 8 16))))
  (case nbytes
    (4 (rx32 index x86))
    (8 (rx64 index x86))
    (16 (rx128 index x86))
    (otherwise 0)))

Theorem: natp-of-xmmi-size

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

Function: !xmmi-size$inline

(defun !xmmi-size$inline (nbytes index val x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 5) nbytes)
          (type (unsigned-byte 4) index)
          (type integer val))
 (declare (xargs :guard (and (member nbytes '(4 8 16))
                             (unsigned-byte-p (ash nbytes 3) val))))
 (case nbytes
   (4 (wx32 index val x86))
   (8 (wx64 index val x86))
   (16 (wx128 index val x86))
   (otherwise x86)))

Theorem: x86p-of-!xmmi-size

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

Subtopics

!xmmi-size

Write val to low nbytes of an XMM register; upper bits of the ZMM register are preserved.

Xmmi-size

Wx64

Write val to low 64 bits of a ZMM register; upper bits are preserved.

Wx32

Write val to low 32 bits of a ZMM register; upper bits are preserved.

Wx128

Write val to low 128 bits of a ZMM register; upper bits are preserved.

Rx64

Rx32

Rx128