		Search-engine friendly clone of the ACL2 documentation.

Modr/m-detection

Compute-modr/m-for-opcodes

Signature
(compute-modr/m-for-opcodes first-opcode num-opcodes inst-lst) → computed-table
Arguments: first-opcode — Guard (24bits-p first-opcode).; num-opcodes — Guard (natp num-opcodes).; inst-lst — Guard (inst-list-p inst-lst).
Returns: computed-table — Type (true-listp computed-table).

Definitions and Theorems

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)