Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968)

Strings are at most 16M on 32 bit OCaml, and the system state
may be bigger.  In this case we write to tmp file and
Marshal.from_channel.  We can't directly use the channel interface
because of badly designed non blocking API (available only on fds and
not channels).

1 files changed, 34 insertions, 5 deletions

diff --git a/lib/cThread.ml b/lib/cThread.ml
index 84e5ae4fe..2d1f10bf3 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -43,6 +43,18 @@ let really_read_fd fd s off len =
     i := !i + r
   done
 
+let really_read_fd_2_oc fd oc len =
+  let i = ref 0 in
+  let size = 4096 in
+  let s = String.create size in
+  while !i < len do
+    let len = len - !i in
+    let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in
+    if r = 0 then raise End_of_file;
+    i := !i + r;
+    output oc s 0 r;
+  done
+
 let thread_friendly_really_read ic s ~off ~len =
   try
     let fd = Unix.descr_of_in_channel ic in
@@ -68,9 +80,26 @@ let thread_friendly_input_value ic =
     let header = String.create Marshal.header_size in
     really_read_fd fd header 0 Marshal.header_size;
     let body_size = Marshal.data_size header 0 in
-    let msg = String.create (body_size + Marshal.header_size) in
-    String.blit header 0 msg 0 Marshal.header_size;
-    really_read_fd fd msg Marshal.header_size body_size;
-    Marshal.from_string msg 0
-  with Unix.Unix_error _ -> raise End_of_file
+    let desired_size = body_size + Marshal.header_size in
+    if desired_size <= Sys.max_string_length then begin
+      let msg = String.create desired_size in
+      String.blit header 0 msg 0 Marshal.header_size;
+      really_read_fd fd msg Marshal.header_size body_size;
+      Marshal.from_string msg 0
+    end else begin
+      (* Workaround for 32 bit systems and data > 16M *)
+      let name, oc =
+        Filename.open_temp_file ~mode:[Open_binary] "coq" "marshal" in
+      try
+        output oc header 0 Marshal.header_size;
+        really_read_fd_2_oc fd oc body_size;
+        close_out oc;
+        let ic = open_in_bin name in
+        let data = Marshal.from_channel ic in
+        close_in ic;
+        Sys.remove name;
+        data
+      with e -> Sys.remove name; raise e
+    end
+  with Unix.Unix_error _ | Sys_error _ -> raise End_of_file