Vex->x
Get the X field of vex-prefixes for the three-byte form,
or 1 for the two-byte form.
- Signature
(vex->x vex-prefixes) → *
- Arguments
- vex-prefixes — Guard (vex-prefixes-p vex-prefixes).
Although the two-byte form has no X bit,
as far as the VEX encoding of the REX byte is concerned,
the two-byte form can be regarded as encoding the value 0
for the X bit of the REX byte.
Since the REX.X encoding in VEX is negated,
this function returns 1 for the two-byte form.
See Intel manual Volume 2 Figure 2-9 of Dec 2023.
Definitions and Theorems
Function: vex->x$inline
(defun vex->x$inline (vex-prefixes)
(declare (xargs :guard (vex-prefixes-p vex-prefixes)))
(case (vex-prefixes->byte0 vex-prefixes)
(196 (vex3-byte1->x (vex-prefixes->byte1 vex-prefixes)))
(otherwise 1)))
