path: root/src/elf_model/elf_section_header_table.lem

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 String_table

open import Bitstring
open import Error
open import Missing_pervasives
open import Show

(** Special section indices. *)

(** [shn_undef]: marks an undefined, missing or irrelevant section reference.
  *)
let shn_undef : nat = 0
(** [shn_loreserve]: this specifies the lower bound of the range of reserved
  * indices.
  *)
let shn_loreserve : nat = 65280 (* 0xff00 *)
(** [shn_loproc]: start of the range reserved for processor-specific semantics.
  *)
let shn_loproc : nat = 65280 (* 0xff00 *)
(** [shn_hiproc]: end of the range reserved for processor-specific semantics.
  *)
let shn_hiproc : nat = 65311 (* 0xff1f *)
(** [shn_loos]: start of the range reserved for operating system-specific
  * semantics.
  *)
let shn_loos : nat = 65312 (* 0xff20 *)
(** [shn_hios]: end of the range reserved for operating system-specific
  * semantics.
  *)
let shn_hios : nat = 65343 (* 0xff3f *)
(** [shn_abs]: specifies the absolute values for the corresponding reference.
  * Symbols defined relative to section number [shn_abs] have absolute values
  * and are not affected by relocation.
  *)
let shn_abs : nat = 65521 (* 0xfff1 *)
(** [shn_common]: symbols defined relative to this index are common symbols,
  * such as unallocated C external variables.
  *)
let shn_common : nat = 65522 (* 0xfff2 *)
(** [shn_xindex]: an escape value.  It indicates the actual section header index
  * is too large to fit in the containing field and is located in another
  * location (specific to the structure where it appears).
  *)
let shn_xindex : nat = 65535 (* 0xffff *)
(** [shn_hireserve]: specifies the upper-bound of reserved values.
  *)
let shn_hireserve : nat = 65535 (* 0xffff *)

val string_of_special_section_index : nat -> string
let string_of_special_section_index i =
  if i = shn_undef then
    "SHN_UNDEF"
  else if i = shn_loreserve then
    "SHN_LORESERVE"
  else if i >= shn_loproc && i <= shn_hiproc then
    "SHN_PROCESSOR_SPECIFIC"
  else if i >= shn_loos && i <= shn_hios then
    "SHN_OS_SPECIFIC"
  else if i = shn_abs then
    "SHN_ABS"
  else if i = shn_common then
    "SHN_COMMON"
  else if i = shn_xindex then
    "SHN_XINDEX"
  else if i = shn_hireserve then
    "SHN_HIRESERVE"
  else
  	"SHN UNDEFINED"

(** Section types. *)

(** Marks the section header as being inactive. *)
let sht_null : nat = 0
(** Section holds information defined by the program. *)
let sht_progbits : nat = 1
(** The following two section types hold a symbol table.  An object file may only
  * have one symbol table of each of the respective types.  The symtab provides
  * a place for link editing, whereas the dynsym section holds a minimal set of
  * dynamic linking symbols
  *)
let sht_symtab : nat = 2
let sht_dynsym : nat = 11
(** Section holds a string table *)
let sht_strtab : nat = 3
(** Section holds relocation entries with explicit addends.  An object file may
  * have multiple section of this type.
  *)
let sht_rela : nat = 4
(** Section holds a symbol hash table.  An object file may only have a single
  * hash table.
  *)
let sht_hash : nat = 5
(** Section holds information for dynamic linking.  An object file may only have
  * a single dynamic section.
  *)
let sht_dynamic : nat = 6
(** Section holds information that marks the file in some way. *)
let sht_note : nat = 7
(** Section occupies no space in the file but otherwise resembles a progbits
  * section.
  *)
let sht_nobits : nat = 8
(** Section holds relocation entries without explicit addends.  An object file
  * may have multiple section of this type.
  *)
let sht_rel : nat = 9
(** Section type is reserved but has an unspecified meaning. *)
let sht_shlib : nat = 10
(** Section contains an array of pointers to initialisation functions.  Each
  * pointer is taken as a parameterless function with a void return type.
  *)
