Source file elf_symbol_table.ml

(*Generated by Lem from elf_symbol_table.lem.*)
(** [elf_symbol_table] provides types, functions and other definitions for
  * working with ELF symbol tables.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
open Lem_tuple
(*import Set*)

open Byte_sequence
open Error
open Missing_pervasives
open Show

open Elf_header
open Elf_types_native_uint
open Endianness
open String_table

(** Undefined symbol index *)

let stn_undef : Nat_big_num.num= ( (Nat_big_num.of_int 0))

(** Symbol binding *)

(** Local symbols are not visible outside of the object file containing their
  * definition.
  *)
let stb_local : Nat_big_num.num= ( (Nat_big_num.of_int 0))

(** Global symbols are visible to all object files being combined.
  *)
let stb_global : Nat_big_num.num= ( (Nat_big_num.of_int 1))

(** Weak symbols resemble global symbols but their definitions have lower
  * precedence.
  *)
let stb_weak : Nat_big_num.num= ( (Nat_big_num.of_int 2))

(** Values in the following range have reserved OS specific semantics.
  *)
let stb_loos : Nat_big_num.num= ( (Nat_big_num.of_int 10))
let stb_hios : Nat_big_num.num= ( (Nat_big_num.of_int 12))

(** Values in the following range have reserved processor specific semantics.
  *)
let stb_loproc : Nat_big_num.num= ( (Nat_big_num.of_int 13))
let stb_hiproc : Nat_big_num.num= ( (Nat_big_num.of_int 15))

(** string_of_symbol_binding b os proc] produces a string representation of
  * binding [m] using printing functions [os] and [proc] for OS- and processor-
  * specific values respectively.
  * OCaml specific definition.
  *)
(*val string_of_symbol_binding : natural -> (natural -> string) -> (natural -> string) -> string*)
let string_of_symbol_binding m os proc:string=
   (if Nat_big_num.equal m stb_local then
    "LOCAL"
  else if Nat_big_num.equal m stb_global then
    "GLOBAL"
  else if Nat_big_num.equal m stb_weak then
    "WEAK"
  else if Nat_big_num.greater_equal m stb_loos && Nat_big_num.less_equal m stb_hios then
    os m
  else if Nat_big_num.greater_equal m stb_loproc && Nat_big_num.less_equal m stb_hiproc then
    proc m
  else
    "Invalid symbol binding")

(** Symbol types *)

(** The symbol's type is not specified.
  *)
let stt_notype : Nat_big_num.num= ( (Nat_big_num.of_int 0))

(** The symbol is associated with a data object such as a variable.
  *)
let stt_object : Nat_big_num.num= ( (Nat_big_num.of_int 1))

(** The symbol is associated with a function or other executable code.
  *)
let stt_func : Nat_big_num.num= ( (Nat_big_num.of_int 2))

(** The symbol is associated with a section.
  *)
let stt_section : Nat_big_num.num= ( (Nat_big_num.of_int 3))

(** Conventionally the symbol's value gives the name of the source file associated
  * with the object file.
  *)
let stt_file : Nat_big_num.num= ( (Nat_big_num.of_int 4))

(** The symbol is an uninitialised common block.
  *)
let stt_common : Nat_big_num.num= ( (Nat_big_num.of_int 5))

(** The symbol specified a Thread Local Storage (TLS) entity.
  *)
let stt_tls : Nat_big_num.num= ( (Nat_big_num.of_int 6))

(** Values in the following range are reserved solely for OS-specific semantics.
  *)
let stt_loos : Nat_big_num.num= ( (Nat_big_num.of_int 10))
let stt_hios : Nat_big_num.num= ( (Nat_big_num.of_int 12))

(** Values in the following range are reserved solely for processor-specific
  * semantics.
  *)
let stt_loproc : Nat_big_num.num= ( (Nat_big_num.of_int 13))
let stt_hiproc : Nat_big_num.num= ( (Nat_big_num.of_int 15))

(** [string_of_symbol_type sym os proc] produces a string representation of
  * symbol type [m] using [os] and [proc] to pretty-print values reserved for
  * OS- and processor-specific functionality.
  *)
