Source file abis.ml

(*Generated by Lem from abis/abis.lem.*)
(** 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.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_num
open Lem_maybe
open Lem_list
open Lem_set
(*import Map*)
open Lem_string
open Show
open Lem_assert_extra
open Error
open Missing_pervasives

open Elf_file
open Elf_header
open Elf_interpreted_section
open Elf_relocation
open Elf_symbol_table
open Elf_program_header_table
open Elf_section_header_table
open Memory_image

open Abi_amd64
open Abi_amd64_relocation

open Abi_aarch64_le
open Abi_aarch64_relocation

open Abi_power64
open Abi_power64_relocation

open Abi_mips64
open Abi_mips64_elf_header
open Abi_mips64_relocation

open Abi_cheri_mips64
open Abi_cheri_mips64_elf_header
open Abi_cheri_mips64_relocation

open Gnu_ext_abi

open Abi_classes
open Abi_utilities
open Elf_types_native_uint

open Memory_image_orderings

(** Relocation operators and their validity on a given platform *)

(*val is_valid_abi_aarch64_relocation_operator : relocation_operator -> bool*)
let is_valid_abi_aarch64_relocation_operator op:bool=
   ((match op with
    | Page -> true
    | G -> true
    | GDat -> true
    | GLDM -> true
    | DTPRel -> true
    | GTPRel -> true
    | TPRel -> true
    | GTLSDesc -> true
    | Delta -> true
    | LDM -> true
    | TLSDesc -> true
    | Indirect -> true
    | _ -> false
  ))

(*val is_valid_abi_aarch64_relocation_operator2 : relocation_operator2 -> bool*)
let is_valid_abi_aarch64_relocation_operator2 op:bool=
   ((match op with
    | GTLSIdx -> true
  ))

(*val is_valid_abi_amd64_relocation_operator : relocation_operator -> bool*)
let is_valid_abi_amd64_relocation_operator op:bool=
   ((match op with
    | Indirect -> true
    | _ -> false (* XXX: not sure about this? *)
  ))

(*val is_valid_abi_amd64_relocation_operator2 : relocation_operator2 -> bool*)
let is_valid_abi_amd64_relocation_operator2 op:bool=
   ((match op with
    | _ -> false
  ))

(*val is_valid_abi_power64_relocation_operator : relocation_operator -> bool*)
let is_valid_abi_power64_relocation_operator op:bool=  false (* TODO *)

(*val is_valid_abi_power64_relocation_operator2 : relocation_operator2 -> bool*)
let is_valid_abi_power64_relocation_operator2 op:bool=
   ((match op with
    | _ -> false
  ))

(** Misc. ABI related stuff *)

type any_abi_feature = Amd64AbiFeature of any_abi_feature amd64_abi_feature
                     | Aarch64LeAbiFeature of aarch64_le_abi_feature

(*val anyAbiFeatureCompare : any_abi_feature -> any_abi_feature -> Basic_classes.ordering*)
let anyAbiFeatureCompare f1 f2:int=
     ((match (f1, f2) with
        (Amd64AbiFeature(af1), Amd64AbiFeature(af2)) -> Abi_amd64.abiFeatureCompare0 af1 af2
       |(Amd64AbiFeature(_), _) -> (-1)
       |(Aarch64LeAbiFeature(af1), Amd64AbiFeature(af2)) -> 1
       |(Aarch64LeAbiFeature(af1), Aarch64LeAbiFeature(af2)) -> Abi_aarch64_le.abiFeatureCompare af1 af2
    ))

(*val anyAbiFeatureTagEquiv : any_abi_feature -> any_abi_feature -> bool*)
let anyAbiFeatureTagEquiv f1 f2:bool=
     ((match (f1, f2) with
        (Amd64AbiFeature(af1), Amd64AbiFeature(af2)) -> Abi_amd64.abiFeatureTagEq0 af1 af2
       |(Amd64AbiFeature(_), _) -> false
       |(Aarch64LeAbiFeature(af1), Amd64AbiFeature(af2)) -> false
       |(Aarch64LeAbiFeature(af1), Aarch64LeAbiFeature(af2)) -> Abi_aarch64_le.abiFeatureTagEq af1 af2
    ))

let instance_Basic_classes_Ord_Abis_any_abi_feature_dict:(any_abi_feature)ord_class= ({

  compare_method = anyAbiFeatureCompare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(anyAbiFeatureCompare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (anyAbiFeatureCompare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(anyAbiFeatureCompare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (anyAbiFeatureCompare f1 f2)(Pset.from_list compare [1; 0])))})

let instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict:(any_abi_feature)abiFeatureTagEquiv_class= ({

  abiFeatureTagEquiv_method = anyAbiFeatureTagEquiv})

let make_elf64_header data osabi abiv ma t entry shoff phoff phnum shnum shstrndx:elf64_header=
       ({ elf64_ident    = ([elf_mn_mag0; elf_mn_mag1; elf_mn_mag2; elf_mn_mag3;
                           Uint32_wrapper.of_bigint elf_class_64;
                           Uint32_wrapper.of_bigint data;
                           Uint32_wrapper.of_bigint elf_ev_current;
                           Uint32_wrapper.of_bigint osabi;
                           Uint32_wrapper.of_bigint abiv;
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0));
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0));
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0));
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0));
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0));
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0));
                           Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))])
       ; elf64_type     = (Uint32_wrapper.of_bigint t)
       ; elf64_machine  = (Uint32_wrapper.of_bigint ma)
       ; elf64_version  = (Uint32_wrapper.of_bigint elf_ev_current)
       ; elf64_entry    = (Uint64_wrapper.of_bigint entry)
       ; elf64_phoff    = (Uint64_wrapper.of_bigint phoff)
       ; elf64_shoff    = (Uint64_wrapper.of_bigint shoff)
       ; elf64_flags    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
       ; elf64_ehsize   = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 64)))
       ; elf64_phentsize= (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 56)))
       ; elf64_phnum    = (Uint32_wrapper.of_bigint phnum)
       ; elf64_shentsize= (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 64)))
       ; elf64_shnum    = (Uint32_wrapper.of_bigint shnum)
       ; elf64_shstrndx = (Uint32_wrapper.of_bigint shstrndx)
       })

(*val phdr_flags_from_section_flags : natural -> string -> natural*)
let phdr_flags_from_section_flags section_flags sec_name:Nat_big_num.num=
     (let flags = (Nat_big_num.bitwise_or elf_pf_r (Nat_big_num.bitwise_or
        (if flag_is_set shf_write section_flags then elf_pf_w else  (Nat_big_num.of_int 0))
        (if flag_is_set shf_execinstr section_flags then elf_pf_x else  (Nat_big_num.of_int 0))))
    in
    (*let _ = errln ("Phdr flags of section " ^ sec_name ^ "(ELF section flags 0x " ^
        (hex_string_of_natural section_flags) ^ ") are 0x" ^ (hex_string_of_natural flags))
    in*)
    flags)

(*val phdr_is_writable : natural -> bool*)
let phdr_is_writable flags:bool=  (Nat_big_num.equal
    (Nat_big_num.bitwise_and flags elf_pf_w) elf_pf_w)

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

(* FIXME: lift this to a personality function of the GNU linker?
 * Not sure really... need to try some other linkers. *)
(*val load_can_combine_flags : can_combine_flags_fn*)
let load_can_combine_flags flagsets:(Nat_big_num.num)option=
     (
    (* The GNU linker happily adds a .rodata section to a RX segment,
     * but not to a RW segment. So the only clear rule is: if any is writable,
     * all must be writable. *)let flagslist = (Pset.elements flagsets)
    in
    let union_flags = (List.fold_left Nat_big_num.bitwise_or( (Nat_big_num.of_int 0)) flagslist)
    in
    if List.exists phdr_is_writable flagslist
    then
        if List.for_all phdr_is_writable flagslist then Some union_flags
        else None
    else
        Some union_flags)

(*val tls_can_combine_flags : can_combine_flags_fn*)
let tls_can_combine_flags flagsets:(Nat_big_num.num)option=  (Some (List.fold_left Nat_big_num.bitwise_or( (Nat_big_num.of_int 0)) (Pset.elements flagsets)))

let maybe_extend_phdr phdr isec1 can_combine_flags:(elf64_program_header_table_entry)option=
     (let new_p_type = (Uint32_wrapper.to_bigint phdr.elf64_p_type)
    in
    let this_section_phdr_flags = (phdr_flags_from_section_flags isec1.elf64_section_flags isec1.elf64_section_name_as_string)
    in
    let maybe_extended_flags = (can_combine_flags(Pset.from_list Nat_big_num.compare [ this_section_phdr_flags; Uint32_wrapper.to_bigint phdr.elf64_p_flags ]))
    in
    if (Lem.option_equal Nat_big_num.equal maybe_extended_flags None) then (*let _ = errln "flag mismatch" in*) None
    else let new_p_flags = ((match maybe_extended_flags with Some flags -> flags | _ -> failwith "impossible" ))
    in
    (* The new filesz is the file end offset of this section,
     * minus the existing file start offset of the phdr.
     * Check that the new section begins after the old offset+filesz. *)
    if Nat_big_num.less isec1.elf64_section_offset (Nat_big_num.add (Uint64_wrapper.to_bigint phdr.elf64_p_offset) (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_filesz))
    then (*let _ = errln "offset went backwards" in*) None
    else
    let new_p_filesz = (Nat_big_num.add (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_filesz) (if Nat_big_num.equal isec1.elf64_section_type sht_progbits then isec1.elf64_section_size else  (Nat_big_num.of_int 0)))
    in
    (* The new memsz is the virtual address end address of this section,
     * minus the existing start vaddr of the phdr.
     * Check that the new section begins after the old vaddr+memsz. *)
    if Nat_big_num.less isec1.elf64_section_addr (Nat_big_num.add (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_vaddr) (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_memsz))
    then (*let _ = errln "vaddr went backwards" in*) None
    else
    let new_p_memsz = (Nat_big_num.add (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_memsz) isec1.elf64_section_size)
    in
    let (one_if_zero : Nat_big_num.num -> Nat_big_num.num) = (fun n -> if Nat_big_num.equal n( (Nat_big_num.of_int 0)) then  (Nat_big_num.of_int 1) else n)
    in
    let new_p_align =  (lcm (one_if_zero (Ml_bindings.nat_big_num_of_uint64 phdr.elf64_p_align)) (one_if_zero isec1.elf64_section_align))
    in
    Some
      { elf64_p_type   = (Uint32_wrapper.of_bigint new_p_type)
       ; elf64_p_flags  = (Uint32_wrapper.of_bigint new_p_flags)
       ; elf64_p_offset = (phdr.elf64_p_offset)
       ; elf64_p_vaddr  = (phdr.elf64_p_vaddr)
       ; elf64_p_paddr  = (phdr.elf64_p_paddr)
       ; elf64_p_filesz = (Uint64_wrapper.of_bigint new_p_filesz)
       ; elf64_p_memsz  = (Uint64_wrapper.of_bigint new_p_memsz)
       ; elf64_p_align  = (Uint64_wrapper.of_bigint new_p_align)
       })

