package linksem

You can search for identifiers within the package.

in-package search v0.2.0

A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

Maintainers

L

Linksem Devs <cl-linksem-dev@lists.cam.ac.uk>

Sources

md5=2075c56715539b3b8f54ae65cc808b8c

sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Elf_program_header_table/index.html

Module `Elf_program_header_table`Source

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.

Segment types

Sourceval elf_pt_null : Nat_big_num.num

Unused array element. All other members of the structure are undefined.

A loadable segment.

Sourceval elf_pt_load : Nat_big_num.num

A loadable segment.

Dynamic linking information.

Sourceval elf_pt_dynamic : Nat_big_num.num

Dynamic linking information.

Specifies the location and size of a null-terminated path name to be used to * invoke an interpreter.

Sourceval elf_pt_interp : Nat_big_num.num

Specifies the location and size of a null-terminated path name to be used to * invoke an interpreter.

Specifies location and size of auxiliary information.

Sourceval elf_pt_note : Nat_big_num.num

Specifies location and size of auxiliary information.

Reserved but with unspecified semantics. If the file contains a segment of * this type then it is to be regarded as non-conformant with the ABI.

Sourceval elf_pt_shlib : Nat_big_num.num

Reserved but with unspecified semantics. If the file contains a segment of * this type then it is to be regarded as non-conformant with the ABI.

Specifies the location and size of the program header table.

Sourceval elf_pt_phdr : Nat_big_num.num

Specifies the location and size of the program header table.

Specifies the thread local storage (TLS) template. Need not be supported.

Sourceval elf_pt_tls : Nat_big_num.num

Specifies the thread local storage (TLS) template. Need not be supported.

Start of reserved indices for operating system specific semantics.

Sourceval elf_pt_loos : Nat_big_num.num

Start of reserved indices for operating system specific semantics.

End of reserved indices for operating system specific semantics.

Sourceval elf_pt_hios : Nat_big_num.num

End of reserved indices for operating system specific semantics.

Start of reserved indices for processor specific semantics.

Sourceval elf_pt_loproc : Nat_big_num.num

Start of reserved indices for processor specific semantics.

End of reserved indices for processor specific semantics.

Sourceval elf_pt_hiproc : Nat_big_num.num

End of reserved indices for processor specific semantics.

val string_of_segment_type : 
  (Nat_big_num.num -> string) ->
  (Nat_big_num.num -> string) ->
  Nat_big_num.num ->
  string

string_of_elf_segment_type os proc st produces a string representation of * the coding of an ELF segment type st using os and proc to render OS- * and processor-specific codings.

Segments permission flags

Sourceval elf_pf_x : Nat_big_num.num

Execute bit

Write bit

Sourceval elf_pf_w : Nat_big_num.num

Write bit

Read bit

Sourceval elf_pf_r : Nat_big_num.num

Read bit

The following two bit ranges are reserved for OS- and processor-specific * flags respectively.

Sourceval elf_pf_maskos : Nat_big_num.num

The following two bit ranges are reserved for OS- and processor-specific * flags respectively.

Sourceval elf_pf_maskproc : Nat_big_num.num

val exact_permissions_of_permission : 
  Nat_big_num.num ->
  Nat_big_num.num Error.error

exact_permission_of_permission m: ELF has two interpretations of a RWX-style * permission bit m, an exact permission and an allowable permission. These * permissions allow us to interpret a flag as an upper bound for behaviour and * an ABI-compliant implementation can choose to interpret the flag m as either. * * In the exact interpretation, the upper bound is exactly the natural interpretation * of the flag. This is encoded in exact_permission_of_permission, which is * a glorified identity function, though included for completeness.

val allowable_permissions_of_permission : 
  Nat_big_num.num ->
  Nat_big_num.num Error.error

allowable_permission_of_permission m: ELF has two interpretations of a RWX-style * permission bit m, an exact permission and an allowable permission. These * permissions allow us to interpret a flag as an upper bound for behaviour and * an ABI-compliant implementation can choose to interpret the flag m as either. * * In the allowable interpretation, the upper bound is more lax than the natural * interpretation of the flag.

Sourceval parse_elf_segment_permissions : Nat_big_num.num -> bool * bool * bool

elf64_interpreted_program_header_flags w extracts a boolean triple of flags * from the flags field of an interpreted segment.

Sourceval string_of_elf_segment_permissions : Nat_big_num.num -> string

string_of_elf_segment_permissions m produces a string-based representation * of an ELF segment's permission field. * TODO: expand this as is needed by the validation tests.

Program header table entry type

Sourcetype elf32_program_header_table_entry = {

elf32_p_type : Uint32_wrapper.uint32;
(*
Type of the segment
*)
elf32_p_offset : Uint32_wrapper.uint32;
(*
Offset from beginning of file for segment
*)
elf32_p_vaddr : Uint32_wrapper.uint32;
(*
Virtual address for segment in memory
*)
elf32_p_paddr : Uint32_wrapper.uint32;
(*
Physical address for segment
*)
elf32_p_filesz : Uint32_wrapper.uint32;
(*
Size of segment in file, in bytes
*)
elf32_p_memsz : Uint32_wrapper.uint32;
(*
Size of segment in memory image, in bytes
*)
elf32_p_flags : Uint32_wrapper.uint32;
(*
Segment flags
*)
elf32_p_align : Uint32_wrapper.uint32;
(*
Segment alignment memory for memory and file
*)

}

