Source file elf_program_header_table.ml

(*Generated by Lem from elf_program_header_table.lem.*)
(** [elf_program_header_table] contains type, functions and other definitions
  * for working with program header tables and their entries and ELF segments.
  * Related files are [elf_interpreted_segments] which extracts information
  * derived from PHTs presented in this file and converts it into a more usable
  * format for processing.
  *
  * FIXME:
  * Bug in Lem as Lem codebase uses [int] type throughout where [BigInt.t]
  * is really needed, hence chokes on huge constants below, which is why they are
  * written in the way that they are.
  *)

open Lem_assert_extra
open Lem_basic_classes
open Lem_bool
open Lem_function
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string
(*import Set*)

open Elf_types_native_uint
open Endianness

open Byte_sequence
open Error
open Missing_pervasives
open Show

(** Segment types *)

(** Unused array element.  All other members of the structure are undefined. *)
let elf_pt_null : Nat_big_num.num= ( (Nat_big_num.of_int 0))
(** A loadable segment. *)
let elf_pt_load : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** Dynamic linking information. *)
let elf_pt_dynamic : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** Specifies the location and size of a null-terminated path name to be used to
  * invoke an interpreter.
  *)
let elf_pt_interp : Nat_big_num.num= ( (Nat_big_num.of_int 3))
(** Specifies location and size of auxiliary information. *)
let elf_pt_note : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** Reserved but with unspecified semantics.  If the file contains a segment of
  * this type then it is to be regarded as non-conformant with the ABI.
  *)
let elf_pt_shlib : Nat_big_num.num= ( (Nat_big_num.of_int 5))
(** Specifies the location and size of the program header table. *)
let elf_pt_phdr : Nat_big_num.num= ( (Nat_big_num.of_int 6))
(** Specifies the thread local storage (TLS) template.  Need not be supported. *)
let elf_pt_tls : Nat_big_num.num= ( (Nat_big_num.of_int 7))
(** Start of reserved indices for operating system specific semantics. *)
let elf_pt_loos : Nat_big_num.num=  (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul (Nat_big_num.mul( (Nat_big_num.of_int 128))( (Nat_big_num.of_int 128)))( (Nat_big_num.of_int 128)))( (Nat_big_num.of_int 256)))( (Nat_big_num.of_int 3))) (* 1610612736 (* 0x60000000 *) *)
(** End of reserved indices for operating system specific semantics. *)
let elf_pt_hios : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 469762047))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 3))) (* 1879048191 (* 0x6fffffff *) *)
(** Start of reserved indices for processor specific semantics. *)
let elf_pt_loproc : Nat_big_num.num=  ( Nat_big_num.mul( (Nat_big_num.of_int 469762048))( (Nat_big_num.of_int 4))) (* 1879048192 (* 0x70000000 *) *)
(** End of reserved indices for processor specific semantics. *)
let elf_pt_hiproc : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 536870911))( (Nat_big_num.of_int 4)))( (Nat_big_num.of_int 3))) (* 2147483647 (* 0x7fffffff *) *)

(** [string_of_elf_segment_type os proc st] produces a string representation of
  * the coding of an ELF segment type [st] using [os] and [proc] to render OS-
  * and processor-specific codings.
  *)
(* XXX: is GNU stuff supposed to be hardcoded here? *)
(*val string_of_segment_type : (natural -> string) -> (natural -> string) -> natural -> string*)
let string_of_segment_type os proc pt:string=
	 (if Nat_big_num.equal pt elf_pt_null then
		"NULL"
	else if Nat_big_num.equal pt elf_pt_load then
		"LOAD"
	else if Nat_big_num.equal pt elf_pt_dynamic then
		"DYNAMIC"
	else if Nat_big_num.equal pt elf_pt_interp then
		"INTERP"
	else if Nat_big_num.equal pt elf_pt_note then
		"NOTE"
	else if Nat_big_num.equal pt elf_pt_shlib then
		"SHLIB"
	else if Nat_big_num.equal pt elf_pt_phdr then
		"PHDR"
	else if Nat_big_num.equal pt elf_pt_tls then
		"TLS"
	else if Nat_big_num.greater_equal pt elf_pt_loos && Nat_big_num.less_equal pt elf_pt_hios then
		os pt
	else if Nat_big_num.greater_equal pt elf_pt_loproc && Nat_big_num.less_equal pt elf_pt_hiproc then
		proc pt
	else
		"Undefined or invalid segment type")

