(*Generated by Lem from elf_symbol_table.lem.*)
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_string

open Bitstring
open Elf_section_header
open Elf_types
open Error
open Show

(** Symbol table indices *)

(** Symbol table index is a subscript into the symbol table, which holds
  * information needed to locate and relocate a program's symbolic definitions
  * and references.  Index 0 designates both the first entry in the table and
  * serves as the undefined symbol index.  [stn_undef] is a mnemonic for that
  * undefined symbol.
  *)
let stn_undef : int =( 0)

(** Symbol bindings *)

(** [elf32_st_bind] unpacks the binding information from the [st_info] field
  * in the record type below.
  *)
let elf32_st_bind i =  
(Int64.to_int (Int64.shift_right i( 4)))
(** [elf64_st_bind] unpacks the binding information from the [st_info] field
  * in the record type below.
  *)
let elf64_st_bind i =  
(Int64.to_int (Int64.shift_right i( 4)))
(** [elf32_st_type] unpacks the type information from the [e32_st_info] field
  * in the record type below.
  *)
let elf32_st_type i =  
(Int64.to_int (Int64.logand i (Int64.of_int( 15)))) (* 0xf *)
(** [elf64_st_type] unpacks the type information from the [e64_st_info] field
  * in the record type below.
  *)
let elf64_st_type i =  
(Int64.to_int (Int64.logand i (Int64.of_int( 15)))) (* 0xf *)
(** [elf32_st_info] unpacks other information from the [e32_st_info] field in the
  * record type below.
  *)
let elf32_st_info b t =  
(let left   = (Int64.shift_left b( 4)) in
  let right  = (Int64.logand t (Int64.of_int( 15)))  in (* 0xf *)
  let result = (Int64.add left right) in
    Int64.to_int result)
(** [elf64_st_info] unpacks other information from the [e64_st_info] field in the
  * record type below.
  *)
let elf64_st_info b t =  
(let left   = (Int64.shift_left b( 4)) in
  let right  = (Int64.logand t (Int64.of_int( 15)))  in (* 0xf *)
  let result = (Int64.add left right) in
    Int64.to_int result)
(** [stb_local]: local symbols are not visible outside the object file
  * containing their definition.
  *)
let stb_local : int =( 0)
(** [stb_global]: global symbols are visible to all object files being combined.
  *)
let stb_global : int =( 1)
(** [stb_weak]: weak symbols resemble global symbols but their definitions have
  * lower precedence.
  *)
let stb_weak : int =( 2)
(** [stb_loos]: start of the range reserved for operating-system specific
  * semantics.
  *)
let stb_loos : int =( 10)
(** [stb_hios]: end of the range reserved for operating-system specific
  * semantics.
  *)
let stb_hios : int =( 12)
(** [stb_loproc]: start of the range reserved for processor specific semantics.
  *)
let stb_loproc : int =( 13)
(** [stb_hiproc]: end of the range reserved for processor specific semantics.
  *)
let stb_hiproc : int =( 15)

(** Symbol types. *)

(** [stt_notype]: the symbol's type is not specified.
  *)
let stt_notype : int =( 0)
(** [stt_object]: the symbol is associated with a data object, such as a
  * variable, an array, and so on.
  *)
let stt_object : int =( 1)
(** [stt_func]: the symbol is associated with a function or other executable
  * code.
  *)
let stt_func : int =( 2)
(** [stt_section]: the symbol is associated with a section.
  *)
let stt_section : int =( 3)
(** [stt_file]: the symbol's name gives the name of the source file associated
  * with the object file.  Must have [stb_local] binding and its section index
  * must be [shn_abs].  It must also precede the other [stb_local] symbols for
  * the file, is present.
  *)
let stt_file : int =( 4)
(** [stt_common]: labels an unitialised common block.
  *)
let stt_common : int =( 5)
(** [stt_tls]: specifies a thread local storage (TLS) entity.  Gives the
  * assigned offset of the symbol, not its address.  TLS symbols may only be
  * referenced by special TLS relocations and TLS relocations may only reference
  * symbols with type [stt_tls].
  *)
let stt_tls : int =( 6)
(** [stt_loos]: start of the range reserved for operating-system specific
  * semantics.
  *)
let stt_loos : int =( 10)
(** [stt_hios]: end of the range reserved for operating-system specific
  * semantics.
  *)
let stt_hios : int =( 12)
(** [stt_loproc]: start of the range reserved for processor specific
  * semantics.
  *)
let stt_loproc : int =( 13)
(** [stt_hiproc]: end of the range reserved for processor specific semantics.
  *)
let stt_hiproc : int =( 15)

(** Symbol visibility. *)

(** [elf32_st_visibility] unpacks visibility information from the [e32_st_other]
  * field in the record type below.
  *)
(*val elf32_st_visibility : unsigned_char -> nat*)
let elf32_st_visibility o =  
(Int64.to_int (Int64.logand o (Int64.of_int( 3)))) (* 0x3 *)

(** [stv_default]: symbol visibility is as specified by the symbol's binding
  * type.  Global and weak symbols are visible outside their defining component
  * (executable or shared object file).  Local symbols are hidden.  Global and
  * weak symbols are also pre-emptable: they may be pre-empted by definitions
  * of the same name in another component.
  *)
