|
|
|---|
|
|
|
|---|
Returns a boolean saying whether a SIB byte is expected to follow a ModR/M byte or not.
This is based on Intel manual, Jan'19, Volume 2, Tables 2-1 and 2-2, as well as AMD manual, Dec'17, Volume 3, Tables A-33 and A-35. When the address size is 32 or 64 bits, Intel Table 2-2 and AMD Table A-35 apply: a SIB byte is expected exactly when ModR/M.mod is not #b11 and ModR/M.r/m is #b100. When the address size is 16 bits, no SIB byte is expected.
Intel Table 2-3 applies to 32-bit addresses, but Section 2.2.1.3 says that it also applies to 64-bit addresses. AMD Table A-35 mentions both 32-bit and 64-bit addressing.
Intel manual, Jan'19, Volume 2, Table 2-7 is not very clear,
giving the impression that a SIB byte may be required
when Mod = 00 and R/M = 101 (last column of first row).
But AMD manual, Dec'17, Volume 3, Table 1-16
(which corresponds to Intel Table 2-7) clearly says that
no SIB byte is present in the first row.
Intel's last column of first row means that,
in order to use
The second argument of this function says whether
the address size is 16 bits or not (i.e. 32 or 64 bits).
In 64-bit mode, this argument is always
Function:
(defun x86-decode-sib-p (modr/m 16-bit-addressp) (declare (type (unsigned-byte 8) modr/m)) (declare (xargs :guard (booleanp 16-bit-addressp))) (let ((__function__ 'x86-decode-sib-p)) (declare (ignorable __function__)) (and (not 16-bit-addressp) (b* ((r/m (modr/m->r/m modr/m)) (mod (modr/m->mod modr/m))) (and (int= r/m 4) (not (int= mod 3)))))))
Theorem:
(defthm booleanp-of-x86-decode-sib-p (implies (n08p modr/m) (b* ((bool (x86-decode-sib-p modr/m 16-bit-addressp))) (booleanp bool))) :rule-classes :rewrite)