(*val string_of_symbol_type : natural -> (natural -> string) -> (natural -> string) -> string*)
let string_of_symbol_type m os proc:string=
   (if Nat_big_num.equal m stt_notype then
    "NOTYPE"
  else if Nat_big_num.equal m stt_object then
    "OBJECT"
  else if Nat_big_num.equal m stt_func then
    "FUNC"
  else if Nat_big_num.equal m stt_section then
    "SECTION"
  else if Nat_big_num.equal m stt_file then
    "FILE"
  else if Nat_big_num.equal m stt_common then
    "COMMON"
  else if Nat_big_num.equal m stt_tls then
    "TLS"
  else if Nat_big_num.greater_equal m stt_loos && Nat_big_num.less_equal m stt_hios then
    os m
  else if Nat_big_num.greater_equal m stt_loproc && Nat_big_num.less_equal m stt_hiproc then
    proc m
  else
    "Invalid symbol type")

(** Symbol visibility *)

(** The visibility of the symbol is as specified by the symbol's binding type.
  *)
let stv_default : Nat_big_num.num= ( (Nat_big_num.of_int 0))

(** The meaning of this visibility may be defined by processor supplements to
  * further constrain hidden symbols.
  *)
let stv_internal : Nat_big_num.num= ( (Nat_big_num.of_int 1))

(** The symbol's name is not visible in other components.
  *)
let stv_hidden : Nat_big_num.num= ( (Nat_big_num.of_int 2))

(** The symbol is visible in other components but not pre-emptable.  That is,
  * references to the symbol in the same component resolve to this symbol even
  * if other symbols of the same name in other components would normally be
  * resolved to instead if we followed the normal rules of symbol resolution.
  *)
let stv_protected : Nat_big_num.num= ( (Nat_big_num.of_int 3))

(** [string_of_symbol_visibility m] produces a string representation of symbol
  * visibility [m].
  *)
(*val string_of_symbol_visibility : natural -> string*)
let string_of_symbol_visibility m:string=
   (if Nat_big_num.equal m stv_default then
    "DEFAULT"
  else if Nat_big_num.equal m stv_internal then
    "INTERNAL"
  else if Nat_big_num.equal m stv_hidden then
    "HIDDEN"
  else if Nat_big_num.equal m stv_protected then
    "PROTECTED"
  else
    "Invalid symbol visibility")

(** Symbol table entry type *)

(** [elf32_symbol_table_entry] is an entry in a symbol table.
  *)
type elf32_symbol_table_entry =
  { elf32_st_name  : Uint32_wrapper.uint32     (** Index into the object file's string table *)
   ; elf32_st_value : Uint32_wrapper.uint32     (** Gives the value of the associated symbol *)
   ; elf32_st_size  : Uint32_wrapper.uint32     (** Size of the associated symbol *)
   ; elf32_st_info  : Uint32_wrapper.uint32  (** Specifies the symbol's type and binding attributes *)
   ; elf32_st_other : Uint32_wrapper.uint32  (** Currently specifies the symbol's visibility *)
   ; elf32_st_shndx : Uint32_wrapper.uint32     (** Section header index symbol is defined with respect to *)
   }

(** [elf32_symbol_table_entry_compare ent1 ent2] is an ordering-comparison function
  * for symbol table entries suitable for constructing sets, finite maps and other
  * ordered data structures from.
  *)
(*val elf32_symbol_table_entry_compare : elf32_symbol_table_entry ->
  elf32_symbol_table_entry -> ordering*)
let elf32_symbol_table_entry_compare ent1 ent2:int= 
     (sextupleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (Uint32_wrapper.to_bigint ent1.elf32_st_name, Uint32_wrapper.to_bigint ent1.elf32_st_value, 
        Uint32_wrapper.to_bigint ent1.elf32_st_size, Uint32_wrapper.to_bigint ent1.elf32_st_info, 
        Uint32_wrapper.to_bigint ent1.elf32_st_other, Uint32_wrapper.to_bigint ent1.elf32_st_shndx)
       (Uint32_wrapper.to_bigint ent2.elf32_st_name, Uint32_wrapper.to_bigint ent2.elf32_st_value, 
        Uint32_wrapper.to_bigint ent2.elf32_st_size, Uint32_wrapper.to_bigint ent2.elf32_st_info, 
        Uint32_wrapper.to_bigint ent2.elf32_st_other, Uint32_wrapper.to_bigint ent2.elf32_st_shndx))

let instance_Basic_classes_Ord_Elf_symbol_table_elf32_symbol_table_entry_dict:(elf32_symbol_table_entry)ord_class= ({

  compare_method = elf32_symbol_table_entry_compare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_symbol_table_entry_compare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_symbol_table_entry_compare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf32_symbol_table_entry_compare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf32_symbol_table_entry_compare f1 f2)(Pset.from_list compare [1; 0])))})
   
