Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 605 deletions

diff --git a/lib/ocaml_rts/linksem/elf_program_header_table.ml b/lib/ocaml_rts/linksem/elf_program_header_table.ml
deleted file mode 100644
index 6afe4d53..00000000
--- a/lib/ocaml_rts/linksem/elf_program_header_table.ml
+++ /dev/null
@@ -1,605 +0,0 @@
-(*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_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")
-    
-(** [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=  
- (if Nat_big_num.equal m(Nat_big_num.of_int 0) then
-    "  "
-  else if Nat_big_num.equal m elf_pf_x then
-    "  E"
-  else if Nat_big_num.equal m elf_pf_w then
-    " W "
-  else if Nat_big_num.equal m elf_pf_r then
-    "R  "
-  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_w) then
-    " WE"
-  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_x elf_pf_r) then
-    "R E"
-  else if Nat_big_num.equal m (Nat_big_num.add elf_pf_w elf_pf_r) then
-    "RW "
-  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
-    "RWE"
-  else
-    "Invalid permisssion flag")
-
-(** 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.uint32 (** Type of the segment *)
-   ; elf32_p_offset : Uint32.uint32  (** Offset from beginning of file for segment *)
-   ; elf32_p_vaddr  : Uint32.uint32 (** Virtual address for segment in memory *)
-   ; elf32_p_paddr  : Uint32.uint32 (** Physical address for segment *)
-   ; elf32_p_filesz : Uint32.uint32 (** Size of segment in file, in bytes *)
-   ; elf32_p_memsz  : Uint32.uint32 (** Size of segment in memory image, in bytes *)
-   ; elf32_p_flags  : Uint32.uint32 (** Segment flags *)
-   ; elf32_p_align  : Uint32.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 [Nat_big_num.of_string (Uint32.to_string h1.elf32_p_type);
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_offset);
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_vaddr);
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_paddr);
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_filesz);
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_memsz); 
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_flags);
-    Nat_big_num.of_string (Uint32.to_string h1.elf32_p_align)]
-    [Nat_big_num.of_string (Uint32.to_string h2.elf32_p_type);
-    Nat_big_num.of_string (Uint32.to_string h2.elf32_p_offset);
-    Nat_big_num.of_string (Uint32.to_string h2.elf32_p_vaddr);
-    Nat_big_num.of_string (Uint32.to_string h2.elf32_p_paddr);
-    Nat_big_num.of_string (Uint32.to_string h2.elf32_p_filesz);
-    Nat_big_num.of_string (Uint32.to_string h2.elf32_p_memsz); 
-    Nat_big_num.of_string (Uint32.to_string h2.elf32_p_flags);
-    Nat_big_num.of_string (Uint32.to_string 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.uint32  (** Type of the segment *)
-   ; elf64_p_flags  : Uint32.uint32  (** Segment flags *)
-   ; elf64_p_offset : Uint64.uint64   (** Offset from beginning of file for segment *)
-   ; elf64_p_vaddr  : Uint64.uint64  (** Virtual address for segment in memory *)
-   ; elf64_p_paddr  : Uint64.uint64  (** Physical address for segment *)
-   ; elf64_p_filesz : Uint64.uint64 (** Size of segment in file, in bytes *)
-   ; elf64_p_memsz  : Uint64.uint64 (** Size of segment in memory image, in bytes *)
-   ; elf64_p_align  : Uint64.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 [Nat_big_num.of_string (Uint32.to_string h1.elf64_p_type);
-    Nat_big_num.of_string (Uint64.to_string 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; 
-    Nat_big_num.of_string (Uint32.to_string h1.elf64_p_flags);
-    Ml_bindings.nat_big_num_of_uint64 h1.elf64_p_align]
-    [Nat_big_num.of_string (Uint32.to_string h2.elf64_p_type);
-    Nat_big_num.of_string (Uint64.to_string 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; 
-    Nat_big_num.of_string (Uint32.to_string 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 (Nat_big_num.of_string (Uint32.to_string entry.elf32_p_type))))
-	; ("\t" ^ ("Offset: " ^ Uint32.to_string entry.elf32_p_offset))
-	; ("\t" ^ ("Virtual address: " ^ Uint32.to_string entry.elf32_p_vaddr))
-	; ("\t" ^ ("Physical address: " ^ Uint32.to_string entry.elf32_p_paddr))
-	; ("\t" ^ ("Segment size (bytes): " ^ Uint32.to_string entry.elf32_p_filesz))
-	; ("\t" ^ ("Segment size in memory image (bytes): " ^ Uint32.to_string entry.elf32_p_memsz))
-	; ("\t" ^ ("Flags: " ^ Uint32.to_string entry.elf32_p_flags))
-  ; ("\t" ^ ("Alignment: " ^ Uint32.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 (Nat_big_num.of_string (Uint32.to_string entry.elf64_p_type))))
-  ; ("\t" ^ ("Offset: " ^ Uint64.to_string entry.elf64_p_offset))
-  ; ("\t" ^ ("Virtual address: " ^ Uint64.to_string entry.elf64_p_vaddr))
-  ; ("\t" ^ ("Physical address: " ^ Uint64.to_string entry.elf64_p_paddr))
-  ; ("\t" ^ ("Segment size (bytes): " ^ Uint64.to_string entry.elf64_p_filesz))
-  ; ("\t" ^ ("Segment size in memory image (bytes): " ^ Uint64.to_string entry.elf64_p_memsz))
-  ; ("\t" ^ ("Flags: " ^ Uint32.to_string entry.elf64_p_flags))
-  ; ("\t" ^ ("Alignment: " ^ Uint64.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=  
- (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=  
- (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)error=	
- (read_elf32_word endian bs >>= (fun (typ, bs) ->
-	read_elf32_off  endian bs >>= (fun (offset, bs) ->
-	read_elf32_addr endian bs >>= (fun (vaddr, bs) ->
-	read_elf32_addr endian bs >>= (fun (paddr, bs) ->
-	read_elf32_word endian bs >>= (fun (filesz, bs) ->
-	read_elf32_word endian bs >>= (fun (memsz, bs) ->
-	read_elf32_word endian bs >>= (fun (flags, bs) ->
-	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)error=  
- (read_elf64_word endian bs >>= (fun (typ, bs) ->
-  read_elf64_word endian bs >>= (fun (flags, bs) ->
-  read_elf64_off  endian bs >>= (fun (offset, bs) ->
-  read_elf64_addr endian bs >>= (fun (vaddr, bs) ->
-  read_elf64_addr endian bs >>= (fun (paddr, bs) ->
-  read_elf64_xword endian bs >>= (fun (filesz, bs) ->
-  read_elf64_xword endian bs >>= (fun (memsz, bs) ->
-  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=  
- (Byte_sequence.concat0 (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=  
- (Byte_sequence.concat0 (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
-  	read_elf32_program_header_table_entry endian bs0 >>= (fun (entry, bs1) ->
-    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
-    read_elf64_program_header_table_entry endian bs0 >>= (fun (entry, bs1) ->
-    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)error=	
- (partition0 table_size bs0 >>= (fun (eat, rest) ->
-	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)error=  
- (partition0 table_size bs0 >>= (fun (eat, rest) ->
-  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 (Nat_big_num.of_string (Uint32.to_string 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 (Nat_big_num.of_string (Uint32.to_string 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 (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_type)) elf_pt_interp then
-    let off = (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_offset)) in
-    let siz = (Nat_big_num.of_string (Uint32.to_string pent.elf32_p_filesz)) in
-      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 (Nat_big_num.of_string (Uint32.to_string pent.elf64_p_type)) elf_pt_interp then
-    let off = (Nat_big_num.of_string (Uint64.to_string pent.elf64_p_offset)) in
-    let siz = (Ml_bindings.nat_big_num_of_uint64 pent.elf64_p_filesz) in
-      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")