remove old elf sources

1 files changed, 0 insertions, 249 deletions

diff --git a/src/elf_model/elf_symbol_table.lem b/src/elf_model/elf_symbol_table.lem
deleted file mode 100644
index 54521157..00000000
--- a/src/elf_model/elf_symbol_table.lem
+++ /dev/null
@@ -1,249 +0,0 @@
-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