Source file load.ml

(*Generated by Lem from load.lem.*)
open Lem_assert_extra
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
open Error

open Elf_dynamic
open Elf_file
open Elf_header
open Elf_interpreted_section
open Elf_memory_image
open Elf_relocation
open Elf_section_header_table
open Elf_symbol_table
open Elf_types_native_uint
open Endianness
open Memory_image
open Missing_pervasives
open Show

open Abi_amd64
open Abi_amd64_relocation

open Abi_mips64
open Abi_mips64_dynamic
open Abi_mips64_relocation

open Abi_cheri_mips64
open Abi_cheri_mips64_capability
open Abi_cheri_mips64_dynamic
open Abi_cheri_mips64_relocation

open Gnu_ext_abi
open Gnu_ext_symbol_versioning


(* Utilities *)

(*val get_section_at_addr : elf64_file -> natural -> maybe elf64_interpreted_section*)
let get_section_at_addr f addr:(elf64_interpreted_section)option=
   (if Nat_big_num.equal addr( (Nat_big_num.of_int 0)) then None else (* TODO: is this the right thing to do? *)
  let l = (List.filter (fun sec -> Nat_big_num.greater_equal
    addr sec.elf64_section_addr && Nat_big_num.less
      addr (Nat_big_num.add sec.elf64_section_addr sec.elf64_section_size)
  ) f.elf64_file_interpreted_sections) in
  (match l with
    | [] -> None
    | [sec] -> Some sec
    | sec::_ -> Some sec (* TODO: remove me *)
    (* | _ ->
      let _ = List.map print_elf64_section l in
      failwith ("get_section_at_addr: " ^ (show (List.length l)) ^ " sections at address 0x" ^ (hex_string_of_natural addr)) *)
  ))

(*val show_section_at_addr : elf64_file -> natural -> string*)
let show_section_at_addr f addr:string=
   ((match get_section_at_addr f addr with
    | Some section ->
      let offset_in_section = (Nat_big_num.sub_nat addr section.elf64_section_addr) in
      "[section at " ^ (section.elf64_section_name_as_string ^ ("+0x" ^ ((hex_string_of_natural offset_in_section) ^ "]")))
    | None ->
      "[unknown section at 0x" ^ ((hex_string_of_natural addr) ^ "]")
  ))


(* Dynamic linker *)

type dynamic_symbol = {
  dynamic_symbol_name : string;
  dynamic_symbol_entry : elf64_symbol_table_entry;
  dynamic_symbol_value : Nat_big_num.num;
  dynamic_symbol_version :  string option;
  dynamic_symbol_version_base : bool
}

