package linksem

  1. Overview
  2. Docs
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type

elf_section_header_table provides types, functions and other definitions * for working with section header tables and their entries.

Special section indices.

See elf_header.lem for shn_undef

val shn_loreserve : Nat_big_num.num

shn_loreserve: this specifies the lower bound of the range of reserved * indices.

shn_loproc: start of the range reserved for processor-specific semantics.

val shn_loproc : Nat_big_num.num

shn_loproc: start of the range reserved for processor-specific semantics.

shn_hiproc: end of the range reserved for processor-specific semantics.

val shn_hiproc : Nat_big_num.num

shn_hiproc: end of the range reserved for processor-specific semantics.

shn_loos: start of the range reserved for operating system-specific * semantics.

val shn_loos : Nat_big_num.num

shn_loos: start of the range reserved for operating system-specific * semantics.

shn_hios: end of the range reserved for operating system-specific * semantics.

val shn_hios : Nat_big_num.num

shn_hios: end of the range reserved for operating system-specific * semantics.

shn_abs: specifies the absolute values for the corresponding reference. * Symbols defined relative to section number shn_abs have absolute values * and are not affected by relocation.

val shn_abs : Nat_big_num.num

shn_abs: specifies the absolute values for the corresponding reference. * Symbols defined relative to section number shn_abs have absolute values * and are not affected by relocation.

shn_common: symbols defined relative to this index are common symbols, * such as unallocated C external variables.

val shn_common : Nat_big_num.num

shn_common: symbols defined relative to this index are common symbols, * such as unallocated C external variables.

See elf_header.lem for shn_xindex.

val shn_hireserve : Nat_big_num.num

shn_hireserve: specifies the upper-bound of reserved values.

val string_of_special_section_index : Nat_big_num.num -> string

string_of_special_section_index m produces a string-based representation * of a section header entry's special section index, m.

Section types.

val sht_null : Nat_big_num.num

Marks the section header as being inactive.

Section holds information defined by the program.

val sht_progbits : Nat_big_num.num

Section holds information defined by the program.

The following two section types hold a symbol table. An object file may only * have one symbol table of each of the respective types. The symtab provides * a place for link editing, whereas the dynsym section holds a minimal set of * dynamic linking symbols

val sht_symtab : Nat_big_num.num

The following two section types hold a symbol table. An object file may only * have one symbol table of each of the respective types. The symtab provides * a place for link editing, whereas the dynsym section holds a minimal set of * dynamic linking symbols

val sht_dynsym : Nat_big_num.num

Section holds a string table

val sht_strtab : Nat_big_num.num

Section holds a string table

Section holds relocation entries with explicit addends. An object file may * have multiple section of this type.

val sht_rela : Nat_big_num.num

Section holds relocation entries with explicit addends. An object file may * have multiple section of this type.

Section holds a symbol hash table. An object file may only have a single * hash table.

val sht_hash : Nat_big_num.num

Section holds a symbol hash table. An object file may only have a single * hash table.

Section holds information for dynamic linking. An object file may only have * a single dynamic section.

val sht_dynamic : Nat_big_num.num

Section holds information for dynamic linking. An object file may only have * a single dynamic section.

Section holds information that marks the file in some way.

val sht_note : Nat_big_num.num

Section holds information that marks the file in some way.

Section occupies no space in the file but otherwise resembles a progbits * section.

val sht_nobits : Nat_big_num.num

Section occupies no space in the file but otherwise resembles a progbits * section.

Section holds relocation entries without explicit addends. An object file * may have multiple section of this type.

val sht_rel : Nat_big_num.num

Section holds relocation entries without explicit addends. An object file * may have multiple section of this type.

Section type is reserved but has an unspecified meaning.

val sht_shlib : Nat_big_num.num

Section type is reserved but has an unspecified meaning.

Section contains an array of pointers to initialisation functions. Each * pointer is taken as a parameterless function with a void return type.

val sht_init_array : Nat_big_num.num

Section contains an array of pointers to initialisation functions. Each * pointer is taken as a parameterless function with a void return type.

