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