diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/elf_symbol_table.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/elf_symbol_table.ml | 563 |
1 files changed, 0 insertions, 563 deletions
diff --git a/lib/ocaml_rts/linksem/elf_symbol_table.ml b/lib/ocaml_rts/linksem/elf_symbol_table.ml deleted file mode 100644 index fc8dc068..00000000 --- a/lib/ocaml_rts/linksem/elf_symbol_table.ml +++ /dev/null @@ -1,563 +0,0 @@ -(*Generated by Lem from elf_symbol_table.lem.*) -(** [elf_symbol_table] provides types, functions and other definitions for - * working with ELF symbol tables. - *) - -open Lem_basic_classes -open Lem_bool -open Lem_list -open Lem_maybe -open Lem_num -open Lem_string -open Lem_tuple -(*import Set*) - -open Byte_sequence -open Error -open Missing_pervasives -open Show - -open Elf_header -open Elf_types_native_uint -open Endianness -open String_table - -(** Undefined symbol index *) - -let stn_undef : Nat_big_num.num= (Nat_big_num.of_int 0) - -(** Symbol binding *) - -(** Local symbols are not visible outside of the object file containing their - * definition. - *) -let stb_local : Nat_big_num.num= (Nat_big_num.of_int 0) - -(** Global symbols are visible to all object files being combined. - *) -let stb_global : Nat_big_num.num= (Nat_big_num.of_int 1) - -(** Weak symbols resemble global symbols but their definitions have lower - * precedence. - *) -let stb_weak : Nat_big_num.num= (Nat_big_num.of_int 2) - -(** Values in the following range have reserved OS specific semantics. - *) -let stb_loos : Nat_big_num.num= (Nat_big_num.of_int 10) -let stb_hios : Nat_big_num.num= (Nat_big_num.of_int 12) - -(** Values in the following range have reserved processor specific semantics. - *) -let stb_loproc : Nat_big_num.num= (Nat_big_num.of_int 13) -let stb_hiproc : Nat_big_num.num= (Nat_big_num.of_int 15) - -(** string_of_symbol_binding b os proc] produces a string representation of - * binding [m] using printing functions [os] and [proc] for OS- and processor- - * specific values respectively. - * OCaml specific definition. - *) -(*val string_of_symbol_binding : natural -> (natural -> string) -> (natural -> string) -> string*) -let string_of_symbol_binding m os proc:string= - (if Nat_big_num.equal m stb_local then - "LOCAL" - else if Nat_big_num.equal m stb_global then - "GLOBAL" - else if Nat_big_num.equal m stb_weak then - "WEAK" - else if Nat_big_num.greater_equal m stb_loos && Nat_big_num.less_equal m stb_hios then - os m - else if Nat_big_num.greater_equal m stb_loproc && Nat_big_num.less_equal m stb_hiproc then - proc m - else - "Invalid symbol binding") - -(** Symbol types *) - -(** The symbol's type is not specified. - *) -let stt_notype : Nat_big_num.num= (Nat_big_num.of_int 0) - -(** The symbol is associated with a data object such as a variable. - *) -let stt_object : Nat_big_num.num= (Nat_big_num.of_int 1) - -(** The symbol is associated with a function or other executable code. - *) -let stt_func : Nat_big_num.num= (Nat_big_num.of_int 2) - -(** The symbol is associated with a section. - *) -let stt_section : Nat_big_num.num= (Nat_big_num.of_int 3) - -(** Conventionally the symbol's value gives the name of the source file associated - * with the object file. - *) -let stt_file : Nat_big_num.num= (Nat_big_num.of_int 4) - -(** The symbol is an uninitialised common block. - *) -let stt_common : Nat_big_num.num= (Nat_big_num.of_int 5) - -(** The symbol specified a Thread Local Storage (TLS) entity. - *) -let stt_tls : Nat_big_num.num= (Nat_big_num.of_int 6) - -(** Values in the following range are reserved solely for OS-specific semantics. - *) -let stt_loos : Nat_big_num.num= (Nat_big_num.of_int 10) -let stt_hios : Nat_big_num.num= (Nat_big_num.of_int 12) - -(** Values in the following range are reserved solely for processor-specific - * semantics. - *) -let stt_loproc : Nat_big_num.num= (Nat_big_num.of_int 13) -let stt_hiproc : Nat_big_num.num= (Nat_big_num.of_int 15) - -(** [string_of_symbol_type sym os proc] produces a string representation of - * symbol type [m] using [os] and [proc] to pretty-print values reserved for - * OS- and processor-specific functionality. - *) -(*val string_of_symbol_type : natural -> (natural -> string) -> (natural -> string) -> string*) -let string_of_symbol_type m os proc:string= - (if Nat_big_num.equal m stt_notype then - "NOTYPE" - else if Nat_big_num.equal m stt_object then - "OBJECT" - else if Nat_big_num.equal m stt_func then - "FUNC" - else if Nat_big_num.equal m stt_section then - "SECTION" - else if Nat_big_num.equal m stt_file then - "FILE" - else if Nat_big_num.equal m stt_common then - "COMMON" - else if Nat_big_num.equal m stt_tls then - "TLS" - else if Nat_big_num.greater_equal m stt_loos && Nat_big_num.less_equal m stt_hios then - os m - else if Nat_big_num.greater_equal m stt_loproc && Nat_big_num.less_equal m stt_hiproc then - proc m - else - "Invalid symbol type") - -(** Symbol visibility *) - -(** The visibility of the symbol is as specified by the symbol's binding type. - *) -let stv_default : Nat_big_num.num= (Nat_big_num.of_int 0) - -(** The meaning of this visibility may be defined by processor supplements to - * further constrain hidden symbols. - *) -let stv_internal : Nat_big_num.num= (Nat_big_num.of_int 1) - -(** The symbol's name is not visible in other components. - *) -let stv_hidden : Nat_big_num.num= (Nat_big_num.of_int 2) - -(** The symbol is visible in other components but not pre-emptable. That is, - * references to the symbol in the same component resolve to this symbol even - * if other symbols of the same name in other components would normally be - * resolved to instead if we followed the normal rules of symbol resolution. - *) -let stv_protected : Nat_big_num.num= (Nat_big_num.of_int 3) - -(** [string_of_symbol_visibility m] produces a string representation of symbol - * visibility [m]. - *) -(*val string_of_symbol_visibility : natural -> string*) -let string_of_symbol_visibility m:string= - (if Nat_big_num.equal m stv_default then - "DEFAULT" - else if Nat_big_num.equal m stv_internal then - "INTERNAL" - else if Nat_big_num.equal m stv_hidden then - "HIDDEN" - else if Nat_big_num.equal m stv_protected then - "PROTECTED" - else - "Invalid symbol visibility") - -(** Symbol table entry type *) - -(** [elf32_symbol_table_entry] is an entry in a symbol table. - *) -type elf32_symbol_table_entry = - { elf32_st_name : Uint32.uint32 (** Index into the object file's string table *) - ; elf32_st_value : Uint32.uint32 (** Gives the value of the associated symbol *) - ; elf32_st_size : Uint32.uint32 (** Size of the associated symbol *) - ; elf32_st_info : Uint32.uint32 (** Specifies the symbol's type and binding attributes *) - ; elf32_st_other : Uint32.uint32 (** Currently specifies the symbol's visibility *) - ; elf32_st_shndx : Uint32.uint32 (** Section header index symbol is defined with respect to *) - } - -(** [elf32_symbol_table_entry_compare ent1 ent2] is an ordering-comparison function - * for symbol table entries suitable for constructing sets, finite maps and other - * ordered data structures from. - *) -(*val elf32_symbol_table_entry_compare : elf32_symbol_table_entry -> - elf32_symbol_table_entry -> ordering*) -let elf32_symbol_table_entry_compare ent1 ent2:int= - (sextupleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (Nat_big_num.of_string (Uint32.to_string ent1.elf32_st_name), Nat_big_num.of_string (Uint32.to_string ent1.elf32_st_value), - Nat_big_num.of_string (Uint32.to_string ent1.elf32_st_size), Nat_big_num.of_string (Uint32.to_string ent1.elf32_st_info), - Nat_big_num.of_string (Uint32.to_string ent1.elf32_st_other), Nat_big_num.of_string (Uint32.to_string ent1.elf32_st_shndx)) - (Nat_big_num.of_string (Uint32.to_string ent2.elf32_st_name), Nat_big_num.of_string (Uint32.to_string ent2.elf32_st_value), - Nat_big_num.of_string (Uint32.to_string ent2.elf32_st_size), Nat_big_num.of_string (Uint32.to_string ent2.elf32_st_info), - Nat_big_num.of_string (Uint32.to_string ent2.elf32_st_other), Nat_big_num.of_string (Uint32.to_string ent2.elf32_st_shndx))) - -let instance_Basic_classes_Ord_Elf_symbol_table_elf32_symbol_table_entry_dict:(elf32_symbol_table_entry)ord_class= ({ - - compare_method = elf32_symbol_table_entry_compare; - - isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_symbol_table_entry_compare f1 f2) (-1)))); - - isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_symbol_table_entry_compare f1 f2)(Pset.from_list compare [(-1); 0]))); - - isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_symbol_table_entry_compare f1 f2) 1))); - - isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_symbol_table_entry_compare f1 f2)(Pset.from_list compare [1; 0])))}) - -(** [elf64_symbol_table_entry] is an entry in a symbol table. - *) -type elf64_symbol_table_entry = - { elf64_st_name : Uint32.uint32 (** Index into the object file's string table *) - ; elf64_st_info : Uint32.uint32 (** Specifies the symbol's type and binding attributes *) - ; elf64_st_other : Uint32.uint32 (** Currently specifies the symbol's visibility *) - ; elf64_st_shndx : Uint32.uint32 (** Section header index symbol is defined with respect to *) - ; elf64_st_value : Uint64.uint64 (** Gives the value of the associated symbol *) - ; elf64_st_size : Uint64.uint64 (** Size of the associated symbol *) - } - -(** [elf64_symbol_table_entry_compare ent1 ent2] is an ordering-comparison function - * for symbol table entries suitable for constructing sets, finite maps and other - * ordered data structures from. - *) -(*val elf64_symbol_table_entry_compare : elf64_symbol_table_entry -> elf64_symbol_table_entry -> - ordering*) -let elf64_symbol_table_entry_compare ent1 ent2:int= - (sextupleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (Nat_big_num.of_string (Uint32.to_string ent1.elf64_st_name), Ml_bindings.nat_big_num_of_uint64 ent1.elf64_st_value, - Ml_bindings.nat_big_num_of_uint64 ent1.elf64_st_size, Nat_big_num.of_string (Uint32.to_string ent1.elf64_st_info), - Nat_big_num.of_string (Uint32.to_string ent1.elf64_st_other), Nat_big_num.of_string (Uint32.to_string ent1.elf64_st_shndx)) - (Nat_big_num.of_string (Uint32.to_string ent2.elf64_st_name), Ml_bindings.nat_big_num_of_uint64 ent2.elf64_st_value, - Ml_bindings.nat_big_num_of_uint64 ent2.elf64_st_size, Nat_big_num.of_string (Uint32.to_string ent2.elf64_st_info), - Nat_big_num.of_string (Uint32.to_string ent2.elf64_st_other), Nat_big_num.of_string (Uint32.to_string ent2.elf64_st_shndx))) - -let instance_Basic_classes_Ord_Elf_symbol_table_elf64_symbol_table_entry_dict:(elf64_symbol_table_entry)ord_class= ({ - - compare_method = elf64_symbol_table_entry_compare; - - isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_symbol_table_entry_compare f1 f2) (-1)))); - - isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_symbol_table_entry_compare f1 f2)(Pset.from_list compare [(-1); 0]))); - - isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_symbol_table_entry_compare f1 f2) 1))); - - isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_symbol_table_entry_compare f1 f2)(Pset.from_list compare [1; 0])))}) - -type elf32_symbol_table = elf32_symbol_table_entry - list - -type elf64_symbol_table = elf64_symbol_table_entry - list - -(** Extraction of symbol table data *) - -(* Functions below common to 32- and 64-bit! *) - -(** [extract_symbol_binding u] extracts a symbol table entry's symbol binding. [u] - * in this case is the [elfXX_st_info] field from a symbol table entry. - *) -(*val extract_symbol_binding : unsigned_char -> natural*) -let extract_symbol_binding entry:Nat_big_num.num= - (Nat_big_num.of_string (Uint32.to_string (Uint32.shift_right entry( 4)))) - -(** [extract_symbol_type u] extracts a symbol table entry's symbol type. [u] - * in this case is the [elfXX_st_info] field from a symbol table entry. - *) -(*val extract_symbol_type : unsigned_char -> natural*) -let extract_symbol_type entry:Nat_big_num.num= - (Nat_big_num.of_string (Uint32.to_string (Uint32.logand entry (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 15)))))) (* 0xf *) - -(** [get_symbol_info u] extracts a symbol table entry's symbol info. [u] - * in this case is the [elfXX_st_info] field from a symbol table entry. - *) -(*val make_symbol_info : natural -> natural -> unsigned_char*) -let make_symbol_info binding1 symtype:Uint32.uint32= - (Uint32.add - (Uint32.shift_left (Uint32.of_string (Nat_big_num.to_string binding1))( 4)) - (Uint32.logand (Uint32.of_string (Nat_big_num.to_string symtype)) - (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 15))))) (*0xf*) - -(** [get_symbol_visibility u] extracts a symbol table entry's symbol visibility. [u] - * in this case is the [elfXX_st_other] field from a symbol table entry. - *) -(*val get_symbol_visibility : unsigned_char -> natural*) -let get_symbol_visibility info:Nat_big_num.num= - (Nat_big_num.of_string (Uint32.to_string (Uint32.logand info (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 3)))))) (* 0x3*) - -(** [make_symbol_other m] converts a natural [m] to an unsigned char suitable - * for use in a symbol table entry's "other" field. - * XXX: WHY? - *) -(*val make_symbol_other : natural -> unsigned_char*) -let make_symbol_other visibility:Uint32.uint32= - (Uint32.of_string (Nat_big_num.to_string visibility)) - -(** [is_elf32_shndx_too_large ent] tests whether the symbol table entry's - * [shndx] field is equal to SHN_XINDEX, in which case the real value is stored - * elsewhere. - *) -(*val is_elf32_shndx_too_large : elf32_symbol_table_entry -> bool*) -let is_elf32_shndx_too_large syment:bool= (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string syment.elf32_st_shndx)) shn_xindex) - -(** [is_elf64_shndx_too_large ent] tests whether the symbol table entry's - * [shndx] field is equal to SHN_XINDEX, in which case the real value is stored - * elsewhere. - *) -(*val is_elf64_shndx_too_large : elf64_symbol_table_entry -> bool*) -let is_elf64_shndx_too_large syment:bool= (Nat_big_num.equal -(Nat_big_num.of_string (Uint32.to_string syment.elf64_st_shndx)) shn_xindex) - -(** NULL tests *) - -(** [is_elf32_null_entry ent] tests whether [ent] is a null symbol table entry, - * i.e. all fields set to [0]. - *) -(*val is_elf32_null_entry : elf32_symbol_table_entry -> bool*) -let is_elf32_null_entry ent:bool= (Nat_big_num.equal - (Nat_big_num.of_string (Uint32.to_string ent.elf32_st_name))(Nat_big_num.of_int 0) - && (( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf32_st_value))(Nat_big_num.of_int 0)) - && (( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf32_st_size))(Nat_big_num.of_int 0)) - && (( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf32_st_info))(Nat_big_num.of_int 0)) - && (( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf32_st_other))(Nat_big_num.of_int 0)) - && ( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf32_st_shndx))(Nat_big_num.of_int 0))))))) - -(** [is_elf64_null_entry ent] tests whether [ent] is a null symbol table entry, - * i.e. all fields set to [0]. - *) -(*val is_elf64_null_entry : elf64_symbol_table_entry -> bool*) -let is_elf64_null_entry ent:bool= (Nat_big_num.equal - (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_name))(Nat_big_num.of_int 0) - && (( Nat_big_num.equal(Ml_bindings.nat_big_num_of_uint64 ent.elf64_st_value)(Nat_big_num.of_int 0)) - && (( Nat_big_num.equal(Ml_bindings.nat_big_num_of_uint64 ent.elf64_st_size)(Nat_big_num.of_int 0)) - && (( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf64_st_info))(Nat_big_num.of_int 0)) - && (( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf64_st_other))(Nat_big_num.of_int 0)) - && ( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string ent.elf64_st_shndx))(Nat_big_num.of_int 0))))))) - -(** Printing symbol table entries *) - -type symtab_print_bundle = - (Nat_big_num.num -> string) * (Nat_big_num.num -> string) - -(** [string_of_elf32_symbol_table_entry ent] produces a string based representation - * of symbol table entry [ent]. - *) -(*val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string*) -let string_of_elf32_symbol_table_entry entry:string= - (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)) - ]) - -(** [string_of_elf64_symbol_table_entry ent] produces a string based representation - * of symbol table entry [ent]. - *) -(*val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string*) -let string_of_elf64_symbol_table_entry entry:string= - (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)) - ]) - -(** [string_of_elf32_symbol_table stbl] produces a string based representation - * of symbol table [stbl]. - *) -(*val string_of_elf32_symbol_table : elf32_symbol_table -> string*) -let string_of_elf32_symbol_table symtab:string= - (unlines (Lem_list.map string_of_elf32_symbol_table_entry symtab)) - -(** [elf64_null_symbol_table_entry] is the null symbol table entry, with all - * fields set to zero. - *) -(*val elf64_null_symbol_table_entry : elf64_symbol_table_entry*) -let elf64_null_symbol_table_entry:elf64_symbol_table_entry= - ({ elf64_st_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_info = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_other = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_shndx = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_value = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_size = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - }) - -(*val string_of_elf64_symbol_table : elf64_symbol_table -> string*) -let string_of_elf64_symbol_table symtab:string= - (unlines (Lem_list.map string_of_elf64_symbol_table_entry symtab)) - -let instance_Show_Show_Elf_symbol_table_elf32_symbol_table_entry_dict:(elf32_symbol_table_entry)show_class= ({ - - show_method = string_of_elf32_symbol_table_entry}) - -let instance_Show_Show_Elf_symbol_table_elf64_symbol_table_entry_dict:(elf64_symbol_table_entry)show_class= ({ - - show_method = string_of_elf64_symbol_table_entry}) - -(** Reading in symbol table (entries) *) - -(** [read_elf32_symbol_table_entry endian bs0] reads an ELF symbol table entry - * record from byte sequence [bs0] assuming endianness [endian], returning the - * remainder of the byte sequence. Fails if the byte sequence is not long enough. - *) -(*val read_elf32_symbol_table_entry : endianness -> byte_sequence -> - error (elf32_symbol_table_entry * byte_sequence)*) -let read_elf32_symbol_table_entry endian bs0:(elf32_symbol_table_entry*byte_sequence)error= - (read_elf32_word endian bs0 >>= (fun (st_name, bs0) -> - read_elf32_addr endian bs0 >>= (fun (st_value, bs0) -> - read_elf32_word endian bs0 >>= (fun (st_size, bs0) -> - read_unsigned_char endian bs0 >>= (fun (st_info, bs0) -> - read_unsigned_char endian bs0 >>= (fun (st_other, bs0) -> - 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 bytes_of_elf32_symbol_table_entry : endianness -> - elf32_symbol_table_entry -> byte_sequence*) -let bytes_of_elf32_symbol_table_entry endian entry:byte_sequence= - (Byte_sequence.from_byte_lists [ - bytes_of_elf32_word endian entry.elf32_st_name - ; bytes_of_elf32_addr endian entry.elf32_st_value - ; bytes_of_elf32_word endian entry.elf32_st_size - ; bytes_of_unsigned_char entry.elf32_st_info - ; bytes_of_unsigned_char entry.elf32_st_other - ; bytes_of_elf32_half endian entry.elf32_st_shndx - ]) - -(** [read_elf64_symbol_table_entry endian bs0] reads an ELF symbol table entry - * record from byte sequence [bs0] assuming endianness [endian], returning the - * remainder of the byte sequence. Fails if the byte sequence is not long enough. - *) -(*val read_elf64_symbol_table_entry : endianness -> byte_sequence -> - error (elf64_symbol_table_entry * byte_sequence)*) -let read_elf64_symbol_table_entry endian bs0:(elf64_symbol_table_entry*byte_sequence)error= - (read_elf64_word endian bs0 >>= (fun (st_name, bs0) -> - read_unsigned_char endian bs0 >>= (fun (st_info, bs0) -> - read_unsigned_char endian bs0 >>= (fun (st_other, bs0) -> - read_elf64_half endian bs0 >>= (fun (st_shndx, bs0) -> - read_elf64_addr endian bs0 >>= (fun (st_value, bs0) -> - 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 bytes_of_elf64_symbol_table_entry : endianness -> - elf64_symbol_table_entry -> byte_sequence*) -let bytes_of_elf64_symbol_table_entry endian entry:byte_sequence= - (Byte_sequence.from_byte_lists [ - bytes_of_elf64_word endian entry.elf64_st_name - ; bytes_of_unsigned_char entry.elf64_st_info - ; bytes_of_unsigned_char entry.elf64_st_other - ; bytes_of_elf64_half endian entry.elf64_st_shndx - ; bytes_of_elf64_addr endian entry.elf64_st_value - ; bytes_of_elf64_xword endian entry.elf64_st_size - ]) - -(** [read_elf32_symbol_table endian bs0] reads a symbol table from byte sequence - * [bs0] assuming endianness [endian]. Assumes [bs0]'s length modulo the size - * of a symbol table entry is 0. Fails otherwise. - *) -(*val read_elf32_symbol_table : endianness -> byte_sequence -> error elf32_symbol_table*) -let rec read_elf32_symbol_table endian bs0:((elf32_symbol_table_entry)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 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)))) - -(** [read_elf64_symbol_table endian bs0] reads a symbol table from byte sequence - * [bs0] assuming endianness [endian]. Assumes [bs0]'s length modulo the size - * of a symbol table entry is 0. Fails otherwise. - *) -(*val read_elf64_symbol_table : endianness -> byte_sequence -> error elf64_symbol_table*) -let rec read_elf64_symbol_table endian bs0:((elf64_symbol_table_entry)list)error= - (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 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)))) - -(** Association map of symbol name, symbol type, symbol size, symbol address - * and symbol binding. - * A PPCMemism. - *) -type symbol_address_map - = (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num)) list - -(** [get_elf32_symbol_image_address symtab stbl] extracts the symbol address map - * from the symbol table [symtab] using the string table [stbl]. - * A PPCMemism. - *) -(*val get_elf32_symbol_image_address : elf32_symbol_table -> string_table -> - error symbol_address_map*) -let get_elf32_symbol_image_address symtab strtab:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*Nat_big_num.num))list)error= - (mapM (fun entry -> - let name1 = (Nat_big_num.of_string (Uint32.to_string entry.elf32_st_name)) in - let addr = (Nat_big_num.of_string (Uint32.to_string entry.elf32_st_value)) in - let size2 = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string entry.elf32_st_size))(Nat_big_num.of_int 8)) in - let typ = (extract_symbol_type entry.elf32_st_info) in - let bnd = (extract_symbol_binding entry.elf32_st_info) in - String_table.get_string_at name1 strtab >>= (fun str -> - return (str, (typ, size2, addr, bnd))) - ) symtab) - -(** [get_elf64_symbol_image_address symtab stbl] extracts the symbol address map - * from the symbol table [symtab] using the string table [stbl]. - * A PPCMemism. - *) -(*val get_elf64_symbol_image_address : elf64_symbol_table -> string_table -> - error symbol_address_map*) -let get_elf64_symbol_image_address symtab strtab:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*Nat_big_num.num))list)error= - (mapM (fun entry -> - let name1 = (Nat_big_num.of_string (Uint32.to_string entry.elf64_st_name)) in - let addr = (Ml_bindings.nat_big_num_of_uint64 entry.elf64_st_value) in - let size2 = (Ml_bindings.nat_big_num_of_uint64 entry.elf64_st_size) in - let typ = (extract_symbol_type entry.elf64_st_info) in - let bnd = (extract_symbol_binding entry.elf64_st_info) in - String_table.get_string_at name1 strtab >>= (fun str -> - return (str, (typ, size2, addr, bnd))) - ) symtab) - -(** [get_el32_symbol_type ent] extracts the symbol type from symbol table entry - * [ent]. - *) -(*val get_elf32_symbol_type : elf32_symbol_table_entry -> natural*) -let get_elf32_symbol_type syment:Nat_big_num.num= (extract_symbol_type syment.elf32_st_info) - -(** [get_el64_symbol_type ent] extracts the symbol type from symbol table entry - * [ent]. - *) -(*val get_elf64_symbol_type : elf64_symbol_table_entry -> natural*) -let get_elf64_symbol_type syment:Nat_big_num.num= (extract_symbol_type syment.elf64_st_info) - -(** [get_el32_symbol_binding ent] extracts the symbol binding from symbol table entry - * [ent]. - *) -(*val get_elf32_symbol_binding : elf32_symbol_table_entry -> natural*) -let get_elf32_symbol_binding syment:Nat_big_num.num= (extract_symbol_binding syment.elf32_st_info) - -(** [get_el64_symbol_binding ent] extracts the symbol binding from symbol table entry - * [ent]. - *) -(*val get_elf64_symbol_binding : elf64_symbol_table_entry -> natural*) -let get_elf64_symbol_binding syment:Nat_big_num.num= (extract_symbol_binding syment.elf64_st_info) |