Section contains an array of pointers to termination functions. Each * pointer is taken as a parameterless function with a void return type.

val sht_fini_array : Nat_big_num.num

Section contains an array of pointers to termination functions. Each * pointer is taken as a parameterless function with a void return type.

Section contains an array of pointers to initialisation functions that are * invoked before all other initialisation functions. Each * pointer is taken as a parameterless function with a void return type.

val sht_preinit_array : Nat_big_num.num

Section contains an array of pointers to initialisation functions that are * invoked before all other initialisation functions. Each * pointer is taken as a parameterless function with a void return type.

Section defines a section group, i.e. a set of sections that are related and * must be treated especially by the linker. May only appear in relocatable * objects.

val sht_group : Nat_big_num.num

Section defines a section group, i.e. a set of sections that are related and * must be treated especially by the linker. May only appear in relocatable * objects.

Section is associated with sections of type SHT_SYMTAB and is required if * any of the section header indices referenced by that symbol table contains * the escape value SHN_XINDEX. * * FIXME: Lem bug as int type used throughout Lem codebase, rather than * BigInt.t, so Lem chokes on these large constants below, hence the weird * way in which they are written.

val sht_symtab_shndx : Nat_big_num.num

Section is associated with sections of type SHT_SYMTAB and is required if * any of the section header indices referenced by that symbol table contains * the escape value SHN_XINDEX. * * FIXME: Lem bug as int type used throughout Lem codebase, rather than * BigInt.t, so Lem chokes on these large constants below, hence the weird * way in which they are written.

val sht_loos : Nat_big_num.num

The following ranges are reserved solely for OS-, processor- and user- * specific semantics, respectively.

val sht_hios : Nat_big_num.num
val sht_loproc : Nat_big_num.num
val sht_hiproc : Nat_big_num.num
val sht_louser : Nat_big_num.num
val sht_hiuser : Nat_big_num.num
val string_of_section_type : (Nat_big_num.num -> string) -> (Nat_big_num.num -> string) -> (Nat_big_num.num -> string) -> Nat_big_num.num -> string

string_of_section_type os proc user i produces a string-based representation * of section type i. Some section types are defined by ABI-specific supplements * in reserved ranges, in which case the functions os, proc and user are * used to produce the string.

Section flag numeric values.

val shf_write : Nat_big_num.num

The section contains data that should be writable during program execution.

The section occupies memory during program execution.

val shf_alloc : Nat_big_num.num

The section occupies memory during program execution.

The section contains executable instructions.

val shf_execinstr : Nat_big_num.num

The section contains executable instructions.

The data in the section may be merged to reduce duplication. Each section * is compared based on name, type and flags set with sections with identical * values at run time being mergeable.

val shf_merge : Nat_big_num.num

The data in the section may be merged to reduce duplication. Each section * is compared based on name, type and flags set with sections with identical * values at run time being mergeable.

The section contains null-terminated character strings.

val shf_strings : Nat_big_num.num

The section contains null-terminated character strings.

The info field of this section header contains a section header table * index.

The info field of this section header contains a section header table * index.

Adds special link ordering for link editors.

Adds special link ordering for link editors.

This section requires special OS-specific processing beyond the standard * link rules.

val shf_os_nonconforming : Nat_big_num.num

This section requires special OS-specific processing beyond the standard * link rules.

This section is a member (potentially the only member) of a link group.

val shf_group : Nat_big_num.num

This section is a member (potentially the only member) of a link group.

This section contains Thread Local Storage (TLS) meaning that each thread of * execution has its own instance of this data.

val shf_tls : Nat_big_num.num

This section contains Thread Local Storage (TLS) meaning that each thread of * execution has its own instance of this data.

This section contains compressed data. Compressed data may not be marked as * allocatable.

val shf_compressed : Nat_big_num.num

This section contains compressed data. Compressed data may not be marked as * allocatable.

All bits included in these masks are reserved for OS and processor specific * semantics respectively.

val shf_mask_os : Nat_big_num.num

All bits included in these masks are reserved for OS and processor specific * semantics respectively.

