summaryrefslogtreecommitdiff
path: root/lib/ocaml_rts/linksem/adaptors/harness_interface.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ocaml_rts/linksem/adaptors/harness_interface.ml')
-rw-r--r--lib/ocaml_rts/linksem/adaptors/harness_interface.ml1154
1 files changed, 1154 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/adaptors/harness_interface.ml b/lib/ocaml_rts/linksem/adaptors/harness_interface.ml
new file mode 100644
index 00000000..8ce4f6bd
--- /dev/null
+++ b/lib/ocaml_rts/linksem/adaptors/harness_interface.ml
@@ -0,0 +1,1154 @@
+(*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."
+ ))
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:22:04 +0000