From 8f47273f118808373649a3a084e4a3c99167edd3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 28 Nov 2017 12:51:24 +0100 Subject: 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. --- checker/analyze.ml | 29 +++++++++++++++++++++++++++++ checker/analyze.mli | 3 +++ checker/check.ml | 21 +++++++++++++++------ checker/check.mllib | 1 + 4 files changed, 48 insertions(+), 6 deletions(-) (limited to 'checker') 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 -- cgit v1.2.3