		Search-engine friendly clone of the ACL2 documentation.

Filtering-instructions

Select-opcode-map

Signature
(select-opcode-map map-key) → inst-lst
Arguments: map-key — Guard (keywordp map-key).
Returns: inst-lst — Type (inst-list-p inst-lst), given the guard.

Definitions and Theorems

Function: select-opcode-map

(defun select-opcode-map (map-key)
 (declare (xargs :guard (keywordp map-key)))
 (declare
  (xargs
       :guard
       (member-equal map-key
                     '(:one-byte :two-byte
                                 :0f-38-three-byte :0f-3a-three-byte
                                 :vex-0f :vex-0f-38
                                 :vex-0f-3a :evex-0f
                                 :evex-0f-38 :evex-0f-3a))))
 (let ((__function__ 'select-opcode-map))
   (declare (ignorable __function__))
   (case map-key
     (:one-byte *one-byte-opcode-map*)
     ((:two-byte :vex-0f :evex-0f)
      *two-byte-opcode-map*)
     ((:0f-38-three-byte :vex-0f-38 :evex-0f-38)
      *0f-38-three-byte-opcode-map*)
     ((:0f-3a-three-byte :vex-0f-3a :evex-0f-3a)
      *0f-3a-three-byte-opcode-map*))))

Theorem: inst-list-p-of-select-opcode-map

(defthm inst-list-p-of-select-opcode-map
 (implies
  (and (keywordp map-key)
       (member-equal map-key
                     '(:one-byte :two-byte
                                 :0f-38-three-byte :0f-3a-three-byte
                                 :vex-0f :vex-0f-38
                                 :vex-0f-3a :evex-0f
                                 :evex-0f-38 :evex-0f-3a)))
  (b* ((inst-lst (select-opcode-map map-key)))
    (inst-list-p inst-lst)))
 :rule-classes :rewrite)