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, 374 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/main_elf.ml b/lib/ocaml_rts/linksem/main_elf.ml new file mode 100644 index 00000000..c5a31ebe --- /dev/null +++ b/lib/ocaml_rts/linksem/main_elf.ml @@ -0,0 +1,374 @@ +(*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 +*) |