• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Axe
    • Execloader
      • Elf-reader
        • Elf64_sym
        • Elf32_sym
        • Elf-header
        • Elf-section-header
        • Elf64-segment-header
        • Elf32-segment-header
        • Elf_bits32
        • Elf_bits8
        • Elf_bits64
        • Elf_bits16
        • Section-info
        • Read-section-headers
        • Read-segment-headers-64
        • Read-segment-headers-32
        • Read-section-names
        • Elf64_sym-info
        • Elf32_sym-info
        • Read-elf-header
        • Parse-symtab-entries
        • Populate-elf-contents
        • Is-elf-content-p
        • Get-string-section-data
        • Get-section-info1
        • Set-elf-stobj-fields
        • Get-named-section-headers
        • Elf-read-mem-null-term
        • Get-section-info
        • Get-symtab-entries
        • Find-label-address-from-elf-symtab-info
        • Section-names
        • Populate-elf
        • Get-label-addresses
        • Elf-read-string-null-term
        • Get-label-address
        • Good-elf-p
        • Elf64_sym-equiv-under-mask
        • Elf64-segment-headers
        • Elf32_sym-equiv-under-mask
        • Elf32-segment-headers
        • Section-info-list
        • Elf64_sym-info-list
        • Elf32_sym-info-list
        • Elf-section-headers
        • Elf64_sym-debug
        • Elf32_sym-debug
      • Mach-o-reader
      • Merge-first-split-bytes
      • Split-bytes
      • Take-till-zero
      • Charlist->bytes
      • Merge-bytes
      • Bytes->charlist
      • String->bytes
      • Bytes->string
  • Math
  • Testing-utilities

• Elf-reader

Populate-elf-contents

Initialize the ELF stobj with contents parsed as an ELF binary

Signature

(populate-elf-contents contents elf state) 
  → 
(mv new-elf state)

Arguments

contents — Guard (byte-listp contents).

Returns

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

Definitions and Theorems

Function: populate-elf-contents

(defun populate-elf-contents (contents elf state)
 (declare (xargs :stobjs (elf state)))
 (declare (xargs :guard (byte-listp contents)))
 (let ((__function__ 'populate-elf-contents))
  (declare (ignorable __function__))
  (b*
   (((mv okp header state)
     (is-elf-content-p contents state))
    ((unless okp)
     (prog2$ (raise "Bad ELF contents!")
             (mv elf state)))
    (elf (!elf-header header elf))
    (file-byte-list contents)
    (elf-file-size (len file-byte-list))
    (elf (!elf-file-size elf-file-size elf))
    ((elf-header header))
    (class header.class)
    (elf-header-size (if (equal class 1) 52 64))
    (elf (!elf-header-size elf-header-size elf))
    (segment-header-offset header.phoff)
    (segment-headers (nthcdr segment-header-offset file-byte-list))
    ((unless (byte-listp segment-headers))
     (prog2$ (er hard? 'elf-file-read
                 "Not enough bytes to read ELF segment headers!")
             (mv elf state)))
    (nsegments header.phnum)
    (?segments
         (if (equal class 1)
             (read-segment-headers-32 nsegments segment-headers nil)
           (read-segment-headers-64 nsegments segment-headers nil)))
    (section-headers
         (get-named-section-headers header file-byte-list))
    (elf (!sections-num header.shnum elf))
    (elf (set-elf-stobj-fields section-headers file-byte-list elf)))
   (mv elf state))))

Theorem: good-elf-p-of-populate-elf-contents.new-elf

(defthm good-elf-p-of-populate-elf-contents.new-elf
  (implies (good-elf-p elf)
           (b* (((mv ?new-elf acl2::?state)
                 (populate-elf-contents contents elf state)))
             (good-elf-p new-elf)))
  :rule-classes :rewrite)