Module Abi_aarch64_relocationSource

abi_aarch64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AArch64 ABI (little-endian case).

Relocations

Sourceval r_aarch64_none : Nat_big_num.num
Sourceval r_aarch64_withdrawn : Nat_big_num.num

Treated as R_AARCH6_NONE

Sourceval r_aarch64_abs64 : Nat_big_num.num
Sourceval r_aarch64_abs32 : Nat_big_num.num
Sourceval r_aarch64_abs16 : Nat_big_num.num
Sourceval r_aarch64_prel64 : Nat_big_num.num
Sourceval r_aarch64_prel32 : Nat_big_num.num
Sourceval r_aarch64_prel16 : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g0 : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g0_nc : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g1 : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g1_nc : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g2 : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g2_nc : Nat_big_num.num
Sourceval r_aarch64_movw_uabs_g3 : Nat_big_num.num
Sourceval r_aarch64_movw_sabs_g0 : Nat_big_num.num
Sourceval r_aarch64_movw_sabs_g1 : Nat_big_num.num
Sourceval r_aarch64_movw_sabs_g2 : Nat_big_num.num
Sourceval r_aarch64_ld_prel_lo19 : Nat_big_num.num
Sourceval r_aarch64_adr_prel_lo21 : Nat_big_num.num
Sourceval r_aarch64_adr_prel_pg_hi21 : Nat_big_num.num
Sourceval r_aarch64_adr_prel_pg_hi21_nc : Nat_big_num.num
Sourceval r_aarch64_add_abs_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst8_abs_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst16_abs_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst32_abs_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst64_abs_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst128_abs_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tstbr14 : Nat_big_num.num
Sourceval r_aarch64_condbr19 : Nat_big_num.num
Sourceval r_aarch64_jump26 : Nat_big_num.num
Sourceval r_aarch64_call26 : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g0 : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g0_nc : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g1 : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g1_nc : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g2 : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g2_nc : Nat_big_num.num
Sourceval r_aarch64_movw_prel_g3 : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g0 : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g0_nc : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g1 : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g1_nc : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g2 : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g2_nc : Nat_big_num.num
Sourceval r_aarch64_movw_gotoff_g3 : Nat_big_num.num
Sourceval r_aarch64_gotrel64 : Nat_big_num.num
Sourceval r_aarch64_gotrel32 : Nat_big_num.num
Sourceval r_aarch64_got_ld_prel19 : Nat_big_num.num
Sourceval r_aarch64_got_ld64_gotoff_lo15 : Nat_big_num.num
Sourceval r_aarch64_adr_got_page : Nat_big_num.num
Sourceval r_aarch64_ld64_got_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ld64_gotpage_lo15 : Nat_big_num.num
Sourceval r_aarch64_tlsgd_adr_prel21 : Nat_big_num.num
Sourceval r_aarch64_tlsgd_adr_page21 : Nat_big_num.num
Sourceval r_aarch64_tlsgd_add_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsgd_movw_g1 : Nat_big_num.num
Sourceval r_aarch64_tlsgd_movw_g0_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_adr_prel21 : Nat_big_num.num
Sourceval r_aarch64_tlsld_adr_page21 : Nat_big_num.num
Sourceval r_aarch64_tlsld_add_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_g1 : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_g0_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_ld_prel19 : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_dtprel_g2 : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_dtprel_g1 : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_dtprel_g1_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_dtprel_g0 : Nat_big_num.num
Sourceval r_aarch64_tlsld_movw_dtprel_g0_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_add_dtprel_hi12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_add_dtprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_add_dtprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst8_dtprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst8_dtprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst16_dtprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst16_dtprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst32_dtprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst32_dtprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst64_dtprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst64_dtprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst128_dtprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsld_ldst128_dtprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsie_movw_gottprel_g1 : Nat_big_num.num
Sourceval r_aarch64_tlsie_movw_gottprel_g0_nc : Nat_big_num.num
Sourceval r_aarch64_tlsie_movw_gottprel_page21 : Nat_big_num.num
Sourceval r_aarch64_tlsie_movw_gottprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsie_movw_gottprel_prel19 : Nat_big_num.num
Sourceval r_aarch64_tlsle_movw_tprel_g2 : Nat_big_num.num
Sourceval r_aarch64_tlsle_movw_tprel_g1 : Nat_big_num.num
Sourceval r_aarch64_tlsle_movw_tprel_g1_nc : Nat_big_num.num
Sourceval r_aarch64_tlsle_movw_tprel_g0 : Nat_big_num.num
Sourceval r_aarch64_tlsle_movw_tprel_g0_nc : Nat_big_num.num
Sourceval r_aarch64_add_tprel_hi12 : Nat_big_num.num
Sourceval r_aarch64_add_tprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_add_tprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst8_tprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_ldst8_tprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst16_tprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_ldst16_tprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst32_tprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_ldst32_tprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst64_tprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_ldst64_tprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_ldst128_tprel_lo12 : Nat_big_num.num
Sourceval r_aarch64_ldst128_tprel_lo12_nc : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_ld_prel19 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_adr_prel21 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_adr_page21 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_ld64_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_add_lo12 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_off_g1 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_off_g0_nc : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_ldr : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_add : Nat_big_num.num
Sourceval r_aarch64_tlsdesc_call : Nat_big_num.num
Sourceval r_aarch64_copy : Nat_big_num.num
Sourceval r_aarch64_glob_dat : Nat_big_num.num
Sourceval r_aarch64_jump_slot : Nat_big_num.num
Sourceval r_aarch64_relative : Nat_big_num.num
Sourceval r_aarch64_tls_dtprel64 : Nat_big_num.num
Sourceval r_aarch64_tls_dtpmod64 : Nat_big_num.num
Sourceval r_aarch64_tls_tprel64 : Nat_big_num.num
Sourceval r_aarch64_tlsdesc : Nat_big_num.num
Sourceval r_aarch64_irelative : Nat_big_num.num
Sourceval string_of_aarch64_relocation_type : Nat_big_num.num -> string

string_of_aarch64_relocation_type m produces a string representation of the * relocation type m.

Sourceval aarch64_le_reloc : Nat_big_num.num -> bool * ('abifeature 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))
Sourceval abi_aarch64_apply_relocation : Elf_relocation.elf64_relocation_a -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Elf_file.elf64_file -> (Uint64_wrapper.uint64, Nat_big_num.num Abi_utilities.relocation_operator_expression * Abi_utilities.integer_bit_width * Nat_big_num.num Abi_utilities.can_fail) Pmap.map Error.error

abi_aarch64_apply_relocation rel s_val p_val got_val ef produces an AST * of the relocation calculation for relocation type rel using s_val, p_val, * and got_val as primitive components. * * TODO: unclear from ABI spec. whether overflow check on relocations is * supposed to cause relocation to fail if not satisfied or whether there is * wrap-around. Resolve.