• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
            • Feature-flag
              • Default-cpuid-flag-fn
              • Feature-flags
            • Linear-memory
            • Rflag-specifications
            • Characterizing-undefined-behavior
            • Top-level-memory
            • App-view
            • 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
                  • Feature-flag
                    • Default-cpuid-flag-fn
                    • Feature-flags
                  • Opcode-maps-structures
                  • Implemented-opcodes
                  • Chk-exc-fn
                  • Filtering-instructions
                  • 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
      • Cpuid

      Feature-flag

      Signature
      (feature-flag feature-flag) → *

      Definitions and Theorems

      Function: feature-flag

      (defun feature-flag (feature-flag)
        (declare (xargs :guard (member-equal feature-flag
                                             *supported-feature-flags*)))
        (let ((__function__ 'feature-flag))
          (declare (ignorable __function__))
          (case feature-flag
            (:sse3 (cpuid-flag 1 :reg 1 :bit 0))
            (:pclmulqdq (cpuid-flag 1 :reg 1 :bit 1))
            (:dtes64 (cpuid-flag 1 :reg 1 :bit 2))
            (:monitor (cpuid-flag 1 :reg 1 :bit 3))
            (:ds-cpl (cpuid-flag 1 :reg 1 :bit 4))
            (:vmx (cpuid-flag 1 :reg 1 :bit 5))
            (:smx (cpuid-flag 1 :reg 1 :bit 6))
            (:eist (cpuid-flag 1 :reg 1 :bit 7))
            (:tm2 (cpuid-flag 1 :reg 1 :bit 8))
            (:ssse3 (cpuid-flag 1 :reg 1 :bit 9))
            (:cnxt-id (cpuid-flag 1 :reg 1 :bit 10))
            (:sdbg (cpuid-flag 1 :reg 1 :bit 11))
            (:fma (cpuid-flag 1 :reg 1 :bit 12))
            (:cmpxchg16b (cpuid-flag 1 :reg 1 :bit 13))
            (:xtpr-up-ctrl (cpuid-flag 1 :reg 1 :bit 14))
            (:pdcm (cpuid-flag 1 :reg 1 :bit 15))
            (:pcid (cpuid-flag 1 :reg 1 :bit 17))
            (:dca (cpuid-flag 1 :reg 1 :bit 18))
            (:sse4.1 (cpuid-flag 1 :reg 1 :bit 19))
            (:sse4.2 (cpuid-flag 1 :reg 1 :bit 20))
            (:x2pic (cpuid-flag 1 :reg 1 :bit 21))
            (:movbe (cpuid-flag 1 :reg 1 :bit 22))
            (:popcnt (cpuid-flag 1 :reg 1 :bit 23))
            (:tsc-deadline (cpuid-flag 1 :reg 1 :bit 24))
            (:aes (cpuid-flag 1 :reg 1 :bit 25))
            (:xsave (cpuid-flag 1 :reg 1 :bit 26))
            (:osxsave (cpuid-flag 1 :reg 1 :bit 27))
            (:avx (cpuid-flag 1 :reg 1 :bit 28))
            (:f16c (cpuid-flag 1 :reg 1 :bit 29))
            (:rdrand (cpuid-flag 1 :reg 1 :bit 30))
            (:fpu (cpuid-flag 1 :reg 2 :bit 0))
            (:vme (cpuid-flag 1 :reg 2 :bit 1))
            (:de (cpuid-flag 1 :reg 2 :bit 2))
            (:pse (cpuid-flag 1 :reg 2 :bit 3))
            (:tsc (cpuid-flag 1 :reg 2 :bit 4))
            (:msr (cpuid-flag 1 :reg 2 :bit 5))
            (:pae (cpuid-flag 1 :reg 2 :bit 6))
            (:mce (cpuid-flag 1 :reg 2 :bit 7))
            (:cx8 (cpuid-flag 1 :reg 2 :bit 8))
            (:apic (cpuid-flag 1 :reg 2 :bit 9))
            (:sep (cpuid-flag 1 :reg 2 :bit 11))
            (:mtrr (cpuid-flag 1 :reg 2 :bit 12))
            (:pge (cpuid-flag 1 :reg 2 :bit 13))
            (:mca (cpuid-flag 1 :reg 2 :bit 14))
            (:cmov (cpuid-flag 1 :reg 2 :bit 15))
            (:pat (cpuid-flag 1 :reg 2 :bit 16))
            (:pse-36 (cpuid-flag 1 :reg 2 :bit 17))
            (:psn (cpuid-flag 1 :reg 2 :bit 18))
            (:clfsh (cpuid-flag 1 :reg 2 :bit 19))
            (:ds (cpuid-flag 1 :reg 2 :bit 21))
            (:acpi (cpuid-flag 1 :reg 2 :bit 22))
            (:mmx (cpuid-flag 1 :reg 2 :bit 23))
            (:fxsr (cpuid-flag 1 :reg 2 :bit 24))
            (:sse (cpuid-flag 1 :reg 2 :bit 25))
            (:sse2 (cpuid-flag 1 :reg 2 :bit 26))
            (:ss (cpuid-flag 1 :reg 2 :bit 27))
            (:htt (cpuid-flag 1 :reg 2 :bit 28))
            (:tm (cpuid-flag 1 :reg 2 :bit 29))
            (:pbe (cpuid-flag 1 :reg 2 :bit 31))
            (:fsgsbase (cpuid-flag 7 :ecx 0 :reg 3 :bit 0))
            (:ia32_tsc_adjust (cpuid-flag 7 :ecx 0 :reg 3 :bit 1))
            (:sgx (cpuid-flag 7 :ecx 0 :reg 3 :bit 2))
            (:bmi1 (cpuid-flag 7 :ecx 0 :reg 3 :bit 3))
            (:hle (cpuid-flag 7 :ecx 0 :reg 3 :bit 4))
            (:avx2 (cpuid-flag 7 :ecx 0 :reg 3 :bit 5))
            (:fdp_excptn_only (cpuid-flag 7 :ecx 0 :reg 3 :bit 6))
            (:smep (cpuid-flag 7 :ecx 0 :reg 3 :bit 7))
            (:bmi2 (cpuid-flag 7 :ecx 0 :reg 3 :bit 8))
            (:rep-movsb-stosb (cpuid-flag 7 :ecx 0 :reg 3 :bit 9))
            (:invpcid (cpuid-flag 7 :ecx 0 :reg 3 :bit 10))
            (:rtm (cpuid-flag 7 :ecx 0 :reg 3 :bit 11))
            (:rdt-m (cpuid-flag 7 :ecx 0 :reg 3 :bit 12))
            (:dep-fpu-cs-ds (cpuid-flag 7 :ecx 0 :reg 3 :bit 13))
            (:mpx (cpuid-flag 7 :ecx 0 :reg 3 :bit 14))
            (:rdt-a (cpuid-flag 7 :ecx 0 :reg 3 :bit 15))
            (:avx512f (cpuid-flag 7 :ecx 0 :reg 3 :bit 16))
            (:avx512dq (cpuid-flag 7 :ecx 0 :reg 3 :bit 17))
            (:rdseed (cpuid-flag 7 :ecx 0 :reg 3 :bit 18))
            (:adx (cpuid-flag 7 :ecx 0 :reg 3 :bit 19))
            (:smap (cpuid-flag 7 :ecx 0 :reg 3 :bit 20))
            (:avx512_ifma (cpuid-flag 7 :ecx 0 :reg 3 :bit 21))
            (:clflushopt (cpuid-flag 7 :ecx 0 :reg 3 :bit 23))
            (:clwb (cpuid-flag 7 :ecx 0 :reg 3 :bit 24))
            (:proc-trace (cpuid-flag 7 :ecx 0 :reg 3 :bit 25))
            (:avx512pf (cpuid-flag 7 :ecx 0 :reg 3 :bit 26))
            (:avx512er (cpuid-flag 7 :ecx 0 :reg 3 :bit 27))
            (:avx512cd (cpuid-flag 7 :ecx 0 :reg 3 :bit 28))
            (:sha (cpuid-flag 7 :ecx 0 :reg 3 :bit 29))
            (:avx512bw (cpuid-flag 7 :ecx 0 :reg 3 :bit 30))
            (:avx512vl (cpuid-flag 7 :ecx 0 :reg 3 :bit 31))
            (:prefetchwt1 (cpuid-flag 7 :ecx 0 :reg 1 :bit 0))
            (:avx512_vbmi (cpuid-flag 7 :ecx 0 :reg 1 :bit 1))
            (:umip (cpuid-flag 7 :ecx 0 :reg 1 :bit 2))
            (:pku (cpuid-flag 7 :ecx 0 :reg 1 :bit 3))
            (:ospke (cpuid-flag 7 :ecx 0 :reg 1 :bit 4))
            (:cet (cpuid-flag 7 :ecx 0 :reg 1 :bit 7))
            (:la57 (cpuid-flag 7 :ecx 0 :reg 1 :bit 16))
            (:mawau (cpuid-flag 7
                                :ecx 0
                                :reg 1
                                :bit 17
                                :width 5))
            (:rdpid (cpuid-flag 7 :ecx 0 :reg 1 :bit 22))
            (:sgx_lc (cpuid-flag 7 :ecx 0 :reg 1 :bit 30))
            (:pks (cpuid-flag 7 :ecx 0 :reg 1 :bit 31))
            (:avx512_4vnniw (cpuid-flag 7 :ecx 0 :reg 2 :bit 2))
            (:avx512_4fmaps (cpuid-flag 7 :ecx 0 :reg 2 :bit 3))
            (:x87-state (cpuid-flag 13 :ecx 0 :reg 0 :bit 0))
            (:sse-state (cpuid-flag 13 :ecx 0 :reg 0 :bit 1))
            (:avx-state (cpuid-flag 13 :ecx 0 :reg 0 :bit 2))
            (:mpx-state (cpuid-flag 13
                                    :ecx 0
                                    :reg 0
                                    :bit 3
                                    :width 2))
            (:avx512-state (cpuid-flag 13
                                       :ecx 0
                                       :reg 0
                                       :bit 5
                                       :width 3))
            (:ia32_xss_0 (cpuid-flag 13 :ecx 0 :reg 0 :bit 8))
            (:pkru (cpuid-flag 13 :ecx 0 :reg 0 :bit 9))
            (:ia32_xss_1 (cpuid-flag 13 :ecx 0 :reg 0 :bit 13))
            (:xsaveopt (cpuid-flag 13 :ecx 1 :reg 0 :bit 0))
            (:xsavec (cpuid-flag 13 :ecx 1 :reg 0 :bit 1))
            (:xgetbv (cpuid-flag 13 :ecx 1 :reg 0 :bit 2))
            (:xss (cpuid-flag 13 :ecx 1 :reg 0 :bit 3))
            (:lahf-sahf (cpuid-flag 2147483649 :reg 1 :bit 0))
            (:lzcnt (cpuid-flag 2147483649 :reg 1 :bit 5))
            (:prfchw (cpuid-flag 2147483649 :reg 1 :bit 8))
            (:sgx1 (cpuid-flag 2147483649 :reg 0 :bit 0))
            (:sgx2 (cpuid-flag 2147483649 :reg 0 :bit 1))
            (:syscall-sysret (cpuid-flag 2147483649 :reg 2 :bit 11))
            (:execute-disable (cpuid-flag 2147483649 :reg 2 :bit 20))
            (:1g-pages (cpuid-flag 2147483649 :reg 2 :bit 26))
            (:rdtscp (cpuid-flag 2147483649 :reg 2 :bit 27))
            (:intel64 (cpuid-flag 2147483649 :reg 2 :bit 29))
            (:maxphyaddr (cpuid-flag 2147483656
                                     :reg 0
                                     :bit 0
                                     :width 8))
            (:linearaddr (cpuid-flag 2147483656
                                     :reg 0
                                     :bit 8
                                     :width 8))
            (otherwise 0))))