diff options
Diffstat (limited to 'src/elf_model/elf_symbol_table.ml')
| -rw-r--r-- | src/elf_model/elf_symbol_table.ml | 408 |
1 files changed, 206 insertions, 202 deletions
diff --git a/src/elf_model/elf_symbol_table.ml b/src/elf_model/elf_symbol_table.ml index a2fed159..369629b0 100644 --- a/src/elf_model/elf_symbol_table.ml +++ b/src/elf_model/elf_symbol_table.ml @@ -2,245 +2,249 @@ open Lem_basic_classes open Lem_bool open Lem_list -open Lem_num +open Lem_maybe open Lem_string +open Lem_tuple -open Bitstring -open Elf_section_header -open Elf_types +open Bitstring_local open Error +open Missing_pervasives open Show -(** Symbol table indices *) +open Elf_types +open Endianness +open String_table + +(** Undefined symbol index *) -(** Symbol table index is a subscript into the symbol table, which holds - * information needed to locate and relocate a program's symbolic definitions - * and references. Index 0 designates both the first entry in the table and - * serves as the undefined symbol index. [stn_undef] is a mnemonic for that - * undefined symbol. - *) let stn_undef : int =( 0) -(** Symbol bindings *) - -(** [elf32_st_bind] unpacks the binding information from the [st_info] field - * in the record type below. - *) -let elf32_st_bind i = -(Int64.to_int (Int64.shift_right i( 4))) -(** [elf64_st_bind] unpacks the binding information from the [st_info] field - * in the record type below. - *) -let elf64_st_bind i = -(Int64.to_int (Int64.shift_right i( 4))) -(** [elf32_st_type] unpacks the type information from the [e32_st_info] field - * in the record type below. - *) -let elf32_st_type i = -(Int64.to_int (Int64.logand i (Int64.of_int( 15)))) (* 0xf *) -(** [elf64_st_type] unpacks the type information from the [e64_st_info] field - * in the record type below. - *) -let elf64_st_type i = -(Int64.to_int (Int64.logand i (Int64.of_int( 15)))) (* 0xf *) -(** [elf32_st_info] unpacks other information from the [e32_st_info] field in the - * record type below. - *) -let elf32_st_info b t = -(let left = (Int64.shift_left b( 4)) in - let right = (Int64.logand t (Int64.of_int( 15))) in (* 0xf *) - let result = (Int64.add left right) in - Int64.to_int result) -(** [elf64_st_info] unpacks other information from the [e64_st_info] field in the - * record type below. - *) -let elf64_st_info b t = -(let left = (Int64.shift_left b( 4)) in - let right = (Int64.logand t (Int64.of_int( 15))) in (* 0xf *) - let result = (Int64.add left right) in - Int64.to_int result) -(** [stb_local]: local symbols are not visible outside the object file - * containing their definition. - *) +(** Symbol binding *) + let stb_local : int =( 0) -(** [stb_global]: global symbols are visible to all object files being combined. - *) let stb_global : int =( 1) -(** [stb_weak]: weak symbols resemble global symbols but their definitions have - * lower precedence. - *) let stb_weak : int =( 2) -(** [stb_loos]: start of the range reserved for operating-system specific - * semantics. - *) let stb_loos : int =( 10) -(** [stb_hios]: end of the range reserved for operating-system specific - * semantics. - *) let stb_hios : int =( 12) -(** [stb_loproc]: start of the range reserved for processor specific semantics. - *) let stb_loproc : int =( 13) -(** [stb_hiproc]: end of the range reserved for processor specific semantics. - *) let stb_hiproc : int =( 15) -(** Symbol types. *) +(*val string_of_symbol_binding : nat -> (nat -> string) -> (nat -> string) -> string*) +let string_of_symbol_binding m os proc = +(if m = stb_local then + "STB_LOCAL" + else if m = stb_global then + "STB_GLOBAL" + else if m = stb_weak then + "STB_WEAK" + else if (m >= stb_loos) && (m <= stb_hios) then + os m + else if (m >= stb_loproc) && (m <= stb_hiproc) then + proc m + else + "Invalid symbol binding") + +(** Symbol types *) -(** [stt_notype]: the symbol's type is not specified. - *) let stt_notype : int =( 0) -(** [stt_object]: the symbol is associated with a data object, such as a - * variable, an array, and so on. - *) let stt_object : int =( 1) -(** [stt_func]: the symbol is associated with a function or other executable - * code. - *) let stt_func : int =( 2) -(** [stt_section]: the symbol is associated with a section. - *) let stt_section : int =( 3) -(** [stt_file]: the symbol's name gives the name of the source file associated - * with the object file. Must have [stb_local] binding and its section index - * must be [shn_abs]. It must also precede the other [stb_local] symbols for - * the file, is present. - *) let stt_file : int =( 4) -(** [stt_common]: labels an unitialised common block. - *) let stt_common : int =( 5) -(** [stt_tls]: specifies a thread local storage (TLS) entity. Gives the - * assigned offset of the symbol, not its address. TLS symbols may only be - * referenced by special TLS relocations and TLS relocations may only reference - * symbols with type [stt_tls]. - *) let stt_tls : int =( 6) -(** [stt_loos]: start of the range reserved for operating-system specific - * semantics. - *) let stt_loos : int =( 10) -(** [stt_hios]: end of the range reserved for operating-system specific - * semantics. - *) let stt_hios : int =( 12) -(** [stt_loproc]: start of the range reserved for processor specific - * semantics. - *) let stt_loproc : int =( 13) -(** [stt_hiproc]: end of the range reserved for processor specific semantics. - *) let stt_hiproc : int =( 15) -(** Symbol visibility. *) - -(** [elf32_st_visibility] unpacks visibility information from the [e32_st_other] - * field in the record type below. - *) -(*val elf32_st_visibility : unsigned_char -> nat*) -let elf32_st_visibility o = -(Int64.to_int (Int64.logand o (Int64.of_int( 3)))) (* 0x3 *) - -(** [stv_default]: symbol visibility is as specified by the symbol's binding - * type. Global and weak symbols are visible outside their defining component - * (executable or shared object file). Local symbols are hidden. Global and - * weak symbols are also pre-emptable: they may be pre-empted by definitions - * of the same name in another component. - *) +(*val string_of_symbol_type : nat -> (nat -> string) -> (nat -> string) -> string*) +let string_of_symbol_type m os proc = +(if m = stt_notype then + "STT_NOTYPE" + else if m = stt_object then + "STT_OBJECT" + else if m = stt_func then + "STT_FUNC" + else if m = stt_section then + "STT_SECTION" + else if m = stt_file then + "STT_FILE" + else if m = stt_common then + "STT_COMMON" + else if m = stt_tls then + "STT_TLS" + else if (m >= stt_loos) && (m <= stt_hios) then + os m + else if (m >= stt_loproc) && (m <= stt_hiproc) then + proc m + else + "Invalid symbol type") + +(** Symbol visibility *) + let stv_default : int =( 0) -(** [stv_internal]: meaning may be further defined by processor supplements to - * further constrain hidden symbols. An internal symbol in a relocatable file - * must be either removed or converted to [stb_local] when the relocatable - * object is included in an executable or shared object by the linker. - *) let stv_internal : int =( 1) -(** [stv_hidden]: a symbol in the current component is hidden if its name is not - * visible to other components, necessarily protecting the symbol. A hidden - * object may still be referenced from another component if its address is - * passed outside. A hidden symbol in a relocatable object must be either - * removed or converted to [stb_local] when the relocatable file is included in - * an executable or shared object by the linker. - *) let stv_hidden : int =( 2) -(** [stv_protected]: a protected symbol is visible in other components but is - * not pre-emptable, so that any reference to such a symbol from within the - * defining component must be resolved to the definition in that component. - * A symbol with [stb_local] binding must not have [stv_protected] visibility. - * If a symbol definition with [stv_protected] visibility from a shared object - * file is taken as resolving a reference from an executable or another shared - * object, the [shn_undef] symbol table entry created has [stv_default] - * visibility. - *) let stv_protected : int =( 3) -(** The symbol table entry type. *) +(*val string_of_symbol_visibility : nat -> string*) +let string_of_symbol_visibility m = +(if m = stv_default then + "STV_DEFAULT" + else if m = stv_internal then + "STV_INTERNAL" + else if m = stv_hidden then + "STV_HIDDEN" + else if m = stv_protected then + "STV_PROTECTED" + else + "Invalid symbol visibility") + +(** ELF32 symbol table type *) type elf32_symbol_table_entry = - { elf32_st_name : Int64.t - ; elf32_st_value : Int64.t - ; elf32_st_size : Int64.t - ; elf32_st_info0 : Int64.t - ; elf32_st_other : Int64.t - ; elf32_st_shndx : Int64.t + { elf32_st_name : Uint32.t + ; elf32_st_value : Uint32.t + ; elf32_st_size : Uint32.t + ; elf32_st_info : Uint32.t + ; elf32_st_other : Uint32.t + ; elf32_st_shndx : Uint32.t } - -let string_of_elf32_symbol_table_entry entry = -(List.fold_right (^) [ - "\t"; "Name: "; Int64.to_string entry.elf32_st_name - ; "\t"; "Size: "; Int64.to_string entry.elf32_st_size - ; "\n\t"; "Value: "; Int64.to_string entry.elf32_st_value - ; "\t"; "Info: "; Int64.to_string entry.elf32_st_info0; "\n\n" - ] "") - -let read_elf32_symbol_table_entry bitstring6 : elf32_symbol_table_entry error = -(Ml_bindings.read_elf32_word bitstring6 >>= (fun (name, bitstring5) -> - Ml_bindings.read_elf32_addr bitstring5 >>= (fun (value, bitstring4) -> - Ml_bindings.read_elf32_word bitstring4 >>= (fun (size, bitstring3) -> - Ml_bindings.read_unsigned_char bitstring3 >>= (fun (info, bitstring2) -> - Ml_bindings.read_unsigned_char bitstring2 >>= (fun (other, bitstring1) -> - Ml_bindings.read_elf32_half bitstring1 >>= (fun (shndx, bitstring0) -> - let entry = ({ elf32_st_name = name; elf32_st_value = value; elf32_st_size = size; elf32_st_info0 = info; elf32_st_other = other; elf32_st_shndx = shndx }) in - return entry))))))) - -let rec read_elf32_symbol_table_entries bs : ( elf32_symbol_table_entry list) error = -(if Bitstring.bitstring_length bs = 0 then - return [] - else - let (cut, rest) = (Utility.partition_bitstring( 128) bs) in - read_elf32_symbol_table_entry cut >>= (fun head -> - read_elf32_symbol_table_entries rest >>= (fun tail -> - return (head::tail)))) - -let rec read_elf32_symbol_tables' offset_sizes bs = -((match offset_sizes with - | [] -> return [] - | x::xs -> - let (offset, size) = x in - let (_, relevant) = (Utility.partition_bitstring offset bs) in - let (cut, _) = (Utility.partition_bitstring size relevant) in - read_elf32_symbol_table_entries cut >>= (fun head -> - read_elf32_symbol_tables' xs bs >>= (fun tail -> - return (head::tail))) - )) + +(** Extraction of symbol table data *) + +(* Functions below common to 32- and 64-bit! *) + +(*val get_symbol_binding : unsigned_char -> nat*) +let get_symbol_binding entry = +(Uint32.to_int (Uint32.shift_right entry( 4))) + +(*val get_symbol_type : unsigned_char -> nat*) +let get_symbol_type entry = +(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 15)))) (* 0xf *) + +(*val get_symbol_info : unsigned_char -> unsigned_char -> nat*) +let get_symbol_info entry0 entry1 = +(Uint32.to_int (Uint32.add + (Uint32.shift_left entry0( 4)) (Uint32.logand entry1 + (Uint32.of_int( 15))))) (*0xf*) + +(*val get_symbol_visibility : unsigned_char -> nat*) +let get_symbol_visibility entry = +(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 3)))) (* 0x3*) + +type symtab_print_bundle = (int -> string) * (int -> string) + +(*val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string*) +let string_of_elf32_symbol_table_entry entry = +(unlines [ +("\t" ^ ("Name: " ^ Uint32.to_string entry.elf32_st_name)) + ; ("\t" ^ ("Value: " ^ Uint32.to_string entry.elf32_st_value)) + ; ("\t" ^ ("Size: " ^ Uint32.to_string entry.elf32_st_size)) + ; ("\t" ^ ("Info: " ^ Uint32.to_string entry.elf32_st_info)) + ; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf32_st_other)) + ; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf32_st_shndx)) + ]) type elf32_symbol_table = elf32_symbol_table_entry list -let read_elf32_symbol_tables sections bs : ( elf32_symbol_table list) error = -(let symtabs = (List.filter (fun sect -> - (Int64.to_int sect.elf32_sh_type = sht_symtab) || - (Int64.to_int sect.elf32_sh_type = sht_dynsym)) sections) - in - let _ = (print_endline ("Symtabs: " ^ natShow (List.length symtabs))) in - let offsets_sizes = (List.map (fun sect -> - let offset = ((Int64.to_int sect.elf32_sh_offset) * 8) in - let size = -(let _ = (print_endline ("YYY size: " ^ natShow (Int64.to_int sect.elf32_sh_size * 8))) in - Int64.to_int sect.elf32_sh_size * 8) - in - (offset, size)) symtabs) - in - read_elf32_symbol_tables' offsets_sizes bs) - -let string_of_elf32_symbol_table tbl = -("Symbol table contents:" ^ ("\n" ^ - List.fold_right (^) (List.map string_of_elf32_symbol_table_entry tbl) "")) +(*val string_of_elf32_symbol_table : elf32_symbol_table -> string*) +let string_of_elf32_symbol_table symtab = +(unlines (List.map string_of_elf32_symbol_table_entry symtab)) + +type 'a hasElf32SymbolTable_class={ + get_elf32_symbol_table_method : 'a -> elf32_symbol_table +} + +(*val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring)*) +let read_elf32_symbol_table_entry endian bs0 = +(Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_name, bs0) -> + Ml_bindings.read_elf32_addr endian bs0 >>= (fun (st_value, bs0) -> + Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_size, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) -> + Ml_bindings.read_elf32_half endian bs0 >>= (fun (st_shndx, bs0) -> + return ({ elf32_st_name = st_name; elf32_st_value = st_value; + elf32_st_size = st_size; elf32_st_info = st_info; + elf32_st_other = st_other; elf32_st_shndx = st_shndx }, bs0)))))))) + +(*val read_elf32_symbol_table : endianness -> bitstring -> error elf32_symbol_table*) +let rec read_elf32_symbol_table endian bs0 = +(if Bitstring.bitstring_length bs0 = 0 then + return [] + else + read_elf32_symbol_table_entry endian bs0 >>= (fun (head, bs0) -> + read_elf32_symbol_table endian bs0 >>= (fun tail -> + return (head::tail)))) + +(** ELF64 symbol table type *) + +type elf64_symbol_table_entry = + { elf64_st_name : Uint32.t + ; elf64_st_info : Uint32.t + ; elf64_st_other : Uint32.t + ; elf64_st_shndx : Uint32.t + ; elf64_st_value : Uint64.t + ; elf64_st_size : Uint64.t + } + +(*val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string*) +let string_of_elf64_symbol_table_entry entry = +(unlines [ +("\t" ^ ("Name: " ^ Uint32.to_string entry.elf64_st_name)) + ; ("\t" ^ ("Info: " ^ Uint32.to_string entry.elf64_st_info)) + ; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf64_st_other)) + ; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf64_st_shndx)) + ; ("\t" ^ ("Value: " ^ Uint64.to_string entry.elf64_st_value)) + ; ("\t" ^ ("Size: " ^ Uint64.to_string entry.elf64_st_size)) + ]) + +type elf64_symbol_table = elf64_symbol_table_entry list + +(*val string_of_elf64_symbol_table : elf64_symbol_table -> string*) +let string_of_elf64_symbol_table symtab = +(unlines (List.map string_of_elf64_symbol_table_entry symtab)) + +type 'a hasElf64SymbolTable_class={ + get_elf64_symbol_table_method : 'a -> elf64_symbol_table +} + +(*val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring)*) +let read_elf64_symbol_table_entry endian bs0 = +(Ml_bindings.read_elf64_word endian bs0 >>= (fun (st_name, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) -> + Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) -> + Ml_bindings.read_elf64_half endian bs0 >>= (fun (st_shndx, bs0) -> + Ml_bindings.read_elf64_addr endian bs0 >>= (fun (st_value, bs0) -> + Ml_bindings.read_elf64_xword endian bs0 >>= (fun (st_size, bs0) -> + return ({ elf64_st_name = st_name; elf64_st_info = st_info; + elf64_st_other = st_other; elf64_st_shndx = st_shndx; + elf64_st_value = st_value; elf64_st_size = st_size }, bs0)))))))) + +(*val read_elf64_symbol_table : endianness -> bitstring -> error elf64_symbol_table*) +let rec read_elf64_symbol_table endian bs0 = +(if Bitstring.bitstring_length bs0 = 0 then + return [] + else + read_elf64_symbol_table_entry endian bs0 >>= (fun (head, bs0) -> + read_elf64_symbol_table endian bs0 >>= (fun tail -> + return (head::tail)))) + +(*val get_elf32_symbol_image_address : elf32_symbol_table -> string_table -> error (list (string * nat))*) +let get_elf32_symbol_image_address symtab strtab = +(mapM (fun entry -> + let name = (Uint32.to_int entry.elf32_st_name) in + let addr = (Uint32.to_int entry.elf32_st_value) in + String_table.get_string_at name strtab >>= (fun str -> + return (str, addr)) + ) symtab) + +(*val get_elf64_symbol_image_address : elf64_symbol_table -> string_table -> error (list (string * nat))*) +let get_elf64_symbol_image_address symtab strtab = +(mapM (fun entry -> + let name = (Uint32.to_int entry.elf64_st_name) in + let addr = (Uint64.to_int entry.elf64_st_value) in + String_table.get_string_at name strtab >>= (fun str -> + return (str, addr)) + ) symtab)
\ No newline at end of file |