		Search-engine friendly clone of the ACL2 documentation.

Modr/m-decoding

Two-byte-opcode-modr/m-p

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

Signature
(two-byte-opcode-modr/m-p proc-mode mandatory-prefix opcode) → bool
Arguments: opcode — Second byte of the two-byte opcode.
Returns: bool — Type (booleanp bool), given (n08p opcode).

Definitions and Theorems

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

(defun two-byte-opcode-modr/m-p$inline
       (proc-mode mandatory-prefix opcode)
 (declare (type (integer 0 4) proc-mode)
          (type (unsigned-byte 8)
                mandatory-prefix)
          (type (unsigned-byte 8) opcode))
 (cond
  ((equal proc-mode 0)
   (64-bit-mode-two-byte-opcode-modr/m-p mandatory-prefix opcode))
  (t
   (32-bit-mode-two-byte-opcode-modr/m-p mandatory-prefix opcode))))

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

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