remove old elf sources

1 files changed, 0 insertions, 249 deletions

diff --git a/src/elf_model/elf_executable_file4.lem b/src/elf_model/elf_executable_file4.lem
deleted file mode 100644
index c6a6b345..00000000
--- a/src/elf_model/elf_executable_file4.lem
+++ /dev/null
@@ -1,249 +0,0 @@
-open import Maybe
-open import Num
-
-open import Elf_executable_file3
-open import Elf_header
-open import Elf_program_header_table
-open import Elf_section_header_table
-open import Elf_types
-open import String_table
-
-open import Bitstring
-open import Error
-open import Missing_pervasives
-open import Show
-open import String
-
-(** Type [elf32_executable_file4] represents the lazy unfolding of a 32-bit ELF
-  * file where the header, program header table and optional section header table
-  * have been filled in, along with the section header string table, with all
-  * other data being left uninterpreted.
-  *)
-type elf32_executable_file4 =
-  <| elf32_executable_file4_header                      : elf32_header (** The ELF header (mandatory) *)
-   ; elf32_executable_file4_program_header_table        : elf32_program_header_table (** The program header table (mandatory) *)
-   ; elf32_executable_file4_section_header_table        : maybe elf32_section_header_table (** The section header table (optional) *)
-   ; elf32_executable_file4_section_header_string_table : string_table
-   ; elf32_executable_file4_body                        : bitstring (** Uninterpreted body *)
-   |>
-
-class (HasElf32ExecutableFile4 'a)
-  val get_elf32_executable_file4 : 'a -> elf32_executable_file4
-end
-
-instance (HasElf32ExecutableFile4 elf32_executable_file4)
-  let get_elf32_executable_file4 f4 = f4
-end
-
-instance (HasElf32ExecutableFile3 elf32_executable_file4)
-  let get_elf32_executable_file3 f4 =
-    <| elf32_executable_file3_header = f4.elf32_executable_file4_header;
-         elf32_executable_file3_program_header_table = f4.elf32_executable_file4_program_header_table;
-         elf32_executable_file3_section_header_table = f4.elf32_executable_file4_section_header_table;
-         elf32_executable_file3_body = f4.elf32_executable_file4_body |>
-end
-
-instance (HasElf32Header elf32_executable_file4)
-  let get_elf32_header f4 = f4.elf32_executable_file4_header
-end
-
-instance (HasElf32ProgramHeaderTable elf32_executable_file4)
-  let get_elf32_program_header_table f4 =
-    Just (f4.elf32_executable_file4_program_header_table)
-end
-
-instance (HasElf32SectionHeaderTable elf32_executable_file4)
-  let get_elf32_section_header_table f4 =
-    f4.elf32_executable_file4_section_header_table
-end
-
-instance (HasElf32SectionHeaderStringTable elf32_executable_file4)
-  let get_elf32_section_header_string_table f4 =
-    f4.elf32_executable_file4_section_header_string_table
-end
-
-(** Type [elf64_executable_file4] represents the lazy unfolding of a 64-bit ELF
-  * file where the header, program header table and optional section header table
-  * have been filled in, along with the section header string table, with all
-  * other data being left uninterpreted.
-  *)
-type elf64_executable_file4 =
-  <| elf64_executable_file4_header                      : elf64_header (** The ELF header (mandatory) *)
-   ; elf64_executable_file4_program_header_table        : elf64_program_header_table (** The program header table (mandatory) *)
-   ; elf64_executable_file4_section_header_table        : maybe elf64_section_header_table (** The section header table (optional) *)
-   ; elf64_executable_file4_section_header_string_table : string_table
-   ; elf64_executable_file4_body                        : bitstring (** Uninterpreted body *)
-   |>
-
-class (HasElf64ExecutableFile4 'a)
-  val get_elf64_executable_file4 : 'a -> elf64_executable_file4
-end
-
-instance (HasElf64ExecutableFile4 elf64_executable_file4)
-  let get_elf64_executable_file4 f4 = f4
-end
-
-instance (HasElf64ExecutableFile3 elf64_executable_file4)
-  let get_elf64_executable_file3 f4 =
-    <| elf64_executable_file3_header = f4.elf64_executable_file4_header;
-         elf64_executable_file3_program_header_table = f4.elf64_executable_file4_program_header_table;
-         elf64_executable_file3_section_header_table = f4.elf64_executable_file4_section_header_table;
-         elf64_executable_file3_body = f4.elf64_executable_file4_body |>
-end
-
-instance (HasElf64Header elf64_executable_file4)
-  let get_elf64_header f4 = f4.elf64_executable_file4_header
-end
-
-instance (HasElf64ProgramHeaderTable elf64_executable_file4)
-  let get_elf64_program_header_table f4 =
-    Just (f4.elf64_executable_file4_program_header_table)
-end
-
-instance (HasElf64SectionHeaderTable elf64_executable_file4)
-  let get_elf64_section_header_table f4 =
-    f4.elf64_executable_file4_section_header_table
-end
-
-instance (HasElf64SectionHeaderStringTable elf64_executable_file4)
-  let get_elf64_section_header_string_table f4 =
-    f4.elf64_executable_file4_section_header_string_table
-end
-
-(** [refine_elf32_executable_file3 f3] refines an elf32_executable_file3 [f3], adding the
-  * section header string table, to obtain an elf32_executable_file4.  May fail if
-  * the offset stored in the ELF header indicating where the string table is stored is
-  * invalid.
-  *)
-val refine_elf32_executable_file3 : elf32_executable_file3 -> error elf32_executable_file4
-let refine_elf32_executable_file3 f3 =
-  let hdr  = f3.elf32_executable_file3_header in
-  let pht  = f3.elf32_executable_file3_program_header_table in
-  let sht  = f3.elf32_executable_file3_section_header_table in
-  let bs0  = f3.elf32_executable_file3_body in
-    match sht with
-      | Nothing  ->
-          return <| elf32_executable_file4_header = hdr;
-            elf32_executable_file4_program_header_table = pht;
-            elf32_executable_file4_section_header_table = Nothing;
-            elf32_executable_file4_section_header_string_table = String_table.empty;
-            elf32_executable_file4_body = bs0 |>
-      | Just sht ->
-        let idx  = nat_of_elf32_half hdr.elf32_shstrndx in
-        let sect = List.index sht idx in
-          match sect with
-            | Nothing -> Fail "refine_elf32_executable_file3: invalid offset into section header table"
-            | Just sect ->
-              let offset = nat_of_elf32_off sect.elf32_sh_offset * 8 in
-              let size   = nat_of_elf32_word sect.elf32_sh_size * 8 in
-              let (_, cut) = Bitstring.partition offset bs0 in
-              let (rel, _) = Bitstring.partition size cut in
-              let strings  = Bitstring.string_of_bitstring rel in
-                return <| elf32_executable_file4_header = hdr;
-                  elf32_executable_file4_program_header_table = pht;
-                  elf32_executable_file4_section_header_table = Just sht;
-                  elf32_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char;
-                  elf32_executable_file4_body = bs0 |>
-          end
-    end
-
-(** [refine_elf64_executable_file3 f3] refines an elf64_executable_file3 [f3], adding the
-  * section header string table, to obtain an elf64_executable_file4.  May fail if
-  * the offset stored in the ELF header indicating where the string table is stored is
-  * invalid.
-  *)
-val refine_elf64_executable_file3 : elf64_executable_file3 -> error elf64_executable_file4
-let refine_elf64_executable_file3 f3 =
-  let hdr  = f3.elf64_executable_file3_header in
-  let pht  = f3.elf64_executable_file3_program_header_table in
-  let sht  = f3.elf64_executable_file3_section_header_table in
-  let bs0  = f3.elf64_executable_file3_body in
-    match sht with
-      | Nothing  ->
-          return <| elf64_executable_file4_header = hdr;
-            elf64_executable_file4_program_header_table = pht;
-            elf64_executable_file4_section_header_table = Nothing;
-            elf64_executable_file4_section_header_string_table = String_table.empty;
-            elf64_executable_file4_body = bs0 |>
-      | Just sht ->
-        let idx  = nat_of_elf64_half hdr.elf64_shstrndx in
-        let sect = List.index sht idx in
-          match sect with
-            | Nothing -> fail "refine_elf32_executable_file3: invalid offset into section header table"
-            | Just sect ->
-              let offset = nat_of_elf64_off sect.elf64_sh_offset * 8 in
-              let size   = nat_of_elf64_xword sect.elf64_sh_size * 8 in
-              let (_, cut) = Bitstring.partition offset bs0 in
-              let (rel, _) = Bitstring.partition size cut in
-              let strings  = Bitstring.string_of_bitstring rel in
-                return <| elf64_executable_file4_header = hdr;
-                  elf64_executable_file4_program_header_table = pht;
-                  elf64_executable_file4_section_header_table = Just sht;
-                  elf64_executable_file4_section_header_string_table = String_table.mk_string_table strings Missing_pervasives.null_char;
-                  elf64_executable_file4_body = bs0 |>
-          end
-    end
-
-(** [read_elf32_executable_file4 bs0] reads an [elf32_executable_file4] in from
-  * bitstring [bs0].
-  *)
-val read_elf32_executable_file4 : bitstring -> error elf32_executable_file4
-let read_elf32_executable_file4 bs0 =
-  read_elf32_executable_file3 bs0 >>= refine_elf32_executable_file3
-
-(** [read_elf64_executable_file4 bs0] reads an [elf64_executable_file4] in from
-  * bitstring [bs0].
-  *)
-val read_elf64_executable_file4 : bitstring -> error elf64_executable_file4
-let read_elf64_executable_file4 bs0 =
-  read_elf64_executable_file3 bs0 >>= refine_elf64_executable_file3
-
-(** [string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string
-  * based representation of elf32_executable_file4 [f4].
-  *)
-val string_of_elf32_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file4 -> string
-let string_of_elf32_executable_file4 hdr_bdl pht_bdl sht_bdl f4 =
-  let sht =
-    match f4.elf32_executable_file4_section_header_table with
-      | Nothing  -> "\tNo section header table present"
-      | Just sht -> string_of_elf32_section_header_table' sht_bdl f4.elf32_executable_file4_section_header_string_table sht
-    end
-  in
-    unlines [
-      "\n*Type elf32_executable_file4"
-    ; "**Header"
-    ; string_of_elf32_header hdr_bdl f4.elf32_executable_file4_header
-    ; "**Program header table:"
-    ; string_of_elf32_program_header_table pht_bdl f4.elf32_executable_file4_program_header_table
-    ; "**Section header table:"
-    ; sht
-    ; "**Section header string table:"
-    ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf32_executable_file4_section_header_string_table))
-    ; "**Body:"
-    ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf32_executable_file4_body)
-    ]
-
-(** [string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4] provides a string
-  * based representation of elf64_executable_file4 [f4].
-  *)
-val string_of_elf64_executable_file4 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file4 -> string
-let string_of_elf64_executable_file4 hdr_bdl pht_bdl sht_bdl f4 =
-  let sht =
-    match f4.elf64_executable_file4_section_header_table with
-      | Nothing  -> "\tNo section header table present"
-      | Just sht -> string_of_elf64_section_header_table' sht_bdl f4.elf64_executable_file4_section_header_string_table sht
-    end
-  in
-    unlines [
-      "\n*Type elf64_executable_file4"
-    ; "**Header"
-    ; string_of_elf64_header hdr_bdl f4.elf64_executable_file4_header
-    ; "**Program header table:"
-    ; string_of_elf64_program_header_table pht_bdl f4.elf64_executable_file4_program_header_table
-    ; "**Section header table:"
-    ; sht
-    ; "**Section header string table:"
-    ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f4.elf64_executable_file4_section_header_string_table))
-    ; "**Body:"
-    ; "\tUninterpreted data of length " ^ show (Bitstring.length f4.elf64_executable_file4_body)
-    ]
\ No newline at end of file