diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 288baaffc..df81cba9b 100644 --- a/infer/src/backend/dom.ml +++ b/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} *) diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index af7943171..27b8f43f3 100644 --- a/infer/src/backend/timeout.ml +++ b/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 -> diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index d51321b99..c19d0d7d4 100644 --- a/infer/src/base/Config.ml +++ b/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) diff --git a/infer/src/base/Serialization.ml b/infer/src/base/Serialization.ml index 4631cb0be..99ebd3905 100644 --- a/infer/src/base/Serialization.ml +++ b/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 () -> - In_channel.close inc ) + SymOp.try_finally ~f:(fun () -> retry_exception ~timeout:1.0 ~catch_exn ~f:read ()) + ~finally:(fun () -> In_channel.close inc ) in let write_to_tmp_file fname data = let fname_tmp = diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index d0bb4f762..1d6bf6c20 100644 --- a/infer/src/base/SymOp.ml +++ b/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 g () - with _ -> (* swallow in favor of the original exception *) () ) + try finally () + with _ -> (* swallow in favor of the original exception *) () ) | exception f_exn -> reraise_after f_exn ~f:(fun () -> - try g () + try finally () with - | g_exn - when (* do not swallow Analysis_failure_exe thrown from g *) - match g_exn with Analysis_failure_exe _ -> false | _ -> true + | finally_exn + when (* do not swallow Analysis_failure_exe thrown from finally *) + match finally_exn with Analysis_failure_exe _ -> false | _ -> true -> () ) let pp_failure_kind fmt = function diff --git a/infer/src/base/SymOp.mli b/infer/src/base/SymOp.mli index 857e92a8e..7991b4504 100644 --- a/infer/src/base/SymOp.mli +++ b/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 -(** [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 : f:(unit -> 'a) -> finally:(unit -> unit) -> 'a +(** [try_finally ~f ~finally] executes [f] and then [finally] even if [f] raises an exception. + Assuming that [finally ()] terminates quickly [Analysis_failure_exe] exceptions are handled correctly. + In particular, an exception raised by [f ()] is delayed until [finally ()] finishes, so [finally ()] should + return reasonably quickly. *) val pp_failure_kind : Format.formatter -> failure_kind -> unit diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index e4dc35412..5dc0a3fa2 100644 --- a/infer/src/base/Utils.ml +++ b/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 res, () = do_finally ~f ~finally in +let try_finally_swallow_timeout ~f ~finally = + 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 = diff --git a/infer/src/base/Utils.mli b/infer/src/base/Utils.mli index d51554b72..ec175a07f 100644 --- a/infer/src/base/Utils.mli +++ b/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 -(** Calls [f] then [finally] even if [f] raised an exception. The original exception is reraised afterwards. *) +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. + Where possible use [SymOp.try_finally] to avoid swallowing timeouts. *)