let sht_init_array : nat = 14
(** Section contains an array of pointers to termination functions.  Each
  * pointer is taken as a parameterless function with a void return type.
  *)
let sht_fini_array : nat = 15
(** Section contains an array of pointers to initialisation functions that are
  * invoked before all other initialisation functions.  Each
  * pointer is taken as a parameterless function with a void return type.
  *)
let sht_preinit_array : nat = 16
(** Section defines a section group, i.e. a set of sections that are related and
  * must be treated especially by the linker.  May only appear in relocatable
  * objects.
  *)
let sht_group : nat = 17
(** Section is associated with sections of type SHT_SYMTAB and is required if
  * any of the section header indices referenced by that symbol table contains
  * the escape value SHN_XINDEX.
  *
  * FIXME: Lem bug as [int] type used throughout Lem codebase, rather than
  * [BigInt.t], so Lem chokes on these large constants below, hence the weird
  * way in which they are written.
  *)
let sht_symtab_shndx : nat = 18
let sht_loos   : nat = 3 * 1024 * 1024 * 512 (* 1610612736 (* 0x60000000 *) *)
let sht_hios   : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *)
let sht_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *)
let sht_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *)
let sht_louser : nat = (536870912 * 4) (* 2147483648 (* 0x80000000 *) *)
let sht_hiuser : nat = (603979775 * 4) + 3 (* 2415919103 (* 0x8fffffff *) *)

val string_of_section_type : (nat -> string) -> (nat -> string) ->
  (nat -> string) -> nat -> string
let string_of_section_type os proc user i =
  if i = sht_null then
    "SHT_NULL"
  else if i = sht_progbits then
    "SHT_PROGBITS"
  else if i = sht_symtab then
    "SHT_SYMTAB"
  else if i = sht_strtab then
    "SHT_STRTAB"
  else if i = sht_rela then
    "SHT_RELA"
  else if i = sht_hash then
    "SHT_HASH"
  else if i = sht_dynamic then
    "SHT_DYNAMIC"
  else if i = sht_note then
    "SHT_NOTE"
  else if i = sht_nobits then
    "SHT_NOBITS"
  else if i = sht_rel then
    "SHT_REL"
  else if i = sht_shlib then
    "SHT_SHLIB"
  else if i = sht_dynsym then
    "SHT_DYNSYM"
  else if i = sht_init_array then
    "SHT_INIT_ARRAY"
  else if i = sht_fini_array then
    "SHT_FINI_ARRAY"
  else if i = sht_preinit_array then
    "SHT_PREINIT_ARRAY"
  else if i = sht_group then
    "SHT_GROUP"
  else if i = sht_symtab_shndx then
    "SHT_SYMTAB_SHNDX"
  else if i >= sht_loos && i <= sht_hios then
    os i 
  else if i >= sht_loproc && i <= sht_hiproc then
    proc i
  else if i >= sht_louser && i <= sht_hiuser then
    user i
  else
    "Undefined or invalid section type"

(** Section header table entry type. *)

(** [elf32_section_header_table_entry] is the type of entries in the section
  * header table in 32-bit ELF files.  Each entry in the table details a section
  * in the body of the ELF file.
  *) 
type elf32_section_header_table_entry =
  <| elf32_sh_name      : elf32_word (** Name of the section *)
   ; elf32_sh_type      : elf32_word (** Type of the section and its semantics *)
   ; elf32_sh_flags     : elf32_word (** Flags associated with the section *)
   ; elf32_sh_addr      : elf32_addr (** Address of first byte of section in memory image *)
   ; elf32_sh_offset    : elf32_off  (** Offset from beginning of file of first byte of section *)
   ; elf32_sh_size      : elf32_word (** Section size in bytes *)
   ; elf32_sh_link      : elf32_word (** Section header table index link *)
   ; elf32_sh_info      : elf32_word (** Extra information, contents depends on type of section *)
   ; elf32_sh_addralign : elf32_word (** Alignment constraints for section *)
   ; elf32_sh_entsize   : elf32_word (** Size of each entry in table, if section is one *)
   |>

