• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
        • Dynamic-instrumentation
        • Initialize-x86-state
          • Init-x86-state-64
          • Load-program-into-memory
          • Init-x86-state
          • !seg-hidden-limiti-from-alist
          • !seg-hidden-basei-from-alist
          • !seg-hidden-attri-from-alist
          • Seg-hidden-limiti-alistp
          • Seg-hidden-basei-alistp
          • !seg-visiblei-from-alist
          • Seg-visiblei-alistp
          • Seg-hidden-attri-alistp
          • Rgfi-alistp
          • N64p-byte-alistp
          • !rgfi-from-alist
          • !msri-from-alist
          • !ctri-from-alist
          • Msri-alistp
          • Ctri-alistp
        • Binary-file-load-fn
        • Read-channel-into-memory
        • Setting-up-page-tables
        • Read-channel-into-byte-list
        • Init-zero-page
        • Linux-load
        • Read-file-into-memory
        • Read-file-into-byte-list
        • Init-sys-view
        • Load-elf-sections
        • Chars-to-c-str
        • String-to-c-str
        • Pack-u64
        • Pack-u32
        • Concrete-simulation-examples
        • Gdt-entry
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Initialize-x86-state

Init-x86-state-64

A variant of init-x86-state that ensures 64-bit mode.

Signature

(init-x86-state-64 status 
                   start-addr gprs ctrs msrs seg-visibles 
                   seg-hidden-bases seg-hidden-limits 
                   seg-hidden-attrs flags mem x86) 
 
  → 
(mv flg x86)

Arguments

start-addr — Guard (canonical-address-p start-addr).

gprs — Guard (rgfi-alistp gprs).

ctrs — Guard (ctri-alistp ctrs).

msrs — Guard (msri-alistp msrs).

seg-visibles — Guard (seg-visiblei-alistp seg-visibles).

seg-hidden-bases — Guard (seg-hidden-basei-alistp seg-hidden-bases).

seg-hidden-limits — Guard (seg-hidden-limiti-alistp seg-hidden-limits).

seg-hidden-attrs — Guard (seg-hidden-attri-alistp seg-hidden-attrs).

flags — Guard (n64p flags).

mem — Guard (n64p-byte-alistp mem).

Returns

x86 — Type (x86p x86), given the guard.

After calling init-x86-state, this function updates x86 to ensure that 64-bit-modep holds. It does so by setting IA32_EFER.LMA and CS.L to 1.

The resulting state does not necessarily satisfy expected invariants for 64-bit mode, but that is also the case with init-x86-state.

In alternative, one can use just init-x86-state with appropriate model-specific and hidden segment register alists. But we find this function convenient for now.

Definitions and Theorems

Function: init-x86-state-64

(defun init-x86-state-64
       (status start-addr gprs ctrs msrs seg-visibles
               seg-hidden-bases seg-hidden-limits
               seg-hidden-attrs flags mem x86)
 (declare (xargs :stobjs (x86)))
 (declare
     (xargs :guard (and (canonical-address-p start-addr)
                        (rgfi-alistp gprs)
                        (ctri-alistp ctrs)
                        (msri-alistp msrs)
                        (seg-visiblei-alistp seg-visibles)
                        (seg-hidden-basei-alistp seg-hidden-bases)
                        (seg-hidden-limiti-alistp seg-hidden-limits)
                        (seg-hidden-attri-alistp seg-hidden-attrs)
                        (n64p flags)
                        (n64p-byte-alistp mem))))
 (let ((__function__ 'init-x86-state-64))
  (declare (ignorable __function__))
  (b*
   (((mv flg x86)
     (init-x86-state status
                     start-addr gprs ctrs msrs seg-visibles
                     seg-hidden-bases seg-hidden-limits
                     seg-hidden-attrs flags mem x86))
    ((when flg) (mv t x86))
    (ia32_efer (n12 (msri 0 x86)))
    (ia32_efer (!ia32_eferbits->lma 1 ia32_efer))
    (x86 (!msri 0 (n64 ia32_efer) x86))
    ((the (unsigned-byte 16) cs-attr)
     (seg-hidden-attri 1 x86))
    (cs-attr (!code-segment-descriptor-attributesbits->l 1 cs-attr))
    (x86 (!seg-hidden-attri 1 cs-attr x86)))
   (mv nil x86))))

Theorem: x86p-of-init-x86-state-64.x86

(defthm x86p-of-init-x86-state-64.x86
 (implies
     (and (x86p x86)
          (canonical-address-p$inline start-addr)
          (rgfi-alistp gprs)
          (ctri-alistp ctrs)
          (msri-alistp msrs)
          (seg-visiblei-alistp seg-visibles)
          (seg-hidden-basei-alistp seg-hidden-bases)
          (seg-hidden-limiti-alistp seg-hidden-limits)
          (seg-hidden-attri-alistp seg-hidden-attrs)
          (n64p$inline flags)
          (n64p-byte-alistp mem))
     (b* (((mv ?flg ?x86)
           (init-x86-state-64 status
                              start-addr gprs ctrs msrs seg-visibles
                              seg-hidden-bases seg-hidden-limits
                              seg-hidden-attrs flags mem x86)))
       (x86p x86)))
 :rule-classes :rewrite)

Theorem: 64-bit-modep-of-init-x86-state-64

(defthm 64-bit-modep-of-init-x86-state-64
  (b* (((mv flg x86-new)
        (init-x86-state-64 status
                           start-addr gprs ctrs msrs seg-visibles
                           seg-hidden-bases seg-hidden-limits
                           seg-hidden-attrs flags mem x86)))
    (implies (not flg)
             (64-bit-modep x86-new))))