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

• Machine
• Opcode-maps

Cpuid

Determining which CPUID features are supported in x86isa

We introduce a constrained function cpuid-flag-fn, which takes the following inputs:

1. eax: 32-bit leaf index
2. ecx: 32-bit sub-leaf index, where applicable
3. reg: index of the output general-purpose register (eax, ebx, ecx, or edx)
4. bit: relevant LSB of reg (0-63)
5. width: width of the flag field of the output register

The only constraint about the return value of this function is that it must be return a natural number of width width. During proofs, you would need to add appropriate hypotheses to your theorems about the values returned by cpuid-flag-fn for a given CPUID leaf, sub-leaf, and relevant output indexing information (i.e., reg and bit). During execution, you can use defattach to execute this function. By default, we use the function default-cpuid-flag-fn as an attachment. Feel free, of course, to use your own attachment, where you can choose to case-split on the leaf/sub-leaf of the CPUID.

We also provide macros the following macros to access CPUID feature flags conveniently.

This constrained function used to take the x86 state as additional argument. This allowed the CPUID features to depend on the state, and potentially to change during execution. However, this was causing the generation of proof goals involving potentially different CPUID feature values before and after any operation on the x86 state, because even innocuous operations like writing to a register give different x86 states and thus potentially different CPUID features. It seems clear that most, if not all, CPUID features should be independent from the x86 state; it is yet unclear whether a few of them might depend on the state. However, if they may change from one state to the other, it seems reasonable for that to happen via particular explicit operations. Since none of the state transitions covered by our formal model causes any changes to CPUID features (not because we ignore the potential change in our modeling, but because the parts of the Intel and AMD documentation that our modeled state transitions are based on neither say nor imply anything about CPUID feature changes), it seemed safe to remove the x86 state from this function's arguments. An oddity of having the x86 state as an argument is that the x86 state argument may have its own values in EAX, ECX, etc., which may differ from the corresponding values passed to the function, which has explicit parameters for those; there is nothing really wrong with this, but it is a sort of redundancy in the inputs of these function and a potential inconsistency between their values as arguments and the corresponding values in the x86 state, and therefore not fully satisfactory. If we ever find that some CPUID features may change during execution, we will extend the model of the x86 state with information about the current values of those features, and we will amend this constrained function to read them from the state.

(cpuid-flag eax &key (ecx '0) (reg '0) (bit '0) (width '1)) (feature-flag feature-flag)

Definitions and Theorems

Theorem: natp-cpuid-flag-fn

(defthm natp-cpuid-flag-fn
  (natp (cpuid-flag-fn eax ecx reg bit width))
  :rule-classes (:type-prescription))

Theorem: unsigned-byte-width-of-cpuid-flag-fn

(defthm unsigned-byte-width-of-cpuid-flag-fn
  (implies (posp width)
           (unsigned-byte-p width
                            (cpuid-flag-fn eax ecx reg bit width))))

Function: default-cpuid-flag-fn

(defun default-cpuid-flag-fn (eax ecx reg bit width)
  (declare (type (unsigned-byte 32) eax)
           (type (unsigned-byte 32) ecx)
           (type (integer 0 63) bit)
           (type (integer 1 32) width))
  (declare (xargs :guard (or (equal reg 0)
                             (equal reg 3)
                             (equal reg 1)
                             (equal reg 2))))
  (let ((__function__ 'default-cpuid-flag-fn))
    (declare (ignorable __function__))
    (case eax
      (2147483656 (case reg
                    (0 (case bit
                         (0 (if (equal width 8) 52 0))
                         (8 (if (equal width 8) 48 0))
                         (t 0)))
                    (t 1)))
      (t 1))))

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

Function: feature-flags

(defun feature-flags (features)
 (declare (xargs :guard (true-listp features)))
 (declare
  (xargs :guard (subsetp-equal features *supported-feature-flags*)))
 (let ((__function__ 'feature-flags))
   (declare (ignorable __function__))
   (cond ((atom features) 1)
         ((eql (feature-flag (first features)) 0)
          0)
         (t (feature-flags (rest features))))))

Subtopics

Feature-flag

Default-cpuid-flag-fn

Feature-flags