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

Module Abi_utilitiesSource

abi_utilities, generic utilities shared between all ABIs.

Sourcetype integer_bit_width =
  1. | I8
    (*

    Signed 8 bit

    *)
  2. | I12
  3. | U12
    (*

    Unsigned 12 bit

    *)
  4. | Low14
  5. | U15
    (*

    Unsigned 15 bit

    *)
  6. | I15
  7. | I16
    (*

    Signed 16 bit

    *)
  8. | Half16ds
  9. | I20
    (*

    Signed 20 bit

    *)
  10. | Low24
  11. | I27
  12. | Word30
  13. | I32
    (*

    Signed 32 bit

    *)
  14. | I48
    (*

    Signed 48 bit

    *)
  15. | I64
    (*

    Signed 64 bit

    *)
  16. | I64X2
    (*

    Signed 128 bit

    *)
  17. | U16
    (*

    Unsigned 16 bit

    *)
  18. | U24
    (*

    Unsigned 24 bit

    *)
  19. | U32
    (*

    Unsigned 32 bit

    *)
  20. | U48
    (*

    Unsigned 48 bit

    *)
  21. | U64
    (*

    Unsigned 64 bit

    *)

integer_bit_width records various bit widths for integral types, as used * in relocation calculations. The names are taken directly from the processor * supplements to keep the calculations as close as possible * to the specification of relocations.

Sourceval natural_of_integer_bit_width : integer_bit_width -> Nat_big_num.num

natural_of_integer_bit_width i computes the bit width of integer bit width * i.

Sourcetype relocation_operator =
  1. | TPRel
  2. | LTOff
  3. | DTPMod
  4. | DTPRel
  5. | Page
  6. | GDat
  7. | G
  8. | GLDM
  9. | GTPRel
  10. | GTLSDesc
  11. | Delta
  12. | LDM
  13. | TLSDesc
  14. | Indirect
  15. | Lo
  16. | Hi
  17. | Ha
  18. | Higher
  19. | HigherA
  20. | Highest
  21. | HighestA

relocation_operator records the operators used to calculate relocations by * the various ABIs. Each ABI will only use a subset of these, and they should * be interpreted on a per-ABI basis. As more ABIs are added, more operators * will be needed, and therefore more constructors in this type will need to * be added. These are unary operators, operating on a single integral type.

Sourcetype relocation_operator2 =
  1. | GTLSIdx

relocation_operator2 is a binary relocation operator, as detailed above.

Generalising and abstracting over relocation calculations and their return * types

Sourcetype ('k, 'v) val_map = ('k, 'v) Pmap.map
Sourceval lookupM : 'a -> 'b -> ('b, 'v) Pmap.map -> 'v Error.error
Sourcetype 'a can_fail =
  1. | CanFail
    (*

    CanFail signals a potential failing relocation calculation when width constraints are invalidated

    *)
  2. | CanFailOnTest of 'a -> bool
    (*

    CanFailOnTest p signals a potentially failing relocation calculation when predicate p on the result of the calculation returns false

    *)
  3. | CannotFail
    (*

    CannotFail states the relocation calculation cannot fail and bit-width constraints should be ignored

    *)

Some relocations may fail, for example: * Page 58, Power ABI: relocation types whose Field column is marked with an * asterisk are subject to failure is the value computed does not fit in the * allocated bits. can_fail type passes this information back to the caller * of the relocation application function.

Sourcetype 'a relocation_operator_expression =
  1. | Lift of 'a
    (*

    Lift a base type into an AST

    *)
  2. | Apply of relocation_operator * 'a relocation_operator_expression
    (*

    Apply a unary operator to an expression

    *)
  3. | Apply2 of relocation_operator2 * 'a relocation_operator_expression * 'a relocation_operator_expression
    (*

    Apply a binary operator to two expressions

    *)
  4. | Plus of 'a relocation_operator_expression * 'a relocation_operator_expression
    (*

    Add two expressions.

    *)
  5. | Minus of 'a relocation_operator_expression * 'a relocation_operator_expression
    (*

    Subtract two expressions.

    *)
  6. | RShift of 'a relocation_operator_expression * Nat_big_num.num
    (*

    Right shift the result of an expression m places.

    *)

relocation_operator_expression is an AST of expressions describing a relocation * calculation. An AST is used as it allows us to unify the treatment of relocation * calculation: rather than passing in dozens of functions to the calculation function * that perform the actual relocation, we can simply return a description (in the form * of the AST below) of the calculation to be carried out and have it interpreted * separately from the function that produces it. The type parameter 'a is the * type of base integral type. This AST suffices for the relocation calculations we * currently have implemented, but adding more ABIs may require that this type is * expanded.

Sourcetype ('addr, 'res) relocation_frame =
  1. | Copy
  2. | NoCopy of ('addr, 'res relocation_operator_expression * integer_bit_width * 'res can_fail) Pmap.map
Sourceval size_of_def : Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num
Sourceval size_of_copy_reloc : 'a -> Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num
Sourceval reloc_site_address : 'a Lem_basic_classes.ord_class -> 'b -> 'a Memory_image.annotated_memory_image -> Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num

Extracting useful information from relocs

Sourceval parse_elf64_relocation_info : Nat_big_num.num -> Nat_big_num.num * Nat_big_num.num