remove old elf sources

1 files changed, 0 insertions, 445 deletions

diff --git a/src/elf_model/elf_section_header_table.lem b/src/elf_model/elf_section_header_table.lem
deleted file mode 100644
index 669a2dce..00000000
--- a/src/elf_model/elf_section_header_table.lem
+++ /dev/null
@@ -1,445 +0,0 @@
-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)
\ No newline at end of file