• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • X86isa-state
        • Syscalls
        • Cpuid
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • App-view
        • Top-level-memory
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
          • Two-byte-opcodes
          • One-byte-opcodes
          • Fp-opcodes
          • Instruction-semantic-functions
          • X86-illegal-instruction
          • Implemented-opcodes
          • Opcode-maps
            • Cpuid
            • Opcode-maps-structures
            • Implemented-opcodes
            • Chk-exc-fn
            • Filtering-instructions
              • Select-insts
              • Remove-insts-with-feat
              • Keep-insts-with-feat
              • Select-opcode-map
            • Addressing-method-code-p
            • Operand-type-code-p
            • Eval-pre-map
          • X86-general-protection
          • X86-device-not-available
          • X86-step-unimplemented
          • Privileged-opcodes
          • Three-byte-opcodes
        • Register-readers-and-writers
        • X86-modes
        • Segmentation
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Quote
• Filtering-instructions

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)