Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 1005 deletions

diff --git a/lib/ocaml_rts/linksem/link.ml b/lib/ocaml_rts/linksem/link.ml
deleted file mode 100644
index 1265de61..00000000
--- a/lib/ocaml_rts/linksem/link.ml
+++ /dev/null
@@ -1,1005 +0,0 @@
-(*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    
- (Nat_big_num.of_string (Uint32.to_string 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 (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 (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 = (get_elf64_relocation_a_type rs.ref_relent) 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(Sequence([])), ((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 (field_is_absolute_addr, applyfn) = (a.reloc (get_elf64_relocation_a_type reloc_site1.ref_relent))
-        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 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 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 Nat_big_num.of_int  
-                                    (* Weak symbol. *)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 (Nat_big_num.of_string (Uint32.to_string 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 _ = errln "Warning: not tagging entry point in output image"
-            in*) 
-            output_image
-    ))