open import Basic_classes
open import Num
open import Maybe
open import String

open import Elf_executable_file2
open import Elf_header
open import Elf_interpreted_segment
open import Elf_types
open import Elf_section_header_table
open import Elf_symbol_table
open import Elf_program_header_table
open import String_table

open import Bitstring
open import Error
open import Missing_pervasives
open import Show

(** Type [elf32_executable_file3] 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, with all other data being left uninterpreted.
  *)
type elf32_executable_file3 =
  <| elf32_executable_file3_header               : elf32_header (** The ELF header (mandatory) *)
   ; elf32_executable_file3_program_header_table : elf32_program_header_table (** The program header table (mandatory) *)
   ; elf32_executable_file3_section_header_table : maybe elf32_section_header_table (** The section header table (optional) *)
   ; elf32_executable_file3_body                 : bitstring (** Uninterpreted body *)
   |>

class (HasElf32ExecutableFile3 'a)
  val get_elf32_executable_file3 : 'a -> elf32_executable_file3
end

instance (HasElf32ExecutableFile3 elf32_executable_file3)
  let get_elf32_executable_file3 f3 = f3
end

instance (HasElf32ExecutableFile2 elf32_executable_file3)
  let get_elf32_executable_file2 f3 =
    <| elf32_executable_file2_header = f3.elf32_executable_file3_header;
         elf32_executable_file2_program_header_table = f3.elf32_executable_file3_program_header_table;
         elf32_executable_file2_body = f3.elf32_executable_file3_body |>
end

instance (HasElf32Header elf32_executable_file3)
  let get_elf32_header f3 = f3.elf32_executable_file3_header
end

instance (HasElf32ProgramHeaderTable elf32_executable_file3)
  let get_elf32_program_header_table f3 =
    Just (f3.elf32_executable_file3_program_header_table)
end

instance (HasElf32SectionHeaderTable elf32_executable_file3)
  let get_elf32_section_header_table f3 =
    f3.elf32_executable_file3_section_header_table
end

(** Type [elf64_executable_file3] 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, with all other data being left uninterpreted.
  *)
type elf64_executable_file3 =
  <| elf64_executable_file3_header               : elf64_header (** The ELF header (mandatory) *)
   ; elf64_executable_file3_program_header_table : elf64_program_header_table (** The program header table (mandatory) *)
   ; elf64_executable_file3_section_header_table : maybe elf64_section_header_table (** The section header table (optional) *)
   ; elf64_executable_file3_body                 : bitstring (** Uninterpreted body *)
   |>

class (HasElf64ExecutableFile3 'a)
  val get_elf64_executable_file3 : 'a -> elf64_executable_file3
end

instance (HasElf64ExecutableFile3 elf64_executable_file3)
  let get_elf64_executable_file3 f3 = f3
end

instance (HasElf64ExecutableFile2 elf64_executable_file3)
  let get_elf64_executable_file2 f3 =
    <| elf64_executable_file2_header = f3.elf64_executable_file3_header;
         elf64_executable_file2_program_header_table = f3.elf64_executable_file3_program_header_table;
         elf64_executable_file2_body = f3.elf64_executable_file3_body |>
end

instance (HasElf64Header elf64_executable_file3)
  let get_elf64_header f3 = f3.elf64_executable_file3_header
end

instance (HasElf64ProgramHeaderTable elf64_executable_file3)
  let get_elf64_program_header_table f3 =
    Just (f3.elf64_executable_file3_program_header_table)
end

instance (HasElf64SectionHeaderTable elf64_executable_file3)
  let get_elf64_section_header_table f3 =
    f3.elf64_executable_file3_section_header_table
end

(** [refine_elf32_executable_file2 f2] refines an elf32_executable_file2 [f2] into
  * an elf32_executable_file3 by adding the optional section header table.
  *)
val refine_elf32_executable_file2 : elf32_executable_file2 -> error elf32_executable_file3
let refine_elf32_executable_file2 f2 =
  let hdr         = f2.elf32_executable_file2_header in
  let pht         = f2.elf32_executable_file2_program_header_table in
  let endian      = get_elf32_header_endianness hdr in
  let bs1         = f2.elf32_executable_file2_body in
  let sentries    = nat_of_elf32_half hdr.elf32_shnum in
  let sentry_size = nat_of_elf32_half hdr.elf32_shentsize * 8 in
  let ssize       = sentries * sentry_size in
    if ssize = 0 then
      return <| elf32_executable_file3_header = hdr;
        elf32_executable_file3_program_header_table = pht;
        elf32_executable_file3_section_header_table = Nothing;
        elf32_executable_file3_body = bs1 |>
    else
      let soffset     = nat_of_elf32_off hdr.elf32_shoff * 8 in
      let (_, scut)   = partition soffset bs1 in
      let (sexact, _) = partition ssize scut in
        (* Bitstring irrelevant below as exact size used... *)
        read_elf32_section_header_table ssize endian sexact >>= fun (sht, _) ->
          return <| elf32_executable_file3_header = hdr;
            elf32_executable_file3_program_header_table = pht;
            elf32_executable_file3_section_header_table = Just sht;
            elf32_executable_file3_body = bs1 |>

(** [refine_elf64_executable_file2 f2] refines an elf64_executable_file2 [f2] into
  * an elf64_executable_file3 by adding the optional section header table.
  *)
val refine_elf64_executable_file2 : elf64_executable_file2 -> error elf64_executable_file3
let refine_elf64_executable_file2 f2 =
  let hdr         = f2.elf64_executable_file2_header in
  let pht         = f2.elf64_executable_file2_program_header_table in
  let endian      = get_elf64_header_endianness hdr in
  let bs1         = f2.elf64_executable_file2_body in
  let sentries    = nat_of_elf64_half hdr.elf64_shnum in
  let sentry_size = nat_of_elf64_half hdr.elf64_shentsize * 8 in
  let ssize       = sentries * sentry_size in
    if ssize = 0 then
      return <| elf64_executable_file3_header = hdr;
        elf64_executable_file3_program_header_table = pht;
        elf64_executable_file3_section_header_table = Nothing;
        elf64_executable_file3_body = bs1 |>
    else
      let soffset     = nat_of_elf64_off hdr.elf64_shoff * 8 in
      let (_, scut)   = partition soffset bs1 in
      let (sexact, _) = partition ssize scut in
        (* Bitstring irrelevant below as exact size used... *)
        read_elf64_section_header_table ssize endian sexact >>= fun (sht, _) ->
          return <| elf64_executable_file3_header = hdr;
            elf64_executable_file3_program_header_table = pht;
            elf64_executable_file3_section_header_table = Just sht;
            elf64_executable_file3_body = bs1 |>

(** [read_elf32_executable_file3 bs0] reads an elf32_executable_file3 from
  * bitstring [bs0].
  *)
val read_elf32_executable_file3 : bitstring -> error elf32_executable_file3
let read_elf32_executable_file3 bs0 =
  read_elf32_executable_file2 bs0 >>= refine_elf32_executable_file2

(** [read_elf64_executable_file3 bs0] reads an elf64_executable_file3 from
  * bitstring [bs0].
  *)
val read_elf64_executable_file3 : bitstring -> error elf64_executable_file3
let read_elf64_executable_file3 bs0 =
  read_elf64_executable_file2 bs0 >>= refine_elf64_executable_file2

(** string_of_elf32_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3]
  * creates a string representation of [f3].
  *)
val string_of_elf32_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf32_executable_file3 -> string
let string_of_elf32_executable_file3 hdr_bdl pht_bdl sht_bdl f3 =
  let sht =
    match f3.elf32_executable_file3_section_header_table with
      | Nothing  -> "\tNo section header table present"
      | Just sht -> string_of_elf32_section_header_table sht_bdl sht
    end
  in
    unlines [
      "\n*Type elf32_executable_file3:"
    ; "**Header:"
    ; string_of_elf32_header hdr_bdl f3.elf32_executable_file3_header
    ; "**Program header table:"
    ; string_of_elf32_program_header_table pht_bdl f3.elf32_executable_file3_program_header_table
    ; "**Section header table:"
    ; sht
    ; "**Body:"
    ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf32_executable_file3_body)
    ]

