diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index d084f82d2..5c430cc83 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -217,7 +217,11 @@ let iterate_callbacks store_summary call_graph exe_env = let reset_summary proc_name = let attributes_opt = Specs.proc_resolve_attributes proc_name in - Specs.reset_summary call_graph proc_name attributes_opt in + let should_reset = + not !Config.ondemand_enabled || + Specs.get_summary proc_name = None in + if should_reset + then Specs.reset_summary call_graph proc_name attributes_opt in (* Make sure summaries exists. *) diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 519e08852..79b431d1e 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -170,6 +170,9 @@ let eradicate = ref false (** should the checkers be run? *) let checkers_enabled () = not !eradicate +(** flag to activate ondemand mode. *) +let ondemand_enabled = ref false + (** Flag for footprint discovery mode *) let footprint = ref true diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index e6534d68d..ca7fb3b78 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -780,7 +780,7 @@ let compute_files_changed_map _exe_env (source_dirs : DB.source_dir list) exclud let exe_env_from_cluster cluster = let _exe_env = let active_procs_opt = - if Ondemand.enabled () + if !Config.ondemand_enabled then None else Some (cluster_to_active_procs cluster) in Exe_env.create active_procs_opt in @@ -871,7 +871,7 @@ let () = match !cluster_cmdline with | None -> if !Config.curr_language = Config.C_CPP && - not (Ondemand.enabled ()) then + not !Config.ondemand_enabled then Objc_preanal.do_objc_preanalysis (); L.stdout "Starting analysis (Infer version %s)@." Version.versionString; | Some clname -> L.stdout "Cluster %s@." clname in @@ -905,7 +905,7 @@ let () = L.err "Found %d source files in %s@." (list_length source_dirs) !Config.results_dir; let clusters = - if Ondemand.enabled () + if !Config.ondemand_enabled then compute_ondemand_clusters source_dirs else diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index eb2952574..ac06fb3c5 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -15,7 +15,7 @@ open Utils let trace = false -let enabled () = false +let () = Config.ondemand_enabled := Config.from_env_variable "INFER_ONDEMAND" let across_files () = true @@ -33,7 +33,34 @@ let unset_analyze_prop () = let nesting = ref 0 -let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name = +let procedure_should_be_analyzed curr_pdesc proc_name = + match AttributesTable.load_attributes proc_name with + | Some proc_attributes -> + let currently_analyzed = + Specs.summary_exists proc_name && + Specs.is_active proc_name in + let already_analyzed = match Specs.get_summary proc_name with + | Some summary -> + Specs.get_timestamp summary > 0 + | None -> + false in + (* The procedure to be analyzed is in the same file as the current one. *) + let same_file proc_attributes = + (Cfg.Procdesc.get_loc curr_pdesc).Location.file + = + proc_attributes.ProcAttributes.loc.Location.file in + + !Config.ondemand_enabled && + proc_attributes.ProcAttributes.is_defined && (* we have the implementation *) + not currently_analyzed && (* avoid infinite loops *) + not already_analyzed && (* avoid re-analysis of the same procedure *) + (across_files () (* whether to push the analysis into other files *) + || same_file proc_attributes) + | None -> + false + +let do_analysis (get_proc_desc : get_proc_desc) curr_pdesc proc_name = + let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let really_do_analysis analyze_proc proc_desc = if trace then L.stderr "[%d] really_do_analysis %a -> %a@." @@ -73,31 +100,9 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name = (Printexc.get_backtrace ()); raise e in - let currently_analyzed = - Specs.summary_exists proc_name && - Specs.is_active proc_name in - let already_analyzed = match Specs.get_summary proc_name with - | Some summary -> - Specs.get_timestamp summary > 0 - | None -> - false in - (* The procedure to be analyzed is in the same file as the current one. *) - let same_file proc_attributes = - match get_proc_desc curr_pname with - | Some curr_pdesc -> - (Cfg.Procdesc.get_loc curr_pdesc).Location.file - = - proc_attributes.ProcAttributes.loc.Location.file - | None -> false in - - match !analyze_proc_fun, AttributesTable.load_attributes proc_name with - | Some analyze_proc, Some proc_attributes - when enabled () && - proc_attributes.ProcAttributes.is_defined && (* we have the implementation *) - not currently_analyzed && (* avoid infinite loops *) - not already_analyzed && (* avoid re-analysis of the same procedure *) - (across_files () (* whether to push the analysis into other files *) - || same_file proc_attributes) -> + match !analyze_proc_fun with + | Some analyze_proc + when procedure_should_be_analyzed curr_pdesc proc_name -> begin match get_proc_desc proc_name with | Some proc_desc -> diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index 7df3fcc35..76842d509 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -13,13 +13,13 @@ type analyze_proc = Procname.t -> unit type get_proc_desc = Procname.t -> Cfg.Procdesc.t option -(** do_analysis get_proc_desc curr_pname proc_name +(** do_analysis get_proc_desc curr_descproc_name performs an on-demand analysis of proc_name - triggered during the analysis of curr_pname. *) -val do_analysis : get_proc_desc -> Procname.t -> Procname.t -> unit + triggered during the analysis of curr_pdesc. *) +val do_analysis : get_proc_desc -> Cfg.Procdesc.t -> Procname.t -> unit -(** Check if on-demand is currently active. *) -val enabled : unit -> bool +(** Check if the procedure called by the current pdesc needs to be analyzed. *) +val procedure_should_be_analyzed : Cfg.Procdesc.t -> Procname.t -> bool (** Mark the return type @Nullable by modifying the spec. *) val proc_add_return_nullable : Procname.t -> unit diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 24c1d05b7..77b590ed4 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -57,7 +57,10 @@ module ST = struct let store_summary proc_name = Option.may (fun summary -> - try Specs.store_summary proc_name summary with Sys_error s -> L.err "%s@." s) + let summary' = + { summary with + Specs.timestamp = summary.Specs.timestamp + 1 } in + try Specs.store_summary proc_name summary' with Sys_error s -> L.err "%s@." s) (Specs.get_summary proc_name) let report_error diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index 92d8dd8f9..d516063a4 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -393,9 +393,14 @@ let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc = | Some pdesc -> let idenv_pname = Idenv.create_from_idenv idenv pdesc in Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in - Ondemand.set_analyze_proc _ondemand; - Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc; - Ondemand.unset_analyze_prop () + if not !Config.ondemand_enabled || + Ondemand.procedure_should_be_analyzed proc_desc proc_name + then + begin + Ondemand.set_analyze_proc _ondemand; + Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc; + Ondemand.unset_analyze_prop () + end (** Call the given check_return_type at the end of every procedure. *) let callback_check_return_type check_return_type all_procs diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index 4929c4245..42833cdfb 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -354,7 +354,7 @@ let check_return_annotation if return_not_nullable && Models.Inference.enabled then Models.Inference.proc_add_return_nullable curr_pname; - if return_not_nullable && Ondemand.enabled () then + if return_not_nullable && !Config.ondemand_enabled then Ondemand.proc_add_return_nullable curr_pname; if return_not_nullable || return_value_not_present then diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index 05505c1f5..fbefc1827 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -557,8 +557,8 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate (* skip othe builtins *) | 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 Ondemand.enabled () then - Ondemand.do_analysis get_proc_desc curr_pname callee_pname; + if !Config.ondemand_enabled then + Ondemand.do_analysis get_proc_desc curr_pdesc callee_pname; let callee_attributes = match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with | Some proc_attributes -> proc_attributes