• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
        • Binary-file-load-fn
        • Setting-up-page-tables
        • Init-sys-view
        • Load-elf-sections
        • Concrete-simulation-examples
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Program-execution

Binary-file-load-fn

Function to read in an ELF or Mach-O binary and load text and data sections into the x86 ISA model's memory

Signature

(binary-file-load-fn filename exld::elf 
                     exld::mach-o x86 state &key (elf 't) 
                     (mach-o 'nil)) 
 
  → 
(mv new-elf new-mach-o new-x86 state)

Arguments

filename — Guard (stringp filename).

elf — Guard (booleanp elf).

mach-o — Guard (booleanp mach-o).

Returns

new-elf — Type (exld::good-elf-p new-elf), given (exld::elfp exld::good-elf-p).

new-mach-o — Type (exld::good-mach-o-p new-mach-o), given (exld::mach-op exld::good-mach-o-p).

new-x86 — Type (x86p new-x86), given (x86p x86).

The following macro makes it convenient to call this function to load a program:

 (binary-file-load "fib.o" :elf t) ;; or :mach-o t

Definitions and Theorems

Function: binary-file-load-fn-fn

(defun
 binary-file-load-fn-fn
 (filename exld::elf
           exld::mach-o x86 state elf mach-o)
 (declare (xargs :stobjs (exld::elf exld::mach-o x86 state)))
 (declare (xargs :guard (and (stringp filename)
                             (booleanp elf)
                             (booleanp mach-o))))
 (let
  ((__function__ 'binary-file-load-fn))
  (declare (ignorable __function__))
  (cond
   ((and elf (not mach-o))
    (b*
     (((mv exld::elf state)
       (exld::populate-elf filename exld::elf state))
      ((mv flg x86)
       (load-elf-sections (exld::@sections exld::elf)
                          x86))
      ((when flg)
       (prog2$
        (raise
         "[ELF]: Error encountered while loading sections in the x86 model's memory!~%")
        (mv exld::elf exld::mach-o x86 state))))
     (mv exld::elf exld::mach-o x86 state)))
   ((and mach-o (not elf))
    (b*
     (((mv ?alst exld::mach-o state)
       (exld::populate-mach-o filename exld::mach-o state))
      ((mv flg0 x86)
       (mach-o-load-text-section exld::mach-o x86))
      ((mv flg1 x86)
       (mach-o-load-data-section exld::mach-o x86))
      ((when (or flg0 flg1))
       (prog2$
        (raise
         "[Mach-O]: Error encountered while loading sections in the x86 model's memory!~%")
        (mv exld::elf exld::mach-o x86 state))))
     (mv exld::elf exld::mach-o x86 state)))
   (t
    (prog2$
     (raise
      "~%We support only ELF and Mach-O files for now! Use this function with either :elf t ~
 or :mach-o t.~%")
     (mv exld::elf exld::mach-o x86 state))))))

Theorem: good-elf-p-of-binary-file-load-fn.new-elf

(defthm
 good-elf-p-of-binary-file-load-fn.new-elf
 (implies
  (exld::elfp exld::good-elf-p)
  (b* (((mv ?new-elf
            ?new-mach-o ?new-x86 acl2::?state)
        (binary-file-load-fn-fn filename exld::elf
                                exld::mach-o x86 state elf mach-o)))
      (exld::good-elf-p new-elf)))
 :rule-classes :rewrite)

Theorem: good-mach-o-p-of-binary-file-load-fn.new-mach-o

(defthm
 good-mach-o-p-of-binary-file-load-fn.new-mach-o
 (implies
  (exld::mach-op exld::good-mach-o-p)
  (b* (((mv ?new-elf
            ?new-mach-o ?new-x86 acl2::?state)
        (binary-file-load-fn-fn filename exld::elf
                                exld::mach-o x86 state elf mach-o)))
      (exld::good-mach-o-p new-mach-o)))
 :rule-classes :rewrite)

Theorem: x86p-of-binary-file-load-fn.new-x86

(defthm
 x86p-of-binary-file-load-fn.new-x86
 (implies
  (x86p x86)
  (b* (((mv ?new-elf
            ?new-mach-o ?new-x86 acl2::?state)
        (binary-file-load-fn-fn filename exld::elf
                                exld::mach-o x86 state elf mach-o)))
      (x86p new-x86)))
 :rule-classes :rewrite)