diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/link.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/link.ml | 1005 |
1 files changed, 1005 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/link.ml b/lib/ocaml_rts/linksem/link.ml new file mode 100644 index 00000000..1265de61 --- /dev/null +++ b/lib/ocaml_rts/linksem/link.ml @@ -0,0 +1,1005 @@ +(*Generated by Lem from link.lem.*) +open Lem_basic_classes +open Lem_function +open Lem_string +open Lem_tuple +open Lem_bool +open Lem_list +open Lem_sorting +open Lem_map +open Lem_set +(*import Set_extra*) +open Lem_num +open Lem_maybe +open Lem_assert_extra +(*import Command_line*) +(*import Input_list*) + +open Byte_sequence +open Default_printing +open Error +open Missing_pervasives +open Show +open Endianness + +open Elf_header +open Elf_interpreted_section +open Elf_interpreted_segment +open Elf_section_header_table +open Elf_program_header_table +open Elf_symbol_table +open Elf_types_native_uint +open Elf_relocation + +open Abis +open Abi_amd64_relocation (* HACK -- remove me *) + +open Input_list +open Linkable_list +(*import Command_line*) + +open Memory_image +open Memory_image_orderings +open Elf_memory_image +open Elf_memory_image_of_elf64_file +open Linker_script + +let all_common_symbols img2:(symbol_definition)list= (List.filter (fun def -> Nat_big_num.equal + (Nat_big_num.of_string (Uint32.to_string def.def_syment.elf64_st_shndx)) shn_common +) (elf_memory_image_defined_symbols img2)) + +(* Q. On what does the decision about a reloc depend? definitely on + * + * -- command-line options applying to the referenc*ed* object; + * (CHECK: I'm inferring that -Bsymbolic, like -Bstatic, applies to the + * *referenced* object, not the referring -- need experimental conf.) + * ACTUALLY, it seems to be global: if a definition goes in the library, + * bind to it; doesn't matter where it comes from. So + * + * -- command-line options applying to the output object / whole link (-Bsymbolic); + * + * -- command-line options applying to the referencing object? + * + * What decision can we make? + * Given a reloc, it might be + * - not bound (weak symbols) -- THIS MEANS it *is* bound but to the value 0! + * - bound to a definition + * + * ... perhaps our distinction is between "firm binding or provisional binding"? + * "final binding or overridable binding"? + * + * Can we also hit cases where the binding is final but can't be relocated til load time? + * YES, e.g. any final R_*_64_64 reference in a shared library's data segment. + * WHAT do we do in these cases? Apply what we can and generate a R_*_RELATIVE? + * Yes, that's where R_*_RELATIVE come from, since they don't appear in .o inputs. + *) + +(*val def_is_in_reloc : linkable_item -> bool*) +let def_is_in_reloc def_item:bool= ((match def_item with + (RelocELF(_), _, _) -> true + | (ScriptAST(_), _, _) -> true + | _ -> false +)) + +let retrieve_binding_for_ref dict_Basic_classes_Eq_b r r_linkable_idx item bindings_by_name:('b*symbol_reference*'d)*'c= + (let maybe_found_bs = (Pmap.lookup r.ref.ref_symname bindings_by_name) + in + (match maybe_found_bs with + None -> failwith "impossible: list of bindings does not include symbol reference (map empty)" + (* FIXME: could this actually be an "undefined symbol" link error perhaps? *) + | Some bis_and_bs -> (match List.filter (fun (b_idx, ((b_ref_idx, b_ref, b_ref_item), b_maybe_def)) -> + if dict_Basic_classes_Eq_b.isEqual_method b_ref_idx r_linkable_idx && (b_ref = r.ref) then + (*let _ = Missing_pervasives.errln ("saw ref from linkable idx " ^ (show r_linkable_idx) + ^ ", ref sym scn " ^ (show r.ref.ref_sym_scn) ^ ", ref sym idx "^ (show r.ref.ref_sym_idx) + ^ ", item " ^ (show item) ^ "; binding to " ^ ( + match b_maybe_def with + Just (def_idx, def, def_item) -> "linkable idx " ^ (show def_idx) ^ + ", def sym scn " ^ (show def.def_sym_scn) ^ ", def sym idx " ^ + (show def.def_sym_idx) + | Nothing -> "no definition" + end + ) + ) + in*) true + else false) bis_and_bs with + [] -> failwith "impossible: list of bindings does not include symbol reference (filtered list empty)" + | [(bi, b)] -> b + | _ -> failwith ("impossible: list of bindings binds reference to symbol `" + ^ (r.ref.ref_symname ^ "' more than one way (filtered list has >1 element)")) + ) + )) + +type reloc_site_resolution = reloc_site * binding * reloc_decision + + +(*val mark_fate_of_relocs : natural -> abi any_abi_feature -> set Command_line.link_option -> + binding_map -> linkable_item -> elf_memory_image -> ((list reloc_site_resolution) * elf_memory_image)*) +let mark_fate_of_relocs linkable_idx a options bindings_by_name item img2:(reloc_site*((Nat_big_num.num*symbol_reference*(linkable_object*input_item*input_options))*(Nat_big_num.num*symbol_definition*(linkable_object*input_item*input_options))option)*reloc_decision)list*(any_abi_feature)annotated_memory_image= +( + (* Our image already models relocation sites. For each relocation *record*, + * we use our bindings to make a decision about whether to apply it or not. + * + * Q1. How do we get the .rela.dyn made? Synthesise a fake reloc section? + * Or pass them through to the linker script separately? + * AHA. Note that the script already has an entry for .rela.dyn. + * And it matches the ordinary rel sections, e.g. .rela.text and so on. + * So if "-q" is active, the applied relocs need to be injected back in *after* the script + * has run. + * So we need both to materialize some relocs into the script inputs, *and* save some for later. + * + * Can we just use memory image metadata as the "saved for later" case? YES, I think so. + * What do we do with metadata that is now being materialized? + * I think we should only remove the metadata when we apply the relocation. + * Q. When do we do that? + * A. *After* address assignment has happened, i.e. all sections are allocated. + *)let building_executable = (Pset.mem (Command_line.OutputKind(Command_line.Executable)) options) in + let building_shared_library = (Pset.mem (Command_line.OutputKind(Command_line.SharedLibrary)) options) in + let bind_functions_early = (Pset.mem Command_line.BindFunctionsEarly options) in + let bind_non_functions_early = (Pset.mem Command_line.BindNonFunctionsEarly options) in + let (new_by_tag, rev_decisions) = (List.fold_left (fun (acc_by_tag, rev_acc_decisions) -> (fun (tag, maybe_range) -> + let pass_through = (Pset.add (tag, maybe_range) acc_by_tag, rev_acc_decisions) + in + (match tag with + SymbolRef(r) -> + (match r.maybe_reloc with + Some reloc1 -> + (* decision: do we want to + * - apply it? if so, do we need a consequent relocation (e.g. R_*_RELATIVE) in the output? + * - PICify it, but leave it interposable? + * - is "PICified, non-interposable" a thing? I don't think so, because non-interposable bindings are + either intra-object *or* necessarily need load-time relocation to account for load addresses. + In fact ELF can't express "non-interposable inter-object bindings" because we can't name + specific objects when binding symbols. + * - leave it alone, i.e. "relocate at load time"? + * + * Some useful questions: is the binding final? + * The GNU linker *never* leaves text relocs alone when generating shared libs; + * it always PICifies them. + * It can leave them alone when generating executables, though. + * This is an approximation; load-time text relocation can make sense for shared libs. + * (but it's dangerous because PC32 relocs might overflow) + *) + let (binding_is_final : Command_line.link_option Pset.set -> binding -> bool) + = (fun options -> (fun ((ref_idx, ref1, ref_item), maybe_def) -> + (match maybe_def with + (* Weak bindings to 0 are final (though libcrunch wishes they weren't!). *) + None -> true + | Some (def_idx, def, def_item) -> Nat_big_num.equal +( + (* Bindings to non-global symbols are final. *)get_elf64_symbol_binding def.def_syment) stb_local + || +( + (* Bindings to hidden- or protected- or internal-visibility globals + * are final. *)Pset.mem (get_symbol_visibility def.def_syment.elf64_st_info)(Pset.from_list Nat_big_num.compare [ stv_hidden; stv_protected; stv_internal ]) + || +( + (* Bindings to global symbols are non-final + * *unless* + * 1. the symbol definition is [going to end up] in the executable + * 2. we're -Bsymbolic, outputting a shared object, + * and the symbol definition is [going to end up] within the same shared object + * 3. we're -Bsymbolic-functions, outputting a shared object, + * and the symbol definition has STT_FUNC and is [going to end up] within the same shared object + * + * ... where "going to end up in an X" means "we're building an X and def is in a RelocELF rather than a SharedELF". + *) + (* 1. *)(building_executable && def_is_in_reloc def_item) || + (* 2 and 3. *) + (building_shared_library && (def_is_in_reloc def_item && + ( ( Nat_big_num.equal(get_elf64_symbol_type def.def_syment) stt_func && bind_functions_early) + || ( not (Nat_big_num.equal (get_elf64_symbol_type def.def_syment) stt_func) && bind_non_functions_early) + )) + ))) + (* FIXME: does it matter if the binding is intra-object or inter-object? + * We don't get inter-object bindings much to non-{default global}s. How much? *) + ))) + in + let (reloc_is_absolute : reloc_site -> bool) = (fun rs -> + let kind = (get_elf64_relocation_a_type rs.ref_relent) in + let (is_abs, _) = (a.reloc kind) in + is_abs) + in + (* What's our decision for this reloc? leave, apply, MakePIC? + * In fact we return both a decision and a maybe-function to create + * the consequent reloc. + * In what circumstances do we leave the reloc? If we're making an executable + and the definition is not in a relocatable input file or archive or script. + Or if we're making a shared library and the reference is "from data". + What does "from data" mean? I think it means it's a PC-relative reloc. + If we compile our code to do movabs $addr, even from a *local* address, + it's not PIC because that address needs load-time fixup. + So actually it's "is absolute address" again. + *) + let b = (retrieve_binding_for_ref + instance_Basic_classes_Eq_Num_natural_dict r linkable_idx item bindings_by_name) + in + let ((ref_idx, _, ref_item), maybe_def) = b + in + let defined_in_shared_lib = ((match maybe_def with + Some (def_idx, def, def_item) -> not (def_is_in_reloc def_item) + | None -> false (* i.e. the "definition", 0, can be "linked in" *) + )) + in + let decide = (fun decision -> ( + (*let _ = errln ("Decided to " ^ match decision with + LeaveReloc -> "leave" + | ApplyReloc -> "apply" + end ^ " relocation in linkable " ^ (show ref_item) ^ "'s image, bound to " ^ + match maybe_def with + Just(def_idx, def, def_item) -> "a definition called `" ^ def.def_symname ^ "' in linkable " ^ + (show def_item) + | Nothing -> "no definition" + end + ) + in*) + Pset.add (SymbolRef({ + ref = (r.ref) + ; maybe_reloc = (r.maybe_reloc) + ; maybe_def_bound_to = (Some (decision, + (match maybe_def with + Some(def_idx, def, def_item) -> + Some { def_symname = (def.def_symname) + ; def_syment = (def.def_syment) + ; def_sym_scn = (def.def_sym_scn) + ; def_sym_idx = (def.def_sym_idx) + ; def_linkable_idx = def_idx + } + | None -> None + ) + )) + } + ), maybe_range) acc_by_tag, +((reloc1, b, decision) :: rev_acc_decisions))) + in + if (building_executable && defined_in_shared_lib) + || (building_shared_library && (reloc_is_absolute reloc1)) + then decide LeaveReloc + else + (* In what circumstances do we apply the reloc? If it's a final binding. *) + if binding_is_final options b then decide ApplyReloc + (* In what circumstances do we MakePIC? If it's a non-absolute relocatable field + * and we're building a shared library. + * + * PIC is a kind of "consequent relocation", so let's think through it. + * A call site that calls <printf> will usually be non-final (overridable). + * Output needs to call <printf@plt>. BUT the trick is as follows: + * the reloc is swizzled so that it binds to the PLT slot <printf@plt>; + * the PLT slot is locally generated, so no reloc is needed. + * So the point is that + * a *non*-applied reloc + * might still need "applying" after a fashion (swizzling). + * The initial reloc is removed! Since PLT means removing relocs from code + * and reproducing their effect using a PLT. + * That's why we need this special MakePIC behaviour. + * Actually, generalise to a ChangeRelocTo. + * + * What about data? + * Suppose I have a shared library containing a read-only pointer to <environ>. + * The binding is final because <environ> is defined in the executable, say. + * PIC doesn't handle this case -- we still need load-time relocation. + * It's PIC, not PID: data can't be made position-independent. + * + * So, at least for simple cases of PIC, we don't need consequent relocation if + * we don't apply the reloc. We'll be removing the reloc. But we *do* need to create + * extra stuff later (PLT, GOT). + *) + else if building_shared_library then decide (* MakePIC *) (ChangeRelocTo(Nat_big_num.of_int 0, r.ref, reloc1)) (* FIXME *) + (* The above are non-exclusive and non-exhaustive. Often, more than one option is available, + * ABIs / practice makes an arbitrary choice. For example, final bindings + * within a library could be realised the PIC way, but aren't (it'd create a + * pointless indirection). *) + else failwith "didn't know what to do with relocation" + | None -> + (* symbol ref with no reloc *) + pass_through + ) + | _ -> pass_through + ) + )) ((Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) []), []) (Pset.elements img2.by_tag)) + in + (List.rev rev_decisions, { elements = (img2.elements) + ; by_tag = new_by_tag + ; by_range = (by_range_from_by_tag + instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_var_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_Num_natural_dict + instance_Basic_classes_SetType_Num_natural_dict))) new_by_tag) + })) + +(*val strip_metadata_sections : list (reloc_site * binding * reloc_decision) -> abi any_abi_feature -> elf_memory_image -> elf_memory_image*) +let strip_metadata_sections reloc_decisions a img2:(any_abi_feature)annotated_memory_image= + (let (section_tags, section_ranges) = (elf_memory_image_section_ranges img2) + in + let rel_sections = (Lem_list.mapMaybe (fun (range_tag1, (el_name, el_range)) -> + (match range_tag1 with + FileFeature(ElfSection(idx1, isec1)) -> + if Pset.mem isec1.elf64_section_type(Pset.from_list Nat_big_num.compare [ sht_rel; sht_rela ]) + then Some (idx1, isec1, el_name) + else None + | _ -> None + ) + ) (list_combine section_tags section_ranges)) + in + let discarded_sections_with_element_name = (Lem_list.mapMaybe (fun (range_tag1, (el_name, el_range)) -> + (match range_tag1 with + FileFeature(ElfSection(idx1, isec1)) -> + if a.section_is_special isec1 img2 (* discard reloc sections, and we'll re-add them *) + then Some (el_name, range_tag1) else None + ) + ) (list_combine section_tags section_ranges)) + in + let discarded_elements_map = (List.fold_left (fun m -> (fun (el_name, range_tag1) -> + (*let _ = errln ("Discarding a metadata element named `" ^ el_name ^ "'") in*) + Pmap.add el_name range_tag1 m + )) (Pmap.empty compare) discarded_sections_with_element_name) + in + let filtered_image = (Memory_image.filter_elements (fun (el_name, el) -> not (Pmap.mem el_name discarded_elements_map)) img2) + in + let new_reloc_section_length = (fun idx1 -> (fun isec1 -> + let retained_relocs_from_this_section = (let x2 = + ([]) in List.fold_right + (fun(reloc1, b, decision) x2 -> + if Nat_big_num.equal (* is it from this section? *) reloc1.ref_rel_scn + idx1 (* are we retaining it? *) && (decision = LeaveReloc) then + (reloc1, b, decision) :: x2 else x2) reloc_decisions x2) + in Nat_big_num.mul (length retained_relocs_from_this_section) isec1.elf64_section_entsize + )) + in + let (new_reloc_elements, new_reloc_tags_and_ranges) = (List.split (let x2 = + ([]) in List.fold_right + (fun(idx1, isec1, el_name) x2 -> + if Nat_big_num.greater (new_reloc_section_length idx1 isec1) + (Nat_big_num.of_int 0) then + (let new_len = (new_reloc_section_length idx1 isec1) in + let new_el = ({ startpos = None ; length1 = (Some new_len); contents = + ([]) }) in + let new_isec = ({ elf64_section_name = (isec1.elf64_section_name) + ; elf64_section_type = (isec1.elf64_section_type) + ; elf64_section_flags = (isec1.elf64_section_flags) + ; elf64_section_addr =(Nat_big_num.of_int 0) (* should be 0 anyway *) + ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored *) + ; elf64_section_size = new_len + ; elf64_section_link = (isec1.elf64_section_link) + ; elf64_section_info = (isec1.elf64_section_info) + ; elf64_section_align = (isec1.elf64_section_align) + ; elf64_section_entsize = (isec1.elf64_section_entsize) + ; elf64_section_body = Byte_sequence.empty (* ignored *) + ; elf64_section_name_as_string = (isec1.elf64_section_name_as_string) + }) in + let new_meta = (FileFeature (ElfSection (idx1, new_isec))) in + ((el_name, new_el), (new_meta, Some + (el_name, (Nat_big_num.of_int 0, new_len))))) + :: x2 else x2) rel_sections x2)) + in + let new_by_tag = (Pset.bigunion (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))))(Pset.from_list (Pset.compare_by (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))))) [ filtered_image.by_tag; (Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) new_reloc_tags_and_ranges) ])) + in + { + elements = (List.fold_right Pmap.union [filtered_image.elements; Lem_map.fromList + (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) new_reloc_elements] (Pmap.empty compare)) + ; by_tag = new_by_tag + ; by_range = (by_range_from_by_tag + instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_var_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_Num_natural_dict + instance_Basic_classes_SetType_Num_natural_dict))) new_by_tag) + }) + + +let expand_sections_for_one_image a options bindings_by_name linkable_idx item strip_relocs:(reloc_site*binding*reloc_decision)list*(any_abi_feature)annotated_memory_image*(input_spec)list= + ((match item with + (RelocELF(img2), (fname1, blob, origin), input_opts) -> + (*let _ = List.foldl (fun _ -> fun (isec, shndx) -> + let _ = errln ("For file " ^ fname ^ " before stripping, saw section idx " ^ (show shndx) ^ + " with name " ^ isec.elf64_section_name_as_string ^ ", first 20 bytes: " ^ (show (take 20 ( + (let maybe_elname = elf_memory_image_element_coextensive_with_section shndx img + in + match maybe_elname with + Nothing -> failwith ("impossible: no such section (" ^ (show shndx) ^ ") in image of " ^ fname) + | Just idstr -> + match Map.lookup idstr img.elements with + Just el -> el.contents + | Nothing -> failwith "no such element" + end + end + ))))) + in + () + ) () (elf_memory_image_sections_with_indices img) + in*) + let ((reloc_decisions : (reloc_site * binding * reloc_decision) list), marked_img) = (mark_fate_of_relocs linkable_idx a options bindings_by_name item img2) + in + (* Now we have a decision for each reloc: Leave, Apply, MakePIC. Which ones + * do we materialize? Only the Leave ones, for now. To support -q we'll + * have to support tweaking this. + * + * For each relocation that we Leave, we figure out its originating section + * and re-create a lookalike in the memory image. + * + * We also get called for the "generated" memory image that contains .plt, + * .rela.plt and so on. We don't strip these, since they actually contain relocs + * that need to go directly into the output file. That's what the strip_relocs + * argument is for. FIXME: refactor this into two functions. + *) + let stripped_img_with_reloc_sections = (if strip_relocs + then (*let _ = errln ("Discarding metadata sections from image of `" ^ fname ^ "'") in*) + strip_metadata_sections reloc_decisions a marked_img + else marked_img) + in + (* Now we have a whole new image! It differs from the old one in that + * - non-special sections have been stripped + * - the relocs we want to participate in linking have been materialized. + *) + (* The "-q" option is tricky. It causes all incoming relocs to be retained, but + * they *don't* participate in linking -- notice that the default linker script + * pulls all .rela.* sections into .rela.dyn, whereas these ones *don't* go in there. + * So FIXME: to support this, we need a way to re-add them, probably when we + * generate meta-output like .symtab etc.. *) + let inputs = + + (List.rev_append (List.rev (let x2 = + ([]) (* not (a.section_is_special isec img *)in + List.fold_right + (fun(isec1, shndx1) x2 -> + if true then + (let short_name = (short_string_of_linkable_item item) in + (*let _ = errln ("For file " ^ short_name ^ " after stripping, saw section idx " ^ (show shndx) ^ + " with name " ^ isec.elf64_section_name_as_string ^ ", first 20 bytes: " ^ (show (take 20 ( + (let maybe_elname = elf_memory_image_element_coextensive_with_section shndx stripped_img_with_reloc_sections + in + match maybe_elname with + Nothing -> failwith ("impossible: no such section (matching " ^ (show shndx) ^ ")") + | Just idstr -> + match Map.lookup idstr stripped_img_with_reloc_sections.elements with + Just el -> el.contents + | Nothing -> failwith "no such element" + end + end + ))))) + in*) + InputSection + ({ idx = linkable_idx ; fname = short_name + ; img = stripped_img_with_reloc_sections ; shndx = shndx1 + ; secname = (isec1.elf64_section_name_as_string) ; isec = isec1 + })) :: x2 else x2) + (elf_memory_image_sections_with_indices stripped_img_with_reloc_sections) + x2)) ( + (* One item per common symbol. FIXME: what about common symbols that have the same name? + * We need to explicitly instantiate common symbols somewhere, probably here. + * This means dropping any that are unreferenced (does it?) and merging any multiply-defined. + * Actually, we deal with section merging at the same time as section concatenation, so during + * linker script processing. For discarding unused common symbols, I *think* that this has already + * been done by discarding unreferenced inputs. *) + let common_symbols = (all_common_symbols stripped_img_with_reloc_sections) + in + (*let _ = errln ("Expanding " ^ (show (length common_symbols)) ^ " common symbols") + in*) + let x2 = ([]) in List.fold_right + (fun def x2 -> + if + (*let _ = Missing_pervasives.outln ((space_padded_and_maybe_newline 20 def.def_symname) + ^ (let hexstr = "0x" ^ (hex_string_of_natural (natural_of_elf64_xword def.def_syment.elf64_st_size)) + in + space_padded_and_maybe_newline 20 hexstr + ) + ^ + fname) + in*) + true then + Common (linkable_idx, fname1, stripped_img_with_reloc_sections, def) :: + x2 else x2) common_symbols x2 + )) + in (reloc_decisions, stripped_img_with_reloc_sections, inputs) + | _ -> failwith "non-reloc linkable not supported yet" +)) + +type reloc_resolution = reloc_site * binding * reloc_decision + +(*val default_merge_generated : abi any_abi_feature -> elf_memory_image -> list (list Linker_script.input_spec) -> list (list Linker_script.input_spec)*) +let default_merge_generated a generated_img input_spec_lists:((input_spec)list)list= +( + (* We expand the sections in the generated image and hang them off + * the first linkable item. *) + (*let _ = errln ("Generated image has " ^ (show (Map.size generated_img.elements)) ^ " elements and " ^ (show (Set.size (generated_img.by_tag))) ^ + " metadata elements (sanity: " ^ (show (Set.size (generated_img.by_range))) ^ ")") + in*)let dummy_input_item = ("(no file)", Input_list.Reloc(Sequence([])), ((Command_line.File(Command_line.Filename("(no file)"), Command_line.null_input_file_options)), [InCommandLine(Nat_big_num.of_int 0)])) + in + let dummy_linkable_item = (RelocELF(generated_img), dummy_input_item, Input_list.null_input_options) + in + let (_, _, generated_inputs) = (expand_sections_for_one_image a(Pset.from_list compare []) (Pmap.empty compare)(Nat_big_num.of_int 0) dummy_linkable_item false) + in + (*let _ = errln ("Generated image yielded " ^ (show (length generated_inputs)) ^ " input items") + in*) + (* okay, hang them off the first one *) + (match input_spec_lists with + [] -> failwith "link job empty" + | first_input_list :: more_input_lists -> ( List.rev_append (List.rev first_input_list) generated_inputs) :: more_input_lists + )) + (* input_spec_lists *) + +(*val expand_sections_for_all_inputs : abi any_abi_feature -> set Command_line.link_option -> binding_map -> + (abi any_abi_feature -> elf_memory_image -> list (list Linker_script.input_spec) -> list (list Linker_script.input_spec)) (* merge_generated *) -> + list (natural * Linkable_list.linkable_item) -> + list (list reloc_resolution * elf_memory_image * list Linker_script.input_spec)*) +let expand_sections_for_all_inputs a options bindings_by_name merge_generated idx_and_linkables:((reloc_site*binding*reloc_decision)list*(any_abi_feature)annotated_memory_image*(input_spec)list)list= + (let (expanded_reloc_lists, expanded_imgs, linker_script_input_lists) = (unzip3 (Lem_list.map (fun (idx1, linkable) -> + expand_sections_for_one_image a options bindings_by_name idx1 linkable true) idx_and_linkables)) + in + let fnames = (Lem_list.map (fun (idx1, (_, (fname1, _, _), _)) -> fname1) idx_and_linkables) + in + (* We pass the collection of linkable images and reloc decision lists + * to an ABI tap function. + * + * This returns us a new *image* containing all the elements. Logically + * this is another participant in the link, which we could expand separately. + * A personality function takes care of actually merging it back into the + * linker script inputs... in the case of the GNU linker, this means pretending + * the generated stuff came from the first input object. + *) + let generated_img = (a.generate_support (* expanded_relocs *) (list_combine fnames expanded_imgs)) + in + (* We need to return a + * + * list (list reloc_decision * elf_memory_image * list Linker_script.input_spec) + * + * i.e. one item for every input image. *) + let (final_input_spec_lists : ( Linker_script.input_spec list) list) = (merge_generated a generated_img linker_script_input_lists) + in + zip3 expanded_reloc_lists expanded_imgs final_input_spec_lists) + +(*val relocate_output_image : abi any_abi_feature -> map string (list (natural * binding)) -> elf_memory_image -> elf_memory_image*) +let relocate_output_image a bindings_by_name img2:(any_abi_feature)annotated_memory_image= + (let relocs = (Multimap.lookupBy0 + (instance_Basic_classes_Ord_Memory_image_range_tag_dict + instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict + (instance_Basic_classes_Ord_tup2_dict + Lem_string_extra.instance_Basic_classes_Ord_string_dict + (instance_Basic_classes_Ord_tup2_dict + instance_Basic_classes_Ord_Num_natural_dict + instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_var_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_Num_natural_dict + instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv + instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (SymbolRef(null_symbol_reference_and_reloc_site)) + img2.by_tag) + in + + (*let _ = errln ("For __libc_multiple_threads (in relocate_output_image), we have " ^ + (let all_bs = match Map.lookup "__libc_multiple_threads" bindings_by_name with + Just l -> l + | Nothing -> [] + end + in + ((show (length all_bs)) ^ + " bindings, of which " ^ + (show (length (List.filter (fun (bi, ((ref_idx, ref, ref_item), maybe_def)) -> + match maybe_def with + Just _ -> true + | _ -> false + end + ) all_bs))) ^ " have defs"))) + in*) + let apply_reloc = (fun img2 -> fun (el_name, start, len) -> fun symref_and_reloc_site -> fun symaddr -> ( + let reloc_site1 = ((match symref_and_reloc_site.maybe_reloc with + None -> failwith "impossible: no reloc site during relocation" + | Some r -> r + )) + in + let (field_is_absolute_addr, applyfn) = (a.reloc (get_elf64_relocation_a_type reloc_site1.ref_relent)) + in + let element1 = ((match Pmap.lookup el_name img2.elements with + None -> failwith "impossible: reloc site in nonexistent section" + | Some e -> e + )) + in + let site_address = ((match element1.startpos with + Some addr -> Nat_big_num.add addr start + | None -> failwith "error: relocation in section with no address" + )) + in + let (width, calculate) = (applyfn img2 site_address symref_and_reloc_site) + in + let existing_field = (extract_natural_field width element1 start) + in + (*let _ = errln ("Existing field has value 0x" ^ (hex_string_of_natural existing_field)) + in*) + (*let _ = errln ("Symaddr has value 0x" ^ (hex_string_of_natural symaddr)) + in*) + let addend = (Nat_big_num.of_int64 reloc_site1.ref_relent.elf64_ra_addend) + in + let new_field_value = (calculate symaddr addend existing_field) + in + (*let _ = errln ("Calculated new field value 0x" ^ (hex_string_of_natural new_field_value)) + in*) + let new_element = (write_natural_field new_field_value width element1 start) + in + { + elements = (Pmap.add el_name new_element (Pmap.remove el_name img2.elements)) + ; by_tag = (Pset.diff img2.by_tag(Pset.from_list (pairCompare compare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare)))) [(SymbolRef(symref_and_reloc_site), Some(el_name, (start, len)))])) + ; by_range = (Pset.diff img2.by_range(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [(Some(el_name, (start, len)), SymbolRef(symref_and_reloc_site))])) + } + )) + in + let relocated_img = (List.fold_left (fun acc_img -> (fun (tag, maybe_range) -> + (match tag with + SymbolRef(x) -> (match x.maybe_reloc with + Some rs -> + (match maybe_range with + None -> failwith "impossible: reloc site with no range" + | Some (el_name, (start, len)) -> + (*let _ = errln ("During relocation, saw a reloc site in element " ^ el_name ^ ", offset 0x" ^ + (hex_string_of_natural start) ^ ", length 0x" ^ (hex_string_of_natural len) ^ + ", reloc type " ^ (* a. *) Abi_amd64_relocation.string_of_amd64_relocation_type (get_elf64_relocation_a_type rs.ref_relent) ^ + ", symbol name `" ^ x.ref.ref_symname ^ "'") + in*) + let symaddr = ((match x.maybe_def_bound_to with + Some(ApplyReloc, Some(bound_def)) -> + (* Here we are mapping + * *from* the definition found in an input object during resolution (bound_def) + * *to* the corresponding symbol in the output image, now that we've built it. + * + * Q. What about ABI-specific interventions, e.g. + * redirecting a symbol reference to its GOT or PLT slot? + * A. Indeed, we need to ask the ABI to give us the target + * address. The default implementation is just to look for + * a matching symbol and use its address. But ABIs can do + * wacky things if they like. + *) + a.get_reloc_symaddr bound_def img2 x.maybe_reloc + | None -> failwith "no def found for bound-to symbol" + | Some(ApplyReloc, None) -> + (*let _ = errln "No definition, so we think this is a weak reference; giving it value 0." + in*) + (* CHECK: does the syment say it's weak? *) + if not (Nat_big_num.equal (get_elf64_symbol_binding x.ref.ref_syment) stb_weak) then + (*let _ = errln "Actually not weak! bailing" + in*) + failwith "not a weak reference, but no binding" + else Nat_big_num.of_int + (* Weak symbol. *)0 + | Some(LeaveReloc, _) -> + (* We shouldn't be seeing this, given that we're applying the reloc Right Now. *) + failwith "internal error: applying reloc that is not to be applied" + )) + in + (*let _ = errln ("Got symaddr: 0x" ^ (hex_string_of_natural symaddr)) + in*) + apply_reloc acc_img (el_name, start, len) x symaddr + ) + | None -> (* okay, do nothing *) acc_img + ) + | _ -> failwith "impossible: not a symbol ref" + ) + )) img2 relocs) + in + relocated_img) + +(*val link : address_expr_fn_map allocated_sections_map -> linker_control_script -> abi any_abi_feature -> set Command_line.link_option -> linkable_list -> elf_memory_image*) +let link alloc_map script1 a options linkables:(any_abi_feature)annotated_memory_image= + (let initial_included_indices = (mapMaybei (fun i -> (fun (obj, inp, (opts : input_options)) -> + if opts.item_force_output + then Some i + else None + )) linkables) + in + let linker_script_linkable_idx = (length linkables) + in + let defmap = (all_definitions_by_name linkables) + in + let (accumulated_bindings : binding list) + = +( (* accumulate_bindings_bf a linkables defmap {} initial_included_indices [] *)accumulate_bindings_objectwise_df a linkables defmap [](Pset.from_list Nat_big_num.compare []) initial_included_indices) + in + (* Keep a map whose keys are referenced objects, and whose values are + * *some* (diagnostic purposes only) reference to that linkable. *) + let referenced_object_indices_and_reasons = (List.fold_left (fun acc_m -> (fun ((ref_idx, ref_sym, ref_linkable), maybe_def_idx_and_sym_and_linkable) -> + (match maybe_def_idx_and_sym_and_linkable with + None -> acc_m + | Some (def_idx, def_sym, def_linkable) -> + (* Make sure the map contains this key. *) + if (Lem.option_equal (Lem.pair_equal (=) + (tripleEqual instance_Basic_classes_Eq_var_dict + (instance_Basic_classes_Eq_tup3_dict + instance_Basic_classes_Eq_string_dict + instance_Basic_classes_Eq_var_dict + (instance_Basic_classes_Eq_tup2_dict + instance_Basic_classes_Eq_var_dict + (instance_Basic_classes_Eq_list_dict + instance_Basic_classes_Eq_var_dict))) + instance_Basic_classes_Eq_var_dict)) (Pmap.lookup def_idx acc_m) None) + then Pmap.add def_idx (ref_sym, ref_linkable) acc_m + else acc_m + ) + )) ((Pmap.empty Nat_big_num.compare) : (Nat_big_num.num, (symbol_reference * linkable_item)) Pmap.map) accumulated_bindings) + in + (* Print something similar to GNU ld's linker map output, about included archive members. *) + (*let _ = Missing_pervasives.outln "Archive member included to satisfy reference by file (symbol)\n" in*) + let linkables_not_discarded = (mapMaybei (fun i -> (fun (obj, inp, opts) -> + let referenced_object_map_entry = (Pmap.lookup i referenced_object_indices_and_reasons) + in + let referenced = ( not ((Lem.option_equal (Lem.pair_equal (=) + (tripleEqual instance_Basic_classes_Eq_var_dict + (instance_Basic_classes_Eq_tup3_dict + instance_Basic_classes_Eq_string_dict + instance_Basic_classes_Eq_var_dict + (instance_Basic_classes_Eq_tup2_dict + instance_Basic_classes_Eq_var_dict + (instance_Basic_classes_Eq_list_dict + instance_Basic_classes_Eq_var_dict))) + instance_Basic_classes_Eq_var_dict)) referenced_object_map_entry None))) + in + (* Print our link map thing *) + (*let _ = ( + if (not referenced) then () else + (* Did it come from an archive? *) + let (name, _, (inp_unit, coordlist)) = inp in + match coordlist with + InArchive(aid, aidx, aname, _) :: _ -> + (* yes, from an archive, so print a line *) + let (ref_sym, (ref_obj, (ref_name, ref_blob, ref_origin), ref_opts)) = match referenced_object_map_entry with + Just(x, y) -> (x, y) + | Nothing -> failwith "impossible: referenced item has no definition" + end + in + let lhs_name = aname ^ "(" ^ name ^ ")" + in + let lhs_name_len = stringLength lhs_name + in + let spacing = if lhs_name_len >= 29 + then ("\n" ^ (makeString 30 #' ')) + else makeString (30 - lhs_name_len) #' ' + in + Missing_pervasives.outln ( + lhs_name ^ spacing ^ + (match ref_origin with + (_, InArchive(bid, bidx, bname, _) :: _) -> bname ^ "(" ^ ref_name ^ ")" + | _ -> ref_name + end) + ^ " (" ^ ref_sym.ref_symname ^ ")" + ) + | _ (* not from an archive *) -> () + end + ) + in*) + if referenced || opts.item_force_output + then Some (i, (obj, inp, opts)) + else None + )) linkables) + in + (*let _ = Missing_pervasives.outln "\nAllocating common symbols\nCommon symbol size file\n" + in*) + (* We have to do a pass over relocations quite early. This is because relocs *do* participate + * in linking. For each reloc, we need to decide whether to apply it or not. For those not applied, + * we include it in a synthesised section that participates in linking. + * + * Similarly, the GOT needs to participate in linking, so that it gets assigned an address + * at the appropriate place (as determined by the script). So we have to generate the GOT + * *before* running the linker script. The GNU linker hangs the whole GOT and PLT content + * off the first input object (usually crt1.o). In general, expand_sections calls an ABI tap + * which synthesises all the necessary things, like (in the GNU case) the .got and .plt sections + * hanging off the first input object. *) + let (initial_bindings_by_name : (string, ( (Nat_big_num.num * binding)list)) Pmap.map) = + (List.fold_left (fun m -> fun (b_idx, ((ref_idx, ref1, ref_item), maybe_def)) -> (match Pmap.lookup ref1.ref_symname m with + None -> Pmap.add ref1.ref_symname [ (b_idx, ((ref_idx, ref1, ref_item), maybe_def)) ] m + | Some ((bi, b) :: more) -> Pmap.add ref1.ref_symname ((b_idx, ((ref_idx, ref1, ref_item), maybe_def)) :: ((bi, b) :: more)) m + | _ -> failwith "impossible: found empty list in map lacking empties by construction" + )) (Pmap.empty compare) (Lem_list.mapi (fun i -> fun b -> (Nat_big_num.of_int i, b)) accumulated_bindings)) + in + let (expanded_triples : ( reloc_resolution list * elf_memory_image * Linker_script.input_spec list) list) + = (expand_sections_for_all_inputs a options initial_bindings_by_name default_merge_generated linkables_not_discarded) + in + let (reloc_resolutions, imgs, input_lists) = (unzip3 expanded_triples) + in + let input_sections = (list_concat input_lists) + in + let seen_ordering = (fun is1 -> (fun is2 -> ( + let toNaturalList = (fun is -> ( + (* We're mapping the item to a list of naturals that determine a + * lexicographic order. The list has a fixed depth: + * + * [within-commandline, within-group, within-archive, section-or-symbol] + * + * For .o files on the command line, we use the command line order. This + * is the first level in the hierarchy. + * + * For .a files with --whole-archive, we want to do the same. Do this + * by using archive position as the second level of the hierarchy, *if* + * the item is marked as force_output. + * + * For other archives, "order seen" means something different: it's + * the order in which they were "pulled in" during input enumeration. Another + * way to say this is that they're ordered by the first binding that was + * made to them. We map these to numbers starting from the size of the archive, + * i.e. so that "force_output" makes an element appear sooner. In practice + * we won't get a mixture of force_output and non- in the same archive, + * so each archive will use only one of the two orderings. + * + * How do sections order relative to common symbols? Again, in practice it + * doesn't matter because no input query will get a mixture of the two. + * For symbols, we start the numbering from the number of sections in the file, + * so symbols always appear later in the sortd order. + *) + let (linkable_idx, section_or_symbol_idx) = ((match is with + Common(idx1, fname1, img2, def) -> (idx1, Nat_big_num.add + (let (_, l) = (elf_memory_image_section_ranges img2) in length l) def.def_sym_idx) + | InputSection(isrec) -> (isrec.idx, isrec.shndx) + )) + in + (match Lem_list.list_index linkables (Nat_big_num.to_int linkable_idx) with + None -> failwith "impossible: linker input not in linkables list" + | Some (obj, (fname1, blob, (inp_unit, coords)), options) -> + let (our_cid, our_gid, our_aid, maybe_archive_size) = ((match coords with + InArchive(aid, aidx, _, asize) :: InGroup(gid1, gidx) :: [InCommandLine(cid)] -> (cid, gid1, aid, Some asize) + | InArchive(aid, aidx, _, asize) :: [InCommandLine(cid)] -> (cid,Nat_big_num.of_int 0, aid, Some asize) + | InGroup(gid1, gidx) :: [InCommandLine(cid)] -> (cid, gid1,Nat_big_num.of_int 0, None) + | [InCommandLine(cid)] -> (cid,Nat_big_num.of_int 0,Nat_big_num.of_int 0, None) + | _ -> failwith "internal error: impossible coordinates" + )) + in + let aid_to_use = (if options.item_force_output then our_aid + else (* how many elements does the archive have? *) + let archive_size = ((match maybe_archive_size with + None -> failwith "impossible: archive with no size" + | Some a -> a + )) + in Nat_big_num.add archive_size + (* search the bindings: we want the index of the first binding + that refers to this object. + *) + (match Lem_list.find_index (fun ((b_ref_idx, b_ref, b_ref_item), b_maybe_def) -> (match b_maybe_def with + Some (b_def_idx, b_def, b_def_item) -> Nat_big_num.equal b_def_idx linkable_idx + | _ -> false + )) accumulated_bindings with + Some n -> Nat_big_num.of_int n + | None -> failwith "impossible: non-force-output object does not contain any bound-to defs" + )) + in + (* do we care about group idx? probably not. *) + [our_cid; aid_to_use; section_or_symbol_idx] + ) + )) + in +(lexicographic_compare Nat_big_num.compare (toNaturalList is1) (toNaturalList is2)) + ))) + in + (* + let get_binding_for_ref = (fun symref -> (fun linkable_idx -> (fun fname -> + let name_matches = match Map.lookup symref.ref_symname bindings_by_name with Just x -> x | Nothing -> [] end + in + match List.filter (fun (bi, ((r_idx, r, r_item), m_d)) -> r_idx = linkable_idx && r = symref) name_matches with + [(b_idx, b)] -> (b_idx, b) + | [] -> failwith "no binding found" + | _ -> failwith ("ambiguous binding found for symbol `" ^ symref.ref_symname ^ "' in file " ^ fname) + end + ))) + in + *) + let (unrelocated_output_image_lacking_abs_symbols, bindings_by_name) + = (interpret_linker_control_script alloc_map script1 linkables linker_script_linkable_idx a input_sections seen_ordering default_place_orphans initial_bindings_by_name) + in + (* also copy over ABS (range-less) symbols from all included input items *) + let all_abs_range_tags_in_included_inputs = (List.concat ( + Lem_list.map (fun (img2, (idx1, linkable)) -> + let abslist = (Lem_list.mapMaybe (fun (tag, maybeRange) -> + (match tag with + SymbolDef(ent) -> if (Lem.option_equal (Lem.pair_equal (=) (Lem.pair_equal Nat_big_num.equal Nat_big_num.equal)) maybeRange None) && Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.def_syment.elf64_st_shndx)) shn_abs + then Some (maybeRange, ent) + else None + | _ -> None + ) + ) (tagged_ranges_matching_tag + instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict (SymbolDef(null_symbol_definition)) img2)) + in + (*let _ = errln ("Copying " ^ (show (length abslist)) ^ " ABS symbols (names: " ^ + List.foldl (fun acc -> fun str -> if stringLength acc = 0 then str else acc ^ ", " ^ str) "" + (List.map (fun (_, x) -> x.def_symname) abslist) + ^ ") from not-discarded linkable item " ^ + (short_string_of_linkable_item linkable)) + in*) + let x2 = ([]) in List.fold_right + (fun(maybe_range, ent) x2 -> + if true then + (maybe_range, SymbolDef + ({ def_symname = (ent.def_symname) + ; def_syment = (ent.def_syment) + ; def_sym_scn = (ent.def_sym_scn) + ; def_sym_idx = (ent.def_sym_idx) + ; def_linkable_idx = idx1 })) :: x2 else x2) + abslist x2 + ) (list_combine imgs linkables_not_discarded) + )) + in + let by_range_including_abs_symbols = + + (Pset.(union) unrelocated_output_image_lacking_abs_symbols.by_range + ((Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) all_abs_range_tags_in_included_inputs))) + in + let unrelocated_output_image = ({ + elements = (unrelocated_output_image_lacking_abs_symbols.elements) + ; by_range = by_range_including_abs_symbols + ; by_tag = (by_tag_from_by_range + (instance_Basic_classes_SetType_Maybe_maybe_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_var_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_Num_natural_dict + instance_Basic_classes_SetType_Num_natural_dict))) instance_Basic_classes_SetType_var_dict by_range_including_abs_symbols) + }) + (* This image has + * - addresses assigned + * - relocations *not* applied + * - no entry point + * - some ABI features not generated? GOT, certainly. HMM. + -- don't consider output features, like symtabs, yet; + -- other ABI features have to be generated before the linker script runs (dyn relocs, GOT, PLT?) + -- ... so we might be okay for now. + *) + in + let remaining_relocs = (Multimap.lookupBy0 + (instance_Basic_classes_Ord_Memory_image_range_tag_dict + instance_Basic_classes_Ord_Abis_any_abi_feature_dict) (instance_Basic_classes_Ord_Maybe_maybe_dict + (instance_Basic_classes_Ord_tup2_dict + Lem_string_extra.instance_Basic_classes_Ord_string_dict + (instance_Basic_classes_Ord_tup2_dict + instance_Basic_classes_Ord_Num_natural_dict + instance_Basic_classes_Ord_Num_natural_dict))) instance_Basic_classes_SetType_var_dict (instance_Basic_classes_SetType_Maybe_maybe_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_var_dict + (instance_Basic_classes_SetType_tup2_dict + instance_Basic_classes_SetType_Num_natural_dict + instance_Basic_classes_SetType_Num_natural_dict))) (Memory_image_orderings.tagEquiv + instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict) (SymbolRef(null_symbol_reference_and_reloc_site)) + unrelocated_output_image.by_tag) + in + let _ = (List.fold_left (fun _ -> (fun (tag, maybe_range) -> + let _ = ((match tag with + SymbolRef(x) -> (match x.maybe_reloc with + Some rs -> + (match maybe_range with + None -> failwith "impossible: reloc site with no range" + | Some (el_name, (start, len)) -> + () (* errln ("After linking, saw a reloc site in element " ^ el_name ^ ", offset 0x" ^ + (hex_string_of_natural start) ^ ", length 0x" ^ (hex_string_of_natural len) ^ + ", reloc type " ^ Abi_amd64_relocation.string_of_amd64_relocation_type (get_elf64_relocation_a_type rs.ref_relent)) *) + ) + | None -> (* okay, do nothing *) () + ) + | _ -> failwith "impossible: not a symbol ref" + )) + in + () + )) () remaining_relocs) + in + (* Before we relocate, we concretise any ABI features that we've linked in. *) + (*let _ = errln "Asking ABI to concretise support structures" in*) + let unrelocated_concrete_output_image = (a.concretise_support unrelocated_output_image) + in + let output_image = (relocate_output_image a bindings_by_name unrelocated_concrete_output_image) + in + let (maybe_entry_point_address : Nat_big_num.num option) = + ((match Command_line.find_option_matching_tag (Command_line.EntryAddress(Nat_big_num.of_int 0)) options with + None -> a.guess_entry_point output_image + | Some(Command_line.EntryAddress(x)) -> Some x + )) + in + (match maybe_entry_point_address with + Some addr -> + (match address_to_element_and_offset addr output_image with + Some (el_name, el_offset) -> + (*let _ = errln ("Tagging element " ^ el_name ^ " as containing entry point at offset 0x" ^ (hex_string_of_natural el_offset)) + in*) + tag_image (EntryPoint) el_name el_offset(Nat_big_num.of_int 0) output_image + | None -> + (* HMM. entry point symbol has no address at present. *) + failwith ("error: entry point address 0x" ^ ((hex_string_of_natural addr) ^ " does not correspond to any element position")) + ) + | None -> + (*let _ = errln "Warning: not tagging entry point in output image" + in*) + output_image + )) |