Merge PR #6266: Safe unmarshalling in the checker

5 files changed, 127 insertions, 24 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
index df75d5b93..7047d8a14 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -55,6 +55,55 @@ let magic_number = "\132\149\166\190"
 
 (** Memory reification *)
 
+module LargeArray :
+sig
+  type 'a t
+  val empty : 'a t
+  val length : 'a t -> int
+  val make : int -> 'a -> 'a t
+  val get : 'a t -> int -> 'a
+  val set : 'a t -> int -> 'a -> unit
+end =
+struct
+
+  let max_length = Sys.max_array_length
+
+  type 'a t = 'a array array * 'a array
+  (** Invariants:
+      - All subarrays of the left array have length [max_length].
+      - The right array has length < [max_length].
+  *)
+
+  let empty = [||], [||]
+
+  let length (vl, vr) =
+    (max_length * Array.length vl) + Array.length vr
+
+  let make n x =
+    let k = n / max_length in
+    let r = n mod max_length in
+    let vl = Array.init k (fun _ -> Array.make max_length x) in
+    let vr = Array.make r x in
+    (vl, vr)
+
+  let get (vl, vr) n =
+    let k = n / max_length in
+    let r = n mod max_length in
+    let len = Array.length vl in
+    if k < len then vl.(k).(r)
+    else if k == len then vr.(r)
+    else invalid_arg "index out of bounds"
+
+  let set (vl, vr) n x =
+    let k = n / max_length in
+    let r = n mod max_length in
+    let len = Array.length vl in
+    if k < len then vl.(k).(r) <- x
+    else if k == len then vr.(r) <- x
+    else invalid_arg "index out of bounds"
+
+end
+
 type repr =
 | RInt of int
 | RBlock of (int * int) (* tag × len *)
@@ -82,7 +131,7 @@ end
 module type S =
 sig
   type input
-  val parse : input -> (data * obj array)
+  val parse : input -> (data * obj LargeArray.t)
 end
 
 module Make(M : Input) =
@@ -261,7 +310,7 @@ let parse_object chan =
 let parse chan =
   let (magic, len, _, _, size) = parse_header chan in
   let () = assert (magic = magic_number) in
-  let memory = Array.make size (Struct ((-1), [||])) in
+  let memory = LargeArray.make size (Struct ((-1), [||])) in
   let current_object = ref 0 in
   let fill_obj = function
   | RPointer n ->
@@ -272,7 +321,7 @@ let parse chan =
     data, None
   | RString s ->
     let data = Ptr !current_object in
-    let () = memory.(!current_object) <- String s in
+    let () = LargeArray.set memory !current_object (String s) in
     let () = incr current_object in
     data, None
   | RBlock (tag, 0) ->
@@ -282,7 +331,7 @@ let parse chan =
   | RBlock (tag, len) ->
     let data = Ptr !current_object in
     let nblock = Array.make len (Atm (-1)) in
-    let () = memory.(!current_object) <- Struct (tag, nblock) in
+    let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in
     let () = incr current_object in
     data, Some nblock
   | RCode addr ->
@@ -343,3 +392,32 @@ module PString = Make(IString)
 
 let parse_channel = PChannel.parse
 let parse_string s = PString.parse (s, ref 0)
