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

1 files changed, 87 insertions, 0 deletions

diff --git a/src/elf_model/string_table.lem b/src/elf_model/string_table.lem
new file mode 100644
index 00000000..8cfe5056
--- /dev/null
+++ b/src/elf_model/string_table.lem
@@ -0,0 +1,87 @@
+open import List
+open import Maybe
+open import Num
+open import String
+
+open import Error
+open import Missing_pervasives
+open import Show
+
+type string_table
+  = Strings of (char * string)
+
+(** [mk_string_table base sep] constructs a string table using [base] as the
+  * base string and [sep] as the delimiting character to use to split [base]
+  * when trying to access the string stored in the table using the functions below.
+  *)
+val mk_string_table : string -> char -> string_table
+let mk_string_table base sep =
+  Strings (sep, base)
+
+(** [empty] is the empty string table with an arbitrary choice of delimiter.
+  *)
+val empty : string_table
+let empty = Strings (Missing_pervasives.null_char, "")
+
+(** [get_delimiating_character tbl] returns the delimiting character associated
+  * with the string table [tbl], used to split the strings.
+  *)
+val get_delimiting_character : string_table -> char
+let get_delimiting_character tbl =
+  match tbl with
+    | Strings (sep, base) -> sep
+  end
+
+(** [get_base_string tbl] returns the base string of the string table [tbl].
+  *)
+val get_base_string : string_table -> string
+let get_base_string tbl =
+  match tbl with
+    | Strings (sep, base) -> base
+  end
+
+(** [get_strings tbl] obtains the strings stored in the table, separated using
+  * the designated separator as a delimiting character.
+  *)
+val get_strings : string_table -> list string
+let get_strings tbl =
+  match tbl with
+    | Strings (sep, base) ->
+        Missing_pervasives.split_string_on_char base sep
+  end
+
+(** [size tbl] returns the number of strings separated by the designated
+  * separator in the string table [tbl].
+  *)
+val size : string_table -> nat
+let size tbl =
+  List.length (get_strings tbl)
+
+(** [get_string_at index tbl] returns the string starting at character [index]
+  * from the start of the base string until the first occurrence of the delimiting
+  * character.
+  *)
+val get_string_at : nat -> string_table -> error string
+let get_string_at index tbl =
+  match Missing_pervasives.string_suffix index (get_base_string tbl) with
+    | Nothing     -> Fail "get_string_at: invalid index into string"
+    | Just suffix ->
+        let delim = get_delimiting_character tbl in
+        let tbl   = mk_string_table suffix delim in
+          match get_strings tbl with
+            | []    -> Fail "get_string_at: empty string returned"
+            | x::xs -> return x
+          end
+  end
+
+class (HasElf32SectionHeaderStringTable 'a)
+  val get_elf32_section_header_string_table : 'a -> string_table
+end
+
+class (HasElf64SectionHeaderStringTable 'a)
+  val get_elf64_section_header_string_table : 'a -> string_table
+end
+
+instance (Show string_table)
+  let show tbl = unlines (get_strings tbl)
+end
\ No newline at end of file