package linksem

You can search for identifiers within the package.

in-package search v0.2.0

package linksem

linksem

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Elf_file`Source

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.

Sourcetype elf32_file = {

elf32_file_header : Elf_header.elf32_header;
(*
The file header.
*)
elf32_file_program_header_table : Elf_program_header_table.elf32_program_header_table;
(*
The program header table.
*)
elf32_file_section_header_table : Elf_section_header_table.elf32_section_header_table;
(*
The section header table.
*)
elf32_file_interpreted_segments : Elf_interpreted_segment.elf32_interpreted_segments;
(*
A more usable interpretation of the file's segments.
*)
elf32_file_interpreted_sections : Elf_interpreted_section.elf32_interpreted_sections;
(*
A more usable interpretation of the file's sections.
*)
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.

val bytes_of_elf32_file : 
  elf32_file ->
  Byte_sequence_wrapper.byte_sequence Error.error

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.

Sourcetype elf64_file = {

elf64_file_header : Elf_header.elf64_header;
(*
The file header.
*)
elf64_file_program_header_table : Elf_program_header_table.elf64_program_header_table;
(*
The program header table.
*)
elf64_file_section_header_table : Elf_section_header_table.elf64_section_header_table;
(*
The section header table.
*)
elf64_file_interpreted_segments : Elf_interpreted_segment.elf64_interpreted_segments;
(*
A more usable interpretation of the file's segments.
*)
elf64_file_interpreted_sections : Elf_interpreted_section.elf64_interpreted_sections;
(*
A more usable interpretation of the file's sections.
*)
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.

Sourcetype elf_file =

| ELF_File_32 of elf32_file
| ELF_File_64 of elf64_file

val bytes_of_elf64_file : 
  elf64_file ->
  Byte_sequence_wrapper.byte_sequence Error.error

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.

val obtain_elf32_program_header_table : 
  Elf_header.elf32_header ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_program_header_table.elf32_program_header_table_entry list Error.error

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.

val obtain_elf64_program_header_table : 
  Elf_header.elf64_header ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_program_header_table.elf64_program_header_table_entry list Error.error

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.

val obtain_elf32_section_header_table : 
  Elf_header.elf32_header ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_section_header_table.elf32_section_header_table_entry list Error.error

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.

val obtain_elf64_section_header_table : 
  Elf_header.elf64_header ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_section_header_table.elf64_section_header_table_entry list Error.error

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.

val obtain_elf32_section_header_string_table : 
  Elf_header.elf32_header ->
  Elf_section_header_table.elf32_section_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence ->
  String_table.string_table option Error.error

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.

val obtain_elf64_section_header_string_table : 
  Elf_header.elf64_header ->
  Elf_section_header_table.elf64_section_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence ->
  String_table.string_table option Error.error

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.

val obtain_elf32_interpreted_segments : 
  Elf_program_header_table.elf32_program_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_interpreted_segment.elf32_interpreted_segment list Error.error

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.

val obtain_elf64_interpreted_segments : 
  Elf_program_header_table.elf64_program_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_interpreted_segment.elf64_interpreted_segment list Error.error

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.

val obtain_elf32_interpreted_sections : 
  String_table.string_table option ->
  Elf_section_header_table.elf32_section_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_interpreted_section.elf32_interpreted_section list Error.error

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.

val obtain_elf64_interpreted_sections : 
  String_table.string_table option ->
  Elf_section_header_table.elf64_section_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence ->
  Elf_interpreted_section.elf64_interpreted_section list Error.error

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.

val compute_differences : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  (Nat_big_num.num * Nat_big_num.num) list ->
  (Nat_big_num.num * Nat_big_num.num) list Error.error

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.

val obtain_elf32_bits_and_bobs : 
  Elf_header.elf32_header ->
  Elf_program_header_table.elf32_program_header_table_entry list ->
  Elf_interpreted_segment.elf32_interpreted_segment list ->
  Elf_section_header_table.elf32_section_header_table_entry list ->
  Elf_interpreted_section.elf32_interpreted_section list ->
  Byte_sequence_wrapper.byte_sequence ->
  (Nat_big_num.num * Byte_sequence_wrapper.byte_sequence) list Error.error

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.

val obtain_elf64_bits_and_bobs : 
  Elf_header.elf64_header ->
  Elf_program_header_table.elf64_program_header_table_entry list ->
  Elf_interpreted_segment.elf64_interpreted_segment list ->
  Elf_section_header_table.elf64_section_header_table_entry list ->
  Elf_interpreted_section.elf64_interpreted_section list ->
  Byte_sequence_wrapper.byte_sequence ->
  (Nat_big_num.num * Byte_sequence_wrapper.byte_sequence) list Error.error

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.

val read_elf32_file : 
  Byte_sequence_wrapper.byte_sequence ->
  elf32_file Error.error

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

val read_elf64_file : 
  Byte_sequence_wrapper.byte_sequence ->
  elf64_file Error.error

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 find_elf32_symbols_by_symtab_idx : 
  Nat_big_num.num ->
  elf32_file ->
  (Elf_symbol_table.elf32_symbol_table_entry list
   * String_table.string_table
   * Nat_big_num.num)
    Error.error

val find_elf32_symtab_by_type : 
  Nat_big_num.num ->
  elf32_file ->
  (Elf_symbol_table.elf32_symbol_table
   * String_table.string_table
   * Nat_big_num.num)
    Error.error

val find_elf64_symbols_by_symtab_idx : 
  Nat_big_num.num ->
  elf64_file ->
  (Elf_symbol_table.elf64_symbol_table_entry list
   * String_table.string_table
   * Nat_big_num.num)
    Error.error

val find_elf64_symtab_by_type : 
  Nat_big_num.num ->
  elf64_file ->
  (Elf_symbol_table.elf64_symbol_table
   * String_table.string_table
   * Nat_big_num.num)
    Error.error

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.

val get_elf64_file_symbol_table : 
  elf64_file ->
  (Elf_symbol_table.elf64_symbol_table_entry list * String_table.string_table)
    Error.error

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.

val get_elf32_symbol_table_by_index : 
  elf32_file ->
  Nat_big_num.num ->
  Elf_symbol_table.elf32_symbol_table Error.error

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.

val get_elf64_symbol_table_by_index : 
  elf64_file ->
  Nat_big_num.num ->
  Elf_symbol_table.elf64_symbol_table Error.error

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.

Sourcetype segment_provenance =

| FromELF
(*
Segment derived directly from the source ELF file.
*)
| 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.

type elf32_executable_process_image =
  (Elf_interpreted_segment.elf32_interpreted_segment * segment_provenance) list
  * Nat_big_num.num
  * Nat_big_num.num

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

type elf64_executable_process_image =
  (Elf_interpreted_segment.elf64_interpreted_segment * segment_provenance) list
  * Nat_big_num.num
  * Nat_big_num.num

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

val get_elf32_executable_image : 
  elf32_file ->
  ((Elf_interpreted_segment.elf32_interpreted_segment * segment_provenance)
     list
   * Nat_big_num.num
   * Nat_big_num.num)
    Error.error

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

val get_elf64_executable_image : 
  elf64_file ->
  ((Elf_interpreted_segment.elf64_interpreted_segment * segment_provenance)
     list
   * Nat_big_num.num
   * Nat_big_num.num)
    Error.error

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.

Sourceval 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.