is_elf32_valid_program_header_table_for_dynamic_linking pht checks whether * a program header table pht is a valid program header table for an ELF file * that will be potentially dynamically linked. Returns true if there is exactly * one segment header of type elf_pt_interp, i.e. contains a string pointing * to the requested dynamic interpreter.

is_elf64_valid_program_header_table_for_dynamic_linking pht checks whether * a program header table pht is a valid program header table for an ELF file * that will be potentially dynamically linked. Returns true if there is exactly * one segment header of type elf_pt_interp, i.e. contains a string pointing * to the requested dynamic interpreter.

dyn_union represents the C-union type used in the definition of elf32_dyn * and elf64_dyn types below. Some section tags correspond to entries where * the fields are either unspecified or ignored, hence the presence of the * D_Ignored constructor.

elf32_dyn captures the notion of an ELF32 dynamic section entry. * Specialises the dyn_union type above to using elf32_word values and * elf32_addr pointers.

elf64_dyn captures the notion of an ELF32 dynamic section entry. * Specialises the dyn_union type above to using elf64_xword values and * elf64_addr pointers.

dt_null marks the end of the dynamic array

dt_needed holds the string table offset of a string containing the name of * a needed library.

dt_needed holds the string table offset of a string containing the name of * a needed library.

dt_pltrelsz holds the size in bytes of relocation entries associated with * the PLT.

dt_pltrelsz holds the size in bytes of relocation entries associated with * the PLT.

dt_pltgot holds an address associated with the PLT or GOT.

dt_pltgot holds an address associated with the PLT or GOT.

dt_hash holds the address of a symbol-table hash.

dt_hash holds the address of a symbol-table hash.

dt_strtab holds the address of the string table.

dt_strtab holds the address of the string table.

dt_symtab holds the address of a symbol table.

dt_symtab holds the address of a symbol table.

dt_rela holds the address of a relocation table.

dt_rela holds the address of a relocation table.

dt_relasz holds the size in bytes of the relocation table.

dt_relasz holds the size in bytes of the relocation table.

dt_relaent holds the size in bytes of a relocation table entry.

dt_relaent holds the size in bytes of a relocation table entry.

dt_strsz holds the size in bytes of the string table.

dt_strsz holds the size in bytes of the string table.

dt_syment holds the size in bytes of a symbol table entry.

dt_syment holds the size in bytes of a symbol table entry.

dt_init holds the address of the initialisation function.

dt_init holds the address of the initialisation function.

dt_fini holds the address of the finalisation function.

dt_fini holds the address of the finalisation function.

dt_soname holds the string table offset of a string containing the shared- * object name.

dt_soname holds the string table offset of a string containing the shared- * object name.

dt_rpath holds the string table offset of a string containing the library * search path.

dt_rpath holds the string table offset of a string containing the library * search path.

dt_symbolic alters the linker's symbol resolution algorithm so that names * are resolved first from the shared object file itself, rather than the * executable file.

dt_symbolic alters the linker's symbol resolution algorithm so that names * are resolved first from the shared object file itself, rather than the * executable file.

dt_rel is similar to dt_rela except its table has implicit addends.

dt_rel is similar to dt_rela except its table has implicit addends.

dt_relsz holds the size in bytes of the dt_rel relocation table.

dt_relsz holds the size in bytes of the dt_rel relocation table.

dt_relent holds the size in bytes of a dt_rel relocation entry.

dt_relent holds the size in bytes of a dt_rel relocation entry.

dt_pltrel specifies the type of relocation entry to which the PLT refers.

dt_pltrel specifies the type of relocation entry to which the PLT refers.

dt_debug is used for debugging and its purpose is not specified in the ABI. * Programs using this entry are not ABI-conformant.

dt_debug is used for debugging and its purpose is not specified in the ABI. * Programs using this entry are not ABI-conformant.