val shf_mask_proc : Nat_big_num.num
val string_of_section_flags : 'a -> 'b -> Nat_big_num.num -> string

string_of_section_flags os proc f produces a string based representation * of section flag f. Some section flags are defined by the ABI and are in * reserved ranges, in which case the flag string is produced by functions * os and proc. * TODO: add more as validation tests require them.

Section compression.

type elf32_compression_header = {
  1. elf32_chdr_type : Uint32_wrapper.uint32;
    (*

    Specifies the compression algorithm

    *)
  2. elf32_chdr_size : Uint32_wrapper.uint32;
    (*

    Size in bytes of the uncompressed data

    *)
  3. elf32_chdr_addralign : Uint32_wrapper.uint32;
    (*

    Specifies the required alignment of the uncompressed data

    *)
}

Type elf32_compression_header provides information about the compression and * decompression of compressed sections. All compressed sections on ELF32 begin * with an elf32_compression_header entry.

type elf64_compression_header = {
  1. elf64_chdr_type : Uint32_wrapper.uint32;
    (*

    Specified the compression algorithm

    *)
  2. elf64_chdr_reserved : Uint32_wrapper.uint32;
    (*

    Reserved.

    *)
  3. elf64_chdr_size : Uint64_wrapper.uint64;
    (*

    Size in bytes of the uncompressed data

    *)
  4. elf64_chdr_addralign : Uint64_wrapper.uint64;
    (*

    Specifies the required alignment of the uncompressed data

    *)
}

Type elf64_compression_header provides information about the compression and * decompression of compressed sections. All compressed sections on ELF64 begin * with an elf64_compression_header entry.

val elfcompress_zlib : Nat_big_num.num

This section is compressed with the ZLIB algorithm. The compressed data begins * at the first byte immediately following the end of the compression header.

val elfcompress_loos : Nat_big_num.num

Values in these ranges are reserved for OS-specific semantics.

val elfcompress_hios : Nat_big_num.num
val elfcompress_loproc : Nat_big_num.num

Values in these ranges are reserved for processor-specific semantics.

val elfcompress_hiproc : Nat_big_num.num

read_elf32_compression_header ed bs0 reads an elf32_compression_header * entry from byte sequence bs0, interpreting bs0 with endianness ed. * Also returns the suffix of bs0 after reading in the compression header. * Fails if the header cannot be read.

read_elf64_compression_header ed bs0 reads an elf64_compression_header * entry from byte sequence bs0, interpreting bs0 with endianness ed. * Also returns the suffix of bs0 after reading in the compression header. * Fails if the header cannot be read.

Section header table entry type.

type elf32_section_header_table_entry = {
  1. elf32_sh_name : Uint32_wrapper.uint32;
    (*

    Name of the section

    *)
  2. elf32_sh_type : Uint32_wrapper.uint32;
    (*

    Type of the section and its semantics

    *)
  3. elf32_sh_flags : Uint32_wrapper.uint32;
    (*

    Flags associated with the section

    *)
  4. elf32_sh_addr : Uint32_wrapper.uint32;
    (*

    Address of first byte of section in memory image

    *)
  5. elf32_sh_offset : Uint32_wrapper.uint32;
    (*

    Offset from beginning of file of first byte of section

    *)
  6. elf32_sh_size : Uint32_wrapper.uint32;
    (*

    Section size in bytes

    *)
  7. elf32_sh_info : Uint32_wrapper.uint32;
    (*

    Extra information, contents depends on type of section

    *)
  8. elf32_sh_addralign : Uint32_wrapper.uint32;
    (*

    Alignment constraints for section

    *)
  9. elf32_sh_entsize : Uint32_wrapper.uint32;
    (*

    Size of each entry in table, if section is one

    *)
}

elf32_section_header_table_entry is the type of entries in the section * header table in 32-bit ELF files. Each entry in the table details a section * in the body of the ELF file.

val elf32_null_section_header : elf32_section_header_table_entry
val compare_elf32_section_header_table_entry : elf32_section_header_table_entry -> elf32_section_header_table_entry -> int

