(*Generated by Lem from elf_interpreted_segment.lem.*)
(** [elf_interpreted_segment] defines interpreted segments, i.e. the contents of
  * a program header table entry converted to more amenable types, and operations
  * built on top of them.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_num
open Lem_string

open Elf_types_native_uint
open Elf_program_header_table

open Byte_sequence
open Missing_pervasives
open Show

open Hex_printing

(** [elf32_interpreted_segment] represents an ELF32 interpreted segment, i.e. the
  * contents of an ELF program header table entry converted into more amenable
  * (infinite precision) types, for manipulation.
  * Invariant: the nth entry of the program header table corresponds to the nth
  * entry of the list of interpreted segments in an [elf32_file] record.  The
  * lengths of the two lists are exactly the same.
  *)
type elf32_interpreted_segment =
  { elf32_segment_body  : byte_sequence        (** Body of the segment *)
   ; elf32_segment_type  : Nat_big_num.num              (** Type of the segment *)
   ; elf32_segment_size  : Nat_big_num.num              (** Size of the segment in bytes *)
   ; elf32_segment_memsz : Nat_big_num.num              (** Size of the segment in memory in bytes *)
   ; elf32_segment_base  : Nat_big_num.num              (** Base address of the segment *)
   ; elf32_segment_paddr : Nat_big_num.num              (** Physical address of segment *)
   ; elf32_segment_align : Nat_big_num.num              (** Alignment of the segment *)
   ; elf32_segment_offset : Nat_big_num.num             (** Offset of the segment *)
   ; elf32_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *)
   }

(** [elf64_interpreted_segment] represents an ELF64 interpreted segment, i.e. the
  * contents of an ELF program header table entry converted into more amenable
  * (infinite precision) types, for manipulation.
  * Invariant: the nth entry of the program header table corresponds to the nth
  * entry of the list of interpreted segments in an [elf64_file] record.  The
  * lengths of the two lists are exactly the same.
  *)
type elf64_interpreted_segment =
  { elf64_segment_body  : byte_sequence        (** Body of the segment *)
   ; elf64_segment_type  : Nat_big_num.num              (** Type of the segment *)
   ; elf64_segment_size  : Nat_big_num.num              (** Size of the segment in bytes *)
   ; elf64_segment_memsz : Nat_big_num.num              (** Size of the segment in memory in bytes *)
   ; elf64_segment_base  : Nat_big_num.num              (** Base address of the segment *)
   ; elf64_segment_paddr : Nat_big_num.num              (** Physical address of segment *)
   ; elf64_segment_align : Nat_big_num.num              (** Alignment of the segment *)
   ; elf64_segment_offset : Nat_big_num.num             (** Offset of the segment *)
   ; elf64_segment_flags : (bool * bool * bool) (** READ, WRITE, EXECUTE flags. *)
   }
   
(** [compare_elf64_interpreted_segment seg1 seg2] is an ordering comparison function
  * on interpreted segments suitable for constructing sets, finite maps and other
  * ordered data types out of.
  *)
(*val compare_elf64_interpreted_segment : elf64_interpreted_segment ->
  elf64_interpreted_segment -> ordering*)
let compare_elf64_interpreted_segment s1 s2:int=   
 (tripleCompare compare_byte_sequence (Lem_list.lexicographic_compare Nat_big_num.compare) (Lem_list.lexicographic_compare Nat_big_num.compare) 
    (s1.elf64_segment_body,
    [s1.elf64_segment_type  ;
     s1.elf64_segment_size  ;
     s1.elf64_segment_memsz ;
     s1.elf64_segment_base  ;
     s1.elf64_segment_paddr ;
     s1.elf64_segment_align ;
     s1.elf64_segment_offset],     
 (let (f1, f2, f3) = (s1.elf64_segment_flags) in
       Lem_list.map natural_of_bool [f1; f2; f3]))
    (s2.elf64_segment_body,
    [s2.elf64_segment_type  ;
     s2.elf64_segment_size  ;
     s2.elf64_segment_memsz ;
     s2.elf64_segment_base  ;
     s2.elf64_segment_paddr ;
     s2.elf64_segment_align ;
     s2.elf64_segment_offset],     
(let (f1, f2, f3) = (s2.elf64_segment_flags) in
       Lem_list.map natural_of_bool [f1; f2; f3])))