dt_textrel absence of this entry indicates that no relocation entry should * cause a modification to a non-writable segment. Otherwise, if present, one * or more relocation entries may request modifications to a non-writable * segment.

dt_textrel absence of this entry indicates that no relocation entry should * cause a modification to a non-writable segment. Otherwise, if present, one * or more relocation entries may request modifications to a non-writable * segment.

dt_jmprel's member holds the address of relocation entries associated with * the PLT.

dt_jmprel's member holds the address of relocation entries associated with * the PLT.

dt_bindnow instructs the linker to process all relocations for the object * containing the entry before transferring control to the program.

dt_bindnow instructs the linker to process all relocations for the object * containing the entry before transferring control to the program.

dt_init_array holds the address to the array of pointers to initialisation * functions.

dt_init_array holds the address to the array of pointers to initialisation * functions.

dt_fini_array holds the address to the array of pointers to finalisation * functions.

dt_fini_array holds the address to the array of pointers to finalisation * functions.

dt_init_arraysz holds the size in bytes of the array of pointers to * initialisation functions.

dt_init_arraysz holds the size in bytes of the array of pointers to * initialisation functions.

dt_fini_arraysz holds the size in bytes of the array of pointers to * finalisation functions.

dt_fini_arraysz holds the size in bytes of the array of pointers to * finalisation functions.

dt_runpath holds an offset into the string table holding a string containing * the library search path.

dt_runpath holds an offset into the string table holding a string containing * the library search path.

dt_flags holds flag values specific to the object being loaded.

dt_flags holds flag values specific to the object being loaded.

dt_preinit_array holds the address to the array of pointers of pre- * initialisation functions.

dt_preinit_array holds the address to the array of pointers of pre- * initialisation functions.

dt_preinit_arraysz holds the size in bytes of the array of pointers of * pre-initialisation functions.

dt_preinit_arraysz holds the size in bytes of the array of pointers of * pre-initialisation functions.

dt_loos and dt_hios: this inclusive range is reserved for OS-specific * semantics.

dt_loos and dt_hios: this inclusive range is reserved for OS-specific * semantics.

dt_loproc and dt_hiproc: this inclusive range is reserved for processor * specific semantics.

dt_loproc and dt_hiproc: this inclusive range is reserved for processor * specific semantics.

string_of_dynamic_tag so t os proc produces a string-based representation of * dynamic section tag t. For tag values between LO_OS and HI_OS os is * used to produce the resulting value. For tag values between LO_PROC and * HI_PROC proc is used to produce the resulting value. Boolean flag so * indicates whether the flag in question is derived from a shared object file, * which alters the printing of ENCODING and PRE_INITARRAY flags.

tag_correspondence is a type used to emulate the functionality of a C-union * in Lem. The type records whether the union should be interpreted as a value, * a pointer, or a "do not care" value. An accompanying function will map a * dynamic section tag to a tag_correspondence, so that transcription functions * know how to properly use the dyn_union value in a dynamic section entry.

tag_correspondence_of_tag tag os_additional_ranges os proc produces a * tag_correspondence value for a given dynamic tag, tag. Some tag values * are reserved for interpretation by the OS or processor supplement (i.e. the * ABI). We therefore also take in a predicate, os_additional_ranges, that * recognises when a tag is "special" for a given ABI, and a means of interpreting * that tag, using os and proc functions.

read_elf32_dyn endian bs0 so os_additional_ranges os proc reads an elf32_dyn * record from byte sequence bs0, assuming endianness endian. As mentioned * above some ABIs reserve additional tag values for their own purposes. These * are recognised by the predicate os_additional_ranges and interpreted by * the functions os and proc. Fails if the transcription of the record from * bs0 fails, or if os or proc fail.

read_elf64_dyn endian bs0 os_additional_ranges os proc reads an elf64_dyn * record from byte sequence bs0, assuming endianness endian. As mentioned * above some ABIs reserve additional tag values for their own purposes. These * are recognised by the predicate os_additional_ranges and interpreted by * the functions os and proc. Fails if the transcription of the record from * bs0 fails, or if os or proc fail.