(** Segments permission flags *)

(** Execute bit *)
let elf_pf_x        : Nat_big_num.num= ( (Nat_big_num.of_int 1))
(** Write bit *)
let elf_pf_w        : Nat_big_num.num= ( (Nat_big_num.of_int 2))
(** Read bit *)
let elf_pf_r        : Nat_big_num.num= ( (Nat_big_num.of_int 4))
(** The following two bit ranges are reserved for OS- and processor-specific
  * flags respectively.
  *)
let elf_pf_maskos   : Nat_big_num.num= ( (Nat_big_num.of_int 267386880))      (* 0x0ff00000 *)
let elf_pf_maskproc : Nat_big_num.num=  (Nat_big_num.mul( (Nat_big_num.of_int 4))( (Nat_big_num.of_int 1006632960))) (* 0xf0000000 *)

(** [exact_permission_of_permission m]: ELF has two interpretations of a RWX-style
  * permission bit [m], an exact permission and an allowable permission.  These
  * permissions allow us to interpret a flag as an upper bound for behaviour and
  * an ABI-compliant implementation can choose to interpret the flag [m] as either.
  *
  * In the exact interpretation, the upper bound is exactly the natural interpretation
  * of the flag.  This is encoded in [exact_permission_of_permission], which is
  * a glorified identity function, though included for completeness.
  *)
(*val exact_permissions_of_permission : natural -> error natural*)
let exact_permissions_of_permission m:(Nat_big_num.num)error=
   (if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then
    return( (Nat_big_num.of_int 0))
  else if Nat_big_num.equal m elf_pf_x then
    return( (Nat_big_num.of_int 1))
  else if Nat_big_num.equal m elf_pf_w then
    return( (Nat_big_num.of_int 2))
  else if Nat_big_num.equal m elf_pf_r then
    return( (Nat_big_num.of_int 4))
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then
    return( (Nat_big_num.of_int 3))
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then
    return( (Nat_big_num.of_int 5))
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then
    return( (Nat_big_num.of_int 6))
  else if Nat_big_num.equal m (Nat_big_num.add (Nat_big_num.add elf_pf_x elf_pf_r) elf_pf_w) then
    return( (Nat_big_num.of_int 7))
  else
    fail "exact_permission_of_permission: invalid permission flag")

(** [allowable_permission_of_permission m]: ELF has two interpretations of a RWX-style
  * permission bit [m], an exact permission and an allowable permission.  These
  * permissions allow us to interpret a flag as an upper bound for behaviour and
  * an ABI-compliant implementation can choose to interpret the flag [m] as either.
  *
  * In the allowable interpretation, the upper bound is more lax than the natural
  * interpretation of the flag.
  *)
(*val allowable_permissions_of_permission : natural -> error natural*)
let allowable_permissions_of_permission m:(Nat_big_num.num)error=
   (if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then
    return( (Nat_big_num.of_int 0))
  else if Nat_big_num.equal m elf_pf_x then
    return( (Nat_big_num.of_int 5))
  else if Nat_big_num.equal m elf_pf_w then
    return( (Nat_big_num.of_int 7))
  else if Nat_big_num.equal m elf_pf_r then
    return( (Nat_big_num.of_int 5))
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then
    return( (Nat_big_num.of_int 7))
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then
    return( (Nat_big_num.of_int 5))
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then
    return( (Nat_big_num.of_int 7))
  else if Nat_big_num.equal m (Nat_big_num.add (Nat_big_num.add elf_pf_x elf_pf_r) elf_pf_w) then
    return( (Nat_big_num.of_int 7))
  else
    fail "exact_permission_of_permission: invalid permission flag")

(** [elf64_interpreted_program_header_flags w] extracts a boolean triple of flags
  * from the flags field of an interpreted segment.
  *)
(*val parse_elf_segment_permissions : natural -> (bool * bool * bool)*)
let parse_elf_segment_permissions m:bool*bool*bool=
   (if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then
    (false, false, false)
  else if Nat_big_num.equal m elf_pf_x then
    (false, false, true)
  else if Nat_big_num.equal m elf_pf_w then
    (false, true, false)
  else if Nat_big_num.equal m elf_pf_r then
    (true, false, false)
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then
    (false, true, true)
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then
    (true, false, true)
  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then
    (true, true, false)
  else if Nat_big_num.equal m (Nat_big_num.add (Nat_big_num.add elf_pf_x elf_pf_r) elf_pf_w) then
    (true, true, true)
  else
    failwith "Invalid permisssion flag")

(** [string_of_elf_segment_permissions m] produces a string-based representation
  * of an ELF segment's permission field.
  * TODO: expand this as is needed by the validation tests.
  *)
(*val string_of_elf_segment_permissions : natural -> string*)
let string_of_elf_segment_permissions m:string=
   (let (r, w, x) = (parse_elf_segment_permissions m) in
  (if r then "R" else " ") ^ ((if w then "W" else " ") ^ (if x then "X" else " ")))

(** Program header table entry type *)

(** Type [elf32_program_header_table_entry] encodes a program header table entry
  * for 32-bit platforms.  Each entry describes a segment in an executable or
  * shared object file.
  *)
type elf32_program_header_table_entry =
  { elf32_p_type   : Uint32_wrapper.uint32 (** Type of the segment *)
   ; elf32_p_offset : Uint32_wrapper.uint32  (** Offset from beginning of file for segment *)
   ; elf32_p_vaddr  : Uint32_wrapper.uint32 (** Virtual address for segment in memory *)
   ; elf32_p_paddr  : Uint32_wrapper.uint32 (** Physical address for segment *)
   ; elf32_p_filesz : Uint32_wrapper.uint32 (** Size of segment in file, in bytes *)
   ; elf32_p_memsz  : Uint32_wrapper.uint32 (** Size of segment in memory image, in bytes *)
   ; elf32_p_flags  : Uint32_wrapper.uint32 (** Segment flags *)
   ; elf32_p_align  : Uint32_wrapper.uint32 (** Segment alignment memory for memory and file *)
   }

(** [compare_elf32_program_header_table_entry ent1 ent2] is an ordering-comparison
  * function on program header table entries suitable for constructing sets,
  * finite maps, and other ordered data types with.
  *)
(*val compare_elf32_program_header_table_entry : elf32_program_header_table_entry ->
  elf32_program_header_table_entry -> ordering*)
let compare_elf32_program_header_table_entry h1 h2:int=
     (lexicographic_compare Nat_big_num.compare [Uint32_wrapper.to_bigint h1.elf32_p_type;
    Uint32_wrapper.to_bigint h1.elf32_p_offset;
    Uint32_wrapper.to_bigint h1.elf32_p_vaddr;
    Uint32_wrapper.to_bigint h1.elf32_p_paddr;
    Uint32_wrapper.to_bigint h1.elf32_p_filesz;
    Uint32_wrapper.to_bigint h1.elf32_p_memsz;
    Uint32_wrapper.to_bigint h1.elf32_p_flags;
    Uint32_wrapper.to_bigint h1.elf32_p_align]
    [Uint32_wrapper.to_bigint h2.elf32_p_type;
    Uint32_wrapper.to_bigint h2.elf32_p_offset;
    Uint32_wrapper.to_bigint h2.elf32_p_vaddr;
    Uint32_wrapper.to_bigint h2.elf32_p_paddr;
    Uint32_wrapper.to_bigint h2.elf32_p_filesz;
    Uint32_wrapper.to_bigint h2.elf32_p_memsz;
    Uint32_wrapper.to_bigint h2.elf32_p_flags;
    Uint32_wrapper.to_bigint h2.elf32_p_align])

let instance_Basic_classes_Ord_Elf_program_header_table_elf32_program_header_table_entry_dict:(elf32_program_header_table_entry)ord_class= ({

  compare_method = compare_elf32_program_header_table_entry;

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

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_program_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0])));

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

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf32_program_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))})

(** Type [elf64_program_header_table_entry] encodes a program header table entry
  * for 64-bit platforms.  Each entry describes a segment in an executable or
  * shared object file.
  *)
