package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/input_list.ml.html
Source file input_list.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
(*Generated by Lem from input_list.lem.*) open Lem_basic_classes open Lem_function open Lem_string open Lem_string_extra open Lem_tuple open Lem_bool open Lem_list open Lem_list_extra open Lem_sorting open Lem_num open Lem_maybe open Lem_assert_extra open Byte_sequence open Default_printing open Error open Missing_pervasives open Show open Archive open Command_line open Elf_types_native_uint open Elf_file open Elf_header (* Here we elaborate away various properties of the command line: * archives, groups, library paths, -l, --as-needed, --whole-archive, * and which inputs can be used to resolve symbols undefined in which other inputs. * * What we get out is a list of input files and the options applying to them. * Input files are either relocatable files, shared objects or linker scripts. *) type input_blob = Reloc of byte_sequence0 | Script of byte_sequence0 | ControlScript (* We remember where the input item came from on the command line, * using "coordinates" identifying the index in the higher-up list * followed by the index within that item. *) type origin_coord = InArchive of (Nat_big_num.num * Nat_big_num.num * string * Nat_big_num.num) (* archive-id, pos-within-archive, archive-name, archive-member-count *) | InGroup of (Nat_big_num.num * Nat_big_num.num) (* group-id, pos-within-group *) | InCommandLine of Nat_big_num.num | Builtin (*val string_of_origin_coord : origin_coord -> string*) let string_of_origin_coord c:string= ((match c with InArchive(aid, aidx, aname, _) -> "at position " ^ ((Nat_big_num.to_string aidx) ^ (" within archive " ^ (aname ^ (" (at position " ^ ((Nat_big_num.to_string aid) ^ ")"))))) | InGroup(gid1, gidx) -> "at position " ^ ((Nat_big_num.to_string gidx) ^ (" within group at position " ^ (Nat_big_num.to_string gid1))) | InCommandLine(cid) -> "(command line)" | Builtin -> "(built-in)" )) let instance_Show_Show_Input_list_origin_coord_dict:(origin_coord)show_class= ({ show_method = string_of_origin_coord}) type input_origin = input_unit * origin_coord list type input_item = string * input_blob * input_origin (*val string_of_input_blob : input_blob -> string*) let string_of_input_blob item:string= ((match item with Reloc(seq) -> "relocatable file (" ^ ((Nat_big_num.to_string (Byte_sequence.length0 seq)) ^ " bytes)") | Shared(seq) -> "shared object (" ^ ((Nat_big_num.to_string (Byte_sequence.length0 seq)) ^ " bytes)") | Script(seq) -> "script (" ^ ((Nat_big_num.to_string (Byte_sequence.length0 seq)) ^ " bytes)") | ControlScript -> "the linker control script" )) let instance_Show_Show_Input_list_input_blob_dict:(input_blob)show_class= ({ show_method = string_of_input_blob}) (*val short_string_of_input_item : input_item -> string*) let short_string_of_input_item item:string= (let (fname1, blob, (u, origin)) = item in (match origin with InArchive(aid, aidx, aname, _) :: _ -> aname ^ ("(" ^ (fname1 ^ ")")) | _ -> fname1 )) (* About symbol resolution and "suppliers". * * Groups change this. * * When we expand a .a file into a list of .o files, what is the supplier * relation among them? I *THINK* that within the archive, each can supply any other, * but outside the archive, each can only supply leftmore. *) type can_supply_function = input_item list -> int -> bool list type input_options = { item_fmt : string ; item_check_sections : bool ; item_copy_dt_needed : bool ; item_force_output : bool (* true for .o, false for .a unless --whole-archive, true for .so with --no-as-needed, false for .so with --as-needed *) } (*val null_input_options : input_options*) let null_input_options:input_options= ({ item_fmt = "" ; item_check_sections = false ; item_copy_dt_needed = false ; item_force_output = true }) (*val string_of_input_options : input_options -> string*) let string_of_input_options opts:string= "(some options)" let instance_Show_Show_Input_list_input_options_dict:(input_options)show_class= ({ show_method = string_of_input_options}) type input_list = (input_item * input_options) list (*val toplevel_dot_o_can_supply : list input_item -> nat -> list bool*) let toplevel_dot_o_can_supply inputs pos:(bool)list= (Lem_list.genlist (fun _ -> true) (List.length inputs)) (*val toplevel_shared_can_supply : list input_item -> nat -> list bool*) let inputs pos:(bool)list= (Lem_list.genlist (fun ndx -> ndx <= pos) (List.length inputs)) (*val toplevel_archive_can_supply : list input_item -> nat -> list bool*) let toplevel_archive_can_supply inputs pos:(bool)list= (Lem_list.genlist (fun ndx -> ndx <= pos) (List.length inputs)) (*val lib_filename_from_spec : string -> string -> string*) let lib_filename_from_spec spec ext:string= ((match (Xstring.explode spec) with ':' :: more -> (Xstring.implode more) | _ -> "lib" ^ (spec ^ ("." ^ ext)) )) (*val find_library_in : string -> list string -> list string -> maybe string*) let find_library_in spec extensions pathlist:(string)option= ( (* Recall the GNU libc's "libc.so is a linker script" hack. * This tells us that we should only look at file extensions, not contents. *)let file_exists name1= ((match Byte_sequence.acquire name1 with (* FIXME: use cheaper call *) Success _ -> true | Fail _ -> false )) in let expand_candidate_libname = (fun path -> fun ext -> (path ^ ("/" ^ (lib_filename_from_spec spec ext)))) in let get_expansions_existing = (fun path -> let x2 = ([]) in List.fold_right (fun cand x2 -> if file_exists cand then cand :: x2 else x2) (Lem_list.map (expand_candidate_libname path) extensions) x2) in let found_by_path = (Lem_list.map (fun path -> (path, get_expansions_existing path)) pathlist) in (* Do we take the first path for which some extension is found? * Or do we keep going if we prefer shared libraries, say? * I think it's the former. *) (match Lem_list.list_find_opt (fun (path, exps) -> (List.length exps) > 0) found_by_path with Some (path, exps) -> Some(List.hd exps) | None -> None )) (*val find_one_library_filename : input_file_options -> string -> string*) let find_one_library_filename options str:string= (let extensions = (if options.input_link_sharedlibs then ["so"; "a"] else ["a"]) in let found = (find_library_in str extensions options.input_libpath) in (match found with None -> failwith ("couldn't find library matching '" ^ (str ^ "'")) | Some result -> result )) (*val is_elf64_with_type : elf64_half -> byte_sequence -> bool*) let is_elf64_with_type typ seq:bool= ( (*let _ = Missing_pervasives.errs ("elf64? " ^ (match seq with Sequence(bs) -> show (List.take 16 bs) end)) in*)(match Elf_file.read_elf64_file seq with Success(e) -> (* let _ = Missing_pervasives.errln ": yes" in *) (e.elf64_file_header.elf64_type = typ) | Fail _ -> (* let _ = Missing_pervasives.errln ": no" in *) false )) (*val is_archive : byte_sequence -> bool*) let is_archive seq:bool= ((match read_archive_global_header seq with Success _ -> true | Fail _ -> false )) (*val open_file_and_expand : string -> input_unit -> natural -> list input_item*) let open_file_and_expand toplevel_fname u fpos:(string*input_blob*(input_unit*(origin_coord)list))list= ((match Byte_sequence.acquire toplevel_fname with Fail _ -> failwith ("could not open file " ^ toplevel_fname) | Success seq -> if is_elf64_with_type (Uint32_wrapper.of_bigint elf_ft_rel) seq then [(toplevel_fname, Reloc(seq), (u, []))] else if is_elf64_with_type (Uint32_wrapper.of_bigint elf_ft_dyn) seq then [(toplevel_fname, Shared(seq), (u, []))] else if is_archive seq then (match read_archive seq with Fail _ -> failwith ("could not read archive " ^ toplevel_fname) | Success (pairs : (string * byte_sequence0) list) -> (*let _ = Missing_pervasives.errln (toplevel_fname ^ " is an archive with " ^ (show (List.length pairs)) ^ " members") in*) let not_elf = (List.filter (fun (inner_fname, seq) -> not (is_elf64_with_type (Uint32_wrapper.of_bigint elf_ft_rel) seq)) pairs) in if List.length not_elf = 0 then mapMaybei (fun (i : Nat_big_num.num) -> (fun ((inner_fname : string), seq) -> let (trimmed_inner_fname : string) = ((match ((Ml_bindings.string_index_of '/' inner_fname) : Nat_big_num.num option) with None -> inner_fname | Some (ind : Nat_big_num.num) -> (match Ml_bindings.string_prefix ind inner_fname with Some s -> s | None -> failwith "impossible: string has character index >= its length" ) )) in Some (trimmed_inner_fname, Reloc(seq), (u, [InArchive(fpos, i, toplevel_fname, length pairs)])) )) pairs else let (names, seqs) = (List.split not_elf) in failwith ("archive with unsupported contents" (*(" ^ (show names) ^ ")*)) ) else [(toplevel_fname, Script(seq), (u, []))] )) (*val make_input_items_and_options : list input_item -> Command_line.input_file_options -> list origin_coord -> list (input_item * input_options)*) let make_input_items_and_options file_list cmdopts coords_to_append:((string*input_blob*(input_unit*(origin_coord)list))*input_options)list= ((match file_list with [] -> failwith "impossible: empty list of files" | [(fname1, Reloc(seq), (u, coords))] -> [((fname1, Reloc(seq), (u, List.rev_append (List.rev coords) coords_to_append)), { item_fmt = (cmdopts.input_fmt) ; item_check_sections = (cmdopts.input_check_sections) ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed) ; item_force_output = true })] | [(fname1, Shared(seq), (u, coords))] -> [((fname1, Shared(seq), (u, List.rev_append (List.rev coords) coords_to_append)), { item_fmt = (cmdopts.input_fmt) ; item_check_sections = (cmdopts.input_check_sections) ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed) ; item_force_output = (if cmdopts.input_as_needed then false else true) })] | [(fname1, Script(seq), (u, coords))] -> [((fname1, Script(seq), (u, List.rev_append (List.rev coords) coords_to_append)), { item_fmt = (cmdopts.input_fmt) ; item_check_sections = (cmdopts.input_check_sections) ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed) ; item_force_output = true })] | _ -> (* guaranteed to be all relocs, from one archive *) let (items_and_options : (input_item * input_options) list) = (mapMaybei (fun i -> (fun (fname1, reloc1, (u, coords)) -> let (item : input_item) = (fname1, reloc1, (u, List.rev_append (List.rev coords) coords_to_append)) in let (options : input_options) = ({ item_fmt = (cmdopts.input_fmt) ; item_check_sections = (cmdopts.input_check_sections) ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed) ; item_force_output = (if cmdopts.input_whole_archive then true else false) }) in Some (item, options) )) file_list) in items_and_options | _ -> failwith "impossible expanded input item" )) (*val elaborate_input_helper : natural -> list Command_line.input_unit -> input_list -> input_list*) let rec elaborate_input_helper input_pos inputs acc:(input_item*input_options)list= ((match inputs with [] -> acc | input :: more_inputs -> (match input with File(spec, options) -> (match spec with Filename(str) -> elaborate_input_helper ( Nat_big_num.add input_pos( (Nat_big_num.of_int 1))) more_inputs ( List.rev_append (List.rev acc) (make_input_items_and_options (open_file_and_expand str input input_pos) options [InCommandLine(input_pos)])) | Libname(str) -> elaborate_input_helper ( Nat_big_num.add input_pos( (Nat_big_num.of_int 1))) more_inputs ( List.rev_append (List.rev acc) (make_input_items_and_options (open_file_and_expand (find_one_library_filename options str) input input_pos) options [InCommandLine(input_pos)])) ) | Group(specs_and_options) -> (* Every member of a group is either a filename or a libname. * First expand the libnames, leaving the Group intact. *) let group_with_lib_files = (Lem_list.map (fun (spec, options) -> (match spec with Filename(str) -> (str, options) | Libname(str) -> (find_one_library_filename options str, options) )) specs_and_options) in (* Now expand archives into file lists. *) let group_with_file_lists = (mapMaybei (fun i -> (fun (str, options) -> Some ((open_file_and_expand str input input_pos), options) )) group_with_lib_files) in (* Now expand them into files and fix up the options appropriately *) let to_add = (mapMaybei (fun index_in_group -> (fun (file_list, options) -> ( Some( make_input_items_and_options file_list options [InGroup(input_pos, index_in_group); InCommandLine(input_pos)] )))) group_with_file_lists) in elaborate_input_helper ( Nat_big_num.add input_pos( (Nat_big_num.of_int 1))) more_inputs ( List.rev_append (List.rev acc) (List.concat to_add)) ) )) (*val elaborate_input : list Command_line.input_unit -> input_list*) let rec elaborate_input inputs:(input_item*input_options)list= (elaborate_input_helper( (Nat_big_num.of_int 0)) inputs [])
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>