• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Execloader
      • Elf-reader
      • Mach-o-reader
        • Read-load_commands
        • Read-section_data_sz_structures
        • Mach-o-section-header
        • Mach-o-header
        • Populate-mach-o-contents
        • Good-mach-o-p
        • Fill-data-segment-bytes
        • Fill-text-segment-bytes
        • Fill-text-text-section-bytes
        • Fill-text-cstring-section-bytes
        • Fill-text-const-section-bytes
        • Fill-data-dyld-section-bytes
        • Fill-data-data-section-bytes
        • Fill-data-const-section-bytes
        • Fill-data-common-section-bytes
        • Fill-data-bss-section-bytes
        • Read-mach_header
        • Populate-mach-o
        • Mach-o-section-headers
      • Merge-first-split-bytes
      • Split-bytes
      • Charlist->bytes
      • Take-till-zero
      • Merge-bytes
      • Bytes->charlist
      • Bytes->string
      • String->bytes
    • Axe
  • Testing-utilities
  • Math

• Mach-o-reader

Read-section_data_sz_structures

Read the section data structures

Signature

(read-section_data_sz_structures 
     nsects sz rest-of-the-file acc mach-o) 
 
  → 
(mv new-acc file-bytes new-mach-o)

Arguments

nsects — Guard (natp nsects).

rest-of-the-file — Guard (byte-listp rest-of-the-file).

acc — Guard (true-listp acc).

Returns

file-bytes — Type (byte-listp file-bytes), given (byte-listp rest-of-the-file).

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

Definitions and Theorems

Function: read-section_data_sz_structures

