Source file link.ml

(*Generated by Lem from link.lem.*)
open Lem_basic_classes
open Lem_function
open Lem_string
open Lem_tuple
open Lem_bool
open Lem_list
open Lem_sorting
open Lem_map
open Lem_set
(*import Set_extra*)
open Lem_num
open Lem_maybe
open Lem_assert_extra
(*import Command_line*)
(*import Input_list*)

open Byte_sequence
open Default_printing
open Error
open Missing_pervasives
open Show
open Endianness

open Elf_header
open Elf_interpreted_section
open Elf_interpreted_segment
open Elf_section_header_table
open Elf_program_header_table
open Elf_symbol_table
open Elf_types_native_uint
open Elf_relocation

open Abis
open Abi_amd64_relocation (* HACK -- remove me *)

open Input_list
open Linkable_list
(*import Command_line*)

open Memory_image
open Memory_image_orderings
open Elf_memory_image
open Elf_memory_image_of_elf64_file
open Linker_script

let all_common_symbols img2:(symbol_definition)list=  (List.filter (fun def -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint def.def_syment.elf64_st_shndx) shn_common
) (elf_memory_image_defined_symbols img2))

(* Q. On what does the decision about a reloc depend? definitely on
 *
 *      -- command-line options applying to the referenc*ed* object;
 *           (CHECK: I'm inferring that -Bsymbolic, like -Bstatic, applies to the
 *                   *referenced* object, not the referring -- need experimental conf.)
 *            ACTUALLY, it seems to be global: if a definition goes in the library,
 *                   bind to it; doesn't matter where it comes from. So
 *
 *      -- command-line options applying to the output object / whole link (-Bsymbolic);
 *
 *      -- command-line options applying to the referencing object?
 *
 *      What decision can we make?
 *      Given a reloc, it might be
 *      - not bound (weak symbols) -- THIS MEANS it *is* bound but to the value 0!
 *      - bound to a definition
 *
 *      ... perhaps our distinction is between "firm binding or provisional binding"?
 *                                            "final binding or overridable binding"?
 *
 *      Can we also hit cases where the binding is final but can't be relocated til load time?
 *      YES, e.g. any final R_*_64_64 reference in a shared library's data segment.
 *      WHAT do we do in these cases? Apply what we can and generate a R_*_RELATIVE?
 *      Yes, that's where R_*_RELATIVE come from, since they don't appear in .o inputs.
 *)

(*val def_is_in_reloc : linkable_item -> bool*)
let def_is_in_reloc def_item:bool=  ((match def_item with
    (RelocELF(_), _, _) -> true
    | (ScriptAST(_), _, _) -> true
    | _ -> false
))

let retrieve_binding_for_ref dict_Basic_classes_Eq_b r r_linkable_idx item bindings_by_name:('b*symbol_reference*'d)*'c=
     (let maybe_found_bs = (Pmap.lookup r.ref.ref_symname bindings_by_name)
    in
    (match maybe_found_bs with
        None -> failwith ("impossible: list of bindings does not include symbol reference `" ^ (r.ref.ref_symname ^ "` (map empty)"))
            (* FIXME: could this actually be an "undefined symbol" link error perhaps? *)
        | Some bis_and_bs -> (match List.filter (fun (b_idx, ((b_ref_idx, b_ref, b_ref_item), b_maybe_def)) ->
            if  dict_Basic_classes_Eq_b.isEqual_method b_ref_idx r_linkable_idx && (b_ref = r.ref) then
            (*let _ = Missing_pervasives.errln ("saw ref from linkable idx " ^ (show r_linkable_idx)
                ^ ", ref sym scn " ^ (show r.ref.ref_sym_scn) ^ ", ref sym idx "^ (show r.ref.ref_sym_idx)
                ^ ", item " ^ (show item) ^ "; binding to " ^ (
                    match b_maybe_def with
                        Just (def_idx, def, def_item) -> "linkable idx " ^ (show def_idx) ^
                            ", def sym scn " ^ (show def.def_sym_scn) ^ ", def sym idx " ^
                            (show def.def_sym_idx)
                      | Nothing -> "no definition"
                    end
                )
            )
            in*) true
            else false) bis_and_bs with
                  [] -> failwith ("impossible: list of bindings does not include symbol reference `" ^ (r.ref.ref_symname ^ "` (filtered list empty)"))
                | [(bi, b)] -> b
                | _ ->  failwith ("impossible: list of bindings binds reference to symbol `"
                    ^ (r.ref.ref_symname ^ "' more than one way (filtered list has >1 element)"))
            )
    ))

type reloc_site_resolution = reloc_site * binding * reloc_decision


(*val mark_fate_of_relocs : natural -> abi any_abi_feature -> set Command_line.link_option ->
    binding_map -> linkable_item -> elf_memory_image -> ((list reloc_site_resolution) * elf_memory_image)*)
