• 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
    • 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-elf-header
        • Read-section-headers
        • Read-segment-headers-64
        • Read-segment-headers-32
        • Read-section-names
        • Elf64_sym-info
        • Elf32_sym-info
        • Parse-symtab-entries
        • Is-elf-content-p
        • Populate-elf-contents
        • Get-string-section-data
        • Get-section-info1
        • Set-elf-stobj-fields
        • Get-named-section-headers
        • Elf-read-mem-null-term
        • Get-section-info
        • Find-label-address-from-elf-symtab-info
        • Section-names
        • Get-symtab-entries
        • Populate-elf
        • Get-label-addresses
        • Get-label-address
        • Elf-read-string-null-term
        • 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
      • Charlist->bytes
      • Take-till-zero
      • Merge-bytes
      • Bytes->charlist
      • Bytes->string
      • String->bytes
    • Axe
  • Testing-utilities
  • Math

• Elf-reader

Read-elf-header

Read the ELF header from the first 64 bytes

Signature

(read-elf-header file-header) → header

Arguments

file-header — Guard (byte-listp file-header).

Returns

header — Type (elf-header-p header).

Definitions and Theorems

Function: read-elf-header

(defun read-elf-header (file-header)
       (declare (xargs :guard (byte-listp file-header)))
       (let ((__function__ 'read-elf-header))
            (declare (ignorable __function__))
            (b* (((mv e_magic file-header)
                  (split-bytes 4 file-header))
                 ((mv e_class file-header)
                  (merge-first-split-bytes 1 file-header))
                 (w (if (equal e_class 1) 4 8))
                 ((mv e_dataenc file-header)
                  (merge-first-split-bytes 1 file-header))
                 ((mv e_identver file-header)
                  (merge-first-split-bytes 1 file-header))
                 ((mv e_osabi file-header)
                  (merge-first-split-bytes 1 file-header))
                 ((mv e_abiver file-header)
                  (merge-first-split-bytes 1 file-header))
                 ((mv e_padding file-header)
                  (split-bytes 7 file-header))
                 ((mv e_type file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_machine file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_version file-header)
                  (merge-first-split-bytes 4 file-header))
                 ((mv e_entry file-header)
                  (merge-first-split-bytes w file-header))
                 ((mv e_phoff file-header)
                  (merge-first-split-bytes w file-header))
                 ((mv e_shoff file-header)
                  (merge-first-split-bytes w file-header))
                 ((mv e_flags file-header)
                  (merge-first-split-bytes 4 file-header))
                 ((mv e_ehsize file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_phentsize file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_phnum file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_shentsize file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_shnum file-header)
                  (merge-first-split-bytes 2 file-header))
                 ((mv e_shstrndx &)
                  (merge-first-split-bytes 2 file-header)))
                (make-elf-header :magic e_magic
                                 :class e_class
                                 :dataenc e_dataenc
                                 :identver e_identver
                                 :osabi e_osabi
                                 :abiver e_abiver
                                 :padding e_padding
                                 :type e_type
                                 :machine e_machine
                                 :version e_version
                                 :entry e_entry
                                 :phoff e_phoff
                                 :shoff e_shoff
                                 :flags e_flags
                                 :ehsize e_ehsize
                                 :phentsize e_phentsize
                                 :phnum e_phnum
                                 :shentsize e_shentsize
                                 :shnum e_shnum
                                 :shstrndx e_shstrndx))))

Theorem: elf-header-p-of-read-elf-header

(defthm elf-header-p-of-read-elf-header
        (b* ((header (read-elf-header file-header)))
            (elf-header-p header))
        :rule-classes :rewrite)