From b881887bf20fddc50e6487077a5915565bdc19ce Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Apr 2016 17:13:46 -0700 Subject: [PATCH] Refactor Utils.SymOp into separate module Summary:public Refactor Utils.SymOp into a separate module, bringing the failure_kind type and associated operations. Reviewed By: cristianoc Differential Revision: D3161640 fb-gh-sync-id: be3d7c9 fbshipit-source-id: be3d7c9 --- infer/src/IR/cg.ml | 2 +- infer/src/backend/SymOp.ml | 154 ++++++++++++++++++++++++++ infer/src/backend/SymOp.mli | 71 ++++++++++++ infer/src/backend/config.ml | 23 ++++ infer/src/backend/dotty.ml | 12 +-- infer/src/backend/errdesc.ml | 4 +- infer/src/backend/exceptions.ml | 2 +- infer/src/backend/inferanalyze.ml | 8 +- infer/src/backend/inferprint.ml | 2 +- infer/src/backend/interproc.ml | 6 +- infer/src/backend/io_infer.ml | 2 +- infer/src/backend/logging.ml | 8 +- infer/src/backend/logging.mli | 2 +- infer/src/backend/ondemand.ml | 2 +- infer/src/backend/paths.ml | 2 +- infer/src/backend/printer.ml | 2 +- infer/src/backend/prover.ml | 4 +- infer/src/backend/specs.ml | 5 +- infer/src/backend/specs.mli | 3 +- infer/src/backend/state.ml | 2 +- infer/src/backend/symExec.ml | 4 +- infer/src/backend/tabulation.ml | 6 +- infer/src/backend/timeout.ml | 8 +- infer/src/backend/timeout.mli | 2 +- infer/src/backend/utils.ml | 173 +----------------------------- infer/src/backend/utils.mli | 74 ------------- 26 files changed, 296 insertions(+), 287 deletions(-) create mode 100644 infer/src/backend/SymOp.ml create mode 100644 infer/src/backend/SymOp.mli diff --git a/infer/src/IR/cg.ml b/infer/src/IR/cg.ml index de8349086..3f1e959ff 100644 --- a/infer/src/IR/cg.ml +++ b/infer/src/IR/cg.ml @@ -328,7 +328,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_failure exn -> - 1 in + let num_specs n = try IList.length (get_specs n) with exn when SymOp.exn_not_failure exn -> - 1 in let get_color (n, _) = if num_specs n != 0 then "green" else "red" in let get_shape (n, _) = diff --git a/infer/src/backend/SymOp.ml b/infer/src/backend/SymOp.ml new file mode 100644 index 000000000..ec60c0669 --- /dev/null +++ b/infer/src/backend/SymOp.ml @@ -0,0 +1,154 @@ +(* + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Symbolic Operations and Failures: the units in which analysis work is measured *) + +open! Utils + +module F = Format + + +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 *) + +(** failure that prevented analysis from finishing *) +exception Analysis_failure_exe of failure_kind + +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 + + +(** Count the number of symbolic operations *) + +(** Timeout in seconds for each function *) +let timeout_seconds = ref (!Config.seconds_per_iteration *. (float_of_int !Config.iterations)) + +(** Timeout in SymOps *) +let timeout_symops = ref (!Config.symops_per_iteration * !Config.iterations) + +let get_timeout_seconds () = !timeout_seconds + +(** Internal state of the module *) +type t = + { + (** Only throw timeout exception when alarm is active *) + mutable alarm_active : bool; + + (** last wallclock set by an alarm, if any *) + mutable last_wallclock : float option; + + (** Number of symop's *) + mutable symop_count : int; + + (** Counter for the total number of symop's. + The new state created when save_state is called shares this counter + if keep_symop_total is true. Otherwise, a new counter is created. *) + symop_total : int ref; + } + +let initial () : t = + { + alarm_active = false; + last_wallclock = None; + symop_count = 0; + symop_total = ref 0; + } + +(** Global State *) +let gs : t ref = ref (initial ()) + +(** Restore the old state. *) +let restore_state state = + gs := state + +(** Return the old state, and revert the current state to the initial one. + If keep_symop_total is true, share the total counter. *) +let save_state ~keep_symop_total = + let old_state = !gs in + let new_state = + let st = initial () in + if keep_symop_total + then + { st with symop_total = old_state.symop_total } + else + st in + gs := new_state; + old_state + +(** handler for the wallclock timeout *) +let wallclock_timeout_handler = ref None + +(** set the handler for the wallclock timeout *) +let set_wallclock_timeout_handler handler = + wallclock_timeout_handler := Some handler + +(** Set the wallclock alarm checked at every pay() *) +let set_wallclock_alarm nsecs = + !gs.last_wallclock <- Some (Unix.gettimeofday () +. nsecs) + +(** Unset the wallclock alarm checked at every pay() *) +let unset_wallclock_alarm () = + !gs.last_wallclock <- None + +(** if the wallclock alarm has expired, raise a timeout exception *) +let check_wallclock_alarm () = + match !gs.last_wallclock, !wallclock_timeout_handler with + | Some alarm_time, Some handler when Unix.gettimeofday () >= alarm_time -> + unset_wallclock_alarm (); + handler () + | _ -> () + +(** Return the time remaining before the wallclock alarm expires *) +let get_remaining_wallclock_time () = + match !gs.last_wallclock with + | Some alarm_time -> + max 0.0 (alarm_time -. Unix.gettimeofday ()) + | None -> + 0.0 + +(** Return the total number of symop's since the beginning *) +let get_total () = + !(!gs.symop_total) + +(** Reset the total number of symop's *) +let reset_total () = + !gs.symop_total := 0 + +(** Count one symop *) +let pay () = + !gs.symop_count <- !gs.symop_count + 1; + !gs.symop_total := !(!gs.symop_total) + 1; + if !gs.symop_count > !timeout_symops && + !gs.alarm_active + then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count)); + check_wallclock_alarm () + +(** Reset the counter *) +let reset_count () = + !gs.symop_count <- 0 + +(** Reset the counter and activate the alarm *) +let set_alarm () = + reset_count (); + !gs.alarm_active <- true + +(** De-activate the alarm *) +let unset_alarm () = + !gs.alarm_active <- false diff --git a/infer/src/backend/SymOp.mli b/infer/src/backend/SymOp.mli new file mode 100644 index 000000000..5d70fa187 --- /dev/null +++ b/infer/src/backend/SymOp.mli @@ -0,0 +1,71 @@ +(* + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Symbolic Operations and Failures: the units in which analysis work is measured *) + +open! Utils + +(** Internal state of the module *) +type t + +(** if the wallclock alarm has expired, raise a timeout exception *) +val check_wallclock_alarm : unit -> unit + +(** Return the time remaining before the wallclock alarm expires *) +val get_remaining_wallclock_time : unit -> float + +(** Timeout in seconds for each function *) +val get_timeout_seconds : unit -> float + +(** Return the total number of symop's since the beginning *) +val get_total : unit -> int + +(** Count one symop *) +val pay : unit -> unit + +(** Reset the total number of symop's *) +val reset_total : unit -> unit + +(** Restore the old state. *) +val restore_state : t -> unit + +(** Return the old state, and revert the current state to the initial one. + If keep_symop_total is true, share the total counter. *) +val save_state : keep_symop_total:bool -> t + +(** Reset the counter and activate the alarm *) +val set_alarm : unit -> unit + +(** Set the wallclock alarm checked at every pay() *) +val set_wallclock_alarm : float -> unit + +(** set the handler for the wallclock timeout *) +val set_wallclock_timeout_handler : (unit -> unit) -> unit + +(** De-activate the alarm *) +val unset_alarm : unit -> unit + +(** Unset the wallclock alarm checked at every pay() *) +val unset_wallclock_alarm : unit -> unit + + +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 Analysis_failure_exe of failure_kind + +(** check that the exception is not a timeout exception *) +val exn_not_failure : exn -> bool + +val pp_failure_kind : Format.formatter -> failure_kind -> unit diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index e2b742669..165d1f144 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -362,6 +362,29 @@ let default_failure_name = "ASSERTION_FAILURE" let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" +(** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *) +let initial_analysis_time = Unix.time () + +let symops_timeout, seconds_timeout = + let default_symops_timeout = 333 in + let default_seconds_timeout = 10.0 in + let long_symops_timeout = 1000 in + let long_seconds_timeout = 30.0 in + if analyze_models then + (* use longer timeouts when analyzing models *) + long_symops_timeout, long_seconds_timeout + else + default_symops_timeout, default_seconds_timeout + +(** number of symops to multiply by the number of iterations, after which there is a timeout *) +let symops_per_iteration = ref symops_timeout + +(** number of seconds to multiply by the number of iterations, after which there is a timeout *) +let seconds_per_iteration = ref seconds_timeout + +(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *) +let iterations = ref 1 + (** experimental: dynamic dispatch for interface calls only in Java. off by default because of the cost *) let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH" diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 9c8f50382..337fd8a32 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -513,7 +513,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_failure exn -> assert false in + with exn when SymOp.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 @@ -877,7 +877,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_failure exn -> + with exn when SymOp.exn_not_failure exn -> () let pp_dotty_prop fmt (prop, cycle) = @@ -890,7 +890,7 @@ let pp_dotty_prop fmt (prop, cycle) = let dotty_prop_to_str prop cycle = try Some (pp_to_string pp_dotty_prop (prop, cycle)) - with exn when exn_not_failure exn -> None + with exn when SymOp.exn_not_failure exn -> None (* create a dotty file with a single proposition *) let dotty_prop_to_dotty_file fname prop cycle = @@ -899,7 +899,7 @@ let dotty_prop_to_dotty_file fname prop cycle = let fmt_dot = Format.formatter_of_out_channel out_dot in pp_dotty_prop fmt_dot (prop, cycle); close_out out_dot - with exn when exn_not_failure exn -> + with exn when SymOp.exn_not_failure exn -> () (* this is used only to print a list of prop parsed with the external parser. Basically deprecated.*) @@ -916,7 +916,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_failure exn -> + with exn when SymOp.exn_not_failure exn -> () (********** START of Print interprocedural cfgs in dotty format *) @@ -1058,7 +1058,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_failure exn -> + with exn when SymOp.exn_not_failure exn -> () (**********************************************************************) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 5a6d7daa2..8f6ab03ed 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -511,7 +511,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (try let t2 = Tenv.expand_type tenv _t2 in Sil.typ_equal t1 t2 - with exn when exn_not_failure exn -> false) + with exn when SymOp.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 @@ -948,7 +948,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_failure exn -> Localise.no_desc) + with exn when SymOp.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 c0f49ec1b..93fcda3c1 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -252,7 +252,7 @@ let recognize_exception exn = | Return_value_ignored (desc, ml_loc) -> (Localise.return_value_ignored, desc, Some ml_loc, Exn_user, Medium, None, Nocat) - | Analysis_failure_exe _ -> + | SymOp.Analysis_failure_exe _ -> (Localise.from_string "Failure_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat) | Skip_function desc -> diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index c8efb3cc1..419f2c2ec 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -60,7 +60,7 @@ let arg_desc = "use file for the err channel" ; "-iterations", - Arg.Int set_iterations, + Arg.Set_int Config.iterations, Some "n", "set the max number of operations for each function, \ expressed as a multiple of symbolic operations (default n=1)" @@ -194,7 +194,7 @@ let arg_desc = "Add buckets to issue descriptions, useful when developing infer" ; "-seconds_per_iteration", - Arg.Set_float seconds_per_iteration, + Arg.Set_float Config.seconds_per_iteration, Some "n", "set the number of seconds per iteration (default n=30)" ; @@ -204,10 +204,10 @@ let arg_desc = "use the multirange subtyping domain" ; "-symops_per_iteration", - Arg.Set_int symops_per_iteration, + Arg.Set_int Config.symops_per_iteration, Some "n", "set the number of symbolic operations per iteration (default n=" - ^ (string_of_int !symops_per_iteration) ^ ")" + ^ (string_of_int !Config.symops_per_iteration) ^ ")" ; "-tracing", Arg.Unit (fun () -> Config.report_runtime_exceptions := true), diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 045c39c9d..990d50b99 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -388,7 +388,7 @@ let summary_values top_proc_set summary = logscale (c1 * in_calls + c2 * out_calls) in let pp_failure failure = - pp_to_string pp_failure_kind failure in + pp_to_string SymOp.pp_failure_kind failure in { vname = Procname.to_string proc_name; diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 35a12db2f..2ac94a460 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -947,7 +947,7 @@ let perform_analysis_phase 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 (Analysis_failure_exe (FKrecursion_timeout recursion_level)) + raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level)) end in let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) = @@ -1330,7 +1330,7 @@ let perform_transition exe_env tenv proc_name = let start_node = Cfg.Procdesc.get_start_node pdesc in f start_node | None -> () - with exn when exn_not_failure exn -> () in + with exn when SymOp.exn_not_failure exn -> () in apply_start_node (do_before_node 0); try Config.allowleak := true; @@ -1338,7 +1338,7 @@ let perform_transition exe_env tenv proc_name = Config.allowleak := allowleak; apply_start_node do_after_node; res - with exn when exn_not_failure exn -> + with exn when SymOp.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; diff --git a/infer/src/backend/io_infer.ml b/infer/src/backend/io_infer.ml index f9f3d9b08..3bc1494c1 100644 --- a/infer/src/backend/io_infer.ml +++ b/infer/src/backend/io_infer.ml @@ -150,7 +150,7 @@ struct let modified_during_analysis path = let fname = get_full_fname path in if DB.file_exists fname then - DB.file_modified_time fname >= initial_analysis_time + DB.file_modified_time fname >= Config.initial_analysis_time else false (** Close an Html file *) diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index eef93cb0f..e1b5ef6de 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -210,12 +210,12 @@ let log_progress_timeout_event failure_kind = if !Config.developer_mode then begin match failure_kind with - | FKtimeout -> + | SymOp.FKtimeout -> log_progress_simple "T" - | FKsymops_timeout _ -> + | SymOp.FKsymops_timeout _ -> log_progress_simple "S" - | FKrecursion_timeout _ -> + | SymOp.FKrecursion_timeout _ -> log_progress_simple "R" - | FKcrash _ -> + | SymOp.FKcrash _ -> log_progress_simple "C" end diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli index 3eaf93cce..684d41d55 100644 --- a/infer/src/backend/logging.mli +++ b/infer/src/backend/logging.mli @@ -151,4 +151,4 @@ val log_progress_file : unit -> unit val log_progress_procedure : unit -> unit (** Progress bar: log a timeout event if in developer mode. *) -val log_progress_timeout_event : failure_kind -> unit +val log_progress_timeout_event : SymOp.failure_kind -> unit diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index bc0b4ce7b..293b429e0 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -191,7 +191,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc raise exn else match exn with - | Analysis_failure_exe kind -> + | 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 kind diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index b1aa40d3e..f1bae8ffd 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -318,7 +318,7 @@ end = struct | Some node -> pos_opt <> None && filter node | None -> false - with exn when exn_not_failure exn -> false in + with exn when SymOp.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 0e2268371..0cc5344fb 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -51,7 +51,7 @@ struct 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 + with exn when SymOp.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 3f9f9fbc4..372a4a59a 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 exn_not_failure exn -> (L.d_decrease_indent 1; raise exn) + with exn when SymOp.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)) @@ -1853,7 +1853,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_failure exn -> + with exn when SymOp.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 232cd5129..340ffc31b 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -292,7 +292,8 @@ type call_stats = CallStats.t (** Execution statistics *) type stats = { stats_time: float; (** Analysis time for the procedure *) - stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *) + stats_failure: + SymOp.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 *) @@ -351,7 +352,7 @@ let pp_time whole_seconds fmt t = else F.fprintf fmt "%f s" t let pp_failure_kind_opt fmt failure_kind_opt = match failure_kind_opt with - | Some failure_kind -> pp_failure_kind fmt failure_kind + | Some failure_kind -> SymOp.pp_failure_kind fmt failure_kind | None -> F.fprintf fmt "NONE" let pp_stats err_log whole_seconds fmt stats = diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 9389ac604..a7398fbd7 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -102,7 +102,8 @@ end (** Execution statistics *) type stats = { stats_time: float; (** Analysis time for the procedure *) - stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *) + stats_failure: + SymOp.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 4920c0d43..78a7e3333 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -269,7 +269,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_failure exn -> pre in + let pre' = try abstract_fun tenv pre with exn when SymOp.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 0b7fe2e38..a8275bdac 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1212,7 +1212,7 @@ and instrs ?(mask_errors=false) 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 tenv pdesc instr p path - with exn when exn_not_failure exn && mask_errors -> + with exn when SymOp.exn_not_failure exn && mask_errors -> let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in let loc = (match ml_source with | Some ml_loc -> "at " ^ (L.ml_loc_to_string ml_loc) @@ -1409,7 +1409,7 @@ and check_variadic_sentinel let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in try instrs tenv pdesc [letderef] result - with e when exn_not_failure e -> + 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 = diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 2d12bd2d9..fba02fb07 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -427,7 +427,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_failure exn -> se1 (* let postcondition override *) + | exn when SymOp.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 *) @@ -504,7 +504,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_failure exn -> + with exn when SymOp.exn_not_failure exn -> L.d_str "cannot star "; Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2; L.d_ln (); @@ -537,7 +537,7 @@ let sigma_star_typ | _ -> star sg1 typings2' end in try star sigma1 typings2 - with exn when exn_not_failure exn -> + with exn when SymOp.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/timeout.ml b/infer/src/backend/timeout.ml index 0b25eacbf..f0e7504d7 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -81,7 +81,7 @@ let set_status status = let timeout_action _ = unset_alarm (); - raise (Analysis_failure_exe (FKtimeout)) + raise (SymOp.Analysis_failure_exe (FKtimeout)) let () = begin match Config.os_type with @@ -111,7 +111,7 @@ let resume_previous_timeout () = let exe_timeout f x = let suspend_existing_timeout_and_start_new_one () = suspend_existing_timeout ~keep_symop_total:true; - set_alarm (get_timeout_seconds ()); + set_alarm (SymOp.get_timeout_seconds ()); SymOp.set_alarm () in try suspend_existing_timeout_and_start_new_one (); @@ -119,10 +119,10 @@ let exe_timeout f x = resume_previous_timeout (); None with - | Analysis_failure_exe kind -> + | SymOp.Analysis_failure_exe kind -> resume_previous_timeout (); L.log_progress_timeout_event kind; - Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_failure_kind kind; + Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind; Some kind | exe -> resume_previous_timeout (); diff --git a/infer/src/backend/timeout.mli b/infer/src/backend/timeout.mli index 1421002b1..756d84919 100644 --- a/infer/src/backend/timeout.mli +++ b/infer/src/backend/timeout.mli @@ -12,7 +12,7 @@ open! Utils (** Handle timeout events *) (** Execute the function up to a given timeout. *) -val exe_timeout : ('a -> unit) -> 'a -> failure_kind option +val exe_timeout : ('a -> unit) -> 'a -> SymOp.failure_kind option (** Resume a previously suspended timeout. *) val resume_previous_timeout : unit -> unit diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 7c966dd67..aa8d43328 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -16,12 +16,6 @@ module F = Format functions and builtin equality. Use IList instead. *) module List = struct end -(** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *) -let initial_analysis_time = Unix.time () - -(** precise time of day at the start of the analysis *) -let initial_timeofday = Unix.gettimeofday () - (** {2 Generic Utility Functions} *) (** Compare police: generic compare disabled. *) @@ -232,175 +226,14 @@ let pp_current_time f () = let tm = Unix.localtime (Unix.time ()) in F.fprintf f "%02d/%02d/%4d %02d:%02d" tm.Unix.tm_mday tm.Unix.tm_mon (tm.Unix.tm_year + 1900) tm.Unix.tm_hour tm.Unix.tm_min +(** precise time of day at the start of the analysis *) +let initial_timeofday = Unix.gettimeofday () + (** Print the time in seconds elapsed since the beginning of the execution of the current command. *) let pp_elapsed_time fmt () = let elapsed = Unix.gettimeofday () -. initial_timeofday in Format.fprintf fmt "%f" elapsed -(** {2 SymOp and Failures: units of symbolic execution} *) - -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 *) - -(** failure that prevented analysis from finishing *) -exception Analysis_failure_exe of failure_kind - -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 - let default_seconds_timeout = 10.0 in - let long_symops_timeout = 1000 in - let long_seconds_timeout = 30.0 in - if Config.analyze_models then - (* use longer timeouts when analyzing models *) - long_symops_timeout, long_seconds_timeout - else - default_symops_timeout, default_seconds_timeout - -(** number of symops to multiply by the number of iterations, after which there is a timeout *) -let symops_per_iteration = ref symops_timeout - -(** number of seconds to multiply by the number of iterations, after which there is a timeout *) -let seconds_per_iteration = ref seconds_timeout - -(** Timeout in seconds for each function *) -let timeout_seconds = ref !seconds_per_iteration - -(** Timeout in SymOps *) -let timeout_symops = ref !symops_per_iteration - -(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *) -let set_iterations n = - timeout_symops := !symops_per_iteration * n; - timeout_seconds := !seconds_per_iteration *. (float_of_int n) - -let get_timeout_seconds () = !timeout_seconds - -(** Count the number of symbolic operations *) -module SymOp = struct - - (** Internal state of the module *) - type t = - { - (** Only throw timeout exception when alarm is active *) - mutable alarm_active : bool; - - (** last wallclock set by an alarm, if any *) - mutable last_wallclock : float option; - - (** Number of symop's *) - mutable symop_count : int; - - (** Counter for the total number of symop's. - The new state created when save_state is called shares this counter - if keep_symop_total is true. Otherwise, a new counter is created. *) - symop_total : int ref; - } - - let initial () : t = - { - alarm_active = false; - last_wallclock = None; - symop_count = 0; - symop_total = ref 0; - } - - (** Global State *) - let gs : t ref = ref (initial ()) - - (** Restore the old state. *) - let restore_state state = - gs := state - - (** Return the old state, and revert the current state to the initial one. - If keep_symop_total is true, share the total counter. *) - let save_state ~keep_symop_total = - let old_state = !gs in - let new_state = - let st = initial () in - if keep_symop_total - then - { st with symop_total = old_state.symop_total } - else - st in - gs := new_state; - old_state - - (** handler for the wallclock timeout *) - let wallclock_timeout_handler = ref None - - (** set the handler for the wallclock timeout *) - let set_wallclock_timeout_handler handler = - wallclock_timeout_handler := Some handler - - (** Set the wallclock alarm checked at every pay() *) - let set_wallclock_alarm nsecs = - !gs.last_wallclock <- Some (Unix.gettimeofday () +. nsecs) - - (** Unset the wallclock alarm checked at every pay() *) - let unset_wallclock_alarm () = - !gs.last_wallclock <- None - - (** if the wallclock alarm has expired, raise a timeout exception *) - let check_wallclock_alarm () = - match !gs.last_wallclock, !wallclock_timeout_handler with - | Some alarm_time, Some handler when Unix.gettimeofday () >= alarm_time -> - unset_wallclock_alarm (); - handler () - | _ -> () - - (** Return the time remaining before the wallclock alarm expires *) - let get_remaining_wallclock_time () = - match !gs.last_wallclock with - | Some alarm_time -> - max 0.0 (alarm_time -. Unix.gettimeofday ()) - | None -> - 0.0 - - (** Return the total number of symop's since the beginning *) - let get_total () = - !(!gs.symop_total) - - (** Reset the total number of symop's *) - let reset_total () = - !gs.symop_total := 0 - - (** Count one symop *) - let pay () = - !gs.symop_count <- !gs.symop_count + 1; - !gs.symop_total := !(!gs.symop_total) + 1; - if !gs.symop_count > !timeout_symops && - !gs.alarm_active - then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count)); - check_wallclock_alarm () - - (** Reset the counter *) - let reset_count () = - !gs.symop_count <- 0 - - (** Reset the counter and activate the alarm *) - let set_alarm () = - reset_count (); - !gs.alarm_active <- true - - (** De-activate the alarm *) - let unset_alarm () = - !gs.alarm_active <- false -end - (** Check if the lhs is a substring of the rhs. *) let string_is_prefix s1 s2 = String.length s1 <= String.length s2 && diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 726d32881..8c6a4d033 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -142,80 +142,6 @@ 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 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 - -(** number of symops to multiply by the number of iterations, after which there is a timeout *) -val symops_per_iteration : int ref - -(** number of seconds to multiply by the number of iterations, after which there is a timeout *) -val seconds_per_iteration : float ref - -(** Timeout in seconds for each function *) -val get_timeout_seconds : unit -> float - -(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *) -val set_iterations : int -> unit - -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 Analysis_failure_exe of failure_kind - -(** check that the exception is not a timeout exception *) -val exn_not_failure : exn -> bool - -val pp_failure_kind : Format.formatter -> failure_kind -> unit - -(** Count the number of symbolic operations *) -module SymOp : sig - (** Internal state of the module *) - type t - - (** if the wallclock alarm has expired, raise a timeout exception *) - val check_wallclock_alarm : unit -> unit - - (** Return the time remaining before the wallclock alarm expires *) - val get_remaining_wallclock_time : unit -> float - - (** Return the total number of symop's since the beginning *) - val get_total : unit -> int - - (** Count one symop *) - val pay : unit -> unit - - (** Reset the total number of symop's *) - val reset_total : unit -> unit - - (** Restore the old state. *) - val restore_state : t -> unit - - (** Return the old state, and revert the current state to the initial one. - If keep_symop_total is true, share the total counter. *) - val save_state : keep_symop_total:bool -> t - - (** Reset the counter and activate the alarm *) - val set_alarm : unit -> unit - - (** Set the wallclock alarm checked at every pay() *) - val set_wallclock_alarm : float -> unit - - (** set the handler for the wallclock timeout *) - val set_wallclock_timeout_handler : (unit -> unit) -> unit - - (** De-activate the alarm *) - val unset_alarm : unit -> unit - - (** Unset the wallclock alarm checked at every pay() *) - val unset_wallclock_alarm : unit -> unit -end - module Arg : sig include module type of Arg with type spec = Arg.spec