Add ocaml run-time and updates to sail for ocaml backend

1 files changed, 317 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/input_list.ml b/lib/ocaml_rts/linksem/input_list.ml
new file mode 100644
index 00000000..fe698586
--- /dev/null
+++ b/lib/ocaml_rts/linksem/input_list.ml
@@ -0,0 +1,317 @@
+(*Generated by Lem from input_list.lem.*)
+open Lem_basic_classes
+open Lem_function
+open Lem_string
+open Lem_string_extra
+open Lem_tuple
+open Lem_bool
+open Lem_list
+open Lem_list_extra
+open Lem_sorting
+open Lem_num
+open Lem_maybe
+open Lem_assert_extra
+
+open Byte_sequence
+open Default_printing
+open Error
+open Missing_pervasives
+open Show
+
+open Archive
+open Command_line
+open Elf_types_native_uint
+open Elf_file
+open Elf_header
+
+(* Here we elaborate away various properties of the command line: 
+ * archives, groups, library paths, -l, --as-needed, --whole-archive,
+ * and which inputs can be used to resolve symbols undefined in which other inputs.
+ * 
+ * What we get out is a list of input files and the options applying to them.
+ * Input files are either relocatable files, shared objects or linker scripts.
+ *)
+
+type input_blob =  Reloc of byte_sequence
+                 | Shared of byte_sequence
+                 | Script of byte_sequence
+                 | ControlScript
+
+(* We remember where the input item came from on the command line,
+ * using "coordinates" identifying the index in the higher-up list
+ * followed by the index within that item. *)
+type origin_coord = InArchive of (Nat_big_num.num * Nat_big_num.num * string * Nat_big_num.num) (* archive-id, pos-within-archive, archive-name, archive-member-count *)
+                  | InGroup of (Nat_big_num.num * Nat_big_num.num)   (* group-id, pos-within-group *)
+                  | InCommandLine of Nat_big_num.num
+                  | Builtin
+
+(*val string_of_origin_coord : origin_coord -> string*)
+let string_of_origin_coord c:string=  ((match c with
+    InArchive(aid, aidx, aname, _) -> "at position " ^ ((Nat_big_num.to_string aidx) ^ (" within archive " ^ (aname ^ (" (at position " ^ ((Nat_big_num.to_string aid) ^ ")")))))
+    | InGroup(gid1, gidx) -> "at position " ^ ((Nat_big_num.to_string gidx) ^ (" within group at position " ^ (Nat_big_num.to_string gid1)))
+    | InCommandLine(cid) -> "(command line)"
+    | Builtin -> "(built-in)"
+))
+
+let instance_Show_Show_Input_list_origin_coord_dict:(origin_coord)show_class= ({
+
+  show_method = string_of_origin_coord})
+
+type input_origin = input_unit * origin_coord list
+
+type input_item = string * input_blob * input_origin
+
+(*val string_of_input_blob : input_blob -> string*)
+let string_of_input_blob item:string=  ((match item with
+    Reloc(seq) -> "relocatable file (" ^ ((Nat_big_num.to_string (Byte_sequence.length0 seq)) ^ " bytes)")
+  | Shared(seq) -> "shared object (" ^ ((Nat_big_num.to_string (Byte_sequence.length0 seq)) ^ " bytes)")
+  | Script(seq) -> "script (" ^ ((Nat_big_num.to_string (Byte_sequence.length0 seq)) ^ " bytes)")
+  | ControlScript -> "the linker control script"
+))
+
+let instance_Show_Show_Input_list_input_blob_dict:(input_blob)show_class= ({
+
+  show_method = string_of_input_blob})
+
+(*val short_string_of_input_item : input_item -> string*)
+let short_string_of_input_item item:string=    
+  (let (fname1, blob, (u, origin)) = item
+    in
+    (match origin with
+        InArchive(aid, aidx, aname, _) :: _ -> aname ^ ("(" ^ (fname1 ^ ")"))
+        | _ -> fname1
+    ))
+
+(* About symbol resolution and "suppliers".
+ * 
+ * Groups change this.
+ * 
+ * When we expand a .a file into a list of .o files, what is the supplier
+ * relation among them? I *THINK* that within the archive, each can supply any other,
+ * but outside the archive, each can only supply leftmore.
+ *)
+
+type can_supply_function = input_item list -> int -> bool list
+
+type input_options =  { item_fmt : string
+                       ; item_check_sections : bool
+                       ; item_copy_dt_needed : bool
+                       ; item_force_output : bool  (* true for .o, false for .a unless --whole-archive, 
+                                                 true for .so with --no-as-needed, 
+                                                 false for .so with --as-needed *)
+                       }
+
+(*val null_input_options : input_options*)
+let null_input_options:input_options=                      
+  ({ item_fmt = ""
+                       ; item_check_sections = false
+                       ; item_copy_dt_needed = false
+                       ; item_force_output = true
+                       })
+
+(*val string_of_input_options : input_options -> string*)
+let string_of_input_options opts:string=  "(some options)"
+
+let instance_Show_Show_Input_list_input_options_dict:(input_options)show_class= ({
+
+  show_method = string_of_input_options})
+
+type input_list = (input_item * input_options) list
+
+(*val toplevel_dot_o_can_supply : list input_item -> nat -> list bool*)
+let toplevel_dot_o_can_supply inputs pos:(bool)list=  
+ (Lem_list.genlist (fun _ -> true) (List.length inputs))
+
+(*val toplevel_shared_can_supply : list input_item -> nat -> list bool*)
+let toplevel_shared_can_supply inputs pos:(bool)list=  
+ (Lem_list.genlist (fun ndx -> ndx <= pos) (List.length inputs))
+ 
+(*val toplevel_archive_can_supply : list input_item -> nat -> list bool*)
+let toplevel_archive_can_supply inputs pos:(bool)list=  
+ (Lem_list.genlist (fun ndx -> ndx <= pos) (List.length inputs))
+
+(*val lib_filename_from_spec : string -> string -> string*)
+let lib_filename_from_spec spec ext:string=    
+ ((match (Xstring.explode spec) with
+        ':' :: more -> (Xstring.implode more)
+        | _ -> "lib" ^ (spec ^ ("." ^ ext))
+    ))
+
+(*val find_library_in : string -> list string -> list string -> maybe string*)
+let find_library_in spec extensions pathlist:(string)option=    
+(  
+    (* Recall the GNU libc's "libc.so is a linker script" hack. 
+     * This tells us that we should only look at file extensions, not contents. *)let file_exists name1=        
+  ((match Byte_sequence.acquire name1 with (* FIXME: use cheaper call *)
+            Success _ -> true
+            | Fail _ -> false
+        ))
+    in
+    let expand_candidate_libname = (fun path -> fun ext -> (path ^ ("/" ^ (lib_filename_from_spec spec ext))))
+    in
+    let get_expansions_existing = (fun path -> 
+        let x2 = ([]) in  List.fold_right (fun cand x2 -> if file_exists cand then cand :: x2 else x2)
+   (Lem_list.map (expand_candidate_libname path) extensions) x2)
+    in
+    let found_by_path = (Lem_list.map (fun path -> (path, get_expansions_existing path)) pathlist)
+    in 
+    (* Do we take the first path for which some extension is found? 
+     * Or do we keep going if we prefer shared libraries, say? 
+     * I think it's the former. *)
+    (match Lem_list.list_find_opt (fun (path, exps) -> (List.length exps) > 0) found_by_path with
+        Some (path, exps) -> Some(List.hd exps)
+        | None -> None
+    ))
+
+(*val find_one_library_filename : input_file_options -> string -> string*)
+let find_one_library_filename options str:string=    
+  (let extensions = (if options.input_link_sharedlibs then ["so"; "a"] else ["a"])
+    in
+    let found = (find_library_in str extensions options.input_libpath)
+    in (match found with
+        None -> failwith ("couldn't find library matching '" ^ (str ^ "'"))
+        | Some result -> result
+    ))
+
+(*val is_elf64_with_type : elf64_half -> byte_sequence -> bool*)
+let is_elf64_with_type typ seq:bool=    
+(  
+    (*let _ = Missing_pervasives.errs ("elf64? " ^ 
+        (match seq with Sequence(bs) -> show (List.take 16 bs) end))
+    in*)(match Elf_file.read_elf64_file seq with
+    Success(e) -> (* let _ = Missing_pervasives.errln ": yes" in *) (e.elf64_file_header.elf64_type = typ)
+    | Fail _ -> (* let _ = Missing_pervasives.errln ": no" in *) false
+    ))
+
+(*val is_archive : byte_sequence -> bool*)
+let is_archive seq:bool=    
+ ((match read_archive_global_header seq with
+        Success _ -> true
+        | Fail _ -> false
+    ))
+
+(*val open_file_and_expand : string -> input_unit -> natural -> list input_item*)
+let open_file_and_expand toplevel_fname u fpos:(string*input_blob*(input_unit*(origin_coord)list))list=    
+  ((match Byte_sequence.acquire toplevel_fname with
+        Fail _ -> failwith ("could not open file " ^ toplevel_fname)
+        | Success seq ->
+            if is_elf64_with_type (Uint32.of_string (Nat_big_num.to_string elf_ft_rel)) seq 
+            then [(toplevel_fname, Reloc(seq), (u, []))]
+            else if is_elf64_with_type (Uint32.of_string (Nat_big_num.to_string elf_ft_dyn)) seq 
+                then [(toplevel_fname, Shared(seq), (u, []))]
+                else if is_archive seq 
+                    then
+                        (match read_archive seq with
+                            Fail _ -> failwith ("could not read archive " ^ toplevel_fname)
+                            | Success (pairs : (string * byte_sequence) list) -> 
+                                (*let _ = Missing_pervasives.errln (toplevel_fname ^ " is an archive with " ^ (show (List.length pairs)) ^ " members")
+                                in*) 
+                                let not_elf = (List.filter (fun (inner_fname, seq) -> not (is_elf64_with_type (Uint32.of_string (Nat_big_num.to_string elf_ft_rel)) seq)) pairs) 
+                                in
+                                if List.length not_elf = 0 
+                                then mapMaybei 
+                                    (fun (i : Nat_big_num.num) -> (fun ((inner_fname : string), seq) -> 
+                                        let (trimmed_inner_fname : string) = ((match ((Ml_bindings.string_index_of '/' inner_fname) :  Nat_big_num.num option) with
+                                            None -> inner_fname
+                                            | Some (ind : Nat_big_num.num) -> (match Ml_bindings.string_prefix ind inner_fname with
+                                                Some s -> s
+                                                | None -> failwith "impossible: string has character index >= its length"
+                                            )
+                                        ))
+                                        in
+                                        Some (trimmed_inner_fname, Reloc(seq), (u, [InArchive(fpos, i, toplevel_fname, length pairs)]))
+                                    )) pairs
+                                else let (names, seqs) = (List.split not_elf) in 
+                                    failwith ("archive with unsupported contents" (*(" ^ (show names) ^ ")*))
+                )
+            else [(toplevel_fname, Script(seq), (u, []))]
+    ))
+
+(*val make_input_items_and_options : list input_item -> Command_line.input_file_options -> list origin_coord -> list (input_item * input_options)*)
+let make_input_items_and_options file_list cmdopts coords_to_append:((string*input_blob*(input_unit*(origin_coord)list))*input_options)list=    
+ ((match file_list with
+         [] -> failwith "impossible: empty list of files"
+       | [(fname1, Reloc(seq), (u, coords))] -> 
+            [((fname1, Reloc(seq), (u,  List.rev_append (List.rev coords) coords_to_append)), 
+                { item_fmt = (cmdopts.input_fmt)
+                 ; item_check_sections = (cmdopts.input_check_sections)
+                 ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed)
+                 ; item_force_output = true
+                 })]
+       | [(fname1, Shared(seq), (u, coords))] ->
+            [((fname1, Shared(seq), (u,  List.rev_append (List.rev coords) coords_to_append)), 
+                 { item_fmt = (cmdopts.input_fmt)
+                  ; item_check_sections = (cmdopts.input_check_sections)
+                  ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed)
+                  ; item_force_output = (if cmdopts.input_as_needed then false else true)
+                  })]
+       | [(fname1, Script(seq), (u, coords))] ->
+            [((fname1, Script(seq), (u,  List.rev_append (List.rev coords) coords_to_append)), 
+                { item_fmt = (cmdopts.input_fmt)
+                 ; item_check_sections = (cmdopts.input_check_sections)
+                 ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed)
+                 ; item_force_output = true
+                 })]
+       | _ -> (* guaranteed to be all relocs, from one archive *)
+            let (items_and_options : (input_item * input_options) list) =                
+ (mapMaybei (fun i -> (fun (fname1, reloc1, (u, coords)) -> 
+                    let (item : input_item) = (fname1, reloc1, (u,  List.rev_append (List.rev coords) coords_to_append))
+                    in
+                    let (options : input_options) =                          
+ ({ item_fmt = (cmdopts.input_fmt)
+                           ; item_check_sections = (cmdopts.input_check_sections)
+                           ; item_copy_dt_needed = (cmdopts.input_copy_dt_needed)
+                           ; item_force_output = (if cmdopts.input_whole_archive then true else false)
+                           })
+                    in Some (item, options)
+                )) file_list)
+            in items_and_options
+       | _ -> failwith "impossible expanded input item"
+   ))
+
+(*val elaborate_input_helper : natural -> list Command_line.input_unit -> input_list -> input_list*)
+let rec elaborate_input_helper input_pos inputs acc:(input_item*input_options)list=    
+  ((match inputs with
+        [] -> acc
+        | input :: more_inputs -> 
+            (match input with 
+                File(spec, options)
+                    -> (match spec with
+                        Filename(str)
+                            -> elaborate_input_helper ( Nat_big_num.add input_pos(Nat_big_num.of_int 1)) more_inputs 
+                                ( List.rev_append (List.rev acc) (make_input_items_and_options
+                                    (open_file_and_expand str input input_pos) options [InCommandLine(input_pos)]))
+                        | Libname(str) 
+                            -> elaborate_input_helper ( Nat_big_num.add input_pos(Nat_big_num.of_int 1)) more_inputs 
+                                ( List.rev_append (List.rev acc) (make_input_items_and_options 
+                                    (open_file_and_expand (find_one_library_filename options str) input input_pos)
+                                        options [InCommandLine(input_pos)]))
+                        )
+                | Group(specs_and_options) ->
+                    (* Every member of a group is either a filename or a libname.
+                     * First expand the libnames, leaving the Group intact. *)
+                    let group_with_lib_files
+                     = (Lem_list.map (fun (spec, options) -> (match spec with 
+                         Filename(str) -> (str, options)
+                         | Libname(str) -> (find_one_library_filename options str, options)
+                         )) specs_and_options)
+                    in
+                    (* Now expand archives into file lists. *)
+                    let group_with_file_lists 
+                     = (mapMaybei (fun i -> (fun (str, options) -> 
+                        Some ((open_file_and_expand str input input_pos), options)
+                        )) group_with_lib_files)
+                    in
+                    (* Now expand them into files and fix up the options appropriately *)
+                    let to_add
+                     = (mapMaybei (fun index_in_group -> (fun (file_list, options) -> (
+                        Some(
+                            make_input_items_and_options file_list options [InGroup(input_pos, index_in_group); InCommandLine(input_pos)]
+                        )))) group_with_file_lists)
+                    in
+                    elaborate_input_helper ( Nat_big_num.add input_pos(Nat_big_num.of_int 1)) more_inputs ( List.rev_append (List.rev acc) (List.concat to_add))
+            )
+    ))
+    
+(*val elaborate_input : list Command_line.input_unit -> input_list*)
+let rec elaborate_input inputs:(input_item*input_options)list=  (elaborate_input_helper(Nat_big_num.of_int 0) inputs [])