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

Module Memory_imageSource

Sourcetype element = {
  1. startpos : Nat_big_num.num option;
  2. length1 : Nat_big_num.num option;
  3. contents : Byte_pattern.byte_pattern;
}
Sourcetype allocated_symbols_map = (string, Nat_big_num.num * Nat_big_num.num) Pmap.map
Sourcetype expr_operand =
  1. | Var of string
  2. | CursorPosition
  3. | Constant of Nat_big_num.num
  4. | UnOp of expr_unary_operation * expr_operand
  5. | BinOp of expr_binary_operation * expr_operand * expr_operand
Sourceand expr_unary_operation =
  1. | Neg of expr_operand
  2. | BitwiseInverse of expr_operand
Sourceand expr_binary_operation =
  1. | Add of expr_operand * expr_operand
  2. | Sub of expr_operand * expr_operand
  3. | BitwiseAnd of expr_operand * expr_operand
  4. | BitwiseOr of expr_operand * expr_operand
Sourcetype expr_binary_relation =
  1. | Lt
  2. | Lte
  3. | Gt
  4. | Gte
  5. | Eq
  6. | Neq
Sourcetype expr =
  1. | False
  2. | True
  3. | Not of expr
  4. | And of expr * expr
  5. | Or of expr * expr
  6. | BinRel of expr_binary_relation * expr_operand
Sourcetype memory_image = (string, element) Pmap.map
Sourcetype range = Nat_big_num.num * Nat_big_num.num
Sourcetype element_range = string * range
Sourcetype elf_file_feature =
  1. | ElfHeader of Elf_header.elf64_header
  2. | ElfSectionHeaderTable of Elf_section_header_table.elf64_section_header_table
  3. | ElfProgramHeaderTable of Elf_program_header_table.elf64_program_header_table
  4. | ElfSection of Nat_big_num.num * Elf_interpreted_section.elf64_interpreted_section
  5. | ElfSegment of Nat_big_num.num * Elf_interpreted_segment.elf64_interpreted_segment
Sourcetype symbol_definition = {
  1. def_symname : string;
  2. def_syment : Elf_symbol_table.elf64_symbol_table_entry;
  3. def_sym_scn : Nat_big_num.num;
  4. def_sym_idx : Nat_big_num.num;
  5. def_linkable_idx : Nat_big_num.num;
}
Sourceval symDefCompare : symbol_definition -> symbol_definition -> int
Sourceval instance_Basic_classes_Ord_Memory_image_symbol_definition_dict : symbol_definition Lem_basic_classes.ord_class
Sourcetype symbol_reference = {
  1. ref_symname : string;
  2. ref_syment : Elf_symbol_table.elf64_symbol_table_entry;
  3. ref_sym_scn : Nat_big_num.num;
  4. ref_sym_idx : Nat_big_num.num;
}
Sourceval symRefCompare : symbol_reference -> symbol_reference -> int
Sourceval instance_Basic_classes_Ord_Memory_image_symbol_reference_dict : symbol_reference Lem_basic_classes.ord_class
Sourcetype reloc_site = {
  1. ref_relent : Elf_relocation.elf64_relocation_a;
  2. ref_rel_scn : Nat_big_num.num;
  3. ref_rel_idx : Nat_big_num.num;
  4. ref_src_scn : Nat_big_num.num;
}
Sourceval relocSiteCompare : reloc_site -> reloc_site -> int
Sourceval instance_Basic_classes_Ord_Memory_image_reloc_site_dict : reloc_site Lem_basic_classes.ord_class
Sourcetype reloc_decision =
  1. | LeaveReloc
  2. | ApplyReloc
  3. | ChangeRelocTo of Nat_big_num.num * symbol_reference * reloc_site
Sourceval relocDecisionCompare : reloc_decision -> reloc_decision -> int
Sourceval instance_Basic_classes_Ord_Memory_image_reloc_decision_dict : reloc_decision Lem_basic_classes.ord_class
Sourcetype symbol_reference_and_reloc_site = {
  1. ref : symbol_reference;
  2. maybe_reloc : reloc_site option;
  3. maybe_def_bound_to : (reloc_decision * symbol_definition option) option;
}
Sourceval instance_Basic_classes_Ord_Memory_image_symbol_reference_and_reloc_site_dict : symbol_reference_and_reloc_site Lem_basic_classes.ord_class
Sourcetype 'abifeature range_tag =
  1. | ImageBase
  2. | EntryPoint
  3. | SymbolDef of symbol_definition
  4. | SymbolRef of symbol_reference_and_reloc_site
  5. | FileFeature of elf_file_feature
  6. | AbiFeature of 'abifeature
