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

1 files changed, 249 insertions, 0 deletions

diff --git a/src/elf_model/elf_symbol_table.lem b/src/elf_model/elf_symbol_table.lem
new file mode 100644
index 00000000..54521157
--- /dev/null
+++ b/src/elf_model/elf_symbol_table.lem
@@ -0,0 +1,249 @@
+open import Basic_classes
+open import Bool
+open import List
+open import Maybe
+open import String
+open import Tuple
+
+open import Bitstring
+open import Error
+open import Missing_pervasives
+open import Show
+
+open import Elf_types
+open import Endianness
+open import String_table
+
+(** Undefined symbol index *)
+
+let stn_undef : nat = 0
+
+(** Symbol binding *)
+
+let stb_local : nat = 0
+let stb_global : nat = 1
+let stb_weak : nat = 2
+let stb_loos : nat = 10
+let stb_hios : nat = 12
+let stb_loproc : nat = 13
+let stb_hiproc : nat = 15
+
+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 *)
+
+let stt_notype : nat = 0
+let stt_object : nat = 1
+let stt_func : nat = 2
+let stt_section : nat = 3
+let stt_file : nat = 4
+let stt_common : nat = 5
+let stt_tls : nat = 6
+let stt_loos : nat = 10
+let stt_hios : nat = 12
+let stt_loproc : nat = 13
+let stt_hiproc : nat = 15
+
+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 : nat = 0
+let stv_internal : nat = 1
+let stv_hidden : nat = 2
+let stv_protected : nat = 3
+
+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  : elf32_word
+   ; elf32_st_value : elf32_addr
+   ; elf32_st_size  : elf32_word
+   ; elf32_st_info  : unsigned_char
+   ; elf32_st_other : unsigned_char
+   ; elf32_st_shndx : elf32_half
+   |>
+
+(** 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 =
+  nat_of_unsigned_char (unsigned_char_rshift entry 4)
+
+val get_symbol_type : unsigned_char -> nat
+let get_symbol_type entry =
+  nat_of_unsigned_char (unsigned_char_land entry (unsigned_char_of_nat 15)) (* 0xf *)
+
+val get_symbol_info : unsigned_char -> unsigned_char -> nat
+let get_symbol_info entry0 entry1 =
+  nat_of_unsigned_char (unsigned_char_plus
+    (unsigned_char_lshift entry0 4) (unsigned_char_land entry1
+      (unsigned_char_of_nat 15))) (*0xf*)  
+
+val get_symbol_visibility : unsigned_char -> nat
+let get_symbol_visibility entry =
+  nat_of_unsigned_char (unsigned_char_land entry (unsigned_char_of_nat 3)) (* 0x3*)
+
+type symtab_print_bundle = (nat -> string) * (nat -> string)
+
+val string_of_elf32_symbol_table_entry : elf32_symbol_table_entry -> string
+let string_of_elf32_symbol_table_entry entry =
+  unlines [
+    "\t" ^ "Name: "  ^ show entry.elf32_st_name
+  ; "\t" ^ "Value: " ^ show entry.elf32_st_value
+  ; "\t" ^ "Size: "  ^ show entry.elf32_st_size
+  ; "\t" ^ "Info: "  ^ show entry.elf32_st_info
+  ; "\t" ^ "Other: " ^ show entry.elf32_st_other
+  ; "\t" ^ "Shndx: " ^ show entry.elf32_st_shndx
+  ]
+
+type elf32_symbol_table = list elf32_symbol_table_entry
+
+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)
+
+class (HasElf32SymbolTable 'a)
+  val get_elf32_symbol_table : 'a -> elf32_symbol_table
+end
+
+val read_elf32_symbol_table_entry : endianness -> bitstring -> error (elf32_symbol_table_entry * bitstring)
+let read_elf32_symbol_table_entry endian bs0 =
+  read_elf32_word endian bs0 >>= fun (st_name, bs0) ->
+  read_elf32_addr endian bs0 >>= fun (st_value, bs0) ->
+  read_elf32_word endian bs0 >>= fun (st_size, bs0) ->
+  read_unsigned_char endian bs0 >>= fun (st_info, bs0) ->
+  read_unsigned_char endian bs0 >>= fun (st_other, bs0) ->
+  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 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  : elf64_word
+   ; elf64_st_info  : unsigned_char
+   ; elf64_st_other : unsigned_char
+   ; elf64_st_shndx : elf64_half
+   ; elf64_st_value : elf64_addr
+   ; elf64_st_size  : elf64_xword
+   |>
+
+val string_of_elf64_symbol_table_entry : elf64_symbol_table_entry -> string
+let string_of_elf64_symbol_table_entry entry =
+  unlines [
+    "\t" ^ "Name: "  ^ show entry.elf64_st_name
+  ; "\t" ^ "Info: "  ^ show entry.elf64_st_info
+  ; "\t" ^ "Other: " ^ show entry.elf64_st_other
+  ; "\t" ^ "Shndx: " ^ show entry.elf64_st_shndx
+  ; "\t" ^ "Value: " ^ show entry.elf64_st_value
+  ; "\t" ^ "Size: "  ^ show entry.elf64_st_size
+  ]
+
+type elf64_symbol_table = list elf64_symbol_table_entry
+
+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)
+
+class (HasElf64SymbolTable 'a)
+  val get_elf64_symbol_table : 'a -> elf64_symbol_table
+end
+
+val read_elf64_symbol_table_entry : endianness -> bitstring -> error (elf64_symbol_table_entry * bitstring)
+let read_elf64_symbol_table_entry endian bs0 =
+  read_elf64_word endian bs0 >>= fun (st_name, bs0) ->
+  read_unsigned_char endian bs0 >>= fun (st_info, bs0) ->
+  read_unsigned_char endian bs0 >>= fun (st_other, bs0) ->
+  read_elf64_half endian bs0 >>= fun (st_shndx, bs0) ->
+  read_elf64_addr endian bs0 >>= fun (st_value, bs0) ->
+  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 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 = nat_of_elf32_word entry.elf32_st_name in
+    let addr = nat_of_elf32_addr 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 = nat_of_elf64_word entry.elf64_st_name in
+    let addr = nat_of_elf64_addr entry.elf64_st_value in
+      String_table.get_string_at name strtab >>= fun str ->
+      return (str, addr)
+  ) symtab
\ No newline at end of file