Pull in updated elf model, make build work again (at least for me)

1 files changed, 206 insertions, 202 deletions

diff --git a/src/elf_model/elf_symbol_table.ml b/src/elf_model/elf_symbol_table.ml
index a2fed159..369629b0 100644
--- a/src/elf_model/elf_symbol_table.ml
+++ b/src/elf_model/elf_symbol_table.ml
@@ -2,245 +2,249 @@
 open Lem_basic_classes
 open Lem_bool
 open Lem_list
-open Lem_num
+open Lem_maybe
 open Lem_string
+open Lem_tuple
 
-open Bitstring
-open Elf_section_header
-open Elf_types
+open Bitstring_local
 open Error
+open Missing_pervasives
 open Show
 
-(** Symbol table indices *)
+open Elf_types
+open Endianness
+open String_table
+
+(** Undefined symbol index *)
 
-(** 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.
-  *)
+(** Symbol binding *)
+
 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. *)
+(*val string_of_symbol_binding : nat -> (nat -> string) -> (nat -> string) -> string*)
+let string_of_symbol_binding m os proc =  
+(if m = stb_local then
+    "STB_LOCAL"
+  else if m = stb_global then
+    "STB_GLOBAL"
+  else if m = stb_weak then
+    "STB_WEAK"
+  else if (m >= stb_loos) && (m <= stb_hios) then
+    os m
+  else if (m >= stb_loproc) && (m <= stb_hiproc) then
+    proc m
+  else
+    "Invalid symbol binding")
+
+(** 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.
-  *)
+(*val string_of_symbol_type : nat -> (nat -> string) -> (nat -> string) -> string*)
+let string_of_symbol_type m os proc =  
+(if m = stt_notype then
+    "STT_NOTYPE"
+  else if m = stt_object then
+    "STT_OBJECT"
+  else if m = stt_func then
+    "STT_FUNC"
+  else if m = stt_section then
+    "STT_SECTION"
+  else if m = stt_file then
+    "STT_FILE"
+  else if m = stt_common then
+    "STT_COMMON"
+  else if m = stt_tls then
+    "STT_TLS"
+  else if (m >= stt_loos) && (m <= stt_hios) then
+    os m
+  else if (m >= stt_loproc) && (m <= stt_hiproc) then
+    proc m
+  else
+    "Invalid symbol type")
+
+(** Symbol visibility *)
+
 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. *)
+(*val string_of_symbol_visibility : nat -> string*)
+let string_of_symbol_visibility m =  
+(if m = stv_default then
+    "STV_DEFAULT"
+  else if m = stv_internal then
+    "STV_INTERNAL"
+  else if m = stv_hidden then
+    "STV_HIDDEN"
+  else if m = stv_protected then
+    "STV_PROTECTED"
+  else
+    "Invalid symbol visibility")
+
+(** ELF32 symbol table 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
+  { elf32_st_name  : Uint32.t
+   ; elf32_st_value : Uint32.t
+   ; elf32_st_size  : Uint32.t
+   ; elf32_st_info  : Uint32.t
+   ; elf32_st_other : Uint32.t
+   ; elf32_st_shndx : Uint32.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)))
-	))
+
+(** Extraction of symbol table data *)
+
+(* Functions below common to 32- and 64-bit! *)
+
+(*val get_symbol_binding : unsigned_char -> nat*)
+let get_symbol_binding entry =  
+(Uint32.to_int (Uint32.shift_right entry( 4)))
+
+(*val get_symbol_type : unsigned_char -> nat*)
+let get_symbol_type entry =  
+(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 15)))) (* 0xf *)
+
+(*val get_symbol_info : unsigned_char -> unsigned_char -> nat*)
+let get_symbol_info entry0 entry1 =  
+(Uint32.to_int (Uint32.add
+    (Uint32.shift_left entry0( 4)) (Uint32.logand entry1
+      (Uint32.of_int( 15))))) (*0xf*)  
+
+(*val get_symbol_visibility : unsigned_char -> nat*)
+let get_symbol_visibility entry =  
+(Uint32.to_int (Uint32.logand entry (Uint32.of_int( 3)))) (* 0x3*)
+
+type symtab_print_bundle = (int -> string) * (int -> string)
+
+(*val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string*)
+let string_of_elf32_symbol_table_entry entry =  
+(unlines [    
+("\t" ^ ("Name: "  ^ Uint32.to_string entry.elf32_st_name))
+  ; ("\t" ^ ("Value: " ^ Uint32.to_string entry.elf32_st_value))
+  ; ("\t" ^ ("Size: "  ^ Uint32.to_string entry.elf32_st_size))
+  ; ("\t" ^ ("Info: "  ^ Uint32.to_string entry.elf32_st_info))
+  ; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf32_st_other))
+  ; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf32_st_shndx))
+  ])
 
 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) ""))