Type elf32_program_header_table_entry encodes a program header table entry * for 32-bit platforms. Each entry describes a segment in an executable or * shared object file.

val compare_elf32_program_header_table_entry : 
  elf32_program_header_table_entry ->
  elf32_program_header_table_entry ->
  int

compare_elf32_program_header_table_entry ent1 ent2 is an ordering-comparison * function on program header table entries suitable for constructing sets, * finite maps, and other ordered data types with.

val instance_Basic_classes_Ord_Elf_program_header_table_elf32_program_header_table_entry_dict : 
  elf32_program_header_table_entry Lem_basic_classes.ord_class

Sourcetype elf64_program_header_table_entry = {

elf64_p_type : Uint32_wrapper.uint32;
(*
Type of the segment
*)
elf64_p_flags : Uint32_wrapper.uint32;
(*
Segment flags
*)
elf64_p_offset : Uint64_wrapper.uint64;
(*
Offset from beginning of file for segment
*)
elf64_p_vaddr : Uint64_wrapper.uint64;
(*
Virtual address for segment in memory
*)
elf64_p_paddr : Uint64_wrapper.uint64;
(*
Physical address for segment
*)
elf64_p_filesz : Uint64_wrapper.uint64;
(*
Size of segment in file, in bytes
*)
elf64_p_memsz : Uint64_wrapper.uint64;
(*
Size of segment in memory image, in bytes
*)
elf64_p_align : Uint64_wrapper.uint64;
(*
Segment alignment memory for memory and file
*)

}

Type elf64_program_header_table_entry encodes a program header table entry * for 64-bit platforms. Each entry describes a segment in an executable or * shared object file.

val compare_elf64_program_header_table_entry : 
  elf64_program_header_table_entry ->
  elf64_program_header_table_entry ->
  int

compare_elf64_program_header_table_entry ent1 ent2 is an ordering-comparison * function on program header table entries suitable for constructing sets, * finite maps, and other ordered data types with.

val instance_Basic_classes_Ord_Elf_program_header_table_elf64_program_header_table_entry_dict : 
  elf64_program_header_table_entry Lem_basic_classes.ord_class

val string_of_elf32_program_header_table_entry : 
  (Nat_big_num.num -> string) ->
  (Nat_big_num.num -> string) ->
  elf32_program_header_table_entry ->
  string

string_of_elf32_program_header_table_entry os proc et produces a string * representation of a 32-bit program header table entry using os and proc * to render OS- and processor-specific entries.

val string_of_elf64_program_header_table_entry : 
  (Nat_big_num.num -> string) ->
  (Nat_big_num.num -> string) ->
  elf64_program_header_table_entry ->
  string

string_of_elf64_program_header_table_entry os proc et produces a string * representation of a 64-bit program header table entry using os and proc * to render OS- and processor-specific entries.

val string_of_elf32_program_header_table_entry_default : 
  elf32_program_header_table_entry ->
  string

string_of_elf32_program_header_table_entry_default et produces a string representation * of table entry et where OS- and processor-specific entries are replaced with * default strings.

val string_of_elf64_program_header_table_entry_default : 
  elf64_program_header_table_entry ->
  string

string_of_elf64_program_header_table_entry_default et produces a string representation * of table entry et where OS- and processor-specific entries are replaced with * default strings.

val instance_Show_Show_Elf_program_header_table_elf32_program_header_table_entry_dict : 
  elf32_program_header_table_entry Show.show_class

val instance_Show_Show_Elf_program_header_table_elf64_program_header_table_entry_dict : 
  elf64_program_header_table_entry Show.show_class

Parsing and blitting

val bytes_of_elf32_program_header_table_entry : 
  Endianness.endianness ->
  elf32_program_header_table_entry ->
  Byte_sequence_wrapper.byte_sequence

bytes_of_elf32_program_header_table_entry ed ent blits a 32-bit program * header table entry ent into a byte sequence assuming endianness ed.

val bytes_of_elf64_program_header_table_entry : 
  Endianness.endianness ->
  elf64_program_header_table_entry ->
  Byte_sequence_wrapper.byte_sequence

bytes_of_elf64_program_header_table_entry ed ent blits a 64-bit program * header table entry ent into a byte sequence assuming endianness ed.

val read_elf32_program_header_table_entry : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (elf32_program_header_table_entry * Byte_sequence_wrapper.byte_sequence)
    Error.error

read_elf32_program_header_table_entry endian bs0 reads an ELF32 program header table * entry from byte sequence bs0 assuming endianness endian. If bs0 is larger * than necessary, the excess is returned from the function, too. * Fails if the entry cannot be read.

val read_elf64_program_header_table_entry : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (elf64_program_header_table_entry * Byte_sequence_wrapper.byte_sequence)
    Error.error

