(compute-modr/m-for-opcodes first-opcode num-opcodes inst-lst) → computed-table
Function:
(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:
(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)