package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Elf_file/index.html
Module Elf_file
Source
Module elf_file
packages all components of an ELF file up into a single * record, provides I/O routines for this record, as well as other utility * functions that operate on an entire ELF file.
type elf32_file = {
elf32_file_header : Elf_header.elf32_header;
(*The file header.
*)elf32_file_program_header_table : Elf_program_header_table.elf32_program_header_table;
(*The program header table.
*)elf32_file_section_header_table : Elf_section_header_table.elf32_section_header_table;
(*The section header table.
*)elf32_file_interpreted_segments : Elf_interpreted_segment.elf32_interpreted_segments;
(*A more usable interpretation of the file's segments.
*)elf32_file_interpreted_sections : Elf_interpreted_section.elf32_interpreted_sections;
(*A more usable interpretation of the file's sections.
*)elf32_file_bits_and_bobs : (Nat_big_num.num * Byte_sequence.byte_sequence0) list;
(*The uninterpreted "rubbish" that may appear in gaps in the binary file.
*)
}
elf32_file
record captures the internal structure of an ELF32 file. * Invariant: length of the program header and section header tables should match * the length of their interpreted counterparts, and the nth element of the * (program/section) header table must correspond to the nth element of the * interpreted (segments/sections), respectively.
bytes_of_elf32_file f1
blits ELF file f1
to a byte sequence, ready for * writing to a binary file. Fails if the invariant on elf32_file
mentioned * above is not respected.
type elf64_file = {
elf64_file_header : Elf_header.elf64_header;
(*The file header.
*)elf64_file_program_header_table : Elf_program_header_table.elf64_program_header_table;
(*The program header table.
*)elf64_file_section_header_table : Elf_section_header_table.elf64_section_header_table;
(*The section header table.
*)elf64_file_interpreted_segments : Elf_interpreted_segment.elf64_interpreted_segments;
(*A more usable interpretation of the file's segments.
*)elf64_file_interpreted_sections : Elf_interpreted_section.elf64_interpreted_sections;
(*A more usable interpretation of the file's sections.
*)elf64_file_bits_and_bobs : (Nat_big_num.num * Byte_sequence.byte_sequence0) list;
(*The uninterpreted "rubbish" that may appear in gaps in the binary file.
*)
}
elf64_file
record captures the internal structure of an ELF32 file. * Invariant: length of the program header and section header tables should match * the length of their interpreted counterparts, and the nth element of the * (program/section) header table must correspond to the nth element of the * interpreted (segments/sections), respectively.
bytes_of_elf64_file f1
blits ELF file f1
to a byte sequence, ready for * writing to a binary file. Fails if the invariant on elf64_file
mentioned * above is not respected.
val obtain_elf32_program_header_table :
Elf_header.elf32_header ->
Byte_sequence_wrapper.byte_sequence ->
Elf_program_header_table.elf32_program_header_table_entry list Error.error
obtain_elf32_program_header_table hdr bs0
reads a file's program header table * from byte sequence bs0
using information gleaned from the file header hdr
. * Fails if transcription fails.
val obtain_elf64_program_header_table :
Elf_header.elf64_header ->
Byte_sequence_wrapper.byte_sequence ->
Elf_program_header_table.elf64_program_header_table_entry list Error.error
obtain_elf64_program_header_table hdr bs0
reads a file's program header table * from byte sequence bs0
using information gleaned from the file header hdr
. * Fails if transcription fails.
val obtain_elf32_section_header_table :
Elf_header.elf32_header ->
Byte_sequence_wrapper.byte_sequence ->
Elf_section_header_table.elf32_section_header_table_entry list Error.error
obtain_elf32_section_header_table hdr bs0
reads a file's section header table * from byte sequence bs0
using information gleaned from the file header hdr
. * Fails if transcription fails.
val obtain_elf64_section_header_table :
Elf_header.elf64_header ->
Byte_sequence_wrapper.byte_sequence ->
Elf_section_header_table.elf64_section_header_table_entry list Error.error
obtain_elf64_section_header_table hdr bs0
reads a file's section header table * from byte sequence bs0
using information gleaned from the file header hdr
. * Fails if transcription fails.
val obtain_elf32_section_header_string_table :
Elf_header.elf32_header ->
Elf_section_header_table.elf32_section_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
String_table.string_table option Error.error
obtain_elf32_section_header_string_table hdr sht bs0
reads a file's section * header string table from byte sequence bs0
using information gleaned from * the file header hdr
and section header table sht
. * Fails if transcription fails.
val obtain_elf64_section_header_string_table :
Elf_header.elf64_header ->
Elf_section_header_table.elf64_section_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
String_table.string_table option Error.error
obtain_elf64_section_header_string_table hdr sht bs0
reads a file's section * header string table from byte sequence bs0
using information gleaned from * the file header hdr
and section header table sht
. * Fails if transcription fails.
val obtain_elf32_interpreted_segments :
Elf_program_header_table.elf32_program_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
Elf_interpreted_segment.elf32_interpreted_segment list Error.error
obtain_elf32_interpreted_segments pht bs0
generates the interpreted segments * of an ELF file from the uninterpreted program header table entries in pht
, * read from byte sequence bs0
. Makes working with segments easier. * May fail if transcription of any segment fails.
val obtain_elf64_interpreted_segments :
Elf_program_header_table.elf64_program_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
Elf_interpreted_segment.elf64_interpreted_segment list Error.error
obtain_elf64_interpreted_segments pht bs0
generates the interpreted segments * of an ELF file from the uninterpreted program header table entries in pht
, * read from byte sequence bs0
. Makes working with segments easier. * May fail if transcription of any segment fails.
val obtain_elf32_interpreted_sections :
String_table.string_table option ->
Elf_section_header_table.elf32_section_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
Elf_interpreted_section.elf32_interpreted_section list Error.error
obtain_elf32_interpreted_section sht bs0
generates the interpreted sections * of an ELF file from the uninterpreted section header table entries in sht
, * read from byte sequence bs0
. Makes working with sections easier. * May fail if transcription of any section fails.
val obtain_elf64_interpreted_sections :
String_table.string_table option ->
Elf_section_header_table.elf64_section_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
Elf_interpreted_section.elf64_interpreted_section list Error.error
obtain_elf64_interpreted_section sht bs0
generates the interpreted sections * of an ELF file from the uninterpreted section header table entries in sht
, * read from byte sequence bs0
. Makes working with sections easier. * May fail if transcription of any section fails.
val find_first_not_in_range :
Nat_big_num.num ->
(Nat_big_num.num * Nat_big_num.num) list ->
Nat_big_num.num
find_first_not_in_range e rngs
for every pair (start, end) in rngs
, finds * the first element, beginning counting from e
, that does not lie between * a start and end value.
val find_first_in_range :
Nat_big_num.num ->
(Nat_big_num.num * Nat_big_num.num) list ->
Nat_big_num.num
find_first_in_range e rngs
for every pair (start, end) in rngs
, finds * the first element, beginning counting from e
, that lies between * a start and end value.
val compute_differences :
Nat_big_num.num ->
Nat_big_num.num ->
(Nat_big_num.num * Nat_big_num.num) list ->
(Nat_big_num.num * Nat_big_num.num) list Error.error
compute_differences start max ranges
is a utility function used for calculating * "dead" spots in an ELF file not covered by any of the interpreted structure * that nevertheless need recording in the bits_and_bobs field of each ELF record * in order to maintain in-out roundtripping up to exact binary equivalence.
val obtain_elf32_bits_and_bobs :
Elf_header.elf32_header ->
Elf_program_header_table.elf32_program_header_table_entry list ->
Elf_interpreted_segment.elf32_interpreted_segment list ->
Elf_section_header_table.elf32_section_header_table_entry list ->
Elf_interpreted_section.elf32_interpreted_section list ->
Byte_sequence_wrapper.byte_sequence ->
(Nat_big_num.num * Byte_sequence_wrapper.byte_sequence) list Error.error
obtain_elf32_bits_and_bobs hdr pht segs sht sects bs0
identifies and records * the "dead" spots of an ELF file not covered by any meaningful structure of the * ELF file format.
val obtain_elf64_bits_and_bobs :
Elf_header.elf64_header ->
Elf_program_header_table.elf64_program_header_table_entry list ->
Elf_interpreted_segment.elf64_interpreted_segment list ->
Elf_section_header_table.elf64_section_header_table_entry list ->
Elf_interpreted_section.elf64_interpreted_section list ->
Byte_sequence_wrapper.byte_sequence ->
(Nat_big_num.num * Byte_sequence_wrapper.byte_sequence) list Error.error
obtain_elf64_bits_and_bobs hdr pht segs sht sects bs0
identifies and records * the "dead" spots of an ELF file not covered by any meaningful structure of the * ELF file format.
read_elf32_file bs0
reads an ELF32 file from byte sequence bs0
. Fails if * transcription fails.
read_elf64_file bs0
reads an ELF64 file from byte sequence bs0
. Fails if * transcription fails.
val get_elf32_file_section_header_string_table :
elf32_file ->
String_table.string_table Error.error
get_elf32_file_secton_header_string_table f1
returns the ELF file, f1
, * section header string table. * TODO: why is this not using obtain_elf32_section_header_string_table above?
val get_elf64_file_section_header_string_table :
elf64_file ->
String_table.string_table Error.error
get_elf64_file_secton_header_string_table f1
returns the ELF file, f1
, * section header string table. * TODO: why is this not using obtain_elf64_section_header_string_table above?
val find_elf32_symbols_by_symtab_idx :
Nat_big_num.num ->
elf32_file ->
(Elf_symbol_table.elf32_symbol_table_entry list
* String_table.string_table
* Nat_big_num.num)
Error.error
val find_elf32_symtab_by_type :
Nat_big_num.num ->
elf32_file ->
(Elf_symbol_table.elf32_symbol_table
* String_table.string_table
* Nat_big_num.num)
Error.error
val find_elf64_symbols_by_symtab_idx :
Nat_big_num.num ->
elf64_file ->
(Elf_symbol_table.elf64_symbol_table_entry list
* String_table.string_table
* Nat_big_num.num)
Error.error
val find_elf64_symtab_by_type :
Nat_big_num.num ->
elf64_file ->
(Elf_symbol_table.elf64_symbol_table
* String_table.string_table
* Nat_big_num.num)
Error.error
get_elf32_file_symbol_string_table f1
returns the ELF file f1
symbol * string table. May fail.
get_elf64_file_symbol_string_table f1
returns the ELF file f1
symbol * string table. May fail.
val get_elf32_string_table_by_index :
elf32_file ->
Nat_big_num.num ->
String_table.string_table Error.error
get_elf32_file_string_table_by_index f1 index
returns the ELF file f1
* string table that is pointed to by the section header table entry at index * index
. May fail if index is out of range, or otherwise.
val get_elf64_string_table_by_index :
elf64_file ->
Nat_big_num.num ->
String_table.string_table Error.error
get_elf64_file_string_table_by_index f1 index
returns the ELF file f1
* string table that is pointed to by the section header table entry at index * index
. May fail if index is out of range, or otherwise.
val get_elf32_file_symbol_table :
elf32_file ->
Elf_symbol_table.elf32_symbol_table_entry list Error.error
get_elf32_file_symbol_table f1
returns the ELF file f1
symbol * table. May fail.
val get_elf64_file_symbol_table :
elf64_file ->
(Elf_symbol_table.elf64_symbol_table_entry list * String_table.string_table)
Error.error
get_elf64_file_symbol_table f1
returns the ELF file f1
symbol * table. May fail.
val get_elf32_file_dynamic_symbol_table :
elf32_file ->
Elf_symbol_table.elf32_symbol_table_entry list Error.error
get_elf32_file_dynamic_symbol_table f1
returns the ELF file f1
dynamic * symbol table. May fail.
val get_elf64_file_dynamic_symbol_table :
elf64_file ->
Elf_symbol_table.elf64_symbol_table_entry list Error.error
get_elf64_file_dynamic_symbol_table f1
returns the ELF file f1
dynamic * symbol table. May fail.
val get_elf32_symbol_table_by_index :
elf32_file ->
Nat_big_num.num ->
Elf_symbol_table.elf32_symbol_table Error.error
get_elf32_file_symbol_table_by_index f1 index
returns the ELF file f1
* symbol table that is pointed to by the section header table entry at index * index
. May fail if index is out of range, or otherwise.
val get_elf64_symbol_table_by_index :
elf64_file ->
Nat_big_num.num ->
Elf_symbol_table.elf64_symbol_table Error.error
get_elf64_file_symbol_table_by_index f1 index
returns the ELF file f1
* symbol table that is pointed to by the section header table entry at index * index
. May fail if index is out of range, or otherwise.
segment_provenance
records whether a segment that appears in an executable * process image has been derived directly from an ELF file, or was automatically * created when the image calculation process noticed a segment with a memory * size greater than its file size. * Really a PPCMemism and not strictly needed for the ELF model itself.
type elf32_executable_process_image =
(Elf_interpreted_segment.elf32_interpreted_segment * segment_provenance) list
* Nat_big_num.num
* Nat_big_num.num
elf32_executable_process_image
is a process image for ELF32 files. Contains * all that is necessary to load the executable components of an ELF32 file * and begin execution. * XXX: (segments, provenance), entry point, machine type
type elf64_executable_process_image =
(Elf_interpreted_segment.elf64_interpreted_segment * segment_provenance) list
* Nat_big_num.num
* Nat_big_num.num
elf64_executable_process_image
is a process image for ELF64 files. Contains * all that is necessary to load the executable components of an ELF64 file * and begin execution. * XXX: (segments, provenance), entry point, machine type
val get_elf32_executable_image :
elf32_file ->
((Elf_interpreted_segment.elf32_interpreted_segment * segment_provenance)
list
* Nat_big_num.num
* Nat_big_num.num)
Error.error
get_elf32_executable_image f1
extracts an executable process image from an * executable ELF file. May fail if extraction is impossible.
val get_elf64_executable_image :
elf64_file ->
((Elf_interpreted_segment.elf64_interpreted_segment * segment_provenance)
list
* Nat_big_num.num
* Nat_big_num.num)
Error.error
get_elf64_executable_image f1
extracts an executable process image from an * executable ELF file. May fail if extraction is impossible.
type global_symbol_init_info =
(string
* (Nat_big_num.num
* Nat_big_num.num
* Nat_big_num.num
* Byte_sequence.byte_sequence0 option
* Nat_big_num.num))
list
global_symbol_init_info
records the name, type, size, address, chunk * of initialisation data (if relevant for that symbol), and binding, of every * global symbol in an ELF file. * Another PPCMemism.
val get_elf32_file_global_symbol_init :
elf32_file ->
(string
* (Nat_big_num.num
* Nat_big_num.num
* Nat_big_num.num
* Byte_sequence_wrapper.byte_sequence option
* Nat_big_num.num))
list
Error.error
get_elf32_file_global_symbol_init f1
extracts the global symbol init info * for ELF file f1
. May fail.
val get_elf64_file_global_symbol_init :
elf64_file ->
(string
* (Nat_big_num.num
* Nat_big_num.num
* Nat_big_num.num
* Byte_sequence_wrapper.byte_sequence option
* Nat_big_num.num))
list
Error.error
get_elf64_file_global_symbol_init f1
extracts the global symbol init info * for ELF file f1
. May fail.
val string_of_elf32_file :
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
((Nat_big_num.num ->
string)
* (Nat_big_num.num ->
string)
* (Nat_big_num.num ->
string)) ->
elf32_file ->
string
string_of_elf32_file hdr_bdl pht_bdl sht_bdl f1
produces a string-based * representation of ELF file f1
using ABI-specific print bundles hdr_bdl
, * pht_bdl
and sht_bdl
.
val string_of_elf64_file :
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
((Nat_big_num.num ->
string)
* (Nat_big_num.num ->
string)
* (Nat_big_num.num ->
string)) ->
elf64_file ->
string
string_of_elf64_file hdr_bdl pht_bdl sht_bdl f1
produces a string-based * representation of ELF file f1
using ABI-specific print bundles hdr_bdl
, * pht_bdl
and sht_bdl
.
flag_is_set flag v
checks whether flag flag
is set in v
. * TODO: move elsewhere. Check whether this is still being used.