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

Module Linker_scriptSource

Sourcetype input_section_rec = {
  1. idx : Nat_big_num.num;
  2. fname : string;
  3. img : Elf_memory_image.elf_memory_image;
  4. shndx : Nat_big_num.num;
  5. secname : string;
  6. isec : Elf_interpreted_section.elf64_interpreted_section;
}
Sourcetype input_spec =
  1. | Common of Nat_big_num.num * string * Elf_memory_image.elf_memory_image * Memory_image.symbol_definition
  2. | InputSection of input_section_rec
Sourcetype symbol_def_policy =
  1. | AlwaysDefine
  2. | ProvideIfUsed
Sourcetype input_selector = input_spec list -> input_spec list
Sourcetype address_expr = Memory_image.expr
Sourcetype output_guard =
  1. | AlwaysOutput
  2. | OnlyIfRo
  3. | OnlyIfRw
Sourcetype symbol_spec = Nat_big_num.num * Uint32_wrapper.uint32 * Uint32_wrapper.uint32
Sourcetype retain_policy =
  1. | DefaultKeep
  2. | KeepEvenWhenGC
Sourcetype address_expr_fn_ref = Nat_big_num.num
Sourcetype 'a address_expr_fn_map = (address_expr_fn_ref, Nat_big_num.num -> 'a -> Nat_big_num.num) Pmap.map
Sourcetype output_section_composition_element =
  1. | IncludeInputSection of retain_policy * input_section_rec
  2. | IncludeCommonSymbol of retain_policy * string * Nat_big_num.num * Memory_image.symbol_definition * Elf_memory_image.elf_memory_image
  3. | Hole of address_expr_fn
  4. | ProvideSymbol of symbol_def_policy * string * symbol_spec
Sourceand sort_policy =
  1. | DefaultSort
  2. | SeenOrder
  3. | ByName
  4. | ByNameThenAlignment
  5. | ByAlignment
  6. | ByAlignmentThenName
  7. | ByInitPriority
Sourceand output_section_spec =
  1. | OutputSectionSpec of output_guard * Nat_big_num.num option * string * output_section_composition_element list
Sourceand allocated_sections_map =
  1. | AllocatedSectionsMap of (string, output_section_spec * Nat_big_num.num) Pmap.map
Sourceand address_expr_fn =
  1. | AddressExprFn of address_expr_fn_ref
Sourcetype script_element =
  1. | DefineSymbol of symbol_def_policy * string * symbol_spec
  2. | AdvanceAddress of address_expr_fn
  3. | MarkAndAlignDataSegment of Nat_big_num.num * Nat_big_num.num
  4. | MarkDataSegmentEnd
  5. | MarkDataSegmentRelroEnd
  6. | OutputSection of output_guard * address_expr_fn option * string * script_element list
  7. | DiscardInput of input_selector
  8. | InputQuery of retain_policy * sort_policy * input_selector
