|
|
|---|
|
|
|
|---|
Functions to read/write into the MMX registers
From Section 12.2, Intel Manual, Volume 3 (System Programming):
The MMX state consists of eight 64-bit registers (MM0 through MM7). These registers are aliased to the low 64-bits (bits 0 through 63) of floating-point registers R0 through R7 (see Figure 12-1). Note that the MMX registers are mapped to the physical locations of the floating-point registers (R0 through R7), not to the relative locations of the registers in the floating-point register stack (ST0 through ST7). As a result, the MMX register mapping is fixed and is not affected by value in the Top Of Stack (TOS) field in the floating-point status word (bits 11 through 13).
From Section 12.2, Intel Manual, Volume 3 (System Programming)
:When a value is written into an MMX register using an MMX instruction, the value also appears in the corresponding floating-point register in bits 0 through 63. Likewise, when a floating-point value written into a floating-point register by a x87 FPU, the low 64 bits of that value also appears in a the corresponding MMX register.
The execution of MMX instructions have several side effects on the x87 FPU state contained in the floating-point registers, the x87 FPU tag word, and the x87 FPU status word. These side effects are as follows:
* When an MMX instruction writes a value into an MMX register, at the same time, bits 64 through 79 of the corresponding floating-point register are set to all 1s.
* When an MMX instruction (other than the EMMS instruction) is executed, each of the tag fields in the x87 FPU tag word is set to 00B (valid). (See also Section 12.2.1, Effect of MMX, x87 FPU, FXSAVE, and FXRSTOR Instructions on the x87 FPU Tag Word.)
* When the EMMS instruction is executed, each tag field in the x87 FPU tag word is set to 11B (empty).
* Each time an MMX instruction is executed, the TOS value is set to 000B. Execution of MMX instructions does not affect the other bits in the x87 FPU status word (bits 0 through 10 and bits 14 and 15) or the contents of the other x87 FPU registers that comprise the x87 FPU state (the x87 FPU control word, instruction pointer, data pointer, or opcode registers).
Function:
(defun mmx$inline (i x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 7) i)) (let ((reg80 (the (unsigned-byte 80) (fp-datai i x86)))) (mbe :logic (part-select reg80 :low 0 :width 64) :exec (logand 18446744073709551615 reg80))))
Theorem:
(defthm n64p-mmx (unsigned-byte-p 64 (mmx i x86)) :rule-classes (:rewrite (:type-prescription :corollary (natp (mmx i x86)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mmx i x86)) (< (mmx i x86) 18446744073709551616)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Function:
(defun !mmx$inline (i v x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 7) i) (type (unsigned-byte 64) v)) (let ((val80 (mbe :logic (part-install 65535 v :low 64 :high 79) :exec (the (unsigned-byte 80) (logior 1208907372870555465154560 v))))) (!fp-datai i val80 x86)))
Theorem:
(defthm x86p-!mmx (implies (x86p x86) (x86p (!mmx i v x86))))
Function:
(defun mmx-instruction-updates$inline (x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard t)) (b* ((x86 (!fp-tag 0 x86)) (fp-status (fp-status x86)) (x86 (!fp-status (!fp-statusbits->top 0 fp-status) x86))) x86))
Theorem:
(defthm x86p-mmx-instruction-updates (implies (x86p x86) (x86p (mmx-instruction-updates x86))))