package linksem

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

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.

type elf32_file = {
  1. elf32_file_header : Elf_header.elf32_header;
    (*

    The file header.

    *)
  2. elf32_file_program_header_table : Elf_program_header_table.elf32_program_header_table;
    (*

    The program header table.

    *)
  3. elf32_file_section_header_table : Elf_section_header_table.elf32_section_header_table;
    (*

    The section header table.

    *)
  4. elf32_file_interpreted_segments : Elf_interpreted_segment.elf32_interpreted_segments;
    (*

    A more usable interpretation of the file's segments.

    *)
  5. elf32_file_interpreted_sections : Elf_interpreted_section.elf32_interpreted_sections;
    (*

    A more usable interpretation of the file's sections.

    *)
  6. elf32_file_bits_and_bobs : (Nat_big_num.num * Byte_sequence.byte_sequence0) list;
    (*

    The uninterpreted "rubbish" that may appear in gaps in the binary file.

    *)
}

elf32_file record captures the internal structure of an ELF32 file. * Invariant: length of the program header and section header tables should match * the length of their interpreted counterparts, and the nth element of the * (program/section) header table must correspond to the nth element of the * interpreted (segments/sections), respectively.

bytes_of_elf32_file f1 blits ELF file f1 to a byte sequence, ready for * writing to a binary file. Fails if the invariant on elf32_file mentioned * above is not respected.

type elf64_file = {
  1. elf64_file_header : Elf_header.elf64_header;
    (*

    The file header.

    *)
  2. elf64_file_program_header_table : Elf_program_header_table.elf64_program_header_table;
    (*

    The program header table.

    *)
  3. elf64_file_section_header_table : Elf_section_header_table.elf64_section_header_table;
    (*

    The section header table.

    *)
  4. elf64_file_interpreted_segments : Elf_interpreted_segment.elf64_interpreted_segments;
    (*

    A more usable interpretation of the file's segments.

    *)
  5. elf64_file_interpreted_sections : Elf_interpreted_section.elf64_interpreted_sections;
    (*

    A more usable interpretation of the file's sections.

    *)
  6. elf64_file_bits_and_bobs : (Nat_big_num.num * Byte_sequence.byte_sequence0) list;
    (*

    The uninterpreted "rubbish" that may appear in gaps in the binary file.

    *)
}

elf64_file record captures the internal structure of an ELF32 file. * Invariant: length of the program header and section header tables should match * the length of their interpreted counterparts, and the nth element of the * (program/section) header table must correspond to the nth element of the * interpreted (segments/sections), respectively.

type elf_file =
  1. | ELF_File_32 of elf32_file
  2. | ELF_File_64 of elf64_file

bytes_of_elf64_file f1 blits ELF file f1 to a byte sequence, ready for * writing to a binary file. Fails if the invariant on elf64_file mentioned * above is not respected.

obtain_elf32_program_header_table hdr bs0 reads a file's program header table * from byte sequence bs0 using information gleaned from the file header hdr. * Fails if transcription fails.

obtain_elf64_program_header_table hdr bs0 reads a file's program header table * from byte sequence bs0 using information gleaned from the file header hdr. * Fails if transcription fails.

obtain_elf32_section_header_table hdr bs0 reads a file's section header table * from byte sequence bs0 using information gleaned from the file header hdr. * Fails if transcription fails.

obtain_elf64_section_header_table hdr bs0 reads a file's section header table * from byte sequence bs0 using information gleaned from the file header hdr. * Fails if transcription fails.

obtain_elf32_section_header_string_table hdr sht bs0 reads a file's section * header string table from byte sequence bs0 using information gleaned from * the file header hdr and section header table sht. * Fails if transcription fails.

obtain_elf64_section_header_string_table hdr sht bs0 reads a file's section * header string table from byte sequence bs0 using information gleaned from * the file header hdr and section header table sht. * Fails if transcription fails.

obtain_elf32_interpreted_segments pht bs0 generates the interpreted segments * of an ELF file from the uninterpreted program header table entries in pht, * read from byte sequence bs0. Makes working with segments easier. * May fail if transcription of any segment fails.

obtain_elf64_interpreted_segments pht bs0 generates the interpreted segments * of an ELF file from the uninterpreted program header table entries in pht, * read from byte sequence bs0. Makes working with segments easier. * May fail if transcription of any segment fails.

obtain_elf32_interpreted_section sht bs0 generates the interpreted sections * of an ELF file from the uninterpreted section header table entries in sht, * read from byte sequence bs0. Makes working with sections easier. * May fail if transcription of any section fails.

obtain_elf64_interpreted_section sht bs0 generates the interpreted sections * of an ELF file from the uninterpreted section header table entries in sht, * read from byte sequence bs0. Makes working with sections easier. * May fail if transcription of any section fails.

val find_first_not_in_range : Nat_big_num.num -> (Nat_big_num.num * Nat_big_num.num) list -> Nat_big_num.num

find_first_not_in_range e rngs for every pair (start, end) in rngs, finds * the first element, beginning counting from e, that does not lie between * a start and end value.

val find_first_in_range : Nat_big_num.num -> (Nat_big_num.num * Nat_big_num.num) list -> Nat_big_num.num

find_first_in_range e rngs for every pair (start, end) in rngs, finds * the first element, beginning counting from e, that lies between * a start and end value.

compute_differences start max ranges is a utility function used for calculating * "dead" spots in an ELF file not covered by any of the interpreted structure * that nevertheless need recording in the bits_and_bobs field of each ELF record * in order to maintain in-out roundtripping up to exact binary equivalence.

obtain_elf32_bits_and_bobs hdr pht segs sht sects bs0 identifies and records * the "dead" spots of an ELF file not covered by any meaningful structure of the * ELF file format.