let make_new_phdr isec1 t maxpagesize1 commonpagesize1:elf64_program_header_table_entry=
     (let rounded_down_offset = (fun isec1 -> round_down_to commonpagesize1 isec1.elf64_section_offset)
    in
    let offset_round_down_amount = (fun isec1 -> Nat_big_num.sub_nat isec1.elf64_section_offset (rounded_down_offset isec1))
    in
    let rounded_down_vaddr = (fun isec1 -> round_down_to commonpagesize1 isec1.elf64_section_addr)
    in
    let vaddr_round_down_amount = (fun isec1 -> Nat_big_num.sub_nat isec1.elf64_section_addr (rounded_down_vaddr isec1))
    in
  { elf64_p_type   = (Uint32_wrapper.of_bigint t) (** Type of the segment *)
   ; elf64_p_flags  = (Uint32_wrapper.of_bigint (phdr_flags_from_section_flags isec1.elf64_section_flags isec1.elf64_section_name_as_string)) (** Segment flags *)
   ; elf64_p_offset = (Uint64_wrapper.of_bigint (rounded_down_offset isec1)) (** Offset from beginning of file for segment *)
   ; elf64_p_vaddr  = (Uint64_wrapper.of_bigint (rounded_down_vaddr isec1)) (** Virtual address for segment in memory *)
   ; elf64_p_paddr  = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) (** Physical address for segment *)
   ; elf64_p_filesz = (Uint64_wrapper.of_bigint (if Nat_big_num.equal isec1.elf64_section_type sht_nobits then  (Nat_big_num.of_int 0) else Nat_big_num.add isec1.elf64_section_size (offset_round_down_amount isec1))) (** Size of segment in file, in bytes *)
   ; elf64_p_memsz  = (Uint64_wrapper.of_bigint ( Nat_big_num.add isec1.elf64_section_size (vaddr_round_down_amount isec1))) (** Size of segment in memory image, in bytes *)
   ; elf64_p_align  = (Uint64_wrapper.of_bigint (* isec.elf64_section_align *) maxpagesize1) (** Segment alignment memory for memory and file *)
   })

(*val make_load_phdrs : forall 'abifeature. natural -> natural -> annotated_memory_image 'abifeature -> list elf64_interpreted_section -> list elf64_program_header_table_entry*)
let make_load_phdrs maxpagesize1 commonpagesize1 img2 section_pairs_bare_sorted_by_address:(elf64_program_header_table_entry)list=
     (
    (* accumulate sections into the phdr *)let rev_list = (List.fold_left (fun accum_phdr_list -> (fun isec1 -> (
        (* Do we have a current phdr? *)
        (match accum_phdr_list with
            [] -> (* no, so make one *)
                (*let _ = errln ("Starting the first LOAD phdr for section " ^ isec.elf64_section_name_as_string)
                in*)
                [make_new_phdr isec1 elf_pt_load maxpagesize1 commonpagesize1]
            | current_phdr :: more ->
                (* can we extend it with the current section? *)
                (match maybe_extend_phdr current_phdr isec1 load_can_combine_flags with
                    None ->
                        (*let _ = errln ("Starting new LOAD phdr for section " ^ isec.elf64_section_name_as_string)
                        in*)
                        (make_new_phdr isec1 elf_pt_load maxpagesize1 commonpagesize1) :: (current_phdr :: more)
                    | Some phdr -> phdr :: more
                )
        )
    ))) [] (List.filter (fun isec1 -> flag_is_set shf_alloc isec1.elf64_section_flags
        && not (flag_is_set shf_tls isec1.elf64_section_flags)) section_pairs_bare_sorted_by_address))
    in
    (*let _ = errln "Successfully made phdrs"
    in*)
    List.rev rev_list)

(*val tls_extend: forall 'abifeature. abi 'abifeature -> abi 'abifeature*)
let tls_extend a:'abifeature abi=
    ({ is_valid_elf_header = (a.is_valid_elf_header)
    ; make_elf_header     = (a.make_elf_header)
    ; reloc               = (a.reloc)
    ; section_is_special  = (a.section_is_special)
    ; section_is_large    = (a.section_is_large)
    ; maxpagesize         = (a.maxpagesize)
    ; minpagesize         = (a.minpagesize)
    ; commonpagesize      = (a.commonpagesize)
    ; symbol_is_generated_by_linker = (a.symbol_is_generated_by_linker)
    ; make_phdrs          = (fun maxpagesize1 -> fun commonpagesize1 -> fun file_type -> fun img2 -> fun section_pairs_bare_sorted_by_address -> (
        let rev_list = (List.fold_left (fun accum_phdr_list -> (fun isec1 -> (
        (match accum_phdr_list with
            [] ->
                (*let _ = errln "Making a new TLS program header" in*)
                [make_new_phdr isec1 elf_pt_tls maxpagesize1 commonpagesize1]
            | current_phdr :: more ->
                (match maybe_extend_phdr current_phdr isec1 tls_can_combine_flags with
                    None ->
                        (make_new_phdr isec1 elf_pt_tls maxpagesize1 commonpagesize1) :: (current_phdr :: more)
                    | Some phdr -> phdr :: more
                )
        )
        ))) [] (List.filter (fun isec1 -> flag_is_set shf_alloc isec1.elf64_section_flags
            && flag_is_set shf_tls isec1.elf64_section_flags) section_pairs_bare_sorted_by_address))
        in 
        List.rev_append (List.rev (a.make_phdrs maxpagesize1 commonpagesize1 file_type img2 section_pairs_bare_sorted_by_address)) (List.rev rev_list)
    ))
    ; max_phnum           = (Nat_big_num.add( (Nat_big_num.of_int 1)) a.max_phnum)
    ; guess_entry_point   = (a.guess_entry_point)
    ; pad_data            = (a.pad_data)
    ; pad_code            = (a.pad_code)
    ; generate_support    = (a.generate_support)
    ; concretise_support  = (a.concretise_support)
    ; get_reloc_symaddr   = (a.get_reloc_symaddr)
    ; parse_reloc_info    = (a.parse_reloc_info)
    })

(* We use these snappily-named functions in relocation calculations. *)

(*val make_default_phdrs : forall 'abifeature. natural -> natural -> natural (* file type *) -> annotated_memory_image 'abifeature -> list elf64_interpreted_section -> list elf64_program_header_table_entry*)
let make_default_phdrs maxpagesize1 commonpagesize1 t img2 section_pairs_bare_sorted_by_address:(elf64_program_header_table_entry)list=
     (
    (* FIXME: do the shared object and dyn. exec. stuff too *)make_load_phdrs maxpagesize1 commonpagesize1 img2 section_pairs_bare_sorted_by_address)

(*val find_start_symbol_address : forall 'abifeature. Ord 'abifeature, AbiFeatureTagEquiv 'abifeature => annotated_memory_image 'abifeature -> maybe natural*)
let find_start_symbol_address dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2:(Nat_big_num.num)option=
     (
    (* Do we have a symbol called "_start"? *)let all_defs = (Memory_image_orderings.defined_symbols_and_ranges 
  dict_Basic_classes_Ord_abifeature dict_Abi_classes_AbiFeatureTagEquiv_abifeature img2)
    in
    let get_entry_point = (fun (maybe_range, symbol_def) ->
        if symbol_def.def_symname = "_start"
        then Some (maybe_range, symbol_def)
        else None
    )
    in
    let all_entry_points = (Lem_list.mapMaybe get_entry_point all_defs)
    in
    (match all_entry_points with
        [(maybe_range, symbol_def)] ->
            (match maybe_range with
                Some (el_name, (el_off, len)) ->
                    (match Pmap.lookup el_name img2.elements with
                        None -> failwith ("_start symbol defined in nonexistent element `" ^ (el_name ^ "'"))
                        | Some el_rec ->
                            (match el_rec.startpos with
                                None -> (*let _ = Missing_pervasives.errln "warning: saw `_start' in element with no assigned address" in *)None
                                | Some x -> (* success! *) Some ( Nat_big_num.add x el_off)
                            )
                    )
                | _ -> (*let _ = Missing_pervasives.errln "warning: `_start' symbol with no range" in*) None
            )
        | [] -> (* no _start symbol *) None
        | _ -> (*let _ = Missing_pervasives.errln ("warning: saw multiple `_start' symbols: " ^
            (let (ranges, defs) = unzip all_entry_points in show ranges)) in *)None
    ))

(*val pad_zeroes : natural -> list byte*)
let pad_zeroes n:(char)list=  (replicate0 n (Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 0)))))

(*val pad_0x90 : natural -> list byte*)
let pad_0x90 n:(char)list=  (replicate0 n (Char.chr (Nat_big_num.to_int ( Nat_big_num.mul( (Nat_big_num.of_int 9))( (Nat_big_num.of_int 16))))))

(* null_abi captures ABI details common to all ELF-based, System V-based systems.
 * HACK: for now, specialise to 64-bit ABIs. *)
