		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.