(** [elf64_symbol_table_entry] is an entry in a symbol table.
  *)
type elf64_symbol_table_entry =
  { elf64_st_name  : Uint32_wrapper.uint32     (** Index into the object file's string table *)
   ; elf64_st_info  : Uint32_wrapper.uint32  (** Specifies the symbol's type and binding attributes *)
   ; elf64_st_other : Uint32_wrapper.uint32  (** Currently specifies the symbol's visibility *)
   ; elf64_st_shndx : Uint32_wrapper.uint32     (** Section header index symbol is defined with respect to *)
   ; elf64_st_value : Uint64_wrapper.uint64     (** Gives the value of the associated symbol *)
   ; elf64_st_size  : Uint64_wrapper.uint64    (** Size of the associated symbol *)
   }

(** [elf64_symbol_table_entry_compare ent1 ent2] is an ordering-comparison function
  * for symbol table entries suitable for constructing sets, finite maps and other
  * ordered data structures from.
  *)
(*val elf64_symbol_table_entry_compare : elf64_symbol_table_entry -> elf64_symbol_table_entry ->
  ordering*)
let elf64_symbol_table_entry_compare ent1 ent2:int= 
     (sextupleCompare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare Nat_big_num.compare (Uint32_wrapper.to_bigint ent1.elf64_st_name, Ml_bindings.nat_big_num_of_uint64 ent1.elf64_st_value, 
        Ml_bindings.nat_big_num_of_uint64 ent1.elf64_st_size, Uint32_wrapper.to_bigint ent1.elf64_st_info, 
        Uint32_wrapper.to_bigint ent1.elf64_st_other, Uint32_wrapper.to_bigint ent1.elf64_st_shndx)
       (Uint32_wrapper.to_bigint ent2.elf64_st_name, Ml_bindings.nat_big_num_of_uint64 ent2.elf64_st_value, 
        Ml_bindings.nat_big_num_of_uint64 ent2.elf64_st_size, Uint32_wrapper.to_bigint ent2.elf64_st_info, 
        Uint32_wrapper.to_bigint ent2.elf64_st_other, Uint32_wrapper.to_bigint ent2.elf64_st_shndx))

let instance_Basic_classes_Ord_Elf_symbol_table_elf64_symbol_table_entry_dict:(elf64_symbol_table_entry)ord_class= ({

  compare_method = elf64_symbol_table_entry_compare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_symbol_table_entry_compare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_symbol_table_entry_compare f1 f2)(Pset.from_list compare [(-1); 0])));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(elf64_symbol_table_entry_compare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (elf64_symbol_table_entry_compare f1 f2)(Pset.from_list compare [1; 0])))})
  
type elf32_symbol_table = elf32_symbol_table_entry
  list
  
type elf64_symbol_table = elf64_symbol_table_entry
  list

(** Extraction of symbol table data *)

(* Functions below common to 32- and 64-bit! *)

(** [extract_symbol_binding u] extracts a symbol table entry's symbol binding.  [u]
  * in this case is the [elfXX_st_info] field from a symbol table entry.
  *)
(*val extract_symbol_binding : unsigned_char -> natural*)
let extract_symbol_binding entry:Nat_big_num.num=
   (Uint32_wrapper.to_bigint (Uint32_wrapper.shift_right entry 4))
  
