Source file elf_file.ml

(*Generated by Lem from elf_file.lem.*)
(** Module [elf_file] packages all components of an ELF file up into a single
  * record, provides I/O routines for this record, as well as other utility
  * functions that operate on an entire ELF file.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_maybe
open Lem_string

open Elf_header
open Elf_interpreted_section
open Elf_interpreted_segment
open Elf_types_native_uint
open Elf_section_header_table
open Elf_symbol_table
open Elf_program_header_table

open String_table

open Byte_sequence
open Error
open Missing_pervasives
open Show

(** [elf32_file] record captures the internal structure of an ELF32 file.
  * Invariant: length of the program header and section header tables should match
  * the length of their interpreted counterparts, and the nth element of the
  * (program/section) header table must correspond to the nth element of the
  * interpreted (segments/sections), respectively.
  *)
type elf32_file =
  { elf32_file_header               : elf32_header                   (** The file header. *)
   ; elf32_file_program_header_table : elf32_program_header_table     (** The program header table. *)
   ; elf32_file_section_header_table : elf32_section_header_table     (** The section header table. *)
   ; elf32_file_interpreted_segments : elf32_interpreted_segments     (** A more usable interpretation of the file's segments. *)
   ; elf32_file_interpreted_sections : elf32_interpreted_sections     (** A more usable interpretation of the file's sections. *)
   ; elf32_file_bits_and_bobs        : (Nat_big_num.num * byte_sequence0) list (** The uninterpreted "rubbish" that may appear in gaps in the binary file. *)
   }

(** [bytes_of_elf32_file f1] blits ELF file [f1] to a byte sequence, ready for
  * writing to a binary file.  Fails if the invariant on [elf32_file] mentioned
  * above is not respected.
  *)
(*val bytes_of_elf32_file : elf32_file -> error byte_sequence*)
let bytes_of_elf32_file ef:(Byte_sequence_wrapper.byte_sequence)error=
   (let endian      = (get_elf32_header_endianness ef.elf32_file_header) in
  let hdr_bytes   = (bytes_of_elf32_header ef.elf32_file_header) in
  let hdr_layout  = ( (Nat_big_num.of_int 0), hdr_bytes) in
  let pht_bytes   = (bytes_of_elf32_program_header_table endian ef.elf32_file_program_header_table) in
  let sht_bytes   = (bytes_of_elf32_section_header_table endian ef.elf32_file_section_header_table) in
  let pht_off     = (Uint32_wrapper.to_bigint ef.elf32_file_header.elf32_phoff) in
  let sht_off     = (Uint32_wrapper.to_bigint ef.elf32_file_header.elf32_shoff) in
  let pht_layout  = (pht_off, pht_bytes) in
  let sht_layout  = (sht_off, sht_bytes) in
  let bab_layout  = (ef.elf32_file_bits_and_bobs) in
  if List.length ef.elf32_file_program_header_table =
    List.length ef.elf32_file_interpreted_segments then
    if List.length ef.elf32_file_section_header_table =
      List.length ef.elf32_file_interpreted_sections then
      let segs_zip  = (Lem_list.list_combine ef.elf32_file_program_header_table ef.elf32_file_interpreted_segments) in
      let sects_zip = (Lem_list.list_combine ef.elf32_file_section_header_table ef.elf32_file_interpreted_sections) in
      let segs_layout =
        (Lem_list.map (fun (seg, interp_seg) ->
          (Uint32_wrapper.to_bigint seg.elf32_p_offset, interp_seg.elf32_segment_body)
        ) (List.filter (fun (x, _) -> not (x.elf32_p_filesz = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0))))) segs_zip))
      in
      let sects_layout =
        (Lem_list.map (fun (sect, interp_sect) ->
          (Uint32_wrapper.to_bigint sect.elf32_sh_offset, interp_sect.elf32_section_body)
        ) (List.filter (fun (x, _) -> not (x.elf32_sh_type = (Uint32_wrapper.of_bigint sht_nobits))) sects_zip))
      in
      let pre_layout =  (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev [hdr_layout; pht_layout; sht_layout]) sects_layout)) segs_layout)) bab_layout) in
      let final_layout =
        (List.sort (fun (off_x, _) (off_y, _) -> Nat_big_num.compare off_x off_y)
          pre_layout)
      in
      let concats =
        (foldM (fun x y ->
          let (current_offset, so_far) = x in
          let (point_to_add, body) = y in
            if Nat_big_num.less point_to_add current_offset then
              let diff = (Nat_big_num.sub_nat current_offset point_to_add) in
                (* Completely contained inside other segment *)
                if Nat_big_num.less (Byte_sequence.length0 body) diff then
                  return (current_offset, so_far)
                else bind (Byte_sequence.partition0 diff body) (fun (_, cut) ->
                  let concat2 = (Byte_sequence.concat [so_far; cut]) in
                  let delta  = (Nat_big_num.add current_offset (Byte_sequence.length0 cut)) in
                    return (delta, concat2))
            else
              let diff   = (Nat_big_num.sub_nat point_to_add current_offset) in
              let reps   = (Byte_sequence.create diff '\000') in
              let concat2 = (Byte_sequence.concat [so_far; reps; body]) in
              let delta  = (Nat_big_num.add point_to_add (Byte_sequence.length0 body)) in
                return (delta, concat2)
        ) ( (Nat_big_num.of_int 0), Byte_sequence.empty) final_layout)
      in bind concats (fun (offset, body) ->
        return body)
    else
      fail "bytes_of_elf32_file: interpreted sections and section header table must have same length"
  else
    fail "bytes_of_elf32_file: interpreted segments and program header table must have same length")

(** [elf64_file] record captures the internal structure of an ELF32 file.
  * Invariant: length of the program header and section header tables should match
  * the length of their interpreted counterparts, and the nth element of the
  * (program/section) header table must correspond to the nth element of the
  * interpreted (segments/sections), respectively.
  *)