type elf64_program_header_table_entry =
  { elf64_p_type   : Uint32_wrapper.uint32  (** Type of the segment *)
   ; elf64_p_flags  : Uint32_wrapper.uint32  (** Segment flags *)
   ; elf64_p_offset : Uint64_wrapper.uint64   (** Offset from beginning of file for segment *)
   ; elf64_p_vaddr  : Uint64_wrapper.uint64  (** Virtual address for segment in memory *)
   ; elf64_p_paddr  : Uint64_wrapper.uint64  (** Physical address for segment *)
   ; elf64_p_filesz : Uint64_wrapper.uint64 (** Size of segment in file, in bytes *)
   ; elf64_p_memsz  : Uint64_wrapper.uint64 (** Size of segment in memory image, in bytes *)
   ; elf64_p_align  : Uint64_wrapper.uint64 (** Segment alignment memory for memory and file *)
   }

(** [compare_elf64_program_header_table_entry ent1 ent2] is an ordering-comparison
  * function on program header table entries suitable for constructing sets,
  * finite maps, and other ordered data types with.
  *)
(*val compare_elf64_program_header_table_entry : elf64_program_header_table_entry ->
  elf64_program_header_table_entry -> ordering*)
let compare_elf64_program_header_table_entry h1 h2:int=
     (lexicographic_compare Nat_big_num.compare [Uint32_wrapper.to_bigint h1.elf64_p_type;
    Uint64_wrapper.to_bigint h1.elf64_p_offset;
    Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_vaddr;
    Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_paddr;
    Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_filesz;
    Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_memsz;
    Uint32_wrapper.to_bigint h1.elf64_p_flags;
    Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_align]
    [Uint32_wrapper.to_bigint h2.elf64_p_type;
    Uint64_wrapper.to_bigint h2.elf64_p_offset;
    Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_vaddr;
    Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_paddr;
    Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_filesz;
    Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_memsz;
    Uint32_wrapper.to_bigint h2.elf64_p_flags;
    Ml_bindings.nat_big_num_of_uint64 h2.elf64_p_align])

let instance_Basic_classes_Ord_Elf_program_header_table_elf64_program_header_table_entry_dict:(elf64_program_header_table_entry)ord_class= ({

  compare_method = compare_elf64_program_header_table_entry;

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

  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_program_header_table_entry f1 f2)(Pset.from_list compare [(-1); 0])));

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

  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_program_header_table_entry f1 f2)(Pset.from_list compare [1; 0])))})


(** [string_of_elf32_program_header_table_entry os proc et] produces a string
  * representation of a 32-bit program header table entry using [os] and [proc]
  * to render OS- and processor-specific entries.
  *)
(*val string_of_elf32_program_header_table_entry : (natural -> string) -> (natural -> string) -> elf32_program_header_table_entry -> string*)
let string_of_elf32_program_header_table_entry os proc entry:string=
	 (unlines [
		("\t" ^ ("Segment type: " ^ string_of_segment_type os proc (Uint32_wrapper.to_bigint entry.elf32_p_type)))
	; ("\t" ^ ("Offset: " ^ Uint32_wrapper.to_string entry.elf32_p_offset))
	; ("\t" ^ ("Virtual address: " ^ Uint32_wrapper.to_string entry.elf32_p_vaddr))
	; ("\t" ^ ("Physical address: " ^ Uint32_wrapper.to_string entry.elf32_p_paddr))
	; ("\t" ^ ("Segment size (bytes): " ^ Uint32_wrapper.to_string entry.elf32_p_filesz))
	; ("\t" ^ ("Segment size in memory image (bytes): " ^ Uint32_wrapper.to_string entry.elf32_p_memsz))
	; ("\t" ^ ("Flags: " ^ Uint32_wrapper.to_string entry.elf32_p_flags))
  ; ("\t" ^ ("Alignment: " ^ Uint32_wrapper.to_string entry.elf32_p_align))
	])

(** [string_of_elf64_program_header_table_entry os proc et] produces a string
  * representation of a 64-bit program header table entry using [os] and [proc]
  * to render OS- and processor-specific entries.
  *)
