package linksem

  1. Overview
  2. Docs
A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct