Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 158 deletions

diff --git a/lib/ocaml_rts/linksem/main_link.ml b/lib/ocaml_rts/linksem/main_link.ml
deleted file mode 100644
index 82999d53..00000000
--- a/lib/ocaml_rts/linksem/main_link.ml
+++ /dev/null
@@ -1,158 +0,0 @@
-(*Generated by Lem from main_link.lem.*)
-open Lem_basic_classes
-open Lem_function
-open Lem_string
-open Lem_tuple
-open Lem_bool
-open Lem_list
-open Lem_sorting
-(*import Map*)
-(*import Set*)
-(*import Set_extra*)
-open Lem_num
-open Lem_maybe
-open Lem_assert_extra
-
-open Byte_sequence
-open Default_printing
-open Error
-open Missing_pervasives
-open Show
-open Endianness
-
-open Elf_header
-open Elf_file
-open Elf_interpreted_section
-open Elf_interpreted_segment
-open Elf_section_header_table
-open Elf_program_header_table
-open Elf_types_native_uint
-open Elf_relocation
-open String_table
-
-open Abi_amd64_elf_header
-open Abi_amd64_serialisation
-open Abis
-(*import Gnu_ext_abi*)
-
-open Command_line
-open Input_list
-open Linkable_list
-
-open Memory_image
-open Elf_memory_image
-open Elf_memory_image_of_elf64_file
-open Elf64_file_of_elf_memory_image
-
-open Linker_script
-open Link
-
-(*val images_consistent : elf_memory_image -> elf_memory_image -> bool*)
-let images_consistent img1 img2:bool= 
-    (* img1.by_tag = img2.by_tag *) true
-
-(*val correctly_linked : abi any_abi_feature -> linkable_list -> list string -> set link_option -> elf64_file -> maybe elf_memory_image*)
-let correctly_linked a linkables names options eout:((any_abi_feature)annotated_memory_image)option=    
-  (let output_image = (elf_memory_image_of_elf64_file a "(output file)" eout)
-    in
-    let (fresh, alloc_map, script1) = (default_linker_control_script(Nat_big_num.of_int 0) (Pmap.empty Nat_big_num.compare) a 
-        (* user_text_segment_start *) ((match Command_line.find_option_matching_tag (TextSegmentStart(Nat_big_num.of_int 0)) options with Some(TextSegmentStart(addr)) -> Some addr | _ -> None ))
-        (* user_data_segment_start *) None
-        (* user_rodata_segment_start *) ((match Command_line.find_option_matching_tag (RodataSegmentStart(Nat_big_num.of_int 0)) options with Some(RodataSegmentStart(addr)) -> Some addr | _ -> None ))
-        (* elf_headers_size *)
-            ( Nat_big_num.add(Nat_big_num.of_int 
-                (* ELF header size *)64) (Nat_big_num.mul a.max_phnum(Nat_big_num.of_int 56)) (* size of one phdr *)
-            ))
-    in
-    let linked_image = (link alloc_map script1 a options linkables)
-    in
-    if images_consistent output_image linked_image then Some linked_image else None)
-
-(* We need to elaborate the command line to handle objects, archives 
- * and archive groups appropriately. 
- * We could imagine a relation between objects such that 
- * (o1, o2) is in the relation
- * iff definitions in o1 might be used to satisfy references in o2. ("o1 supplies o2")
- * If o1 is a .o, all other .o files are searched.
- * If o1 comes from an archive and is not in a group, it only supplies *preceding* objects (whether from an archive or a .o).
- * If o1 comes from an archive in a group, it supplies preceding objects and any objects from the same group.
- * 
- * That doesn't capture the ordering, though: 
- * for each object, there's an ordered list of other objects 
- * in which to search for the *first* definition. *)
-
-let ( _:unit) =  
-(let res =    
-(let (input_units1, link_options1) = (command_line ())
-    in
-    let items_and_options = (elaborate_input input_units1)
-    in
-    let (input_items, item_options) = (List.split items_and_options)
-    in
-    let _ = (prerr_endline ("Got " ^ ((Pervasives.string_of_int (List.length input_items)) ^ (" input items: {"
-        ^ ((List.fold_left (^) "" (Lem_list.map (fun item -> (string_of_triple 
-  instance_Show_Show_string_dict instance_Show_Show_Input_list_input_blob_dict (instance_Show_Show_tup2_dict instance_Show_Show_Command_line_input_unit_dict
-   (instance_Show_Show_list_dict
-      instance_Show_Show_Input_list_origin_coord_dict)) item) ^ ",\n") input_items)) ^ "}")))))
-    in
-    let output_filename = ((match Command_line.find_option_matching_tag (Command_line.OutputFilename("")) link_options1 with
-        None -> "impossible: no output file specified, despite default value of `a.out'"
-        | Some (Command_line.OutputFilename(s)) -> s
-        | _ -> "impossible: bad output filename option returned"
-    ))
-    in
-    Byte_sequence.acquire output_filename >>= (fun out ->
-    let _ = (prerr_endline ("Successfully opened output file")) in
-    Elf_file.read_elf64_file out >>= (fun eout ->
-    let _ = (prerr_endline ("Output file seems to be an ELF file")) in
-    let guessed_abi = (list_find_opt (fun a -> a.is_valid_elf_header eout.elf64_file_header) all_abis)
-    in
-    let a = ((match guessed_abi with
-      Some a -> if (* get_elf64_osabi eout.elf64_file_header = elf_osabi_gnu *) true
-                    (* The GNU linker does not set the ABI to "GNU", but happily uses GNU extensions.
-                     * FIXME: delegate to a personality function here
-                     *)
-                    then let _ = (prerr_endline "Using GNU-extended ABI") in Gnu_ext_abi.gnu_extend (Abis.tls_extend a) 
-                    else (Abis.tls_extend a)
-      | None -> failwith "output file does not conform to any known ABI"
-    ))
-    in
-    let make_linkable = (fun (it, opts) -> linkable_item_of_input_item_and_options a it opts)
-    in
-    let linkable_items_and_options = (Lem_list.map make_linkable items_and_options)
-    in
-    let names = (Lem_list.map  
-  (string_of_triple instance_Show_Show_string_dict
-     instance_Show_Show_Input_list_input_blob_dict
-     (instance_Show_Show_tup2_dict
-        instance_Show_Show_Command_line_input_unit_dict
-        (instance_Show_Show_list_dict
-           instance_Show_Show_Input_list_origin_coord_dict))) input_items)
-    in 
-    let maybe_symbolic_image = (correctly_linked a linkable_items_and_options names link_options1 eout)
-    in
-    let v = ((match maybe_symbolic_image with 
-        None -> false 
-        | Some img2 ->
-            (* generate some output, using the symbolic image we just got *)
-            let our_output_filename = (output_filename ^ ".test-out")
-            in
-            let f = (elf64_file_of_elf_memory_image a (fun x -> x) our_output_filename img2)
-            in
-            (match 
-            bytes_of_elf64_file f >>= (fun bytes -> 
-                Byte_sequence.serialise our_output_filename bytes)
-            with
-                Success _ -> true
-                | Fail s -> let _ = (print_endline ("error writing output: " ^ s)) in true
-            )
-    ))
-    in
-    return (string_of_bool v))))
-  in
-    (match res with
-      | Fail err  -> prerr_endline ("[!]: " ^ err)
-      | Success e -> prerr_endline e
-    ))
-
-