package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Elf_symbol_table/index.html
Module Elf_symbol_table
Source
elf_symbol_table
provides types, functions and other definitions for * working with ELF symbol tables.
Undefined symbol index
Symbol binding
Local symbols are not visible outside of the object file containing their * definition.
Global symbols are visible to all object files being combined.
Weak symbols resemble global symbols but their definitions have lower * precedence.
Values in the following range have reserved OS specific semantics.
Values in the following range have reserved processor specific semantics.
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
The symbol's type is not specified.
The symbol is associated with a data object such as a variable.
The symbol is associated with a function or other executable code.
The symbol is associated with a section.
Conventionally the symbol's value gives the name of the source file associated * with the object file.
The symbol is an uninitialised common block.
The symbol specified a Thread Local Storage (TLS) entity.
Values in the following range are reserved solely for OS-specific semantics.
Values in the following range are reserved solely for processor-specific * semantics.
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
The visibility of the symbol is as specified by the symbol's binding type.
The meaning of this visibility may be defined by processor supplements to * further constrain hidden symbols.
The symbol's name is not visible in other components.
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.
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
Extraction of symbol table data
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.
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.
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.
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.
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?
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.
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
is_elf32_null_entry ent
tests whether ent
is a null symbol table entry, * i.e. all fields set to 0
.
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
string_of_elf32_symbol_table_entry ent
produces a string based representation * of symbol table entry ent
.
string_of_elf64_symbol_table_entry ent
produces a string based representation * of symbol table entry ent
.
string_of_elf32_symbol_table stbl
produces a string based representation * of symbol table stbl
.
elf64_null_symbol_table_entry
is the null symbol table entry, with all * fields set to zero.
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.
get_el32_symbol_type ent
extracts the symbol type from symbol table entry * ent
.
get_el64_symbol_type ent
extracts the symbol type from symbol table entry * ent
.
get_el32_symbol_binding ent
extracts the symbol binding from symbol table entry * ent
.
get_el64_symbol_binding ent
extracts the symbol binding from symbol table entry * ent
.