• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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)