compare_elf32_section_header_table_entry ent1 ent2 is an ordering comparison * function on section header table entries suitable for use in constructing * sets, finite maps and other ordered data types.

val instance_Basic_classes_Ord_Elf_section_header_table_elf32_section_header_table_entry_dict : elf32_section_header_table_entry Lem_basic_classes.ord_class
type elf64_section_header_table_entry = {
  1. elf64_sh_name : Uint32_wrapper.uint32;
    (*

    Name of the section

    *)
  2. elf64_sh_type : Uint32_wrapper.uint32;
    (*

    Type of the section and its semantics

    *)
  3. elf64_sh_flags : Uint64_wrapper.uint64;
    (*

    Flags associated with the section

    *)
  4. elf64_sh_addr : Uint64_wrapper.uint64;
    (*

    Address of first byte of section in memory image

    *)
  5. elf64_sh_offset : Uint64_wrapper.uint64;
    (*

    Offset from beginning of file of first byte of section

    *)
  6. elf64_sh_size : Uint64_wrapper.uint64;
    (*

    Section size in bytes

    *)
  7. elf64_sh_info : Uint32_wrapper.uint32;
    (*

    Extra information, contents depends on type of section

    *)
  8. elf64_sh_addralign : Uint64_wrapper.uint64;
    (*

    Alignment constraints for section

    *)
  9. elf64_sh_entsize : Uint64_wrapper.uint64;
    (*

    Size of each entry in table, if section is one

    *)
}

elf64_section_header_table_entry is the type of entries in the section * header table in 64-bit ELF files. Each entry in the table details a section * in the body of the ELF file.

val elf64_null_section_header : elf64_section_header_table_entry
val compare_elf64_section_header_table_entry : elf64_section_header_table_entry -> elf64_section_header_table_entry -> int

compare_elf64_section_header_table_entry ent1 ent2 is an ordering comparison * function on section header table entries suitable for use in constructing * sets, finite maps and other ordered data types.

val instance_Basic_classes_Ord_Elf_section_header_table_elf64_section_header_table_entry_dict : elf64_section_header_table_entry Lem_basic_classes.ord_class

Section header table type

type elf32_section_header_table = elf32_section_header_table_entry list

Type elf32_section_header_table represents a section header table for 32-bit * ELF files. A section header table is an array (implemented as a list, here) * of section header table entries.

type elf64_section_header_table = elf64_section_header_table_entry list

Type elf64_section_header_table represents a section header table for 64-bit * ELF files. A section header table is an array (implemented as a list, here) * of section header table entries.

Parsing and blitting

val bytes_of_elf32_section_header_table_entry : Endianness.endianness -> elf32_section_header_table_entry -> Byte_sequence_wrapper.byte_sequence

bytes_of_elf32_section_header_table_entry ed ent blits ent to a byte sequence * assuming endianness ed.

val read_elf32_section_header_table_entry : Endianness.endianness -> Byte_sequence_wrapper.byte_sequence -> (elf32_section_header_table_entry * Byte_sequence_wrapper.byte_sequence) Error.error

read_elf32_section_header_table_entry ed bs0 reads a section header table * entry from bs0 assuming endianness ed. Also returns the suffix of bs0 * after parsing. Fails if the entry cannot be read.

val bytes_of_elf64_section_header_table_entry : Endianness.endianness -> elf64_section_header_table_entry -> Byte_sequence_wrapper.byte_sequence

bytes_of_elf64_section_header_table_entry ed ent blits ent to a byte sequence * assuming endianness ed.

val read_elf64_section_header_table_entry : Endianness.endianness -> Byte_sequence_wrapper.byte_sequence -> (elf64_section_header_table_entry * Byte_sequence_wrapper.byte_sequence) Error.error

read_elf64_section_header_table_entry ed bs0 reads a section header table * entry from bs0 assuming endianness ed. Also returns the suffix of bs0 * after parsing. Fails if the entry cannot be read.

bytes_of_elf32_section_header_table ed tbl blits section header table tbl * to a byte sequence assuming endianness ed.