(** [elf64_section_header_table_entry] is the type of entries in the section
  * header table in 64-bit ELF files.  Each entry in the table details a section
  * in the body of the ELF file.
  *) 
type elf64_section_header_table_entry =
  <| elf64_sh_name      : elf64_word (** Name of the section *)
   ; elf64_sh_type      : elf64_word (** Type of the section and its semantics *)
   ; elf64_sh_flags     : elf64_xword (** Flags associated with the section *)
   ; elf64_sh_addr      : elf64_addr (** Address of first byte of section in memory image *)
   ; elf64_sh_offset    : elf64_off  (** Offset from beginning of file of first byte of section *)
   ; elf64_sh_size      : elf64_xword (** Section size in bytes *)
   ; elf64_sh_link      : elf64_word (** Section header table index link *)
   ; elf64_sh_info      : elf64_word (** Extra information, contents depends on type of section *)
   ; elf64_sh_addralign : elf64_xword (** Alignment constraints for section *)
   ; elf64_sh_entsize   : elf64_xword (** Size of each entry in table, if section is one *)
   |>

val read_elf32_section_header_table_entry : endianness -> bitstring -> error (elf32_section_header_table_entry * bitstring)
let read_elf32_section_header_table_entry endian bs =
	read_elf32_word endian bs >>= fun (sh_name, bs) ->
	read_elf32_word endian bs >>= fun (sh_type, bs) ->
	read_elf32_word endian bs >>= fun (sh_flags, bs) ->
	read_elf32_addr endian bs >>= fun (sh_addr, bs) ->
	read_elf32_off  endian bs >>= fun (sh_offset, bs) ->
	read_elf32_word endian bs >>= fun (sh_size, bs) ->
	read_elf32_word endian bs >>= fun (sh_link, bs) ->
	read_elf32_word endian bs >>= fun (sh_info, bs) ->
	read_elf32_word endian bs >>= fun (sh_addralign, bs) ->
	read_elf32_word endian bs >>= fun (sh_entsize, bs) ->
		return (<| elf32_sh_name = sh_name; elf32_sh_type = sh_type;
                elf32_sh_flags = sh_flags; elf32_sh_addr = sh_addr;
                elf32_sh_offset = sh_offset; elf32_sh_size = sh_size;
                elf32_sh_link = sh_link; elf32_sh_info = sh_info;
                elf32_sh_addralign = sh_addralign; elf32_sh_entsize = sh_entsize |>, bs)


val read_elf64_section_header_table_entry : endianness -> bitstring -> error (elf64_section_header_table_entry * bitstring)
let read_elf64_section_header_table_entry endian bs =
  read_elf64_word endian bs >>= fun (sh_name, bs) ->
  read_elf64_word endian bs >>= fun (sh_type, bs) ->
  read_elf64_xword endian bs >>= fun (sh_flags, bs) ->
  read_elf64_addr endian bs >>= fun (sh_addr, bs) ->
  read_elf64_off  endian bs >>= fun (sh_offset, bs) ->
  read_elf64_xword endian bs >>= fun (sh_size, bs) ->
  read_elf64_word endian bs >>= fun (sh_link, bs) ->
  read_elf64_word endian bs >>= fun (sh_info, bs) ->
  read_elf64_xword endian bs >>= fun (sh_addralign, bs) ->
  read_elf64_xword endian bs >>= fun (sh_entsize, bs) ->
    return (<| elf64_sh_name = sh_name; elf64_sh_type = sh_type;
                elf64_sh_flags = sh_flags; elf64_sh_addr = sh_addr;
                elf64_sh_offset = sh_offset; elf64_sh_size = sh_size;
                elf64_sh_link = sh_link; elf64_sh_info = sh_info;
                elf64_sh_addralign = sh_addralign; elf64_sh_entsize = sh_entsize |>, bs)

