diff options
Diffstat (limited to 'src/elf_model/elf_executable_file4.lem')
| -rw-r--r-- | src/elf_model/elf_executable_file4.lem | 249 |
1 files changed, 249 insertions, 0 deletions
diff --git a/src/elf_model/elf_executable_file4.lem b/src/elf_model/elf_executable_file4.lem new file mode 100644 index 00000000..c6a6b345 --- /dev/null +++ b/src/elf_model/elf_executable_file4.lem @@ -0,0 +1,249 @@ +open import Maybe +open import Num + +open import Elf_executable_file3 +open import Elf_header +open import Elf_program_header_table +open import Elf_section_header_table +open import Elf_types +open import String_table + +open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String + +(** Type [elf32_executable_file4] 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, along with the section header string table, with all + * other data being left uninterpreted. + *) +type elf32_executable_file4 = + <| elf32_executable_file4_header : elf32_header (** The ELF header (mandatory) *) + ; elf32_executable_file4_program_header_table : elf32_program_header_table (** The program header table (mandatory) *) + ; elf32_executable_file4_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *) + ; elf32_executable_file4_section_header_string_table : string_table + ; elf32_executable_file4_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf32ExecutableFile4 'a) + val get_elf32_executable_file4 : 'a -> elf32_executable_file4 +end + +instance (HasElf32ExecutableFile4 elf32_executable_file4) + let get_elf32_executable_file4 f4 = f4 +end + +instance (HasElf32ExecutableFile3 elf32_executable_file4) + let get_elf32_executable_file3 f4 = + <| elf32_executable_file3_header = f4.elf32_executable_file4_header; + elf32_executable_file3_program_header_table = f4.elf32_executable_file4_program_header_table; + elf32_executable_file3_section_header_table = f4.elf32_executable_file4_section_header_table; + elf32_executable_file3_body = f4.elf32_executable_file4_body |> +end + +instance (HasElf32Header elf32_executable_file4) + let get_elf32_header f4 = f4.elf32_executable_file4_header +end + +instance (HasElf32ProgramHeaderTable elf32_executable_file4) + let get_elf32_program_header_table f4 = + Just (f4.elf32_executable_file4_program_header_table) +end + +instance (HasElf32SectionHeaderTable elf32_executable_file4) + let get_elf32_section_header_table f4 = + f4.elf32_executable_file4_section_header_table +end + +instance (HasElf32SectionHeaderStringTable elf32_executable_file4) + let get_elf32_section_header_string_table f4 = + f4.elf32_executable_file4_section_header_string_table +end + +(** Type [elf64_executable_file4] 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, along with the section header string table, with all + * other data being left uninterpreted. + *) +type elf64_executable_file4 = + <| elf64_executable_file4_header : elf64_header (** The ELF header (mandatory) *) + ; elf64_executable_file4_program_header_table : elf64_program_header_table (** The program header table (mandatory) *) + ; elf64_executable_file4_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *) + ; elf64_executable_file4_section_header_string_table : string_table + ; elf64_executable_file4_body : bitstring (** Uninterpreted body *) + |> + +class (HasElf64ExecutableFile4 'a) + val get_elf64_executable_file4 : 'a -> elf64_executable_file4 +end + +instance (HasElf64ExecutableFile4 elf64_executable_file4) + let get_elf64_executable_file4 f4 = f4 +end + +instance (HasElf64ExecutableFile3 elf64_executable_file4) + let get_elf64_executable_file3 f4 = + <| elf64_executable_file3_header = f4.elf64_executable_file4_header; + elf64_executable_file3_program_header_table = f4.elf64_executable_file4_program_header_table; + elf64_executable_file3_section_header_table = f4.elf64_executable_file4_section_header_table; + elf64_executable_file3_body = f4.elf64_executable_file4_body |> +end + +instance (HasElf64Header elf64_executable_file4) + let get_elf64_header f4 = f4.elf64_executable_file4_header +end + +instance (HasElf64ProgramHeaderTable elf64_executable_file4) + let get_elf64_program_header_table f4 = + Just (f4.elf64_executable_file4_program_header_table) +end + +instance (HasElf64SectionHeaderTable elf64_executable_file4) + let get_elf64_section_header_table f4 = + f4.elf64_executable_file4_section_header_table +end + +instance (HasElf64SectionHeaderStringTable elf64_executable_file4) + let get_elf64_section_header_string_table f4 = + f4.elf64_executable_file4_section_header_string_table +end + +(** [refine_elf32_executable_file3 f3] refines an elf32_executable_file3 [f3], adding the + * section header string table, to obtain an elf32_executable_file4. May fail if + * the offset stored in the ELF header indicating where the string table is stored is + * invalid. + *) +val refine_elf32_executable_file3 : elf32_executable_file3 -> error elf32_executable_file4 +let refine_elf32_executable_file3 f3 = + let hdr = f3.elf32_executable_file3_header in + let pht = f3.elf32_executable_file3_program_header_table in + let sht = f3.elf32_executable_file3_section_header_table in + let bs0 = f3.elf32_executable_file3_body in + match sht with + | Nothing -> + return <| elf32_executable_file4_header = hdr; + elf32_executable_file4_program_header_table = pht; + elf32_executable_file4_section_header_table = Nothing; + elf32_executable_file4_section_header_string_table = String_table.empty; + elf32_executable_file4_body = bs0 |> + | Just sht -> + let idx = nat_of_elf32_half hdr.elf32_shstrndx in + let sect = List.index sht idx in + match sect with + | Nothing -> Fail "refine_elf32_executable_file3: 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 <| elf32_executable_file4_header = hdr; + elf32_executable_file4_program_header_table = pht; + elf32_executable_file4_section_header_table = Just sht; + elf32_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char; + elf32_executable_file4_body = bs0 |> + end + end + +(** [refine_elf64_executable_file3 f3] refines an elf64_executable_file3 [f3], adding the + * section header string table, to obtain an elf64_executable_file4. May fail if + * the offset stored in the ELF header indicating where the string table is stored is + * invalid. + *) +val refine_elf64_executable_file3 : elf64_executable_file3 -> error elf64_executable_file4 +let refine_elf64_executable_file3 f3 = + let hdr = f3.elf64_executable_file3_header in + let pht = f3.elf64_executable_file3_program_header_table in + let sht = f3.elf64_executable_file3_section_header_table in + let bs0 = f3.elf64_executable_file3_body in + match sht with + | Nothing -> + return <| elf64_executable_file4_header = hdr; + elf64_executable_file4_program_header_table = pht; + elf64_executable_file4_section_header_table = Nothing; + elf64_executable_file4_section_header_string_table = String_table.empty; + elf64_executable_file4_body = bs0 |> + | Just sht -> + let idx = nat_of_elf64_half hdr.elf64_shstrndx in + let sect = List.index sht idx in + match sect with + | Nothing -> fail "refine_elf32_executable_file3: 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 <| elf64_executable_file4_header = hdr; + elf64_executable_file4_program_header_table = pht; + elf64_executable_file4_section_header_table = Just sht; + elf64_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char; + elf64_executable_file4_body = bs0 |> + end + end + +(** [read_elf32_executable_file4 bs0] reads an [elf32_executable_file4] in from + * bitstring [bs0]. + *) +val read_elf32_executable_file4 : bitstring -> error elf32_executable_file4 +let read_elf32_executable_file4 bs0 = + read_elf32_executable_file3 bs0 >>= refine_elf32_executable_file3 + +(** [read_elf64_executable_file4 bs0] reads an [elf64_executable_file4] in from + * bitstring [bs0]. + *) +val read_elf64_executable_file4 : bitstring -> error elf64_executable_file4 +let read_elf64_executable_file4 bs0 = + read_elf64_executable_file3 bs0 >>= refine_elf64_executable_file3 + +(** [string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string + * based representation of elf32_executable_file4 [f4]. + *) +val string_of_elf32_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file4 -> string +let string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4 = + let sht = + match f4.elf32_executable_file4_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf32_section_header_table' sht_bdl f4.elf32_executable_file4_section_header_string_table sht + end + in + unlines [ + "\n*Type elf32_executable_file4" + ; "**Header" + ; string_of_elf32_header hdr_bdl f4.elf32_executable_file4_header + ; "**Program header table:" + ; string_of_elf32_program_header_table pht_bdl f4.elf32_executable_file4_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf32_executable_file4_section_header_string_table)) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf32_executable_file4_body) + ] + +(** [string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string + * based representation of elf64_executable_file4 [f4]. + *) +val string_of_elf64_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file4 -> string +let string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4 = + let sht = + match f4.elf64_executable_file4_section_header_table with + | Nothing -> "\tNo section header table present" + | Just sht -> string_of_elf64_section_header_table' sht_bdl f4.elf64_executable_file4_section_header_string_table sht + end + in + unlines [ + "\n*Type elf64_executable_file4" + ; "**Header" + ; string_of_elf64_header hdr_bdl f4.elf64_executable_file4_header + ; "**Program header table:" + ; string_of_elf64_program_header_table pht_bdl f4.elf64_executable_file4_program_header_table + ; "**Section header table:" + ; sht + ; "**Section header string table:" + ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf64_executable_file4_section_header_string_table)) + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf64_executable_file4_body) + ]
\ No newline at end of file |