(** string_of_elf64_executable_file3 hdr_os hdr_proc pht_os pht_proc sht_oc sht_proc sht_user f3]
  * creates a string representation of [f3].
  *)
val string_of_elf64_executable_file3 : hdr_print_bundle -> pht_print_bundle -> sht_print_bundle -> elf64_executable_file3 -> string
let string_of_elf64_executable_file3 hdr_bdl pht_bdl sht_bdl f3 =
  let sht =
    match f3.elf64_executable_file3_section_header_table with
      | Nothing  -> "\tNo section header table present"
      | Just sht -> string_of_elf64_section_header_table sht_bdl sht
    end
  in
    unlines [
      "\n*Type elf64_executable_file3:"
    ; "**Header:"
    ; string_of_elf64_header hdr_bdl f3.elf64_executable_file3_header
    ; "**Program header table:"
    ; string_of_elf64_program_header_table pht_bdl f3.elf64_executable_file3_program_header_table
    ; "**Section header table:"
    ; sht
    ; "**Body:"
    ; "\tUninterpreted data of length " ^ show (Bitstring.length f3.elf64_executable_file3_body)
    ]

val get_elf32_section_header_string_table : elf32_executable_file3 -> error string_table
let get_elf32_section_header_string_table f3 =
  let bs0 = f3.elf32_executable_file3_body in
  match f3.elf32_executable_file3_section_header_table with
    | Nothing  -> return String_table.empty
    | Just sht ->
      let idx  = nat_of_elf32_half f3.elf32_executable_file3_header.elf32_shstrndx in
        match List.index sht idx with
          | Nothing -> fail "get_elf32_string_table: 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 (String_table.mk_string_table strings Missing_pervasives.null_char)
        end
  end