bytes_of_elf64_section_header_table ed tbl blits section header table tbl * to a byte sequence assuming endianness ed.

read_elf32_section_header_table' ed bs0 parses an ELF32 section header table * from byte sequence bs0 assuming endianness ed. Assumes bs0 is of the * exact length required to parse the entire table. * Fails if any of the section header table entries cannot be parsed.

read_elf64_section_header_table' ed bs0 parses an ELF64 section header table * from byte sequence bs0 assuming endianness ed. Assumes bs0 is of the * exact length required to parse the entire table. * Fails if any of the section header table entries cannot be parsed.

read_elf32_section_header_table sz ed bs0 parses an ELF32 section header * table from a sz sized prefix of byte sequence bs0 assuming endianness * ed. The suffix of bs0 remaining after parsing is also returned. * Fails if any of the section header entries cannot be parsed or if sz is * greater than the length of bs0.

read_elf64_section_header_table sz ed bs0 parses an ELF64 section header * table from a sz sized prefix of byte sequence bs0 assuming endianness * ed. The suffix of bs0 remaining after parsing is also returned. * Fails if any of the section header entries cannot be parsed or if sz is * greater than the length of bs0.

Correctness criteria

val elf32_size_correct : elf32_section_header_table_entry -> 'a list -> bool

TODO: what is going on here?

val elf64_size_correct : elf64_section_header_table_entry -> 'a list -> bool

TODO: what is going on here?

val is_elf32_addr_addralign_correct : elf32_section_header_table_entry -> bool

is_elf32_addr_addralign_correct ent checks whether an internal address * alignment constraint is met on section header table ent. * TODO: needs tweaking to add in power-of-two constraint, too.

val is_elf64_addr_addralign_correct : elf64_section_header_table_entry -> bool

is_elf64_addr_addralign_correct ent checks whether an internal address * alignment constraint is met on section header table ent. * TODO: needs tweaking to add in power-of-two constraint, too.

val is_valid_elf32_section_header_table : elf32_section_header_table_entry list -> bool

is_valid_elf32_section_header_table sht checks whether all entries of * section header table sht are valid.

val is_valid_elf64_section_header_table : elf64_section_header_table_entry list -> bool

is_valid_elf64_section_header_table sht checks whether all entries of * section header table sht are valid.

Pretty printing

type sht_print_bundle = (Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)

The sht_print_bundle type is used to tidy up other type signatures. Some of the * top-level string_of_ functions require six or more functions passed to them, * which quickly gets out of hand. This type is used to reduce that complexity. * The first component of the type is an OS specific print function, the second is * a processor specific print function.

val string_of_elf32_section_header_table_entry : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> elf32_section_header_table_entry -> string

string_of_elf32_section_header_table_entry sht ent produces a string * representation of section header table entry ent using sht, a * sht_print_bundle. * OCaml specific definition.

val string_of_elf64_section_header_table_entry : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> elf64_section_header_table_entry -> string

string_of_elf64_section_header_table_entry sht ent produces a string * representation of section header table entry ent using sht, a * sht_print_bundle. * OCaml specific definition.

val string_of_elf32_section_header_table_entry' : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> String_table.string_table -> elf32_section_header_table_entry -> string

string_of_elf32_section_header_table_entry' sht stab ent produces a string * representation of section header table entry ent using sht and section * header string table stab to print the name of the section header entry * correctly. * OCaml specific definition.

val string_of_elf64_section_header_table_entry' : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> String_table.string_table -> elf64_section_header_table_entry -> string

string_of_elf64_section_header_table_entry' sht stab ent produces a string * representation of section header table entry ent using sht and section * header string table stab to print the name of the section header entry * correctly. * OCaml specific definition.

The following defintions are default printing functions, with no ABI-specific * functionality, in order to produce a Show instance for section header * table entries.

