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

1 files changed, 1187 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/elf_section_header_table.ml b/lib/ocaml_rts/linksem/elf_section_header_table.ml
new file mode 100644
index 00000000..b750c103
--- /dev/null
+++ b/lib/ocaml_rts/linksem/elf_section_header_table.ml
@@ -0,0 +1,1187 @@
+(*Generated by Lem from elf_section_header_table.lem.*)
+(** [elf_section_header_table] provides types, functions and other definitions
+  * for working with section header tables and their entries.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_function
+open Lem_list
+open Lem_map
+open Lem_maybe
+open Lem_num
+open Lem_string
+
+open Byte_sequence
+open Error
+open Missing_pervasives
+open Show
+
+open Endianness
+open String_table
+
+open Elf_header
+open Elf_types_native_uint
+open Elf_program_header_table
+
+(** Special section indices. *)
+
+(** See elf_header.lem for shn_undef *)
+
+(** [shn_loreserve]: this specifies the lower bound of the range of reserved
+  * indices.
+  *)
+let shn_loreserve : Nat_big_num.num= (Nat_big_num.of_int 65280) (* 0xff00 *)
+(** [shn_loproc]: start of the range reserved for processor-specific semantics.
+  *)
+let shn_loproc : Nat_big_num.num= (Nat_big_num.of_int 65280) (* 0xff00 *)
+(** [shn_hiproc]: end of the range reserved for processor-specific semantics.
+  *)
+let shn_hiproc : Nat_big_num.num= (Nat_big_num.of_int 65311) (* 0xff1f *)
+(** [shn_loos]: start of the range reserved for operating system-specific
+  * semantics.
+  *)
+let shn_loos : Nat_big_num.num= (Nat_big_num.of_int 65312) (* 0xff20 *)
+(** [shn_hios]: end of the range reserved for operating system-specific
+  * semantics.
+  *)
+let shn_hios : Nat_big_num.num= (Nat_big_num.of_int 65343) (* 0xff3f *)
+(** [shn_abs]: specifies the absolute values for the corresponding reference.
+  * Symbols defined relative to section number [shn_abs] have absolute values
+  * and are not affected by relocation.
+  *)
+let shn_abs : Nat_big_num.num= (Nat_big_num.of_int 65521) (* 0xfff1 *)
+(** [shn_common]: symbols defined relative to this index are common symbols,
+  * such as unallocated C external variables.
+  *)
+let shn_common : Nat_big_num.num= (Nat_big_num.of_int 65522) (* 0xfff2 *)
+
+(** See elf_header.lem for shn_xindex. *)
+
+(** [shn_hireserve]: specifies the upper-bound of reserved values.
+  *)
+let shn_hireserve : Nat_big_num.num= (Nat_big_num.of_int 65535) (* 0xffff *)
+
+(** [string_of_special_section_index m] produces a string-based representation
+  * of a section header entry's special section index, [m].
+  *)
+(*val string_of_special_section_index : natural -> string*)
+let string_of_special_section_index i:string=  
+ (if Nat_big_num.equal i shn_undef then
+    "SHN_UNDEF"
+  else if Nat_big_num.equal i shn_loreserve then
+    "SHN_LORESERVE"
+  else if Nat_big_num.greater_equal i shn_loproc && Nat_big_num.less_equal i shn_hiproc then
+    "SHN_PROCESSOR_SPECIFIC"
+  else if Nat_big_num.greater_equal i shn_loos && Nat_big_num.less_equal i shn_hios then
+    "SHN_OS_SPECIFIC"
+  else if Nat_big_num.equal i shn_abs then
+    "SHN_ABS"
+  else if Nat_big_num.equal i shn_common then
+    "SHN_COMMON"
+  else if Nat_big_num.equal i shn_xindex then
+    "SHN_XINDEX"
+  else if Nat_big_num.equal i shn_hireserve then
+    "SHN_HIRESERVE"
+  else
+  	"SHN UNDEFINED")
+
+(** Section types. *)
+
+(** Marks the section header as being inactive. *)
+let sht_null : Nat_big_num.num= (Nat_big_num.of_int 0)
+(** Section holds information defined by the program. *)
+let sht_progbits : Nat_big_num.num= (Nat_big_num.of_int 1)
+(** The following two section types hold a symbol table.  An object file may only
+  * have one symbol table of each of the respective types.  The symtab provides
+  * a place for link editing, whereas the dynsym section holds a minimal set of
+  * dynamic linking symbols
+  *)
+let sht_symtab : Nat_big_num.num= (Nat_big_num.of_int 2)
+let sht_dynsym : Nat_big_num.num= (Nat_big_num.of_int 11)
+(** Section holds a string table *)
+let sht_strtab : Nat_big_num.num= (Nat_big_num.of_int 3)
+(** Section holds relocation entries with explicit addends.  An object file may
+  * have multiple section of this type.
+  *)
+let sht_rela : Nat_big_num.num= (Nat_big_num.of_int 4)
+(** Section holds a symbol hash table.  An object file may only have a single
+  * hash table.
+  *)
+let sht_hash : Nat_big_num.num= (Nat_big_num.of_int 5)
+(** Section holds information for dynamic linking.  An object file may only have
+  * a single dynamic section.
+  *)
+let sht_dynamic : Nat_big_num.num= (Nat_big_num.of_int 6)
+(** Section holds information that marks the file in some way. *)
+let sht_note : Nat_big_num.num= (Nat_big_num.of_int 7)
+(** Section occupies no space in the file but otherwise resembles a progbits
+  * section.
+  *)
+let sht_nobits : Nat_big_num.num= (Nat_big_num.of_int 8)
+(** Section holds relocation entries without explicit addends.  An object file
+  * may have multiple section of this type.
+  *)
+let sht_rel : Nat_big_num.num= (Nat_big_num.of_int 9)
+(** Section type is reserved but has an unspecified meaning. *)
+let sht_shlib : Nat_big_num.num= (Nat_big_num.of_int 10)
+(** Section contains an array of pointers to initialisation functions.  Each
+  * pointer is taken as a parameterless function with a void return type.
+  *)
+let sht_init_array : Nat_big_num.num= (Nat_big_num.of_int 14)
+(** Section contains an array of pointers to termination functions.  Each
+  * pointer is taken as a parameterless function with a void return type.
+  *)
+let sht_fini_array : Nat_big_num.num= (Nat_big_num.of_int 15)
+(** Section contains an array of pointers to initialisation functions that are
+  * invoked before all other initialisation functions.  Each
+  * pointer is taken as a parameterless function with a void return type.
+  *)
+let sht_preinit_array : Nat_big_num.num= (Nat_big_num.of_int 16)
+(** Section defines a section group, i.e. a set of sections that are related and
+  * must be treated especially by the linker.  May only appear in relocatable
+  * objects.
+  *)
+let sht_group : Nat_big_num.num= (Nat_big_num.of_int 17)
+(** Section is associated with sections of type SHT_SYMTAB and is required if
+  * any of the section header indices referenced by that symbol table contains
+  * the escape value SHN_XINDEX.
+  *
+  * FIXME: Lem bug as [int] type used throughout Lem codebase, rather than
+  * [BigInt.t], so Lem chokes on these large constants below, hence the weird
+  * way in which they are written.
+  *)
+let sht_symtab_shndx : Nat_big_num.num= (Nat_big_num.of_int 18)
+
+(** The following ranges are reserved solely for OS-, processor- and user-
+  * specific semantics, respectively.
+  *)
+let sht_loos   : Nat_big_num.num=  (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul(Nat_big_num.of_int 3)(Nat_big_num.of_int 1024))(Nat_big_num.of_int 1024))(Nat_big_num.of_int 512)) (* 1610612736 (* 0x60000000 *) *)
+let sht_hios   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 469762047)(Nat_big_num.of_int 4))(Nat_big_num.of_int 3)) (* 1879048191 (* 0x6fffffff *) *)
+let sht_loproc : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 469762048)(Nat_big_num.of_int 4)) (* 1879048192 (* 0x70000000 *) *)
+let sht_hiproc : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 536870911)(Nat_big_num.of_int 4))(Nat_big_num.of_int 3)) (* 2147483647 (* 0x7fffffff *) *)
+let sht_louser : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 536870912)(Nat_big_num.of_int 4)) (* 2147483648 (* 0x80000000 *) *)
+let sht_hiuser : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 603979775)(Nat_big_num.of_int 4))(Nat_big_num.of_int 3)) (* 2415919103 (* 0x8fffffff *) *)
+
+(** [string_of_section_type os proc user i] produces a string-based representation
+  * of section type [i].  Some section types are defined by ABI-specific supplements
+  * in reserved ranges, in which case the functions [os], [proc] and [user] are
+  * used to produce the string.
+  *)
+(*val string_of_section_type : (natural -> string) -> (natural -> string) ->
+  (natural -> string) -> natural -> string*)
+let string_of_section_type os proc user i:string=  
+ (if Nat_big_num.equal i sht_null then
+    "NULL"
+  else if Nat_big_num.equal i sht_progbits then
+    "PROGBITS"
+  else if Nat_big_num.equal i sht_symtab then
+    "SYMTAB"
+  else if Nat_big_num.equal i sht_strtab then
+    "STRTAB"
+  else if Nat_big_num.equal i sht_rela then
+    "RELA"
+  else if Nat_big_num.equal i sht_hash then
+    "HASH"
+  else if Nat_big_num.equal i sht_dynamic then
+    "DYNAMIC"
+  else if Nat_big_num.equal i sht_note then
+    "NOTE"
+  else if Nat_big_num.equal i sht_nobits then
+    "NOBITS"
+  else if Nat_big_num.equal i sht_rel then
+    "REL"
+  else if Nat_big_num.equal i sht_shlib then
+    "SHLIB"
+  else if Nat_big_num.equal i sht_dynsym then
+    "DYNSYM"
+  else if Nat_big_num.equal i sht_init_array then
+    "INIT_ARRAY"
+  else if Nat_big_num.equal i sht_fini_array then
+    "FINI_ARRAY"
+  else if Nat_big_num.equal i sht_preinit_array then
+    "PREINIT_ARRAY"
+  else if Nat_big_num.equal i sht_group then
+    "GROUP"
+  else if Nat_big_num.equal i sht_symtab_shndx then
+    "SYMTAB_SHNDX"
+  else if Nat_big_num.greater_equal i sht_loos && Nat_big_num.less_equal i sht_hios then
+    os i 
+  else if Nat_big_num.greater_equal i sht_loproc && Nat_big_num.less_equal i sht_hiproc then
+    proc i
+  else if Nat_big_num.greater_equal i sht_louser && Nat_big_num.less_equal i sht_hiuser then
+    user i
+  else
+    "Undefined or invalid section type")
+
+(** Section flag numeric values. *)
+
+(** The section contains data that should be writable during program execution.
+  *)
+let shf_write            : Nat_big_num.num= (Nat_big_num.of_int 1)
+(** The section occupies memory during program execution.
+  *)
+let shf_alloc            : Nat_big_num.num= (Nat_big_num.of_int 2)
+(** The section contains executable instructions.
+  *)
+let shf_execinstr        : Nat_big_num.num= (Nat_big_num.of_int 4)
+(** The data in the section may be merged to reduce duplication.  Each section
+  * is compared based on name, type and flags set with sections with identical
+  * values at run time being mergeable.
+  *)
+let shf_merge            : Nat_big_num.num= (Nat_big_num.of_int 16)
+(** The section contains null-terminated character strings.
+  *)
+let shf_strings          : Nat_big_num.num= (Nat_big_num.of_int 32)
+(** The [info] field of this section header contains a section header table
+  * index.
+  *)
+let shf_info_link        : Nat_big_num.num= (Nat_big_num.of_int 64)
+(** Adds special link ordering for link editors.
+  *)
+let shf_link_order       : Nat_big_num.num= (Nat_big_num.of_int 128)
+(** This section requires special OS-specific processing beyond the standard
+  * link rules.
+  *)
+let shf_os_nonconforming : Nat_big_num.num= (Nat_big_num.of_int 256)
+(** This section is a member (potentially the only member) of a link group.
+  *)
+let shf_group            : Nat_big_num.num= (Nat_big_num.of_int 512)
+(** This section contains Thread Local Storage (TLS) meaning that each thread of
+  * execution has its own instance of this data.
+  *)
+let shf_tls              : Nat_big_num.num= (Nat_big_num.of_int 1024)
+(** This section contains compressed data.  Compressed data may not be marked as
+  * allocatable.
+  *)
+let shf_compressed       : Nat_big_num.num= (Nat_big_num.of_int 2048)
+(** All bits included in these masks are reserved for OS and processor specific
+  * semantics respectively.
+  *)
+let shf_mask_os          : Nat_big_num.num= (Nat_big_num.of_int 267386880)      (* 0x0ff00000 *)
+let shf_mask_proc        : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 1006632960)) (* 0xf0000000 *)
+
+(** [string_of_section_flags os proc f] produces a string based representation
+  * of section flag [f].  Some section flags are defined by the ABI and are in
+  * reserved ranges, in which case the flag string is produced by functions
+  * [os] and [proc].
+  * TODO: add more as validation tests require them.
+  *)
+(*val string_of_section_flags : (natural -> string) -> (natural -> string) ->
+  natural -> string*)
+let string_of_section_flags os proc f:string=  
+ (if Nat_big_num.equal f shf_write then
+    "W"
+  else if Nat_big_num.equal f shf_alloc then
+    "  A"
+  else if Nat_big_num.equal f shf_execinstr then
+    "  X"
+  else if Nat_big_num.equal f (Nat_big_num.add shf_alloc shf_execinstr) then
+    " AX"
+  else if Nat_big_num.equal f (Nat_big_num.add shf_write shf_alloc) then
+    " WA"
+  else if Nat_big_num.equal f shf_merge then
+    " M "
+  else if Nat_big_num.equal f (Nat_big_num.add shf_merge shf_alloc) then
+    " AM"
+  else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_merge shf_alloc) shf_strings) then
+    "AMS"
+  else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_alloc shf_execinstr) shf_group) then
+    "AXG"
+  else if Nat_big_num.equal f shf_strings then
+    "  S"
+  else if Nat_big_num.equal f (Nat_big_num.add shf_merge shf_strings) then
+    " MS"
+  else if Nat_big_num.equal f shf_tls then
+    "  T"
+  else if Nat_big_num.equal f (Nat_big_num.add shf_tls shf_alloc) then
+    " AT"
+  else if Nat_big_num.equal f (Nat_big_num.add (Nat_big_num.add shf_write shf_alloc) shf_tls) then
+    "WAT"
+  else if Nat_big_num.equal f shf_info_link then
+    "  I"
+  else if Nat_big_num.equal f (Nat_big_num.add shf_alloc shf_info_link) then
+    " AI"
+  else
+    "   ")
+
+(** Section compression. *)
+
+(** Type [elf32_compression_header] provides information about the compression and
+  * decompression of compressed sections.  All compressed sections on ELF32 begin
+  * with an [elf32_compression_header] entry.
+  *)
+type elf32_compression_header =
+  { elf32_chdr_type      : Uint32.uint32  (** Specifies the compression algorithm *)
+   ; elf32_chdr_size      : Uint32.uint32  (** Size in bytes of the uncompressed data *)
+   ; elf32_chdr_addralign : Uint32.uint32  (** Specifies the required alignment of the uncompressed data *)
+   }
+
+(** Type [elf64_compression_header] provides information about the compression and
+  * decompression of compressed sections.  All compressed sections on ELF64 begin
+  * with an [elf64_compression_header] entry.
+  *)   
+type elf64_compression_header =
+  { elf64_chdr_type      : Uint32.uint32  (** Specified the compression algorithm *)
+   ; elf64_chdr_reserved  : Uint32.uint32  (** Reserved. *)
+   ; elf64_chdr_size      : Uint64.uint64 (** Size in bytes of the uncompressed data *)
+   ; elf64_chdr_addralign : Uint64.uint64 (** Specifies the required alignment of the uncompressed data *)
+   }
+
+(** This section is compressed with the ZLIB algorithm.  The compressed data begins
+  * at the first byte immediately following the end of the compression header.
+  *)   
+let elfcompress_zlib   : Nat_big_num.num= (Nat_big_num.of_int 1)
+
+(** Values in these ranges are reserved for OS-specific semantics.
+  *)
+let elfcompress_loos   : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 402653184))       (* 0x60000000 *)
+let elfcompress_hios   : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524095))(Nat_big_num.of_int 1)) (* 0x6fffffff *)
+
+(** Values in these ranges are reserved for processor-specific semantics.
+  *)
+let elfcompress_loproc : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 469762048))        (* 0x70000000 *)
+let elfcompress_hiproc : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 1073741823))(Nat_big_num.of_int 1)) (* 0x7fffffff *)
+
+(** [read_elf32_compression_header ed bs0] reads an [elf32_compression_header]
+  * entry from byte sequence [bs0], interpreting [bs0] with endianness [ed].
+  * Also returns the suffix of [bs0] after reading in the compression header.
+  * Fails if the header cannot be read.
+  *)
+(*val read_elf32_compression_header : endianness -> byte_sequence ->
+  error (elf32_compression_header * byte_sequence)*)
+let read_elf32_compression_header ed bs0:(elf32_compression_header*byte_sequence)error=  
+ (read_elf32_word ed bs0 >>= (fun (typ, bs1) ->
+  read_elf32_word ed bs1 >>= (fun (siz, bs2) ->
+  read_elf32_word ed bs2 >>= (fun (ali, bs3) ->
+  return ({ elf32_chdr_type = typ; elf32_chdr_size = siz;
+    elf32_chdr_addralign = ali }, bs3)))))
+
+(** [read_elf64_compression_header ed bs0] reads an [elf64_compression_header]
+  * entry from byte sequence [bs0], interpreting [bs0] with endianness [ed].
+  * Also returns the suffix of [bs0] after reading in the compression header.
+  * Fails if the header cannot be read.
+  *)
+(*val read_elf64_compression_header : endianness -> byte_sequence ->
+  error (elf64_compression_header * byte_sequence)*)
+let read_elf64_compression_header ed bs0:(elf64_compression_header*byte_sequence)error=  
+ (read_elf64_word ed bs0  >>= (fun (typ, bs1) ->
+  read_elf64_word ed bs1  >>= (fun (res, bs2) ->
+  read_elf64_xword ed bs2 >>= (fun (siz, bs3) ->
+  read_elf64_xword ed bs3 >>= (fun (ali, bs4) ->
+  return ({ elf64_chdr_type = typ; elf64_chdr_reserved = res;
+    elf64_chdr_size = siz; elf64_chdr_addralign = ali }, bs4))))))
+
+(** Section header table entry type. *)
+
+(** [elf32_section_header_table_entry] is the type of entries in the section
+  * header table in 32-bit ELF files.  Each entry in the table details a section
+  * in the body of the ELF file.
+  *) 
+type elf32_section_header_table_entry =
+  { elf32_sh_name      : Uint32.uint32 (** Name of the section *)
+   ; elf32_sh_type      : Uint32.uint32 (** Type of the section and its semantics *)
+   ; elf32_sh_flags     : Uint32.uint32 (** Flags associated with the section *)
+   ; elf32_sh_addr      : Uint32.uint32 (** Address of first byte of section in memory image *)
+   ; elf32_sh_offset    : Uint32.uint32  (** Offset from beginning of file of first byte of section *)
+   ; elf32_sh_size      : Uint32.uint32 (** Section size in bytes *)
+   ; elf32_sh_link      : Uint32.uint32 (** Section header table index link *)
+   ; elf32_sh_info      : Uint32.uint32 (** Extra information, contents depends on type of section *)
+   ; elf32_sh_addralign : Uint32.uint32 (** Alignment constraints for section *)
+   ; elf32_sh_entsize   : Uint32.uint32 (** Size of each entry in table, if section is one *)
+   }
+   
+let elf32_null_section_header:elf32_section_header_table_entry=  
+ ({ elf32_sh_name      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_type      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_flags     = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_addr      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_offset    = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) 
+   ; elf32_sh_size      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_link      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_info      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_addralign = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf32_sh_entsize   = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   })
+   
+(** [compare_elf32_section_header_table_entry ent1 ent2] is an ordering comparison
+  * function on section header table entries suitable for use in constructing
+  * sets, finite maps and other ordered data types.
+  *)
+(*val compare_elf32_section_header_table_entry : elf32_section_header_table_entry ->
+  elf32_section_header_table_entry -> ordering*)
+let compare_elf32_section_header_table_entry h1 h2:int=    
+ (lexicographic_compare Nat_big_num.compare 
+    [Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_name);
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_type); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_flags);
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_addr); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_offset);
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_size); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_link); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_info); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_addralign); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf32_sh_entsize)]
+    [Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_name);
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_type); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_flags);
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_addr); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_offset);
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_size); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_link); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_info); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_addralign); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf32_sh_entsize)])
+
+let instance_Basic_classes_Ord_Elf_section_header_table_elf32_section_header_table_entry_dict:(elf32_section_header_table_entry)ord_class= ({
+
+  compare_method = compare_elf32_section_header_table_entry;
+
+  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_section_header_table_entry f1 f2) (-1))));
+
+  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_section_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0])));
+
+  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf32_section_header_table_entry f1 f2) 1)));
+
+  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_section_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))})
+
+(** [elf64_section_header_table_entry] is the type of entries in the section
+  * header table in 64-bit ELF files.  Each entry in the table details a section
+  * in the body of the ELF file.
+  *) 
+type elf64_section_header_table_entry =
+  { elf64_sh_name      : Uint32.uint32  (** Name of the section *)
+   ; elf64_sh_type      : Uint32.uint32  (** Type of the section and its semantics *)
+   ; elf64_sh_flags     : Uint64.uint64 (** Flags associated with the section *)
+   ; elf64_sh_addr      : Uint64.uint64  (** Address of first byte of section in memory image *)
+   ; elf64_sh_offset    : Uint64.uint64   (** Offset from beginning of file of first byte of section *)
+   ; elf64_sh_size      : Uint64.uint64 (** Section size in bytes *)
+   ; elf64_sh_link      : Uint32.uint32  (** Section header table index link *)
+   ; elf64_sh_info      : Uint32.uint32  (** Extra information, contents depends on type of section *)
+   ; elf64_sh_addralign : Uint64.uint64 (** Alignment constraints for section *)
+   ; elf64_sh_entsize   : Uint64.uint64 (** Size of each entry in table, if section is one *)
+   }
+   
+let elf64_null_section_header:elf64_section_header_table_entry=  
+ ({ elf64_sh_name      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) 
+   ; elf64_sh_type      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) 
+   ; elf64_sh_flags     = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf64_sh_addr      = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) 
+   ; elf64_sh_offset    = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))  
+   ; elf64_sh_size      = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf64_sh_link      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) 
+   ; elf64_sh_info      = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) 
+   ; elf64_sh_addralign = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   ; elf64_sh_entsize   = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))
+   })
+
+(** [compare_elf64_section_header_table_entry ent1 ent2] is an ordering comparison
+  * function on section header table entries suitable for use in constructing
+  * sets, finite maps and other ordered data types.
+  *)
+(*val compare_elf64_section_header_table_entry : elf64_section_header_table_entry ->
+  elf64_section_header_table_entry -> ordering*)
+let compare_elf64_section_header_table_entry h1 h2:int=    
+ (lexicographic_compare Nat_big_num.compare 
+    [Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_name);
+    Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_type); 
+    Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_flags;
+    Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_addr; 
+    Nat_big_num.of_string (Uint64.to_string h1.elf64_sh_offset);
+    Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_size; 
+    Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_link); 
+    Nat_big_num.of_string (Uint32.to_string h1.elf64_sh_info); 
+    Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_addralign; 
+    Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_entsize]
+    [Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_name);
+    Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_type); 
+    Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_flags;
+    Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_addr; 
+    Nat_big_num.of_string (Uint64.to_string h2.elf64_sh_offset);
+    Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_size; 
+    Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_link); 
+    Nat_big_num.of_string (Uint32.to_string h2.elf64_sh_info); 
+    Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_addralign; 
+    Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_entsize])
+
+let instance_Basic_classes_Ord_Elf_section_header_table_elf64_section_header_table_entry_dict:(elf64_section_header_table_entry)ord_class= ({
+
+  compare_method = compare_elf64_section_header_table_entry;
+
+  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_section_header_table_entry f1 f2) (-1))));
+
+  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_section_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0])));
+
+  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_section_header_table_entry f1 f2) 1)));
+
+  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_section_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))})
+
+(** Section header table type *)
+
+(** Type [elf32_section_header_table] represents a section header table for 32-bit
+  * ELF files.  A section header table is an array (implemented as a list, here)
+  * of section header table entries.
+  *)
+type elf32_section_header_table = elf32_section_header_table_entry
+  list
+
+(** Type [elf64_section_header_table] represents a section header table for 64-bit
+  * ELF files.  A section header table is an array (implemented as a list, here)
+  * of section header table entries.
+  *)
+type elf64_section_header_table = elf64_section_header_table_entry
+  list
+
+(** Parsing and blitting *)
+
+(** [bytes_of_elf32_section_header_table_entry ed ent] blits [ent] to a byte sequence
+  * assuming endianness [ed].
+  *)
+(*val bytes_of_elf32_section_header_table_entry : endianness ->
+  elf32_section_header_table_entry -> byte_sequence*)
+let bytes_of_elf32_section_header_table_entry endian entry:byte_sequence=  
+ (Byte_sequence.from_byte_lists [
+    bytes_of_elf32_word endian entry.elf32_sh_name
+  ; bytes_of_elf32_word endian entry.elf32_sh_type
+  ; bytes_of_elf32_word endian entry.elf32_sh_flags
+  ; bytes_of_elf32_addr endian entry.elf32_sh_addr
+  ; bytes_of_elf32_off  endian entry.elf32_sh_offset
+  ; bytes_of_elf32_word endian entry.elf32_sh_size
+  ; bytes_of_elf32_word endian entry.elf32_sh_link
+  ; bytes_of_elf32_word endian entry.elf32_sh_info
+  ; bytes_of_elf32_word endian entry.elf32_sh_addralign
+  ; bytes_of_elf32_word endian entry.elf32_sh_entsize
+  ])
+
+(** [read_elf32_section_header_table_entry ed bs0] reads a section header table
+  * entry from [bs0] assuming endianness [ed].  Also returns the suffix of [bs0]
+  * after parsing.  Fails if the entry cannot be read.
+  *)
+(*val read_elf32_section_header_table_entry : endianness -> byte_sequence ->
+  error (elf32_section_header_table_entry * byte_sequence)*)
+let read_elf32_section_header_table_entry endian bs:(elf32_section_header_table_entry*byte_sequence)error=	
+ (read_elf32_word endian bs >>= (fun (sh_name, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_type, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_flags, bs) ->
+	read_elf32_addr endian bs >>= (fun (sh_addr, bs) ->
+	read_elf32_off  endian bs >>= (fun (sh_offset, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_size, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_link, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_info, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_addralign, bs) ->
+	read_elf32_word endian bs >>= (fun (sh_entsize, bs) ->
+		return ({ elf32_sh_name = sh_name; elf32_sh_type = sh_type;
+                elf32_sh_flags = sh_flags; elf32_sh_addr = sh_addr;
+                elf32_sh_offset = sh_offset; elf32_sh_size = sh_size;
+                elf32_sh_link = sh_link; elf32_sh_info = sh_info;
+                elf32_sh_addralign = sh_addralign; elf32_sh_entsize = sh_entsize }, bs))))))))))))
+
+(** [bytes_of_elf64_section_header_table_entry ed ent] blits [ent] to a byte sequence
+  * assuming endianness [ed].
+  *)
+(*val bytes_of_elf64_section_header_table_entry : endianness ->
+  elf64_section_header_table_entry -> byte_sequence*)
+let bytes_of_elf64_section_header_table_entry endian entry:byte_sequence=  
+ (Byte_sequence.from_byte_lists [
+    bytes_of_elf64_word  endian entry.elf64_sh_name
+  ; bytes_of_elf64_word  endian entry.elf64_sh_type
+  ; bytes_of_elf64_xword endian entry.elf64_sh_flags
+  ; bytes_of_elf64_addr  endian entry.elf64_sh_addr
+  ; bytes_of_elf64_off   endian entry.elf64_sh_offset
+  ; bytes_of_elf64_xword endian entry.elf64_sh_size
+  ; bytes_of_elf64_word  endian entry.elf64_sh_link
+  ; bytes_of_elf64_word  endian entry.elf64_sh_info
+  ; bytes_of_elf64_xword endian entry.elf64_sh_addralign
+  ; bytes_of_elf64_xword endian entry.elf64_sh_entsize
+  ])
+
+(** [read_elf64_section_header_table_entry ed bs0] reads a section header table
+  * entry from [bs0] assuming endianness [ed].  Also returns the suffix of [bs0]
+  * after parsing.  Fails if the entry cannot be read.
+  *)
+(*val read_elf64_section_header_table_entry : endianness -> byte_sequence ->
+  error (elf64_section_header_table_entry * byte_sequence)*)
+let read_elf64_section_header_table_entry endian bs:(elf64_section_header_table_entry*byte_sequence)error=  
+ (read_elf64_word endian bs  >>= (fun (sh_name, bs) ->
+  read_elf64_word endian bs  >>= (fun (sh_type, bs) ->
+  read_elf64_xword endian bs >>= (fun (sh_flags, bs) ->
+  read_elf64_addr endian bs  >>= (fun (sh_addr, bs) ->
+  read_elf64_off  endian bs  >>= (fun (sh_offset, bs) ->
+  read_elf64_xword endian bs >>= (fun (sh_size, bs) ->
+  read_elf64_word endian bs  >>= (fun (sh_link, bs) ->
+  read_elf64_word endian bs  >>= (fun (sh_info, bs) ->
+  read_elf64_xword endian bs >>= (fun (sh_addralign, bs) ->
+  read_elf64_xword endian bs >>= (fun (sh_entsize, bs) ->
+    return ({ elf64_sh_name = sh_name; elf64_sh_type = sh_type;
+                elf64_sh_flags = sh_flags; elf64_sh_addr = sh_addr;
+                elf64_sh_offset = sh_offset; elf64_sh_size = sh_size;
+                elf64_sh_link = sh_link; elf64_sh_info = sh_info;
+                elf64_sh_addralign = sh_addralign; elf64_sh_entsize = sh_entsize }, bs))))))))))))
+
+(** [bytes_of_elf32_section_header_table ed tbl] blits section header table [tbl]
+  * to a byte sequence assuming endianness [ed].
+  *)
+(*val bytes_of_elf32_section_header_table : endianness ->
+  elf32_section_header_table -> byte_sequence*)
+let bytes_of_elf32_section_header_table endian tbl:byte_sequence=  
+ (Byte_sequence.concat0 (Lem_list.map (bytes_of_elf32_section_header_table_entry endian) tbl))
+  
+(** [bytes_of_elf64_section_header_table ed tbl] blits section header table [tbl]
+  * to a byte sequence assuming endianness [ed].
+  *)
+(*val bytes_of_elf64_section_header_table : endianness ->
+  elf64_section_header_table -> byte_sequence*)
+let bytes_of_elf64_section_header_table endian tbl:byte_sequence=  
+ (Byte_sequence.concat0 (Lem_list.map (bytes_of_elf64_section_header_table_entry endian) tbl))
+
+(** [read_elf32_section_header_table' ed bs0] parses an ELF32 section header table
+  * from byte sequence [bs0] assuming endianness [ed].  Assumes [bs0] is of the
+  * exact length required to parse the entire table.
+  * Fails if any of the section header table entries cannot be parsed.
+  *)
+(*val read_elf32_section_header_table' : endianness -> byte_sequence ->
+  error elf32_section_header_table*)
+let rec read_elf32_section_header_table' endian bs0:((elf32_section_header_table_entry)list)error=  
+ (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then
+    return []
+  else
+    read_elf32_section_header_table_entry endian bs0 >>= (fun (entry, bs1) ->
+    read_elf32_section_header_table' endian bs1 >>= (fun tail ->
+    return (entry::tail))))
+    
+(** [read_elf64_section_header_table' ed bs0] parses an ELF64 section header table
+  * from byte sequence [bs0] assuming endianness [ed].  Assumes [bs0] is of the
+  * exact length required to parse the entire table.
+  * Fails if any of the section header table entries cannot be parsed.
+  *)
+(*val read_elf64_section_header_table' : endianness -> byte_sequence ->
+  error elf64_section_header_table*)
+let rec read_elf64_section_header_table' endian bs0:((elf64_section_header_table_entry)list)error=  
+ (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then
+    return []
+  else
+    read_elf64_section_header_table_entry endian bs0 >>= (fun (entry, bs1) ->
+    read_elf64_section_header_table' endian bs1 >>= (fun tail ->
+    return (entry::tail))))
+
+(** [read_elf32_section_header_table sz ed bs0] parses an ELF32 section header
+  * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness
+  * [ed].  The suffix of [bs0] remaining after parsing is also returned.
+  * Fails if any of the section header entries cannot be parsed or if [sz] is
+  * greater than the length of [bs0].
+  *)
+(*val read_elf32_section_header_table : natural -> endianness -> byte_sequence ->
+  error (elf32_section_header_table * byte_sequence)*)
+let read_elf32_section_header_table table_size endian bs0:((elf32_section_header_table_entry)list*byte_sequence)error=  
+ (partition0 table_size bs0 >>= (fun (eat, rest) ->
+  read_elf32_section_header_table' endian eat >>= (fun entries ->
+  return (entries, rest))))
+
+
+(** [read_elf64_section_header_table sz ed bs0] parses an ELF64 section header
+  * table from a [sz] sized prefix of byte sequence [bs0] assuming endianness
+  * [ed].  The suffix of [bs0] remaining after parsing is also returned.
+  * Fails if any of the section header entries cannot be parsed or if [sz] is
+  * greater than the length of [bs0].
+  *)
+(*val read_elf64_section_header_table : natural -> endianness -> byte_sequence ->
+  error (elf64_section_header_table * byte_sequence)*)
+let read_elf64_section_header_table table_size endian bs0:((elf64_section_header_table_entry)list*byte_sequence)error=  
+ (partition0 table_size bs0 >>= (fun (eat, rest) ->
+  read_elf64_section_header_table' endian eat >>= (fun entries ->
+  return (entries, rest))))
+
+
+(** Correctness criteria *)
+
+(** TODO: what is going on here? *)
+(*val elf32_size_correct : elf32_section_header_table_entry ->
+  elf32_section_header_table -> bool*)
+let elf32_size_correct hdr tbl:bool=  
+ (let m = (Nat_big_num.of_string (Uint32.to_string hdr.elf32_sh_size)) in
+    if Nat_big_num.equal m(Nat_big_num.of_int 0) then
+      true
+    else Nat_big_num.equal
+      m (Nat_big_num.of_int (List.length tbl)))
+
+
+(** TODO: what is going on here? *)
+(*val elf64_size_correct : elf64_section_header_table_entry ->
+  elf64_section_header_table -> bool*)
+let elf64_size_correct hdr tbl:bool=  
+ (let m = (Ml_bindings.nat_big_num_of_uint64 hdr.elf64_sh_size) in
+    if Nat_big_num.equal m(Nat_big_num.of_int 0) then
+      true
+    else Nat_big_num.equal
+      m (Nat_big_num.of_int (List.length tbl)))
+
+
+(** [is_elf32_addr_addralign_correct ent] checks whether an internal address
+  * alignment constraint is met on section header table [ent].
+  * TODO: needs tweaking to add in power-of-two constraint, too.
+  *)
+(*val is_elf32_addr_addralign_correct : elf32_section_header_table_entry -> bool*)
+let is_elf32_addr_addralign_correct ent:bool=  
+ (let align = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_addralign)) in
+  let addr  = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_addr)) in
+    if Nat_big_num.equal (Nat_big_num.modulus addr align)(Nat_big_num.of_int 0) then Nat_big_num.equal
+      align(Nat_big_num.of_int 0) || Nat_big_num.equal align(Nat_big_num.of_int 1) (* TODO: or a power of two *)
+    else
+      false)
+    
+(** [is_elf64_addr_addralign_correct ent] checks whether an internal address
+  * alignment constraint is met on section header table [ent].
+  * TODO: needs tweaking to add in power-of-two constraint, too.
+  *)
+(*val is_elf64_addr_addralign_correct : elf64_section_header_table_entry -> bool*)
+let is_elf64_addr_addralign_correct ent:bool=  
+ (let align = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_addralign) in
+  let addr  = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_addr) in
+    if Nat_big_num.equal (Nat_big_num.modulus addr align)(Nat_big_num.of_int 0) then Nat_big_num.equal
+      align(Nat_big_num.of_int 0) || Nat_big_num.equal align(Nat_big_num.of_int 1) (* TODO: or a power of two *)
+    else
+      false)
+
+(** [is_valid_elf32_section_header_table sht] checks whether all entries of
+  * section header table [sht] are valid.
+  *)
+(*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*)
+let is_valid_elf32_section_header_table tbl:bool=  
+ ((match tbl with
+    | []    -> true
+    | x::xs -> Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_type)) sht_null && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_flags))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_addr))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_info))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_addralign))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf32_sh_entsize))(Nat_big_num.of_int 0) &&
+        elf32_size_correct x tbl)))))))
+        (* XXX: more correctness criteria in time *)
+  ))
+  
+(** [is_valid_elf64_section_header_table sht] checks whether all entries of
+  * section header table [sht] are valid.
+  *)
+(*val is_valid_elf64_section_header_table : elf64_section_header_table -> bool*)
+let is_valid_elf64_section_header_table tbl:bool=  
+ ((match tbl with
+    | []    -> true
+    | x::xs -> Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf64_sh_type)) sht_null && (Nat_big_num.equal        
+(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_flags)(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_addr)(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Nat_big_num.of_string (Uint32.to_string x.elf64_sh_info))(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_addralign)(Nat_big_num.of_int 0) && (Nat_big_num.equal        
+(Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_entsize)(Nat_big_num.of_int 0) &&
+        elf64_size_correct x tbl)))))))
+        (* XXX: more correctness criteria in time *)
+  ))
+
+(** Pretty printing *)
+
+(** The [sht_print_bundle] type is used to tidy up other type signatures.  Some of the
+  * top-level string_of_ functions require six or more functions passed to them,
+  * which quickly gets out of hand.  This type is used to reduce that complexity.
+  * The first component of the type is an OS specific print function, the second is
+  * a processor specific print function.
+  *)
+type sht_print_bundle =
+  (Nat_big_num.num -> string) * (Nat_big_num.num -> string) * (Nat_big_num.num -> string)
+
+(** [string_of_elf32_section_header_table_entry sht ent] produces a string
+  * representation of section header table entry [ent] using [sht], a
+  * [sht_print_bundle].
+  * OCaml specific definition.
+  *)
+(*val string_of_elf32_section_header_table_entry : sht_print_bundle ->
+  elf32_section_header_table_entry -> string*)
+let string_of_elf32_section_header_table_entry (os, proc, user) entry:string=  
+ (unlines [    
+("\t" ^ ("Name: "    ^ Uint32.to_string entry.elf32_sh_name))
+  ; ("\t" ^ ("Type: "    ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf32_sh_type))))
+  ; ("\t" ^ ("Flags: "   ^ Uint32.to_string entry.elf32_sh_flags))
+  ; ("\t" ^ ("Address: " ^ Uint32.to_string entry.elf32_sh_addr))
+  ; ("\t" ^ ("Size: "    ^ Uint32.to_string entry.elf32_sh_size))
+  ])
+
+(** [string_of_elf64_section_header_table_entry sht ent] produces a string
+  * representation of section header table entry [ent] using [sht], a
+  * [sht_print_bundle].
+  * OCaml specific definition.
+  *)
+(*val string_of_elf64_section_header_table_entry : sht_print_bundle ->
+  elf64_section_header_table_entry -> string*)
+let string_of_elf64_section_header_table_entry (os, proc, user) entry:string=  
+ (unlines [    
+("\t" ^ ("Name: "    ^ Uint32.to_string entry.elf64_sh_name))
+  ; ("\t" ^ ("Type: "    ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf64_sh_type))))
+  ; ("\t" ^ ("Flags: "   ^ Uint64.to_string entry.elf64_sh_flags))
+  ; ("\t" ^ ("Address: " ^ Uint64.to_string entry.elf64_sh_addr))
+  ; ("\t" ^ ("Size: "    ^ Uint64.to_string entry.elf64_sh_size))
+  ])
+
+(** [string_of_elf32_section_header_table_entry' sht stab ent] produces a string
+  * representation of section header table entry [ent] using [sht] and section
+  * header string table [stab] to print the name of the section header entry
+  * correctly.
+  * OCaml specific definition.
+  *)
+(*val string_of_elf32_section_header_table_entry' : sht_print_bundle ->
+  string_table -> elf32_section_header_table_entry -> string*)
+let string_of_elf32_section_header_table_entry' (os, proc, user) stbl entry:string=  
+ (let name1 =    
+((match get_string_at (Nat_big_num.of_string (Uint32.to_string entry.elf32_sh_name)) stbl with
+      | Fail _ -> "Invalid index into string table"
+      | Success i -> i
+    ))
+  in
+    unlines [      
+("\t" ^ ("Name: "    ^ name1))
+    ; ("\t" ^ ("Type: "    ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf32_sh_type))))
+    ; ("\t" ^ ("Flags: "   ^ Uint32.to_string entry.elf32_sh_flags))
+    ; ("\t" ^ ("Address: " ^ Uint32.to_string entry.elf32_sh_addr))
+    ; ("\t" ^ ("Size: "    ^ Uint32.to_string entry.elf32_sh_size))
+    ])
+
+(** [string_of_elf64_section_header_table_entry' sht stab ent] produces a string
+  * representation of section header table entry [ent] using [sht] and section
+  * header string table [stab] to print the name of the section header entry
+  * correctly.
+  * OCaml specific definition.
+  *)
+(*val string_of_elf64_section_header_table_entry' : sht_print_bundle ->
+  string_table -> elf64_section_header_table_entry -> string*)
+let string_of_elf64_section_header_table_entry' (os, proc, user) stbl entry:string=  
+ (let name1 =    
+((match get_string_at (Nat_big_num.of_string (Uint32.to_string entry.elf64_sh_name)) stbl with
+      | Fail _ -> "Invalid index into string table"
+      | Success i -> i
+    ))
+  in
+    unlines [      
+("\t" ^ ("Name: "    ^ name1))
+    ; ("\t" ^ ("Type: "    ^ string_of_section_type os proc user (Nat_big_num.of_string (Uint32.to_string entry.elf64_sh_type))))
+    ; ("\t" ^ ("Flags: "   ^ Uint64.to_string entry.elf64_sh_flags))
+    ; ("\t" ^ ("Address: " ^ Uint64.to_string entry.elf64_sh_addr))
+    ; ("\t" ^ ("Size: "    ^ Uint64.to_string entry.elf64_sh_size))
+    ])
+
+(** The following defintions are default printing functions, with no ABI-specific
+  * functionality, in order to produce a [Show] instance for section header
+  * table entries.
+  *)
+  
+(*val string_of_elf32_section_header_table_entry_default : elf32_section_header_table_entry -> string*)
+let string_of_elf32_section_header_table_entry_default:elf32_section_header_table_entry ->string=  
+ (string_of_elf32_section_header_table_entry
+    (((fun y->"*Default OS specific print*")),
+      ((fun y->"*Default processor specific print*")),
+      ((fun y->"*Default user specific print*"))))
+
+let instance_Show_Show_Elf_section_header_table_elf32_section_header_table_entry_dict:(elf32_section_header_table_entry)show_class= ({
+
+  show_method = string_of_elf32_section_header_table_entry_default})
+
+(*val string_of_elf64_section_header_table_entry_default : elf64_section_header_table_entry -> string*)
+let string_of_elf64_section_header_table_entry_default:elf64_section_header_table_entry ->string=  
+ (string_of_elf64_section_header_table_entry
+    (((fun y->"*Default OS specific print*")),
+      ((fun y->"*Default processor specific print*")),
+      ((fun y->"*Default user specific print*"))))
+
+let instance_Show_Show_Elf_section_header_table_elf64_section_header_table_entry_dict:(elf64_section_header_table_entry)show_class= ({
+
+  show_method = string_of_elf64_section_header_table_entry_default})
+
+(*val string_of_elf32_section_header_table : sht_print_bundle ->
+  elf32_section_header_table -> string*)
+let string_of_elf32_section_header_table sht_bdl tbl:string=  
+ (unlines (Lem_list.map (string_of_elf32_section_header_table_entry sht_bdl) tbl))
+
+(*val string_of_elf32_section_header_table_default : elf32_section_header_table ->
+  string*)
+let string_of_elf32_section_header_table_default:elf32_section_header_table ->string=  
+ (string_of_elf32_section_header_table
+    (((fun y->"*Default OS specific print*")),
+      ((fun y->"*Default processor specific print*")),
+      ((fun y->"*Default user specific print*"))))
+
+(*val string_of_elf64_section_header_table : sht_print_bundle ->
+  elf64_section_header_table -> string*)
+let string_of_elf64_section_header_table sht_bdl tbl:string=  
+ (unlines (Lem_list.map (string_of_elf64_section_header_table_entry sht_bdl) tbl))
+  
+(*val string_of_elf64_section_header_table_default : elf64_section_header_table ->
+  string*)
+let string_of_elf64_section_header_table_default:elf64_section_header_table ->string=  
+ (string_of_elf64_section_header_table
+    (((fun y->"*Default OS specific print*")),
+      ((fun y->"*Default processor specific print*")),
+      ((fun y->"*Default user specific print*"))))
+
+(*val string_of_elf32_section_header_table' : sht_print_bundle -> string_table ->
+  elf32_section_header_table -> string*)
+let string_of_elf32_section_header_table' sht_bdl stbl tbl:string=  
+ (unlines (Lem_list.map (string_of_elf32_section_header_table_entry' sht_bdl stbl) tbl))
+
+(*val string_of_elf64_section_header_table' : sht_print_bundle -> string_table ->
+  elf64_section_header_table -> string*)
+let string_of_elf64_section_header_table' sht_bdl stbl tbl:string=  
+ (unlines (Lem_list.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl))
+  
+(** Section to segment mappings *)
+
+(** [elf32_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf:
+  *
+  * #define ELF_TBSS_SPECIAL(sec_hdr, segment)			\
+  *   (((sec_hdr)->sh_flags & SHF_TLS) != 0				\
+  *   && (sec_hdr)->sh_type == SHT_NOBITS				\
+  *   && (segment)->p_type != PT_TLS)
+  *
+  * From readelf source code, file [internal.h].
+  *
+  *)
+(*val is_elf32_tbss_special : elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool*)
+let is_elf32_tbss_special sec_hdr segment:bool=  (not ((Uint32.logand sec_hdr.elf32_sh_flags (Uint32.of_string (Nat_big_num.to_string shf_tls))) = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))) &&    
+(( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string sec_hdr.elf32_sh_type)) sht_nobits) &&
+    ( not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string segment.elf32_p_type)) elf_pt_tls))))
+    
+(** [elf64_tbss_special shdr seg] implements the ELF_TBSS_SPECIAL macro from readelf:
+  *
+  * #define ELF_TBSS_SPECIAL(sec_hdr, segment)			\
+  *   (((sec_hdr)->sh_flags & SHF_TLS) != 0				\
+  *   && (sec_hdr)->sh_type == SHT_NOBITS				\
+  *   && (segment)->p_type != PT_TLS)
+  *
+  * From readelf source code, file [internal.h].
+  *
+  *)
+(*val is_elf64_tbss_special : elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool*)
+let is_elf64_tbss_special sec_hdr segment:bool=  (not ((Uint64.logand sec_hdr.elf64_sh_flags (Uint64.of_string (Nat_big_num.to_string shf_tls))) = (Uint64.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)))) &&    
+(( Nat_big_num.equal(Nat_big_num.of_string (Uint32.to_string sec_hdr.elf64_sh_type)) sht_nobits) &&
+    ( not (Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string segment.elf64_p_type)) elf_pt_tls))))
+
+(** [get_elf32_section_to_segment_mapping hdr sht pht isin stbl] computes the
+  * section to segment mapping for an ELF file using information in the section
+  * header table [sht], program header table [pht] and file header [hdr].  A
+  * string table [stbl] is taken to produce the string output.  The test whether
+  * a section lies withing a segment is ABI specific, so [isin] is used to perform
+  * the test.
+  *)
+(*val get_elf32_section_to_segment_mapping : elf32_header -> elf32_section_header_table -> elf32_program_header_table_entry ->
+  (elf32_header -> elf32_section_header_table_entry -> elf32_program_header_table_entry -> bool) ->
+  string_table -> error (list string)*)
+let rec get_elf32_section_to_segment_mapping hdr sects pent isin stbl:((string)list)error=  
+ ((match sects with
+    | []    -> return []
+    | x::xs ->
+      if is_elf32_tbss_special x pent then
+        get_elf32_section_to_segment_mapping hdr xs pent isin stbl
+      else if not (isin hdr x pent) then
+        get_elf32_section_to_segment_mapping hdr xs pent isin stbl
+      else
+        let nm = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_name)) in
+          get_string_at nm stbl >>= (fun str ->
+          get_elf32_section_to_segment_mapping hdr xs pent isin stbl >>= (fun tl ->
+          return (str :: tl)))
+  ))
+  
+(** [get_elf64_section_to_segment_mapping hdr sht pht isin stbl] computes the
+  * section to segment mapping for an ELF file using information in the section
+  * header table [sht], program header table [pht] and file header [hdr].  A
+  * string table [stbl] is taken to produce the string output.  The test whether
+  * a section lies withing a segment is ABI specific, so [isin] is used to perform
+  * the test.
+  *)
+(*val get_elf64_section_to_segment_mapping : elf64_header -> elf64_section_header_table -> elf64_program_header_table_entry ->
+  (elf64_header -> elf64_section_header_table_entry -> elf64_program_header_table_entry -> bool) ->
+  string_table -> error (list string)*)
+let rec get_elf64_section_to_segment_mapping hdr sects pent isin stbl:((string)list)error=  
+ ((match sects with
+    | []    -> return []
+    | x::xs ->
+      if not (isin hdr x pent) then
+        get_elf64_section_to_segment_mapping hdr xs pent isin stbl
+      else if is_elf64_tbss_special x pent then
+        get_elf64_section_to_segment_mapping hdr xs pent isin stbl
+      else
+        let nm = (Nat_big_num.of_string (Uint32.to_string x.elf64_sh_name)) in
+          get_string_at nm stbl >>= (fun str ->
+          get_elf64_section_to_segment_mapping hdr xs pent isin stbl >>= (fun tl ->
+          return (str :: tl)))
+  ))
+  
+(** Section groups *)
+
+(** This is a COMDAT group and may duplicate other COMDAT groups in other object
+  * files.
+  *)
+let grp_comdat   : Nat_big_num.num= (Nat_big_num.of_int 1)
+
+(** Any bits in the following mask ranges are reserved exclusively for OS and
+  * processor specific semantics, respectively.
+  *)
+let grp_maskos   : Nat_big_num.num= (Nat_big_num.of_int 267386880)      (* 0x0ff00000 *)
+let grp_maskproc : Nat_big_num.num=  (Nat_big_num.mul(Nat_big_num.of_int 4)(Nat_big_num.of_int 1006632960)) (* 0xf0000000 *)
+
+(** [obtain_elf32_section_group_indices endian sht bs0] extracts all section header
+  * table indices of sections that are marked as being part of a section group.
+  *)
+(*val obtain_elf32_section_group_indices : endianness -> elf32_section_header_table -> byte_sequence
+  -> error (list (natural * list elf32_word))*)
+let obtain_elf32_section_group_indices endian sht bs0:((Nat_big_num.num*(Uint32.uint32)list)list)error=  
+ (let filtered = (List.filter (fun ent -> Nat_big_num.equal    
+(Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) sht_group) sht)
+  in
+    mapM (fun grp ->
+      let off = (Nat_big_num.of_string (Uint32.to_string grp.elf32_sh_offset)) in
+      let siz = (Nat_big_num.of_string (Uint32.to_string grp.elf32_sh_size)) in
+      let cnt = (Nat_big_num.div siz(Nat_big_num.of_int 4)) (* size of elf32_word in bytes *) in
+      Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
+      Error.repeatM' cnt rel (read_elf32_word endian) >>= (fun (mems, _) ->
+      (match mems with
+        | []    -> fail "obtain_elf32_section_group_indices: section group sections must consist of at least one elf32_word"
+        | x::xs ->
+          let flag = (Nat_big_num.of_string (Uint32.to_string x)) in
+            return (flag, xs)
+      )))
+    ) filtered)
+    
+(** [obtain_elf64_section_group_indices endian sht bs0] extracts all section header
+  * table indices of sections that are marked as being part of a section group.
+  *)
+(*val obtain_elf64_section_group_indices : endianness -> elf64_section_header_table -> byte_sequence
+  -> error (list (natural * list elf64_word))*)
+let obtain_elf64_section_group_indices endian sht bs0:((Nat_big_num.num*(Uint32.uint32)list)list)error=  
+ (let filtered = (List.filter (fun ent -> Nat_big_num.equal    
+(Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) sht_group) sht)
+  in
+    mapM (fun grp ->
+      let off = (Nat_big_num.of_string (Uint64.to_string grp.elf64_sh_offset)) in
+      let siz = (Ml_bindings.nat_big_num_of_uint64 grp.elf64_sh_size) in
+      let cnt = (Nat_big_num.div siz(Nat_big_num.of_int 4)) (* size of elf64_word in bytes *) in
+      Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
+      Error.repeatM' cnt rel (read_elf64_word endian) >>= (fun (mems, _) ->
+      (match mems with
+        | []    -> fail "obtain_elf64_section_group_indices: section group sections must consist of at least one elf64_word"
+        | x::xs ->
+          let flag = (Nat_big_num.of_string (Uint32.to_string x)) in
+            return (flag, xs)
+      )))
+    ) filtered)
+
+(** [obtain_elf32_tls_template sht] extracts the TLS template (i.e. all sections
+  * in section header table [sht] that have their TLS flag bit set).
+  *)
+(*val obtain_elf32_tls_template : elf32_section_header_table -> elf32_section_header_table*)
+let obtain_elf32_tls_template sht:(elf32_section_header_table_entry)list=  
+ (List.filter (fun ent ->
+    let flags = (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_flags)) in not (Nat_big_num.equal (Nat_big_num.bitwise_and flags shf_tls)(Nat_big_num.of_int 0))) sht)
+
+(** [obtain_elf64_tls_template sht] extracts the TLS template (i.e. all sections
+  * in section header table [sht] that have their TLS flag bit set).
+  *)
+(*val obtain_elf64_tls_template : elf64_section_header_table -> elf64_section_header_table*)
+let obtain_elf64_tls_template sht:(elf64_section_header_table_entry)list=  
+ (List.filter (fun ent ->
+    let flags = (Ml_bindings.nat_big_num_of_uint64 ent.elf64_sh_flags) in not (Nat_big_num.equal (Nat_big_num.bitwise_and flags shf_tls)(Nat_big_num.of_int 0))) sht)
+      
+(** [obtain_elf32_hash_table endian sht bs0] extracts a hash table from an ELF file
+  * providing a section of type SHT_HASH exists in section header table [sht].
+  * Extraction is from byte sequence [bs0] assuming endianness [endian].  The
+  * return type represents the number of buckets, the number of chains, the buckets
+  * and finally the chains.
+  *)
+(*val obtain_elf32_hash_table : endianness -> elf32_section_header_table -> byte_sequence ->
+  error (elf32_word * elf32_word * list elf32_word * list elf32_word)*)
+let obtain_elf32_hash_table endian sht bs0:(Uint32.uint32*Uint32.uint32*(Uint32.uint32)list*(Uint32.uint32)list)error=  
+ (let filtered = (List.filter (fun ent -> Nat_big_num.equal    
+(Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) sht_hash) sht)
+  in
+    (match filtered with
+      | []  -> fail "obtain_elf32_hash_table: no section header table entry of type sht_hash"
+      | [x] ->
+        let siz = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_size)) in
+        let off = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset)) in
+        Byte_sequence.offset_and_cut siz off bs0 >>= (fun rel ->
+        read_elf32_word endian rel >>= (fun (nbucket, rel) ->
+        read_elf32_word endian rel >>= (fun (nchain, rel) ->
+        Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nbucket)) rel (read_elf32_word endian) >>= (fun (buckets, rel) ->
+        Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nchain)) rel (read_elf32_word endian) >>= (fun (chain, _) ->
+        return (nbucket, nchain, buckets, chain))))))
+      | _   -> fail "obtain_elf32_hash_table: multiple section header table entries of type sht_hash"
+    ))
+    
+(** [obtain_elf64_hash_table endian sht bs0] extracts a hash table from an ELF file
+  * providing a section of type SHT_HASH exists in section header table [sht].
+  * Extraction is from byte sequence [bs0] assuming endianness [endian].  The
+  * return type represents the number of buckets, the number of chains, the buckets
+  * and finally the chains.
+  *)
+(*val obtain_elf64_hash_table : endianness -> elf64_section_header_table -> byte_sequence ->
+  error (elf64_word * elf64_word * list elf64_word * list elf64_word)*)
+let obtain_elf64_hash_table endian sht bs0:(Uint32.uint32*Uint32.uint32*(Uint32.uint32)list*(Uint32.uint32)list)error=  
+ (let filtered = (List.filter (fun ent -> Nat_big_num.equal    
+(Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) sht_hash) sht)
+  in
+    (match filtered with
+      | []  -> fail "obtain_elf64_hash_table: no section header table entry of type sht_hash"
+      | [x] ->
+        let siz = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in
+        let off = (Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset)) in
+        Byte_sequence.offset_and_cut siz off bs0 >>= (fun rel ->
+        read_elf64_word endian rel >>= (fun (nbucket, rel) ->
+        read_elf64_word endian rel >>= (fun (nchain, rel) ->
+        Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nbucket)) rel (read_elf64_word endian) >>= (fun (buckets, rel) ->
+        Error.repeatM' (Nat_big_num.of_string (Uint32.to_string nchain)) rel (read_elf64_word endian) >>= (fun (chain, _) ->
+        return (nbucket, nchain, buckets, chain))))))
+      | _   -> fail "obtain_elf64_hash_table: multiple section header table entries of type sht_hash"
+    ))
+
+(** Special sections *)
+
+(** [construct_special_sections] contains a finite map from section name (as
+  * a string) to the expected attributes and flags expected of that section,
+  * as specified in the ELF specification.
+  * NOTE: some of these are overriden by the ABI.
+  *)
+(*val elf_special_sections : Map.map string (natural * natural)*)
+let elf_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map=    
+ (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [
+      (".bss", (sht_nobits, Nat_big_num.add shf_alloc shf_write))
+    ; (".comment", (sht_progbits,Nat_big_num.of_int 0))
+    ; (".data", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+    ; (".data1", (sht_progbits, Nat_big_num.add shf_alloc shf_write))
+    ; (".debug", (sht_progbits,Nat_big_num.of_int 0))
+    (* ; (".dynamic", (sht_dynamic, ?)) *)
+    ; (".dynstr", (sht_strtab, shf_alloc))
+    ; (".dynsym", (sht_dynsym, shf_alloc))
+    ; (".fini", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr))
+    ; (".fini_array", (sht_fini_array, Nat_big_num.add shf_alloc shf_write))
+    (* ; (".got", (sht_progbits, ?)) *)
+    ; (".hash", (sht_hash, shf_alloc))
+    ; (".init", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr))
+    ; (".init_array", (sht_init_array, Nat_big_num.add shf_alloc shf_write))
+    (* ; (".interp", (sht_progbits, ?)) *)
+    ; (".line", (sht_progbits,Nat_big_num.of_int 0))
+    ; (".note", (sht_note,Nat_big_num.of_int 0))
+    (* ; (".plt", (sht_progbits, ?)) *)
+    ; (".preinit_array", (sht_preinit_array, Nat_big_num.add shf_alloc shf_write))
+    (* ; (".relname", (sht_rel, ?)) *)
+    (* ; (".relaname", (sht_rela, ?)) *)
+    ; (".rodata", (sht_progbits, shf_alloc))
+    ; (".rodata1", (sht_progbits, shf_alloc))
+    ; (".shstrtab", (sht_strtab,Nat_big_num.of_int 0))
+    (* ; (".strtab", (sht_strtab, ?)) *)
+    (* ; (".symtab", (sht_symtab, ?)) *)
+    (* ; (".symtab_shndx", (sht_symtab_shndx, ?)) *)
+    ; (".tbss", (sht_nobits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls))
+    ; (".tdata", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls))
+    ; (".tdata1", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_tls))
+    ; (".text", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr))
+    ])