• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
            • X86isa-state-history
            • Environment-field
            • Physical-memory-model
            • Save-restore
              • Restore-x86
              • Save-x86
          • 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
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • X86isa-state

Save-restore

Tools for saving and restoring the x86 state

While most ACL2 objects can be serialized using ACL2::serialize, stobjs can not. The x86 state is an absstobj, so we can't directly use serialize. Instead, we convert the state, excluding the memory, into a cons tree and write that out to a file with serialize. Then, we write the low n bytes, where n is user specified, of memory out to disk in another file, thereby avoiding constructing a potentially very large cons tree. Restoring the state is essentially the process in reverse.

Subtopics

Restore-x86
Save-x86