		Search-engine friendly clone of the ACL2 documentation.

Decoding-and-spec-utils

Sib-decoding

Functions to detect and decode SIB bytes

Definitions and Theorems

Function: x86-decode-sib-p

(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: booleanp-of-x86-decode-sib-p

(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)

Subtopics

Sib-structures: Bitstruct definitions to store a SIB byte and its fields.
X86-decode-sib-p: Returns a boolean saying whether a SIB byte is expected to follow a ModR/M byte or not.