remove old elf sources

1 files changed, 0 insertions, 339 deletions

diff --git a/src/elf_model/elf_executable_file5.lem b/src/elf_model/elf_executable_file5.lem
deleted file mode 100644
index 164cccb6..00000000
--- a/src/elf_model/elf_executable_file5.lem
+++ /dev/null
@@ -1,339 +0,0 @@
-open import Basic_classes
-open import List
-open import Maybe
-open import Num
-open import Tuple
-
-open import Elf_executable_file4
-open import Elf_header
-open import Elf_interpreted_segment
-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_file5] is an elf32_executable_file4 type where segments
-  * have been read from the program header table and interpreted.  A process
-  * image can be obtained from this type.
-  *)
-type elf32_executable_file5 =
-  <| elf32_executable_file5_header                      : elf32_header (** The ELF header (mandatory) *)
-   ; elf32_executable_file5_program_header_table        : elf32_program_header_table (** The program header table (mandatory) *)
-   ; elf32_executable_file5_section_header_table        : maybe elf32_section_header_table (** The section header table (optional) *)
-   ; elf32_executable_file5_section_header_string_table : string_table (** The section header string table *)
-   ; elf32_executable_file5_segments                    : list elf32_interpreted_segment (** The list of segments as described by the program header table *)
-   ; elf32_executable_file5_body                        : bitstring (** Uninterpreted body *)
-   |>
-
-class (HasElf32ExecutableFile5 'a)
-  val get_elf32_executable_file5 : 'a -> elf32_executable_file5
-end
-
-instance (HasElf32ExecutableFile5 elf32_executable_file5)
-  let get_elf32_executable_file5 f5 = f5
-end
-
-instance (HasElf32ExecutableFile4 elf32_executable_file5)
-  let get_elf32_executable_file4 f5 =
-    <| elf32_executable_file4_header = f5.elf32_executable_file5_header;
-         elf32_executable_file4_program_header_table = f5.elf32_executable_file5_program_header_table;
-         elf32_executable_file4_section_header_table = f5.elf32_executable_file5_section_header_table;
-         elf32_executable_file4_section_header_string_table = f5.elf32_executable_file5_section_header_string_table;
-         elf32_executable_file4_body = f5.elf32_executable_file5_body |>
-end
-
-instance (HasElf32Header elf32_executable_file5)
-  let get_elf32_header f5 = f5.elf32_executable_file5_header
-end
-
-instance (HasElf32ProgramHeaderTable elf32_executable_file5)
-  let get_elf32_program_header_table f5 = Just (f5.elf32_executable_file5_program_header_table)
-end
-
-instance (HasElf32SectionHeaderTable elf32_executable_file5)
-  let get_elf32_section_header_table f5 = f5.elf32_executable_file5_section_header_table
-end
-
-instance (HasElf32SectionHeaderStringTable elf32_executable_file5)
-  let get_elf32_section_header_string_table f5 = f5.elf32_executable_file5_section_header_string_table
-end
-
-(** Type [elf64_executable_file5] is an elf64_executable_file4 type where segments
-  * have been read from the program header table and interpreted.  A process
-  * image can be obtained from this type.
-  *)
-type elf64_executable_file5 =
-  <| elf64_executable_file5_header                      : elf64_header (** The ELF header (mandatory) *)
-   ; elf64_executable_file5_program_header_table        : elf64_program_header_table (** The program header table (mandatory) *)
-   ; elf64_executable_file5_section_header_table        : maybe elf64_section_header_table (** The section header table (optional) *)
-   ; elf64_executable_file5_section_header_string_table : string_table (** The section header string table *)
-   ; elf64_executable_file5_segments                    : list elf64_interpreted_segment (** The list of segments as described by the program header table *)
-   ; elf64_executable_file5_body                        : bitstring (** Uninterpreted body *)
-   |>
-
-class (HasElf64ExecutableFile5 'a)
-  val get_elf64_executable_file5 : 'a -> elf64_executable_file5
-end
-
-instance (HasElf64ExecutableFile5 elf64_executable_file5)
-  let get_elf64_executable_file5 f5 = f5
-end
-
-instance (HasElf64ExecutableFile4 elf64_executable_file5)
-  let get_elf64_executable_file4 f5 =
-    <| elf64_executable_file4_header = f5.elf64_executable_file5_header;
-         elf64_executable_file4_program_header_table = f5.elf64_executable_file5_program_header_table;
-         elf64_executable_file4_section_header_table = f5.elf64_executable_file5_section_header_table;
-         elf64_executable_file4_section_header_string_table = f5.elf64_executable_file5_section_header_string_table;
-         elf64_executable_file4_body = f5.elf64_executable_file5_body |>
-end
-
-instance (HasElf64Header elf64_executable_file5)
-  let get_elf64_header f5 = f5.elf64_executable_file5_header
-end
-
-instance (HasElf64ProgramHeaderTable elf64_executable_file5)
-  let get_elf64_program_header_table f5 = Just (f5.elf64_executable_file5_program_header_table)
-end
-
-instance (HasElf64SectionHeaderTable elf64_executable_file5)
-  let get_elf64_section_header_table f5 = f5.elf64_executable_file5_section_header_table
-end
-
-instance (HasElf64SectionHeaderStringTable elf64_executable_file5)
-  let get_elf64_section_header_string_table f5 = f5.elf64_executable_file5_section_header_string_table
-end
-
-(** [refine_elf32_executable_file4 f4] refines an elf32_executable_file4 [f4] into
-  * an elf32_executable_file5 by adding the interpreted segment field.  Fails
-  * if an interpreted segment has a memory size smaller than its associated
-  * file size, an invalidation of the ELF spec.
-  *)
-val refine_elf32_executable_file4 : elf32_executable_file4 -> error elf32_executable_file5
-let refine_elf32_executable_file4 f4 =
-  let pht  = f4.elf32_executable_file4_program_header_table in
-  let bdy  = f4.elf32_executable_file4_body in
-  let segs =
-    List.map (fun ph ->
-      let offset   = nat_of_elf32_off ph.elf32_p_offset * 8  in
-      let size     = nat_of_elf32_word ph.elf32_p_filesz * 8 in
-      let relevant = Bitstring.offset_and_cut offset size bdy in
-      let vaddr    = nat_of_elf32_addr ph.elf32_p_vaddr  in
-      let memsz    = nat_of_elf32_word ph.elf32_p_memsz * 8 in
-      let typ      = nat_of_elf32_word ph.elf32_p_type   in
-      let flags    = elf32_interpret_program_header_flags ph.elf32_p_flags in
-        <| elf32_segment_body = relevant;
-             elf32_segment_type = typ;
-             elf32_segment_size = size;
-             elf32_segment_memsz = memsz;
-             elf32_segment_base  = vaddr;
-             elf32_segment_flags = flags |>
-    ) pht
-  in
-  let segs =
-    mapM (fun sg ->
-      if sg.elf32_segment_memsz < sg.elf32_segment_size then
-        Fail "refine_elf32_executable_file4: memory size of segment cannot be less than file size"
-      else
-        return sg) segs
-  in
-    segs >>= fun segs ->
-    return <|
-      elf32_executable_file5_header = f4.elf32_executable_file4_header;
-      elf32_executable_file5_program_header_table = f4.elf32_executable_file4_program_header_table;
-      elf32_executable_file5_section_header_table = f4.elf32_executable_file4_section_header_table;
-      elf32_executable_file5_section_header_string_table = f4.elf32_executable_file4_section_header_string_table;
-      elf32_executable_file5_segments = segs;
-      elf32_executable_file5_body = f4.elf32_executable_file4_body |>
-
-(** [refine_elf64_executable_file4 f4] refines an elf64_executable_file4 [f4] into
-  * an elf64_executable_file5 by adding the interpreted segment field.  Fails
-  * if an interpreted segment has a memory size smaller than its associated
-  * file size, an invalidation of the ELF spec.
-  *)
-val refine_elf64_executable_file4 : elf64_executable_file4 -> error elf64_executable_file5
-let refine_elf64_executable_file4 f4 =
-  let pht  = f4.elf64_executable_file4_program_header_table in
-  let bdy  = f4.elf64_executable_file4_body in
-  let segs =
-    List.map (fun ph ->
-      let offset   = nat_of_elf64_off ph.elf64_p_offset * 8  in
-      let size     = nat_of_elf64_xword ph.elf64_p_filesz * 8 in
-      let relevant = Bitstring.offset_and_cut offset size bdy in
-      let vaddr    = nat_of_elf64_addr ph.elf64_p_vaddr  in
-      let memsz    = nat_of_elf64_xword ph.elf64_p_memsz * 8 in
-      let typ      = nat_of_elf64_word ph.elf64_p_type   in
-      let flags    = elf64_interpret_program_header_flags ph.elf64_p_flags in
-        <| elf64_segment_body = relevant;
-             elf64_segment_type = typ;
-             elf64_segment_size = size;
-             elf64_segment_memsz = memsz;
-             elf64_segment_base  = vaddr;
-             elf64_segment_flags = flags |>
-    ) pht
-  in
-  let segs =
-    mapM (fun sg ->
-      if sg.elf64_segment_memsz < sg.elf64_segment_size then
-        fail "refine_elf64_executable_file4: memory size of segment cannot be less than file size"
-      else
-        return sg) segs
-  in
-    segs >>= fun segs ->
-    return <|
-      elf64_executable_file5_header = f4.elf64_executable_file4_header;
-      elf64_executable_file5_program_header_table = f4.elf64_executable_file4_program_header_table;
-      elf64_executable_file5_section_header_table = f4.elf64_executable_file4_section_header_table;
-      elf64_executable_file5_section_header_string_table = f4.elf64_executable_file4_section_header_string_table;
-      elf64_executable_file5_segments = segs;
-      elf64_executable_file5_body = f4.elf64_executable_file4_body |>
-
-(** [read_elf32_executable_file5 bs0] reads an elf32_executable_file5 from bitstring
-  * [bs0].
-  *)
-val read_elf32_executable_file5 : bitstring -> error elf32_executable_file5
-let read_elf32_executable_file5 bs0 =
-  read_elf32_executable_file4 bs0 >>= refine_elf32_executable_file4
-
-(** [read_elf64_executable_file5 bs0] reads an elf64_executable_file5 from bitstring
-  * [bs0].
-  *)
-val read_elf64_executable_file5 : bitstring -> error elf64_executable_file5
-let read_elf64_executable_file5 bs0 =
-  read_elf64_executable_file4 bs0 >>= refine_elf64_executable_file4
-
-(** [elf32_construct_image f5] constructs a memory image from an elf32_executable5 object
-  * [f5].  The function returns the following:
-  *    * A list of bytes with a corresponding address where they should be located
-  *      in the program image and,
-  *    * The entry point for the process.  All addresses in the aforementioned list
-  *      should be interpreted wrt this address.
-  * [construct_image] fails if a loadable segment has a memory size smaller than
-  * its associated file size, an error according to the ELF spec.  This should
-  * never happen as relevant checks are made when refining an elf_executable_file4
-  * into an elf_executable_file5.  The function may also fail if there are no loadable
-  * segments in this executable file, again an error.
-  * By the ELF specification, you may assume that the list of bitstring, elf32_addr
-  * pairs is sorted ascending on the second component, i.e. that all pairs are in
-  * order of the address at which point they should be loaded in memory.
-  *)
-val elf32_construct_image : elf32_executable_file5 -> error (list (bitstring * nat) * nat)
-let elf32_construct_image f5 =
-  let segs = f5.elf32_executable_file5_segments in
-  let entr = f5.elf32_executable_file5_header.elf32_entry in
-  match List.filter (fun sg -> sg.elf32_segment_type = elf_pt_load) segs with
-    | []    -> fail "elf32_construct_image: an executable ELF file must have at least one loadable segment"
-    | load  ->
-      mapM (fun sg ->
-        if sg.elf32_segment_memsz = 0 then
-          return []
-        else if sg.elf32_segment_memsz = sg.elf32_segment_size then
-          return [(sg.elf32_segment_body, sg.elf32_segment_base)]
-        else if sg.elf32_segment_size < sg.elf32_segment_memsz then
-          (* Cannot be negative due to check in constructing [f5]. *)
-          let diff  = sg.elf32_segment_memsz - sg.elf32_segment_size in
-          let zeros = Bitstring.zeros diff in
-          let addr  = sg.elf32_segment_base + sg.elf32_segment_size in
-            return [(sg.elf32_segment_body, sg.elf32_segment_base); (zeros, addr)]
-        else
-          fail "elf32_construct_image: invariant invalidated") load >>= fun bs_base ->
-      return (List.concat bs_base, nat_of_elf32_addr entr)
-  end
-
-(** [elf64_construct_image f5] constructs a memory image from an elf64_executable5 object
-  * [f5].  The function returns the following:
-  *    * A list of bytes with a corresponding address where they should be located
-  *      in the program image and,
-  *    * The entry point for the process.  All addresses in the aforementioned list
-  *      should be interpreted wrt this address.
-  * [construct_image] fails if a loadable segment has a memory size smaller than
-  * its associated file size, an error according to the ELF spec.  This should
-  * never happen as relevant checks are made when refining an elf_executable_file4
-  * into an elf_executable_file5.  The function may also fail if there are no loadable
-  * segments in this executable file, again an error.
-  * By the ELF specification, you may assume that the list of bitstring, elf32_addr
-  * pairs is sorted ascending on the second component, i.e. that all pairs are in
-  * order of the address at which point they should be loaded in memory.
-  *)
-val elf64_construct_image : elf64_executable_file5 -> error (list (bitstring * nat) * nat)
-let elf64_construct_image f5 =
-  let segs = f5.elf64_executable_file5_segments in
-  let entr = f5.elf64_executable_file5_header.elf64_entry in
-  match List.filter (fun sg -> sg.elf64_segment_type = elf_pt_load) segs with
-    | []    -> fail "elf64_construct_image: an executable ELF file must have at least one loadable segment"
-    | load  ->
-      mapM (fun sg ->
-        if sg.elf64_segment_memsz = 0 then
-          return []
-        else if sg.elf64_segment_memsz = sg.elf64_segment_size then
-          return [(sg.elf64_segment_body, sg.elf64_segment_base)]
-        else if sg.elf64_segment_size < sg.elf64_segment_memsz then
-          (* Cannot be negative due to check in constructing [f5]. *)
-          let diff  = sg.elf64_segment_memsz - sg.elf64_segment_size in
-          let zeros = Bitstring.zeros diff in
-          let addr  = sg.elf64_segment_base + sg.elf64_segment_size in
-            return [(sg.elf64_segment_body, sg.elf64_segment_base); (zeros, addr)]
-        else
-          fail "elf64_construct_image: invariant invalidated") load >>= fun bs_base ->
-      return (List.concat bs_base, nat_of_elf64_addr entr)
-  end
-
-(** [string_of_elf32_executable_file5 hdr_bdl pht_bdl sht_bdl f5] produces a string
-  * representation of elf32_executable_file5 [f5] using user-supplied print bundles.
-  *)
-val string_of_elf32_executable_file5 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file5 -> string
-let string_of_elf32_executable_file5 hdr_bdl pht_bdl sht_bdl f5 =
-  let sht =
-    match f5.elf32_executable_file5_section_header_table with
-      | Nothing  -> "\tNo section header table present"
-      | Just sht -> string_of_elf32_section_header_table' sht_bdl f5.elf32_executable_file5_section_header_string_table sht
-    end
-  in
-  unlines [
-    "\n*Type elf32_executable_file5"
-    ; "**Header"
-    ; string_of_elf32_header hdr_bdl f5.elf32_executable_file5_header
-    ; "**Program header table:"
-    ; string_of_elf32_program_header_table pht_bdl f5.elf32_executable_file5_program_header_table
-    ; "**Section header table:"
-    ; sht
-    ; "**Section header string table:"
-    ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f5.elf32_executable_file5_section_header_string_table))
-    ; "**Interpreted segments:"
-    ; unlines (List.map (fun x -> "\n" ^ string_of_elf32_interpreted_segment x) f5.elf32_executable_file5_segments)
-    ; "**Body:"
-    ; "\tUninterpreted data of length " ^ show (Bitstring.length f5.elf32_executable_file5_body)
-    ]
-
-(** [string_of_elf64_executable_file5 hdr_bdl pht_bdl sht_bdl f5] produces a string
-  * representation of elf64_executable_file5 [f5] using user-supplied print bundles.
-  *)
-val string_of_elf64_executable_file5 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file5 -> string
-let string_of_elf64_executable_file5 hdr_bdl pht_bdl sht_bdl f5 =
-  let sht =
-    match f5.elf64_executable_file5_section_header_table with
-      | Nothing  -> "\tNo section header table present"
-      | Just sht -> string_of_elf64_section_header_table' sht_bdl f5.elf64_executable_file5_section_header_string_table sht
-    end
-  in
-  unlines [
-    "\n*Type elf64_executable_file5"
-    ; "**Header"
-    ; string_of_elf64_header hdr_bdl f5.elf64_executable_file5_header
-    ; "**Program header table:"
-    ; string_of_elf64_program_header_table pht_bdl f5.elf64_executable_file5_program_header_table
-    ; "**Section header table:"
-    ; sht
-    ; "**Section header string table:"
-    ; unlines (List.map (fun x -> "\t" ^ x) (get_strings f5.elf64_executable_file5_section_header_string_table))
-    ; "**Interpreted segments:"
-    ; unlines (List.map (fun x -> "\n" ^ string_of_elf64_interpreted_segment x) f5.elf64_executable_file5_segments)
-    ; "**Body:"
-    ; "\tUninterpreted data of length " ^ show (Bitstring.length f5.elf64_executable_file5_body)
-    ]
\ No newline at end of file