(*val string_of_elf64_program_header_table_entry : (natural -> string) -> (natural -> string) -> elf64_program_header_table_entry -> string*)
let string_of_elf64_program_header_table_entry os proc entry:string=
   (unlines [
    ("\t" ^ ("Segment type: " ^ string_of_segment_type os proc (Uint32_wrapper.to_bigint entry.elf64_p_type)))
  ; ("\t" ^ ("Offset: " ^ Uint64_wrapper.to_string entry.elf64_p_offset))
  ; ("\t" ^ ("Virtual address: " ^ Uint64_wrapper.to_string entry.elf64_p_vaddr))
  ; ("\t" ^ ("Physical address: " ^ Uint64_wrapper.to_string entry.elf64_p_paddr))
  ; ("\t" ^ ("Segment size (bytes): " ^ Uint64_wrapper.to_string entry.elf64_p_filesz))
  ; ("\t" ^ ("Segment size in memory image (bytes): " ^ Uint64_wrapper.to_string entry.elf64_p_memsz))
  ; ("\t" ^ ("Flags: " ^ Uint32_wrapper.to_string entry.elf64_p_flags))
  ; ("\t" ^ ("Alignment: " ^ Uint64_wrapper.to_string entry.elf64_p_align))
  ])

(** [string_of_elf32_program_header_table_entry_default et] produces a string representation
  * of table entry [et] where OS- and processor-specific entries are replaced with
  * default strings.
  *)
(*val string_of_elf32_program_header_table_entry_default : elf32_program_header_table_entry -> string*)
let string_of_elf32_program_header_table_entry_default:elf32_program_header_table_entry ->string=
	 (string_of_elf32_program_header_table_entry
    ((fun y->"*Default OS specific print*"))
      ((fun y->"*Default processor specific print*")))

(** [string_of_elf64_program_header_table_entry_default et] produces a string representation
  * of table entry [et] where OS- and processor-specific entries are replaced with
  * default strings.
  *)
(*val string_of_elf64_program_header_table_entry_default : elf64_program_header_table_entry -> string*)
let string_of_elf64_program_header_table_entry_default:elf64_program_header_table_entry ->string=
   (string_of_elf64_program_header_table_entry
    ((fun y->"*Default OS specific print*"))
      ((fun y->"*Default processor specific print*")))

let instance_Show_Show_Elf_program_header_table_elf32_program_header_table_entry_dict:(elf32_program_header_table_entry)show_class= ({

  show_method = string_of_elf32_program_header_table_entry_default})

let instance_Show_Show_Elf_program_header_table_elf64_program_header_table_entry_dict:(elf64_program_header_table_entry)show_class= ({

  show_method = string_of_elf64_program_header_table_entry_default})

(** Parsing and blitting *)

(** [bytes_of_elf32_program_header_table_entry ed ent] blits a 32-bit program
  * header table entry [ent] into a byte sequence assuming endianness [ed].
  *)
(*val bytes_of_elf32_program_header_table_entry : endianness -> elf32_program_header_table_entry -> byte_sequence*)
let bytes_of_elf32_program_header_table_entry endian entry:Byte_sequence_wrapper.byte_sequence=
   (Byte_sequence.from_byte_lists [
    bytes_of_elf32_word endian entry.elf32_p_type
  ; bytes_of_elf32_off  endian entry.elf32_p_offset
  ; bytes_of_elf32_addr endian entry.elf32_p_vaddr
  ; bytes_of_elf32_addr endian entry.elf32_p_paddr
  ; bytes_of_elf32_word endian entry.elf32_p_filesz
  ; bytes_of_elf32_word endian entry.elf32_p_memsz
  ; bytes_of_elf32_word endian entry.elf32_p_flags
  ; bytes_of_elf32_word endian entry.elf32_p_align
  ])

(** [bytes_of_elf64_program_header_table_entry ed ent] blits a 64-bit program
  * header table entry [ent] into a byte sequence assuming endianness [ed].
  *)
(*val bytes_of_elf64_program_header_table_entry : endianness -> elf64_program_header_table_entry -> byte_sequence*)
let bytes_of_elf64_program_header_table_entry endian entry:Byte_sequence_wrapper.byte_sequence=
   (Byte_sequence.from_byte_lists [
    bytes_of_elf64_word  endian entry.elf64_p_type
  ; bytes_of_elf64_word  endian entry.elf64_p_flags
  ; bytes_of_elf64_off   endian entry.elf64_p_offset
  ; bytes_of_elf64_addr  endian entry.elf64_p_vaddr
  ; bytes_of_elf64_addr  endian entry.elf64_p_paddr
  ; bytes_of_elf64_xword endian entry.elf64_p_filesz
  ; bytes_of_elf64_xword endian entry.elf64_p_memsz
  ; bytes_of_elf64_xword endian entry.elf64_p_align
  ])