(*val null_abi : abi any_abi_feature*)
let null_abi:(any_abi_feature)abi=  ({
      is_valid_elf_header = is_valid_elf64_header
    ; make_elf_header = (make_elf64_header elf_data_2lsb elf_osabi_none( (Nat_big_num.of_int 0)) elf_ma_none)
    ; reloc = noop_reloc
    ; section_is_special = elf_section_is_special
    ; section_is_large = (fun s -> (fun f -> false))
    ; maxpagesize = (Nat_big_num.mul (Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 256)))( (Nat_big_num.of_int 4096))) (* 2MB; bit of a guess, based on gdb and prelink code *)
    ; minpagesize =( (Nat_big_num.of_int 1024)) (* bit of a guess again *)
    ; commonpagesize =( (Nat_big_num.of_int 4096))
    ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_")
    ; make_phdrs = make_default_phdrs
    ; max_phnum =( (Nat_big_num.of_int 2))
    ; guess_entry_point = 
  (find_start_symbol_address
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; pad_data = pad_zeroes
    ; pad_code = pad_zeroes
    ; generate_support = ( (* fun _ -> *)fun _ -> get_empty_memory_image ())
    ; concretise_support = (fun img2 -> img2)
    ; get_reloc_symaddr = 
  (default_get_reloc_symaddr
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; parse_reloc_info = parse_elf64_relocation_info
    })

(*val got_entry_ordering : (string * maybe symbol_definition) -> (string * maybe symbol_definition) -> Basic_classes.ordering*)
let got_entry_ordering (s1, md1) (s2, md2):int=  (compare s1 s2) (* FIXME *)

let is_ifunc_def:(symbol_definition)option ->bool=  (fun maybe_def ->
(match maybe_def with
 None -> false
 | Some d -> Nat_big_num.equal (get_elf64_symbol_type d.def_syment) stt_gnu_ifunc
))

let amd64_reloc_needs_got_slot:'a ->reloc_site ->(symbol_definition)option ->bool=   (fun symref -> fun rr -> fun maybe_def ->
    let (rel_type1, _) = (parse_elf64_relocation_info rr.ref_relent.elf64_ra_info) in
    if ( Pset.mem rel_type1(Pset.from_list Nat_big_num.compare [
        r_x86_64_got32; r_x86_64_gotpcrel; r_x86_64_gottpoff; r_x86_64_gotoff64; r_x86_64_gotpc32 (* ; r_x86_64_gotpc32_tlsdesc *)
    ])) then
       true
    else if is_ifunc_def maybe_def
         then
         (* This reference is bound to a STT_GNU_IFUNC definition.
          * What now needs to happen is as follows.
          * - we ensure that a GOT entry is generated for this symbol (we do this here);
          * - we ensure that a PLT entry (specifically .iplt) is generated for the symbol (Below);
          * - on making the GOT, we also generate a .rela.plt relocation record covering the GOT slot;
          * - when applying the relocation, of whatever kind, the address of the PLT slot
          *      is the address input to the calculation
          * - the code marked by the STT_GNU_IFUNC symbol definition is not the function
          *      to call; it's the function that calculates the address of the function to call!
          *      this becomes the addend of the R_X86_64_IRELATIVE Elf64_Rela marking the GOT slot
          * - note that for static linking, the GOT is usually pre-filled (cf. dynamically when it is filled by JUMP_SLOT relocs).
          *      ... but our GOT entries *must* have corresponding R_X86_64_IRELATIVEs generated
          *)
          true
    else false)


let amd64_reloc_needs_plt_slot (symref : symbol_reference_and_reloc_site) rr maybe_def ref_is_statically_linked:bool=
     (let (rel_type1, _) = (parse_elf64_relocation_info rr.ref_relent.elf64_ra_info) in
    if ( Pset.mem rel_type1(Pset.from_list Nat_big_num.compare [
        r_x86_64_plt32      (* NOTE: when generating shared libs, it starts to matter
                             * where the definition is -- anything that is locally interposable
                             * or undefined will need a slot. See amd64_get_reloc_symaddr. *)
    ])) then
       not (ref_is_statically_linked rr)
    else if is_ifunc_def maybe_def
         then
         true
    else
        (* not a PLT ref *)
        false)

let amd64_find_got_label_and_element img2:((string*(symbol_definition)option)list*element)option=
     ((match Pmap.lookup ".got" img2.elements with
        None -> (* got no GOT? okay... *) None
        | Some got_el ->
            (* Find the GOT tag. *)
            let tags_and_ranges = (Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0([])))) img2.by_tag)
            in
            (match tags_and_ranges with
                [] -> failwith "error: GOT element but no ABI feature GOT tag"
                | [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), _)] -> Some (l, got_el)
                | _ -> failwith ("multiple GOT elements/tags")
            )
    ))

let amd64_find_plt_label_and_element img2:((string*(symbol_definition)option*(any_abi_feature)plt_entry_content_fn)list*element)option=
     ((match Pmap.lookup ".plt" img2.elements with
        None -> (* got no PLT? okay... *) None
        | Some plt_el ->
            (* Find the PLT tag. *)
            let tags_and_ranges = (Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0([])))) img2.by_tag)
            in
            (match tags_and_ranges with
                [] -> failwith "error: PLT element but no ABI feature PLT tag"
                | [(AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0(l))), _)] -> Some (l, plt_el)
                | _ -> failwith ("multiple PLT elements/tags")
            )
    ))

let got_slot_index_for_symname dict_Basic_classes_Eq_a symname got_label:(int)option=
     (Lem_list.find_index (fun (s, _) -> 
  dict_Basic_classes_Eq_a.isEqual_method s symname) got_label)

(*val amd64_get_reloc_symaddr : symbol_definition -> annotated_memory_image any_abi_feature -> list (maybe element_range * symbol_definition) -> maybe reloc_site -> natural*)
let amd64_get_reloc_symaddr the_input_def output_img ranges_and_defs maybe_reloc1:Nat_big_num.num=
         (
    (* The default implementation simply looks up a "matching" symbol in the output image
     * and calculates its address.
     *
     * That's normally fine, even for via-GOT references since their calculations don't
     * use the symaddr. For via-PLT references, we need to use the PLT slot address.
     * HMM. Isn't this duplicating the role of functions like amd64_plt_slot_addr?

     * Recall that we created this get_reloc_symaddr mechanism to deal with IFUNC symbols.
     * With an IFUNC symbol, we reference it simply using a PC32 relocation, but the address
     * that gets filled in isn't the IFUNC address; it's the corresponding PLT slot.
     * HMM: does this happen for other PC32 references? If so, we'll need this mechanism
     * there. And it certainly does, because relocatable object code never uses PLT32
     * relocs.
     *
     * I had previously tried to handle this issue in mark_fate_of_relocs, using the
     * 1-argument ApplyReloc(_) and MakePIC to encode the "replacement". But at that stage,
     * which is ABI-independent and happens before address assignment?, we can't know enough.
     *)
    (* match bound_def_in_input with
        Nothing -> 0
        | Just the_input_def -> *)if is_ifunc_def (Some(the_input_def))
        then
            (* We need to return the address of the "matching" PLT slot.
             * PLT label entries are (symname, maybe_def, content_fn). *)
            (match amd64_find_plt_label_and_element output_img with
                None -> failwith "error: ifunc but no PLT"
                | Some (l, plt_el) ->
                (match Lem_list.find_index (fun (symname, _, _) -> symname = the_input_def.def_symname) l with
                    (* FIXME: using symnames seems wrong *)
                    Some idx1 ->
                        (match plt_el.startpos with
                            Some addr -> Nat_big_num.add addr (Nat_big_num.mul (Nat_big_num.of_int idx1)( (Nat_big_num.of_int 16))) (* size of a PLT entry *)
                            | None -> failwith "error: PLT has no address assigned"
                        )
                    | None -> (Nat_big_num.of_int 0)
                )
            )
        else default_get_reloc_symaddr 
  instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict the_input_def output_img ranges_and_defs maybe_reloc1)
    (* end *)

