		Search-engine friendly clone of the ACL2 documentation.

Prefix-modrm-sib-decoding

Modr/m-detection

Utilities to detect which opcodes need a ModR/M byte

Definitions and Theorems

Function: operand-needs-modr/m-p

(defun operand-needs-modr/m-p (operand)
 (declare (xargs :guard (operand-type-p operand)))
 (let ((__function__ 'operand-needs-modr/m-p))
  (declare (ignorable __function__))
  (b* (((when (null operand)) nil)
       (zop (car operand)))
   (cdr (assoc-equal
             :modr/m?
             (cdr (assoc-equal zop *z-addressing-method-info*)))))))

Function: inst-needs-modr/m-p

(defun inst-needs-modr/m-p (inst)
  (declare (xargs :guard (inst-p inst)))
  (let ((__function__ 'inst-needs-modr/m-p))
    (declare (ignorable __function__))
    (b* (((inst inst))
         (opcode inst.opcode)
         ((opcode opcode))
         ((when (or (member-equal :|1A| opcode.superscripts)
                    (member-equal :|1C| opcode.superscripts)))
          t)
         (operands inst.operands)
         ((unless operands) nil)
         ((operands operands)))
      (or (operand-needs-modr/m-p operands.op1)
          (operand-needs-modr/m-p operands.op2)
          (operand-needs-modr/m-p operands.op3)
          (operand-needs-modr/m-p operands.op4)))))

Function: any-inst-needs-modr/m-p

(defun any-inst-needs-modr/m-p (inst-lst)
  (declare (xargs :guard (inst-list-p inst-lst)))
  (let ((__function__ 'any-inst-needs-modr/m-p))
    (declare (ignorable __function__))
    (if (endp inst-lst)
        nil
      (or (inst-needs-modr/m-p (car inst-lst))
          (any-inst-needs-modr/m-p (cdr inst-lst))))))

Function: compute-modr/m-for-opcodes

(defun compute-modr/m-for-opcodes
       (first-opcode num-opcodes inst-lst)
  (declare (xargs :guard (and (24bits-p first-opcode)
                              (natp num-opcodes)
                              (inst-list-p inst-lst))))
  (let ((__function__ 'compute-modr/m-for-opcodes))
    (declare (ignorable __function__))
    (b* (((when (zp num-opcodes)) nil)
         (rest (if (24bits-p (1+ first-opcode))
                   (compute-modr/m-for-opcodes (1+ first-opcode)
                                               (1- num-opcodes)
                                               inst-lst)
                 (er hard? 'compute-modr/m-for-opcodes
                     "Illegal opcode ~s0.~%"
                     (str::hexify (1+ first-opcode)))))
         (same-opcode-insts (select-insts inst-lst
                                          :opcode first-opcode))
         ((when (endp same-opcode-insts))
          (cons 0 rest)))
      (cons (if (any-inst-needs-modr/m-p same-opcode-insts)
                1
              0)
            rest))))

Theorem: true-listp-of-compute-modr/m-for-opcodes

(defthm true-listp-of-compute-modr/m-for-opcodes
 (b*
  ((computed-table
    (compute-modr/m-for-opcodes first-opcode num-opcodes inst-lst)))
  (true-listp computed-table))
 :rule-classes :rewrite)

Subtopics

Compute-modr/m-for-opcodes
Inst-needs-modr/m-p: Given an inst-p, determine whether it requires a ModR/M byte or not.
Operand-needs-modr/m-p: True if operand needs a modr/m byte
Any-inst-needs-modr/m-p: Does any instruction in inst-lst require a ModR/M byte?