open import Basic_classes
open import Bool
open import Num
open import String

open import Elf_types

open import Bitstring
open import Missing_pervasives
open import Show

type elf32_interpreted_segment =
  <| elf32_segment_body  : bitstring            (** Body of the segment *)
   ; elf32_segment_type  : nat                  (** Type of the segment *)
   ; elf32_segment_size  : nat                  (** Size of the segment in bytes *)
   ; elf32_segment_memsz : nat                  (** Size of the segment in memory in bytes *)
   ; elf32_segment_base  : nat                  (** Base address of the segment *)
   ; elf32_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *)
   |>

type elf64_interpreted_segment =
  <| elf64_segment_body  : bitstring            (** Body of the segment *)
   ; elf64_segment_type  : nat                  (** Type of the segment *)
   ; elf64_segment_size  : nat                  (** Size of the segment in bytes *)
   ; elf64_segment_memsz : nat                  (** Size of the segment in memory in bytes *)
   ; elf64_segment_base  : nat                  (** Base address of the segment *)
   ; elf64_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *)
   |>

val elf32_interpret_program_header_flags : elf32_word -> (bool * bool * bool)
let elf32_interpret_program_header_flags flags =
  let zero = elf32_word_of_int32 0 in
  let one  = elf32_word_of_int32 1 in
  let two  = elf32_word_of_int32 2 in
  let four = elf32_word_of_int32 4 in
    (not (elf32_word_land flags one = zero),
      not (elf32_word_land flags two = zero),
      not (elf32_word_land flags four = zero))

val elf64_interpret_program_header_flags : elf64_word -> (bool * bool * bool)
let elf64_interpret_program_header_flags flags =
  let zero = elf64_word_of_int32 0 in
  let one  = elf64_word_of_int32 1 in
  let two  = elf64_word_of_int32 2 in
  let four = elf64_word_of_int32 4 in
    (not (elf64_word_land flags one = zero),
      not (elf64_word_land flags two = zero),
      not (elf64_word_land flags four = zero))

val string_of_flags : (bool * bool * bool) -> string
let string_of_flags flags =
  match flags with
    | (read, write, execute) ->
        bracket [show read; show write; show execute]
  end

val string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string
let string_of_elf32_interpreted_segment seg =
  unlines [
    "Body of length: " ^ show (Bitstring.length seg.elf32_segment_body)
  ; "Segment type: " ^ show seg.elf32_segment_type
  ; "Segment size: " ^ show seg.elf32_segment_size
  ; "Segment memory size: " ^ show seg.elf32_segment_memsz
  ; "Segment base address: " ^ show seg.elf32_segment_base
  ; "Segment flags: " ^ string_of_flags seg.elf32_segment_flags
  ]

val string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string
let string_of_elf64_interpreted_segment seg =
  unlines [
    "Body of length: " ^ show (Bitstring.length seg.elf64_segment_body)
  ; "Segment type: " ^ show seg.elf64_segment_type
  ; "Segment size: " ^ show seg.elf64_segment_size
  ; "Segment memory size: " ^ show seg.elf64_segment_memsz
  ; "Segment base address: " ^ show seg.elf64_segment_base
  ; "Segment flags: " ^ string_of_flags seg.elf64_segment_flags
  ]