Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 568 deletions

diff --git a/lib/ocaml_rts/linksem/linkable_list.ml b/lib/ocaml_rts/linksem/linkable_list.ml
deleted file mode 100644
index c128563c..00000000
--- a/lib/ocaml_rts/linksem/linkable_list.ml
+++ /dev/null
@@ -1,568 +0,0 @@
-(*Generated by Lem from linkable_list.lem.*)
-open Lem_basic_classes
-open Lem_function
-open Lem_string
-open Lem_string_extra
-open Lem_tuple
-open Lem_bool
-open Lem_list
-open Lem_list_extra
-open Lem_set
-open Lem_set_extra
-(*import Map*)
-open Lem_sorting
-open Lem_num
-open Lem_maybe
-open Lem_assert_extra
-
-open Byte_sequence
-open Default_printing
-open Error
-open Missing_pervasives
-open Show
-
-open Elf_types_native_uint
-open Elf_memory_image
-open Elf_header
-open Elf_file
-open Memory_image
-open Elf_memory_image
-open Elf_section_header_table
-open Elf_symbol_table
-open String_table
-open Input_list
-
-open Elf_memory_image
-open Elf_memory_image_of_elf64_file
-
-type script = byte_sequence (* FIXME *)
-
-type linkable_object = RelocELF of elf_memory_image    (* memory image without address assignments *)
-                     | SharedELF of elf_memory_image   (* memory image with address assignments *)
-                     | ScriptAST of script       (* FIXME: should be elaborated away *)
-                     | ControlScriptDefs
-
-(*val string_of_linkable_object : linkable_object -> string*)
-let string_of_linkable_object l:string=  ((match l with
-    RelocELF(_)    -> "a relocatable file (...)"
-    | SharedELF(_) -> "a shared library (...)"
-    | ScriptAST(_) -> "a linker script (...)"
-    | ControlScriptDefs -> "the control script"
-))
-
-(* We keep the original input item around, hence the filename and byte sequence
- * and options. *)
-type linkable_item = linkable_object * input_item * input_options
-
-(*val short_string_of_linkable_item : linkable_item -> string*)
-let short_string_of_linkable_item item:string=    
-  (let (obj, inp, opts) = item
-    in
-    short_string_of_input_item inp)
-
-let instance_Show_Show_Linkable_list_linkable_object_dict:(linkable_object)show_class= ({
-
-  show_method = string_of_linkable_object})
-
-type linkable_list = linkable_item list
-
-type symbol_resolution_oracle = linkable_list -> int -> string -> int list
-type binding      = (Nat_big_num.num * symbol_reference * linkable_item) *  (Nat_big_num.num * symbol_definition * linkable_item)option
-type binding_list = binding list
-type binding_map  = (string, ( (Nat_big_num.num * binding)list)) Pmap.map
-
-
-let image_of_linkable_item item:(Abis.any_abi_feature)annotated_memory_image=  ((match item with
-    (RelocELF(image), _, _) -> image
-    | (SharedELF(image), _, _) -> image
-    | _ -> failwith "no image"
-))
-
-(*val linkable_item_of_input_item_and_options : forall 'abifeature. abi 'abifeature -> input_item -> input_options -> linkable_item*)
-let linkable_item_of_input_item_and_options a it opts:linkable_object*(string*input_blob*(Command_line.input_unit*(origin_coord)list))*input_options=    
-  ((match ((match it with
-        (fname1, Reloc(seq), origin) -> 
-            (*let _ = Missing_pervasives.errln ("Considering relocatable file " ^ fname) in*)
-            Elf_file.read_elf64_file seq >>= (fun e ->
-            return (RelocELF(elf_memory_image_of_elf64_file a fname1 e), it, opts))
-        | (fname1, Shared(seq), origin) -> 
-            (*let _ = Missing_pervasives.errln ("Skipping shared object " ^ fname) in *)
-            fail "unsupported input item"
-        | (fname1, Script(seq), origin) -> 
-            (*let _ = Missing_pervasives.errln ("Skipping linker script " ^ fname) in*)
-            fail "unsupported input item"
-        ))
-    with
-        Success(item) -> item
-        | Fail(str) -> failwith (str ^ ": non-ELF or non-relocatable input file")
-    ))
-
-(*val string_of_linkable : linkable_item -> string*)
-let string_of_linkable l:string=  ((match l with 
-    (_, item, _) -> string_of_triple 
-  instance_Show_Show_string_dict instance_Show_Show_Input_list_input_blob_dict (instance_Show_Show_tup2_dict
-   Command_line.instance_Show_Show_Command_line_input_unit_dict
-   (instance_Show_Show_list_dict
-      instance_Show_Show_Input_list_origin_coord_dict)) item
-))
-
-(* How do we signal "multiple definitions"? 
- * This is part of the policy baked into the particular oracle:
- * are multiple definitions okay, or do we fail?
- * 
- * NOTE that multiple definitions *globally* is not the same as 
- * multiple definitions as candidates for a given binding. We
- * can get the former even if we don't have the latter, in some
- * weird group/archive arrangements. The right place to detect
- * this condition is probably when generating the output symtab.
- *)
-
-(*val add_definition_to_map : (natural * symbol_definition * linkable_item) -> Map.map string (list (natural * symbol_definition * linkable_item))
-                    -> Map.map string (list (natural * symbol_definition * linkable_item))*)
-let add_definition_to_map def_idx_and_def_and_linkable m:((string),((Nat_big_num.num*symbol_definition*(linkable_object*input_item*input_options))list))Pmap.map=    
-  (let (def_idx, def, def_linkable) = def_idx_and_def_and_linkable
-    in
-    (match Pmap.lookup def.def_symname m with
-        Some curlist -> Pmap.add def.def_symname ((def_idx, def, def_linkable) :: curlist) m
-        | None -> Pmap.add def.def_symname [(def_idx, def, def_linkable)] m
-    ))
-
-(*val all_definitions_by_name : linkable_list -> Map.map string (list (natural * symbol_definition * linkable_item))*)
-let all_definitions_by_name linkables:((string),((Nat_big_num.num*symbol_definition*linkable_item)list))Pmap.map=    
-(  
-    (* Now that linkables are ELF memory images, we can make the 
-     * list of definitions much more easily. *)let list_of_deflists = (Lem_list.mapi (fun (idx1 : int) -> (fun (item : linkable_item) ->
-        let img2 = (image_of_linkable_item item)
-        in 
-        let (all_def_tags, all_def_ranges)
-         = (List.split (Multimap.lookupBy0 
-  (Memory_image_orderings.instance_Basic_classes_Ord_Memory_image_range_tag_dict
-     Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
-   (instance_Basic_classes_Ord_tup2_dict
-      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
-    Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (SymbolDef(null_symbol_definition)) img2.by_tag))
-        in
-        let all_defs = (Lem_list.map (fun tag -> (match tag with
-            SymbolDef(def) -> (def, item)
-            | _ -> failwith "matched tag not a symbol definition"
-        )) all_def_tags)
-        in
-        let x2 = ([]) in  List.fold_right
-   (fun(def, def_linkable) x2 ->
-    if true then (Nat_big_num.of_int idx1, def, def_linkable) :: x2 else x2)
-   all_defs x2
-    )) linkables)
-    in
-    List.fold_left (fun accum -> (fun deflist -> 
-        List.fold_left (fun m -> (fun (def_idx, def, def_linkable) -> add_definition_to_map (def_idx, def, def_linkable) m)) accum deflist
-    )) (Pmap.empty compare) list_of_deflists)
- 
-type binding_oracle = 
-    linkable_list 
-    -> (string, ( (Nat_big_num.num * symbol_definition * linkable_item)list)) Pmap.map
-    -> (Nat_big_num.num * symbol_reference * linkable_item)
-    ->  (Nat_big_num.num * symbol_definition * linkable_item)option
-
-(*val resolve_one_reference_default : forall 'abifeature. abi 'abifeature -> binding_oracle*)
-let resolve_one_reference_default a linkables defmap ref_idx_and_ref_and_linkable:(Nat_big_num.num*symbol_definition*(linkable_object*(string*input_blob*(Command_line.input_unit*(origin_coord)list))*input_options))option=    
- (let (ref_idx, ref1, ref_linkable) = ref_idx_and_ref_and_linkable
-    in
-    (* Get the list of all definitions whose name matches. 
-     * Don't match empty names. 
-     * How should we handle common symbols here?
-     * A common symbol is a potential definition, so it goes in the def list.
-     *)
-    let (defs_and_linkables_with_matching_name : (Nat_big_num.num * symbol_definition * linkable_item) list)
-     = ((match Pmap.lookup ref1.ref_symname defmap with
-        Some (l : ( (Nat_big_num.num * symbol_definition * linkable_item)list)) -> l
-        | None -> []
-    ))
-    in
-    (* Filter the list by eligibility rules. 
-     * Normally, 
-     * 
-     * - any .o file can supply any other .o file on the command line
-     * - any .a file supplies only files appearing to its left
-     *      i.e. "it is searched once for definitions"
-     * - does a .o file supply a .a file? to both its right and left? Experimentally, YES.
-     *
-     * So the restrictions are
-     * - archives may not supply weak references
-     * - archives may only supply to the left, or to themselves, or to objects in the same group
-     *)
-    let (ref_obj, (ref_fname, ref_blob, (ref_u, ref_coords)), ref_options) = ref_linkable
-    in
-    let ref_is_weak = (Nat_big_num.equal (get_elf64_symbol_binding ref1.ref_syment) stb_weak)
-    in
-    let def_is_eligible = (fun (def_idx, def, def_linkable) -> 
-        let ref_is_unnamed = (ref1.ref_symname = "")
-        in
-        let ref_is_to_defined_or_common_symbol = ( not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ref1.ref_syment.elf64_st_shndx)) stn_undef))
-        in
-        let def_sym_is_ref_sym = ( Nat_big_num.equal ref_idx def_idx && (Nat_big_num.equal ref1.ref_sym_scn def.def_sym_scn
-            && Nat_big_num.equal ref1.ref_sym_idx def.def_sym_idx))
-        in
-        let (def_obj, (def_fname, def_blob, def_origin), def_options) = def_linkable
-        in
-        let (def_u, def_coords) = def_origin
-        in
-        let (def_in_group, def_in_archive) = ((match def_coords with
-              InArchive(aid, aidx, _, _) :: InGroup(gid1, gidx) :: [_] -> (Some gid1, Some aid)
-            | InArchive(aid, aidx, _, _) :: [_]                       -> (None, Some aid)
-            | InGroup(gid1, gidx) :: [_]                              -> (Some gid1, None)
-            | [_]                                                    -> (None, None)
-            | _ -> failwith "internal error: didn't understand origin coordinates of definition"
-        ))
-        in
-        let ref_is_leftmore = (Nat_big_num.less_equal ref_idx def_idx)
-        in
-        (* For simplicity we include the case of "same archive" in "in group with". *)
-        let ref_is_in_group_with_def = ((match def_in_group with 
-              None -> false
-            | Some def_gid -> 
-                (match ref_coords with
-                  InArchive(_, _, _, _) :: InGroup(gid1, _) :: [_] -> Nat_big_num.equal gid1 def_gid
-                | InGroup(gid1, _) :: [_]                       -> Nat_big_num.equal gid1 def_gid
-                | _ -> false
-                )
-            ))
-        in
-        (* but maybe same archive? *)
-        (* DEBUGGING: print some stuff out if we care about this symbol. *)let _ =            
- (if (ref_fname = "backtrace.o") && (def.def_symname = "_Unwind_GetCFA") then 
-                (*Missing_pervasives.errln ("saw backtrace.o referencing _Unwind_GetCFA; coords are "
-                    ^ "def: " ^ (show def_coords) ^ ", ref: " ^ (show ref_coords) ^ "; ref_is_in_group_with_def: " 
-                    ^ (show ref_is_in_group_with_def) ^ "; def_in_group: " ^ (show def_in_group))*)
-              ()
-            else ())
-        in
-        let ref_and_def_are_in_same_archive = ((match (def_coords, ref_coords) with
-            (InArchive(x1, _, _, _) :: _, InArchive(x2, _, _, _) :: _) -> Nat_big_num.equal x1 x2
-            | _ -> false
-        ))
-        in
-        let def_is_in_archive = ((match def_in_archive with
-            Some _ -> true
-            | None -> false
-        ))
-        in
-        if ref_is_to_defined_or_common_symbol then def_sym_is_ref_sym
-        else 
-            if ref_is_unnamed then false
-            else
-                if def_is_in_archive
-                then
-                    (* Weak references *can* be resolved to archive members...
-                     * if the reference itself is also in the archive. *)
-                    ((not ref_is_weak) || ref_and_def_are_in_same_archive)
-                    && (
-                           ref_is_leftmore
-                        || (ref_and_def_are_in_same_archive
-                        || ref_is_in_group_with_def)
-                    )
-                else 
-                    true
-    )
-    in
-    let eligible_defs = (List.filter def_is_eligible defs_and_linkables_with_matching_name)
-    in
-    let (maybe_target_def_idx, maybe_target_def, maybe_target_def_linkable) = ((match eligible_defs with 
-        [] -> (None, None, None)
-        | [(def_idx, def, def_linkable)] -> (Some def_idx, Some def, Some def_linkable)
-        | (d_idx, d, d_l) :: more_pairs -> 
-            (* Break ties by
-             * - putting defs in relocs (or --defsym or linker script, a.k.a. command line) ahead of defs in archives;
-             * - else whichever definition appeared first in the left-to-right order. 
-             *)
-            let sorted = (insertSortBy (fun (d_idx1, d1, (_, (_, _, (_, d_l1_coords)), _)) -> (fun (d_idx2, d2, (_, (_, _, (_, d_l2_coords)), _)) -> 
-                (match (d_l1_coords, d_l2_coords) with
-                      (InCommandLine(_) :: _, InCommandLine(_) :: _) -> Nat_big_num.less d_idx1 d_idx2
-                    | (InCommandLine(_) :: _, _)                     -> (* command-line wins *) true
-                    | (_,                     InCommandLine(_) :: _) -> (* command-line wins *) false
-                    | (_, _) -> Nat_big_num.less d_idx1 d_idx2
-                ))) eligible_defs)
-            in
-            (match sorted with 
-                (first_d_idx, first_d, first_d_l) :: _ -> (Some first_d_idx, Some first_d, Some first_d_l)
-                | _ -> failwith "impossible: sorted list is shorter than original"
-            )
-    ))
-    in 
-    let refstr = ("`" 
-                ^ (ref1.ref_symname ^ ("' (" ^                
- ((if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ref1.ref_syment.elf64_st_shndx)) shn_undef then "UND" else "defined") ^                
- (" symbol at index " ^ ((Nat_big_num.to_string ref1.ref_sym_idx) ^ (" in symtab "
-                ^ ((Nat_big_num.to_string ref1.ref_sym_scn) ^ (" in " ^ (ref_fname
-                ^ ")"))))))))))
-    in
-    (*let _ = Missing_pervasives.errs ("Bound a reference from " ^ refstr ^ " to ")
-    in*)
-    (match (maybe_target_def_idx, maybe_target_def, maybe_target_def_linkable) with
-        (Some target_def_idx, Some target_def, Some target_def_linkable) ->
-            (*let _ = Missing_pervasives.errln (" a definition in "^ (show (target_def_linkable)))
-            in*)
-            Some(target_def_idx, target_def, target_def_linkable)
-    |  (None, None, None) -> 
-            (*let _ = Missing_pervasives.errln " no definition"
-            in*)
-            if ref_is_weak (* || a.symbol_is_generated_by_linker ref.ref_symname *) then None 
-            else (* failwith ("undefined symbol: " ^ refstr) *) None
-            (* FIXME: do a check, *after* the linker script has been interpreted, 
-             * that all remaining undefined symbols are permitted by the ABI/policy. *)
-    | _ -> failwith "impossible: non-matching maybes for target_def_idx and target_def"
-    ))
-
-(*val resolve_all :
-    linkable_list
-    -> Map.map string (list (natural * symbol_definition * linkable_item))                (* all definitions *)
-    -> binding_oracle
-    -> list (natural * symbol_reference * linkable_item)
-    -> list ((natural * symbol_reference * linkable_item) * maybe (natural * symbol_definition * linkable_item))*)
-let resolve_all linkables all_defs oracle refs:((Nat_big_num.num*symbol_reference*(linkable_object*input_item*input_options))*(Nat_big_num.num*symbol_definition*linkable_item)option)list=    
-  (Lem_list.map (fun (ref_idx, ref1, ref_linkable) -> ((ref_idx, ref1, ref_linkable), (oracle linkables all_defs (ref_idx, ref1, ref_linkable)))) refs)
-
-(* To accumulate which inputs are needed, we work with a list of undefineds, starting with those
- * in the  forced-output objects. We then iteratively build a list of all needed symbol definitions,
- * pulling in the objects that contain them, until we reach a fixed point. *)
-(*val resolve_undefs_in_one_object : 
-    linkable_list
-    -> Map.map string (list (natural * symbol_definition * linkable_item))                (* all definitions *)
-    -> binding_oracle
-    -> natural
-    -> list ((natural * symbol_reference * linkable_item) * maybe (natural * symbol_definition * linkable_item))*)
-let resolve_undefs_in_one_object linkables all_defs oracle idx1:((Nat_big_num.num*symbol_reference*linkable_item)*(Nat_big_num.num*symbol_definition*linkable_item)option)list=    
-( 
-    (* Get this object's list of references *)let item = ((match Lem_list.list_index linkables (Nat_big_num.to_int idx1) with
-        Some it -> it
-        | None -> failwith "impossible: linkable not in list of linkables"
-    ))
-    in
-    let img2 = (image_of_linkable_item item)
-    in 
-    let (all_ref_tags, all_ref_ranges)
-     = (List.split (Multimap.lookupBy0 
-  (Memory_image_orderings.instance_Basic_classes_Ord_Memory_image_range_tag_dict
-     Abis.instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict
-   (instance_Basic_classes_Ord_tup2_dict
-      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
-    Abis.instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (SymbolRef(null_symbol_reference_and_reloc_site)) img2.by_tag))
-    in
-    (* By using SymbolRef, we are extracting and binding each relocation site individually. 
-     * since there might be more than one relocation site referencing the same symbol name, 
-     * in a given object.
-     * 
-     * We are also binding SymbolRefs that have no relocation, which occur when there's
-     * an UND symbol which is not actually used by a relocation site, but is nevertheless 
-     * in need of being resolved.
-     * 
-     * We don't (for the moment) want to make different decisions for different reloc sites
-     * in the same object referencing the same symbol. So we dedup from a list to a set.
-     *)
-    let all_refs = (Pset.from_list compare (Lem_list.map (fun tag -> (match tag with
-        SymbolRef(r) -> r.ref
-        | _ -> failwith "matched tag not a relocation site"
-    )) all_ref_tags))
-    in
-    let ref_triples = (let x2 =(Pset.from_list (tripleCompare Nat_big_num.compare compare (tripleCompare compare (tripleCompare compare compare (pairCompare compare (lexicographic_compare compare))) compare)) 
-  []) in  Pset.fold
-   (fun ref1 x2 -> if true then Pset.add (idx1, ref1, item) x2 else x2)
-   all_refs x2)
-    in
-    (*let _ = Missing_pervasives.errln ("object " ^ (show item) ^ " has " ^ 
-        (show (Set.size ref_triples)) ^ " reloc references (symname, sym_scn, sym_idx, st_shndx) (" ^ 
-        (show (List.map (fun x -> ("\"" ^ x.ref_symname ^ "\"", x.ref_sym_scn, x.ref_sym_idx, natural_of_elf64_half x.ref_syment.elf64_st_shndx)) (Set_extra.toList all_refs))) ^ ")")
-    in*)
-    let und_ref_triples = (let x2 =(Pset.from_list (tripleCompare Nat_big_num.compare compare (tripleCompare compare (tripleCompare compare compare (pairCompare compare (lexicographic_compare compare))) compare)) 
-  []) in  Pset.fold
-   (fun(idx1, ref1, ref_item) x2 ->
-    if Nat_big_num.equal
-         (Nat_big_num.of_string
-            (Uint32.to_string ref1.ref_syment.elf64_st_shndx)) shn_undef then
-      Pset.add (idx1, ref1, ref_item) x2 else x2) ref_triples x2)
-    in
-    (*let _ = Missing_pervasives.errln ("... of which " ^
-        (show (Set.size und_ref_triples)) ^ " are to undefined symbols: (symname, sym_scn, sym_idx, st_shndx) (" ^ 
-        (show (List.map (fun (idx, x, _) -> ("\"" ^ x.ref_symname ^ "\"", x.ref_sym_scn, x.ref_sym_idx, natural_of_elf64_half x.ref_syment.elf64_st_shndx)) (Set_extra.toList und_ref_triples))) ^ ")")
-    in*)
-    resolve_all linkables all_defs oracle (Pset.elements ref_triples))
-
-(*val accumulate_bindings_bf : forall 'abifeature.
-    abi 'abifeature
-    -> linkable_list
-    -> Map.map string (list (natural * symbol_definition * linkable_item))                (* all definitions *)
-    -> set natural                                        (* inputs fully-bound so far *)
-    -> list natural                                       (* ordered list of inputs to bind next *)
-    -> list ((natural * symbol_reference * linkable_item) * maybe (natural * symbol_definition * linkable_item))  (* bindings made so far *)
-    -> list ((natural * symbol_reference * linkable_item) * maybe (natural * symbol_definition * linkable_item))*)  (* all accumulated bindings bindings *)
-let rec accumulate_bindings_bf a linkables all_defs fully_bound to_bind bindings_accum:((Nat_big_num.num*symbol_reference*linkable_item)*(Nat_big_num.num*symbol_definition*linkable_item)option)list=    
-( 
-    (* This is like foldl, except that each stage
-     * can add stuff to the work list *)(match to_bind with 
-        [] -> bindings_accum (* termination *)
-        | l_idx :: more_idx ->
-            (* Get the new bindings for this object *)
-            let new_bindings = (resolve_undefs_in_one_object
-                linkables
-                all_defs
-                (resolve_one_reference_default a)
-                l_idx)
-            in
-            let new_fully_bound = (Pset.add l_idx fully_bound)
-            in
-            (* Which of the new bindings are to objects 
-             * not yet fully bound or not yet in the to-bind list? *)
-            let new_bindings_def_idx = (list_concat_map (fun (ref1, maybe_def_and_idx_and_linkable) -> 
-                (match maybe_def_and_idx_and_linkable with 
-                    Some (def_idx, def, def_linkable) -> [def_idx]
-                    | None -> []
-                )
-            ) new_bindings) 
-            in
-            let new_bindings_def_idx_set = (Pset.from_list Nat_big_num.compare new_bindings_def_idx)
-            in
-            let included_linkables_idx =  (Pset.(union) fully_bound ((Pset.from_list Nat_big_num.compare to_bind)))
-            in
-            let new_l_idx = (Pset.diff new_bindings_def_idx_set included_linkables_idx)
-            in
-            let new_l_idx_list = (Pset.elements new_l_idx)
-            in
-            (*let _ = Missing_pervasives.errln (
-                if List.null new_l_idx_list 
-                then
-                    "Fully bound references in  " ^ (show (List.index linkables (natFromNatural l_idx)))
-                        ^ " using only already-included linkables (" 
-                        ^ (show (List.map (fun i -> List.index linkables (natFromNatural i)) (Set_extra.toList included_linkables_idx)))
-                else
-                    "Including additional linkables "
-                    ^ (show (List.mapMaybe (fun i -> List.index linkables (natFromNatural i)) new_l_idx_list))
-                    )
-            in*)
-            accumulate_bindings_bf
-                a
-                linkables
-                all_defs
-                new_fully_bound
-                ( List.rev_append (List.rev more_idx) new_l_idx_list)
-                ( List.rev_append (List.rev bindings_accum) new_bindings)
-    ))
-
-(* We need a generalised kind of depth-first search in which there are multiple start points. 
- * Also, we always work one object at a time, not one edge at a time; when we pull in an object,
- * we resolve *all* the references therein.
- *)
-(*val accumulate_bindings_objectwise_df : forall 'abifeature.
-    abi 'abifeature
-    -> linkable_list
-    -> Map.map string (list (natural * symbol_definition * linkable_item))                (* all definitions *)
-
-    -> list ((natural * symbol_reference * linkable_item) * maybe (natural * symbol_definition * linkable_item))  (* bindings made so far *)
-    -> set natural                                        (* inputs fully-bound so far -- these are "black" *)
-    -> list natural                                       (* inputs scheduled for binding -- these include 
-                                                             any "grey" (in-progress) nodes *and*
-                                                             any nodes that we have committed to exploring 
-                                                             (the "start nodes").
-                                                             Because we're depth-first, we prepend our adjacent
-                                                             nodes to this list, making them grey, then we 
-                                                             recurse by taking from the head. We must always
-                                                             filter out the prepended nodes from the existing list, 
-                                                             to ensure we don't recurse infinitely. *)
-    -> list ((natural * symbol_reference * linkable_item) * maybe (natural * symbol_definition * linkable_item))*)  (* all accumulated bindings bindings *)
-let rec accumulate_bindings_objectwise_df a linkables all_defs bindings_accum blacks greys:((Nat_big_num.num*symbol_reference*linkable_item)*(Nat_big_num.num*symbol_definition*linkable_item)option)list=    
- ((match greys with 
-        [] -> bindings_accum (* termination *)
-        | l_idx :: more_idx ->
-            (* Get the new bindings for this object *)
-            let new_bindings = (resolve_undefs_in_one_object
-                linkables
-                all_defs
-                (resolve_one_reference_default a)
-                l_idx)
-            in 
-            (* We pull in the whole object at a time ("objectwise"), so by definition,
-             * we have created bindings for everything in this object; it's now black. *)
-            let new_fully_bound = (Pset.add l_idx blacks)
-            in
-            (* Which of the new bindings are to objects 
-             * not yet fully bound or not yet in the to-bind list? *)
-            let new_bindings_def_idx = (list_concat_map (fun (ref1, maybe_def_and_idx_and_linkable) -> 
-                (match maybe_def_and_idx_and_linkable with 
-                    Some (def_idx, def, def_linkable) -> [def_idx]
-                    | None -> []
-                )
-            ) new_bindings) 
-            in
-            let new_bindings_def_idx_set = (Pset.from_list Nat_big_num.compare new_bindings_def_idx)
-            in
-            (* this is the "black or grey" set. *)
-            let included_linkables_idx =  (Pset.(union) blacks ((Pset.from_list Nat_big_num.compare greys)))
-            in
-            (* these are the white ones that we're adjacent to *)
-            let new_l_idx = (Pset.diff new_bindings_def_idx_set included_linkables_idx)
-            in
-            let new_l_idx_list = (Pset.elements new_l_idx)
-            in
-            (* What is the new grey-alike list? (This is the list we tail-recurse down.)
-             * It's
-             * - the existing grey-alike list
-             * - with any new (were-white) objects prepended
-             * - ... and filtered to *remove* these from the existing list (avoid duplication).
-             *)
-            let new_grey_list =  (List.rev_append (List.rev new_l_idx_list) (List.filter (fun x -> not ( Pset.mem x new_l_idx)) more_idx))
-            in
-            (* whether or not we've not uncovered any new white nodes, we tail-recurse  *)
-            (*let _ = (if List.null new_l_idx_list then
-                Missing_pervasives.errln ("Fully bound references in  " ^ (show (List.index linkables (natFromNatural l_idx)))
-                    ^ " using only already-included linkables (" 
-                    ^ (show (List.map (fun i -> List.index linkables (natFromNatural i)) (Set_extra.toList included_linkables_idx)))
-                ) else Missing_pervasives.errln ("Including additional linkables "
-            ^ (show (List.mapMaybe (fun i -> List.index linkables (natFromNatural i)) new_l_idx_list))))
-            in*)
-            accumulate_bindings_objectwise_df
-                a
-                linkables
-                all_defs
-                ( List.rev_append (List.rev bindings_accum) new_bindings)
-                (new_fully_bound : Nat_big_num.num Pset.set)
-                (new_grey_list : Nat_big_num.num list)
-   ))
-
-(* Rather than recursively expanding the link by searching for definitions of undefs, 
- * the GNU linker works by recursing/looping along the list of *linkables*, testing whether
- * any of the defs satisfies a currently-undef'd thing. On adding a new undef'd thing, 
- * we re-search only from the current archive, not from the beginning (i.e. the 
- * "def_is_leftmore or def_in_same_archive" logic).
- *
- * Why is this not the same as depth-first? One example is if we pull in a new object
- * which happens to have two undefs: one satisfied by the *first* element in the current archive,
- * and one satisfied by the last. 
- * 
- * In the GNU algorithm, we'll pull in the first archive element immediately afterwards, because
- * we'll re-traverse the archive and find it's needed.
- * 
- * In the depth-first algorithm, it depends entirely on the ordering of the new bindings, i.e.
- * the symtab ordering of the two undefs. If the later-in-archive def was bound *first*, we'll
- * recurse down *that* object's dependencies first.
- * 
- * So if we sort the new grey list
- * so that bindings formed in order of *current archive def pos*,
- * will we get the same behaviour?
- * We can't really do this, because we have no "current archive".
- * 
- * Need to rewrite the algorithm to fold along the list of linkables.
- *)