(*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)