		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Read-section-headers

Read ELF section headers

Signature
(read-section-headers nsections w rest-of-the-file acc) → section-headers
Arguments: nsections — Guard (natp nsections).; w — Guard (natp w).; rest-of-the-file — Guard (byte-listp rest-of-the-file).; acc — Guard (elf-section-headers-p acc).
Returns: section-headers — Type (elf-section-headers-p section-headers), given (elf-section-headers-p acc).

Definitions and Theorems

Function: read-section-headers

(defun read-section-headers (nsections w rest-of-the-file acc)
 (declare (xargs :guard (and (natp nsections)
                             (natp w)
                             (byte-listp rest-of-the-file)
                             (elf-section-headers-p acc))))
 (let ((__function__ 'read-section-headers))
  (declare (ignorable __function__))
  (if (zp nsections)
      (reverse acc)
   (b*
    (((unless (or (equal w 4) (equal w 8)))
      (prog2$
       (raise
        "Width of fields expected to be either 4 or 8, but it is ~x0 instead!"
        w)
       (reverse acc)))
     ((mv sh_name rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv sh_type rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv sh_flags rest-of-the-file)
      (merge-first-split-bytes w rest-of-the-file))
     ((mv sh_addr rest-of-the-file)
      (merge-first-split-bytes w rest-of-the-file))
     ((mv sh_offset rest-of-the-file)
      (merge-first-split-bytes w rest-of-the-file))
     ((mv sh_size rest-of-the-file)
      (merge-first-split-bytes w rest-of-the-file))
     ((mv sh_link rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv sh_info rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv sh_addralign rest-of-the-file)
      (merge-first-split-bytes w rest-of-the-file))
     ((mv sh_entsize rest-of-the-file)
      (merge-first-split-bytes w rest-of-the-file))
     (section (make-elf-section-header :name sh_name
                                       :type sh_type
                                       :flags sh_flags
                                       :addr sh_addr
                                       :offset sh_offset
                                       :size sh_size
                                       :link sh_link
                                       :info sh_info
                                       :addralign sh_addralign
                                       :entsize sh_entsize)))
    (read-section-headers (1- nsections)
                          w
                          rest-of-the-file (cons section acc))))))

Theorem: elf-section-headers-p-of-read-section-headers

(defthm elf-section-headers-p-of-read-section-headers
 (implies
   (elf-section-headers-p acc)
   (b*
     ((section-headers
           (read-section-headers nsections w rest-of-the-file acc)))
     (elf-section-headers-p section-headers)))
 :rule-classes :rewrite)