Add ocaml run-time and updates to sail for ocaml backend

1 files changed, 305 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/elf_interpreted_section.ml b/lib/ocaml_rts/linksem/elf_interpreted_section.ml
new file mode 100644
index 00000000..7fcf59b4
--- /dev/null
+++ b/lib/ocaml_rts/linksem/elf_interpreted_section.ml
@@ -0,0 +1,305 @@
+(*Generated by Lem from elf_interpreted_section.lem.*)
+(** Module [elf_interpreted_section] provides a record of "interpreted" sections,
+  * i.e. the data stored in the section header table converted to more amenable
+  * infinite precision types, and operation on those records.
+  *)
+
+open Lem_basic_classes
+open Lem_bool
+open Lem_list
+open Lem_maybe
+open Lem_num
+open Lem_string
+
+open Byte_sequence
+open Error
+open String_table
+
+open Elf_types_native_uint
+open Elf_section_header_table
+
+open Missing_pervasives
+open Show
+
+(** [elf32_interpreted_section] exactly mirrors the structure of a section header
+  * table entry, barring the conversion of all fields to more amenable types.
+  *)
+type elf32_interpreted_section =
+  { elf32_section_name    : Nat_big_num.num       (** Name of the section *)
+   ; elf32_section_type    : Nat_big_num.num       (** Type of the section *)
+   ; elf32_section_flags   : Nat_big_num.num       (** Flags associated with the section *)
+   ; elf32_section_addr    : Nat_big_num.num       (** Base address of the section in memory *)
+   ; elf32_section_offset  : Nat_big_num.num       (** Offset from beginning of file *)
+   ; elf32_section_size    : Nat_big_num.num       (** Section size in bytes *)
+   ; elf32_section_link    : Nat_big_num.num       (** Section header table index link *)
+   ; elf32_section_info    : Nat_big_num.num       (** Extra information, depends on section type *)
+   ; elf32_section_align   : Nat_big_num.num       (** Alignment constraints for section *)
+   ; elf32_section_entsize : Nat_big_num.num       (** Size of each entry in table, if section is one *)
+   ; elf32_section_body    : byte_sequence (** Body of section *)
+   ; elf32_section_name_as_string : string (** Name of the section, as a string; "" for no name (name = 0) *)
+   }
+   
+(** [elf32_interpreted_section_equal s1 s2] is an equality test on interpreted
+  * sections [s1] and [s2].
+  *)
+(*val elf32_interpreted_section_equal : elf32_interpreted_section -> elf32_interpreted_section -> bool*)
+let elf32_interpreted_section_equal x y:bool=  (Nat_big_num.equal
+    x.elf32_section_name y.elf32_section_name && (Nat_big_num.equal
+    x.elf32_section_type y.elf32_section_type && (Nat_big_num.equal
+    x.elf32_section_flags y.elf32_section_flags && (Nat_big_num.equal
+    x.elf32_section_addr y.elf32_section_addr && (Nat_big_num.equal
+    x.elf32_section_offset y.elf32_section_offset && (Nat_big_num.equal
+    x.elf32_section_size y.elf32_section_size && (Nat_big_num.equal
+    x.elf32_section_link y.elf32_section_link && (Nat_big_num.equal
+    x.elf32_section_info y.elf32_section_info && (Nat_big_num.equal
+    x.elf32_section_align y.elf32_section_align && (Nat_big_num.equal
+    x.elf32_section_entsize y.elf32_section_entsize && (equal
+    x.elf32_section_body y.elf32_section_body &&    
+(x.elf32_section_name_as_string = y.elf32_section_name_as_string))))))))))))
+
+let instance_Basic_classes_Eq_Elf_interpreted_section_elf32_interpreted_section_dict:(elf32_interpreted_section)eq_class= ({
+
+  isEqual_method = elf32_interpreted_section_equal;
+
+  isInequal_method = (fun x y->not (elf32_interpreted_section_equal x y))})
+
+(** [elf64_interpreted_section] exactly mirrors the structure of a section header
+  * table entry, barring the conversion of all fields to more amenable types.
+  *)
+type elf64_interpreted_section =
+  { elf64_section_name    : Nat_big_num.num       (** Name of the section *)
+   ; elf64_section_type    : Nat_big_num.num       (** Type of the section *)
+   ; elf64_section_flags   : Nat_big_num.num       (** Flags associated with the section *)
+   ; elf64_section_addr    : Nat_big_num.num       (** Base address of the section in memory *)
+   ; elf64_section_offset  : Nat_big_num.num       (** Offset from beginning of file *)
+   ; elf64_section_size    : Nat_big_num.num       (** Section size in bytes *)
+   ; elf64_section_link    : Nat_big_num.num       (** Section header table index link *)
+   ; elf64_section_info    : Nat_big_num.num       (** Extra information, depends on section type *)
+   ; elf64_section_align   : Nat_big_num.num       (** Alignment constraints for section *)
+   ; elf64_section_entsize : Nat_big_num.num       (** Size of each entry in table, if section is one *)
+   ; elf64_section_body    : byte_sequence (** Body of section *)
+   ; elf64_section_name_as_string : string (** Name of the section, as a string; "" for no name (name = 0) *)
+   }
+
+(** [compare_elf64_interpreted_section s1 s2] is an ordering comparison function
+  * on interpreted sections suitable for use in sets, finite maps and other
+  * ordered structures.
+  *)
+(*val compare_elf64_interpreted_section : elf64_interpreted_section -> elf64_interpreted_section ->
+  ordering*)
+let compare_elf64_interpreted_section s1 s2:int=    
+ (pairCompare (lexicographic_compare Nat_big_num.compare) compare_byte_sequence 
+    ([s1.elf64_section_name    ;
+      s1.elf64_section_type    ;
+      s1.elf64_section_flags   ;
+      s1.elf64_section_addr    ;
+      s1.elf64_section_offset  ;
+      s1.elf64_section_size    ;
+      s1.elf64_section_link    ;
+      s1.elf64_section_info    ;
+      s1.elf64_section_align   ;
+      s1.elf64_section_entsize], s1.elf64_section_body)
+    ([s2.elf64_section_name    ;
+      s2.elf64_section_type    ;
+      s2.elf64_section_flags   ;
+      s2.elf64_section_addr    ;
+      s2.elf64_section_offset  ;
+      s2.elf64_section_size    ;
+      s2.elf64_section_link    ;
+      s2.elf64_section_info    ;
+      s2.elf64_section_align   ;
+      s2.elf64_section_entsize], s2.elf64_section_body))
+
+let instance_Basic_classes_Ord_Elf_interpreted_section_elf64_interpreted_section_dict:(elf64_interpreted_section)ord_class= ({
+
+  compare_method = compare_elf64_interpreted_section;
+
+  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_section f1 f2) (-1))));
+
+  isLessEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_interpreted_section f1 f2)(Pset.from_list compare [(-1); 0])));
+
+  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(compare_elf64_interpreted_section f1 f2) 1)));
+
+  isGreaterEqual_method = (fun f1 -> (fun f2 -> Pset.mem (compare_elf64_interpreted_section f1 f2)(Pset.from_list compare [1; 0])))})
+
+(** [elf64_interpreted_section_equal s1 s2] is an equality test on interpreted
+  * sections [s1] and [s2].
+  *)
+(*val elf64_interpreted_section_equal : elf64_interpreted_section -> elf64_interpreted_section -> bool*)
+let elf64_interpreted_section_equal x y:bool=  (Nat_big_num.equal
+    x.elf64_section_name y.elf64_section_name && (Nat_big_num.equal
+    x.elf64_section_type y.elf64_section_type && (Nat_big_num.equal
+    x.elf64_section_flags y.elf64_section_flags && (Nat_big_num.equal
+    x.elf64_section_addr y.elf64_section_addr && (Nat_big_num.equal
+    x.elf64_section_offset y.elf64_section_offset && (Nat_big_num.equal
+    x.elf64_section_size y.elf64_section_size && (Nat_big_num.equal
+    x.elf64_section_link y.elf64_section_link && (Nat_big_num.equal
+    x.elf64_section_info y.elf64_section_info && (Nat_big_num.equal
+    x.elf64_section_align y.elf64_section_align && (Nat_big_num.equal
+    x.elf64_section_entsize y.elf64_section_entsize && (equal
+    x.elf64_section_body y.elf64_section_body &&    
+(x.elf64_section_name_as_string = y.elf64_section_name_as_string))))))))))))
+
+(** [null_elf32_interpreted_section] --- the null interpreted section.
+  *)
+(*val null_elf32_interpreted_section : elf32_interpreted_section*)
+let null_elf32_interpreted_section:elf32_interpreted_section=  
+ ({ elf32_section_name =(Nat_big_num.of_int 0)
+   ; elf32_section_type =(Nat_big_num.of_int 0)
+   ; elf32_section_flags =(Nat_big_num.of_int 0)
+   ; elf32_section_addr =(Nat_big_num.of_int 0)
+   ; elf32_section_offset =(Nat_big_num.of_int 0)
+   ; elf32_section_size =(Nat_big_num.of_int 0)
+   ; elf32_section_link =(Nat_big_num.of_int 0)
+   ; elf32_section_info =(Nat_big_num.of_int 0)
+   ; elf32_section_align =(Nat_big_num.of_int 0)
+   ; elf32_section_entsize =(Nat_big_num.of_int 0) 
+   ; elf32_section_body = Byte_sequence.empty
+   ; elf32_section_name_as_string = ""
+   })
+
+(** [null_elf64_interpreted_section] --- the null interpreted section.
+  *)
+(*val null_elf64_interpreted_section : elf64_interpreted_section*)
+let null_elf64_interpreted_section:elf64_interpreted_section=  
+ ({ elf64_section_name =(Nat_big_num.of_int 0)
+   ; elf64_section_type =(Nat_big_num.of_int 0)
+   ; elf64_section_flags =(Nat_big_num.of_int 0)
+   ; elf64_section_addr =(Nat_big_num.of_int 0)
+   ; elf64_section_offset =(Nat_big_num.of_int 0)
+   ; elf64_section_size =(Nat_big_num.of_int 0)
+   ; elf64_section_link =(Nat_big_num.of_int 0)
+   ; elf64_section_info =(Nat_big_num.of_int 0)
+   ; elf64_section_align =(Nat_big_num.of_int 0)
+   ; elf64_section_entsize =(Nat_big_num.of_int 0) 
+   ; elf64_section_body = Byte_sequence.empty
+   ; elf64_section_name_as_string = ""
+   })
+
+let instance_Basic_classes_Eq_Elf_interpreted_section_elf64_interpreted_section_dict:(elf64_interpreted_section)eq_class= ({
+
+  isEqual_method = elf64_interpreted_section_equal;
+
+  isInequal_method = (fun x y->not (elf64_interpreted_section_equal x y))})
+
+(** [elf64_interpreted_section_matches_section_header sect ent] checks whether
+  * the interpreted section and the corresponding section header table entry
+  * match.
+  *)
+(*val elf64_interpreted_section_matches_section_header : 
+    elf64_interpreted_section
+        -> elf64_section_header_table_entry
+            -> bool*)
+let elf64_interpreted_section_matches_section_header i sh:bool=  (Nat_big_num.equal
+  i.elf64_section_name (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_name)) && (Nat_big_num.equal
+  i.elf64_section_type (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_type)) && (Nat_big_num.equal
+  i.elf64_section_flags (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_flags) && (Nat_big_num.equal
+  i.elf64_section_addr (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addr) && (Nat_big_num.equal
+  i.elf64_section_offset (Nat_big_num.of_string (Uint64.to_string sh.elf64_sh_offset)) && (Nat_big_num.equal
+  i.elf64_section_size (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_size) && (Nat_big_num.equal
+  i.elf64_section_link (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_link)) && (Nat_big_num.equal
+  i.elf64_section_info (Nat_big_num.of_string (Uint32.to_string sh.elf64_sh_info)) && (Nat_big_num.equal
+  i.elf64_section_align (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_addralign) (* WHY? *) && Nat_big_num.equal
+  i.elf64_section_entsize (Ml_bindings.nat_big_num_of_uint64 sh.elf64_sh_entsize))))))))))
+  (* Don't compare the name as a string, because it's implied by the shshtrtab index. *)
+  (* NOTE that we can have multiple sections *indistinguishable*
+   * except by their section header table index. Imagine 
+   * multiple zero-size bss sections at the same address with the same name.
+   * That's why in elf_memory_image we always label each ElfSection
+   * with its SHT index.
+   *)
+
+type elf32_interpreted_sections = elf32_interpreted_section list
+type elf64_interpreted_sections = elf64_interpreted_section list
+
+(** [string_of_elf32_interpreted_section sect] returns a string-based representation
+  * of interpreted section, [sect].
+  *)
+(*val string_of_elf32_interpreted_section : elf32_interpreted_section -> string*)
+let string_of_elf32_interpreted_section is:string=   
+ (unlines [     
+("Name: " ^ (is.elf32_section_name_as_string ^ ("(" ^ ((Nat_big_num.to_string is.elf32_section_name) ^ ")"))))
+   ; ("Type: " ^ Nat_big_num.to_string is.elf32_section_type) 
+   ; ("Flags: " ^ Nat_big_num.to_string is.elf32_section_type)
+   ; ("Base address: " ^ Nat_big_num.to_string is.elf32_section_addr)
+   ; ("Section offset: " ^ Nat_big_num.to_string is.elf32_section_offset)
+   ; ("Section size: " ^ Nat_big_num.to_string is.elf32_section_size)
+   ; ("Link: " ^ Nat_big_num.to_string is.elf32_section_link)
+   ; ("Info: " ^ Nat_big_num.to_string is.elf32_section_info)
+   ; ("Section alignment: " ^ Nat_big_num.to_string is.elf32_section_align)
+   ; ("Entry size: " ^ Nat_big_num.to_string is.elf32_section_entsize)
+   ])
+
+(** [string_of_elf64_interpreted_section sect] returns a string-based representation
+  * of interpreted section, [sect].
+  *)
+(*val string_of_elf64_interpreted_section : elf64_interpreted_section -> string*)
+let string_of_elf64_interpreted_section is:string=   
+ (unlines [     
+("Name: " ^ (is.elf64_section_name_as_string ^ ("(" ^ ((Nat_big_num.to_string is.elf64_section_name) ^ ")"))))
+   ; ("Type: " ^ Nat_big_num.to_string is.elf64_section_type) 
+   ; ("Flags: " ^ Nat_big_num.to_string is.elf64_section_type)
+   ; ("Base address: " ^ Nat_big_num.to_string is.elf64_section_addr)
+   ; ("Section offset: " ^ Nat_big_num.to_string is.elf64_section_offset)
+   ; ("Section size: " ^ Nat_big_num.to_string is.elf64_section_size)
+   ; ("Link: " ^ Nat_big_num.to_string is.elf64_section_link)
+   ; ("Info: " ^ Nat_big_num.to_string is.elf64_section_info)
+   ; ("Section alignment: " ^ Nat_big_num.to_string is.elf64_section_align)
+   ; ("Entry size: " ^ Nat_big_num.to_string is.elf64_section_entsize)
+   ])
+   
+(** [is_valid_elf32_section_header_table_entry sect stab] checks whether a
+  * interpreted section conforms with the prescribed flags and types declared
+  * in the "special sections" table of the ELF specification.
+  * TODO: some of these entries in the table are overridden by ABI supplements.
+  * Make sure it is these that are passed in rather than the default table
+  * declared in the spec?
+  *)
+(*val is_valid_elf32_section_header_table_entry : elf32_interpreted_section ->
+  string_table -> bool*)
+let is_valid_elf32_section_header_table_entry ent stbl:bool=  
+ ((match String_table.get_string_at ent.elf32_section_name stbl with
+    | Fail    f    -> false
+    | Success name1 ->
+      (match Pmap.lookup name1 elf_special_sections with
+        | None           -> false (* ??? *)
+        | Some (typ, flags) -> Nat_big_num.equal
+            typ ent.elf32_section_type && Nat_big_num.equal flags ent.elf32_section_flags
+      )
+  ))
+  
+(** [is_valid_elf64_section_header_table_entry sect stab] checks whether a
+  * interpreted section conforms with the prescribed flags and types declared
+  * in the "special sections" table of the ELF specification.
+  * TODO: some of these entries in the table are overridden by ABI supplements.
+  * Make sure it is these that are passed in rather than the default table
+  * declared in the spec?
+  *)  
+(*val is_valid_elf64_section_header_table_entry : elf64_interpreted_section ->
+  string_table -> bool*)
+let is_valid_elf64_section_header_table_entry ent stbl:bool=  
+ ((match String_table.get_string_at ent.elf64_section_name stbl with
+    | Fail    f    -> false
+    | Success name1 ->
+      (match Pmap.lookup name1 elf_special_sections with
+        | None           -> false (* ??? *)
+        | Some (typ, flags) -> Nat_big_num.equal
+            typ ent.elf64_section_type && Nat_big_num.equal flags ent.elf64_section_flags
+      )
+  ))
+  
+(** [is_valid_elf32_section_header_table sects] checks whether all entries in
+  * [sect] are valid.
+  *)
+(*val is_valid_elf32_section_header_table : list elf32_interpreted_section ->
+  string_table -> bool*)
+let is_valid_elf32_section_header_table0 ents stbl:bool=  
+ (List.for_all (fun x -> is_valid_elf32_section_header_table_entry x stbl) ents)
+  
+(** [is_valid_elf64_section_header_table sects] checks whether all entries in
+  * [sect] are valid.
+  *)
+(*val is_valid_elf64_section_header_table : list elf64_interpreted_section ->
+  string_table -> bool*)
+let is_valid_elf64_section_header_table0 ents stbl:bool=  
+ (List.for_all (fun x -> is_valid_elf64_section_header_table_entry x stbl) ents)