(*Generated by Lem from command_line.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 (*import Set*) (*import Set_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 (* Here we try to model the command line of GNU ld.bfd. * * Some options are global modifiers affecting the link output. * Others have effect only for some subset of input files. * Typically some mutually-exclusive possibilities exist * whereby each argument selects one such possibility for all subsequent input files, * until a different argument selects another possibility for ensuring inputs. *) type input_file_spec = Filename of string (* /path/to/file.{o,a,so,...} -- might be script! *) | Libname of string (* -llib *) (*val string_of_input_file_spec : input_file_spec -> string*) let string_of_input_file_spec spec:string= ((match spec with Filename(s) -> "file `" ^ (s ^ "'") | Libname(s) -> "library `" ^ (s ^ "'") )) let instance_Show_Show_Command_line_input_file_spec_dict:(input_file_spec)show_class= ({ show_method = string_of_input_file_spec}) type input_file_options = { input_fmt : string ; input_libpath : string list ; input_link_sharedlibs : bool (* -Bstatic *) ; input_check_sections : bool ; input_copy_dt_needed : bool ; input_whole_archive : bool ; input_as_needed : bool } (*val null_input_file_options : input_file_options*) let null_input_file_options:input_file_options= ({ input_fmt = "" ; input_libpath = ([]) ; input_link_sharedlibs = false ; input_check_sections = false ; input_copy_dt_needed = false ; input_whole_archive = false ; input_as_needed = false }) type output_kind = Executable | SharedLibrary type link_option = OutputFilename of string | OutputKind of output_kind | ForceCommonDefined of bool (* -d, -dc, -dp *) | Soname of string (* -soname *) | EntryAddress of Nat_big_num.num | TextSegmentStart of Nat_big_num.num | RodataSegmentStart of Nat_big_num.num | LdataSegmentStart of Nat_big_num.num | BindFunctionsEarly (* -Bsymbolic-functions *) | BindNonFunctionsEarly (* the remainder of -Bsymbolic *) (* more here! *) (*val tagEqual : link_option -> link_option -> bool*) let tagEqual opt1 opt2:bool= ((match (opt1, opt2) with (* FIXME: Lem BUG here! says "duplicate binding" *) (OutputFilename(_), OutputFilename(_)) -> true | (OutputKind(_), OutputKind(_)) -> true (* | (ForceCommonDefined, ForceCommonDefined) -> true *) | (Soname(_), Soname(_)) -> true (* | (EntryAddress, EntryAddress) -> true *) | (TextSegmentStart(_), TextSegmentStart(_)) -> true | (RodataSegmentStart(_), RodataSegmentStart(_)) -> true | (LdataSegmentStart(_), LdataSegmentStart(_)) -> true (* | (BindFunctionsEarly, BindFunctionsEarly) -> true *) (* | (BindNonFunctionsEarly, BindNonFunctionsEarly) -> true *) | _ -> false )) (* To allow filtering out a previous setting for a given option, we define * an equality relation that is true if options are of the same constructor. * Seems like a bit of a HACK. *) let instance_Basic_classes_Eq_Command_line_link_option_dict:(link_option)eq_class= ({ isEqual_method = (fun opt1 -> (fun opt2 -> (match (opt1, opt2) with | (OutputFilename(_), OutputFilename(_)) -> true | (ForceCommonDefined(_), ForceCommonDefined(_)) -> true | (Soname(_), Soname(_)) -> true | (EntryAddress(_), EntryAddress(_)) -> true | _ -> false ) )); isInequal_method = (fun opt1 -> (fun opt2 -> not ( ((fun opt1 -> (fun opt2 -> (match (opt1, opt2) with | (OutputFilename(_), OutputFilename(_)) -> true | (ForceCommonDefined(_), ForceCommonDefined(_)) -> true | (Soname(_), Soname(_)) -> true | (EntryAddress(_), EntryAddress(_)) -> true | _ -> false ) ))opt1 opt2))))}) type input_file_and_options = input_file_spec * input_file_options type input_unit = File of input_file_and_options | Group of (input_file_and_options) list (* NOT recursive *) | BuiltinControlScript (* for uniformity when processing script defs *) (*val string_of_input_unit : input_unit -> string*) let string_of_input_unit u:string= ((match u with File(spec, opts) -> "single " ^ (string_of_input_file_spec spec) | Group(spec_opt_list) -> "group: [" ^ ((string_of_list instance_Show_Show_Command_line_input_file_spec_dict (Lem_list.map (fun (spec, opts) -> spec) spec_opt_list)) ^ "]") | BuiltinControlScript -> "(built-in control script)" )) let instance_Show_Show_Command_line_input_unit_dict:(input_unit)show_class= ({ show_method = string_of_input_unit}) (* Reading the command-line: * we encode the meaning of a linker command token * using a reader function interpreting a list of argument definitions. * Lookahead is necessary: sometimes the interpretation of an option * depends on the next argument (e.g. whether it's a file, directory or another option). * The list of argument definitions is from lists of strings to constructor function invocations. * We use lists of strings since many options have synonyms. * The strings are interpreted as regular expressions and any matched groups are collected together * as a second argument list; this is because some arguments are of the form --blah=NUM or similar. *) (* As we read the command line, we keep a current state which is the collection * of seen input files, seen whole-link options, and input file options that will * apply to any input files we add subsequently. *) type command_state = { input_units : input_unit list ; link_options : link_option Pset.set ; current_input_options : input_file_options ; current_group : ( input_file_and_options list)option } (* This is the "default state" when we start reading input options *) (*val initial_state : list command_state*) (* the stack *) let initial_state0:(command_state)list= ([{ input_units = ([]) ; link_options =(Pset.from_list compare [OutputFilename("a.out"); OutputKind(Executable)]) ; current_input_options = ({ input_fmt = "elf64-x86-64" (* FIXME *) ; input_libpath = (["/usr/lib"]) (* FIXME: this probably isn't the right place to supply the default search path *) ; input_link_sharedlibs = true ; input_check_sections = true ; input_copy_dt_needed = false ; input_whole_archive = false ; input_as_needed = true (* FIXME *) }) ; current_group = None }]) type interpreted_command_line = input_unit list * link_option Pset.set (*val add_input_file : list command_state -> string -> list command_state*) let add_input_file (state1 :: more) s:(command_state)list= (let chars = (Xstring.explode s) in let spec = ((match chars with '-' :: 'l' :: more -> Libname(Xstring.implode more) | '-' :: more -> failwith ("not a valid option or input file: " ^ s) | _ -> Filename(s) )) in if (Lem.option_equal (listEqualBy (Lem.pair_equal (=) (=))) state1.current_group None) then { input_units = (List.rev_append (List.rev state1.input_units) [File(spec, state1.current_input_options)]) ; link_options = (state1.link_options) ; current_input_options = (state1.current_input_options) ; current_group = (state1.current_group) } :: more else { input_units = (state1.input_units) ; link_options = (state1.link_options) ; current_input_options = (state1.current_input_options) ; current_group = (let toAppend = ([(spec, state1.current_input_options)]) in (match state1.current_group with Some l -> Some( List.rev_append (List.rev l) toAppend) | None -> Some(toAppend) )) } :: more) (*val start_group : list command_state -> list command_state*) let start_group (state1 :: more):(command_state)list= ({ input_units = (state1.input_units) ; link_options = (state1.link_options) ; current_input_options = (state1.current_input_options) ; current_group = ((match state1.current_group with None -> Some [] | _ -> failwith "cannot nest groups" )) } :: more) (*val end_group : list command_state -> list command_state*) let end_group (state1 :: more):(command_state)list= ({ input_units = (List.rev_append (List.rev state1.input_units) ((match state1.current_group with Some l -> [Group(l)] | None -> failwith "end group without start group" ))) ; link_options = (state1.link_options) ; current_input_options = (state1.current_input_options) ; current_group = None } :: more) type option_token = string type option_argspecs = string list * string list type option_argvals = string list * string list (*val set_or_replace_option : link_option -> list command_state -> list command_state*) let set_or_replace_option opt state_list:(command_state)list= ((match state_list with [] -> failwith "error: no state" | state1 :: more -> { input_units = (state1.input_units) ; link_options = (Pset.add opt (Pset.filter (fun existing -> ((fun opt1 -> (fun opt2 -> not ( ((fun opt1 -> (fun opt2 -> (match (opt1, opt2) with | (OutputFilename(_), OutputFilename(_)) -> true | (ForceCommonDefined(_), ForceCommonDefined(_)) -> true | (Soname(_), Soname(_)) -> true | (EntryAddress(_), EntryAddress(_)) -> true | _ -> false ) ))opt1 opt2)))) existing opt)) state1.link_options)) ; current_input_options = (state1.current_input_options) ; current_group = (state1.current_group) } :: more )) (*val find_option_matching_tag : link_option -> set link_option -> maybe link_option*) let rec find_option_matching_tag tag options:(link_option)option= (Lem_list.list_find_opt (tagEqual tag) (Pset.elements options)) (*val extract_hex_addend : char -> maybe natural*) let extract_hex_addend x:(Nat_big_num.num)option= (if x = '0' then Some(Nat_big_num.of_int 0) else if x = '1' then Some(Nat_big_num.of_int 1) else if x = '2' then Some(Nat_big_num.of_int 2) else if x = '3' then Some(Nat_big_num.of_int 3) else if x = '4' then Some(Nat_big_num.of_int 4) else if x = '5' then Some(Nat_big_num.of_int 5) else if x = '6' then Some(Nat_big_num.of_int 6) else if x = '7' then Some(Nat_big_num.of_int 7) else if x = '8' then Some(Nat_big_num.of_int 8) else if x = '9' then Some(Nat_big_num.of_int 9) else if x = 'a' then Some(Nat_big_num.of_int 10) else if x = 'b' then Some(Nat_big_num.of_int 11) else if x = 'c' then Some(Nat_big_num.of_int 12) else if x = 'd' then Some(Nat_big_num.of_int 13) else if x = 'e' then Some(Nat_big_num.of_int 14) else if x = 'f' then Some(Nat_big_num.of_int 15) else None) (*val accumulate_hex_chars : natural -> list char -> natural*) let rec accumulate_hex_chars acc chars:Nat_big_num.num= ((match chars with | [] -> acc | x::xs -> (match extract_hex_addend x with | None -> acc | Some addend -> accumulate_hex_chars ( Nat_big_num.add (Nat_big_num.mul acc(Nat_big_num.of_int 16)) addend) xs ) )) (*val extract_dec_addend : char -> maybe natural*) let extract_dec_addend x:(Nat_big_num.num)option= (if x = '0' then Some(Nat_big_num.of_int 0) else if x = '1' then Some(Nat_big_num.of_int 1) else if x = '2' then Some(Nat_big_num.of_int 2) else if x = '3' then Some(Nat_big_num.of_int 3) else if x = '4' then Some(Nat_big_num.of_int 4) else if x = '5' then Some(Nat_big_num.of_int 5) else if x = '6' then Some(Nat_big_num.of_int 6) else if x = '7' then Some(Nat_big_num.of_int 7) else if x = '8' then Some(Nat_big_num.of_int 8) else if x = '9' then Some(Nat_big_num.of_int 9) else None) (*val accumulate_dec_chars : natural -> list char -> natural*) let rec accumulate_dec_chars acc chars:Nat_big_num.num= ((match chars with | [] -> acc | x::xs -> (match extract_dec_addend x with | None -> acc | Some addend -> accumulate_hex_chars ( Nat_big_num.add (Nat_big_num.mul acc(Nat_big_num.of_int 16)) addend) xs ) )) (*val parse_address : string -> natural*) let parse_address s:Nat_big_num.num= ((match Xstring.explode s with '0' :: 'x' :: more -> accumulate_hex_chars(Nat_big_num.of_int 0) more | chars -> accumulate_dec_chars(Nat_big_num.of_int 0) chars )) type option_def = ( option_token list) * option_argspecs * (option_argvals -> command_state list -> command_state list) * string (* the table is a list of: ... options and their arg names ... and the option's meaning as a function... and a help string *) (*val command_line_table : list option_def*) let command_line_table:((string)list*((string)list*(string)list)*((string)list*(string)list ->(command_state)list ->(command_state)list)*string)list= ([ (* per-input options *) (["-b"; "--format"], (["TARGET"], []), (fun args -> (fun state1 -> state1)), "Specify target for following input files"); (["-L"; "--library-path"], (["DIRECTORY"], []), (fun args -> (fun state1 -> state1)), "Add DIRECTORY to library search path"); (["--as-needed"], ([], []), (fun _ -> (fun state1 -> state1)), "Only set DT_NEEDED for following dynamic libs if used"); (["--no-as-needed"], ([], []), (fun _ -> (fun state1 -> state1)), "Always set DT_NEEDED for dynamic libraries mentioned on the command line"); (["-Bdynamic"; "-dy"; "-call_shared"], ([], []), (fun _ -> (fun state1 -> state1)), "Link against shared libraries"); (["-Bstatic"; "-dn"; "-non_shared"; "-static"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not link against shared libraries"); (["--check-sections"], ([], []), (fun _ -> (fun state1 -> state1)), "Check section addresses for overlaps (default) **srk** not sure it's per-input!"); (["--no-check-sections"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not check section addresses for overlaps **srk** not sure it's per-input!"); (["--copy-dt-needed-entries"], ([], []), (fun _ -> (fun state1 -> state1)), "Copy DT_NEEDED links mentioned inside DSOs that follow"); (["--no-copy-dt-needed-entries"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not copy DT_NEEDED links mentioned inside DSOs that follow"); (["--no-whole-archive"], ([], []), (fun _ -> (fun state1 -> state1)), "Turn off --whole-archive"); (["-rpath-link"], (["PATH"], []), (fun _ -> (fun state1 -> state1)), "Set link time shared library search path **srk** not sure it's per-input!"); (["--whole-archive"], ([], []), (fun _ -> (fun state1 -> state1)), "Include all objects from following archives"); (* linker plugin control *) (["-plugin"], (["PLUGIN"], []), (fun _ -> (fun state1 -> state1)), "Load named plugin"); (["-plugin-opt"], (["ARG"], []), (fun _ -> (fun state1 -> state1)), "Send arg to last-loaded plugin"); (* output / whole-job options (some may be repeated with different args, but most not): *) (["-A"; "--architecture"], (["ARCH"], []), (fun _ -> (fun state1 -> state1)), "Set architecture"); (["-EB"], ([], []), (fun _ -> (fun state1 -> state1)), "Link big-endian objects"); (["-EL"], ([], []), (fun _ -> (fun state1 -> state1)), "Link little-endian objects"); (["-R"; "--just-symbols"], (["DIR"], []), (fun _ -> (fun state1 -> state1)), "**srk** (if directory, same as --rpath)"); (["-d"; "-dc"; "-dp"], ([], []), (fun _ -> (fun state1 -> state1)), "Force common symbols to be defined"); (["-e"; "--entry"], (["ADDRESS"], []), (fun _ -> (fun state1 -> state1)), "Set start address"); (["-E"; "--export-dynamic"], ([], []), (fun _ -> (fun state1 -> state1)), "Export all dynamic symbols"); (["--no-export-dynamic"], ([], []), (fun _ -> (fun state1 -> state1)), "Undo the effect of --export-dynamic"); (["-f"; "--auxiliary"], (["SHLIB"], []), (fun _ -> (fun state1 -> state1)), "Auxiliary filter for shared object symbol table"); (["-F"; "--filter"], (["SHLIB"], []), (fun _ -> (fun state1 -> state1)), "Filter for shared object symbol table"); (["-G"; "--gpsize"], (["SIZE"], []), (fun _ -> (fun state1 -> state1)), "Small data size (if no size, same as --shared) **srk NOTE this quirk!**"); (["-h"; "-soname"], (["FILENAME"], []), (fun _ -> (fun state1 -> state1)), "Set internal name of shared library"); (["-I"; "--dynamic-linker"], (["PROGRAM"], []), (fun _ -> (fun state1 -> state1)), "Set PROGRAM as the dynamic linker to use"); (["--sysroot="], ([], ["DIRECTORY"]), (fun _ -> (fun state1 -> state1)), "Override the default sysroot location"); (["-m"], (["EMULATION"], []), (fun _ -> (fun state1 -> state1)), "Set emulation"); (["-n"; "--nmagic"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not page align data"); (["-N"; "--omagic"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not page align data, do not make text readonly"); (["--no-omagic"], ([], []), (fun _ -> (fun state1 -> state1)), "Page align data, make text readonly"); (["-o"; "--output"], (["FILE"], []), (fun argvals -> set_or_replace_option (OutputFilename(List.hd (fst argvals)))), "Set output file name"); (["-O"], ([], []), (fun _ -> (fun state1 -> state1)), "Optimise output file"); (["-q"; "--emit-relocs"], ([], []), (fun _ -> (fun state1 -> state1)), "Generate relocations in final output"); (["-r"; "-i"; "--relocatable"], ([], []), (fun _ -> (fun state1 -> state1)), "Generate relocatable output"); (["-s"; "--strip-all"], ([], []), (fun _ -> (fun state1 -> state1)), "Strip all symbols"); (["-S"; "--strip-debug"], ([], []), (fun _ -> (fun state1 -> state1)), "Strip debugging symbols"); (["--strip-discarded"], ([], []), (fun _ -> (fun state1 -> state1)), "Strip symbols in discarded sections"); (["--no-strip-discarded"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not strip symbols in discarded sections"); (["--default-script"; "-dT"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Read default linker script"); (["--unique="], ([], ["SECTION"]), (fun _ -> (fun state1 -> state1)), "Don't merge input [SECTION | orphan] sections"); (["-Ur"], ([], []), (fun _ -> (fun state1 -> state1)), "Build global constructor/destructor tables ( **srk**: like -r, but... )"); (["-x"; "--discard-all"], ([], []), (fun _ -> (fun state1 -> state1)), "Discard all local symbols"); (["-X"; "--discard-locals"], ([], []), (fun _ -> (fun state1 -> state1)), "Discard temporary local symbols (default)"); (["--discard-none"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't discard any local symbols"); (["-Bsymbolic"], ([], []), (fun argvals -> (fun state1 -> set_or_replace_option BindFunctionsEarly (set_or_replace_option BindNonFunctionsEarly state1))), "Bind global references locally"); (["-Bsymbolic-functions"], ([], []), (fun argvals -> set_or_replace_option (BindFunctionsEarly)), "Bind global function references locally"); (["--force-exe-suffix"], ([], []), (fun _ -> (fun state1 -> state1)), "Force generation of file with .exe suffix"); (["--gc-sections"], ([], []), (fun _ -> (fun state1 -> state1)), "**srk: uncertain: can repeat?** Remove unused sections (on some targets)"); (["--no-gc-sections"], ([], []), (fun _ -> (fun state1 -> state1)), "**srk: uncertain: can repeat?** Don't remove unused sections (default)"); (["--hash-size="], ([], ["NUMBER"]), (fun _ -> (fun state1 -> state1)), "Set default hash table size close to "); (["--no-define-common"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not define Common storage"); (["--no-undefined"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not allow unresolved references in object files"); (["--allow-shlib-undefined"], ([], []), (fun _ -> (fun state1 -> state1)), "Allow unresolved references in shared libraries"); (["--no-allow-shlib-undefined"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not allow unresolved references in shared libs"); (["--default-symver"], ([], []), (fun _ -> (fun state1 -> state1)), "Create default symbol version"); (["--default-imported-symver"], ([], []), (fun _ -> (fun state1 -> state1)), "Create default symbol version for imported symbols"); (["-nostdlib"], ([], []), (fun _ -> (fun state1 -> state1)), "Only use library directories specified on the command line"); (["--oformat"], (["TARGET"], []), (fun _ -> (fun state1 -> state1)), "Specify target of output file"); (["--relax"], ([], []), (fun _ -> (fun state1 -> state1)), "Reduce code size by using target specific optimisations"); (["--no-relax"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not use relaxation techniques to reduce code size"); (["--retain-symbols-file"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Keep only symbols listed in FILE"); (["-rpath"], (["PATH"], []), (fun _ -> (fun state1 -> state1)), "Set runtime shared library search path"); (["-shared"; "-Bshareable"], ([], []), (fun argvals -> set_or_replace_option (OutputKind(SharedLibrary))), "Create a shared library"); (["-pie"; "--pic-executable"], ([], []), (fun _ -> (fun state1 -> state1)), "Create a position independent executable"); (["--sort-common="],(* (ascending|descending) *)([], ["order"]), (fun _ -> (fun state1 -> state1)), "Sort common symbols by alignment [in specified order]"); (["--sort-section="],(* (name|alignment) *) ([], ["key"]), (fun _ -> (fun state1 -> state1)), "Sort sections by name or maximum alignment"); (["--spare-dynamic-tags"], (["COUNT"], []), (fun _ -> (fun state1 -> state1)), "How many tags to reserve in .dynamic section"); (["--split-by-file="], ([], ["SIZE"]), (fun _ -> (fun state1 -> state1)), "Split output sections every SIZE octets"); (["--split-by-reloc="], ([], ["COUNT"]), (fun _ -> (fun state1 -> state1)), "Split output sections every COUNT relocs"); (["--traditional-format"], ([], []), (fun _ -> (fun state1 -> state1)), "Use same format as native linker"); (["--unresolved-symbols="], ([], ["method"]), (fun _ -> (fun state1 -> state1)), "How to handle unresolved symbols. is: ignore-all, report-all, ignore-in-object-files, ignore-in-shared-libs"); (["--dynamic-list-data"], ([], []), (fun _ -> (fun state1 -> state1)), "Add data symbols to dynamic list"); (["--dynamic-list-cpp-new"], ([], []), (fun _ -> (fun state1 -> state1)), "Use C++ operator new/delete dynamic list"); (["--dynamic-list-cpp-typeinfo "], ([], []), (fun _ -> (fun state1 -> state1)), "Use C++ typeinfo dynamic list"); (["--dynamic-list"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Read dynamic list"); (["--wrap"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Use wrapper functions for SYMBOL"); (* the following are specific to ELF emulations *) (["--audit=(.*)"], ([], ["AUDITLIB"]), (fun _ -> (fun state1 -> state1)), "Specify a library to use for auditing"); (["-Bgroup"], ([], []), (fun _ -> (fun state1 -> state1)), "Selects group name lookup rules for DSO"); (["--build-id="], ([], ["STYLE"]), (fun _ -> (fun state1 -> state1)), "Generate build ID note"); (["-P"], (["AUDITLIB"], []), (fun _ -> (fun state1 -> state1)), "Specify a library to use for auditing dependencies"); (["--depaudit="], ([], ["AUDITLIB"]), (fun _ -> (fun state1 -> state1)), "Specify a library to use for auditing dependencies"); (["--disable-new-dtags"], ([], []), (fun _ -> (fun state1 -> state1)), "Disable new dynamic tags"); (["--enable-new-dtags"], ([], []), (fun _ -> (fun state1 -> state1)), "Enable new dynamic tags"); (["--eh-frame-hdr"], ([], []), (fun _ -> (fun state1 -> state1)), "Create .eh_frame_hdr section"); (["--exclude-libs="], ([], ["LIBS"]), (fun _ -> (fun state1 -> state1)), "Make all symbols in LIBS hidden"); (["--hash-style="], ([], ["STYLE"]), (fun _ -> (fun state1 -> state1)), "Set hash style to sysv, gnu or both"); (* NOTE: for these to work, we hack our word-splitter to merge -z options into a single word with a single space in *) (["-z combreloc"], ([], []), (fun _ -> (fun state1 -> state1)), "Merge dynamic relocs into one section and sort"); (["-z common-page-size="], ([], ["SIZE"]), (fun _ -> (fun state1 -> state1)), "Set common page size to SIZE"); (["-z defs"], ([], []), (fun _ -> (fun state1 -> state1)), "Report unresolved symbols in object files."); (["-z execstack"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark executable as requiring executable stack"); (["-z global"], ([], []), (fun _ -> (fun state1 -> state1)), "Make symbols in DSO available for subsequently loaded objects"); (["-z initfirst"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark DSO to be initialized first at runtime"); (["-z interpose"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark object to interpose all DSOs but executable"); (["-z lazy"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark object lazy runtime binding (default)"); (["-z loadfltr"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark object requiring immediate process"); (["-z max-page-size="], ([], ["SIZE"]), (fun _ -> (fun state1 -> state1)), "Set maximum page size to SIZE"); (["-z nocombreloc"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't merge dynamic relocs into one section"); (["-z nocopyreloc"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't create copy relocs"); (["-z nodefaultlib"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark object not to use default search paths"); (["-z nodelete"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark DSO non-deletable at runtime"); (["-z nodlopen"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark DSO not available to dlopen"); (["-z nodump"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark DSO not available to dldump"); (["-z noexecstack"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark executable as not requiring executable stack"); (["-z norelro"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't create RELRO program header"); (["-z now"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark object non-lazy runtime binding"); (["-z origin"], ([], []), (fun _ -> (fun state1 -> state1)), "Mark object requiring immediate $ORIGIN processing at runtime"); (["-z relro"], ([], []), (fun _ -> (fun state1 -> state1)), "Create RELRO program header"); (["-z stacksize="], ([], ["SIZE"]), (fun _ -> (fun state1 -> state1)), "Set size of stack segment"); (["-z bndplt"], ([], []), (fun _ -> (fun state1 -> state1)), "Always generate BND prefix in PLT entries"); (["--ld-generated-unwind-info"], ([], []), (fun _ -> (fun state1 -> state1)), "Generate exception handling info for PLT."); (["--no-ld-generated-unwind-info"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't do so."); (* quasi-input options (can be repeated): *) (["-c"; "--mri-script"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Read MRI format linker script"); (["-l"; "--library"], (["LIBNAME"], []), (fun _ -> (fun state1 -> state1)), "Search for library LIBNAME"); (* (["-R" ,"--just-symbols"], (["FILE"], []), fun _ -> (fun state -> state), "Just link symbols"), *) (* Handled above! *) (["-T"; "--script"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Read linker script"); (["-u"; "--undefined"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Start with undefined reference to SYMBOL"); (["-("; "--start-group"], ([], []), (fun _ -> (fun state1 -> start_group state1)), "Start a group"); (["-)"; "--end-group"], ([], []), (fun _ -> (fun state1 -> end_group state1)), "End a group"); (["--defsym"], (["SYMBOL=EXPRESSION"], []), (fun _ -> (fun state1 -> state1)), "Define a symbol"); (["-fini"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Call SYMBOL at unload-time"); (["-init"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Call SYMBOL at load-time"); (["--section-start"], (["SECTION=ADDRESS"], []), (fun _ -> (fun state1 -> state1)), "Set address of named section"); (["-Tbss"], (["ADDRESS"], []), (fun _ -> (fun state1 -> state1)), "Set address of .bss section"); (["-Tdata"], (["ADDRESS"], []), (fun _ -> (fun state1 -> state1)), "Set address of .data section"); (["-Ttext"], (["ADDRESS"], []), (fun _ -> (fun state1 -> state1)), "Set address of .text section"); (["-Ttext-segment"], (["ADDRESS"], []), (fun argvals -> set_or_replace_option (TextSegmentStart(parse_address (List.hd (fst argvals))))), "Set address of text segment"); (["-Trodata-segment"], (["ADDRESS"], []), (fun argvals -> set_or_replace_option (RodataSegmentStart(parse_address (List.hd (fst argvals))))), "Set address of rodata segment"); (["-Tldata-segment"], (["ADDRESS"], []), (fun argvals -> set_or_replace_option (LdataSegmentStart(parse_address (List.hd (fst argvals))))), "Set address of ldata segment"); (["--version-script"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Read version information script"); (["--version-exports-section"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Take export symbols list from .exports, using SYMBOL as the version."); (* linker internal debugging/diagnostics and performance tuning *) (["-M"; "--print-map"], ([], []), (fun _ -> (fun state1 -> state1)), "Print map file on standard output"); (["-t"; "--trace"], ([], []), (fun _ -> (fun state1 -> state1)), "Trace file opens"); (["-v"; "--version"], ([], []), (fun _ -> (fun state1 -> state1)), "Print version information"); (["-V"], ([], []), (fun _ -> (fun state1 -> state1)), "Print version and emulation information"); (["-y"; "--trace-symbol"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Trace mentions of SYMBOL"); (["--cref"], ([], []), (fun _ -> (fun state1 -> state1)), "Output cross reference table"); (["--demangle="], ([], ["STYLE"]), (fun _ -> (fun state1 -> state1)), "Demangle symbol names [using STYLE]"); (["--print-gc-sections"], ([], []), (fun _ -> (fun state1 -> state1)), "List removed unused sections on stderr"); (["--no-print-gc-sections"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not list removed unused sections"); (["-Map"], (["FILE"], []), (fun _ -> (fun state1 -> state1)), "Write a map file"); (["-Map="], ([], ["FILE"]), (fun _ -> (fun state1 -> state1)), "Write a map file"); (["--help"], ([], []), (fun _ -> (fun state1 -> state1)), "Print option help"); (["--no-keep-memory"], ([], []), (fun _ -> (fun state1 -> state1)), "Use less memory and more disk I/O"); (["--no-demangle"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not demangle symbol names"); (["--print-output-format"], ([], []), (fun _ -> (fun state1 -> state1)), "Print default output format"); (["--print-sysroot"], ([], []), (fun _ -> (fun state1 -> state1)), "Print current sysroot"); (["--reduce-memory-overheads"], ([], []), (fun _ -> (fun state1 -> state1)), "Reduce memory overheads, possibly taking much longer"); (["--stats"], ([], []), (fun _ -> (fun state1 -> state1)), "Print memory usage statistics"); (["--target-help"], ([], []), (fun _ -> (fun state1 -> state1)), "Display target specific options"); (["--verbose="], ([], ["NUMBER"]), (fun _ -> (fun state1 -> state1)), "Output lots of information during link"); (* unknown *) (["--embedded-relocs"], ([], []), (fun _ -> (fun state1 -> state1)), "Generate embedded relocs"); (["--task-link"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Do task level linking"); (* compatibility *) (["-a"], (["KEYWORD"], []), (fun _ -> (fun state1 -> state1)), "Shared library control for HP/UX compatibility"); (["-Y"], (["PATH"], []), (fun _ -> (fun state1 -> state1)), "Default search path for Solaris compatibility"); (* permissiveness controls (tightening/loosening) *) (["--accept-unknown-input-arch"], ([], []), (fun _ -> (fun state1 -> state1)), "Accept input files whose architecture cannot be determined"); (["--no-accept-unknown-input-arch"], ([], []), (fun _ -> (fun state1 -> state1)), "Reject input files whose architecture is unknown"); (["--fatal-warnings"], ([], []), (fun _ -> (fun state1 -> state1)), "Treat warnings as errors"); (["--no-fatal-warnings"], ([], []), (fun _ -> (fun state1 -> state1)), "Do not treat warnings as errors (default)"); (["--allow-multiple-definition"], ([], []), (fun _ -> (fun state1 -> state1)), "Allow multiple definitions"); (["--no-undefined-version"], ([], []), (fun _ -> (fun state1 -> state1)), "Disallow undefined version"); (["--noinhibit-exec"], ([], []), (fun _ -> (fun state1 -> state1)), "Create an output file even if errors occur"); (["--error-unresolved-symbols"], ([], []), (fun _ -> (fun state1 -> state1)), "Report unresolved symbols as errors"); (["--ignore-unresolved-symbol"], (["SYMBOL"], []), (fun _ -> (fun state1 -> state1)), "Unresolved SYMBOL will not cause an error or warning"); (* permissiveness, specific to ELF emulation *) (["-z muldefs"], ([], []), (fun _ -> (fun state1 -> state1)), "Allow multiple definitions"); (* warnings (enabling/disabling) *) (["--no-warn-mismatch"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't warn about mismatched input files"); (["--no-warn-search-mismatch"], ([], []), (fun _ -> (fun state1 -> state1)), "Don't warn on finding an incompatible library"); (["--warn-common"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn about duplicate common symbols"); (["--warn-constructors"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn if global constructors/destructors are seen"); (["--warn-multiple-gp"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn if the multiple GP values are used"); (["--warn-once"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn only once per undefined symbol"); (["--warn-section-align"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn if start of section changes due to alignment"); (["--warn-shared-textrel"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn if shared object has DT_TEXTREL"); (["--warn-alternate-em"], ([], []), (fun _ -> (fun state1 -> state1)), "Warn if an object has alternate ELF machine code"); (["--warn-unresolved-symbols"], ([], []), (fun _ -> (fun state1 -> state1)), "Report unresolved symbols as warnings"); (* meta-options *) (["--push-state"], ([], []), (fun _ -> (fun state1 -> state1)), "Push state of flags governing input file handling"); (["--pop-state"], ([], []), (fun _ -> (fun state1 -> state1)), "Pop state of flags governing input file handling") (*(["@FILE"], [], fun _ -> (fun state -> state), "Read options from FILE") *) (* processed during word-splitting phase *); ]) (*val delete_trailing_equals: string -> maybe string*) let delete_trailing_equals str:(string)option= (let cs = (Xstring.explode str) in if (listEqualBy (=) ['='] (drop0 ( Nat_big_num.sub_nat(length cs)(Nat_big_num.of_int 1)) cs)) then Some (Xstring.implode ((take0 ( Nat_big_num.sub_nat(length cs)(Nat_big_num.of_int 1)) cs))) else (* let _ = Missing_pervasives.errln ("No trailing equals: " ^ str) in *) None) (*val string_following_equals_at : nat -> string -> maybe string*) let string_following_equals_at pos str:(string)option= (let (first, second) = (Lem_list.split_at pos (Xstring.explode str)) in (match second with '=' :: rest -> Some (Xstring.implode rest) | _ -> (* let _ = Missing_pervasives.errln ("No trailing equals at " ^ (show pos) ^ ": " ^ str) in *) None )) (*val equal_modulo_trailing_equals : string -> string -> bool*) let equal_modulo_trailing_equals argstr argdef:bool= ( (* we allow argdef to have a trailing equals; if it does, * we allow the argstring to have the equals (or not) and trailing stuff, * which will become an arg *)let result = ((match (delete_trailing_equals argdef) with Some matched -> let following_equals = (string_following_equals_at (String.length matched) argstr) in (match following_equals with Some following -> (* okay; does the pre-equals part match? *) matched = Xstring.implode (Lem_list.take ( Nat_num.nat_monus(String.length argdef)( 1)) (Xstring.explode argstr)) | _ -> (* the argstr is allowed not to have a trailing equals *) argstr = matched ) | None -> (* no trailing equals *) argdef = argstr )) in (* let _ = Missing_pervasives.errln ("Do '" ^ argstr ^ "' and '" ^ argdef ^ "' match modulo trailing equals? " ^ (show result)) in *) result) (*val matching_arg_and_alias : string -> list option_def -> maybe (string * option_def)*) let rec matching_arg_and_alias arg options:(string*((string)list*((string)list*(string)list)*(option_argvals ->(command_state)list ->(command_state)list)*string))option= ((match options with [] -> None | (aliases, argspec, meaning, doc) :: more_opts -> (match list_find_opt (fun alias -> equal_modulo_trailing_equals arg alias) aliases with Some found_alias -> Some (found_alias, (aliases, argspec, meaning, doc)) | None -> matching_arg_and_alias arg more_opts ) )) (* We don't try to convert from strings to other things here; * everything we record is either a bool, meaning option -A was "present", for some A, * or a string somearg, meaning option -A somearg was present, for some A. *) (* The above suffices to understand each concrete argument. * Now we define an "interpreted command line" that includes * some useful structure. *) (*val read_one_arg : list command_state -> list string -> (list command_state * list string)*) let read_one_arg state_stack args:(command_state)list*(string)list= ( (* Get the first string and look it up in our table. *)(match args with [] -> (state_stack, []) | some_arg :: more -> (match (matching_arg_and_alias some_arg command_line_table) with (* We need to handle argdefs that have trailing equals. This means * an extra arg might follow the equals. We need some helper functions. *) Some (alias, (aliases, (argspec_extras, argspec_regex), meaning, doc)) -> (* Return a new state, by applying the argument's meaning. * We have to supply the option's argument strings to the meaning function. *) let argstrings = (Lem_list.take (List.length argspec_extras) more) in let regex_matches = ((match delete_trailing_equals some_arg with Some prefix -> (match (string_following_equals_at ( Nat_num.nat_monus(String.length alias)( 1)) some_arg) with Some following_equals -> [following_equals] | None -> failwith "impossible: '=' not where it was a moment ago" ) | None -> [] )) in let new_state_stack = (meaning (argstrings, regex_matches) state_stack) in (new_state_stack, drop0 (length argspec_extras) more) | None -> (* If we didn't match any args, we ought to be an input file. *) (add_input_file state_stack some_arg, more) ) )) (* To fold over the command-line arguments we need a fold that passes * suffixes of the list, not individual elements, and gives us back * the continuation that we need to fold over: a pair of folded-value, new-list. *) (*val foldl_suffix : forall 'a 'b. ('a -> list 'b -> ('a * list 'b)) -> 'a -> list 'b -> 'a*) (* originally foldl *) let rec foldl_suffix f a l:'a= ((match l with | [] -> a | x :: xs -> let (new_a, new_list) = (f a l) in foldl_suffix f new_a new_list )) (* the word-splitting in argv needs a little fixing up. *) (*val cook_argv : list string -> list string -> list string*) let rec cook_argv acc args:(string)list= ((match args with [] -> acc | "-z" :: more -> (match more with [] -> failwith "-z must be followed by another argument" | something :: yetmore -> cook_argv ( List.rev_append (List.rev acc) [("-z " ^ something)]) yetmore ) | something :: more -> cook_argv ( List.rev_append (List.rev acc) [something]) more )) (*val command_line : unit -> interpreted_command_line*) let command_line:unit ->(input_unit)list*(link_option)Pset.set= (fun _ -> ( let cooked_argv = (cook_argv [] (List.tl Ml_bindings.argv_list)) in (* Now we use our fold-alike. *) (match foldl_suffix read_one_arg initial_state0 cooked_argv with state1 :: rest_of_stack -> (state1.input_units, state1.link_options) | _ -> failwith "no command state left" ) ))