(* *)
(*val amd64_generate_support : (* list (list reloc_site_resolution) -> *) list (string * annotated_memory_image any_abi_feature) -> annotated_memory_image any_abi_feature*)
let amd64_generate_support (* reloc_resolution_lists *) input_fnames_and_imgs:(any_abi_feature)annotated_memory_image=
     (
    (* We generate a basic GOT. At the moment we can only describe the GOT
     * contents abstractly, not as its binary content, because addresses
     * have not yet been fixed.
     *
     * To do this, we create a set of Abi_amd64.GOTEntry records, one for
     * each distinct symbol that is referenced by one or more GOT-based relocations.
     * To enumerate these, we look at all the symbol refs in the image.
     *)let ref_is_statically_linked = (fun _ -> true)
    in
    let (fnames, input_imgs) = (List.split input_fnames_and_imgs)
    in
    let tags_and_ranges_by_image = (Lem_list.mapi (fun i -> fun (fname1, img2) ->
        (i, fname1, Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (SymbolRef(null_symbol_reference_and_reloc_site)) img2.by_tag)
    ) input_fnames_and_imgs)
    in
    let refs_via_got = (list_concat_map (fun (i, fname1, tags_and_ranges) -> Lem_list.mapMaybe (fun (tag, maybe_range) -> (match tag with
         SymbolRef(symref) ->
            (* Is this ref a relocation we're going to apply, and does it reference the GOT? *)
            (match (symref.maybe_reloc, symref.maybe_def_bound_to) with
                (None, _) -> None
                | (Some rr, Some(ApplyReloc, maybe_def)) ->
                    if amd64_reloc_needs_got_slot symref rr maybe_def then
                        (*let _ = errln ("Saw a via-GOT symbol reference: to `" ^ symref.ref.ref_symname ^ "' coming from linkable " ^ (show i) ^ " (" ^
                            fname ^ "), logically from section " ^ (show rr.ref_src_scn)) in *)
                        Some (symref.ref.ref_symname, maybe_def)
                    else None
                | (Some rr, Some(makePIC0, maybe_def)) -> failwith "FIXME: PIC support please"
            )
         | _ -> failwith "impossible: reloc site tag is not a SymbolRef"
    )) tags_and_ranges) tags_and_ranges_by_image)
    in
    let (symnames, maybe_defs) = (List.split refs_via_got)
    in
    (*let _ = errln ("GOT includes defs with names: " ^ (show (Set_extra.toList (Set.fromList symnames))))
    in*)
    let got_pairs_set = (Pset.from_list (pairCompare compare (maybeCompare compare)) refs_via_got)
    in
    let got_defs_set = (Pset.from_list (maybeCompare compare) maybe_defs)
    in
    (* This is where we fix the order of the GOT entries. *)
    let got_pairs_list = (Pset.elements got_pairs_set)
    in
    let got_idx_and_maybe_def_by_symname_map = (Lem_map.fromList 
  (Lem_map.instance_Map_MapKeyType_var_dict
     instance_Basic_classes_SetType_var_dict) (mapi (fun slot_idx -> fun (symname, maybe_def) -> (symname, (slot_idx, maybe_def))) got_pairs_list))
    in
    let got_ifunc_set = (let x2 =(Pset.from_list (maybeCompare compare) 
  []) in  Pset.fold
   (fun maybe_d x2 ->
    if is_ifunc_def maybe_d then Pset.add maybe_d x2 else x2) got_defs_set 
 x2)
    in
    (* Quirk: what if we have the same def appearing under two different symnames?
     * This shouldn't happen, at present.
     * What if we have the same symname related to two different defs? This also
     * shouldn't happen, because only global symbols go in the GOT, so we don't have
     * to worry about local symbols with the same name as another symbol. But still, it
     * could plausibly happen in some situations with weird symbol visibilities or binding. *)
    (* if Set.size pairs_set <> Set.size defs_set then
        failwith "something quirky going on with GOT symbol defs and their names"
    else *)
(*    let name_def_pairs = List.foldl (fun acc -> fun (idx, symname, (maybe_range, rr)) ->
        Set.insert (

                symname, (match rr.maybe_def_bound_to with
        Map.lookup symname acc with
            Nothing -> [item]
            | Just l -> item :: l
        end) acc) {} refs_via_got
    in *)
    let got_nentries = (Nat_big_num.of_int (Pset.cardinal got_pairs_set))
    in
    let got_entrysize =( (Nat_big_num.of_int 8))
    in
    (* We also need a PLT... sort of. We need a way to resolve via-PLT relocs.
     * But we might do so without actually creating a (non-zero-length) PLT.
     * Again, this is to accommodate the sorts of optimisations the GNU linker does.
     *
     * Note that every PLT entry has a corresponding GOT entry. Here we are simply
     * enumerating the via-PLT relocs that imply a PLT entry. We look their GOT
     * slots up later, by symbol name. *)
    let refs_via_plt = (list_concat_map (fun (i, fname1, tags_and_ranges) -> Lem_list.mapMaybe (fun (tag, maybe_range) -> (match tag with
         SymbolRef(symref) ->
            (* Is this ref a relocation we're going to apply, and does it reference the GOT? *)
            (match (symref.maybe_reloc, symref.maybe_def_bound_to) with
                (None, _) -> None
                | (Some rr, Some(ApplyReloc, maybe_def)) ->
                    if amd64_reloc_needs_plt_slot symref rr maybe_def ref_is_statically_linked
                    then
                        (*let _ = if is_ifunc_def maybe_def then
                         (* we ensure that a PLT entry (specifically .iplt) is generated for the symbol *)
                         errln ("Saw a reference to IFUNC symbol `" ^ symref.ref.ref_symname ^ "'; ref is coming from linkable " ^ (show i) ^ " (" ^
                            fname ^ "), relent idx " ^ (show rr.ref_rel_idx) ^ " logically from section " ^ (show rr.ref_src_scn) )
                        else
                        errln ("Saw a via-PLT symbol reference: to `" ^ symref.ref.ref_symname ^ "' coming from linkable " ^ (show i) ^ " (" ^
                            fname ^ "), relent idx " ^ (show rr.ref_rel_idx) ^ " logically from section " ^ (show rr.ref_src_scn) ^
                            match maybe_def with Just _ -> ", with definition" | Nothing -> ", not bound to anything" end
                            )
                        in*)
                        Some(symref.ref.ref_symname, maybe_def)
                    else None
                | (Some rr, Some(makePIC0, maybe_def)) -> failwith "FIXME: PIC support please"
            )
         | _ -> failwith "impossible: reloc site tag is not a SymbolRef"
    )) tags_and_ranges) tags_and_ranges_by_image)
    in
    (*let _ = errln ("Saw " ^ (show (length refs_via_plt)) ^ " relocations of a via-PLT type")
    in*)
    (* account for the optimisations we did on GOT slots *)
    let refs_via_plt_having_got_slot = (Lem_list.mapMaybe (fun (symname, _) ->
        (match Pmap.lookup symname got_idx_and_maybe_def_by_symname_map with
            Some(idx1, maybe_d) -> Some (symname, idx1, maybe_d)
            | None -> None
            )
        ) refs_via_plt)
    in
    (*let _ = errln ("Saw " ^ (show (length refs_via_plt_having_got_slot)) ^ " relocations of a via-PLT type where we instantiated a GOT slot for the symbol")
    in*)
    let (plt_symnames, plt_got_idxs, plt_ref_bound_to_maybe_defs) = (unzip3 refs_via_plt_having_got_slot)
    in
    let plt_symnames_excluding_header = (Pset.elements ((Pset.from_list compare plt_symnames)))
    in
    (*let _ = errln ("PLT symnames: " ^ (show plt_symnames_excluding_header))
    in*)
    let n_iplt_entries = (Pset.cardinal got_ifunc_set)
        (* The content of the IPLT entries depends on the address assignment of GOT slots
         * and the IFUNCs that they reference. We need to reserve space for them here, though. *)
    in
    (*let _ = errln ("We think there should be " ^ (show n_iplt_entries) ^ " PLT entries due to references to IFUNC symbols")
    in*)
    (* let got_entries_referencing_functions =  (List.filter (fun (symname, maybe_def) ->
            match def with
                Just d -> d.def_syment
                | Nothing -> false
            end) refs_via_got)
    in *)
    let plt_needs_header_entry = ((List.length plt_symnames_excluding_header) > n_iplt_entries)
    in
    (*let _ = errln ("PLT needs header entry? " ^ (show plt_needs_header_entry))
    in*)
    let total_n_plt_entries = (Nat_big_num.add (if plt_needs_header_entry then  (Nat_big_num.of_int 1) else  (Nat_big_num.of_int 0)) (Missing_pervasives.length plt_symnames_excluding_header))
    in
    (*let _ = errln ("PLT total entry count: " ^ (show total_n_plt_entries))
    in*)
    let new_by_range =(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [
        (Some(".plt", ( (Nat_big_num.of_int 0), Nat_big_num.mul( (Nat_big_num.of_int 16)) total_n_plt_entries)), AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0(
                 (* header content fn *)
                 (* the header entry is required only for dynamic linking, which is not supported yet *)
                 (* (if plt_needs_header_entry then
                    ("", Nothing, (((fun (got_base_addr : natural) -> fun (plt_base_addr : natural) ->
                     (0, [byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0;
                      byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0;
                      byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0;
                      byte_of_natural 0; byte_of_natural 0; byte_of_natural 0; byte_of_natural 0]))) : plt_entry_content_fn any_abi_feature))
                 else ("", Nothing, (((fun (got_base_addr : natural) -> fun (plt_base_addr : natural) -> (0, []))) : plt_entry_content_fn any_abi_feature))
                 )
                 ++ *) (
                 mapi (fun plt_entry_idx_not_counting_header -> (fun symname ->
                    (* We want to label the PLT entry with a function that
                     * - accepts the PLT base address, the GOT base address and the GOT slot number;
                     * - closure-captures whatever else it needs (whether we're inserting a PLT header);
                     * - yields the *full contents of the PLT entry* before relocation.
                     * - recall that PLT entries might be "header" (the special one at the start),
                     *      "normal" (to be relocated with R_X86_64_JUMP_SLOT)
                     *   or "irelative" (to be relocated with R_X86_64_IRELATIVE).
                     *    Q. Why are R_X86_64_JUMP_SLOT necessary?
                     *       The PLT entries are doing relative addressing, and
                     *       the offset to the GOT entry is known at link time,
                     *       so the linker should be able to fill them in. In
                     *       fact, it does. HMM. Understand this better. *)
                    (* What is the GOT slot number? *)
                    let (got_slot_idx, maybe_def) = ((match Pmap.lookup symname got_idx_and_maybe_def_by_symname_map with
                        Some(idx1, maybe_d) -> (Nat_big_num.of_int idx1, maybe_d)
                        | None -> failwith ("GOT does not contain symbol `" ^ (symname ^ "' required by PLT entry"))
                        ))
                    in
                    (symname, maybe_def, ((fun (got_base_addr : Nat_big_num.num) -> fun (plt_base_addr : Nat_big_num.num) ->
                        (* Okay, now we can generate the entry. NOTE that we're lexically still in generate_support,
                         * but we'll be called from concretise_support. The code that generates the header
                         * entry is actually in concretise_support.
                         *
                         * If the entry is a normal entry, it looks like
                         *
                               0x0000000000400410 <+0>:     ff 25 02 0c 20 00       jmpq   *0x200c02(%rip)        # 0x601018 <puts@got.plt>
                               0x0000000000400416 <+6>:     68 00 00 00 00  pushq  $0x0
                               0x000000000040041b <+11>:    e9 e0 ff ff ff  jmpq   0x400400
                         *
                         * If the entry is an irelative entry, it looks like
                         *
                              400350:       ff 25 02 fd 2b 00       jmpq   *0x2bfd02(%rip)        # 6c0058 <_GLOBAL_OFFSET_TABLE_+0x58>
                              400356:       68 00 00 00 00          pushq  $0x0
                              40035b:       e9 00 00 00 00          jmpq   400360 <check_one_fd.part.0>

                         * ... i.e. basically the same but the pushq and jmpq have literal-zero args (they're not used).
                         *)
                        let this_plt_slot_base_addr = (Nat_big_num.add plt_base_addr (Nat_big_num.mul( (Nat_big_num.of_int 16)) (
                            Nat_big_num.add(Nat_big_num.of_int plt_entry_idx_not_counting_header) (if plt_needs_header_entry then  (Nat_big_num.of_int 1) else  (Nat_big_num.of_int 0)))))
                        in
                        (*let _ = Missing_pervasives.errln ("PLT slot base address for symname `" ^ symname ^ "': 0x" ^
                            (hex_string_of_natural this_plt_slot_base_addr))
                        in*)
                        let got_slot_addr = (Nat_big_num.add got_base_addr (Nat_big_num.mul( (Nat_big_num.of_int 8)) got_slot_idx))
                        in
                        (*let _ = Missing_pervasives.errln ("GOT slot address for symname `" ^ symname ^ "' (idx " ^ (show got_slot_idx) ^ "): 0x" ^
                            (hex_string_of_natural got_slot_addr))
                        in*)
                        let maybe_header_entry_address = (if plt_needs_header_entry then Some(plt_base_addr) else None)
                        in
                        let offset_to_got_slot = (Nat_big_num.sub ( got_slot_addr) (( Nat_big_num.add this_plt_slot_base_addr( (Nat_big_num.of_int 6)))))
                        in
                        (*let _ = Missing_pervasives.errln ("PLT's PC-relative index to GOT slot for symname `" ^ symname ^ "' (GOT idx " ^ (show got_slot_idx) ^ ") is (decimal)" ^
                            (show offset_to_got_slot))
                        in*)
                        let content_bytes = 
                        (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev [Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 255))); Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 37)))]) (* offset to the GOT entry, from the *next* instruction start, signed 32-bit LE *) (to_le_signed_bytes( (Nat_big_num.of_int 4)) offset_to_got_slot))) [Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 104)))])) (* plt slot number not including header, 32-bit LE *) (to_le_unsigned_bytes( (Nat_big_num.of_int 4)) ((Nat_big_num.of_int plt_entry_idx_not_counting_header))))) [Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 233)))])) (to_le_signed_bytes( (Nat_big_num.of_int 4)) (
                            if is_ifunc_def maybe_def
                            then  (Nat_big_num.of_int 0)
                            else (match maybe_header_entry_address with
                                None -> failwith "normal PLT entry but no PLT header!"
                                | Some header_entry_address -> Nat_big_num.sub ( header_entry_address) (( Nat_big_num.add this_plt_slot_base_addr( (Nat_big_num.of_int 16))))
                                )
                        )))
                        in
                        (*let _ = errln ("Created a PLT entry consisting of " ^ (show (length content_bytes)) ^ " bytes.")
                        in*)
                        (this_plt_slot_base_addr, content_bytes)
                        (*
                        match maybe_def with
                            Nothing -> 0
                            | Just sd ->
                                match Memory_image_orderings.find_defs_matching sd img with
                                    [] -> failwith ("no matching definitions for PLT entry named " ^ symname)
                                    | [(Just(def_el_name, (def_start, def_len)), d)] ->
                                        match element_and_offset_to_address (def_el_name, def_start) img with
                                            Nothing -> failwith ("PLT: no address for definition offset in element " ^ def_el_name)
                                            | Just x ->
                                                let _ = errln ("PLT slot for symbol `" ^ symname ^
                                                    "' calculated at (non-PLT) address 0x" ^ (hex_string_of_natural x) ^
                                                    " (offset 0x" ^ (hex_string_of_natural def_start) ^ " in element " ^ def_el_name ^ ")")
                                                in
                                                x
                                        end
                                    | _ -> failwith ("multiple matching definitions for PLT entry named " ^ symname)
                                end
                        end
                        *)

                    ) : any_abi_feature plt_entry_content_fn))
                ))
                plt_symnames)
            )))
        )
    ;   (Some(".plt", ( (Nat_big_num.of_int 0), Nat_big_num.mul( (Nat_big_num.of_int 16)) total_n_plt_entries)), FileFeature(ElfSection( (Nat_big_num.of_int 1),
          { elf64_section_name =( (Nat_big_num.of_int 0)) (* ignored *)
           ; elf64_section_type = sht_progbits
           ; elf64_section_flags = shf_alloc
           ; elf64_section_addr =( (Nat_big_num.of_int 0)) (* ignored -- covered by element *)
           ; elf64_section_offset =( (Nat_big_num.of_int 0)) (* ignored -- will be replaced when file offsets are assigned *)
           ; elf64_section_size = (Nat_big_num.mul( (Nat_big_num.of_int 16)) total_n_plt_entries) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *)
           ; elf64_section_link =( (Nat_big_num.of_int 0))
           ; elf64_section_info =( (Nat_big_num.of_int 0))
           ; elf64_section_align =( (Nat_big_num.of_int 16))
           ; elf64_section_entsize =( (Nat_big_num.of_int 16))
           ; elf64_section_body = Byte_sequence.empty (* ignored *)
           ; elf64_section_name_as_string = ".plt"
           }
        )))
        (* For each GOT entry that corresponds to a thread-local symbol, we also need to
         * generate a relocation record. HMM. These new relocation records are ones we don't
         * yet have decisions for. That might be a problem.
         *
         * In fact, this approach is not appropriate for static linking. Just put the offsets
         * in there when we concretise the GOT. Something like this will be good for
         * dynamic linking, though. At the moment, creating a SymbolRef at this stage
         * is problematic because it's not in the bindings list. When we generate shared
         * objects, we'll have to revisit that code. *)
        (* (Just(".got", (i * got_entrysize, 8)), SymbolRef( <|
                ref = <| ref_symname = symname
                       ; ref_syment = sd.def_syment
                       ; ref_sym_scn = 0
                       ; ref_sym_idx = 0
                       |>
                ; maybe_def_bound_to = Just(ApplyReloc, Just sd)
                ; maybe_reloc = Just(
                  <|
                        ref_relent  =
                            <| elf64_ra_offset = elf64_addr_of_natural 0
                             ; elf64_ra_info   = elf64_xword_of_natural r_x86_64_tpoff64
                             ; elf64_ra_addend = elf64_sxword_of_integer 0
                             |>
                      ; ref_rel_scn = 0
                      ; ref_rel_idx = 0
                      ; ref_src_scn = 0
                   |>
                )
              |>))
              | forall ((i, symname, sd) IN (Set.fromList (mapMaybei (fun i -> fun (symname, maybe_def) ->
                match maybe_def with Nothing -> Nothing | Just sd -> Just(i, symname, sd) end) refs_via_got)))
              | get_elf64_symbol_type sd.def_syment = stt_tls
     *)
    ;   (Some(".got", ( (Nat_big_num.of_int 0), Nat_big_num.mul got_nentries got_entrysize)), AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(got_pairs_list))))
    ;   (Some(".got", ( (Nat_big_num.of_int 0), Nat_big_num.mul got_nentries got_entrysize)), FileFeature(ElfSection( (Nat_big_num.of_int 2),
          { elf64_section_name =( (Nat_big_num.of_int 0)) (* ignored *)
           ; elf64_section_type = sht_progbits
           ; elf64_section_flags = (Nat_big_num.bitwise_or shf_write shf_alloc)
           ; elf64_section_addr =( (Nat_big_num.of_int 0)) (* ignored -- covered by element *)
           ; elf64_section_offset =( (Nat_big_num.of_int 0)) (* ignored -- will be replaced when file offsets are assigned *)
           ; elf64_section_size = (Nat_big_num.mul got_nentries got_entrysize) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *)
           ; elf64_section_link =( (Nat_big_num.of_int 0))
           ; elf64_section_info =( (Nat_big_num.of_int 0))
           ; elf64_section_align =( (Nat_big_num.of_int 8))
           ; elf64_section_entsize = got_entrysize
           ; elf64_section_body = Byte_sequence.empty (* ignored *)
           ; elf64_section_name_as_string = ".got"
           }
        )))
    ;   (* FIXME: I've a feeling _GLOBAL_OFFSET_TABLE_ generally doesn't mark the *start* of the GOT;
         * it's some distance in. What about .got.plt? *)
        (Some(".got", ( (Nat_big_num.of_int 0), Nat_big_num.mul got_nentries got_entrysize)), SymbolDef({
              def_symname = "_GLOBAL_OFFSET_TABLE_"
            ; def_syment =    ({ elf64_st_name  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* ignored *)
                               ; elf64_st_info  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* FIXME *)
                               ; elf64_st_other = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* FIXME *)
                               ; elf64_st_shndx = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 1)))
                               ; elf64_st_value = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0))) (* ignored *)
                               ; elf64_st_size  = (Uint64_wrapper.of_bigint ( Nat_big_num.mul got_nentries got_entrysize)) (* FIXME: start later, smaller size? zero size? *)
                               })
            ; def_sym_scn =( (Nat_big_num.of_int 1))
            ; def_sym_idx =( (Nat_big_num.of_int 1))
            ; def_linkable_idx =( (Nat_big_num.of_int 0))
            }))
    ; (Some(".rela.iplt", ( (Nat_big_num.of_int 0), (* size of an Elf64_Rela *) Nat_big_num.mul( (Nat_big_num.of_int 24)) (Nat_big_num.of_int n_iplt_entries))), FileFeature(ElfSection( (Nat_big_num.of_int 3),
          { elf64_section_name =( (Nat_big_num.of_int 0)) (* ignored *)
           ; elf64_section_type = sht_rela
           ; elf64_section_flags = (Nat_big_num.bitwise_or shf_alloc shf_info_link)
           ; elf64_section_addr =( (Nat_big_num.of_int 0)) (* ignored -- covered by element *)
           ; elf64_section_offset =( (Nat_big_num.of_int 0)) (* ignored -- will be replaced when file offsets are assigned *)
           ; elf64_section_size = ( (* size of an Elf64_Rela *)Nat_big_num.mul( (Nat_big_num.of_int 24)) (Nat_big_num.of_int n_iplt_entries)) (* ignored? NO, we use it in linker_script to avoid plumbing through the element record *)
           ; elf64_section_link =( (Nat_big_num.of_int 0))
           ; elf64_section_info =( (* FIXME: want this to be the PLT section shndx *) (Nat_big_num.of_int 0))
           ; elf64_section_align =( (Nat_big_num.of_int 8))
           ; elf64_section_entsize =( (Nat_big_num.of_int 24))
           ; elf64_section_body = Byte_sequence.empty (* ignored *)
           ; elf64_section_name_as_string = ".rela.iplt"
           }
        )))
    ])
    in
    {  elements = (Pmap.add ".got" {
                    startpos = None
               ;    length1 = (Some ( Nat_big_num.mul got_nentries got_entrysize))
               ;    contents = ([])
               } (Pmap.add ".plt" {
                    startpos = None
               ;    length1 = (let len = (Nat_big_num.mul( (Nat_big_num.of_int 16)) total_n_plt_entries) in
                        (*let _ = errln ("PLT length in element: " ^ (show len) ^ " bytes")
                        in *) Some ( Nat_big_num.mul( (Nat_big_num.of_int 16)) total_n_plt_entries))
               ;    contents = ([])
               } (Pmap.add ".rela.iplt" {
                    startpos = None
               ;    length1 = (Some ( (* size of an Elf64_Rela *) Nat_big_num.mul( (Nat_big_num.of_int 24)) (Nat_big_num.of_int n_iplt_entries)))
               ;    contents = ([])
               } (Pmap.empty compare)
               )))
     ;   by_tag = (by_tag_from_by_range 
  (instance_Basic_classes_SetType_Maybe_maybe_dict
     (instance_Basic_classes_SetType_tup2_dict
        instance_Basic_classes_SetType_var_dict
        (instance_Basic_classes_SetType_tup2_dict
           instance_Basic_classes_SetType_Num_natural_dict
           instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict new_by_range)
     ;   by_range = new_by_range
     })

(*val amd64_concretise_support : annotated_memory_image any_abi_feature -> annotated_memory_image any_abi_feature*)
let amd64_concretise_support orig_img:(any_abi_feature)annotated_memory_image=
     (
    (*let _ = errln "Concretising amd64 ABI support structures"
    in*)
    (* Fill in the GOT contents. *)(match amd64_find_got_label_and_element orig_img with
        None -> orig_img (* no GOT, but that's okay *)
        | Some (got_l, got_el) ->
    let got_base_addr = ((match got_el.startpos with
        Some a -> a
        | None -> failwith "GOT has no address assigned"
    ))
    in
    let (ranges_and_defs : ( element_range option * symbol_definition) list) = (Memory_image_orderings.defined_symbols_and_ranges 
  instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict orig_img)
    in
    let got_entry_bytes_for = (fun img2 -> fun symname -> fun maybe_def -> fun plt_l -> fun maybe_plt_el -> (match maybe_def with
        None -> replicate0( (Nat_big_num.of_int 8)) (Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 0))))
        | Some sd ->
            (* What should the GOT slot be initialized to point to?
             * If there's a PLT entry, we should point to that + 6,
             * i.e. the second instruction.
             *
             * If there's not, then it might be a thread-local. *)
            (match Lem_list.find_index (fun (plt_symname, _, _) -> symname = plt_symname) plt_l with
                Some plt_slot_idx ->
                    (match maybe_plt_el with
                        None -> failwith "GOT slot with PLT entry but no PLT element"
                       | Some plt_el ->
                    (match plt_el.startpos with
                        Some addr -> natural_to_le_byte_list_padded_to( (Nat_big_num.of_int 8)) ( Nat_big_num.add (Nat_big_num.add addr ( Nat_big_num.mul(Nat_big_num.of_int plt_slot_idx)( (Nat_big_num.of_int 16))))( (Nat_big_num.of_int 6)))
                        | None -> failwith ("no PLT!")
                    )
                    )
                | None ->
                    (* Just look for a definition. *)
                        (match Memory_image_orderings.find_defs_matching sd ranges_and_defs with
                        [] -> failwith ("no matching definitions for GOT entry named " ^ symname)
                        | [(Some(def_el_name, (def_start, def_len)), d)] ->
                            (match element_and_offset_to_address (def_el_name, def_start) img2 with
                                None -> failwith ("no address for definition offset in element " ^ def_el_name)
                                | Some x ->
                                    (* If sd is a TLS symbol, we want its offset from the *end* of the
                                     * TLS segment. *)
                                    (* FIXME: factor out this logic so that it lives in the TLS ABI spec. *)
                                    if Nat_big_num.equal (get_elf64_symbol_type sd.def_syment) stt_tls then
                                        (* FIXME: the right way to do this is to mark the segments in the image
                                         * *first*. They can't have ranges, because they span many elements,
                                         * but they can have vaddr ranges as arguments. *)
                                        let offs = (i2n_signed 64 (Nat_big_num.sub( (Nat_big_num.of_int 0))( (Nat_big_num.of_int 8))))
                                        in
                                        (*let _ = errln ("GOT slot for TLS symbol `" ^ symname ^
                                            "' created containing offset 0x" ^ (hex_string_of_natural offs))
                                        in*)
                                        natural_to_le_byte_list offs
                                    else (*let _ = errln ("GOT slot for symbol `" ^ symname ^
                                        "' created pointing to address 0x" ^ (hex_string_of_natural x) ^
                                        " (offset 0x" ^ (hex_string_of_natural def_start) ^ " in element " ^ def_el_name ^ ")")
                                    in*)
                                    natural_to_le_byte_list_padded_to( (Nat_big_num.of_int 8)) x
                            )
                        | [(None, _)]  -> failwith ("matching definition for GOT entry named " ^ (symname ^ " has no range"))
                        | _ -> failwith ("multiple matching definitions for GOT entry named " ^ symname)
                    )
            )
    ))
    in
    let concretise_got = (fun img2 -> fun plt_l -> fun maybe_plt_el ->
        let l = got_l
        (*       Just(got_el_name, (got_start_off, got_len)))] ->   *)
        in
        (*let _ = errln ("Concretising a GOT of " ^ (show (length l)) ^ " entries.")
        in*)
        let got_entry_contents = (Lem_list.map (fun (symname, maybe_def) ->
            Lem_list.map (fun b -> Some b) (got_entry_bytes_for img2 symname maybe_def plt_l maybe_plt_el)) l)
        in
        (* We replace the GOT element's contents with the concrete addresses
         * of the symbols it should contain. We leave the metadata label in there,
         * for the relocation logic to find. If we change the order of entries,
         * change it there too. *)
        let got_content = (List.concat got_entry_contents)
        in
        let new_got_el =
            ({ contents = got_content
             ; startpos = (got_el.startpos)
             ; length1   = (got_el.length1)
             })
        in
        let new_got_tag = (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))))
        in
        let got_range = (Some(".got", ( (Nat_big_num.of_int 0), Nat_big_num.mul( (Nat_big_num.of_int 8)) (length l))))
        in
        let new_by_tag =
             (Pset.(union)( Pset.diff(img2.by_tag : (( any_abi_feature range_tag) * ( element_range option)) Pset.set)(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), got_range)]))(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [(new_got_tag, got_range)]))
        in
        let new_elements_map = (Pmap.add ".got" new_got_el (
            Pmap.remove ".got" img2.elements
        ))
        in
        { elements = new_elements_map
         ; by_tag   = new_by_tag
         ; by_range = (by_range_from_by_tag 
  instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict))) new_by_tag)
         })
    in
    (match amd64_find_plt_label_and_element orig_img with
        None -> concretise_got orig_img [] None (* no PLT, but possibly a GOT *)
        | Some (plt_l, plt_el) ->
    let plt_base_addr = ((match plt_el.startpos with
        Some a -> a
        | None -> failwith "PLT has no address assigned"
    ))
    in
    let concretise_plt = (fun img2 ->
       let l = plt_l
       in
        (* We replace the PLT element's contents with the concrete entries
         * for each of the symbols in the table. We leave the metadata label in there,
         * for the relocation logic to find. If we change the order of entries,
         * change it there too. *)
        let all_content = (List.concat (Lem_list.map (fun (_, _, plt_content_fn) ->
            let (_, content) = (plt_content_fn got_base_addr plt_base_addr) in
            content
        ) l))
        in
        (*let _ = errln ("Got " ^ (show (length all_content)) ^ " bytes of PLT content")
        in
        let _ = errln ("Generated PLT reserved " ^ (show (match plt_el.length with
            Just n -> n
            | Nothing -> failwith "PLT has no length"
        end)) ^ " bytes of PLT content")
        in*)
        let new_plt_el =
            ({ contents = (Lem_list.map (fun b -> Some b) all_content)
             ; startpos = (plt_el.startpos)
             ; length1   = (Some(length all_content))
             })
        in
        let new_elements_map = (Pmap.add ".plt" new_plt_el (
            Pmap.remove ".plt" img2.elements
        ))
        in
        { elements = new_elements_map
         ; by_tag   = (img2.by_tag)
         ; by_range = (img2.by_range)
         })
    in
    let concretise_rela_plt = (fun img2 ->
        let maybe_rela_plt_el = (Pmap.lookup ".rela.plt" img2.elements)
        in
        let maybe_new_rela_plt_el = ((match maybe_rela_plt_el with
            None -> (* got no .rela.plt? okay... *)
                (*let _ = errln "No .rela.plt found"
                in*)
                None
            | Some rela_plt_el ->
                let got_entry_iplt_widget_for = (fun symname -> fun maybe_def -> (match maybe_def with
                    None -> None
                    | Some sd ->
                        if not (Nat_big_num.equal (get_elf64_symbol_type sd.def_syment) stt_gnu_ifunc) then None
                        else Some(fun index_in_got ->
                            (* This is a 24-byte Elf64_Rela. *)
                            let (r_offset : Nat_big_num.num) (* GOT *slot* address! *) =
                                ((match got_el.startpos with
                                    None -> failwith "internal error: GOT has no assigned address"
                                    | Some addr -> Nat_big_num.add addr ( Nat_big_num.mul( (Nat_big_num.of_int 8)) index_in_got)
                                ))
                            in
                            let (r_info : Nat_big_num.num) = r_x86_64_irelative in
                            ( List.rev_append (List.rev (List.rev_append (List.rev (natural_to_le_byte_list_padded_to( (Nat_big_num.of_int 8)) r_offset)) (natural_to_le_byte_list_padded_to( (Nat_big_num.of_int 8)) r_info)))
                            (* r_addend -- address of the ifunc definition.
                             * NOTE that this is NOT the same as the GOT entry bytes.
                             * It's the actual address of the ifunc, whereas
                             * the GOT entry is initialized to point back into the PLT entry. *) (match Memory_image_orderings.find_defs_matching sd ranges_and_defs with
                                  [] -> failwith ("impossible: IPLT entry widget found matching ifunc definition for " ^ symname)
                                | [(Some(def_el_name, (def_start, def_len)), d)] ->
                                    (match element_and_offset_to_address (def_el_name, def_start) img2 with
                                        None -> failwith ("no address for ifunc definition offset in element " ^ def_el_name)
                                        | Some x ->
                                            (* If sd is a TLS symbol, we want its offset from the *end* of the
                                             * TLS segment. *)
                                            (* FIXME: factor out this logic so that it lives in the TLS ABI spec. *)
                                            if not (Nat_big_num.equal (get_elf64_symbol_type sd.def_syment) stt_gnu_ifunc)
                                            then failwith "impossible: found ifunc definition that is not an ifunc"
                                            else
                                                natural_to_le_byte_list_padded_to( (Nat_big_num.of_int 8)) x
                                    )
                                | _ -> failwith "impossible: more than one ifunc definition"
                             )
                           ))
                        (* end Just sd *)
                    ))
                in
                let rela_iplt_widgets = (Lem_list.map (fun (symname, maybe_def) -> got_entry_iplt_widget_for symname maybe_def) got_l)
                in
                let new_content_bytelists =
                    (mapi (fun i -> fun rela_widget ->
                    (match rela_widget with
                        Some f -> f (Nat_big_num.of_int i)
                        | None -> []
                    )
                    ) rela_iplt_widgets)
                in
                let new_contents = (Lem_list.map (fun b -> Some b) (List.concat new_content_bytelists))
                in
                (*let _ = errln ("Concretised .rela.plt; first 24 bytes: " ^ (show (take 24 new_contents)))
                in*)
                Some(
                    { contents = new_contents
                     ; startpos = (rela_plt_el.startpos)
                     ; length1   = (rela_plt_el.length1)
                     }
                )
        ))
        in
        let new_elements_map = ((match maybe_new_rela_plt_el with
            Some new_rela_plt_el -> Pmap.add ".rela.plt" new_rela_plt_el (
                Pmap.remove ".rela.plt" img2.elements
            )
            | None -> img2.elements
        ))
        in
        { elements = new_elements_map
         ; by_tag   = (img2.by_tag)
         ; by_range = (img2.by_range)
         })
    in
    concretise_rela_plt (concretise_plt (concretise_got orig_img plt_l (Some plt_el)))
) ))

