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