type elf64_file =
  { elf64_file_header               : elf64_header                   (** The file header. *)
   ; elf64_file_program_header_table : elf64_program_header_table     (** The program header table. *)
   ; elf64_file_section_header_table : elf64_section_header_table     (** The section header table. *)
   ; elf64_file_interpreted_segments : elf64_interpreted_segments     (** A more usable interpretation of the file's segments. *)
   ; elf64_file_interpreted_sections : elf64_interpreted_sections     (** A more usable interpretation of the file's sections. *)
   ; elf64_file_bits_and_bobs        : (Nat_big_num.num * byte_sequence0) list (** The uninterpreted "rubbish" that may appear in gaps in the binary file. *)
   }


type elf_file =
  | ELF_File_32 of elf32_file
  | ELF_File_64 of elf64_file




(** [bytes_of_elf64_file f1] blits ELF file [f1] to a byte sequence, ready for
  * writing to a binary file.  Fails if the invariant on [elf64_file] mentioned
  * above is not respected.
  *)
(*val bytes_of_elf64_file : elf64_file -> error byte_sequence*)
let bytes_of_elf64_file ef:(Byte_sequence_wrapper.byte_sequence)error=
   (let endian      = (get_elf64_header_endianness ef.elf64_file_header) in
  let hdr_bytes   = (bytes_of_elf64_header ef.elf64_file_header) in
  let hdr_layout  = ( (Nat_big_num.of_int 0), hdr_bytes) in
  let pht_bytes   = (bytes_of_elf64_program_header_table endian ef.elf64_file_program_header_table) in
  let sht_bytes   = (bytes_of_elf64_section_header_table endian ef.elf64_file_section_header_table) in
  let pht_off     = (Uint64_wrapper.to_bigint ef.elf64_file_header.elf64_phoff) in
  let sht_off     = (Uint64_wrapper.to_bigint ef.elf64_file_header.elf64_shoff) in
  let pht_layout  = (pht_off, pht_bytes) in
  let sht_layout  = (sht_off, sht_bytes) in
  let bab_layout  = (ef.elf64_file_bits_and_bobs) in
  if (* List.length ef.elf64_file_program_header_table =
    List.length ef.elf64_file_interpreted_segments *) true then
    if List.length ef.elf64_file_section_header_table =
      List.length ef.elf64_file_interpreted_sections then
      let segs_zip  = (Lem_list.list_combine ef.elf64_file_program_header_table ef.elf64_file_interpreted_segments) in
      let sects_zip = (Lem_list.list_combine ef.elf64_file_section_header_table ef.elf64_file_interpreted_sections) in
      let segs_layout = ([]) (*
        List.map (fun (seg, interp_seg) ->
          (natural_of_elf64_off seg.elf64_p_offset, interp_seg.elf64_segment_body)
        ) (List.filter (fun (x, _) -> x.elf64_p_filesz <> elf64_xword_of_natural 0) segs_zip) *)
      in
      let sects_layout =
        (Lem_list.map (fun (sect, interp_sect) ->
          (Uint64_wrapper.to_bigint sect.elf64_sh_offset, interp_sect.elf64_section_body)
        ) (List.filter (fun (x, _) -> not (x.elf64_sh_type = (Uint32_wrapper.of_bigint sht_nobits))) sects_zip))
      in
      let pre_layout =  (List.rev_append (List.rev (List.rev_append (List.rev (List.rev_append (List.rev [hdr_layout; pht_layout; sht_layout]) sects_layout)) segs_layout)) bab_layout) in
      let final_layout =
        (List.sort (fun (off_x, _) (off_y, _) -> Nat_big_num.compare off_x off_y)
          pre_layout)
      in
      let concats =
        (foldM (fun x y ->
          let (current_offset, so_far) = x in
          let (point_to_add, body) = y in
            if Nat_big_num.less point_to_add current_offset then
              let diff = (Nat_big_num.sub_nat current_offset point_to_add) in
                (* Completely contained inside other segment *)
                if Nat_big_num.less (Byte_sequence.length0 body) diff then
                  return (current_offset, so_far)
                else bind (Byte_sequence.partition0 diff body) (fun (_, cut) ->
                  let concat2 = (Byte_sequence.concat [so_far; cut]) in
                  let delta  = (Nat_big_num.add current_offset (Byte_sequence.length0 cut)) in
                    return (delta, concat2))
            else
              let diff   = (Nat_big_num.sub_nat point_to_add current_offset) in
              let reps   = (Byte_sequence.create diff '\000') in
              let concat2 = (Byte_sequence.concat [so_far; reps; body]) in
              let delta  = (Nat_big_num.add point_to_add (Byte_sequence.length0 body)) in
                return (delta, concat2)
        ) ( (Nat_big_num.of_int 0), Byte_sequence.empty) final_layout)
      in bind concats (fun (offset, body) ->
        return body)
    else
      fail "bytes_of_elf64_file: interpreted sections and section header table must have same length"
  else
    fail "bytes_of_elf64_file: interpreted segments and program header table must have same length")

(** [obtain_elf32_program_header_table hdr bs0] reads a file's program header table
  * from byte sequence [bs0] using information gleaned from the file header [hdr].
  * Fails if transcription fails.
  *)
(*val obtain_elf32_program_header_table : elf32_header -> byte_sequence
  -> error elf32_program_header_table*)
let obtain_elf32_program_header_table hdr bs0:((elf32_program_header_table_entry)list)error=
   (let endian      = (get_elf32_header_endianness hdr) in
  let pentries    = (Uint32_wrapper.to_bigint hdr.elf32_phnum)     in
  let pentry_size = (Uint32_wrapper.to_bigint hdr.elf32_phentsize) in
  let psize       = (Nat_big_num.mul pentries pentry_size) in
    if Nat_big_num.equal psize( (Nat_big_num.of_int 0)) then
      return []
    else
      let poffset = (Uint32_wrapper.to_bigint hdr.elf32_phoff) in bind (Byte_sequence.offset_and_cut poffset psize bs0) (fun pexact -> bind (
      (* Byte sequence irrelevant below as exact size used... *)read_elf32_program_header_table psize endian pexact) (fun (pht, _) ->
      return pht)))

(** [obtain_elf64_program_header_table hdr bs0] reads a file's program header table
  * from byte sequence [bs0] using information gleaned from the file header [hdr].
  * Fails if transcription fails.
  *)
(*val obtain_elf64_program_header_table : elf64_header -> byte_sequence
  -> error elf64_program_header_table*)
let obtain_elf64_program_header_table hdr bs0:((elf64_program_header_table_entry)list)error=
   (let endian      = (get_elf64_header_endianness hdr) in
  let pentries    = (Uint32_wrapper.to_bigint hdr.elf64_phnum)     in
  let pentry_size = (Uint32_wrapper.to_bigint hdr.elf64_phentsize) in
  let psize       = (Nat_big_num.mul pentries pentry_size) in
    if Nat_big_num.equal psize( (Nat_big_num.of_int 0)) then
      return []
    else
      let poffset = (Uint64_wrapper.to_bigint hdr.elf64_phoff) in bind (Byte_sequence.offset_and_cut poffset psize bs0) (fun pexact -> bind (
      (* Byte sequence irrelevant below as exact size used... *)read_elf64_program_header_table psize endian pexact) (fun (pht, _) ->
      return pht)))

(** [obtain_elf32_section_header_table hdr bs0] reads a file's section header table
  * from byte sequence [bs0] using information gleaned from the file header [hdr].
  * Fails if transcription fails.
  *)
(*val obtain_elf32_section_header_table : elf32_header -> byte_sequence
  -> error elf32_section_header_table*)
let obtain_elf32_section_header_table hdr bs0:((elf32_section_header_table_entry)list)error=
   (let endian      = (get_elf32_header_endianness hdr) in
  let sentries    = (Uint32_wrapper.to_bigint hdr.elf32_shnum) in
  let sentry_size = (Uint32_wrapper.to_bigint hdr.elf32_shentsize) in
  let ssize       = (Nat_big_num.mul sentries sentry_size) in
    if Nat_big_num.equal ssize( (Nat_big_num.of_int 0)) then
      return []
    else
      let soffset = (Uint32_wrapper.to_bigint hdr.elf32_shoff) in bind (Byte_sequence.offset_and_cut soffset ssize bs0) (fun sexact -> bind (
      (* Byte sequence irrelevant below as exact size used... *)read_elf32_section_header_table ssize endian sexact) (fun (sht, _) ->
      return sht)))

(** [obtain_elf64_section_header_table hdr bs0] reads a file's section header table
  * from byte sequence [bs0] using information gleaned from the file header [hdr].
  * Fails if transcription fails.
  *)
(*val obtain_elf64_section_header_table : elf64_header -> byte_sequence -> error elf64_section_header_table*)
let obtain_elf64_section_header_table hdr bs0:((elf64_section_header_table_entry)list)error=
   (let endian      = (get_elf64_header_endianness hdr) in
  let sentries    = (Uint32_wrapper.to_bigint hdr.elf64_shnum) in
  let sentry_size = (Uint32_wrapper.to_bigint hdr.elf64_shentsize) in
  let ssize       = (Nat_big_num.mul sentries sentry_size) in
    if Nat_big_num.equal ssize( (Nat_big_num.of_int 0)) then
      return []
    else
      let soffset = (Uint64_wrapper.to_bigint hdr.elf64_shoff) in bind (Byte_sequence.offset_and_cut soffset ssize bs0) (fun sexact -> bind (
      (* Byte sequence irrelevant below as exact size used... *)read_elf64_section_header_table ssize endian sexact) (fun (sht, _) ->
      return sht)))

(** [obtain_elf32_section_header_string_table hdr sht bs0] reads a file's section
  * header string table from byte sequence [bs0] using information gleaned from
  * the file header [hdr] and section header table [sht].
  * Fails if transcription fails.
  *)
(*val obtain_elf32_section_header_string_table : elf32_header ->
  elf32_section_header_table -> byte_sequence -> error (maybe string_table)*)
let obtain_elf32_section_header_string_table hdr sht bs0:((string_table)option)error=
   (if Nat_big_num.equal (Uint32_wrapper.to_bigint hdr.elf32_shstrndx) shn_undef then
    return None
  else bind (match Ml_bindings.list_index_big_int (Uint32_wrapper.to_bigint hdr.elf32_shstrndx) sht with
      None -> fail "no section header string table"
      | Some x -> return x
    ) (fun sh -> bind (Byte_sequence.offset_and_cut (Uint32_wrapper.to_bigint sh.elf32_sh_offset) (Uint32_wrapper.to_bigint sh.elf32_sh_size) bs0) (fun sexact ->
    return (Some (string_table_of_byte_sequence sexact)))))

(** [obtain_elf64_section_header_string_table hdr sht bs0] reads a file's section
  * header string table from byte sequence [bs0] using information gleaned from
  * the file header [hdr] and section header table [sht].
  * Fails if transcription fails.
  *)
(*val obtain_elf64_section_header_string_table : elf64_header ->
  elf64_section_header_table -> byte_sequence -> error (maybe string_table)*)
let obtain_elf64_section_header_string_table hdr sht bs0:((string_table)option)error=
   (if Nat_big_num.equal (Uint32_wrapper.to_bigint hdr.elf64_shstrndx) shn_undef then
    return None
  else bind (match Ml_bindings.list_index_big_int (Uint32_wrapper.to_bigint hdr.elf64_shstrndx) sht with
      None -> fail "no section header string table"
      | Some x -> return x
    ) (fun sh -> bind (Byte_sequence.offset_and_cut (Uint64_wrapper.to_bigint sh.elf64_sh_offset) (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) bs0) (fun sexact ->
    return (Some (string_table_of_byte_sequence sexact)))))

(** [obtain_elf32_interpreted_segments pht bs0] generates the interpreted segments
  * of an ELF file from the uninterpreted program header table entries in [pht],
  * read from byte sequence [bs0].  Makes working with segments easier.
  * May fail if transcription of any segment fails.
  *)
(*val obtain_elf32_interpreted_segments : elf32_program_header_table -> byte_sequence
  -> error elf32_interpreted_segments*)
let obtain_elf32_interpreted_segments pht bdy:((elf32_interpreted_segment)list)error=
   (mapM (fun ph ->
    let offset   = (Uint32_wrapper.to_bigint ph.elf32_p_offset)  in
    let size2     = (Uint32_wrapper.to_bigint ph.elf32_p_filesz) in bind (if Nat_big_num.equal size2( (Nat_big_num.of_int 0)) then
         return Byte_sequence.empty
       else
         Byte_sequence.offset_and_cut offset size2 bdy) (fun relevant ->
    let vaddr    = (Uint32_wrapper.to_bigint ph.elf32_p_vaddr) in
    let paddr    = (Uint32_wrapper.to_bigint ph.elf32_p_paddr) in
    let memsz    = (Uint32_wrapper.to_bigint ph.elf32_p_memsz) in
    let typ      = (Uint32_wrapper.to_bigint ph.elf32_p_type)  in
    let align    = (Uint32_wrapper.to_bigint ph.elf32_p_align) in
    let flags    = (parse_elf_segment_permissions (Uint32_wrapper.to_bigint ph.elf32_p_flags)) in
      if Nat_big_num.less memsz size2 then
        fail "obtain_elf32_interpreted_segments: memory size of segment cannot be less than file size"
      else
        return { elf32_segment_body = relevant; elf32_segment_type = typ;
                    elf32_segment_size = size2; elf32_segment_memsz = memsz;
                    elf32_segment_base  = vaddr; elf32_segment_flags = flags;
                    elf32_segment_paddr = paddr; elf32_segment_align = align;
                    elf32_segment_offset = offset })
    ) pht)

(** [obtain_elf64_interpreted_segments pht bs0] generates the interpreted segments
  * of an ELF file from the uninterpreted program header table entries in [pht],
  * read from byte sequence [bs0].  Makes working with segments easier.
  * May fail if transcription of any segment fails.
  *)
(*val obtain_elf64_interpreted_segments : elf64_program_header_table -> byte_sequence
  -> error elf64_interpreted_segments*)
let obtain_elf64_interpreted_segments pht bdy:((elf64_interpreted_segment)list)error=
   (mapM (fun ph ->
    let offset   = (Uint64_wrapper.to_bigint   ph.elf64_p_offset)  in
    let size2     = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_filesz) in bind (if Nat_big_num.equal size2( (Nat_big_num.of_int 0)) then
         return Byte_sequence.empty
       else
         Byte_sequence.offset_and_cut offset size2 bdy) (fun relevant ->
    let vaddr    = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_vaddr) in
    let paddr    = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_paddr) in
    let memsz    = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_memsz) in
    let typ      = (Uint32_wrapper.to_bigint  ph.elf64_p_type)  in
    let align    = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_align) in
    let flags    = (parse_elf_segment_permissions (Uint32_wrapper.to_bigint ph.elf64_p_flags)) in
      (* TODO: this happens in coredumps, just disabling this check for now *)
      (* if memsz < size then
        fail ("obtain_elf64_interpreted_segments: memory size of segment (0x" ^ (hex_string_of_natural memsz) ^ ") cannot be less than file size (0x" ^ (hex_string_of_natural size) ^ ")")
      else *)
        return { elf64_segment_body = relevant; elf64_segment_type = typ;
                    elf64_segment_size = size2; elf64_segment_memsz = memsz;
                    elf64_segment_base  = vaddr; elf64_segment_flags = flags;
                    elf64_segment_align = align; elf64_segment_paddr = paddr;
                    elf64_segment_offset = offset })
    ) pht)