(** [extract_symbol_type u] extracts a symbol table entry's symbol type.  [u]
  * in this case is the [elfXX_st_info] field from a symbol table entry.
  *)
(*val extract_symbol_type : unsigned_char -> natural*)
let extract_symbol_type entry:Nat_big_num.num=
   (Uint32_wrapper.to_bigint (Uint32_wrapper.logand entry (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 15))))) (* 0xf *)

(** [get_symbol_info u] extracts a symbol table entry's symbol info.  [u]
  * in this case is the [elfXX_st_info] field from a symbol table entry.
  *)
(*val make_symbol_info : natural -> natural -> unsigned_char*)
let make_symbol_info binding1 symtype:Uint32_wrapper.uint32=
   (Uint32_wrapper.add
    (Uint32_wrapper.shift_left (Uint32_wrapper.of_bigint binding1) 4)
    (Uint32_wrapper.logand (Uint32_wrapper.of_bigint symtype)
      (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 15))))) (*0xf*)  

(** [get_symbol_visibility u] extracts a symbol table entry's symbol visibility.  [u]
  * in this case is the [elfXX_st_other] field from a symbol table entry.
  *)
(*val get_symbol_visibility : unsigned_char -> natural*)
let get_symbol_visibility info:Nat_big_num.num=
   (Uint32_wrapper.to_bigint (Uint32_wrapper.logand info (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 3))))) (* 0x3*)
  
(** [make_symbol_other m] converts a natural [m] to an unsigned char suitable
  * for use in a symbol table entry's "other" field.
  * XXX: WHY?
  *)
(*val make_symbol_other : natural -> unsigned_char*)
let make_symbol_other visibility:Uint32_wrapper.uint32=
   (Uint32_wrapper.of_bigint visibility)
  
(** [is_elf32_shndx_too_large ent] tests whether the symbol table entry's
  * [shndx] field is equal to SHN_XINDEX, in which case the real value is stored
  * elsewhere.
  *)
(*val is_elf32_shndx_too_large : elf32_symbol_table_entry -> bool*)
let is_elf32_shndx_too_large syment:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint syment.elf32_st_shndx) shn_xindex)
  
(** [is_elf64_shndx_too_large ent] tests whether the symbol table entry's
  * [shndx] field is equal to SHN_XINDEX, in which case the real value is stored
  * elsewhere.
  *)
(*val is_elf64_shndx_too_large : elf64_symbol_table_entry -> bool*)
let is_elf64_shndx_too_large syment:bool=  (Nat_big_num.equal
  (Uint32_wrapper.to_bigint syment.elf64_st_shndx) shn_xindex)

(** NULL tests *)

(** [is_elf32_null_entry ent] tests whether [ent] is a null symbol table entry,
  * i.e. all fields set to [0].
  *)
(*val is_elf32_null_entry : elf32_symbol_table_entry -> bool*)
let is_elf32_null_entry ent:bool=  (Nat_big_num.equal 
    (Uint32_wrapper.to_bigint ent.elf32_st_name)( (Nat_big_num.of_int 0))
    && (( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf32_st_value)( (Nat_big_num.of_int 0)))
    && (( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf32_st_size)( (Nat_big_num.of_int 0)))
    && (( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf32_st_info)( (Nat_big_num.of_int 0)))
    && (( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf32_st_other)( (Nat_big_num.of_int 0)))
    && ( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf32_st_shndx)( (Nat_big_num.of_int 0))))))))
    
(** [is_elf64_null_entry ent] tests whether [ent] is a null symbol table entry,
  * i.e. all fields set to [0].
  *)
(*val is_elf64_null_entry : elf64_symbol_table_entry -> bool*)
let is_elf64_null_entry ent:bool=  (Nat_big_num.equal 
    (Uint32_wrapper.to_bigint ent.elf64_st_name)( (Nat_big_num.of_int 0))
    && (( Nat_big_num.equal(Ml_bindings.nat_big_num_of_uint64 ent.elf64_st_value)( (Nat_big_num.of_int 0)))
    && (( Nat_big_num.equal(Ml_bindings.nat_big_num_of_uint64 ent.elf64_st_size)( (Nat_big_num.of_int 0)))
    && (( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf64_st_info)( (Nat_big_num.of_int 0)))
    && (( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf64_st_other)( (Nat_big_num.of_int 0)))
    && ( Nat_big_num.equal(Uint32_wrapper.to_bigint ent.elf64_st_shndx)( (Nat_big_num.of_int 0))))))))

