		Search-engine friendly clone of the ACL2 documentation.

Modr/m-decoding

Vex-opcode-modr/m-p

Returns t if a VEX-encoded opcode requires a ModR/M byte; nil otherwise.

Signature
(vex-opcode-modr/m-p vex-prefixes opcode) → bool
Returns: bool — Type (booleanp bool).

Definitions and Theorems

Function: vex-opcode-modr/m-p$inline

(defun vex-opcode-modr/m-p$inline (vex-prefixes opcode)
  (declare (type (unsigned-byte 24) vex-prefixes)
           (type (unsigned-byte 8) opcode))
  (declare (xargs :guard (vex-prefixes-byte0-p vex-prefixes)))
  (if (not (equal opcode 119))
      t
    (not (vex-prefixes-map-p 15 vex-prefixes))))

Theorem: booleanp-of-vex-opcode-modr/m-p

(defthm booleanp-of-vex-opcode-modr/m-p
  (b* ((bool (vex-opcode-modr/m-p$inline vex-prefixes opcode)))
    (booleanp bool))
  :rule-classes :rewrite)