package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Elf_program_header_table/index.html
Module Elf_program_header_table
Source
elf_program_header_table
contains type, functions and other definitions * for working with program header tables and their entries and ELF segments. * Related files are elf_interpreted_segments
which extracts information * derived from PHTs presented in this file and converts it into a more usable * format for processing. * * FIXME: * Bug in Lem as Lem codebase uses int
type throughout where BigInt.t
* is really needed, hence chokes on huge constants below, which is why they are * written in the way that they are.
Segment types
Unused array element. All other members of the structure are undefined.
A loadable segment.
A loadable segment.
Dynamic linking information.
Dynamic linking information.
Specifies the location and size of a null-terminated path name to be used to * invoke an interpreter.
Specifies the location and size of a null-terminated path name to be used to * invoke an interpreter.
Specifies location and size of auxiliary information.
Specifies location and size of auxiliary information.
Reserved but with unspecified semantics. If the file contains a segment of * this type then it is to be regarded as non-conformant with the ABI.
Reserved but with unspecified semantics. If the file contains a segment of * this type then it is to be regarded as non-conformant with the ABI.
Specifies the location and size of the program header table.
Specifies the location and size of the program header table.
Specifies the thread local storage (TLS) template. Need not be supported.
Specifies the thread local storage (TLS) template. Need not be supported.
Start of reserved indices for operating system specific semantics.
Start of reserved indices for operating system specific semantics.
End of reserved indices for operating system specific semantics.
End of reserved indices for operating system specific semantics.
Start of reserved indices for processor specific semantics.
Start of reserved indices for processor specific semantics.
End of reserved indices for processor specific semantics.
End of reserved indices for processor specific semantics.
val string_of_segment_type :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Nat_big_num.num ->
string
string_of_elf_segment_type os proc st
produces a string representation of * the coding of an ELF segment type st
using os
and proc
to render OS- * and processor-specific codings.
Segments permission flags
Execute bit
Write bit
Write bit
Read bit
Read bit
The following two bit ranges are reserved for OS- and processor-specific * flags respectively.
The following two bit ranges are reserved for OS- and processor-specific * flags respectively.
exact_permission_of_permission m
: ELF has two interpretations of a RWX-style * permission bit m
, an exact permission and an allowable permission. These * permissions allow us to interpret a flag as an upper bound for behaviour and * an ABI-compliant implementation can choose to interpret the flag m
as either. * * In the exact interpretation, the upper bound is exactly the natural interpretation * of the flag. This is encoded in exact_permission_of_permission
, which is * a glorified identity function, though included for completeness.
allowable_permission_of_permission m
: ELF has two interpretations of a RWX-style * permission bit m
, an exact permission and an allowable permission. These * permissions allow us to interpret a flag as an upper bound for behaviour and * an ABI-compliant implementation can choose to interpret the flag m
as either. * * In the allowable interpretation, the upper bound is more lax than the natural * interpretation of the flag.
elf64_interpreted_program_header_flags w
extracts a boolean triple of flags * from the flags field of an interpreted segment.
string_of_elf_segment_permissions m
produces a string-based representation * of an ELF segment's permission field. * TODO: expand this as is needed by the validation tests.
Program header table entry type
type elf32_program_header_table_entry = {
elf32_p_type : Uint32_wrapper.uint32;
(*Type of the segment
*)elf32_p_offset : Uint32_wrapper.uint32;
(*Offset from beginning of file for segment
*)elf32_p_vaddr : Uint32_wrapper.uint32;
(*Virtual address for segment in memory
*)elf32_p_paddr : Uint32_wrapper.uint32;
(*Physical address for segment
*)elf32_p_filesz : Uint32_wrapper.uint32;
(*Size of segment in file, in bytes
*)elf32_p_memsz : Uint32_wrapper.uint32;
(*Size of segment in memory image, in bytes
*)elf32_p_flags : Uint32_wrapper.uint32;
(*Segment flags
*)elf32_p_align : Uint32_wrapper.uint32;
(*Segment alignment memory for memory and file
*)
}
Type elf32_program_header_table_entry
encodes a program header table entry * for 32-bit platforms. Each entry describes a segment in an executable or * shared object file.
val compare_elf32_program_header_table_entry :
elf32_program_header_table_entry ->
elf32_program_header_table_entry ->
int
compare_elf32_program_header_table_entry ent1 ent2
is an ordering-comparison * function on program header table entries suitable for constructing sets, * finite maps, and other ordered data types with.
val instance_Basic_classes_Ord_Elf_program_header_table_elf32_program_header_table_entry_dict :
elf32_program_header_table_entry Lem_basic_classes.ord_class
type elf64_program_header_table_entry = {
elf64_p_type : Uint32_wrapper.uint32;
(*Type of the segment
*)elf64_p_flags : Uint32_wrapper.uint32;
(*Segment flags
*)elf64_p_offset : Uint64_wrapper.uint64;
(*Offset from beginning of file for segment
*)elf64_p_vaddr : Uint64_wrapper.uint64;
(*Virtual address for segment in memory
*)elf64_p_paddr : Uint64_wrapper.uint64;
(*Physical address for segment
*)elf64_p_filesz : Uint64_wrapper.uint64;
(*Size of segment in file, in bytes
*)elf64_p_memsz : Uint64_wrapper.uint64;
(*Size of segment in memory image, in bytes
*)elf64_p_align : Uint64_wrapper.uint64;
(*Segment alignment memory for memory and file
*)
}
Type elf64_program_header_table_entry
encodes a program header table entry * for 64-bit platforms. Each entry describes a segment in an executable or * shared object file.
val compare_elf64_program_header_table_entry :
elf64_program_header_table_entry ->
elf64_program_header_table_entry ->
int
compare_elf64_program_header_table_entry ent1 ent2
is an ordering-comparison * function on program header table entries suitable for constructing sets, * finite maps, and other ordered data types with.
val instance_Basic_classes_Ord_Elf_program_header_table_elf64_program_header_table_entry_dict :
elf64_program_header_table_entry Lem_basic_classes.ord_class
val string_of_elf32_program_header_table_entry :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
elf32_program_header_table_entry ->
string
string_of_elf32_program_header_table_entry os proc et
produces a string * representation of a 32-bit program header table entry using os
and proc
* to render OS- and processor-specific entries.
val string_of_elf64_program_header_table_entry :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
elf64_program_header_table_entry ->
string
string_of_elf64_program_header_table_entry os proc et
produces a string * representation of a 64-bit program header table entry using os
and proc
* to render OS- and processor-specific entries.
val string_of_elf32_program_header_table_entry_default :
elf32_program_header_table_entry ->
string
string_of_elf32_program_header_table_entry_default et
produces a string representation * of table entry et
where OS- and processor-specific entries are replaced with * default strings.
val string_of_elf64_program_header_table_entry_default :
elf64_program_header_table_entry ->
string
string_of_elf64_program_header_table_entry_default et
produces a string representation * of table entry et
where OS- and processor-specific entries are replaced with * default strings.
val instance_Show_Show_Elf_program_header_table_elf32_program_header_table_entry_dict :
elf32_program_header_table_entry Show.show_class
val instance_Show_Show_Elf_program_header_table_elf64_program_header_table_entry_dict :
elf64_program_header_table_entry Show.show_class
Parsing and blitting
val bytes_of_elf32_program_header_table_entry :
Endianness.endianness ->
elf32_program_header_table_entry ->
Byte_sequence_wrapper.byte_sequence
bytes_of_elf32_program_header_table_entry ed ent
blits a 32-bit program * header table entry ent
into a byte sequence assuming endianness ed
.
val bytes_of_elf64_program_header_table_entry :
Endianness.endianness ->
elf64_program_header_table_entry ->
Byte_sequence_wrapper.byte_sequence
bytes_of_elf64_program_header_table_entry ed ent
blits a 64-bit program * header table entry ent
into a byte sequence assuming endianness ed
.
val read_elf32_program_header_table_entry :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf32_program_header_table_entry * Byte_sequence_wrapper.byte_sequence)
Error.error
read_elf32_program_header_table_entry endian bs0
reads an ELF32 program header table * entry from byte sequence bs0
assuming endianness endian
. If bs0
is larger * than necessary, the excess is returned from the function, too. * Fails if the entry cannot be read.
val read_elf64_program_header_table_entry :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf64_program_header_table_entry * Byte_sequence_wrapper.byte_sequence)
Error.error
read_elf64_program_header_table_entry endian bs0
reads an ELF64 program header table * entry from byte sequence bs0
assuming endianness endian
. If bs0
is larger * than necessary, the excess is returned from the function, too. * Fails if the entry cannot be read.
Program header table type
Type elf32_program_header_table
represents a program header table for 32-bit * ELF files. A program header table is an array (implemented as a list, here) * of program header table entries.
Type elf64_program_header_table
represents a program header table for 64-bit * ELF files. A program header table is an array (implemented as a list, here) * of program header table entries.
val bytes_of_elf32_program_header_table :
Endianness.endianness ->
elf32_program_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence
bytes_of_elf32_program_header_table ed tbl
blits an ELF32 program header * table into a byte sequence assuming endianness ed
.
val bytes_of_elf64_program_header_table :
Endianness.endianness ->
elf64_program_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence
bytes_of_elf64_program_header_table ed tbl
blits an ELF64 program header * table into a byte sequence assuming endianness ed
.
val read_elf32_program_header_table' :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
elf32_program_header_table_entry list Error.error
read_elf32_program_header_table' endian bs0
reads an ELF32 program header table from * byte_sequence bs0
assuming endianness endian
. The byte_sequence bs0
is assumed * to have exactly the correct size for the table. For internal use, only. Use * read_elf32_program_header_table
below instead.
val read_elf64_program_header_table' :
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
elf64_program_header_table_entry list Error.error
read_elf64_program_header_table' endian bs0
reads an ELF64 program header table from * byte_sequence bs0
assuming endianness endian
. The byte_sequence bs0
is assumed * to have exactly the correct size for the table. For internal use, only. Use * read_elf32_program_header_table
below instead.
val read_elf32_program_header_table :
Nat_big_num.num ->
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf32_program_header_table_entry list * Byte_sequence_wrapper.byte_sequence)
Error.error
read_elf32_program_header_table table_size endian bs0
reads an ELF32 program header * table from byte_sequence bs0
assuming endianness endian
based on the size (in bytes) passed in via table_size
. * This table_size
argument should be equal to the number of entries in the * table multiplied by the fixed entry size. Bitstring bs0
may be larger than * necessary, in which case the excess is returned.
val read_elf64_program_header_table :
Nat_big_num.num ->
Endianness.endianness ->
Byte_sequence_wrapper.byte_sequence ->
(elf64_program_header_table_entry list * Byte_sequence_wrapper.byte_sequence)
Error.error
read_elf64_program_header_table table_size endian bs0
reads an ELF64 program header * table from byte_sequence bs0
assuming endianness endian
based on the size (in bytes) passed in via table_size
. * This table_size
argument should be equal to the number of entries in the * table multiplied by the fixed entry size. Bitstring bs0
may be larger than * necessary, in which case the excess is returned.
The pht_print_bundle
type is used to tidy up other type signatures. Some of the * top-level string_of_ functions require six or more functions passed to them, * which quickly gets out of hand. This type is used to reduce that complexity. * The first component of the type is an OS specific print function, the second is * a processor specific print function.
val string_of_elf32_program_header_table :
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
elf32_program_header_table_entry list ->
string
string_of_elf32_program_header_table os proc tbl
produces a string representation * of program header table tbl
using os
and proc
to render OS- and processor- * specific entries.
val string_of_elf64_program_header_table :
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
elf64_program_header_table_entry list ->
string
string_of_elf64_program_header_table os proc tbl
produces a string representation * of program header table tbl
using os
and proc
to render OS- and processor- * specific entries.
Static/dynamic linkage
get_elf32_dynamic_linked pht
tests whether an ELF32 file is a dynamically * linked object by traversing the program header table and attempting to find * a header describing a segment with the name of an associated interpreter. * Returns true
if any such header is found, false
--- indicating static * linkage --- otherwise.
get_elf64_dynamic_linked pht
tests whether an ELF64 file is a dynamically * linked object by traversing the program header table and attempting to find * a header describing a segment with the name of an associated interpreter. * Returns true
if any such header is found, false
--- indicating static * linkage --- otherwise.
get_elf32_static_linked
is a utility function defined as the inverse * of get_elf32_dynamic_linked
.
get_elf64_static_linked
is a utility function defined as the inverse * of get_elf64_dynamic_linked
.
val get_elf32_requested_interpreter :
elf32_program_header_table_entry ->
Byte_sequence_wrapper.byte_sequence ->
string Error.error
get_elf32_requested_interpreter ent bs0
extracts the requested interpreter * of a dynamically linkable ELF file from that file's program header table * entry of type PT_INTERP, ent
. Interpreter string is extracted from byte * sequence bs0
. * Fails if ent
is not of type PT_INTERP, or if transcription otherwise fails.
val get_elf64_requested_interpreter :
elf64_program_header_table_entry ->
Byte_sequence_wrapper.byte_sequence ->
string Error.error
get_elf64_requested_interpreter ent bs0
extracts the requested interpreter * of a dynamically linkable ELF file from that file's program header table * entry of type PT_INTERP, ent
. Interpreter string is extracted from byte * sequence bs0
. * Fails if ent
is not of type PT_INTERP, or if transcription otherwise fails.