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_segment/index.html

Module Elf_interpreted_segmentSource

elf_interpreted_segment defines interpreted segments, i.e. the contents of * a program header table entry converted to more amenable types, and operations * built on top of them.

Sourcetype elf32_interpreted_segment = {
  1. elf32_segment_body : Byte_sequence.byte_sequence0;
    (*

    Body of the segment

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

    Type of the segment

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

    Size of the segment in bytes

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

    Size of the segment in memory in bytes

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

    Base address of the segment

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

    Physical address of segment

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

    Alignment of the segment

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

    Offset of the segment

    *)
  9. elf32_segment_flags : bool * bool * bool;
    (*

    READ, WRITE, EXECUTE flags.

    *)
}

elf32_interpreted_segment represents an ELF32 interpreted segment, i.e. the * contents of an ELF program header table entry converted into more amenable * (infinite precision) types, for manipulation. * Invariant: the nth entry of the program header table corresponds to the nth * entry of the list of interpreted segments in an elf32_file record. The * lengths of the two lists are exactly the same.

Sourcetype elf64_interpreted_segment = {
  1. elf64_segment_body : Byte_sequence.byte_sequence0;
    (*

    Body of the segment

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

    Type of the segment

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

    Size of the segment in bytes

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

    Size of the segment in memory in bytes

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

    Base address of the segment

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

    Physical address of segment

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

    Alignment of the segment

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

    Offset of the segment

    *)
  9. elf64_segment_flags : bool * bool * bool;
    (*

    READ, WRITE, EXECUTE flags.

    *)
}

elf64_interpreted_segment represents an ELF64 interpreted segment, i.e. the * contents of an ELF program header table entry converted into more amenable * (infinite precision) types, for manipulation. * Invariant: the nth entry of the program header table corresponds to the nth * entry of the list of interpreted segments in an elf64_file record. The * lengths of the two lists are exactly the same.

Sourceval compare_elf64_interpreted_segment : elf64_interpreted_segment -> elf64_interpreted_segment -> int

compare_elf64_interpreted_segment seg1 seg2 is an ordering comparison function * on interpreted segments suitable for constructing sets, finite maps and other * ordered data types out of.

Sourceval instance_Basic_classes_Ord_Elf_interpreted_segment_elf64_interpreted_segment_dict : elf64_interpreted_segment Lem_basic_classes.ord_class
Sourcetype elf32_interpreted_segments = elf32_interpreted_segment list
Sourcetype elf64_interpreted_segments = elf64_interpreted_segment list
Sourceval string_of_flags : (bool * bool * bool) -> string

string_of_flags bs produces a string-based representation of an interpreted * segments flags (represented as a boolean triple).

Sourceval string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string

string_of_elf32_interpreted_segment seg produces a string-based representation * of interpreted segment seg.

Sourceval string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string

string_of_elf64_interpreted_segment seg produces a string-based representation * of interpreted segment seg.