		Search-engine friendly clone of the ACL2 documentation.

Legacy-prefixes-decoding

Inst-prefix-byte-group-code

Takes in a single instruction and figures out if it is a prefix byte; if so, the prefix group number is returned.

Signature
(inst-prefix-byte-group-code inst) → *
Arguments: inst — Guard (inst-p inst).

The return value 0 corresponds to "not a prefix" and 1, 2, 3 and 4 correspond to the prefix group of byte.

Note that legacy prefixes are a part of the one-byte opcode map.

Definitions and Theorems

Function: inst-prefix-byte-group-code

(defun inst-prefix-byte-group-code (inst)
  (declare (xargs :guard (inst-p inst)))
  (let ((__function__ 'inst-prefix-byte-group-code))
    (declare (ignorable __function__))
    (b* (((inst inst)))
      (cond ((keywordp inst.mnemonic)
             (case inst.mnemonic
               (:prefix-lock 1)
               (:prefix-repne 1)
               (:prefix-rep/repe 1)
               (:prefix-es 2)
               (:prefix-cs 2)
               (:prefix-ss 2)
               (:prefix-ds 2)
               (:prefix-fs 2)
               (:prefix-gs 2)
               (:prefix-opsize 3)
               (:prefix-addrsize 4)
               (t 0)))
            (t 0)))))