read_elf64_program_header_table_entry endian bs0 reads an ELF64 program header table * entry from byte sequence bs0 assuming endianness endian. If bs0 is larger * than necessary, the excess is returned from the function, too. * Fails if the entry cannot be read.

Program header table type

Sourcetype elf32_program_header_table = elf32_program_header_table_entry list

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

Sourcetype elf64_program_header_table = elf64_program_header_table_entry list

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

val bytes_of_elf32_program_header_table : 
  Endianness.endianness ->
  elf32_program_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence

bytes_of_elf32_program_header_table ed tbl blits an ELF32 program header * table into a byte sequence assuming endianness ed.

val bytes_of_elf64_program_header_table : 
  Endianness.endianness ->
  elf64_program_header_table_entry list ->
  Byte_sequence_wrapper.byte_sequence

bytes_of_elf64_program_header_table ed tbl blits an ELF64 program header * table into a byte sequence assuming endianness ed.

val read_elf32_program_header_table' : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  elf32_program_header_table_entry list Error.error

read_elf32_program_header_table' endian bs0 reads an ELF32 program header table from * byte_sequence bs0 assuming endianness endian. The byte_sequence bs0 is assumed * to have exactly the correct size for the table. For internal use, only. Use * read_elf32_program_header_table below instead.

val read_elf64_program_header_table' : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  elf64_program_header_table_entry list Error.error

read_elf64_program_header_table' endian bs0 reads an ELF64 program header table from * byte_sequence bs0 assuming endianness endian. The byte_sequence bs0 is assumed * to have exactly the correct size for the table. For internal use, only. Use * read_elf32_program_header_table below instead.

val read_elf32_program_header_table : 
  Nat_big_num.num ->
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (elf32_program_header_table_entry list * Byte_sequence_wrapper.byte_sequence)
    Error.error

read_elf32_program_header_table table_size endian bs0 reads an ELF32 program header * table from byte_sequence bs0 assuming endianness endian based on the size (in bytes) passed in via table_size. * This table_size argument should be equal to the number of entries in the * table multiplied by the fixed entry size. Bitstring bs0 may be larger than * necessary, in which case the excess is returned.

val read_elf64_program_header_table : 
  Nat_big_num.num ->
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (elf64_program_header_table_entry list * Byte_sequence_wrapper.byte_sequence)
    Error.error

read_elf64_program_header_table table_size endian bs0 reads an ELF64 program header * table from byte_sequence bs0 assuming endianness endian based on the size (in bytes) passed in via table_size. * This table_size argument should be equal to the number of entries in the * table multiplied by the fixed entry size. Bitstring bs0 may be larger than * necessary, in which case the excess is returned.

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

The pht_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_program_header_table : 
  ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
  elf32_program_header_table_entry list ->
  string

string_of_elf32_program_header_table os proc tbl produces a string representation * of program header table tbl using os and proc to render OS- and processor- * specific entries.

val string_of_elf64_program_header_table : 
  ((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
  elf64_program_header_table_entry list ->
  string

string_of_elf64_program_header_table os proc tbl produces a string representation * of program header table tbl using os and proc to render OS- and processor- * specific entries.

Static/dynamic linkage

Sourceval get_elf32_dynamic_linked : elf32_program_header_table_entry list -> bool

get_elf32_dynamic_linked pht tests whether an ELF32 file is a dynamically * linked object by traversing the program header table and attempting to find * a header describing a segment with the name of an associated interpreter. * Returns true if any such header is found, false --- indicating static * linkage --- otherwise.

Sourceval get_elf64_dynamic_linked : elf64_program_header_table_entry list -> bool

get_elf64_dynamic_linked pht tests whether an ELF64 file is a dynamically * linked object by traversing the program header table and attempting to find * a header describing a segment with the name of an associated interpreter. * Returns true if any such header is found, false --- indicating static * linkage --- otherwise.

Sourceval get_elf32_static_linked : elf32_program_header_table_entry list -> bool

get_elf32_static_linked is a utility function defined as the inverse * of get_elf32_dynamic_linked.

Sourceval get_elf64_static_linked : elf64_program_header_table_entry list -> bool

get_elf64_static_linked is a utility function defined as the inverse * of get_elf64_dynamic_linked.

val get_elf32_requested_interpreter : 
  elf32_program_header_table_entry ->
  Byte_sequence_wrapper.byte_sequence ->
  string Error.error

get_elf32_requested_interpreter ent bs0 extracts the requested interpreter * of a dynamically linkable ELF file from that file's program header table * entry of type PT_INTERP, ent. Interpreter string is extracted from byte * sequence bs0. * Fails if ent is not of type PT_INTERP, or if transcription otherwise fails.

val get_elf64_requested_interpreter : 
  elf64_program_header_table_entry ->
  Byte_sequence_wrapper.byte_sequence ->
  string Error.error

get_elf64_requested_interpreter ent bs0 extracts the requested interpreter * of a dynamically linkable ELF file from that file's program header table * entry of type PT_INTERP, ent. Interpreter string is extracted from byte * sequence bs0. * Fails if ent is not of type PT_INTERP, or if transcription otherwise fails.