Module `Abis`Source

The abis module is the top-level module for all ABI related code, including * some generic functionality that works across all ABIs, and a primitive attempt * at abstracting over ABIs for purposes of linking.

Relocation operators and their validity on a given platform

Source

val is_valid_abi_aarch64_relocation_operator : 
  Abi_utilities.relocation_operator ->
  bool

Source

val is_valid_abi_aarch64_relocation_operator2 : 
  Abi_utilities.relocation_operator2 ->
  bool

Source

val is_valid_abi_amd64_relocation_operator : 
  Abi_utilities.relocation_operator ->
  bool

Sourceval is_valid_abi_amd64_relocation_operator2 : 'a -> bool

Sourceval is_valid_abi_power64_relocation_operator : 'a -> bool

Sourceval is_valid_abi_power64_relocation_operator2 : 'a -> bool

Misc. ABI related stuff

Sourcetype any_abi_feature =

| Amd64AbiFeature of any_abi_feature Abi_amd64.amd64_abi_feature
| Aarch64LeAbiFeature of Abi_aarch64_le.aarch64_le_abi_feature

Sourceval anyAbiFeatureCompare : any_abi_feature -> any_abi_feature -> int

Sourceval anyAbiFeatureTagEquiv : any_abi_feature -> any_abi_feature -> bool

Source

val instance_Basic_classes_Ord_Abis_any_abi_feature_dict : 
  any_abi_feature Lem_basic_classes.ord_class

Source

val instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict : 
  any_abi_feature Abi_classes.abiFeatureTagEquiv_class

Source

val make_elf64_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 ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Elf_header.elf64_header

Sourceval phdr_flags_from_section_flags : Nat_big_num.num -> 'a -> Nat_big_num.num

Sourceval phdr_is_writable : Nat_big_num.num -> bool

Sourcetype can_combine_flags_fn = Nat_big_num.num Pset.set -> Nat_big_num.num option

Sourceval load_can_combine_flags : Nat_big_num.num Pset.set -> Nat_big_num.num option

Sourceval tls_can_combine_flags : Nat_big_num.num Pset.set -> Nat_big_num.num option

Source

val maybe_extend_phdr : 
  Elf_program_header_table.elf64_program_header_table_entry ->
  Elf_interpreted_section.elf64_interpreted_section ->
  (Nat_big_num.num Pset.set -> Nat_big_num.num option) ->
  Elf_program_header_table.elf64_program_header_table_entry option

Source

val make_new_phdr : 
  Elf_interpreted_section.elf64_interpreted_section ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Elf_program_header_table.elf64_program_header_table_entry

Source

val make_load_phdrs : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a ->
  Elf_interpreted_section.elf64_interpreted_section list ->
  Elf_program_header_table.elf64_program_header_table_entry list

Sourceval tls_extend : 'abifeature Memory_image.abi -> 'abifeature Memory_image.abi

Source

val make_default_phdrs : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a ->
  'b ->
  Elf_interpreted_section.elf64_interpreted_section list ->
  Elf_program_header_table.elf64_program_header_table_entry list

Source

val find_start_symbol_address : 
  'a Lem_basic_classes.ord_class ->
  'a Abi_classes.abiFeatureTagEquiv_class ->
  'a Memory_image.annotated_memory_image ->
  Nat_big_num.num option

Sourceval pad_zeroes : Nat_big_num.num -> char list

Sourceval pad_0x90 : Nat_big_num.num -> char list

Sourceval null_abi : any_abi_feature Memory_image.abi

Sourceval got_entry_ordering : ('a * 'b) -> ('a * 'c) -> int

Sourceval is_ifunc_def : Memory_image.symbol_definition option -> bool

Source

val amd64_reloc_needs_got_slot : 
  'a ->
  Memory_image.reloc_site ->
  Memory_image.symbol_definition option ->
  bool

Source

val amd64_reloc_needs_plt_slot : 
  Memory_image.symbol_reference_and_reloc_site ->
  Memory_image.reloc_site ->
  Memory_image.symbol_definition option ->
  (Memory_image.reloc_site -> bool) ->
  bool

Source

val amd64_find_got_label_and_element : 
  any_abi_feature Memory_image.annotated_memory_image ->
  ((string * Memory_image.symbol_definition option) list * Memory_image.element)
    option

Source

val amd64_find_plt_label_and_element : 
  any_abi_feature Memory_image.annotated_memory_image ->
  ((string
    * Memory_image.symbol_definition option
    * (Nat_big_num.num ->
    Nat_big_num.num ->
    Nat_big_num.num * char list))
     list
   * Memory_image.element)
    option

Source

val got_slot_index_for_symname : 
  'a Lem_basic_classes.eq_class ->
  'a ->
  ('a * 'b) list ->
  int option

Source

val amd64_get_reloc_symaddr : 
  Memory_image.symbol_definition ->
  any_abi_feature Memory_image.annotated_memory_image ->
  (Memory_image.element_range option * Memory_image.symbol_definition) list ->
  'a ->
  Nat_big_num.num

Source

val amd64_generate_support : 
  ('a * any_abi_feature Memory_image.annotated_memory_image) list ->
  any_abi_feature Memory_image.annotated_memory_image

Source

val amd64_concretise_support : 
  any_abi_feature Memory_image.annotated_memory_image ->
  any_abi_feature Memory_image.annotated_memory_image

Source

val amd64_got_slot_idx : 
  any_abi_feature Memory_image.annotated_memory_image ->
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num

Source

val amd64_got_slot_addr : 
  any_abi_feature Memory_image.annotated_memory_image ->
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num

Source

val amd64_plt_slot_addr : 
  any_abi_feature Memory_image.annotated_memory_image ->
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num ->
  Nat_big_num.num

Source

val amd64_base_addr : 
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num ->
  Nat_big_num.num

amd64_base_addr rr site_addr computes back the base address at which a * shared object has been loaded into memory during execution. It's kind of * lame to have this function because the linker will do the opposite operation * when relocating, but I don't want to add a new argument to the reloc * function.

Source

val amd64_reloc : 
  Nat_big_num.num ->
  bool
  * (any_abi_feature Memory_image.annotated_memory_image ->
  Nat_big_num.num ->
  Memory_image.symbol_reference_and_reloc_site ->
  Nat_big_num.num
  * (Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num))

amd64_reloc r yields a function that applies relocations of type r.

Sourceval sysv_amd64_std_abi : any_abi_feature Memory_image.abi

Sourceval sysv_aarch64_le_std_abi : any_abi_feature Memory_image.abi

Sourceval sysv_mips64_std_abi : any_abi_feature Memory_image.abi

Sourceval sysv_cheri_mips64_std_abi : any_abi_feature Memory_image.abi

Sourceval all_abis : any_abi_feature Memory_image.abi list

package linksem

Module AbisSource

Module `Abis`Source