(** Printing symbol table entries *)

type symtab_print_bundle =
  (Nat_big_num.num -> string) * (Nat_big_num.num -> string)

(** [string_of_elf32_symbol_table_entry ent] produces a string based representation
  * of symbol table entry [ent].
  *)
(*val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string*)
let string_of_elf32_symbol_table_entry entry:string=
   (unlines [
    ("\t" ^ ("Name: "  ^ Uint32_wrapper.to_string entry.elf32_st_name))
  ; ("\t" ^ ("Value: " ^ Uint32_wrapper.to_string entry.elf32_st_value))
  ; ("\t" ^ ("Size: "  ^ Uint32_wrapper.to_string entry.elf32_st_size))
  ; ("\t" ^ ("Info: "  ^ Uint32_wrapper.to_string entry.elf32_st_info))
  ; ("\t" ^ ("Other: " ^ Uint32_wrapper.to_string entry.elf32_st_other))
  ; ("\t" ^ ("Shndx: " ^ Uint32_wrapper.to_string entry.elf32_st_shndx))
  ])
  
(** [string_of_elf64_symbol_table_entry ent] produces a string based representation
  * of symbol table entry [ent].
  *)
(*val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string*)
let string_of_elf64_symbol_table_entry entry:string=
   (unlines [
    ("\t" ^ ("Name: "  ^ Uint32_wrapper.to_string entry.elf64_st_name))
  ; ("\t" ^ ("Info: "  ^ Uint32_wrapper.to_string entry.elf64_st_info))
  ; ("\t" ^ ("Other: " ^ Uint32_wrapper.to_string entry.elf64_st_other))
  ; ("\t" ^ ("Shndx: " ^ Uint32_wrapper.to_string entry.elf64_st_shndx))
  ; ("\t" ^ ("Value: " ^ Uint64_wrapper.to_string entry.elf64_st_value))
  ; ("\t" ^ ("Size: "  ^ Uint64_wrapper.to_string entry.elf64_st_size))
  ])

(** [string_of_elf32_symbol_table stbl] produces a string based representation
  * of symbol table [stbl].
  *)
(*val string_of_elf32_symbol_table : elf32_symbol_table -> string*)
let string_of_elf32_symbol_table symtab:string=
   (unlines (Lem_list.map string_of_elf32_symbol_table_entry symtab))
  
(** [elf64_null_symbol_table_entry] is the null symbol table entry, with all
  * fields set to zero.
  *)
(*val elf64_null_symbol_table_entry : elf64_symbol_table_entry*)
let elf64_null_symbol_table_entry:elf64_symbol_table_entry=
   ({ elf64_st_name  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_st_info  = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_st_other = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_st_shndx = (Uint32_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_st_value = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   ; elf64_st_size  = (Uint64_wrapper.of_bigint( (Nat_big_num.of_int 0)))
   })

(*val string_of_elf64_symbol_table : elf64_symbol_table -> string*)
let string_of_elf64_symbol_table symtab:string=
   (unlines (Lem_list.map string_of_elf64_symbol_table_entry symtab))
  
let instance_Show_Show_Elf_symbol_table_elf32_symbol_table_entry_dict:(elf32_symbol_table_entry)show_class= ({

  show_method = string_of_elf32_symbol_table_entry})

let instance_Show_Show_Elf_symbol_table_elf64_symbol_table_entry_dict:(elf64_symbol_table_entry)show_class= ({

  show_method = string_of_elf64_symbol_table_entry})

(** Reading in symbol table (entries) *)

(** [read_elf32_symbol_table_entry endian bs0] reads an ELF symbol table entry
  * record from byte sequence [bs0] assuming endianness [endian], returning the
  * remainder of the byte sequence.  Fails if the byte sequence is not long enough.
  *)
(*val read_elf32_symbol_table_entry : endianness -> byte_sequence ->
  error (elf32_symbol_table_entry * byte_sequence)*)
let read_elf32_symbol_table_entry endian bs0:(elf32_symbol_table_entry*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs0) (fun (st_name, bs0) -> bind (read_elf32_addr endian bs0) (fun (st_value, bs0) -> bind (read_elf32_word endian bs0) (fun (st_size, bs0) -> bind (read_unsigned_char endian bs0) (fun (st_info, bs0) -> bind (read_unsigned_char endian bs0) (fun (st_other, bs0) -> bind (read_elf32_half endian bs0) (fun (st_shndx, bs0) ->
    return ({ elf32_st_name = st_name; elf32_st_value = st_value;
                 elf32_st_size = st_size; elf32_st_info = st_info;
                 elf32_st_other = st_other; elf32_st_shndx = st_shndx }, bs0))))))))

