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, 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. - *) |