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/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