(** [obtain_elf32_interpreted_section sht bs0] generates the interpreted sections
  * of an ELF file from the uninterpreted section header table entries in [sht],
  * read from byte sequence [bs0].  Makes working with sections easier.
  * May fail if transcription of any section fails.
  *)
(*val obtain_elf32_interpreted_sections : maybe string_table -> elf32_section_header_table
  -> byte_sequence -> error elf32_interpreted_sections*)
let obtain_elf32_interpreted_sections shstrtab sht bs0:((elf32_interpreted_section)list)error=
   (mapM (fun sh ->
    let offset = (Uint32_wrapper.to_bigint  sh.elf32_sh_offset) in
    let size2   = (Uint32_wrapper.to_bigint sh.elf32_sh_size) in
    let name1   = (Uint32_wrapper.to_bigint sh.elf32_sh_name) in
    let typ    = (Uint32_wrapper.to_bigint sh.elf32_sh_type) in
    let filesz = (if Nat_big_num.equal typ sht_nobits then  (Nat_big_num.of_int 0) else size2) in
    let flags  = (Uint32_wrapper.to_bigint sh.elf32_sh_flags) in
    let base   = (Uint32_wrapper.to_bigint sh.elf32_sh_addr) in
    let link1   = (Uint32_wrapper.to_bigint sh.elf32_sh_link) in
    let info   = (Uint32_wrapper.to_bigint sh.elf32_sh_info) in
    let align  = (Uint32_wrapper.to_bigint sh.elf32_sh_addralign) in
    let entry_size = (Uint32_wrapper.to_bigint sh.elf32_sh_entsize) in
    let name_string =
      ((match shstrtab with
        None -> ""
      | Some shstrtab ->
          (match (get_string_at name1 shstrtab) with
            | Success n -> n
            | Fail _ -> ""
          )
      ))
    in bind (if Nat_big_num.equal filesz( (Nat_big_num.of_int 0)) then
        return Byte_sequence.empty
      else
        Byte_sequence.offset_and_cut offset filesz bs0) (fun relevant ->
      return { elf32_section_name = name1; elf32_section_type = typ;
          elf32_section_size = size2; elf32_section_offset = offset;
          elf32_section_flags = flags; elf32_section_addr = base;
          elf32_section_link = link1; elf32_section_info = info;
          elf32_section_align = align; elf32_section_body = relevant;
          elf32_section_entsize = entry_size;
          elf32_section_name_as_string = name_string })
  ) sht)

(** [obtain_elf64_interpreted_section sht bs0] generates the interpreted sections
  * of an ELF file from the uninterpreted section header table entries in [sht],
  * read from byte sequence [bs0].  Makes working with sections easier.
  * May fail if transcription of any section fails.
  *)
(*val obtain_elf64_interpreted_sections : maybe string_table -> elf64_section_header_table
  -> byte_sequence -> error elf64_interpreted_sections*)
let obtain_elf64_interpreted_sections shstrtab sht bs0:((elf64_interpreted_section)list)error=
   (mapM (fun sh ->
    let offset = (Uint64_wrapper.to_bigint   sh.elf64_sh_offset) in
    let size2   = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) in
    let name1   = (Uint32_wrapper.to_bigint  sh.elf64_sh_name) in
    let typ    = (Uint32_wrapper.to_bigint  sh.elf64_sh_type) in
    let filesz = (if Nat_big_num.equal typ sht_nobits then  (Nat_big_num.of_int 0) else size2) in
    let flags  = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_flags) in
    let base   = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addr) in
    let link1   = (Uint32_wrapper.to_bigint  sh.elf64_sh_link) in
    let info   = (Uint32_wrapper.to_bigint  sh.elf64_sh_info) in
    let align  = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addralign) in
    let entry_size = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_entsize) in
    let name_string =
      ((match shstrtab with
        None -> ""
      | Some shstrtab ->
          (match (get_string_at name1 shstrtab) with
            | Success n -> n
            | Fail _ -> ""
          )
      ))
    in bind (if Nat_big_num.equal filesz( (Nat_big_num.of_int 0)) then
        return Byte_sequence.empty
      else
        Byte_sequence.offset_and_cut offset filesz bs0) (fun relevant ->
      return { elf64_section_name = name1; elf64_section_type = typ;
          elf64_section_size = size2; elf64_section_offset = offset;
          elf64_section_flags = flags; elf64_section_addr = base;
          elf64_section_link = link1; elf64_section_info = info;
          elf64_section_align = align; elf64_section_body = relevant;
          elf64_section_entsize = entry_size;
          elf64_section_name_as_string = name_string })
  ) sht)