(*val bytes_of_elf32_symbol_table_entry : endianness ->
  elf32_symbol_table_entry -> byte_sequence*)
let bytes_of_elf32_symbol_table_entry endian entry:Byte_sequence_wrapper.byte_sequence=
   (Byte_sequence.from_byte_lists [
    bytes_of_elf32_word endian entry.elf32_st_name
  ; bytes_of_elf32_addr endian entry.elf32_st_value
  ; bytes_of_elf32_word endian entry.elf32_st_size
  ; bytes_of_unsigned_char entry.elf32_st_info
  ; bytes_of_unsigned_char entry.elf32_st_other
  ; bytes_of_elf32_half endian entry.elf32_st_shndx
  ])

(** [read_elf64_symbol_table_entry endian bs0] reads an ELF symbol table entry
  * record from byte sequence [bs0] assuming endianness [endian], returning the
  * remainder of the byte sequence.  Fails if the byte sequence is not long enough.
  *)       
(*val read_elf64_symbol_table_entry : endianness -> byte_sequence ->
  error (elf64_symbol_table_entry * byte_sequence)*)
let read_elf64_symbol_table_entry endian bs0:(elf64_symbol_table_entry*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_word endian bs0) (fun (st_name, bs0) -> bind (read_unsigned_char endian bs0) (fun (st_info, bs0) -> bind (read_unsigned_char endian bs0) (fun (st_other, bs0) -> bind (read_elf64_half endian bs0) (fun (st_shndx, bs0) -> bind (read_elf64_addr endian bs0) (fun (st_value, bs0) -> bind (read_elf64_xword endian bs0) (fun (st_size, bs0) ->
    return ({ elf64_st_name = st_name; elf64_st_info = st_info;
                 elf64_st_other = st_other; elf64_st_shndx = st_shndx;
                 elf64_st_value = st_value; elf64_st_size = st_size }, bs0))))))))

(*val bytes_of_elf64_symbol_table_entry : endianness ->
  elf64_symbol_table_entry -> byte_sequence*)
let bytes_of_elf64_symbol_table_entry endian entry:Byte_sequence_wrapper.byte_sequence=
   (Byte_sequence.from_byte_lists [
    bytes_of_elf64_word endian entry.elf64_st_name
  ; bytes_of_unsigned_char entry.elf64_st_info
  ; bytes_of_unsigned_char entry.elf64_st_other
  ; bytes_of_elf64_half endian entry.elf64_st_shndx
  ; bytes_of_elf64_addr  endian entry.elf64_st_value
  ; bytes_of_elf64_xword endian entry.elf64_st_size
  ])

(** [read_elf32_symbol_table endian bs0] reads a symbol table from byte sequence
  * [bs0] assuming endianness [endian].  Assumes [bs0]'s length modulo the size
  * of a symbol table entry is 0.  Fails otherwise.
  *)
(*val read_elf32_symbol_table : endianness -> byte_sequence -> error elf32_symbol_table*)
let rec read_elf32_symbol_table endian bs0:((elf32_symbol_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_symbol_table_entry endian bs0) (fun (head, bs0) -> bind (read_elf32_symbol_table endian bs0) (fun tail ->
    return (head::tail))))
    
