• 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
      • 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-text-section-bytes
        • Fill-text-segment-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
      • Take-till-zero
      • Charlist->bytes
      • Merge-bytes
      • Bytes->charlist
      • String->bytes
      • Bytes->string
  • Math
  • Testing-utilities

• Mach-o-reader

Populate-mach-o-contents

Initialize the Mach-O stobj with file-byte-list

Signature

(populate-mach-o-contents file-byte-list mach-o state) 
  → 
(mv err new-mach-o new-state)

Arguments

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

Returns

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

new-state — Type (state-p new-state), given (state-p state).

Definitions and Theorems

Function: populate-mach-o-contents

(defun populate-mach-o-contents (file-byte-list mach-o state)
 (declare (xargs :stobjs (mach-o state)))
 (declare (xargs :guard (byte-listp file-byte-list)))
 (let ((__function__ 'populate-mach-o-contents))
  (declare (ignorable __function__))
  (b*
   ((file-size (len file-byte-list))
    (mach-o (!mach-o-file-size file-size mach-o))
    (file-header (take 32 file-byte-list))
    ((when (not (byte-listp file-header)))
     (cw "Header could not be read.~%")
     (mv t mach-o state))
    ((mach-o-header header)
     (read-mach_header file-header))
    (magic header.magic)
    ((when (and (not (equal magic *mh_magic*))
                (not (equal magic *mh_cigam*))
                (not (equal magic *mh_magic_64*))
                (not (equal magic *mh_cigam_64*))))
     (cw
      "Error: Not a Mach-O object file (as suggested by the magic number).~%")
     (mv t mach-o state))
    ((when (not (unsigned-byte-p 64 header.sizeofcmds)))
     (cw "Mach-O File Read Error: Sizeofcmds ~x0 ill-formed~%"
         header.sizeofcmds)
     (mv t mach-o state))
    (mach-o (!load-cmds-size header.sizeofcmds mach-o))
    (mach-o-header-size (if (and (or (equal magic *mh_magic*)
                                     (equal magic *mh_cigam*))
                                 (equal header.reserved nil))
                            28
                          32))
    (mach-o (!mach-o-header-size mach-o-header-size mach-o))
    (file-byte-list (nthcdr mach-o-header-size file-byte-list))
    (ncmds (nfix header.ncmds))
    ((mv cmds remaining-file mach-o)
     (read-load_commands ncmds file-byte-list nil mach-o))
    (h-size (@mach-o-header-size mach-o))
    (lc-size (@load-cmds-size mach-o))
    ((mv flg mach-o state)
     (fill-text-segment-bytes h-size
                              lc-size remaining-file mach-o state))
    ((when flg) (mv flg mach-o state))
    ((mv flg mach-o state)
     (fill-data-segment-bytes h-size
                              lc-size remaining-file mach-o state))
    ((when flg) (mv flg mach-o state)))
   (mv (list 'header header (list 'cmds cmds))
       mach-o state))))

Theorem: good-mach-o-p-of-populate-mach-o-contents.new-mach-o

(defthm good-mach-o-p-of-populate-mach-o-contents.new-mach-o
 (implies
      (good-mach-o-p mach-o)
      (b* (((mv ?err ?new-mach-o ?new-state)
            (populate-mach-o-contents file-byte-list mach-o state)))
        (good-mach-o-p new-mach-o)))
 :rule-classes :rewrite)

Theorem: state-p-of-populate-mach-o-contents.new-state

(defthm state-p-of-populate-mach-o-contents.new-state
 (implies
      (state-p state)
      (b* (((mv ?err ?new-mach-o ?new-state)
            (populate-mach-o-contents file-byte-list mach-o state)))
        (state-p new-state)))
 :rule-classes :rewrite)