• 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
        • Dynamic-instrumentation
        • Initialize-x86-state
        • 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
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Program-execution

Init-zero-page

Signature

(init-zero-page zero-page-ptr command-line-ptr 
                disk-image-ptr disk-image-size 
                kernel-ptr kernel-image x86) 
 
  → 
x86

Arguments

zero-page-ptr — Guard (canonical-address-p zero-page-ptr).

command-line-ptr — Guard (canonical-address-p command-line-ptr).

disk-image-ptr — Guard (canonical-address-p disk-image-ptr).

disk-image-size — Guard (natp disk-image-size).

kernel-ptr — Guard (n32p kernel-ptr).

kernel-image — Guard (byte-listp kernel-image).

Definitions and Theorems

Function: init-zero-page

(defun init-zero-page (zero-page-ptr command-line-ptr
                                     disk-image-ptr disk-image-size
                                     kernel-ptr kernel-image x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (and (canonical-address-p zero-page-ptr)
                             (canonical-address-p command-line-ptr)
                             (canonical-address-p disk-image-ptr)
                             (natp disk-image-size)
                             (n32p kernel-ptr)
                             (byte-listp kernel-image))))
 (declare
  (xargs :guard (and (canonical-address-p (+ zero-page-ptr 4095)))))
 (let ((__function__ 'init-zero-page))
   (declare (ignorable __function__))
   (b*
    (((unless (> (len kernel-image) 529))
      x86)
     ((unless (> (len kernel-image) (+ 620 497)))
      x86)
     (setup-header (take 620 (nthcdr 497 kernel-image)))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 497)
                             setup-header x86))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 506)
                             '(255 255)
                             x86))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 528)
                             '(255)
                             x86))
     (loadflags (logand (nth 529 kernel-image) 95))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 529)
                             (list loadflags)
                             x86))
     ((mv & x86)
      (write-bytes-to-memory (+ zero-page-ptr 532)
                             (pack-u32 kernel-ptr)
                             x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 536)
           (pack-u32 (logand 4294967295 disk-image-ptr))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 540)
           (pack-u32 (logand 4294967295 disk-image-size))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 552)
           (pack-u32 (logand 4294967295 command-line-ptr))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 192)
           (pack-u32 (logand 4294967295 (ash disk-image-ptr -32)))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 196)
           (pack-u32 (logand 4294967295 (ash disk-image-size -32)))
           x86))
     ((mv & x86)
      (write-bytes-to-memory
           (+ zero-page-ptr 200)
           (pack-u32 (logand 4294967295 (ash command-line-ptr -32)))
           x86)))
    x86)))