diff options
Diffstat (limited to 'src/elf_model/elf_linking_file2.lem')
| -rw-r--r-- | src/elf_model/elf_linking_file2.lem | 150 |
1 files changed, 143 insertions, 7 deletions
diff --git a/src/elf_model/elf_linking_file2.lem b/src/elf_model/elf_linking_file2.lem index df69b5c9..4242f8d6 100644 --- a/src/elf_model/elf_linking_file2.lem +++ b/src/elf_model/elf_linking_file2.lem @@ -1,13 +1,149 @@ +open import Basic_classes +open import Bool +open import Maybe +open import Num + open import Bitstring +open import Error +open import Missing_pervasives +open import Show +open import String +open import Elf_file1 open import Elf_header open import Elf_section_header_table - -open import Maybe +open import Elf_types type elf32_linking_file2 = - <| elf32_executable_file2_header : elf32_header - ; elf32_executable_file2_program_header_table : maybe elf32_program_header_table - ; elf32_executable_file2_body : bitstring - ; elf32_executable_file2_section_header_table : elf32_section_header_table - |>
\ No newline at end of file + <| elf32_linking_file2_header : elf32_header + ; elf32_linking_file2_body : bitstring + ; elf32_linking_file2_section_header_table : elf32_section_header_table + |> + +class (HasElf32LinkingFile2 'a) + val get_elf32_linking_file2 : 'a -> elf32_linking_file2 +end + +instance (HasElf32LinkingFile2 elf32_linking_file2) + let get_elf32_linking_file2 f2 = f2 +end + +instance (HasElf32File1 elf32_linking_file2) + let get_elf32_file1 f2 = + <| elf32_file1_header = f2.elf32_linking_file2_header; + elf32_file1_body = f2.elf32_linking_file2_body |> +end + +instance (HasElf32Header elf32_linking_file2) + let get_elf32_header f2 = f2.elf32_linking_file2_header +end + +instance (HasElf32SectionHeaderTable elf32_linking_file2) + let get_elf32_section_header_table f2 = Just f2.elf32_linking_file2_section_header_table +end + +type elf64_linking_file2 = + <| elf64_linking_file2_header : elf64_header + ; elf64_linking_file2_body : bitstring + ; elf64_linking_file2_section_header_table : elf64_section_header_table + |> + +class (HasElf64LinkingFile2 'a) + val get_elf64_linking_file2 : 'a -> elf64_linking_file2 +end + +instance (HasElf64LinkingFile2 elf64_linking_file2) + let get_elf64_linking_file2 f2 = f2 +end + +instance (HasElf64File1 elf64_linking_file2) + let get_elf64_file1 f2 = + <| elf64_file1_header = f2.elf64_linking_file2_header; + elf64_file1_body = f2.elf64_linking_file2_body |> +end + +instance (HasElf64Header elf64_linking_file2) + let get_elf64_header f2 = f2.elf64_linking_file2_header +end + +instance (HasElf64SectionHeaderTable elf64_linking_file2) + let get_elf64_section_header_table f2 = Just f2.elf64_linking_file2_section_header_table +end + +val refine_elf32_file1 : elf32_file1 -> error elf32_linking_file2 +let refine_elf32_file1 f1 = + if not (is_linkable_elf32_file1 f1) then + fail "refine_elf32_file1: not a linkable file" + else + let hdr = f1.elf32_file1_header in + let endian = get_elf32_header_endianness hdr in + let bs1 = f1.elf32_file1_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 + fail "refine_elf32_file1: section header table not present" + 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_linking_file2_header = hdr; + elf32_linking_file2_body = bs1; + elf32_linking_file2_section_header_table = sht |> + +val read_elf32_linking_file2 : bitstring -> error elf32_linking_file2 +let read_elf32_linking_file2 bs0 = + read_elf32_file1 bs0 >>= refine_elf32_file1 + +val string_of_elf32_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf32_linking_file2 -> string +let string_of_elf32_linking_file2 hdr_bdl sht_bdl f2 = + unlines [ + "\n*Type elf32_linking_file2:" + ; "**Header:" + ; string_of_elf32_header hdr_bdl f2.elf32_linking_file2_header + ; "**Program header table:" + ; string_of_elf32_section_header_table sht_bdl f2.elf32_linking_file2_section_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf32_linking_file2_body) + ] + +val refine_elf64_file1 : elf64_file1 -> error elf64_linking_file2 +let refine_elf64_file1 f1 = + if not (is_linkable_elf64_file1 f1) then + fail "refine_elf64_file1: not a linkable file" + else + let hdr = f1.elf64_file1_header in + let endian = get_elf64_header_endianness hdr in + let bs1 = f1.elf64_file1_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 + fail "refine_elf64_file1: section header table not present" + 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_linking_file2_header = hdr; + elf64_linking_file2_body = bs1; + elf64_linking_file2_section_header_table = sht |> + +val read_elf64_linking_file2 : bitstring -> error elf64_linking_file2 +let read_elf64_linking_file2 bs0 = + read_elf64_file1 bs0 >>= refine_elf64_file1 + +val string_of_elf64_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf64_linking_file2 -> string +let string_of_elf64_linking_file2 hdr_bdl sht_bdl f2 = + unlines [ + "\n*Type elf64_linking_file2:" + ; "**Header:" + ; string_of_elf64_header hdr_bdl f2.elf64_linking_file2_header + ; "**Program header table:" + ; string_of_elf64_section_header_table sht_bdl f2.elf64_linking_file2_section_header_table + ; "**Body:" + ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf64_linking_file2_body) + ]
\ No newline at end of file |