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

1 files changed, 306 insertions, 0 deletions

diff --git a/src/elf_model/elf_program_header_table.lem b/src/elf_model/elf_program_header_table.lem
new file mode 100644
index 00000000..ad97d566
--- /dev/null
+++ b/src/elf_model/elf_program_header_table.lem
@@ -0,0 +1,306 @@
+open import Basic_classes
+open import Bool
+open import Function
+open import List
+open import Maybe
+open import Num
+open import String
+
+open import Elf_types
+open import Endianness
+
+open import Bitstring
+open import Error
+open import Missing_pervasives
+open import Show
+
+(** Segment types
+  *
+  * FIXME: Bug in Lem as Lem codebase uses [int] type throughout where [BigInt.t]
+  * is really needed, hence chokes on huge constants below, which is why they are
+  * written in the way that they are.
+  *)
+
+(** Unused array element.  All other members of the structure are undefined. *)
+let elf_pt_null : nat = 0
+(** A loadable segment. *)
+let elf_pt_load : nat = 1
+(** Dynamic linking information. *)
+let elf_pt_dynamic : nat = 2
+(** Specifies the location and size of a null-terminated path name to be used to
+  * invoke an interpreter.
+  *)
+let elf_pt_interp : nat = 3
+(** Specifies location and size of auxiliary information. *)
+let elf_pt_note : nat = 4
+(** Reserved but with unspecified semantics.  If the file contains a segment of
+  * this type then it is to be regarded as non-conformant with the ABI.
+  *)
+let elf_pt_shlib : nat = 5
+(** Specifies the location and size of the program header table. *)
+let elf_pt_phdr : nat = 6
+(** Specifies the thread local storage (TLS) template.  Need not be supported. *)
+let elf_pt_tls : nat = 7
+(** Start of reserved indices for operating system specific semantics. *)
+let elf_pt_loos : nat = 128 * 128 * 128 * 256 * 3 (* 1610612736 (* 0x60000000 *) *)
+(** End of reserved indices for operating system specific semantics. *)
+let elf_pt_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *)
+(** Start of reserved indices for processor specific semantics. *)
+let elf_pt_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *)
+(** End of reserved indices for processor specific semantics. *)
+let elf_pt_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *)
+
+(** [string_of_elf_segment_type os proc st] produces a string representation of
+  * the coding of an ELF segment type [st] using [os] and [proc] to render OS-
+  * and processor-specific codings.
+  *)
+val string_of_elf_segment_type : (nat -> string) -> (nat -> string) -> nat -> string
+let string_of_elf_segment_type os proc pt =
+	if pt = elf_pt_null then
+		"PT_NULL"
+	else if pt = elf_pt_load then
+		"PT_LOAD"
+	else if pt = elf_pt_dynamic then
+		"PT_DYNAMIC"
+	else if pt = elf_pt_interp then
+		"PT_INTERP"
+	else if pt = elf_pt_note then
+		"PT_NOTE"
+	else if pt = elf_pt_shlib then
+		"PT_SHLIB"
+	else if pt = elf_pt_phdr then
+		"PT_PHDR"
+	else if pt = elf_pt_tls then
+		"PT_TLS"
+	else if pt >= elf_pt_loos && pt <= elf_pt_hios then
+		os pt
+	else if pt >= elf_pt_loproc && pt <= elf_pt_hiproc then
+		proc pt
+	else
+		"Undefined or invalid segment type"
+
+(** Program header table entry type *)
+
+(** Type [elf32_program_header_table_entry] encodes a program header table entry
+  * for 32-bit platforms.  Each entry describes a segment in an executable or
+  * shared object file.
+  *)
+type elf32_program_header_table_entry =
+  <| elf32_p_type   : elf32_word (** Type of the segment *)
+   ; elf32_p_offset : elf32_off  (** Offset from beginning of file for segment *)
+   ; elf32_p_vaddr  : elf32_addr (** Virtual address for segment in memory *)
+   ; elf32_p_paddr  : elf32_addr (** Physical address for segment *)
+   ; elf32_p_filesz : elf32_word (** Size of segment in file, in bytes *)
+   ; elf32_p_memsz  : elf32_word (** Size of segment in memory image, in bytes *)
+   ; elf32_p_flags  : elf32_word (** Segment flags *)
+   ; elf32_p_align  : elf32_word (** Segment alignment memory for memory and file *)
+   |>
+
+(** Type [elf64_program_header_table_entry] encodes a program header table entry
+  * for 64-bit platforms.  Each entry describes a segment in an executable or
+  * shared object file.
+  *)
+type elf64_program_header_table_entry =
+  <| elf64_p_type   : elf64_word  (** Type of the segment *)
+   ; elf64_p_flags  : elf64_word  (** Segment flags *)
+   ; elf64_p_offset : elf64_off   (** Offset from beginning of file for segment *)
+   ; elf64_p_vaddr  : elf64_addr  (** Virtual address for segment in memory *)
+   ; elf64_p_paddr  : elf64_addr  (** Physical address for segment *)
+   ; elf64_p_filesz : elf64_xword (** Size of segment in file, in bytes *)
+   ; elf64_p_memsz  : elf64_xword (** Size of segment in memory image, in bytes *)
+   ; elf64_p_align  : elf64_xword (** Segment alignment memory for memory and file *)
+   |>
+  
+(** [string_of_elf32_program_header_table_entry os proc et] produces a string
+  * representation of a 32-bit program header table entry using [os] and [proc]
+  * to render OS- and processor-specific entries.
+  *)
+val string_of_elf32_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf32_program_header_table_entry -> string
+let string_of_elf32_program_header_table_entry os proc entry =
+	unlines [
+		"\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf32_word entry.elf32_p_type)
+	; "\t" ^ "Offset: " ^ show entry.elf32_p_offset
+	; "\t" ^ "Virtual address: " ^ show entry.elf32_p_vaddr
+	; "\t" ^ "Physical address: " ^ show entry.elf32_p_paddr
+	; "\t" ^ "Segment size (bytes): " ^ show entry.elf32_p_filesz
+	; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf32_p_memsz
+	; "\t" ^ "Flags: " ^ show entry.elf32_p_flags
+  ; "\t" ^ "Alignment: " ^ show entry.elf32_p_align
+	]
+
+(** [string_of_elf64_program_header_table_entry os proc et] produces a string
+  * representation of a 64-bit program header table entry using [os] and [proc]
+  * to render OS- and processor-specific entries.
+  *)
+val string_of_elf64_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf64_program_header_table_entry -> string
+let string_of_elf64_program_header_table_entry os proc entry =
+  unlines [
+    "\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf64_word entry.elf64_p_type)
+  ; "\t" ^ "Offset: " ^ show entry.elf64_p_offset
+  ; "\t" ^ "Virtual address: " ^ show entry.elf64_p_vaddr
+  ; "\t" ^ "Physical address: " ^ show entry.elf64_p_paddr
+  ; "\t" ^ "Segment size (bytes): " ^ show entry.elf64_p_filesz
+  ; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf64_p_memsz
+  ; "\t" ^ "Flags: " ^ show entry.elf64_p_flags
+  ; "\t" ^ "Alignment: " ^ show entry.elf64_p_align
+  ]
+
+(** [string_of_elf32_program_header_table_entry_default et] produces a string representation
+  * of table entry [et] where OS- and processor-specific entries are replaced with
+  * default strings.
+  *)
+val string_of_elf32_program_header_table_entry_default : elf32_program_header_table_entry -> string
+let string_of_elf32_program_header_table_entry_default =
+	string_of_elf32_program_header_table_entry
+    (const "*Default OS specific print*")
+      (const "*Default processor specific print*")
+
+(** [string_of_elf64_program_header_table_entry_default et] produces a string representation
+  * of table entry [et] where OS- and processor-specific entries are replaced with
+  * default strings.
+  *)
+val string_of_elf64_program_header_table_entry_default : elf64_program_header_table_entry -> string
+let string_of_elf64_program_header_table_entry_default =
+  string_of_elf64_program_header_table_entry
+    (const "*Default OS specific print*")
+      (const "*Default processor specific print*")
+	
+instance (Show elf32_program_header_table_entry)
+	let show = string_of_elf32_program_header_table_entry_default
+end
+
+instance (Show elf64_program_header_table_entry)
+  let show = string_of_elf64_program_header_table_entry_default
+end
+
+(** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table
+  * entry from bitstring [bs0] assuming endianness [endian].  If [bs0] is larger
+  * than necessary, the excess is returned from the function, too.
+  *)
+val read_elf32_program_header_table_entry : endianness -> bitstring -> error (elf32_program_header_table_entry * bitstring)
+let read_elf32_program_header_table_entry endian bs =
+	read_elf32_word endian bs >>= fun (typ, bs) ->
+	read_elf32_off  endian bs >>= fun (offset, bs) ->
+	read_elf32_addr endian bs >>= fun (vaddr, bs) ->
+	read_elf32_addr endian bs >>= fun (paddr, bs) ->
+	read_elf32_word endian bs >>= fun (filesz, bs) ->
+	read_elf32_word endian bs >>= fun (memsz, bs) ->
+	read_elf32_word endian bs >>= fun (flags, bs) ->
+	read_elf32_word endian bs >>= fun (align, bs) ->
+		return (<| elf32_p_type = typ; elf32_p_offset = offset;
+                elf32_p_vaddr = vaddr; elf32_p_paddr = paddr;
+                elf32_p_filesz = filesz; elf32_p_memsz = memsz;
+                elf32_p_flags = flags; elf32_p_align = align |>, bs)
+
+val read_elf64_program_header_table_entry : endianness -> bitstring -> error (elf64_program_header_table_entry * bitstring)
+let read_elf64_program_header_table_entry endian bs =
+  read_elf64_word endian bs >>= fun (typ, bs) ->
+  read_elf64_word endian bs >>= fun (flags, bs) ->
+  read_elf64_off  endian bs >>= fun (offset, bs) ->
+  read_elf64_addr endian bs >>= fun (vaddr, bs) ->
+  read_elf64_addr endian bs >>= fun (paddr, bs) ->
+  read_elf64_xword endian bs >>= fun (filesz, bs) ->
+  read_elf64_xword endian bs >>= fun (memsz, bs) ->
+  read_elf64_xword endian bs >>= fun (align, bs) ->
+    return (<| elf64_p_type = typ; elf64_p_offset = offset;
+                elf64_p_vaddr = vaddr; elf64_p_paddr = paddr;
+                elf64_p_filesz = filesz; elf64_p_memsz = memsz;
+                elf64_p_flags = flags; elf64_p_align = align |>, bs)
+
+(** Program header table type *)
+
+(** Type [elf32_program_header_table] represents a program header table for 32-bit
+  * ELF files.  A program header table is an array (implemented as a list, here)
+  * of program header table entries.
+  *)
+type elf32_program_header_table =
+  list elf32_program_header_table_entry
+
+class (HasElf32ProgramHeaderTable 'a)
+  val get_elf32_program_header_table : 'a -> maybe elf32_program_header_table
+end
+
+(** Type [elf64_program_header_table] represents a program header table for 64-bit
+  * ELF files.  A program header table is an array (implemented as a list, here)
+  * of program header table entries.
+  *)
+type elf64_program_header_table =
+  list elf64_program_header_table_entry
+
+class (HasElf64ProgramHeaderTable 'a)
+  val get_elf64_program_header_table : 'a -> maybe elf64_program_header_table
+end
+
+(** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from
+  * bitstring [bs0] assuming endianness [endian].  The bitstring [bs0] is assumed
+  * to have exactly the correct size for the table.  For internal use, only.  Use
+  * [read_elf32_program_header_table] below instead.
+  *)
+let rec read_elf32_program_header_table' endian bs0 =
+	if length bs0 = 0 then
+  	return []
+  else
+  	read_elf32_program_header_table_entry endian bs0 >>= fun (entry, bs1) ->
+    read_elf32_program_header_table' endian bs1 >>= fun tail ->
+    return (entry::tail)
+
+(** [read_elf64_program_header_table' endian bs0] reads an ELF64 program header table from
+  * bitstring [bs0] assuming endianness [endian].  The bitstring [bs0] is assumed
+  * to have exactly the correct size for the table.  For internal use, only.  Use
+  * [read_elf32_program_header_table] below instead.
+  *)
+let rec read_elf64_program_header_table' endian bs0 =
+  if length bs0 = 0 then
+    return []
+  else
+    read_elf64_program_header_table_entry endian bs0 >>= fun (entry, bs1) ->
+    read_elf64_program_header_table' endian bs1 >>= fun tail ->
+    return (entry::tail)
+
+(** [read_elf32_program_header_table table_size endian bs0] reads an ELF32 program header
+  * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
+  * This [table_size] argument should be equal to the number of entries in the
+  * table multiplied by the fixed entry size.  Bitstring [bs0] may be larger than
+  * necessary, in which case the excess is returned.
+  *)
+val read_elf32_program_header_table : nat -> endianness -> bitstring -> error (elf32_program_header_table * bitstring)
+let read_elf32_program_header_table table_size endian bs0 =
+	let (eat, rest) = partition table_size bs0 in
+		read_elf32_program_header_table' endian eat >>= fun table ->
+		return (table, rest)
+
+(** [read_elf64_program_header_table table_size endian bs0] reads an ELF64 program header
+  * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
+  * This [table_size] argument should be equal to the number of entries in the
+  * table multiplied by the fixed entry size.  Bitstring [bs0] may be larger than
+  * necessary, in which case the excess is returned.
+  *)
+val read_elf64_program_header_table : nat -> endianness -> bitstring -> error (elf64_program_header_table * bitstring)
+let read_elf64_program_header_table table_size endian bs0 =
+  let (eat, rest) = partition table_size bs0 in
+    read_elf64_program_header_table' endian eat >>= fun table ->
+    return (table, rest)
+
+(** The [pht_print_bundle] type is used to tidy up other type signatures.  Some of the
+  * top-level string_of_ functions require six or more functions passed to them,
+  * which quickly gets out of hand.  This type is used to reduce that complexity.
+  * The first component of the type is an OS specific print function, the second is
+  * a processor specific print function.
+  *)
+type pht_print_bundle = (nat -> string) * (nat -> string)
+
+(** [string_of_elf32_program_header_table os proc tbl] produces a string representation
+  * of program header table [tbl] using [os] and [proc] to render OS- and processor-
+  * specific entries.
+  *)
+val string_of_elf32_program_header_table : pht_print_bundle -> elf32_program_header_table -> string
+let string_of_elf32_program_header_table (os, proc) tbl =
+  unlines (List.map (string_of_elf32_program_header_table_entry os proc) tbl)
+
+(** [string_of_elf64_program_header_table os proc tbl] produces a string representation
+  * of program header table [tbl] using [os] and [proc] to render OS- and processor-
+  * specific entries.
+  *)
+val string_of_elf64_program_header_table : pht_print_bundle -> elf64_program_header_table -> string
+let string_of_elf64_program_header_table (os, proc) tbl =
+  unlines (List.map (string_of_elf64_program_header_table_entry os proc) tbl)