		Search-engine friendly clone of the ACL2 documentation.

Modr/m-decoding

Three-byte-opcode-modr/m-p

Returns t if a three-byte opcode requires a ModR/M byte; nil otherwise. Doesn't account for AVX/AVX2/AVX512 instructions.

Signature
(three-byte-opcode-modr/m-p proc-mode mandatory-prefix escape-byte opcode) → bool
Arguments: escape-byte — Second byte of the three-byte opcode --- either #x38 or #x3A.; opcode — Third byte of the three-byte opcode.
Returns: bool — Type (booleanp bool), given (n08p opcode).

Definitions and Theorems

Function: three-byte-opcode-modr/m-p$inline

(defun three-byte-opcode-modr/m-p$inline
       (proc-mode mandatory-prefix escape-byte opcode)
  (declare (type (integer 0 4) proc-mode)
           (type (unsigned-byte 8)
                 mandatory-prefix)
           (type (unsigned-byte 8) escape-byte)
           (type (unsigned-byte 8) opcode))
  (declare (xargs :guard (or (equal escape-byte 56)
                             (equal escape-byte 58))))
  (cond ((equal escape-byte 56)
         (if (equal proc-mode 0)
             (64-bit-mode-0f-38-three-byte-opcode-modr/m-p
                  mandatory-prefix opcode)
           (32-bit-mode-0f-38-three-byte-opcode-modr/m-p
                mandatory-prefix opcode)))
        (t (if (equal proc-mode 0)
               (64-bit-mode-0f-3a-three-byte-opcode-modr/m-p
                    mandatory-prefix opcode)
             (32-bit-mode-0f-3a-three-byte-opcode-modr/m-p
                  mandatory-prefix opcode)))))

Theorem: booleanp-of-three-byte-opcode-modr/m-p

(defthm booleanp-of-three-byte-opcode-modr/m-p
  (implies (n08p opcode)
           (b* ((bool (three-byte-opcode-modr/m-p$inline
                           proc-mode
                           mandatory-prefix escape-byte opcode)))
             (booleanp bool)))
  :rule-classes :rewrite)