Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 167 deletions

diff --git a/lib/ocaml_rts/linksem/elf_interpreted_segment.ml b/lib/ocaml_rts/linksem/elf_interpreted_segment.ml
deleted file mode 100644
index 1971f350..00000000
--- a/lib/ocaml_rts/linksem/elf_interpreted_segment.ml
+++ /dev/null
@@ -1,167 +0,0 @@
-(*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)
-  ])