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)
    ]