(*val amd64_got_slot_idx : annotated_memory_image any_abi_feature -> symbol_reference_and_reloc_site -> natural*)
let amd64_got_slot_idx img2 rr:Nat_big_num.num=
     (
    (*let _ = errln ("Looking up GOT slot for symbol " ^ rr.ref.ref_symname) in*)(match Pmap.lookup ".got" img2.elements with
        None -> (* got no GOT? okay... *) failwith "got no GOT"
        | Some got_el ->
            (* Find the GOT tag. *)
            let tags_and_ranges = (Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0([])))) img2.by_tag)
            in
            (match tags_and_ranges with
                [] -> failwith "error: GOT element but no ABI feature GOT tag"
                | [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), Some(got_el_name, (got_start_off, got_len)))] ->
                    (* Find the slot corresponding to rr, if we have one. *)
                    let got_addr = ((match got_el.startpos with Some addr -> addr | None -> failwith "GOT has no addr at reloc time" ))
                    in
                    (match rr.maybe_def_bound_to with
                        Some (_, Some(d)) ->
                            (match Lem_list.find_index (fun (symname, maybe_def) -> (Lem.option_equal (=) (Some(d)) maybe_def)) l with
                                Some idx1 -> Nat_big_num.of_int idx1
                             |  None -> failwith ("no GOT slot for reloc against `" ^ (rr.ref.ref_symname ^ "'"))
                            )
                        | Some(_, None) -> (* HACK: look for the weak symname. Really want more (ref-based) labelling. *)
                            (match Lem_list.find_index (fun (symname, _) -> symname = rr.ref.ref_symname) l with
                                Some idx1 -> Nat_big_num.of_int idx1
                             |  None -> failwith ("no GOT slot for reloc against undefined symbol `" ^ (rr.ref.ref_symname ^ "'"))
                            )
                        | _ -> failwith "GOT: unbound def"
                    )
                | _ -> failwith "got bad GOT"
            )
    ))

