Add ocaml run-time and updates to sail for ocaml backend

1 files changed, 568 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/linkable_list.ml b/lib/ocaml_rts/linksem/linkable_list.ml
new file mode 100644
index 00000000..c128563c
--- /dev/null
+++ b/lib/ocaml_rts/linksem/linkable_list.ml
@@ -0,0 +1,568 @@
+(*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.
+ *)