(** [find_first_not_in_range e rngs] for every pair (start, end) in [rngs], finds
  * the first element, beginning counting from [e], that does not lie between
  * a start and end value.
  *)
(*val find_first_not_in_range : natural -> list (natural * natural) -> natural*)
let rec find_first_not_in_range start ranges:Nat_big_num.num=
   ((match List.filter (fun (x, y) -> Nat_big_num.greater_equal start x && Nat_big_num.less_equal start y) ranges with
    | [] -> start
    | _  -> find_first_not_in_range ( Nat_big_num.add start( (Nat_big_num.of_int 1))) ranges
  ))

(** [find_first_in_range e rngs] for every pair (start, end) in [rngs], finds
  * the first element, beginning counting from [e], that lies between
  * a start and end value.
  *)
(*val find_first_in_range : natural -> list (natural * natural) -> natural*)
let rec find_first_in_range start ranges:Nat_big_num.num=
   ((match List.filter (fun (x, y) -> Nat_big_num.greater_equal start x && Nat_big_num.less_equal start y) ranges with
    | [] -> find_first_in_range ( Nat_big_num.add start( (Nat_big_num.of_int 1))) ranges
    | _  -> start
  ))

(** [compute_differences start max ranges] is a utility function used for calculating
  * "dead" spots in an ELF file not covered by any of the interpreted structure
  * that nevertheless need recording in the bits_and_bobs field of each ELF record
  * in order to maintain in-out roundtripping up to exact binary equivalence.
  *)
(*val compute_differences : natural -> natural -> list (natural * natural) -> error (list (natural * natural))*)
let rec compute_differences start max ranges:((Nat_big_num.num*Nat_big_num.num)list)error=
   (if Nat_big_num.equal start max then
    return []
  else if Nat_big_num.greater start max then
    fail "compute_differences: passed maximum"
  else
    let first = (find_first_not_in_range start ranges) in
      if Nat_big_num.greater_equal first max then
        return []
      else
        let last1 = (find_first_in_range first ranges) in
          if Nat_big_num.greater last1 max then
            return [(first, max)]
          else bind (compute_differences last1 max ranges) (fun tail ->
            return ((first, last1)::tail)))

(** [obtain_elf32_bits_and_bobs hdr pht segs sht sects bs0] identifies and records
  * the "dead" spots of an ELF file not covered by any meaningful structure of the
  * ELF file format.
  *)
(*val obtain_elf32_bits_and_bobs : elf32_header -> elf32_program_header_table -> elf32_interpreted_segments
  -> elf32_section_header_table -> elf32_interpreted_sections -> byte_sequence -> error (list (natural * byte_sequence))*)
let obtain_elf32_bits_and_bobs hdr segs interp_segs sects interp_sects bs0:((Nat_big_num.num*Byte_sequence_wrapper.byte_sequence)list)error=
   (let hdr_off_len  = ( (Nat_big_num.of_int 0), Uint32_wrapper.to_bigint hdr.elf32_ehsize) in
  let pht_off      = (Uint32_wrapper.to_bigint hdr.elf32_phoff) in
  let pht_len      = (Nat_big_num.mul (Uint32_wrapper.to_bigint hdr.elf32_phentsize) (Uint32_wrapper.to_bigint hdr.elf32_phnum)) in
  let pht_off_len  = (pht_off, Nat_big_num.add pht_off pht_len) in
  let sht_off      = (Uint32_wrapper.to_bigint hdr.elf32_shoff) in
  let sht_len      = (Nat_big_num.mul (Uint32_wrapper.to_bigint hdr.elf32_shentsize) (Uint32_wrapper.to_bigint hdr.elf32_shnum)) in
  let sht_off_len  = (sht_off, Nat_big_num.add sht_off sht_len) in
    if List.length interp_segs = List.length segs then
      let seg_zip = (Lem_list.list_combine segs interp_segs) in
      if List.length interp_sects = List.length sects then
        let sect_zip = (Lem_list.list_combine sects interp_sects) in
        let seg_off_len  =
          (Lem_list.map (fun (seg, interp_seg) ->
            let start = (Uint32_wrapper.to_bigint seg.elf32_p_offset) in
            let len   = (interp_seg.elf32_segment_size) in
            (start, Nat_big_num.add start len)) seg_zip)
        in
        let sect_off_len =
          (Lem_list.map (fun (sect, interp_sect) ->
            let start = (Uint32_wrapper.to_bigint sect.elf32_sh_offset) in
            let len   = (interp_sect.elf32_section_size) in
            (start, Nat_big_num.add start len)) sect_zip)
        in
        let pre_layout   = (hdr_off_len :: (pht_off_len :: (sht_off_len ::  List.rev_append (List.rev seg_off_len) sect_off_len))) in
        let layout       =
          (List.sort (fun (off_x, _) (off_y, _) ->
            Nat_big_num.compare off_x off_y
          ) pre_layout)
        in bind (compute_differences( (Nat_big_num.of_int 0)) (Byte_sequence.length0 bs0) layout) (fun diffs ->
            mapM (fun (start, len) -> bind (Byte_sequence.offset_and_cut start ( Nat_big_num.sub_nat len start) bs0) (fun rel ->
              return (start, rel))
            ) diffs)
      else
        fail "obtain_elf32_bits_and_bobs: section header table and interpreted section differ in length"
    else
      fail "obtain_elf32_bits_and_bobs: program header table and interpreted segments differ in length")

(** [obtain_elf64_bits_and_bobs hdr pht segs sht sects bs0] identifies and records
  * the "dead" spots of an ELF file not covered by any meaningful structure of the
  * ELF file format.
  *)
(*val obtain_elf64_bits_and_bobs : elf64_header -> elf64_program_header_table -> elf64_interpreted_segments
  -> elf64_section_header_table -> elf64_interpreted_sections -> byte_sequence -> error (list (natural * byte_sequence))*)
let obtain_elf64_bits_and_bobs hdr segs interp_segs sects interp_sects bs0:((Nat_big_num.num*Byte_sequence_wrapper.byte_sequence)list)error=
   (let hdr_off_len  = ( (Nat_big_num.of_int 0), Uint32_wrapper.to_bigint hdr.elf64_ehsize) in

  let pht_off      = (Uint64_wrapper.to_bigint hdr.elf64_phoff) in
  let pht_len      = (Nat_big_num.mul (Uint32_wrapper.to_bigint hdr.elf64_phentsize) (Uint32_wrapper.to_bigint hdr.elf64_phnum)) in
  let pht_off_len  = (pht_off, Nat_big_num.add pht_off pht_len) in
  let sht_off      = (Uint64_wrapper.to_bigint hdr.elf64_shoff) in
  let sht_len      = (Nat_big_num.mul (Uint32_wrapper.to_bigint hdr.elf64_shentsize) (Uint32_wrapper.to_bigint hdr.elf64_shnum)) in
  let sht_off_len  = (sht_off, Nat_big_num.add sht_off sht_len) in
    if List.length interp_segs = List.length segs then
      let seg_zip = (Lem_list.list_combine segs interp_segs) in
      if List.length interp_sects = List.length sects then
        let sect_zip = (Lem_list.list_combine sects interp_sects) in
        let seg_off_len  =
          (Lem_list.map (fun (seg, interp_seg) ->
            let start = (Uint64_wrapper.to_bigint seg.elf64_p_offset) in
            let len   = (interp_seg.elf64_segment_size) in
            (start, Nat_big_num.add start len)) seg_zip)
        in
        let sect_off_len =
          (Lem_list.map (fun (sect, interp_sect) ->
            let start = (Uint64_wrapper.to_bigint sect.elf64_sh_offset) in
            let len   = (interp_sect.elf64_section_size) in
            (start, Nat_big_num.add start len)) sect_zip)
        in
        let pre_layout   = (hdr_off_len :: (pht_off_len :: (sht_off_len ::  List.rev_append (List.rev seg_off_len) sect_off_len))) in
        let layout       =
          (List.sort (fun (off_x, _) (off_y, _) ->
            Nat_big_num.compare off_x off_y
          ) pre_layout)
        in bind (compute_differences( (Nat_big_num.of_int 0)) (Byte_sequence.length0 bs0) layout) (fun diffs ->
            mapM (fun (start, finish) -> bind (Byte_sequence.offset_and_cut start ( Nat_big_num.sub_nat finish start) bs0) (fun rel ->
              return (start, rel))
            ) diffs)
      else
        fail "obtain_elf64_bits_and_bobs: section header table and interpreted section differ in length"
    else
      fail "obtain_elf64_bits_and_bobs: program header table and interpreted segments differ in length")

