From 6ae0ebe48974a37280c3306cd717ec87051aedad Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 26 Oct 2016 14:12:58 -0700 Subject: [PATCH] [infer][java] Store the procedure descriptions in the summary to run the analyis with lazy dynamic dispatch across modules Summary: The lazy dynamic dispatch algorithm works by re-analyzing the generic methods with the more specialized types encountered during the symbolic execution. In order to do that, the analysis must access the procedure description of the method to reanalyze in order to run the analysis of the specialized procedure description on demand. This diff adds the procedure description on the summary as the summary are stored in the Buck cache and can easily be retrieved by procname. Reviewed By: sblackshear Differential Revision: D4077415 fbshipit-source-id: c2f1cc8 --- infer/src/backend/callbacks.ml | 2 +- infer/src/backend/interproc.ml | 15 +++++++++++++-- infer/src/backend/ondemand.ml | 6 +++++- infer/src/backend/specs.ml | 10 +++++++--- infer/src/backend/specs.mli | 8 +++++--- infer/src/backend/symExec.ml | 7 ++++++- infer/src/base/Config.ml | 2 ++ 7 files changed, 39 insertions(+), 11 deletions(-) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 57a36fe8a..3491295e0 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -165,7 +165,7 @@ let iterate_callbacks store_summary call_graph exe_env = let should_reset = Specs.get_summary proc_name = None in if should_reset - then Specs.reset_summary call_graph proc_name attributes_opt in + then Specs.reset_summary call_graph proc_name attributes_opt None in (* Make sure summaries exists. *) IList.iter reset_summary procs_to_analyze; diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 3e8a987b8..348f82d10 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1459,7 +1459,11 @@ let do_analysis exe_env = let attributes = { (Cfg.Procdesc.get_attributes pdesc) with ProcAttributes.err_log = static_err_log; } in - Specs.init_summary (dep, nodes, proc_flags, calls, None, attributes) in + let proc_desc_option = + if Config.dynamic_dispatch_lazy + then Some pdesc + else None in + Specs.init_summary (dep, nodes, proc_flags, calls, None, attributes, proc_desc_option) in IList.iter (fun ((pn, _) as x) -> @@ -1472,7 +1476,14 @@ let do_analysis exe_env = let callbacks = let get_proc_desc proc_name = - Exe_env.get_proc_desc exe_env proc_name in + match Exe_env.get_proc_desc exe_env proc_name with + | Some pdesc -> Some pdesc + | None when Config.dynamic_dispatch_lazy -> + Option.map_default + (fun summary -> summary.Specs.proc_desc_option) + None + (Specs.get_summary proc_name) + | None -> None in let analyze_ondemand source proc_desc = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index d99355881..89c92d46e 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -136,7 +136,11 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_ let cg = Cg.create (Some source) in Cg.add_defined_node cg callee_pname; cg in - Specs.reset_summary call_graph callee_pname attributes_opt; + let callee_pdesc_option = + if Config.dynamic_dispatch_lazy + then Some callee_pdesc + else None in + Specs.reset_summary call_graph callee_pname attributes_opt callee_pdesc_option; Specs.set_status callee_pname Specs.ACTIVE; source in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 13e93c1bb..d34eb66b7 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -339,6 +339,7 @@ type summary = status: status; (** ACTIVE when the proc is being analyzed *) timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) attributes : ProcAttributes.t; (** Attributes of the procedure *) + proc_desc_option : Cfg.Procdesc.t option; } type spec_tbl = (summary * DB.origin) Procname.Hash.t @@ -770,7 +771,8 @@ let empty_payload = let init_summary (depend_list, nodes, proc_flags, calls, in_out_calls_opt, - proc_attributes) = + proc_attributes, + proc_desc_option) = let dependency_map = mk_initial_dependency_map depend_list in let summary = { @@ -785,11 +787,12 @@ let init_summary attributes = { proc_attributes with ProcAttributes.proc_flags = proc_flags; }; + proc_desc_option; } in Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, DB.Res_dir) (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) -let reset_summary call_graph proc_name attributes_opt = +let reset_summary call_graph proc_name attributes_opt proc_desc_option = let dependents = Cg.get_defined_children call_graph proc_name in let proc_attributes = match attributes_opt with | Some attributes -> @@ -802,7 +805,8 @@ let reset_summary call_graph proc_name attributes_opt = proc_flags_empty (), [], Some (Cg.get_calls call_graph proc_name), - proc_attributes + proc_attributes, + proc_desc_option ) (* =============== END of support for spec tables =============== *) diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 0dd92e75d..522bbee4c 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -144,6 +144,7 @@ type summary = status: status; (** ACTIVE when the proc is being analyzed *) timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) attributes : ProcAttributes.t; (** Attributes of the procedure *) + proc_desc_option : Cfg.Procdesc.t option; } (** Add the summary to the table for the given function *) @@ -217,11 +218,12 @@ val init_summary : proc_flags * (* procedure flags *) (Procname.t * Location.t) list * (* calls *) (Cg.in_out_calls option) * (* in and out calls *) - ProcAttributes.t (* attributes of the procedure *) - ) -> unit + ProcAttributes.t * (* attributes of the procedure *) + Cfg.Procdesc.t option) (* procdesc option *) + -> unit (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) -val reset_summary : Cg.t -> Procname.t -> ProcAttributes.t option -> unit +val reset_summary : Cg.t -> Procname.t -> ProcAttributes.t option -> Cfg.Procdesc.t option -> unit (** Load procedure summary from the given file *) val load_summary : DB.filename -> summary option diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 624e53145..1f8a2fc36 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1060,7 +1060,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), actual_params, loc, call_flags) when Config.dynamic_dispatch_lazy -> - let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in + let norm_prop, norm_args = + normalize_params + tenv + current_pname + prop_ + (call_constructor_url_update_args callee_pname actual_params) in let exec_skip_call skipped_pname ret_annots ret_type = skip_call norm_prop path skipped_pname ret_annots loc ret_id (Some ret_type) norm_args in let resolved_pname, summary_opt = diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 4e2536908..51f9184a1 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -809,11 +809,13 @@ and dotty_cfg_libs = and dynamic_dispatch_lazy = CLOpt.mk_bool ~long:"dynamic-dispatch-lazy" + ~exes:CLOpt.[Java] "Handle dynamic dispatch by following the JVM semantics and creating procedure descriptions \ during the symbolic execution using the type information found in the abstract state" and dynamic_dispatch_sound = CLOpt.mk_bool ~long:"dynamic-dispatch-sound" + ~exes:CLOpt.[Java] "Dynamic dispatch for interface calls in Java" and enable_checks =