let stv_default : int =( 0)
(** [stv_internal]: meaning may be further defined by processor supplements to
  * further constrain hidden symbols.  An internal symbol in a relocatable file
  * must be either removed or converted to [stb_local] when the relocatable
  * object is included in an executable or shared object by the linker.
  *)
let stv_internal : int =( 1)
(** [stv_hidden]: a symbol in the current component is hidden if its name is not
  * visible to other components, necessarily protecting the symbol.  A hidden
  * object may still be referenced from another component if its address is
  * passed outside.  A hidden symbol in a relocatable object must be either
  * removed or converted to [stb_local] when the relocatable file is included in
  * an executable or shared object by the linker.
  *)
let stv_hidden : int =( 2)
(** [stv_protected]: a protected symbol is visible in other components but is
  * not pre-emptable, so that any reference to such a symbol from within the
  * defining component must be resolved to the definition in that component.
  * A symbol with [stb_local] binding must not have [stv_protected] visibility.
  * If a symbol definition with [stv_protected] visibility from a shared object
  * file is taken as resolving a reference from an executable or another shared
  * object, the [shn_undef] symbol table entry created has [stv_default]
  * visibility.
  *)
let stv_protected : int =( 3)

(** The symbol table entry type. *)

type elf32_symbol_table_entry =
  { elf32_st_name  : Int64.t
   ; elf32_st_value : Int64.t
   ; elf32_st_size  : Int64.t
   ; elf32_st_info0  : Int64.t
   ; elf32_st_other : Int64.t
   ; elf32_st_shndx : Int64.t
   }
   
let string_of_elf32_symbol_table_entry entry =	
(List.fold_right (^) [
		"\t"; "Name: "; Int64.to_string entry.elf32_st_name
	; "\t"; "Size: "; Int64.to_string entry.elf32_st_size
	; "\n\t"; "Value: "; Int64.to_string entry.elf32_st_value
	; "\t"; "Info: "; Int64.to_string entry.elf32_st_info0; "\n\n"
	] "")
   
let read_elf32_symbol_table_entry bitstring6 : elf32_symbol_table_entry error =	
(Ml_bindings.read_elf32_word bitstring6 >>= (fun (name, bitstring5) ->
	Ml_bindings.read_elf32_addr bitstring5 >>= (fun (value, bitstring4) ->
	Ml_bindings.read_elf32_word bitstring4 >>= (fun (size, bitstring3) ->
	Ml_bindings.read_unsigned_char bitstring3 >>= (fun (info, bitstring2) ->
	Ml_bindings.read_unsigned_char bitstring2 >>= (fun (other, bitstring1) ->
	Ml_bindings.read_elf32_half bitstring1 >>= (fun (shndx, bitstring0) ->
	let entry = ({ elf32_st_name = name; elf32_st_value = value; elf32_st_size = size; elf32_st_info0 = info; elf32_st_other = other; elf32_st_shndx = shndx }) in
	return entry)))))))
	
let rec read_elf32_symbol_table_entries bs : ( elf32_symbol_table_entry list) error =	
(if Bitstring.bitstring_length bs = 0 then
		return []
	else
		let (cut, rest) = (Utility.partition_bitstring( 128) bs) in
		read_elf32_symbol_table_entry cut >>= (fun head ->
		read_elf32_symbol_table_entries rest >>= (fun tail ->
		return (head::tail))))
	
let rec read_elf32_symbol_tables' offset_sizes bs =	
((match offset_sizes with
		| []    -> return []
		| x::xs ->
			let (offset, size) = x in
			let (_, relevant)  = (Utility.partition_bitstring offset bs) in
			let (cut, _)    = (Utility.partition_bitstring size relevant) in
			read_elf32_symbol_table_entries cut >>= (fun head ->
			read_elf32_symbol_tables' xs bs >>= (fun tail ->
			return (head::tail)))
	))

type elf32_symbol_table = elf32_symbol_table_entry list

let read_elf32_symbol_tables sections bs : ( elf32_symbol_table list) error =	
(let symtabs = (List.filter (fun sect ->
		(Int64.to_int sect.elf32_sh_type = sht_symtab) ||
			(Int64.to_int sect.elf32_sh_type = sht_dynsym)) sections)
	in
	let _ = (print_endline ("Symtabs: " ^ natShow (List.length symtabs))) in
	let offsets_sizes = (List.map (fun sect ->
		let offset = ((Int64.to_int sect.elf32_sh_offset) * 8) in
		let size   =			
(let _ = (print_endline ("YYY size: " ^ natShow (Int64.to_int sect.elf32_sh_size * 8))) in
			Int64.to_int sect.elf32_sh_size * 8)
		in
			(offset, size)) symtabs)
	in
		read_elf32_symbol_tables' offsets_sizes bs)
			
let string_of_elf32_symbol_table tbl =	
("Symbol table contents:" ^ ("\n" ^
		List.fold_right (^) (List.map string_of_elf32_symbol_table_entry tbl) ""))