obtain_elf64_bits_and_bobs hdr pht segs sht sects bs0 identifies and records * the "dead" spots of an ELF file not covered by any meaningful structure of the * ELF file format.

read_elf32_file bs0 reads an ELF32 file from byte sequence bs0. Fails if * transcription fails.

read_elf64_file bs0 reads an ELF64 file from byte sequence bs0. Fails if * transcription fails.

val get_elf32_file_section_header_string_table : elf32_file -> String_table.string_table Error.error

get_elf32_file_secton_header_string_table f1 returns the ELF file, f1, * section header string table. * TODO: why is this not using obtain_elf32_section_header_string_table above?

val get_elf64_file_section_header_string_table : elf64_file -> String_table.string_table Error.error

get_elf64_file_secton_header_string_table f1 returns the ELF file, f1, * section header string table. * TODO: why is this not using obtain_elf64_section_header_string_table above?

val get_elf32_file_symbol_string_table : elf32_file -> String_table.string_table Error.error

get_elf32_file_symbol_string_table f1 returns the ELF file f1 symbol * string table. May fail.

val get_elf64_file_symbol_string_table : elf64_file -> String_table.string_table Error.error

get_elf64_file_symbol_string_table f1 returns the ELF file f1 symbol * string table. May fail.

val get_elf32_string_table_by_index : elf32_file -> Nat_big_num.num -> String_table.string_table Error.error

get_elf32_file_string_table_by_index f1 index returns the ELF file f1 * string table that is pointed to by the section header table entry at index * index. May fail if index is out of range, or otherwise.

val get_elf64_string_table_by_index : elf64_file -> Nat_big_num.num -> String_table.string_table Error.error

get_elf64_file_string_table_by_index f1 index returns the ELF file f1 * string table that is pointed to by the section header table entry at index * index. May fail if index is out of range, or otherwise.

val get_elf32_file_symbol_table : elf32_file -> Elf_symbol_table.elf32_symbol_table_entry list Error.error

get_elf32_file_symbol_table f1 returns the ELF file f1 symbol * table. May fail.

get_elf64_file_symbol_table f1 returns the ELF file f1 symbol * table. May fail.

val get_elf32_file_dynamic_symbol_table : elf32_file -> Elf_symbol_table.elf32_symbol_table_entry list Error.error

get_elf32_file_dynamic_symbol_table f1 returns the ELF file f1 dynamic * symbol table. May fail.

val get_elf64_file_dynamic_symbol_table : elf64_file -> Elf_symbol_table.elf64_symbol_table_entry list Error.error

get_elf64_file_dynamic_symbol_table f1 returns the ELF file f1 dynamic * symbol table. May fail.

get_elf32_file_symbol_table_by_index f1 index returns the ELF file f1 * symbol table that is pointed to by the section header table entry at index * index. May fail if index is out of range, or otherwise.

get_elf64_file_symbol_table_by_index f1 index returns the ELF file f1 * symbol table that is pointed to by the section header table entry at index * index. May fail if index is out of range, or otherwise.

type segment_provenance =
  1. | FromELF
    (*

    Segment derived directly from the source ELF file.

    *)
  2. | AutoGenerated
    (*

    Automatically generated during process extraction as memory size is greater than file size.

    *)

segment_provenance records whether a segment that appears in an executable * process image has been derived directly from an ELF file, or was automatically * created when the image calculation process noticed a segment with a memory * size greater than its file size. * Really a PPCMemism and not strictly needed for the ELF model itself.

elf32_executable_process_image is a process image for ELF32 files. Contains * all that is necessary to load the executable components of an ELF32 file * and begin execution. * XXX: (segments, provenance), entry point, machine type

elf64_executable_process_image is a process image for ELF64 files. Contains * all that is necessary to load the executable components of an ELF64 file * and begin execution. * XXX: (segments, provenance), entry point, machine type

get_elf32_executable_image f1 extracts an executable process image from an * executable ELF file. May fail if extraction is impossible.

get_elf64_executable_image f1 extracts an executable process image from an * executable ELF file. May fail if extraction is impossible.

type global_symbol_init_info = (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Byte_sequence.byte_sequence0 option * Nat_big_num.num)) list

global_symbol_init_info records the name, type, size, address, chunk * of initialisation data (if relevant for that symbol), and binding, of every * global symbol in an ELF file. * Another PPCMemism.

val get_elf32_file_global_symbol_init : elf32_file -> (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Byte_sequence_wrapper.byte_sequence option * Nat_big_num.num)) list Error.error

get_elf32_file_global_symbol_init f1 extracts the global symbol init info * for ELF file f1. May fail.

val get_elf64_file_global_symbol_init : elf64_file -> (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Byte_sequence_wrapper.byte_sequence option * Nat_big_num.num)) list Error.error

get_elf64_file_global_symbol_init f1 extracts the global symbol init info * for ELF file f1. May fail.

val string_of_elf32_file : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> elf32_file -> string

string_of_elf32_file hdr_bdl pht_bdl sht_bdl f1 produces a string-based * representation of ELF file f1 using ABI-specific print bundles hdr_bdl, * pht_bdl and sht_bdl.

val string_of_elf64_file : ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> ((Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)) -> elf64_file -> string

string_of_elf64_file hdr_bdl pht_bdl sht_bdl f1 produces a string-based * representation of ELF file f1 using ABI-specific print bundles hdr_bdl, * pht_bdl and sht_bdl.

val flag_is_set : Nat_big_num.num -> Nat_big_num.num -> bool

flag_is_set flag v checks whether flag flag is set in v. * TODO: move elsewhere. Check whether this is still being used.