package linksem

You can search for identifiers within the package.

in-package search v0.2.0

linksem_zarith

Legend:
Library
Module
Module type
Parameter
Class
Class type

abi_utilities, generic utilities shared between all ABIs.

type integer_bit_width =

| I8
(*
Signed 8 bit
*)
| I12
| U12
(*
Unsigned 12 bit
*)
| Low14
| U15
(*
Unsigned 15 bit
*)
| I15
| I16
(*
Signed 16 bit
*)
| Half16ds
| I20
(*
Signed 20 bit
*)
| Low24
| I27
| Word30
| I32
(*
Signed 32 bit
*)
| I48
(*
Signed 48 bit
*)
| I64
(*
Signed 64 bit
*)
| I64X2
(*
Signed 128 bit
*)
| U16
(*
Unsigned 16 bit
*)
| U24
(*
Unsigned 24 bit
*)
| U32
(*
Unsigned 32 bit
*)
| U48
(*
Unsigned 48 bit
*)
| 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.

val 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.

type relocation_operator =

| TPRel
| LTOff
| DTPMod
| DTPRel
| Page
| GDat
| G
| GLDM
| GTPRel
| GTLSDesc
| Delta
| LDM
| TLSDesc
| Indirect
| Lo
| Hi
| Ha
| Higher
| HigherA
| Highest
| 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.

type relocation_operator2 =

| GTLSIdx

relocation_operator2 is a binary relocation operator, as detailed above.

Generalising and abstracting over relocation calculations and their return * types

type ('k, 'v) val_map = ('k, 'v) Pmap.map

val lookupM : 'a -> 'b -> ('b, 'v) Pmap.map -> 'v Error.error

type 'a can_fail =

| CanFail
(*
CanFail signals a potential failing relocation calculation when width constraints are invalidated
*)
| CanFailOnTest of 'a -> bool
(*
CanFailOnTest p signals a potentially failing relocation calculation when predicate p on the result of the calculation returns false
*)
| 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.

type 'a relocation_operator_expression =

| Lift of 'a
(*
Lift a base type into an AST
*)
| Apply of relocation_operator * 'a relocation_operator_expression
(*
Apply a unary operator to an expression
*)
| Apply2 of relocation_operator2 * 'a relocation_operator_expression * 'a relocation_operator_expression
(*
Apply a binary operator to two expressions
*)
| Plus of 'a relocation_operator_expression * 'a relocation_operator_expression
(*
Add two expressions.
*)
| Minus of 'a relocation_operator_expression * 'a relocation_operator_expression
(*
Subtract two expressions.
*)
| 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.

type ('addr, 'res) relocation_frame =

| Copy
| NoCopy of ('addr, 'res relocation_operator_expression * integer_bit_width * 'res can_fail) Pmap.map

val size_of_def : 
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num

val size_of_copy_reloc : 
  'a ->
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num

val 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

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