Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 671 deletions

diff --git a/lib/ocaml_rts/linksem/command_line.ml b/lib/ocaml_rts/linksem/command_line.ml
deleted file mode 100644
index 62d4b87e..00000000
--- a/lib/ocaml_rts/linksem/command_line.ml
+++ /dev/null
@@ -1,671 +0,0 @@
-(*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"
-    )
-))