diff --git a/src/elf_file.lem b/src/elf_file.lem index be3b101..f5b5e01 100644 --- a/src/elf_file.lem +++ b/src/elf_file.lem @@ -61,7 +61,7 @@ let bytes_of_elf32_file ef = if List.length ef.elf32_file_section_header_table = List.length ef.elf32_file_interpreted_sections then let segs_zip = List.zip ef.elf32_file_program_header_table ef.elf32_file_interpreted_segments in - let sects_zip = List.zip ef.elf32_file_section_header_table (List.reverse ef.elf32_file_interpreted_sections) in + let sects_zip = List.zip ef.elf32_file_section_header_table ef.elf32_file_interpreted_sections in let segs_layout = List.map (fun (seg, interp_seg) -> (natural_of_elf32_off seg.elf32_p_offset, interp_seg.elf32_segment_body) @@ -273,7 +273,7 @@ let obtain_elf64_section_header_table hdr bs0 = (* Byte sequence irrelevant below as exact size used... *) read_elf64_section_header_table ssize endian sexact >>= fun (sht, _) -> return sht - + (** [obtain_elf32_section_header_string_table hdr sht bs0] reads a file's section * header string table from byte sequence [bs0] using information gleaned from * the file header [hdr] and section header table [sht]. @@ -285,13 +285,13 @@ let obtain_elf32_section_header_string_table hdr sht bs0 = if (natural_of_elf32_half hdr.elf32_shstrndx) = shn_undef then return Nothing else - match index (natural_of_elf32_half hdr.elf32_shstrndx) sht with + match index (natural_of_elf32_half hdr.elf32_shstrndx) sht with Nothing -> fail "no section header string table" | Just x -> return x end >>= fun sh -> Byte_sequence.offset_and_cut (natural_of_elf32_off sh.elf32_sh_offset) (natural_of_elf32_word sh.elf32_sh_size) bs0 >>= fun sexact -> return (Just (string_table_of_byte_sequence sexact)) - + (** [obtain_elf64_section_header_string_table hdr sht bs0] reads a file's section * header string table from byte sequence [bs0] using information gleaned from * the file header [hdr] and section header table [sht]. @@ -303,7 +303,7 @@ let obtain_elf64_section_header_string_table hdr sht bs0 = if (natural_of_elf64_half hdr.elf64_shstrndx) = shn_undef then return Nothing else - match index (natural_of_elf64_half hdr.elf64_shstrndx) sht with + match index (natural_of_elf64_half hdr.elf64_shstrndx) sht with Nothing -> fail "no section header string table" | Just x -> return x end >>= fun sh -> @@ -562,7 +562,7 @@ val obtain_elf64_bits_and_bobs : elf64_header -> elf64_program_header_table -> e -> elf64_section_header_table -> elf64_interpreted_sections -> byte_sequence -> error (list (natural * byte_sequence)) let obtain_elf64_bits_and_bobs hdr segs interp_segs sects interp_sects bs0 = let hdr_off_len = (0, natural_of_elf64_half hdr.elf64_ehsize) in - + let pht_off = natural_of_elf64_off hdr.elf64_phoff in let pht_len = natural_of_elf64_half hdr.elf64_phentsize * natural_of_elf64_half hdr.elf64_phnum in let pht_off_len = (pht_off, pht_off + pht_len) in @@ -680,17 +680,17 @@ let get_elf64_file_section_header_string_table f3 = let strings = Byte_sequence.string_of_byte_sequence rel in return (String_table.mk_string_table strings Missing_pervasives.null_char) end - + val find_elf32_symbols_by_symtab_idx : natural -> elf32_file -> error (elf32_symbol_table * string_table * natural) let find_elf32_symbols_by_symtab_idx sec_idx f = match List.index f.elf32_file_interpreted_sections (natFromNatural sec_idx) with Nothing -> fail "impossible: interpreted section found but not indexable" | Just sec -> return sec - end >>= fun sec -> + end >>= fun sec -> match List.index f.elf32_file_interpreted_sections (natFromNatural sec.elf32_section_link) with Nothing -> fail "no associated strtab" | Just strs -> return strs - end >>= fun strs -> + end >>= fun strs -> let strings = Byte_sequence.string_of_byte_sequence strs.elf32_section_body in let strtab = String_table.mk_string_table strings null_char in let endian = get_elf32_header_endianness f.elf32_file_header in @@ -700,7 +700,7 @@ let find_elf32_symbols_by_symtab_idx sec_idx f = val find_elf32_symtab_by_type : natural -> elf32_file -> error (elf32_symbol_table * string_table * natural) let find_elf32_symtab_by_type t f = let found_symtab_index = find_index (fun sh -> sh.elf32_section_type = t) f.elf32_file_interpreted_sections in - match found_symtab_index with + match found_symtab_index with Nothing -> fail "no such symtab" | Just sec_idx -> return sec_idx end >>= fun sec_idx -> find_elf32_symbols_by_symtab_idx sec_idx f @@ -710,11 +710,11 @@ let find_elf64_symbols_by_symtab_idx sec_idx f = match List.index f.elf64_file_interpreted_sections (natFromNatural sec_idx) with Nothing -> fail "impossible: interpreted section found but not indexable" | Just sec -> return sec - end >>= fun sec -> + end >>= fun sec -> match List.index f.elf64_file_interpreted_sections (natFromNatural sec.elf64_section_link) with Nothing -> fail "no associated strtab" | Just strs -> return strs - end >>= fun strs -> + end >>= fun strs -> let strings = Byte_sequence.string_of_byte_sequence strs.elf64_section_body in let strtab = String_table.mk_string_table strings null_char in let endian = get_elf64_header_endianness f.elf64_file_header in @@ -724,7 +724,7 @@ let find_elf64_symbols_by_symtab_idx sec_idx f = val find_elf64_symtab_by_type : natural -> elf64_file -> error (elf64_symbol_table * string_table * natural) let find_elf64_symtab_by_type t f = let found_symtab_index = find_index (fun sh -> sh.elf64_section_type = t) f.elf64_file_interpreted_sections in - match found_symtab_index with + match found_symtab_index with Nothing -> fail "no such symtab" | Just sec_idx -> return sec_idx end >>= fun sec_idx -> find_elf64_symbols_by_symtab_idx sec_idx f @@ -882,8 +882,8 @@ let get_elf64_file_dynamic_symbol_table ef = | _ -> fail "obtain_elf64_dynamic_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" end - -(** [get_elf32_file_symbol_table_by_index f1 index] returns the ELF file [f1] + +(** [get_elf32_file_symbol_table_by_index f1 index] returns the ELF file [f1] * symbol table that is pointed to by the section header table entry at index * [index]. May fail if index is out of range, or otherwise. *) @@ -898,8 +898,8 @@ let get_elf32_symbol_table_by_index ef link = | Just sym -> read_elf32_symbol_table endian sym.elf32_section_body end - -(** [get_elf32_file_string_table_by_index f1 index] returns the ELF file [f1] + +(** [get_elf32_file_string_table_by_index f1 index] returns the ELF file [f1] * string table that is pointed to by the section header table entry at index * [index]. May fail if index is out of range, or otherwise. *) @@ -912,8 +912,8 @@ let get_elf32_string_table_by_index ef link = | Nothing -> fail "get_elf32_string_table_by_index: invalid index" | Just sym -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym.elf32_section_body) Missing_pervasives.null_char) end - -(** [get_elf64_file_symbol_table_by_index f1 index] returns the ELF file [f1] + +(** [get_elf64_file_symbol_table_by_index f1 index] returns the ELF file [f1] * symbol table that is pointed to by the section header table entry at index * [index]. May fail if index is out of range, or otherwise. *) @@ -928,8 +928,8 @@ let get_elf64_symbol_table_by_index ef link = | Just sym -> read_elf64_symbol_table endian sym.elf64_section_body end - -(** [get_elf64_file_string_table_by_index f1 index] returns the ELF file [f1] + +(** [get_elf64_file_string_table_by_index f1 index] returns the ELF file [f1] * string table that is pointed to by the section header table entry at index * [index]. May fail if index is out of range, or otherwise. *) @@ -1012,7 +1012,7 @@ let get_elf32_executable_image f3 = * executable ELF file. May fail if extraction is impossible. *) val get_elf64_executable_image : elf64_file -> error elf64_executable_process_image -let get_elf64_executable_image f3 = +let get_elf64_executable_image f3 = if is_elf64_executable_file f3.elf64_file_header then let entr = f3.elf64_file_header.elf64_entry in let segs = f3.elf64_file_interpreted_segments in @@ -1189,10 +1189,10 @@ let {ocaml} string_of_elf64_file hdr_bdl pht_bdl sht_bdl f3 = * TODO: move elsewhere. Check whether this is still being used. *) val flag_is_set : natural -> natural -> bool -let flag_is_set flag v = - (* HACK: convert to elf64_xword first. Flags never live +let flag_is_set flag v = + (* HACK: convert to elf64_xword first. Flags never live * in objects bigger than 64 bits. *) - elf64_xword_land - (elf64_xword_of_natural v) + elf64_xword_land + (elf64_xword_of_natural v) (elf64_xword_of_natural flag) = (elf64_xword_of_natural flag) diff --git a/src/elf_section_header_table.lem b/src/elf_section_header_table.lem index 2c6c91f..bf808c1 100644 --- a/src/elf_section_header_table.lem +++ b/src/elf_section_header_table.lem @@ -205,7 +205,7 @@ let string_of_section_type os proc user i = else if i = sht_symtab_shndx then "SYMTAB_SHNDX" else if i >= sht_loos && i <= sht_hios then - os i + os i else if i >= sht_loproc && i <= sht_hiproc then proc i else if i >= sht_louser && i <= sht_hiuser then @@ -319,7 +319,7 @@ type elf32_compression_header = (** Type [elf64_compression_header] provides information about the compression and * decompression of compressed sections. All compressed sections on ELF64 begin * with an [elf64_compression_header] entry. - *) + *) type elf64_compression_header = <| elf64_chdr_type : elf64_word (** Specified the compression algorithm *) ; elf64_chdr_reserved : elf64_word (** Reserved. *) @@ -329,7 +329,7 @@ type elf64_compression_header = (** This section is compressed with the ZLIB algorithm. The compressed data begins * at the first byte immediately following the end of the compression header. - *) + *) let elfcompress_zlib : natural = 1 (** Values in these ranges are reserved for OS-specific semantics. @@ -376,7 +376,7 @@ let read_elf64_compression_header ed bs0 = (** [elf32_section_header_table_entry] is the type of entries in the section * header table in 32-bit ELF files. Each entry in the table details a section * in the body of the ELF file. - *) + *) type elf32_section_header_table_entry = <| elf32_sh_name : elf32_word (** Name of the section *) ; elf32_sh_type : elf32_word (** Type of the section and its semantics *) @@ -389,47 +389,47 @@ type elf32_section_header_table_entry = ; elf32_sh_addralign : elf32_word (** Alignment constraints for section *) ; elf32_sh_entsize : elf32_word (** Size of each entry in table, if section is one *) |> - + let (elf32_null_section_header : elf32_section_header_table_entry) = <| elf32_sh_name = elf32_word_of_natural 0 ; elf32_sh_type = elf32_word_of_natural 0 ; elf32_sh_flags = elf32_word_of_natural 0 ; elf32_sh_addr = elf32_addr_of_natural 0 - ; elf32_sh_offset = elf32_off_of_natural 0 + ; elf32_sh_offset = elf32_off_of_natural 0 ; elf32_sh_size = elf32_word_of_natural 0 ; elf32_sh_link = elf32_word_of_natural 0 ; elf32_sh_info = elf32_word_of_natural 0 ; elf32_sh_addralign = elf32_word_of_natural 0 ; elf32_sh_entsize = elf32_word_of_natural 0 |> - + (** [compare_elf32_section_header_table_entry ent1 ent2] is an ordering comparison * function on section header table entries suitable for use in constructing * sets, finite maps and other ordered data types. *) val compare_elf32_section_header_table_entry : elf32_section_header_table_entry -> elf32_section_header_table_entry -> ordering -let compare_elf32_section_header_table_entry h1 h2 = - compare +let compare_elf32_section_header_table_entry h1 h2 = + compare [natural_of_elf32_word h1.elf32_sh_name; - natural_of_elf32_word h1.elf32_sh_type; + natural_of_elf32_word h1.elf32_sh_type; natural_of_elf32_word h1.elf32_sh_flags; - natural_of_elf32_addr h1.elf32_sh_addr; + natural_of_elf32_addr h1.elf32_sh_addr; natural_of_elf32_off h1.elf32_sh_offset; - natural_of_elf32_word h1.elf32_sh_size; - natural_of_elf32_word h1.elf32_sh_link; - natural_of_elf32_word h1.elf32_sh_info; - natural_of_elf32_word h1.elf32_sh_addralign; + natural_of_elf32_word h1.elf32_sh_size; + natural_of_elf32_word h1.elf32_sh_link; + natural_of_elf32_word h1.elf32_sh_info; + natural_of_elf32_word h1.elf32_sh_addralign; natural_of_elf32_word h1.elf32_sh_entsize] [natural_of_elf32_word h2.elf32_sh_name; - natural_of_elf32_word h2.elf32_sh_type; + natural_of_elf32_word h2.elf32_sh_type; natural_of_elf32_word h2.elf32_sh_flags; - natural_of_elf32_addr h2.elf32_sh_addr; + natural_of_elf32_addr h2.elf32_sh_addr; natural_of_elf32_off h2.elf32_sh_offset; - natural_of_elf32_word h2.elf32_sh_size; - natural_of_elf32_word h2.elf32_sh_link; - natural_of_elf32_word h2.elf32_sh_info; - natural_of_elf32_word h2.elf32_sh_addralign; + natural_of_elf32_word h2.elf32_sh_size; + natural_of_elf32_word h2.elf32_sh_link; + natural_of_elf32_word h2.elf32_sh_info; + natural_of_elf32_word h2.elf32_sh_addralign; natural_of_elf32_word h2.elf32_sh_entsize] instance (Ord elf32_section_header_table_entry) @@ -443,7 +443,7 @@ end (** [elf64_section_header_table_entry] is the type of entries in the section * header table in 64-bit ELF files. Each entry in the table details a section * in the body of the ELF file. - *) + *) type elf64_section_header_table_entry = <| elf64_sh_name : elf64_word (** Name of the section *) ; elf64_sh_type : elf64_word (** Type of the section and its semantics *) @@ -456,16 +456,16 @@ type elf64_section_header_table_entry = ; elf64_sh_addralign : elf64_xword (** Alignment constraints for section *) ; elf64_sh_entsize : elf64_xword (** Size of each entry in table, if section is one *) |> - + let (elf64_null_section_header : elf64_section_header_table_entry) = - <| elf64_sh_name = elf64_word_of_natural 0 - ; elf64_sh_type = elf64_word_of_natural 0 + <| elf64_sh_name = elf64_word_of_natural 0 + ; elf64_sh_type = elf64_word_of_natural 0 ; elf64_sh_flags = elf64_xword_of_natural 0 - ; elf64_sh_addr = elf64_addr_of_natural 0 - ; elf64_sh_offset = elf64_off_of_natural 0 + ; elf64_sh_addr = elf64_addr_of_natural 0 + ; elf64_sh_offset = elf64_off_of_natural 0 ; elf64_sh_size = elf64_xword_of_natural 0 - ; elf64_sh_link = elf64_word_of_natural 0 - ; elf64_sh_info = elf64_word_of_natural 0 + ; elf64_sh_link = elf64_word_of_natural 0 + ; elf64_sh_info = elf64_word_of_natural 0 ; elf64_sh_addralign = elf64_xword_of_natural 0 ; elf64_sh_entsize = elf64_xword_of_natural 0 |> @@ -476,27 +476,27 @@ let (elf64_null_section_header : elf64_section_header_table_entry) = *) val compare_elf64_section_header_table_entry : elf64_section_header_table_entry -> elf64_section_header_table_entry -> ordering -let compare_elf64_section_header_table_entry h1 h2 = - compare +let compare_elf64_section_header_table_entry h1 h2 = + compare [natural_of_elf64_word h1.elf64_sh_name; - natural_of_elf64_word h1.elf64_sh_type; + natural_of_elf64_word h1.elf64_sh_type; natural_of_elf64_xword h1.elf64_sh_flags; - natural_of_elf64_addr h1.elf64_sh_addr; + natural_of_elf64_addr h1.elf64_sh_addr; natural_of_elf64_off h1.elf64_sh_offset; - natural_of_elf64_xword h1.elf64_sh_size; - natural_of_elf64_word h1.elf64_sh_link; - natural_of_elf64_word h1.elf64_sh_info; - natural_of_elf64_xword h1.elf64_sh_addralign; + natural_of_elf64_xword h1.elf64_sh_size; + natural_of_elf64_word h1.elf64_sh_link; + natural_of_elf64_word h1.elf64_sh_info; + natural_of_elf64_xword h1.elf64_sh_addralign; natural_of_elf64_xword h1.elf64_sh_entsize] [natural_of_elf64_word h2.elf64_sh_name; - natural_of_elf64_word h2.elf64_sh_type; + natural_of_elf64_word h2.elf64_sh_type; natural_of_elf64_xword h2.elf64_sh_flags; - natural_of_elf64_addr h2.elf64_sh_addr; + natural_of_elf64_addr h2.elf64_sh_addr; natural_of_elf64_off h2.elf64_sh_offset; - natural_of_elf64_xword h2.elf64_sh_size; - natural_of_elf64_word h2.elf64_sh_link; - natural_of_elf64_word h2.elf64_sh_info; - natural_of_elf64_xword h2.elf64_sh_addralign; + natural_of_elf64_xword h2.elf64_sh_size; + natural_of_elf64_word h2.elf64_sh_link; + natural_of_elf64_word h2.elf64_sh_info; + natural_of_elf64_xword h2.elf64_sh_addralign; natural_of_elf64_xword h2.elf64_sh_entsize] instance (Ord elf64_section_header_table_entry) @@ -616,7 +616,7 @@ val bytes_of_elf32_section_header_table : endianness -> elf32_section_header_table -> byte_sequence let bytes_of_elf32_section_header_table endian tbl = Byte_sequence.concat (List.map (bytes_of_elf32_section_header_table_entry endian) tbl) - + (** [bytes_of_elf64_section_header_table ed tbl] blits section header table [tbl] * to a byte sequence assuming endianness [ed]. *) @@ -637,9 +637,9 @@ let rec read_elf32_section_header_table' endian bs0 = return [] else read_elf32_section_header_table_entry endian bs0 >>= fun (entry, bs1) -> - read_elf32_section_header_table' endian bs1 >>= fun tail -> - return (entry::tail) - + read_elf32_section_header_table' endian bs1 >>= fun sht -> + return (sht ++ [entry]) + (** [read_elf64_section_header_table' ed bs0] parses an ELF64 section header table * from byte sequence [bs0] assuming endianness [ed]. Assumes [bs0] is of the * exact length required to parse the entire table. @@ -652,8 +652,8 @@ let rec read_elf64_section_header_table' endian bs0 = return [] else read_elf64_section_header_table_entry endian bs0 >>= fun (entry, bs1) -> - read_elf64_section_header_table' endian bs1 >>= fun tail -> - return (entry::tail) + read_elf64_section_header_table' endian bs1 >>= fun sht -> + return (sht ++ [entry]) (** [read_elf32_section_header_table sz ed bs0] parses an ELF32 section header * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness @@ -719,7 +719,7 @@ let is_elf32_addr_addralign_correct ent = align = 0 || align = 1 (* TODO: or a power of two *) else false - + (** [is_elf64_addr_addralign_correct ent] checks whether an internal address * alignment constraint is met on section header table [ent]. * TODO: needs tweaking to add in power-of-two constraint, too. @@ -752,7 +752,7 @@ let is_valid_elf32_section_header_table tbl = elf32_size_correct x tbl (* XXX: more correctness criteria in time *) end - + (** [is_valid_elf64_section_header_table sht] checks whether all entries of * section header table [sht] are valid. *) @@ -866,7 +866,7 @@ let string_of_elf64_section_header_table_entry' (os, proc, user) stbl entry = * functionality, in order to produce a [Show] instance for section header * table entries. *) - + val string_of_elf32_section_header_table_entry_default : elf32_section_header_table_entry -> string let string_of_elf32_section_header_table_entry_default = string_of_elf32_section_header_table_entry @@ -906,7 +906,7 @@ val string_of_elf64_section_header_table : sht_print_bundle -> elf64_section_header_table -> string let string_of_elf64_section_header_table sht_bdl tbl = unlines (List.map (string_of_elf64_section_header_table_entry sht_bdl) tbl) - + val string_of_elf64_section_header_table_default : elf64_section_header_table -> string let string_of_elf64_section_header_table_default = @@ -924,7 +924,7 @@ val string_of_elf64_section_header_table' : sht_print_bundle -> string_table -> elf64_section_header_table -> string let string_of_elf64_section_header_table' sht_bdl stbl tbl = unlines (List.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl) - + (** Section to segment mappings *) (** [elf32_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf: @@ -942,7 +942,7 @@ let is_elf32_tbss_special sec_hdr segment = (elf32_word_land sec_hdr.elf32_sh_flags (elf32_word_of_natural shf_tls)) <> elf32_word_of_natural 0 && ((natural_of_elf32_word sec_hdr.elf32_sh_type) = sht_nobits) && ((natural_of_elf32_word segment.elf32_p_type) <> elf_pt_tls) - + (** [elf64_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf: * * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ @@ -983,7 +983,7 @@ let rec get_elf32_section_to_segment_mapping hdr sects pent isin stbl = get_elf32_section_to_segment_mapping hdr xs pent isin stbl >>= fun tl -> return (str :: tl) end - + (** [get_elf64_section_to_segment_mapping hdr sht pht isin stbl] computes the * section to segment mapping for an ELF file using information in the section * header table [sht], program header table [pht] and file header [hdr]. A @@ -1008,7 +1008,7 @@ let rec get_elf64_section_to_segment_mapping hdr sects pent isin stbl = get_elf64_section_to_segment_mapping hdr xs pent isin stbl >>= fun tl -> return (str :: tl) end - + (** Section groups *) (** This is a COMDAT group and may duplicate other COMDAT groups in other object @@ -1044,7 +1044,7 @@ let obtain_elf32_section_group_indices endian sht bs0 = return (flag, xs) end ) filtered - + (** [obtain_elf64_section_group_indices endian sht bs0] extracts all section header * table indices of sections that are marked as being part of a section group. *) @@ -1074,7 +1074,7 @@ let obtain_elf64_section_group_indices endian sht bs0 = val obtain_elf32_tls_template : elf32_section_header_table -> elf32_section_header_table let obtain_elf32_tls_template sht = List.filter (fun ent -> - let flags = natural_of_elf32_word ent.elf32_sh_flags in + let flags = natural_of_elf32_word ent.elf32_sh_flags in natural_land flags shf_tls <> 0) sht (** [obtain_elf64_tls_template sht] extracts the TLS template (i.e. all sections @@ -1083,9 +1083,9 @@ let obtain_elf32_tls_template sht = val obtain_elf64_tls_template : elf64_section_header_table -> elf64_section_header_table let obtain_elf64_tls_template sht = List.filter (fun ent -> - let flags = natural_of_elf64_xword ent.elf64_sh_flags in + let flags = natural_of_elf64_xword ent.elf64_sh_flags in natural_land flags shf_tls <> 0) sht - + (** [obtain_elf32_hash_table endian sht bs0] extracts a hash table from an ELF file * providing a section of type SHT_HASH exists in section header table [sht]. * Extraction is from byte sequence [bs0] assuming endianness [endian]. The @@ -1111,7 +1111,7 @@ let obtain_elf32_hash_table endian sht bs0 = return (nbucket, nchain, buckets, chain) | _ -> fail "obtain_elf32_hash_table: multiple section header table entries of type sht_hash" end - + (** [obtain_elf64_hash_table endian sht bs0] extracts a hash table from an ELF file * providing a section of type SHT_HASH exists in section header table [sht]. * Extraction is from byte sequence [bs0] assuming endianness [endian]. The