val string_of_elf32_section_header_table_entry_default : elf32_section_header_table_entry -> string
val instance_Show_Show_Elf_section_header_table_elf32_section_header_table_entry_dict : elf32_section_header_table_entry Show.show_class
val string_of_elf64_section_header_table_entry_default : elf64_section_header_table_entry -> string
val instance_Show_Show_Elf_section_header_table_elf64_section_header_table_entry_dict : elf64_section_header_table_entry Show.show_class
val string_of_elf32_section_header_table : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> elf32_section_header_table_entry list -> string
val string_of_elf32_section_header_table_default : elf32_section_header_table -> string
val string_of_elf64_section_header_table : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> elf64_section_header_table_entry list -> string
val string_of_elf64_section_header_table_default : elf64_section_header_table -> string
val string_of_elf32_section_header_table' : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> String_table.string_table -> elf32_section_header_table_entry list -> string
val string_of_elf64_section_header_table' : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> String_table.string_table -> elf64_section_header_table_entry list -> string

Section to segment mappings

elf32_tbss_special shdr seg implements the ELF_TBSS_SPECIAL macro from readelf: * * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ * (((sec_hdr)->sh_flags & SHF_TLS) != 0 \ * && (sec_hdr)->sh_type == SHT_NOBITS \ * && (segment)->p_type != PT_TLS) * * From readelf source code, file internal.h. *

elf64_tbss_special shdr seg implements the ELF_TBSS_SPECIAL macro from readelf: * * #define ELF_TBSS_SPECIAL(sec_hdr, segment) \ * (((sec_hdr)->sh_flags & SHF_TLS) != 0 \ * && (sec_hdr)->sh_type == SHT_NOBITS \ * && (segment)->p_type != PT_TLS) * * From readelf source code, file internal.h. *

get_elf32_section_to_segment_mapping hdr sht pht isin stbl computes the * section to segment mapping for an ELF file using information in the section * header table sht, program header table pht and file header hdr. A * string table stbl is taken to produce the string output. The test whether * a section lies withing a segment is ABI specific, so isin is used to perform * the test.

get_elf64_section_to_segment_mapping hdr sht pht isin stbl computes the * section to segment mapping for an ELF file using information in the section * header table sht, program header table pht and file header hdr. A * string table stbl is taken to produce the string output. The test whether * a section lies withing a segment is ABI specific, so isin is used to perform * the test.

Section groups

val grp_comdat : Nat_big_num.num

This is a COMDAT group and may duplicate other COMDAT groups in other object * files.

val grp_maskos : Nat_big_num.num

Any bits in the following mask ranges are reserved exclusively for OS and * processor specific semantics, respectively.

val grp_maskproc : Nat_big_num.num

obtain_elf32_section_group_indices endian sht bs0 extracts all section header * table indices of sections that are marked as being part of a section group.

obtain_elf64_section_group_indices endian sht bs0 extracts all section header * table indices of sections that are marked as being part of a section group.

val obtain_elf32_tls_template : elf32_section_header_table_entry list -> elf32_section_header_table_entry list

obtain_elf32_tls_template sht extracts the TLS template (i.e. all sections * in section header table sht that have their TLS flag bit set).

val obtain_elf64_tls_template : elf64_section_header_table_entry list -> elf64_section_header_table_entry list

obtain_elf64_tls_template sht extracts the TLS template (i.e. all sections * in section header table sht that have their TLS flag bit set).

obtain_elf32_hash_table endian sht bs0 extracts a hash table from an ELF file * providing a section of type SHT_HASH exists in section header table sht. * Extraction is from byte sequence bs0 assuming endianness endian. The * return type represents the number of buckets, the number of chains, the buckets * and finally the chains.

obtain_elf64_hash_table endian sht bs0 extracts a hash table from an ELF file * providing a section of type SHT_HASH exists in section header table sht. * Extraction is from byte sequence bs0 assuming endianness endian. The * return type represents the number of buckets, the number of chains, the buckets * and finally the chains.

Special sections

val elf_special_sections : (string, Nat_big_num.num * Nat_big_num.num) Pmap.map

construct_special_sections contains a finite map from section name (as * a string) to the expected attributes and flags expected of that section, * as specified in the ELF specification. * NOTE: some of these are overriden by the ABI.