obtain_elf32_dynamic_section_contents' endian bs0 os_additional_ranges os * proc exhaustively reads in elf32_dyn values from byte sequence bs0, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf32_dyn entry is not 0.

obtain_elf64_dynamic_section_contents' endian bs0 os_additional_ranges os * proc exhaustively reads in elf64_dyn values from byte sequence bs0, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf64_dyn entry is not 0.

obtain_elf32_dynamic_section_contents' f1 os_additional_ranges os * proc bs0 exhaustively reads in elf32_dyn values from byte sequence bs0, * obtaining endianness and the section header table from elf32_file f1, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf32_dyn entry is not 0.

obtain_elf64_dynamic_section_contents' f1 os_additional_ranges os * proc bs0 exhaustively reads in elf64_dyn values from byte sequence bs0, * obtaining endianness and the section header table from elf64_file f1, * interpreting ABI-specific dynamic tags with os_additional_ranges, os, and * proc as mentioned above. Fails if bs0's length modulo the size of an * elf64_dyn entry is not 0.

df_origin specific that the object being loaded may make reference to the * $(ORIGIN) substitution string.

df_symbolic changes the linker's symbol resolution algorithm, resolving * symbols first from the shared object file rather than the executable file.

df_symbolic changes the linker's symbol resolution algorithm, resolving * symbols first from the shared object file rather than the executable file.

df_textrel if this flag is not set then no relocation entry should cause * modification to a non-writable segment.

df_textrel if this flag is not set then no relocation entry should cause * modification to a non-writable segment.

df_bindnow if set this instructs the linker to process all relocation entries * of the containing object before transferring control to the program.

df_bindnow if set this instructs the linker to process all relocation entries * of the containing object before transferring control to the program.

df_static_tls if set instructs the linker to reject all attempts to load * the containing file dynamically.

df_static_tls if set instructs the linker to reject all attempts to load * the containing file dynamically.

check_flag is a utility function for testing whether a flag is set. * TODO: so simple it is probably unneccessary now.

string_of_dt_flag f produces a string-based representation of dynamic * section flag f.

rel_type represents the two types of relocation records potentially present * in an ELF file: relocation, and relocation with addends.

string_of_rel_type r produces a string-based representation of rel_type, * r.

Type dyn_value represents the value of an ELF dynamic section entry. Values * can represent various different types of objects (e.g. paths to libraries, or * flags, or sizes of other entries in a file), and this type collates them all. * Parameterised over two type variables so the type can be shared between ELF32 * and ELF64.

elf32_dyn_value and elf64_dyn_value are specialisations of dyn_value * fixing the correct types for the 'addr and 'size type variables.

get_string_table_of_elf32_dyn_section endian dyns sht bs0 searches through * dynamic section entries dyns looking for one pointing to a string table, looks * up the corresponding section header sht pointed to by that dynamic * section entry, finds the section in bs0 and decodes a string table from that * section assuming endianness endian. May fail.

get_string_table_of_elf64_dyn_section endian dyns sht bs0 searches through * dynamic section entries dyns looking for one pointing to a string table, looks * up the corresponding section header sht pointed to by that dynamic * section entry, finds the section in bs0 and decodes a string table from that * section assuming endianness endian. May fail.

get_value_of_elf32_dyn so dyn os_additional_ranges os proc stab returns the value * stored in a dynamic section entry dyn, using os_additional_ranges and * os to decode ABI-reserved tags. String table stab is used to correctly * decode library and run paths, etc. * May fail.

get_value_of_elf64_dyn dyn os_additional_ranges os proc stab returns the value * stored in a dynamic section entry dyn, using os_additional_ranges and * os to decode ABI-reserved tags. String table stab is used to correctly * decode library and run paths, etc. * May fail.