• 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
        • 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
          • 64-bit-modep
          • X86-operation-mode
        • 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

• X86-modes

64-bit-modep

Check whether we are in 64-bit mode.

Signature

(64-bit-modep x86) → *

Given the modeling assumption stated in x86-modes, this predicate discriminates between 64-bit mode and the other two modes (collectively, 32-bit mode). Based on Intel manual, Mar'17, Vol. 3A, Sec. 2.2 (near Fig. 2-3), the discrimination is based on the IA32_EFER.LME and CS.L bits: if they are both 1, we are in 64-bit mode, otherwise we are in 32-bit mode (protected mode if IA32_EFER.LME is 0, compatibility mode if IA32_EFER.LME is 1 and CS.L is 0; note that when IA32_EFER.LME is 0, CS.L should be 0, according to Intel manual, Mar'17, Vol. 3A, Sec. 3.4.5).

This predicate does not include state invariants such as the constraints imposed by the 64-bit mode consistency checks described in Intel manual, Mar'17, Vol. 3A, Sec. 9.8.5.

This predicate is useful as a hypothesis of theorems about either 64-bit or 32-bit mode.

Since (xr :msr ... x86) returns a 64-bit value but the IA32_EFER register consists of 12 bits. So we use n12 to make ia32_eferBits functions applicable.

Definitions and Theorems

Function: 64-bit-modep

(defun 64-bit-modep (x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard t))
 (mbe
    :logic
    (b* ((ia32_efer (n12 (msri 0 x86)))
         (ia32_efer.lma (ia32_eferbits->lma ia32_efer))
         (cs-attr (seg-hidden-attri 1 x86))
         (cs.l (code-segment-descriptor-attributesbits->l cs-attr)))
      (and (equal ia32_efer.lma 1)
           (equal cs.l 1)))
    :exec
    (b* (((the (unsigned-byte 32)
               ia32_efer-low-32)
          (bitsets::bignum-extract (msri 0 x86)
                                   0))
         ((the (unsigned-byte 12) ia32_efer)
          (mbe :logic (n12 ia32_efer-low-32)
               :exec (logand 4095
                             (the (unsigned-byte 32)
                                  ia32_efer-low-32))))
         (ia32_efer.lma (ia32_eferbits->lma ia32_efer))
         ((the (unsigned-byte 16) cs-attr)
          (seg-hidden-attri 1 x86))
         (cs.l (code-segment-descriptor-attributesbits->l cs-attr)))
      (and (equal ia32_efer.lma 1)
           (equal cs.l 1)))))

Theorem: 64-bit-modep-of-xw

(defthm 64-bit-modep-of-xw
  (implies (and (not (equal fld :msr))
                (not (equal fld :seg-hidden-attr)))
           (equal (64-bit-modep (xw fld index value x86))
                  (64-bit-modep x86))))

Theorem: 64-bit-modep-of-write-user-rflags

(defthm 64-bit-modep-of-write-user-rflags
  (equal (64-bit-modep (write-user-rflags vector mask x86))
         (64-bit-modep x86)))