		Search-engine friendly clone of the ACL2 documentation.

Legacy-prefixes-decoding

Inst-list-prefix-byte-group-code

Takes in a list of instructions and returns prefix byte group code for each of the constituent instructions

Signature
(inst-list-prefix-byte-group-code first-opcode num-opcodes inst-lst) → *
Arguments: first-opcode — Guard (24bits-p first-opcode).; num-opcodes — Guard (natp num-opcodes).; inst-lst — Guard (inst-list-p inst-lst).

Source: Intel Manuals, Vol. 2, Section 2.1.1.

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

Definitions and Theorems

Function: inst-list-prefix-byte-group-code

(defun inst-list-prefix-byte-group-code
       (first-opcode num-opcodes inst-lst)
 (declare (xargs :guard (and (24bits-p first-opcode)
                             (natp num-opcodes)
                             (inst-list-p inst-lst))))
 (let ((__function__ 'inst-list-prefix-byte-group-code))
  (declare (ignorable __function__))
  (b* (((when (zp num-opcodes)) nil)
       (rest (if (24bits-p (1+ first-opcode))
                 (inst-list-prefix-byte-group-code (1+ first-opcode)
                                                   (1- num-opcodes)
                                                   inst-lst)
               (er hard? 'inst-list-prefix-byte-group-code
                   "Illegal opcode ~s0.~%"
                   (str::hexify (1+ first-opcode)))))
       (same-opcode-insts (select-insts inst-lst
                                        :opcode first-opcode))
       ((when (equal (len same-opcode-insts) 1))
        (cons (inst-prefix-byte-group-code (car same-opcode-insts))
              rest)))
    (cons 0 rest))))