Source file harness_interface.ml

(*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 (Uint32_wrapper.to_bigint hdr.elf32_type)))
  ; ("  Machine:" ^ ("                           " ^ string_of_elf_machine_architecture (Uint32_wrapper.to_bigint hdr.elf32_machine)))
  ; ("  Version:" ^ ("                           " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint hdr.elf32_version))))
  ; ("  Entry point address:" ^ ("               " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint hdr.elf32_entry))))
  ; ("  Start of program headers:" ^ ("          " ^ (Uint32_wrapper.to_string hdr.elf32_phoff ^ " (bytes into file)")))
  ; ("  Start of section headers:" ^ ("          " ^ (Uint32_wrapper.to_string hdr.elf32_shoff ^ " (bytes into file)")))
  ; ("  Flags:" ^ ("                             " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint hdr.elf32_flags))))
  ; ("  Size of this header:" ^ ("               " ^ (Uint32_wrapper.to_string hdr.elf32_ehsize ^ " (bytes)")))
  ; ("  Size of program headers:" ^ ("           " ^ (Uint32_wrapper.to_string hdr.elf32_phentsize ^ " (bytes)")))
  ; ("  Number of program headers:" ^ ("         " ^ Uint32_wrapper.to_string hdr.elf32_phnum))
  ; ("  Size of section headers:" ^ ("           " ^ (Uint32_wrapper.to_string hdr.elf32_shentsize ^ " (bytes)")))
  ; ("  Number of section headers:" ^ ("         " ^ Uint32_wrapper.to_string hdr.elf32_shnum))
  ; ("  Section header string table index:" ^ (" " ^ Uint32_wrapper.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 (Uint32_wrapper.to_bigint hdr.elf64_type)))
  ; ("  Machine:" ^ ("                           " ^ string_of_elf_machine_architecture (Uint32_wrapper.to_bigint hdr.elf64_machine)))
  ; ("  Version:" ^ ("                           " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint 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_wrapper.to_string hdr.elf64_phoff ^ " (bytes into file)")))
  ; ("  Start of section headers:" ^ ("          " ^ (Uint64_wrapper.to_string hdr.elf64_shoff ^ " (bytes into file)")))
  ; ("  Flags:" ^ ("                             " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint hdr.elf64_flags))))
  ; ("  Size of this header:" ^ ("               " ^ (Uint32_wrapper.to_string hdr.elf64_ehsize ^ " (bytes)")))
  ; ("  Size of program headers:" ^ ("           " ^ (Uint32_wrapper.to_string hdr.elf64_phentsize ^ " (bytes)")))
  ; ("  Number of program headers:" ^ ("         " ^ Uint32_wrapper.to_string hdr.elf64_phnum))
  ; ("  Size of section headers:" ^ ("           " ^ (Uint32_wrapper.to_string hdr.elf64_shentsize ^ " (bytes)")))
  ; ("  Number of section headers:" ^ ("         " ^ Uint32_wrapper.to_string hdr.elf64_shnum))
  ; ("  Section header string table index:" ^ (" " ^ Uint32_wrapper.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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint pent.elf32_p_offset))
  ; " "
  ; ("0x" ^ unsafe_hex_string_of_natural 8 (Uint32_wrapper.to_bigint pent.elf32_p_vaddr))
  ; " "
  ; ("0x" ^ unsafe_hex_string_of_natural 8 (Uint32_wrapper.to_bigint pent.elf32_p_paddr))
  ; " "
  ; ("0x" ^ unsafe_hex_string_of_natural 5 (Uint32_wrapper.to_bigint pent.elf32_p_filesz))
  ; " "
  ; ("0x" ^ unsafe_hex_string_of_natural 5 (Uint32_wrapper.to_bigint pent.elf32_p_memsz))
  ; " "
  ; string_of_elf_segment_permissions (Uint32_wrapper.to_bigint pent.elf32_p_flags)
  ; " "
  ; ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint pent.elf32_p_align))
  ] ^
    (if Nat_big_num.equal (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint64_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint hdr.elf32_type))
      ; ("Entry point " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Uint32_wrapper.to_bigint hdr.elf32_entry)))
      ; ("There are " ^ (Stdlib.string_of_int (List.length pht) ^ (" program headers, starting at offset " ^ Uint32_wrapper.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 (Uint32_wrapper.to_bigint hdr.elf64_type))
      ; ("Entry point " ^ ("0x" ^ unsafe_hex_string_of_natural 1 (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_entry)))
      ; ("There are " ^ (Stdlib.string_of_int (List.length pht) ^ (" program headers, starting at offset " ^ Uint64_wrapper.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 = (Stdlib.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 (Uint32_wrapper.to_bigint sec.elf32_sh_name) stbl with
        | Fail err   -> ("", ("ERR " ^ err))
        | Success nm ->
          if Nat_big_num.equal (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint sec.elf32_sh_addr)))
    in
    let str = (str ^ (gap ^ addr)) in
    let off = (unsafe_hex_string_of_natural 6 (Uint32_wrapper.to_bigint sec.elf32_sh_offset)) in
    let str = (str ^ (" " ^ off)) in
    let size2 = (unsafe_hex_string_of_natural 6 (Uint32_wrapper.to_bigint sec.elf32_sh_size)) in
    let str = (str ^ (" " ^ size2)) in
    let es  = (unsafe_hex_string_of_natural 2 (Uint32_wrapper.to_bigint sec.elf32_sh_entsize)) in
    let str = (str ^ (" " ^ es)) in
    let flg = (string_of_section_flags os proc (Uint32_wrapper.to_bigint sec.elf32_sh_flags)) in
    let str = (str ^ (" " ^ flg)) in
    let (gap, lnk) =
      (let l  = (Nat_big_num.to_string (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 = (Stdlib.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 (Uint32_wrapper.to_bigint sec.elf64_sh_name) stbl with
        | Fail err   -> ("", ("ERR " ^ err))
        | Success nm ->
          if Nat_big_num.equal (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint64_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 " ^ (Stdlib.string_of_int (List.length sht) ^ (" section headers, starting at offset 0x" ^ (unsafe_hex_string_of_natural 0 (Uint32_wrapper.to_bigint 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 " ^ (Stdlib.string_of_int (List.length sht) ^ (" section headers, starting at offset 0x" ^ (unsafe_hex_string_of_natural 0 (Uint64_wrapper.to_bigint hdr.elf64_shoff) ^ ":"))))
  ; ""
  ; "Section Headers:"
  ; harness_string_of_elf64_sht os proc usr sht stbl
  ] ^ harness_sht64_flag_legend (Uint32_wrapper.to_bigint 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  = (Uint32_wrapper.to_bigint rel.elf32_r_offset) in
  let inf  = (Uint32_wrapper.to_bigint rel.elf32_r_info) in
  let typ  = (Missing_pervasives.unsafe_string_take( (Nat_big_num.of_int 22)) (os( (Nat_big_num.of_int 0)))) in (* FIXME *)
  let typs =
    (let len = (Nat_big_num.of_int ( Nat_num.nat_monus 22 (String.length typ))) in
      concatS (replicate0 len " "))
  in
  let idx1  =( (Nat_big_num.of_int 0)) in (* FIXME *)
    (match Lem_list.list_index symtab (Nat_big_num.to_int idx1) with
      | None  -> "harness_string_of_elf32_reloc_entry: Nothing returned"
      | Some sym1 ->
        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 sym1 -> (Uint32_wrapper.to_bigint sym1.elf32_st_name,
                Uint32_wrapper.to_bigint sym1.elf32_st_value, get_elf32_symbol_type sym1,
                  Uint32_wrapper.to_bigint sym1.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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint sym1.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( (Nat_big_num.of_int 0)))) in (*FIXME *)
  let typs   =
    (let len = (Nat_big_num.of_int ( Nat_num.nat_monus 22 (String.length typ))) in
      concatS (replicate0 len " "))
  in
  let idx1  =( (Nat_big_num.of_int 0)) in (* FIXME *)
  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 sym1 -> (Uint32_wrapper.to_bigint sym1.elf64_st_name,
        Ml_bindings.nat_big_num_of_uint64 sym1.elf64_st_value, get_elf64_symbol_type sym1,
          Uint32_wrapper.to_bigint sym1.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 (Uint32_wrapper.to_bigint 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 =
  (bind (mapM (fun ent ->
      let off = (Uint32_wrapper.to_bigint  ent.elf32_sh_offset) in
      let siz = (Uint32_wrapper.to_bigint ent.elf32_sh_size) in
      let lnk = (Uint32_wrapper.to_bigint ent.elf32_sh_link) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rels -> bind (Elf_relocation.read_elf32_relocation_section' endian rels) (fun sect -> bind (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  = (Uint32_wrapper.to_bigint ent.elf32_sh_name) in
      let off = (unsafe_hex_string_of_natural 0 (Uint32_wrapper.to_bigint ent.elf32_sh_offset)) in
      let len = (Stdlib.string_of_int (List.length rels)) in bind (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 =
  (bind (mapM (fun ent ->
      let off = (Uint64_wrapper.to_bigint  ent.elf64_sh_offset) in
      let siz = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_size) in
      let lnk = (Uint32_wrapper.to_bigint ent.elf64_sh_link) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun rels -> bind (Elf_relocation.read_elf64_relocation_a_section' endian rels) (fun sect -> bind (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  = (Uint32_wrapper.to_bigint ent.elf64_sh_name) in
      let off = (unsafe_hex_string_of_natural 0 (Uint64_wrapper.to_bigint ent.elf64_sh_offset)) in
      let len = (Stdlib.string_of_int (List.length rels)) in bind (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_wrapper.of_bigint 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_wrapper.of_bigint 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 (Uint32_wrapper.to_bigint ent.elf32_st_value)) in
  let siz = (Nat_big_num.to_string (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint 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 sym1 = "" in
  let num =
    (let temp = (Stdlib.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
    ; sym1
    ])

(*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 = (bind (mapM (fun ent ->
      let off = (Uint32_wrapper.to_bigint  ent.elf32_sh_offset) in
      let siz = (Uint32_wrapper.to_bigint ent.elf32_sh_size) in
      let lnk = (Uint32_wrapper.to_bigint ent.elf32_sh_link) in
      let typ = (Uint32_wrapper.to_bigint ent.elf32_sh_type) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun syms -> bind (Elf_symbol_table.read_elf32_symbol_table endian syms) (fun sect -> bind (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  = (Uint32_wrapper.to_bigint ent.elf32_sh_name) in
      let len = (Stdlib.string_of_int (List.length syms)) in bind (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_wrapper.of_bigint sht_dynsym) ||
    (x.elf32_sh_type = Uint32_wrapper.of_bigint 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 (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint 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 = (Stdlib.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 =
  (bind (mapM (fun ent ->
      let off = (Uint64_wrapper.to_bigint  ent.elf64_sh_offset) in
      let siz = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_size) in
      let lnk = (Uint32_wrapper.to_bigint ent.elf64_sh_link) in
      let typ = (Uint32_wrapper.to_bigint ent.elf64_sh_type) in bind (Byte_sequence.offset_and_cut off siz bs0) (fun syms -> bind (Elf_symbol_table.read_elf64_symbol_table endian syms) (fun sect -> bind (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  = (Uint32_wrapper.to_bigint ent.elf64_sh_name) in
      let len = (Stdlib.string_of_int (List.length syms)) in bind (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_wrapper.of_bigint sht_dynsym) ||
    (x.elf64_sh_type = Uint32_wrapper.of_bigint 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
    ))



(* convenient symbol table extractor for read-dwarf *)
(*
  val read_dwarf_symbol_table_of_elf64_syms' : endianness -> (natural -> string) -> (natural -> string) -> elf64_file -> elf64_section_header_table -> elf64_section_header_table -> string_table -> byte_sequence -> list (string * natural)
let {ocaml} read_dwarf_symbol_table_of_elf64_syms' endian os proc f1 filtered_sht sht shdr bs0 =
  let rels =
    mapM (fun ent ->
      let off = natural_of_elf64_off  ent.elf64_sh_offset in
      let siz = natural_of_elf64_xword ent.elf64_sh_size in
      let lnk = natural_of_elf64_word ent.elf64_sh_link in
      let typ = natural_of_elf64_word 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  = natural_of_elf64_word ent.elf64_sh_name in
      let len = show (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" (List.mapi (fun n ->
        read_dwarf_symbol_table_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)
    end

val read_dwarf_symbol_table_of_elf64_syms : elf64_file -> (natural -> string) -> (natural -> string) -> byte_sequence -> string
let {ocaml} read_dwarf_symbol_table_of_elf64_syms f1 os proc bs0 =
  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 = elf64_word_of_natural sht_dynsym ||
    x.elf64_sh_type = elf64_word_of_natural 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" ^ *)
        read_dwarf_symbol_table_of_elf64_syms' endian os proc f1 sym_secs sht shdr bs0
    end
*)
(* end *)

  
(*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 (Uint32_wrapper.to_bigint a))
    (fun s -> Uint32_wrapper.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_wrapper.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 = (Uint32_wrapper.to_bigint dyn.elf32_p_offset) in
  let siz = (Uint32_wrapper.to_bigint dyn.elf32_p_filesz) in
  let shared_object = (is_elf32_shared_object_file f1.elf32_file_header) in
  let res = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (obtain_elf32_dynamic_section_contents f1 os_additional_ranges os proc bs0) (fun dyns -> bind (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 = (Stdlib.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_wrapper.of_bigint 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 = (Uint64_wrapper.to_bigint 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 = (bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (obtain_elf64_dynamic_section_contents f1 os_additional_ranges os proc bs0) (fun dyns -> bind (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 = (Stdlib.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_wrapper.of_bigint 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."
    ))