package linksem

  1. Overview
  2. Docs

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