		Search-engine friendly clone of the ACL2 documentation.

Gpr-indices

Reg-indexp

Valid GPR index recognizer

Signature
(reg-indexp reg rex-byte) → *

General-purpose register indices are 3 bits except in 64-bit mode, where they can have 4 bits depending on the rex prefix.

Definitions and Theorems

Function: reg-indexp

(defun reg-indexp (reg rex-byte)
  (declare (type (unsigned-byte 8) rex-byte))
  (let ((__function__ 'reg-indexp))
    (declare (ignorable __function__))
    (if (eql rex-byte 0)
        (n03p reg)
      (n04p reg))))

Theorem: reg-indexp-for-3-bits

(defthm reg-indexp-for-3-bits
  (implies (and (syntaxp (quotep reg)) (n03p reg))
           (reg-indexp reg rex)))

Theorem: reg-indexp-logand-7

(defthm reg-indexp-logand-7
  (implies (n08p rex-byte)
           (reg-indexp (loghead 3 modr/m)
                       rex-byte)))