diff options
Diffstat (limited to 'src/elf_model/elf_executable_file3.lem')
| -rw-r--r-- | src/elf_model/elf_executable_file3.lem | 505 |
1 files changed, 0 insertions, 505 deletions
diff --git a/src/elf_model/elf_executable_file3.lem b/src/elf_model/elf_executable_file3.lem deleted file mode 100644 index 56b2b611..00000000 --- a/src/elf_model/elf_executable_file3.lem +++ /dev/null @@ -1,505 +0,0 @@ -open import Basic_classes -open import Num -open import Maybe -open import String - -open import Elf_executable_file2 -open import Elf_header -open import Elf_interpreted_segment -open import Elf_types -open import Elf_section_header_table -open import Elf_symbol_table -open import Elf_program_header_table -open import String_table - -open import Bitstring -open import Error -open import Missing_pervasives -open import Show - -(** Type [elf32_executable_file3] represents the lazy unfolding of a 32-bit ELF - * file where the header, program header table and optional section header table - * have been filled in, with all other data being left uninterpreted. - *) -type elf32_executable_file3 = - <| elf32_executable_file3_header : elf32_header (** The ELF header (mandatory) *) - ; elf32_executable_file3_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) - ; elf32_executable_file3_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *) - ; elf32_executable_file3_body : bitstring (** Uninterpreted body *) - |> - -class (HasElf32ExecutableFile3 'a) - val get_elf32_executable_file3 : 'a -> elf32_executable_file3 -end - -instance (HasElf32ExecutableFile3 elf32_executable_file3) - let get_elf32_executable_file3 f3 = f3 -end - -instance (HasElf32ExecutableFile2 elf32_executable_file3) - let get_elf32_executable_file2 f3 = - <| elf32_executable_file2_header = f3.elf32_executable_file3_header; - elf32_executable_file2_program_header_table = f3.elf32_executable_file3_program_header_table; - elf32_executable_file2_body = f3.elf32_executable_file3_body |> -end - -instance (HasElf32Header elf32_executable_file3) - let get_elf32_header f3 = f3.elf32_executable_file3_header -end - -instance (HasElf32ProgramHeaderTable elf32_executable_file3) - let get_elf32_program_header_table f3 = - Just (f3.elf32_executable_file3_program_header_table) -end - -instance (HasElf32SectionHeaderTable elf32_executable_file3) - let get_elf32_section_header_table f3 = - f3.elf32_executable_file3_section_header_table -end - -(** Type [elf64_executable_file3] represents the lazy unfolding of a 64-bit ELF - * file where the header, program header table and optional section header table - * have been filled in, with all other data being left uninterpreted. - *) -type elf64_executable_file3 = - <| elf64_executable_file3_header : elf64_header (** The ELF header (mandatory) *) - ; elf64_executable_file3_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) - ; elf64_executable_file3_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *) - ; elf64_executable_file3_body : bitstring (** Uninterpreted body *) - |> - -class (HasElf64ExecutableFile3 'a) - val get_elf64_executable_file3 : 'a -> elf64_executable_file3 -end - -instance (HasElf64ExecutableFile3 elf64_executable_file3) - let get_elf64_executable_file3 f3 = f3 -end - -instance (HasElf64ExecutableFile2 elf64_executable_file3) - let get_elf64_executable_file2 f3 = - <| elf64_executable_file2_header = f3.elf64_executable_file3_header; - elf64_executable_file2_program_header_table = f3.elf64_executable_file3_program_header_table; - elf64_executable_file2_body = f3.elf64_executable_file3_body |> -end - -instance (HasElf64Header elf64_executable_file3) - let get_elf64_header f3 = f3.elf64_executable_file3_header -end - -instance (HasElf64ProgramHeaderTable elf64_executable_file3) - let get_elf64_program_header_table f3 = - Just (f3.elf64_executable_file3_program_header_table) -end - -instance (HasElf64SectionHeaderTable elf64_executable_file3) - let get_elf64_section_header_table f3 = - f3.elf64_executable_file3_section_header_table -end - -(** [refine_elf32_executable_file2 f2] refines an elf32_executable_file2 [f2] into - * an elf32_executable_file3 by adding the optional section header table. - *) -val refine_elf32_executable_file2 : elf32_executable_file2 -> error elf32_executable_file3 -let refine_elf32_executable_file2 f2 = - let hdr = f2.elf32_executable_file2_header in - let pht = f2.elf32_executable_file2_program_header_table in - let endian = get_elf32_header_endianness hdr in - let bs1 = f2.elf32_executable_file2_body in - let sentries = nat_of_elf32_half hdr.elf32_shnum in - let sentry_size = nat_of_elf32_half hdr.elf32_shentsize * 8 in - let ssize = sentries * sentry_size in - if ssize = 0 then - return <| elf32_executable_file3_header = hdr; - elf32_executable_file3_program_header_table = pht; - elf32_executable_file3_section_header_table = Nothing; - elf32_executable_file3_body = bs1 |> - else - let soffset = nat_of_elf32_off hdr.elf32_shoff * 8 in - let (_, scut) = partition soffset bs1 in - let (sexact, _) = partition ssize scut in - (* Bitstring irrelevant below as exact size used... *) - read_elf32_section_header_table ssize endian sexact >>= fun (sht, _) -> - return <| elf32_executable_file3_header = hdr; - elf32_executable_file3_program_header_table = pht; - elf32_executable_file3_section_header_table = Just sht; - elf32_executable_file3_body = bs1 |> - -(** [refine_elf64_executable_file2 f2] refines an elf64_executable_file2 [f2] into - * an elf64_executable_file3 by adding the optional section header table. - *) -val refine_elf64_executable_file2 : elf64_executable_file2 -> error elf64_executable_file3 -let refine_elf64_executable_file2 f2 = - let hdr = f2.elf64_executable_file2_header in - let pht = f2.elf64_executable_file2_program_header_table in - let endian = get_elf64_header_endianness hdr in - let bs1 = f2.elf64_executable_file2_body in - let sentries = nat_of_elf64_half hdr.elf64_shnum in - let sentry_size = nat_of_elf64_half hdr.elf64_shentsize * 8 in - let ssize = sentries * sentry_size in - if ssize = 0 then - return <| elf64_executable_file3_header = hdr; - elf64_executable_file3_program_header_table = pht; - elf64_executable_file3_section_header_table = Nothing; - elf64_executable_file3_body = bs1 |> - else - let soffset = nat_of_elf64_off hdr.elf64_shoff * 8 in - let (_, scut) = partition soffset bs1 in - let (sexact, _) = partition ssize scut in - (* Bitstring irrelevant below as exact size used... *) - read_elf64_section_header_table ssize endian sexact >>= fun (sht, _) -> - return <| elf64_executable_file3_header = hdr; - elf64_executable_file3_program_header_table = pht; - elf64_executable_file3_section_header_table = Just sht; - elf64_executable_file3_body = bs1 |> - -(** [read_elf32_executable_file3 bs0] reads an elf32_executable_file3 from - * bitstring [bs0]. - *) -val read_elf32_executable_file3 : bitstring -> error elf32_executable_file3 -let read_elf32_executable_file3 bs0 = - read_elf32_executable_file2 bs0 >>= refine_elf32_executable_file2 - -(** [read_elf64_executable_file3 bs0] reads an elf64_executable_file3 from - * bitstring [bs0]. - *) -val read_elf64_executable_file3 : bitstring -> error elf64_executable_file3 -let read_elf64_executable_file3 bs0 = - read_elf64_executable_file2 bs0 >>= refine_elf64_executable_file2 - -(** string_of_elf32_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3] - * creates a string representation of [f3]. - *) -val string_of_elf32_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file3 -> string -let string_of_elf32_executable_file3 hdr_bdl pht_bdl sht_bdl f3 = - let sht = - match f3.elf32_executable_file3_section_header_table with - | Nothing -> "\tNo section header table present" - | Just sht -> string_of_elf32_section_header_table sht_bdl sht - end - in - unlines [ - "\n*Type elf32_executable_file3:" - ; "**Header:" - ; string_of_elf32_header hdr_bdl f3.elf32_executable_file3_header - ; "**Program header table:" - ; string_of_elf32_program_header_table pht_bdl f3.elf32_executable_file3_program_header_table - ; "**Section header table:" - ; sht - ; "**Body:" - ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf32_executable_file3_body) - ] - -(** string_of_elf64_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3] - * creates a string representation of [f3]. - *) -val string_of_elf64_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file3 -> string -let string_of_elf64_executable_file3 hdr_bdl pht_bdl sht_bdl f3 = - let sht = - match f3.elf64_executable_file3_section_header_table with - | Nothing -> "\tNo section header table present" - | Just sht -> string_of_elf64_section_header_table sht_bdl sht - end - in - unlines [ - "\n*Type elf64_executable_file3:" - ; "**Header:" - ; string_of_elf64_header hdr_bdl f3.elf64_executable_file3_header - ; "**Program header table:" - ; string_of_elf64_program_header_table pht_bdl f3.elf64_executable_file3_program_header_table - ; "**Section header table:" - ; sht - ; "**Body:" - ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_executable_file3_body) - ] - -val get_elf32_section_header_string_table : elf32_executable_file3 -> error string_table -let get_elf32_section_header_string_table f3 = - let bs0 = f3.elf32_executable_file3_body in - match f3.elf32_executable_file3_section_header_table with - | Nothing -> return String_table.empty - | Just sht -> - let idx = nat_of_elf32_half f3.elf32_executable_file3_header.elf32_shstrndx in - match List.index sht idx with - | Nothing -> fail "get_elf32_string_table: invalid offset into section header table" - | Just sect -> - let offset = nat_of_elf32_off sect.elf32_sh_offset * 8 in - let size = nat_of_elf32_word sect.elf32_sh_size * 8 in - let (_, cut) = Bitstring.partition offset bs0 in - let (rel, _) = Bitstring.partition size cut in - let strings = Bitstring.string_of_bitstring rel in - return (String_table.mk_string_table strings Missing_pervasives.null_char) - end - end - -val get_elf64_section_header_string_table : elf64_executable_file3 -> error string_table -let get_elf64_section_header_string_table f3 = - let bs0 = f3.elf64_executable_file3_body in - match f3.elf64_executable_file3_section_header_table with - | Nothing -> return String_table.empty - | Just sht -> - let idx = nat_of_elf64_half f3.elf64_executable_file3_header.elf64_shstrndx in - match List.index sht idx with - | Nothing -> fail "get_elf64_string_table: invalid offset into section header table" - | Just sect -> - let offset = nat_of_elf64_off sect.elf64_sh_offset * 8 in - let size = nat_of_elf64_xword sect.elf64_sh_size * 8 in - let (_, cut) = Bitstring.partition offset bs0 in - let (rel, _) = Bitstring.partition size cut in - let strings = Bitstring.string_of_bitstring rel in - return (String_table.mk_string_table strings Missing_pervasives.null_char) - end - end - -val get_elf32_symbol_string_table : elf32_executable_file3 -> error string_table -let get_elf32_symbol_string_table f3 = - let bs0 = f3.elf32_executable_file3_body in - let hdr = f3.elf32_executable_file3_header in - match f3.elf32_executable_file3_section_header_table with - | Nothing -> return String_table.empty - | Just sht -> - let strtabs = Missing_pervasives.mapMaybei (fun index sect -> - if nat_of_elf32_word sect.elf32_sh_type = sht_strtab then - if index = nat_of_elf32_half hdr.elf32_shstrndx then - Nothing - else - Just sect - else - Nothing) sht - in - let strings = List.map (fun sect -> - let offset = nat_of_elf32_off sect.elf32_sh_offset * 8 in - let size = nat_of_elf32_word sect.elf32_sh_size * 8 in - let bs1 = Bitstring.offset_and_cut offset size bs0 in - let strings = Bitstring.string_of_bitstring bs1 in - String_table.mk_string_table strings Missing_pervasives.null_char) strtabs - in - String_table.concat strings - end - -val get_elf64_symbol_string_table : elf64_executable_file3 -> error string_table -let get_elf64_symbol_string_table f3 = - let bs0 = f3.elf64_executable_file3_body in - let hdr = f3.elf64_executable_file3_header in - match f3.elf64_executable_file3_section_header_table with - | Nothing -> return String_table.empty - | Just sht -> - let strtabs = Missing_pervasives.mapMaybei (fun index sect -> - if nat_of_elf64_word sect.elf64_sh_type = sht_strtab then - if index = nat_of_elf64_half hdr.elf64_shstrndx then - Nothing - else - Just sect - else - Nothing) sht - in - let strings = List.map (fun sect -> - let offset = nat_of_elf64_off sect.elf64_sh_offset * 8 in - let size = nat_of_elf64_xword sect.elf64_sh_size * 8 in - let bs1 = Bitstring.offset_and_cut offset size bs0 in - let strings = Bitstring.string_of_bitstring bs1 in - String_table.mk_string_table strings Missing_pervasives.null_char) strtabs - in - String_table.concat strings - end - -val get_elf32_interpreted_segments : elf32_executable_file3 -> error (list elf32_interpreted_segment) -let get_elf32_interpreted_segments f3 = - let pht = f3.elf32_executable_file3_program_header_table in - let bdy = f3.elf32_executable_file3_body in - let segs = - List.map (fun ph -> - let offset = nat_of_elf32_off ph.elf32_p_offset * 8 in - let size = nat_of_elf32_word ph.elf32_p_filesz * 8 in - let relevant = Bitstring.offset_and_cut offset size bdy in - let vaddr = nat_of_elf32_addr ph.elf32_p_vaddr in - let memsz = nat_of_elf32_word ph.elf32_p_memsz * 8 in - let typ = nat_of_elf32_word ph.elf32_p_type in - let flags = elf32_interpret_program_header_flags ph.elf32_p_flags in - <| elf32_segment_body = relevant; elf32_segment_type = typ; - elf32_segment_size = size; elf32_segment_memsz = memsz; - elf32_segment_base = vaddr; elf32_segment_flags = flags |> - ) pht - in - mapM (fun sg -> - if sg.elf32_segment_memsz < sg.elf32_segment_size then - fail "get_elf32_interpreted_segments: memory size of segment cannot be less than file size" - else - return sg) segs - -val get_elf64_interpreted_segments : elf64_executable_file3 -> error (list elf64_interpreted_segment) -let get_elf64_interpreted_segments f3 = - let pht = f3.elf64_executable_file3_program_header_table in - let bdy = f3.elf64_executable_file3_body in - let segs = - List.map (fun ph -> - let offset = nat_of_elf64_off ph.elf64_p_offset * 8 in - let size = nat_of_elf64_xword ph.elf64_p_filesz * 8 in - let relevant = Bitstring.offset_and_cut offset size bdy in - let vaddr = nat_of_elf64_addr ph.elf64_p_vaddr in - let memsz = nat_of_elf64_xword ph.elf64_p_memsz * 8 in - let typ = nat_of_elf64_word ph.elf64_p_type in - let flags = elf64_interpret_program_header_flags ph.elf64_p_flags in - <| elf64_segment_body = relevant; elf64_segment_type = typ; - elf64_segment_size = size; elf64_segment_memsz = memsz; - elf64_segment_base = vaddr; elf64_segment_flags = flags |> - ) pht - in - mapM (fun sg -> - if sg.elf64_segment_memsz < sg.elf64_segment_size then - fail "get_elf64_interpreted_segments: memory size of segment cannot be less than file size" - else - return sg) segs - -type executable_process_image = - list (bitstring * nat) * nat - -val get_elf32_executable_image : elf32_executable_file3 -> error executable_process_image -let get_elf32_executable_image f3 = - let entr = f3.elf32_executable_file3_header.elf32_entry in - get_elf32_interpreted_segments f3 >>= fun segs -> - match List.filter (fun sg -> 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 sg.elf32_segment_memsz = 0 then - return [] - else if sg.elf32_segment_memsz = sg.elf32_segment_size then - return [(sg.elf32_segment_body, sg.elf32_segment_base)] - else if sg.elf32_segment_size < sg.elf32_segment_memsz then - (* Cannot be negative due to check in constructing [segs]. *) - let diff = sg.elf32_segment_memsz - sg.elf32_segment_size in - let zeros = Bitstring.zeros diff in - let addr = sg.elf32_segment_base + sg.elf32_segment_size in - return [(sg.elf32_segment_body, sg.elf32_segment_base); (zeros, addr)] - else - fail "get_elf32_executable_image: invariant invalidated") load >>= fun bs_base -> - return (List.concat bs_base, nat_of_elf32_addr entr) - end - -val get_elf64_executable_image : elf64_executable_file3 -> error executable_process_image -let get_elf64_executable_image f3 = - let entr = f3.elf64_executable_file3_header.elf64_entry in - get_elf64_interpreted_segments f3 >>= fun segs -> - match List.filter (fun sg -> 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 sg.elf64_segment_memsz = 0 then - return [] - else if sg.elf64_segment_memsz = sg.elf64_segment_size then - return [(sg.elf64_segment_body, sg.elf64_segment_base)] - else if sg.elf64_segment_size < sg.elf64_segment_memsz then - (* Cannot be negative due to check in constructing [segs]. *) - let diff = sg.elf64_segment_memsz - sg.elf64_segment_size in - let zeros = Bitstring.zeros diff in - let addr = sg.elf64_segment_base + sg.elf64_segment_size in - return [(sg.elf64_segment_body, sg.elf64_segment_base); (zeros, addr)] - else - fail "get_elf64_executable_image: invariant invalidated") load >>= fun bs_base -> - return (List.concat bs_base, nat_of_elf64_addr entr) - end - -val get_elf32_symbol_table : elf32_executable_file3 -> error elf32_symbol_table -let get_elf32_symbol_table f3 = - let bs0 = f3.elf32_executable_file3_body in - let hdr = f3.elf32_executable_file3_header in - let endian = get_elf32_header_endianness hdr in - match f3.elf32_executable_file3_section_header_table with - | Nothing -> return [] - | Just sects -> - let symtabs = List.filter (fun sect -> - nat_of_elf32_word sect.elf32_sh_type = sht_symtab) sects - in - if List.length symtabs = 0 then - return [] - else if List.length symtabs = 1 then - match List.index symtabs 0 with - | Nothing -> fail "get_elf32_symbol_table: invariant failed" - | Just symtab -> - let offset = nat_of_elf32_off symtab.elf32_sh_offset * 8 in - let size = nat_of_elf32_word symtab.elf32_sh_size * 8 in - let relevant = Bitstring.offset_and_cut offset size bs0 in - read_elf32_symbol_table endian relevant - end - else - fail "get_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB" - end - -val get_elf64_symbol_table : elf64_executable_file3 -> error elf64_symbol_table -let get_elf64_symbol_table f3 = - let bs0 = f3.elf64_executable_file3_body in - let hdr = f3.elf64_executable_file3_header in - let endian = get_elf64_header_endianness hdr in - match f3.elf64_executable_file3_section_header_table with - | Nothing -> return [] - | Just sects -> - let symtabs = List.filter (fun sect -> - nat_of_elf64_word sect.elf64_sh_type = sht_symtab) sects - in - if List.length symtabs = 0 then - return [] - else if List.length symtabs = 1 then - match List.index symtabs 0 with - | Nothing -> fail "get_elf64_symbol_table: invariant failed" - | Just symtab -> - let offset = nat_of_elf64_off symtab.elf64_sh_offset * 8 in - let size = nat_of_elf64_xword symtab.elf64_sh_size * 8 in - let relevant = Bitstring.offset_and_cut offset size bs0 in - read_elf64_symbol_table endian relevant - end - else - fail "get_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB" - end - -val get_elf32_dynamic_symbol_table : elf32_executable_file3 -> error elf32_symbol_table -let get_elf32_dynamic_symbol_table f3 = - let bs0 = f3.elf32_executable_file3_body in - let hdr = f3.elf32_executable_file3_header in - let endian = get_elf32_header_endianness hdr in - match f3.elf32_executable_file3_section_header_table with - | Nothing -> return [] - | Just sects -> - let symtabs = List.filter (fun sect -> - nat_of_elf32_word sect.elf32_sh_type = sht_dynsym) sects - in - if List.length symtabs = 0 then - return [] - else if List.length symtabs = 1 then - match List.index symtabs 0 with - | Nothing -> fail "get_elf32_symbol_table: invariant failed" - | Just symtab -> - let offset = nat_of_elf32_off symtab.elf32_sh_offset * 8 in - let size = nat_of_elf32_word symtab.elf32_sh_size * 8 in - let relevant = Bitstring.offset_and_cut offset size bs0 in - read_elf32_symbol_table endian relevant - end - else - fail "get_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" - end - -val get_elf64_dynamic_symbol_table : elf64_executable_file3 -> error elf64_symbol_table -let get_elf64_dynamic_symbol_table f3 = - let bs0 = f3.elf64_executable_file3_body in - let hdr = f3.elf64_executable_file3_header in - let endian = get_elf64_header_endianness hdr in - match f3.elf64_executable_file3_section_header_table with - | Nothing -> return [] - | Just sects -> - let symtabs = List.filter (fun sect -> - nat_of_elf64_word sect.elf64_sh_type = sht_dynsym) sects - in - if List.length symtabs = 0 then - return [] - else if List.length symtabs = 1 then - match List.index symtabs 0 with - | Nothing -> fail "get_elf64_symbol_table: invariant failed" - | Just symtab -> - let offset = nat_of_elf64_off symtab.elf64_sh_offset * 8 in - let size = nat_of_elf64_xword symtab.elf64_sh_size * 8 in - let relevant = Bitstring.offset_and_cut offset size bs0 in - read_elf64_symbol_table endian relevant - end - else - fail "get_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM" - end
\ No newline at end of file |