+
+let instantiate (p, mem) =
+  let len = LargeArray.length mem in
+  let ans = LargeArray.make len (Obj.repr 0) in
+  (** First pass: initialize the subobjects *)
+  for i = 0 to len - 1 do
+    let obj = match LargeArray.get mem i with
+    | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
+    | String str -> Obj.repr str
+    in
+    LargeArray.set ans i obj
+  done;
+  let get_data = function
+  | Int n -> Obj.repr n
+  | Ptr p -> LargeArray.get ans p
+  | Atm tag -> Obj.new_block tag 0
+  | Fun _ -> assert false (** We shouldn't serialize closures *)
+  in
+  (** Second pass: set the pointers *)
+  for i = 0 to len - 1 do
+    match LargeArray.get mem i with
+    | Struct (_, blk) ->
+      let obj = LargeArray.get ans i in
+      for k = 0 to Array.length blk - 1 do
+        Obj.set_field obj k (get_data blk.(k))
+      done
+    | String _ -> ()
+  done;
+  get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 42efcf01d..9c837643f 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -8,8 +8,20 @@ type obj =
 | Struct of int * data array (* tag × data *)
 | String of string
 
-val parse_channel : in_channel -> (data * obj array)
-val parse_string : string -> (data * obj array)
+module LargeArray :
+sig
+  type 'a t
+  val empty : 'a t
+  val length : 'a t -> int
+  val make : int -> 'a -> 'a t
+  val get : 'a t -> int -> 'a
+  val set : 'a t -> int -> 'a -> unit
+end
+(** A data structure similar to arrays but allowing to overcome the 2^22 length
+    limitation on 32-bit architecture. *)
+
+val parse_channel : in_channel -> (data * obj LargeArray.t)
+val parse_string : string -> (data * obj LargeArray.t)
 
 (** {6 Functorized version} *)
 
@@ -26,10 +38,13 @@ end
 module type S =
 sig
   type input
-  val parse : input -> (data * obj array)
+  val parse : input -> (data * obj LargeArray.t)
   (** Return the entry point and the reification of the memory out of a
       marshalled structure. *)
 end
 
 module Make (M : Input) : S with type input = M.t
 (** Functorized version of the previous code. *)
+
+val instantiate : data * obj LargeArray.t -> Obj.t
+(** Create the OCaml object out of the reified representation. *)
diff --git a/checker/check.ml b/checker/check.ml
index 21fdba1fa..44105aa72 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -308,18 +308,27 @@ let name_clash_message dir mdir f =
 (* Dependency graph *)
 let depgraph = ref LibraryMap.empty
 
+let marshal_in_segment f ch =
+  try
+    let stop = input_binary_int ch in
+    let v = Analyze.instantiate (Analyze.parse_channel ch) in
+    let digest = Digest.input ch in
+    Obj.obj v, stop, digest
+  with _ ->
+    user_err (str "Corrupted file " ++ quote (str f))
+
 let intern_from_file (dir, f) =
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
       let ch = System.with_magic_number_check raw_intern_library f in
-      let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
-      let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
-      let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
-      let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
-      let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
+      let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in
+      let (md:Cic.library_disk), _, digest = marshal_in_segment f ch in
+      let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in
+      let (discharging:'a option), _, _ = marshal_in_segment f ch in
+      let (tasks:'a option), _, _ = marshal_in_segment f ch in
       let (table:Cic.opaque_table), pos, checksum =
-        System.marshal_in_segment f ch in
+        marshal_in_segment f ch in
       (* Verification of the final checksum *)
       let () = close_in ch in
       let ch = open_in_bin f in
diff --git a/checker/check.mllib b/checker/check.mllib
index 488507a13..f79ba66e3 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,6 @@
 Coq_config
 
+Analyze
 Hook
 Terminal
 Canary
diff --git a/checker/votour.ml b/checker/votour.ml
index b7c898232..77c9999c4 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -77,8 +77,8 @@ struct
 
   type obj = data
 
-  let memory = ref [||]
-  let sizes = ref [||]
+  let memory = ref LargeArray.empty
+  let sizes = ref LargeArray.empty
   (** size, in words *)
 
   let ws = Sys.word_size / 8
@@ -86,10 +86,10 @@ struct
   let rec init_size seen k = function
   | Int _ | Atm _ | Fun _ -> k 0
   | Ptr p ->
-    if seen.(p) then k 0
+    if LargeArray.get seen p then k 0
     else
-      let () = seen.(p) <- true in
-      match (!memory).(p) with
+      let () = LargeArray.set seen p true in
+      match LargeArray.get !memory p with
       | Struct (tag, os) ->
         let len = Array.length os in
         let rec fold i accu k =
@@ -97,30 +97,30 @@ struct
           else
             init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
         in
-        fold 0 1 (fun size -> let () = (!sizes).(p) <- size in k size)
+        fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
       | String s ->
         let size = 2 + (String.length s / ws) in
-        let () = (!sizes).(p) <- size in
+        let () = LargeArray.set !sizes p size in
         k size
 
   let size = function
   | Int _ | Atm _ | Fun _ -> 0
-  | Ptr p -> (!sizes).(p)
+  | Ptr p -> LargeArray.get !sizes p
 
   let repr = function
   | Int i -> INT i
   | Atm t -> BLOCK (t, [||])
   | Fun _ -> OTHER
   | Ptr p ->
-    match (!memory).(p) with
+    match LargeArray.get !memory p with
     | Struct (tag, os) -> BLOCK (tag, os)
     | String s -> STRING s
 
   let input ch =
     let obj, mem = parse_channel ch in
     let () = memory := mem in
-    let () = sizes := Array.make (Array.length mem) (-1) in
-    let seen = Array.make (Array.length mem) false in
+    let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in
+    let seen = LargeArray.make (LargeArray.length mem) false in
     let () = init_size seen ignore obj in
     obj