(** [read_elf32_file bs0] reads an ELF32 file from byte sequence [bs0].  Fails if
  * transcription fails.
  *)
(*val read_elf32_file : byte_sequence -> error elf32_file*)
let read_elf32_file bs0:(elf32_file)error=  (bind (read_elf32_header bs0) (fun (hdr, bs1) -> bind (obtain_elf32_program_header_table hdr bs0) (fun pht  -> bind (obtain_elf32_section_header_table hdr bs0) (fun sht  -> bind (obtain_elf32_section_header_string_table hdr sht bs0) (fun shstrtab -> bind (obtain_elf32_interpreted_segments pht bs0) (fun segs -> bind (obtain_elf32_interpreted_sections shstrtab sht bs0) (fun sects -> bind (obtain_elf32_bits_and_bobs hdr pht segs sht sects bs0) (fun bits_and_bobs ->
  return { elf32_file_header = hdr;
              elf32_file_program_header_table = pht;
              elf32_file_section_header_table = sht;
              elf32_file_interpreted_segments = segs;
              elf32_file_interpreted_sections = sects;
              elf32_file_bits_and_bobs = bits_and_bobs }))))))))

(** [read_elf64_file bs0] reads an ELF64 file from byte sequence [bs0].  Fails if
  * transcription fails.
  *)
(*val read_elf64_file : byte_sequence -> error elf64_file*)
let read_elf64_file bs0:(elf64_file)error=  (bind (read_elf64_header bs0) (fun (hdr, bs1) -> bind (obtain_elf64_program_header_table hdr bs0) (fun pht  -> bind (obtain_elf64_section_header_table hdr bs0) (fun sht  -> bind (obtain_elf64_section_header_string_table hdr sht bs0) (fun shstrtab -> bind (obtain_elf64_interpreted_segments pht bs0) (fun segs -> bind (obtain_elf64_interpreted_sections shstrtab sht bs0) (fun sects -> bind (obtain_elf64_bits_and_bobs hdr pht segs sht sects bs0) (fun bits_and_bobs ->
  return { elf64_file_header = hdr;
              elf64_file_program_header_table = pht;
              elf64_file_section_header_table = sht;
              elf64_file_interpreted_segments = segs;
              elf64_file_interpreted_sections = sects;
              elf64_file_bits_and_bobs = bits_and_bobs }))))))))

(** [get_elf32_file_secton_header_string_table f1] returns the ELF file, [f1],
  * section header string table.
  * TODO: why is this not using obtain_elf32_section_header_string_table above?
  *)
(*val get_elf32_file_section_header_string_table : elf32_file -> error string_table*)
let get_elf32_file_section_header_string_table f3:(string_table)error=
   (let hdr  = (f3.elf32_file_header) in
  let sht  = (f3.elf32_file_section_header_table) in
  let segs = (f3.elf32_file_interpreted_segments) in
  let idx1  = (Uint32_wrapper.to_bigint hdr.elf32_shstrndx) in bind (bytes_of_elf32_file f3) (fun bs0 ->
    (match Ml_bindings.list_index_big_int idx1 sht with
      | None -> fail "obtain_elf32_string_table: invalid offset into section header table"
      | Some sect ->
          let offset = (Uint32_wrapper.to_bigint sect.elf32_sh_offset) in
          let size2   = (Uint32_wrapper.to_bigint sect.elf32_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel ->
          let strings  = (Byte_sequence.string_of_byte_sequence rel) in
          return (String_table.mk_string_table strings Missing_pervasives.null_char))
    )))

(** [get_elf64_file_secton_header_string_table f1] returns the ELF file, [f1],
  * section header string table.
  * TODO: why is this not using obtain_elf64_section_header_string_table above?
  *)
(*val get_elf64_file_section_header_string_table : elf64_file -> error string_table*)
let get_elf64_file_section_header_string_table f3:(string_table)error=
   (let hdr  = (f3.elf64_file_header) in
  let sht  = (f3.elf64_file_section_header_table) in
  let segs = (f3.elf64_file_interpreted_segments) in
  let idx1  = (Uint32_wrapper.to_bigint hdr.elf64_shstrndx) in bind (bytes_of_elf64_file f3) (fun bs0 ->
    (match Ml_bindings.list_index_big_int idx1 sht with
      | None -> fail "obtain_elf64_string_table: invalid offset into section header table"
      | Some sect ->
          let offset = (Uint64_wrapper.to_bigint   sect.elf64_sh_offset) in
          let size2   = (Ml_bindings.nat_big_num_of_uint64 sect.elf64_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun rel ->
          let strings  = (Byte_sequence.string_of_byte_sequence rel) in
          return (String_table.mk_string_table strings Missing_pervasives.null_char))
    )))

(*val find_elf32_symbols_by_symtab_idx : natural -> elf32_file -> error (elf32_symbol_table * string_table * natural)*)
let find_elf32_symbols_by_symtab_idx sec_idx f:((elf32_symbol_table_entry)list*string_table*Nat_big_num.num)error=  (bind (match Lem_list.list_index f.elf32_file_interpreted_sections (Nat_big_num.to_int sec_idx) with
        None -> fail "impossible: interpreted section found but not indexable"
        | Some sec -> return sec
    ) (fun sec -> bind (match Lem_list.list_index f.elf32_file_interpreted_sections (Nat_big_num.to_int sec.elf32_section_link) with
        None -> fail "no associated strtab"
        | Some strs -> return strs
    ) (fun strs ->
    let strings = (Byte_sequence.string_of_byte_sequence strs.elf32_section_body) in
    let strtab = (String_table.mk_string_table strings null_char) in
    let endian = (get_elf32_header_endianness f.elf32_file_header) in bind (read_elf32_symbol_table endian sec.elf32_section_body) (fun symtab ->
    return (symtab, strtab, sec_idx)))))

(*val find_elf32_symtab_by_type : natural -> elf32_file -> error (elf32_symbol_table * string_table * natural)*)
let find_elf32_symtab_by_type t f:(elf32_symbol_table*string_table*Nat_big_num.num)error=
     (let found_symtab_index = (find_index0 (fun sh -> Nat_big_num.equal sh.elf32_section_type t) f.elf32_file_interpreted_sections) in bind (match found_symtab_index with
        None -> fail "no such symtab"
        | Some sec_idx -> return sec_idx
    ) (fun sec_idx -> find_elf32_symbols_by_symtab_idx sec_idx f))

(*val find_elf64_symbols_by_symtab_idx : natural -> elf64_file -> error (elf64_symbol_table * string_table * natural)*)
let find_elf64_symbols_by_symtab_idx sec_idx f:((elf64_symbol_table_entry)list*string_table*Nat_big_num.num)error=  (bind (match Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int sec_idx) with
        None -> fail "impossible: interpreted section found but not indexable"
        | Some sec -> return sec
    ) (fun sec -> bind (match Lem_list.list_index f.elf64_file_interpreted_sections (Nat_big_num.to_int sec.elf64_section_link) with
        None -> fail "no associated strtab"
        | Some strs -> return strs
    ) (fun strs ->
    let strings = (Byte_sequence.string_of_byte_sequence strs.elf64_section_body) in
    let strtab = (String_table.mk_string_table strings null_char) in
    let endian = (get_elf64_header_endianness f.elf64_file_header) in bind (read_elf64_symbol_table endian sec.elf64_section_body) (fun symtab ->
    return (symtab, strtab, sec_idx)))))

(*val find_elf64_symtab_by_type : natural -> elf64_file -> error (elf64_symbol_table * string_table * natural)*)
let find_elf64_symtab_by_type t f:(elf64_symbol_table*string_table*Nat_big_num.num)error=
     (let found_symtab_index = (find_index0 (fun sh -> Nat_big_num.equal sh.elf64_section_type t) f.elf64_file_interpreted_sections) in bind (match found_symtab_index with
        None -> fail "no such symtab"
        | Some sec_idx -> return sec_idx
    ) (fun sec_idx -> find_elf64_symbols_by_symtab_idx sec_idx f))

