diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index 6de00ee0f..6ca8bb66a 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -255,7 +255,7 @@ let filter_max exe_env filter set priority_set = (** Main algorithm responsible for driving the analysis of an Exe_env (set of procedures). The algorithm computes dependencies between procedures, propagates results, and handles fixpoints in the call graph. *) -let main_algorithm exe_env analyze_proc filter_out process_result : unit = +let main_algorithm exe_env analyze_proc process_result : unit = let call_graph = Exe_env.get_cg exe_env in let filter_initial (pname, _) = let summary = Specs.get_summary_unsafe "main_algorithm" pname in @@ -286,14 +286,8 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit = (Specs.pp_summary pe_text whole_seconds) (Specs.get_summary_unsafe "main_algorithm" pname) end; - if filter_out exe_env pname - then - post_process_procs exe_env [pname] - else - begin - Specs.update_dependency_map pname; - process_result exe_env elem (analyze_proc exe_env pname); - end in + Specs.update_dependency_map pname; + process_result exe_env elem (analyze_proc exe_env pname) in while not (WeightedPnameSet.is_empty !G.wpnames_todo) do begin if !trace then begin @@ -318,16 +312,13 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary type process_result = Exe_env.t -> WeightedPname.t -> Specs.summary -> unit -type filter_out = Exe_env.t -> Procname.t -> bool - (** Execute [analyze_proc] respecting dependencies between procedures, - and apply [process_result] to the result of the analysis. - If [filter_out] returns true, don't analyze the procedure. *) + and apply [process_result] to the result of the analysis. *) let interprocedural_algorithm (exe_env: Exe_env.t) (_analyze_proc: analyze_proc) (_process_result: process_result) - (filter_out: filter_out) : unit = + : 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; @@ -357,4 +348,4 @@ let interprocedural_algorithm let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in Reporting.log_error pname exn'; post_process_procs exe_env [pname] in - main_algorithm exe_env analyze_proc filter_out process_result + main_algorithm exe_env analyze_proc process_result diff --git a/infer/src/backend/fork.mli b/infer/src/backend/fork.mli index bd60c35c1..53b2d9a42 100644 --- a/infer/src/backend/fork.mli +++ b/infer/src/backend/fork.mli @@ -29,9 +29,6 @@ type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary type process_result = Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit -type filter_out = Exe_env.t -> Procname.t -> bool - (** Execute [analyze_proc] respecting dependencies between procedures, - and apply [process_result] to the result of the analysis. - If [filter_out] returns true, don't analyze the procedure. *) -val interprocedural_algorithm : Exe_env.t -> analyze_proc -> process_result -> filter_out -> unit + and apply [process_result] to the result of the analysis. *) +val interprocedural_algorithm : Exe_env.t -> analyze_proc -> process_result -> unit diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index ebcf9cacb..cb439d3f6 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -391,7 +391,6 @@ module Simulator = struct (** Simulate the analysis only *) let timestamp = max 1 (prev_summary.Specs.timestamp) in { prev_summary with Specs.timestamp = timestamp } - let filter_out _ _ = false end let analyze exe_env = @@ -412,7 +411,6 @@ let analyze exe_env = exe_env Simulator.analyze_proc Simulator.process_result - Simulator.filter_out end else (* full analysis *) begin diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 37acaaeed..af5a21a6e 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1179,25 +1179,54 @@ let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary let procs_done = Fork.procs_become_done call_graph proc_name in Fork.post_process_procs exe_env procs_done -let filter_out_ondemand exe_env proc_name = - let to_analyze = - if !Config.ondemand_enabled then - try - let cfg = Exe_env.get_cfg exe_env proc_name in - match Cfg.Procdesc.find_from_name cfg proc_name with - | Some pdesc -> - let reactive_changed = - if !Config.reactive_mode - then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed - else true in +let analyze_proc_for_ondemand exe_env proc_name = + let saved_footprint = !Config.footprint in + Config.footprint := true; + let summaryfp = analyze_proc exe_env proc_name in + Specs.add_summary proc_name summaryfp; + let cg = Cg.create () in + Cg.add_defined_node cg proc_name; + perform_transition exe_env cg proc_name; + Config.footprint := false; + let summaryre = analyze_proc exe_env proc_name in + Specs.add_summary proc_name summaryre; + Config.footprint := saved_footprint + +let interprocedural_algorithm_ondemand exe_env : unit = + let call_graph = Exe_env.get_cg exe_env in + let filter_initial proc_name = + let summary = Specs.get_summary_unsafe "main_algorithm" proc_name in + Specs.get_timestamp summary = 0 in + let procs_to_analyze = + IList.filter filter_initial (Cg.get_defined_nodes call_graph) in + let to_analyze proc_name = + try + let cfg = Exe_env.get_cfg exe_env proc_name in + match Cfg.Procdesc.find_from_name cfg proc_name with + | Some pdesc -> + let reactive_changed = + if !Config.reactive_mode + then (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.changed + else true in + if reactive_changed && (* in reactive mode, only analyze changed procedures *) Ondemand.procedure_should_be_analyzed pdesc proc_name - | None -> - true - with Not_found -> true - else - true in - not to_analyze + then + Some pdesc + else + None + | None -> + None + with Not_found -> + None in + let process_one_proc proc_name = + match to_analyze proc_name with + | Some pdesc -> + Ondemand.do_analysis ~propagate_exceptions:false pdesc proc_name + | None -> + () in + IList.iter process_one_proc procs_to_analyze + (** Perform the analysis of an exe_env *) let do_analysis exe_env = @@ -1238,24 +1267,18 @@ let do_analysis exe_env = let callee_cfg = Exe_env.get_cfg exe_env proc_name in Cfg.Procdesc.find_from_name callee_cfg proc_name in let analyze_ondemand proc_name = - let saved_footprint = !Config.footprint in - Config.footprint := true; - let summaryfp = analyze_proc exe_env proc_name in - Specs.add_summary proc_name summaryfp; - let cg = Cg.create () in - Cg.add_defined_node cg proc_name; - perform_transition exe_env cg proc_name; - Config.footprint := false; - let summaryre = analyze_proc exe_env proc_name in - Specs.add_summary proc_name summaryre; - Config.footprint := saved_footprint; - () in + analyze_proc_for_ondemand exe_env proc_name in { Ondemand.analyze_ondemand; get_proc_desc; } in - Ondemand.set_callbacks callbacks; - Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out_ondemand; - Ondemand.unset_callbacks () - + if !Config.ondemand_enabled + then + begin + Ondemand.set_callbacks callbacks; + interprocedural_algorithm_ondemand exe_env; + Ondemand.unset_callbacks () + end + else + Fork.interprocedural_algorithm exe_env analyze_proc process_result let visited_and_total_nodes cfg = let all_nodes = diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index dd70186a5..5db1dffc9 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -98,7 +98,8 @@ type global_state = } let save_global_state () = - Timeout.suspend_existing_timeout (); + Timeout.suspend_existing_timeout + ~keep_symop_total:false; (* use a new global counter for the callee *) { abs_val = !Config.abs_val; abstraction_rules = Abs.get_current_rules (); @@ -121,7 +122,7 @@ let restore_global_state st = State.restore_state st.symexec_state; Timeout.resume_previous_timeout () -let do_analysis curr_pdesc callee_pname = +let do_analysis ~propagate_exceptions curr_pdesc callee_pname = let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let really_do_analysis analyze_proc = @@ -159,20 +160,42 @@ let do_analysis curr_pdesc callee_pname = Specs.add_summary callee_pname summary'; Checkers.ST.store_summary callee_pname in + let log_error_and_continue exn kind = + Reporting.log_error callee_pname exn; + let prev_summary = Specs.get_summary_unsafe "Ondemand.do_analysis" callee_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 + let new_summary = + { prev_summary with Specs.stats; payload; timestamp; } in + Specs.add_summary callee_pname new_summary in + let old_state = save_global_state () in preprocess (); try analyze_proc callee_pname; postprocess (); restore_global_state old_state; - with e -> + with exn -> L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@." Procname.pp callee_pname - (Printexc.to_string e) + (Printexc.to_string exn) (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000)) (Printexc.get_backtrace ()); restore_global_state old_state; - raise e in + if propagate_exceptions + then + raise exn + else + match exn with + | 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 + | _ -> + (* this happens with assert false or some other unrecognized exception *) + log_error_and_continue exn (FKcrash (Printexc.to_string exn)) in match !callbacks_ref with | Some callbacks diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index 0502ee85f..f862210be 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -25,7 +25,7 @@ type callbacks = (** do_analysis curr_pdesc proc_name performs an on-demand analysis of proc_name triggered during the analysis of curr_pname. *) -val do_analysis : Cfg.Procdesc.t -> Procname.t -> unit +val do_analysis : propagate_exceptions:bool -> Cfg.Procdesc.t -> Procname.t -> unit val one_cluster_per_procedure : unit -> bool diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index faf72534a..5ea49b522 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1092,7 +1092,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in let exec_one_pname pname = if !Config.ondemand_enabled then - Ondemand.do_analysis pdesc pname; + Ondemand.do_analysis ~propagate_exceptions:true pdesc pname; let exec_skip_call ret_type = skip_call norm_prop path pname loc ret_ids (Some ret_type) url_handled_args in match Specs.get_summary pname with @@ -1118,7 +1118,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path | resolved_pname :: _ -> resolved_pname | [] -> fn in if !Config.ondemand_enabled then - Ondemand.do_analysis pdesc resolved_pname; + Ondemand.do_analysis ~propagate_exceptions:true pdesc resolved_pname; let callee_pdesc_opt = Cfg.Procdesc.find_from_name cfg resolved_pname in let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in let sentinel_result = diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index 6a94be9c5..1dbb31a9d 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -65,9 +65,9 @@ let get_seconds_remaining () = | Config.Win32 -> SymOp.get_remaining_wallclock_time () -let get_current_status () = +let get_current_status ~keep_symop_total = let seconds_remaining = get_seconds_remaining () in - let symop_state = SymOp.save_state () in + let symop_state = SymOp.save_state ~keep_symop_total in { seconds_remaining; symop_state; @@ -97,8 +97,8 @@ let unwind () = SymOp.unset_alarm (); GlobalState.pop () -let suspend_existing_timeout () = - let current_status = get_current_status () in +let suspend_existing_timeout ~keep_symop_total = + let current_status = get_current_status ~keep_symop_total in unset_alarm (); GlobalState.push current_status @@ -108,7 +108,7 @@ let resume_previous_timeout () = let exe_timeout f x = let suspend_existing_timeout_and_start_new_one () = - suspend_existing_timeout (); + suspend_existing_timeout ~keep_symop_total:true; set_alarm (get_timeout_seconds ()); SymOp.set_alarm () in try diff --git a/infer/src/backend/timeout.mli b/infer/src/backend/timeout.mli index f5305dcdd..45b3dfdf5 100644 --- a/infer/src/backend/timeout.mli +++ b/infer/src/backend/timeout.mli @@ -16,4 +16,4 @@ val exe_timeout : ('a -> unit) -> 'a -> failure_kind option val resume_previous_timeout : unit -> unit (** Suspend the current timeout. It must be resumed later. *) -val suspend_existing_timeout : unit -> unit +val suspend_existing_timeout : keep_symop_total:bool -> unit diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 2798424a6..3be6778cf 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -320,11 +320,10 @@ module SymOp = struct (** Number of symop's *) mutable symop_count : int; - (** Total number of symop's since the beginning *) - mutable symop_total : int; - - (** Time in the beginning *) - mutable timer : float; + (** 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 = @@ -332,8 +331,7 @@ module SymOp = struct alarm_active = false; last_wallclock = None; symop_count = 0; - symop_total = 0; - timer = Unix.gettimeofday (); + symop_total = ref 0; } (** Global State *) @@ -343,10 +341,18 @@ module SymOp = struct let restore_state state = gs := state - (** Return the old state, and revert the current state to the initial one. *) - let save_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 - gs := initial (); + 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 *) @@ -382,42 +388,33 @@ module SymOp = struct (** Return the total number of symop's since the beginning *) let get_total () = - !gs.symop_total + !(!gs.symop_total) (** Reset the total number of symop's *) let reset_total () = - !gs.symop_total <- 0 + !gs.symop_total := 0 (** Count one symop *) let pay () = !gs.symop_count <- !gs.symop_count + 1; - !gs.symop_total <- !gs.symop_total + 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 counters *) - let reset () = - !gs.symop_count <- 0; - !gs.timer <- Unix.gettimeofday () + (** Reset the counter *) + let reset_count () = + !gs.symop_count <- 0 (** Reset the counter and activate the alarm *) let set_alarm () = - reset (); + reset_count (); !gs.alarm_active <- true (** De-activate the alarm *) let unset_alarm () = !gs.alarm_active <- false - - let report_stats f symops elapsed = - F.fprintf f "SymOp stats -- symops:%d time:%f symops/sec:%f" symops elapsed ((float_of_int symops) /. elapsed) - - (** Report the stats since the last reset *) - let report f () = - let elapsed = Unix.gettimeofday () -. !gs.timer in - report_stats f !gs.symop_count elapsed end (** Check if the lhs is a substring of the rhs. *) diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index b127ae2f8..890cebf47 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -199,17 +199,15 @@ module SymOp : sig (** Count one symop *) val pay : unit -> unit - (** Report the stats since the last reset *) - val report : Format.formatter -> 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. *) - val save_state : unit -> t + (** 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 diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index 1556aee1f..f66df05db 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/infer/src/checkers/performanceCritical.ml @@ -156,7 +156,7 @@ let collect_calls tenv caller_pdesc checked_pnames call_summary (pname, _) = if Procname.Set.mem pname !checked_pnames then call_summary else begin - Ondemand.do_analysis caller_pdesc pname; + Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc pname; checked_pnames := Procname.Set.add pname !checked_pnames; let call_loc = lookup_location pname in let updated_expensive_calls = diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 12586f9fd..7ea81ecba 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -557,7 +557,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags) when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None -> if !Config.ondemand_enabled then - Ondemand.do_analysis curr_pdesc callee_pname; + Ondemand.do_analysis ~propagate_exceptions:true curr_pdesc callee_pname; let callee_attributes = match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with | Some proc_attributes -> proc_attributes diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index 30d0f4c48..f1fdff859 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -85,7 +85,6 @@ let init_global_state source_file = DB.current_source := source_file; DB.Results_dir.init (); Ident.NameGenerator.reset (); - SymOp.reset_total (); JContext.reset_exn_node_table (); let nLOC = FileLOC.file_get_loc (DB.source_file_to_string source_file) in Config.nLOC := nLOC diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index 02796d95c..633d3d234 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -41,7 +41,6 @@ let init_global_state source_filename = end; DB.Results_dir.init (); Ident.NameGenerator.reset (); - SymOp.reset_total (); Config.nLOC := FileLOC.file_get_loc source_filename let store_icfg tenv cg cfg =