(** The [sht_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 sht_print_bundle = (nat -> string) * (nat -> string) * (nat -> string)

val string_of_elf32_section_header_table_entry : sht_print_bundle -> elf32_section_header_table_entry -> string
let string_of_elf32_section_header_table_entry (os, proc, user) entry =
  unlines [
    "\t" ^ "Name: "    ^ show entry.elf32_sh_name
  ; "\t" ^ "Type: "    ^ string_of_section_type os proc user (nat_of_elf32_word entry.elf32_sh_type)
  ; "\t" ^ "Flags: "   ^ show entry.elf32_sh_flags
  ; "\t" ^ "Address: " ^ show entry.elf32_sh_addr
  ; "\t" ^ "Size: "    ^ show entry.elf32_sh_size
  ]

val string_of_elf64_section_header_table_entry : sht_print_bundle -> elf64_section_header_table_entry -> string
let string_of_elf64_section_header_table_entry (os, proc, user) entry =
  unlines [
    "\t" ^ "Name: "    ^ show entry.elf64_sh_name
  ; "\t" ^ "Type: "    ^ string_of_section_type os proc user (nat_of_elf64_word entry.elf64_sh_type)
  ; "\t" ^ "Flags: "   ^ show entry.elf64_sh_flags
  ; "\t" ^ "Address: " ^ show entry.elf64_sh_addr
  ; "\t" ^ "Size: "    ^ show entry.elf64_sh_size
  ]

val string_of_elf32_section_header_table_entry' : sht_print_bundle -> string_table -> elf32_section_header_table_entry -> string
let string_of_elf32_section_header_table_entry' (os, proc, user) stbl entry =
  let name =
    match get_string_at (nat_of_elf32_word entry.elf32_sh_name) stbl with
      | Fail _ -> "Invalid index into string table"
      | Success i -> i
    end
  in
    unlines [
      "\t" ^ "Name: "    ^ name
    ; "\t" ^ "Type: "    ^ string_of_section_type os proc user (nat_of_elf32_word entry.elf32_sh_type)
    ; "\t" ^ "Flags: "   ^ show entry.elf32_sh_flags
    ; "\t" ^ "Address: " ^ show entry.elf32_sh_addr
    ; "\t" ^ "Size: "    ^ show entry.elf32_sh_size
    ]

val string_of_elf64_section_header_table_entry' : sht_print_bundle -> string_table -> elf64_section_header_table_entry -> string
let string_of_elf64_section_header_table_entry' (os, proc, user) stbl entry =
  let name =
    match get_string_at (nat_of_elf64_word entry.elf64_sh_name) stbl with
      | Fail _ -> "Invalid index into string table"
      | Success i -> i
    end
  in
    unlines [
      "\t" ^ "Name: "    ^ name
    ; "\t" ^ "Type: "    ^ string_of_section_type os proc user (nat_of_elf64_word entry.elf64_sh_type)
    ; "\t" ^ "Flags: "   ^ show entry.elf64_sh_flags
    ; "\t" ^ "Address: " ^ show entry.elf64_sh_addr
    ; "\t" ^ "Size: "    ^ show entry.elf64_sh_size
    ]

let string_of_elf32_section_header_table_entry_default =
  string_of_elf32_section_header_table_entry
    ((const "*Default OS specific print*"),
      (const "*Default processor specific print*"),
      (const "*Default user specific print*"))

instance (Show elf32_section_header_table_entry)
  let show = string_of_elf32_section_header_table_entry_default
end

let string_of_elf64_section_header_table_entry_default =
  string_of_elf64_section_header_table_entry
    ((const "*Default OS specific print*"),
      (const "*Default processor specific print*"),
      (const "*Default user specific print*"))

instance (Show elf64_section_header_table_entry)
  let show = string_of_elf64_section_header_table_entry_default
end

(** Section header table type. *)

(** Type [elf32_section_header_table] represents a section header table for 32-bit
  * ELF files.  A section header table is an array (implemented as a list, here)
  * of section header table entries.
  *)
type elf32_section_header_table =
  list elf32_section_header_table_entry

class (HasElf32SectionHeaderTable 'a)
  val get_elf32_section_header_table : 'a -> maybe elf32_section_header_table
end

(** Type [elf64_section_header_table] represents a section header table for 64-bit
  * ELF files.  A section header table is an array (implemented as a list, here)
  * of section header table entries.
  *)
type elf64_section_header_table =
  list elf64_section_header_table_entry

class (HasElf64SectionHeaderTable 'a)
  val get_elf64_section_header_table : 'a -> maybe elf64_section_header_table
end

let rec read_elf32_section_header_table' endian bs0 =
  if length bs0 = 0 then
    return []
  else
    read_elf32_section_header_table_entry endian bs0 >>= fun (entry, bs1) ->
    read_elf32_section_header_table' endian bs1 >>= fun tail ->
    return (entry::tail)

val read_elf32_section_header_table : nat -> endianness -> bitstring -> error (elf32_section_header_table * bitstring)
let read_elf32_section_header_table table_size endian bs0 =
  let (eat, rest) = partition table_size bs0 in
  	read_elf32_section_header_table' endian eat >>= fun entries ->
    return (entries, rest)
;;

let rec read_elf64_section_header_table' endian bs0 =
  if length bs0 = 0 then
    return []
  else
    read_elf64_section_header_table_entry endian bs0 >>= fun (entry, bs1) ->
    read_elf64_section_header_table' endian bs1 >>= fun tail ->
    return (entry::tail)

val read_elf64_section_header_table : nat -> endianness -> bitstring -> error (elf64_section_header_table * bitstring)
let read_elf64_section_header_table table_size endian bs0 =
  let (eat, rest) = partition table_size bs0 in
    read_elf64_section_header_table' endian eat >>= fun entries ->
    return (entries, rest)
;;

val elf32_size_correct : elf32_section_header_table_entry -> elf32_section_header_table -> bool
let elf32_size_correct hdr tbl =
  match nat_of_elf32_word hdr.elf32_sh_size with
    | 0 -> true
    | m -> m = List.length tbl
  end
;;

val is_valid_elf32_section_header_table : elf32_section_header_table -> bool
let is_valid_elf32_section_header_table tbl =
  match tbl with
    | []    -> false
    | x::xs ->
        nat_of_elf32_word x.elf32_sh_name = 0 &&
        nat_of_elf32_word x.elf32_sh_type = sht_null &&
        nat_of_elf32_word x.elf32_sh_flags = 0 &&
        nat_of_elf32_addr x.elf32_sh_addr = 0 &&
        nat_of_elf32_off x.elf32_sh_offset = 0 &&
        nat_of_elf32_word x.elf32_sh_info = 0 &&
        nat_of_elf32_word x.elf32_sh_addralign = 0 &&
        nat_of_elf32_word x.elf32_sh_entsize = 0 &&
        elf32_size_correct x tbl
        (* XXX: more correctness criteria in time *)
  end

val string_of_elf32_section_header_table : sht_print_bundle -> elf32_section_header_table -> string
let string_of_elf32_section_header_table sht_bdl tbl =
  unlines (List.map (string_of_elf32_section_header_table_entry sht_bdl) tbl)

val string_of_elf32_section_header_table' : sht_print_bundle -> string_table -> elf32_section_header_table -> string
let string_of_elf32_section_header_table' sht_bdl stbl tbl =
  unlines (List.map (string_of_elf32_section_header_table_entry' sht_bdl stbl) tbl)

val string_of_elf64_section_header_table : sht_print_bundle -> elf64_section_header_table -> string
let string_of_elf64_section_header_table sht_bdl tbl =
  unlines (List.map (string_of_elf64_section_header_table_entry sht_bdl) tbl)

val string_of_elf64_section_header_table' : sht_print_bundle -> string_table -> elf64_section_header_table -> string
let string_of_elf64_section_header_table' sht_bdl stbl tbl =
  unlines (List.map (string_of_elf64_section_header_table_entry' sht_bdl stbl) tbl)