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

Module Elf_relocationSource

elf_relocation formalises types, functions and other definitions for working * with ELF relocation and relocation with addend entries.

ELF relocation records

Sourcetype elf32_relocation = {
  1. elf32_r_offset : Uint32_wrapper.uint32;
    (*

    Address at which to relocate

    *)
  2. elf32_r_info : Uint32_wrapper.uint32;
    (*

    Symbol table index/type of relocation to apply

    *)
}

elf32_relocation is a simple relocation record (without addend).

Sourcetype elf32_relocation_a = {
  1. elf32_ra_offset : Uint32_wrapper.uint32;
    (*

    Address at which to relocate

    *)
  2. elf32_ra_info : Uint32_wrapper.uint32;
    (*

    Symbol table index/type of relocation to apply

    *)
  3. elf32_ra_addend : Int32.t;
    (*

    Addend used to compute value to be stored

    *)
}

elf32_relocation_a is a relocation record with addend.

Sourcetype elf64_relocation = {
  1. elf64_r_offset : Uint64_wrapper.uint64;
    (*

    Address at which to relocate

    *)
  2. elf64_r_info : Uint64_wrapper.uint64;
    (*

    Symbol table index/type of relocation to apply

    *)
}

elf64_relocation is a simple relocation record (without addend).

Sourcetype elf64_relocation_a = {
  1. elf64_ra_offset : Uint64_wrapper.uint64;
    (*

    Address at which to relocate

    *)
  2. elf64_ra_info : Uint64_wrapper.uint64;
    (*

    Symbol table index/type of relocation to apply

    *)
  3. elf64_ra_addend : Int64.t;
    (*

    Addend used to compute value to be stored

    *)
}

elf64_relocation_a is a relocation record with addend.

Sourceval elf64_relocation_a_compare : elf64_relocation_a -> elf64_relocation_a -> int

elf64_relocation_a_compare r1 r2 is an ordering comparison function for * relocation with addend records suitable for constructing sets, finite map * and other ordered data structures. * NB: we exclusively use elf64_relocation_a in range tags, regardless of what * file/reloc the info came from, so only this one needs an Ord instance.

Sourceval instance_Basic_classes_Ord_Elf_relocation_elf64_relocation_a_dict : elf64_relocation_a Lem_basic_classes.ord_class

Reading relocation entries

read_elf32_relocation ed bs0 parses an elf32_relocation record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.

read_elf64_relocation ed bs0 parses an elf64_relocation record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.

read_elf32_relocation_a ed bs0 parses an elf32_relocation_a record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.

read_elf64_relocation_a ed bs0 parses an elf64_relocation_a record from * byte sequence bs0 assuming endianness ed. The suffix of bs0 remaining * after parsing is also returned. * Fails if the relocation record cannot be parsed.

read_elf32_relocation_section' ed bs0 parses a list of elf32_relocation * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.

read_elf64_relocation_section' ed bs0 parses a list of elf64_relocation * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.

read_elf32_relocation_a_section' ed bs0 parses a list of elf32_relocation_a * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.

read_elf64_relocation_a_section' ed bs0 parses a list of elf64_relocation_a * records from byte sequence bs0, which is assumed to have the exact size * required, assuming endianness ed. * Fails if any of the records cannot be parsed.

read_elf32_relocation_section sz ed bs0 reads in a list of elf32_relocation * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.

read_elf64_relocation_section sz ed bs0 reads in a list of elf64_relocation * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.

read_elf32_relocation_a_section sz ed bs0 reads in a list of elf32_relocation_a * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.

read_elf64_relocation_a_section sz ed bs0 reads in a list of elf64_relocation_a * records from a prefix of bs0 of size sz assuming endianness ed. The * suffix of bs0 remaining after parsing is also returned. * Fails if any of the records cannot be parsed or if the length of bs0 is * less than sz.