		Search-engine friendly clone of the ACL2 documentation.

Select-insts

Select instructions satisfying some conditions, and then either remove the selection or keep only the selection

Signature
(select-insts inst-lst &key (get/rem ':get) (opcode 'nil) (mode 'nil) (prefix 'nil) (vex? 'nil) (fn? 'nil)) → new-inst-lst
Arguments: inst-lst — Guard (inst-list-p inst-lst).; get/rem — Either get or remove the selected instructions.
Guard (member-equal get/rem '(:get :rem)).; opcode — If specified, select all instructions with the same opcode.
Guard (or (eql opcode nil) (24bits-p opcode)).; mode — If specified, select all instructions with the same mode of operation.
Guard (op-mode-p mode).; prefix — If specified, select all instructions with the same prefix.
Guard (op-pfx-p prefix).; vex? — If t, select all instructions with a non-nil opcode.vex field.
Guard (booleanp vex?).; fn? — If t, select all instructions with a non-nil inst.fn field.
Guard (booleanp fn?).
Returns: new-inst-lst — Type (inst-list-p new-inst-lst), given (inst-list-p inst-lst).

Definitions and Theorems

Function: select-insts-fn

(defun select-insts-fn
       (inst-lst get/rem opcode mode prefix vex? fn?)
 (declare (xargs :guard (and (inst-list-p inst-lst)
                             (member-equal get/rem '(:get :rem))
                             (or (eql opcode nil) (24bits-p opcode))
                             (op-mode-p mode)
                             (op-pfx-p prefix)
                             (booleanp vex?)
                             (booleanp fn?))))
 (let ((__function__ 'select-insts))
   (declare (ignorable __function__))
   (b* (((when (endp inst-lst)) nil)
        (rest (select-insts (cdr inst-lst)
                            :get/rem get/rem
                            :opcode opcode
                            :mode mode
                            :prefix prefix
                            :vex? vex?
                            :fn? fn?))
        (inst (car inst-lst))
        ((inst inst))
        ((opcode inst.opcode))
        (match? (and (if (not opcode)
                         t
                       (equal opcode inst.opcode.op))
                     (if (not mode)
                         t
                       (equal mode inst.opcode.mode))
                     (if (not prefix)
                         t
                       (if (equal prefix :no-prefix)
                           (or (equal prefix inst.opcode.pfx)
                               (not inst.opcode.pfx))
                         (equal prefix inst.opcode.pfx)))
                     (if (not vex?)
                         t
                       (if inst.opcode.vex t nil))
                     (if (not fn?) t (if inst.fn t nil)))))
     (if (eql get/rem :get)
         (append (and match? (list inst)) rest)
       (append (if match? nil (list inst))
               rest)))))

Theorem: inst-list-p-of-select-insts

(defthm inst-list-p-of-select-insts
 (implies
   (inst-list-p inst-lst)
   (b* ((new-inst-lst
             (select-insts-fn inst-lst
                              get/rem opcode mode prefix vex? fn?)))
     (inst-list-p new-inst-lst)))
 :rule-classes :rewrite)