(*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 " )) 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 *)