[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

@@ -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;

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

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
 

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 =============== *)

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

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 =

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 =