		Search-engine friendly clone of the ACL2 documentation.

Prefix-modrm-sib-decoding

Instructions-with-mandatory-prefixes

Based off opcode-maps, pre-computing the opcodes that have a valid instruction corresponding to the following prefixes: :NO-PREFIX :66 :F3 :F2.

Definitions and Theorems

Function: opcode-present?

(defun opcode-present? (first-opcode num-opcodes inst-lst)
  (declare (xargs :guard (and (24bits-p first-opcode)
                              (natp num-opcodes)
                              (inst-list-p inst-lst))))
  (let ((__function__ 'opcode-present?))
    (declare (ignorable __function__))
    (b* (((when (zp num-opcodes)) nil)
         (rest (if (24bits-p (1+ first-opcode))
                   (opcode-present? (1+ first-opcode)
                                    (1- num-opcodes)
                                    inst-lst)
                 (er hard? 'opcode-present?
                     "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 1 rest))))

Theorem: true-listp-of-opcode-present?

(defthm true-listp-of-opcode-present?
  (b* ((lst (opcode-present? first-opcode num-opcodes inst-lst)))
    (true-listp lst))
  :rule-classes :rewrite)

Subtopics

Opcode-present?: Returns a 256-element list, where a 1 at a position i denotes that at least one instruction with opcode i exists in inst-lst; 0 denotes no such instruction is present.