Source file command_line.ml

(*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 <NUMBER>");
  (["--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.  <method> 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"
    )
))