• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • 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-byte-list1
        • Setting-up-page-tables
        • Init-zero-page
        • Load-file-into-memory
        • Linux-load
        • 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
      • Booting-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

A convenient function to populate the x86 state's instruction pointer, registers, and memory.

Signature

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

Returns

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

Definitions and Theorems

Function: init-x86-state

(defun init-x86-state (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))
   (declare (ignorable __function__))
   (b* ((x86 (!ms status x86))
        (x86 (!fault status x86))
        (x86 (!rip start-addr x86))
        ((mv flg0 x86)
         (load-program-into-memory mem x86))
        ((when flg0)
         (mv (cons 'load-program-into-memory flg0)
             x86))
        (x86 (!rgfi-from-alist gprs x86))
        (x86 (!msri-from-alist msrs x86))
        (x86 (!ctri-from-alist ctrs x86))
        (x86 (!seg-visiblei-from-alist seg-visibles x86))
        (x86 (!seg-hidden-basei-from-alist seg-hidden-bases x86))
        (x86 (!seg-hidden-limiti-from-alist seg-hidden-limits x86))
        (x86 (!seg-hidden-attri-from-alist seg-hidden-attrs x86))
        (x86 (!rflags (n32 flags) x86)))
     (mv nil x86))))

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

(defthm x86p-of-init-x86-state.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 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)