• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • 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
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)