• 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
            • 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))))