(*val find_sym : list dynamic_symbol -> string -> maybe string -> maybe dynamic_symbol*)
let find_sym syms name1 version:(dynamic_symbol)option=
   (
  (* TODO: index symbols by name to speed up lookups *)let matches = (List.filter (fun sym1 -> sym1.dynamic_symbol_name = name1) syms) in
  let version_matches = (List.filter (fun sym1 -> (Lem.option_equal (=) sym1.dynamic_symbol_version version)) matches) in
  (match version_matches with
    | [] ->
      (match version with
        | Some _ ->
          (* Reference requested a specific version, accept only if the
             definition doesn't use symbol versioning. *)
          (match matches with
            | [sym1] ->
              (* TODO: check the reference doesn't come from the same file as
                 this symbol (if it's the case, fatal error). *)
              (* Make sure the definition doesn't use symbol versioning *)
              (match sym1.dynamic_symbol_version with
                | Some _ -> None
                | None -> Some sym1
              )
            | _ -> None
          )
        | None ->
          (* Reference without version *)
          (match matches with
            | [] -> None
            | [sym1] ->
              (* If there is exactly one version for which this symbol is
                 defined, then this version is accepted. *)
              Some sym1
            | _ ->
              (* Multiple results with different versions, fallback to base
                 definition *)
              (* TODO: add support for: 2 is the name given later to the
                 baseline of symbols once the library started using symbol
                 versioning *)
              Lem_list.list_find_opt (fun sym1 -> sym1.dynamic_symbol_version_base) matches
          )
      )
    | [sym1] ->
      Some sym1
    | sym1 :: _ ->
      Some sym1 (* When overriding symbols we just add the new one before in the list *)
    (* | _ ->
      failwith ("find_sym: multiple symbols for `" ^ name ^ "` version " ^ (show version)) *)
  ))

(*val is_data_section : elf64_interpreted_section -> bool*)
let is_data_section sec:bool=
   (false
  || ((sec.elf64_section_name_as_string = ".data")
  || ((sec.elf64_section_name_as_string = ".sdata") (* initialized short data *)
  || ((sec.elf64_section_name_as_string = ".sbss") (* uninitialized short data *)
  || ((sec.elf64_section_name_as_string = ".tdata") (* initialized thread-local data *)
  || ((sec.elf64_section_name_as_string = ".tbss") (* uninitialized thread-local data *)
  || ((sec.elf64_section_name_as_string = ".dynamic")
  || ((sec.elf64_section_name_as_string = ".data.rel.ro") (* TODO: remove me? *)
  || (sec.elf64_section_name_as_string = ".rld_map"))))))))) (* TODO: remove me *)

(*val is_unsupported_relocation_type: elf64_file -> natural -> bool*)
let is_unsupported_relocation_type f rel_type1:bool=
   (
  (* TODO: add support for TLS relocs *)if Abi_amd64.header_is_amd64 f.elf64_file_header then Nat_big_num.equal
    rel_type1 r_x86_64_irelative || (Nat_big_num.equal rel_type1 r_x86_64_tpoff64
      || (Nat_big_num.equal rel_type1 r_x86_64_dtpoff64 || Nat_big_num.equal rel_type1 r_x86_64_dtpmod64))
  else if Abi_mips64.header_is_mips64 f.elf64_file_header
      || Abi_cheri_mips64.header_is_cheri_mips64 f.elf64_file_header then Nat_big_num.equal
    rel_type1 r_mips_tls_tprel64 || Nat_big_num.equal rel_type1 r_mips_tls_dtpmod64
  else
    false)

(*val apply_relocation : forall 'abifeature. abi 'abifeature -> elf64_file -> annotated_memory_image 'abifeature -> natural -> elf64_relocation_a -> symbol_reference_and_reloc_site -> maybe dynamic_symbol -> bool -> annotated_memory_image 'abifeature*)
let apply_relocation abi1 f img2 base reloc1 symref_and_reloc_site maybe_sym ignore_data_sections:'abifeature annotated_memory_image=
   (let endian = (get_elf64_header_endianness f.elf64_file_header) in
  let (rel_type1, _) = (abi1.parse_reloc_info reloc1.elf64_ra_info) in
  let offset = (Ml_bindings.nat_big_num_of_uint64 reloc1.elf64_ra_offset) in
  let addend = (Nat_big_num.of_int64 reloc1.elf64_ra_addend) in
  let addr = (Nat_big_num.add base offset) in
  (* TODO: support is_absolute? *)
  let (is_absolute, applyfn) = (abi1.reloc rel_type1) in
  let (width, calcfn) = (applyfn img2 addr symref_and_reloc_site) in
  let _ = (prerr_endline ("Relocation of type 0x" ^ ((hex_string_of_natural rel_type1) ^ (" at 0x" ^ ((hex_string_of_natural addr) ^ (" (offset 0x" ^ ((hex_string_of_natural offset) ^ ("), size 0x" ^ ((hex_string_of_natural width) ^ (" in " ^ (show_section_at_addr f offset))))))))))) in

  (* TODO: is there a way to make this nicer? *)
  if Nat_big_num.equal rel_type1( (Nat_big_num.of_int 0)) then
    let _ = (prerr_endline "  Skipping NONE relocation") in
    img2
  else

  let is_in_data_section =
    (if ignore_data_sections then
      false
    else
      (match get_section_at_addr f offset with
        | Some sec -> is_data_section sec
        | None -> false
      ))
  in
  if is_in_data_section then
    let _ = (prerr_endline "  Relocation inside a data section, ignoring") in
    img2
  else
    (* TODO: hard fail if symbol name is non-empty but find_sym returns Nothing? *)
    let maybe_sym_addr = ((match maybe_sym with
      | Some sym1 ->
        if Nat_big_num.equal (get_elf64_symbol_type sym1.dynamic_symbol_entry) stt_gnu_ifunc then
          let _ = (prerr_endline "  Symbol is an ifunc") in
          None
        else
          Some sym1.dynamic_symbol_value
      | None ->
        Some( (Nat_big_num.of_int 0)) (* This isn't pretty, but doing something else would be complicated *)
    )) in

    let maybe_sym_addr =
      (if is_unsupported_relocation_type f rel_type1 then
        let _ = (prerr_endline ("  Giving up on this one: unsupported relocation type")) in
        None
      else
        maybe_sym_addr)
    in
    (match maybe_sym_addr with
      | Some sym_addr ->
        if header_is_pure_cheri_mips64 f.elf64_file_header
            && Nat_big_num.equal rel_type1 r_mips_cheri_capability then
          (* CHERI capability relocations are special snowflakes, they aren't
             just an address. *)
          (* TODO: find a better solution *)
          let cap_bp = (abi_cheri_mips64_write_capability_byte_pattern endian None
            None None None (Some( (Nat_big_num.of_int 42))) (Some( (Nat_big_num.of_int 42))) (Some( (Nat_big_num.of_int 42)))) in (* TODO *)
          let _ = (prerr_endline ("  Relocating CHERI capability `" ^ (symref_and_reloc_site.ref.ref_symname ^ "`"))) in
          write_memory_image img2 addr cap_bp
        else
          let existing_bytes = (assert_unwrap_maybe (read_memory_image img2 addr width)) in
          let existing_value = (Memory_image.natural_of_byte_list endian existing_bytes) in
          let new_value = (calcfn sym_addr addend existing_value) in
          let field_bytes = (Memory_image.natural_to_byte_list_padded_to endian width new_value) in
          let field_bp = (Lem_list.map (fun b -> Some b) field_bytes) in
          let _ = (prerr_endline ("  Relocating `" ^ (symref_and_reloc_site.ref.ref_symname ^ ("` (existing=0x" ^ ((hex_string_of_natural existing_value) ^ (" addend=" ^ ((Nat_big_num.to_string addend) ^ (") to 0x" ^ ((hex_string_of_natural new_value) ^ (" (symbol address 0x" ^ ((hex_string_of_natural sym_addr) ^ ")"))))))))))) in
          write_memory_image img2 addr field_bp
      | None ->
        let _ = (prerr_endline ("  Masking relocation for `" ^ (symref_and_reloc_site.ref.ref_symname ^ "`"))) in
        mask_memory_image img2 addr width
    ))

(*val get_sym_ref_version : natural -> maybe gnu_ext_interpreted_versym_table -> string -> natural -> natural -> maybe string*)
let get_sym_ref_version dynsym_scnidx maybe_versym_table sym_name sym_scn sym_idx:(string)option=
   (if not (Nat_big_num.equal dynsym_scnidx sym_scn) then None else
  (match maybe_versym_table with
    | Some versym_table ->
      (* TODO: unify get_gnu_ext_interpreted_verneed and get_gnu_ext_interpreted_verdef *)
      (match get_gnu_ext_interpreted_verneed versym_table sym_idx with
        | Success None -> None
        | Success (Some vernaux) ->
          (* TODO: handle vernaux.gnu_ext_interpreted_vernaux_verneed.gnu_ext_interpreted_verneed_file *)
          Some vernaux.gnu_ext_interpreted_vernaux_name
        | Fail errmsg ->
          (* TODO: failwith errmsg *)
          (* No verneed found, maybe this DSO is defining the symbol and has a reloc bound to it *)
          (match get_gnu_ext_interpreted_verdef versym_table sym_idx with
            | Success (GnuExtInterpretedVerdefVersion verdef) ->
              Some verdef.gnu_ext_interpreted_verdef_name
            | _ ->
              None
          )
      )
    | None ->
      None
  ))

(*val mask_data_sections : forall 'abifeature. elf64_file -> annotated_memory_image 'abifeature -> annotated_memory_image 'abifeature*)
let mask_data_sections f img2:'abifeature annotated_memory_image=
   (let data_sections = (List.filter is_data_section f.elf64_file_interpreted_sections) in
  List.fold_left (fun img2 sec ->
    let _ = (prerr_endline ("Masking " ^ (sec.elf64_section_name_as_string ^ (" at 0x" ^ ((hex_string_of_natural sec.elf64_section_addr) ^ (", size 0x" ^ (hex_string_of_natural sec.elf64_section_size))))))) in
    mask_memory_image img2 sec.elf64_section_addr sec.elf64_section_size
  ) img2 data_sections)

(*val mask_relocations : forall 'abifeature. abi 'abifeature -> elf64_file -> annotated_memory_image 'abifeature -> annotated_memory_image 'abifeature*)
let mask_relocations abi1 f img2:'abifeature annotated_memory_image=
   (let all_relocs = (Elf_memory_image.extract_all_relocs "<input file>" f) in
  List.fold_left (fun img2 (scn, rel_idx, rel_src_scn, rel) ->
    let addr = (Ml_bindings.nat_big_num_of_uint64 rel.elf64_ra_offset) in
    let (rel_type1, _) = (abi1.parse_reloc_info rel.elf64_ra_info) in
    let (is_absolute, applyfn) = (abi1.reloc rel_type1) in
    let (width, calcfn) = (applyfn img2 addr Memory_image.null_symbol_reference_and_reloc_site) in
    let _ = (prerr_endline ("Masking relocation of type 0x" ^ ((hex_string_of_natural rel_type1) ^ (" at 0x" ^ ((hex_string_of_natural addr) ^ (", size 0x" ^ ((hex_string_of_natural width) ^ (" in " ^ (show_section_at_addr f addr))))))))) in
    (* let _ = Missing_pervasives.errln ("Relocation info: " ^ (show rel.elf64_ra_info)) in *)
    mask_memory_image img2 addr width
  ) img2 all_relocs)

let amd64_address_size : Nat_big_num.num= ( (Nat_big_num.of_int 8))

(*val init_amd64_pltgot : forall 'abifeature 'size. annotated_memory_image 'abifeature -> natural -> list (natural * dyn_value elf64_addr 'size) -> annotated_memory_image 'abifeature*)
let init_amd64_pltgot img2 base dyns:'abifeature annotated_memory_image=
   (let maybe_pltgot_offset = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Elf_dynamic.dt_pltgot
  ) dyns) in
  (match maybe_pltgot_offset with
    | Some (_, Address pltgot_offset) ->
      let pltgot_addr = (Nat_big_num.add base (Ml_bindings.nat_big_num_of_uint64 pltgot_offset)) in
      let _ = (prerr_endline ("Initializing PLTGOT at 0x" ^ (hex_string_of_natural pltgot_addr))) in
      (* The second entry contains a linker-specific value. FreeBSD's rtld-elf
         uses it to store a pointer to an internal data structure, glibc's
         linker leaves it zeroed. *)
      let img2 = (mask_memory_image img2 ( Nat_big_num.add pltgot_addr amd64_address_size) amd64_address_size) in
      (* The third entry contains the dynamic linker entry point *)
      let img2 = (mask_memory_image img2 ( Nat_big_num.add pltgot_addr (Nat_big_num.mul( (Nat_big_num.of_int 2)) amd64_address_size)) amd64_address_size) in
      img2
    | None ->
      let _ = (prerr_endline ("No DT_PLTGOT in .dynamic, skipping PLTGOT initialization")) in
      img2
  ))

let mips64_address_size : Nat_big_num.num= ( (Nat_big_num.of_int 8))

(*val apply_mips64_local_got_relocations : forall 'abifeature. endianness -> annotated_memory_image 'abifeature -> natural -> natural -> natural -> (annotated_memory_image 'abifeature * natural)*)
let rec apply_mips64_local_got_relocations endian img2 base got_entry_addr local_gotno:'abifeature annotated_memory_image*Nat_big_num.num=
   (if Nat_big_num.equal local_gotno( (Nat_big_num.of_int 0)) then (img2, got_entry_addr) else
  let _ = (prerr_endline ("MIPS local .got relocation at 0x" ^ ((hex_string_of_natural got_entry_addr) ^ (" (remaining: " ^ ((Nat_big_num.to_string local_gotno) ^ ")"))))) in
  let width = mips64_address_size in
  let existing_bytes = (assert_unwrap_maybe (read_memory_image img2 got_entry_addr width)) in
  let existing_value = (Memory_image.natural_of_byte_list endian existing_bytes) in
  let new_value = (Nat_big_num.add base existing_value) in
  let field_bytes = (Memory_image.natural_to_byte_list_padded_to endian width new_value) in
  let field_bp = (Lem_list.map (fun b -> Some b) field_bytes) in
  let _ = (prerr_endline ("  Relocating MIPS64 local .got entry from 0x" ^ ((hex_string_of_natural existing_value) ^ (" to 0x" ^ (hex_string_of_natural new_value))))) in
  let img2 = (write_memory_image img2 got_entry_addr field_bp) in
  apply_mips64_local_got_relocations endian img2 base ( Nat_big_num.add got_entry_addr width) ( Nat_big_num.sub_nat local_gotno( (Nat_big_num.of_int 1))))

let rec apply_mips64_global_got_relocations' abi1 f img2 dynsyms syms dynsym_scnidx maybe_versym_table base got_entry_addr (symtabno : Nat_big_num.num) ignore_data_sections:'a annotated_memory_image*Nat_big_num.num=
   (if Nat_big_num.equal symtabno( (Nat_big_num.of_int 0)) then (img2, got_entry_addr) else
  let endian = (get_elf64_header_endianness f.elf64_file_header) in
  (match syms with
    | (sym_name, sym_entry, scnidx, symidx) :: syms ->
      let ra_info = (Uint64_wrapper.of_bigint Abi_mips64_relocation.r_mips_jump_slot) in
      let ra_info = ((match endian with
        | Little -> Uint64_wrapper.shift_left ra_info 56
        | Big -> ra_info
      )) in

      let reloc1 = ({
        elf64_ra_offset = (Uint64_wrapper.of_bigint ( Nat_big_num.sub_nat got_entry_addr base));
        elf64_ra_info = ra_info;
        elf64_ra_addend = (Nat_big_num.to_int64( (Nat_big_num.of_int 0)))
      }) in

      (* TODO: unify this with normal relocs *)
      let maybe_sym =
        (
        (* TODO: remove these special cases, especially the last one *)if not (sym_name = "") then
          let maybe_sym_version = (get_sym_ref_version dynsym_scnidx maybe_versym_table sym_name scnidx symidx) in
          let _ = (prerr_endline ("Searching for symbol `" ^ (sym_name ^ ("`, version " ^ (string_of_maybe 
  instance_Show_Show_string_dict maybe_sym_version))))) in
          find_sym dynsyms sym_name maybe_sym_version
        else
          None)
      in

      (* let sym_addr = base + natural_of_elf64_addr sym_entry.elf64_st_value in *)
      let symref_and_reloc_site = null_symbol_reference_and_reloc_site in
      let img2 = (apply_relocation abi1 f img2 base reloc1 symref_and_reloc_site maybe_sym ignore_data_sections) in

      apply_mips64_global_got_relocations' abi1 f img2 dynsyms syms dynsym_scnidx maybe_versym_table base ( Nat_big_num.add got_entry_addr mips64_address_size) ( Nat_big_num.sub_nat symtabno( (Nat_big_num.of_int 1))) ignore_data_sections
    | _ -> failwith "apply_mips64_global_got_relocations': not enough symbols"
  ))

let apply_mips64_global_got_relocations abi1 f img2 dynsyms dynsym_scnidx maybe_versym_table base got_entry_addr symtab_addr gotsym symtabno ignore_data_sections:'a annotated_memory_image*Nat_big_num.num=
   (let symtab_triples = (mapMaybei (fun scnidx isec1 ->
    if Nat_big_num.equal isec1.elf64_section_addr (Ml_bindings.nat_big_num_of_uint64 symtab_addr) then
      (match find_elf64_symbols_by_symtab_idx scnidx f with
        | Fail _ -> None
        | Success triple -> Some triple
      )
    else
      None
  ) f.elf64_file_interpreted_sections) in
  let (syms : (string * elf64_symbol_table_entry * Nat_big_num.num (* scnidx *) * Nat_big_num.num (* symidx *)) list) =
    ((match symtab_triples with
      | [triple] -> Elf_memory_image.extract_all_symbols triple
      | [] -> failwith "apply_mips64_global_got_relocations: no .symtab found"
      | _ -> failwith "apply_mips64_global_got_relocations: multiple .symtab sections not supported for MIPS64"
    ))
  in
  let syms = (Lem_list.drop (Nat_big_num.to_int gotsym) syms) in
  apply_mips64_global_got_relocations' abi1 f img2 dynsyms syms dynsym_scnidx maybe_versym_table base got_entry_addr ( Nat_big_num.sub_nat symtabno gotsym) ignore_data_sections)

(* MIPS uses an ugly packed form for GOT relocations. See musl's do_mips_relocs
   function. *)
let apply_mips64_got_relocations abi1 f img2 dynsyms base dyns dynsym_scnidx maybe_versym_table ignore_data_sections:'a annotated_memory_image=
   (let maybe_got_offset = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal tag Elf_dynamic.dt_pltgot) dyns) in
  let got_offset = ((match maybe_got_offset with
    | Some (_, Address got) -> got
    | None -> failwith "apply_mips64_got_relocations: missing DT_PLTGOT in .dynamic"
  )) in
  let got_addr = (Nat_big_num.add base (Ml_bindings.nat_big_num_of_uint64 got_offset)) in
  let got_entry_addr = got_addr in

  (* Apply local .got relocs *)
  let maybe_local_gotno = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Abi_mips64_dynamic.abi_mips64_dt_local_gotno
  ) dyns) in
  let (img2, got_entry_addr) = ((match maybe_local_gotno with
    | Some (_, Numeric local_gotno) ->
      (* The first entry is reserved to hold the address of the entry point in
         the dynamic linker to call when lazy resolving text symbols. The second
         entry is reserved by DSOs linked with GNU's ld to hold the base address
         of the loaded DSO. GNU DSOs have the MSB of the second entry set to 1.
         IRL, some ld.so implementations skip both (uclibc), some relocate both
         (musl), so we'll just don't check those two.
         TODO: check the MSB of the second entry and only mask it if it's GNU. *)
      let reserved_num =( (Nat_big_num.of_int 2)) in
      let img2 = (mask_memory_image img2 got_entry_addr ( Nat_big_num.mul reserved_num mips64_address_size)) in
      let got_entry_addr = (Nat_big_num.add got_addr (Nat_big_num.mul reserved_num mips64_address_size)) in
      let local_gotno = (Nat_big_num.sub_nat local_gotno reserved_num) in

      let _ = (prerr_endline ("Applying " ^ ((Nat_big_num.to_string local_gotno) ^ " MIPS64 local .got relocations"))) in
      let endian = (get_elf64_header_endianness f.elf64_file_header) in
      apply_mips64_local_got_relocations endian img2 base got_entry_addr local_gotno
    | None ->
      let _ = (prerr_endline "Not applying MIPS64 .got relocations: missing DT_LOCAL_GOTNO") in
      (img2, got_addr)
  )) in

  (* Apply R_MIPS_JUMP_SLOT relocs *)
  let maybe_symtab_addr = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Elf_dynamic.dt_symtab
  ) dyns) in
  let symtab_addr = ((match maybe_symtab_addr with
    | Some (_, Address symtab_addr) -> symtab_addr
    | None -> failwith "apply_mips64_got_relocations: missing DT_SYMTAB in .dynamic"
  )) in
  let maybe_gotsym = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Abi_mips64_dynamic.abi_mips64_dt_gotsym
  ) dyns) in
  let gotsym = ((match maybe_gotsym with
    | Some (_, Numeric gotsym) -> gotsym
    | None -> failwith "apply_mips64_got_relocations: missing DT_MIPS_GOTSYM in .dynamic"
  )) in
  let maybe_symtabno = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Abi_mips64_dynamic.abi_mips64_dt_symtabno
  ) dyns) in
  let symtabno = ((match maybe_symtabno with
    | Some (_, Numeric symtabno) -> symtabno
    | None -> failwith "apply_mips64_got_relocations: missing DT_MIPS_SYMTABNO in .dynamic"
  )) in
  let (img2, got_entry_addr) = (apply_mips64_global_got_relocations abi1 f img2 dynsyms dynsym_scnidx maybe_versym_table base got_entry_addr symtab_addr gotsym symtabno ignore_data_sections) in

  img2)

