		Search-engine friendly clone of the ACL2 documentation.

Modr/m-detection

Inst-needs-modr/m-p

Given an inst-p, determine whether it requires a ModR/M byte or not.

Signature
(inst-needs-modr/m-p inst) → *
Arguments: inst — Guard (inst-p inst).

Definitions and Theorems

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