Add ocaml run-time and updates to sail for ocaml backend

1 files changed, 1198 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/elf_file.ml b/lib/ocaml_rts/linksem/elf_file.ml
new file mode 100644
index 00000000..fda353f8
--- /dev/null
+++ b/lib/ocaml_rts/linksem/elf_file.ml
@@ -0,0 +1,1198 @@
+(*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)))