• 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
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
        • Virtualization-for-validation
          • Virtualization-for-validation-debugging
          • Virtualization-for-validation-limitations
          • Dump-virtualizable-state
          • Write-virtualizable-mem
          • Validate-insts
          • Run-until-rip-or-n
          • Validate-inst
          • Write-val1
          • Write-bytes
        • Dynamic-instrumentation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Virtualization-for-validation

Dump-virtualizable-state

Write the a subset of the model state to a file in a format that can be read by our virtualization-for-validation tools.

Signature

(dump-virtualizable-state filename x86 state) → state

Definitions and Theorems

Function: dump-virtualizable-state

(defun dump-virtualizable-state (filename x86 state)
  (declare (xargs :stobjs (x86 state)))
  (declare (xargs :guard t))
  (let ((__function__ 'dump-virtualizable-state))
    (declare (ignorable __function__))
    (b* (((mv channel state)
          (open-output-channel filename
                               :byte state))
         ((mv state size)
          (write-packed-struct-with-size
               ((64 (rgfi 0 x86))
                (64 (rgfi 1 x86))
                (64 (rgfi 2 x86))
                (64 (rgfi 3 x86))
                (64 (rgfi 4 x86))
                (64 (rgfi 5 x86))
                (64 (rgfi 6 x86))
                (64 (rgfi 7 x86))
                (64 (rgfi 8 x86))
                (64 (rgfi 9 x86))
                (64 (rgfi 10 x86))
                (64 (rgfi 11 x86))
                (64 (rgfi 12 x86))
                (64 (rgfi 13 x86))
                (64 (rgfi 14 x86))
                (64 (rgfi 15 x86))
                (64 (rip x86))
                (32 (rflags x86))
                (16 (seg-visiblei *cs* x86))
                (64 (seg-hidden-basei *cs* x86))
                (32 (seg-hidden-limiti *cs* x86))
                (16 (seg-hidden-attri *cs* x86))
                (16 (seg-visiblei *ds* x86))
                (64 (seg-hidden-basei *ds* x86))
                (32 (seg-hidden-limiti *ds* x86))
                (16 (seg-hidden-attri *ds* x86))
                (16 (seg-visiblei *es* x86))
                (64 (seg-hidden-basei *es* x86))
                (32 (seg-hidden-limiti *es* x86))
                (16 (seg-hidden-attri *es* x86))
                (16 (seg-visiblei *fs* x86))
                (64 (seg-hidden-basei *fs* x86))
                (32 (seg-hidden-limiti *fs* x86))
                (16 (seg-hidden-attri *fs* x86))
                (16 (seg-visiblei *gs* x86))
                (64 (seg-hidden-basei *gs* x86))
                (32 (seg-hidden-limiti *gs* x86))
                (16 (seg-hidden-attri *gs* x86))
                (16 (seg-visiblei *ss* x86))
                (64 (seg-hidden-basei *ss* x86))
                (32 (seg-hidden-limiti *ss* x86))
                (16 (seg-hidden-attri *ss* x86))
                (16 (ssr-visiblei *tr* x86))
                (64 (ssr-hidden-basei *tr* x86))
                (32 (ssr-hidden-limiti *tr* x86))
                (16 (ssr-hidden-attri *tr* x86))
                (16 (ssr-visiblei *ldtr* x86))
                (64 (ssr-hidden-basei *ldtr* x86))
                (32 (ssr-hidden-limiti *ldtr* x86))
                (16 (ssr-hidden-attri *ldtr* x86))
                (80 (stri *gdtr* x86))
                (80 (stri *idtr* x86))
                (64 (ctri *cr0* x86))
                (64 (ctri *cr2* x86))
                (64 (ctri *cr3* x86))
                (64 (ctri *cr4* x86))
                (64 (ctri *cr8* x86))
                (64 (msri *ia32_efer-idx* x86))
                (64 (msri *ia32_fs_base-idx* x86))
                (64 (msri *ia32_gs_base-idx* x86)))
               channel state))
         (size (logtail 3 size))
         (offset (+ size (logand (- size) (- 4096 1))))
         (padding (- offset size))
         (state (write-bytes (acl2::repeat padding 0)
                             channel state))
         (state (write-virtualizable-mem 0 (ash 1 32)
                                         channel x86 state))
         (state (close-output-channel channel state)))
      state)))