(* This function must be called after normal relocs have been applied *)
let apply_cheri_mips64_cap_relocations f img2 base dyns ignore_data_sections:'a annotated_memory_image=
   (let maybe_cap_relocs = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Abi_cheri_mips64_dynamic.abi_cheri_dt___caprelocs
  ) dyns) in
  let cap_relocs_addr = ((match maybe_cap_relocs with
    | Some (_, Address cap_relocs_addr) -> Ml_bindings.nat_big_num_of_uint64 cap_relocs_addr
    | None -> failwith "apply_cheri_mips64_cap_relocations: missing DT_CHERI___CAPRELOCS in .dynamic"
  )) in
  let maybe_cap_relocssz = (Lem_list.list_find_opt (fun (tag, _) -> Nat_big_num.equal
    tag Abi_cheri_mips64_dynamic.abi_cheri_dt___caprelocssz
  ) dyns) in
  let cap_relocssz = ((match maybe_cap_relocssz with
    | Some (_, Numeric cap_relocssz) -> cap_relocssz
    | None -> failwith "apply_cheri_mips64_cap_relocations: missing DT_CHERI___CAPRELOCSSZ in .dynamic"
  )) in

  (* We need to read our memory image because some relocations have been applied
     to the __cap_relocs section. *)
  let cap_relocs_bs = ((match read_memory_image_byte_sequence img2 ( Nat_big_num.add base cap_relocs_addr) cap_relocssz with
    | Some bs -> bs
    | None -> failwith "apply_cheri_mips64_cap_relocations: cannot dereference DT_CHERI___CAPRELOCS"
  )) in

  let endian = (get_elf64_header_endianness f.elf64_file_header) in
  let cap_relocs = ((match read_cheri_mips64_cap_relocs endian cap_relocs_bs with
    | Success cap_relocs -> cap_relocs
    | Fail errmsg -> failwith errmsg
  )) in
  let img2 = (List.fold_left (fun img2 reloc1 ->
    let is_func = (cheri_mips64_cap_reloc_is_function reloc1) in
    let loc = (Ml_bindings.nat_big_num_of_uint64 reloc1.cheri_mips64_cap_reloc_location) in
    let obj = (Ml_bindings.nat_big_num_of_uint64 reloc1.cheri_mips64_cap_reloc_object) in
    let offset = (Ml_bindings.nat_big_num_of_uint64 reloc1.cheri_mips64_cap_reloc_offset) in
    let size2 = (Ml_bindings.nat_big_num_of_uint64 reloc1.cheri_mips64_cap_reloc_size) in

    let is_in_data_section =
      (if ignore_data_sections then
        false
      else
        (match get_section_at_addr f ( Nat_big_num.sub_nat loc base) with
          | Some sec -> is_data_section sec
          | None -> false
        ))
    in
    if is_in_data_section then
      let _ = (prerr_endline ("Skipping __cap_relocs relocation at 0x" ^ ((hex_string_of_natural loc) ^ ": in a data section"))) in
      img2
    else

    let (cursor, cap_base, len) =
      (if Nat_big_num.equal obj( (Nat_big_num.of_int 0)) then
        ( (Nat_big_num.of_int 0), (Nat_big_num.of_int 0), (Nat_big_num.of_int 0))
      else
        let cursor = (Nat_big_num.add obj offset) in
        if is_func then
          (cursor, (Nat_big_num.of_int 0), size2)
        else
          (cursor, obj, size2))
    in
    let cap_bp = (abi_cheri_mips64_write_capability_byte_pattern endian None
      None None None (Some cursor) (Some cap_base) (Some len)) in
    let _ = (prerr_endline (
      "Applying __cap_relocs relocation at 0x" ^ ((hex_string_of_natural loc)
        ^ (" in " ^ ((show_section_at_addr f ( Nat_big_num.sub_nat loc base))
        ^ (" offset=0x" ^ ((hex_string_of_natural offset)
        ^ (" size=0x" ^ ((hex_string_of_natural size2)
        ^ (" object=0x" ^ ((hex_string_of_natural obj)
        ^ (" cursor=0x" ^ ((hex_string_of_natural cursor)
        ^ (" base=0x" ^ ((hex_string_of_natural cap_base)
        ^ (" len=0x" ^ ((hex_string_of_natural len)
        ^ (" is_func=" ^ (string_of_bool is_func)))))))))))))))))
    )) in
    (* let _ = Missing_pervasives.errln (string_of_byte_pattern cap_bp) in *)
    write_memory_image img2 loc cap_bp
  ) img2 cap_relocs) in

  img2)

