diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 33ffea1b4..288baaffc 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -1564,10 +1564,11 @@ 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 - try - if Rename.check lost_little then ( CheckJoin.final () ; (s1, s2, s3) ) - else ( L.d_strln "failed Rename.check" ; CheckJoin.final () ; raise Sil.JoinFail ) - with exn -> CheckJoin.final () ; reraise exn + Utils.try_finally + ~f:(fun () -> + if Rename.check lost_little then (s1, s2, s3) + else ( L.d_strln "failed Rename.check" ; raise Sil.JoinFail )) + ~finally:CheckJoin.final let rec sigma_partial_meet' tenv (sigma_acc: Prop.sigma) (sigma1_in: Prop.sigma) (sigma2_in: Prop.sigma) : Prop.sigma = @@ -1806,13 +1807,9 @@ let prop_partial_meet tenv p1 p2 = FreshVarExp.init () ; Todo.init () ; try - let res = eprop_partial_meet tenv p1 p2 in - Rename.final () ; FreshVarExp.final () ; Todo.final () ; Some res - with exn -> - Rename.final () ; - FreshVarExp.final () ; - Todo.final () ; - match exn with Sil.JoinFail -> None | _ -> reraise exn + Utils.try_finally ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2)) ~finally:(fun () -> + Rename.final () ; FreshVarExp.final () ; Todo.final () ) + with Sil.JoinFail -> None let eprop_partial_join' tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.t) : Prop.normal Prop.t = @@ -1914,21 +1911,15 @@ let prop_partial_join pname tenv mode p1 p2 = FreshVarExp.init () ; Todo.init () ; try - let p1', p2' = footprint_partial_join' tenv p1 p2 in - let rename_footprint = Rename.reset () in - Todo.reset rename_footprint ; - let res = Some (eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2')) in - if !Config.footprint then JoinState.set_footprint false ; - Rename.final () ; - FreshVarExp.final () ; - Todo.final () ; - res - with exn -> - Rename.final () ; - FreshVarExp.final () ; - Todo.final () ; - if !Config.footprint then JoinState.set_footprint false ; - match exn with Sil.JoinFail -> None | _ -> reraise exn ) + Utils.try_finally + ~f:(fun () -> + let p1', p2' = footprint_partial_join' tenv p1 p2 in + let rename_footprint = Rename.reset () in + Todo.reset rename_footprint ; + let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in + if !Config.footprint then JoinState.set_footprint false ; + Some res) ~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final () ) + with Sil.JoinFail -> None ) | Some _ -> res_by_implication_only @@ -1937,10 +1928,8 @@ let eprop_partial_join tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed P Rename.init () ; FreshVarExp.init () ; Todo.init () ; - try - let res = eprop_partial_join' tenv mode ep1 ep2 in - Rename.final () ; FreshVarExp.final () ; Todo.final () ; res - with exn -> Rename.final () ; FreshVarExp.final () ; Todo.final () ; reraise exn + Utils.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/interproc.ml b/infer/src/backend/interproc.ml index c7b2497bc..0240a243c 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -443,10 +443,10 @@ let forward_tabulate tenv proc_cfg wl = L.d_decrease_indent 1 ; L.d_ln () with exn -> - let backtrace = Caml.Printexc.get_raw_backtrace () in - if Exceptions.handle_exception exn && !Config.footprint then ( - handle_exn exn ; L.d_decrease_indent 1 ; L.d_ln () ) - else reraise ~backtrace exn + reraise_if exn ~f:(fun () -> not !Config.footprint || not (Exceptions.handle_exception exn)) ; + handle_exn exn ; + L.d_decrease_indent 1 ; + L.d_ln () in let do_node curr_node pathset_todo session handle_exn = check_prop_size pathset_todo ; @@ -473,13 +473,11 @@ let forward_tabulate tenv proc_cfg wl = if !handle_exn_called then Printer.force_delayed_prints () ; do_after_node curr_node with exn -> - let backtrace = Caml.Printexc.get_raw_backtrace () in - if Exceptions.handle_exception exn then ( - handle_exn_node curr_node exn ; - Printer.force_delayed_prints () ; - do_after_node curr_node ; - if not !Config.footprint then raise RE_EXE_ERROR ) - else reraise ~backtrace exn + reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ; + handle_exn_node curr_node exn ; + Printer.force_delayed_prints () ; + do_after_node curr_node ; + if not !Config.footprint then raise RE_EXE_ERROR in while not (Worklist.is_empty wl) do let curr_node = Worklist.remove wl in diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 03e70413e..61ad8c7e6 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -147,19 +147,17 @@ let run_proc_analysis analyze_proc curr_pdesc callee_pdesc = let final_summary = postprocess summary in restore_global_state old_state ; final_summary with exn -> - restore_global_state old_state ; - if Config.keep_going then ( - L.internal_error "@\nERROR RUNNING BACKEND: %a %s@\n@\nBACK TRACE@\n%s@?" Typ.Procname.pp - callee_pname (Exn.to_string exn) (Printexc.get_backtrace ()) ; - match exn with - | SymOp.Analysis_failure_exe kind - -> (* in production mode, log the timeout/crash and continue with the summary we had before - the failure occurred *) - log_error_and_continue exn initial_summary kind - | _ - -> (* this happens with assert false or some other unrecognized exception *) - log_error_and_continue exn initial_summary (FKcrash (Exn.to_string exn)) ) - else reraise exn + reraise_if exn ~f:(fun () -> restore_global_state old_state ; not Config.keep_going) ; + L.internal_error "@\nERROR RUNNING BACKEND: %a %s@\n@\nBACK TRACE@\n%s@?" Typ.Procname.pp + callee_pname (Exn.to_string exn) (Printexc.get_backtrace ()) ; + match exn with + | SymOp.Analysis_failure_exe kind + -> (* in production mode, log the timeout/crash and continue with the summary we had before + the failure occurred *) + log_error_and_continue exn initial_summary kind + | _ + -> (* this happens with assert false or some other unrecognized exception *) + log_error_and_continue exn initial_summary (FKcrash (Exn.to_string exn)) let analyze_proc_desc curr_pdesc callee_pdesc : Specs.summary option = let callee_pname = Procdesc.get_proc_name callee_pdesc in diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 8b092cce3..5f7e9ea50 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -17,7 +17,7 @@ module F = Format let decrease_indent_when_exception thunk = try thunk () - with exn when SymOp.exn_not_failure exn -> L.d_decrease_indent 1 ; reraise exn + with exn when SymOp.exn_not_failure exn -> reraise_after exn ~f:(fun () -> L.d_decrease_indent 1) let compute_max_from_nonempty_int_list l = uw (List.max_elt ~cmp:IntLit.compare_value l) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index f6504603a..1940cc958 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1401,16 +1401,14 @@ and instrs ?(mask_errors= false) tenv pdesc instrs ppl = L.d_ln () ; try sym_exec tenv pdesc instr p path with exn -> - let backtrace = Caml.Printexc.get_raw_backtrace () in - if SymOp.exn_not_failure exn && mask_errors then - let error = Exceptions.recognize_exception exn in - let loc = - match error.ml_loc with Some ml_loc -> "at " ^ L.ml_loc_to_string ml_loc | None -> "" - in - L.d_warning ("Generated Instruction Failed with: " ^ error.name.IssueType.unique_id ^ loc) ; - L.d_ln () ; - [(p, path)] - else reraise ~backtrace exn + reraise_if exn ~f:(fun () -> not mask_errors || not (SymOp.exn_not_failure exn)) ; + let error = Exceptions.recognize_exception exn in + let loc = + match error.ml_loc with Some ml_loc -> "at " ^ L.ml_loc_to_string ml_loc | None -> "" + in + L.d_warning ("Generated Instruction Failed with: " ^ error.name.IssueType.unique_id ^ loc) ; + L.d_ln () ; + [(p, path)] in let f plist instr = List.concat_map ~f:(exe_instr instr) plist in List.fold ~f ~init:ppl instrs @@ -1606,14 +1604,13 @@ and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos let load_instr = Sil.Load (tmp_id_deref, lexp, typ, loc) in try instrs tenv pdesc [load_instr] result with e when SymOp.exn_not_failure e -> - if not fails_on_nil then - let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in - let err_desc = - Errdesc.explain_dereference tenv ~use_buckets:true ~is_premature_nil:true deref_str prop_ - loc - in - raise (Exceptions.Premature_nil_termination (err_desc, __POS__)) - else reraise e + reraise_if e ~f:(fun () -> fails_on_nil) ; + let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in + let err_desc = + Errdesc.explain_dereference tenv ~use_buckets:true ~is_premature_nil:true deref_str prop_ + loc + in + raise (Exceptions.Premature_nil_termination (err_desc, __POS__)) in (* fold_left reverses the arguments back so that we report an *) (* error on the first premature nil argument *) @@ -1804,11 +1801,10 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), State.mark_instr_ok () ; Paths.PathSet.from_renamed_list results with exn -> - let backtrace = Caml.Printexc.get_raw_backtrace () in - if Exceptions.handle_exception exn && !Config.footprint then ( - handle_exn exn ; (* calls State.mark_instr_fail *) - Paths.PathSet.empty ) - else reraise ~backtrace exn + reraise_if exn ~f:(fun () -> not !Config.footprint || not (Exceptions.handle_exception exn)) ; + handle_exn exn ; + (* calls State.mark_instr_fail *) + Paths.PathSet.empty (** {2 Lifted Abstract Transfer Functions} *) diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index 219d5ecb2..af7943171 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -99,11 +99,11 @@ let exe_timeout f x = Option.iter (SymOp.get_timeout_seconds ()) ~f:set_alarm ; SymOp.set_alarm () in - try suspend_existing_timeout_and_start_new_one () ; f x ; resume_previous_timeout () ; None with - | SymOp.Analysis_failure_exe kind - -> resume_previous_timeout () ; - L.progressbar_timeout_event kind ; - Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ; - Some kind - | exe - -> resume_previous_timeout () ; reraise exe + try + Utils.try_finally + ~f:(fun () -> suspend_existing_timeout_and_start_new_one () ; f x ; None) + ~finally:resume_previous_timeout + with SymOp.Analysis_failure_exe kind -> + L.progressbar_timeout_event kind ; + Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ; + Some kind diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 6eedc0b40..96e033c38 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2412,11 +2412,11 @@ let specs_library = let set_reference_and_call_function reference value f x = let saved = !reference in let restore () = reference := saved in - try - reference := value ; - let res = f x in - restore () ; res - with exn -> restore () ; reraise exn + Utils.try_finally + ~f:(fun () -> + reference := value ; + f x) + ~finally:restore (** Current Objective-C Automatic Reference Counting (ARC) mode *) let arc_mode = ref false diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index cd3a08303..d0bb4f762 100644 --- a/infer/src/base/SymOp.ml +++ b/infer/src/base/SymOp.ml @@ -28,22 +28,18 @@ let try_finally ?(fail_early= false) f g = | r -> g () ; r | exception (Analysis_failure_exe _ as f_exn) - -> let backtrace = Caml.Printexc.get_raw_backtrace () in - ( if not fail_early then - try g () - with _ -> () (* swallow in favor of the original exception *) ) ; - reraise ~backtrace f_exn + -> reraise_after f_exn ~f:(fun () -> + if not fail_early then + try g () + with _ -> (* swallow in favor of the original exception *) () ) | exception f_exn - -> let f_backtrace = Caml.Printexc.get_raw_backtrace () in - match g () with - | () - -> reraise ~backtrace:f_backtrace f_exn - | exception (Analysis_failure_exe _ as g_exn) - -> reraise g_exn - | exception _ - -> reraise ~backtrace:f_backtrace f_exn - -let finally_try g f = try_finally f g + -> reraise_after f_exn ~f:(fun () -> + try g () + with + | g_exn + when (* do not swallow Analysis_failure_exe thrown from g *) + match g_exn with Analysis_failure_exe _ -> false | _ -> true + -> () ) let pp_failure_kind fmt = function | FKtimeout diff --git a/infer/src/base/SymOp.mli b/infer/src/base/SymOp.mli index e1abb6db8..857e92a8e 100644 --- a/infer/src/base/SymOp.mli +++ b/infer/src/base/SymOp.mli @@ -73,7 +73,4 @@ val try_finally : ?fail_early:bool -> (unit -> 'a) -> (unit -> unit) -> 'a return reasonably quickly. [~fail_early=true] can be passed to skip executing [g ()] when [f ()] raises a [Analysis_failure_exe] exception. *) -val finally_try : (unit -> unit) -> (unit -> 'a) -> 'a -(** [finally_try g f] is equivalent to [try_finally f g]. *) - val pp_failure_kind : Format.formatter -> failure_kind -> unit diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index a10840c38..e4dc35412 100644 --- a/infer/src/base/Utils.ml +++ b/infer/src/base/Utils.ml @@ -165,29 +165,32 @@ 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 g = +let do_finally ~f ~finally = let res = try f () with exc -> - let backtrace = Caml.Printexc.get_raw_backtrace () in - ( try g () |> ignore - with _ -> () (* swallow in favor of the original exception *) ) ; - reraise ~backtrace exc + reraise_after exc ~f:(fun () -> + try finally () |> ignore + with _ -> (* swallow in favor of the original exception *) () ) in - let res' = g () in + let res' = finally () in (res, res') +let try_finally ~f ~finally = + let res, () = do_finally ~f ~finally in + res + let with_file_in file ~f = let ic = In_channel.create file in let f () = f ic in - let g () = In_channel.close ic in - do_finally f g |> fst + let finally () = In_channel.close ic in + try_finally ~f ~finally let with_file_out file ~f = let oc = Out_channel.create file in let f () = f oc in - let g () = Out_channel.close oc in - do_finally f g |> fst + let finally () = Out_channel.close oc in + try_finally ~f ~finally let write_json_to_file destfile json = with_file_out destfile ~f:(fun oc -> Yojson.Basic.pretty_to_channel oc json) @@ -199,8 +202,8 @@ let consume_in chan_in = let with_process_in command read = let chan = Unix.open_process_in command in let f () = read chan in - let g () = consume_in chan ; Unix.close_process_in chan in - do_finally f g + let finally () = consume_in chan ; Unix.close_process_in chan in + do_finally ~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 be634bc68..d51554b72 100644 --- a/infer/src/base/Utils.mli +++ b/infer/src/base/Utils.mli @@ -94,3 +94,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. *) diff --git a/infer/src/clang/Capture.ml b/infer/src/clang/Capture.ml index 6ce955dc0..963bfc337 100644 --- a/infer/src/clang/Capture.ml +++ b/infer/src/clang/Capture.ml @@ -93,9 +93,8 @@ let run_clang_frontend ast_source = let run_and_validate_clang_frontend ast_source = try run_clang_frontend ast_source with exc -> - if not Config.keep_going then reraise exc - else - L.internal_error "ERROR RUNNING CAPTURE: %a@\n%s@\n" Exn.pp exc (Printexc.get_backtrace ()) + reraise_if exc ~f:(fun () -> not Config.keep_going) ; + L.internal_error "ERROR RUNNING CAPTURE: %a@\n%s@\n" Exn.pp exc (Printexc.get_backtrace ()) let run_clang clang_command read = let exit_with_error exit_code = diff --git a/infer/src/integration/Javac.ml b/infer/src/integration/Javac.ml index b83a52a02..a3971ca7e 100644 --- a/infer/src/integration/Javac.ml +++ b/infer/src/integration/Javac.ml @@ -59,27 +59,25 @@ let compile compiler build_prog build_args = let shell_cmd = Utils.shell_escape_command cmd in let shell_cmd_redirected = Printf.sprintf "%s 2>'%s'" shell_cmd verbose_out_file in L.(debug Capture Quiet) "Trying to execute: %s@." shell_cmd_redirected ; - let error_k_or_fail err_msg = - match (error_k, err_msg) with - | Some k, `UnixError (err, log) + match Utils.with_process_in shell_cmd_redirected In_channel.input_all with + | log, Error err -> ( + match error_k with + | Some k -> L.(debug Capture Quiet) "*** Failed: %s!@\n%s@." (Unix.Exit_or_signal.to_string_hum (Error err)) log ; k () - | Some k, `ExceptionError exn - -> L.(debug Capture Quiet) "*** Failed: %a!@\n" Exn.pp exn ; k () - | None, `UnixError (err, log) + | None -> let verbose_errlog = Utils.with_file_in verbose_out_file ~f:In_channel.input_all in L.(die UserError) "@\n*** Failed to execute compilation command: %s@\n*** Command: %s@\n*** Output:@\n%s%s@\n*** Infer needs a working compilation command to run.@." - (Unix.Exit_or_signal.to_string_hum (Error err)) shell_cmd log verbose_errlog - | None, `ExceptionError exn - -> reraise exn - in - match Utils.with_process_in shell_cmd_redirected In_channel.input_all with - | log, Error err - -> error_k_or_fail (`UnixError (err, log)) + (Unix.Exit_or_signal.to_string_hum (Error err)) shell_cmd log verbose_errlog ) | exception exn - -> error_k_or_fail (`ExceptionError exn) + -> reraise_if exn ~f:(fun () -> + match error_k with + | Some k + -> L.(debug Capture Quiet) "*** Failed: %a!@\n" Exn.pp exn ; k () ; false + | None + -> true ) | log, Ok () -> L.(debug Capture Quiet) "*** Success. Logs:@\n%s" log in diff --git a/infer/src/istd/IStd.ml b/infer/src/istd/IStd.ml index 52677efa6..5475b4bb8 100644 --- a/infer/src/istd/IStd.ml +++ b/infer/src/istd/IStd.ml @@ -63,12 +63,17 @@ module PVariant = struct let ( = ) (v1: [> ]) (v2: [> ]) = Polymorphic_compare.( = ) v1 v2 end -let reraise ?backtrace:backtrace0 exn = - let backtrace = - match backtrace0 with Some bt -> bt | None -> Caml.Printexc.get_raw_backtrace () - in +(** Reraise the exception after doing f. Always reraise immediately after catching the exception, otherwise the backtrace can be wrong *) +let reraise_after ~f exn = + let backtrace = Caml.Printexc.get_raw_backtrace () in + let () = f () in Caml.Printexc.raise_with_backtrace exn backtrace +(** Reraise the exception if f returns true. Always reraise immediately after catching the exception, otherwise the backtrace can be wrong *) +let reraise_if ~f exn = + let backtrace = Caml.Printexc.get_raw_backtrace () in + if f () then Caml.Printexc.raise_with_backtrace exn backtrace + let failwith _ : [`use_Logging_die_instead] = assert false let failwithf _ : [`use_Logging_die_instead] = assert false diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index ff1c3b7d7..cb7ce0199 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -202,7 +202,9 @@ let compute_source_icfg linereader classes program tenv source_basename package_ {JContext.cg= Cg.create source_file; JContext.cfg= Cfg.create_cfg (); JContext.tenv= tenv} in let select test procedure cn node = - if test node then try procedure cn node with Bir.Subroutine -> () | e -> reraise e + if test node then + try procedure cn node + with Bir.Subroutine -> () in let () = JBasics.ClassMap.iter @@ -216,9 +218,6 @@ let compute_class_icfg source_file linereader program tenv node = let icfg = {JContext.cg= Cg.create source_file; JContext.cfg= Cfg.create_cfg (); JContext.tenv= tenv} in - ( try create_icfg source_file linereader program icfg (Javalib.get_name node) node with - | Bir.Subroutine - -> () - | e - -> reraise e ) ; + ( try create_icfg source_file linereader program icfg (Javalib.get_name node) node + with Bir.Subroutine -> () ) ; (icfg.JContext.cg, icfg.JContext.cfg)