|
|
|---|
|
|
|
|---|
Read the load commands (which in turn read the section data structures; see read-section_data_sz_structures)
(read-load_commands ncmds rest-of-the-file acc mach-o) → (mv new-acc file-bytes new-mach-o)
Function:
(defun read-load_commands (ncmds rest-of-the-file acc mach-o) (declare (xargs :stobjs (mach-o))) (declare (xargs :guard (and (natp ncmds) (byte-listp rest-of-the-file) (true-listp acc)))) (let ((__function__ 'read-load_commands)) (declare (ignorable __function__)) (if (zp ncmds) (mv (reverse acc) rest-of-the-file mach-o) (b* (((mv cmd rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv cmdsize rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv cmd_list remaining-file mach-o) (cond ((equal cmd *lc_uuid*) (b* (((mv uuid rest-of-the-file) (merge-first-split-bytes 16 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'uuid uuid)) rest-of-the-file mach-o))) ((equal cmd *lc_segment*) (b* (((mv segbytes rest-of-the-file) (split-bytes 16 rest-of-the-file)) ((mv vmaddr rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv vmsize rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv fileoff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv filesize rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv maxprot rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv initprot rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nsects 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)) (segname (bytes->string segbytes)) ((when (not (<= (* nsects 68) (len rest-of-the-file)))) (b* ((- (cw "Error: End of file reached unexpectedly.~%"))) (mv (reverse acc) rest-of-the-file mach-o))) ((mv section_ds rest-of-the-file mach-o) (read-section_data_sz_structures nsects 4 rest-of-the-file nil mach-o))) (if (atom section_ds) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'segname segname) (cons 'vmaddr vmaddr) (cons 'vmsize vmsize) (cons 'fileoff fileoff) (cons 'filesize filesize) (cons 'maxprot maxprot) (cons 'initprot initprot) (cons 'nsects nsects) (cons 'flags flags)) rest-of-the-file mach-o) (mv (append (list (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'segname segname) (cons 'vmaddr vmaddr) (cons 'vmsize vmsize) (cons 'fileoff fileoff) (cons 'filesize filesize) (cons 'maxprot maxprot) (cons 'initprot initprot) (cons 'nsects nsects) (cons 'flags flags))) section_ds) rest-of-the-file mach-o)))) ((equal cmd *lc_segment_64*) (b* (((mv segbytes rest-of-the-file) (split-bytes 16 rest-of-the-file)) ((mv vmaddr rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv vmsize rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv fileoff rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv filesize rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv maxprot rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv initprot rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nsects 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)) (segname (bytes->string segbytes)) ((when (not (<= (* nsects 80) (len rest-of-the-file)))) (b* ((- (cw "Error: End of file reached unexpectedly.~%"))) (mv (reverse acc) rest-of-the-file mach-o))) ((mv section_64_ds rest-of-the-file mach-o) (read-section_data_sz_structures nsects 8 rest-of-the-file nil mach-o))) (if (atom section_64_ds) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'segname segname) (cons 'vmaddr vmaddr) (cons 'vmsize vmsize) (cons 'fileoff fileoff) (cons 'filesize filesize) (cons 'maxprot maxprot) (cons 'initprot initprot) (cons 'nsects nsects) (cons 'flags flags)) rest-of-the-file mach-o) (mv (append (list (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'segname segname) (cons 'vmaddr vmaddr) (cons 'vmsize vmsize) (cons 'fileoff fileoff) (cons 'filesize filesize) (cons 'maxprot maxprot) (cons 'initprot initprot) (cons 'nsects nsects) (cons 'flags flags))) section_64_ds) rest-of-the-file mach-o)))) ((equal cmd *lc_twolevel_hints*) (b* (((mv offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nhints rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'offset offset) (cons 'nhints nhints)) rest-of-the-file mach-o))) ((member-equal cmd (list *lc_load_dylib* *lc_load_weak_dylib* *lc_id_dylib*)) (b* (((mv dylib.name->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv dylib.timestamp rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv dylib.current_version rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv dylib.compatibility_version rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (lc_str-size (nfix (- cmdsize dylib.name->lc_str.offset))) (rest-of-the-file (nthcdr (nfix (- dylib.name->lc_str.offset (* 6 4))) rest-of-the-file)) ((mv lc_str->bytes rest-of-the-file) (split-bytes lc_str-size rest-of-the-file)) (lc_str->str (bytes->string lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'dylib.name->lc_str.offset dylib.name->lc_str.offset) (cons 'dylib.timestamp dylib.timestamp) (cons 'dylib.current_version dylib.current_version) (cons 'dylib.compatibility_version dylib.compatibility_version) (cons 'dylib.name->lc_str.offset lc_str->str)) rest-of-the-file mach-o))) ((member-equal cmd (list *lc_id_dylinker* *lc_load_dylinker*)) (b* (((mv name->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (lc_str-size (nfix (- cmdsize name->lc_str.offset))) (rest-of-the-file (nthcdr (nfix (- name->lc_str.offset (* 3 4))) rest-of-the-file)) ((mv lc_str->bytes rest-of-the-file) (split-bytes lc_str-size rest-of-the-file)) (lc_str->str (bytes->string lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'name->lc_str.offset name->lc_str.offset) (cons 'lc_str->str lc_str->str)) rest-of-the-file mach-o))) ((equal cmd *lc_prebound_dylib*) (b* (((mv name->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nmodules rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv linked_modules->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (linked_modules-lc_str-size (nfix (- cmdsize linked_modules->lc_str.offset))) (name-lc_str-size (nfix (- (nfix (- cmdsize name->lc_str.offset)) linked_modules-lc_str-size))) (rest-of-the-file (nthcdr (nfix (- name->lc_str.offset (* 5 4))) rest-of-the-file)) ((mv name-lc_str->bytes rest-of-the-file) (split-bytes name-lc_str-size rest-of-the-file)) (name-lc_str->str (bytes->string name-lc_str->bytes)) ((mv linked_modules-lc_str->bytes rest-of-the-file) (split-bytes linked_modules-lc_str-size rest-of-the-file)) (linked_modules-lc_str->str (bytes->string linked_modules-lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'name->lc_str.offset name->lc_str.offset) (cons 'nmodules nmodules) (cons 'linked_modules->lc_str.offset linked_modules->lc_str.offset) (cons 'name-lc_str->str name-lc_str->str) (cons 'linked_modules-lc_str->str linked_modules-lc_str->str)) rest-of-the-file mach-o))) ((member-equal cmd (list *lc_thread* *lc_unixthread*)) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize)) rest-of-the-file mach-o)) ((equal cmd *lc_routines*) (b* (((mv init_address rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv init_module 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)) ((mv reserved3 rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv reserved4 rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv reserved5 rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv reserved6 rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'init_address init_address) (cons 'init_module init_module) (cons 'reserved1 reserved1) (cons 'reserved2 reserved2) (cons 'reserved3 reserved3) (cons 'reserved4 reserved4) (cons 'reserved5 reserved5) (cons 'reserved6 reserved6)) rest-of-the-file mach-o))) ((equal cmd *lc_routines_64*) (b* (((mv init_address rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv init_module rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv reserved1 rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv reserved2 rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv reserved3 rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv reserved4 rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv reserved5 rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv reserved6 rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'init_address init_address) (cons 'init_module init_module) (cons 'reserved1 reserved1) (cons 'reserved2 reserved2) (cons 'reserved3 reserved3) (cons 'reserved4 reserved4) (cons 'reserved5 reserved5) (cons 'reserved6 reserved6)) rest-of-the-file mach-o))) ((equal cmd *lc_sub_framework*) (b* (((mv umbrella->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (lc_str-size (nfix (- cmdsize umbrella->lc_str.offset))) (rest-of-the-file (nthcdr (nfix (- umbrella->lc_str.offset (* 3 4))) rest-of-the-file)) ((mv lc_str->bytes rest-of-the-file) (split-bytes lc_str-size rest-of-the-file)) (lc_str->str (bytes->string lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'umbrella->lc_str.offset umbrella->lc_str.offset) (cons 'lc_str->str lc_str->str)) rest-of-the-file mach-o))) ((equal cmd *lc_sub_umbrella*) (b* (((mv sub_umbrella->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (lc_str-size (nfix (- cmdsize sub_umbrella->lc_str.offset))) (rest-of-the-file (nthcdr (nfix (- sub_umbrella->lc_str.offset (* 3 4))) rest-of-the-file)) ((mv lc_str->bytes rest-of-the-file) (split-bytes lc_str-size rest-of-the-file)) (lc_str->str (bytes->string lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'sub_umbrella->lc_str.offset sub_umbrella->lc_str.offset) (cons 'lc_str->str lc_str->str)) rest-of-the-file mach-o))) ((equal cmd *lc_sub_library*) (b* (((mv sub_library->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (lc_str-size (nfix (- cmdsize sub_library->lc_str.offset))) (rest-of-the-file (nthcdr (nfix (- sub_library->lc_str.offset (* 3 4))) rest-of-the-file)) ((mv lc_str->bytes rest-of-the-file) (split-bytes lc_str-size rest-of-the-file)) (lc_str->str (bytes->string lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'sub_library->lc_str.offset sub_library->lc_str.offset) (cons 'lc_str->str lc_str->str)) rest-of-the-file mach-o))) ((equal cmd *lc_sub_client*) (b* (((mv client->lc_str.offset rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) (lc_str-size (nfix (- cmdsize client->lc_str.offset))) (rest-of-the-file (nthcdr (nfix (- client->lc_str.offset (* 3 4))) rest-of-the-file)) ((mv lc_str->bytes rest-of-the-file) (split-bytes lc_str-size rest-of-the-file)) (lc_str->str (bytes->string lc_str->bytes))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'client->lc_str.offset client->lc_str.offset) (cons 'lc_str->str lc_str->str)) rest-of-the-file mach-o))) ((equal cmd *lc_symtab*) (b* (((mv symoff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nsyms rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv stroff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv strsize rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'symoff symoff) (cons 'nsyms nsyms) (cons 'stroff stroff) (cons 'strsize strsize)) rest-of-the-file mach-o))) ((equal cmd *lc_dysymtab*) (b* (((mv ilocalsym rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nlocalsym rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv iextdefsym rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nextdefsym rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv iundefsym rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nundefsym rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv tocoff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv ntoc rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv modtaboff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nmodtab rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv extrefsymoff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nextrefsyms rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv indirectsymoff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nindirectsyms rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv extreloff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nextrel rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv locreloff rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv nlocrel rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'ilocalsym ilocalsym) (cons 'nlocalsym nlocalsym) (cons 'iextdefsym iextdefsym) (cons 'nextdefsym nextdefsym) (cons 'iundefsym iundefsym) (cons 'nundefsym nundefsym) (cons 'tocoff tocoff) (cons 'ntoc ntoc) (cons 'modtaboff modtaboff) (cons 'nmodtab nmodtab) (cons 'extrefsymoff extrefsymoff) (cons 'nextrefsyms nextrefsyms) (cons 'indirectsymoff indirectsymoff) (cons 'nindirectsyms nindirectsyms) (cons 'extreloff extreloff) (cons 'nextrel nextrel) (cons 'locreloff locreloff) (cons 'nlocrel nlocrel)) rest-of-the-file mach-o))) ((member-equal cmd (list *lc_dyld_info* *lc_dyld_info_only*)) (b* (((mv rebase_off rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv rebase_size rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv bind_off rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv bind_size rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv weak_bind_off rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv weak_bind_size rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv lazy_bind_off rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv lazy_bind_size rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv export_off rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv export_size rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'rebase_off rebase_off) (cons 'rebase_size rebase_size) (cons 'bind_off bind_off) (cons 'bind_size bind_size) (cons 'weak_bind_off weak_bind_off) (cons 'weak_bind_size weak_bind_size) (cons 'lazy_bind_off lazy_bind_off) (cons 'lazy_bind_size lazy_bind_size) (cons 'export_off export_off) (cons 'export_size export_size)) rest-of-the-file mach-o))) ((member-equal cmd (list *lc_code_signature* *lc_segment_split_info* *lc_function_starts* *lc_data_in_code* *lc_dylib_code_sign_drs*)) (b* (((mv data_off rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv data_size rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'data_off data_off) (cons 'data_size data_size)) rest-of-the-file mach-o))) ((member-equal cmd (list *lc_version_min_macosx* *lc_version_min_iphoneos*)) (b* (((mv version rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file)) ((mv sdk rest-of-the-file) (merge-first-split-bytes 4 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'version version) (cons 'sdk sdk)) rest-of-the-file mach-o))) ((equal cmd *lc_source_version*) (b* (((mv version rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'version version)) rest-of-the-file mach-o))) ((equal cmd *lc_main*) (b* (((mv entryoff rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file)) ((mv stacksize rest-of-the-file) (merge-first-split-bytes 8 rest-of-the-file))) (mv (list (cons 'cmd cmd) (cons 'cmdsize cmdsize) (cons 'entryoff entryoff) (cons 'stacksize stacksize)) rest-of-the-file mach-o))) (t (mv (cw "(Unrecognized/unimplemented load command:~x0)~%" cmd) rest-of-the-file mach-o))))) (read-load_commands (1- ncmds) remaining-file (cons cmd_list acc) mach-o)))))
Theorem:
(defthm byte-listp-of-read-load_commands.file-bytes (implies (byte-listp rest-of-the-file) (b* (((mv ?new-acc ?file-bytes ?new-mach-o) (read-load_commands ncmds rest-of-the-file acc mach-o))) (byte-listp file-bytes))) :rule-classes :rewrite)
Theorem:
(defthm good-mach-o-p-of-read-load_commands.new-mach-o (implies (good-mach-o-p mach-o) (b* (((mv ?new-acc ?file-bytes ?new-mach-o) (read-load_commands ncmds rest-of-the-file acc mach-o))) (good-mach-o-p new-mach-o))) :rule-classes :rewrite)