(** [get_elf32_file_symbol_string_table f1] returns the ELF file [f1] symbol
  * string table.  May fail.
  *)
(*val get_elf32_file_symbol_string_table : elf32_file -> error string_table*)
let get_elf32_file_symbol_string_table f3:(string_table)error=
   (let hdr     = (f3.elf32_file_header) in
  let sht     = (f3.elf32_file_section_header_table) in
  let segs    = (f3.elf32_file_interpreted_segments) in
  let strtabs = (Missing_pervasives.mapMaybei (fun index sect ->
    if Nat_big_num.equal (Uint32_wrapper.to_bigint sect.elf32_sh_type) sht_strtab then
      if Nat_big_num.equal index (Uint32_wrapper.to_bigint hdr.elf32_shstrndx) then
        None
      else
        Some sect
    else
      None) sht)
  in bind (bytes_of_elf32_file f3) (fun bs0 ->
    bind (mapM (fun sect ->
      let offset  = (Uint32_wrapper.to_bigint  sect.elf32_sh_offset) in
      let size2    = (Uint32_wrapper.to_bigint sect.elf32_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun bs1 ->
      let strings = (Byte_sequence.string_of_byte_sequence bs1) in
      return (String_table.mk_string_table strings Missing_pervasives.null_char))) strtabs) (fun strings ->
      String_table.concat0 strings)))

(** [get_elf64_file_symbol_string_table f1] returns the ELF file [f1] symbol
  * string table.  May fail.
  *)
(*val get_elf64_file_symbol_string_table : elf64_file -> error string_table*)
let get_elf64_file_symbol_string_table f3:(string_table)error=
   (let hdr     = (f3.elf64_file_header) in
  let sht     = (f3.elf64_file_section_header_table) in
  let segs    = (f3.elf64_file_interpreted_segments) in
  let strtabs = (Missing_pervasives.mapMaybei (fun index sect ->
    if Nat_big_num.equal (Uint32_wrapper.to_bigint sect.elf64_sh_type) sht_strtab then
      if false (* PS HACK *) (*index = natural_of_elf64_half hdr.elf64_shstrndx *) then
        None
      else
        Some sect
    else
      None) sht)
  in bind (bytes_of_elf64_file f3) (fun bs0 ->
    bind (mapM (fun sect ->
      let offset  = (Uint64_wrapper.to_bigint   sect.elf64_sh_offset) in
      let size2    = (Ml_bindings.nat_big_num_of_uint64 sect.elf64_sh_size) in bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun bs1 ->
      let strings = (Byte_sequence.string_of_byte_sequence bs1) in
      return (String_table.mk_string_table strings Missing_pervasives.null_char))) strtabs) (fun strings ->
      String_table.concat0 strings)))

(** [get_elf32_file_string_table_by_index f1 index] returns the ELF file [f1]
  * string table that is pointed to by the section header table entry at index
  * [index].  May fail if index is out of range, or otherwise.
  *)
(*val get_elf32_string_table_by_index : elf32_file -> natural -> error string_table*)
let get_elf32_string_table_by_index ef link1:(string_table)error=
   (let hdr     = (ef.elf32_file_header) in
  let sht     = (ef.elf32_file_section_header_table) in
  let sects   = (ef.elf32_file_interpreted_sections) in
    (match Lem_list.list_index sects (Nat_big_num.to_int link1) with
      | None  -> fail "get_elf32_string_table_by_index: invalid index"
      | Some sym1 -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym1.elf32_section_body) Missing_pervasives.null_char)
    ))

(** [get_elf64_file_string_table_by_index f1 index] returns the ELF file [f1]
  * string table that is pointed to by the section header table entry at index
  * [index].  May fail if index is out of range, or otherwise.
  *)
(*val get_elf64_string_table_by_index : elf64_file -> natural -> error string_table*)
let get_elf64_string_table_by_index ef link1:(string_table)error=
   (let hdr     = (ef.elf64_file_header) in
  let sht     = (ef.elf64_file_section_header_table) in
  let sects   = (ef.elf64_file_interpreted_sections) in
    (match Lem_list.list_index sects (Nat_big_num.to_int link1) with
      | None  -> fail "get_elf64_string_table_by_index: invalid index"
      | Some sym1 -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym1.elf64_section_body) Missing_pervasives.null_char)
    ))

        
(** [get_elf32_file_symbol_table f1] returns the ELF file [f1] symbol
  * table.  May fail.
  *)
(*val get_elf32_file_symbol_table : elf32_file -> error elf32_symbol_table*)
let get_elf32_file_symbol_table f3:((elf32_symbol_table_entry)list)error=
   (let hdr     = (f3.elf32_file_header) in
  let sht     = (f3.elf32_file_section_header_table) in
  let segs    = (f3.elf32_file_interpreted_segments) in
  let endian  = (get_elf32_header_endianness hdr) in
  let symtabs = (List.filter (fun sect -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint sect.elf32_sh_type) sht_symtab
    ) sht)
  in
    (match symtabs with
      | [] -> return []
      | [symtab] ->
        let offset = (Uint32_wrapper.to_bigint symtab.elf32_sh_offset) in
        let size2   = (Uint32_wrapper.to_bigint symtab.elf32_sh_size) in bind (bytes_of_elf32_file f3) (fun bs0 -> bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun relevant ->
        read_elf32_symbol_table endian relevant))
      | _ ->
        fail "obtain_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB"
    ))

(** [get_elf64_file_symbol_table f1] returns the ELF file [f1] symbol
  * table.  May fail.
  *)
(*val get_elf64_file_symbol_table : elf64_file -> error (elf64_symbol_table * string_table)*)
let get_elf64_file_symbol_table f3:((elf64_symbol_table_entry)list*string_table)error=
   (let hdr     = (f3.elf64_file_header) in
  let sht     = (f3.elf64_file_section_header_table) in
  let segs    = (f3.elf64_file_interpreted_segments) in
  let endian  = (get_elf64_header_endianness hdr) in
  let symtabs = (List.filter (fun sect -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint sect.elf64_sh_type) sht_symtab
    ) sht)
  in
    (match symtabs with
      | [] -> return ([],String_table.dummy_strtab)
      | [symtab] ->
        let lnk = (Uint32_wrapper.to_bigint symtab.elf64_sh_link) in bind (get_elf64_string_table_by_index f3 lnk) (fun strtab ->
        let offset = (Uint64_wrapper.to_bigint   symtab.elf64_sh_offset) in
        let size2   = (Ml_bindings.nat_big_num_of_uint64 symtab.elf64_sh_size) in bind (bytes_of_elf64_file f3) (fun bs0 -> bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun relevant -> bind (read_elf64_symbol_table endian relevant) (fun symtab ->
          return (symtab,strtab)))))
      | _ ->
        fail "obtain_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB"
    ))

(** [get_elf32_file_dynamic_symbol_table f1] returns the ELF file [f1] dynamic
  * symbol table.  May fail.
  *)
(*val get_elf32_file_dynamic_symbol_table : elf32_file -> error elf32_symbol_table*)
let get_elf32_file_dynamic_symbol_table ef:((elf32_symbol_table_entry)list)error=
   (let hdr     = (ef.elf32_file_header) in
  let sht     = (ef.elf32_file_section_header_table) in
  let segs    = (ef.elf32_file_interpreted_segments) in
  let endian  = (get_elf32_header_endianness hdr) in
  let symtabs = (List.filter (fun sect -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint sect.elf32_sh_type) sht_dynsym
    ) sht)
  in
    (match symtabs with
      | [] -> return []
      | [symtab] ->
        let offset = (Uint32_wrapper.to_bigint symtab.elf32_sh_offset) in
        let size2   = (Uint32_wrapper.to_bigint symtab.elf32_sh_size) in bind (bytes_of_elf32_file ef) (fun bs0 -> bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun relevant ->
        read_elf32_symbol_table endian relevant))
      | _ ->
        fail "obtain_elf32_dynamic_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM"
    ))

(** [get_elf64_file_dynamic_symbol_table f1] returns the ELF file [f1] dynamic
  * symbol table.  May fail.
  *)