let instance_Basic_classes_Ord_Elf_interpreted_segment_elf64_interpreted_segment_dict:(elf64_interpreted_segment)ord_class= ({

  compare_method = compare_elf64_interpreted_segment;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_segment f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> let result = (compare_elf64_interpreted_segment f1 f2) in Lem.orderingEqual result (-1) || Lem.orderingEqual result 0));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_segment f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> let result = (compare_elf64_interpreted_segment f1 f2) in Lem.orderingEqual result 1 || Lem.orderingEqual result 0))})

type elf32_interpreted_segments = elf32_interpreted_segment list
type elf64_interpreted_segments = elf64_interpreted_segment list

(** [elf32_interpreted_program_header_flags w] extracts a boolean triple of flags
  * from the flags field of an interpreted segment.
  *)
(*val elf32_interpret_program_header_flags : elf32_word -> (bool * bool * bool)*)
let elf32_interpret_program_header_flags flags:bool*bool*bool=  
 (let zero = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) in
  let one  = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))) in
  let two  = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 2))) in
  let four = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 4))) in
    (not (Uint32.logand flags one = zero),
      not (Uint32.logand flags two = zero),
      not (Uint32.logand flags four = zero)))

(** [elf64_interpreted_program_header_flags w] extracts a boolean triple of flags
  * from the flags field of an interpreted segment.
  *)
(*val elf64_interpret_program_header_flags : elf64_word -> (bool * bool * bool)*)
let elf64_interpret_program_header_flags flags:bool*bool*bool=  
 (let zero = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0))) in
  let one  = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 1))) in
  let two  = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 2))) in
  let four = (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 4))) in
    (not (Uint32.logand flags one = zero),
      not (Uint32.logand flags two = zero),
      not (Uint32.logand flags four = zero)))

(** [string_of_flags bs] produces a string-based representation of an interpreted
  * segments flags (represented as a boolean triple).
  *)
(*val string_of_flags : (bool * bool * bool) -> string*)
let string_of_flags flags:string=  
 ((match flags with
    | (read, write, execute) ->
        bracket [string_of_bool read; string_of_bool write; string_of_bool execute]
  ))

(** [string_of_elf32_interpreted_segment seg] produces a string-based representation
  * of interpreted segment [seg].
  *)
(*val string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string*)
let string_of_elf32_interpreted_segment seg:string=  
 (unlines [    
("Body of length: " ^ unsafe_hex_string_of_natural( 16) (Byte_sequence.length0 seg.elf32_segment_body))
  ; ("Segment type: " ^ string_of_segment_type (fun _ -> "ABI specific") (fun _ -> "ABI specific") seg.elf32_segment_type)
  ; ("Segment size: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_size)
  ; ("Segment memory size: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_memsz)
  ; ("Segment base address: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_base)
  ; ("Segment physical address: " ^ unsafe_hex_string_of_natural( 16) seg.elf32_segment_paddr)
  ; ("Segment flags: " ^ string_of_flags seg.elf32_segment_flags)
  ])

(** [string_of_elf64_interpreted_segment seg] produces a string-based representation
  * of interpreted segment [seg].
  *)
(*val string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string*)
let string_of_elf64_interpreted_segment seg:string=  
 (unlines [    
("Body of length: " ^ unsafe_hex_string_of_natural( 16) (Byte_sequence.length0 seg.elf64_segment_body))
  ; ("Segment type: " ^ string_of_segment_type (fun _ -> "ABI specific") (fun _ -> "ABI specific") seg.elf64_segment_type)
  ; ("Segment size: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_size)
  ; ("Segment memory size: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_memsz)
  ; ("Segment base address: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_base)
  ; ("Segment physical address: " ^ unsafe_hex_string_of_natural( 16) seg.elf64_segment_paddr)
  ; ("Segment flags: " ^ string_of_flags seg.elf64_segment_flags)
  ])