		Search-engine friendly clone of the ACL2 documentation.

Prefix-modrm-sib-decoding

Legacy-prefixes-decoding

Functions to detect and decode legacy prefixes

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)))))

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))))

Function: get-one-byte-prefix-array-code

(defun get-one-byte-prefix-array-code (byte)
  (declare (type (unsigned-byte 8) byte))
  (let ((__function__ 'get-one-byte-prefix-array-code))
    (declare (ignorable __function__))
    (aref1 'one-byte-prefixes-group-code-info
           *one-byte-prefixes-group-code-info-ar*
           (mbe :logic (loghead 8 byte)
                :exec byte))))

Theorem: natp-of-get-one-byte-prefix-array-code

(defthm natp-of-get-one-byte-prefix-array-code
  (b* ((code (get-one-byte-prefix-array-code byte)))
    (natp code))
  :rule-classes (:rewrite :type-prescription))

Theorem: upper-bound-get-one-byte-prefix-array-code

(defthm upper-bound-get-one-byte-prefix-array-code
  (<= (get-one-byte-prefix-array-code x)
      4))

Subtopics

Inst-list-prefix-byte-group-code: Takes in a list of instructions and returns prefix byte group code for each of the constituent instructions
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.
Get-one-byte-prefix-array-code