+(*val string_of_elf32_symbol_table : elf32_symbol_table -> string*)
+let string_of_elf32_symbol_table symtab =  
+(unlines (List.map string_of_elf32_symbol_table_entry symtab))
+
+type 'a hasElf32SymbolTable_class={
+  get_elf32_symbol_table_method : 'a -> elf32_symbol_table
+}
+
+(*val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring)*)
+let read_elf32_symbol_table_entry endian bs0 =  
+(Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_name, bs0) ->
+  Ml_bindings.read_elf32_addr endian bs0 >>= (fun (st_value, bs0) ->
+  Ml_bindings.read_elf32_word endian bs0 >>= (fun (st_size, bs0) ->
+  Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) ->
+  Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) ->
+  Ml_bindings.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 read_elf32_symbol_table : endianness -> bitstring -> error elf32_symbol_table*)
+let rec read_elf32_symbol_table endian bs0 =  
+(if Bitstring.bitstring_length bs0 = 0 then
+    return []
+  else
+    read_elf32_symbol_table_entry endian bs0 >>= (fun (head, bs0) ->
+    read_elf32_symbol_table endian bs0 >>= (fun tail ->
+    return (head::tail))))
+
+(** ELF64 symbol table type *)
+
+type elf64_symbol_table_entry =
+  { elf64_st_name  : Uint32.t
+   ; elf64_st_info  : Uint32.t
+   ; elf64_st_other : Uint32.t
+   ; elf64_st_shndx : Uint32.t
+   ; elf64_st_value : Uint64.t
+   ; elf64_st_size  : Uint64.t
+   }
+
+(*val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string*)
+let string_of_elf64_symbol_table_entry entry =  
+(unlines [    
+("\t" ^ ("Name: "  ^ Uint32.to_string entry.elf64_st_name))
+  ; ("\t" ^ ("Info: "  ^ Uint32.to_string entry.elf64_st_info))
+  ; ("\t" ^ ("Other: " ^ Uint32.to_string entry.elf64_st_other))
+  ; ("\t" ^ ("Shndx: " ^ Uint32.to_string entry.elf64_st_shndx))
+  ; ("\t" ^ ("Value: " ^ Uint64.to_string entry.elf64_st_value))
+  ; ("\t" ^ ("Size: "  ^ Uint64.to_string entry.elf64_st_size))
+  ])
+
+type elf64_symbol_table = elf64_symbol_table_entry list
+
+(*val string_of_elf64_symbol_table : elf64_symbol_table -> string*)
+let string_of_elf64_symbol_table symtab =  
+(unlines (List.map string_of_elf64_symbol_table_entry symtab))
+
+type 'a hasElf64SymbolTable_class={
+  get_elf64_symbol_table_method : 'a -> elf64_symbol_table
+}
+
+(*val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring)*)
+let read_elf64_symbol_table_entry endian bs0 =  
+(Ml_bindings.read_elf64_word endian bs0 >>= (fun (st_name, bs0) ->
+  Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_info, bs0) ->
+  Ml_bindings.read_unsigned_char endian bs0 >>= (fun (st_other, bs0) ->
+  Ml_bindings.read_elf64_half endian bs0 >>= (fun (st_shndx, bs0) ->
+  Ml_bindings.read_elf64_addr endian bs0 >>= (fun (st_value, bs0) ->
+  Ml_bindings.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 read_elf64_symbol_table : endianness -> bitstring -> error elf64_symbol_table*)
+let rec read_elf64_symbol_table endian bs0 =  
+(if Bitstring.bitstring_length bs0 = 0 then
+    return []
+  else
+    read_elf64_symbol_table_entry endian bs0 >>= (fun (head, bs0) ->
+    read_elf64_symbol_table endian bs0 >>= (fun tail ->
+    return (head::tail))))
+
+(*val get_elf32_symbol_image_address : elf32_symbol_table -> string_table -> error (list (string * nat))*)
+let get_elf32_symbol_image_address symtab strtab =  
+(mapM (fun entry ->
+    let name = (Uint32.to_int entry.elf32_st_name) in
+    let addr = (Uint32.to_int entry.elf32_st_value) in
+      String_table.get_string_at name strtab >>= (fun str ->
+      return (str, addr))
+  ) symtab)
+
+(*val get_elf64_symbol_image_address : elf64_symbol_table -> string_table -> error (list (string * nat))*)
+let get_elf64_symbol_image_address symtab strtab =  
+(mapM (fun entry ->
+    let name = (Uint32.to_int entry.elf64_st_name) in
+    let addr = (Uint64.to_int entry.elf64_st_value) in
+      String_table.get_string_at name strtab >>= (fun str ->
+      return (str, addr))
+  ) symtab)
\ No newline at end of file