		Search-engine friendly clone of the ACL2 documentation.

Prefix-modrm-sib-decoding

Compute-mandatory-prefix-for-three-byte-opcode

Three-byte opcodes: picks the appropriate SIMD prefix as the mandatory prefix, if applicable

Signature
(compute-mandatory-prefix-for-three-byte-opcode proc-mode second-escape-byte opcode prefixes) → mandatory-prefix
Arguments: second-escape-byte — Second byte of the three-byte opcode; either 0x38 or 0x3A.; opcode — Third byte of the three-byte opcode.
Returns: mandatory-prefix — Type (unsigned-byte-p 8 mandatory-prefix).

Definitions and Theorems

Function: compute-mandatory-prefix-for-three-byte-opcode$inline

(defun compute-mandatory-prefix-for-three-byte-opcode$inline
       (proc-mode second-escape-byte opcode prefixes)
  (declare (type (integer 0 4) proc-mode)
           (type (unsigned-byte 8)
                 second-escape-byte)
           (type (unsigned-byte 8) opcode)
           (type (unsigned-byte 52) prefixes))
  (declare (xargs :guard (or (equal second-escape-byte 56)
                             (equal second-escape-byte 58))))
  (case second-escape-byte
    (56 (compute-mandatory-prefix-for-0f-38-three-byte-opcode
             proc-mode opcode prefixes))
    (58 (compute-mandatory-prefix-for-0f-3a-three-byte-opcode
             proc-mode opcode prefixes))
    (otherwise 0)))

Theorem: return-type-of-compute-mandatory-prefix-for-three-byte-opcode

(defthm
      return-type-of-compute-mandatory-prefix-for-three-byte-opcode
  (b* ((mandatory-prefix (compute-mandatory-prefix-for-three-byte-opcode$inline
                              proc-mode
                              second-escape-byte opcode prefixes)))
    (unsigned-byte-p 8 mandatory-prefix))
  :rule-classes :rewrite)