package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/index.html
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 ABIAbi_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
Theabis
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
Moduleelf_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
Moduleelf_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 areelf_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 usesint
type throughout whereBigInt.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 bindingsEndianness
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 modulegnu_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
Thegnu_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 typeclassShow
and associated functions for pretty * printing arbitrary values.String_table
Thestring_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 ABIAbi_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
Theabis
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
Moduleelf_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
Moduleelf_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 areelf_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 usesint
type throughout whereBigInt.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 bindingsEndianness
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 modulegnu_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
Thegnu_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 typeclassShow
and associated functions for pretty * printing arbitrary values.String_table
Thestring_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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page