diff options
Diffstat (limited to 'src/elf_model/sail_interface.lem')
| -rw-r--r-- | src/elf_model/sail_interface.lem | 88 |
1 files changed, 82 insertions, 6 deletions
diff --git a/src/elf_model/sail_interface.lem b/src/elf_model/sail_interface.lem index 7bfad805..6c474fa7 100644 --- a/src/elf_model/sail_interface.lem +++ b/src/elf_model/sail_interface.lem @@ -12,10 +12,14 @@ open import Missing_pervasives open import Show open import Elf_header -open import Elf_executable_file5 +open import Elf_executable_file3 open import Elf_types -val populate : string -> list (bitstring * nat) * nat +type elf_class + = ELF_Class_32 + | ELF_Class_64 + +val populate : string -> executable_process_image * elf_class let populate fname = let res = (* Acquire the data from the file... *) @@ -29,11 +33,13 @@ let populate fname = * what we have read... *) if nat_of_unsigned_char c = Elf_header.elf_class_32 then - Elf_executable_file5.read_elf32_executable_file5 bs0 >>= - Elf_executable_file5.elf32_construct_image + Elf_executable_file3.read_elf32_executable_file3 bs0 >>= fun ef5 -> + Elf_executable_file3.get_elf32_executable_image ef5 >>= fun (chunks, entry) -> + return ((chunks, entry), ELF_Class_32) else if nat_of_unsigned_char c = Elf_header.elf_class_64 then - Elf_executable_file5.read_elf64_executable_file5 bs0 >>= - Elf_executable_file5.elf64_construct_image + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun ef5 -> + Elf_executable_file3.get_elf64_executable_image ef5 >>= fun (chunks, entry) -> + return ((chunks, entry), ELF_Class_64) else fail "populate: ELF class unrecognised" end @@ -41,4 +47,74 @@ let populate fname = match res with | Fail err -> failwith err | Success chunks -> chunks + end + +val obtain_symbol_to_address_mapping : string -> list (string * nat) +let obtain_symbol_to_address_mapping fname = + let res = + (* Acquire the data from the file... *) + Bitstring.acquire fname >>= fun bs0 -> + (* Read the magic number and the flags in the header... *) + repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= fun (ident, bs) -> + match List.index ident 4 with + | Nothing -> fail "populate: ELF ident transcription error" + | Just c -> + (* Calculate whether we are dealing with a 32- or 64-bit file based on + * what we have read... + *) + if nat_of_unsigned_char c = Elf_header.elf_class_32 then + Elf_executable_file3.read_elf32_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf32_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf32_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf32_symbol_image_address symtab strtab >>= fun strs -> + return strs + else if nat_of_unsigned_char c = Elf_header.elf_class_64 then + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf64_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf64_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf64_symbol_image_address symtab strtab >>= fun strs -> + return strs + else + fail "obtain_symbol_to_address_mapping: ELF class unrecognised" + end + in + match res with + | Fail err -> failwith err + | Success strs -> strs + end + +val populate_and_obtain_symbol_to_address_mapping : string -> ((executable_process_image * elf_class) * list (string * nat)) +let populate_and_obtain_symbol_to_address_mapping fname = + let res = + (* Acquire the data from the file... *) + Bitstring.acquire fname >>= fun bs0 -> + (* Read the magic number and the flags in the header... *) + repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= fun (ident, bs) -> + match List.index ident 4 with + | Nothing -> fail "populate: ELF ident transcription error" + | Just c -> + (* Calculate whether we are dealing with a 32- or 64-bit file based on + * what we have read... + *) + if nat_of_unsigned_char c = Elf_header.elf_class_32 then + Elf_executable_file3.read_elf32_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf32_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf32_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf32_symbol_image_address symtab strtab >>= fun strs -> + Elf_executable_file3.get_elf32_executable_image f1 >>= fun (chunks, entry) -> + return (((chunks, entry), ELF_Class_32), strs) + else if nat_of_unsigned_char c = Elf_header.elf_class_64 then + Elf_executable_file3.read_elf64_executable_file3 bs0 >>= fun f1 -> + Elf_executable_file3.get_elf64_symbol_table f1 >>= fun symtab -> + Elf_executable_file3.get_elf64_symbol_string_table f1 >>= fun strtab -> + Elf_symbol_table.get_elf64_symbol_image_address symtab strtab >>= fun strs -> + Elf_executable_file3.get_elf64_executable_image f1 >>= fun (chunks, entry) -> + return (((chunks, entry), ELF_Class_64), strs) + else + fail "populate_and_obtain_symbol_to_address_mapping: ELF class unrecognised" + end + in + match res with + | Fail err -> failwith err + | Success res -> res end
\ No newline at end of file |