package linksem

You can search for identifiers within the package.

in-package search v0.2.0

package linksem

linksem_zarith

Legend:
Library
Module
Module type
Parameter
Class
Class type

elf_symbol_table provides types, functions and other definitions for * working with ELF symbol tables.

Undefined symbol index

val stn_undef : Nat_big_num.num

Symbol binding

val stb_local : Nat_big_num.num

Local symbols are not visible outside of the object file containing their * definition.

val stb_global : Nat_big_num.num

Global symbols are visible to all object files being combined.

val stb_weak : Nat_big_num.num

Weak symbols resemble global symbols but their definitions have lower * precedence.

val stb_loos : Nat_big_num.num

Values in the following range have reserved OS specific semantics.

val stb_hios : Nat_big_num.num

val stb_loproc : Nat_big_num.num

Values in the following range have reserved processor specific semantics.

val stb_hiproc : Nat_big_num.num

val string_of_symbol_binding : 
  Nat_big_num.num ->
  (Nat_big_num.num -> string) ->
  (Nat_big_num.num -> string) ->
  string

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.

Symbol types

val stt_notype : Nat_big_num.num

The symbol's type is not specified.

val stt_object : Nat_big_num.num

The symbol is associated with a data object such as a variable.

val stt_func : Nat_big_num.num

The symbol is associated with a function or other executable code.

val stt_section : Nat_big_num.num

The symbol is associated with a section.

val stt_file : Nat_big_num.num

Conventionally the symbol's value gives the name of the source file associated * with the object file.

val stt_common : Nat_big_num.num

The symbol is an uninitialised common block.

val stt_tls : Nat_big_num.num

The symbol specified a Thread Local Storage (TLS) entity.

val stt_loos : Nat_big_num.num

Values in the following range are reserved solely for OS-specific semantics.

val stt_hios : Nat_big_num.num

val stt_loproc : Nat_big_num.num

Values in the following range are reserved solely for processor-specific * semantics.

val stt_hiproc : Nat_big_num.num

val string_of_symbol_type : 
  Nat_big_num.num ->
  (Nat_big_num.num -> string) ->
  (Nat_big_num.num -> string) ->
  string

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.

Symbol visibility

val stv_default : Nat_big_num.num

The visibility of the symbol is as specified by the symbol's binding type.

val stv_internal : Nat_big_num.num

The meaning of this visibility may be defined by processor supplements to * further constrain hidden symbols.

val stv_hidden : Nat_big_num.num

The symbol's name is not visible in other components.

val stv_protected : Nat_big_num.num

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.

val string_of_symbol_visibility : Nat_big_num.num -> string

string_of_symbol_visibility m produces a string representation of symbol * visibility m.

Symbol table entry type

type elf32_symbol_table_entry = {

elf32_st_name : Uint32_wrapper.uint32;
(*
Index into the object file's string table
*)
elf32_st_value : Uint32_wrapper.uint32;
(*
Gives the value of the associated symbol
*)
elf32_st_size : Uint32_wrapper.uint32;
(*
Size of the associated symbol
*)
elf32_st_info : Uint32_wrapper.uint32;
(*
Specifies the symbol's type and binding attributes
*)
elf32_st_other : Uint32_wrapper.uint32;
(*
Currently specifies the symbol's visibility
*)
elf32_st_shndx : Uint32_wrapper.uint32;
(*
Section header index symbol is defined with respect to
*)

}

elf32_symbol_table_entry is an entry in a symbol table.

val elf32_symbol_table_entry_compare : 
  elf32_symbol_table_entry ->
  elf32_symbol_table_entry ->
  int

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 instance_Basic_classes_Ord_Elf_symbol_table_elf32_symbol_table_entry_dict : 
  elf32_symbol_table_entry Lem_basic_classes.ord_class

type elf64_symbol_table_entry = {

elf64_st_name : Uint32_wrapper.uint32;
(*
Index into the object file's string table
*)
elf64_st_info : Uint32_wrapper.uint32;
(*
Specifies the symbol's type and binding attributes
*)
elf64_st_other : Uint32_wrapper.uint32;
(*
Currently specifies the symbol's visibility
*)
elf64_st_shndx : Uint32_wrapper.uint32;
(*
Section header index symbol is defined with respect to
*)
elf64_st_value : Uint64_wrapper.uint64;
(*
Gives the value of the associated symbol
*)
elf64_st_size : Uint64_wrapper.uint64;
(*
Size of the associated symbol
*)

}