(defun
 read-section_data_sz_structures
 (nsects sz rest-of-the-file acc mach-o)
 (declare (xargs :stobjs (mach-o)))
 (declare (xargs :guard (and (natp nsects)
                             (byte-listp rest-of-the-file)
                             (true-listp acc))))
 (declare
      (xargs :guard (and (or (and (equal sz 4)
                                  (<= (* nsects 68)
                                      (len rest-of-the-file)))
                             (and (equal sz 8)
                                  (<= (* nsects 80)
                                      (len rest-of-the-file)))))))
 (let
  ((__function__ 'read-section_data_sz_structures))
  (declare (ignorable __function__))
  (if
   (zp nsects)
   (mv (reverse acc)
       rest-of-the-file mach-o)
   (b*
    (((mv sectbytes rest-of-the-file)
      (split-bytes 16 rest-of-the-file))
     ((mv segbytes rest-of-the-file)
      (split-bytes 16 rest-of-the-file))
     ((mv addr rest-of-the-file)
      (merge-first-split-bytes sz rest-of-the-file))
     ((mv size rest-of-the-file)
      (merge-first-split-bytes sz rest-of-the-file))
     ((mv offset rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv align rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv reloff rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv nreloc rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv flags rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv reserved1 rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     ((mv reserved2 rest-of-the-file)
      (merge-first-split-bytes 4 rest-of-the-file))
     (sectname (bytes->string sectbytes))
     (segname (bytes->string segbytes))
     (sect (merge-bytes (take-till-zero sectbytes)))
     (seg (merge-bytes (take-till-zero segbytes)))
     ((mv reserved3 rest-of-the-file)
      (if (equal sz 8)
          (merge-first-split-bytes 4 rest-of-the-file)
          (mv nil rest-of-the-file)))
     (mach-o
      (cond
       ((equal seg *mach-o-text*)
        (cond
         ((equal sect *text-text*)
          (b* ((mach-o (!text-text-section-addr addr mach-o))
               (mach-o (!text-text-section-size size mach-o))
               (mach-o (!text-text-section-offset offset mach-o)))
              mach-o))
         ((equal sect *text-cstring*)
          (b*
             ((mach-o (!text-cstring-section-addr addr mach-o))
              (mach-o (!text-cstring-section-size size mach-o))
              (mach-o (!text-cstring-section-offset offset mach-o)))
             mach-o))
         ((equal sect *text-const*)
          (b* ((mach-o (!text-const-section-addr addr mach-o))
               (mach-o (!text-const-section-size size mach-o))
               (mach-o (!text-const-section-offset offset mach-o)))
              mach-o))
         (t mach-o)))
       ((equal seg *mach-o-data*)
        (cond
         ((equal sect *data-data*)
          (b* ((mach-o (!data-data-section-addr addr mach-o))
               (mach-o (!data-data-section-size size mach-o))
               (mach-o (!data-data-section-offset offset mach-o)))
              mach-o))
         ((equal sect *data-dyld*)
          (b* ((mach-o (!data-dyld-section-addr addr mach-o))
               (mach-o (!data-dyld-section-size size mach-o))
               (mach-o (!data-dyld-section-offset offset mach-o)))
              mach-o))
         ((equal sect *data-const*)
          (b* ((mach-o (!data-const-section-addr addr mach-o))
               (mach-o (!data-const-section-size size mach-o))
               (mach-o (!data-const-section-offset offset mach-o)))
              mach-o))
         ((equal sect *data-bss*)
          (b* ((mach-o (!data-bss-section-addr addr mach-o))
               (mach-o (!data-bss-section-size size mach-o))
               (mach-o (!data-bss-section-offset offset mach-o)))
              mach-o))
         ((equal sect *data-common*)
          (b* ((mach-o (!data-common-section-addr addr mach-o))
               (mach-o (!data-common-section-size size mach-o))
               (mach-o (!data-common-section-offset offset mach-o)))
              mach-o))
         (t mach-o)))
       (t mach-o))))
    (read-section_data_sz_structures
         (1- nsects)
         sz rest-of-the-file
         (cons (list (cons 'sectname sectname)
                     (cons 'segname segname)
                     (cons 'addr addr)
                     (cons 'size size)
                     (cons 'offset offset)
                     (cons 'align align)
                     (cons 'reloff reloff)
                     (cons 'nreloc nreloc)
                     (cons 'flags flags)
                     (cons 'reserved1 reserved1)
                     (cons 'reserved2 reserved2)
                     (cons 'reserved3 reserved3))
               acc)
         mach-o)))))

Theorem: byte-listp-of-read-section_data_sz_structures.file-bytes

(defthm byte-listp-of-read-section_data_sz_structures.file-bytes
        (implies (byte-listp rest-of-the-file)
                 (b* (((mv ?new-acc ?file-bytes ?new-mach-o)
                       (read-section_data_sz_structures
                            nsects sz rest-of-the-file acc mach-o)))
                     (byte-listp file-bytes)))
        :rule-classes :rewrite)

Theorem: good-mach-o-p-of-read-section_data_sz_structures.new-mach-o

(defthm good-mach-o-p-of-read-section_data_sz_structures.new-mach-o
        (implies (good-mach-o-p mach-o)
                 (b* (((mv ?new-acc ?file-bytes ?new-mach-o)
                       (read-section_data_sz_structures
                            nsects sz rest-of-the-file acc mach-o)))
                     (good-mach-o-p new-mach-o)))
        :rule-classes :rewrite)

Theorem: len-mv-nth-1-read-section_data_sz_structures-sz=4

(defthm
  len-mv-nth-1-read-section_data_sz_structures-sz=4
  (implies (and (natp nsects)
                (and (equal sz 4)
                     (<= (* nsects 68)
                         (len (double-rewrite rest-of-the-file))))
                (byte-listp (double-rewrite rest-of-the-file)))
           (<= (- (len (double-rewrite rest-of-the-file))
                  (* nsects 68))
               (len (mv-nth 1
                            (read-section_data_sz_structures
                                 nsects
                                 sz rest-of-the-file acc mach-o)))))
  :rule-classes :linear)

Theorem: len-mv-nth-1-read-section_data_sz_structures-sz=8

(defthm
  len-mv-nth-1-read-section_data_sz_structures-sz=8
  (implies (and (natp nsects)
                (and (equal sz 8)
                     (<= (* nsects 80)
                         (len (double-rewrite rest-of-the-file))))
                (byte-listp (double-rewrite rest-of-the-file)))
           (<= (- (len (double-rewrite rest-of-the-file))
                  (* nsects 80))
               (len (mv-nth 1
                            (read-section_data_sz_structures
                                 nsects
                                 sz rest-of-the-file acc mach-o)))))
  :rule-classes :linear)