(** [read_elf32_program_header_table_entry endian bs0] reads an ELF32 program header table
  * entry from byte sequence [bs0] assuming endianness [endian].  If [bs0] is larger
  * than necessary, the excess is returned from the function, too.
  * Fails if the entry cannot be read.
  *)
(*val read_elf32_program_header_table_entry : endianness -> byte_sequence ->
  error (elf32_program_header_table_entry * byte_sequence)*)
let read_elf32_program_header_table_entry endian bs:(elf32_program_header_table_entry*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf32_word endian bs) (fun (typ, bs) -> bind (read_elf32_off  endian bs) (fun (offset, bs) -> bind (read_elf32_addr endian bs) (fun (vaddr, bs) -> bind (read_elf32_addr endian bs) (fun (paddr, bs) -> bind (read_elf32_word endian bs) (fun (filesz, bs) -> bind (read_elf32_word endian bs) (fun (memsz, bs) -> bind (read_elf32_word endian bs) (fun (flags, bs) -> bind (read_elf32_word endian bs) (fun (align, bs) ->
		return ({ elf32_p_type = typ; elf32_p_offset = offset;
                elf32_p_vaddr = vaddr; elf32_p_paddr = paddr;
                elf32_p_filesz = filesz; elf32_p_memsz = memsz;
                elf32_p_flags = flags; elf32_p_align = align }, bs))))))))))

(** [read_elf64_program_header_table_entry endian bs0] reads an ELF64 program header table
  * entry from byte sequence [bs0] assuming endianness [endian].  If [bs0] is larger
  * than necessary, the excess is returned from the function, too.
  * Fails if the entry cannot be read.
  *)
(*val read_elf64_program_header_table_entry : endianness -> byte_sequence ->
  error (elf64_program_header_table_entry * byte_sequence)*)
let read_elf64_program_header_table_entry endian bs:(elf64_program_header_table_entry*Byte_sequence_wrapper.byte_sequence)error=  (bind (read_elf64_word endian bs) (fun (typ, bs) -> bind (read_elf64_word endian bs) (fun (flags, bs) -> bind (read_elf64_off  endian bs) (fun (offset, bs) -> bind (read_elf64_addr endian bs) (fun (vaddr, bs) -> bind (read_elf64_addr endian bs) (fun (paddr, bs) -> bind (read_elf64_xword endian bs) (fun (filesz, bs) -> bind (read_elf64_xword endian bs) (fun (memsz, bs) -> bind (read_elf64_xword endian bs) (fun (align, bs) ->
    return ({ elf64_p_type = typ; elf64_p_offset = offset;
                elf64_p_vaddr = vaddr; elf64_p_paddr = paddr;
                elf64_p_filesz = filesz; elf64_p_memsz = memsz;
                elf64_p_flags = flags; elf64_p_align = align }, bs))))))))))

(** Program header table type *)

(** Type [elf32_program_header_table] represents a program header table for 32-bit
  * ELF files.  A program header table is an array (implemented as a list, here)
  * of program header table entries.
  *)
type elf32_program_header_table = elf32_program_header_table_entry
  list

(** Type [elf64_program_header_table] represents a program header table for 64-bit
  * ELF files.  A program header table is an array (implemented as a list, here)
  * of program header table entries.
  *)
type elf64_program_header_table = elf64_program_header_table_entry
  list

(** [bytes_of_elf32_program_header_table ed tbl] blits an ELF32 program header
  * table into a byte sequence assuming endianness [ed].
  *)
let bytes_of_elf32_program_header_table endian tbl:Byte_sequence_wrapper.byte_sequence=
   (Byte_sequence.concat (Lem_list.map (bytes_of_elf32_program_header_table_entry endian) tbl))

(** [bytes_of_elf64_program_header_table ed tbl] blits an ELF64 program header
  * table into a byte sequence assuming endianness [ed].
  *)
let bytes_of_elf64_program_header_table endian tbl:Byte_sequence_wrapper.byte_sequence=
   (Byte_sequence.concat (Lem_list.map (bytes_of_elf64_program_header_table_entry endian) tbl))

