Abi_aarch64_leabi_aarch64_le contains top-level definition for the AArch64 ABI (little-endian case).
Abi_aarch64_le_elf_headerabi_aarch64_le_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AArch64 ABI (little-endian).
Abi_aarch64_le_serialisationabi_aarch64_le_serialisation, code for producing an AARCH64 conformant * ELF binary file from executable (machine code) data. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_aarch64_program_header_tableabi_aarch64_program_header_table, AARCH64 ABI specific program header * table related flags, data, etc.
Abi_aarch64_relocationabi_aarch64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AArch64 ABI (little-endian case).
Abi_aarch64_section_header_tableabi_aarch64_section_header_table, AARCH64 ABI specific definitions related * to the section header table.
Abi_aarch64_symbol_tableabi_aarch64_symbol_table, symbol table specific defintions for the AARCH64 * ABI.
Abi_amd64abi_amd64 contains top-level definition for the AMD64 ABI.
Abi_amd64_elf_headerabi_amd64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AMD64 ABI.
Abi_amd64_program_header_tableabi_amd64_program_header_table, program header table specific definitions * for the AMD64 ABI.
Abi_amd64_relocationabi_amd64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AMD64 ABI.
Abi_amd64_section_header_tableabi_amd64_section_header_table module contains section header table * specific definitions for the AMD64 ABI.
Abi_amd64_serialisationabi_amd64_serialisation contains code for producing an AMD64 conformant * ELF file from executable (machine) code. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_amd64_symbol_tableabi_amd64_symbol_table, AMD64 ABI specific definitions for the ELF symbol * table.
Abi_mips64_elf_headerabi_mips64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the MIPS64 ABI.
Abi_mips64_program_header_tableabi_mips64_program_header_table, program header table specific definitions * for the MIPS64 ABI.
Abi_mips64_relocationabi_mips64_relocation contains types and definitions relating to ABI * specific relocation functionality for the MIPS64 ABI.
Abi_mips64_section_header_tableabi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
Abi_mips64_serialisationabi_mips64_serialisation contains code for producing an MIPS64 conformant * ELF file from executable (machine) code. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_mips64_symbol_tableabi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
Abi_power64abi_power64 contains top-level definition for the PowerPC64 ABI.
Abi_power64_elf_headerabi_power64_elf_header, Power64 ABI specific definitions related to the * ELF file header.
Abi_power64_relocationabi_power64_relocation contains types and definitions specific to * relocations in the Power64 ABI
Abi_power64_section_header_tableabi_power64_section_header_table contains Power64 ABI specific definitions * related to the section header table.
Abi_riscvabi_riscv contains top-level definition for the RISCV ABI.
Abi_riscv_elf_headerabi_riscv_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the RISCV ABI.
Abi_riscv_program_header_tableabi_riscv_program_header_table, program header table specific definitions * for the RISCV ABI.
Abi_riscv_relocationabi_riscv_relocation contains types and definitions relating to ABI * specific relocation functionality for the RISCV ABI.
Abi_riscv_section_header_tableabi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
Abi_riscv_serialisationabi_riscv_serialisation contains code for producing an RISCV conformant * ELF file from executable (machine) code. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_riscv_symbol_tableabi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
Abi_utilitiesabi_utilities, generic utilities shared between all ABIs.
Abi_x86_relocationabi_x86_relocation contains X86 ABI specific definitions relating to * relocations.
AbisThe abis module is the top-level module for all ABI related code, including * some generic functionality that works across all ABIs, and a primitive attempt * at abstracting over ABIs for purposes of linking.
Elf_dynamicelf_dynamic module exports types and definitions relating to the dynamic * section and dynamic linking functionality of an ELF file.
Elf_fileModule 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.
Elf_headerelf_header includes types, functions and other definitions for working with * ELF headers.
Elf_interpreted_sectionModule elf_interpreted_section provides a record of "interpreted" sections, * i.e. the data stored in the section header table converted to more amenable * infinite precision types, and operation on those records.
Elf_interpreted_segmentelf_interpreted_segment defines interpreted segments, i.e. the contents of * a program header table entry converted to more amenable types, and operations * built on top of them.
Elf_noteelf_note contains data types and functions for interpreting the .note * section/segment of an ELF file, and extracting information from that * section/segment.
Elf_program_header_tableelf_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.
Elf_relocationelf_relocation formalises types, functions and other definitions for working * with ELF relocation and relocation with addend entries.
Elf_section_header_tableelf_section_header_table provides types, functions and other definitions * for working with section header tables and their entries.
Elf_symbol_tableelf_symbol_table provides types, functions and other definitions for * working with ELF symbol tables.
Gnu_ext_dynamicgnu_ext_dynamic contains GNU extension specific definitions related to the * .dynamic section of an ELF file.
Gnu_ext_notegnu_ext_note contains GNU extension specific definitions relating to the * .note section/segment of an ELF file.
Gnu_ext_program_header_tablegnu_ext_program_header_table contains GNU extension specific functionality * related to the program header table.
Gnu_ext_section_header_tableThe module gnu_ext_section_header_table implements function, definitions * and types relating to the GNU extensions to the standard ELF section header * table.
Gnu_ext_section_to_segment_mappinggnu_ext_section_to_segment_mapping contains (GNU specific) functionality * relating to calculating the section to segment mapping for an ELF file. In * particular, the test over whether a section is inside a segment is ABI * specific. This module provides that test.
Gnu_ext_symbol_versioningThe gnu_ext_symbol_versioning defines constants, types and functions * relating to the GNU symbol versioning extensions (i.e. contents of * GNU_VERSYM sections). * * TODO: work out what is going on with symbol versioning. The specification * is completely opaque.
Gnu_ext_types_native_uintgnu_ext_types_native_uint provides extended types defined by the GNU * extensions over and above the based ELF types.
Hex_printinghex_printing is a utility module for converting natural numbers and integers * into hex strings of various widths. Split into a new module as both the * validation code and the main program need this functionality.
Showshow.lem exports the typeclass Show and associated functions for pretty * printing arbitrary values.
String_tableThe string_table module implements string tables. An ELF file may have * multiple different string tables used for different purposes. A string * table is a string coupled with a delimiting character. Strings may be indexed * at any position, not necessarily on a delimiter boundary.
Abi_aarch64_leabi_aarch64_le contains top-level definition for the AArch64 ABI (little-endian case).
Abi_aarch64_le_elf_headerabi_aarch64_le_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AArch64 ABI (little-endian).
Abi_aarch64_le_serialisationabi_aarch64_le_serialisation, code for producing an AARCH64 conformant * ELF binary file from executable (machine code) data. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_aarch64_program_header_tableabi_aarch64_program_header_table, AARCH64 ABI specific program header * table related flags, data, etc.
Abi_aarch64_relocationabi_aarch64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AArch64 ABI (little-endian case).
Abi_aarch64_section_header_tableabi_aarch64_section_header_table, AARCH64 ABI specific definitions related * to the section header table.
Abi_aarch64_symbol_tableabi_aarch64_symbol_table, symbol table specific defintions for the AARCH64 * ABI.
Abi_amd64abi_amd64 contains top-level definition for the AMD64 ABI.
Abi_amd64_elf_headerabi_amd64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AMD64 ABI.
Abi_amd64_program_header_tableabi_amd64_program_header_table, program header table specific definitions * for the AMD64 ABI.
Abi_amd64_relocationabi_amd64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AMD64 ABI.
Abi_amd64_section_header_tableabi_amd64_section_header_table module contains section header table * specific definitions for the AMD64 ABI.
Abi_amd64_serialisationabi_amd64_serialisation contains code for producing an AMD64 conformant * ELF file from executable (machine) code. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_amd64_symbol_tableabi_amd64_symbol_table, AMD64 ABI specific definitions for the ELF symbol * table.
Abi_mips64_elf_headerabi_mips64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the MIPS64 ABI.
Abi_mips64_program_header_tableabi_mips64_program_header_table, program header table specific definitions * for the MIPS64 ABI.
Abi_mips64_relocationabi_mips64_relocation contains types and definitions relating to ABI * specific relocation functionality for the MIPS64 ABI.
Abi_mips64_section_header_tableabi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
Abi_mips64_serialisationabi_mips64_serialisation contains code for producing an MIPS64 conformant * ELF file from executable (machine) code. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_mips64_symbol_tableabi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
Abi_power64abi_power64 contains top-level definition for the PowerPC64 ABI.
Abi_power64_elf_headerabi_power64_elf_header, Power64 ABI specific definitions related to the * ELF file header.
Abi_power64_relocationabi_power64_relocation contains types and definitions specific to * relocations in the Power64 ABI
Abi_power64_section_header_tableabi_power64_section_header_table contains Power64 ABI specific definitions * related to the section header table.
Abi_riscvabi_riscv contains top-level definition for the RISCV ABI.
Abi_riscv_elf_headerabi_riscv_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the RISCV ABI.
Abi_riscv_program_header_tableabi_riscv_program_header_table, program header table specific definitions * for the RISCV ABI.
Abi_riscv_relocationabi_riscv_relocation contains types and definitions relating to ABI * specific relocation functionality for the RISCV ABI.
Abi_riscv_section_header_tableabi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
Abi_riscv_serialisationabi_riscv_serialisation contains code for producing an RISCV conformant * ELF file from executable (machine) code. * Used in ongoing experiments with CakeML. * * XXX: experimental, and outdated. Commented out for now until attention turns * to CakeML again.
Abi_riscv_symbol_tableabi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
Abi_utilitiesabi_utilities, generic utilities shared between all ABIs.
Abi_x86_relocationabi_x86_relocation contains X86 ABI specific definitions relating to * relocations.
AbisThe abis module is the top-level module for all ABI related code, including * some generic functionality that works across all ABIs, and a primitive attempt * at abstracting over ABIs for purposes of linking.
Elf_dynamicelf_dynamic module exports types and definitions relating to the dynamic * section and dynamic linking functionality of an ELF file.
Elf_fileModule 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.
Elf_headerelf_header includes types, functions and other definitions for working with * ELF headers.
Elf_interpreted_sectionModule elf_interpreted_section provides a record of "interpreted" sections, * i.e. the data stored in the section header table converted to more amenable * infinite precision types, and operation on those records.
Elf_interpreted_segmentelf_interpreted_segment defines interpreted segments, i.e. the contents of * a program header table entry converted to more amenable types, and operations * built on top of them.
Elf_noteelf_note contains data types and functions for interpreting the .note * section/segment of an ELF file, and extracting information from that * section/segment.
Elf_program_header_tableelf_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.
Elf_relocationelf_relocation formalises types, functions and other definitions for working * with ELF relocation and relocation with addend entries.
Elf_section_header_tableelf_section_header_table provides types, functions and other definitions * for working with section header tables and their entries.
Elf_symbol_tableelf_symbol_table provides types, functions and other definitions for * working with ELF symbol tables.
Gnu_ext_dynamicgnu_ext_dynamic contains GNU extension specific definitions related to the * .dynamic section of an ELF file.
Gnu_ext_notegnu_ext_note contains GNU extension specific definitions relating to the * .note section/segment of an ELF file.
Gnu_ext_program_header_tablegnu_ext_program_header_table contains GNU extension specific functionality * related to the program header table.
Gnu_ext_section_header_tableThe module gnu_ext_section_header_table implements function, definitions * and types relating to the GNU extensions to the standard ELF section header * table.
Gnu_ext_section_to_segment_mappinggnu_ext_section_to_segment_mapping contains (GNU specific) functionality * relating to calculating the section to segment mapping for an ELF file. In * particular, the test over whether a section is inside a segment is ABI * specific. This module provides that test.
Gnu_ext_symbol_versioningThe gnu_ext_symbol_versioning defines constants, types and functions * relating to the GNU symbol versioning extensions (i.e. contents of * GNU_VERSYM sections). * * TODO: work out what is going on with symbol versioning. The specification * is completely opaque.
Gnu_ext_types_native_uintgnu_ext_types_native_uint provides extended types defined by the GNU * extensions over and above the based ELF types.
Hex_printinghex_printing is a utility module for converting natural numbers and integers * into hex strings of various widths. Split into a new module as both the * validation code and the main program need this functionality.
Showshow.lem exports the typeclass Show and associated functions for pretty * printing arbitrary values.
String_tableThe string_table module implements string tables. An ELF file may have * multiple different string tables used for different purposes. A string * table is a string coupled with a delimiting character. Strings may be indexed * at any position, not necessarily on a delimiter boundary.