(*val get_elf64_file_dynamic_symbol_table : elf64_file -> error elf64_symbol_table*)
let get_elf64_file_dynamic_symbol_table ef:((elf64_symbol_table_entry)list)error=
   (let hdr     = (ef.elf64_file_header) in
  let sht     = (ef.elf64_file_section_header_table) in
  let segs    = (ef.elf64_file_interpreted_segments) in
  let endian  = (get_elf64_header_endianness hdr) in
  let symtabs = (List.filter (fun sect -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint sect.elf64_sh_type) sht_dynsym
    ) sht)
  in
    (match symtabs with
      | [] -> return []
      | [symtab] ->
        let offset = (Uint64_wrapper.to_bigint   symtab.elf64_sh_offset) in
        let size2   = (Ml_bindings.nat_big_num_of_uint64 symtab.elf64_sh_size) in bind (bytes_of_elf64_file ef) (fun bs0 -> bind (Byte_sequence.offset_and_cut offset size2 bs0) (fun relevant ->
        read_elf64_symbol_table endian relevant))
      | _ ->
        fail "obtain_elf64_dynamic_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM"
    ))

(** [get_elf32_file_symbol_table_by_index f1 index] returns the ELF file [f1]
  * symbol table that is pointed to by the section header table entry at index
  * [index].  May fail if index is out of range, or otherwise.
  *)
(*val get_elf32_symbol_table_by_index : elf32_file -> natural -> error elf32_symbol_table*)
let get_elf32_symbol_table_by_index ef link1:(elf32_symbol_table)error=
   (let hdr     = (ef.elf32_file_header) in
  let sht     = (ef.elf32_file_section_header_table) in
  let sects   = (ef.elf32_file_interpreted_sections) in
  let endian  = (get_elf32_header_endianness hdr) in
    (match Lem_list.list_index sects (Nat_big_num.to_int link1) with
      | None  -> fail "get_elf32_symbol_table_by_index: invalid index"
      | Some sym1 ->
        read_elf32_symbol_table endian sym1.elf32_section_body
    ))

(** [get_elf64_file_symbol_table_by_index f1 index] returns the ELF file [f1]
  * symbol table that is pointed to by the section header table entry at index
  * [index].  May fail if index is out of range, or otherwise.
  *)
(*val get_elf64_symbol_table_by_index : elf64_file -> natural -> error elf64_symbol_table*)
let get_elf64_symbol_table_by_index ef link1:(elf64_symbol_table)error=
   (let hdr     = (ef.elf64_file_header) in
  let sht     = (ef.elf64_file_section_header_table) in
  let sects   = (ef.elf64_file_interpreted_sections) in
  let endian  = (get_elf64_header_endianness hdr) in
    (match Lem_list.list_index sects (Nat_big_num.to_int link1) with
      | None  -> fail "get_elf64_symbol_table_by_index: invalid index"
      | Some sym1 ->
        read_elf64_symbol_table endian sym1.elf64_section_body
    ))


(** [segment_provenance] records whether a segment that appears in an executable
  * process image has been derived directly from an ELF file, or was automatically
  * created when the image calculation process noticed a segment with a memory
  * size greater than its file size.
  * Really a PPCMemism and not strictly needed for the ELF model itself.
  *)
type segment_provenance
  = FromELF       (** Segment derived directly from the source ELF file. *)
  | AutoGenerated (** Automatically generated during process extraction as memory size is greater than file size. *)

(** [elf32_executable_process_image] is a process image for ELF32 files.  Contains
  * all that is necessary to load the executable components of an ELF32 file
  * and begin execution.
  * XXX: (segments, provenance), entry point, machine type
  *)
type elf32_executable_process_image =
  ( (elf32_interpreted_segment * segment_provenance)list * Nat_big_num.num * Nat_big_num.num)

(** [elf64_executable_process_image] is a process image for ELF64 files.  Contains
  * all that is necessary to load the executable components of an ELF64 file
  * and begin execution.
  * XXX: (segments, provenance), entry point, machine type
  *)
type elf64_executable_process_image =
  ( (elf64_interpreted_segment * segment_provenance)list * Nat_big_num.num * Nat_big_num.num)

(** [get_elf32_executable_image f1] extracts an executable process image from an
  * executable ELF file.  May fail if extraction is impossible.
  *)
(*val get_elf32_executable_image : elf32_file -> error elf32_executable_process_image*)
let get_elf32_executable_image f3:((elf32_interpreted_segment*segment_provenance)list*Nat_big_num.num*Nat_big_num.num)error=
   (if is_elf32_executable_file f3.elf32_file_header then
    let entr = (f3.elf32_file_header.elf32_entry) in
    let segs = (f3.elf32_file_interpreted_segments) in
    let mach = (f3.elf32_file_header.elf32_machine) in
      (match List.filter (fun sg -> Nat_big_num.equal sg.elf32_segment_type elf_pt_load) segs with
        | []    -> fail "get_elf32_executable_image: an executable ELF file must have at least one loadable segment"
        | load  -> bind (mapM (fun sg ->
              if Nat_big_num.equal sg.elf32_segment_memsz( (Nat_big_num.of_int 0)) then
                return []
              else if Nat_big_num.equal sg.elf32_segment_memsz sg.elf32_segment_size then
                return [(sg, FromELF)]
              else if Nat_big_num.less sg.elf32_segment_size sg.elf32_segment_memsz then
                (* Cannot be negative due to check in constructing [segs]. *)
                let diff  = (Nat_big_num.sub_nat sg.elf32_segment_memsz sg.elf32_segment_size) in
                let zeros1 = (Byte_sequence.zeros diff) in
                let addr  = (Nat_big_num.add sg.elf32_segment_base sg.elf32_segment_size) in
                let align = (sg.elf32_segment_align) in
                let paddr = (sg.elf32_segment_paddr) in
                let seg   =
                  ({ elf32_segment_body = zeros1; elf32_segment_type = (sg.elf32_segment_type);
                      elf32_segment_size = diff; elf32_segment_memsz = diff;
                      elf32_segment_base = addr; elf32_segment_flags = (sg.elf32_segment_flags);
                      elf32_segment_align = align; elf32_segment_paddr = paddr;
                      elf32_segment_offset = (sg.elf32_segment_offset) })
                in
                  return [(sg, FromELF); (seg, AutoGenerated)]
              else
                fail "get_elf32_executable_image: invariant invalidated") load) (fun bs_base ->
            return (List.concat bs_base, Uint32_wrapper.to_bigint entr, Uint32_wrapper.to_bigint mach))
      )
  else
    fail "get_elf32_executable_image: not an ELF executable file")

(** [get_elf64_executable_image f1] extracts an executable process image from an
  * executable ELF file.  May fail if extraction is impossible.
  *)
(*val get_elf64_executable_image : elf64_file -> error elf64_executable_process_image*)
let get_elf64_executable_image f3:((elf64_interpreted_segment*segment_provenance)list*Nat_big_num.num*Nat_big_num.num)error=
   (if is_elf64_executable_file f3.elf64_file_header then
    let entr = (f3.elf64_file_header.elf64_entry) in
    let segs = (f3.elf64_file_interpreted_segments) in
    let mach = (f3.elf64_file_header.elf64_machine) in
      (match List.filter (fun sg -> Nat_big_num.equal sg.elf64_segment_type elf_pt_load) segs with
        | []    -> fail "get_elf64_executable_image: an executable ELF file must have at least one loadable segment"
        | load  -> bind (mapM (fun sg ->
              if Nat_big_num.equal sg.elf64_segment_memsz( (Nat_big_num.of_int 0)) then
                return []
              else if Nat_big_num.equal sg.elf64_segment_memsz sg.elf64_segment_size then
                return [(sg, FromELF)]
              else if Nat_big_num.less sg.elf64_segment_size sg.elf64_segment_memsz then
                (* Cannot be negative due to check in constructing [segs]. *)
                let diff  = (Nat_big_num.sub_nat sg.elf64_segment_memsz sg.elf64_segment_size) in
                let zeros1 = (Byte_sequence.zeros diff) in
                let addr  = (Nat_big_num.add sg.elf64_segment_base sg.elf64_segment_size) in
                let align = (sg.elf64_segment_align) in
                let paddr = (sg.elf64_segment_paddr) in
                let seg   =
                  ({ elf64_segment_body = zeros1; elf64_segment_type = (sg.elf64_segment_type);
                      elf64_segment_size = diff; elf64_segment_memsz = diff;
                      elf64_segment_base = addr; elf64_segment_flags = (sg.elf64_segment_flags);
                      elf64_segment_align = align; elf64_segment_paddr = paddr;
                      elf64_segment_offset = (sg.elf64_segment_offset) })
                in
                  return [(sg, FromELF); (seg, AutoGenerated)]
              else
                fail "get_elf64_executable_image: invariant invalidated") load) (fun bs_base ->
            return (List.concat bs_base, Ml_bindings.nat_big_num_of_uint64 entr, Uint32_wrapper.to_bigint mach))
      )
  else
    fail "elf64_get_executable_image: not an executable ELF file")

