Use SymOp.try_finally to avoid swallowing timeouts

Reviewed By: jberdine

Differential Revision: D5932891

fbshipit-source-id: 7c95be8

infer/src/backend/dom.ml

@@ -1564,7 +1564,7 @@ let sigma_partial_join tenv mode (sigma1: Prop.sigma) (sigma2: Prop.sigma)
   CheckJoin.init mode sigma1 sigma2 ;
   let lost_little = CheckJoin.lost_little in
   let s1, s2, s3 = sigma_partial_join' tenv mode [] sigma1 sigma2 in
-  Utils.try_finally
+  SymOp.try_finally
     ~f:(fun () ->
       if Rename.check lost_little then (s1, s2, s3)
       else ( L.d_strln "failed Rename.check" ; raise Sil.JoinFail ))
@@ -1807,7 +1807,7 @@ let prop_partial_meet tenv p1 p2 =
   FreshVarExp.init () ;
   Todo.init () ;
   try
-    Utils.try_finally ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2)) ~finally:(fun () ->
+    SymOp.try_finally ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2)) ~finally:(fun () ->
         Rename.final () ; FreshVarExp.final () ; Todo.final () )
   with Sil.JoinFail -> None
 
@@ -1911,7 +1911,7 @@ let prop_partial_join pname tenv mode p1 p2 =
       FreshVarExp.init () ;
       Todo.init () ;
       try
-        Utils.try_finally
+        SymOp.try_finally
           ~f:(fun () ->
             let p1', p2' = footprint_partial_join' tenv p1 p2 in
             let rename_footprint = Rename.reset () in
@@ -1928,7 +1928,7 @@ let eprop_partial_join tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed P
   Rename.init () ;
   FreshVarExp.init () ;
   Todo.init () ;
-  Utils.try_finally ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2) ~finally:(fun () ->
+  SymOp.try_finally ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2) ~finally:(fun () ->
       Rename.final () ; FreshVarExp.final () ; Todo.final () )
 
 (** {2 Join and Meet for Propset} *)

infer/src/backend/timeout.ml

@@ -100,7 +100,7 @@ let exe_timeout f x =
     SymOp.set_alarm ()
   in
   try
-    Utils.try_finally
+    SymOp.try_finally
       ~f:(fun () -> suspend_existing_timeout_and_start_new_one () ; f x ; None)
       ~finally:resume_previous_timeout
   with SymOp.Analysis_failure_exe kind ->

infer/src/base/Config.ml

@@ -2417,7 +2417,7 @@ let specs_library =
 let set_reference_and_call_function reference value f x =
   let saved = !reference in
   let restore () = reference := saved in
-  Utils.try_finally
+  Utils.try_finally_swallow_timeout
     ~f:(fun () ->
       reference := value ;
       f x)

infer/src/base/Serialization.ml

@@ -94,8 +94,8 @@ let create_serializer (key: Key.t) : 'a serializer =
         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:1.0 ~catch_exn ~f:read ()) (fun () ->
+        SymOp.try_finally ~f:(fun () -> retry_exception ~timeout:1.0 ~catch_exn ~f:read ())
-            In_channel.close inc )
+          ~finally:(fun () -> In_channel.close inc )
   in
   let write_to_tmp_file fname data =
     let fname_tmp =

infer/src/base/SymOp.ml

@@ -23,22 +23,21 @@ exception Analysis_failure_exe of failure_kind(** failure that prevented analysi
 
 let exn_not_failure = function Analysis_failure_exe _ -> false | _ -> true
 
-let try_finally ?(fail_early= false) f g =
+let try_finally ~f ~finally =
   match f () with
   | r
-   -> g () ; r
+   -> finally () ; r
   | exception (Analysis_failure_exe _ as f_exn)
    -> reraise_after f_exn ~f:(fun () ->
-          if not fail_early then
+          try finally ()
-            try g ()
+          with _ -> (* swallow in favor of the original exception *) () )
-            with _ -> (* swallow in favor of the original exception *) () )
   | exception f_exn
    -> reraise_after f_exn ~f:(fun () ->
-          try g ()
+          try finally ()
           with
-          | g_exn
+          | finally_exn
-          when (* do not swallow Analysis_failure_exe thrown from g *)
+          when (* do not swallow Analysis_failure_exe thrown from finally *)
-               match g_exn with Analysis_failure_exe _ -> false | _ -> true
+               match finally_exn with Analysis_failure_exe _ -> false | _ -> true
           -> () )
 
 let pp_failure_kind fmt = function

