Add in elf model from Dominic/Stephen. Make run_power build again. Does not effectively use elf model yet

1 files changed, 246 insertions, 0 deletions

diff --git a/src/elf_model/elf_symbol_table.ml b/src/elf_model/elf_symbol_table.ml
new file mode 100644
index 00000000..a2fed159
--- /dev/null
+++ b/src/elf_model/elf_symbol_table.ml
@@ -0,0 +1,246 @@
+(*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) ""))