(** [read_elf64_symbol_table endian bs0] reads a symbol table from byte sequence
  * [bs0] assuming endianness [endian].  Assumes [bs0]'s length modulo the size
  * of a symbol table entry is 0.  Fails otherwise.
  *)
(*val read_elf64_symbol_table : endianness -> byte_sequence -> error elf64_symbol_table*)
let rec read_elf64_symbol_table endian bs0:((elf64_symbol_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_symbol_table_entry endian bs0) (fun (head, bs0) -> bind (read_elf64_symbol_table endian bs0) (fun tail ->
    return (head::tail))))

(** Association map of symbol name, symbol type, symbol size, symbol address
  * and symbol binding.
  * A PPCMemism.
  *)
type symbol_address_map
  = (string * (Nat_big_num.num * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num)) list

(** [get_elf32_symbol_image_address symtab stbl] extracts the symbol address map
  * from the symbol table [symtab] using the string table [stbl].
  * A PPCMemism.
  *)
(*val get_elf32_symbol_image_address : elf32_symbol_table -> string_table ->
  error symbol_address_map*)
let get_elf32_symbol_image_address symtab strtab:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*Nat_big_num.num))list)error=
   (mapM (fun entry ->
    let name1 = (Uint32_wrapper.to_bigint entry.elf32_st_name) in
    let addr = (Uint32_wrapper.to_bigint entry.elf32_st_value) in
    let size2 = (Nat_big_num.mul (Uint32_wrapper.to_bigint entry.elf32_st_size)( (Nat_big_num.of_int 8))) in
    let typ  = (extract_symbol_type entry.elf32_st_info) in
    let bnd  = (extract_symbol_binding entry.elf32_st_info) in bind (String_table.get_string_at name1 strtab) (fun str ->
      return (str, (typ, size2, addr, bnd)))
  ) symtab)

(** [get_elf64_symbol_image_address symtab stbl] extracts the symbol address map
  * from the symbol table [symtab] using the string table [stbl].
  * A PPCMemism.
  *)
(*val get_elf64_symbol_image_address : elf64_symbol_table -> string_table ->
  error symbol_address_map*)
let get_elf64_symbol_image_address symtab strtab:((string*(Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*Nat_big_num.num))list)error=
   (mapM (fun entry ->
    let name1 = (Uint32_wrapper.to_bigint entry.elf64_st_name) in
    let addr = (Ml_bindings.nat_big_num_of_uint64 entry.elf64_st_value) in
    let size2 = (Ml_bindings.nat_big_num_of_uint64 entry.elf64_st_size) in
    let typ  = (extract_symbol_type entry.elf64_st_info) in
    let bnd  = (extract_symbol_binding entry.elf64_st_info) in bind (String_table.get_string_at name1 strtab) (fun str ->
      return (str, (typ, size2, addr, bnd)))
  ) symtab)

(** [get_el32_symbol_type ent] extracts the symbol type from symbol table entry
  * [ent].
  *)
(*val get_elf32_symbol_type : elf32_symbol_table_entry -> natural*)
let get_elf32_symbol_type syment:Nat_big_num.num=  (extract_symbol_type syment.elf32_st_info)

(** [get_el64_symbol_type ent] extracts the symbol type from symbol table entry
  * [ent].
  *)
(*val get_elf64_symbol_type : elf64_symbol_table_entry -> natural*)
let get_elf64_symbol_type syment:Nat_big_num.num=  (extract_symbol_type syment.elf64_st_info)

(** [get_el32_symbol_binding ent] extracts the symbol binding from symbol table entry
  * [ent].
  *)
(*val get_elf32_symbol_binding : elf32_symbol_table_entry -> natural*)
let get_elf32_symbol_binding syment:Nat_big_num.num=  (extract_symbol_binding syment.elf32_st_info)

(** [get_el64_symbol_binding ent] extracts the symbol binding from symbol table entry
  * [ent].
  *)
(*val get_elf64_symbol_binding : elf64_symbol_table_entry -> natural*)
let get_elf64_symbol_binding syment:Nat_big_num.num=  (extract_symbol_binding syment.elf64_st_info)