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

1 files changed, 150 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/archive.ml b/lib/ocaml_rts/linksem/archive.ml
new file mode 100644
index 00000000..cd4480b4
--- /dev/null
+++ b/lib/ocaml_rts/linksem/archive.ml
@@ -0,0 +1,150 @@
+(*Generated by Lem from archive.lem.*)
+open Lem_basic_classes
+open Lem_bool
+open Lem_list
+open Lem_num
+open Lem_maybe
+open Lem_string
+open Show
+open Lem_assert_extra
+
+open Missing_pervasives
+open Byte_sequence
+open Error
+
+type archive_entry_header =
+  { name      : string
+   ; timestamp : Nat_big_num.num
+   ; uid       : int
+   ; gid       : int
+   ; mode      : int
+   ; size      : int (* 1GB should be enough *)
+   }
+
+type archive_global_header = char
+  list
+
+(*val string_of_byte_sequence : byte_sequence -> string*)
+let string_of_byte_sequence0 seq:string=  
+ ((match seq with
+    | Sequence bs -> Xstring.implode (Lem_list.map (fun x-> x) bs)
+  ))
+
+(*val read_archive_entry_header : natural -> byte_sequence -> error (archive_entry_header * natural * byte_sequence)*)
+let read_archive_entry_header seq_length seq:(archive_entry_header*Nat_big_num.num*byte_sequence)error=  
+ (let magic_bytes = ([Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 96)) (* 0x60 *); Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 10)) (* 0x0a *)]) in
+        let header_length =(Nat_big_num.of_int 60) in
+        (* let _ = Missing_pervasives.errs ("Archive entry header? " ^ (show (take 16 bs)) ^ "? ") in *)
+        partition_with_length header_length seq_length seq >>= (fun (header, rest) -> 
+        offset_and_cut(Nat_big_num.of_int 58)(Nat_big_num.of_int 2) header >>= (fun magic -> 
+        offset_and_cut(Nat_big_num.of_int 0)(Nat_big_num.of_int 16) header >>= (fun name1 -> 
+        offset_and_cut(Nat_big_num.of_int 16)(Nat_big_num.of_int 12) header >>= (fun timestamp_str -> 
+        offset_and_cut(Nat_big_num.of_int 28)(Nat_big_num.of_int 6)  header >>= (fun uid_str -> 
+        offset_and_cut(Nat_big_num.of_int 34)(Nat_big_num.of_int 6)  header >>= (fun gid_str -> 
+        offset_and_cut(Nat_big_num.of_int 40)(Nat_big_num.of_int 8)  header >>= (fun mode_str -> 
+        offset_and_cut(Nat_big_num.of_int 48)(Nat_big_num.of_int 10) header >>= (fun size_str -> 
+        let size2 = (natural_of_decimal_string (string_of_byte_sequence0 size_str)) in 
+                (* let _ = Missing_pervasives.errln (": yes, size " ^ (show size)) in *)
+        return ({ name = (string_of_byte_sequence0 name1); timestamp = ((Nat_big_num.of_int 0 : Nat_big_num.num)) (* FIXME *);
+          uid =( 0) (* FIXME *) ; gid =( 0) (* FIXME *) ; mode =( 0) (* FIXME *);
+            size = (Nat_big_num.to_int size2) (* FIXME *) }, Nat_big_num.sub_nat seq_length header_length, rest))))))))))
+
+(*val read_archive_global_header : byte_sequence -> error (archive_global_header * byte_sequence)*)
+let read_archive_global_header seq:((char)list*byte_sequence)error=  
+ ((match seq with
+    | Sequence bs ->
+            (* let _ = Missing_pervasives.errs ("Archive? " ^ (show (take 16 bs)) ^ "? ")
+            in*)
+      let chars = (Lem_list.map (fun x-> x) (take0(Nat_big_num.of_int 8) bs)) in 
+        if Xstring.implode chars = "!<arch>\n" then
+          (* let _ = Missing_pervasives.errln ": yes" in *)
+          return (chars, Sequence(drop0(Nat_big_num.of_int 8) bs))
+        else
+          (* let _ = Missing_pervasives.errln ": no" in *)
+          fail "read_archive_global_header: not an archive"
+    ))
+
+(*val accum_archive_contents : (list (string * byte_sequence)) -> maybe string -> natural -> byte_sequence -> error (list (string * byte_sequence))*)
+let rec accum_archive_contents accum extended_filenames whole_seq_length whole_seq:((string*byte_sequence)list)error=  
+(  
+  (* let _ = Missing_pervasives.errs "Can read a header? " in *)if not (Nat_big_num.equal (Byte_sequence.length0 whole_seq) whole_seq_length) then    
+(assert false) (* invariant: whole_seq_length always equal to length of whole_seq, so the length is only
+      computed one.  This "fail" needed for Isabelle termination proofs... *)
+  else
+  (match (read_archive_entry_header whole_seq_length whole_seq) with
+    | Fail _ -> return accum
+    | Success (hdr, (seq_length : Nat_big_num.num), seq) ->
+    (match seq with
+      | Sequence next_bs ->
+        (* let _ = Missing_pervasives.errln ("yes; next_bs has length " ^ (show (List.length next_bs))) in *)
+        let amount_to_drop =          
+(if (hdr.size mod  2) = 0 then
+            (Nat_big_num.of_int hdr.size)
+          else Nat_big_num.add
+            (Nat_big_num.of_int hdr.size)(Nat_big_num.of_int 1))
+        in
+        if Nat_big_num.equal amount_to_drop(Nat_big_num.of_int 0) then
+          fail "accum_archive_contents: amount to drop from byte sequence is 0"
+        else
+        (*let _ = Missing_pervasives.errln ("amount_to_drop is " ^ (show amount_to_drop)) in*)
+        let chunk = (Sequence(Lem_list.take hdr.size next_bs))
+        in
+        (*let _ = Missing_pervasives.errs ("Processing archive header named " ^ hdr.name)
+        in*)
+        let (new_accum, (new_extended_filenames :  string option)) =          
+(let name1 = (Xstring.explode hdr.name) in
+            if (listEqualBy (=) name1 ['/'; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' ']) then
+              (* SystemV symbol lookup table; we skip this *) (accum, extended_filenames)
+            else
+              (match name1 with
+                | x::xs ->
+                  if x = '/' then
+                    (match xs with
+                      | y::ys ->
+                        if y = '/' then
+                          (accum, Some (string_of_byte_sequence0 chunk))
+                        else
+                          let index = (natural_of_decimal_string (Xstring.implode xs)) in
+                            (match extended_filenames with 
+                              | None -> failwith "corrupt archive: reference to non-existent extended filenames"
+                              | Some s -> 
+                                let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in
+                                let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in 
+                                let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in
+                                  (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*)
+                                  (((ext_name, chunk) :: accum), extended_filenames)
+                           )
+                      | [] ->
+                        let index = (natural_of_decimal_string (Xstring.implode xs)) in
+                          (match extended_filenames with 
+                            | None -> failwith "corrupt archive: reference to non-existent extended filenames"
+                            | Some s -> 
+                              let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in
+                              let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in 
+                              let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in
+                                (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*)
+                                (((ext_name, chunk) :: accum), extended_filenames)
+                         )
+                    )
+                  else
+                    (((hdr.name, chunk) :: accum), extended_filenames)
+                | [] -> (((hdr.name, chunk) :: accum), extended_filenames)
+              ))
+        in
+          (match (Byte_sequence.dropbytes amount_to_drop seq) with
+            | Fail _ -> return accum
+            | Success new_seq ->
+              accum_archive_contents new_accum new_extended_filenames ( Nat_big_num.sub_nat seq_length amount_to_drop) new_seq
+          )
+    )
+  ))
+
+(*val read_archive : byte_sequence -> error (list (string * byte_sequence))*)
+let read_archive bs:((string*byte_sequence)list)error=    
+  (read_archive_global_header bs >>= (fun (hdr, seq) -> 
+    let result = (accum_archive_contents [] None (Byte_sequence.length0 seq) seq)  in 
+    (* let _ = Missing_pervasives.errln "Finished reading archive" in *)
+    (match result with
+        Success r -> Success (List.rev r)
+        | Fail x -> Fail x
+    )))