let mark_fate_of_relocs linkable_idx a options bindings_by_name item img2:(reloc_site*((Nat_big_num.num*symbol_reference*(linkable_object*input_item*input_options))*(Nat_big_num.num*symbol_definition*(linkable_object*input_item*input_options))option)*reloc_decision)list*(any_abi_feature)annotated_memory_image=
     (
    (* Our image already models relocation sites. For each relocation *record*,
     * we use our bindings to make a decision about whether to apply it or not.
     *
     * Q1. How do we get the .rela.dyn made? Synthesise a fake reloc section?
     * Or pass them through to the linker script separately?
     * AHA. Note that the script already has an entry for .rela.dyn.
     * And it matches the ordinary rel sections, e.g. .rela.text and so on.
     * So if "-q" is active, the applied relocs need to be injected back in *after* the script
     * has run.
     * So we need both to materialize some relocs into the script inputs, *and* save some for later.
     *
     * Can we just use memory image metadata as the "saved for later" case? YES, I think so.
     * What do we do with metadata that is now being materialized?
     * I think we should only remove the metadata when we apply the relocation.
     * Q. When do we do that?
     * A. *After* address assignment has happened, i.e. all sections are allocated.
     *)let building_executable = (Pset.mem (Command_line.OutputKind(Command_line.Executable)) options) in
    let building_shared_library = (Pset.mem (Command_line.OutputKind(Command_line.SharedLibrary)) options) in
    let bind_functions_early = (Pset.mem Command_line.BindFunctionsEarly options) in
    let bind_non_functions_early = (Pset.mem Command_line.BindNonFunctionsEarly options) in
    let (new_by_tag, rev_decisions) = (List.fold_left (fun (acc_by_tag, rev_acc_decisions) -> (fun (tag, maybe_range) ->
        let pass_through = (Pset.add (tag, maybe_range) acc_by_tag, rev_acc_decisions)
        in
        (match tag with
            SymbolRef(r) ->
                (match r.maybe_reloc with
                    Some reloc1 ->
                        (* decision: do we want to
                         *  - apply it?   if so, do we need a consequent relocation (e.g. R_*_RELATIVE) in the output?
                         *  - PICify it, but leave it interposable?
                         *  - is "PICified, non-interposable" a thing? I don't think so, because non-interposable bindings are
                                     either intra-object *or* necessarily need load-time relocation to account for load addresses.
                                     In fact ELF can't express "non-interposable inter-object bindings" because we can't name
                                     specific objects when binding symbols.
                         *  - leave it alone, i.e. "relocate at load time"?
                         *
                         * Some useful questions: is the binding final?
                         * The GNU linker *never* leaves text relocs alone when generating shared libs;
                         * it always PICifies them.
                         * It can leave them alone when generating executables, though.
                         * This is an approximation; load-time text relocation can make sense for shared libs.
                         *     (but it's dangerous because PC32 relocs might overflow)
                         *)
                        let (binding_is_final : Command_line.link_option Pset.set -> binding -> bool)
                         = (fun options -> (fun ((ref_idx, ref1, ref_item), maybe_def) ->
                            (match maybe_def with
                                (* Weak bindings to 0 are final (though libcrunch wishes they weren't!). *)
                                None -> true
                                | Some (def_idx, def, def_item) -> Nat_big_num.equal
                                    (
                                    (* Bindings to non-global symbols are final. *)get_elf64_symbol_binding def.def_syment) stb_local
                                    ||
                                    (
                                    (* Bindings to hidden- or protected- or internal-visibility globals
                                     *    are final. *)Pset.mem (get_symbol_visibility def.def_syment.elf64_st_info)(Pset.from_list Nat_big_num.compare [ stv_hidden; stv_protected; stv_internal ])
                                    ||
                                    (
                                    (* Bindings to global symbols are non-final
                                     *    *unless*
                                     *      1. the symbol definition is [going to end up] in the executable
                                     *      2. we're -Bsymbolic, outputting a shared object,
                                     *           and the symbol definition is [going to end up] within the same shared object
                                     *      3. we're -Bsymbolic-functions, outputting a shared object,
                                     *           and the symbol definition has STT_FUNC and is [going to end up] within the same shared object
                                     *
                                     * ... where "going to end up in an X" means "we're building an X and def is in a RelocELF rather than a SharedELF".
                                     *)
                                    (* 1. *)(building_executable && def_is_in_reloc def_item) ||
                                    (* 2 and 3. *)
                                    (building_shared_library && (def_is_in_reloc def_item &&
                                        (  ( Nat_big_num.equal(get_elf64_symbol_type def.def_syment) stt_func  && bind_functions_early)
                                        || ( not (Nat_big_num.equal (get_elf64_symbol_type def.def_syment) stt_func) && bind_non_functions_early)
                                        ))
                                    )))
                                    (* FIXME: does it matter if the binding is intra-object or inter-object?
                                     * We don't get inter-object bindings much to non-{default global}s. How much? *)
                            )))
                        in
                        let (reloc_is_absolute : reloc_site -> bool) = (fun rs ->
                            let (kind, _) = (a.parse_reloc_info rs.ref_relent.elf64_ra_info) in
                            let (is_abs, _) = (a.reloc kind) in
                            is_abs)
                        in
                        (* What's our decision for this reloc? leave, apply, MakePIC?
                         * In fact we return both a decision and a maybe-function to create
                         * the consequent reloc.
                         * In what circumstances do we leave the reloc? If we're making an executable
                               and the definition is not in a relocatable input file or archive or script.
                               Or if we're making a shared library and the reference is "from data".
                               What does "from data" mean? I think it means it's a PC-relative reloc.
                               If we compile our code to do movabs $addr, even from a *local* address,
                               it's not PIC because that address needs load-time fixup.
                               So actually it's "is absolute address" again.
                         *)
                        let b = (retrieve_binding_for_ref 
  instance_Basic_classes_Eq_Num_natural_dict r linkable_idx item bindings_by_name)
                        in
                        let ((ref_idx, _, ref_item), maybe_def) = b
                        in
                        let defined_in_shared_lib = ((match maybe_def with
                            Some (def_idx, def, def_item) -> not (def_is_in_reloc def_item)
                            | None -> false (* i.e. the "definition", 0, can be "linked in" *)
                        ))
                        in
                        let decide = (fun decision -> (
                            (*let _ = errln ("Decided to " ^ match decision with
                                LeaveReloc -> "leave"
                                | ApplyReloc -> "apply"
                            end ^ " relocation in linkable " ^ (show ref_item) ^ "'s image, bound to " ^
                            match maybe_def with
                                Just(def_idx, def, def_item) -> "a definition called `" ^ def.def_symname ^ "' in linkable " ^
                                    (show def_item)
                                | Nothing -> "no definition"
                            end
                            )
                            in*)
                            Pset.add (SymbolRef({
                                ref           = (r.ref)
                                ; maybe_reloc = (r.maybe_reloc)
                                ; maybe_def_bound_to = (Some (decision,
                                    (match maybe_def with
                                        Some(def_idx, def, def_item) ->
                                                Some { def_symname = (def.def_symname)
                                                      ; def_syment  = (def.def_syment)
                                                      ; def_sym_scn = (def.def_sym_scn)
                                                      ; def_sym_idx = (def.def_sym_idx)
                                                      ; def_linkable_idx = def_idx
                                                      }
                                        | None -> None
                                    )
                                    ))
                                }
                            ), maybe_range) acc_by_tag,
                            ((reloc1, b, decision) :: rev_acc_decisions)))
                        in
                        if (building_executable && defined_in_shared_lib)
                        || (building_shared_library && (reloc_is_absolute reloc1))
                        then decide LeaveReloc
                        else
                        (* In what circumstances do we apply the reloc? If it's a final binding. *)
                        if binding_is_final options b then decide ApplyReloc
                        (* In what circumstances do we MakePIC? If it's a non-absolute relocatable field
                         *     and we're building a shared library.
                         *
                         * PIC is a kind of "consequent relocation", so let's think through it.
                         * A call site that calls <printf>      will usually be non-final (overridable).
                         * Output needs to call   <printf@plt>. BUT the trick is as follows:
                         *        the reloc is swizzled so that it binds to the PLT slot <printf@plt>;
                         *        the PLT slot is locally generated, so no reloc is needed.
                         * So the point is that
                         *        a *non*-applied reloc
                         *        might still need "applying" after a fashion (swizzling).
                         * The initial reloc is removed! Since PLT means removing relocs from code
                         * and reproducing their effect using a PLT.
                         * That's why we need this special MakePIC behaviour.
                         * Actually, generalise to a ChangeRelocTo.
                         *
                         * What about data?
                         * Suppose I have a shared library containing a read-only pointer to <environ>.
                         * The binding is final because <environ> is defined in the executable, say.
                         * PIC doesn't handle this case -- we still need load-time relocation.
                         * It's PIC, not PID: data can't be made position-independent.
                         *
                         * So, at least for simple cases of PIC, we don't need consequent relocation if
                         * we don't apply the reloc. We'll be removing the reloc. But we *do* need to create
                         * extra stuff later (PLT, GOT).
                         *)
                        else if building_shared_library then decide (* MakePIC *) (ChangeRelocTo( (Nat_big_num.of_int 0), r.ref, reloc1)) (* FIXME *)
                        (* The above are non-exclusive and non-exhaustive. Often, more than one option is available,
                         * ABIs / practice makes an arbitrary choice. For example, final bindings
                         * within a library could be realised the PIC way, but aren't (it'd create a
                         * pointless indirection). *)
                        else failwith "didn't know what to do with relocation"
                    | None ->
                        (* symbol ref with no reloc *)
                        pass_through
                )
        |   _ -> pass_through
        )
    )) ((Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) []), []) (Pset.elements img2.by_tag))
    in
    (List.rev rev_decisions, { elements = (img2.elements)
      ; 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)
      }))

(*val strip_metadata_sections : list (reloc_site * binding * reloc_decision) -> abi any_abi_feature -> elf_memory_image -> elf_memory_image*)
let strip_metadata_sections reloc_decisions a img2:(any_abi_feature)annotated_memory_image=
     (let (section_tags, section_ranges) = (elf_memory_image_section_ranges img2)
    in
    let rel_sections = (Lem_list.mapMaybe (fun (range_tag1, (el_name, el_range)) ->
        (match range_tag1 with
            FileFeature(ElfSection(idx1, isec1)) ->
                if Pset.mem isec1.elf64_section_type(Pset.from_list Nat_big_num.compare [ sht_rel; sht_rela ])
                then Some (idx1, isec1, el_name)
                else None
            | _ -> None
        )
    ) (list_combine section_tags section_ranges))
    in
    let discarded_sections_with_element_name = (Lem_list.mapMaybe (fun (range_tag1, (el_name, el_range)) ->
        (match range_tag1 with
            FileFeature(ElfSection(idx1, isec1)) ->
                if a.section_is_special isec1 img2 (* discard reloc sections, and we'll re-add them *)
                then Some (el_name, range_tag1) else None
        )
    ) (list_combine section_tags section_ranges))
    in
    let discarded_elements_map = (List.fold_left (fun m -> (fun (el_name, range_tag1) ->
        (*let _ = errln ("Discarding a metadata element named `" ^ el_name ^ "'") in*)
        Pmap.add el_name range_tag1 m
        )) (Pmap.empty compare) discarded_sections_with_element_name)
    in
    let filtered_image = (Memory_image.filter_elements (fun (el_name, el) -> not (Pmap.mem el_name discarded_elements_map)) img2)
    in
    let new_reloc_section_length = (fun idx1 -> (fun isec1 ->
        let retained_relocs_from_this_section = (let x2 = 
  ([]) in  List.fold_right
   (fun(reloc1, b, decision) x2 ->
    if Nat_big_num.equal (* is it from this section? *) reloc1.ref_rel_scn
         idx1 (* are we retaining it? *) && (decision = LeaveReloc) then
      (reloc1, b, decision) :: x2 else x2) reloc_decisions x2)
        in Nat_big_num.mul (length retained_relocs_from_this_section) isec1.elf64_section_entsize
    ))
    in
    let (new_reloc_elements, new_reloc_tags_and_ranges) = (List.split (let x2 = 
  ([]) in  List.fold_right
   (fun(idx1, isec1, el_name) x2 ->
    if Nat_big_num.greater (new_reloc_section_length idx1 isec1)
         ( (Nat_big_num.of_int 0)) then
      (let new_len = (new_reloc_section_length idx1 isec1) in
       let new_el = ({ startpos = None ; length1 = (Some new_len); contents = 
                     ([]) }) in
       let new_isec = ({ elf64_section_name = (isec1.elf64_section_name)
                       ; elf64_section_type = (isec1.elf64_section_type)
                       ; elf64_section_flags = (isec1.elf64_section_flags)
                       ; elf64_section_addr =( (Nat_big_num.of_int 0)) (* should be 0 anyway *)
                       ; elf64_section_offset =( (Nat_big_num.of_int 0)) (* ignored *)
                       ; elf64_section_size = new_len
                       ; elf64_section_link = (isec1.elf64_section_link)
                       ; elf64_section_info = (isec1.elf64_section_info)
                       ; elf64_section_align = (isec1.elf64_section_align)
                       ; elf64_section_entsize = (isec1.elf64_section_entsize)
                       ; elf64_section_body = Byte_sequence.empty (* ignored *)
                       ; elf64_section_name_as_string = (isec1.elf64_section_name_as_string)
                       }) in
       let new_meta = (FileFeature (ElfSection (idx1, new_isec))) in
       ((el_name, new_el), (new_meta, Some
                                        (el_name, ( (Nat_big_num.of_int 0), new_len)))))
        :: x2 else x2) rel_sections x2))
    in
    let new_by_tag = (Pset.bigunion (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))))(Pset.from_list (Pset.compare_by (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))))) [ filtered_image.by_tag; (Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) new_reloc_tags_and_ranges) ]))
    in
    {
        elements = (List.fold_right Pmap.union [filtered_image.elements; Lem_map.fromList 
  (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) new_reloc_elements] (Pmap.empty compare))
     ;  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)
     })


