package linksem

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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?

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?

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.

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.

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.

get_elf32_file_symbol_table f1 returns the ELF file f1 symbol * table. May fail.

get_elf64_file_symbol_table f1 returns the ELF file f1 symbol * table. May fail.

get_elf32_file_dynamic_symbol_table f1 returns the ELF file f1 dynamic * symbol table. May fail.

get_elf64_file_dynamic_symbol_table f1 returns the ELF file f1 dynamic * symbol table. May fail.

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.

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.

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

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

get_elf32_executable_image f1 extracts an executable process image from an * executable ELF file. May fail if extraction is impossible.

get_elf64_executable_image f1 extracts an executable process image from an * executable ELF file. May fail if extraction is impossible.

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.

get_elf32_file_global_symbol_init f1 extracts the global symbol init info * for ELF file f1. May fail.

get_elf64_file_global_symbol_init f1 extracts the global symbol init info * for ELF file f1. May fail.

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.

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.