(** [read_elf32_program_header_table' endian bs0] reads an ELF32 program header table from
  * byte_sequence [bs0] assuming endianness [endian].  The byte_sequence [bs0] is assumed
  * to have exactly the correct size for the table.  For internal use, only.  Use
  * [read_elf32_program_header_table] below instead.
  *)
let rec read_elf32_program_header_table' endian bs0:((elf32_program_header_table_entry)list)error=
	 (if Nat_big_num.equal (Byte_sequence.length0 bs0)( (Nat_big_num.of_int 0)) then
  	return []
  else bind (read_elf32_program_header_table_entry endian bs0) (fun (entry, bs1) -> bind (read_elf32_program_header_table' endian bs1) (fun tail ->
    return (entry::tail))))

(** [read_elf64_program_header_table' endian bs0] reads an ELF64 program header table from
  * byte_sequence [bs0] assuming endianness [endian].  The byte_sequence [bs0] is assumed
  * to have exactly the correct size for the table.  For internal use, only.  Use
  * [read_elf32_program_header_table] below instead.
  *)
let rec read_elf64_program_header_table' endian bs0:((elf64_program_header_table_entry)list)error=
   (if Nat_big_num.equal (Byte_sequence.length0 bs0)( (Nat_big_num.of_int 0)) then
    return []
  else bind (read_elf64_program_header_table_entry endian bs0) (fun (entry, bs1) -> bind (read_elf64_program_header_table' endian bs1) (fun tail ->
    return (entry::tail))))

(** [read_elf32_program_header_table table_size endian bs0] reads an ELF32 program header
  * table from byte_sequence [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
  * This [table_size] argument should be equal to the number of entries in the
  * table multiplied by the fixed entry size.  Bitstring [bs0] may be larger than
  * necessary, in which case the excess is returned.
  *)
(*val read_elf32_program_header_table : natural -> endianness -> byte_sequence ->
  error (elf32_program_header_table * byte_sequence)*)
let read_elf32_program_header_table table_size endian bs0:((elf32_program_header_table_entry)list*Byte_sequence_wrapper.byte_sequence)error=  (bind (partition0 table_size bs0) (fun (eat, rest) -> bind (read_elf32_program_header_table' endian eat) (fun table ->
	return (table, rest))))

(** [read_elf64_program_header_table table_size endian bs0] reads an ELF64 program header
  * table from byte_sequence [bs0] assuming endianness [endian] based on the size (in bytes) passed in via [table_size].
  * This [table_size] argument should be equal to the number of entries in the
  * table multiplied by the fixed entry size.  Bitstring [bs0] may be larger than
  * necessary, in which case the excess is returned.
  *)
(*val read_elf64_program_header_table : natural -> endianness -> byte_sequence ->
  error (elf64_program_header_table * byte_sequence)*)
let read_elf64_program_header_table table_size endian bs0:((elf64_program_header_table_entry)list*Byte_sequence_wrapper.byte_sequence)error=  (bind (partition0 table_size bs0) (fun (eat, rest) -> bind (read_elf64_program_header_table' endian eat) (fun table ->
  return (table, rest))))

(** The [pht_print_bundle] type is used to tidy up other type signatures.  Some of the
  * top-level string_of_ functions require six or more functions passed to them,
  * which quickly gets out of hand.  This type is used to reduce that complexity.
  * The first component of the type is an OS specific print function, the second is
  * a processor specific print function.
  *)
type pht_print_bundle = (Nat_big_num.num -> string) * (Nat_big_num.num -> string)

(** [string_of_elf32_program_header_table os proc tbl] produces a string representation
  * of program header table [tbl] using [os] and [proc] to render OS- and processor-
  * specific entries.
  *)
(*val string_of_elf32_program_header_table : pht_print_bundle -> elf32_program_header_table -> string*)
let string_of_elf32_program_header_table (os, proc) tbl:string=
   (unlines (Lem_list.map (string_of_elf32_program_header_table_entry os proc) tbl))

(** [string_of_elf64_program_header_table os proc tbl] produces a string representation
  * of program header table [tbl] using [os] and [proc] to render OS- and processor-
  * specific entries.
  *)
(*val string_of_elf64_program_header_table : pht_print_bundle -> elf64_program_header_table -> string*)
let string_of_elf64_program_header_table (os, proc) tbl:string=
   (unlines (Lem_list.map (string_of_elf64_program_header_table_entry os proc) tbl))

(** Static/dynamic linkage *)

(** [get_elf32_dynamic_linked pht] tests whether an ELF32 file is a dynamically
  * linked object by traversing the program header table and attempting to find
  * a header describing a segment with the name of an associated interpreter.
  * Returns [true] if any such header is found, [false] --- indicating static
  * linkage --- otherwise.
  *)
(*val get_elf32_dynamic_linked : elf32_program_header_table -> bool*)
let get_elf32_dynamic_linked pht:bool=
   (List.exists (fun p -> Nat_big_num.equal (Uint32_wrapper.to_bigint p.elf32_p_type) elf_pt_interp) pht)

(** [get_elf64_dynamic_linked pht] tests whether an ELF64 file is a dynamically
  * linked object by traversing the program header table and attempting to find
  * a header describing a segment with the name of an associated interpreter.
  * Returns [true] if any such header is found, [false] --- indicating static
  * linkage --- otherwise.
  *)
(*val get_elf64_dynamic_linked : elf64_program_header_table -> bool*)
let get_elf64_dynamic_linked pht:bool=
   (List.exists (fun p -> Nat_big_num.equal (Uint32_wrapper.to_bigint p.elf64_p_type) elf_pt_interp) pht)

(** [get_elf32_static_linked] is a utility function defined as the inverse
  * of [get_elf32_dynamic_linked].
  *)
(*val get_elf32_static_linked : elf32_program_header_table -> bool*)
let get_elf32_static_linked pht:bool=
   (not (get_elf32_dynamic_linked pht))

(** [get_elf64_static_linked] is a utility function defined as the inverse
  * of [get_elf64_dynamic_linked].
  *)
(*val get_elf64_static_linked : elf64_program_header_table -> bool*)
let get_elf64_static_linked pht:bool=
   (not (get_elf64_dynamic_linked pht))

(** [get_elf32_requested_interpreter ent bs0] extracts the requested interpreter
  * of a dynamically linkable ELF file from that file's program header table
  * entry of type PT_INTERP, [ent].  Interpreter string is extracted from byte
  * sequence [bs0].
  * Fails if [ent] is not of type PT_INTERP, or if transcription otherwise fails.
  *)
(*val get_elf32_requested_interpreter : elf32_program_header_table_entry ->
  byte_sequence -> error string*)
let get_elf32_requested_interpreter pent bs0:(string)error=
   (if Nat_big_num.equal (Uint32_wrapper.to_bigint pent.elf32_p_type) elf_pt_interp then
    let off = (Uint32_wrapper.to_bigint  pent.elf32_p_offset) in
    let siz = (Uint32_wrapper.to_bigint pent.elf32_p_filesz) in bind (Byte_sequence.offset_and_cut off ( Nat_big_num.sub_nat siz( (Nat_big_num.of_int 1))) bs0) (fun cut ->
      return (Byte_sequence.string_of_byte_sequence cut))
  else
    fail "get_elf32_requested_interpreter: not an INTERP segment header")

(** [get_elf64_requested_interpreter ent bs0] extracts the requested interpreter
  * of a dynamically linkable ELF file from that file's program header table
  * entry of type PT_INTERP, [ent].  Interpreter string is extracted from byte
  * sequence [bs0].
  * Fails if [ent] is not of type PT_INTERP, or if transcription otherwise fails.
  *)
(*val get_elf64_requested_interpreter : elf64_program_header_table_entry ->
  byte_sequence -> error string*)
let get_elf64_requested_interpreter pent bs0:(string)error=
   (if Nat_big_num.equal (Uint32_wrapper.to_bigint pent.elf64_p_type) elf_pt_interp then
    let off = (Uint64_wrapper.to_bigint   pent.elf64_p_offset) in
    let siz = (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_filesz) in bind (Byte_sequence.offset_and_cut off ( Nat_big_num.sub_nat siz( (Nat_big_num.of_int 1))) bs0) (fun cut ->
      return (Byte_sequence.string_of_byte_sequence cut))
  else
    fail "get_elf64_requested_interpreter: not an INTERP segment header")