let sym_add_verdef sym1 verdef:dynamic_symbol=
   (
  (* let _ = Missing_pervasives.errln ("Symbol `" ^ sym.dynamic_symbol_name ^ "`, version `" ^ verdef_aux ^ "`") in *){
    dynamic_symbol_name = (sym1.dynamic_symbol_name);
    dynamic_symbol_entry = (sym1.dynamic_symbol_entry);
    dynamic_symbol_value = (sym1.dynamic_symbol_value);
    dynamic_symbol_version = (Some verdef.gnu_ext_interpreted_verdef_name);
    dynamic_symbol_version_base = (Nat_big_num.equal
      (* TODO: what's the difference between those two? *)
      verdef.gnu_ext_interpreted_verdef_ndx gnu_ext_verdef_base_unspecified
      || Nat_big_num.equal verdef.gnu_ext_interpreted_verdef_ndx gnu_ext_verdef_base_versioned)
  })

(*val extract_dynsyms : elf64_file -> natural -> list dynamic_symbol -> natural -> maybe gnu_ext_interpreted_versym_table -> error (list dynamic_symbol)*)
let extract_dynsyms f base existing_syms symtab_scnidx maybe_versym_table:((dynamic_symbol)list)error=
   (let symtab_scn = (assert_unwrap_maybe (Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int symtab_scnidx))) in bind (find_elf64_symbols_by_symtab_idx symtab_scnidx f) (fun triple ->
  let syms = (Elf_memory_image.extract_all_symbols triple) in
  let syms = (List.filter (fun (sym_name, sym_entry, scnidx, symidx) ->
    let sym_binding = (get_elf64_symbol_binding sym_entry) in
    let sym_value = (Ml_bindings.nat_big_num_of_uint64 sym_entry.elf64_st_value) in
    ( Nat_big_num.equal sym_binding Elf_symbol_table.stb_global || Nat_big_num.equal sym_binding Elf_symbol_table.stb_weak)
      (* We're only interested in symbols defined in this DSO *)
      && not (Nat_big_num.equal (Uint32_wrapper.to_bigint sym_entry.elf64_st_shndx)( (Nat_big_num.of_int 0)))
  ) syms) in
  let syms = (Lem_list.map (fun (sym_name, sym_entry, scnidx, symidx) ->
    (* let _ = Missing_pervasives.errln ("Library exports dynamic symbol: " ^ sym_name) in *)
    let is_abs = (Nat_big_num.equal (Uint32_wrapper.to_bigint sym_entry.elf64_st_shndx) shn_abs) in
    let sym_value =
      (if is_abs then
        Ml_bindings.nat_big_num_of_uint64 sym_entry.elf64_st_value
      else Nat_big_num.add
        base (Ml_bindings.nat_big_num_of_uint64 sym_entry.elf64_st_value))
    in
    let sym1 = ({
      dynamic_symbol_name = sym_name;
      dynamic_symbol_entry = sym_entry;
      dynamic_symbol_value = sym_value;
      dynamic_symbol_version = None;
      dynamic_symbol_version_base = false
    }) in
    (sym1, symidx)
  ) syms) in bind (match maybe_versym_table with
    | Some versym_table ->
      if List.length versym_table.gnu_ext_interpreted_versym_table_entries < List.length syms then
        Error.fail "extract_dynsyms: versym table too short"
      else
      bind (return ()) (fun () ->
      Error.foldM (fun syms (sym1, symidx) -> bind (get_gnu_ext_interpreted_verdef versym_table symidx) (fun verdef_lookup ->
        let versioned_sym = ((match verdef_lookup with
          | GnuExtInterpretedVerdefVersion verdef ->
            sym_add_verdef sym1 verdef
          | GnuExtInterpretedVerdefHidden verdef ->
            (* TODO: symbol is hidden and cannot be referenced outside of this object *)
            sym_add_verdef sym1 verdef
          | _ -> sym1 (* TODO: ignore local dynsyms? *)
        )) in
        return (versioned_sym :: syms))
      ) [] syms)
    | None ->
      let syms = (Lem_list.map (fun (sym1, symidx) -> sym1) syms) in
      return syms
  ) (fun syms ->

  (* Filter out symbols that are ignored because already defined in another object *)
  let syms = (List.fold_left (fun syms sym1 ->
    let sym_name = (sym1.dynamic_symbol_name) in
    let sym_entry = (sym1.dynamic_symbol_entry) in
    let sym_addr = (sym1.dynamic_symbol_value) in
    let sym_version = (sym1.dynamic_symbol_version) in
    let sym_binding = (get_elf64_symbol_binding sym_entry) in
    let _ = (prerr_endline ("Processing symbol `" ^ (sym_name ^ ("`, 0x" ^ ((hex_string_of_natural sym_addr) ^ (", binding=" ^ ((Nat_big_num.to_string sym_binding) ^ (", version=" ^ (string_of_maybe 
  instance_Show_Show_string_dict sym_version))))))))) in
    (* Check if this symbol has already been defined in another object. Only
       check the symbol name, we don't care about the version here. *)
    let maybe_existing = (find_sym existing_syms sym_name None) in
    (match maybe_existing with
      | Some existing ->
        let existing_entry = (existing.dynamic_symbol_entry) in
        let existing_addr = (existing.dynamic_symbol_value) in
        let existing_version = (existing.dynamic_symbol_version) in
        if Nat_big_num.equal (get_elf64_symbol_binding existing_entry) Elf_symbol_table.stb_weak && not (Nat_big_num.equal sym_binding Elf_symbol_table.stb_weak) then
          (* Existing symbol is weak and the new one isn't, replace it *)
          let _ = (prerr_endline ("Overriding weak symbol `" ^ (sym_name ^ ("`, 0x" ^ ((hex_string_of_natural existing_addr) ^ (" -> 0x" ^ (hex_string_of_natural sym_addr))))))) in
          sym1 :: syms
        else if Nat_big_num.equal (Uint32_wrapper.to_bigint existing_entry.elf64_st_shndx) shn_undef && not (Nat_big_num.equal (Uint32_wrapper.to_bigint sym_entry.elf64_st_shndx)( (Nat_big_num.of_int 0))) then
          (* Existing symbol has an undefined ndx and the new one has a defined one, replace it *)
          (* TODO: why is this the right thing to do? *)
          let _ = (prerr_endline ("Overriding symbol with undefined ndx `" ^ (sym_name ^ ("`, 0x" ^ ((hex_string_of_natural existing_addr) ^ (" -> 0x" ^ (hex_string_of_natural sym_addr))))))) in
          sym1 :: syms
        else if not ((Lem.option_equal (=) existing_version None)) && (not ((Lem.option_equal (=) sym_version None)) && not ((Lem.option_equal (=) sym_version existing_version))) then
          (* Existing symbol has a version, and this symbol has a different version: keep both *)
          let _ = (prerr_endline ("Adding new version `" ^ ((string_of_maybe 
  instance_Show_Show_string_dict sym_version) ^ ("` of symbol `" ^ (sym_name ^ ("` (already have: `" ^ ((string_of_maybe 
  instance_Show_Show_string_dict existing_version) ^ "`)"))))))) in
          sym1 :: syms
        (* else if get_elf64_symbol_binding existing_entry = Elf_symbol_table.stb_weak && sym_binding = Elf_symbol_table.stb_weak then
          (* TODO: is this really the right thing to do? *)
          let _ = Missing_pervasives.errln ("Overriding weak symbol with another weak symbol `" ^ sym_name ^ "`, 0x" ^ (hex_string_of_natural existing_addr) ^ " -> 0x" ^ (hex_string_of_natural sym_addr)) in
          sym :: syms *)
        else
          let _ = (prerr_endline ("Multiple definitions of `" ^ (sym_name ^ ("` version " ^ ((string_of_maybe 
  instance_Show_Show_string_dict sym_version) ^ ", only keeping the first one"))))) in
          syms
      | None ->
        sym1 :: syms
    )
  ) [] syms) in
  return syms)))