remove old elf sources

1 files changed, 0 insertions, 306 deletions

diff --git a/src/elf_model/elf_program_header_table.lem b/src/elf_model/elf_program_header_table.lem
deleted file mode 100644
index ad97d566..00000000
--- a/src/elf_model/elf_program_header_table.lem
+++ /dev/null
@@ -1,306 +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 Bitstring
-open import Error
-open import Missing_pervasives
-open import Show
-
-(** Segment types
-  *
-  * FIXME: Bug in Lem as Lem codebase uses [int] type throughout where [BigInt.t]
-  * is really needed, hence chokes on huge constants below, which is why they are
-  * written in the way that they are.
-  *)
-
-(** Unused array element.  All other members of the structure are undefined. *)
-let elf_pt_null : nat = 0
-(** A loadable segment. *)
-let elf_pt_load : nat = 1
-(** Dynamic linking information. *)
-let elf_pt_dynamic : nat = 2
-(** Specifies the location and size of a null-terminated path name to be used to
-  * invoke an interpreter.
-  *)
-let elf_pt_interp : nat = 3
-(** Specifies location and size of auxiliary information. *)
-let elf_pt_note : nat = 4
-(** Reserved but with unspecified semantics.  If the file contains a segment of
-  * this type then it is to be regarded as non-conformant with the ABI.
-  *)
-let elf_pt_shlib : nat = 5
-(** Specifies the location and size of the program header table. *)
-let elf_pt_phdr : nat = 6
-(** Specifies the thread local storage (TLS) template.  Need not be supported. *)
-let elf_pt_tls : nat = 7
-(** Start of reserved indices for operating system specific semantics. *)
-let elf_pt_loos : nat = 128 * 128 * 128 * 256 * 3 (* 1610612736 (* 0x60000000 *) *)
-(** End of reserved indices for operating system specific semantics. *)
-let elf_pt_hios : nat = (469762047 * 4) + 3 (* 1879048191 (* 0x6fffffff *) *)
-(** Start of reserved indices for processor specific semantics. *)
-let elf_pt_loproc : nat = (469762048 * 4) (* 1879048192 (* 0x70000000 *) *)
-(** End of reserved indices for processor specific semantics. *)
-let elf_pt_hiproc : nat = (536870911 * 4) + 3 (* 2147483647 (* 0x7fffffff *) *)
-
-(** [string_of_elf_segment_type os proc st] produces a string representation of
-  * the coding of an ELF segment type [st] using [os] and [proc] to render OS-
-  * and processor-specific codings.
-  *)
-val string_of_elf_segment_type : (nat -> string) -> (nat -> string) -> nat -> string
-let string_of_elf_segment_type os proc pt =
-	if pt = elf_pt_null then
-		"PT_NULL"
-	else if pt = elf_pt_load then
-		"PT_LOAD"
-	else if pt = elf_pt_dynamic then
-		"PT_DYNAMIC"
-	else if pt = elf_pt_interp then
-		"PT_INTERP"
-	else if pt = elf_pt_note then
-		"PT_NOTE"
-	else if pt = elf_pt_shlib then
-		"PT_SHLIB"
-	else if pt = elf_pt_phdr then
-		"PT_PHDR"
-	else if pt = elf_pt_tls then
-		"PT_TLS"
-	else if pt >= elf_pt_loos && pt <= elf_pt_hios then
-		os pt
-	else if pt >= elf_pt_loproc && pt <= elf_pt_hiproc then
-		proc pt
-	else
-		"Undefined or invalid segment type"
-
-(** Program header table entry type *)
-
-(** Type [elf32_program_header_table_entry] encodes a program header table entry
-  * for 32-bit platforms.  Each entry describes a segment in an executable or
-  * shared object file.
-  *)
-type elf32_program_header_table_entry =
-  <| elf32_p_type   : elf32_word (** Type of the segment *)
-   ; elf32_p_offset : elf32_off  (** Offset from beginning of file for segment *)
-   ; elf32_p_vaddr  : elf32_addr (** Virtual address for segment in memory *)
-   ; elf32_p_paddr  : elf32_addr (** Physical address for segment *)
-   ; elf32_p_filesz : elf32_word (** Size of segment in file, in bytes *)
-   ; elf32_p_memsz  : elf32_word (** Size of segment in memory image, in bytes *)
-   ; elf32_p_flags  : elf32_word (** Segment flags *)
-   ; elf32_p_align  : elf32_word (** Segment alignment memory for memory and file *)
-   |>
-
-(** Type [elf64_program_header_table_entry] encodes a program header table entry
-  * for 64-bit platforms.  Each entry describes a segment in an executable or
-  * shared object file.
-  *)
-type elf64_program_header_table_entry =
-  <| elf64_p_type   : elf64_word  (** Type of the segment *)
-   ; elf64_p_flags  : elf64_word  (** Segment flags *)
-   ; elf64_p_offset : elf64_off   (** Offset from beginning of file for segment *)
-   ; elf64_p_vaddr  : elf64_addr  (** Virtual address for segment in memory *)
-   ; elf64_p_paddr  : elf64_addr  (** Physical address for segment *)
-   ; elf64_p_filesz : elf64_xword (** Size of segment in file, in bytes *)
-   ; elf64_p_memsz  : elf64_xword (** Size of segment in memory image, in bytes *)
-   ; elf64_p_align  : elf64_xword (** Segment alignment memory for memory and file *)
-   |>
-  
-(** [string_of_elf32_program_header_table_entry os proc et] produces a string
-  * representation of a 32-bit program header table entry using [os] and [proc]
-  * to render OS- and processor-specific entries.
-  *)
-val string_of_elf32_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf32_program_header_table_entry -> string
-let string_of_elf32_program_header_table_entry os proc entry =
-	unlines [
-		"\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf32_word entry.elf32_p_type)
-	; "\t" ^ "Offset: " ^ show entry.elf32_p_offset
-	; "\t" ^ "Virtual address: " ^ show entry.elf32_p_vaddr
-	; "\t" ^ "Physical address: " ^ show entry.elf32_p_paddr
-	; "\t" ^ "Segment size (bytes): " ^ show entry.elf32_p_filesz
-	; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf32_p_memsz
-	; "\t" ^ "Flags: " ^ show entry.elf32_p_flags
-  ; "\t" ^ "Alignment: " ^ show entry.elf32_p_align
-	]
-
-(** [string_of_elf64_program_header_table_entry os proc et] produces a string
-  * representation of a 64-bit program header table entry using [os] and [proc]
-  * to render OS- and processor-specific entries.
-  *)
-val string_of_elf64_program_header_table_entry : (nat -> string) -> (nat -> string) -> elf64_program_header_table_entry -> string
-let string_of_elf64_program_header_table_entry os proc entry =
-  unlines [
-    "\t" ^ "Segment type: " ^ string_of_elf_segment_type os proc (nat_of_elf64_word entry.elf64_p_type)
-  ; "\t" ^ "Offset: " ^ show entry.elf64_p_offset
-  ; "\t" ^ "Virtual address: " ^ show entry.elf64_p_vaddr
-  ; "\t" ^ "Physical address: " ^ show entry.elf64_p_paddr
-  ; "\t" ^ "Segment size (bytes): " ^ show entry.elf64_p_filesz
-  ; "\t" ^ "Segment size in memory image (bytes): " ^ show entry.elf64_p_memsz
-  ; "\t" ^ "Flags: " ^ show entry.elf64_p_flags
-  ; "\t" ^ "Alignment: " ^ show entry.elf64_p_align
-  ]
-
-(** [string_of_elf32_program_header_table_entry_default et] produces a string representation
-  * of table entry [et] where OS- and processor-specific entries are replaced with
-  * default strings.
-  *)
-val string_of_elf32_program_header_table_entry_default : elf32_program_header_table_entry -> string
-let string_of_elf32_program_header_table_entry_default =
-	string_of_elf32_program_header_table_entry
-    (const "*Default OS specific print*")
-      (const "*Default processor specific print*")
-
-(** [string_of_elf64_program_header_table_entry_default et] produces a string representation
-  * of table entry [et] where OS- and processor-specific entries are replaced with
-  * default strings.
-  *)
-val string_of_elf64_program_header_table_entry_default : elf64_program_header_table_entry -> string
-let string_of_elf64_program_header_table_entry_default =
-  string_of_elf64_program_header_table_entry
-    (const "*Default OS specific print*")
-      (const "*Default processor specific print*")
-	
-instance (Show elf32_program_header_table_entry)
-	let show = string_of_elf32_program_header_table_entry_default
-end
-
-instance (Show elf64_program_header_table_entry)
-  let show = string_of_elf64_program_header_table_entry_default
-end
-
-(** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table
-  * entry from bitstring [bs0] assuming endianness [endian].  If [bs0] is larger
-  * than necessary, the excess is returned from the function, too.
-  *)
-val read_elf32_program_header_table_entry : endianness -> bitstring -> error (elf32_program_header_table_entry * bitstring)
-let read_elf32_program_header_table_entry endian bs =
-	read_elf32_word endian bs >>= fun (typ, bs) ->
-	read_elf32_off  endian bs >>= fun (offset, bs) ->
-	read_elf32_addr endian bs >>= fun (vaddr, bs) ->
-	read_elf32_addr endian bs >>= fun (paddr, bs) ->
-	read_elf32_word endian bs >>= fun (filesz, bs) ->
-	read_elf32_word endian bs >>= fun (memsz, bs) ->
-	read_elf32_word endian bs >>= fun (flags, bs) ->
-	read_elf32_word endian bs >>= fun (align, bs) ->
-		return (<| elf32_p_type = typ; elf32_p_offset = offset;
-                elf32_p_vaddr = vaddr; elf32_p_paddr = paddr;
-                elf32_p_filesz = filesz; elf32_p_memsz = memsz;
-                elf32_p_flags = flags; elf32_p_align = align |>, bs)
-
-val read_elf64_program_header_table_entry : endianness -> bitstring -> error (elf64_program_header_table_entry * bitstring)
-let read_elf64_program_header_table_entry endian bs =
-  read_elf64_word endian bs >>= fun (typ, bs) ->
-  read_elf64_word endian bs >>= fun (flags, bs) ->
-  read_elf64_off  endian bs >>= fun (offset, bs) ->
-  read_elf64_addr endian bs >>= fun (vaddr, bs) ->
-  read_elf64_addr endian bs >>= fun (paddr, bs) ->
-  read_elf64_xword endian bs >>= fun (filesz, bs) ->
-  read_elf64_xword endian bs >>= fun (memsz, bs) ->
-  read_elf64_xword endian bs >>= fun (align, bs) ->
-    return (<| elf64_p_type = typ; elf64_p_offset = offset;
-                elf64_p_vaddr = vaddr; elf64_p_paddr = paddr;
-                elf64_p_filesz = filesz; elf64_p_memsz = memsz;
-                elf64_p_flags = flags; elf64_p_align = align |>, bs)
-
-(** Program header table type *)
-
-(** Type [elf32_program_header_table] represents a program header table for 32-bit
-  * ELF files.  A program header table is an array (implemented as a list, here)
-  * of program header table entries.
-  *)
-type elf32_program_header_table =
-  list elf32_program_header_table_entry
-
-class (HasElf32ProgramHeaderTable 'a)
-  val get_elf32_program_header_table : 'a -> maybe elf32_program_header_table
-end
-
-(** Type [elf64_program_header_table] represents a program header table for 64-bit
-  * ELF files.  A program header table is an array (implemented as a list, here)
-  * of program header table entries.
-  *)
-type elf64_program_header_table =
-  list elf64_program_header_table_entry
-
-class (HasElf64ProgramHeaderTable 'a)
-  val get_elf64_program_header_table : 'a -> maybe elf64_program_header_table
-end
-
-(** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from
-  * bitstring [bs0] assuming endianness [endian].  The bitstring [bs0] is assumed
-  * to have exactly the correct size for the table.  For internal use, only.  Use
-  * [read_elf32_program_header_table] below instead.
-  *)
-let rec read_elf32_program_header_table' endian bs0 =
-	if length bs0 = 0 then
-  	return []
-  else
-  	read_elf32_program_header_table_entry endian bs0 >>= fun (entry, bs1) ->
-    read_elf32_program_header_table' endian bs1 >>= fun tail ->
-    return (entry::tail)
-
-(** [read_elf64_program_header_table' endian bs0] reads an ELF64 program header table from
-  * bitstring [bs0] assuming endianness [endian].  The bitstring [bs0] is assumed
-  * to have exactly the correct size for the table.  For internal use, only.  Use
-  * [read_elf32_program_header_table] below instead.
-  *)
-let rec read_elf64_program_header_table' endian bs0 =
-  if length bs0 = 0 then
-    return []
-  else
-    read_elf64_program_header_table_entry endian bs0 >>= fun (entry, bs1) ->
-    read_elf64_program_header_table' endian bs1 >>= fun tail ->
-    return (entry::tail)
-
-(** [read_elf32_program_header_table table_size endian bs0] reads an ELF32 program header
-  * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
-  * This [table_size] argument should be equal to the number of entries in the
-  * table multiplied by the fixed entry size.  Bitstring [bs0] may be larger than
-  * necessary, in which case the excess is returned.
-  *)
-val read_elf32_program_header_table : nat -> endianness -> bitstring -> error (elf32_program_header_table * bitstring)
-let read_elf32_program_header_table table_size endian bs0 =
-	let (eat, rest) = partition table_size bs0 in
-		read_elf32_program_header_table' endian eat >>= fun table ->
-		return (table, rest)
-
-(** [read_elf64_program_header_table table_size endian bs0] reads an ELF64 program header
-  * table from bitstring [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
-  * This [table_size] argument should be equal to the number of entries in the
-  * table multiplied by the fixed entry size.  Bitstring [bs0] may be larger than
-  * necessary, in which case the excess is returned.
-  *)
-val read_elf64_program_header_table : nat -> endianness -> bitstring -> error (elf64_program_header_table * bitstring)
-let read_elf64_program_header_table table_size endian bs0 =
-  let (eat, rest) = partition table_size bs0 in
-    read_elf64_program_header_table' endian eat >>= fun table ->
-    return (table, rest)
-
-(** The [pht_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 pht_print_bundle = (nat -> string) * (nat -> string)
-
-(** [string_of_elf32_program_header_table os proc tbl] produces a string representation
-  * of program header table [tbl] using [os] and [proc] to render OS- and processor-
-  * specific entries.
-  *)
-val string_of_elf32_program_header_table : pht_print_bundle -> elf32_program_header_table -> string
-let string_of_elf32_program_header_table (os, proc) tbl =
-  unlines (List.map (string_of_elf32_program_header_table_entry os proc) tbl)
-
-(** [string_of_elf64_program_header_table os proc tbl] produces a string representation
-  * of program header table [tbl] using [os] and [proc] to render OS- and processor-
-  * specific entries.
-  *)
-val string_of_elf64_program_header_table : pht_print_bundle -> elf64_program_header_table -> string
-let string_of_elf64_program_header_table (os, proc) tbl =
-  unlines (List.map (string_of_elf64_program_header_table_entry os proc) tbl)