Use safe demarshalling in the checker.

Instead of relying on the OCaml demarshaller, which is not resilient against
ill-formed data, we reuse the safe demarshaller from votour. This ensures that
garbage files do not trigger memory violations.

4 files changed, 48 insertions, 6 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
index 2f3ee0356..7047d8a14 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -392,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 1b6c94759..9c837643f 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -45,3 +45,6 @@ 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 180ca1ece..dfc271995 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -298,18 +298,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