|
|
|---|
|
|
|
|---|
Write to doubleword general-purpose registers
(wr32 reg val x86) → x86
Note Intel Vol. 1 Sec. 3.4.1.1 p. 3-17, which says the following about 64-bit mode:
32-bit operands generate a 32-bit result, zero-extended to a 64-bit result in the destination general-purpose register.
This is also confirmed by AMD manual, Jun'15, Vol. 3, App. B.1, under `No Extension of 8-Bit and 16-Bit Results'.
In 32-bit mode, the upper 32 bits are undefined, as specified by the following quote from the same page as above:
Because the upper 32 bits of 64-bit general-purpose registers are undefined in 32-bit modes, the upper 32 bits of any general-purpose register are not preserved when switching from 64-bit mode to a 32-bit mode (to protected mode or compatibility mode). Software must not depend on these bits to maintain a value after a 64-bit to 32-bit mode switch.
This function is used both in 64-bit mode and in 32-bit mode. Since in 32-bit mode the high 32 bits of general-purpose registers are not accessible, it is fine for this function to set those bits to 0, as opposed to, for example, setting them to undefined values as done by the semantic functions of certain instructions for certain flags. The switching from 32-bit mode to 64-bit mode (when modeled) will set the high 32 bits of general-purpose registers to undefined values.
Function:
(defun wr32$inline (reg val x86) (declare (xargs :stobjs (x86))) (declare (type (unsigned-byte 4) reg) (type (unsigned-byte 32) val)) (!rgfi reg (mbe :logic (n32 val) :exec val) x86))
Theorem:
(defthm x86p-wr32 (implies (x86p x86) (x86p (wr32 reg val x86))))