diff --git a/infer/src/backend/SymOp.ml b/infer/src/backend/SymOp.ml
index 243a22b02..f01d4c8d0 100644
--- a/infer/src/backend/SymOp.ml
+++ b/infer/src/backend/SymOp.ml
@@ -28,6 +28,26 @@ let exn_not_failure = function
   | Analysis_failure_exe _ -> false
   | _ -> true
 
+let try_finally ?(fail_early=false) f g =
+  match f () with
+  | r ->
+      g () ;
+      r
+  | exception (Analysis_failure_exe _ as f_exn) ->
+      if not fail_early then
+        (try g () with _ -> ());
+      raise f_exn
+  | exception f_exn ->
+      match g () with
+      | () ->
+          raise f_exn
+      | exception (Analysis_failure_exe _ as g_exn) ->
+          raise g_exn
+      | exception _ ->
+          raise f_exn
+
+let finally_try g f = try_finally f g
+
 let pp_failure_kind fmt = function
   | FKtimeout -> F.fprintf fmt "TIMEOUT"
   | FKsymops_timeout symops -> F.fprintf fmt "SYMOPS TIMEOUT (%d)" symops
diff --git a/infer/src/backend/SymOp.mli b/infer/src/backend/SymOp.mli
index 5d70fa187..dc07dd793 100644
--- a/infer/src/backend/SymOp.mli
+++ b/infer/src/backend/SymOp.mli
@@ -68,4 +68,14 @@ exception Analysis_failure_exe of failure_kind
 (** check that the exception is not a timeout exception *)
 val exn_not_failure : exn -> bool
 
+(** [try_finally ~fail_early f g] executes [f] and then [g] even if [f] raises an exception.
+    Assuming that [g ()] terminates quickly [Analysis_failure_exe] exceptions are handled correctly.
+    In particular, an exception raised by [f ()] is delayed until [g ()] finishes, so [g ()] should
+    return reasonably quickly.  [~fail_early=true] can be passed to skip executing [g ()] when [f
+    ()] raises a [Analysis_failure_exe] exception. *)
+val try_finally : ?fail_early:bool -> (unit -> 'a) -> (unit -> unit) -> 'a
+
+(** [finally_try g f] is equivalent to [try_finally f g]. *)
+val finally_try : (unit -> unit) -> (unit -> 'a) -> 'a
+
 val pp_failure_kind : Format.formatter -> failure_kind -> unit
diff --git a/infer/src/backend/serialization.ml b/infer/src/backend/serialization.ml
index 738ecc28f..fa3c892d4 100644
--- a/infer/src/backend/serialization.ml
+++ b/infer/src/backend/serialization.ml
@@ -59,24 +59,28 @@ let create_serializer (key : key) : 'a serializer =
     try
       match_data (Marshal.from_string str 0) "string"
     with Sys_error _ -> None in
-  let from_file (_fname : DB.filename) : 'a option =
-    let read () =
-      try
-        let fname = DB.filename_to_string _fname in
-        let inc = open_in_bin fname in
-        let value_option = match_data (Marshal.from_channel inc) fname in
-        close_in inc;
-        value_option
-      with
-      | Sys_error _ -> None in
-    let timeout = 1.0 in
-    let catch_exn = function
-      | End_of_file -> true
-      | Failure _ -> true (* handle input_value: truncated object *)
-      | _ -> false in
-    (* Retry to read for 1 second in case of end of file, *)
-    (* which indicates that another process is writing the same file. *)
-    retry_exception timeout catch_exn read () in
+  let from_file (fname_ : DB.filename) : 'a option =
+    let fname = DB.filename_to_string fname_ in
+    match open_in_bin fname with
+    | exception Sys_error _ ->
+        None
+    | inc ->
+        let read () =
+          try
+            seek_in inc 0 ;
+            match_data (Marshal.from_channel inc) fname
+          with
+          | Sys_error _ -> None in
+        let timeout = 1.0 in
+        let catch_exn = function
+          | End_of_file -> true
+          | Failure _ -> true (* handle input_value: truncated object *)
+          | _ -> false in
+        (* Retry to read for 1 second in case of end of file, *)
+        (* which indicates that another process is writing the same file. *)
+        SymOp.try_finally
+          (fun () -> retry_exception timeout catch_exn read ())
+          (fun () -> close_in inc) in
   let to_file (fname : DB.filename) (value : 'a) =
     let fname_str = DB.filename_to_string fname in
     (* support nonblocking reads and writes in parallel: *)