(*Generated by Lem from adaptors/harness_interface.lem.*) open Lem_basic_classes open Lem_bool open Lem_function open Lem_maybe open Lem_num open Lem_string open Byte_sequence open Error open Hex_printing open Missing_pervasives open Show open Default_printing open Endianness open String_table open Elf_dynamic open Elf_file open Elf_header open Elf_program_header_table open Elf_relocation open Elf_section_header_table open Elf_symbol_table open Elf_types_native_uint open Gnu_ext_dynamic open Gnu_ext_section_header_table open Gnu_ext_section_to_segment_mapping open Gnu_ext_symbol_versioning (*val concatS' : list string -> string -> string*) let rec concatS' ss accum:string= ((match ss with | [] -> accum | s::ss -> concatS' ss (accum^s) )) (*val concatS : list string -> string*) let concatS ss:string= (concatS' ss "") (*val harness_string_of_elf32_file_header : elf32_header -> string*) let harness_string_of_elf32_file_header hdr:string= (unlines [ "ELF Header:" ; (" Magic:" ^ (" " ^ unsafe_hex_string_of_uc_list (hdr.elf32_ident))) ; (" Class:" ^ (" " ^ string_of_elf_file_class (get_elf32_file_class hdr))) ; (" Data:" ^ (" " ^ string_of_elf_data_encoding (get_elf32_data_encoding hdr))) ; (" Version:" ^ (" " ^ string_of_elf_version_number (get_elf32_version_number hdr))) ; (" OS/ABI:" ^ (" " ^ string_of_elf_osabi_version ((fun y->"Architecture defined")) (get_elf32_osabi hdr))) ; (" ABI Version:" ^ (" " ^ Nat_big_num.to_string (get_elf32_abi_version hdr))) ; (" Type:" ^ (" " ^ string_of_elf_file_type default_os_specific_print default_proc_specific_print (Nat_big_num.of_string (Uint32.to_string hdr.elf32_type)))) ; (" Machine:" ^ (" " ^ string_of_elf_machine_architecture (Nat_big_num.of_string (Uint32.to_string hdr.elf32_machine)))) ; (" Version:" ^ (" " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_version))))) ; (" Entry point address:" ^ (" " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_entry))))) ; (" Start of program headers:" ^ (" " ^ (Uint32.to_string hdr.elf32_phoff ^ " (bytes into file)"))) ; (" Start of section headers:" ^ (" " ^ (Uint32.to_string hdr.elf32_shoff ^ " (bytes into file)"))) ; (" Flags:" ^ (" " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_flags))))) ; (" Size of this header:" ^ (" " ^ (Uint32.to_string hdr.elf32_ehsize ^ " (bytes)"))) ; (" Size of program headers:" ^ (" " ^ (Uint32.to_string hdr.elf32_phentsize ^ " (bytes)"))) ; (" Number of program headers:" ^ (" " ^ Uint32.to_string hdr.elf32_phnum)) ; (" Size of section headers:" ^ (" " ^ (Uint32.to_string hdr.elf32_shentsize ^ " (bytes)"))) ; (" Number of section headers:" ^ (" " ^ Uint32.to_string hdr.elf32_shnum)) ; (" Section header string table index:" ^ (" " ^ Uint32.to_string hdr.elf32_shstrndx)) ]) (*val harness_string_of_elf64_file_header : elf64_header -> string*) let harness_string_of_elf64_file_header hdr:string= (unlines [ "ELF Header:" ; (" Magic:" ^ (" " ^ unsafe_hex_string_of_uc_list (hdr.elf64_ident))) ; (" Class:" ^ (" " ^ string_of_elf_file_class (get_elf64_file_class hdr))) ; (" Data:" ^ (" " ^ string_of_elf_data_encoding (get_elf64_data_encoding hdr))) ; (" Version:" ^ (" " ^ string_of_elf_version_number (get_elf64_version_number hdr))) ; (" OS/ABI:" ^ (" " ^ string_of_elf_osabi_version ((fun y->"Architecture defined")) (get_elf64_osabi hdr))) ; (" ABI Version:" ^ (" " ^ Nat_big_num.to_string (get_elf64_abi_version hdr))) ; (" Type:" ^ (" " ^ string_of_elf_file_type default_os_specific_print default_proc_specific_print (Nat_big_num.of_string (Uint32.to_string hdr.elf64_type)))) ; (" Machine:" ^ (" " ^ string_of_elf_machine_architecture (Nat_big_num.of_string (Uint32.to_string hdr.elf64_machine)))) ; (" Version:" ^ (" " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string hdr.elf64_version))))) ; (" Entry point address:" ^ (" " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_entry)))) ; (" Start of program headers:" ^ (" " ^ (Uint64.to_string hdr.elf64_phoff ^ " (bytes into file)"))) ; (" Start of section headers:" ^ (" " ^ (Uint64.to_string hdr.elf64_shoff ^ " (bytes into file)"))) ; (" Flags:" ^ (" " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string hdr.elf64_flags))))) ; (" Size of this header:" ^ (" " ^ (Uint32.to_string hdr.elf64_ehsize ^ " (bytes)"))) ; (" Size of program headers:" ^ (" " ^ (Uint32.to_string hdr.elf64_phentsize ^ " (bytes)"))) ; (" Number of program headers:" ^ (" " ^ Uint32.to_string hdr.elf64_phnum)) ; (" Size of section headers:" ^ (" " ^ (Uint32.to_string hdr.elf64_shentsize ^ " (bytes)"))) ; (" Number of section headers:" ^ (" " ^ Uint32.to_string hdr.elf64_shnum)) ; (" Section header string table index:" ^ (" " ^ Uint32.to_string hdr.elf64_shstrndx)) ]) (*val harness_string_of_elf32_program_header_table_entry : (natural -> string) -> (natural -> string) -> byte_sequence -> elf32_program_header_table_entry -> string*) let harness_string_of_elf32_program_header_table_entry os proc bs0 pent:string= (let typ = (string_of_segment_type os proc (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_type))) in let typ_s = (let len = (Nat_num.nat_monus( 15) (String.length typ)) in if len <= 0 then "" else concatS (replicate0 (Nat_big_num.of_int len) " ")) in concatS [ " " ; typ ; typ_s ; ("0x" ^ unsafe_hex_string_of_natural( 6) (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_offset))) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 8) (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_vaddr))) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 8) (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_paddr))) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 5) (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_filesz))) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 5) (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_memsz))) ; " " ; string_of_elf_segment_permissions (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_flags)) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_align))) ] ^ (if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_type)) elf_pt_interp then (match Elf_program_header_table.get_elf32_requested_interpreter pent bs0 with | Fail f -> "\n [Requesting program interpreter: " ^ (f ^ "]") | Success s -> "\n [Requesting program interpreter: " ^ (s ^ "]") ) else "")) (*val harness_string_of_elf64_program_header_table_entry : (natural -> string) -> (natural -> string) -> byte_sequence -> elf64_program_header_table_entry -> string*) let harness_string_of_elf64_program_header_table_entry os proc bs0 pent:string= (let typ = (string_of_segment_type os proc (Nat_big_num.of_string (Uint32.to_string pent.elf64_p_type))) in let typ_s = (let len = (Nat_num.nat_monus( 15) (String.length typ)) in if len <= 0 then "" else concatS (replicate0 (Nat_big_num.of_int len) " ")) in concatS [ " " ; typ ; typ_s ; ("0x" ^ unsafe_hex_string_of_natural( 6) (Nat_big_num.of_string (Uint64.to_string pent.elf64_p_offset))) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 16) (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_vaddr)) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 16) (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_paddr)) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 6) (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_filesz)) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 6) (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_memsz)) ; " " ; string_of_elf_segment_permissions (Nat_big_num.of_string (Uint32.to_string pent.elf64_p_flags)) ; " " ; ("0x" ^ unsafe_hex_string_of_natural( 1) (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_align)) ] ^ (if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string pent.elf64_p_type)) elf_pt_interp then (match Elf_program_header_table.get_elf64_requested_interpreter pent bs0 with | Fail f -> "\n [Requesting program interpreter: " ^ (f ^ "]") | Success s -> "\n [Requesting program interpreter: " ^ (s ^ "]") ) else "")) (*val harness_string_of_efl32_pht : (natural -> string) -> (natural -> string) -> elf32_program_header_table -> byte_sequence -> string*) let harness_string_of_elf32_pht os proc pht bs0:string= (" Type Offset VirtAddr PhysAddr FileSiz MemSiz Flg Align\n" ^ unlines (Lem_list.map (harness_string_of_elf32_program_header_table_entry os proc bs0) pht)) (*val harness_string_of_efl64_pht : (natural -> string) -> (natural -> string) -> elf64_program_header_table -> byte_sequence -> string*) let harness_string_of_elf64_pht os proc pht bs0:string= (" Type Offset VirtAddr PhysAddr FileSiz MemSiz Flg Align\n" ^ unlines (Lem_list.map (harness_string_of_elf64_program_header_table_entry os proc bs0) pht)) (*val harness_string_of_elf32_segment_section_mappings : elf32_header -> elf32_program_header_table -> elf32_section_header_table -> string_table -> string*) let harness_string_of_elf32_segment_section_mappings hdr pht sht stbl:string= (let map1 = (Lem_list.mapi (fun i -> fun pent -> let mapping = ((match get_elf32_section_to_segment_mapping hdr sht pent elf32_section_in_segment stbl with | Fail err -> [("ERR: " ^ err)] | Success mp -> intercalate " " mp )) in let str = (let temp = (concatS mapping) in if temp = "" then temp else temp ^ " ") in concatS [ (" " ^ Ml_bindings.hex_string_of_nat_pad2 i) ; " " ; str ] ) pht) in concatS (intercalate "\n" map1)) (*val harness_string_of_elf64_segment_section_mappings : elf64_header -> elf64_program_header_table -> elf64_section_header_table -> string_table -> string*) let harness_string_of_elf64_segment_section_mappings hdr pht sht stbl:string= (let map1 = (Lem_list.mapi (fun i -> fun pent -> let mapping = ((match get_elf64_section_to_segment_mapping hdr sht pent elf64_section_in_segment stbl with | Fail err -> [("ERR: " ^ err)] | Success mp -> intercalate " " mp )) in let str = (let temp = (concatS mapping) in if temp = "" then temp else temp ^ " ") in concatS [ (" " ^ Ml_bindings.hex_string_of_nat_pad2 i) ; " " ; str ] ) pht) in concatS (intercalate "\n" map1)) (*val harness_string_of_elf32_program_headers : (natural -> string) -> (natural -> string) -> elf32_header -> elf32_program_header_table -> elf32_section_header_table -> string_table -> byte_sequence -> string*) let harness_string_of_elf32_program_headers os proc hdr pht sht stbl bs0:string= (let pht_len = (List.length pht) in if pht_len = 0 then "\nThere are no program headers in this file." else unlines [ "" ; ("Elf file type is " ^ string_of_elf_file_type default_os_specific_print default_proc_specific_print (Nat_big_num.of_string (Uint32.to_string hdr.elf32_type))) ; ("Entry point " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_entry)))) ; ("There are " ^ (Pervasives.string_of_int (List.length pht) ^ (" program headers, starting at offset " ^ Uint32.to_string hdr.elf32_phoff))) ; "" ; "Program Headers:" ; harness_string_of_elf32_pht os proc pht bs0 ; "" ; " Section to Segment mapping:" ; " Segment Sections..." ; harness_string_of_elf32_segment_section_mappings hdr pht sht stbl ]) (*val harness_string_of_elf64_program_headers : (natural -> string) -> (natural -> string) -> elf64_header -> elf64_program_header_table -> elf64_section_header_table -> string_table -> byte_sequence -> string*) let harness_string_of_elf64_program_headers os proc hdr pht sht stbl bs0:string= (let pht_len = (List.length pht) in if pht_len = 0 then "\nThere are no program headers in this file." else unlines [ "" ; ("Elf file type is " ^ string_of_elf_file_type default_os_specific_print default_proc_specific_print (Nat_big_num.of_string (Uint32.to_string hdr.elf64_type))) ; ("Entry point " ^ ("0x" ^ unsafe_hex_string_of_natural( 1) (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_entry))) ; ("There are " ^ (Pervasives.string_of_int (List.length pht) ^ (" program headers, starting at offset " ^ Uint64.to_string hdr.elf64_phoff))) ; "" ; "Program Headers:" ; harness_string_of_elf64_pht os proc pht bs0 ; "" ; " Section to Segment mapping:" ; " Segment Sections..." ; harness_string_of_elf64_segment_section_mappings hdr pht sht stbl ]) (*val harness_sht32_flag_legend : string*) let harness_sht32_flag_legend:string= "\nKey to Flags: W (write), A (alloc), X (execute), M (merge), S (strings) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific)" (*val harness_sht64_flag_legend : natural -> string*) let harness_sht64_flag_legend mach:string= (if Nat_big_num.equal mach elf_ma_x86_64 || (Nat_big_num.equal mach elf_ma_l10m || Nat_big_num.equal mach elf_ma_k10m) then "\nKey to Flags: W (write), A (alloc), X (execute), M (merge), S (strings), l (large) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific)" else "\nKey to Flags: W (write), A (alloc), X (execute), M (merge), S (strings) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific)") (*val harness_string_of_elf32_sht : (natural -> string) -> (natural -> string) -> (natural -> string) -> elf32_section_header_table -> string_table -> string*) let harness_string_of_elf32_sht os proc usr sht stbl:string= (" [Nr] Name Type Addr Off Size ES Flg Lk Inf Al\n" ^ unlines (Lem_list.mapi (fun i -> fun sec -> let is = (let temp = (Pervasives.string_of_int i) in if String.length temp = 1 then " " ^ temp else temp) in let str = (" [" ^ (is ^ "]")) in let ((gap : string), name1) = ((match String_table.get_string_at (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_name)) stbl with | Fail err -> ("", ("ERR " ^ err)) | Success nm -> if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_type)) sht_null then let gap = (List.fold_right (^) (Missing_pervasives.replicate0(Nat_big_num.of_int 17) " ") " ") in (gap, "") else let glen = (Nat_big_num.of_int ( Nat_num.nat_monus( 17) (String.length nm))) in let gap = (List.fold_right (^) (Missing_pervasives.replicate0 glen " ") " ") in (gap, nm) )) in let str = (str ^ (" " ^ (name1 ^ gap))) in let typ = (string_of_section_type os proc usr (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_type))) in let str = (str ^ typ) in let (gap, addr) = (let mx = (Nat_big_num.of_int ( Nat_num.nat_monus( 15) (String.length typ))) in let gap = (List.fold_right (^) (Missing_pervasives.replicate0 mx " ") " ") in (gap, unsafe_hex_string_of_natural( 8) (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_addr)))) in let str = (str ^ (gap ^ addr)) in let off = (unsafe_hex_string_of_natural( 6) (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_offset))) in let str = (str ^ (" " ^ off)) in let size2 = (unsafe_hex_string_of_natural( 6) (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_size))) in let str = (str ^ (" " ^ size2)) in let es = (unsafe_hex_string_of_natural( 2) (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_entsize))) in let str = (str ^ (" " ^ es)) in let flg = (string_of_section_flags os proc (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_flags))) in let str = (str ^ (" " ^ flg)) in let (gap, lnk) = (let l = (Nat_big_num.to_string (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_link))) in let gp = (Nat_big_num.of_int ( Nat_num.nat_monus( 2) (String.length l))) in let gp = (List.fold_right (^) (replicate0 gp " ") " ") in (gp, l)) in let str = (str ^ (gap ^ lnk)) in let (gap, info) = (let i = (Nat_big_num.to_string (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_info))) in let gp = (Nat_big_num.of_int ( Nat_num.nat_monus( 3) (String.length i))) in let gp = (List.fold_right (^) (replicate0 gp " ") " ") in (gp, i)) in let str = (str ^ (gap ^ info)) in let (gap, align) = (let a = (Nat_big_num.to_string (Nat_big_num.of_string (Uint32.to_string sec.elf32_sh_addralign))) in let gp = (Nat_big_num.of_int ( Nat_num.nat_monus( 2) (String.length a))) in let gp = (List.fold_right (^) (replicate0 gp " ") " ") in (gp, a)) in let str = (str ^ (gap ^ align)) in str) sht)) (*val harness_string_of_elf64_sht : (natural -> string) -> (natural -> string) -> (natural -> string) -> elf64_section_header_table -> string_table -> string*) let harness_string_of_elf64_sht os proc usr sht stbl:string= (" [Nr] Name Type Address Off Size ES Flg Lk Inf Al\n" ^ unlines (Lem_list.mapi (fun i -> fun sec -> let is = (let temp = (Pervasives.string_of_int i) in if String.length temp = 1 then " " ^ temp else temp) in let str = (" [" ^ (is ^ "]")) in let ((gap : string), name1) = ((match String_table.get_string_at (Nat_big_num.of_string (Uint32.to_string sec.elf64_sh_name)) stbl with | Fail err -> ("", ("ERR " ^ err)) | Success nm -> if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string sec.elf64_sh_type)) sht_null then let gap = (List.fold_right (^) (Missing_pervasives.replicate0(Nat_big_num.of_int 17) " ") " ") in (gap, "") else let glen = (Nat_big_num.of_int ( Nat_num.nat_monus( 17) (String.length nm))) in let gap = (List.fold_right (^) (Missing_pervasives.replicate0 glen " ") " ") in (gap, nm) )) in let str = (str ^ (" " ^ (name1 ^ gap))) in let typ = (string_of_section_type os proc usr (Nat_big_num.of_string (Uint32.to_string sec.elf64_sh_type))) in let str = (str ^ typ) in let (gap, addr) = (let mx = (Nat_big_num.of_int ( Nat_num.nat_monus( 15) (String.length typ))) in let gap = (List.fold_right (^) (Missing_pervasives.replicate0 mx " ") " ") in (gap, unsafe_hex_string_of_natural( 16) (Ml_bindings.nat_big_num_of_uint64 sec.elf64_sh_addr))) in let str = (str ^ (gap ^ addr)) in let off = (unsafe_hex_string_of_natural( 6) (Nat_big_num.of_string (Uint64.to_string sec.elf64_sh_offset))) in let str = (str ^ (" " ^ off)) in let size2 = (unsafe_hex_string_of_natural( 6) (Ml_bindings.nat_big_num_of_uint64 sec.elf64_sh_size)) in let str = (str ^ (" " ^ size2)) in let es = (unsafe_hex_string_of_natural( 2) (Ml_bindings.nat_big_num_of_uint64 sec.elf64_sh_entsize)) in let str = (str ^ (" " ^ es)) in let flg = (string_of_section_flags os proc (Ml_bindings.nat_big_num_of_uint64 sec.elf64_sh_flags)) in let str = (str ^ (" " ^ flg)) in let (gap, lnk) = (let l = (Nat_big_num.to_string (Nat_big_num.of_string (Uint32.to_string sec.elf64_sh_link))) in let gp = (Nat_big_num.of_int ( Nat_num.nat_monus( 2) (String.length l))) in let gp = (List.fold_right (^) (replicate0 gp " ") " ") in (gp, l)) in let str = (str ^ (gap ^ lnk)) in let (gap, info) = (let i = (Nat_big_num.to_string (Nat_big_num.of_string (Uint32.to_string sec.elf64_sh_info))) in let gp = (Nat_big_num.of_int ( Nat_num.nat_monus( 3) (String.length i))) in let gp = (List.fold_right (^) (replicate0 gp " ") " ") in (gp, i)) in let str = (str ^ (gap ^ info)) in let (gap, align) = (let a = (Nat_big_num.to_string (Ml_bindings.nat_big_num_of_uint64 sec.elf64_sh_addralign)) in let gp = (Nat_big_num.of_int ( Nat_num.nat_monus( 2) (String.length a))) in let gp = (List.fold_right (^) (replicate0 gp " ") " ") in (gp, a)) in let str = (str ^ (gap ^ align)) in str) sht)) (*val harness_string_of_elf32_section_headers : (natural -> string) -> (natural -> string) -> (natural -> string) -> elf32_header -> elf32_section_header_table -> string_table -> string*) let harness_string_of_elf32_section_headers os proc usr hdr sht stbl:string= (unlines [ ("There are " ^ (Pervasives.string_of_int (List.length sht) ^ (" section headers, starting at offset 0x" ^ (unsafe_hex_string_of_natural( 0) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shoff)) ^ ":")))) ; "" ; "Section Headers:" ; harness_string_of_elf32_sht os proc usr sht stbl ] ^ harness_sht32_flag_legend) (*val harness_string_of_elf64_section_headers : (natural -> string) -> (natural -> string) -> (natural -> string) -> elf64_header -> elf64_section_header_table -> string_table -> string*) let harness_string_of_elf64_section_headers os proc usr hdr sht stbl:string= (unlines [ ("There are " ^ (Pervasives.string_of_int (List.length sht) ^ (" section headers, starting at offset 0x" ^ (unsafe_hex_string_of_natural( 0) (Nat_big_num.of_string (Uint64.to_string hdr.elf64_shoff)) ^ ":")))) ; "" ; "Section Headers:" ; harness_string_of_elf64_sht os proc usr sht stbl ] ^ harness_sht64_flag_legend (Nat_big_num.of_string (Uint32.to_string hdr.elf64_machine))) (*val harness_string_of_elf32_reloc_entry : (natural -> string) -> elf32_section_header_table -> elf32_symbol_table -> string_table -> string_table -> elf32_relocation -> string*) let harness_string_of_elf32_reloc_entry os sht symtab stbl sechdr_stbl rel:string= (let off = (Nat_big_num.of_string (Uint32.to_string rel.elf32_r_offset)) in let inf = (Nat_big_num.of_string (Uint32.to_string rel.elf32_r_info)) in let typ = (Missing_pervasives.unsafe_string_take(Nat_big_num.of_int 22) (os (extract_elf32_relocation_r_type rel.elf32_r_info))) in let typs = (let len = (Nat_big_num.of_int ( Nat_num.nat_monus( 22) (String.length typ))) in concatS (replicate0 len " ")) in let idx1 = (extract_elf32_relocation_r_sym rel.elf32_r_info) in (match Lem_list.list_index symtab (Nat_big_num.to_int idx1) with | None -> "harness_string_of_elf32_reloc_entry: Nothing returned" | Some sym -> let (nm, value, symtyp, secthdr) = ((match Lem_list.list_index symtab (Nat_big_num.to_int idx1) with | None -> (stn_undef,Nat_big_num.of_int 0,Nat_big_num.of_int 0,Nat_big_num.of_int 0) | Some sym -> (Nat_big_num.of_string (Uint32.to_string sym.elf32_st_name), Nat_big_num.of_string (Uint32.to_string sym.elf32_st_value), get_elf32_symbol_type sym, Nat_big_num.of_string (Uint32.to_string sym.elf32_st_shndx)) )) in if Nat_big_num.equal symtyp stt_section then let vlu = (" " ^ unsafe_hex_string_of_natural( 8) value) in let nm = ((match Lem_list.list_index sht (Nat_big_num.to_int secthdr) with | None -> "XXX" | Some shdr -> (match String_table.get_string_at (Nat_big_num.of_string (Uint32.to_string shdr.elf32_sh_name)) sechdr_stbl with | Fail f -> f | Success n -> n ) )) in concatS [ unsafe_hex_string_of_natural( 8) off ; " " ; unsafe_hex_string_of_natural( 8) inf ; " " ; typ ; typs ; vlu ; " " ; nm ] else if Nat_big_num.equal nm stn_undef then concatS [ unsafe_hex_string_of_natural( 8) off ; " " ; unsafe_hex_string_of_natural( 8) inf ; " " ; typ ; typs ] else let vlu = (" " ^ unsafe_hex_string_of_natural( 8) (Nat_big_num.of_string (Uint32.to_string sym.elf32_st_value))) in let nm = ((match String_table.get_string_at nm stbl with | Fail f -> f | Success n -> n )) in concatS [ unsafe_hex_string_of_natural( 8) off ; " " ; unsafe_hex_string_of_natural( 8) inf ; " " ; typ ; typs ; vlu ; " " ; nm ] )) (*val harness_string_of_elf64_reloc_a_entry : (natural -> string) -> elf64_symbol_table -> elf64_section_header_table -> string_table -> string_table -> elf64_relocation_a -> string*) let harness_string_of_elf64_reloc_a_entry os symtab sht stbl sechdr_stbl rel:string= (let off = (Ml_bindings.nat_big_num_of_uint64 rel.elf64_ra_offset) in let inf = (Ml_bindings.nat_big_num_of_uint64 rel.elf64_ra_info) in let add = (Nat_big_num.of_int64 rel.elf64_ra_addend) in let typ = (Missing_pervasives.unsafe_string_take(Nat_big_num.of_int 22) (os (extract_elf64_relocation_r_type rel.elf64_ra_info))) in let typs = (let len = (Nat_big_num.of_int ( Nat_num.nat_monus( 22) (String.length typ))) in concatS (replicate0 len " ")) in let idx1 = (extract_elf64_relocation_r_sym rel.elf64_ra_info) in let (nm, value, symtyp, secthdr) = ((match Lem_list.list_index symtab (Nat_big_num.to_int idx1) with | None -> (stn_undef,Nat_big_num.of_int 0,Nat_big_num.of_int 0,Nat_big_num.of_int 0) | Some sym -> (Nat_big_num.of_string (Uint32.to_string sym.elf64_st_name), Ml_bindings.nat_big_num_of_uint64 sym.elf64_st_value, get_elf64_symbol_type sym, Nat_big_num.of_string (Uint32.to_string sym.elf64_st_shndx)) )) in if Nat_big_num.equal symtyp stt_section then let vlu = (" " ^ unsafe_hex_string_of_natural( 16) value) in let nm = ((match Lem_list.list_index sht (Nat_big_num.to_int secthdr) with | None -> "XXX" | Some shdr -> (match String_table.get_string_at (Nat_big_num.of_string (Uint32.to_string shdr.elf64_sh_name)) sechdr_stbl with | Fail f -> f | Success n -> n ) )) in concatS [ unsafe_hex_string_of_natural( 16) off ; " " ; unsafe_hex_string_of_natural( 16) inf ; " " ; typ ; typs ; vlu ; " " ; nm ; " + " ; Ml_bindings.hex_string_of_big_int_no_padding add ] else if Nat_big_num.equal nm stn_undef then concatS [ unsafe_hex_string_of_natural( 16) off ; " " ; unsafe_hex_string_of_natural( 16) inf ; " " ; typ ; typs ; " " ; Ml_bindings.hex_string_of_big_int_no_padding add ] else let vlu = (" " ^ unsafe_hex_string_of_natural( 16) value) in let nm = ((match String_table.get_string_at nm stbl with | Fail f -> f | Success n -> n )) in concatS [ unsafe_hex_string_of_natural( 16) off ; " " ; unsafe_hex_string_of_natural( 16) inf ; " " ; typ ; typs ; vlu ; " " ; nm ; " + " ; Ml_bindings.hex_string_of_big_int_no_padding add ]) (*val harness_string_of_elf32_relocs' : endianness -> (natural -> string) -> elf32_file -> elf32_section_header_table -> elf32_section_header_table -> string_table -> string_table -> byte_sequence -> string*) let harness_string_of_elf32_relocs' endian os f1 sht_relocs sht shdr stbl bs0:string= (let rels = (mapM (fun ent -> let off = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_offset)) in let siz = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_size)) in let lnk = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_link)) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun rels -> Elf_relocation.read_elf32_relocation_section' endian rels >>= (fun sect -> Elf_file.get_elf32_symbol_table_by_index f1 lnk >>= (fun symtab -> return (sect, ent, symtab)))) ) sht_relocs >>= mapM (fun (rels, ent, symtab) -> let nm = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_name)) in let off = (unsafe_hex_string_of_natural( 0) (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_offset))) in let len = (Pervasives.string_of_int (List.length rels)) in String_table.get_string_at nm shdr >>= (fun nm -> let hdr = ("Relocation section '" ^ (nm ^ ("' at offset 0x" ^ (off ^ (" contains " ^ (len ^ " entries:\n")))))) in let ttl = " Offset Info Type Sym. Value Symbol's Name\n" in let body = (concatS (intercalate "\n" (Lem_list.map (harness_string_of_elf32_reloc_entry os sht symtab stbl shdr) rels))) in return (hdr ^ (ttl ^ body))))) in (match rels with | Fail err -> err | Success s -> concatS (intercalate "\n\n" s) )) (*val harness_string_of_elf64_relocs' : endianness -> (natural -> string) -> elf64_file -> elf64_section_header_table -> elf64_section_header_table -> string_table -> string_table -> byte_sequence -> string*) let harness_string_of_elf64_relocs' endian os f1 reloc_sht sht shdr stbl bs0:string= (let rels = (mapM (fun ent -> let off = (Nat_big_num.of_string (Uint64.to_string ent.elf64_sh_offset)) in let siz = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_size) in let lnk = (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_link)) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun rels -> Elf_relocation.read_elf64_relocation_a_section' endian rels >>= (fun sect -> Elf_file.get_elf64_symbol_table_by_index f1 lnk >>= (fun symtab -> return (sect, ent, symtab)))) ) reloc_sht >>= mapM (fun (rels, ent, symtab) -> let nm = (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_name)) in let off = (unsafe_hex_string_of_natural( 0) (Nat_big_num.of_string (Uint64.to_string ent.elf64_sh_offset))) in let len = (Pervasives.string_of_int (List.length rels)) in String_table.get_string_at nm shdr >>= (fun nm -> let hdr = ("Relocation section '" ^ (nm ^ ("' at offset 0x" ^ (off ^ (" contains " ^ (len ^ " entries:\n")))))) in let ttl = " Offset Info Type Symbol's Value Symbol's Name + Addend\n" in let body = (concatS (intercalate "\n" (Lem_list.map (harness_string_of_elf64_reloc_a_entry os symtab sht stbl shdr) rels))) in return (hdr ^ (ttl ^ body))))) in (match rels with | Fail err -> err | Success s -> concatS (intercalate "\n\n" s) )) (*val harness_string_of_elf32_relocs : elf32_file -> (natural -> string) -> byte_sequence -> string*) let harness_string_of_elf32_relocs f1 os bs0:string= (let hdr = (f1.elf32_file_header) in let sht = (f1.elf32_file_section_header_table) in let endian = (get_elf32_header_endianness hdr) in let rel_secs = (List.filter (fun x -> x.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_rel)) sht) in if List.length rel_secs = 0 then "\nThere are no relocations in this file." else (match get_elf32_file_symbol_string_table f1 with | Fail err -> err | Success stbl -> (match get_elf32_file_section_header_string_table f1 with | Fail err -> err | Success shdr -> "\n" ^ harness_string_of_elf32_relocs' endian os f1 rel_secs sht shdr stbl bs0 ) )) (*val harness_string_of_elf64_relocs : elf64_file -> (natural -> string) -> byte_sequence -> string*) let harness_string_of_elf64_relocs f1 os bs0:string= (let hdr = (f1.elf64_file_header) in let sht = (f1.elf64_file_section_header_table) in let endian = (get_elf64_header_endianness hdr) in let rel_secs = (List.filter (fun x -> x.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_rela)) sht) in if List.length rel_secs = 0 then "\nThere are no relocations in this file." else (match get_elf64_file_symbol_string_table f1 with | Fail err -> err | Success stbl -> (match get_elf64_file_section_header_string_table f1 with | Fail err -> err | Success shdr -> "\n" ^ harness_string_of_elf64_relocs' endian os f1 rel_secs sht shdr stbl bs0 ) )) (*val harness_string_of_elf32_symbol_table_entry : nat -> (natural -> string) -> (natural -> string) -> byte_sequence -> string_table -> elf32_symbol_table_entry -> string*) let harness_string_of_elf32_symbol_table_entry num os proc bs0 stbl ent:string= (let vlu = (unsafe_hex_string_of_natural( 8) (Nat_big_num.of_string (Uint32.to_string ent.elf32_st_value))) in let siz = (Nat_big_num.to_string (Nat_big_num.of_string (Uint32.to_string ent.elf32_st_size))) in let siz_pad = (let pad = (Nat_num.nat_monus( 5) (String.length siz)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let typ = (string_of_symbol_type (get_elf32_symbol_type ent) os proc) in let bnd = (string_of_symbol_binding (get_elf32_symbol_binding ent) os proc) in let bnd_pad = (let pad = (Nat_num.nat_monus( 6) (String.length typ)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let vis = (string_of_symbol_visibility (Nat_big_num.of_string (Uint32.to_string ent.elf32_st_other))) in let vis_pad = (let pad = (Nat_num.nat_monus( 6) (String.length bnd)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let ndx = (let tmp = (Nat_big_num.of_string (Uint32.to_string ent.elf32_st_shndx)) in if Nat_big_num.equal tmp shn_undef then "UND" else if Nat_big_num.equal tmp shn_abs then "ABS" else Nat_big_num.to_string tmp) in let ndx_pad = (let pad = (Nat_num.nat_monus( 3) (String.length ndx)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let nm = (let idx1 = (Nat_big_num.of_string (Uint32.to_string ent.elf32_st_name)) in if Nat_big_num.equal idx1(Nat_big_num.of_int 0) then "" else (match String_table.get_string_at idx1 stbl with | Fail err -> err | Success s -> s )) in let sym = "" in let num = (let temp = (Pervasives.string_of_int num) in let pad = (Nat_num.nat_monus( 3) (String.length temp)) in if pad = 0 then temp else let spcs = (concatS (replicate0 (Nat_big_num.of_int pad) " ")) in spcs ^ temp) in concatS [ " " ; (num ^ ":") ; " " ; vlu ; " " ; siz_pad; siz ; " " ; typ ; " " ; bnd_pad; bnd ; " " ; vis_pad; vis ; " " ; ndx_pad; ndx ; " " ; nm ; sym ]) (*val harness_string_of_elf32_syms' : endianness -> (natural -> string) -> (natural -> string) -> elf32_file -> elf32_section_header_table -> elf32_section_header_table -> string_table -> byte_sequence -> string*) let harness_string_of_elf32_syms' endian os proc f1 filtered_sht sht shdr bs0:string= (let rels = (mapM (fun ent -> let off = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_offset)) in let siz = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_size)) in let lnk = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_link)) in let typ = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun syms -> Elf_symbol_table.read_elf32_symbol_table endian syms >>= (fun sect -> Elf_file.get_elf32_string_table_by_index f1 lnk >>= (fun strtab -> return (sect, ent, strtab, typ)))) ) filtered_sht >>= (fun sects -> mapM (fun (syms, ent, strtab, typ) -> let nm = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_name)) in let len = (Pervasives.string_of_int (List.length syms)) in String_table.get_string_at nm shdr >>= (fun nm -> let hdr = ("Symbol table '" ^ (nm ^ ("' contains " ^ (len ^ " entries:\n")))) in let ttl = " Num: Value Size Type Bind Vis Ndx Name\n" in let body = (concatS (intercalate "\n" (Lem_list.mapi (fun n -> harness_string_of_elf32_symbol_table_entry n os proc bs0 strtab) syms))) in return (hdr ^ (ttl ^ body)))) sects)) in (match rels with | Fail err -> err | Success s -> concatS (intercalate "\n\n" s) )) (*val harness_string_of_elf32_syms : elf32_file -> (natural -> string) -> (natural -> string) -> byte_sequence -> string*) let harness_string_of_elf32_syms f1 os proc bs0:string= (let hdr = (f1.elf32_file_header) in let sht = (f1.elf32_file_section_header_table) in let endian = (get_elf32_header_endianness hdr) in let sym_secs = (List.filter (fun x -> (x.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_dynsym)) || (x.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_symtab))) sht) in if List.length sym_secs = 0 then "\nThere are no symbols in this file." else (match get_elf32_file_section_header_string_table f1 with | Fail err -> err | Success shdr -> "\n" ^ harness_string_of_elf32_syms' endian os proc f1 sym_secs sht shdr bs0 )) (*val harness_string_of_elf64_symbol_table_entry : nat -> (natural -> string) -> (natural -> string) -> string_table -> elf64_symbol_table_entry -> string*) let harness_string_of_elf64_symbol_table_entry num os proc stbl ent:string= (let vlu = (unsafe_hex_string_of_natural( 16) (Ml_bindings.nat_big_num_of_uint64 ent.elf64_st_value)) in let siz = (Nat_big_num.to_string (Ml_bindings.nat_big_num_of_uint64 ent.elf64_st_size)) in let siz_pad = (let pad = (Nat_num.nat_monus( 5) (String.length siz)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let typ = (string_of_symbol_type (get_elf64_symbol_type ent) os proc) in let bnd = (string_of_symbol_binding (get_elf64_symbol_binding ent) os proc) in let bnd_pad = (let pad = (Nat_num.nat_monus( 8) (String.length typ)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let vis = (string_of_symbol_visibility (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_other))) in let vis_pad = (let pad = (Nat_num.nat_monus( 6) (String.length bnd)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let ndx = (let tmp = (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_shndx)) in if Nat_big_num.equal tmp shn_undef then "UND" else if Nat_big_num.equal tmp shn_abs then "ABS" else Nat_big_num.to_string tmp) in let ndx_pad = (let pad = (Nat_num.nat_monus( 3) (String.length ndx)) in if pad = 0 then "" else concatS (replicate0 (Nat_big_num.of_int pad) " ")) in let nm = (let idx1 = (Nat_big_num.of_string (Uint32.to_string ent.elf64_st_name)) in if Nat_big_num.equal idx1(Nat_big_num.of_int 0) then "" else (match String_table.get_string_at idx1 stbl with | Fail err -> err | Success s -> s )) in let num = (let temp = (Pervasives.string_of_int num) in let pad = (Nat_num.nat_monus( 3) (String.length temp)) in if pad = 0 then temp else let spcs = (concatS (replicate0 (Nat_big_num.of_int pad) " ")) in spcs ^ temp) in concatS [ " " ; (num ^ ":") ; " " ; vlu ; " " ; siz_pad; siz ; " " ; typ ; bnd_pad; bnd ; " " ; vis_pad; vis ; " " ; ndx_pad; ndx ; " " ; nm ]) (*val harness_string_of_elf64_syms' : endianness -> (natural -> string) -> (natural -> string) -> elf64_file -> elf64_section_header_table -> elf64_section_header_table -> string_table -> byte_sequence -> string*) let harness_string_of_elf64_syms' endian os proc f1 filtered_sht sht shdr bs0:string= (let rels = (mapM (fun ent -> let off = (Nat_big_num.of_string (Uint64.to_string ent.elf64_sh_offset)) in let siz = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_size) in let lnk = (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_link)) in let typ = (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) in Byte_sequence.offset_and_cut off siz bs0 >>= (fun syms -> Elf_symbol_table.read_elf64_symbol_table endian syms >>= (fun sect -> Elf_file.get_elf64_string_table_by_index f1 lnk >>= (fun strtab -> return (sect, ent, strtab, typ)))) ) filtered_sht >>= mapM (fun (syms, ent, strtab, typ) -> let nm = (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_name)) in let len = (Pervasives.string_of_int (List.length syms)) in String_table.get_string_at nm shdr >>= (fun nm -> let hdr = ("Symbol table '" ^ (nm ^ ("' contains " ^ (len ^ " entries:\n")))) in let ttl = " Num: Value Size Type Bind Vis Ndx Name\n" in let body = (concatS (intercalate "\n" (Lem_list.mapi (fun n -> harness_string_of_elf64_symbol_table_entry n os proc strtab) syms))) in return (hdr ^ (ttl ^ body))))) in (match rels with | Fail err -> err | Success s -> concatS (intercalate "\n\n" s) )) (*val harness_string_of_elf64_syms : elf64_file -> (natural -> string) -> (natural -> string) -> byte_sequence -> string*) let harness_string_of_elf64_syms f1 os proc bs0:string= (let hdr = (f1.elf64_file_header) in let sht = (f1.elf64_file_section_header_table) in let endian = (get_elf64_header_endianness hdr) in let sym_secs = (List.filter (fun x -> (x.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_dynsym)) || (x.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_symtab))) sht) in if List.length sym_secs = 0 then "\nThere are no symbols in this file." else (match get_elf64_file_section_header_string_table f1 with | Fail err -> err | Success shdr -> "\n" ^ harness_string_of_elf64_syms' endian os proc f1 sym_secs sht shdr bs0 )) (*val string_of_unix_time : natural -> string*) (*val string_of_dyn_value : forall 'addr 'size. dyn_value 'addr 'size -> ('addr -> string) -> ('size -> string) -> string*) let string_of_dyn_value dyn addr size2:string= ((match dyn with | Address a -> addr a | Size s -> size2 s | FName f -> f | Path p -> p | SOName f -> "Library soname: [" ^ (f ^ "]") | RPath p -> "Library rpath: [" ^ (p ^ "]") | RunPath p -> "Library runpath: [" ^ (p ^ "]") | Flags f -> string_of_dt_flag f | Flags1 f -> "Flags: " ^ gnu_string_of_dt_flag_1 f | Ignored -> "" | Checksum s -> "0x" ^ unsafe_hex_string_of_natural( 0) s | Library l -> "Shared library: [" ^ (l ^ "]") | Numeric n -> Nat_big_num.to_string n | RelType r -> string_of_rel_type r | Timestamp t -> Ml_bindings.string_of_unix_time t | Null -> "0x0" )) (*val string_of_elf32_dyn_value : elf32_dyn_value -> string*) let string_of_elf32_dyn_value dyn:string= (string_of_dyn_value dyn (fun a -> "0x" ^ unsafe_hex_string_of_natural( 0) (Nat_big_num.of_string (Uint32.to_string a))) (fun s -> Uint32.to_string s ^ " (bytes)")) (*val string_of_elf64_dyn_value : elf64_dyn_value -> string*) let string_of_elf64_dyn_value dyn:string= (string_of_dyn_value dyn (fun a -> "0x" ^ unsafe_hex_string_of_natural( 0) (Ml_bindings.nat_big_num_of_uint64 a)) (fun s -> Uint64.to_string s ^ " (bytes)")) (*val harness_string_of_elf32_dyn_entry : bool -> elf32_dyn -> (natural -> bool) -> (natural -> string) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> string_table -> string*) let harness_string_of_elf32_dyn_entry shared_object dyn os_additional_tags typ os_dyn proc_dyn stbl:string= (let tag = (unsafe_hex_string_of_natural( 8) (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag))) in let typ = ("(" ^ (typ (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) ^ ")")) in let vlu = ((match get_value_of_elf32_dyn shared_object dyn os_additional_tags os_dyn proc_dyn stbl with | Fail f -> f | Success v -> string_of_elf32_dyn_value v )) in let vlu_pad = (let pad = (Nat_num.nat_monus( 29) (String.length typ)) in if pad = 0 then "" else let reps = (replicate0 (Nat_big_num.of_int pad) " ") in concatS reps) in concatS [ " " ; ("0x" ^ tag) ; " " ; typ ; vlu_pad; vlu ]) (*val harness_string_of_elf32_dynamic_section' : elf32_file -> elf32_program_header_table_entry -> byte_sequence -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> (natural -> string) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> string*) let harness_string_of_elf32_dynamic_section' f1 dyn bs0 os_additional_ranges os proc os_print os_dyn proc_dyn:string= (let endian = (get_elf32_header_endianness f1.elf32_file_header) in let sht = (f1.elf32_file_section_header_table) in let off = (Nat_big_num.of_string (Uint32.to_string dyn.elf32_p_offset)) in let siz = (Nat_big_num.of_string (Uint32.to_string dyn.elf32_p_filesz)) in let shared_object = (is_elf32_shared_object_file f1.elf32_file_header) in let res = (Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> obtain_elf32_dynamic_section_contents f1 os_additional_ranges os proc bs0 >>= (fun dyns -> get_string_table_of_elf32_dyn_section endian dyns sht bs0 >>= (fun stbl -> return (Lem_list.map (fun x -> harness_string_of_elf32_dyn_entry shared_object x os_additional_ranges os_print os_dyn proc_dyn stbl) dyns))))) in (match res with | Fail f -> f | Success s -> let off = (unsafe_hex_string_of_natural( 0) off) in let entries = (Pervasives.string_of_int (List.length s)) in concatS [ "\n" ; ("Dynamic section at offset 0x" ^ (off ^ (" contains " ^ (entries ^ " entries:\n")))) ; " Tag Type Name/Value\n" ; concatS (intercalate "\n" s) ] )) (*val harness_string_of_elf32_dynamic_section : elf32_file -> byte_sequence -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> (natural -> string) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> (elf32_dyn -> string_table -> error elf32_dyn_value) -> string*) let harness_string_of_elf32_dynamic_section f1 bs0 os_additional_ranges os proc os_print os_dyn proc_dyn:string= (let pht = (f1.elf32_file_program_header_table) in let dyn = (List.filter (fun x -> x.elf32_p_type = Uint32.of_string (Nat_big_num.to_string elf_pt_dynamic) ) pht) in let print_msg = (is_elf32_shared_object_file f1.elf32_file_header || is_elf32_executable_file f1.elf32_file_header) in (match dyn with | [] -> if print_msg then "\nThere is no dynamic section in this file." else "" | [x] -> harness_string_of_elf32_dynamic_section' f1 x bs0 os_additional_ranges os proc os_print os_dyn proc_dyn | _ -> "Multiple dynamic sections detected." )) (*val harness_string_of_elf64_dyn_entry : bool -> elf64_dyn -> (natural -> bool) -> (natural -> string) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> string_table -> string*) let harness_string_of_elf64_dyn_entry shared_object dyn os_additional_ranges typ os_dyn proc_dyn stbl:string= (let tag = (unsafe_hex_string_of_natural( 16) (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag))) in let typ = ("(" ^ (typ (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) ^ ")")) in let vlu = ((match get_value_of_elf64_dyn shared_object dyn os_additional_ranges os_dyn proc_dyn stbl with | Fail f -> f | Success v -> string_of_elf64_dyn_value v )) in let vlu_pad = (let pad = (Nat_num.nat_monus( 21) (String.length typ)) in if pad = 0 then "" else let reps = (replicate0 (Nat_big_num.of_int pad) " ") in concatS reps) in concatS [ " " ; ("0x" ^ tag) ; " " ; typ ; vlu_pad; vlu ]) (*val harness_string_of_elf64_dynamic_section' : elf64_file -> elf64_program_header_table_entry -> byte_sequence -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> (natural -> string) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> string*) let harness_string_of_elf64_dynamic_section' f1 dyn bs0 os_additional_ranges os proc os_print os_dyn proc_dyn:string= (let endian = (get_elf64_header_endianness f1.elf64_file_header) in let sht = (f1.elf64_file_section_header_table) in let off = (Nat_big_num.of_string (Uint64.to_string dyn.elf64_p_offset)) in let siz = (Ml_bindings.nat_big_num_of_uint64 dyn.elf64_p_filesz) in let shared_object = (is_elf64_shared_object_file f1.elf64_file_header) in let res = (Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel -> obtain_elf64_dynamic_section_contents f1 os_additional_ranges os proc bs0 >>= (fun dyns -> get_string_table_of_elf64_dyn_section endian dyns sht bs0 >>= (fun stbl -> return (Lem_list.map (fun x -> harness_string_of_elf64_dyn_entry shared_object x os_additional_ranges os_print os_dyn proc_dyn stbl) dyns))))) in (match res with | Fail f -> f | Success s -> let off = (unsafe_hex_string_of_natural( 0) off) in let entries = (Pervasives.string_of_int (List.length s)) in concatS [ "\n" ; ("Dynamic section at offset 0x" ^ (off ^ (" contains " ^ (entries ^ " entries:\n")))) ; " Tag Type Name/Value\n" ; concatS (intercalate "\n" s) ] )) (*val harness_string_of_elf64_dynamic_section : elf64_file -> byte_sequence -> (natural -> bool) -> (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) -> (natural -> string) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> (elf64_dyn -> string_table -> error elf64_dyn_value) -> string*) let harness_string_of_elf64_dynamic_section f1 bs0 os_additional_ranges os proc os_print os_dyn proc_dyn:string= (let pht = (f1.elf64_file_program_header_table) in let print_msg = (is_elf64_shared_object_file f1.elf64_file_header || is_elf64_executable_file f1.elf64_file_header) in let dyn = (List.filter (fun x -> x.elf64_p_type = Uint32.of_string (Nat_big_num.to_string elf_pt_dynamic) ) pht) in (match dyn with | [] -> if print_msg then "\nThere is no dynamic section in this file." else "" | [x] -> harness_string_of_elf64_dynamic_section' f1 x bs0 os_additional_ranges os proc os_print os_dyn proc_dyn | _ -> "Multiple dynamic sections detected." ))