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

1 files changed, 298 insertions, 0 deletions

diff --git a/src/elf_model/elf_section_header.ml b/src/elf_model/elf_section_header.ml
new file mode 100644
index 00000000..1a73d35f
--- /dev/null
+++ b/src/elf_model/elf_section_header.ml
@@ -0,0 +1,298 @@
+(*Generated by Lem from elf_section_header.lem.*)
+open Lem_basic_classes
+open Lem_bool
+open Lem_list
+open Lem_num
+open Lem_string
+
+open Bitstring
+open Error
+open Elf_types
+open Show
+
+(** Special section indices. *)
+
+(** [shn_undef]: marks an undefined, missing or irrelevant section reference.
+  *)
+let shn_undef : int =( 0)
+(** [shn_loreserve]: this specifies the lower bound of the range of reserved
+  * indices.
+  *)
+let shn_loreserve : int =( 65280) (* 0xff00 *)
+(** [shn_loproc]: start of the range reserved for processor-specific semantics.
+  *)
+let shn_loproc : int =( 65280) (* 0xff00 *)
+(** [shn_hiproc]: end of the range reserved for processor-specific semantics.
+  *)
+let shn_hiproc : int =( 65311) (* 0xff1f *)
+(** [shn_loos]: start of the range reserved for operating system-specific
+  * semantics.
+  *)
+let shn_loos : int =( 65312) (* 0xff20 *)
+(** [shn_hios]: end of the range reserved for operating system-specific
+  * semantics.
+  *)
+let shn_hios : 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 : int =( 65521) (* 0xfff1 *)
+(** [shn_common]: symbols defined relative to this index are common symbols,
+  * such as unallocated C external variables.
+  *)
+let shn_common : int =( 65522) (* 0xfff2 *)
+(** [shn_xindex]: an escape value.  It indicates the actual section header index
+  * is too large to fit in the containing field and is located in another
+  * location (specific to the structure where it appears).
+  *)
+let shn_xindex : int =( 65535) (* 0xffff *)
+(** [shn_hireserve]: specifies the upper-bound of reserved values.
+  *)
+let shn_hireserve : int =( 65535) (* 0xffff *)
+
+(*val string_of_special_section_index : nat -> string*)
+let string_of_special_section_index i =  
+(if i = shn_undef then
+    "SHN_UNDEF"
+  else if i = shn_loreserve then
+    "SHN_LORESERVE"
+  else if (i >= shn_loproc) && (i <= shn_hiproc) then
+    "SHN_PROCESSOR_SPECIFIC"
+  else if (i >= shn_loos) && (i <= shn_hios) then
+    "SHN_OS_SPECIFIC"
+  else if i = shn_abs then
+    "SHN_ABS"
+  else if i = shn_common then
+    "SHN_COMMON"
+  else if i = shn_xindex then
+    "SHN_XINDEX"
+  else if i = shn_hireserve then
+    "SHN_HIRESERVE"
+  else
+  	"SHN UNDEFINED")
+
+(** Section types. *)
+
+(** Marks the section header as being inactive. *)
+let sht_null : int =( 0)
+(** Section holds information defined by the program. *)
+let sht_progbits : 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 : int =( 2)
+let sht_dynsym : int =( 11)
+(** Section holds a string table *)
+let sht_strtab : int =( 3)
+(** Section holds relocation entries with explicit addends.  An object file may
+  * have multiple section of this type.
+  *)
+let sht_rela : int =( 4)
+(** Section holds a symbol hash table.  An object file may only have a single
+  * hash table.
+  *)
+let sht_hash : int =( 5)
+(** Section holds information for dynamic linking.  An object file may only have
+  * a single dynamic section.
+  *)
+let sht_dynamic : int =( 6)
+(** Section holds information that marks the file in some way. *)
+let sht_note : int =( 7)
+(** Section occupies no space in the file but otherwise resembles a progbits
+  * section.
+  *)
+let sht_nobits : int =( 8)
+(** Section holds relocation entries without explicit addends.  An object file
+  * may have multiple section of this type.
+  *)
+let sht_rel : int =( 9)
+(** Section type is reserved but has an unspecified meaning. *)
+let sht_shlib : 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 : 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 : 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 : 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 : 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.
+  *)
+let sht_symtab_shndx : int =( 18)
+(** XXX: broken for the time being due to Lem bug. *)
+let sht_loos : int =( 0)
+let sht_hios : int =( 0)
+let sht_loproc : int =( 0)
+let sht_hiproc : int =( 0)
+let sht_louser : int =( 0)
+let sht_hiuser : int =( 0)
+(* XXX: constants too big for Lem to parse, apparently!
+let sht_loos : nat = 1610612736 (* 0x60000000 *)
+let sht_hios : nat = 1879048191 (* 0x6fffffff *)
+let sht_loproc : nat = 1879048192 (* 0x70000000 *)
+let sht_hiproc : nat = 2147483647 (* 0x7fffffff *)
+let sht_louser : nat = 2147483648 (* 0x80000000 *)
+let sht_hiuser : nat = 2415919103 (* 0x8fffffff *)
+*)
+
+let string_of_section_type i =  
+(if i = sht_null then
+    "SHT_NULL"
+  else if i = sht_progbits then
+    "SHT_PROGBITS"
+  else if i = sht_symtab then
+    "SHT_SYMTAB"
+  else if i = sht_strtab then
+    "SHT_STRTAB"
+  else if i = sht_rela then
+    "SHT_RELA"
+  else if i = sht_hash then
+    "SHT_HASH"
+  else if i = sht_dynamic then
+    "SHT_DYNAMIC"
+  else if i = sht_note then
+    "SHT_NOTE"
+  else if i = sht_nobits then
+    "SHT_NOBITS"
+  else if i = sht_rel then
+    "SHT_REL"
+  else if i = sht_shlib then
+    "SHT_SHLIB"
+  else if i = sht_dynsym then
+    "SHT_DYNSYM"
+  else if i = sht_init_array then
+    "SHT_INIT_ARRAY"
+  else if i = sht_fini_array then
+    "SHT_FINI_ARRAY"
+  else if i = sht_preinit_array then
+    "SHT_PREINIT_ARRAY"
+  else if i = sht_group then
+    "SHT_GROUP"
+  else if i = sht_symtab_shndx then
+    "SHT_SYMTAB_SHNDX"
+  else if (i >= sht_loos) && (i <= sht_hios) then
+    "SHT_OS_SPECIFIC"  
+  else if (i >= sht_loproc) && (i <= sht_hiproc) then
+    "SHT_PROCESSOR_SPECIFIC"
+  else if (i >= sht_louser) && (i <= sht_hiuser) then
+    "SHT_USER_SPECIFIC"
+  else
+    "SHT UNDEFINED")
+
+(** Section header table entry type. *)
+
+type elf32_section_header_table_entry =
+  { elf32_sh_name      : Int64.t
+   ; elf32_sh_type      : Int64.t
+   ; elf32_sh_flags     : Int64.t
+   ; elf32_sh_addr      : Int64.t
+   ; elf32_sh_offset    : Int64.t
+   ; elf32_sh_size      : Int64.t
+   ; elf32_sh_link      : Int64.t
+   ; elf32_sh_info      : Int64.t
+   ; elf32_sh_addralign : Int64.t
+   ; elf32_sh_entsize   : Int64.t
+   }
+
+let read_elf32_section_header_table_entry (bs : Bitstring.bitstring) =	
+(Ml_bindings.read_elf32_word bs >>= (fun (sh_name, bs) ->
+	Ml_bindings.read_elf32_word bs >>= (fun (sh_type, bs) ->
+	Ml_bindings.read_elf32_word bs >>= (fun (sh_flags, bs) ->
+	Ml_bindings.read_elf32_addr bs >>= (fun (sh_addr, bs) ->
+	Ml_bindings.read_elf32_off bs >>= (fun (sh_offset, bs) ->
+	Ml_bindings.read_elf32_word bs >>= (fun (sh_size, bs) ->
+	Ml_bindings.read_elf32_word bs >>= (fun (sh_link, bs) ->
+	Ml_bindings.read_elf32_word bs >>= (fun (sh_info, bs) ->
+	Ml_bindings.read_elf32_word bs >>= (fun (sh_addralign, bs) ->
+	Ml_bindings.read_elf32_word 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
+			 })))))))))))
+
+let string_of_elf32_section_header_table_entry entry =  
+(List.fold_right (^) [
+    "\t"; "Name: "; Int64.to_string entry.elf32_sh_name
+  ; "\t"; "Type: "; string_of_section_type (Int64.to_int entry.elf32_sh_type)
+  ; "\n\t"; "Flags: "; Int64.to_string entry.elf32_sh_flags
+  ; "\t"; "Address: "; Int64.to_string entry.elf32_sh_addr
+  ; "\t"; "Size: "; Int64.to_string entry.elf32_sh_size; "\n\n"
+  ] "")
+  
+let instance_Show_Show_Elf_section_header_elf32_section_header_table_entry_dict =({
+
+  show_method = string_of_elf32_section_header_table_entry})
+
+(** Section header table type. *)
+
+type elf32_section_header_table = elf32_section_header_table_entry list
+;;
+
+let rec read_elf32_section_header_table' entry_size bitstring0 =  
+(if Bitstring.bitstring_length bitstring0 = 0 then
+    return []
+  else
+    let (eat, rest) = (Utility.partition_bitstring entry_size bitstring0) in
+      read_elf32_section_header_table_entry eat >>= (fun sect ->
+      read_elf32_section_header_table' entry_size rest     >>= (fun tail ->
+      return (sect::tail))))
+
+(*val read_elf32_section_header_table : nat -> nat -> nat -> bitstring -> error (elf32_section_header_table * bitstring)*)
+let read_elf32_section_header_table size entry_size offset bitstring0 =	
+(let (prefix, relevant) = (Utility.partition_bitstring offset bitstring0) in
+  let (eat, rest) = (Utility.partition_bitstring (size * entry_size) relevant) in
+  	read_elf32_section_header_table' entry_size eat >>= (fun entries ->
+    return (entries, rest)))
+;;
+
+(*val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool*)
+let elf32_size_correct hdr tbl =  
+((match Int64.to_int hdr.elf32_sh_size with
+    | 0 -> true
+    | m -> m = List.length tbl
+  ))
+;;
+
+(*val is_valid_elf32_section_header_table : elf32_section_header_table -> bool*)
+let is_valid_elf32_section_header_table tbl =  
+((match tbl with
+    | []    -> false
+    | x::xs ->        
+(Int64.to_int x.elf32_sh_name = 0) &&
+        ((Int64.to_int x.elf32_sh_type = sht_null) &&
+        ((Int64.to_int x.elf32_sh_flags = 0) &&
+        ((Int64.to_int x.elf32_sh_addr = 0) &&
+        ((Int64.to_int x.elf32_sh_offset = 0) &&
+        ((Int64.to_int x.elf32_sh_info = 0) &&
+        ((Int64.to_int x.elf32_sh_addralign = 0) &&
+        ((Int64.to_int x.elf32_sh_entsize = 0) &&
+        elf32_size_correct x tbl)))))))
+        (* XXX: more correctness criteria in time *)
+  ))
+  
+let string_of_elf32_section_header_table (tbl : elf32_section_header_table) : string =	
+("Section header table:" ^ ("\n" ^
+		List.fold_right (^) (List.map string_of_elf32_section_header_table_entry tbl) ""))