linksem
  1. Overview
  2. Docs
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
type element = {
  1. startpos : Nat_big_num.num option;
  2. length1 : Nat_big_num.num option;
  3. contents : Byte_pattern.byte_pattern;
}
type allocated_symbols_map = (string, Nat_big_num.num * Nat_big_num.num) Pmap.map
type 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
and expr_unary_operation =
  1. | Neg of expr_operand
  2. | BitwiseInverse of expr_operand
and 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
type expr_binary_relation =
  1. | Lt
  2. | Lte
  3. | Gt
  4. | Gte
  5. | Eq
  6. | Neq
type 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
type memory_image = (string, element) Pmap.map
type element_range = string * range
type 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;
}
val symDefCompare : symbol_definition -> symbol_definition -> int
val instance_Basic_classes_Ord_Memory_image_symbol_definition_dict : symbol_definition Lem_basic_classes.ord_class
type 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;
}
val symRefCompare : symbol_reference -> symbol_reference -> int
val instance_Basic_classes_Ord_Memory_image_symbol_reference_dict : symbol_reference Lem_basic_classes.ord_class
type 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;
}
val relocSiteCompare : reloc_site -> reloc_site -> int
val instance_Basic_classes_Ord_Memory_image_reloc_site_dict : reloc_site Lem_basic_classes.ord_class
type reloc_decision =
  1. | LeaveReloc
  2. | ApplyReloc
  3. | ChangeRelocTo of Nat_big_num.num * symbol_reference * reloc_site
val relocDecisionCompare : reloc_decision -> reloc_decision -> int
val instance_Basic_classes_Ord_Memory_image_reloc_decision_dict : reloc_decision Lem_basic_classes.ord_class
type 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;
}
val symRefAndRelocSiteCompare : symbol_reference_and_reloc_site -> symbol_reference_and_reloc_site -> int
val instance_Basic_classes_Ord_Memory_image_symbol_reference_and_reloc_site_dict : symbol_reference_and_reloc_site Lem_basic_classes.ord_class
type !'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
type !'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;
}
val get_empty_memory_image : unit -> 'abifeature annotated_memory_image
val elf_section_is_special : Elf_interpreted_section.elf64_interpreted_section -> 'a -> bool
type null_abi_feature = unit
type !'abifeature reloc_fn = Nat_big_num.num -> bool * 'abifeature reloc_apply_fn
val noop_reloc_calculate : 'a -> 'b -> Nat_big_num.num -> Nat_big_num.num
val 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)
type !'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;
}
val uint32_max : Nat_big_num.num
val uint64_max : Nat_big_num.num
val address_of_range : (string * (Nat_big_num.num * 'a)) -> 'b annotated_memory_image -> Nat_big_num.num
val range_contains : (Nat_big_num.num * Nat_big_num.num) -> (Nat_big_num.num * Nat_big_num.num) -> bool
val range_overlaps : (Nat_big_num.num * Nat_big_num.num) -> (Nat_big_num.num * Nat_big_num.num) -> bool
val is_partition : (Nat_big_num.num * Nat_big_num.num) list -> (Nat_big_num.num * Nat_big_num.num) list -> bool
val expand_sorted_ranges : (Nat_big_num.num * Nat_big_num.num) list -> Nat_big_num.num -> bool list -> bool list
val expand_unsorted_ranges : (Nat_big_num.num * Nat_big_num.num) list -> Nat_big_num.num -> bool list -> bool list
val swap_pairs : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> ('b * 'a) Pset.set -> ('a * 'b) Pset.set
val 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
val 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
val filter_elements : ((string * element) -> bool) -> 'abifeature annotated_memory_image -> 'abifeature annotated_memory_image
val tag_image : 'abifeature range_tag -> string -> Nat_big_num.num -> Nat_big_num.num -> 'abifeature annotated_memory_image -> 'abifeature annotated_memory_image
val address_to_element_and_offset : Nat_big_num.num -> 'a annotated_memory_image -> (string * Nat_big_num.num) option
val element_and_offset_to_address : (string * Nat_big_num.num) -> 'a annotated_memory_image -> Nat_big_num.num option
val null_symbol_reference : symbol_reference
val null_elf_relocation_a : Elf_relocation.elf64_relocation_a
val null_symbol_reference_and_reloc_site : symbol_reference_and_reloc_site
val null_symbol_definition : symbol_definition
val pattern_possible_starts_in_one_byte_sequence : 'a option list -> 'a list -> Nat_big_num.num -> Nat_big_num.num list
val compute_virtual_address_adjustment : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
val natural_of_be_byte_list : char list -> Nat_big_num.num
val natural_of_le_byte_list : char list -> Nat_big_num.num
val natural_of_byte_list : Endianness.endianness -> char list -> Nat_big_num.num
val extract_natural_field : Nat_big_num.num -> element -> Nat_big_num.num -> Nat_big_num.num
val natural_to_le_byte_list : Nat_big_num.num -> char list
val natural_to_be_byte_list : Nat_big_num.num -> char list
val natural_to_byte_list : Endianness.endianness -> Nat_big_num.num -> char list
val natural_to_le_byte_list_padded_to : Nat_big_num.num -> Nat_big_num.num -> char list
val natural_to_be_byte_list_padded_to : Nat_big_num.num -> Nat_big_num.num -> char list
val natural_to_byte_list_padded_to : Endianness.endianness -> Nat_big_num.num -> Nat_big_num.num -> char list
val to_le_signed_bytes : Nat_big_num.num -> Nat_big_num.num -> char list
val to_le_unsigned_bytes : Nat_big_num.num -> Nat_big_num.num -> char list
val write_natural_field : Nat_big_num.num -> Nat_big_num.num -> element -> Nat_big_num.num -> element
val read_memory_image : 'a annotated_memory_image -> Nat_big_num.num -> Nat_big_num.num -> char list option
val read_memory_image_byte_sequence : 'a annotated_memory_image -> Nat_big_num.num -> Nat_big_num.num -> Byte_sequence_wrapper.byte_sequence option
val write_memory_image : 'abifeature annotated_memory_image -> Nat_big_num.num -> Byte_pattern.byte_pattern_element list -> 'abifeature annotated_memory_image
val memory_image_element_at : 'a annotated_memory_image -> Nat_big_num.num -> element option