diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/linkable_list.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/linkable_list.ml | 568 |
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. + *) |