Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 250 deletions

diff --git a/lib/ocaml_rts/linksem/adaptors/sail_interface.ml b/lib/ocaml_rts/linksem/adaptors/sail_interface.ml
deleted file mode 100644
index f3024467..00000000
--- a/lib/ocaml_rts/linksem/adaptors/sail_interface.ml
+++ /dev/null
@@ -1,250 +0,0 @@
-(*Generated by Lem from adaptors/sail_interface.lem.*)
-open Lem_basic_classes
-open Lem_function
-open Lem_list
-open Lem_maybe
-open Lem_num
-open Lem_string
-open Lem_tuple
-
-open Lem_assert_extra
-
-open Byte_sequence
-open Error
-open Missing_pervasives
-open Show
-
-open Elf_header
-open Elf_file
-open Elf_interpreted_section
-open Elf_interpreted_segment
-open String_table
-open Elf_symbol_table
-open Elf_program_header_table
-open Elf_types_native_uint
-
-open Hex_printing
-
-type executable_process_image =
-  | ELF_Class_32 of elf32_executable_process_image
-  | ELF_Class_64 of elf64_executable_process_image
-
-(*val string_of_segment_provenance : segment_provenance -> string*)
-let string_of_segment_provenance p:string=  
- ((match p with
-    | FromELF -> "Segment from ELF file"
-    | AutoGenerated -> "Segment auto generated"
-  ))
-
-(*val string_of_executable_process_image : executable_process_image -> string*)
-let string_of_executable_process_image img2:string=  
- ((match img2 with
-    | ELF_Class_32 (segs, entry_point, machine_type) ->
-        let machine_type = (string_of_elf_machine_architecture machine_type) in
-        let entry_point  = (unsafe_hex_string_of_natural( 16) entry_point) in
-        let segs         = (Lem_list.map (fun (seg, prov) ->
-                             let prov = (string_of_segment_provenance prov) in
-                             let seg  = (string_of_elf32_interpreted_segment seg) in
-                                 "Segment provenance: " ^ (prov ^ ("\n" ^ seg))
-                           ) segs)
-        in
-          unlines ( List.rev_append (List.rev [
-            "32-bit ELF executable image"
-          ; ("Machine type: " ^ machine_type)
-          ; ("Entry point: " ^ entry_point)
-          ; ""
-          ]) segs)
-    | ELF_Class_64 (segs, entry_point, machine_type) ->
-        let machine_type = (string_of_elf_machine_architecture machine_type) in
-        let entry_point  = (unsafe_hex_string_of_natural( 16) entry_point) in
-        let segs         = (intercalate "\n" (Lem_list.map (fun (seg, prov) ->
-                             let prov = (string_of_segment_provenance prov) in
-                             let seg  = (string_of_elf64_interpreted_segment seg) in
-                                 "Segment provenance: " ^ (prov ^ ("\n" ^ seg))
-                           ) segs))
-        in
-          unlines ( List.rev_append (List.rev [
-            "64-bit ELF executable image"
-          ; ("Machine type: " ^ machine_type)
-          ; ("Entry point: " ^ entry_point)
-          ; ""
-          ]) segs)
-  ))
-
-(*val populate : string -> error executable_process_image*)
-let populate fname1:(executable_process_image)error=  
-( 
-  (* Acquire the data from the file... *)Byte_sequence.acquire fname1 >>= (fun bs0 ->
-  (* Read the magic number and the flags in the header... *)
-  repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
-    (match Lem_list.list_index ident( 4) with
-      | None -> fail "populate: ELF ident transcription error"
-      | Some c  ->
-        (* Calculate whether we are dealing with a 32- or 64-bit file based on
-         * what we have read...
-         *)
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
-          Elf_file.read_elf32_file bs0 >>= (fun ef5 ->
-          if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then
-            Elf_file.get_elf32_executable_image ef5 >>= (fun img2 ->
-            return (ELF_Class_32 img2))
-          else
-            fail "populate: not a statically linked executable")
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
-          Elf_file.read_elf64_file bs0 >>= (fun ef5 ->
-          if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then
-            Elf_file.get_elf64_executable_image ef5 >>= (fun img2 ->
-            return (ELF_Class_64 img2))
-          else
-            fail "populate: not a statically linked executable")
-        else
-          fail "populate: ELF class unrecognised"
-    ))))
-
-(*val populate' : byte_sequence -> error executable_process_image*)
-let populate' bs0:(executable_process_image)error=  
-( 
-  (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
-    (match Lem_list.list_index ident( 4) with
-      | None -> fail "populate': ELF ident transcription error"
-      | Some c  ->
-        (* Calculate whether we are dealing with a 32- or 64-bit file based on
-         * what we have read...
-         *)
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
-          Elf_file.read_elf32_file bs0 >>= (fun ef5 ->
-          if Elf_program_header_table.get_elf32_static_linked ef5.elf32_file_program_header_table then
-            Elf_file.get_elf32_executable_image ef5 >>= (fun img2 ->
-            return (ELF_Class_32 img2))
-          else
-            fail "populate': not a statically linked executable")
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
-          Elf_file.read_elf64_file bs0 >>= (fun ef5 ->
-          if Elf_program_header_table.get_elf64_static_linked ef5.elf64_file_program_header_table then
-            Elf_file.get_elf64_executable_image ef5 >>= (fun img2 ->
-            return (ELF_Class_64 img2))
-          else
-            fail "populate': not a statically linked executable")
-        else
-          fail "populate': ELF class unrecognised"
-    )))
-
-(*val obtain_global_symbol_init_info : string -> error global_symbol_init_info*)
-let obtain_global_symbol_init_info fname1:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
-( 
-  (* Acquire the data from the file... *)Byte_sequence.acquire fname1 >>= (fun bs0 ->
-  (* Read the magic number and the flags in the header... *)
-  repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
-    (match Lem_list.list_index ident( 4) with
-      | None -> fail "obtain_global_symbol_init_info: ELF ident transcription error"
-      | Some c  ->
-        (* Calculate whether we are dealing with a 32- or 64-bit file based on
-         * what we have read...
-         *)
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
-          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
-            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
-            return init1)
-          else
-            fail "obtain_global_symbol_init_info: not a statically linked executable")
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
-          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
-            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
-            return init1)
-          else
-            fail "obtain_global_symbol_init_info: not a statically linked executable")
-        else
-          fail "obtain_global_symbol_init_info: ELF class unrecognised"
-    ))))
-
-(*val obtain_global_symbol_init_info' : byte_sequence -> error global_symbol_init_info*)
-let obtain_global_symbol_init_info' bs0:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
-( 
-  (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
-    (match Lem_list.list_index ident( 4) with
-      | None -> fail "obtain_global_symbol_init_info': ELF ident transcription error"
-      | Some c  ->
-        (* Calculate whether we are dealing with a 32- or 64-bit file based on
-         * what we have read...
-         *)
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
-          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
-            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
-            return init1)
-          else
-            fail "obtain_global_symbol_init_info': not a statically linked executable")
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
-          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
-            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
-            return init1)
-          else
-            fail "obtain_global_symbol_init_info': not a statically linked executable")
-        else
-          fail "obtain_global_symbol_init_info': ELF class unrecognised"
-    )))
-
-(*val populate_and_obtain_global_symbol_init_info : string -> error (elf_file * executable_process_image * global_symbol_init_info)*)
-let populate_and_obtain_global_symbol_init_info fname1:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
-( 
-  (* Acquire the data from the file... *)Byte_sequence.acquire fname1 >>= (fun bs0 ->
-  (* Read the magic number and the flags in the header... *)
-  repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
-    (match Lem_list.list_index ident( 4) with
-      | None -> fail "populate_and_obtain_global_symbol_init_info: ELF ident transcription error"
-      | Some c  ->
-        (* Calculate whether we are dealing with a 32- or 64-bit file based on
-         * what we have read...
-         *)
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
-          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
-            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
-            Elf_file.get_elf32_executable_image f1 >>= (fun img2 ->           
-            return ((ELF_File_32 f1), (ELF_Class_32 img2), init1)))
-          else
-            fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable")
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
-          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
-            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
-            Elf_file.get_elf64_executable_image f1 >>= (fun img2 ->
-            return ((ELF_File_64 f1), (ELF_Class_64 img2), init1)))
-          else
-            fail "populate_and_obtain_global_symbol_init_info: not a statically linked executable")
-        else
-          fail "populate_and_obtain_global_symbol_init_info: ELF class unrecognised"
-    ))))
-
-(*val populate_and_obtain_global_symbol_init_info' : byte_sequence -> error (elf_file * executable_process_image * global_symbol_init_info)*)
-let populate_and_obtain_global_symbol_init_info' bs0:(elf_file*executable_process_image*(string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(byte_sequence)option*Nat_big_num.num))list)error=  
-( 
-  (* Read the magic number and the flags in the header... *)repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) ->
-    (match Lem_list.list_index ident( 4) with
-      | None -> fail "populate_and_obtain_global_symbol_init_info': ELF ident transcription error"
-      | Some c  ->
-        (* Calculate whether we are dealing with a 32- or 64-bit file based on
-         * what we have read...
-         *)
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then
-          Elf_file.read_elf32_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf32_static_linked f1.elf32_file_program_header_table then
-            Elf_file.get_elf32_file_global_symbol_init f1 >>= (fun init1 ->
-            Elf_file.get_elf32_executable_image f1 >>= (fun img2 ->           
-            return ((ELF_File_32 f1), (ELF_Class_32 img2), init1)))
-          else
-            fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable")
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then
-          Elf_file.read_elf64_file bs0 >>= (fun f1 ->
-          if Elf_program_header_table.get_elf64_static_linked f1.elf64_file_program_header_table then
-            Elf_file.get_elf64_file_global_symbol_init f1 >>= (fun init1 ->
-            Elf_file.get_elf64_executable_image f1 >>= (fun img2 ->
-            return ((ELF_File_64 f1), (ELF_Class_64 img2), init1)))
-          else
-            fail "populate_and_obtain_global_symbol_init_info': not a statically linked executable")
-        else
-          fail "populate_and_obtain_global_symbol_init_info': ELF class unrecognised"
-    )))