val get_elf64_section_header_string_table : elf64_executable_file3 -> error string_table
let get_elf64_section_header_string_table f3 =
  let bs0 = f3.elf64_executable_file3_body in
  match f3.elf64_executable_file3_section_header_table with
    | Nothing  -> return String_table.empty
    | Just sht ->
      let idx  = nat_of_elf64_half f3.elf64_executable_file3_header.elf64_shstrndx in
        match List.index sht idx with
          | Nothing -> fail "get_elf64_string_table: 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 (String_table.mk_string_table strings Missing_pervasives.null_char)
        end
  end

val get_elf32_symbol_string_table : elf32_executable_file3 -> error string_table
let get_elf32_symbol_string_table f3 =
  let bs0 = f3.elf32_executable_file3_body in
  let hdr = f3.elf32_executable_file3_header in
    match f3.elf32_executable_file3_section_header_table with
      | Nothing  -> return String_table.empty
      | Just sht ->
        let strtabs = Missing_pervasives.mapMaybei (fun index sect ->
          if nat_of_elf32_word sect.elf32_sh_type = sht_strtab then
            if index = nat_of_elf32_half hdr.elf32_shstrndx then
              Nothing
            else
              Just sect
          else
            Nothing) sht
        in
        let strings = List.map (fun 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 bs1     = Bitstring.offset_and_cut offset size bs0 in
            let strings = Bitstring.string_of_bitstring bs1 in
              String_table.mk_string_table strings Missing_pervasives.null_char) strtabs
        in
          String_table.concat strings
    end

val get_elf64_symbol_string_table : elf64_executable_file3 -> error string_table
let get_elf64_symbol_string_table f3 =
  let bs0 = f3.elf64_executable_file3_body in
  let hdr = f3.elf64_executable_file3_header in
    match f3.elf64_executable_file3_section_header_table with
      | Nothing  -> return String_table.empty
      | Just sht ->
        let strtabs = Missing_pervasives.mapMaybei (fun index sect ->
          if nat_of_elf64_word sect.elf64_sh_type = sht_strtab then
            if index = nat_of_elf64_half hdr.elf64_shstrndx then
              Nothing
            else
              Just sect
          else
            Nothing) sht
        in
        let strings = List.map (fun 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 bs1     = Bitstring.offset_and_cut offset size bs0 in
            let strings = Bitstring.string_of_bitstring bs1 in
              String_table.mk_string_table strings Missing_pervasives.null_char) strtabs
        in
          String_table.concat strings
    end

val get_elf32_interpreted_segments : elf32_executable_file3 -> error (list elf32_interpreted_segment)
let get_elf32_interpreted_segments f3 =
  let pht = f3.elf32_executable_file3_program_header_table in
  let bdy = f3.elf32_executable_file3_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
    mapM (fun sg ->
      if sg.elf32_segment_memsz < sg.elf32_segment_size then
        fail "get_elf32_interpreted_segments: memory size of segment cannot be less than file size"
      else
        return sg) segs

val get_elf64_interpreted_segments : elf64_executable_file3 -> error (list elf64_interpreted_segment)
let get_elf64_interpreted_segments f3 =
  let pht = f3.elf64_executable_file3_program_header_table in
  let bdy = f3.elf64_executable_file3_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
    mapM (fun sg ->
      if sg.elf64_segment_memsz < sg.elf64_segment_size then
        fail "get_elf64_interpreted_segments: memory size of segment cannot be less than file size"
      else
        return sg) segs

type executable_process_image =
  list (bitstring * nat) * nat

val get_elf32_executable_image : elf32_executable_file3 -> error executable_process_image
let get_elf32_executable_image f3 =
  let entr = f3.elf32_executable_file3_header.elf32_entry in
  get_elf32_interpreted_segments f3 >>= fun segs ->
    match List.filter (fun sg -> sg.elf32_segment_type = elf_pt_load) segs with
      | []    -> fail "get_elf32_executable_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 [segs]. *)
              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 "get_elf32_executable_image: invariant invalidated") load >>= fun bs_base ->
          return (List.concat bs_base, nat_of_elf32_addr entr)
    end

val get_elf64_executable_image : elf64_executable_file3 -> error executable_process_image
let get_elf64_executable_image f3 =
  let entr = f3.elf64_executable_file3_header.elf64_entry in
  get_elf64_interpreted_segments f3 >>= fun segs ->
    match List.filter (fun sg -> sg.elf64_segment_type = elf_pt_load) segs with
      | []    -> fail "get_elf64_executable_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 [segs]. *)
              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 "get_elf64_executable_image: invariant invalidated") load >>= fun bs_base ->
          return (List.concat bs_base, nat_of_elf64_addr entr)
    end

