diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/main_elf.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/main_elf.ml | 374 |
1 files changed, 0 insertions, 374 deletions
diff --git a/lib/ocaml_rts/linksem/main_elf.ml b/lib/ocaml_rts/linksem/main_elf.ml deleted file mode 100644 index c5a31ebe..00000000 --- a/lib/ocaml_rts/linksem/main_elf.ml +++ /dev/null @@ -1,374 +0,0 @@ -(*Generated by Lem from main_elf.lem.*) -(** [main_elf], the main module for the test program of the ELF development. - * Run like so: - * ./main_elf.opt --FLAG BINARY - * where: - * BINARY is an ELF binary - * FLAG is in the set { file-header, program-headers, section-headers, - * dynamic, relocs, symbols } - * - *) - -open Lem_basic_classes -open Lem_function -open Lem_maybe -open Lem_list -open Lem_num -open Lem_string -open Lem_tuple - -open Byte_sequence -open Default_printing -open Error -open Hex_printing -open Missing_pervasives -open Show -open Lem_assert_extra - -open Endianness - -open Elf_dynamic -open Elf_header -open Elf_file -open Elf_program_header_table -open Elf_section_header_table -open Elf_types_native_uint - -open Harness_interface -open Sail_interface - -open Abi_aarch64_relocation - -open Abi_amd64_elf_header -open Abi_amd64_relocation -open Abi_amd64_serialisation - -open Abi_power64_dynamic - -open Abi_x86_relocation - -open Abi_power64_relocation - -open Gnu_ext_dynamic -open Gnu_ext_program_header_table -open Gnu_ext_section_header_table - -open Dwarf - -let default_hdr_bdl:('a ->string)*('b ->string)= - (default_os_specific_print, default_proc_specific_print) - -let default_pht_bdl:('a ->string)*('b ->string)= - (default_os_specific_print, default_proc_specific_print) - -let default_sht_bdl:('b ->string)*('a ->string)*('c ->string)= - (default_os_specific_print, default_proc_specific_print, default_user_specific_print) - - -(* unrolled and made tail recursive for efficiency on large ELF files...*) -(*val chunks : list string -> list (list string) -> list (list string) * nat*) -let rec chunks (ss : string list) (accum : ( string list) list):((string)list)list*int= - ((match ss with - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::s11::s12::s13::s14::s15::s16::ss -> - chunks ss ([(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9);(s12^s11);(s14^s13);(s16^s15)]::accum) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::s11::s12::s13::s14::s15::[] -> - let buff = ([(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9);(s12^s11);(s14^s13);("00"^s15)]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 15) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::s11::s12::s13::s14::ss -> - let bits = (replicate0(Nat_big_num.of_int 1) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9);(s12^s11);(s14^s13)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 14) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::s11::s12::s13::[] -> - let bits = (replicate0(Nat_big_num.of_int 1) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9);(s12^s11);("00"^s13)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 13) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::s11::s12::[] -> - let bits = (replicate0(Nat_big_num.of_int 2) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9);(s12^s11)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 12) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::s11::[] -> - let bits = (replicate0(Nat_big_num.of_int 2) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9);("00"^s11)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 11) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::s10::[] -> - let bits = (replicate0(Nat_big_num.of_int 3) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7);(s10^s9)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 10) - | s1::s2::s3::s4::s5::s6::s7::s8::s9::[] -> - let bits = (replicate0(Nat_big_num.of_int 3) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7);("00"^s9)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 9) - | s1::s2::s3::s4::s5::s6::s7::s8::[] -> - let bits = (replicate0(Nat_big_num.of_int 4) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);(s8^s7)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 8) - | s1::s2::s3::s4::s5::s6::s7::[] -> - let bits = (replicate0(Nat_big_num.of_int 4) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5);("00"^s7)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 7) - | s1::s2::s3::s4::s5::s6::[] -> - let bits = (replicate0(Nat_big_num.of_int 5) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);(s6^s5)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 6) - | s1::s2::s3::s4::s5::[] -> - let bits = (replicate0(Nat_big_num.of_int 5) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3);("00"^s5)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 5) - | s1::s2::s3::s4::[] -> - let bits = (replicate0(Nat_big_num.of_int 6) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);(s4^s3)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 4) - | s1::s2::s3::[] -> - let bits = (replicate0(Nat_big_num.of_int 6) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1);("00"^s3)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 3) - | s1::s2::[] -> - let bits = (replicate0(Nat_big_num.of_int 7) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [(s2^s1)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 2) - | s1::[] -> - let bits = (replicate0(Nat_big_num.of_int 7) " ") in - let fixed = (intercalate " " bits) in - let buff = (List.rev_append (List.rev [("00"^s1)]) [concatS fixed]) in - ( List.rev_append (List.rev (List.rev accum)) [buff], 1) - | [] -> (List.rev accum, 0) - )) - -(*val provide_offsets : (list (list string) * nat) -> list (string * list string)*) -let provide_offsets (ss, ed):(string*(string)list)list= - - (List.rev_append (List.rev (Lem_list.mapi (fun i x -> - let hx = (unsafe_hex_string_of_natural( 7) ( Nat_big_num.mul(Nat_big_num.of_int i)(Nat_big_num.of_int 16))) in - (hx, x)) ss)) (if ed = 0 then - [(unsafe_hex_string_of_natural( 7) ( Nat_big_num.mul(Nat_big_num.of_int (List.length ss))(Nat_big_num.of_int 16)), [])] - else - [(unsafe_hex_string_of_natural( 7) ( Nat_big_num.add( Nat_big_num.mul(Nat_big_num.of_int ( Nat_num.nat_monus(List.length ss)( 1)))(Nat_big_num.of_int 16)) (Nat_big_num.of_int ed)), [])])) - -(*val create_chunks : byte_sequence -> list (string * list string)*) -let create_chunks bs0:(string*(string)list)list= - (let ss = (Lem_list.map (fun x -> - unsafe_hex_string_of_natural( 2) (natural_of_byte x)) - (Byte_sequence.byte_list_of_byte_sequence bs0)) - in - provide_offsets (chunks ss [])) - -(*val print_chunk : string * list string -> string*) -let print_chunk (off, ss):string= - ((match ss with - | [] -> off - | _ -> off ^ (" " ^ concatS (intercalate " " ss)) - )) - -(*val obtain_abi_specific_string_of_reloc_type : natural -> (natural -> string)*) -let obtain_abi_specific_string_of_reloc_type mach:Nat_big_num.num ->string= - (if Nat_big_num.equal mach elf_ma_ppc64 then - string_of_ppc64_relocation_type - else if Nat_big_num.equal mach elf_ma_386 then - string_of_x86_relocation_type - else if Nat_big_num.equal mach elf_ma_aarch64 then - string_of_aarch64_relocation_type - else if Nat_big_num.equal mach elf_ma_x86_64 then - string_of_amd64_relocation_type - (*else if mach = elf_ma_mips then - string_of_mips64_relocation_type*) - else - (fun y->"Cannot deduce ABI")) - -let ( _:unit) = -(let res = -(let (flag, arg) = -((match Ml_bindings.argv_list with - | progname::flag::fname1::more -> (flag, fname1) - | _ -> failwith "usage: main_elf <flag> <fname>" - )) - in - Byte_sequence.acquire arg >>= (fun bs0 -> - repeatM' Elf_header.ei_nident bs0 (read_unsigned_char Endianness.default_endianness) >>= (fun (ident, bs) -> - (match Lem_list.list_index ident( 4) with - | None -> failwith "ELF ident transcription error" - | Some c -> - if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_32 then - let ret = -(if flag = "--file-header" then - Elf_header.read_elf32_header bs0 >>= (fun (hdr, _) -> - return (Harness_interface.harness_string_of_elf32_file_header hdr)) - else if flag = "--program-headers" then - Elf_file.read_elf32_file bs0 >>= (fun f1 -> - get_elf32_file_section_header_string_table f1 >>= (fun stbl -> - return (Harness_interface.harness_string_of_elf32_program_headers - string_of_gnu_ext_segment_type - (fun x -> - Nat_big_num.to_string x) - f1.elf32_file_header - f1.elf32_file_program_header_table - f1.elf32_file_section_header_table - stbl - bs0))) - else if flag = "--section-headers" then - Elf_file.read_elf32_file bs0 >>= (fun f1 -> - get_elf32_file_section_header_string_table f1 >>= (fun stbl -> - return (Harness_interface.harness_string_of_elf32_section_headers - string_of_gnu_ext_section_type - (fun x -> Nat_big_num.to_string x) - (fun x -> Nat_big_num.to_string x) - f1.elf32_file_header - f1.elf32_file_section_header_table - stbl))) - else if flag = "--relocs" then - Elf_file.read_elf32_file bs0 >>= (fun f1 -> - let print_reloc = (obtain_abi_specific_string_of_reloc_type (Nat_big_num.of_string (Uint32.to_string f1.elf32_file_header.elf32_machine))) in - return (Harness_interface.harness_string_of_elf32_relocs - f1 - print_reloc - bs0)) -(* else if flag = "--symbols" then - Harness_interface.harness_string_of_elf32_syms - f1 - show - show - bs0 *) - else if flag = "--dynamic" then - Elf_file.read_elf32_file bs0 >>= (fun f1 -> - let so = (is_elf32_shared_object_file f1.elf32_file_header) in - return (Harness_interface.harness_string_of_elf32_dynamic_section - f1 - bs0 - gnu_ext_os_additional_ranges - (fun x -> gnu_ext_tag_correspondence_of_tag x) - (fun x -> gnu_ext_tag_correspondence_of_tag x) - (fun x -> string_of_dynamic_tag so x gnu_ext_os_additional_ranges string_of_gnu_ext_dynamic_tag (fun _ -> "proc: from main_elf")) - gnu_ext_elf32_value_of_elf32_dyn - (fun _ _ -> Error.fail "proc: from main_elf"))) - else if flag = "--in-out" then - Elf_file.read_elf32_file bs0 >>= (fun f1 -> - (match Elf_file.bytes_of_elf32_file f1 with - | Fail f -> return f - | Success s -> - let chunks1 = (create_chunks s) in - let lines = (concatS (intercalate "\n" (Lem_list.map print_chunk chunks1))) in - return lines - )) - else if flag = "--debug-dump=info" then - Elf_file.read_elf32_file bs0 >>= (fun f1 -> - get_elf32_file_section_header_string_table f1 >>= (fun stbl -> - return (Dwarf.harness_string_of_elf32_debug_info_section - f1 - bs0 - (*string_of_gnu_ext_section_type - (fun x -> show x) - (fun x -> show x) - f1.elf32_file_header - f1.elf32_file_section_header_table - stbl*) - ))) - else - failwith "Unrecognised flag") - in - ret - else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string c)) Elf_header.elf_class_64 then - let ret = -(if flag = "--file-header" then - Elf_header.read_elf64_header bs0 >>= (fun (hdr, _) -> - return (Harness_interface.harness_string_of_elf64_file_header hdr)) - else if flag = "--program-headers" then - Elf_file.read_elf64_file bs0 >>= (fun f1 -> - get_elf64_file_section_header_string_table f1 >>= (fun stbl -> - return (Harness_interface.harness_string_of_elf64_program_headers - string_of_gnu_ext_segment_type - (fun x -> - Nat_big_num.to_string x) - f1.elf64_file_header - f1.elf64_file_program_header_table - f1.elf64_file_section_header_table - stbl - bs0))) - else if flag = "--section-headers" then - Elf_file.read_elf64_file bs0 >>= (fun f1 -> - get_elf64_file_section_header_string_table f1 >>= (fun stbl -> - return (Harness_interface.harness_string_of_elf64_section_headers - string_of_gnu_ext_section_type - (fun x -> Nat_big_num.to_string x) - (fun x -> Nat_big_num.to_string x) - f1.elf64_file_header - f1.elf64_file_section_header_table - stbl))) - else if flag = "--relocs" then - Elf_file.read_elf64_file bs0 >>= (fun f1 -> - let print_reloc = (obtain_abi_specific_string_of_reloc_type (Nat_big_num.of_string (Uint32.to_string f1.elf64_file_header.elf64_machine))) in - return (Harness_interface.harness_string_of_elf64_relocs - f1 - print_reloc - bs0)) - (*else if flag = "--symbols" then - Harness_interface.harness_string_of_elf64_syms - f1 - show - show - bs0*) - else if flag = "--dynamic" then - Elf_file.read_elf64_file bs0 >>= (fun f1 -> - let so = (is_elf64_shared_object_file f1.elf64_file_header) in - return (Harness_interface.harness_string_of_elf64_dynamic_section - f1 - bs0 - gnu_ext_os_additional_ranges - (fun x -> gnu_ext_tag_correspondence_of_tag x) - (fun x -> abi_power64_tag_correspondence_of_tag x) (* ABI! *) - (fun x -> string_of_dynamic_tag so x gnu_ext_os_additional_ranges string_of_gnu_ext_dynamic_tag string_of_abi_power64_dynamic_tag) - gnu_ext_elf64_value_of_elf64_dyn - abi_power64_elf64_value_of_elf64_dyn)) (* ABI! *) - else if flag = "--in-out" then - Elf_file.read_elf64_file bs0 >>= (fun f1 -> - (match Elf_file.bytes_of_elf64_file f1 with - | Fail f -> return f - | Success s -> - let chunks1 = (create_chunks s) in - let lines = (concatS (intercalate "\n" (Lem_list.map print_chunk chunks1))) in - return lines - )) - else if flag = "--debug-dump=info" then - Elf_file.read_elf64_file bs0 >>= (fun f1 -> - get_elf64_file_section_header_string_table f1 >>= (fun stbl -> - return (Dwarf.harness_string_of_elf64_debug_info_section - f1 - bs0 - (*string_of_gnu_ext_section_type - (fun x -> show x) - (fun x -> show x) - f1.elf64_file_header - f1.elf64_file_section_header_table - stbl*) - ))) - else - failwith "Unimplemented (for ELF64) or unrecognised flag") - in - ret - else - failwith "ELF ident transcription error" - )))) - in - (match res with - | Fail err -> prerr_endline ("[!]: " ^ err) - | Success e -> print_endline (string_of_string e) - )) - -(* -let _ = - match Sail_interface.populate_and_obtain_global_symbol_init_info "../test/mixed-binaries/tiny-istatic-with-malloc/tiny-tinystatic-with-malloc" with - | Fail err -> Missing_pervasives.errln ("[!]: " ^ err) - | Success (img, syms) -> Missing_pervasives.outln (Sail_interface.string_of_executable_process_image img) - end -*) |