(*val amd64_got_slot_addr : annotated_memory_image any_abi_feature -> symbol_reference_and_reloc_site -> natural*)
let amd64_got_slot_addr img2 rr:Nat_big_num.num=
     ((match Pmap.lookup ".got" img2.elements with
        None -> (* got no GOT? okay... *) failwith "got no GOT"
        | Some got_el ->
            (* Find the GOT tag. *)
            let tags_and_ranges = (Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0([])))) img2.by_tag)
            in
            (match tags_and_ranges with
                [] -> failwith "error: GOT element but no ABI feature GOT tag"
                | [(AbiFeature(Amd64AbiFeature(Abi_amd64.GOT0(l))), Some(got_el_name, (got_start_off, got_len)))] ->
                    (* Find the slot corresponding to rr, if we have one. *)
                    let got_addr = ((match got_el.startpos with Some addr -> addr | None -> failwith "GOT has no addr at reloc time" ))
                    in Nat_big_num.add (Nat_big_num.mul( (Nat_big_num.of_int 8)) (amd64_got_slot_idx img2 rr)) got_addr
                | _ -> failwith "got bad GOT"
            )
    ))

(*val amd64_plt_slot_addr : annotated_memory_image any_abi_feature -> symbol_reference_and_reloc_site -> natural -> natural*)
let amd64_plt_slot_addr img2 rr raw_addr:Nat_big_num.num=
     ((match Pmap.lookup ".plt" img2.elements with
        None ->
            (* got no PLT? okay... under static linking this can happen.
               We use the actual symbol address of the *)
            (*let _ = errln "Warning: no PLT, so attempting to use actual symbol address as PLT slot address"
            in*)
            (* if raw_addr = 0 then failwith "bailing rather than resolving PLT slot to null address (perhaps conservatively)" else  *)
            raw_addr
        | Some plt_el ->
            (* Find the PLT tag. *)
            let tags_and_ranges = (Multimap.lookupBy0 
  (instance_Basic_classes_Ord_Memory_image_range_tag_dict
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
   (instance_Basic_classes_Ord_tup2_dict
      Lem_string_extra.instance_Basic_classes_Ord_string_dict
      (instance_Basic_classes_Ord_tup2_dict
         instance_Basic_classes_Ord_Num_natural_dict
         instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict
   (instance_Basic_classes_SetType_tup2_dict
      instance_Basic_classes_SetType_var_dict
      (instance_Basic_classes_SetType_tup2_dict
         instance_Basic_classes_SetType_Num_natural_dict
         instance_Basic_classes_SetType_Num_natural_dict)))  (Memory_image_orderings.tagEquiv
    instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0([])))) img2.by_tag)
            in
            (match tags_and_ranges with
                [] -> failwith "error: PLT element but no ABI feature PLT tag"
                | [(AbiFeature(Amd64AbiFeature(Abi_amd64.PLT0(l))), Some(plt_el_name, (plt_start_off, plt_len)))] ->
                    let plt_addr = ((match plt_el.startpos with Some addr -> addr | None -> failwith "PLT has no addr at reloc time" ))
                    in
                    (* Find the slot corresponding to rr, if we have one. *)
                    (match rr.maybe_def_bound_to with
                        Some (_, Some(d)) ->
                            (match Lem_list.mapMaybe (fun (symname, maybe_def, fn) -> if (Lem.option_equal (=) (Some(d)) maybe_def) then Some fn else None) l with
                                [fn] ->
                                    let got_addr =
                                         ((match Pmap.lookup ".got" img2.elements with
                                            None -> (* got no GOT? okay... *) failwith "got no GOT (applying PLT calculation)"
                                            | Some got_el -> (match got_el.startpos with
                                                Some addr -> addr
                                                | None -> failwith "concrete GOT has no addr"
                                                )
                                        ))
                                    in
                                    let (addr, content) = (fn got_addr plt_addr)
                                    in
                                    (*let _ = errln ("Calculated PLT slot for `" ^ d.def_symname ^ "', from PLT addr " ^ (hex_string_of_natural plt_addr)
                                        ^ " and GOT addr " ^ (hex_string_of_natural got_addr) ^ ", as " ^ (hex_string_of_natural addr))
                                    in*)
                                    addr
                                | [] -> (* failwith ("internal error: no PLT entry for reloc against `" ^ rr.ref.ref_symname ^ "'") *)
                                    (* If we got no PLT slot, we assume it's because the PLT entry was optimised out.
                                     * So we just return the address of the symbol itself. *)
                                    (*let _ = errln ("No PLT entry for reloc against `" ^ rr.ref.ref_symname ^
                                        "', which we assume was optimised to avoid the GOT")
                                    in*)
                                    let (ranges_and_defs : ( element_range option * symbol_definition) list) = (defined_symbols_and_ranges 
  instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict img2)
                                    in
                                    (match Memory_image_orderings.find_defs_matching d ranges_and_defs with
                                        [] -> (Nat_big_num.of_int 0) (* HMM -- should be an error? *)
                                        | [(Some(el_name, (start_off, len)), matching_d)] ->
                                            (match element_and_offset_to_address (el_name, start_off) img2 with
                                                Some a -> a
                                                | None -> failwith ("internal error: could not get address for PLT-short-circuited symbol `" ^ (rr.ref.ref_symname ^ "'"))
                                            )
                                        | _ -> failwith ("output image has multiple and/or no-location definitions to which via-PLT ref to `" ^ (rr.ref.ref_symname ^ "' could resolve"))
                                    )
                                | _ ->  failwith ("internal error: multiple PLT entries for reloc against `" ^ (rr.ref.ref_symname ^ "'"))
                            )
                        | Some(_, None) -> (* weak, so 0 *) (Nat_big_num.of_int 0)
                        | _ -> failwith "PLT: unbound def"
                    )
                | _ -> failwith "got bad PLT"
            )
    ))