val get_elf32_symbol_table : elf32_executable_file3 -> error elf32_symbol_table
let get_elf32_symbol_table f3 =
  let bs0 = f3.elf32_executable_file3_body in
  let hdr = f3.elf32_executable_file3_header in
  let endian = get_elf32_header_endianness hdr in
  match f3.elf32_executable_file3_section_header_table with
    | Nothing    -> return []
    | Just sects ->
      let symtabs = List.filter (fun sect ->
        nat_of_elf32_word sect.elf32_sh_type = sht_symtab) sects
      in
        if List.length symtabs = 0 then
          return []
        else if List.length symtabs = 1 then
          match List.index symtabs 0 with
            | Nothing -> fail "get_elf32_symbol_table: invariant failed"
            | Just symtab ->
              let offset = nat_of_elf32_off symtab.elf32_sh_offset * 8 in
              let size   = nat_of_elf32_word symtab.elf32_sh_size * 8 in
              let relevant = Bitstring.offset_and_cut offset size bs0 in
                read_elf32_symbol_table endian relevant
          end
        else
          fail "get_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB"
  end

val get_elf64_symbol_table : elf64_executable_file3 -> error elf64_symbol_table
let get_elf64_symbol_table f3 =
  let bs0 = f3.elf64_executable_file3_body in
  let hdr = f3.elf64_executable_file3_header in
  let endian = get_elf64_header_endianness hdr in
  match f3.elf64_executable_file3_section_header_table with
    | Nothing    -> return []
    | Just sects ->
      let symtabs = List.filter (fun sect ->
        nat_of_elf64_word sect.elf64_sh_type = sht_symtab) sects
      in
        if List.length symtabs = 0 then
          return []
        else if List.length symtabs = 1 then
          match List.index symtabs 0 with
            | Nothing -> fail "get_elf64_symbol_table: invariant failed"
            | Just symtab ->
              let offset = nat_of_elf64_off symtab.elf64_sh_offset * 8 in
              let size   = nat_of_elf64_xword symtab.elf64_sh_size * 8 in
              let relevant = Bitstring.offset_and_cut offset size bs0 in
                read_elf64_symbol_table endian relevant
          end
        else
          fail "get_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_SYMTAB"
  end

val get_elf32_dynamic_symbol_table : elf32_executable_file3 -> error elf32_symbol_table
let get_elf32_dynamic_symbol_table f3 =
  let bs0 = f3.elf32_executable_file3_body in
  let hdr = f3.elf32_executable_file3_header in
  let endian = get_elf32_header_endianness hdr in
  match f3.elf32_executable_file3_section_header_table with
    | Nothing    -> return []
    | Just sects ->
      let symtabs = List.filter (fun sect ->
        nat_of_elf32_word sect.elf32_sh_type = sht_dynsym) sects
      in
        if List.length symtabs = 0 then
          return []
        else if List.length symtabs = 1 then
          match List.index symtabs 0 with
            | Nothing -> fail "get_elf32_symbol_table: invariant failed"
            | Just symtab ->
              let offset = nat_of_elf32_off symtab.elf32_sh_offset * 8 in
              let size   = nat_of_elf32_word symtab.elf32_sh_size * 8 in
              let relevant = Bitstring.offset_and_cut offset size bs0 in
                read_elf32_symbol_table endian relevant
          end
        else
          fail "get_elf32_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM"
  end

val get_elf64_dynamic_symbol_table : elf64_executable_file3 -> error elf64_symbol_table
let get_elf64_dynamic_symbol_table f3 =
  let bs0 = f3.elf64_executable_file3_body in
  let hdr = f3.elf64_executable_file3_header in
  let endian = get_elf64_header_endianness hdr in
  match f3.elf64_executable_file3_section_header_table with
    | Nothing    -> return []
    | Just sects ->
      let symtabs = List.filter (fun sect ->
        nat_of_elf64_word sect.elf64_sh_type = sht_dynsym) sects
      in
        if List.length symtabs = 0 then
          return []
        else if List.length symtabs = 1 then
          match List.index symtabs 0 with
            | Nothing -> fail "get_elf64_symbol_table: invariant failed"
            | Just symtab ->
              let offset = nat_of_elf64_off symtab.elf64_sh_offset * 8 in
              let size   = nat_of_elf64_xword symtab.elf64_sh_size * 8 in
              let relevant = Bitstring.offset_and_cut offset size bs0 in
                read_elf64_symbol_table endian relevant
          end
        else
          fail "get_elf64_symbol_table: an ELF file may only have one symbol table of type SHT_DYNSYM"
  end