diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/linker_script.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/linker_script.ml | 2783 |
1 files changed, 0 insertions, 2783 deletions
diff --git a/lib/ocaml_rts/linksem/linker_script.ml b/lib/ocaml_rts/linksem/linker_script.ml deleted file mode 100644 index 535d9037..00000000 --- a/lib/ocaml_rts/linksem/linker_script.ml +++ /dev/null @@ -1,2783 +0,0 @@ -(*Generated by Lem from linker_script.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_num -open Lem_maybe -open Lem_assert_extra -open Lem_set -(*import Map*) - -open Byte_sequence -open Default_printing -open Error -open Missing_pervasives -open Show - -open Elf_header -open Elf_file -open Elf_interpreted_section - -open Abis -open Command_line -open Input_list -open Linkable_list -open Memory_image -open Elf_memory_image (* HMM -- ideally we'd be ELF-agnostic in this file. - But Abstract_abi is now merged into Elf_memory_image, so never mind. *) -open Elf_memory_image_of_elf64_file -open Elf_relocation -open Elf_symbol_table -open Elf_section_header_table -open Elf_types_native_uint -open Memory_image_orderings - -(* We model two kinds of linker script: "implicit scripts", which are supplied - * on the command line as input objects, and "control scripts" of which there - * is exactly one per link job. The abstract syntax of each script comes from the - * same grammar. - * - * We define the control script as a bunch of functions, to allow for - * link jobs where we don't have an AST and the script behaviour is hard-coded. - *) - -(* Input sections come from individual (relocatable) ELF files. - * The name of this file is important! - * - * Each input "section" is always an identified section or common symbol - * *within* some ELF memory image. *) - -type input_section_rec = { - idx : Nat_big_num.num (* linkable idx *) -; fname : string -; img : elf_memory_image -; shndx : Nat_big_num.num -; secname: string -; isec : elf64_interpreted_section -} - -type input_spec - = Common of (Nat_big_num.num * string * elf_memory_image * symbol_definition) (* string is symbol name -- must be a COMMON symbol *) - | InputSection of input_section_rec - -(* A control script defines - * - output sections - * - a mapping from output sections to (ordered) input sections - * - extra symbols - * - output format etc. (skip this for now) - *) - -(* We will have to deal with merging etc. at some point, somewhere - * (maybe here, maybe not); for now we just produce an ordered list - * of sections. - *) - -(* We can't model linker scripts as plain Lem functions without writing - * them to a very different structure than that of scripts. The reason is that - * certain features of the script language necessitate multiple passes - * over the script structure. For example, to figure out how big an - * output section is, hence where to begin the next section, you need to - * know which of the input sections are marked for KEEP. For that, you need - * a def-use graph over input sections. But for that, you also need to account - * for *all* symbol definitions, and the script itself is allowed to add new - * ones (right in among its input sections). So we have to do one pass to - * enumerate the symbol additions, and another pass to eliminate sections - * that we don't want to KEEP. - * - * Other gotchas include: - * - * - symbol provision and address advancement can occur in among the input - * section queries, but also outside any output section. - * - * - semantics of DATA_SEGMENT_ALIGN depend on future script contents - * - * - ONLY_IF_RO and ONLY_IF_RW are tricky: need to evaluate the input section - * queries - * - * - semantics of empty sections are subtle (". = ." will force an empty section - * to be emitted, but ". = . + 0" will not do so). - * - * Our approach is to define an interpreter for (at present) most of the script - * language. - *) - -type symbol_def_policy = AlwaysDefine - | ProvideIfUsed - -type input_selector = input_spec list -> input_spec list - -type address_expr = Memory_image.expr - -type output_guard = AlwaysOutput - | OnlyIfRo - | OnlyIfRw - -type symbol_spec = (Nat_big_num.num * Uint32.uint32 * Uint32.uint32) (* size, info, other *) - -type retain_policy - = DefaultKeep - | KeepEvenWhenGC - -type address_expr_fn_ref = Nat_big_num.num -type 'a address_expr_fn_map = (address_expr_fn_ref, (Nat_big_num.num -> 'a -> Nat_big_num.num)) Pmap.map -(* 'a = allocated_sections_map *) - -type output_section_composition_element - = IncludeInputSection of (retain_policy * input_section_rec) - | IncludeCommonSymbol of (retain_policy * string (* file *) * Nat_big_num.num (* linkable_idx *) * symbol_definition * elf_memory_image) - | Hole of address_expr_fn (* compute the next addr to continue layout at *) - | ProvideSymbol of (symbol_def_policy * string * symbol_spec) -and -sort_policy - = DefaultSort (* Use command line sort option, else "seen" order *) - | SeenOrder (* Always use "seen" order *) - | ByName - | ByNameThenAlignment - | ByAlignment - | ByAlignmentThenName - | ByInitPriority -and -(* This mirrors the OutputSection constructor, except that the script elements have become - * output_section_composition_elements, and we might store the size here. *) -output_section_spec = - OutputSectionSpec of (output_guard * Nat_big_num.num option * string * ( output_section_composition_element list)) -and -allocated_sections_map = - AllocatedSectionsMap of (string, (output_section_spec (* OutputSection element idx *) * Nat_big_num.num)) Pmap.map -and -address_expr_fn - = AddressExprFn of address_expr_fn_ref - -type script_element = - DefineSymbol of (symbol_def_policy * string * symbol_spec) -| AdvanceAddress of address_expr_fn -| MarkAndAlignDataSegment of (Nat_big_num.num * Nat_big_num.num) (* maxpagesize, commonpagesize *) -| MarkDataSegmentEnd -| MarkDataSegmentRelroEnd (*of (allocated_sections_map -> (natural * (natural -> natural))) DPM: commented out because of positivity constrains in Isabelle *) -| OutputSection of (output_guard * ( (* address_expr *) address_expr_fn option) * string * script_element list) -| DiscardInput of input_selector - (* Input queries can only occur within an output section. - Output sections may not nest within other output sections. - (Ideally we would use something like polymorphic variants to encode this.) - *) -| InputQuery of (retain_policy * sort_policy * input_selector) - -(* A linker control script is a function from inputs to output elements. - * We can define them in syntax (using an interpreter) - * or in Lem directly (as functions). *) -type linker_control_script = script_element list -type labelled_linker_control_script = (script_element * Nat_big_num.num) list - -(*val all_suffixes : list char -> list (list char)*) -let rec all_suffixes chars:((char)list)list= - ((match chars with - [] -> [[]] - | c :: morecs -> chars :: (all_suffixes morecs) - )) - -(*val glob_match : list char -> list char -> bool*) -let rec glob_match pat str:bool= - ((match (pat, str) with - ([], []) -> true - | ('?':: morepat, _ :: morestr) -> glob_match morepat morestr - | ('*':: morepat, _) -> - (* if any suffix of the remaining string matches - * the remaining pattern, we've matched the pattern - * from '*' onwards. *) - let or_suffix_match = (fun matched -> (fun newlist -> - matched || glob_match morepat newlist)) - in - List.fold_left (or_suffix_match) false (all_suffixes str) - | (patc :: morepat, c :: morestr) -> (patc = c) && glob_match morepat morestr - | ([], _) -> (* ran out of pattern *) false - | (_, []) -> (* ran out of str *) false - )) - -(*val default_symbol_spec : symbol_spec*) -let default_symbol_spec:Nat_big_num.num*Uint32.uint32*Uint32.uint32= (Nat_big_num.of_int 0, Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)), Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) -(*val hidden_symbol_spec : symbol_spec*) -let hidden_symbol_spec:Nat_big_num.num*Uint32.uint32*Uint32.uint32= (Nat_big_num.of_int 0, Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)), Uint32.of_string (Nat_big_num.to_string stv_hidden)) - -(* These Lem functions replicate linker script functions or builtin behaviours. *) - -(*val only_sections : input_selector*) -let only_sections inputs:(input_spec)list= (Lem_list.mapMaybe - (fun i -> (match i with - | InputSection(_) -> Some(i) - | _ -> None - )) inputs) - -(*val filter_and_concat : (input_spec -> bool) -> input_selector*) (* a.k.a. list input_spec -> list input_spec *) -let filter_and_concat p inputs:(input_spec)list= (List.filter p inputs) - -(*val name_matches : string -> input_spec -> bool*) -let name_matches pat input:bool= - ((match input with - InputSection(inp) -> - (*let _ = errln ("Does section name `" ^ inp.secname ^ "' match glob pattern `" ^ pat ^ "'? ") in - let result = *)glob_match (Xstring.explode pat) (Xstring.explode inp.secname) (*in - let _ = errln (if result then "yes" else "no") - in result*) - | _ -> false - )) - -(*val file_matches : string -> input_spec -> bool*) -let file_matches pat input:bool= - ((match input with - InputSection(inp) -> glob_match (Xstring.explode pat) (Xstring.explode inp.fname) - | _ -> false - )) - -let compareInputSpecByNameThenAlignment i1 i2:int= - (let toPair = (fun is -> ((match is with - Common(idx1, fname1, img2, def) -> ("COMMON" (* FIXME: is this right? *), Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value) - | InputSection(isrec) -> (isrec.isec.elf64_section_name_as_string, isrec.isec.elf64_section_align) - ))) - in (pairCompare compare Nat_big_num.compare (toPair i1) (toPair i2))) - -let compareInputSpecByAlignment i1 i2:int= - (let toNatural = (fun is -> ((match is with - Common(idx1, fname1, img2, def) -> Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value - | InputSection(isrec) -> isrec.isec.elf64_section_align - ))) - in Nat_big_num.compare (toNatural i1) (toNatural i2)) - -let compareInputSpecByName i1 i2:int= - (let toString = (fun is -> ((match is with - Common(idx1, fname1, img2, def) -> "COMMON" - | InputSection(isrec) -> isrec.isec.elf64_section_name_as_string - ))) - in compare (toString i1) (toString i2)) - -let compareInputSpecByAlignmentThenName i1 i2:int= - (let toPair = (fun is -> ((match is with - Common(idx1, fname1, img2, def) -> (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value, - "COMMON" (* FIXME: is this right? *)) - | InputSection(isrec) -> (isrec.isec.elf64_section_align, isrec.isec.elf64_section_name_as_string) - ))) - in (pairCompare Nat_big_num.compare compare (toPair i1) (toPair i2))) - -let compareInputSpecByInitPriority i1 i2:int= 0 (* FIXME *) - -(* DATA_SEGMENT_ALIGN is defined by two formulae - * (over pos and commonpagesize/maxpagesize) - * "... depending on whether the latter uses fewer COMMONPAGESIZE sized - pages for the data segment (area between the result of this - expression and `DATA_SEGMENT_END') than the former or not. If the - latter form is used, it means COMMONPAGESIZE bytes of runtime - memory will be saved at the expense of up to COMMONPAGESIZE wasted - bytes in the on-disk file." - - So the amount of padding that gets inserted here depends on the location - of something that comes *later*, namely DATA_SEGMENT_END. - So, we can't model it as a function of the current position. - Instead, we add MarkDataSegmentEnd and friends - to the script_element ADT. - *) - -let has_writability:'a ->input_spec ->bool= (fun writable -> (fun input_sec -> ( - (match input_sec with - Common(_, _, _, _) - -> (* all common symbols are potentially writable *) true - | InputSection(inp) - -> let (flags : Nat_big_num.num) = ((match elf_memory_image_section_by_index inp.shndx inp.img with - Some x -> x.elf64_section_flags - | None -> failwith ("impossible: no such section" (*(index " ^ (show inp.shndx) ^ ")""*)) - )) - in - flag_is_set shf_write flags - ) -))) - -(* LARGE_COMMON seems to have been defined in this patch set: - https://sourceware.org/ml/binutils/2005-07/txt00014.txt - and at the time was "only for x86-64". It seems to be analogous - to ".lbss", i.e. "large bss". libbfd defines SHF_X86_64_LARGE. - The best comment seems to be in llvm's Support/ELF.h: - -0814 // If an object file section does not have this flag set, then it may not hold -0815 // more than 2GB and can be freely referred to in objects using smaller code -0816 // models. Otherwise, only objects using larger code models can refer to them. -0817 // For example, a medium code model object can refer to data in a section that -0818 // sets this flag besides being able to refer to data in a section that does -0819 // not set it; likewise, a small code model object can refer only to code in a -0820 // section that does not set this flag. - - *) - -(*val address_zero : natural -> address_expr_fn_map allocated_sections_map -> - (natural * address_expr_fn_map allocated_sections_map * address_expr_fn)*) -let address_zero fresh alloc_map:Nat_big_num.num*((Nat_big_num.num),(Nat_big_num.num ->allocated_sections_map ->Nat_big_num.num))Pmap.map*address_expr_fn= - (let alloc_map' = (Pmap.add fresh (fun pos -> (fun secs ->Nat_big_num.of_int 0)) alloc_map) in - let fresh' = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - (fresh', alloc_map', AddressExprFn fresh)) - -(* -val output_sec_composition_size : list output_section_composition_element -> natural -let output_sec_composition_size comp = List.foldl (+) 0 (List.map size_of_output_section_composition_element comp) -*) -(*val do_output_section_layout_starting_at_addr : natural -> allocated_sections_map -> list output_section_composition_element -> (natural * list natural)*) -let do_output_section_layout_starting_at_addr start_addr (AllocatedSectionsMap secs) comps:Nat_big_num.num*(Nat_big_num.num)list= -( - (* map out where we plumb in each section, accounting for their alignment *)List.fold_left (fun (next_free_addr, addr_list) -> (fun comp_el -> (match comp_el with - IncludeInputSection(retain_pol, irec (* fname, linkable_idx, shndx, isec, img *)) -> - let aligned_next_free = (align_up_to irec.isec.elf64_section_align next_free_addr) - in - (*let _ = errln ("Aligned start address up to 0x" ^ hex_string_of_natural aligned_next_free ^ - " (align 0x" ^ (hex_string_of_natural irec.isec.elf64_section_align) ^ - ") for included output section `" ^ - irec.isec.elf64_section_name_as_string ^ "' from file `" ^ irec.fname ^ "'") - in*) - ( Nat_big_num.add aligned_next_free irec.isec.elf64_section_size, List.rev_append (List.rev addr_list) [aligned_next_free]) - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> - let aligned_next_free = (align_up_to (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value) next_free_addr) - in - ( Nat_big_num.add aligned_next_free (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_size), List.rev_append (List.rev addr_list) [aligned_next_free]) - (*| Hole(AddressExprFn f) -> (f next_free_addr secs, addr_list ++ [next_free_addr])*) - | ProvideSymbol(pol, name1, spec) -> (next_free_addr, List.rev_append (List.rev addr_list) [next_free_addr]) - ) - )) (start_addr, []) comps) - -(*val output_sec_composition_size_given_start_addr : natural -> allocated_sections_map -> list output_section_composition_element -> natural*) -let output_sec_composition_size_given_start_addr start_addr secs comp:Nat_big_num.num= - (let (end_addr, comp_addrs) = (do_output_section_layout_starting_at_addr start_addr secs comp) - in Nat_big_num.sub_nat - end_addr start_addr) - -(*val sizeof : string -> allocated_sections_map -> natural*) -let sizeof secname1 (AllocatedSectionsMap secs):Nat_big_num.num= - ((match Pmap.lookup secname1 secs with - Some(OutputSectionSpec (_, maybe_addr, _, comp), _) -> (match maybe_addr with - Some addr -> output_sec_composition_size_given_start_addr addr (AllocatedSectionsMap secs) comp - | None -> failwith ("error: sizeof applied to section without defined start address") - ) - | None -> failwith ("error: sizeof applied to non-existent section name " ^ secname1) - )) - -(*val alignof_output_section_composition_element : output_section_composition_element -> natural*) -let alignof_output_section_composition_element comp:Nat_big_num.num= - ((match comp with - IncludeInputSection(_, irec) -> irec.isec.elf64_section_align - | IncludeCommonSymbol(_, _, _, def, _) -> Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value - | _ ->Nat_big_num.of_int 1 (* CHECK *) - )) - -(*val alignof_output_section : list output_section_composition_element -> natural*) -let alignof_output_section comps:Nat_big_num.num= - (let aligns = (Lem_list.map alignof_output_section_composition_element comps) - in - List.fold_left (fun acc_lcm -> fun next -> lcm acc_lcm next)(Nat_big_num.of_int 1) aligns) - -(*val default_linker_control_script : natural -> address_expr_fn_map allocated_sections_map -> - abi any_abi_feature -> maybe natural -> maybe natural -> maybe natural -> - natural -> (natural * address_expr_fn_map allocated_sections_map * linker_control_script)*) -let default_linker_control_script fresh alloc_map a user_text_segment_start user_data_segment_start user_rodata_segment_start elf_headers_size:Nat_big_num.num*((Nat_big_num.num),(Nat_big_num.num ->allocated_sections_map ->Nat_big_num.num))Pmap.map*(script_element)list= - (let segment_start name1 default= ((match name1 with - "ldata-segment" -> (match user_data_segment_start with - None -> default - | Some addr -> (* fun _ -> *) addr - ) - | "text-segment" -> (match user_text_segment_start with - None -> default - | Some addr -> (* fun _ -> *) addr - ) - )) - in - let is_large_common = (fun inp -> (* FIXME: treat large commons separately *) false - ) - in - let is_common = (fun isec1 -> (match isec1 with - Common(idx1, fname1, img2, def) -> (*let _ = errln ("Common or large-common symbol: " ^ def.def_symname) in *) - not (is_large_common isec1) - | _ -> false - )) - in - let alloc_fn1 = (fun _ -> (fun _ -> Nat_big_num.add (segment_start "text-segment" ( Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 1048576))) elf_headers_size)) in - let alloc_fn1_ref = fresh in - let alloc_map = (Pmap.add alloc_fn1_ref alloc_fn1 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn2 = (fun addr -> (fun _ -> Nat_big_num.sub_nat - (* (align_up_to a.maxpagesize addr) - (natural_land (a.maxpagesize - addr) (a.maxpagesize - 1)) *) - (* - FIXME: understand the intention of this assignment. - Evaluating a simple example of this (from true-static-uClibc) - - (ALIGN (0x200000) - ((0x200000 - .) & 0x1fffff)) - - starting from 0x00000000004017dc - means - 0x600000 - ((0x200000 - 0x4017dc) & 0x1fffff) - i.e. - 0x600000 - (((-0x2017dc)) & 0x1fffff) - i.e. - 0x600000 - ( -0x2017dc - & 0x1fffff ) - - which really does come to (according to bash) 0x4017dc - i.e. we subtract 0x1fe824 from 0x600000 - and end up back where we started. - - What does ANDing a negative number mean? - It doesn't seem to work for us. - Well, to take the negation we flip every bit and add one. - So if we don't want to do a subtraction that might go negative, - we can instead add the complement. - *) - (align_up_to a.maxpagesize addr) (Nat_big_num.bitwise_and ( Nat_big_num.add a.maxpagesize (compl64 addr)) ( Nat_big_num.sub_nat a.maxpagesize(Nat_big_num.of_int 1))))) in - let (fresh, alloc_map, (address_zero_fn : address_expr_fn)) = (address_zero fresh alloc_map) in - let alloc_fn2_ref = fresh in - let alloc_map = (Pmap.add alloc_fn2_ref alloc_fn2 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn3 = (fun pos -> (fun secs -> align_up_to (if Nat_big_num.equal pos(Nat_big_num.of_int 0) then (Nat_big_num.div(Nat_big_num.of_int 64)(Nat_big_num.of_int 8)) else Nat_big_num.of_int 1) pos)) in - let alloc_fn3_ref = fresh in - let alloc_map = (Pmap.add alloc_fn3_ref alloc_fn3 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn4 = (fun pos -> (fun secs -> align_up_to (Nat_big_num.div(Nat_big_num.of_int 64)(Nat_big_num.of_int 8)) pos)) in - let alloc_fn4_ref = fresh in - let alloc_map = (Pmap.add alloc_fn4_ref alloc_fn4 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn5 = (fun pos -> (fun secs -> segment_start "ldata-segment" pos)) in - let alloc_fn5_ref = fresh in - let alloc_map = (Pmap.add alloc_fn5_ref alloc_fn5 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn6 = (fun pos -> fun secs -> align_up_to ( Nat_big_num.add a.maxpagesize ( Nat_big_num.sub_nat(Nat_big_num.bitwise_and pos a.maxpagesize)(Nat_big_num.of_int 1))) pos) in - let alloc_fn6_ref = fresh in - let alloc_map = (Pmap.add alloc_fn6_ref alloc_fn6 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn7 = (fun pos -> (fun secs -> (if not (Nat_big_num.equal pos(Nat_big_num.of_int 0)) then Nat_big_num.div(Nat_big_num.of_int 64)(Nat_big_num.of_int 8) else Nat_big_num.of_int 1))) in - let alloc_fn7_ref = fresh in - let alloc_map = (Pmap.add alloc_fn7_ref alloc_fn7 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - let alloc_fn8 = (fun pos -> (fun secs -> align_up_to (Nat_big_num.div(Nat_big_num.of_int 64)(Nat_big_num.of_int 8)) pos)) in - let alloc_fn8_ref = fresh in - let alloc_map = (Pmap.add alloc_fn8_ref alloc_fn8 alloc_map) in - let fresh = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - (fresh, alloc_map, [ - (* For now, we base our script on the GNU bfd linker's scripts. - Here's the static -z combreloc one. - -/* Script for -z combreloc: combine and sort reloc sections */ -/* Copyright (C) 2014 Free Software Foundation, Inc. - Copying and distribution of this script, with or without modification, - are permitted in any medium without royalty provided the copyright - notice and this notice are preserved. */ -OUTPUT_FORMAT("elf64-x86-64", "elf64-x86-64", - "elf64-x86-64") -OUTPUT_ARCH(i386:x86-64) -ENTRY(_start) -SEARCH_DIR("=/usr/x86_64-linux-gnu/lib64"); SEARCH_DIR("=/usr/local/lib/x86_64-linux-gnu"); SEARCH_DIR("=/usr/local/lib64"); SEARCH_DIR("=/lib/x86_64-linux-gnu"); SEARCH_DIR("=/lib64"); SEARCH_DIR("=/usr/lib/x86_64-linux-gnu"); SEARCH_DIR("=/usr/lib64"); SEARCH_DIR("=/usr/x86_64-linux-gnu/lib"); SEARCH_DIR("=/usr/local/lib"); SEARCH_DIR("=/lib"); SEARCH_DIR("=/usr/lib"); -SECTIONS -{ - /* Read-only sections, merged into text segment: */ - PROVIDE (__executable_start = SEGMENT_START("text-segment", 0x400000)); . = SEGMENT_START("text-segment", 0x400000) + SIZEOF_HEADERS; - .interp : { *(.interp) } - .note.gnu.build-id : { *(.note.gnu.build-id) } - .hash : { *(.hash) } - .gnu.hash : { *(.gnu.hash) } - .dynsym : { *(.dynsym) } - .dynstr : { *(.dynstr) } - .gnu.version : { *(.gnu.version) } - .gnu.version_d : { *(.gnu.version_d) } - .gnu.version_r : { *(.gnu.version_r) } - .rela.dyn : - { - *(.rela.init) - *(.rela.text .rela.text.* .rela.gnu.linkonce.t.* ) - *(.rela.fini) - *(.rela.rodata .rela.rodata.* .rela.gnu.linkonce.r.* ) - *(.rela.data .rela.data.* .rela.gnu.linkonce.d.* ) - *(.rela.tdata .rela.tdata.* .rela.gnu.linkonce.td.* ) - *(.rela.tbss .rela.tbss.* .rela.gnu.linkonce.tb.* ) - *(.rela.ctors) - *(.rela.dtors) - *(.rela.got) - *(.rela.bss .rela.bss.* .rela.gnu.linkonce.b.* ) - *(.rela.ldata .rela.ldata.* .rela.gnu.linkonce.l.* ) - *(.rela.lbss .rela.lbss.* .rela.gnu.linkonce.lb.* ) - *(.rela.lrodata .rela.lrodata.* .rela.gnu.linkonce.lr.* ) - *(.rela.ifunc) - } - .rela.plt : - { - *(.rela.plt) - PROVIDE_HIDDEN (__rela_iplt_start = .); - *(.rela.iplt) - PROVIDE_HIDDEN (__rela_iplt_end = .); - } - .init : - { - KEEP ( *(SORT_NONE(.init))) - } - .plt : { *(.plt) *(.iplt) } - .plt.bnd : { *(.plt.bnd) } - .text : - { - *(.text.unlikely .text.*_unlikely .text.unlikely.* ) - *(.text.exit .text.exit.* ) - *(.text.startup .text.startup.* ) - *(.text.hot .text.hot.* ) - *(.text .stub .text.* .gnu.linkonce.t.* ) - /* .gnu.warning sections are handled specially by elf32.em. */ - *(.gnu.warning) - } - .fini : - { - KEEP ( *(SORT_NONE(.fini))) - } - PROVIDE (__etext = .); - PROVIDE (_etext = .); - PROVIDE (etext = .); - .rodata : { *(.rodata .rodata.* .gnu.linkonce.r.* ) } - .rodata1 : { *(.rodata1) } - .eh_frame_hdr : { *(.eh_frame_hdr) } - .eh_frame : ONLY_IF_RO { KEEP ( *(.eh_frame)) } - .gcc_except_table : ONLY_IF_RO { *(.gcc_except_table - .gcc_except_table.* ) } - /* These sections are generated by the Sun/Oracle C++ compiler. */ - .exception_ranges : ONLY_IF_RO { *(.exception_ranges - .exception_ranges* ) } - /* Adjust the address for the data segment. We want to adjust up to - the same address within the page on the next page up. */ - . = ALIGN (CONSTANT (MAXPAGESIZE)) - ((CONSTANT (MAXPAGESIZE) - .) & (CONSTANT (MAXPAGESIZE) - 1)); . = DATA_SEGMENT_ALIGN (CONSTANT (MAXPAGESIZE), CONSTANT (COMMONPAGESIZE)); - /* Exception handling */ - .eh_frame : ONLY_IF_RW { KEEP ( *(.eh_frame)) } - .gcc_except_table : ONLY_IF_RW { *(.gcc_except_table .gcc_except_table.* ) } - .exception_ranges : ONLY_IF_RW { *(.exception_ranges .exception_ranges* ) } - /* Thread Local Storage sections */ - .tdata : { *(.tdata .tdata.* .gnu.linkonce.td.* ) } - .tbss : { *(.tbss .tbss.* .gnu.linkonce.tb.* ) *(.tcommon) } - .preinit_array : - { - PROVIDE_HIDDEN (__preinit_array_start = .); - KEEP ( *(.preinit_array)) - PROVIDE_HIDDEN (__preinit_array_end = .); - } - .init_array : - { - PROVIDE_HIDDEN (__init_array_start = .); - KEEP ( *(SORT_BY_INIT_PRIORITY(.init_array.* ) SORT_BY_INIT_PRIORITY(.ctors.* ))) - KEEP ( *(.init_array EXCLUDE_FILE ( *crtbegin.o *crtbegin?.o *crtend.o *crtend?.o ) .ctors)) - PROVIDE_HIDDEN (__init_array_end = .); - } - .fini_array : - { - PROVIDE_HIDDEN (__fini_array_start = .); - KEEP ( *(SORT_BY_INIT_PRIORITY(.fini_array.* ) SORT_BY_INIT_PRIORITY(.dtors.* ))) - KEEP ( *(.fini_array EXCLUDE_FILE ( *crtbegin.o *crtbegin?.o *crtend.o *crtend?.o ) .dtors)) - PROVIDE_HIDDEN (__fini_array_end = .); - } - .ctors : - { - /* gcc uses crtbegin.o to find the start of - the constructors, so we make sure it is - first. Because this is a wildcard, it - doesn't matter if the user does not - actually link against crtbegin.o; the - linker won't look for a file to match a - wildcard. The wildcard also means that it - doesn't matter which directory crtbegin.o - is in. */ - KEEP ( *crtbegin.o(.ctors)) - KEEP ( *crtbegin?.o(.ctors)) - /* We don't want to include the .ctor section from - the crtend.o file until after the sorted ctors. - The .ctor section from the crtend file contains the - end of ctors marker and it must be last */ - KEEP ( *(EXCLUDE_FILE ( *crtend.o *crtend?.o ) .ctors)) - KEEP ( *(SORT(.ctors.* ))) - KEEP ( *(.ctors)) - } - .dtors : - { - KEEP ( *crtbegin.o(.dtors)) - KEEP ( *crtbegin?.o(.dtors)) - KEEP ( *(EXCLUDE_FILE ( *crtend.o *crtend?.o ) .dtors)) - KEEP ( *(SORT(.dtors.* ))) - KEEP ( *(.dtors)) - } - .jcr : { KEEP ( *(.jcr)) } - .data.rel.ro : { *(.data.rel.ro.local* .gnu.linkonce.d.rel.ro.local.* ) *(.data.rel.ro .data.rel.ro.* .gnu.linkonce.d.rel.ro.* ) } - .dynamic : { *(.dynamic) } - .got : { *(.got) *(.igot) } - . = DATA_SEGMENT_RELRO_END (SIZEOF (.got.plt) >= 24 ? 24 : 0, .); - .got.plt : { *(.got.plt) *(.igot.plt) } - .data : - { - *(.data .data.* .gnu.linkonce.d.* ) - SORT(CONSTRUCTORS) - } - .data1 : { *(.data1) } - _edata = .; PROVIDE (edata = .); - . = .; - __bss_start = .; - .bss : - { - *(.dynbss) - *(.bss .bss.* .gnu.linkonce.b.* ) - *(COMMON) - /* Align here to ensure that the .bss section occupies space up to - _end. Align after .bss to ensure correct alignment even if the - .bss section disappears because there are no input sections. - FIXME: Why do we need it? When there is no .bss section, we don't - pad the .data section. */ - . = ALIGN(. != 0 ? 64 / 8 : 1); - } - .lbss : - { - *(.dynlbss) - *(.lbss .lbss.* .gnu.linkonce.lb.* ) - *(LARGE_COMMON) - } - . = ALIGN(64 / 8); - . = SEGMENT_START("ldata-segment", .); - .lrodata ALIGN(CONSTANT (MAXPAGESIZE)) + (. & (CONSTANT (MAXPAGESIZE) - 1)) : - { - *(.lrodata .lrodata.* .gnu.linkonce.lr.* ) - } - .ldata ALIGN(CONSTANT (MAXPAGESIZE)) + (. & (CONSTANT (MAXPAGESIZE) - 1)) : - { - *(.ldata .ldata.* .gnu.linkonce.l.* ) - . = ALIGN(. != 0 ? 64 / 8 : 1); - } - . = ALIGN(64 / 8); - _end = .; PROVIDE (end = .); - . = DATA_SEGMENT_END (.); - /* Stabs debugging sections. */ - .stab 0 : { *(.stab) } - .stabstr 0 : { *(.stabstr) } - .stab.excl 0 : { *(.stab.excl) } - .stab.exclstr 0 : { *(.stab.exclstr) } - .stab.index 0 : { *(.stab.index) } - .stab.indexstr 0 : { *(.stab.indexstr) } - .comment 0 : { *(.comment) } - /* DWARF debug sections. - Symbols in the DWARF debugging sections are relative to the beginning - of the section so we begin them at 0. */ - /* DWARF 1 */ - .debug 0 : { *(.debug) } - .line 0 : { *(.line) } - /* GNU DWARF 1 extensions */ - .debug_srcinfo 0 : { *(.debug_srcinfo) } - .debug_sfnames 0 : { *(.debug_sfnames) } - /* DWARF 1.1 and DWARF 2 */ - .debug_aranges 0 : { *(.debug_aranges) } - .debug_pubnames 0 : { *(.debug_pubnames) } - /* DWARF 2 */ - .debug_info 0 : { *(.debug_info .gnu.linkonce.wi.* ) } - .debug_abbrev 0 : { *(.debug_abbrev) } - .debug_line 0 : { *(.debug_line .debug_line.* .debug_line_end ) } - .debug_frame 0 : { *(.debug_frame) } - .debug_str 0 : { *(.debug_str) } - .debug_loc 0 : { *(.debug_loc) } - .debug_macinfo 0 : { *(.debug_macinfo) } - /* SGI/MIPS DWARF 2 extensions */ - .debug_weaknames 0 : { *(.debug_weaknames) } - .debug_funcnames 0 : { *(.debug_funcnames) } - .debug_typenames 0 : { *(.debug_typenames) } - .debug_varnames 0 : { *(.debug_varnames) } - /* DWARF 3 */ - .debug_pubtypes 0 : { *(.debug_pubtypes) } - .debug_ranges 0 : { *(.debug_ranges) } - /* DWARF Extension. */ - .debug_macro 0 : { *(.debug_macro) } - .gnu.attributes 0 : { KEEP ( *(.gnu.attributes)) } - /DISCARD/ : { *(.note.GNU-stack) *(.gnu_debuglink) *(.gnu.lto_* ) } -} - *) - - (* function from - inputs and configuration - to - output sections-with-address-and-policy, output symbols-with-address-and-attributes, - discards, orphans - BUT - 1. policy is not a property of output sections, but of *inputs within outputs* - i.e. KEEP( *(.init)) - - what's helpful for writing such functions? - - e.g. only_if_ro (input_query) (output ): - - i.e. ++ only_if_ro OutputSection(AlwaysOutput, Nothing, ".eh_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame"))]) - - want to take a bunch of outputs - and return a bunch of outputs? - - if so, need to return a "current address" - - *) - (DefineSymbol(ProvideIfUsed, "__executable_start", default_symbol_spec)) - ; AdvanceAddress(AddressExprFn alloc_fn1_ref) - ; OutputSection(AlwaysOutput, None, ".interp", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".interp"))]) - ; OutputSection(AlwaysOutput, None, ".note.gnu.build-id", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".note.gnu.build-id"))]) - ; OutputSection(AlwaysOutput, None, ".hash", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".hash"))]) - ; OutputSection(AlwaysOutput, None, ".gnu.hash", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.hash"))]) - ; OutputSection(AlwaysOutput, None, ".dynsym", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynsym"))]) - ; OutputSection(AlwaysOutput, None, ".dynstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynstr"))]) - ; OutputSection(AlwaysOutput, None, ".gnu.version", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.version"))]) - ; OutputSection(AlwaysOutput, None, ".gnu.version_d", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.version_d"))]) - ; OutputSection(AlwaysOutput, None, ".gnu.version_r", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".gnu.version_r"))]) - ; OutputSection(AlwaysOutput, None, ".rela.dyn", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.init")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.text" s || (name_matches ".rela.text.*" s || name_matches ".rela.gnu.linkonce.t.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.rodata" s || (name_matches ".rela.rodata.*" s || name_matches ".rela.gnu.linkonce.r.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.data" s || (name_matches ".rela.data.*" s || name_matches ".rela.gnu.linkonce.d.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.tdata" s || (name_matches ".rela.tdata.*" s || name_matches ".rela.gnu.linkonce.td.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.tbss" s || (name_matches ".rela.tbss.*" s || name_matches ".rela.gnu.linkonce.tb.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.ctors")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.got")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.bss" s || (name_matches ".rela.bss.*" s || name_matches ".rela.gnu.linkonce.b.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.ldata" s || (name_matches ".rela.ldata.*" s || name_matches ".rela.gnu.linkonce.l.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rela.lbss" s || (name_matches ".rela.lbss.*" s || name_matches ".rela.gnu.linkonce.lb.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.ifunc")) - ]) - ; OutputSection(AlwaysOutput, None, ".rela.plt", [ - InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.plt")) - ; DefineSymbol(ProvideIfUsed, "__rela_iplt_start", (Nat_big_num.of_int 0, make_symbol_info stb_local stt_notype (* FIXME *), make_symbol_other stv_hidden)) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".rela.iplt")) - ; DefineSymbol(ProvideIfUsed, "__rela_iplt_end", (Nat_big_num.of_int 0, make_symbol_info stb_local stt_notype (* FIXME *), make_symbol_other stv_hidden)) - ]) - ; OutputSection(AlwaysOutput, None, ".init", [ - InputQuery(KeepEvenWhenGC, SeenOrder, filter_and_concat (name_matches ".init")) - ]) - ; OutputSection(AlwaysOutput, None, ".plt", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".plt")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".iplt")) - ]) - ; OutputSection(AlwaysOutput, None, ".plt.bnd", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".plt.bnd"))]) - ; OutputSection(AlwaysOutput, None, ".text", [ - InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".text.unlikely" s || (name_matches ".text.*_unlikely" s || name_matches ".text.unlikely.*" s) - )) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".text.exit" s || name_matches ".text.exit.*" s)) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".text.startup" s || name_matches ".text.startup.*" s)) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".text.hot" s || name_matches ".text.hot.*" s)) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".text" s || (name_matches ".stub" s || (name_matches ".text.*" s || name_matches ".gnu.linkonce.t.*" s)))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - (* ".gnu.warning sections are handled specially by elf32.em." - * GAH. That means that what we specify here is not (completely) what - * needs to happen with these sections. *) - fun s -> name_matches ".gnu_warning" s)) - ]) - ; OutputSection(AlwaysOutput, None, ".fini", [ - InputQuery(KeepEvenWhenGC, SeenOrder, filter_and_concat (name_matches ".fini")) - ]) - ; DefineSymbol(ProvideIfUsed, "__etext", default_symbol_spec) - ; DefineSymbol(ProvideIfUsed, "_etext", default_symbol_spec) - ; DefineSymbol(ProvideIfUsed, "etext", default_symbol_spec) - ; OutputSection(AlwaysOutput, None, ".rodata", [ - InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".rodata" s || (name_matches ".rodata.*" s || name_matches ".gnu.linkonce.r.*" s) - ))]) - ; OutputSection(AlwaysOutput, None, ".eh_frame_hdr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame_hdr")) ]) - ; OutputSection(OnlyIfRo, None, ".eh_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame"))]) - ; OutputSection(OnlyIfRo, None, ".gcc_except_table", [InputQuery(DefaultKeep, DefaultSort, - filter_and_concat (fun s -> name_matches ".gcc_except_table" s || name_matches ".gcc_except_table.*" s))]) - ; OutputSection(OnlyIfRo, None, ".exception_ranges", [InputQuery(DefaultKeep, DefaultSort, - filter_and_concat (fun s -> name_matches ".exception_ranges" s || name_matches ".exception_ranges*" s))]) - ; AdvanceAddress(AddressExprFn alloc_fn2_ref) - ; MarkAndAlignDataSegment( Nat_big_num.mul (Nat_big_num.mul(Nat_big_num.of_int (* a.maxpagesize *)2)(Nat_big_num.of_int 1024))(Nat_big_num.of_int 1024) (* <-- for some reason binutils assumes 2MB max page size, - even if ABI says smaller *), a.commonpagesize) - ; OutputSection(OnlyIfRw, None, ".eh_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".eh_frame"))]) - ; OutputSection(OnlyIfRw, None, ".gcc_except_table", [InputQuery(DefaultKeep, DefaultSort, - filter_and_concat (fun s -> name_matches ".gcc_except_table" s || name_matches ".gcc_except_table.*" s))]) - ; OutputSection(OnlyIfRw, None, ".exception_ranges", [InputQuery(DefaultKeep, DefaultSort, - filter_and_concat (fun s -> name_matches ".exception_ranges" s || name_matches ".exception_ranges*" s))]) - ; OutputSection(AlwaysOutput, None, ".tdata", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat - (fun s -> name_matches ".tdata" s || (name_matches ".tdata.*" s || name_matches ".gnu.linkonce.td.*" s)))]) - ; OutputSection(AlwaysOutput, None, ".tbss", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat - (fun s -> name_matches ".tbss" s || (name_matches ".tbss.*" s || name_matches ".gnu.linkonce.tb.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".tcommon"))]) - ; OutputSection(AlwaysOutput, None, ".preinit_array", [ - DefineSymbol(ProvideIfUsed, "__preinit_array_start", default_symbol_spec) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> name_matches ".preinit_array" s)) - ; DefineSymbol(ProvideIfUsed, "__preinit_array_end", default_symbol_spec) - ]) - ; OutputSection(AlwaysOutput, None, ".init_array", [ - DefineSymbol(ProvideIfUsed, "__init_array_start", default_symbol_spec) - ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".init_array.*" s)) - ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".ctors.*" s)) - ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat - (fun s -> name_matches ".init_array" s - || (name_matches ".ctors" s && not (file_matches "*crtbegin.o" s || (file_matches "*crtbegin?.o" s - || (file_matches "*crtend.o" s || file_matches "*crtend?.o " s))))) - ) - ; DefineSymbol(ProvideIfUsed, "__init_array_end", default_symbol_spec) - ]) - ; OutputSection(AlwaysOutput, None, ".fini_array", [ - DefineSymbol(ProvideIfUsed, "__fini_array_start", default_symbol_spec) - ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".fini_array.*" s)) - ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat (fun s -> name_matches ".dtors.*" s)) - ; InputQuery(KeepEvenWhenGC, ByInitPriority, filter_and_concat - (fun s -> name_matches ".fini_array" s - || (name_matches ".dtors" s && not (file_matches "*crtbegin.o" s || (file_matches "*crtbegin?.o" s - || (file_matches "*crtend.o" s || file_matches "*crtend?.o " s))))) - ) - ; DefineSymbol(ProvideIfUsed, "__fini_array_end", default_symbol_spec) - ]) - ; OutputSection(AlwaysOutput, None, ".ctors", [ - InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin.o" s && name_matches ".ctors" s)) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin?.o" s && name_matches ".ctors" s)) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat - (fun s -> not (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".ctors" s)) - ; InputQuery(KeepEvenWhenGC, ByName, filter_and_concat (fun s -> name_matches ".ctors.*" s)) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat - (fun s -> (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".ctors" s)) - (* NOTE: this exclusion is implicit in the usual linker script, - * because it won't match an input section more than once. We should - * just replicate this behaviour, since other parts of the script might rely on it - * less obviously. *) - ]) - ; OutputSection(AlwaysOutput, None, ".dtors", [ - InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin.o" s && name_matches ".dtors" s)) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (fun s -> file_matches "*crtbegin?.o" s && name_matches ".dtors" s)) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat - (fun s -> not (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".dtors" s)) - ; InputQuery(KeepEvenWhenGC, ByName, filter_and_concat (fun s -> name_matches ".dtors.*" s)) - ; InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat - (fun s -> (file_matches "*crtend.o" s || file_matches "*crtend?.o" s) && name_matches ".dtors" s)) - ]) - ; OutputSection(AlwaysOutput, None, ".jcr", [InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (name_matches ".jcr"))]) - ; OutputSection(AlwaysOutput, None, ".data.rel.ro", [ - InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".data.rel.ro.local*" s || name_matches ".gnu.linkonce.d.rel.ro.local.*" s - )); - InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".data.rel.ro" s || (name_matches ".data.rel.ro.*" s || name_matches ".gnu.linkonce.d.rel.ro.*" s) - )) - ]) - ; OutputSection(AlwaysOutput, None, ".dynamic", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynamic"))]) - ; OutputSection(AlwaysOutput, None, ".got", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".got")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".igot")) - ]) - ; MarkDataSegmentRelroEnd (*(fun secs -> (if (sizeof ".got.plt" secs) >= 24 then 24 else 0, (fun pos -> pos)))*) - ; OutputSection(AlwaysOutput, None, ".got.plt", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".got.plt")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".igot.plt")) - ]) - ; OutputSection(AlwaysOutput, None, ".data", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".data" s || (name_matches ".data.*" s || name_matches ".gnu.linkonce.d.*" s))) - (* the script also has SORT(CONSTRUCTORS) here, but it has no effect for ELF (I think) *) - ]) - ; OutputSection(AlwaysOutput, None, ".data1", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".data1"))]) - ; DefineSymbol(AlwaysDefine, "_edata", default_symbol_spec) - ; DefineSymbol(ProvideIfUsed, "edata", default_symbol_spec) - ; (* . = .; <-- does this do anything? YES! It forces an output section to be emitted. - Since it occurs *outside* any output section, - it is assumed to start - *) - DefineSymbol(AlwaysDefine, "__bss_start", default_symbol_spec) - ; OutputSection(AlwaysOutput, None, ".bss", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynbss")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".bss" s || (name_matches ".bss.*" s || name_matches ".gnu.linkonce.b.*" s))) - ; InputQuery(DefaultKeep, DefaultSort, (fun inputlist -> - (*let _ = errln "Looking for commons" in *) - let result = (filter_and_concat is_common inputlist) - in - (*let _ = errln ("Got " ^ (show (length (result))) ^ " commons; sanity check: input list contains " ^ - (show (length inputlist)) ^ " of which " ^ - (show (length (List.filter (fun inp -> match inp with - Common _ -> true - | _ -> false - end) inputlist))) ^ " are commons." - ) - in*) result) - ) - ]) - ; AdvanceAddress(AddressExprFn alloc_fn3_ref) - ; OutputSection(AlwaysOutput, None, ".lbss", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynlbss")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".dynlbss")) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".lbss" s || (name_matches ".lbss.*" s || name_matches ".gnu.linkonce.lb.*" s) - )) - ; InputQuery(DefaultKeep, DefaultSort, filter_and_concat (is_large_common)) - ]) - ; AdvanceAddress(AddressExprFn alloc_fn4_ref) - ; AdvanceAddress(AddressExprFn alloc_fn5_ref) - ; OutputSection(AlwaysOutput, Some (AddressExprFn alloc_fn6_ref), - ".lrodata", - [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".lrodata" s || (name_matches ".lrodata.*" s || name_matches ".gnu.linkonce.lr.*" s) - )) - ; AdvanceAddress(AddressExprFn alloc_fn7_ref) - ]) - ; AdvanceAddress(AddressExprFn alloc_fn8_ref) - ; DefineSymbol(AlwaysDefine, "_end", default_symbol_spec) - ; DefineSymbol(ProvideIfUsed, "end", default_symbol_spec) - ; MarkDataSegmentEnd - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stabstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stabstr"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.excl", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.excl"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.exclstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.exclstr"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.index", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.index"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".stab.indexstr", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".stab.indexstr"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".comment", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".comment"))]) - (* DWARF debug sections. - Symbols in the DWARF debugging sections are relative to the beginning - of the section so we begin them at 0. *) - (* DWARF 1 *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".line", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".line"))]) - (* GNU DWARF 1 extensions *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_srcinfo", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_srcinfo"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_sfnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_sfname"))]) - (* DWARF 1.1 and DWARF 2 *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_aranges", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_aranges"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_pubnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_pubnames"))]) - (* DWARF 2 *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_info", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".debug_info" s || name_matches ".gnu.linkonce.wi.*" s))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_abbrev", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_abbrev"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_line", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat ( - fun s -> name_matches ".debug_line" s || (name_matches ".debug_line.*" s || name_matches ".debug_line_end" s)))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_frame", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_frame"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_str", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_str"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_loc", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_loc"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_macinfo", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_macinfo"))]) - (* SGI/MIPS DWARF 2 extensions *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_weaknames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_weaknames"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_funcnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_funcnames"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_typenames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_typenames"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_varnames", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_varnames"))]) - (* DWARF 3 *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_pubtypes", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_pubtypes"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_ranges", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_ranges"))]) - (* DWARF Extension. *) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".debug_macro", [InputQuery(DefaultKeep, DefaultSort, filter_and_concat (name_matches ".debug_macro"))]) - ; OutputSection(AlwaysOutput, Some address_zero_fn, ".gnu.attributes", [InputQuery(KeepEvenWhenGC, DefaultSort, filter_and_concat (name_matches ".gnu.attributes"))]) - ; DiscardInput(filter_and_concat (fun s -> name_matches ".note.GNU-stack" s || (name_matches ".gnu_debuglink" s || name_matches ".gnu.lto_*" s))) - (* NOTE: orphan sections are dealt with in the core linking logic, - not the script. *) - ])) - -let interpret_guard guard comp name1:bool= - ((match guard with - always0 -> true - | OnlyIfRo -> - let v = (List.for_all (fun comp_el -> (match comp_el with - IncludeInputSection(retainpol, (* fname, linkable_idx, shndx, isec, img *) irec) -> Nat_big_num.equal(Nat_big_num.of_int - (* is this section read-only? if it doesn't have shf_write, yes *)0) (Nat_big_num.bitwise_and irec.isec.elf64_section_flags shf_write) - | _ -> (* holes, common symbols and provided symbols shouldn't prevent ONLY_IF_RO *) true - )) comp) - in (*let _ = errln ("only_if_ro evaluated " ^ (show v) ^ " for output section " ^ name) - in*) v - | OnlyIfRw -> - let v = (List.for_all (fun comp_el -> (match comp_el with - IncludeInputSection(retainpol, (* fname, linkable_idx, shndx, isec, img *) irec) -> not (Nat_big_num.equal(Nat_big_num.of_int - (* is this section read-only? if it doesn't have shf_write, yes *)0) (Nat_big_num.bitwise_and irec.isec.elf64_section_flags shf_write)) - | _ -> (* holes etc. shouldn't prevent ONLY_IF_RW *) true - )) comp) - in (*let _ = errln ("only_if_rw evaluated " ^ (show v) ^ " for output section " ^ name) - in *)v - )) - -(* Passes over the script: - * - * 1. assign input sections to output sections (or discard) and define symbols. - * - * 2. compute def-use and optionally GC, removing unwanted sections and symbols - * - * 3. build image, assigning addresses as we go. - * - * Some passes require matching/retrieving what a previous pass on the same node did. - * So we give each script element a natural "idx" label. - *) -(*val label_script_aux : natural -> linker_control_script -> labelled_linker_control_script*) -let label_script_aux start script1:(script_element*Nat_big_num.num)list= - (mapi (fun i -> fun el -> (el, ( Nat_big_num.add start (Nat_big_num.of_int i)))) script1) - -(*val label_script : linker_control_script -> labelled_linker_control_script*) -let label_script script1:(script_element*Nat_big_num.num)list= (label_script_aux(Nat_big_num.of_int 0) script1) - -type input_output_assignment = ( input_spec list * (output_section_spec * Nat_big_num.num) list) - -(*val assign_inputs_to_output_sections : - input_output_assignment -> (* accumulator: list of discards, list of output compositions (these include symbols) *) - set (natural * natural) -> (* used sections *) - set (natural * natural * natural) -> (* used commons *) - list input_spec -> (* remaining inputs *) - maybe (output_section_spec * natural) -> (* cur_sec -- the current output section spec and its OutputSection script item idx *) - maybe input_spec -> (* last input section to be output -- might not have one *) - (input_spec -> input_spec -> Basic_classes.ordering) (* "seen ordering" *) -> - labelled_linker_control_script -> - input_output_assignment*) (* accumulated result *) -let rec assign_inputs_to_output_sections acc used_sections used_commons inputs (cur_output_sec : (output_section_spec * Nat_big_num.num)option) last_input_sec seen_ordering script1:(input_spec)list*(output_section_spec*Nat_big_num.num)list= - (let (rev_discards, rev_outputs) = acc in - let flush_output_sec - = (fun maybe_output_sec_and_idx -> (match (maybe_output_sec_and_idx : (output_section_spec * Nat_big_num.num)option) with - Some (OutputSectionSpec (guard, addr, name1, comp), script_idx) -> - (*let _ = errln ("Guardedly flushing output section named " ^ name ^ " with " ^ ( - match addr with Nothing -> "no address yet" | Just a -> "address 0x" ^ (hex_string_of_natural a) end - ) ^ " and composed of " ^ (show (length comp)) ^ " constituents.") - in*) - (* evaluate the guard *) - if interpret_guard guard comp name1 - then (* do it *) (rev_discards, (((OutputSectionSpec (guard, addr, name1, comp)), script_idx) :: rev_outputs)) - else (* ignore it *) acc - | None -> (* for convenience, make this a no-op rather than error *) - (* failwith "internal error: flushing output section with no current output section" *) - acc - )) - in - (match script1 with - [] -> flush_output_sec cur_output_sec - | (element1, idx1) :: more_elements_and_idx -> - let do_nothing = (acc, used_sections, used_commons, cur_output_sec, last_input_sec) - in - let (new_acc, new_used_sections, new_used_commons, (new_cur_output_sec : (output_section_spec * Nat_big_num.num)option), new_last_input_sec) - = ((match element1 with - DefineSymbol(symdefpol, name1, (symsize, syminfo, symother)) -> - (* Label the current section in the image - * with a new symbol definition. If there isn't - * a current section, use the ABS section (what is that labelling?). *) - (acc, - used_sections, - used_commons, - (match (cur_output_sec : (output_section_spec * Nat_big_num.num)option) with - None -> (*let _ = errln ("FIXME: for defining `" ^ name ^ "': ABS symbol defs not yet supported") in*) None - | Some ((OutputSectionSpec (guard, maybe_addr, secname1, comp)), output_script_idx) -> - (*let _ = errln ("Including a symbol named `" ^ name ^ " in composition of output section `" ^ secname ^ "'") in*) - Some ((OutputSectionSpec (guard, maybe_addr, secname1, - List.rev_append (List.rev comp) [ProvideSymbol(symdefpol, name1, (symsize, syminfo, symother))])) - , output_script_idx) - ), - last_input_sec) - | AdvanceAddress(AddressExprFn advance_fn) -> - (* If we're inside a section, insert a hole, - * else just update the logical address *) - (*let _ = errln ("Advancing location counter") in*) - (match cur_output_sec with - None -> do_nothing - (* This assignment is setting a new LMA. *) - (* (acc, *) - | Some (sec, idx1) -> do_nothing - ) - | MarkAndAlignDataSegment(maxpagesize1, commonpagesize1) -> - (* The "data segment end" is a distinguished label, - * so we can encode the whole thing into a conditional. *) - (*let _ = errln ("Mark/aligning data segment") in*) - do_nothing - | MarkDataSegmentEnd -> - (*let _ = errln ("Marking data segment end") in*) - do_nothing - | MarkDataSegmentRelroEnd(*(fun_from_secs_to_something)*) -> - (*let _ = errln ("Marking data segment relro end") in*) - do_nothing - | OutputSection(outputguard, maybe_expr, name1, sub_elements) -> - (* If we have a current output section, finish it and add it to the image. - * Q. Where do guards ("ONLY_IF_RO" etc) get evaluated? - * A. Inside flush_output_sec. *) - (*let _ = errln ("Recursively composing a new output section `" ^ name ^ "'...") in*) - let acc_with_output_sec = (flush_output_sec cur_output_sec) - in - let new_cur_output_sec = (Some((OutputSectionSpec(outputguard, (* maybe_expr pos secs *) None, name1, [])), idx1)) - in - (* Recurse down the list of input queries, assigning them to this output sec - * Note that output sections may not nest within other output sections. - * At the end of the list of sub_elements, we will flush the section we built up. - *) - let final_acc - = (assign_inputs_to_output_sections acc used_sections used_commons inputs new_cur_output_sec last_input_sec seen_ordering (label_script sub_elements)) - in - (* NOTE that this sub-accumulation will never add a new output section - * because output sections can't nest. *) - (final_acc, used_sections, used_commons, (* cur_output_sec *) None, last_input_sec) - | DiscardInput(selector) -> - let selected = (selector inputs) - in - let (rev_discards, rev_outputs) = acc in - (*let _ = Missing_pervasives.errln ("Processing discard rule; selected " ^ (show (length selected)) - ^ " inputs.") - in*) - (( List.rev_append (List.rev (List.rev (let x2 = - ([]) in List.fold_right (fun i x2 -> if true then i :: x2 else x2) selected x2))) rev_discards, rev_outputs), used_sections, used_commons, cur_output_sec, last_input_sec) - | InputQuery(retainpol, sortpol, selector) -> - (* Input queries can only occur within an output section. *) - (match cur_output_sec with - None -> failwith "linker script error: input query without output section" - | Some ((OutputSectionSpec (output_guard1, output_sec_addr, output_sec_name, output_composition)), output_script_idx) -> - (* Add them to the current output spec. We have to be careful about ordering: - * according to the GNU ld manual (and observed behaviour), by default - * "the linker will place files and sections matched by wildcards in the order - * in which they are seen during the link". For .o files on the command line, - * this means the command line order. But for members of archives, it means - * the order in which they were "pulled in" during input enumeration. We - * actually don't compute this here; it is passed in from our caller in link.lem. *) - let sortfun = ((match sortpol with - DefaultSort -> List.sort seen_ordering (* FIXME: pay attention to command line *) - | SeenOrder -> List.sort seen_ordering - | ByName -> List.sort compareInputSpecByName - | ByNameThenAlignment -> List.sort compareInputSpecByNameThenAlignment - | ByAlignment -> List.sort compareInputSpecByAlignment - | ByAlignmentThenName -> List.sort compareInputSpecByAlignmentThenName - | ByInitPriority -> List.sort compareInputSpecByInitPriority - )) - in - let selected = (selector inputs) - in - let selected_deduplicated = (List.filter (fun inp -> (match inp with - InputSection(irec) -> not ( Pset.mem(irec.idx, irec.shndx) used_sections) - | Common(idx1, fname1, img2, def) -> not ( Pset.mem(idx1, def.def_sym_scn, def.def_sym_idx) used_commons) - )) selected) - in - (*let _ = errln ("Evaluated an input query, yielding " ^ - (show (length selected)) ^ " undeduplicated and " ^ - (show (length selected_deduplicated)) ^ - " deduplicated results, to be added to composition currently of " ^ - (show (length output_composition)) ^ " items.") in*) - (* Search input memory images for matching sections. *) - let sorted_selected_inputs = (sortfun selected_deduplicated) - in - let (sectionMatchList : input_section_rec list) = (Lem_list.mapMaybe (fun inp -> - (match inp with - InputSection(x) -> - (*let _ = errln ("Matched an input section named " ^ x.isec.elf64_section_name_as_string ^ - " in a file " ^ x.fname ^ " with first 20 bytes " ^ (show (take 20 - (let maybe_elname = elf_memory_image_element_coextensive_with_section x.shndx x.img - in - match maybe_elname with - Nothing -> failwith ("impossible: no such element (matching shndx " ^ (show x.shndx) ^ ")") - | Just idstr -> - match Map.lookup idstr x.img.elements with - Just el -> el.contents - | Nothing -> failwith "no such element" - end - end - )))) - in*) - Some x - | _ -> None - )) sorted_selected_inputs) - in - let commonMatchList = (Lem_list.mapMaybe (fun inp -> - (match inp with - | Common(idx1, fname1, img2, def) -> Some(idx1, fname1, img2, def) - | _ -> None - )) sorted_selected_inputs) - in - - (acc, - Pset.(union) used_sections (let x2 =(Pset.from_list (pairCompare Nat_big_num.compare Nat_big_num.compare) - []) in List.fold_right - (fun irec x2 -> if true then Pset.add (irec.idx, irec.shndx) x2 else x2) - sectionMatchList x2), - Pset.(union) used_commons (let x2 =(Pset.from_list (tripleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare) - []) in List.fold_right - (fun(idx1, fname1, img2, def) x2 -> - if true then Pset.add (idx1, def.def_sym_scn, def.def_sym_idx) x2 else x2) - commonMatchList x2), - (* new_cur_output_spec *) Some ( - (OutputSectionSpec(output_guard1, output_sec_addr, output_sec_name, - List.rev_append (List.rev (List.rev_append (List.rev output_composition) (let x2 = - ([]) in List.fold_right - (fun input_sec x2 -> - if true then - IncludeInputSection - (retainpol, (* input_sec.fname, input_sec.idx, input_sec.shndx, input_sec.isec, input_sec.img *) input_sec) - :: x2 else x2) sectionMatchList x2))) (let x2 = ([]) in List.fold_right - (fun(idx1, fname1, img2, def) x2 -> - if true then - IncludeCommonSymbol (DefaultKeep, fname1, idx1, def, img2) :: x2 else - x2) commonMatchList x2) - )), output_script_idx), - last_input_sec - ) - ) - )) - in - (*let _ = match new_cur_output_sec with - Just (OutputSectionSpec (guard, addr, name, comp), script_idx) -> - errln ("Now output section `" ^ name ^ "' is composed of " ^ (show (length comp)) ^ " elements.") - | Nothing -> () - end in*) - assign_inputs_to_output_sections new_acc new_used_sections new_used_commons - (inputs : input_spec list) - (new_cur_output_sec) - (new_last_input_sec : input_spec option) - seen_ordering - (more_elements_and_idx : labelled_linker_control_script) - )) - -(* NOTE: this is also responsible for deleting any PROVIDEd symbols that - * were not actually referenced. BUT HOW, if we haven't built the image and - * hence haven't added the symbols yet? Symbols affect reachability, so - * we're going to have to figure this out. Really we want a memory image that - * does not yet have addresses assigned, but does have the symbols inserted. - * BUT even that is not right, because we want to be able to remove some - * sections (GC them). So the section composition is not yet fixed. So we have - * a problem. - * - * Note that the only symbols we have to remove are ones that were PROVIDEd - * in our output composition. So doing the GC on output compositions seems - * sane. We can get the graph's edge list by inspecting the constituent memory - * images from which each output section composition element is drawn. - * Collecting sections and collecting symbols seems fair. Note that symbols - * can never be placed mid-section (I don't think?? they can use arbitrary - * expressions, but not that depend on whether an input section is included - * or not) so removing a section should never imply the removal of a symbol. - * - * So that implies we need not yet build a memory image. - *) -(*val compute_def_use_and_gc : allocated_sections_map -> allocated_sections_map*) -let compute_def_use_and_gc outputs_by_name:allocated_sections_map= outputs_by_name (* FIXME: implement GC *) - -let output_section_type comp:Nat_big_num.num= -( - (* are we composed entirely of nobits sections and common symbols? *)let all_nobits = (List.for_all (fun comp_el -> - (match comp_el with - IncludeInputSection(retain_pol,(* fname, linkable_idx, shndx, isec, img *) irec) -> Nat_big_num.equal - irec.isec.elf64_section_type sht_nobits - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> true - | _ -> (* padding and symdefs can be nobits *) true - )) comp) - in - if all_nobits then sht_nobits else sht_progbits) - -let output_section_flags comp:Nat_big_num.num= - (let writable = (List.exists (fun comp_el -> - (match comp_el with - IncludeInputSection(retain_pol, (* fname, linkable_idx, shndx, isec, img *) irec) -> - flag_is_set shf_write irec.isec.elf64_section_flags - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> - (* assume common symbols are writable *) true - | _ -> (* padding and symdefs do not make a section writable *) false - )) comp) - in - let executable = (List.exists (fun comp_el -> - (match comp_el with - IncludeInputSection(retain_pol,(* fname, linkable_idx, shndx, isec, img *) irec) -> - flag_is_set shf_execinstr irec.isec.elf64_section_flags - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> - (* assume common symbols are not executable, since they're zeroed *) false - | _ -> (* padding and symdefs do not make a section executable -- HMM *) false - )) comp) - in - let alloc = (List.exists (fun comp_el -> - (match comp_el with - IncludeInputSection(retain_pol, (* fname, linkable_idx, shndx, isec, img *) irec) -> - flag_is_set shf_alloc irec.isec.elf64_section_flags - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> - (* common symbols are allocatable *) true - | ProvideSymbol(pol, name1, spec) -> - (* symbols make a section allocatable? HMM *) true - | _ -> (* padding does not make a section allocatable *) false - )) comp) - in - let is_thread_local_yesnomaybe = (fun comp_el -> - (match comp_el with - IncludeInputSection(retain_pol, (* fname, linkable_idx, shndx, isec, img *) irec) -> - Some(flag_is_set shf_tls irec.isec.elf64_section_flags) - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> - (* FIXME: support tcommon *) Some(false) - | ProvideSymbol(pol, name1, spec) -> - (* linker script symbols shouldn't be defined here, unless they can be declared thread-local (FIXME: can they?) *) - Some false - | _ -> (* padding does not make a section thread-local, or non-. *) None - ) - ) - in - let thread_local = ( - (* Is any element positively thread-local? *) - let v = (List.fold_left (fun acc_ynm -> fun comp_el -> - let new_ynm = (is_thread_local_yesnomaybe comp_el) - in - (match (acc_ynm, new_ynm) with - (None, None) -> None - | (None, Some x) -> Some x - | (Some x, None) -> Some x - | (Some true, Some false) -> Some true - | (Some true, Some true) -> Some true - | (Some false, Some false) -> Some false - | (Some true, Some false) -> Some true - )) None comp) - in - if (Lem.option_equal (=) v (Some(true))) && not ( (Lem.option_equal (=)(Some(true)) (* are *all* either don't-care or positively thread-local? *) - (List.fold_left (fun acc_ynm -> fun comp_el -> - let new_ynm = (is_thread_local_yesnomaybe comp_el) - in - (match (acc_ynm, new_ynm) with - (None, None) -> None - | (None, Some x) -> Some x - | (Some x, None) -> Some x - | (Some true, Some false) -> Some false - | (Some true, Some true) -> Some true - | (Some false, Some false) -> Some false - | (Some true, Some false) -> Some false - )) None comp))) then failwith "error: section mixes thread-local and non-thread-local inputs" - else (match v with - None -> false - | Some x -> x - ) - ) - in - Nat_big_num.bitwise_or - (if thread_local then shf_tls else Nat_big_num.of_int 0) - (Nat_big_num.bitwise_or - (if executable then shf_execinstr else Nat_big_num.of_int 0) - (Nat_big_num.bitwise_or - (if writable then shf_write else Nat_big_num.of_int 0) - (if alloc then shf_alloc else Nat_big_num.of_int 0) - ) - )) - -let symbol_def_for_provide_symbol name1 size2 info other control_script_linkable_idx:symbol_definition= - ({ - def_symname = (*let _ = errln ("Linker script is defining symbol called `" ^ name ^ "'") in*) name1 - ; def_syment = ({ - elf64_st_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* ignored *) - ; elf64_st_info = info - ; elf64_st_other = other - ; elf64_st_shndx = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_value = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* ignored *) - ; elf64_st_size = (Uint64.of_string (Nat_big_num.to_string size2)) - }) - ; def_sym_scn =(Nat_big_num.of_int 0) - ; def_sym_idx =(Nat_big_num.of_int 0) - ; def_linkable_idx = control_script_linkable_idx - }) - -(*val assign_dot_to_itself : natural -> address_expr_fn_map allocated_sections_map -> (natural * address_expr_fn_map allocated_sections_map * address_expr_fn)*) -let assign_dot_to_itself fresh alloc_map:Nat_big_num.num*((Nat_big_num.num),(Nat_big_num.num ->allocated_sections_map ->Nat_big_num.num))Pmap.map*address_expr_fn= - (let fn = (fun dot -> fun _ -> dot) in - let alloc_map' = (Pmap.add fresh fn alloc_map) in - let fresh' = (Nat_big_num.add(Nat_big_num.of_int 1) fresh) in - (fresh', alloc_map', AddressExprFn fresh)) - -(*val build_image : - address_expr_fn_map allocated_sections_map -> (* global dictionary of address_expr_fn_ref -> address_expr_fn *) - elf_memory_image -> (* accumulator *) - natural -> (* location counter *) - allocated_sections_map -> (* outputs constructed earlier *) - (Map.map string (list (natural * binding))) -> (* bindings_by_name *) - labelled_linker_control_script -> - natural -> (* control_script_linkable_idx *) - (Map.map string (list symbol_definition)) -> (* linker_defs_by_name *) - (elf_memory_image * allocated_sections_map)*) (* accumulated result *) -let rec build_image alloc_map acc pos (AllocatedSectionsMap outputs_by_name) bindings_by_name script1 control_script_linkable_idx linker_defs_by_name:(any_abi_feature)annotated_memory_image*allocated_sections_map= - (let (add_output_section : (Nat_big_num.num * elf_memory_image) -> output_section_spec -> (Nat_big_num.num * elf_memory_image * Nat_big_num.num * output_section_spec)) - = (fun ((*scn_idx, *)pos, acc_img) -> - (fun (OutputSectionSpec (guard, addr, secname1, comp)) -> - (*let _ = errln ("Computing composition of output section `" ^ secname ^ "' from " ^ (show (length comp)) ^ " elements") - in*) - let unaligned_start_addr = ((match addr with - Some a -> failwith ("internal error: section " ^ (secname1 ^ ": did not expect address to be assigned yet")) - | None -> pos - )) - in - let align = (alignof_output_section comp) - in - (*let _ = errln ("Aligning start of output section " ^ secname ^ " up to a " ^ (show align) ^ "-byte address boundary") - in*) - let output_section_start_addr = (align_up_to align unaligned_start_addr) - in - let (end_addr, comp_addrs) = (do_output_section_layout_starting_at_addr output_section_start_addr (AllocatedSectionsMap outputs_by_name) comp) - in - let size2 = (Nat_big_num.sub_nat end_addr output_section_start_addr) - in - (*let _ = Missing_pervasives.outln ( - if List.null comp then secname else ( - ((space_padded_and_maybe_newline 16 secname) ^ - ("0x" ^ (left_zero_padded_to 16 (hex_string_of_natural output_section_start_addr))) ^ " " ^ - (left_space_padded_to 10 ("0x" ^ (hex_string_of_natural size)))) - ) - ) - in*) - let (concatenated_content, final_addr, new_range_tag_pairs) = (List.fold_left (fun (accum_pat, accum_current_addr, accum_meta) -> (fun (comp_el, comp_addr) -> - (*let _ = errln ("Adding an element to composition of output section `" ^ secname ^ "', current address 0x" ^ (hex_string_of_natural accum_current_addr)) - in*) - let make_line = (fun namestr -> (fun addrstr -> (fun szstr -> (fun rhs -> ( - (space_padded_and_maybe_newline(Nat_big_num.of_int 16) (" " ^ namestr)) ^ - (("0x" ^ (left_zero_padded_to(Nat_big_num.of_int 16) addrstr)) ^ (" " ^ - ((left_space_padded_to(Nat_big_num.of_int 10) ("0x" ^ szstr)) ^ (" " ^ rhs)))) - ))))) - in - let (sz, comp_el_pat, this_el_meta) = ((match comp_el with - | IncludeInputSection(retainpolicy, (* fname, linkable_idx, shndx, isec, img *) irec) -> - (* We want to get the input section as a byte pattern *) - (*let _ = errln ("Processing inclusion of input section `" ^ irec.isec.elf64_section_name_as_string - ^ "' from file `" ^ irec.fname - ^ "' into output section `" ^ secname - ^ "'") - in*) - let maybe_secname = (elf_memory_image_element_coextensive_with_section irec.shndx irec.img) - in - (match maybe_secname with - None -> failwith ("impossible: no such section" (*(matching irec.shndx " ^ (show irec.shndx) ^ ")""*)) - | Some idstr -> - (*let _ = errln ("Found element named " ^ idstr ^ " coextensive with section named " ^ - irec.isec.elf64_section_name_as_string ^ " in file " ^ irec.fname) - in*) - (match Pmap.lookup idstr irec.img.elements with - Some el -> - (*let _ = Missing_pervasives.outln (make_line irec.isec.elf64_section_name_as_string - (hex_string_of_natural comp_addr) (hex_string_of_natural irec.isec.elf64_section_size) - irec.fname) - in*) - let section_el_name = (get_unique_name_for_section_from_index irec.shndx irec.isec irec.img) - in - (*let _ = errln ("Copying metadata for output section `" ^ section_el_name ^ "'") in*) - let range_or_sym_is_in_this_sec = (fun maybe_range -> (fun tag -> - (* is it within the section we're outputting? - * first we needs its element name. *) - (* filter out ones that don't overlap *) - (match maybe_range with - Some(el_name, (start, len)) -> - (* img and shndx came as a unit, so they're definitely - * talking about the same file *) - (* shndx = sym_shndx *) - section_el_name = el_name - | None -> - (* ABS symbols have this property *) - (match tag with - SymbolDef(def) -> - (* don't match section symbols, or we'll be inundated *) - let sym_shndx = (Nat_big_num.of_string (Uint32.to_string def.def_syment.elf64_st_shndx)) - in - if not (Nat_big_num.equal sym_shndx shn_abs) || ( not (Nat_big_num.equal (get_elf64_symbol_type def.def_syment) stt_section)) then false - else ( - let abs_address = (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_value) - in - (* check it against our section *) - let section_end_addr = (Nat_big_num.add accum_current_addr irec.isec.elf64_section_size) - in - ( Nat_big_num.greater_equal abs_address accum_current_addr - && Nat_big_num.less abs_address section_end_addr) - (* FIXME: argument that this should be <=, i.e. can mark end addr *) - (* PROBLEM: this is all very well, but there's no reason why - * ABS symbols need to point at an address within some output - * section. They can just be arbitrary values. This is a bit of an - * abuse if we do it within the C language (to get the value, you - * have to do "(int) &sym", i.e. create a meaningless pointer - * intermediate) but arguably is okay in an impl-def way. - * - * WHAT to do? well, just always output the ABS symbols, for now. - * - * The example that provoked this is in glibc's - * locale/lc-address.c, which compiles down to create - * the following ABS symbol: - * - * 0000000000000001 g *ABS* 0000000000000000 _nl_current_LC_ADDRESS_used - * - * ... i.e. the _nl_current_LC_ADDRESS_used appears to be just a flag. - * - * Where can we handle this? We don't see ABS symbols since they - * aren't associated with sections. We simply need to copy over - * all the ABS symbols appearing in included input objects. - * That means there's no point doing anything with them here - * while we're fiddling with sections. Do it later in a whole- - * -image pass. - *) - && false (* ... at least until we see a better way *) - ) - | _ -> false - ) - ) - )) - in - let ranges_and_tags = (let x2 = - ([]) in List.fold_right - (fun(maybe_range, tag) x2 -> - if range_or_sym_is_in_this_sec maybe_range tag then - (maybe_range, tag) :: x2 else x2) (Pset.elements irec.img.by_range) - x2) - in - let included_defs = (let x2 = - ([]) in List.fold_right - (fun(maybe_range, def) x2 -> - if range_or_sym_is_in_this_sec maybe_range (SymbolDef (def)) then - def :: x2 else x2) - (elf_memory_image_defined_symbols_and_ranges irec.img) x2) - in - let included_global_defs = (let x2 = - ([]) in List.fold_right - (fun def x2 -> - if not - (Nat_big_num.equal - ( - (* filter out locals *) get_elf64_symbol_binding def.def_syment) - stb_local) then def :: x2 else x2) included_defs x2) - in - (* What symbol defs are being included? *) - (* For each global symbol defined in the section, output a line. *) - (*let _ = Missing_pervasives.outs (List.foldl (^) "" ( - List.map (fun def -> (make_line "" - (hex_string_of_natural (comp_addr + (natural_of_elf64_addr def.def_syment.elf64_st_value))) - (hex_string_of_natural (natural_of_elf64_xword def.def_syment.elf64_st_size)) - (" " ^ def.def_symname)) ^ "\n" - ) included_global_defs - )) - in*) - let (new_ranges_and_tags : (( element_range option) * ( any_abi_feature range_tag)) Pset.set) - = (Lem_set.setMapMaybe - (instance_Basic_classes_SetType_tup2_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))) - instance_Basic_classes_SetType_var_dict) (instance_Basic_classes_SetType_tup2_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))) - instance_Basic_classes_SetType_var_dict) (fun (maybe_range, tag) -> - (* How do we update existing metadata? In general, - * we get a new range. *) - let new_range = ((match maybe_range with - None -> None - | Some(el_name, (start, len)) -> - Some(secname1, -( (* FIXME: pass this through a section-to-element gensym. - We can just (for now) define output element names - to equal the section names, since we have no unnamed - output sections and no output common symbols. *)let new_start_off = (Nat_big_num.add start ( Nat_big_num.sub_nat comp_addr output_section_start_addr)) - in - (*let _ = errln ("Calculated element offset 0x" ^ (hex_string_of_natural new_start_off) ^ - " in element " ^ secname ^ " for tag at address 0x" ^ (hex_string_of_natural accum_current_addr) ^ - " , start offset 0x" ^ (hex_string_of_natural start) ^ ", output section start addr 0x" ^ - (hex_string_of_natural output_section_start_addr) ^ ", comp_addr 0x" ^ (hex_string_of_natural comp_addr)) - in*) - (new_start_off, - len))) - )) - in - (match tag with - (* If it's a section, we discard it. - * We will add a new section record at the end. (FIXME) *) - | FileFeature(ElfSection(idx1, isec1)) -> None - (* If it's a symbol def, we propagate it. - * We record its linkable idx, so we can - * match it later with the bindings we formed - * earlier. - * FIXME: this is a bit nasty. Perhaps we - * should replace syment with a minimal structure - * that avoids duplication. Same for isecs. *) - | SymbolDef(def) -> - (* if get_elf64_symbol_type def.def_syment = stt_section - then Nothing FIXME: also re-create the section symbol when we create the ElfSection - else *) (* This doesn't work -- some refs might be bound to this symbol. - Instead, strip the symbol when we generate the output symtab (FIXME). *) - (*let _ = errln ("Copying symbol named `" ^ def.def_symname ^ "'") - in*) - Some(new_range, SymbolDef({ - 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 = (irec.idx) - })) - | AbiFeature(x) -> Some(new_range, AbiFeature(x)) - (* If it's a symbol ref with no reloc site, we discard it? *) - | SymbolRef(r) -> - (*let _ = if r.ref.ref_symname = "_start" then errln ("Saw ref to _start, " - ^ "in section " ^ irec.isec.elf64_section_name_as_string ^ " of linkable " ^ (show irec.idx)) - else () - in*) - let get_binding_for_ref = (fun symref -> (fun linkable_idx -> (fun fname1 -> - let name_matches1 = ((match Pmap.lookup symref.ref_symname bindings_by_name with Some x -> x | None -> [] )) - in - (match List.filter (fun (bi, ((r_idx, r, r_item), m_d)) -> Nat_big_num.equal r_idx linkable_idx && (r = symref)) name_matches1 with - [(b_idx, b)] -> (b_idx, b) - | [] -> failwith "no binding found" - | _ -> failwith ("ambiguous binding found for symbol `" ^ (symref.ref_symname ^ ("' in file " ^ fname1))) - ) - ))) - in - let (bi, b) = (get_binding_for_ref r.ref irec.idx irec.fname) - in - let ((ref_idx, ref1, ref_linkable), maybe_def) = b - in - (match r.maybe_reloc with - None -> None - (* If it's a reloc site, we need to somehow point it - * at the *definition* that it was bound to. YES. - * reloc_sites are - - type reloc_site = <| - ref_relent : elf64_relocation_a - ; ref_rel_scn : natural --the relocation section idx - ; ref_rel_idx : natural --the index of the relocation rec - ; ref_src_scn : natural --the section *from which* the reference logically comes - |> - - type elfNN_relocation_a = - <| elfNN_ra_offset : elf32_addr --Address at which to relocate - ; elfNN_ra_info : elf32_word --Symbol table index/type of relocation to apply - ; elfNN_ra_addend : elf32_sword --Addend used to compute value to be stored - |> - - * ... of which ref_src_scn, ref_rel_idx, - * ref_rel_scn and elfNN_ra_offset can be ignored. - * - * What *is* important is that we somehow point at - * the symbol definition (or perhaps *un*definition, - * if we're generating a shared library) that it - * refers to. - * - * For that, we update ra_info use the 1 + binding_idx, - * i.e. consider that there is a fresh symbol table - * and that it has a distinct entry for each binding. - * - * FIXME: we also need to account for - * reloc decisions -- MakePIC etc. - *) - | Some(rs) -> Some(new_range, SymbolRef( - { ref = ({ - (* This is not the place to be fixing up - * symbol references. We can't yet patch the element content, - * because we haven't yet decided on the address of everything. - * - * That said, we *do* need to represent the old ref in the new - * linked-image context. That's *all* we should be doing, right now. - * - *) - ref_symname = (ref1.ref_symname) - ; ref_syment = - ({ elf64_st_name = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* unused *) - ; elf64_st_info = (ref1.ref_syment.elf64_st_info) - ; elf64_st_other = (ref1.ref_syment.elf64_st_other) - ; elf64_st_shndx = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int (* shn_abs *)0))) - ; elf64_st_value = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - ; elf64_st_size = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) - }) - ; ref_sym_scn =(Nat_big_num.of_int 0) - ; ref_sym_idx =(Nat_big_num.of_int 0) - (* match maybe_def with Just _ -> 1+bi | Nothing -> 0 end *) - }) - ; maybe_reloc = (Some { - ref_relent = ({ - elf64_ra_offset = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) (* ignored *) - ; elf64_ra_info = (Uint64.logor - (* HACK: use bi as the symbol index. *) - (Uint64.of_string (Nat_big_num.to_string (get_elf64_relocation_a_type rs.ref_relent))) - (Uint64.shift_left - (* ... actually, don't, now we have maybe_def_bound_to *) - (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int (* (1+bi) *)0)))( 32) - ) - ) - ; elf64_ra_addend = (rs.ref_relent.elf64_ra_addend) - }) - ; ref_rel_scn =(Nat_big_num.of_int 0) - ; ref_rel_idx =(Nat_big_num.of_int 0) - ; ref_src_scn =(Nat_big_num.of_int 0) - }) - ; maybe_def_bound_to = -( - (* Re-search the bindings list for a match, because we might have - * re-bound this symbol since we created the image. FIXME: since - * we do this, is there anything gained from populating this field - * earlier? Probably best not to. *)let (possible_bindings : (Nat_big_num.num * binding) list) - = ((match Pmap.lookup ref1.ref_symname bindings_by_name with - Some l -> if ref1.ref_symname = "__fini_array_end" then - (*let _ = errln ("Found " ^ (show (length l)) ^ " bindings for __fini_array_end, of which " ^ - (show (length (List.filter (fun (bi, (r, maybe_d)) -> maybe_d <> Nothing) l))) ^ - " are with definition") - in*) l - else l - | None -> [] - )) - in - (* what's the actual binding? *) - (match r.maybe_def_bound_to with - None -> failwith ("at this stage, all references must have a decision: `" ^ (ref1.ref_symname ^ "'")) - | Some(decision, _) -> - (* Search the list of bindings for a possibly-updated - * binding for this reference. *) - let matching_possibles = (List.filter (fun (bi, ((ref_idx, ref1, ref_item), maybe_d)) -> - (match maybe_d with - None -> false - | Some (def_idx, def, def_item) -> Nat_big_num.equal - (* match the *reference*, whose linkable we're processing now *) - irec.idx ref_idx - && (Nat_big_num.equal r.ref.ref_sym_scn ref1.ref_sym_scn - && Nat_big_num.equal r.ref.ref_sym_idx ref1.ref_sym_idx) - - (* - def.def_syment = sd.def_syment - && def.def_sym_scn = sd.def_sym_scn - && def.def_sym_idx = sd.def_sym_idx - && def_idx = sd.def_linkable_idx *) - ) - ) possible_bindings) - in - (*let _ = errln ("For a ref to `" ^ ref.ref_symname ^ - "', possibles list is: " ^ ( - List.foldl (fun x -> fun y -> x ^ ", " ^ y) "" (List.map (fun (bi, ((_, _, _), maybe_d)) -> - match maybe_d with - Just(def_idx, def, def_item) -> - "`" ^ def.def_symname ^ "' " ^ - "in linkable " ^ (show def_idx) ^ - ", section " ^ (show def.def_sym_scn) ^ - ", sym idx " ^ (show def.def_sym_idx) - | _ -> failwith "impossible: just filtered out no-def bindings" - end - ) matching_possibles) - )) - in*) - let new_bound_to = ((match matching_possibles with - [] -> Some(ApplyReloc, None) - | [(bi, ((rl, r, ri), maybe_d))] -> - Some(decision, - (match maybe_d 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 - )) - | _ -> failwith ("After linker script, ambiguous bindings for `" ^ (ref1.ref_symname ^ "'")) - )) - in - if not ((Lem.option_equal (Lem.pair_equal (=) (Lem.option_equal (=))) new_bound_to r.maybe_def_bound_to)) then - (*let _ = errln ("Changed binding for reference to `" ^ ref.ref_symname ^ - "' in linkable " ^ (show irec.idx)) - in*) - new_bound_to - else if (Lem.option_equal (Lem.pair_equal (=) (Lem.option_equal (=))) new_bound_to None) then failwith "really need a decision by now" - else new_bound_to - )) - - (* if irec.fname = "libc.a(__uClibc_main.os)" - && irec.isec.elf64_section_name_as_string = ".data.rel.local" - then - let _ = errln ("Saw the bugger: " ^ (match r.maybe_def_bound_to with - Just(decision, Just(sd)) -> show sd.def_syment - | _ -> "(not complete)" - end)) - in r.maybe_def_bound_to - else r.maybe_def_bound_to - *) - } - )) - ) (* match maybe_reloc *) - ) (* match tag *) - ) ((Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) ranges_and_tags))) (* end mapMaybe fn *) - in - let isec_sz = (irec.isec.elf64_section_size) in - let maybe_el_sz = (el.length1) in - let contents_sz = (length el.contents) in - let (actual_sz, padded_contents) = - ((match maybe_el_sz with - Some el_sz -> - let diff = (Nat_big_num.sub_nat el_sz contents_sz) in - if Nat_big_num.less diff(Nat_big_num.of_int 0) then - (* contents greater than what the el says, so chop the end off *) - (*let _ = Missing_pervasives.errln ("Warning: size mismatch for section " ^ irec.isec.elf64_section_name_as_string ^ - " from " ^ irec.fname) - in*) - (el_sz, take0 el_sz el.contents) - else (el_sz, List.rev_append (List.rev el.contents) (replicate0 diff None)) - | None -> - if not (Nat_big_num.equal (length el.contents) isec_sz) - then failwith "input section size not equal to its content pattern length" - else (isec_sz, el.contents) - )) - in - (*let _ = errln ("Saw first 20 bytes of section " ^ irec.isec.elf64_section_name_as_string ^ - " from " ^ irec.fname ^ " as " ^ (show (take 20 padded_contents))) - in*) - (actual_sz, padded_contents, new_ranges_and_tags) - | _ -> failwith "impossible: no such element" - ) (* match Map.lookup idstr img.elements *) - ) (* match maybe_secname *) - | IncludeCommonSymbol(retain_pol, fname1, linkable_idx, def, img2) -> - (*let _ = errln ("Including common symbol called `" ^ def.def_symname ^ "'") - in*) - (* We want to get the common symbol as a byte pattern *) - let sz = (Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_size) - in - let content = (Missing_pervasives.replicate0 sz (Some(Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 0))))) - in - (*let _ = Missing_pervasives.outln (make_line "COMMON" (hex_string_of_natural comp_addr) - (hex_string_of_natural sz) fname) - in*) - (sz, content,(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [(Some(secname1, ( Nat_big_num.sub_nat comp_addr output_section_start_addr, sz)), SymbolDef({ - 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 = linkable_idx - }))])) -(* | Hole(AddressExprFn f) -> - let next_addr = f addr (AllocatedSectionsMap outputs_by_name) - in - let n = next_addr - addr - in - let content = Missing_pervasives.replicate n Nothing - in - let _ = Missing_pervasives.outln (make_line "*fill*" (hex_string_of_natural comp_addr) - (hex_string_of_natural n) - "") - in - (next_addr - addr, content, {}) *) - | ProvideSymbol(pol, name1, (size2, info, other)) -> - (*let _ = errln ("Creating symbol definition named `" ^ name ^ "' in output section `" ^ secname ^ "'") - in*) - let symaddr = accum_current_addr (* FIXME: support others *) - in - (*let _ = Missing_pervasives.outln (make_line "" (hex_string_of_natural symaddr) "" ("PROVIDE (" ^ name ^ ", .)")) - in*) - (Nat_big_num.of_int (* sz *)0, (* comp_el_pat *) [],(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [( - Some(secname1, (( Nat_big_num.sub_nat symaddr output_section_start_addr),Nat_big_num.of_int 0)), - SymbolDef(symbol_def_for_provide_symbol name1 size2 info other control_script_linkable_idx) - )]) - ) - )) (* match comp_el_pat *) - in - (*let _ = errln ("Appending byte pattern to section " ^ secname ^ ", first 20 bytes: " ^ - (show (take 20 comp_el_pat))) - in*) - let new_content = (append_to_byte_pattern_at_offset ( Nat_big_num.sub_nat comp_addr output_section_start_addr) accum_pat comp_el_pat) - in - let new_addr = (Nat_big_num.add comp_addr sz) - in - let new_meta = (Pset.(union) accum_meta this_el_meta) - in - (new_content, new_addr, new_meta) - )) ([], output_section_start_addr,(Pset.from_list (pairCompare (maybeCompare (pairCompare compare (pairCompare Nat_big_num.compare Nat_big_num.compare))) compare) [])) (list_combine comp comp_addrs)) - in - let concat_sec_el = ({ - Memory_image.startpos = (Some(output_section_start_addr)) - ; Memory_image.length1 = (Some(size2)) - ; Memory_image.contents = concatenated_content - }) - in - (*let _ = Missing_pervasives.outln "" in*) - (* Make a new element in the image, also transferring metadata from input elements - * as appropriate. *) - let new_by_range_list = - ((Some(secname1, (Nat_big_num.of_int 0, size2)), FileFeature(ElfSection(Nat_big_num.of_int (* We don't yet konw where this'll come in the output file, so ... *) (* scn_idx *)0, - { elf64_section_name =(Nat_big_num.of_int 0) (* ignored *) - ; elf64_section_type = (output_section_type comp) - ; elf64_section_flags = (output_section_flags comp) - ; elf64_section_addr =(Nat_big_num.of_int 0) (* ignored -- covered by element *) - ; elf64_section_offset =(Nat_big_num.of_int 0) (* ignored -- will be replaced when file offsets are assigned *) - ; elf64_section_size =(Nat_big_num.of_int 0) (* ignored *) - ; elf64_section_link =(Nat_big_num.of_int 0) (* HMM *) - ; elf64_section_info =(Nat_big_num.of_int 0) (* HMM *) - ; elf64_section_align = (alignof_output_section comp) - ; elf64_section_entsize =(Nat_big_num.of_int 0) (* HMM *) - ; elf64_section_body = Byte_sequence.empty (* ignored *) - ; elf64_section_name_as_string = secname1 (* can't rely on this being ignored *) - } - ))) :: Pset.elements new_range_tag_pairs) - in - (*let _ = errln ("Metadata for new section " ^ secname ^ " consists of " ^ (show (length new_by_range_list)) ^ " tags.") - in*) - let new_by_range = (List.fold_left (fun m -> fun (maybe_range, tag) -> - let new_s = (Pset.add (maybe_range, tag) m) - in - (* let _ = errln ("Inserting an element into by_range; before: " ^ (show (Set.size m)) ^ "; after: " ^ (show (Set.size new_s))) - in *) - new_s - ) acc_img.by_range new_by_range_list) - in - let new_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 new_by_range) - in - let _ = - (let section_tags_bare = (List.filter (fun (maybe_range, tag) -> - (match tag with - | FileFeature(ElfSection(idx1, isec1)) -> true - | _ -> false - )) (Pset.elements new_by_range)) - in - (* errln ("Total metadata now includes " ^ (show (length section_tags_bare)) ^ " sections; are by_range and " - ^ "by_tag consistent? " ^ (show (new_by_tag = by_tag_from_by_range new_by_range))) *) ()) - in - (* this expression is the return value of add_output_section *) - ( Nat_big_num.add - (* new_pos *) output_section_start_addr size2, - (* new_acc *) { - elements = (Pmap.add secname1 concat_sec_el acc_img.elements) - (* tag it as a section, and transfer any tags *) - ; by_range = (* let _ = errln ("Returning from add_output_section a by_range with " ^ - (show (Set.size new_by_range))) in *) new_by_range - ; by_tag = new_by_tag - }, - (* sec_sz *) size2, - (* replacement_output_sec *) (OutputSectionSpec (guard, Some(output_section_start_addr), secname1, comp)) - ) - )) (* end add_output_section *) - in - (match script1 with - [] -> (acc, (AllocatedSectionsMap outputs_by_name)) - | (element1, el_idx) :: more_elements_and_idx -> - let do_nothing = (acc, pos, (AllocatedSectionsMap outputs_by_name)) in - let (new_acc, new_pos, new_outputs_by_name) = - ((match element1 with - DefineSymbol(symdefpol, name1, (symsize, syminfo, symother)) -> - (* We've already added this to the output composition. *) - do_nothing - | AdvanceAddress(AddressExprFn advance_fn_ref) -> - let advance_fn = -((match Pmap.lookup advance_fn_ref alloc_map with - | Some m -> m - | None -> failwith "alloc_map invariant failure" - )) - in - let new_pos = (advance_fn pos (AllocatedSectionsMap outputs_by_name)) - in - (acc, new_pos, (AllocatedSectionsMap outputs_by_name)) - (* FIXME: the allocated sections map is the subset of the outputs_by_name map - * that has been allocated -- meaning *both* sized *and* placed. - * Since we're a multi-pass interpreter, we've sized everything already, but - * only a subset has been placed. So we need to weed out all elements from - * outputs_by_name that don't correspond to a section in the accumulated image. - * We should probably include the section's range_tag in the allocated_sections_map, - * which would force us to do this, but at the moment neither of these is done. *) - | MarkAndAlignDataSegment(maxpagesize1, commonpagesize1) -> - (* GNU linker manual says: - - "DATA_SEGMENT_ALIGN(MAXPAGESIZE, COMMONPAGESIZE) - is equivalent to either - (ALIGN(MAXPAGESIZE) + (. & (MAXPAGESIZE - 1))) - or - (ALIGN(MAXPAGESIZE) + (. & (MAXPAGESIZE - COMMONPAGESIZE))) - depending on whether the latter uses fewer COMMONPAGESIZE sized - pages for the data segment (area between the result of this - expression and `DATA_SEGMENT_END') than the former or not. If the - latter form is used, it means COMMONPAGESIZE bytes of runtime - memory will be saved at the expense of up to COMMONPAGESIZE wasted - bytes in the on-disk file." - - In other words, we're marking the beginning of the data segment - by aligning our position upwards by an amount that - - - guarantees we're on a new page... - - - ... but (option 1) at an address that's congruent, modulo the max page size - (e.g. for 64kB maxpage, 4kB commonpage, we AND with 0xffff) - - - ... (option 2) at an offset that's at the commonpagesize boundary - immediately preceding the lowest congruent address - (e.g. for 64kB maxpage, 4kB commonpage, we AND with 0xf000, - so if we're at pos 0x1234, we bump up to 0x11000). - - FIXME: - - The GNU linker seems to bump up to 0x12000 here, not 0x11000. - Specifically, - - DATA_SEGMENT_ALIGN (0x200000, 0x1000) - - bumps 0x4017dc up to 0x602000. - - This is indeed better, because it allows the next section - to be output without a big gap in the file. - - LOAD 0x0000000000000000 0x0000000000400000 0x0000000000400000 - 0x00000000000017dc 0x00000000000017dc R E 200000 - LOAD 0x0000000000002000 0x0000000000602000 0x0000000000602000 - 0x0000000000000120 0x0000000000000ce8 RW 200000 - - ... whereas if the second LOAD began at address 0x601000, - the file offset of its first section would have to be 0x11000. - - So what *should* the formula be? - It needs to calculate the next address which - - - is a commonpagesize boundary; - - - is minimally >= the current address, modulo the commonpagesize - - - is minimally >= the current address, modulo the maxpagesize. - - The AND operation gives us something that is minimally *below* - the commonpagesize boundary. I think we need to add COMMONPAGESIZE. - - The code does this (in ldexp.c around line 478 as of binutils 2.25): - - expld.result.value = align_n (expld.dot, maxpage); - /* omit relro phase */ - if (expld.dataseg.phase == exp_dataseg_adjust) - { - if (commonpage < maxpage) - expld.result.value += ((expld.dot + commonpage - 1) - & (maxpage - commonpage)); - } - else - { - expld.result.value += expld.dot & (maxpage - 1); - - Which amounts to: - - 1. first, align up to maxpage. So for our example, we're now 0x10000. - or for our real example, we're now 0x600000 - - THEN since the first phase (expld_dataseg_none) - hits the final "else" case, - we immediately restore the modulus of the address, - giving 0x60188c. - or 0x6019ac the second time around (FIXME: why two?) - - 2. next, on the relevant phase (pass) of the script interpreter, - i.e. OPTION 2 - if commonpage < maxpage, - bump up the *non-maxpage-aligned non-modulo-restored* address - by - (. + commonpage - 1) & (maxpage - commonpage) - - i.e. for our example earlier - (0x01234 + 0x1000 - 1) & (0xf000) - = - 0x02233 & 0xf000 - = - 0x02000 - - i.e. for our real example - (0x4019ac + 0x1000 - 1) & (0x1ff000) - = - 0x4019ac + 0x1000 - 1) & 0x1ff000 - = - 0x002000 - - 3. OPTION 1 is implemented by the trailing "else {" - -- it restores the modulus. - - So the problem with our original logic (below) was that - it did what the manual says, not what the code does. - Specifically, the code for option 2 does - - (. + commonpagesize - 1) & (maxpagesize - commonpagesize) - - and NOT simply - - . & (maxpagesize - commonpagesize). - - FIXME: report this bug. - - - Note that intervening commands can do arbitrary things to the location - counter, so we can't do any short-cut arithmetic based on section sizes; - we actually have to run the layout procedure til we hit the end of the - data segment, and then see how we do. - - We run this function *forward* with the first option on a subset - of the script ending with the end of the data segment. - We then see what comes back. - - *) - (* let num_pages_used *) - (*let _ = errln ("Option 1 congruence add-in from pos 0x" ^ (hex_string_of_natural pos) ^ ", maxpagesize 0x" ^ - (hex_string_of_natural maxpagesize) ^ " is 0x" ^ (hex_string_of_natural (natural_land pos (maxpagesize - 1)))) - in*) - let option1 = (Nat_big_num.add (align_up_to maxpagesize1 pos) (Nat_big_num.bitwise_and pos ( Nat_big_num.sub_nat maxpagesize1(Nat_big_num.of_int 1)))) - in - (*let _ = errln ("Mark/align data segment: option 1 is to bump pos to 0x" ^ (hex_string_of_natural option1)) - in*) - let option2 = (Nat_big_num.add (align_up_to maxpagesize1 pos) (Nat_big_num.bitwise_and ( Nat_big_num.sub_nat (Nat_big_num.add pos commonpagesize1)(Nat_big_num.of_int 1)) ( Nat_big_num.sub_nat maxpagesize1 commonpagesize1))) - in - (*let _ = errln ("Mark/align data segment: option 2 is to bump pos to 0x" ^ (hex_string_of_natural option2)) - in*) - let data_segment_endpos = (fun startpos1 -> - (* run forward from here until MarkDataSegmentEnd, - * accumulating the actually-made outputs by name and their sizes *) - let (endpos, _) = (List.fold_left (fun (curpos, seen_end) -> fun (new_script_item, new_script_item_idx) -> - (*let _ = errln ("Folding at pos 0x" ^ (hex_string_of_natural curpos)) - in*) - if seen_end - then (curpos, true) - else let (newpos, new_seen) = ((match new_script_item with - | MarkDataSegmentEnd -> - (*let _ = errln "data segment end" - in*) - (* break the loop early here *) - (curpos, true) - | OutputSection(outputguard, maybe_expr, name1, sub_elements) -> - (*let _ = errln ("output section " ^ name) - in*) - let maybe_found = (Pmap.lookup name1 outputs_by_name) - in - let (OutputSectionSpec (guard, addr, secname1, comp), seen_script_el_idx) = ((match maybe_found with - Some (f, seen_script_el_idx) -> (f, seen_script_el_idx) - | None -> failwith "internal error: output section not found" - )) - in - (* Sometimes a given output section name, say .eh_frame, can come from multiple - * script elements with disjoint guard conditions (only_if_ro and only_if_rw, say). - * Only one of them will actually be selected when the guard is being evaluated. - * So when we "replay" the sections' output here, we want to skip the ones whose - * guards were false. The way we implement this is to store the originating script - * element idx in the allocated_output_sections map. We can test that against our - * current script element_idx here *) - let replay_output = ( Nat_big_num.equal seen_script_el_idx el_idx) - in - if replay_output - then ( - let unaligned_start_addr = curpos - in - let start_addr = (align_up_to (alignof_output_section comp) unaligned_start_addr) - in - let (end_addr, comp_addrs) = (do_output_section_layout_starting_at_addr start_addr (AllocatedSectionsMap outputs_by_name) comp) - in - let size2 = (Nat_big_num.sub_nat end_addr start_addr) - in - (end_addr, (* seen_end *) false) - ) - else (curpos, (* seen_end *) false) - | AdvanceAddress(AddressExprFn advance_fn_ref) -> - (*let _ = errln "Advance address" - in*) - let advance_fn = -((match Pmap.lookup advance_fn_ref alloc_map with - | Some m -> m - | None -> failwith "alloc_map invariant failed" - )) - in - let new_pos = (advance_fn curpos (AllocatedSectionsMap outputs_by_name)) - in - (new_pos, false) - | _ -> (curpos, seen_end) - )) - in - if Nat_big_num.less newpos curpos then failwith "went backwards" else (newpos, new_seen) - ) (startpos1, false) more_elements_and_idx) - in endpos - ) - in - let endpos_option1 = (data_segment_endpos option1) - in - let endpos_option2 = (data_segment_endpos option2) - in - (*let _ = errln ("Mark/align data segment: option 1 gives an endpos of 0x" ^ (hex_string_of_natural endpos_option1)) - in*) - (*let _ = errln ("Mark/align data segment: option 2 gives an endpos of 0x" ^ (hex_string_of_natural endpos_option2)) - in*) - let npages = (fun startpos1 -> (fun endpos -> Nat_big_num.div - ( Nat_big_num.sub_nat(align_up_to commonpagesize1 endpos) - (round_down_to commonpagesize1 startpos1)) commonpagesize1 - )) - in - let npages_option1 = (npages option1 endpos_option1) - in - let npages_option2 = (npages option2 endpos_option1) - in - (*let _ = errln ("Mark/align data segment: option 1 uses " ^ (show npages_option1) ^ " COMMONPAGESIZE-sized pages") - in*) - (*let _ = errln ("Mark/align data segment: option 2 uses " ^ (show npages_option2) ^ " COMMONPAGESIZE-sized pages") - in*) - if Nat_big_num.less npages_option1 npages_option2 - then (*let _ = errln "Choosing option 1" in*) (acc, option1, (AllocatedSectionsMap outputs_by_name)) - else (*let _ = errln "Choosing option 2" in*) (acc, option2, (AllocatedSectionsMap outputs_by_name)) - | MarkDataSegmentEnd -> do_nothing - | MarkDataSegmentRelroEnd(*(fun_from_secs_to_something)*) -> do_nothing - | OutputSection(outputguard, maybe_expr, name1, sub_elements) -> - (* Get the composition we computed earlier, and actually put it in - * the image, assigning an address to it. *) - let maybe_found = (Pmap.lookup name1 outputs_by_name) - in - let (found, seen_script_el_idx) = ((match maybe_found with - Some (f, saved_idx) -> (f, saved_idx) - | None -> failwith "internal error: output section not found" - )) - in - let (OutputSectionSpec (guard, addr, secname1, comp)) = found - in - (* let next_free_section_idx = 1 + naturalFromNat (Map.size outputs_by_name) - in *) - let count_sections_in_image = (fun img2 -> ( - let (section_tags, section_ranges) = (elf_memory_image_section_ranges img2) - in - let section_tags_bare = (Lem_list.map (fun tag -> - (match tag with - | FileFeature(ElfSection(idx1, isec1)) -> true - | _ -> false - )) section_tags) - in - length section_tags_bare - )) - in - (* Do we actually want to add an output section? Skip empty sections. - * CARE: we actually want to heed the proper ld semantics for empty sections - * (e.g. ". = ." will force output). From the GNU ld manual: - - The linker will not normally create output sections with no contents. - This is for convenience when referring to input sections that may or - may not be present in any of the input files. For example: - .foo : { *(.foo) } - will only create a `.foo' section in the output file if there is a - `.foo' section in at least one input file, and if the input sections - are not all empty. Other link script directives that allocate space in - an output section will also create the output section. So too will - assignments to dot even if the assignment does not create space, except - for `. = 0', `. = . + 0', `. = sym', `. = . + sym' and `. = ALIGN (. != - 0, expr, 1)' when `sym' is an absolute symbol of value 0 defined in the - script. This allows you to force output of an empty section with `. = - .'. - - The linker will ignore address assignments ( *note Output Section - Address::) on discarded output sections, except when the linker script - defines symbols in the output section. In that case the linker will - obey the address assignments, possibly advancing dot even though the - section is discarded. - - * It follows that we might discard the output section, - * but *retain* the symbol definitions within it, - * and keep the dot-advancements that - * In other words, we care about two things: - * - * -- whether there are any non-empty input sections, *or* - * non-excluded assignments to dot, inside the composition: - * this controls whether the section is output - - * -- whether the script defines symbols in the section; if so - * then *even if the section is discarded* - * we must honour the address assignments, - * which means using the ending address of do_output_section_layout_starting_at_addr, - * *and* - * we must retain the symbol definitions (which now could - * end up going in some other section? HMM...) - *) - let comp_element_allocates_space = (fun comp_el -> (match comp_el with - IncludeInputSection(_, irec) -> Nat_big_num.greater - (*let _ = errln ("Saw an input section named `" ^ irec.isec.elf64_section_name_as_string ^ - "' of size " ^ (show irec.isec.elf64_section_size)) - in*) - irec.isec.elf64_section_size(Nat_big_num.of_int 0) - | IncludeCommonSymbol(retain_pol, fname1, idx1, def, img2) -> Nat_big_num.greater -(Ml_bindings.nat_big_num_of_uint64 def.def_syment.elf64_st_size)(Nat_big_num.of_int 0) - | ProvideSymbol(pol, name1, spec) -> true (* HACK: what else makes sense here? *) - | Hole(AddressExprFn(address_fn_ref)) -> - let address_fn = -((match Pmap.lookup address_fn_ref alloc_map with - | Some m -> m - | None -> failwith "alloc_map invariant failed" - )) - in - let assignment_is_excluded = (fun f -> - (* really makes you wish you were programming in Lisp *) - let always_gives_0 = - ( Nat_big_num.equal(f(Nat_big_num.of_int 0) (AllocatedSectionsMap outputs_by_name))(Nat_big_num.of_int 0) - && Nat_big_num.equal (f(Nat_big_num.of_int 42) (AllocatedSectionsMap outputs_by_name))(Nat_big_num.of_int 0)) (* FIXME: this is wrong *) - in - let always_gives_dot = - ( Nat_big_num.equal(f(Nat_big_num.of_int 0) (AllocatedSectionsMap outputs_by_name))(Nat_big_num.of_int 0) - && Nat_big_num.equal (f(Nat_big_num.of_int 42) (AllocatedSectionsMap outputs_by_name))(Nat_big_num.of_int 42)) (* FIXME: this is wrong *) - in - (* FIXME: what are the semantics of function equality in Lem? *) - always_gives_0 || (always_gives_dot (*&& (AddressExprFn(f)) <> assign_dot_to_itself*) (* FIXME DPM: almost certainly not what is meant... *))) - in - not (assignment_is_excluded address_fn) - )) - in - let section_contains_non_empty_inputs = -(List.exists comp_element_allocates_space comp) - in - (* See note in MarkDataSegmentEnd case about script element idx. Short version: - * multiple output section stanzas, for a given section name, may be in the script, - * but only one was activated by the section composition pass. Ignore the others. *) - let do_output = (( Nat_big_num.equal seen_script_el_idx el_idx) && section_contains_non_empty_inputs) - in - if not do_output then - (*let _ = errln ("At pos 0x" ^ (hex_string_of_natural pos) ^ ", skipping output section " ^ name ^ - " because " ^ (if not section_contains_non_empty_inputs - then "it contains no non-empty inputs" - else "it was excluded by its output guard")) - in*) - (acc, pos, (AllocatedSectionsMap outputs_by_name)) - else ( - (* let _ = errln ("Before adding output section, we have " ^ (show (count_sections_in_image acc)) - ^ " sections.") - in *) - let (new_pos, new_acc, sec_sz, replacement_output_sec) - = (add_output_section ((* next_free_section_idx, *) pos, acc) found) - in - (*let _ = errln ("At pos 0x" ^ (hex_string_of_natural pos) ^ ", adding output section " ^ name ^ - " composed of " ^ (show (length comp)) ^ " items, new pos is 0x" ^ (hex_string_of_natural new_pos)) - in*) - (* let _ = errln ("Received from add_output_section a by_range with " ^ (show (Set.size new_acc.by_range)) - ^ " metadata records of which " ^ (show (Set.size { - (r, t) - | forall ((r, t) IN new_acc.by_range) - | match t with FileFeature(ElfSection(x)) -> true | _ -> false end - } - )) ^ " are ELF sections; one more time: " ^ (show (Set.size { - (t, r) - | forall ((t, r) IN new_acc.by_tag) - | match t with FileFeature(ElfSection(x)) -> true | _ -> false end - } - )) ^ "; count_sections_in_image says " ^ (show ( - length (Multimap.lookupBy Memory_image_orderings.tagEquiv (FileFeature(ElfSection(0, null_elf64_interpreted_section))) new_acc.by_tag) - )) - ) - in *) - (* let _ = errln ("After adding output section, we have " ^ (show (count_sections_in_image new_acc)) - ^ " sections.") - in *) - (new_acc, new_pos, (AllocatedSectionsMap (Pmap.add name1 (replacement_output_sec, el_idx) (Pmap.remove name1 outputs_by_name)))) - ) - | DiscardInput(selector) -> do_nothing - | InputQuery(retainpol, sortpol, selector) -> do_nothing - )) - in - (* recurse *) - build_image alloc_map new_acc new_pos new_outputs_by_name bindings_by_name more_elements_and_idx control_script_linkable_idx linker_defs_by_name - )) - -(* -let rec consecutive_commons rev_acc l = - match l with - [] -> reverse rev_acc - | IncludeCommonSymbol(pol, fname, def, img) :: rest -> - consecutive_commons ((pol, fname, def, img) :: rev_acc) rest - | _ -> reverse rev_acc -end -*) - -(*val default_place_orphans : input_output_assignment -> list input_spec -> input_output_assignment*) -let default_place_orphans (discards, outputs) inputs:(input_spec)list*(output_section_spec*Nat_big_num.num)list= -( - (* Try to emulate the GNU linker. - * Its docs say: - - "It attempts to place orphan sections after - non-orphan sections of the same attribute, such as code vs data, - loadable vs non-loadable, etc. If there is not enough room to do this - then it places at the end of the file. - - - For ELF targets, the attribute of the section includes section type - as well as section flag." - - * It places the .tm_clone_table orphan - - [ 9] .tm_clone_table PROGBITS 0000000000000000 00000160 - 0000000000000000 0000000000000000 WA 0 0 8 - - as - - .data 0x0000000000602120 0x0 crtend.o - .data 0x0000000000602120 0x0 crtn.o - - .tm_clone_table - 0x0000000000602120 0x0 - .tm_clone_table - 0x0000000000602120 0x0 crtbeginT.o - .tm_clone_table - 0x0000000000602120 0x0 crtend.o - - .data1 - *(.data1) - 0x0000000000602120 _edata = . - - i.e. between .data and .data1. In the script: - - .got.plt : { *(.got.plt) *(.igot.plt) } - .data : - { - *(.data .data.* .gnu.linkonce.d.* ) - SORT(CONSTRUCTORS) - } - .data1 : { *(.data1) } - _edata = .; PROVIDE (edata = .); - . = .; - __bss_start = .; - - i.e. no clear reason for why between .data and .data1. In the code: - - (see elf32em.c line 1787 in binutils 2.25) - - ... the key bit of code is as follows. - - place = NULL; - if ((s->flags & (SEC_ALLOC | SEC_DEBUGGING)) == 0) - place = &hold[orphan_nonalloc]; - else if ((s->flags & SEC_ALLOC) == 0) - ; - else if ((s->flags & SEC_LOAD) != 0 - && ((iself && sh_type == SHT_NOTE) - || (!iself && CONST_STRNEQ (secname, ".note")))) - place = &hold[orphan_interp]; - else if ((s->flags & (SEC_LOAD | SEC_HAS_CONTENTS | SEC_THREAD_LOCAL)) == 0) - place = &hold[orphan_bss]; - else if ((s->flags & SEC_SMALL_DATA) != 0) - place = &hold[orphan_sdata]; - else if ((s->flags & SEC_THREAD_LOCAL) != 0) - place = &hold[orphan_tdata]; - else if ((s->flags & SEC_READONLY) == 0) - place = &hold[orphan_data]; - else if (((iself && (sh_type == SHT_RELA || sh_type == SHT_REL)) - || (!iself && CONST_STRNEQ (secname, ".rel"))) - && (s->flags & SEC_LOAD) != 0) - place = &hold[orphan_rel]; - else if ((s->flags & SEC_CODE) == 0) - place = &hold[orphan_rodata]; - else - place = &hold[orphan_text]; - - - .. we replicate it here. - *)let output_irecs = (List.fold_left (fun acc -> fun outp -> ((match outp with - (OutputSectionSpec(guard, maybe_addr, name1, comp), script_el_idx) -> - let all_irecs = (List.fold_left (fun inner_acc -> fun comp_el -> (match comp_el with - IncludeInputSection(_, irec) -> Pset.add irec inner_acc - | _ -> inner_acc - ))(Pset.from_list compare []) comp) - in - Pset.(union) all_irecs acc - | _ -> acc - )))(Pset.from_list compare []) outputs) - in - let (orphans : input_spec list) = (List.filter (fun inp -> (match inp with - InputSection(irec) -> let v = (not ( Pset.mem irec output_irecs)) - in (*let _ = if v then errln ("Saw an orphan input section: " ^ - irec.secname ^ " in " ^ irec.fname) else () - in*) v - | _ -> false - )) inputs) - in - let place_one_orphan = (fun acc -> fun input -> ( - let irec = ((match input with - InputSection(irec) -> irec - | _ -> failwith "impossible: orphan section is not a section" - )) - in - let (discards, outputs) = acc in - let find_output = (fun maybe_name -> fun maybe_type -> fun flags_must_have -> fun flags_must_not_have -> ( - Missing_pervasives.find_index0 (fun (OutputSectionSpec (guard, maybe_addr, name1, comp), script_el_idx) -> - let flags = (output_section_flags comp) in - (match maybe_name with Some n -> n = name1 | None -> true ) - && ((match maybe_type with Some t -> Nat_big_num.equal (output_section_type comp) t | None -> true ) - && (Pset.for_all (fun x -> flag_is_set x flags) flags_must_have - && Pset.for_all (fun x -> not (flag_is_set x flags)) flags_must_not_have)) - ) outputs - )) - in - let place_after_nonalloc = (find_output None None(Pset.from_list Nat_big_num.compare [])(Pset.from_list Nat_big_num.compare [ shf_alloc ])) in - let place_after_interp = (find_output (Some(".interp")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc ])(Pset.from_list Nat_big_num.compare [])) in - let place_after_bss = (find_output (Some(".bss")) (Some(sht_nobits))(Pset.from_list Nat_big_num.compare [ shf_alloc; shf_write])(Pset.from_list Nat_big_num.compare [])) in - let place_after_rodata = (find_output (Some(".rodata")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc ])(Pset.from_list Nat_big_num.compare [ shf_write ])) in - let place_after_rel = (find_output (Some(".rela.dyn")) (Some(sht_rela))(Pset.from_list Nat_big_num.compare [])(Pset.from_list Nat_big_num.compare [])) in - let place_after_data = (find_output (Some(".data")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc; shf_write ])(Pset.from_list Nat_big_num.compare [])) in - let place_after_text = (find_output (Some(".text")) (Some(sht_progbits))(Pset.from_list Nat_big_num.compare [ shf_alloc; shf_execinstr ])(Pset.from_list Nat_big_num.compare [])) in - let (place_after : Nat_big_num.num option) = ((match input with - InputSection(irec) -> - (* HACK: simulates GNU linker, but this logic ought to go elsewhere *) - if irec.isec.elf64_section_name_as_string = ".note.GNU-stack" then None - else - if not (flag_is_set shf_alloc irec.isec.elf64_section_flags) - && (* not flag_is_set shf_alloc irec.isec.elf64_section_flags *) (* no debugging, for now *) true - then place_after_nonalloc - else (* FIXME: reinstate alloc-debugging case *) - if Nat_big_num.equal irec.isec.elf64_section_type sht_note (* FIXME: replicate iself logic *) - || (irec.isec.elf64_section_name_as_string = ".note") - then place_after_interp - else if Nat_big_num.equal irec.isec.elf64_section_type sht_nobits - then place_after_bss - else (* FIXME: implement thread-local case *) - if not (flag_is_set shf_write irec.isec.elf64_section_flags) - && not (flag_is_set shf_execinstr irec.isec.elf64_section_flags) - then place_after_rodata - else if flag_is_set shf_write irec.isec.elf64_section_flags - && not (flag_is_set shf_execinstr irec.isec.elf64_section_flags) - then place_after_data - else place_after_text - )) - in - let (discards, outputs) = acc in - (match place_after with - Some idx1 -> (* The section exists and has the flags we expected, and is at output idx *) - (discards, mapi (fun i -> fun output -> - (* FIXME: also fix up flags, alignment etc. *) - let (OutputSectionSpec (guard, maybe_addr, name1, comp), script_el_idx) = output in - if Nat_big_num.equal (Nat_big_num.of_int i) idx1 then (OutputSectionSpec(guard, maybe_addr, name1, List.rev_append (List.rev comp) [IncludeInputSection(DefaultKeep, irec)]), script_el_idx) else output - ) outputs - ) - | None -> - (*let _ = errln ("Warning: discarding orphan section `" ^ irec.isec.elf64_section_name_as_string - ^ "' from file `" ^ irec.fname ^ "'") - in*) - ( List.rev_append (List.rev discards) [input], outputs) - ) - )) - in - List.fold_left place_one_orphan (discards, outputs) orphans) - -(*val interpret_linker_control_script : - address_expr_fn_map allocated_sections_map -> - linker_control_script - -> linkable_list - -> natural (* control_script_linkable_idx *) - -> abi any_abi_feature - -> list input_spec - -> (input_spec -> input_spec -> ordering) (* seen ordering *) - -> (input_output_assignment -> list input_spec -> input_output_assignment) (* place orphans *) - -> (Map.map string (list (natural * binding))) (* initial_bindings_by_name *) - -> (elf_memory_image * Map.map string (list (natural * binding)))*) -let interpret_linker_control_script alloc_map script1 linkables control_script_linkable_idx a inputs seen_ordering place_orphans initial_bindings_by_name:(any_abi_feature)annotated_memory_image*((string),((Nat_big_num.num*binding)list))Pmap.map= - (let labelled_script = (label_script script1) - in - (*let _ = List.mapi (fun i -> fun input -> - errln ("Input " ^ (show i) ^ " is " ^ - match input with - InputSection(inp) -> - "input section, name `" ^ inp.secname ^ - "', from file `" ^ inp.fname ^ "' (linkable idx " ^ (show inp.idx) ^ ")" - | Common(idx, symname, img, def) -> - "common symbol `" ^ symname ^ "'" - end - ) - ) inputs - in*) - let (discards_before_orphans, outputs_before_orphans) - = (assign_inputs_to_output_sections ([], [])(Pset.from_list (pairCompare Nat_big_num.compare Nat_big_num.compare) [])(Pset.from_list (tripleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare) []) inputs None None seen_ordering labelled_script) - in - (* place orphans *) - let (discards, outputs) = (place_orphans (discards_before_orphans, outputs_before_orphans) inputs) - in - (* In assigning inputs to outputs, we may also have defined some symbols. These affect the - * bindings that are formed. So, we rewrite the bindings here. Note that we have to do so here, - * not in the caller, because these extra bindings can affect the reachability calculation - * during GC. *) - let (linker_defs_by_name, (bindings_by_name : ( (string, ( (Nat_big_num.num * binding)list))Pmap.map))) = ( - let (script_defs_by_name : (string, ( (symbol_definition * symbol_def_policy)list)) Pmap.map) - = (List.fold_left (fun acc -> (fun ((OutputSectionSpec (guard, maybe_addr, secname1, comp)), script_el_idx) -> - List.fold_left (fun inner_acc -> fun comp_el -> ( - (match comp_el with - ProvideSymbol(pol, name1, (size2, info, other)) -> - (*let _ = errln ("Linker script defining symbol `" ^ name ^ "'") - in*) - let def = (symbol_def_for_provide_symbol name1 size2 info other control_script_linkable_idx) - in - let v = ((match Pmap.lookup name1 inner_acc with - None -> [(def, pol)] - | Some l -> (def, pol) :: l - )) - in - Pmap.add name1 v inner_acc - | _ -> inner_acc - ) - )) (acc : (string, ( (symbol_definition * symbol_def_policy)list)) Pmap.map) comp - )) (Pmap.empty compare) outputs) - in - (* Now that we've made these definitions, what bindings are affected? - * We also use this opportunity to bind references to linker-generated symbols, - * such as _GLOBAL_OFFSET_TABLE_, since any definitions of these should now be merged - * into our inputs. *) - (* bit of a HACK: reconstruct the linkable img and idx from the input items *) - let idx_to_img = (List.fold_left (fun acc_m -> fun item -> - (match item with - Common(idx1, _, img2, symdef) -> Pmap.add idx1 img2 (Pmap.remove idx1 acc_m) - | InputSection(irec) -> Pmap.add irec.idx irec.img (Pmap.remove irec.idx acc_m) - ) - ) (Pmap.empty Nat_big_num.compare) inputs) - in - let (lowest_idx : Nat_big_num.num) = ((match Pset.min_elt_opt (Pmap.domain idx_to_img) - with Some x -> x - | None -> failwith "internal error: no linkable items" - )) - in - let first_linkable_item = ((match linkables with x :: more -> x | _ -> failwith "internal error: no linkables" )) - in - let (control_script_input_item : input_item) = ( - "(built-in control script)", - ControlScript, - (BuiltinControlScript, [Builtin]) - ) - in - let (control_script_linkable_item : linkable_item) = ( - ControlScriptDefs, control_script_input_item, - { item_fmt = "" - ; item_check_sections = false - ; item_copy_dt_needed = false - ; item_force_output = true - } - ) - in - let updated_bindings_and_new_defs = (Pmap.map (fun b_list_initial -> - Lem_list.map (fun (b_idx, b_initial) -> - let ((iref_idx, iref, iref_item), maybe_idef) = b_initial - in - (*let _ = errln ("Looking for linker script or linker-generated defs of symbol `" ^ iref.ref_symname ^ "'") - in*) - let possible_script_defs = ((match Pmap.lookup iref.ref_symname script_defs_by_name with - Some l -> l - | None -> [] - )) - in - let (possible_linker_generated_def : symbol_definition option) = - (if a.symbol_is_generated_by_linker iref.ref_symname - then (* can we find a definition by this name? *) - ((match Pmap.lookup lowest_idx idx_to_img with - None -> failwith "no lowest idx found" - | Some img2 -> - (match List.filter (fun def -> def.def_symname = iref.ref_symname) (defined_symbols - instance_Basic_classes_Ord_Abis_any_abi_feature_dict instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict img2) with - [] -> None - | [def] -> Some(def) - | _ -> failwith ("first linkable has multiple defs of name `" ^ (iref.ref_symname ^ "'")) - ) - )) - else None) - in - (* If the binding has no def, we always use the def we have. - * If the binding has a def, we use our def only if the policy is AlwaysDefine. *) - (*let _ = errs ("Do we override binding " ^ (show b_idx) ^ ", symbol named `" ^ - iref.ref_symname ^ "'? ") - in*) - (* FIXME: check real semantics of defining symbols like '_GLOBAL_OFFSET_TABLE_' in linker script or input objects. - * This is really just a guess. *) - let new_b_and_maybe_new_def = ((match (maybe_idef, possible_script_defs, possible_linker_generated_def) with - | (_, [], None) -> (*let _ = errln "no" in *) - (((iref_idx, iref, iref_item), maybe_idef), None) - | (None, [], Some(def)) -> (*let _ = errln "yes (was undefined)" in*) - (((iref_idx, iref, iref_item), Some(lowest_idx, def, first_linkable_item)), Some(def)) - | (_, [(def, AlwaysDefine)], _) -> (*let _ = errln "yes (linker script provides unconditional def)" in*) - (((iref_idx, iref, iref_item), Some (control_script_linkable_idx, def, control_script_linkable_item)), Some(def)) - | (Some existing_def, ([(def, ProvideIfUsed)]), _) -> (*let _ = errln "no" in*) - (((iref_idx, iref, iref_item), Some existing_def), None) - | (None, [(def, ProvideIfUsed)], _) -> (*let _ = errln "yes (linker script provides if-used def)" in*) - (((iref_idx, iref, iref_item), Some (control_script_linkable_idx, def, control_script_linkable_item)), Some(def)) - | (_, pair1 :: pair2 :: more, _) -> (*let _ = errln "error" in*) - failwith "ambiguous symbol binding in linker control script" - )) - in - (b_idx, new_b_and_maybe_new_def) - ) b_list_initial - ) initial_bindings_by_name) - in - let (new_symbol_defs_map : (string, ( ( symbol_definition option)list)) Pmap.map) - = (Pmap.map (fun b_pair_list -> Lem_list.map (fun (b_idx, (new_b, maybe_new_def)) -> maybe_new_def) b_pair_list) updated_bindings_and_new_defs) - in - let (new_symbol_defs_by_name : (string, ( symbol_definition list)) Pmap.map) = (Pmap.map - (fun v -> Lem_list.mapMaybe id0 v) new_symbol_defs_map) - in - (* { List.mapMaybe id maybe_def_list | forall ((_, maybe_def_list) IN (Map.toSet new_symbol_defs_map)) | true } - in*) - (*let new_symbol_defs = List.concat (Set_extra.toList new_symbol_def_list_set) - in*) - let updated_bindings = (Pmap.map (fun b_pair_list -> Lem_list.map (fun (b_idx, (new_b, maybe_new_def)) -> (b_idx, new_b)) b_pair_list) updated_bindings_and_new_defs) - in - (new_symbol_defs_by_name, updated_bindings) - ) - in - (*let _ = errln ("For __fini_array_end, we have " ^ - (let all_bs = match Map.lookup "__fini_array_end" 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 outputs_by_name = - (let insert_fun = (fun m -> (fun (OutputSectionSpec(guard, maybe_addr, name1, compos), script_idx) -> Pmap.add name1 ((OutputSectionSpec (guard, maybe_addr, name1, compos)), script_idx) m)) - in - List.fold_left insert_fun (Pmap.empty compare) outputs) - in - (* Print the link map's "discarded input sections" output. *) - (*let _ = Missing_pervasives.outln "\nDiscarded input sections\n" - in*) - let discard_line = (fun i -> ((match i with - InputSection(s) -> - let lpadded_secname = (" " ^ s.secname) - in - lpadded_secname ^ ((space_padding_and_maybe_newline(Nat_big_num.of_int 16) lpadded_secname) ^ ("0x0000000000000000" (* FIXME *) - ^ (" 0x" ^ ((hex_string_of_natural s.isec.elf64_section_size) ^ (" " - ^ (s.fname ^ "\n")))))) - | Common(idx1, fname1, img2, def) -> "" (* don't print discard lines for discarded commons *) - ))) - in - (*let _ = Missing_pervasives.outs (List.foldl (fun str -> (fun input -> (str ^ (discard_line input)))) "" (reverse discards)) - in*) - let outputs_by_name_after_gc = (compute_def_use_and_gc (AllocatedSectionsMap outputs_by_name)) - in - (*let _ = Missing_pervasives.outs "\nMemory Configuration\n\nName Origin Length Attributes\n*default* 0x0000000000000000 0xffffffffffffffff\n" - in - let _ = Missing_pervasives.outln "\nLinker script and memory map\n" - in*) - (* FIXME: print LOAD and START_GROUP trace *) - let (img2, outputs_by_name_with_position) - = (build_image alloc_map empty_elf_memory_image(Nat_big_num.of_int 0) outputs_by_name_after_gc bindings_by_name labelled_script control_script_linkable_idx linker_defs_by_name) - in - (*let _ = errln ("Final image has " ^ (show (Map.size img.elements)) ^ " elements and " - ^ (show (Set.size img.by_tag)) ^ " metadata tags, of which " ^ ( - let (section_tags, section_ranges) = elf_memory_image_section_ranges img - in - let section_tags_bare = List.map (fun tag -> - match tag with - | FileFeature(ElfSection(idx, isec)) -> (idx, isec) - | _ -> failwith "not section tag" - end) section_tags - in - show (length section_tags_bare) - ) ^ " are sections.") - in*) - (* The link map output for the section/address assignment basically mirrors our notion of - * output section composition. In the following: - - 0x0000000000400000 PROVIDE (__executable_start, 0x400000) - 0x0000000000400190 . = (0x400000 + SIZEOF_HEADERS) - -.interp - *(.interp) - -.note.ABI-tag 0x0000000000400190 0x20 - .note.ABI-tag 0x0000000000400190 0x20 crt1.o - -.note.gnu.build-id - 0x00000000004001b0 0x24 - *(.note.gnu.build-id) - .note.gnu.build-id - 0x00000000004001b0 0x24 crt1.o - -.hash - *(.hash) - -.gnu.hash - *(.gnu.hash) - -... we can see that - - - symbol provision, holes and output sections all get lines - - - each output section appears with its name left-aligned, and its address, - if any, appearing afterwards; if so, the section's total size also follows. - - - each input query is printed verbatim, e.g. "*(.note.gnu.build-id)" - - - underneath this, a line is printed for each input section that was included, - with its address and size. This can spill onto a second line in the usual way. - - - holes are shown as "*fill*" - - - provided symbols are shown as in the linker script source. - - PROBLEM: we don't have the script in source form, so we can't print the queries verbatim. - I should really annotate each query with its source form; when the script is parsed from source, - this can be inserted automatically. For the moment, what to do? I could annotate each script - element manually. For the moment, for diffing purposes, filter out lines with asterisks. - - *) - (img2, bindings_by_name)) |