linksem

API

Library linksem_num

• Abi_aarch64_le abi_aarch64_le contains top-level definition for the AArch64 ABI (little-endian case).
• Abi_aarch64_le_elf_header abi_aarch64_le_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AArch64 ABI (little-endian).
• Abi_aarch64_le_serialisation abi_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_table abi_aarch64_program_header_table, AARCH64 ABI specific program header * table related flags, data, etc.
• Abi_aarch64_relocation abi_aarch64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AArch64 ABI (little-endian case).
• Abi_aarch64_section_header_table abi_aarch64_section_header_table, AARCH64 ABI specific definitions related * to the section header table.
• Abi_aarch64_symbol_table abi_aarch64_symbol_table, symbol table specific defintions for the AARCH64 * ABI.
• Abi_amd64 abi_amd64 contains top-level definition for the AMD64 ABI.
• Abi_amd64_elf_header abi_amd64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AMD64 ABI.
• Abi_amd64_program_header_table abi_amd64_program_header_table, program header table specific definitions * for the AMD64 ABI.
• Abi_amd64_relocation abi_amd64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AMD64 ABI.
• Abi_amd64_section_header_table abi_amd64_section_header_table module contains section header table * specific definitions for the AMD64 ABI.
• Abi_amd64_serialisation abi_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_table abi_amd64_symbol_table, AMD64 ABI specific definitions for the ELF symbol * table.
• Abi_cheri_mips64
• Abi_cheri_mips64_capability
• Abi_cheri_mips64_dynamic
• Abi_cheri_mips64_elf_header
• Abi_cheri_mips64_relocation
• Abi_classes
• Abi_mips64 abi_mips64 contains top-level definition for the MIPS64 ABI.
• Abi_mips64_dynamic
• Abi_mips64_elf_header abi_mips64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the MIPS64 ABI.
• Abi_mips64_program_header_table abi_mips64_program_header_table, program header table specific definitions * for the MIPS64 ABI.
• Abi_mips64_relocation abi_mips64_relocation contains types and definitions relating to ABI * specific relocation functionality for the MIPS64 ABI.
• Abi_mips64_section_header_table abi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
• Abi_mips64_serialisation abi_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_table abi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
• Abi_power64 abi_power64 contains top-level definition for the PowerPC64 ABI.
• Abi_power64_dynamic
• Abi_power64_elf_header abi_power64_elf_header, Power64 ABI specific definitions related to the * ELF file header.
• Abi_power64_relocation abi_power64_relocation contains types and definitions specific to * relocations in the Power64 ABI
• Abi_power64_section_header_table abi_power64_section_header_table contains Power64 ABI specific definitions * related to the section header table.
• Abi_riscv abi_riscv contains top-level definition for the RISCV ABI.
• Abi_riscv_elf_header abi_riscv_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the RISCV ABI.
• Abi_riscv_program_header_table abi_riscv_program_header_table, program header table specific definitions * for the RISCV ABI.
• Abi_riscv_relocation abi_riscv_relocation contains types and definitions relating to ABI * specific relocation functionality for the RISCV ABI.
• Abi_riscv_section_header_table abi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
• Abi_riscv_serialisation abi_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_table abi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
• Abi_utilities abi_utilities, generic utilities shared between all ABIs.
• Abi_x86_relocation abi_x86_relocation contains X86 ABI specific definitions relating to * relocations.
• Abis The 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.
• Abstract_linker_script
• Archive
• Auxv
• Byte_pattern
• Byte_pattern_extra
• Byte_sequence
• Byte_sequence_impl byte_sequence_ocaml.lem, a list of bytes used for ELF I/O and other basic * tasks in the ELF model.
• Byte_sequence_wrapper
• Command_line
• Default_printing
• Dwarf ***************** experimental DWARF reading ***********
• Dwarf_ctypes
• Elf64_file_of_elf_memory_image
• Elf_dynamic elf_dynamic module exports types and definitions relating to the dynamic * section and dynamic linking functionality of an ELF file.
• Elf_file 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.
• Elf_header elf_header includes types, functions and other definitions for working with * ELF headers.
• Elf_interpreted_section Module 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_segment elf_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_memory_image
• Elf_memory_image_of_elf64_file
• Elf_note elf_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_table 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.
• Elf_relocation elf_relocation formalises types, functions and other definitions for working * with ELF relocation and relocation with addend entries.
• Elf_section_header_table elf_section_header_table provides types, functions and other definitions * for working with section header tables and their entries.
• Elf_symbol_table elf_symbol_table provides types, functions and other definitions for * working with ELF symbol tables.
• Elf_types_native_uint unsigned char type and bindings
• Endianness endian.lem defines a type for describing the endianness of an ELF file, * and functions and other operations over that type.
• Error
• Filesystem
• Filesystem_wrapper
• Gnu_ext_abi
• Gnu_ext_dynamic gnu_ext_dynamic contains GNU extension specific definitions related to the * .dynamic section of an ELF file.
• Gnu_ext_note gnu_ext_note contains GNU extension specific definitions relating to the * .note section/segment of an ELF file.
• Gnu_ext_program_header_table gnu_ext_program_header_table contains GNU extension specific functionality * related to the program header table.
• Gnu_ext_section_header_table The 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_mapping gnu_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_versioning The 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_uint gnu_ext_types_native_uint provides extended types defined by the GNU * extensions over and above the based ELF types.
• Harness_interface
• Hex_printing hex_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.
• Input_list
• Ldconfig
• Link
• Linkable_list
• Linker_script
• Load
• Memory_image
• Memory_image_orderings
• Missing_pervasives
• Ml_bindings
• Multimap
• Sail_interface
• Show show.lem exports the typeclass Show and associated functions for pretty * printing arbitrary values.
• String_table The 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.
• Test_image
• Uint32_wrapper
• Uint64_wrapper