(** [global_symbol_init_info] records the name, type, size, address, chunk
  * of initialisation data (if relevant for that symbol), and binding, of every
  * global symbol in an ELF file.
  * Another PPCMemism.
  *)
type global_symbol_init_info
  = (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num *  byte_sequence0 option * Nat_big_num.num)) list

(** [get_elf32_file_global_symbol_init f1] extracts the global symbol init info
  * for ELF file [f1].  May fail.
  *)
(*val get_elf32_file_global_symbol_init : elf32_file -> error global_symbol_init_info*)
let get_elf32_file_global_symbol_init f3:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(Byte_sequence_wrapper.byte_sequence)option*Nat_big_num.num))list)error=
   (if is_elf32_executable_file f3.elf32_file_header then
    let segs   = (f3.elf32_file_interpreted_segments) in bind (bytes_of_elf32_file f3) (fun bs0 -> bind (get_elf32_file_symbol_table f3) (fun symtab -> bind (get_elf32_file_symbol_string_table f3) (fun strtab -> bind (Elf_symbol_table.get_elf32_symbol_image_address symtab strtab) (fun strs ->
      let mapped = (mapM (fun (symbol, (typ, size2, addr, bind1)) ->
        if Nat_big_num.equal typ Elf_symbol_table.stt_object then bind (get_elf32_executable_image f3) (fun (img2, entry, mach) ->
          let chunks2 =
            (List.filter (fun (chunk, _) -> Nat_big_num.greater_equal
              addr chunk.elf32_segment_base &&
                (if Nat_big_num.greater size2( (Nat_big_num.of_int 0))
                 then Nat_big_num.less_equal (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf32_segment_base chunk.elf32_segment_size)
                 (* We don't consider a zero-size symbol one byte after a section
                    (i.e. addr = segment_base + segment_size) to be inside that section. *)
                 else Nat_big_num.less (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf32_segment_base chunk.elf32_segment_size))
            ) img2)
          in
            (match chunks2 with
              | []    -> return (symbol, (typ, size2, addr, None, bind1))
              | [(x, _)]   ->
                let rebase   = (Nat_big_num.sub_nat addr x.elf32_segment_base) in bind (Byte_sequence.offset_and_cut rebase size2 x.elf32_segment_body) (fun relevant ->
                  return (symbol, (typ, size2, addr, Some relevant, bind1)))
              | x::xs -> fail "get_elf32_global_symbol_init: invariant failed, global variable appears in multiple segments"
            ))
        else
          return (symbol, (typ, size2, addr, None, bind1))) strs)
      in
        mapped))))
  else
    fail "get_elf32_file_global_symbol_init: not an executable ELF file")

(** [get_elf64_file_global_symbol_init f1] extracts the global symbol init info
  * for ELF file [f1].  May fail.
  *)
(*val get_elf64_file_global_symbol_init : elf64_file -> error global_symbol_init_info*)
let get_elf64_file_global_symbol_init f3:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*(Byte_sequence_wrapper.byte_sequence)option*Nat_big_num.num))list)error=
   (if is_elf64_executable_file f3.elf64_file_header then
    let segs   = (f3.elf64_file_interpreted_segments) in bind (bytes_of_elf64_file f3) (fun bs0 -> bind (get_elf64_file_symbol_table f3) (fun (symtab,strtab) -> bind (
(* PS HACK: make this more like harness_interface.lem harness_string_of_elf64_syms' *)

(* WAS *)
(*    get_elf64_file_symbol_string_table f3 >>= fun strtab ->*)Elf_symbol_table.get_elf64_symbol_image_address symtab strtab) (fun strs ->
      let mapped = (mapM (fun (symbol, (typ, size2, addr, bind1)) ->
        if Nat_big_num.equal typ Elf_symbol_table.stt_object then bind (get_elf64_executable_image f3) (fun (img2, entry, mach) ->
          let chunks2 =
            (List.filter (fun (chunk, _) -> Nat_big_num.greater_equal
              addr chunk.elf64_segment_base &&
                (if Nat_big_num.greater size2( (Nat_big_num.of_int 0))
                 then Nat_big_num.less_equal (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf64_segment_base chunk.elf64_segment_size)
                 (* We don't consider a zero-size symbol one byte after a section
                    (i.e. addr = segment_base + segment_size) to be inside that section. *)
                 else Nat_big_num.less (Nat_big_num.add addr size2) (Nat_big_num.add chunk.elf64_segment_base chunk.elf64_segment_size))
            ) img2)
          in
            (match chunks2 with
              | []    -> return (symbol, (typ, size2, addr, None, bind1))
              | [(x, _)]   ->
                let rebase   = (Nat_big_num.sub_nat addr x.elf64_segment_base) in bind (Byte_sequence.offset_and_cut rebase size2 x.elf64_segment_body) (fun relevant ->
                  return (symbol, (typ, size2, addr, Some relevant, bind1)))
              | x::xs -> fail "get_elf64_global_symbol_init: invariant failed, global variable appears in multiple segments"
            ))
        else
          return (symbol, (typ, size2, addr, None, bind1))) strs)
      in
        mapped)))
  else
    fail "get_elf64_global_symbol_init: not an executable ELF file")

(** [string_of_elf32_file hdr_bdl pht_bdl sht_bdl f1] produces a string-based
  * representation of ELF file [f1] using ABI-specific print bundles [hdr_bdl],
  * [pht_bdl] and [sht_bdl].
  *)
(*val string_of_elf32_file : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_file -> string*)
let string_of_elf32_file hdr_bdl pht_bdl sht_bdl f3:string=
   ((match get_elf32_file_section_header_string_table f3 with
    | Fail err ->
      unlines [
        "\nError obtaining ELF section header string table:"
      ; err
      ]
    | Success strtab ->
      unlines [
        "\n*Type elf32_file:"
      ; "**Header:"
      ; string_of_elf32_header hdr_bdl f3.elf32_file_header
      ; "**Program header table:"
      ; string_of_elf32_program_header_table pht_bdl f3.elf32_file_program_header_table
      ; "**Section header table:"
      ; string_of_elf32_section_header_table' sht_bdl strtab f3.elf32_file_section_header_table
      ; "**Bits and bobs (unused junk space):"
      ; string_of_list 
  (instance_Show_Show_tup2_dict instance_Show_Show_Num_natural_dict
     Byte_sequence_impl.instance_Show_Show_Byte_sequence_impl_byte_sequence_dict) f3.elf32_file_bits_and_bobs
      ]
  ))

(** [string_of_elf64_file hdr_bdl pht_bdl sht_bdl f1] produces a string-based
  * representation of ELF file [f1] using ABI-specific print bundles [hdr_bdl],
  * [pht_bdl] and [sht_bdl].
  *)
(*val string_of_elf64_file : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_file -> string*)
let string_of_elf64_file hdr_bdl pht_bdl sht_bdl f3:string=
   ((match get_elf64_file_section_header_string_table f3 with
    | Fail err ->
      unlines [
        "\nError obtaining ELF section header string table:"
      ; err
      ]
    | Success strtab ->
      unlines [
        "\n*Type elf64_file:"
      ; "**Header:"
      ; string_of_elf64_header hdr_bdl f3.elf64_file_header
      ; "**Program header table:"
      ; string_of_elf64_program_header_table pht_bdl f3.elf64_file_program_header_table
      ; "**Section header table:"
      ; string_of_elf64_section_header_table' sht_bdl strtab f3.elf64_file_section_header_table
      ; "**Bits and bobs (unused junk space):"
      ; string_of_list 
  (instance_Show_Show_tup2_dict instance_Show_Show_Num_natural_dict
     Byte_sequence_impl.instance_Show_Show_Byte_sequence_impl_byte_sequence_dict) f3.elf64_file_bits_and_bobs
      ]
  ))

(** [flag_is_set flag v] checks whether flag [flag] is set in [v].
  * TODO: move elsewhere.  Check whether this is still being used.
  *)
(*val flag_is_set : natural -> natural -> bool*)
let flag_is_set flag v:bool=
     (
    (* HACK: convert to elf64_xword first. Flags never live
     * in objects bigger than 64 bits. *)Uint64_wrapper.logand
            (Uint64_wrapper.of_bigint v)
            (Uint64_wrapper.of_bigint flag)
    = (Uint64_wrapper.of_bigint flag))