infer/src/base/SymOp.mli

@@ -66,11 +66,10 @@ exception Analysis_failure_exe of failure_kind(** Timeout exception *)
 val exn_not_failure : exn -> bool
 (** check that the exception is not a timeout exception *)
 
-val try_finally : ?fail_early:bool -> (unit -> 'a) -> (unit -> unit) -> 'a
+val try_finally : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a
-(** [try_finally ~fail_early f g] executes [f] and then [g] even if [f] raises an exception.
+(** [try_finally ~f ~finally] executes [f] and then [finally] even if [f] raises an exception.
-    Assuming that [g ()] terminates quickly [Analysis_failure_exe] exceptions are handled correctly.
+    Assuming that [finally ()] terminates quickly [Analysis_failure_exe] exceptions are handled correctly.
-    In particular, an exception raised by [f ()] is delayed until [g ()] finishes, so [g ()] should
+    In particular, an exception raised by [f ()] is delayed until [finally ()] finishes, so [finally ()] should
-    return reasonably quickly.  [~fail_early=true] can be passed to skip executing [g ()] when [f
+    return reasonably quickly. *)
-    ()] raises a [Analysis_failure_exe] exception. *)
 
 val pp_failure_kind : Format.formatter -> failure_kind -> unit

infer/src/base/Utils.ml

@@ -165,7 +165,7 @@ let read_json_file path =
   try Ok (Yojson.Basic.from_file path)
   with Sys_error msg | Yojson.Json_error msg -> Error msg
 
-let do_finally ~f ~finally =
+let do_finally_swallow_timeout ~f ~finally =
   let res =
     try f ()
     with exc ->
@@ -176,21 +176,21 @@ let do_finally ~f ~finally =
   let res' = finally () in
   (res, res')
 
-let try_finally ~f ~finally =
+let try_finally_swallow_timeout ~f ~finally =
-  let res, () = do_finally ~f ~finally in
+  let res, () = do_finally_swallow_timeout ~f ~finally in
   res
 
 let with_file_in file ~f =
   let ic = In_channel.create file in
   let f () = f ic in
   let finally () = In_channel.close ic in
-  try_finally ~f ~finally
+  try_finally_swallow_timeout ~f ~finally
 
 let with_file_out file ~f =
   let oc = Out_channel.create file in
   let f () = f oc in
   let finally () = Out_channel.close oc in
-  try_finally ~f ~finally
+  try_finally_swallow_timeout ~f ~finally
 
 let write_json_to_file destfile json =
   with_file_out destfile ~f:(fun oc -> Yojson.Basic.pretty_to_channel oc json)
@@ -203,7 +203,7 @@ let with_process_in command read =
   let chan = Unix.open_process_in command in
   let f () = read chan in
   let finally () = consume_in chan ; Unix.close_process_in chan in
-  do_finally ~f ~finally
+  do_finally_swallow_timeout ~f ~finally
 
 let shell_escape_command cmd =
   let escape arg =

infer/src/base/Utils.mli

@@ -95,5 +95,6 @@ val write_file_with_locking : ?delete:bool -> f:(Out_channel.t -> unit) -> strin
 val rmtree : string -> unit
 (** [rmtree path] removes [path] and, if [path] is a directory, recursively removes its contents *)
 
-val try_finally : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a
+val try_finally_swallow_timeout : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a
-(** Calls [f] then [finally] even if [f] raised an exception. The original exception is reraised afterwards. *)
+(** Calls [f] then [finally] even if [f] raised an exception. The original exception is reraised afterwards.
+    Where possible use [SymOp.try_finally] to avoid swallowing timeouts. *)