open import Basic_classes
open import Bool
open import Maybe
open import Num

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

open import Elf_file1
open import Elf_header
open import Elf_section_header_table
open import Elf_types

type elf32_linking_file2 =
  <| elf32_linking_file2_header               : elf32_header
   ; elf32_linking_file2_body                 : bitstring
   ; elf32_linking_file2_section_header_table : elf32_section_header_table
   |>

class (HasElf32LinkingFile2 'a)
  val get_elf32_linking_file2 : 'a -> elf32_linking_file2
end

instance (HasElf32LinkingFile2 elf32_linking_file2)
  let get_elf32_linking_file2 f2 = f2
end

instance (HasElf32File1 elf32_linking_file2)
  let get_elf32_file1 f2 =
    <| elf32_file1_header = f2.elf32_linking_file2_header;
         elf32_file1_body = f2.elf32_linking_file2_body |>
end

instance (HasElf32Header elf32_linking_file2)
  let get_elf32_header f2 = f2.elf32_linking_file2_header
end

instance (HasElf32SectionHeaderTable elf32_linking_file2)
  let get_elf32_section_header_table f2 = Just f2.elf32_linking_file2_section_header_table
end

type elf64_linking_file2 =
  <| elf64_linking_file2_header               : elf64_header
   ; elf64_linking_file2_body                 : bitstring
   ; elf64_linking_file2_section_header_table : elf64_section_header_table
   |>

class (HasElf64LinkingFile2 'a)
  val get_elf64_linking_file2 : 'a -> elf64_linking_file2
end

instance (HasElf64LinkingFile2 elf64_linking_file2)
  let get_elf64_linking_file2 f2 = f2
end

instance (HasElf64File1 elf64_linking_file2)
  let get_elf64_file1 f2 =
    <| elf64_file1_header = f2.elf64_linking_file2_header;
         elf64_file1_body = f2.elf64_linking_file2_body |>
end

instance (HasElf64Header elf64_linking_file2)
  let get_elf64_header f2 = f2.elf64_linking_file2_header
end

instance (HasElf64SectionHeaderTable elf64_linking_file2)
  let get_elf64_section_header_table f2 = Just f2.elf64_linking_file2_section_header_table
end

val refine_elf32_file1 : elf32_file1 -> error elf32_linking_file2
let refine_elf32_file1 f1 =
  if not (is_linkable_elf32_file1 f1) then
    fail "refine_elf32_file1: not a linkable file"
  else
    let hdr         = f1.elf32_file1_header in
    let endian      = get_elf32_header_endianness hdr in
    let bs1         = f1.elf32_file1_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
        fail "refine_elf32_file1: section header table not present"
      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_linking_file2_header = hdr;
              elf32_linking_file2_body = bs1;
              elf32_linking_file2_section_header_table = sht |>

val read_elf32_linking_file2 : bitstring -> error elf32_linking_file2
let read_elf32_linking_file2 bs0 =
  read_elf32_file1 bs0 >>= refine_elf32_file1

val string_of_elf32_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf32_linking_file2 -> string
let string_of_elf32_linking_file2 hdr_bdl sht_bdl f2 =
  unlines [
    "\n*Type elf32_linking_file2:"
  ; "**Header:"
  ; string_of_elf32_header hdr_bdl f2.elf32_linking_file2_header
  ; "**Program header table:"
  ; string_of_elf32_section_header_table sht_bdl f2.elf32_linking_file2_section_header_table
  ; "**Body:"
  ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf32_linking_file2_body)
  ]

val refine_elf64_file1 : elf64_file1 -> error elf64_linking_file2
let refine_elf64_file1 f1 =
  if not (is_linkable_elf64_file1 f1) then
    fail "refine_elf64_file1: not a linkable file"
  else
    let hdr         = f1.elf64_file1_header in
    let endian      = get_elf64_header_endianness hdr in
    let bs1         = f1.elf64_file1_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
        fail "refine_elf64_file1: section header table not present"
      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_linking_file2_header = hdr;
              elf64_linking_file2_body = bs1;
              elf64_linking_file2_section_header_table = sht |>

val read_elf64_linking_file2 : bitstring -> error elf64_linking_file2
let read_elf64_linking_file2 bs0 =
  read_elf64_file1 bs0 >>= refine_elf64_file1

val string_of_elf64_linking_file2 : hdr_print_bundle -> sht_print_bundle -> elf64_linking_file2 -> string
let string_of_elf64_linking_file2 hdr_bdl sht_bdl f2 =
  unlines [
    "\n*Type elf64_linking_file2:"
  ; "**Header:"
  ; string_of_elf64_header hdr_bdl f2.elf64_linking_file2_header
  ; "**Program header table:"
  ; string_of_elf64_section_header_table sht_bdl f2.elf64_linking_file2_section_header_table
  ; "**Body:"
  ; "\tUninterpreted data of length " ^ show (Bitstring.length f2.elf64_linking_file2_body)
  ]