Sourcetype linker_control_script = script_element list
Sourcetype labelled_linker_control_script = (script_element * Nat_big_num.num) list
Sourceval all_suffixes : char list -> char list list
Sourceval glob_match : char list -> char list -> bool
Sourceval default_symbol_spec : Nat_big_num.num * Uint32_wrapper.uint32 * Uint32_wrapper.uint32
Sourceval hidden_symbol_spec : Nat_big_num.num * Uint32_wrapper.uint32 * Uint32_wrapper.uint32
Sourceval only_sections : input_spec list -> input_spec list
Sourceval filter_and_concat : (input_spec -> bool) -> input_spec list -> input_spec list
Sourceval name_matches : string -> input_spec -> bool
Sourceval file_matches : string -> input_spec -> bool
Sourceval compareInputSpecByNameThenAlignment : input_spec -> input_spec -> int
Sourceval compareInputSpecByAlignment : input_spec -> input_spec -> int
Sourceval compareInputSpecByName : input_spec -> input_spec -> int
Sourceval compareInputSpecByAlignmentThenName : input_spec -> input_spec -> int
Sourceval compareInputSpecByInitPriority : 'a -> 'b -> int
Sourceval has_writability : 'a -> input_spec -> bool
Sourceval address_zero : Nat_big_num.num -> (Nat_big_num.num, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map -> Nat_big_num.num * (Nat_big_num.num, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map * address_expr_fn
Sourceval do_output_section_layout_starting_at_addr : Nat_big_num.num -> allocated_sections_map -> output_section_composition_element list -> Nat_big_num.num * Nat_big_num.num list
Sourceval output_sec_composition_size_given_start_addr : Nat_big_num.num -> allocated_sections_map -> output_section_composition_element list -> Nat_big_num.num
Sourceval sizeof : string -> allocated_sections_map -> Nat_big_num.num
Sourceval alignof_output_section_composition_element : output_section_composition_element -> Nat_big_num.num
Sourceval alignof_output_section : output_section_composition_element list -> Nat_big_num.num
Sourceval default_linker_control_script : Nat_big_num.num -> (Nat_big_num.num, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map -> 'a Memory_image.abi -> Nat_big_num.num option -> Nat_big_num.num option -> 'b -> Nat_big_num.num -> Nat_big_num.num * (Nat_big_num.num, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map * script_element list
Sourceval interpret_guard : output_guard -> output_section_composition_element list -> 'a -> bool
Sourceval label_script_aux : Nat_big_num.num -> script_element list -> (script_element * Nat_big_num.num) list
Sourceval label_script : script_element list -> (script_element * Nat_big_num.num) list
Sourcetype input_output_assignment = input_spec list * (output_section_spec * Nat_big_num.num) list
Sourceval assign_inputs_to_output_sections : (input_spec list * (output_section_spec * Nat_big_num.num) list) -> (Nat_big_num.num * Nat_big_num.num) Pset.set -> (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num) Pset.set -> input_spec list -> (output_section_spec * Nat_big_num.num) option -> input_spec option -> (input_spec -> input_spec -> int) -> labelled_linker_control_script -> input_spec list * (output_section_spec * Nat_big_num.num) list
Sourceval output_section_type : output_section_composition_element list -> Nat_big_num.num
Sourceval output_section_flags : output_section_composition_element list -> Nat_big_num.num
Sourceval symbol_def_for_provide_symbol : string -> Nat_big_num.num -> Uint32_wrapper.uint32 -> Uint32_wrapper.uint32 -> Nat_big_num.num -> Memory_image.symbol_definition
Sourceval assign_dot_to_itself : Nat_big_num.num -> (Nat_big_num.num, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map -> Nat_big_num.num * (Nat_big_num.num, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map * address_expr_fn
Sourceval build_image : 'a Memory_image.abi -> (address_expr_fn_ref, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map -> Elf_memory_image.elf_memory_image -> Nat_big_num.num -> allocated_sections_map -> (string, (Nat_big_num.num * ((Nat_big_num.num * Memory_image.symbol_reference * Linkable_list.linkable_item) * (Nat_big_num.num * Memory_image.symbol_definition * Linkable_list.linkable_item) option)) list) Pmap.map -> (script_element * Nat_big_num.num) list -> Nat_big_num.num -> 'b -> Abis.any_abi_feature Memory_image.annotated_memory_image * allocated_sections_map
Sourceval default_place_orphans : (input_spec list * (output_section_spec * Nat_big_num.num) list) -> input_spec list -> input_spec list * (output_section_spec * Nat_big_num.num) list
Sourceval interpret_linker_control_script : (address_expr_fn_ref, Nat_big_num.num -> allocated_sections_map -> Nat_big_num.num) Pmap.map -> script_element list -> Linkable_list.linkable_item list -> Nat_big_num.num -> 'a Memory_image.abi -> input_spec list -> (input_spec -> input_spec -> int) -> ((input_spec list * (output_section_spec * Nat_big_num.num) list) -> input_spec list -> 'b * (output_section_spec * Nat_big_num.num) list) -> (string, (Nat_big_num.num * ((Nat_big_num.num * Memory_image.symbol_reference * Linkable_list.linkable_item) * (Nat_big_num.num * Memory_image.symbol_definition * Linkable_list.linkable_item) option)) list) Pmap.map -> Abis.any_abi_feature Memory_image.annotated_memory_image * (string, (Nat_big_num.num * Linkable_list.binding) list) Pmap.map