(*Generated by Lem from elf_file.lem.*) (** Module [elf_file] packages all components of an ELF file up into a single * record, provides I/O routines for this record, as well as other utility * functions that operate on an entire ELF file. *) open Lem_basic_classes open Lem_bool open Lem_list open Lem_num open Lem_maybe open Lem_string open Elf_header open Elf_interpreted_section open Elf_interpreted_segment open Elf_types_native_uint open Elf_section_header_table open Elf_symbol_table open Elf_program_header_table open String_table open Byte_sequence open Error open Missing_pervasives open Show (** [elf32_file] record captures the internal structure of an ELF32 file. * Invariant: length of the program header and section header tables should match * the length of their interpreted counterparts, and the nth element of the * (program/section) header table must correspond to the nth element of the * interpreted (segments/sections), respectively. *) type elf32_file = { elf32_file_header : elf32_header (** The file header. *) ; elf32_file_program_header_table : elf32_program_header_table (** The program header table. *) ; elf32_file_section_header_table : elf32_section_header_table (** The section header table. *) ; elf32_file_interpreted_segments : elf32_interpreted_segments (** A more usable interpretation of the file's segments. *) ; elf32_file_interpreted_sections : elf32_interpreted_sections (** A more usable interpretation of the file's sections. *) ; elf32_file_bits_and_bobs : (Nat_big_num.num * byte_sequence) list (** The uninterpreted "rubbish" that may appear in gaps in the binary file. *) } (** [bytes_of_elf32_file f1] blits ELF file [f1] to a byte sequence, ready for * writing to a binary file. Fails if the invariant on [elf32_file] mentioned * above is not respected. *) (*val bytes_of_elf32_file : elf32_file -> error byte_sequence*) let bytes_of_elf32_file ef:(byte_sequence)error= (let endian = (get_elf32_header_endianness ef.elf32_file_header) in let hdr_bytes = (bytes_of_elf32_header ef.elf32_file_header) in let hdr_layout = (Nat_big_num.of_int 0, hdr_bytes) in let pht_bytes = (bytes_of_elf32_program_header_table endian ef.elf32_file_program_header_table) in let sht_bytes = (bytes_of_elf32_section_header_table endian ef.elf32_file_section_header_table) in let pht_off = (Nat_big_num.of_string (Uint32.to_string ef.elf32_file_header.elf32_phoff)) in let sht_off = (Nat_big_num.of_string (Uint32.to_string ef.elf32_file_header.elf32_shoff)) in let pht_layout = (pht_off, pht_bytes) in let sht_layout = (sht_off, sht_bytes) in let bab_layout = (ef.elf32_file_bits_and_bobs) in if List.length ef.elf32_file_program_header_table = List.length ef.elf32_file_interpreted_segments then if List.length ef.elf32_file_section_header_table = List.length ef.elf32_file_interpreted_sections then let segs_zip = (Lem_list.list_combine ef.elf32_file_program_header_table ef.elf32_file_interpreted_segments) in let sects_zip = (Lem_list.list_combine ef.elf32_file_section_header_table ef.elf32_file_interpreted_sections) in let segs_layout = (Lem_list.map (fun (seg, interp_seg) -> (Nat_big_num.of_string (Uint32.to_string seg.elf32_p_offset), interp_seg.elf32_segment_body) ) (List.filter (fun (x, _) -> not (x.elf32_p_filesz = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) segs_zip)) in let sects_layout = (Lem_list.map (fun (sect, interp_sect) -> (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset), interp_sect.elf32_section_body) ) (List.filter (fun (x, _) -> not (x.elf32_sh_type = (Uint32.of_string (Nat_big_num.to_string sht_nobits)))) sects_zip)) in let pre_layout = (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev [hdr_layout; pht_layout; sht_layout]) sects_layout)) segs_layout)) bab_layout) in let final_layout = (List.sort (fun (off_x, _) (off_y, _) -> Nat_big_num.compare off_x off_y) pre_layout) in let concats = (foldM (fun x y -> let (current_offset, so_far) = x in let (point_to_add, body) = y in if Nat_big_num.less point_to_add current_offset then let diff = (Nat_big_num.sub_nat current_offset point_to_add) in (* Completely contained inside other segment *) if Nat_big_num.less (Byte_sequence.length0 body) diff then return (current_offset, so_far) else Byte_sequence.partition0 diff body >>= (fun (_, cut) -> let concat3 = (Byte_sequence.concat0 [so_far; cut]) in let delta = (Nat_big_num.add current_offset (Byte_sequence.length0 cut)) in return (delta, concat3)) else let diff = (Nat_big_num.sub_nat point_to_add current_offset) in let reps = (Byte_sequence.create diff '\000') in let concat3 = (Byte_sequence.concat0 [so_far; reps; body]) in let delta = (Nat_big_num.add point_to_add (Byte_sequence.length0 body)) in return (delta, concat3) ) (Nat_big_num.of_int 0, Byte_sequence.empty) final_layout) in concats >>= (fun (offset, body) -> return body) else fail "bytes_of_elf32_file: interpreted sections and section header table must have same length" else fail "bytes_of_elf32_file: interpreted segments and program header table must have same length") (** [elf64_file] record captures the internal structure of an ELF32 file. * Invariant: length of the program header and section header tables should match * the length of their interpreted counterparts, and the nth element of the * (program/section) header table must correspond to the nth element of the * interpreted (segments/sections), respectively. *) type elf64_file = { elf64_file_header : elf64_header (** The file header. *) ; elf64_file_program_header_table : elf64_program_header_table (** The program header table. *) ; elf64_file_section_header_table : elf64_section_header_table (** The section header table. *) ; elf64_file_interpreted_segments : elf64_interpreted_segments (** A more usable interpretation of the file's segments. *) ; elf64_file_interpreted_sections : elf64_interpreted_sections (** A more usable interpretation of the file's sections. *) ; elf64_file_bits_and_bobs : (Nat_big_num.num * byte_sequence) list (** The uninterpreted "rubbish" that may appear in gaps in the binary file. *) } type elf_file = | ELF_File_32 of elf32_file | ELF_File_64 of elf64_file (** [bytes_of_elf64_file f1] blits ELF file [f1] to a byte sequence, ready for * writing to a binary file. Fails if the invariant on [elf64_file] mentioned * above is not respected. *) (*val bytes_of_elf64_file : elf64_file -> error byte_sequence*) let bytes_of_elf64_file ef:(byte_sequence)error= (let endian = (get_elf64_header_endianness ef.elf64_file_header) in let hdr_bytes = (bytes_of_elf64_header ef.elf64_file_header) in let hdr_layout = (Nat_big_num.of_int 0, hdr_bytes) in let pht_bytes = (bytes_of_elf64_program_header_table endian ef.elf64_file_program_header_table) in let sht_bytes = (bytes_of_elf64_section_header_table endian ef.elf64_file_section_header_table) in let pht_off = (Nat_big_num.of_string (Uint64.to_string ef.elf64_file_header.elf64_phoff)) in let sht_off = (Nat_big_num.of_string (Uint64.to_string ef.elf64_file_header.elf64_shoff)) in let pht_layout = (pht_off, pht_bytes) in let sht_layout = (sht_off, sht_bytes) in let bab_layout = (ef.elf64_file_bits_and_bobs) in if (* List.length ef.elf64_file_program_header_table = List.length ef.elf64_file_interpreted_segments *) true then if List.length ef.elf64_file_section_header_table = List.length ef.elf64_file_interpreted_sections then let segs_zip = (Lem_list.list_combine ef.elf64_file_program_header_table ef.elf64_file_interpreted_segments) in let sects_zip = (Lem_list.list_combine ef.elf64_file_section_header_table ef.elf64_file_interpreted_sections) in let segs_layout = ([]) (* List.map (fun (seg, interp_seg) -> (natural_of_elf64_off seg.elf64_p_offset, interp_seg.elf64_segment_body) ) (List.filter (fun (x, _) -> x.elf64_p_filesz <> elf64_xword_of_natural 0) segs_zip) *) in let sects_layout = (Lem_list.map (fun (sect, interp_sect) -> (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset), interp_sect.elf64_section_body) ) (List.filter (fun (x, _) -> not (x.elf64_sh_type = (Uint32.of_string (Nat_big_num.to_string sht_nobits)))) sects_zip)) in let pre_layout = (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev [hdr_layout; pht_layout; sht_layout]) sects_layout)) segs_layout)) bab_layout) in let final_layout = (List.sort (fun (off_x, _) (off_y, _) -> Nat_big_num.compare off_x off_y) pre_layout) in let concats = (foldM (fun x y -> let (current_offset, so_far) = x in let (point_to_add, body) = y in if Nat_big_num.less point_to_add current_offset then let diff = (Nat_big_num.sub_nat current_offset point_to_add) in (* Completely contained inside other segment *) if Nat_big_num.less (Byte_sequence.length0 body) diff then return (current_offset, so_far) else Byte_sequence.partition0 diff body >>= (fun (_, cut) -> let concat3 = (Byte_sequence.concat0 [so_far; cut]) in let delta = (Nat_big_num.add current_offset (Byte_sequence.length0 cut)) in return (delta, concat3)) else let diff = (Nat_big_num.sub_nat point_to_add current_offset) in let reps = (Byte_sequence.create diff '\000') in let concat3 = (Byte_sequence.concat0 [so_far; reps; body]) in let delta = (Nat_big_num.add point_to_add (Byte_sequence.length0 body)) in return (delta, concat3) ) (Nat_big_num.of_int 0, Byte_sequence.empty) final_layout) in concats >>= (fun (offset, body) -> return body) else fail "bytes_of_elf64_file: interpreted sections and section header table must have same length" else fail "bytes_of_elf64_file: interpreted segments and program header table must have same length") (** [obtain_elf32_program_header_table hdr bs0] reads a file's program header table * from byte sequence [bs0] using information gleaned from the file header [hdr]. * Fails if transcription fails. *) (*val obtain_elf32_program_header_table : elf32_header -> byte_sequence -> error elf32_program_header_table*) let obtain_elf32_program_header_table hdr bs0:((elf32_program_header_table_entry)list)error= (let endian = (get_elf32_header_endianness hdr) in let pentries = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phnum)) in let pentry_size = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phentsize)) in let psize = (Nat_big_num.mul pentries pentry_size) in if Nat_big_num.equal psize(Nat_big_num.of_int 0) then return [] else let poffset = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phoff)) in Byte_sequence.offset_and_cut poffset psize bs0 >>= (fun pexact -> (* Byte sequence irrelevant below as exact size used... *) read_elf32_program_header_table psize endian pexact >>= (fun (pht, _) -> return pht))) (** [obtain_elf64_program_header_table hdr bs0] reads a file's program header table * from byte sequence [bs0] using information gleaned from the file header [hdr]. * Fails if transcription fails. *) (*val obtain_elf64_program_header_table : elf64_header -> byte_sequence -> error elf64_program_header_table*) let obtain_elf64_program_header_table hdr bs0:((elf64_program_header_table_entry)list)error= (let endian = (get_elf64_header_endianness hdr) in let pentries = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phnum)) in let pentry_size = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phentsize)) in let psize = (Nat_big_num.mul pentries pentry_size) in if Nat_big_num.equal psize(Nat_big_num.of_int 0) then return [] else let poffset = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_phoff)) in Byte_sequence.offset_and_cut poffset psize bs0 >>= (fun pexact -> (* Byte sequence irrelevant below as exact size used... *) read_elf64_program_header_table psize endian pexact >>= (fun (pht, _) -> return pht))) (** [obtain_elf32_section_header_table hdr bs0] reads a file's section header table * from byte sequence [bs0] using information gleaned from the file header [hdr]. * Fails if transcription fails. *) (*val obtain_elf32_section_header_table : elf32_header -> byte_sequence -> error elf32_section_header_table*) let obtain_elf32_section_header_table hdr bs0:((elf32_section_header_table_entry)list)error= (let endian = (get_elf32_header_endianness hdr) in let sentries = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shnum)) in let sentry_size = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shentsize)) in let ssize = (Nat_big_num.mul sentries sentry_size) in if Nat_big_num.equal ssize(Nat_big_num.of_int 0) then return [] else let soffset = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shoff)) in Byte_sequence.offset_and_cut soffset ssize bs0 >>= (fun sexact -> (* Byte sequence irrelevant below as exact size used... *) read_elf32_section_header_table ssize endian sexact >>= (fun (sht, _) -> return sht))) (** [obtain_elf64_section_header_table hdr bs0] reads a file's section header table * from byte sequence [bs0] using information gleaned from the file header [hdr]. * Fails if transcription fails. *) (*val obtain_elf64_section_header_table : elf64_header -> byte_sequence -> error elf64_section_header_table*) let obtain_elf64_section_header_table hdr bs0:((elf64_section_header_table_entry)list)error= (let endian = (get_elf64_header_endianness hdr) in let sentries = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shnum)) in let sentry_size = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shentsize)) in let ssize = (Nat_big_num.mul sentries sentry_size) in if Nat_big_num.equal ssize(Nat_big_num.of_int 0) then return [] else let soffset = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_shoff)) in Byte_sequence.offset_and_cut soffset ssize bs0 >>= (fun sexact -> (* 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]. * Fails if transcription fails. *) (*val obtain_elf32_section_header_string_table : elf32_header -> elf32_section_header_table -> byte_sequence -> error (maybe string_table)*) let obtain_elf32_section_header_string_table hdr sht bs0:((string_table)option)error= (if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) shn_undef then return None else (match Ml_bindings.list_index_big_int (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) sht with None -> fail "no section header string table" | Some x -> return x ) >>= (fun sh -> Byte_sequence.offset_and_cut (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_offset)) (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_size)) bs0 >>= (fun sexact -> return (Some (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]. * Fails if transcription fails. *) (*val obtain_elf64_section_header_string_table : elf64_header -> elf64_section_header_table -> byte_sequence -> error (maybe string_table)*) let obtain_elf64_section_header_string_table hdr sht bs0:((string_table)option)error= (if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) shn_undef then return None else (match Ml_bindings.list_index_big_int (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) sht with None -> fail "no section header string table" | Some x -> return x ) >>= (fun sh -> Byte_sequence.offset_and_cut (Nat_big_num.of_string (Uint64.to_string sh.elf64_sh_offset)) (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) bs0 >>= (fun sexact -> return (Some (string_table_of_byte_sequence sexact))))) (** [obtain_elf32_interpreted_segments pht bs0] generates the interpreted segments * of an ELF file from the uninterpreted program header table entries in [pht], * read from byte sequence [bs0]. Makes working with segments easier. * May fail if transcription of any segment fails. *) (*val obtain_elf32_interpreted_segments : elf32_program_header_table -> byte_sequence -> error elf32_interpreted_segments*) let obtain_elf32_interpreted_segments pht bdy:((elf32_interpreted_segment)list)error= (mapM (fun ph -> let offset = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_offset)) in let size2 = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_filesz)) in (if Nat_big_num.equal size2(Nat_big_num.of_int 0) then return Byte_sequence.empty else Byte_sequence.offset_and_cut offset size2 bdy) >>= (fun relevant -> let vaddr = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_vaddr)) in let paddr = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_paddr)) in let memsz = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_memsz)) in let typ = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_type)) in let align = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_align)) in let flags = (elf32_interpret_program_header_flags ph.elf32_p_flags) in if Nat_big_num.less memsz size2 then fail "obtain_elf32_interpreted_segments: memory size of segment cannot be less than file size" else return { elf32_segment_body = relevant; elf32_segment_type = typ; elf32_segment_size = size2; elf32_segment_memsz = memsz; elf32_segment_base = vaddr; elf32_segment_flags = flags; elf32_segment_paddr = paddr; elf32_segment_align = align; elf32_segment_offset = offset }) ) pht) (** [obtain_elf64_interpreted_segments pht bs0] generates the interpreted segments * of an ELF file from the uninterpreted program header table entries in [pht], * read from byte sequence [bs0]. Makes working with segments easier. * May fail if transcription of any segment fails. *) (*val obtain_elf64_interpreted_segments : elf64_program_header_table -> byte_sequence -> error elf64_interpreted_segments*) let obtain_elf64_interpreted_segments pht bdy:((elf64_interpreted_segment)list)error= (mapM (fun ph -> let offset = (Nat_big_num.of_string (Uint64.to_string ph.elf64_p_offset)) in let size2 = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_filesz) in (if Nat_big_num.equal size2(Nat_big_num.of_int 0) then return Byte_sequence.empty else Byte_sequence.offset_and_cut offset size2 bdy) >>= (fun relevant -> let vaddr = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_vaddr) in let paddr = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_paddr) in let memsz = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_memsz) in let typ = (Nat_big_num.of_string (Uint32.to_string ph.elf64_p_type)) in let align = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_align) in let flags = (elf64_interpret_program_header_flags ph.elf64_p_flags) in if Nat_big_num.less memsz size2 then fail "obtain_elf64_interpreted_segments: memory size of segment cannot be less than file size" else return { elf64_segment_body = relevant; elf64_segment_type = typ; elf64_segment_size = size2; elf64_segment_memsz = memsz; elf64_segment_base = vaddr; elf64_segment_flags = flags; elf64_segment_align = align; elf64_segment_paddr = paddr; elf64_segment_offset = offset }) ) pht) (** [obtain_elf32_interpreted_section sht bs0] generates the interpreted sections * of an ELF file from the uninterpreted section header table entries in [sht], * read from byte sequence [bs0]. Makes working with sections easier. * May fail if transcription of any section fails. *) (*val obtain_elf32_interpreted_sections : maybe string_table -> elf32_section_header_table -> byte_sequence -> error elf32_interpreted_sections*) let obtain_elf32_interpreted_sections shstrtab sht bs0:((elf32_interpreted_section)list)error= (mapM (fun sh -> let offset = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_offset)) in let size2 = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_size)) in let name1 = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_name)) in let typ = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_type)) in let filesz = (if Nat_big_num.equal typ sht_nobits then Nat_big_num.of_int 0 else size2) in let flags = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_flags)) in let base = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_addr)) in let link1 = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_link)) in let info = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_info)) in let align = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_addralign)) in let entry_size = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_entsize)) in let name_string = ((match shstrtab with None -> "" | Some shstrtab -> (match (get_string_at name1 shstrtab) with | Success n -> n | Fail _ -> "" ) )) in (if Nat_big_num.equal filesz(Nat_big_num.of_int 0) then return Byte_sequence.empty else Byte_sequence.offset_and_cut offset filesz bs0) >>= (fun relevant -> return { elf32_section_name = name1; elf32_section_type = typ; elf32_section_size = size2; elf32_section_offset = offset; elf32_section_flags = flags; elf32_section_addr = base; elf32_section_link = link1; elf32_section_info = info; elf32_section_align = align; elf32_section_body = relevant; elf32_section_entsize = entry_size; elf32_section_name_as_string = name_string }) ) sht) (** [obtain_elf64_interpreted_section sht bs0] generates the interpreted sections * of an ELF file from the uninterpreted section header table entries in [sht], * read from byte sequence [bs0]. Makes working with sections easier. * May fail if transcription of any section fails. *) (*val obtain_elf64_interpreted_sections : maybe string_table -> elf64_section_header_table -> byte_sequence -> error elf64_interpreted_sections*) let obtain_elf64_interpreted_sections shstrtab sht bs0:((elf64_interpreted_section)list)error= (mapM (fun sh -> let offset = (Nat_big_num.of_string (Uint64.to_string sh.elf64_sh_offset)) in let size2 = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) in let name1 = (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_name)) in let typ = (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_type)) in let filesz = (if Nat_big_num.equal typ sht_nobits then Nat_big_num.of_int 0 else size2) in let flags = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_flags) in let base = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addr) in let link1 = (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_link)) in let info = (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_info)) in let align = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addralign) in let entry_size = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_entsize) in let name_string = ((match shstrtab with None -> "" | Some shstrtab -> (match (get_string_at name1 shstrtab) with | Success n -> n | Fail _ -> "" ) )) in (if Nat_big_num.equal filesz(Nat_big_num.of_int 0) then return Byte_sequence.empty else Byte_sequence.offset_and_cut offset filesz bs0) >>= (fun relevant -> return { elf64_section_name = name1; elf64_section_type = typ; elf64_section_size = size2; elf64_section_offset = offset; elf64_section_flags = flags; elf64_section_addr = base; elf64_section_link = link1; elf64_section_info = info; elf64_section_align = align; elf64_section_body = relevant; elf64_section_entsize = entry_size; elf64_section_name_as_string = name_string }) ) sht) (** [find_first_not_in_range e rngs] for every pair (start, end) in [rngs], finds * the first element, beginning counting from [e], that does not lie between * a start and end value. *) (*val find_first_not_in_range : natural -> list (natural * natural) -> natural*) let rec find_first_not_in_range start ranges:Nat_big_num.num= ((match List.filter (fun (x, y) -> Nat_big_num.greater_equal start x && Nat_big_num.less_equal start y) ranges with | [] -> start | _ -> find_first_not_in_range ( Nat_big_num.add start(Nat_big_num.of_int 1)) ranges )) (** [find_first_in_range e rngs] for every pair (start, end) in [rngs], finds * the first element, beginning counting from [e], that lies between * a start and end value. *) (*val find_first_in_range : natural -> list (natural * natural) -> natural*) let rec find_first_in_range start ranges:Nat_big_num.num= ((match List.filter (fun (x, y) -> Nat_big_num.greater_equal start x && Nat_big_num.less_equal start y) ranges with | [] -> find_first_in_range ( Nat_big_num.add start(Nat_big_num.of_int 1)) ranges | _ -> start )) (** [compute_differences start max ranges] is a utility function used for calculating * "dead" spots in an ELF file not covered by any of the interpreted structure * that nevertheless need recording in the bits_and_bobs field of each ELF record * in order to maintain in-out roundtripping up to exact binary equivalence. *) (*val compute_differences : natural -> natural -> list (natural * natural) -> error (list (natural * natural))*) let rec compute_differences start max ranges:((Nat_big_num.num*Nat_big_num.num)list)error= (if Nat_big_num.equal start max then return [] else if Nat_big_num.greater start max then fail "compute_differences: passed maximum" else let first = (find_first_not_in_range start ranges) in if Nat_big_num.greater_equal first max then return [] else let last1 = (find_first_in_range first ranges) in if Nat_big_num.greater last1 max then return [(first, max)] else compute_differences last1 max ranges >>= (fun tail -> return ((first, last1)::tail))) (** [obtain_elf32_bits_and_bobs hdr pht segs sht sects bs0] identifies and records * the "dead" spots of an ELF file not covered by any meaningful structure of the * ELF file format. *) (*val obtain_elf32_bits_and_bobs : elf32_header -> elf32_program_header_table -> elf32_interpreted_segments -> elf32_section_header_table -> elf32_interpreted_sections -> byte_sequence -> error (list (natural * byte_sequence))*) let obtain_elf32_bits_and_bobs hdr segs interp_segs sects interp_sects bs0:((Nat_big_num.num*byte_sequence)list)error= (let hdr_off_len = (Nat_big_num.of_int 0, Nat_big_num.of_string (Uint32.to_string hdr.elf32_ehsize)) in let pht_off = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phoff)) in let pht_len = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phentsize)) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phnum))) in let pht_off_len = (pht_off, Nat_big_num.add pht_off pht_len) in let sht_off = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shoff)) in let sht_len = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shentsize)) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shnum))) in let sht_off_len = (sht_off, Nat_big_num.add sht_off sht_len) in if List.length interp_segs = List.length segs then let seg_zip = (Lem_list.list_combine segs interp_segs) in if List.length interp_sects = List.length sects then let sect_zip = (Lem_list.list_combine sects interp_sects) in let seg_off_len = (Lem_list.map (fun (seg, interp_seg) -> let start = (Nat_big_num.of_string (Uint32.to_string seg.elf32_p_offset)) in let len = (interp_seg.elf32_segment_size) in (start, Nat_big_num.add start len)) seg_zip) in let sect_off_len = (Lem_list.map (fun (sect, interp_sect) -> let start = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset)) in let len = (interp_sect.elf32_section_size) in (start, Nat_big_num.add start len)) sect_zip) in let pre_layout = (hdr_off_len :: (pht_off_len :: (sht_off_len :: List.rev_append (List.rev seg_off_len) sect_off_len))) in let layout = (List.sort (fun (off_x, _) (off_y, _) -> Nat_big_num.compare off_x off_y ) pre_layout) in compute_differences(Nat_big_num.of_int 0) (Byte_sequence.length0 bs0) layout >>= (fun diffs -> mapM (fun (start, len) -> Byte_sequence.offset_and_cut start ( Nat_big_num.sub_nat len start) bs0 >>= (fun rel -> return (start, rel)) ) diffs) else fail "obtain_elf32_bits_and_bobs: section header table and interpreted section differ in length" else fail "obtain_elf32_bits_and_bobs: program header table and interpreted segments differ in length") (** [obtain_elf64_bits_and_bobs hdr pht segs sht sects bs0] identifies and records * the "dead" spots of an ELF file not covered by any meaningful structure of the * ELF file format. *) (*val obtain_elf64_bits_and_bobs : elf64_header -> elf64_program_header_table -> elf64_interpreted_segments -> 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:((Nat_big_num.num*byte_sequence)list)error= (let hdr_off_len = (Nat_big_num.of_int 0, Nat_big_num.of_string (Uint32.to_string hdr.elf64_ehsize)) in let pht_off = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_phoff)) in let pht_len = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phentsize)) (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phnum))) in let pht_off_len = (pht_off, Nat_big_num.add pht_off pht_len) in let sht_off = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_shoff)) in let sht_len = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shentsize)) (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shnum))) in let sht_off_len = (sht_off, Nat_big_num.add sht_off sht_len) in if List.length interp_segs = List.length segs then let seg_zip = (Lem_list.list_combine segs interp_segs) in if List.length interp_sects = List.length sects then let sect_zip = (Lem_list.list_combine sects interp_sects) in let seg_off_len = (Lem_list.map (fun (seg, interp_seg) -> let start = (Nat_big_num.of_string (Uint64.to_string seg.elf64_p_offset)) in let len = (interp_seg.elf64_segment_size) in (start, Nat_big_num.add start len)) seg_zip) in let sect_off_len = (Lem_list.map (fun (sect, interp_sect) -> let start = (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset)) in let len = (interp_sect.elf64_section_size) in (start, Nat_big_num.add start len)) sect_zip) in let pre_layout = (hdr_off_len :: (pht_off_len :: (sht_off_len :: List.rev_append (List.rev seg_off_len) sect_off_len))) in let layout = (List.sort (fun (off_x, _) (off_y, _) -> Nat_big_num.compare off_x off_y ) pre_layout) in compute_differences(Nat_big_num.of_int 0) (Byte_sequence.length0 bs0) layout >>= (fun diffs -> mapM (fun (start, finish) -> Byte_sequence.offset_and_cut start ( Nat_big_num.sub_nat finish start) bs0 >>= (fun rel -> return (start, rel)) ) diffs) else fail "obtain_elf64_bits_and_bobs: section header table and interpreted section differ in length" else fail "obtain_elf64_bits_and_bobs: program header table and interpreted segments differ in length") (** [read_elf32_file bs0] reads an ELF32 file from byte sequence [bs0]. Fails if * transcription fails. *) (*val read_elf32_file : byte_sequence -> error elf32_file*) let read_elf32_file bs0:(elf32_file)error= (read_elf32_header bs0 >>= (fun (hdr, bs1) -> obtain_elf32_program_header_table hdr bs0 >>= (fun pht -> obtain_elf32_section_header_table hdr bs0 >>= (fun sht -> obtain_elf32_section_header_string_table hdr sht bs0 >>= (fun shstrtab -> obtain_elf32_interpreted_segments pht bs0 >>= (fun segs -> obtain_elf32_interpreted_sections shstrtab sht bs0 >>= (fun sects -> obtain_elf32_bits_and_bobs hdr pht segs sht sects bs0 >>= (fun bits_and_bobs -> return { elf32_file_header = hdr; elf32_file_program_header_table = pht; elf32_file_section_header_table = sht; elf32_file_interpreted_segments = segs; elf32_file_interpreted_sections = sects; elf32_file_bits_and_bobs = bits_and_bobs })))))))) (** [read_elf64_file bs0] reads an ELF64 file from byte sequence [bs0]. Fails if * transcription fails. *) (*val read_elf64_file : byte_sequence -> error elf64_file*) let read_elf64_file bs0:(elf64_file)error= (read_elf64_header bs0 >>= (fun (hdr, bs1) -> obtain_elf64_program_header_table hdr bs0 >>= (fun pht -> obtain_elf64_section_header_table hdr bs0 >>= (fun sht -> obtain_elf64_section_header_string_table hdr sht bs0 >>= (fun shstrtab -> obtain_elf64_interpreted_segments pht bs0 >>= (fun segs -> obtain_elf64_interpreted_sections shstrtab sht bs0 >>= (fun sects -> obtain_elf64_bits_and_bobs hdr pht segs sht sects bs0 >>= (fun bits_and_bobs -> return { elf64_file_header = hdr; elf64_file_program_header_table = pht; elf64_file_section_header_table = sht; elf64_file_interpreted_segments = segs; elf64_file_interpreted_sections = sects; elf64_file_bits_and_bobs = bits_and_bobs })))))))) (** [get_elf32_file_secton_header_string_table f1] returns the ELF file, [f1], * section header string table. * TODO: why is this not using obtain_elf32_section_header_string_table above? *) (*val get_elf32_file_section_header_string_table : elf32_file -> error string_table*) let get_elf32_file_section_header_string_table f3:(string_table)error= (let hdr = (f3.elf32_file_header) in let sht = (f3.elf32_file_section_header_table) in let segs = (f3.elf32_file_interpreted_segments) in let idx1 = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) in bytes_of_elf32_file f3 >>= (fun bs0 -> (match Ml_bindings.list_index_big_int idx1 sht with | None -> fail "obtain_elf32_string_table: invalid offset into section header table" | Some sect -> let offset = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset)) in let size2 = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_size)) in Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel -> let strings = (Byte_sequence.string_of_byte_sequence rel) in return (String_table.mk_string_table strings Missing_pervasives.null_char)) ))) (** [get_elf64_file_secton_header_string_table f1] returns the ELF file, [f1], * section header string table. * TODO: why is this not using obtain_elf64_section_header_string_table above? *) (*val get_elf64_file_section_header_string_table : elf64_file -> error string_table*) let get_elf64_file_section_header_string_table f3:(string_table)error= (let hdr = (f3.elf64_file_header) in let sht = (f3.elf64_file_section_header_table) in let segs = (f3.elf64_file_interpreted_segments) in let idx1 = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) in bytes_of_elf64_file f3 >>= (fun bs0 -> (match Ml_bindings.list_index_big_int idx1 sht with | None -> fail "obtain_elf64_string_table: invalid offset into section header table" | Some sect -> let offset = (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset)) in let size2 = (Ml_bindings.nat_big_num_of_uint64 sect.elf64_sh_size) in Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel -> let strings = (Byte_sequence.string_of_byte_sequence rel) in return (String_table.mk_string_table strings Missing_pervasives.null_char)) ))) (*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:((elf32_symbol_table_entry)list*string_table*Nat_big_num.num)error= ((match Lem_list.list_index f.elf32_file_interpreted_sections (Nat_big_num.to_int sec_idx) with None -> fail "impossible: interpreted section found but not indexable" | Some sec -> return sec ) >>= (fun sec -> (match Lem_list.list_index f.elf32_file_interpreted_sections (Nat_big_num.to_int sec.elf32_section_link) with None -> fail "no associated strtab" | Some strs -> return strs ) >>= (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 read_elf32_symbol_table endian sec.elf32_section_body >>= (fun symtab -> return (symtab, strtab, sec_idx))))) (*val find_elf32_symtab_by_type : natural -> elf32_file -> error (elf32_symbol_table * string_table * natural)*) let find_elf32_symtab_by_type t f:(elf32_symbol_table*string_table*Nat_big_num.num)error= (let found_symtab_index = (find_index0 (fun sh -> Nat_big_num.equal sh.elf32_section_type t) f.elf32_file_interpreted_sections) in (match found_symtab_index with None -> fail "no such symtab" | Some sec_idx -> return sec_idx ) >>= (fun sec_idx -> find_elf32_symbols_by_symtab_idx sec_idx f)) (*val find_elf64_symbols_by_symtab_idx : natural -> elf64_file -> error (elf64_symbol_table * string_table * natural)*) let find_elf64_symbols_by_symtab_idx sec_idx f:((elf64_symbol_table_entry)list*string_table*Nat_big_num.num)error= ((match Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int sec_idx) with None -> fail "impossible: interpreted section found but not indexable" | Some sec -> return sec ) >>= (fun sec -> (match Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int sec.elf64_section_link) with None -> fail "no associated strtab" | Some strs -> return strs ) >>= (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 read_elf64_symbol_table endian sec.elf64_section_body >>= (fun symtab -> return (symtab, strtab, sec_idx))))) (*val find_elf64_symtab_by_type : natural -> elf64_file -> error (elf64_symbol_table * string_table * natural)*) let find_elf64_symtab_by_type t f:(elf64_symbol_table*string_table*Nat_big_num.num)error= (let found_symtab_index = (find_index0 (fun sh -> Nat_big_num.equal sh.elf64_section_type t) f.elf64_file_interpreted_sections) in (match found_symtab_index with None -> fail "no such symtab" | Some sec_idx -> return sec_idx ) >>= (fun sec_idx -> find_elf64_symbols_by_symtab_idx sec_idx f)) (** [get_elf32_file_symbol_string_table f1] returns the ELF file [f1] symbol * string table. May fail. *) (*val get_elf32_file_symbol_string_table : elf32_file -> error string_table*) let get_elf32_file_symbol_string_table f3:(string_table)error= (let hdr = (f3.elf32_file_header) in let sht = (f3.elf32_file_section_header_table) in let segs = (f3.elf32_file_interpreted_segments) in let strtabs = (Missing_pervasives.mapMaybei (fun index sect -> if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_type)) sht_strtab then if Nat_big_num.equal index (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) then None else Some sect else None) sht) in bytes_of_elf32_file f3 >>= (fun bs0 -> mapM (fun sect -> let offset = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset)) in let size2 = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_size)) in Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun bs1 -> let strings = (Byte_sequence.string_of_byte_sequence bs1) in return (String_table.mk_string_table strings Missing_pervasives.null_char))) strtabs >>= (fun strings -> String_table.concat1 strings))) (** [get_elf64_file_symbol_string_table f1] returns the ELF file [f1] symbol * string table. May fail. *) (*val get_elf64_file_symbol_string_table : elf64_file -> error string_table*) let get_elf64_file_symbol_string_table f3:(string_table)error= (let hdr = (f3.elf64_file_header) in let sht = (f3.elf64_file_section_header_table) in let segs = (f3.elf64_file_interpreted_segments) in let strtabs = (Missing_pervasives.mapMaybei (fun index sect -> if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sect.elf64_sh_type)) sht_strtab then if Nat_big_num.equal index (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) then None else Some sect else None) sht) in bytes_of_elf64_file f3 >>= (fun bs0 -> mapM (fun sect -> let offset = (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset)) in let size2 = (Ml_bindings.nat_big_num_of_uint64 sect.elf64_sh_size) in Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun bs1 -> let strings = (Byte_sequence.string_of_byte_sequence bs1) in return (String_table.mk_string_table strings Missing_pervasives.null_char))) strtabs >>= (fun strings -> String_table.concat1 strings))) (** [get_elf32_file_symbol_table f1] returns the ELF file [f1] symbol * table. May fail. *) (*val get_elf32_file_symbol_table : elf32_file -> error elf32_symbol_table*) let get_elf32_file_symbol_table f3:((elf32_symbol_table_entry)list)error= (let hdr = (f3.elf32_file_header) in let sht = (f3.elf32_file_section_header_table) in let segs = (f3.elf32_file_interpreted_segments) in let endian = (get_elf32_header_endianness hdr) in let symtabs = (List.filter (fun sect -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_type)) sht_symtab ) sht) in (match symtabs with | [] -> return [] | [symtab] -> let offset = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_offset)) in let size2 = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_size)) in bytes_of_elf32_file f3 >>= (fun bs0 -> Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun relevant -> read_elf32_symbol_table endian relevant)) | _ -> fail "obtain_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB" )) (** [get_elf64_file_symbol_table f1] returns the ELF file [f1] symbol * table. May fail. *) (*val get_elf64_file_symbol_table : elf64_file -> error elf64_symbol_table*) let get_elf64_file_symbol_table f3:((elf64_symbol_table_entry)list)error= (let hdr = (f3.elf64_file_header) in let sht = (f3.elf64_file_section_header_table) in let segs = (f3.elf64_file_interpreted_segments) in let endian = (get_elf64_header_endianness hdr) in let symtabs = (List.filter (fun sect -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sect.elf64_sh_type)) sht_symtab ) sht) in (match symtabs with | [] -> return [] | [symtab] -> let offset = (Nat_big_num.of_string (Uint64.to_string symtab.elf64_sh_offset)) in let size2 = (Ml_bindings.nat_big_num_of_uint64 symtab.elf64_sh_size) in bytes_of_elf64_file f3 >>= (fun bs0 -> Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun relevant -> read_elf64_symbol_table endian relevant)) | _ -> fail "obtain_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB" )) (** [get_elf32_file_dynamic_symbol_table f1] returns the ELF file [f1] dynamic * symbol table. May fail. *) (*val get_elf32_file_dynamic_symbol_table : elf32_file -> error elf32_symbol_table*) let get_elf32_file_dynamic_symbol_table ef:((elf32_symbol_table_entry)list)error= (let hdr = (ef.elf32_file_header) in let sht = (ef.elf32_file_section_header_table) in let segs = (ef.elf32_file_interpreted_segments) in let endian = (get_elf32_header_endianness hdr) in let symtabs = (List.filter (fun sect -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_type)) sht_dynsym ) sht) in (match symtabs with | [] -> return [] | [symtab] -> let offset = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_offset)) in let size2 = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_size)) in bytes_of_elf32_file ef >>= (fun bs0 -> Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun relevant -> read_elf32_symbol_table endian relevant)) | _ -> fail "obtain_elf32_dynamic_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" )) (** [get_elf64_file_dynamic_symbol_table f1] returns the ELF file [f1] dynamic * symbol table. May fail. *) (*val get_elf64_file_dynamic_symbol_table : elf64_file -> error elf64_symbol_table*) let get_elf64_file_dynamic_symbol_table ef:((elf64_symbol_table_entry)list)error= (let hdr = (ef.elf64_file_header) in let sht = (ef.elf64_file_section_header_table) in let segs = (ef.elf64_file_interpreted_segments) in let endian = (get_elf64_header_endianness hdr) in let symtabs = (List.filter (fun sect -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sect.elf64_sh_type)) sht_dynsym ) sht) in (match symtabs with | [] -> return [] | [symtab] -> let offset = (Nat_big_num.of_string (Uint64.to_string symtab.elf64_sh_offset)) in let size2 = (Ml_bindings.nat_big_num_of_uint64 symtab.elf64_sh_size) in bytes_of_elf64_file ef >>= (fun bs0 -> Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun relevant -> read_elf64_symbol_table endian relevant)) | _ -> fail "obtain_elf64_dynamic_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" )) (** [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. *) (*val get_elf32_symbol_table_by_index : elf32_file -> natural -> error elf32_symbol_table*) let get_elf32_symbol_table_by_index ef link1:(elf32_symbol_table)error= (let hdr = (ef.elf32_file_header) in let sht = (ef.elf32_file_section_header_table) in let sects = (ef.elf32_file_interpreted_sections) in let endian = (get_elf32_header_endianness hdr) in (match Lem_list.list_index sects (Nat_big_num.to_int link1) with | None -> fail "get_elf32_symbol_table_by_index: invalid index" | Some sym -> read_elf32_symbol_table endian sym.elf32_section_body )) (** [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. *) (*val get_elf32_string_table_by_index : elf32_file -> natural -> error string_table*) let get_elf32_string_table_by_index ef link1:(string_table)error= (let hdr = (ef.elf32_file_header) in let sht = (ef.elf32_file_section_header_table) in let sects = (ef.elf32_file_interpreted_sections) in (match Lem_list.list_index sects (Nat_big_num.to_int link1) with | None -> fail "get_elf32_string_table_by_index: invalid index" | Some sym -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym.elf32_section_body) Missing_pervasives.null_char) )) (** [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. *) (*val get_elf64_symbol_table_by_index : elf64_file -> natural -> error elf64_symbol_table*) let get_elf64_symbol_table_by_index ef link1:(elf64_symbol_table)error= (let hdr = (ef.elf64_file_header) in let sht = (ef.elf64_file_section_header_table) in let sects = (ef.elf64_file_interpreted_sections) in let endian = (get_elf64_header_endianness hdr) in (match Lem_list.list_index sects (Nat_big_num.to_int link1) with | None -> fail "get_elf64_symbol_table_by_index: invalid index" | Some sym -> read_elf64_symbol_table endian sym.elf64_section_body )) (** [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. *) (*val get_elf64_string_table_by_index : elf64_file -> natural -> error string_table*) let get_elf64_string_table_by_index ef link1:(string_table)error= (let hdr = (ef.elf64_file_header) in let sht = (ef.elf64_file_section_header_table) in let sects = (ef.elf64_file_interpreted_sections) in (match Lem_list.list_index sects (Nat_big_num.to_int link1) with | None -> fail "get_elf64_string_table_by_index: invalid index" | Some sym -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym.elf64_section_body) Missing_pervasives.null_char) )) (** [segment_provenance] records whether a segment that appears in an executable * process image has been derived directly from an ELF file, or was automatically * created when the image calculation process noticed a segment with a memory * size greater than its file size. * Really a PPCMemism and not strictly needed for the ELF model itself. *) type segment_provenance = FromELF (** Segment derived directly from the source ELF file. *) | AutoGenerated (** Automatically generated during process extraction as memory size is greater than file size. *) (** [elf32_executable_process_image] is a process image for ELF32 files. Contains * all that is necessary to load the executable components of an ELF32 file * and begin execution. * XXX: (segments, provenance), entry point, machine type *) type elf32_executable_process_image = ( (elf32_interpreted_segment * segment_provenance)list * Nat_big_num.num * Nat_big_num.num) (** [elf64_executable_process_image] is a process image for ELF64 files. Contains * all that is necessary to load the executable components of an ELF64 file * and begin execution. * XXX: (segments, provenance), entry point, machine type *) type elf64_executable_process_image = ( (elf64_interpreted_segment * segment_provenance)list * Nat_big_num.num * Nat_big_num.num) (** [get_elf32_executable_image f1] extracts an executable process image from an * executable ELF file. May fail if extraction is impossible. *) (*val get_elf32_executable_image : elf32_file -> error elf32_executable_process_image*) let get_elf32_executable_image f3:((elf32_interpreted_segment*segment_provenance)list*Nat_big_num.num*Nat_big_num.num)error= (if is_elf32_executable_file f3.elf32_file_header then let entr = (f3.elf32_file_header.elf32_entry) in let segs = (f3.elf32_file_interpreted_segments) in let mach = (f3.elf32_file_header.elf32_machine) in (match List.filter (fun sg -> Nat_big_num.equal sg.elf32_segment_type elf_pt_load) segs with | [] -> fail "get_elf32_executable_image: an executable ELF file must have at least one loadable segment" | load -> mapM (fun sg -> if Nat_big_num.equal sg.elf32_segment_memsz(Nat_big_num.of_int 0) then return [] else if Nat_big_num.equal sg.elf32_segment_memsz sg.elf32_segment_size then return [(sg, FromELF)] else if Nat_big_num.less sg.elf32_segment_size sg.elf32_segment_memsz then (* Cannot be negative due to check in constructing [segs]. *) let diff = (Nat_big_num.sub_nat sg.elf32_segment_memsz sg.elf32_segment_size) in let zeros1 = (Byte_sequence.zeros diff) in let addr = (Nat_big_num.add sg.elf32_segment_base sg.elf32_segment_size) in let align = (sg.elf32_segment_align) in let paddr = (sg.elf32_segment_paddr) in let seg = ({ elf32_segment_body = zeros1; elf32_segment_type = (sg.elf32_segment_type); elf32_segment_size = diff; elf32_segment_memsz = diff; elf32_segment_base = addr; elf32_segment_flags = (sg.elf32_segment_flags); elf32_segment_align = align; elf32_segment_paddr = paddr; elf32_segment_offset = (sg.elf32_segment_offset) }) in return [(sg, FromELF); (seg, AutoGenerated)] else fail "get_elf32_executable_image: invariant invalidated") load >>= (fun bs_base -> return (List.concat bs_base, Nat_big_num.of_string (Uint32.to_string entr), Nat_big_num.of_string (Uint32.to_string mach))) ) else fail "get_elf32_executable_image: not an ELF executable file") (** [get_elf64_executable_image f1] extracts an executable process image from an * 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:((elf64_interpreted_segment*segment_provenance)list*Nat_big_num.num*Nat_big_num.num)error= (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 let mach = (f3.elf64_file_header.elf64_machine) in (match List.filter (fun sg -> Nat_big_num.equal sg.elf64_segment_type elf_pt_load) segs with | [] -> fail "get_elf64_executable_image: an executable ELF file must have at least one loadable segment" | load -> mapM (fun sg -> if Nat_big_num.equal sg.elf64_segment_memsz(Nat_big_num.of_int 0) then return [] else if Nat_big_num.equal sg.elf64_segment_memsz sg.elf64_segment_size then return [(sg, FromELF)] else if Nat_big_num.less sg.elf64_segment_size sg.elf64_segment_memsz then (* Cannot be negative due to check in constructing [segs]. *) let diff = (Nat_big_num.sub_nat sg.elf64_segment_memsz sg.elf64_segment_size) in let zeros1 = (Byte_sequence.zeros diff) in let addr = (Nat_big_num.add sg.elf64_segment_base sg.elf64_segment_size) in let align = (sg.elf64_segment_align) in let paddr = (sg.elf64_segment_paddr) in let seg = ({ elf64_segment_body = zeros1; elf64_segment_type = (sg.elf64_segment_type); elf64_segment_size = diff; elf64_segment_memsz = diff; elf64_segment_base = addr; elf64_segment_flags = (sg.elf64_segment_flags); elf64_segment_align = align; elf64_segment_paddr = paddr; elf64_segment_offset = (sg.elf64_segment_offset) }) in return [(sg, FromELF); (seg, AutoGenerated)] else fail "get_elf64_executable_image: invariant invalidated") load >>= (fun bs_base -> return (List.concat bs_base, Ml_bindings.nat_big_num_of_uint64 entr, Nat_big_num.of_string (Uint32.to_string mach))) ) else fail "elf64_get_executable_image: not an executable ELF file") (** [global_symbol_init_info] records the name, type, size, address, chunk * of initialisation data (if relevant for that symbol), and binding, of every * global symbol in an ELF file. * Another PPCMemism. *) type global_symbol_init_info = (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * byte_sequence option * Nat_big_num.num)) list (** [get_elf32_file_global_symbol_init f1] extracts the global symbol init info * for ELF file [f1]. May fail. *) (*val get_elf32_file_global_symbol_init : elf32_file -> error global_symbol_init_info*) let get_elf32_file_global_symbol_init f3:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error= (if is_elf32_executable_file f3.elf32_file_header then let segs = (f3.elf32_file_interpreted_segments) in bytes_of_elf32_file f3 >>= (fun bs0 -> get_elf32_file_symbol_table f3 >>= (fun symtab -> get_elf32_file_symbol_string_table f3 >>= (fun strtab -> Elf_symbol_table.get_elf32_symbol_image_address symtab strtab >>= (fun strs -> let mapped = (mapM (fun (symbol, (typ, size2, addr, bind)) -> if Nat_big_num.equal typ Elf_symbol_table.stt_object then get_elf32_executable_image f3 >>= (fun (img2, entry, mach) -> let chunks1 = (List.filter (fun (chunk, _) -> Nat_big_num.greater_equal addr chunk.elf32_segment_base && (if Nat_big_num.greater size2(Nat_big_num.of_int 0) then Nat_big_num.less_equal (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf32_segment_base chunk.elf32_segment_size) (* We don't consider a zero-size symbol one byte after a section (i.e. addr = segment_base + segment_size) to be inside that section. *) else Nat_big_num.less (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf32_segment_base chunk.elf32_segment_size)) ) img2) in (match chunks1 with | [] -> fail "get_elf32_global_symbol_init: global variable not present in executable image" | [(x, _)] -> let rebase = (Nat_big_num.sub_nat addr x.elf32_segment_base) in Byte_sequence.offset_and_cut rebase size2 x.elf32_segment_body >>= (fun relevant -> return (symbol, (typ, size2, addr, Some relevant, bind))) | x::xs -> fail "get_elf32_global_symbol_init: invariant failed, global variable appears in multiple segments" )) else return (symbol, (typ, size2, addr, None, bind))) strs) in mapped)))) else fail "get_elf32_file_global_symbol_init: not an executable ELF file") (** [get_elf64_file_global_symbol_init f1] extracts the global symbol init info * for ELF file [f1]. May fail. *) (*val get_elf64_file_global_symbol_init : elf64_file -> error global_symbol_init_info*) let get_elf64_file_global_symbol_init f3:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error= (if is_elf64_executable_file f3.elf64_file_header then let segs = (f3.elf64_file_interpreted_segments) in bytes_of_elf64_file f3 >>= (fun bs0 -> get_elf64_file_symbol_table f3 >>= (fun symtab -> get_elf64_file_symbol_string_table f3 >>= (fun strtab -> Elf_symbol_table.get_elf64_symbol_image_address symtab strtab >>= (fun strs -> let mapped = (mapM (fun (symbol, (typ, size2, addr, bind)) -> if Nat_big_num.equal typ Elf_symbol_table.stt_object then get_elf64_executable_image f3 >>= (fun (img2, entry, mach) -> let chunks1 = (List.filter (fun (chunk, _) -> Nat_big_num.greater_equal addr chunk.elf64_segment_base && (if Nat_big_num.greater size2(Nat_big_num.of_int 0) then Nat_big_num.less_equal (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf64_segment_base chunk.elf64_segment_size) (* We don't consider a zero-size symbol one byte after a section (i.e. addr = segment_base + segment_size) to be inside that section. *) else Nat_big_num.less (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf64_segment_base chunk.elf64_segment_size)) ) img2) in (match chunks1 with | [] -> fail "get_elf64_global_symbol_init: global variable not present in executable image" | [(x, _)] -> let rebase = (Nat_big_num.sub_nat addr x.elf64_segment_base) in Byte_sequence.offset_and_cut rebase size2 x.elf64_segment_body >>= (fun relevant -> return (symbol, (typ, size2, addr, Some relevant, bind))) | x::xs -> fail "get_elf64_global_symbol_init: invariant failed, global variable appears in multiple segments" )) else return (symbol, (typ, size2, addr, None, bind))) strs) in mapped)))) else fail "get_elf64_global_symbol_init: not an executable ELF file") (** [string_of_elf32_file hdr_bdl pht_bdl sht_bdl f1] produces a string-based * representation of ELF file [f1] using ABI-specific print bundles [hdr_bdl], * [pht_bdl] and [sht_bdl]. *) (*val string_of_elf32_file : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_file -> string*) let string_of_elf32_file hdr_bdl pht_bdl sht_bdl f3:string= ((match get_elf32_file_section_header_string_table f3 with | Fail err -> unlines [ "\nError obtaining ELF section header string table:" ; err ] | Success strtab -> unlines [ "\n*Type elf32_file:" ; "**Header:" ; string_of_elf32_header hdr_bdl f3.elf32_file_header ; "**Program header table:" ; string_of_elf32_program_header_table pht_bdl f3.elf32_file_program_header_table ; "**Section header table:" ; string_of_elf32_section_header_table' sht_bdl strtab f3.elf32_file_section_header_table ; "**Bits and bobs (unused junk space):" ; string_of_list (instance_Show_Show_tup2_dict instance_Show_Show_Num_natural_dict instance_Show_Show_Byte_sequence_byte_sequence_dict) f3.elf32_file_bits_and_bobs ] )) (** [string_of_elf64_file hdr_bdl pht_bdl sht_bdl f1] produces a string-based * representation of ELF file [f1] using ABI-specific print bundles [hdr_bdl], * [pht_bdl] and [sht_bdl]. *) (*val string_of_elf64_file : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_file -> string*) let string_of_elf64_file hdr_bdl pht_bdl sht_bdl f3:string= ((match get_elf64_file_section_header_string_table f3 with | Fail err -> unlines [ "\nError obtaining ELF section header string table:" ; err ] | Success strtab -> unlines [ "\n*Type elf64_file:" ; "**Header:" ; string_of_elf64_header hdr_bdl f3.elf64_file_header ; "**Program header table:" ; string_of_elf64_program_header_table pht_bdl f3.elf64_file_program_header_table ; "**Section header table:" ; string_of_elf64_section_header_table' sht_bdl strtab f3.elf64_file_section_header_table ; "**Bits and bobs (unused junk space):" ; string_of_list (instance_Show_Show_tup2_dict instance_Show_Show_Num_natural_dict instance_Show_Show_Byte_sequence_byte_sequence_dict) f3.elf64_file_bits_and_bobs ] )) (** [flag_is_set flag v] checks whether flag [flag] is set in [v]. * TODO: move elsewhere. Check whether this is still being used. *) (*val flag_is_set : natural -> natural -> bool*) let flag_is_set flag v:bool= ( (* HACK: convert to elf64_xword first. Flags never live * in objects bigger than 64 bits. *)Uint64.logand (Uint64.of_string (Nat_big_num.to_string v)) (Uint64.of_string (Nat_big_num.to_string flag)) = (Uint64.of_string (Nat_big_num.to_string flag)))