Source file elf_section_header_table.ml

(*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_wrapper.uint32  (** Specifies the compression algorithm *)
   ; elf32_chdr_size      : Uint32_wrapper.uint32  (** Size in bytes of the uncompressed data *)
   ; elf32_chdr_addralign : Uint32_wrapper.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_wrapper.uint32  (** Specified the compression algorithm *)
   ; elf64_chdr_reserved  : Uint32_wrapper.uint32  (** Reserved. *)
   ; elf64_chdr_size      : Uint64_wrapper.uint64 (** Size in bytes of the uncompressed data *)
   ; elf64_chdr_addralign : Uint64_wrapper.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_wrapper.byte_sequence)error=  (bind (read_elf32_word ed bs0) (fun (typ, bs1) -> bind (read_elf32_word ed bs1) (fun (siz, bs2) -> bind (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_wrapper.byte_sequence)error=   (bind (read_elf64_word ed bs0) (fun (typ, bs1) ->  bind (read_elf64_word ed bs1) (fun (res, bs2) -> bind (read_elf64_xword ed bs2) (fun (siz, bs3) -> bind (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_wrapper.uint32 (** Name of the section *)
   ; elf32_sh_type      : Uint32_wrapper.uint32 (** Type of the section and its semantics *)
   ; elf32_sh_flags     : Uint32_wrapper.uint32 (** Flags associated with the section *)
   ; elf32_sh_addr      : Uint32_wrapper.uint32 (** Address of first byte of section in memory image *)
   ; elf32_sh_offset    : Uint32_wrapper.uint32  (** Offset from beginning of file of first byte of section *)
   ; elf32_sh_size      : Uint32_wrapper.uint32 (** Section size in bytes *)
   ; elf32_sh_link      : Uint32_wrapper.uint32 (** Section header table index link *)
   ; elf32_sh_info      : Uint32_wrapper.uint32 (** Extra information, contents depends on type of section *)
   ; elf32_sh_addralign : Uint32_wrapper.uint32 (** Alignment constraints for section *)
   ; elf32_sh_entsize   : Uint32_wrapper.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_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_type      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_flags     = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_addr      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_offset    = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_size      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_link      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_info      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_addralign = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf32_sh_entsize   = (Uint32_wrapper.of_bigint( (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
    [Uint32_wrapper.to_bigint h1.elf32_sh_name;
    Uint32_wrapper.to_bigint h1.elf32_sh_type;
    Uint32_wrapper.to_bigint h1.elf32_sh_flags;
    Uint32_wrapper.to_bigint h1.elf32_sh_addr;
    Uint32_wrapper.to_bigint h1.elf32_sh_offset;
    Uint32_wrapper.to_bigint h1.elf32_sh_size;
    Uint32_wrapper.to_bigint h1.elf32_sh_link;
    Uint32_wrapper.to_bigint h1.elf32_sh_info;
    Uint32_wrapper.to_bigint h1.elf32_sh_addralign;
    Uint32_wrapper.to_bigint h1.elf32_sh_entsize]
    [Uint32_wrapper.to_bigint h2.elf32_sh_name;
    Uint32_wrapper.to_bigint h2.elf32_sh_type;
    Uint32_wrapper.to_bigint h2.elf32_sh_flags;
    Uint32_wrapper.to_bigint h2.elf32_sh_addr;
    Uint32_wrapper.to_bigint h2.elf32_sh_offset;
    Uint32_wrapper.to_bigint h2.elf32_sh_size;
    Uint32_wrapper.to_bigint h2.elf32_sh_link;
    Uint32_wrapper.to_bigint h2.elf32_sh_info;
    Uint32_wrapper.to_bigint h2.elf32_sh_addralign;
    Uint32_wrapper.to_bigint 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_wrapper.uint32  (** Name of the section *)
   ; elf64_sh_type      : Uint32_wrapper.uint32  (** Type of the section and its semantics *)
   ; elf64_sh_flags     : Uint64_wrapper.uint64 (** Flags associated with the section *)
   ; elf64_sh_addr      : Uint64_wrapper.uint64  (** Address of first byte of section in memory image *)
   ; elf64_sh_offset    : Uint64_wrapper.uint64   (** Offset from beginning of file of first byte of section *)
   ; elf64_sh_size      : Uint64_wrapper.uint64 (** Section size in bytes *)
   ; elf64_sh_link      : Uint32_wrapper.uint32  (** Section header table index link *)
   ; elf64_sh_info      : Uint32_wrapper.uint32  (** Extra information, contents depends on type of section *)
   ; elf64_sh_addralign : Uint64_wrapper.uint64 (** Alignment constraints for section *)
   ; elf64_sh_entsize   : Uint64_wrapper.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_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_type      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_flags     = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_addr      = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_offset    = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_size      = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_link      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_info      = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_addralign = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_sh_entsize   = (Uint64_wrapper.of_bigint( (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
    [Uint32_wrapper.to_bigint h1.elf64_sh_name;
    Uint32_wrapper.to_bigint 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;
    Uint64_wrapper.to_bigint h1.elf64_sh_offset;
    Ml_bindings.nat_big_num_of_uint64 h1.elf64_sh_size;
    Uint32_wrapper.to_bigint h1.elf64_sh_link;
    Uint32_wrapper.to_bigint 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]
    [Uint32_wrapper.to_bigint h2.elf64_sh_name;
    Uint32_wrapper.to_bigint 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;
    Uint64_wrapper.to_bigint h2.elf64_sh_offset;
    Ml_bindings.nat_big_num_of_uint64 h2.elf64_sh_size;
    Uint32_wrapper.to_bigint h2.elf64_sh_link;
    Uint32_wrapper.to_bigint 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_wrapper.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_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs) (fun (sh_name, bs) -> bind (read_elf32_word endian bs) (fun (sh_type, bs) -> bind (read_elf32_word endian bs) (fun (sh_flags, bs) -> bind (read_elf32_addr endian bs) (fun (sh_addr, bs) -> bind (read_elf32_off  endian bs) (fun (sh_offset, bs) -> bind (read_elf32_word endian bs) (fun (sh_size, bs) -> bind (read_elf32_word endian bs) (fun (sh_link, bs) -> bind (read_elf32_word endian bs) (fun (sh_info, bs) -> bind (read_elf32_word endian bs) (fun (sh_addralign, bs) -> bind (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_wrapper.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_wrapper.byte_sequence)error=   (bind (read_elf64_word endian bs) (fun (sh_name, bs) ->  bind (read_elf64_word endian bs) (fun (sh_type, bs) -> bind (read_elf64_xword endian bs) (fun (sh_flags, bs) ->  bind (read_elf64_addr endian bs) (fun (sh_addr, bs) ->  bind (read_elf64_off  endian bs) (fun (sh_offset, bs) -> bind (read_elf64_xword endian bs) (fun (sh_size, bs) ->  bind (read_elf64_word endian bs) (fun (sh_link, bs) ->  bind (read_elf64_word endian bs) (fun (sh_info, bs) -> bind (read_elf64_xword endian bs) (fun (sh_addralign, bs) -> bind (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_wrapper.byte_sequence=
   (Byte_sequence.concat (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_wrapper.byte_sequence=
   (Byte_sequence.concat (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 bind (read_elf32_section_header_table_entry endian bs0) (fun (entry, bs1) -> bind (read_elf32_section_header_table' endian bs1) (fun sht ->
    return (entry :: sht))))

(** [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 bind (read_elf64_section_header_table_entry endian bs0) (fun (entry, bs1) -> bind (read_elf64_section_header_table' endian bs1) (fun sht ->
    return (entry :: sht))))

(** [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_wrapper.byte_sequence)error=  (bind (partition0 table_size bs0) (fun (eat, rest) -> bind (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_wrapper.byte_sequence)error=  (bind (partition0 table_size bs0) (fun (eat, rest) -> bind (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 = (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint ent.elf32_sh_addralign) in
  let addr  = (Uint32_wrapper.to_bigint 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
        (Uint32_wrapper.to_bigint x.elf32_sh_name)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint x.elf32_sh_type) sht_null && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint x.elf32_sh_flags)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint x.elf32_sh_addr)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint x.elf32_sh_offset)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint x.elf32_sh_info)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint x.elf32_sh_addralign)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint 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
        (Uint32_wrapper.to_bigint x.elf64_sh_name)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint 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
        (Uint64_wrapper.to_bigint x.elf64_sh_offset)( (Nat_big_num.of_int 0)) && (Nat_big_num.equal
        (Uint32_wrapper.to_bigint 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_wrapper.to_string entry.elf32_sh_name))
  ; ("\t" ^ ("Type: "    ^ string_of_section_type os proc user (Uint32_wrapper.to_bigint entry.elf32_sh_type)))
  ; ("\t" ^ ("Flags: "   ^ Uint32_wrapper.to_string entry.elf32_sh_flags))
  ; ("\t" ^ ("Address: " ^ Uint32_wrapper.to_string entry.elf32_sh_addr))
  ; ("\t" ^ ("Size: "    ^ Uint32_wrapper.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_wrapper.to_string entry.elf64_sh_name))
  ; ("\t" ^ ("Type: "    ^ string_of_section_type os proc user (Uint32_wrapper.to_bigint entry.elf64_sh_type)))
  ; ("\t" ^ ("Flags: "   ^ Uint64_wrapper.to_string entry.elf64_sh_flags))
  ; ("\t" ^ ("Address: " ^ Uint64_wrapper.to_string entry.elf64_sh_addr))
  ; ("\t" ^ ("Size: "    ^ Uint64_wrapper.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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint entry.elf32_sh_type)))
    ; ("\t" ^ ("Flags: "   ^ Uint32_wrapper.to_string entry.elf32_sh_flags))
    ; ("\t" ^ ("Address: " ^ Uint32_wrapper.to_string entry.elf32_sh_addr))
    ; ("\t" ^ ("Size: "    ^ Uint32_wrapper.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 (Uint32_wrapper.to_bigint 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 (Uint32_wrapper.to_bigint entry.elf64_sh_type)))
    ; ("\t" ^ ("Flags: "   ^ Uint64_wrapper.to_string entry.elf64_sh_flags))
    ; ("\t" ^ ("Address: " ^ Uint64_wrapper.to_string entry.elf64_sh_addr))
    ; ("\t" ^ ("Size: "    ^ Uint64_wrapper.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_wrapper.logand sec_hdr.elf32_sh_flags (Uint32_wrapper.of_bigint shf_tls)) = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))) &&
    (( Nat_big_num.equal(Uint32_wrapper.to_bigint sec_hdr.elf32_sh_type) sht_nobits) &&
    ( not (Nat_big_num.equal (Uint32_wrapper.to_bigint 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_wrapper.logand sec_hdr.elf64_sh_flags (Uint64_wrapper.of_bigint shf_tls)) = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))) &&
    (( Nat_big_num.equal(Uint32_wrapper.to_bigint sec_hdr.elf64_sh_type) sht_nobits) &&
    ( not (Nat_big_num.equal (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint x.elf32_sh_name) in bind (get_string_at nm stbl) (fun str -> bind (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 = (Uint32_wrapper.to_bigint x.elf64_sh_name) in bind (get_string_at nm stbl) (fun str -> bind (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_wrapper.uint32)list)list)error=
   (let filtered = (List.filter (fun ent -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint ent.elf32_sh_type) sht_group) sht)
  in
    mapM (fun grp ->
      let off = (Uint32_wrapper.to_bigint grp.elf32_sh_offset) in
      let siz = (Uint32_wrapper.to_bigint 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 bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (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 = (Uint32_wrapper.to_bigint 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_wrapper.uint32)list)list)error=
   (let filtered = (List.filter (fun ent -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint ent.elf64_sh_type) sht_group) sht)
  in
    mapM (fun grp ->
      let off = (Uint64_wrapper.to_bigint 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 bind (Byte_sequence.offset_and_cut off siz bs0) (fun rel -> bind (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 = (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint 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_wrapper.uint32*Uint32_wrapper.uint32*(Uint32_wrapper.uint32)list*(Uint32_wrapper.uint32)list)error=
   (let filtered = (List.filter (fun ent -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint 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 = (Uint32_wrapper.to_bigint x.elf32_sh_size) in
        let off = (Uint32_wrapper.to_bigint  x.elf32_sh_offset) in bind (Byte_sequence.offset_and_cut siz off bs0) (fun rel -> bind (read_elf32_word endian rel) (fun (nbucket, rel) -> bind (read_elf32_word endian rel) (fun (nchain, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint nbucket) rel (read_elf32_word endian)) (fun (buckets, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint 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_wrapper.uint32*Uint32_wrapper.uint32*(Uint32_wrapper.uint32)list*(Uint32_wrapper.uint32)list)error=
   (let filtered = (List.filter (fun ent -> Nat_big_num.equal
    (Uint32_wrapper.to_bigint 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 = (Uint64_wrapper.to_bigint  x.elf64_sh_offset) in bind (Byte_sequence.offset_and_cut siz off bs0) (fun rel -> bind (read_elf64_word endian rel) (fun (nbucket, rel) -> bind (read_elf64_word endian rel) (fun (nchain, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint nbucket) rel (read_elf64_word endian)) (fun (buckets, rel) -> bind (Error.repeatM' (Uint32_wrapper.to_bigint 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))
    ])