Sourcetype 'abifeature annotated_memory_image = {
  1. elements : memory_image;
  2. by_range : (element_range option * 'abifeature range_tag) Pset.set;
  3. by_tag : ('abifeature range_tag, element_range option) Multimap.multimap;
}
Sourceval get_empty_memory_image : unit -> 'abifeature annotated_memory_image
Sourceval elf_section_is_special : Elf_interpreted_section.elf64_interpreted_section -> 'a -> bool
Sourcetype null_abi_feature = unit
Sourcetype reloc_calculate_fn = Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourcetype 'abifeature reloc_apply_fn = 'abifeature annotated_memory_image -> Nat_big_num.num -> symbol_reference_and_reloc_site -> Nat_big_num.num * reloc_calculate_fn
Sourcetype 'abifeature reloc_fn = Nat_big_num.num -> bool * 'abifeature reloc_apply_fn
Sourceval noop_reloc_calculate : 'a -> 'b -> Nat_big_num.num -> Nat_big_num.num
Sourceval noop_reloc_apply : 'a -> 'b -> 'c -> Nat_big_num.num * (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num)
Sourceval noop_reloc : 'a -> bool * ('abifeature annotated_memory_image -> Nat_big_num.num -> symbol_reference_and_reloc_site -> Nat_big_num.num * reloc_calculate_fn)
Sourcetype 'abifeature abi = {
  1. is_valid_elf_header : Elf_header.elf64_header -> bool;
  2. make_elf_header : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Elf_header.elf64_header;
  3. reloc : 'abifeature reloc_fn;
  4. section_is_special : Elf_interpreted_section.elf64_interpreted_section -> 'abifeature annotated_memory_image -> bool;
  5. section_is_large : Elf_interpreted_section.elf64_interpreted_section -> 'abifeature annotated_memory_image -> bool;
  6. maxpagesize : Nat_big_num.num;
  7. minpagesize : Nat_big_num.num;
  8. commonpagesize : Nat_big_num.num;
  9. symbol_is_generated_by_linker : string -> bool;
  10. make_phdrs : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> 'abifeature annotated_memory_image -> Elf_interpreted_section.elf64_interpreted_section list -> Elf_program_header_table.elf64_program_header_table_entry list;
  11. max_phnum : Nat_big_num.num;
  12. guess_entry_point : 'abifeature annotated_memory_image -> Nat_big_num.num option;
  13. pad_data : Nat_big_num.num -> char list;
  14. pad_code : Nat_big_num.num -> char list;
  15. generate_support : (string * 'abifeature annotated_memory_image) list -> 'abifeature annotated_memory_image;
  16. concretise_support : 'abifeature annotated_memory_image -> 'abifeature annotated_memory_image;
  17. get_reloc_symaddr : symbol_definition -> 'abifeature annotated_memory_image -> (element_range option * symbol_definition) list -> reloc_site option -> Nat_big_num.num;
  18. parse_reloc_info : Uint64_wrapper.uint64 -> Nat_big_num.num * Nat_big_num.num;
}
Sourceval align_up_to : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval round_down_to : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval uint32_max : Nat_big_num.num
Sourceval uint64_max : Nat_big_num.num
Sourceval compl64 : Nat_big_num.num -> Nat_big_num.num
Sourceval gcd : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval lcm : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval address_of_range : (string * (Nat_big_num.num * 'a)) -> 'b annotated_memory_image -> Nat_big_num.num
Sourceval range_contains : (Nat_big_num.num * Nat_big_num.num) -> (Nat_big_num.num * Nat_big_num.num) -> bool
Sourceval range_overlaps : (Nat_big_num.num * Nat_big_num.num) -> (Nat_big_num.num * Nat_big_num.num) -> bool
Sourceval is_partition : (Nat_big_num.num * Nat_big_num.num) list -> (Nat_big_num.num * Nat_big_num.num) list -> bool
Sourceval nat_range : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num list
Sourceval expand_sorted_ranges : (Nat_big_num.num * Nat_big_num.num) list -> Nat_big_num.num -> bool list -> bool list
Sourceval expand_unsorted_ranges : (Nat_big_num.num * Nat_big_num.num) list -> Nat_big_num.num -> bool list -> bool list
Sourceval swap_pairs : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> ('b * 'a) Pset.set -> ('a * 'b) Pset.set
Sourceval by_range_from_by_tag : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> ('a * 'b) Pset.set -> ('b * 'a) Pset.set
Sourceval by_tag_from_by_range : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> ('a * 'b) Pset.set -> ('b * 'a) Pset.set
Sourceval filter_elements : ((string * element) -> bool) -> 'abifeature annotated_memory_image -> 'abifeature annotated_memory_image
Sourceval tag_image : 'abifeature range_tag -> string -> Nat_big_num.num -> Nat_big_num.num -> 'abifeature annotated_memory_image -> 'abifeature annotated_memory_image
Sourceval address_to_element_and_offset : Nat_big_num.num -> 'a annotated_memory_image -> (string * Nat_big_num.num) option
Sourceval element_and_offset_to_address : (string * Nat_big_num.num) -> 'a annotated_memory_image -> Nat_big_num.num option
Sourceval null_symbol_reference : symbol_reference
Sourceval null_elf_relocation_a : Elf_relocation.elf64_relocation_a
Sourceval null_symbol_reference_and_reloc_site : symbol_reference_and_reloc_site
Sourceval null_symbol_definition : symbol_definition
Sourceval pattern_possible_starts_in_one_byte_sequence : 'a option list -> 'a list -> Nat_big_num.num -> Nat_big_num.num list
Sourceval compute_virtual_address_adjustment : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval natural_of_be_byte_list : char list -> Nat_big_num.num
Sourceval natural_of_le_byte_list : char list -> Nat_big_num.num
Sourceval natural_of_byte_list : Endianness.endianness -> char list -> Nat_big_num.num
Sourceval extract_natural_field : Nat_big_num.num -> element -> Nat_big_num.num -> Nat_big_num.num
Sourceval natural_to_le_byte_list : Nat_big_num.num -> char list
Sourceval natural_to_be_byte_list : Nat_big_num.num -> char list
Sourceval natural_to_byte_list : Endianness.endianness -> Nat_big_num.num -> char list
Sourceval natural_to_le_byte_list_padded_to : Nat_big_num.num -> Nat_big_num.num -> char list
Sourceval natural_to_be_byte_list_padded_to : Nat_big_num.num -> Nat_big_num.num -> char list
Sourceval natural_to_byte_list_padded_to : Endianness.endianness -> Nat_big_num.num -> Nat_big_num.num -> char list
Sourceval n2i : Nat_big_num.num -> Nat_big_num.num
Sourceval i2n : Nat_big_num.num -> Nat_big_num.num
Sourceval i2n_signed : Nat_num.nat -> Nat_big_num.num -> Nat_big_num.num
Sourceval to_le_signed_bytes : Nat_big_num.num -> Nat_big_num.num -> char list
Sourceval to_le_unsigned_bytes : Nat_big_num.num -> Nat_big_num.num -> char list
Sourceval write_natural_field : Nat_big_num.num -> Nat_big_num.num -> element -> Nat_big_num.num -> element
Sourceval read_memory_image : 'a annotated_memory_image -> Nat_big_num.num -> Nat_big_num.num -> char list option
Sourceval read_memory_image_byte_sequence : 'a annotated_memory_image -> Nat_big_num.num -> Nat_big_num.num -> Byte_sequence_wrapper.byte_sequence option
Sourceval write_memory_image : 'abifeature annotated_memory_image -> Nat_big_num.num -> Byte_pattern.byte_pattern_element list -> 'abifeature annotated_memory_image
Sourceval mask_memory_image : 'a annotated_memory_image -> Nat_big_num.num -> Nat_big_num.num -> 'a annotated_memory_image
Sourceval memory_image_element_at : 'a annotated_memory_image -> Nat_big_num.num -> element option
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