elf64_symbol_table_entry is an entry in a symbol table.

val elf64_symbol_table_entry_compare : 
  elf64_symbol_table_entry ->
  elf64_symbol_table_entry ->
  int

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 instance_Basic_classes_Ord_Elf_symbol_table_elf64_symbol_table_entry_dict : 
  elf64_symbol_table_entry Lem_basic_classes.ord_class

type elf32_symbol_table = elf32_symbol_table_entry list

type elf64_symbol_table = elf64_symbol_table_entry list

Extraction of symbol table data

val extract_symbol_binding : Nat_big_num.num -> Nat_big_num.num

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_type : Nat_big_num.num -> Nat_big_num.num

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 make_symbol_info : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  Uint32_wrapper.uint32

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 get_symbol_visibility : Nat_big_num.num -> Nat_big_num.num

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 make_symbol_other : Nat_big_num.num -> Uint32_wrapper.uint32

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 is_elf32_shndx_too_large : elf32_symbol_table_entry -> bool

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_elf64_shndx_too_large : elf64_symbol_table_entry -> bool

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.

NULL tests

val is_elf32_null_entry : elf32_symbol_table_entry -> bool

is_elf32_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

is_elf64_null_entry ent tests whether ent is a null symbol table entry, * i.e. all fields set to 0.

Printing symbol table entries

type symtab_print_bundle =
  (Nat_big_num.num -> string) * (Nat_big_num.num -> string)

val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string

string_of_elf32_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

string_of_elf64_symbol_table_entry ent produces a string based representation * of symbol table entry ent.

val string_of_elf32_symbol_table : elf32_symbol_table_entry list -> string

string_of_elf32_symbol_table stbl produces a string based representation * of symbol table stbl.

val elf64_null_symbol_table_entry : elf64_symbol_table_entry

elf64_null_symbol_table_entry is the null symbol table entry, with all * fields set to zero.

val string_of_elf64_symbol_table : elf64_symbol_table_entry list -> string

val instance_Show_Show_Elf_symbol_table_elf32_symbol_table_entry_dict : 
  elf32_symbol_table_entry Show.show_class

val instance_Show_Show_Elf_symbol_table_elf64_symbol_table_entry_dict : 
  elf64_symbol_table_entry Show.show_class

Reading in symbol table (entries)

val read_elf32_symbol_table_entry : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (elf32_symbol_table_entry * Byte_sequence_wrapper.byte_sequence) Error.error

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 bytes_of_elf32_symbol_table_entry : 
  Endianness.endianness ->
  elf32_symbol_table_entry ->
  Byte_sequence_wrapper.byte_sequence

val read_elf64_symbol_table_entry : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (elf64_symbol_table_entry * Byte_sequence_wrapper.byte_sequence) Error.error

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 bytes_of_elf64_symbol_table_entry : 
  Endianness.endianness ->
  elf64_symbol_table_entry ->
  Byte_sequence_wrapper.byte_sequence

val read_elf32_symbol_table : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  elf32_symbol_table_entry list Error.error

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_elf64_symbol_table : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  elf64_symbol_table_entry list Error.error

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.

type symbol_address_map =
  (string
   * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num))
    list

Association map of symbol name, symbol type, symbol size, symbol address * and symbol binding. * A PPCMemism.

val get_elf32_symbol_image_address : 
  elf32_symbol_table_entry list ->
  String_table.string_table ->
  (string
   * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num))
    list
    Error.error

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_elf64_symbol_image_address : 
  elf64_symbol_table_entry list ->
  String_table.string_table ->
  (string
   * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num))
    list
    Error.error

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_elf32_symbol_type : elf32_symbol_table_entry -> Nat_big_num.num

get_el32_symbol_type ent extracts the symbol type from symbol table entry * ent.

val get_elf64_symbol_type : elf64_symbol_table_entry -> Nat_big_num.num

get_el64_symbol_type ent extracts the symbol type from symbol table entry * ent.

val get_elf32_symbol_binding : elf32_symbol_table_entry -> Nat_big_num.num

get_el32_symbol_binding ent extracts the symbol binding from symbol table entry * ent.

val get_elf64_symbol_binding : elf64_symbol_table_entry -> Nat_big_num.num

get_el64_symbol_binding ent extracts the symbol binding from symbol table entry * ent.