Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 1198 deletions

diff --git a/lib/ocaml_rts/linksem/elf_file.ml b/lib/ocaml_rts/linksem/elf_file.ml
deleted file mode 100644
index fda353f8..00000000
--- a/lib/ocaml_rts/linksem/elf_file.ml
+++ /dev/null
@@ -1,1198 +0,0 @@
-(*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_sequence) 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)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     = (Nat_big_num.of_string (Uint32.to_string ef.elf32_file_header.elf32_phoff)) in
-  let sht_off     = (Nat_big_num.of_string (Uint32.to_string 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) ->
-          (Nat_big_num.of_string (Uint32.to_string seg.elf32_p_offset), interp_seg.elf32_segment_body)
-        ) (List.filter (fun (x, _) -> not (x.elf32_p_filesz = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))))) segs_zip))
-      in
-      let sects_layout =        
-(Lem_list.map (fun (sect, interp_sect) ->
-          (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset), interp_sect.elf32_section_body)
-        ) (List.filter (fun (x, _) -> not (x.elf32_sh_type = (Uint32.of_string (Nat_big_num.to_string 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
-                  Byte_sequence.partition0 diff body >>= (fun (_, cut) ->
-                  let concat3 = (Byte_sequence.concat0 [so_far; cut]) in
-                  let delta  = (Nat_big_num.add current_offset (Byte_sequence.length0 cut)) in
-                    return (delta, concat3))
-            else
-              let diff   = (Nat_big_num.sub_nat point_to_add current_offset) in
-              let reps   = (Byte_sequence.create diff '\000') in
-              let concat3 = (Byte_sequence.concat0 [so_far; reps; body]) in
-              let delta  = (Nat_big_num.add point_to_add (Byte_sequence.length0 body)) in
-                return (delta, concat3)
-        ) (Nat_big_num.of_int 0, Byte_sequence.empty) final_layout)
-      in
-        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_sequence) 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)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     = (Nat_big_num.of_string (Uint64.to_string ef.elf64_file_header.elf64_phoff)) in
-  let sht_off     = (Nat_big_num.of_string (Uint64.to_string 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) ->
-          (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset), interp_sect.elf64_section_body)
-        ) (List.filter (fun (x, _) -> not (x.elf64_sh_type = (Uint32.of_string (Nat_big_num.to_string 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
-                  Byte_sequence.partition0 diff body >>= (fun (_, cut) ->
-                  let concat3 = (Byte_sequence.concat0 [so_far; cut]) in
-                  let delta  = (Nat_big_num.add current_offset (Byte_sequence.length0 cut)) in
-                    return (delta, concat3))
-            else
-              let diff   = (Nat_big_num.sub_nat point_to_add current_offset) in
-              let reps   = (Byte_sequence.create diff '\000') in
-              let concat3 = (Byte_sequence.concat0 [so_far; reps; body]) in
-              let delta  = (Nat_big_num.add point_to_add (Byte_sequence.length0 body)) in
-                return (delta, concat3)
-        ) (Nat_big_num.of_int 0, Byte_sequence.empty) final_layout)
-      in
-        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    = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phnum))     in
-  let pentry_size = (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phoff)) in
-      Byte_sequence.offset_and_cut poffset psize bs0 >>= (fun pexact ->
-      (* 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    = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phnum))     in
-  let pentry_size = (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_phoff)) in
-      Byte_sequence.offset_and_cut poffset psize bs0 >>= (fun pexact ->
-      (* 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    = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shnum)) in
-  let sentry_size = (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shoff)) in
-      Byte_sequence.offset_and_cut soffset ssize bs0 >>= (fun sexact ->
-      (* 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    = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shnum)) in
-  let sentry_size = (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_shoff)) in
-      Byte_sequence.offset_and_cut soffset ssize bs0 >>= (fun sexact ->
-      (* 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 (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) shn_undef then
-    return None
-  else
-    (match Ml_bindings.list_index_big_int (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) sht with 
-      None -> fail "no section header string table"
-      | Some x -> return x
-    ) >>= (fun sh ->
-    Byte_sequence.offset_and_cut (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_offset)) (Nat_big_num.of_string (Uint32.to_string 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 (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) shn_undef then
-    return None
-  else
-    (match Ml_bindings.list_index_big_int (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) sht with 
-      None -> fail "no section header string table"
-      | Some x -> return x
-    ) >>= (fun sh ->
-    Byte_sequence.offset_and_cut (Nat_big_num.of_string (Uint64.to_string 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   = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_offset))  in
-    let size2     = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_filesz)) in
-      (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    = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_vaddr)) in
-    let paddr    = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_paddr)) in
-    let memsz    = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_memsz)) in
-    let typ      = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_type))  in
-    let align    = (Nat_big_num.of_string (Uint32.to_string ph.elf32_p_align)) in
-    let flags    = (elf32_interpret_program_header_flags 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   = (Nat_big_num.of_string (Uint64.to_string ph.elf64_p_offset))  in
-    let size2     = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_filesz) in
-      (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      = (Nat_big_num.of_string (Uint32.to_string ph.elf64_p_type))  in
-    let align    = (Ml_bindings.nat_big_num_of_uint64 ph.elf64_p_align) in
-    let flags    = (elf64_interpret_program_header_flags ph.elf64_p_flags) in
-      if Nat_big_num.less memsz size2 then
-        fail "obtain_elf64_interpreted_segments: memory size of segment cannot be less than file 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 = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_offset)) in
-    let size2   = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_size)) in
-    let name1   = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_name)) in
-    let typ    = (Nat_big_num.of_string (Uint32.to_string 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  = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_flags)) in
-    let base   = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_addr)) in
-    let link1   = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_link)) in
-    let info   = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_info)) in
-    let align  = (Nat_big_num.of_string (Uint32.to_string sh.elf32_sh_addralign)) in
-    let entry_size = (Nat_big_num.of_string (Uint32.to_string 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
-      (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 = (Nat_big_num.of_string (Uint64.to_string sh.elf64_sh_offset)) in
-    let size2   = (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) in
-    let name1   = (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_name)) in
-    let typ    = (Nat_big_num.of_string (Uint32.to_string 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   = (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_link)) in
-    let info   = (Nat_big_num.of_string (Uint32.to_string 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
-      (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
-            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)list)error=  
- (let hdr_off_len  = (Nat_big_num.of_int 0, Nat_big_num.of_string (Uint32.to_string hdr.elf32_ehsize)) in
-  let pht_off      = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phoff)) in
-  let pht_len      = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phentsize)) (Nat_big_num.of_string (Uint32.to_string hdr.elf32_phnum))) in
-  let pht_off_len  = (pht_off, Nat_big_num.add pht_off pht_len) in
-  let sht_off      = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shoff)) in
-  let sht_len      = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shentsize)) (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint32.to_string 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
-          compute_differences(Nat_big_num.of_int 0) (Byte_sequence.length0 bs0) layout >>= (fun diffs ->
-            mapM (fun (start, len) ->
-              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)list)error=  
- (let hdr_off_len  = (Nat_big_num.of_int 0, Nat_big_num.of_string (Uint32.to_string hdr.elf64_ehsize)) in
-  
-  let pht_off      = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_phoff)) in
-  let pht_len      = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phentsize)) (Nat_big_num.of_string (Uint32.to_string hdr.elf64_phnum))) in
-  let pht_off_len  = (pht_off, Nat_big_num.add pht_off pht_len) in
-  let sht_off      = (Nat_big_num.of_string (Uint64.to_string hdr.elf64_shoff)) in
-  let sht_len      = (Nat_big_num.mul (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shentsize)) (Nat_big_num.of_string (Uint32.to_string 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 = (Nat_big_num.of_string (Uint64.to_string 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 = (Nat_big_num.of_string (Uint64.to_string 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
-          compute_differences(Nat_big_num.of_int 0) (Byte_sequence.length0 bs0) layout >>= (fun diffs ->
-            mapM (fun (start, finish) ->
-              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=  
- (read_elf32_header bs0 >>= (fun (hdr, bs1) ->
-  obtain_elf32_program_header_table hdr bs0 >>= (fun pht  ->
-  obtain_elf32_section_header_table hdr bs0 >>= (fun sht  ->
-  obtain_elf32_section_header_string_table hdr sht bs0 >>= (fun shstrtab ->
-  obtain_elf32_interpreted_segments pht bs0 >>= (fun segs ->
-  obtain_elf32_interpreted_sections shstrtab sht bs0 >>= (fun sects ->
-  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=  
- (read_elf64_header bs0 >>= (fun (hdr, bs1) ->
-  obtain_elf64_program_header_table hdr bs0 >>= (fun pht  ->
-  obtain_elf64_section_header_table hdr bs0 >>= (fun sht  ->
-  obtain_elf64_section_header_string_table hdr sht bs0 >>= (fun shstrtab ->
-  obtain_elf64_interpreted_segments pht bs0 >>= (fun segs ->
-  obtain_elf64_interpreted_sections shstrtab sht bs0 >>= (fun sects ->
-  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  = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) in
-  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 = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset)) in
-          let size2   = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_size)) in
-          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  = (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) in
-  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 = (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset)) in
-          let size2   = (Ml_bindings.nat_big_num_of_uint64 sect.elf64_sh_size) in
-          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=    
- ((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 -> 
-    (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
-    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
-    (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=    
- ((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 -> 
-    (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
-    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
-    (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 (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_type)) sht_strtab then
-      if Nat_big_num.equal index (Nat_big_num.of_string (Uint32.to_string hdr.elf32_shstrndx)) then
-        None
-      else
-        Some sect
-    else
-      None) sht)
-  in
-    bytes_of_elf32_file f3 >>= (fun bs0 ->
-    mapM (fun sect ->
-      let offset  = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_offset)) in
-      let size2    = (Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_size)) in
-      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.concat1 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 (Nat_big_num.of_string (Uint32.to_string sect.elf64_sh_type)) sht_strtab then
-      if Nat_big_num.equal index (Nat_big_num.of_string (Uint32.to_string hdr.elf64_shstrndx)) then
-        None
-      else
-        Some sect
-    else
-      None) sht)
-  in
-    bytes_of_elf64_file f3 >>= (fun bs0 ->
-    mapM (fun sect ->
-      let offset  = (Nat_big_num.of_string (Uint64.to_string sect.elf64_sh_offset)) in
-      let size2    = (Ml_bindings.nat_big_num_of_uint64 sect.elf64_sh_size) in
-      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.concat1 strings)))
-
-(** [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    
-(Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_type)) sht_symtab
-    ) sht)
-  in
-    (match symtabs with
-      | [] -> return []
-      | [symtab] ->
-        let offset = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_offset)) in
-        let size2   = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_size)) in
-        bytes_of_elf32_file f3 >>= (fun bs0 ->
-        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*)
-let get_elf64_file_symbol_table f3:((elf64_symbol_table_entry)list)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    
-(Nat_big_num.of_string (Uint32.to_string sect.elf64_sh_type)) sht_symtab
-    ) sht)
-  in
-    (match symtabs with
-      | [] -> return []
-      | [symtab] ->
-        let offset = (Nat_big_num.of_string (Uint64.to_string symtab.elf64_sh_offset)) in
-        let size2   = (Ml_bindings.nat_big_num_of_uint64 symtab.elf64_sh_size) in
-        bytes_of_elf64_file f3 >>= (fun bs0 ->
-        Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun relevant ->
-        read_elf64_symbol_table endian relevant))
-      | _ ->
-        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    
-(Nat_big_num.of_string (Uint32.to_string sect.elf32_sh_type)) sht_dynsym
-    ) sht)
-  in
-    (match symtabs with
-      | [] -> return []
-      | [symtab] ->
-        let offset = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_offset)) in
-        let size2   = (Nat_big_num.of_string (Uint32.to_string symtab.elf32_sh_size)) in
-        bytes_of_elf32_file ef >>= (fun bs0 ->
-        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    
-(Nat_big_num.of_string (Uint32.to_string sect.elf64_sh_type)) sht_dynsym
-    ) sht)
-  in
-    (match symtabs with
-      | [] -> return []
-      | [symtab] ->
-        let offset = (Nat_big_num.of_string (Uint64.to_string symtab.elf64_sh_offset)) in
-        let size2   = (Ml_bindings.nat_big_num_of_uint64 symtab.elf64_sh_size) in
-        bytes_of_elf64_file ef >>= (fun bs0 ->
-        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 sym ->
-        read_elf32_symbol_table endian sym.elf32_section_body
-    ))
-    
-(** [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 sym -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym.elf32_section_body) Missing_pervasives.null_char)
-    ))
-    
-(** [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 sym ->
-        read_elf64_symbol_table endian sym.elf64_section_body
-    ))
-    
-(** [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 sym -> return (mk_string_table (Byte_sequence.string_of_byte_sequence sym.elf64_section_body) Missing_pervasives.null_char)
-    ))
-
-(** [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  ->
-            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, Nat_big_num.of_string (Uint32.to_string entr), Nat_big_num.of_string (Uint32.to_string 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  ->
-            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, Nat_big_num.of_string (Uint32.to_string 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_sequence 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)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
-    bytes_of_elf32_file f3 >>= (fun bs0 ->
-    get_elf32_file_symbol_table f3 >>= (fun symtab ->
-    get_elf32_file_symbol_string_table f3 >>= (fun strtab ->
-    Elf_symbol_table.get_elf32_symbol_image_address symtab strtab >>= (fun strs ->
-      let mapped = (mapM (fun (symbol, (typ, size2, addr, bind)) ->
-        if Nat_big_num.equal typ Elf_symbol_table.stt_object then
-          get_elf32_executable_image f3 >>= (fun (img2, entry, mach) ->
-          let chunks1 =            
-(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 chunks1 with
-              | []    -> fail "get_elf32_global_symbol_init: global variable not present in executable image"
-              | [(x, _)]   ->
-                let rebase   = (Nat_big_num.sub_nat addr x.elf32_segment_base) in
-                Byte_sequence.offset_and_cut rebase size2 x.elf32_segment_body >>= (fun relevant ->
-                  return (symbol, (typ, size2, addr, Some relevant, bind)))
-              | x::xs -> fail "get_elf32_global_symbol_init: invariant failed, global variable appears in multiple segments"
-            ))
-        else
-          return (symbol, (typ, size2, addr, None, bind))) 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)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
-    bytes_of_elf64_file f3 >>= (fun bs0 ->
-    get_elf64_file_symbol_table f3 >>= (fun symtab ->
-    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, bind)) ->
-        if Nat_big_num.equal typ Elf_symbol_table.stt_object then
-          get_elf64_executable_image f3 >>= (fun (img2, entry, mach) ->
-          let chunks1 =            
-(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 chunks1 with
-              | []    -> fail "get_elf64_global_symbol_init: global variable not present in executable image"
-              | [(x, _)]   ->
-                let rebase   = (Nat_big_num.sub_nat addr x.elf64_segment_base) in
-                Byte_sequence.offset_and_cut rebase size2 x.elf64_segment_body >>= (fun relevant ->
-                  return (symbol, (typ, size2, addr, Some relevant, bind)))
-              | x::xs -> fail "get_elf64_global_symbol_init: invariant failed, global variable appears in multiple segments"
-            ))
-        else
-          return (symbol, (typ, size2, addr, None, bind))) 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
-     instance_Show_Show_Byte_sequence_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
-     instance_Show_Show_Byte_sequence_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.logand 
-            (Uint64.of_string (Nat_big_num.to_string v)) 
-            (Uint64.of_string (Nat_big_num.to_string flag))
-    = (Uint64.of_string (Nat_big_num.to_string flag)))