Library linksem_zarith

• Abi_aarch64_le abi_aarch64_le contains top-level definition for the AArch64 ABI (little-endian case).
• Abi_aarch64_le_elf_header abi_aarch64_le_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AArch64 ABI (little-endian).
• Abi_aarch64_le_serialisation abi_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_table abi_aarch64_program_header_table, AARCH64 ABI specific program header * table related flags, data, etc.
• Abi_aarch64_relocation abi_aarch64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AArch64 ABI (little-endian case).
• Abi_aarch64_section_header_table abi_aarch64_section_header_table, AARCH64 ABI specific definitions related * to the section header table.
• Abi_aarch64_symbol_table abi_aarch64_symbol_table, symbol table specific defintions for the AARCH64 * ABI.
• Abi_amd64 abi_amd64 contains top-level definition for the AMD64 ABI.
• Abi_amd64_elf_header abi_amd64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the AMD64 ABI.
• Abi_amd64_program_header_table abi_amd64_program_header_table, program header table specific definitions * for the AMD64 ABI.
• Abi_amd64_relocation abi_amd64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AMD64 ABI.
• Abi_amd64_section_header_table abi_amd64_section_header_table module contains section header table * specific definitions for the AMD64 ABI.
• Abi_amd64_serialisation abi_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_table abi_amd64_symbol_table, AMD64 ABI specific definitions for the ELF symbol * table.
• Abi_cheri_mips64
• Abi_cheri_mips64_capability
• Abi_cheri_mips64_dynamic
• Abi_cheri_mips64_elf_header
• Abi_cheri_mips64_relocation
• Abi_classes
• Abi_mips64 abi_mips64 contains top-level definition for the MIPS64 ABI.
• Abi_mips64_dynamic
• Abi_mips64_elf_header abi_mips64_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the MIPS64 ABI.
• Abi_mips64_program_header_table abi_mips64_program_header_table, program header table specific definitions * for the MIPS64 ABI.
• Abi_mips64_relocation abi_mips64_relocation contains types and definitions relating to ABI * specific relocation functionality for the MIPS64 ABI.
• Abi_mips64_section_header_table abi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
• Abi_mips64_serialisation abi_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_table abi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
• Abi_power64 abi_power64 contains top-level definition for the PowerPC64 ABI.
• Abi_power64_dynamic
• Abi_power64_elf_header abi_power64_elf_header, Power64 ABI specific definitions related to the * ELF file header.
• Abi_power64_relocation abi_power64_relocation contains types and definitions specific to * relocations in the Power64 ABI
• Abi_power64_section_header_table abi_power64_section_header_table contains Power64 ABI specific definitions * related to the section header table.
• Abi_riscv abi_riscv contains top-level definition for the RISCV ABI.
• Abi_riscv_elf_header abi_riscv_elf_header contains types and definitions relating to ABI * specific ELF header functionality for the RISCV ABI.
• Abi_riscv_program_header_table abi_riscv_program_header_table, program header table specific definitions * for the RISCV ABI.
• Abi_riscv_relocation abi_riscv_relocation contains types and definitions relating to ABI * specific relocation functionality for the RISCV ABI.
• Abi_riscv_section_header_table abi_mips64_section_header_table module contains section header table * specific definitions for the MIPS64 ABI.
• Abi_riscv_serialisation abi_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_table abi_mips64_symbol_table, MIPS64 ABI specific definitions for the ELF symbol * table.
• Abi_utilities abi_utilities, generic utilities shared between all ABIs.
• Abi_x86_relocation abi_x86_relocation contains X86 ABI specific definitions relating to * relocations.
• Abis The 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.
• Abstract_linker_script
• Archive
• Auxv
• Byte_pattern
• Byte_pattern_extra
• Byte_sequence
• Byte_sequence_impl byte_sequence_ocaml.lem, a list of bytes used for ELF I/O and other basic * tasks in the ELF model.
• Byte_sequence_wrapper
• Command_line
• Default_printing
• Dwarf ***************** experimental DWARF reading ***********
• Dwarf_ctypes
• Elf64_file_of_elf_memory_image
• Elf_dynamic elf_dynamic module exports types and definitions relating to the dynamic * section and dynamic linking functionality of an ELF file.
• Elf_file 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.
• Elf_header elf_header includes types, functions and other definitions for working with * ELF headers.
• Elf_interpreted_section Module 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_segment elf_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_memory_image
• Elf_memory_image_of_elf64_file
• Elf_note elf_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_table 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.
• Elf_relocation elf_relocation formalises types, functions and other definitions for working * with ELF relocation and relocation with addend entries.
• Elf_section_header_table elf_section_header_table provides types, functions and other definitions * for working with section header tables and their entries.
• Elf_symbol_table elf_symbol_table provides types, functions and other definitions for * working with ELF symbol tables.
• Elf_types_native_uint unsigned char type and bindings
• Endianness endian.lem defines a type for describing the endianness of an ELF file, * and functions and other operations over that type.
• Error
• Filesystem
• Filesystem_wrapper
• Gnu_ext_abi
• Gnu_ext_dynamic gnu_ext_dynamic contains GNU extension specific definitions related to the * .dynamic section of an ELF file.
• Gnu_ext_note gnu_ext_note contains GNU extension specific definitions relating to the * .note section/segment of an ELF file.
• Gnu_ext_program_header_table gnu_ext_program_header_table contains GNU extension specific functionality * related to the program header table.
• Gnu_ext_section_header_table The 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_mapping gnu_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_versioning The 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_uint gnu_ext_types_native_uint provides extended types defined by the GNU * extensions over and above the based ELF types.
• Harness_interface
• Hex_printing hex_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.
• Input_list
• Ldconfig
• Link
• Linkable_list
• Linker_script
• Load
• Memory_image
• Memory_image_orderings
• Missing_pervasives
• Ml_bindings
• Multimap
• Sail_interface
• Show show.lem exports the typeclass Show and associated functions for pretty * printing arbitrary values.
• String_table The 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.
• Test_image
• Uint32_wrapper
• Uint64_wrapper