From 15480f34d52da7cbb742941eed5d8341e2edfc0d Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 17 Dec 2015 18:04:18 -0800 Subject: [PATCH] distinguishing between failures and timeouts Summary: public Crashes during the analysis are classified as timeouts in the .specs file. In addition, when there is a timeout, it does not say *why* the timeout occurred (hard time, symops, or recursion). This diff adds this information to the .specs file and adds a "fail hard" mode where crashes and timeouts will actually stop the analysis in developer mode (but will still be hidden in the normal production mode). Reviewed By: jeremydubreil Differential Revision: D2725382 fb-gh-sync-id: b0b4e5e --- infer/src/backend/cg.ml | 2 +- infer/src/backend/dotty.ml | 10 +++--- infer/src/backend/errdesc.ml | 4 +-- infer/src/backend/exceptions.ml | 4 +-- infer/src/backend/fork.ml | 54 ++++++++++++++++----------------- infer/src/backend/fork.mli | 2 +- infer/src/backend/inferprint.ml | 11 +++++-- infer/src/backend/interproc.ml | 14 +++++---- infer/src/backend/paths.ml | 2 +- infer/src/backend/printer.ml | 10 +++--- infer/src/backend/prover.ml | 4 +-- infer/src/backend/specs.ml | 16 +++++----- infer/src/backend/specs.mli | 2 +- infer/src/backend/state.ml | 2 +- infer/src/backend/symExec.ml | 6 ++-- infer/src/backend/tabulation.ml | 6 ++-- infer/src/backend/utils.ml | 27 +++++++++++------ infer/src/backend/utils.mli | 17 ++++++----- 18 files changed, 106 insertions(+), 87 deletions(-) diff --git a/infer/src/backend/cg.ml b/infer/src/backend/cg.ml index e3e401129..6991f1d4a 100644 --- a/infer/src/backend/cg.ml +++ b/infer/src/backend/cg.ml @@ -357,7 +357,7 @@ let store_to_file (filename : DB.filename) (call_graph : t) = let pp_graph_dotty get_specs (g: t) fmt = let nodes_with_calls = get_all_nodes g in - let num_specs n = try IList.length (get_specs n) with exn when exn_not_timeout exn -> - 1 in + let num_specs n = try IList.length (get_specs n) with exn when exn_not_failure exn -> - 1 in let get_color (n, calls) = if num_specs n != 0 then "green" else "red" in let get_shape (n, calls) = diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index b430b9048..f886540ee 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -559,7 +559,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle = let nodes_e = select_nodes_exp_lambda dotnodes e lambda in let address_struct_id = try get_coordinate_id (IList.hd (IList.filter (is_source_node_of_exp e) nodes_e)) - with exn when exn_not_timeout exn -> (* L.out "@\n@\n PROBLEMS!!!!!!!!!!@.@.@."; *) assert false in + with exn when exn_not_failure exn -> assert false in (* we need to exclude the address node from the sorce of fields. no fields should start from there*) let nl'= IList.filter (fun id -> address_struct_id != id) nl in let links_from_fields = IList.flatten (IList.map ff nl') in @@ -923,7 +923,7 @@ let pp_dotty_prop_list_in_path f plist prev_n curr_n = pp_dotty f (Generic_proposition) po None) plist; if prev_n <> - 1 then F.fprintf f "\n state%iN ->state%iN\n" prev_n curr_n; F.fprintf f "\n } \n" - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> () (* create a dotty file with a single proposition *) @@ -937,7 +937,7 @@ let dotty_prop_to_dotty_file fname prop cycle = pp_dotty fmt_dot Generic_proposition prop (Some cycle); Format.fprintf fmt_dot "@\n}"; close_out out_dot - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> () (* this is used only to print a list of prop parsed with the external parser. Basically deprecated.*) @@ -954,7 +954,7 @@ let pp_proplist_parsed2dotty_file filename plist = let fmt = F.formatter_of_out_channel outc in F.fprintf fmt "#### Dotty version: ####@.%a@.@." pp_list plist; close_out outc - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> () (********** START of Print interprocedural cfgs in dotty format *) @@ -1095,7 +1095,7 @@ let pp_speclist_to_file (filename : DB.filename) spec_list = let pp_speclist_dotty_file (filename : DB.filename) spec_list = try pp_speclist_to_file filename spec_list - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> () (**********************************************************************) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 40063fdba..0bf8b97ca 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -490,7 +490,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (try let t2 = Sil.expand_type tenv _t2 in Sil.typ_equal t1 t2 - with exn when exn_not_timeout exn -> false) + with exn when exn_not_failure exn -> false) | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _)) when is_file -> (* must be a file opened with "open" *) true | _ -> false in @@ -875,7 +875,7 @@ let explain_nth_function_parameter use_buckets deref_str prop n pvar_off = Some (dexp_apply_pvar_off de pvar_off) | None -> None in create_dereference_desc ~use_buckets dexp_opt' deref_str prop loc - with exn when exn_not_timeout exn -> Localise.no_desc) + with exn when exn_not_failure exn -> Localise.no_desc) | _ -> Localise.no_desc (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *) diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 6dd1ab19b..3700e9e65 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -198,8 +198,8 @@ let recognize_exception exn = (Localise.return_statement_missing, desc, Some mloc, Exn_user, Medium, None, Nocat) | Return_value_ignored (desc, mloc) -> (Localise.return_value_ignored, desc, Some mloc, Exn_user, Medium, None, Nocat) - | Timeout_exe _ -> - (Localise.from_string "Timeout_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat) + | Analysis_failure_exe _ -> + (Localise.from_string "Failure_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat) | Skip_function desc -> (Localise.skip_function, desc, None, Exn_developer, Low, None, Nocat) | Skip_pointer_dereference (desc, mloc) -> diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index d2dcbd8f5..a9023267d 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -242,7 +242,7 @@ let filter_max exe_env cg filter set priority_set = (** Handle timeout events *) module Timeout : sig (** execute the function up to a given timeout given by the parameter *) - val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option + val exe_timeout : int -> ('a -> unit) -> 'a -> failure_kind option end = struct let set_alarm nsecs = match Config.os_type with @@ -258,17 +258,9 @@ end = struct | Config.Unix | Config.Cygwin -> set_alarm 0 | Config.Win32 -> SymOp.unset_wallclock_alarm () - let pp_kind f = function - | TOtime -> - F.fprintf f "time" - | TOrecursion n -> - F.fprintf f "recursion %d" n - | TOsymops n -> - F.fprintf f "SymOps %d" n - let timeout_action _ = unset_alarm (); - raise (Timeout_exe (TOtime)) + raise (Analysis_failure_exe (FKtimeout)) let () = begin match Config.os_type with @@ -307,14 +299,14 @@ end = struct restore_timeout () in try before (); - let res = f x in + f x; after (); - Some res + None with - | Timeout_exe kind -> + | Analysis_failure_exe kind -> after (); - Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_kind kind; - None + Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_failure_kind kind; + Some kind | exe -> after (); raise exe @@ -412,21 +404,27 @@ let interprocedural_algorithm (_process_result: process_result) (filter_out: filter_out) : unit = let analyze_proc exe_env pname = (* wrap _analyze_proc and handle exceptions *) + let log_error_and_continue exn kind = + Reporting.log_error pname exn; + let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in + let timestamp = max 1 (prev_summary.Specs.timestamp) in + let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in + let payload = + { prev_summary.Specs.payload with Specs.preposts = Some []; } in + { prev_summary with Specs.stats; payload; timestamp; } in + try _analyze_proc exe_env pname with + | exn when !Config.developer_mode -> + (* in developer mode, fail hard on crashes/timeout *) + raise exn + | Analysis_failure_exe kind as exn -> + (* in production mode, log the timeout/crash and continue with the summary we had before + the failure occurred *) + log_error_and_continue exn kind | exn -> - Reporting.log_error pname exn; - let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in - let timestamp = max 1 (prev_summary.Specs.timestamp) in - let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in - let payload = - { prev_summary.Specs.payload with - Specs.preposts = Some []; } in - let summ = - { prev_summary with - Specs.stats; - payload; - timestamp; } in - summ in + (* this happens due to exceptions from assert false or some other unrecognized exception *) + log_error_and_continue exn (FKcrash (Printexc.to_string exn)) in + let process_result exe_env (pname, calls) summary = (* wrap _process_result and handle exceptions *) try _process_result exe_env (pname, calls) summary with diff --git a/infer/src/backend/fork.mli b/infer/src/backend/fork.mli index 53f8aee04..8d4e04ed9 100644 --- a/infer/src/backend/fork.mli +++ b/infer/src/backend/fork.mli @@ -13,7 +13,7 @@ (** Handle timeout events *) module Timeout : sig (** execute the function up to a given timeout given by the iterations parameter *) - val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option + val exe_timeout : int -> ('a -> unit) -> 'a -> Utils.failure_kind option end val this_cluster_files : int ref (** Number of files in the current cluster *) diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 10af48236..5d8bd0919 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -276,12 +276,17 @@ let summary_values top_proc_set summary = let call_rank = let c1 = 1 and c2 = 1 in logscale (c1 * in_calls + c2 * out_calls) in + + let pp_failure failure = + pp_to_string pp_failure_kind failure in + + let cyclomatic = stats.Specs.cyclomatic in { vname = Procname.to_string proc_name; vname_id = Procname.to_filename proc_name; vspecs = IList.length specs; vtime = Printf.sprintf "%.0f" stats.Specs.stats_time; - vto = if stats.Specs.stats_timeout then "TO" else " "; + vto = Option.map_default pp_failure "NONE" stats.Specs.stats_failure; vsymop = stats.Specs.symops; verr = Errlog.size (fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint) @@ -746,7 +751,9 @@ module Stats = struct let is_defective = found_errors in let is_verified = specs <> [] && not is_defective in let is_checked = not (is_defective || is_verified) in - let is_timeout = Specs.(summary.stats.stats_timeout) in + let is_timeout = match Specs.(summary.stats.stats_failure) with + | None | Some (FKcrash _) -> false + | _ -> true in stats.nprocs <- stats.nprocs + 1; stats.nspecs <- stats.nspecs + (IList.length specs); if is_verified then stats.nverified <- stats.nverified + 1; diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 373925f9d..a283cf25a 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -900,7 +900,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t if recursion_level > !Config.max_recursion then begin L.err "Reached maximum level of recursion, raising a Timeout@."; - raise (Timeout_exe (TOrecursion recursion_level)) + raise (Analysis_failure_exe (FKrecursion_timeout recursion_level)) end in let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list) = @@ -1093,12 +1093,14 @@ let update_summary prev_summary specs proc_name elapsed res = let timestamp = max 1 (prev_summary.Specs.timestamp + if changed then 1 else 0) in let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in - let timeout = res == None || prev_summary.Specs.stats.Specs.stats_timeout in + let failure = match res with + | None -> prev_summary.Specs.stats.Specs.stats_failure + | Some failure_kind -> res in let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time; Specs.symops = symops; - Specs.stats_timeout = timeout } in + Specs.stats_failure = failure; } in let payload = { prev_summary.Specs.payload with Specs.preposts = Some new_specs; } in @@ -1148,7 +1150,7 @@ let perform_transition exe_env cg proc_name = let start_node = Cfg.Procdesc.get_start_node pdesc in f start_node | None -> () - with exn when exn_not_timeout exn -> () in + with exn when exn_not_failure exn -> () in apply_start_node (do_before_node 0); try Config.allowleak := true; @@ -1156,7 +1158,7 @@ let perform_transition exe_env cg proc_name = Config.allowleak := allowleak; apply_start_node do_after_node; res - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> apply_start_node do_after_node; Config.allowleak := allowleak; L.err "Error in collect_preconditions for %a@." Procname.pp proc_name; @@ -1354,7 +1356,7 @@ let print_stats_cfg proc_shadowed proc_is_active cfg = | [], _ -> incr num_nospec_error_proc | _, _ -> incr num_spec_error_proc in tot_symops := !tot_symops + stats.Specs.symops; - if stats.Specs.stats_timeout then incr num_timeout; + if Option.is_some stats.Specs.stats_failure then incr num_timeout; Errlog.extend_table err_table err_log in let print_file_stats fmt () = let num_errors = Errlog.err_table_size_footprint Exceptions.Kerror err_table in diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 2f37ff023..7bc78ff0f 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -311,7 +311,7 @@ end = struct | Some node -> pos_opt <> None && filter node | None -> false - with exn when exn_not_timeout exn -> false in + with exn when exn_not_failure exn -> false in let position_seen = ref false in let inverse_sequence = let log = ref [] in diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 3fa168478..8ca494405 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -351,11 +351,11 @@ end = struct try Some (Hashtbl.find hash fname) with Not_found -> - try - let lines_arr = read_file (DB.source_file_to_string fname) in - Hashtbl.add hash fname lines_arr; - Some lines_arr - with exn when exn_not_timeout exn -> None + try + let lines_arr = read_file (DB.source_file_to_string fname) in + Hashtbl.add hash fname lines_arr; + Some lines_arr + with exn when exn_not_failure exn -> None let from_file_linenum_original hash fname linenum = match file_data hash fname with diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index c8dc43ff1..0fd2acb5f 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -16,7 +16,7 @@ open Utils let decrease_indent_when_exception thunk = try (thunk ()) - with exn when exn_not_timeout exn -> (L.d_decrease_indent 1; raise exn) + with exn when exn_not_failure exn -> (L.d_decrease_indent 1; raise exn) let compute_max_from_nonempty_int_list l = IList.hd (IList.rev (IList.sort Sil.Int.compare_value l)) @@ -1757,7 +1757,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 decrease_indent_when_exception (fun () -> try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2 - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> begin (L.d_strln_color Red) "backtracking lseg: trying rhs of length exactly 1"; let (_, para_inst3) = Sil.hpara_instantiate para2 _e2 _f2 elist2 in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 32c89b65a..e1a047b5d 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -288,7 +288,7 @@ type call_stats = CallStats.t (** Execution statistics *) type stats = { stats_time: float; (** Analysis time for the procedure *) - stats_timeout: bool; (** Flag to indicate whether a timeout occurred *) + stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *) stats_calls: Cg.in_out_calls; (** num of procs calling, and called *) symops: int; (** Number of SymOp's throughout the whole analysis of the function *) mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *) @@ -342,12 +342,14 @@ let pp_time whole_seconds fmt t = if whole_seconds then F.fprintf fmt "%3.0f s" t else F.fprintf fmt "%f s" t -let pp_timeout fmt = function - | true -> F.fprintf fmt "Y" - | false -> F.fprintf fmt "N" +let pp_failure_kind_opt fmt failure_kind_opt = match failure_kind_opt with + | Some failure_kind -> pp_failure_kind fmt failure_kind + | None -> F.fprintf fmt "NONE" let pp_stats err_log whole_seconds fmt stats = - F.fprintf fmt "TIME:%a TIMEOUT:%a SYMOPS:%d CALLS:%d,%d@\n" (pp_time whole_seconds) stats.stats_time pp_timeout stats.stats_timeout stats.symops stats.stats_calls.Cg.in_calls stats.stats_calls.Cg.out_calls; + F.fprintf fmt "TIME:%a FAILURE:%a SYMOPS:%d CALLS:%d,%d@\n" (pp_time whole_seconds) + stats.stats_time pp_failure_kind_opt stats.stats_failure stats.symops + stats.stats_calls.Cg.in_calls stats.stats_calls.Cg.out_calls; F.fprintf fmt "ERRORS: @[%a@]@." Errlog.pp_errors err_log; F.fprintf fmt "WARNINGS: @[%a@]" Errlog.pp_warnings err_log @@ -463,7 +465,7 @@ let pp_spec_table pe whole_seconds fmt () = let empty_stats calls cyclomatic in_out_calls_opt = { stats_time = 0.0; - stats_timeout = false; + stats_failure = None; stats_calls = (match in_out_calls_opt with | Some in_out_calls -> in_out_calls @@ -737,7 +739,7 @@ let get_iterations proc_name = try let time_str = Hashtbl.find proc_flags proc_flag_iterations in Pervasives.int_of_string time_str - with exn when exn_not_timeout exn -> !iterations_cmdline + with exn when exn_not_failure exn -> !iterations_cmdline (** Return the specs and parameters for the proc in the spec table *) let get_specs_formals proc_name = diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 7532a0088..8f115a5d2 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -102,7 +102,7 @@ end (** Execution statistics *) type stats = { stats_time: float; (** Analysis time for the procedure *) - stats_timeout: bool; (** Flag to indicate whether a timeout occurred *) + stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *) stats_calls: Cg.in_out_calls; (** num of procs calling, and called *) symops: int; (** Number of SymOp's throughout the whole analysis of the function *) mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *) diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 64542c1f6..7c812eaa4 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -234,7 +234,7 @@ let extract_pre p tenv pdesc abstract_fun = Sil.sub_of_list (IList.map (fun id -> incr count; (id, Sil.Var (Ident.create_normal Ident.name_spec !count))) idlist) in let _, p' = Cfg.remove_locals_formals pdesc p in let pre, _ = Prop.extract_spec p' in - let pre' = try abstract_fun tenv pre with exn when exn_not_timeout exn -> pre in + let pre' = try abstract_fun tenv pre with exn when exn_not_failure exn -> pre in Prop.normalize (Prop.prop_sub sub pre') (** return the normalized precondition extracted form the last prop seen, if any diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 5a7c13228..d2f419682 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -654,7 +654,7 @@ let redirect_shared_ptr tenv cfg pname actual_params = let name = Mangled.to_string cl_name in name = "shared_ptr" || name = "__shared_ptr" | t -> false - with exn when exn_not_timeout exn -> false in + with exn when exn_not_failure exn -> false in (* We pattern match over some specific library function, *) (* so we make precise matching to distinghuis between *) (* references and pointers in C++ *) @@ -1141,7 +1141,7 @@ and sym_exec_generated mask_errors cfg tenv pdesc instrs ppl = let exe_instr instr (p, path) = L.d_str "Executing Generated Instruction "; Sil.d_instr instr; L.d_ln (); try sym_exec cfg tenv pdesc instr p path - with exn when exn_not_timeout exn && mask_errors -> + with exn when exn_not_failure exn && mask_errors -> let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in let loc = (match ml_source with | Some (src, l, c) -> "at "^(src^" "^(string_of_int l)) @@ -1316,7 +1316,7 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in try sym_exec_generated false cfg tenv pdesc [letderef] result - with e when exn_not_timeout e -> + with e when exn_not_failure e -> if not fails_on_nil then let deref_str = Localise.deref_str_nil_argument_in_variadic_method callee_pname nargs i in let err_desc = diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 13ef81264..af7eeb52a 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -403,7 +403,7 @@ let rec fsel_star_fld fsel1 fsel2 = match fsel1, fsel2 with and array_content_star se1 se2 = try sexp_star_fld se1 se2 with - | exn when exn_not_timeout exn -> se1 (* let postcondition override *) + | exn when exn_not_failure exn -> se1 (* let postcondition override *) and esel_star_fld esel1 esel2 = match esel1, esel2 with | [], esel2 -> (* don't know whether element is read or written in fun call with array *) @@ -476,7 +476,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr end in try star sigma1 sigma2 - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> L.d_str "cannot star "; Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2; L.d_ln (); @@ -510,7 +510,7 @@ let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) lis | _ -> star sg1 typings2' end in try star sigma1 typings2 - with exn when exn_not_timeout exn -> + with exn when exn_not_failure exn -> L.d_str "cannot star "; Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2; L.d_ln (); diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index c376977e8..4dee4aeed 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -257,20 +257,27 @@ let pp_ml_location_opt fmt mloco = | None -> () | Some mloc -> F.fprintf fmt "(%a)" pp_ml_location mloc -(** {2 SymOp and Timeouts: units of symbolic execution} *) +(** {2 SymOp and Failures: units of symbolic execution} *) -type timeout_kind = - | TOtime (* max time exceeded *) - | TOsymops of int (* max symop's exceeded *) - | TOrecursion of int (* max recursion level exceeded *) +type failure_kind = + | FKtimeout (* max time exceeded *) + | FKsymops_timeout of int (* max symop's exceeded *) + | FKrecursion_timeout of int (* max recursion level exceeded *) + | FKcrash of string (* uncaught exception or failed assertion *) -(** Timeout exception *) -exception Timeout_exe of timeout_kind +(** failure that prevented analysis from finishing *) +exception Analysis_failure_exe of failure_kind -let exn_not_timeout = function - | Timeout_exe _ -> false +let exn_not_failure = function + | Analysis_failure_exe _ -> false | _ -> true +let pp_failure_kind fmt = function + | FKtimeout -> F.fprintf fmt "TIMEOUT" + | FKsymops_timeout symops -> F.fprintf fmt "SYMOPS TIMEOUT (%d)" symops + | FKrecursion_timeout level -> F.fprintf fmt "RECURSION TIMEOUT(%d)" level + | FKcrash msg -> F.fprintf fmt "CRASH (%s)" msg + let symops_timeout, seconds_timeout = (* default timeout and long timeout are the same for now, but this will change shortly *) let default_symops_timeout = 333 in @@ -358,7 +365,7 @@ module SymOp = struct let pay () = incr symop_count; incr symop_total; if !symop_count > !timeout_symops && !alarm_active - then raise (Timeout_exe (TOsymops !symop_count)); + then raise (Analysis_failure_exe (FKsymops_timeout !symop_count)); check_wallclock_alarm () (** Reset the counters *) diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 9bd832ba7..a360a2dc8 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -154,7 +154,7 @@ val pp_current_time : Format.formatter -> unit -> unit (** Print the time in seconds elapsed since the beginning of the execution of the current command. *) val pp_elapsed_time : Format.formatter -> unit -> unit -(** {2 SymOp and Timeouts: units of symbolic execution} *) +(** {2 SymOp and Failures: units of symbolic execution} *) (** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *) val initial_analysis_time : float @@ -174,16 +174,19 @@ val get_timeout_seconds : unit -> int (** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *) val set_iterations : int -> unit -type timeout_kind = - | TOtime (* max time exceeded *) - | TOsymops of int (* max symop's exceeded *) - | TOrecursion of int (* max recursion level exceeded *) +type failure_kind = + | FKtimeout (* max time exceeded *) + | FKsymops_timeout of int (* max symop's exceeded *) + | FKrecursion_timeout of int (* max recursion level exceeded *) + | FKcrash of string (* uncaught exception or failed assertion *) (** Timeout exception *) -exception Timeout_exe of timeout_kind +exception Analysis_failure_exe of failure_kind (** check that the exception is not a timeout exception *) -val exn_not_timeout : exn -> bool +val exn_not_failure : exn -> bool + +val pp_failure_kind : Format.formatter -> failure_kind -> unit (** Count the number of symbolic operations *) module SymOp : sig