From 22aad3e33a038a9a20d8410cf3d45841ff5c05c5 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Fri, 9 Oct 2015 09:24:26 -0700 Subject: [PATCH] Add basic support for on-demand for the core Infer analysis. Reviewed By: @jvillard Differential Revision: D2507560 fb-gh-sync-id: 0dead86 --- infer/src/backend/fork.ml | 52 ++++++++++++++++++++++++++------- infer/src/backend/interproc.ml | 34 +++++++++++++++++++-- infer/src/backend/ondemand.ml | 41 +++++++++++++++++--------- infer/src/backend/ondemand.mli | 22 +++++++++----- infer/src/backend/specs.ml | 2 +- infer/src/backend/symExec.ml | 4 +++ infer/src/checkers/eradicate.ml | 19 +++++++----- infer/src/checkers/typeCheck.ml | 2 +- 8 files changed, 131 insertions(+), 45 deletions(-) diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index 15b75bf22..af6a25c04 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -277,24 +277,42 @@ end = struct ignore (Gc.create_alarm SymOp.check_wallclock_alarm) end + let current_timeouts = ref [] + let exe_timeout iterations f x = - try + let restore_timeout () = + match !current_timeouts with + | prev_iterations :: _ -> + set_alarm prev_iterations + | [] -> + () in + let unwind () = + let pop () = match !current_timeouts with + | _ :: l -> current_timeouts := l + | [] -> () in + unset_alarm (); + SymOp.unset_alarm (); + pop () in + let before () = + current_timeouts := iterations :: !current_timeouts; set_iterations iterations; set_alarm (get_timeout_seconds ()); - SymOp.set_alarm (); + SymOp.set_alarm () in + let after () = + unwind (); + restore_timeout () in + try + before (); let res = f x in - unset_alarm (); - SymOp.unset_alarm (); + after (); Some res with | Timeout_exe kind -> - unset_alarm (); - SymOp.unset_alarm (); + after (); Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_kind kind; None | exe -> - unset_alarm (); - SymOp.unset_alarm (); + after (); raise exe end @@ -321,6 +339,18 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit = (proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) && (Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0 || not (proc_is_up_to_date call_graph pname)) in + let filter_out_ondemand pname = + if !Config.ondemand_enabled then + try + let cfg = Exe_env.get_cfg exe_env pname in + match Cfg.Procdesc.find_from_name cfg pname with + | Some pdesc -> + not (Ondemand.procedure_should_be_analyzed pdesc pname) + | None -> + false + with Not_found -> false + else + false in let process_one_proc pname (calls: Cg.in_out_calls) = DB.current_source := (Specs.get_summary_unsafe "main_algorithm" pname) @@ -333,7 +363,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 call_graph pname + if filter_out call_graph pname || + filter_out_ondemand pname then post_process_procs exe_env [pname] else @@ -357,7 +388,8 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit = with Not_found -> (* no analyzable procs *) L.err "Error: can't analyze any procs. Printing current spec table@\n@[%a@]@." (Specs.pp_spec_table pe_text false) (); - raise (Failure "Stopping") + if !Config.ondemand_enabled then wpnames_todo := WeightedPnameSet.empty + else raise (Failure "Stopping") end done diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index b2d7eed6d..ddbabed47 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1245,8 +1245,35 @@ let do_analysis exe_env = if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children) else if !Config.only_nospecs then filter_nospecs else (fun _ -> true) in - list_iter (fun x -> if filter x then init_proc x) procs_and_defined_children; - Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out + list_iter + (fun ((pn, _) as x) -> + let should_init () = + not !Config.ondemand_enabled || + Specs.get_summary pn = None in + if filter x && + should_init () + then init_proc x) + procs_and_defined_children; + + let callbacks = + let get_proc_desc proc_name = + 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 + let _summaryfp = analyze_proc exe_env proc_name in + let cg = Cg.create () in + Cg.add_node cg proc_name; + perform_transition exe_env cg proc_name; + let _summaryre = analyze_proc exe_env proc_name in + Config.footprint := saved_footprint; + () in + { Ondemand.analyze_ondemand; get_proc_desc; } in + + Ondemand.set_callbacks callbacks; + Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out; + Ondemand.unset_callbacks () + let visited_and_total_nodes cfg = let all_nodes = @@ -1283,7 +1310,8 @@ let print_stats_cfg proc_shadowed proc_is_active cfg = let num_timeout = ref 0 in let compute_stats_proc proc_desc = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in - if proc_shadowed proc_desc then + if proc_shadowed proc_desc || + Specs.get_summary proc_name = None then L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name else let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index ac06fb3c5..cbfabcbac 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -15,21 +15,29 @@ open Utils let trace = false -let () = Config.ondemand_enabled := Config.from_env_variable "INFER_ONDEMAND" +let () = Config.ondemand_enabled := + Config.from_env_variable "INFER_ONDEMAND" && + not Config.analyze_models let across_files () = true -type analyze_proc = Procname.t -> unit +type analyze_ondemand = Procname.t -> unit type get_proc_desc = Procname.t -> Cfg.Procdesc.t option -let analyze_proc_fun = ref None +type callbacks = + { + analyze_ondemand : analyze_ondemand; + get_proc_desc : get_proc_desc; + } -let set_analyze_proc (analyze_proc : analyze_proc) = - analyze_proc_fun := Some analyze_proc +let callbacks_ref = ref None -let unset_analyze_prop () = - analyze_proc_fun := None +let set_callbacks (callbacks : callbacks) = + callbacks_ref := Some callbacks + +let unset_callbacks () = + callbacks_ref := None let nesting = ref 0 @@ -50,16 +58,20 @@ let procedure_should_be_analyzed curr_pdesc proc_name = = proc_attributes.ProcAttributes.loc.Location.file in + let is_harness () = + string_contains "InferGeneratedHarness" (Procname.to_simplified_string proc_name) 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) + (across_files () || (* whether to push the analysis into other files *) + same_file proc_attributes) && + not (is_harness ()) (* skip harness procedures *) | None -> false -let do_analysis (get_proc_desc : get_proc_desc) curr_pdesc proc_name = +let do_analysis curr_pdesc proc_name = let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in let really_do_analysis analyze_proc proc_desc = @@ -100,13 +112,14 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pdesc proc_name = (Printexc.get_backtrace ()); raise e in - match !analyze_proc_fun with - | Some analyze_proc + match !callbacks_ref with + | Some callbacks when procedure_should_be_analyzed curr_pdesc proc_name -> + begin - match get_proc_desc proc_name with + match callbacks.get_proc_desc proc_name with | Some proc_desc -> - really_do_analysis analyze_proc proc_desc + really_do_analysis callbacks.analyze_ondemand proc_desc | None -> () end | _ -> diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index 76842d509..60033c763 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -9,14 +9,20 @@ (** Module for on-demand analysis. *) -type analyze_proc = Procname.t -> unit +type analyze_ondemand = Procname.t -> unit type get_proc_desc = Procname.t -> Cfg.Procdesc.t option -(** do_analysis get_proc_desc curr_descproc_name +type callbacks = + { + analyze_ondemand : analyze_ondemand; + get_proc_desc : get_proc_desc; + } + +(** do_analysis curr_pdesc proc_name performs an on-demand analysis of proc_name - triggered during the analysis of curr_pdesc. *) -val do_analysis : get_proc_desc -> Cfg.Procdesc.t -> Procname.t -> unit + triggered during the analysis of curr_pname. *) +val do_analysis : Cfg.Procdesc.t -> Procname.t -> unit (** Check if the procedure called by the current pdesc needs to be analyzed. *) val procedure_should_be_analyzed : Cfg.Procdesc.t -> Procname.t -> bool @@ -24,8 +30,8 @@ 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 -(** Set the function to be used to perform on-demand analysis. *) -val set_analyze_proc : analyze_proc -> unit +(** Set the callbacks used to perform on-demand analysis. *) +val set_callbacks : callbacks -> unit -(** Unset the function to be used to perform on-demand analysis. *) -val unset_analyze_prop : unit -> unit +(** Unset the callbacks used to perform on-demand analysis. *) +val unset_callbacks : unit -> unit diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 3f3ffc015..e9e51b513 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -396,7 +396,7 @@ let describe_status summary = ("Status", if summary.status == ACTIVE then "ACTIVE" else "INACTIVE") let describe_phase summary = - ("Phase", if summary.phase == FOOTPRINT then "FOOTRPRINT" else "RE_EXECUTION") + ("Phase", if summary.phase == FOOTPRINT then "FOOTPRINT" else "RE_EXECUTION") (** Return the signature of a procedure declaration as a string *) let get_signature summary = diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index f0764c8eb..ae694fc18 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -963,6 +963,10 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path if call_flags.Sil.cf_virtual then resolve_virtual_pname cfg tenv prop_r n_actual_params fn else fn in + + if !Config.ondemand_enabled then + Ondemand.do_analysis pdesc callee_pname; + let ret_typ_opt = match Cfg.Procdesc.find_from_name cfg resolved_pname with | None -> None diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index d516063a4..006250964 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -387,19 +387,22 @@ let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc = check_extension = false; check_ret_type = []; } in - let _ondemand pname = - match get_proc_desc pname with - | None -> () - | 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 + let callbacks = + let analyze_ondemand pname = + match get_proc_desc pname with + | None -> () + | 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.analyze_ondemand; get_proc_desc; } in + if not !Config.ondemand_enabled || Ondemand.procedure_should_be_analyzed proc_desc proc_name then begin - Ondemand.set_analyze_proc _ondemand; + Ondemand.set_callbacks callbacks; Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc; - Ondemand.unset_analyze_prop () + Ondemand.unset_callbacks () end (** Call the given check_return_type at the end of every procedure. *) diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index fbefc1827..0171ad944 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -558,7 +558,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 get_proc_desc curr_pdesc callee_pname; + Ondemand.do_analysis curr_pdesc callee_pname; let callee_attributes = match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with | Some proc_attributes -> proc_attributes