open import Basic_classes
open import String

open import Endianness

open import Elf_header
open import Elf_types

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

(** Type [elf32_file1] represents the first lazy unfolding of the structure
  * of an ELF file, wherein the ELF header is populated and all other data
  * is left uninterpreted.
  *)
type elf32_file1 =
  <| elf32_file1_header : elf32_header (** The ELF header (mandatory) *)
   ; elf32_file1_body   : bitstring    (** Uninterpreted data *)
   |>

class (HasElf32File1 'a)
  val get_elf32_file1 : 'a -> elf32_file1
end

instance (HasElf32File1 elf32_file1)
  let get_elf32_file1 f1 = f1
end

instance (HasElf32Header elf32_file1)
  let get_elf32_header file1 = file1.elf32_file1_header
end

(** Type [elf64_file1] represents the first lazy unfolding of the structure
  * of an ELF file, wherein the ELF header is populated and all other data
  * is left uninterpreted.
  *)
type elf64_file1 =
  <| elf64_file1_header : elf64_header (** The ELF header (mandatory) *)
   ; elf64_file1_body   : bitstring    (** Uninterpreted data *)
   |>

class (HasElf64File1 'a)
  val get_elf64_file1 : 'a -> elf64_file1
end

instance (HasElf64File1 elf64_file1)
  let get_elf64_file1 f1 = f1
end

instance (HasElf64Header elf64_file1)
  let get_elf64_header file1 = file1.elf64_file1_header
end

val string_of_elf32_file1 : hdr_print_bundle -> elf32_file1 -> string
let string_of_elf32_file1 hdr_bdl f1 =
  unlines [
    "\n*Type elf32_file1:"
  ; "**Header:"
  ; string_of_elf32_header hdr_bdl f1.elf32_file1_header
  ; "Body:"
  ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf32_file1_body)
  ]

val string_of_elf64_file1 : hdr_print_bundle -> elf64_file1 -> string
let string_of_elf64_file1 hdr_bdl f1 =
  unlines [
    "\n*Type elf64_file1:"
  ; "**Header:"
  ; string_of_elf64_header hdr_bdl f1.elf64_file1_header
  ; "Body:"
  ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf64_file1_body)
  ]

(** [is_executable_efl32_file1] tests whether the ELF file is an executable
  * file type.
  *)
val is_executable_elf32_file1 : elf32_file1 -> bool
let is_executable_elf32_file1 f1 =
  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_exec

(** [is_executable_efl64_file1] tests whether the ELF file is an executable
  * file type.
  *)
val is_executable_elf64_file1 : elf64_file1 -> bool
let is_executable_elf64_file1 f1 =
  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_exec

(** [is_shared_object_elf32_file1] tests whether the ELF file is a shared object
  * file type.
  *)
val is_shared_object_elf32_file1 : elf32_file1 -> bool
let is_shared_object_elf32_file1 f1 =
  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_dyn

(** [is_shared_object_elf64_file1] tests whether the ELF file is a shared object
* file type.
*)
val is_shared_object_elf64_file1 : elf64_file1 -> bool
let is_shared_object_elf64_file1 f1 =
  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_dyn

(** [read_elf32_file1 bs] lazily unfolds [bs] revealing the ELF file's header,
  * leaving all other data uninterpreted.
  *)
val read_elf32_file1 : bitstring -> error elf32_file1
let read_elf32_file1 bs0 =
  read_elf32_header bs0 >>= fun (hdr, bs1) ->
  return <| elf32_file1_header = hdr; elf32_file1_body = bs0 |>

(** [read_elf64_file1 bs] lazily unfolds [bs] revealing the ELF file's header,
  * leaving all other data uninterpreted.
  *)
val read_elf64_file1 : bitstring -> error elf64_file1
let read_elf64_file1 bs0 =
  read_elf64_header bs0 >>= fun (hdr, bs1) ->
  return <| elf64_file1_header = hdr; elf64_file1_body = bs0 |>