package linksem

  1. Overview
  2. Docs
A formalisation of the core ELF and DWARF file formats written in Lem

Install 

dune-project
 Dependency

github.com Edit opam file Versions (2)

Authors

  1. S
    Stephen Kell
  2. D
    Dominic Mulligan
  3. P
    Peter Sewell

Maintainers

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

Sources

0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Elf_interpreted_section/index.html

Module Elf_interpreted_sectionSource

Module elf_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.

Sourcetype elf32_interpreted_section = {
  1. elf32_section_name : Nat_big_num.num;
    (*

    Name of the section

    *)
  2. elf32_section_type : Nat_big_num.num;
    (*

    Type of the section

    *)
  3. elf32_section_flags : Nat_big_num.num;
    (*

    Flags associated with the section

    *)
  4. elf32_section_addr : Nat_big_num.num;
    (*

    Base address of the section in memory

    *)
  5. elf32_section_offset : Nat_big_num.num;
    (*

    Offset from beginning of file

    *)
  6. elf32_section_size : Nat_big_num.num;
    (*

    Section size in bytes

    *)
  7. elf32_section_info : Nat_big_num.num;
    (*

    Extra information, depends on section type

    *)
  8. elf32_section_align : Nat_big_num.num;
    (*

    Alignment constraints for section

    *)
  9. elf32_section_entsize : Nat_big_num.num;
    (*

    Size of each entry in table, if section is one

    *)
  10. elf32_section_body : Byte_sequence.byte_sequence0;
    (*

    Body of section

    *)
  11. elf32_section_name_as_string : string;
    (*

    Name of the section, as a string; "" for no name (name = 0)

    *)
}

elf32_interpreted_section exactly mirrors the structure of a section header * table entry, barring the conversion of all fields to more amenable types.

Sourceval elf32_interpreted_section_equal : elf32_interpreted_section -> elf32_interpreted_section -> bool

elf32_interpreted_section_equal s1 s2 is an equality test on interpreted * sections s1 and s2.

Sourceval instance_Basic_classes_Eq_Elf_interpreted_section_elf32_interpreted_section_dict : elf32_interpreted_section Lem_basic_classes.eq_class
Sourcetype elf64_interpreted_section = {
  1. elf64_section_name : Nat_big_num.num;
    (*

    Name of the section

    *)
  2. elf64_section_type : Nat_big_num.num;
    (*

    Type of the section

    *)
  3. elf64_section_flags : Nat_big_num.num;
    (*

    Flags associated with the section

    *)
  4. elf64_section_addr : Nat_big_num.num;
    (*

    Base address of the section in memory

    *)
  5. elf64_section_offset : Nat_big_num.num;
    (*

    Offset from beginning of file

    *)
  6. elf64_section_size : Nat_big_num.num;
    (*

    Section size in bytes

    *)
  7. elf64_section_info : Nat_big_num.num;
    (*

    Extra information, depends on section type

    *)
  8. elf64_section_align : Nat_big_num.num;
    (*

    Alignment constraints for section

    *)
  9. elf64_section_entsize : Nat_big_num.num;
    (*

    Size of each entry in table, if section is one

    *)
  10. elf64_section_body : Byte_sequence.byte_sequence0;
    (*

    Body of section

    *)
  11. elf64_section_name_as_string : string;
    (*

    Name of the section, as a string; "" for no name (name = 0)

    *)
}

elf64_interpreted_section exactly mirrors the structure of a section header * table entry, barring the conversion of all fields to more amenable types.

Sourceval compare_elf64_interpreted_section : elf64_interpreted_section -> elf64_interpreted_section -> int

compare_elf64_interpreted_section s1 s2 is an ordering comparison function * on interpreted sections suitable for use in sets, finite maps and other * ordered structures.

Sourceval instance_Basic_classes_Ord_Elf_interpreted_section_elf64_interpreted_section_dict : elf64_interpreted_section Lem_basic_classes.ord_class
Sourceval elf64_interpreted_section_equal : elf64_interpreted_section -> elf64_interpreted_section -> bool

elf64_interpreted_section_equal s1 s2 is an equality test on interpreted * sections s1 and s2.

Sourceval null_elf32_interpreted_section : elf32_interpreted_section

null_elf32_interpreted_section --- the null interpreted section.

Sourceval null_elf64_interpreted_section : elf64_interpreted_section

null_elf64_interpreted_section --- the null interpreted section.

Sourceval instance_Basic_classes_Eq_Elf_interpreted_section_elf64_interpreted_section_dict : elf64_interpreted_section Lem_basic_classes.eq_class
Sourceval elf64_interpreted_section_matches_section_header : elf64_interpreted_section -> Elf_section_header_table.elf64_section_header_table_entry -> bool

elf64_interpreted_section_matches_section_header sect ent checks whether * the interpreted section and the corresponding section header table entry * match.

Sourcetype elf32_interpreted_sections = elf32_interpreted_section list
Sourcetype elf64_interpreted_sections = elf64_interpreted_section list
Sourceval string_of_elf32_interpreted_section : elf32_interpreted_section -> string

string_of_elf32_interpreted_section sect returns a string-based representation * of interpreted section, sect.

Sourceval string_of_elf64_interpreted_section : elf64_interpreted_section -> string

string_of_elf64_interpreted_section sect returns a string-based representation * of interpreted section, sect.

Sourceval is_valid_elf32_section_header_table_entry : elf32_interpreted_section -> String_table.string_table -> bool

is_valid_elf32_section_header_table_entry sect stab checks whether a * interpreted section conforms with the prescribed flags and types declared * in the "special sections" table of the ELF specification. * TODO: some of these entries in the table are overridden by ABI supplements. * Make sure it is these that are passed in rather than the default table * declared in the spec?

Sourceval is_valid_elf64_section_header_table_entry : elf64_interpreted_section -> String_table.string_table -> bool

is_valid_elf64_section_header_table_entry sect stab checks whether a * interpreted section conforms with the prescribed flags and types declared * in the "special sections" table of the ELF specification. * TODO: some of these entries in the table are overridden by ABI supplements. * Make sure it is these that are passed in rather than the default table * declared in the spec?

Sourceval is_valid_elf32_section_header_table0 : elf32_interpreted_section list -> String_table.string_table -> bool

is_valid_elf32_section_header_table sects checks whether all entries in * sect are valid.

Sourceval is_valid_elf64_section_header_table0 : elf64_interpreted_section list -> String_table.string_table -> bool

is_valid_elf64_section_header_table sects checks whether all entries in * sect are valid.