diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/adaptors/sail_interface.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/adaptors/sail_interface.ml | 250 |
1 files changed, 250 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/adaptors/sail_interface.ml b/lib/ocaml_rts/linksem/adaptors/sail_interface.ml new file mode 100644 index 00000000..f3024467 --- /dev/null +++ b/lib/ocaml_rts/linksem/adaptors/sail_interface.ml @@ -0,0 +1,250 @@ +(*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" + ))) |