let expand_sections_for_one_image a options bindings_by_name linkable_idx item strip_relocs:(reloc_site*binding*reloc_decision)list*(any_abi_feature)annotated_memory_image*(input_spec)list=
     ((match item with
    (RelocELF(img2), (fname1, blob, origin), input_opts) ->
        (*let _ = List.foldl (fun _ -> fun (isec, shndx) ->
            let _ = errln ("For file " ^ fname ^ " before stripping, saw section idx " ^ (show shndx) ^
                " with name " ^ isec.elf64_section_name_as_string ^ ", first 20 bytes: " ^ (show (take 20 (
                    (let maybe_elname = elf_memory_image_element_coextensive_with_section shndx img
                     in
                     match maybe_elname with
                        Nothing -> failwith ("impossible: no such section (" ^ (show shndx) ^ ") in image of " ^ fname)
                        | Just idstr ->
                            match Map.lookup idstr img.elements with
                                Just el -> el.contents
                                | Nothing -> failwith "no such element"
                            end
                    end
                    )))))
                in
                ()
            ) () (elf_memory_image_sections_with_indices img)
        in*)
        let ((reloc_decisions : (reloc_site * binding * reloc_decision) list), marked_img) = (mark_fate_of_relocs linkable_idx a options bindings_by_name item img2)
        in
        (* Now we have a decision for each reloc: Leave, Apply, MakePIC. Which ones
         * do we materialize? Only the Leave ones, for now. To support -q we'll
         * have to support tweaking this.
         *
         * For each relocation that we Leave, we figure out its originating section
         * and re-create a lookalike in the memory image.
         *
         * We also get called for the "generated" memory image that contains .plt,
         * .rela.plt and so on. We don't strip these, since they actually contain relocs
         * that need to go directly into the output file. That's what the strip_relocs
         * argument is for. FIXME: refactor this into two functions.
         *)
        let stripped_img_with_reloc_sections = (if strip_relocs
            then (*let _ = errln ("Discarding metadata sections from image of `" ^ fname ^ "'") in*)
            strip_metadata_sections reloc_decisions a marked_img
            else marked_img)
        in
        (* Now we have a whole new image! It differs from the old one in that
         * - non-special sections have been stripped
         * - the relocs we want to participate in linking have been materialized.
         *)
        (* The "-q" option is tricky. It causes all incoming relocs to be retained, but
         * they *don't* participate in linking -- notice that the default linker script
         * pulls all .rela.* sections into .rela.dyn, whereas these ones *don't* go in there.
         * So FIXME: to support this, we need a way to re-add them, probably when we
         * generate meta-output like .symtab etc.. *)
        let inputs =
        
        (List.rev_append (List.rev (let x2 = 
  ([]) (* not (a.section_is_special isec img *)in  
  List.fold_right
    (fun(isec1, shndx1) x2 ->
     if true then
       (let short_name = (short_string_of_linkable_item item) in
        (*let _ = errln ("For file " ^ short_name ^ " after stripping, saw section idx " ^ (show shndx) ^
                " with name " ^ isec.elf64_section_name_as_string ^ ", first 20 bytes: " ^ (show (take 20 (
                    (let maybe_elname = elf_memory_image_element_coextensive_with_section shndx stripped_img_with_reloc_sections
                     in
                     match maybe_elname with
                        Nothing -> failwith ("impossible: no such section (matching " ^ (show shndx) ^ ")")
                        | Just idstr ->
                            match Map.lookup idstr stripped_img_with_reloc_sections.elements with
                                Just el -> el.contents
                                | Nothing -> failwith "no such element"
                            end
                    end
                    )))))
            in*)
        InputSection
            ({ idx = linkable_idx ; fname = short_name
             ; img = stripped_img_with_reloc_sections ; shndx = shndx1
             ; secname = (isec1.elf64_section_name_as_string) ; isec = isec1
             })) :: x2 else x2)
    (elf_memory_image_sections_with_indices stripped_img_with_reloc_sections)
    x2)) (
        (* One item per common symbol. FIXME: what about common symbols that have the same name?
         * We need to explicitly instantiate common symbols somewhere, probably here.
         * This means dropping any that are unreferenced (does it?) and merging any multiply-defined.
         * Actually, we deal with section merging at the same time as section concatenation, so during
         * linker script processing. For discarding unused common symbols, I *think* that this has already
         * been done by discarding unreferenced inputs.  *)
        let common_symbols = (all_common_symbols stripped_img_with_reloc_sections)
        in
        (*let _ = errln ("Expanding " ^ (show (length common_symbols)) ^ " common symbols")
        in*)
        let x2 = ([]) in  List.fold_right
   (fun def x2 ->
    if
    (*let _ = Missing_pervasives.outln ((space_padded_and_maybe_newline 20 def.def_symname)
                ^ (let hexstr = "0x" ^ (hex_string_of_natural (natural_of_elf64_xword def.def_syment.elf64_st_size))
                  in
                  space_padded_and_maybe_newline 20 hexstr
                  )
                ^
                fname)
            in*)
    true then
      Common (linkable_idx, fname1, stripped_img_with_reloc_sections, def) ::
        x2 else x2) common_symbols x2
        ))
        in (reloc_decisions, stripped_img_with_reloc_sections, inputs)
    | _ -> failwith "non-reloc linkable not supported yet"
))

type reloc_resolution = reloc_site * binding * reloc_decision

(*val default_merge_generated : abi any_abi_feature -> elf_memory_image -> list (list Linker_script.input_spec) -> list (list Linker_script.input_spec)*)
let default_merge_generated a generated_img input_spec_lists:((input_spec)list)list=
     (
    (* We expand the sections in the generated image and hang them off
     * the first linkable item. *)
    (*let _ = errln ("Generated image has " ^ (show (Map.size generated_img.elements)) ^ " elements and " ^ (show (Set.size (generated_img.by_tag))) ^
        " metadata elements (sanity: " ^ (show (Set.size (generated_img.by_range))) ^ ")")
    in*)let dummy_input_item = ("(no file)", Input_list.Reloc(Byte_sequence.empty), ((Command_line.File(Command_line.Filename("(no file)"), Command_line.null_input_file_options)), [InCommandLine( (Nat_big_num.of_int 0))]))
    in
    let dummy_linkable_item = (RelocELF(generated_img), dummy_input_item, Input_list.null_input_options)
    in
    let (_, _, generated_inputs) = (expand_sections_for_one_image a(Pset.from_list compare []) (Pmap.empty compare)( (Nat_big_num.of_int 0)) dummy_linkable_item false)
    in
    (*let _ = errln ("Generated image yielded " ^ (show (length generated_inputs)) ^ " input items")
    in*)
    (* okay, hang them off the first one *)
    (match input_spec_lists with
        [] -> failwith "link job empty"
        | first_input_list :: more_input_lists -> ( List.rev_append (List.rev first_input_list) generated_inputs) :: more_input_lists
    ))
    (* input_spec_lists *)

(*val expand_sections_for_all_inputs : abi any_abi_feature -> set Command_line.link_option -> binding_map ->
    (abi any_abi_feature -> elf_memory_image -> list (list Linker_script.input_spec) -> list (list Linker_script.input_spec)) (* merge_generated *) ->
    list (natural * Linkable_list.linkable_item) ->
    list (list reloc_resolution * elf_memory_image * list Linker_script.input_spec)*)
let expand_sections_for_all_inputs a options bindings_by_name merge_generated idx_and_linkables:((reloc_site*binding*reloc_decision)list*(any_abi_feature)annotated_memory_image*(input_spec)list)list=
     (let (expanded_reloc_lists, expanded_imgs, linker_script_input_lists) = (unzip3 (Lem_list.map (fun (idx1, linkable) ->
        expand_sections_for_one_image a options bindings_by_name idx1 linkable true) idx_and_linkables))
    in
    let fnames = (Lem_list.map (fun (idx1, (_, (fname1, _, _), _)) -> fname1) idx_and_linkables)
    in
    (* We pass the collection of linkable images and reloc decision lists
     * to an ABI tap function.
     *
     * This returns us a new *image* containing all the elements. Logically
     * this is another participant in the link, which we could expand separately.
     * A personality function takes care of actually merging it back into the
     * linker script inputs... in the case of the GNU linker, this means pretending
     * the generated stuff came from the first input object.
     *)
    let generated_img = (a.generate_support (* expanded_relocs *) (list_combine fnames expanded_imgs))
    in
    (* We need to return a
     *
     *    list (list reloc_decision * elf_memory_image * list Linker_script.input_spec)
     *
     * i.e. one item for every input image. *)
    let (final_input_spec_lists : ( Linker_script.input_spec list) list) = (merge_generated a generated_img linker_script_input_lists)
    in
    zip3 expanded_reloc_lists expanded_imgs final_input_spec_lists)

(*val relocate_output_image : abi any_abi_feature -> map string (list (natural * binding)) -> elf_memory_image -> elf_memory_image*)
let relocate_output_image a bindings_by_name img2:(any_abi_feature)annotated_memory_image=
     (let relocs = (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)
    in

    (*let _ = errln ("For __libc_multiple_threads (in relocate_output_image), we have " ^
        (let all_bs = match Map.lookup "__libc_multiple_threads" bindings_by_name with
            Just l -> l
            | Nothing -> []
        end
        in
        ((show (length all_bs)) ^
        " bindings, of which " ^
        (show (length (List.filter (fun (bi, ((ref_idx, ref, ref_item), maybe_def)) ->
            match maybe_def with
                Just _ -> true
                | _ -> false
            end
        ) all_bs))) ^ " have defs")))
    in*)
    let apply_reloc = (fun img2 -> fun (el_name, start, len) -> fun symref_and_reloc_site -> fun symaddr -> (
        let reloc_site1 = ((match symref_and_reloc_site.maybe_reloc with
            None -> failwith "impossible: no reloc site during relocation"
            | Some r -> r
        ))
        in
        let (rel_type1, _) = (a.parse_reloc_info reloc_site1.ref_relent.elf64_ra_info)
        in
        let (field_is_absolute_addr, applyfn) = (a.reloc rel_type1)
        in
        let element1 = ((match Pmap.lookup el_name img2.elements with
            None -> failwith "impossible: reloc site in nonexistent section"
            | Some e -> e
        ))
        in
        let site_address = ((match element1.startpos with
            Some addr -> Nat_big_num.add addr start
            | None -> failwith "error: relocation in section with no address"
        ))
        in
        let (width, calculate) = (applyfn img2 site_address symref_and_reloc_site)
        in
        let existing_field = (extract_natural_field width element1 start)
        in
        (*let _ = errln ("Existing field has value 0x" ^ (hex_string_of_natural existing_field))
        in*)
        (*let _ = errln ("Symaddr has value 0x" ^ (hex_string_of_natural symaddr))
        in*)
        let addend = (Nat_big_num.of_int64 reloc_site1.ref_relent.elf64_ra_addend)
        in
        let new_field_value = (calculate symaddr addend existing_field)
        in
        (*let _ = errln ("Calculated new field value 0x" ^ (hex_string_of_natural new_field_value))
        in*)
        let new_element = (write_natural_field new_field_value width element1 start)
        in
        {
            elements = (Pmap.add el_name new_element (Pmap.remove el_name img2.elements))
         ;  by_tag   = (Pset.diff img2.by_tag(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [(SymbolRef(symref_and_reloc_site), Some(el_name, (start, len)))]))
         ;  by_range = (Pset.diff img2.by_range(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [(Some(el_name, (start, len)), SymbolRef(symref_and_reloc_site))]))
         }
    ))
    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 img2)
    in
    let relocated_img = (List.fold_left (fun acc_img -> (fun (tag, maybe_range) ->
        (match tag with
            SymbolRef(x) -> (match x.maybe_reloc with
                Some rs ->
                    (match maybe_range with
                        None -> failwith "impossible: reloc site with no range"
                        | Some (el_name, (start, len)) ->
                            (*let _ = errln ("During relocation, saw a reloc site in element " ^ el_name ^ ", offset 0x" ^
                                (hex_string_of_natural start) ^ ", length 0x" ^ (hex_string_of_natural len) ^
                                ", reloc type " ^ (* a. *) Abi_amd64_relocation.string_of_amd64_relocation_type (get_elf64_relocation_a_type rs.ref_relent) ^
                                ", symbol name `" ^ x.ref.ref_symname ^ "'")
                            in*)
                            let symaddr = ((match x.maybe_def_bound_to with
                                Some(ApplyReloc, Some(bound_def)) ->
                                    (* Here we are mapping
                                     * *from* the definition found in an input object during resolution (bound_def)
                                     * *to* the corresponding symbol in the output image, now that we've built it.
                                     *
                                     * Q. What about ABI-specific interventions, e.g.
                                     * redirecting a symbol reference to its GOT or PLT slot?
                                     * A. Indeed, we need to ask the ABI to give us the target
                                     * address. The default implementation is just to look for
                                     * a matching symbol and use its address. But ABIs can do
                                     * wacky things if they like.
                                     *)
                                    a.get_reloc_symaddr bound_def img2 ranges_and_defs x.maybe_reloc
                                | None -> failwith "no def found for bound-to symbol"
                                | Some(ApplyReloc, None) ->
                                    (*let _ = errln "No definition, so we think this is a weak reference; giving it value 0."
                                    in*)
                                    (* CHECK: does the syment say it's weak? *)
                                    if not (Nat_big_num.equal (get_elf64_symbol_binding x.ref.ref_syment) stb_weak) then
                                        (*let _ = errln "Actually not weak! bailing"
                                        in*)
                                        failwith "not a weak reference, but no binding"
                                    else 
                                    (* Weak symbol. *) (Nat_big_num.of_int 0)
                                | Some(LeaveReloc, _) ->
                                    (* We shouldn't be seeing this, given that we're applying the reloc Right Now. *)
                                    failwith "internal error: applying reloc that is not to be applied"
                            ))
                            in
                            (*let _ = errln ("Got symaddr: 0x" ^ (hex_string_of_natural symaddr))
                            in*)
                            apply_reloc acc_img (el_name, start, len) x symaddr
                    )
                | None -> (* okay, do nothing *) acc_img
                )
            | _ -> failwith "impossible: not a symbol ref"
        )
    )) img2 relocs)
    in
    relocated_img)

(*val link : address_expr_fn_map allocated_sections_map -> linker_control_script -> abi any_abi_feature -> set Command_line.link_option -> linkable_list -> elf_memory_image*)
let link alloc_map script1 a options linkables:(any_abi_feature)annotated_memory_image=
     (let initial_included_indices = (mapMaybei (fun i -> (fun (obj, inp, (opts : input_options)) ->
        if opts.item_force_output
        then Some i
        else None
    )) linkables)
    in
    let linker_script_linkable_idx = (length linkables)
    in
    let defmap =  (all_definitions_by_name linkables)
    in
    let (accumulated_bindings : binding list)
     =
          ( (* accumulate_bindings_bf a linkables defmap {} initial_included_indices []  *)accumulate_bindings_objectwise_df a linkables defmap [](Pset.from_list Nat_big_num.compare []) initial_included_indices)
    in
    (* Keep a map whose keys are referenced objects, and whose values are
     * *some* (diagnostic purposes only) reference to that linkable. *)
    let referenced_object_indices_and_reasons = (List.fold_left (fun acc_m -> (fun ((ref_idx, ref_sym, ref_linkable), maybe_def_idx_and_sym_and_linkable) ->
        (match maybe_def_idx_and_sym_and_linkable with
            None -> acc_m
            | Some (def_idx, def_sym, def_linkable) ->
                (* Make sure the map contains this key. *)
                if (Lem.option_equal (Lem.pair_equal (=) 
  (tripleEqual instance_Basic_classes_Eq_var_dict
     (instance_Basic_classes_Eq_tup3_dict
        instance_Basic_classes_Eq_string_dict
        instance_Basic_classes_Eq_var_dict
        (instance_Basic_classes_Eq_tup2_dict
           instance_Basic_classes_Eq_var_dict
           (instance_Basic_classes_Eq_list_dict
              instance_Basic_classes_Eq_var_dict)))
     instance_Basic_classes_Eq_var_dict)) (Pmap.lookup def_idx acc_m) None)
                    then Pmap.add def_idx (ref_sym, ref_linkable) acc_m
                    else acc_m
        )
    )) ((Pmap.empty Nat_big_num.compare) : (Nat_big_num.num, (symbol_reference * linkable_item)) Pmap.map) accumulated_bindings)
    in
    (* Print something similar to GNU ld's linker map output, about included archive members. *)
    (*let _ = Missing_pervasives.outln "Archive member included to satisfy reference by file (symbol)\n" in*)
    let linkables_not_discarded = (mapMaybei (fun i -> (fun (obj, inp, opts) ->
        let referenced_object_map_entry = (Pmap.lookup i referenced_object_indices_and_reasons)
        in
        let referenced = ( not ((Lem.option_equal (Lem.pair_equal (=) 
  (tripleEqual instance_Basic_classes_Eq_var_dict
     (instance_Basic_classes_Eq_tup3_dict
        instance_Basic_classes_Eq_string_dict
        instance_Basic_classes_Eq_var_dict
        (instance_Basic_classes_Eq_tup2_dict
           instance_Basic_classes_Eq_var_dict
           (instance_Basic_classes_Eq_list_dict
              instance_Basic_classes_Eq_var_dict)))
     instance_Basic_classes_Eq_var_dict)) referenced_object_map_entry None)))
        in
        (* Print our link map thing *)
        (*let _ = (
            if (not referenced) then () else
                (* Did it come from an archive? *)
                let (name, _, (inp_unit, coordlist)) = inp in
                match coordlist with
                    InArchive(aid, aidx, aname, _) :: _ ->
                        (* yes, from an archive, so print a line *)
                        let (ref_sym, (ref_obj, (ref_name, ref_blob, ref_origin), ref_opts)) = match referenced_object_map_entry with
                            Just(x, y) -> (x, y)
                            | Nothing -> failwith "impossible: referenced item has no definition"
                        end
                        in
                        let lhs_name = aname ^ "(" ^ name ^ ")"
                        in
                        let lhs_name_len = stringLength lhs_name
                        in
                        let spacing = if lhs_name_len >= 29
                            then ("\n" ^ (makeString 30 #' '))
                            else makeString (30 - lhs_name_len) #' '
                        in
                        Missing_pervasives.outln (
                            lhs_name ^ spacing ^
                            (match ref_origin with
                                (_, InArchive(bid, bidx, bname, _) :: _) -> bname ^ "(" ^ ref_name ^ ")"
                                | _ -> ref_name
                            end)
                            ^ " (" ^ ref_sym.ref_symname ^ ")"
                        )
                    | _ (* not from an archive *) -> ()
                end
        )
        in*)
        if referenced || opts.item_force_output
        then Some (i, (obj, inp, opts))
        else None
    )) linkables)
    in
    (*let _ = Missing_pervasives.outln "\nAllocating common symbols\nCommon symbol       size              file\n"
    in*)
    (* We have to do a pass over relocations quite early. This is because relocs *do* participate
     * in linking. For each reloc, we need to decide whether to apply it or not. For those not applied,
     * we include it in a synthesised section that participates in linking.
     *
     * Similarly, the GOT needs to participate in linking, so that it gets assigned an address
     * at the appropriate place (as determined by the script). So we have to generate the GOT
     * *before* running the linker script. The GNU linker hangs the whole GOT and PLT content
     * off the first input object (usually crt1.o). In general, expand_sections calls an ABI tap
     * which synthesises all the necessary things, like (in the GNU case) the .got and .plt sections
     * hanging off the first input object. *)
    let (initial_bindings_by_name : (string, ( (Nat_big_num.num * binding)list)) Pmap.map) =
        (List.fold_left (fun m -> fun (b_idx, ((ref_idx, ref1, ref_item), maybe_def)) -> (match Pmap.lookup ref1.ref_symname m with
            None                  -> Pmap.add ref1.ref_symname [ (b_idx, ((ref_idx, ref1, ref_item), maybe_def)) ] m
            | Some ((bi, b) :: more) -> Pmap.add ref1.ref_symname  ((b_idx, ((ref_idx, ref1, ref_item), maybe_def)) :: ((bi, b) :: more)) m
            | _ -> failwith "impossible: found empty list in map lacking empties by construction"
        )) (Pmap.empty compare) (Lem_list.mapi (fun i -> fun b -> (Nat_big_num.of_int i, b)) accumulated_bindings))
    in
    let (expanded_triples : ( reloc_resolution list * elf_memory_image * Linker_script.input_spec list) list)
     = (expand_sections_for_all_inputs a options initial_bindings_by_name default_merge_generated linkables_not_discarded)
    in
    let (reloc_resolutions, imgs, input_lists) = (unzip3 expanded_triples)
    in
    let input_sections = (list_concat input_lists)
    in
    let seen_ordering = (fun is1 -> (fun is2 -> (
        let toNaturalList = (fun is -> (
            (* We're mapping the item to a list of naturals that determine a
             * lexicographic order. The list has a fixed depth:
             *
             * [within-commandline, within-group, within-archive, section-or-symbol]
             *
             * For .o files on the command line, we use the command line order. This
             * is the first level in the hierarchy.
             *
             * For .a files with --whole-archive, we want to do the same. Do this
             * by using archive position as the second level of the hierarchy, *if*
             * the item is marked as force_output.
             *
             * For other archives, "order seen" means something different: it's
             * the order in which they were "pulled in" during input enumeration. Another
             * way to say this is that they're ordered by the first binding that was
             * made to them. We map these to numbers starting from the size of the archive,
             * i.e. so that "force_output" makes an element appear sooner. In practice
             * we won't get a mixture of force_output and non- in the same archive,
             * so each archive will use only one of the two orderings.
             *
             * How do sections order relative to common symbols? Again, in practice it
             * doesn't matter because no input query will get a mixture of the two.
             * For symbols, we start the numbering from the number of sections in the file,
             * so symbols always appear later in the sortd order.
             *)
            let (linkable_idx, section_or_symbol_idx) = ((match is with
                Common(idx1, fname1, img2, def) -> (idx1, Nat_big_num.add
                    (let (_, l) = (elf_memory_image_section_ranges img2) in length l) def.def_sym_idx)
                | InputSection(isrec) -> (isrec.idx, isrec.shndx)
            ))
            in
            (match Lem_list.list_index linkables (Nat_big_num.to_int linkable_idx) with
                None -> failwith "impossible: linker input not in linkables list"
                | Some (obj, (fname1, blob, (inp_unit, coords)), options) ->
                    let (our_cid, our_gid, our_aid, maybe_archive_size) = ((match coords with
                      InArchive(aid, aidx, _, asize) :: InGroup(gid1, gidx) :: [InCommandLine(cid)] -> (cid, gid1, aid, Some asize)
                    | InArchive(aid, aidx, _, asize) :: [InCommandLine(cid)]                       -> (cid, (Nat_big_num.of_int 0), aid,   Some asize)
                    | InGroup(gid1, gidx) :: [InCommandLine(cid)]                                   -> (cid, gid1, (Nat_big_num.of_int 0),   None)
                    | [InCommandLine(cid)]                                                         -> (cid, (Nat_big_num.of_int 0), (Nat_big_num.of_int 0),     None)
                    | _ -> failwith "internal error: impossible coordinates"
                    ))
                    in
                    let aid_to_use = (if options.item_force_output then our_aid
                    else (* how many elements does the archive have? *)
                        let archive_size = ((match maybe_archive_size with
                            None -> failwith "impossible: archive with no size"
                            | Some a -> a
                        ))
                        in Nat_big_num.add archive_size
                        (* search the bindings: we want the index of the first binding
                           that refers to this object.
                         *)
                        (match Lem_list.find_index (fun ((b_ref_idx, b_ref, b_ref_item), b_maybe_def) -> (match b_maybe_def with
                            Some (b_def_idx, b_def, b_def_item) -> Nat_big_num.equal b_def_idx linkable_idx
                            | _ -> false
                        )) accumulated_bindings with
                            Some n -> Nat_big_num.of_int n
                            | None -> failwith "impossible: non-force-output object does not contain any bound-to defs"
                        ))
                    in
                    (* do we care about group idx? probably not. *)
                    [our_cid; aid_to_use; section_or_symbol_idx]
            )
        ))
        in
        (lexicographic_compare Nat_big_num.compare (toNaturalList is1) (toNaturalList is2))
    )))
    in
    (*
    let get_binding_for_ref = (fun symref -> (fun linkable_idx -> (fun fname ->
        let name_matches = match Map.lookup symref.ref_symname bindings_by_name with Just x -> x | Nothing -> [] end
        in
        match List.filter (fun (bi, ((r_idx, r, r_item), m_d)) -> r_idx = linkable_idx && r = symref) name_matches with
            [(b_idx, b)] -> (b_idx, b)
            | [] -> failwith "no binding found"
            | _  -> failwith ("ambiguous binding found for symbol `" ^ symref.ref_symname ^ "' in file " ^ fname)
        end
    )))
    in
    *)
    let (unrelocated_output_image_lacking_abs_symbols, bindings_by_name)
     = (interpret_linker_control_script alloc_map script1 linkables linker_script_linkable_idx a input_sections seen_ordering default_place_orphans initial_bindings_by_name)
    in
    (* also copy over ABS (range-less) symbols from all included input items *)
    let all_abs_range_tags_in_included_inputs = (List.concat (
        Lem_list.map (fun (img2, (idx1, linkable)) ->
          let abslist = (Lem_list.mapMaybe (fun (tag, maybeRange) ->
            (match tag with
                SymbolDef(ent) -> if (Lem.option_equal (Lem.pair_equal (=) (Lem.pair_equal Nat_big_num.equal Nat_big_num.equal)) maybeRange None) && Nat_big_num.equal (Uint32_wrapper.to_bigint ent.def_syment.elf64_st_shndx) shn_abs
                    then Some (maybeRange, ent)
                    else None
                | _ -> None
            )
          ) (tagged_ranges_matching_tag 
  instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict (SymbolDef(null_symbol_definition)) img2))
          in
          (*let _ = errln ("Copying " ^ (show (length abslist)) ^ " ABS symbols (names: " ^
            List.foldl (fun acc -> fun str -> if stringLength acc = 0 then str else acc ^ ", " ^ str) ""
                (List.map (fun (_, x) -> x.def_symname) abslist)
            ^ ") from not-discarded linkable item " ^
            (short_string_of_linkable_item linkable))
          in*)
          let x2 = ([]) in  List.fold_right
   (fun(maybe_range, ent) x2 ->
    if true then
      (maybe_range, SymbolDef
                        ({ def_symname = (ent.def_symname)
                         ; def_syment = (ent.def_syment)
                         ; def_sym_scn = (ent.def_sym_scn)
                         ; def_sym_idx = (ent.def_sym_idx)
                         ; def_linkable_idx = idx1 })) :: x2 else x2) 
 abslist x2
        ) (list_combine imgs linkables_not_discarded)
    ))
    in
    let by_range_including_abs_symbols =
        
        (Pset.(union) unrelocated_output_image_lacking_abs_symbols.by_range
        ((Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) all_abs_range_tags_in_included_inputs)))
    in
    let unrelocated_output_image = ({
        elements = (unrelocated_output_image_lacking_abs_symbols.elements)
    ;   by_range = by_range_including_abs_symbols
    ;   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 by_range_including_abs_symbols)
    })
    (* This image has
     * - addresses assigned
     * - relocations *not* applied
     * - no entry point
     * - some ABI features not generated? GOT, certainly. HMM.
           -- don't consider output features, like symtabs, yet;
           -- other ABI features have to be generated before the linker script runs (dyn relocs, GOT, PLT?)
           -- ... so we might be okay for now.
     *)
    in
    let remaining_relocs = (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))
        unrelocated_output_image.by_tag)
    in
    let _ = (List.fold_left (fun _ -> (fun (tag, maybe_range) ->
        let _ = ((match tag with
            SymbolRef(x) -> (match x.maybe_reloc with
                Some rs ->
                    (match maybe_range with
                        None -> failwith "impossible: reloc site with no range"
                        | Some (el_name, (start, len)) ->
                            () (* errln ("After linking, saw a reloc site in element " ^ el_name ^ ", offset 0x" ^
                                (hex_string_of_natural start) ^ ", length 0x" ^ (hex_string_of_natural len) ^
                                ", reloc type " ^ Abi_amd64_relocation.string_of_amd64_relocation_type (get_elf64_relocation_a_type rs.ref_relent)) *)
                    )
                | None -> (* okay, do nothing *) ()
                )
            | _ -> failwith "impossible: not a symbol ref"
        ))
        in
        ()
    )) () remaining_relocs)
    in
    (* Before we relocate, we concretise any ABI features that we've linked in. *)
    (*let _ = errln "Asking ABI to concretise support structures" in*)
    let unrelocated_concrete_output_image = (a.concretise_support unrelocated_output_image)
    in
    let output_image = (relocate_output_image a bindings_by_name unrelocated_concrete_output_image)
    in
    let (maybe_entry_point_address :  Nat_big_num.num option) =
        ((match Command_line.find_option_matching_tag (Command_line.EntryAddress( (Nat_big_num.of_int 0))) options with
            None -> a.guess_entry_point output_image
            | Some(Command_line.EntryAddress(x)) -> Some x
        ))
    in
    (match maybe_entry_point_address with
        Some addr ->
            (match address_to_element_and_offset addr output_image with
                Some (el_name, el_offset) ->
                    (*let _ = errln ("Tagging element " ^ el_name ^ " as containing entry point at offset 0x" ^ (hex_string_of_natural el_offset))
                    in*)
                    tag_image (EntryPoint) el_name el_offset( (Nat_big_num.of_int 0)) output_image
                | None ->
                    (* HMM. entry point symbol has no address at present. *)
                    failwith ("error: entry point address 0x" ^ ((hex_string_of_natural addr) ^ " does not correspond to any element position"))
            )
        | None ->
            let _ = (prerr_endline "Warning: not tagging entry point in output image")
            in
            output_image
    ))