(** [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. *)
(*val amd64_base_addr : symbol_reference_and_reloc_site -> natural -> natural*)
let amd64_base_addr rr site_addr:Nat_big_num.num=
     (let reloc_site1 = ((match rr.maybe_reloc with
    | None -> failwith "amd64_base_addr: no reloc site during relocation"
    | Some rs -> rs
    )) in
    let offset = (Ml_bindings.nat_big_num_of_uint64 reloc_site1.ref_relent.elf64_ra_offset) in Nat_big_num.sub_nat
    site_addr offset)

(** [amd64_reloc r] yields a function that applies relocations of type [r]. *)
(*val amd64_reloc : reloc_fn any_abi_feature*)
let amd64_reloc r:bool*((any_abi_feature)annotated_memory_image ->Nat_big_num.num ->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))=
     (
    (* See AMD64 ABI Draft 0.99.7 Table 4.10 (page 71) *)(match (string_of_amd64_relocation_type r) with
    | "R_X86_64_NONE" ->            (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 0), (fun s -> fun a -> fun e -> failwith "amd64_reloc: tried to apply a R_X86_64_NONE relocation"))))))
    | "R_X86_64_64" ->              (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> i2n ( Nat_big_num.add(n2i s) a)))))))
    | "R_X86_64_PC32" ->            (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n_signed 32 ( Nat_big_num.sub( Nat_big_num.add(n2i s) a) (n2i site_addr))))))))
    | "R_X86_64_GOT32" ->           (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n_signed 32 ( Nat_big_num.add(n2i (amd64_got_slot_idx img2 rr)) a)))))))
    | "R_X86_64_PLT32" ->           (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n_signed 32 ( Nat_big_num.sub (Nat_big_num.add(n2i (amd64_plt_slot_addr img2 rr s)) a) (n2i site_addr))) )))) )
    | "R_X86_64_COPY" ->            (false, (fun img2 -> (fun site_addr -> (fun rr -> (size_of_copy_reloc img2 rr, (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_COPY") (* FIXME *))))))
    | "R_X86_64_GLOB_DAT" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> s))))))
    | "R_X86_64_JUMP_SLOT" ->       (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> s))))))
    | "R_X86_64_RELATIVE" ->        (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> i2n ( Nat_big_num.add(n2i (amd64_base_addr rr site_addr)) a)))))))
    | "R_X86_64_GOTPCREL" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n_signed 32 ( Nat_big_num.sub (Nat_big_num.add(n2i (amd64_got_slot_addr img2 rr)) a) (n2i site_addr))) )))) )
    | "R_X86_64_32" ->              (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n ( Nat_big_num.add(n2i s) a)))))))
    | "R_X86_64_32S" ->             (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n_signed 32 ( Nat_big_num.add(n2i s) a)))))))
    | "R_X86_64_16" ->              (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 2), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_16") (* FIXME *))))))
    | "R_X86_64_PC16" ->            (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 2), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_PC16") (* FIXME *))))))
    | "R_X86_64_8" ->               (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 1), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_8") (* FIXME *))))))
    | "R_X86_64_PC8" ->             (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 1), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_PC8") (* FIXME *))))))
    | "R_X86_64_DTPMOD64" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_DTPMOD64") (* FIXME *))))))
    | "R_X86_64_DTPOFF64" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_DTPOFF64") (* FIXME *))))))
    | "R_X86_64_TPOFF64" ->         (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> i2n_signed 64 (Nat_big_num.sub( (Nat_big_num.of_int 0))( (Nat_big_num.of_int 8))))  (* FIXME *))))))
    | "R_X86_64_TLSGD" ->           (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_TLSGD") (* FIXME *))))))
    | "R_X86_64_TLSLD" ->           (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_TLSLD") (* FIXME *))))))
    | "R_X86_64_DTPOFF32" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_DTPOFF32") (* FIXME *))))))
    | "R_X86_64_GOTTPOFF" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> i2n_signed 32 ( Nat_big_num.sub (Nat_big_num.add(n2i (amd64_got_slot_addr img2 rr)) a) (n2i site_addr))))))))
    | "R_X86_64_TPOFF32" ->         (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_TPOFF32") (* FIXME *))))))
    | "R_X86_64_PC64" ->            (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_PC64") (* FIXME *))))))
    | "R_X86_64_GOTOFF64" ->        (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_GOTOFF64") (* FIXME *))))))
    | "R_X86_64_GOTPC32" ->         (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_GOTPC32") (* FIXME *))))))
    | "R_X86_64_SIZE32" ->          (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_SIZE32") (* FIXME *))))))
    | "R_X86_64_SIZE64" ->          (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_SIZE64") (* FIXME *))))))
    | "R_X86_64_GOTPC32_TLSDESC" -> (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 4), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_GOTPC32_TLSDESC") (* FIXME *))))))
    | "R_X86_64_TLSDESC_CALL" ->    (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 0) (* FIXME *), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_TLSDESC_CALL") (* FIXME *))))))
    | "R_X86_64_TLSDESC" ->         (false, (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 16), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_TLSDESC") (* FIXME *))))))
    | "R_X86_64_IRELATIVE" ->       (true,  (fun img2 -> (fun site_addr -> (fun rr -> ( (Nat_big_num.of_int 8), (fun s -> fun a -> fun e -> failwith "amd64_reloc: unimplemented R_X86_64_IRELATIVE") (* FIXME *))))))
    | _ -> failwith ("unrecognised relocation " ^ (string_of_amd64_relocation_type r))
    ))

(*val sysv_amd64_std_abi : abi any_abi_feature*)
let sysv_amd64_std_abi:(any_abi_feature)abi=
    ({ is_valid_elf_header = header_is_amd64
    ; make_elf_header = (make_elf64_header elf_data_2lsb elf_osabi_none( (Nat_big_num.of_int 0)) elf_ma_x86_64)
    ; reloc = amd64_reloc
    ; section_is_special = section_is_special2
    ; section_is_large = (fun s -> (fun f -> flag_is_set shf_x86_64_large s.elf64_section_flags))
    ; maxpagesize =( (Nat_big_num.of_int 65536))
    ; minpagesize =( (Nat_big_num.of_int 4096))
    ; commonpagesize =( (Nat_big_num.of_int 4096))
      (* XXX: DPM, changed from explicit reference to null_abi field due to problems in HOL4. *)
    ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_")
    ; make_phdrs = make_default_phdrs
    ; max_phnum =( (Nat_big_num.of_int 2)) (* incremented by extensions *)
    ; guess_entry_point = 
  (find_start_symbol_address
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; pad_data = pad_zeroes
    ; pad_code = pad_0x90
    ; generate_support = amd64_generate_support
    ; concretise_support = amd64_concretise_support
    ; get_reloc_symaddr = amd64_get_reloc_symaddr
    ; parse_reloc_info = parse_elf64_relocation_info
    })

(*val sysv_aarch64_le_std_abi : abi any_abi_feature*)
let sysv_aarch64_le_std_abi:(any_abi_feature)abi=
    ({ is_valid_elf_header = header_is_aarch64_le
    ; make_elf_header = (make_elf64_header elf_data_2lsb elf_osabi_none( (Nat_big_num.of_int 0)) elf_ma_aarch64)
    ; reloc = aarch64_le_reloc
    ; section_is_special = section_is_special2
    ; section_is_large = (fun _ -> (fun _ -> false))
    ; maxpagesize = (Nat_big_num.mul (Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 256)))( (Nat_big_num.of_int 4096))) (* 2MB; bit of a guess, based on gdb and prelink code *)
    ; minpagesize =( (Nat_big_num.of_int 1024)) (* bit of a guess again *)
    ; commonpagesize =( (Nat_big_num.of_int 4096))
    ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_")
    ; make_phdrs = make_default_phdrs
    ; max_phnum =( (Nat_big_num.of_int 2)) (* incremented by extensions *)
    ; guess_entry_point = 
  (find_start_symbol_address
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; pad_data = pad_zeroes
    ; pad_code = pad_zeroes
    ; generate_support = ( (* fun _ -> *)fun _ -> get_empty_memory_image ())
    ; concretise_support = (fun img2 -> img2)
    ; get_reloc_symaddr = 
  (default_get_reloc_symaddr
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; parse_reloc_info = parse_elf64_relocation_info
    })

(*val sysv_mips64_std_abi : abi any_abi_feature*)
let sysv_mips64_std_abi:(any_abi_feature)abi=  ({
      is_valid_elf_header = header_is_mips64
    ; make_elf_header = (make_elf64_header abi_mips64_data_encoding elf_osabi_none( (Nat_big_num.of_int 0)) elf_ma_mips)
    ; reloc = mips64_reloc
    ; section_is_special = elf_section_is_special
    ; section_is_large = (fun s -> (fun f -> false))
    ; maxpagesize = abi_mips64_page_size_max
    ; minpagesize = abi_mips64_page_size_min
    ; commonpagesize =( (Nat_big_num.of_int 4096))
    ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_")
    ; make_phdrs = make_default_phdrs
    ; max_phnum =( (Nat_big_num.of_int 2))
    ; guess_entry_point = 
  (find_start_symbol_address
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (* TODO: on MIPS it's __start, not _start *)
    ; pad_data = pad_zeroes
    ; pad_code = pad_zeroes
    ; generate_support = ( (* fun _ -> *)fun _ -> get_empty_memory_image ())
    ; concretise_support = (fun img2 -> img2)
    ; get_reloc_symaddr = 
  (default_get_reloc_symaddr
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; parse_reloc_info = abi_mips_parse_elf64_relocation_info
    })

(*val sysv_cheri_mips64_std_abi : abi any_abi_feature*)
let sysv_cheri_mips64_std_abi:(any_abi_feature)abi=  ({
      is_valid_elf_header = header_is_cheri_mips64
    ; make_elf_header = (make_elf64_header abi_cheri_mips64_data_encoding elf_osabi_none( (Nat_big_num.of_int 0)) elf_ma_mips)
    ; reloc = cheri_mips64_reloc
    ; section_is_special = elf_section_is_special
    ; section_is_large = (fun s -> (fun f -> false))
    ; maxpagesize = abi_cheri_mips64_page_size_max
    ; minpagesize = abi_cheri_mips64_page_size_min
    ; commonpagesize =( (Nat_big_num.of_int 4096))
    ; symbol_is_generated_by_linker = (fun symname -> symname = "_GLOBAL_OFFSET_TABLE_")
    ; make_phdrs = make_default_phdrs
    ; max_phnum =( (Nat_big_num.of_int 2))
    ; guess_entry_point = 
  (find_start_symbol_address
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (* TODO: on MIPS it's __start, not _start *)
    ; pad_data = pad_zeroes
    ; pad_code = pad_zeroes
    ; generate_support = ( (* fun _ -> *)fun _ -> get_empty_memory_image ())
    ; concretise_support = (fun img2 -> img2)
    ; get_reloc_symaddr = 
  (default_get_reloc_symaddr
     instance_Basic_classes_Ord_Abis_any_abi_feature_dict
     instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict)
    ; parse_reloc_info = parse_elf64_relocation_info
    })

(*val all_abis : list (abi any_abi_feature)*)
let all_abis:((any_abi_feature)abi)list=  ([
  sysv_amd64_std_abi;
  sysv_aarch64_le_std_abi;
  sysv_mips64_std_abi;
  sysv_cheri_mips64_std_abi;
  null_abi
])