Add the possibility to analyze procedure descriptions on-demand without serialization

Summary:public
In order to implement the lazy dynamic dispatch algorithm, we need to generate a procedure description based on the types encountered during the symbolic execution. This diff adds support for analyzing such a prodecure description directly, without having to first serialize it to disk, which is slow and not necessary.

Reviewed By: cristianoc

Differential Revision: D3028226

fb-gh-sync-id: 1b2360e
shipit-source-id: 1b2360e

infer/src/backend/cfg.ml

@@ -701,7 +701,7 @@ module Node = struct
               new_node in
           converted_node :: (loop other_node) in
     ignore (loop [callee_start_node]);
-    pdesc_tbl_add cfg resolved_proc_name resolved_proc_desc
+    resolved_proc_desc
 
 end
 (* =============== END of module Node =============== *)
@@ -1151,30 +1151,21 @@ let specialize_types caller_cfg callee_proc_name resolved_proc_name args =
   (** TODO (#9333890): This currently only works when the callee is defined in the same file.
       Add support to search for the callee procedure description in the execution environment *)
   match Procdesc.find_from_name caller_cfg resolved_proc_name with
-  | Some _ -> ()
+  | Some pdesc -> Some pdesc
   | None ->
-      begin
+      Option.map
-        match Procdesc.find_from_name caller_cfg callee_proc_name with
+        (fun callee_proc_desc ->
-        | None -> ()
+           let callee_attributes = Procdesc.get_attributes callee_proc_desc in
-        | Some callee_proc_desc ->
+           let resolved_formals =
-            let callee_attributes = Procdesc.get_attributes callee_proc_desc in
+             IList.fold_left2
-            let resolved_formals =
+               (fun accu (name, _) (_, arg_typ) -> (name, arg_typ) :: accu)
-              IList.fold_left2
+               [] callee_attributes.ProcAttributes.formals args |> IList.rev in
-                (fun accu (name, _) (_, arg_typ) -> (name, arg_typ) :: accu)
+           let resolved_attributes =
-                [] callee_attributes.ProcAttributes.formals args |> IList.rev in
+             { callee_attributes with
-            let resolved_attributes =
+               ProcAttributes.formals = resolved_formals;
-              { callee_attributes with
+               proc_name = resolved_proc_name;
-                ProcAttributes.formals = resolved_formals;
+             } in
-                proc_name = resolved_proc_name;
+           AttributesTable.store_attributes resolved_attributes;
-              } in
+           Procdesc.specialize_types
-            AttributesTable.store_attributes resolved_attributes;
+             caller_cfg callee_proc_desc resolved_attributes resolved_formals)
-            Procdesc.specialize_types
+        (Procdesc.find_from_name caller_cfg callee_proc_name)
-              caller_cfg callee_proc_desc resolved_attributes resolved_formals;
-            begin
-              let source_file = resolved_attributes.ProcAttributes.loc.Location.file in
-              let source_dir = DB.source_dir_from_source_file source_file in
-              let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
-              let save_sources = false in
-              store_cfg_to_file cfg_file save_sources caller_cfg
-            end
-      end

infer/src/backend/cfg.mli

@@ -317,4 +317,5 @@ val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Pr
     (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but
     all the type of the parameters are replaced in the instructions according to the list.
     The virtual calls are also replaced to match the parameter types *)
-val specialize_types : cfg -> Procname.t -> Procname.t -> (Sil.exp * Sil.typ) list -> unit
+val specialize_types :
+  cfg -> Procname.t -> Procname.t -> (Sil.exp * Sil.typ) list -> Procdesc.t option

infer/src/backend/interproc.ml

@@ -1280,7 +1280,7 @@ let interprocedural_algorithm exe_env : unit =
   let process_one_proc proc_name =
     match to_analyze proc_name with
     | Some pdesc ->
-        Ondemand.do_analysis ~propagate_exceptions:false pdesc proc_name
+        Ondemand.analyze_proc_name ~propagate_exceptions:false pdesc proc_name
     | None ->
         () in
   IList.iter process_one_proc procs_to_analyze
@@ -1323,20 +1323,17 @@ let do_analysis exe_env =
     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 analyze_ondemand proc_desc =
-      match get_proc_desc proc_name with
+      let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
-      | Some proc_desc ->
+      let summaryfp =
-          let summaryfp =
+        run_in_footprint_mode (analyze_proc exe_env) proc_desc in
-            run_in_footprint_mode (analyze_proc exe_env) proc_desc in
+      Specs.add_summary proc_name summaryfp;
-          Specs.add_summary proc_name summaryfp;
+
-
+      perform_transition exe_env proc_name;
-          perform_transition exe_env proc_name;
+
-
+      let summaryre =
-          let summaryre =
+        run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
-            run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
+      Specs.add_summary proc_name summaryre in
-          Specs.add_summary proc_name summaryre
-      | None ->
-          () in
     {
       Ondemand.analyze_ondemand;
       get_cfg;

infer/src/backend/ondemand.ml

@@ -39,7 +39,7 @@ let read_dirs_to_analyze () =
 let dirs_to_analyze =
   lazy (read_dirs_to_analyze ())
 
-type analyze_ondemand = Procname.t -> unit
+type analyze_ondemand = Cfg.Procdesc.t -> unit
 
 type get_cfg = Procname.t -> Cfg.cfg option
 
@@ -62,21 +62,24 @@ let unset_callbacks () =
 
 let nesting = ref 0
 
+let should_be_analyzed proc_attributes proc_name =
+  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
+  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 *)
+
 let procedure_should_be_analyzed proc_name =
   match AttributesTable.load_attributes proc_name with
   | Some proc_attributes ->
-      let currently_analyzed =
+      should_be_analyzed proc_attributes proc_name
-        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
-
-      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 *)
   | None ->
       false
 
@@ -117,86 +120,102 @@ let restore_global_state st =
   State.restore_state st.symexec_state;
   Timeout.resume_previous_timeout ()
 
-(** do_analysis curr_pdesc proc_name
+
-    performs an on-demand analysis of proc_name
+let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc =
-    triggered during the analysis of curr_pname. *)
-let do_analysis ~propagate_exceptions curr_pdesc callee_pname =
   let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
+  let callee_pname = Cfg.Procdesc.get_proc_name callee_pdesc in
+
+  (** Dot means start of a procedure *)
+  L.log_progress_procedure ();
+  if trace () then L.stderr "[%d] run_proc_analysis %a -> %a@."
+      !nesting
+      Procname.pp curr_pname
+      Procname.pp callee_pname;
+
+  let preprocess () =
+    incr nesting;
+    let attributes_opt =
+      Specs.proc_resolve_attributes callee_pname in
+    Option.may
+      (fun attribute ->
+         DB.current_source := attribute.ProcAttributes.loc.Location.file;
+         let attribute_pname = attribute.ProcAttributes.proc_name in
+         if not (Procname.equal callee_pname attribute_pname) then
+           failwith ("ERROR: "^(Procname.to_string callee_pname)
+                     ^" not equal to "^(Procname.to_string attribute_pname)))
+      attributes_opt;
+    let call_graph =
+      let cg = Cg.create () in
+      Cg.add_defined_node cg callee_pname;
+      cg in
+    Specs.reset_summary call_graph callee_pname attributes_opt;
+    Specs.set_status callee_pname Specs.ACTIVE in
+
+  let postprocess () =
+    decr nesting;
+    let summary = Specs.get_summary_unsafe "ondemand" callee_pname in
+    let summary' =
+      { summary with
+        Specs.status = Specs.INACTIVE;
+        timestamp = summary.Specs.timestamp + 1 } in
+    Specs.add_summary callee_pname summary';
+    Checkers.ST.store_summary callee_pname;
+    Printer.proc_write_log false callee_pdesc 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_pdesc;
+    postprocess ();
+    restore_global_state old_state;
+  with exn ->
+    L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@."
+      Procname.pp callee_pname
+      (Printexc.to_string exn)
+      (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000))
+      (Printexc.get_backtrace ());
+    restore_global_state old_state;
+    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))
+
+
+let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc =
+  let callee_pname = Cfg.Procdesc.get_proc_name callee_pdesc in
+  let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in
+  match !callbacks_ref with
+  | Some callbacks
+    when should_be_analyzed proc_attributes callee_pname ->
+      run_proc_analysis
+        ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc
+  | _ -> ()
+
 
-  let really_do_analysis callee_pdesc analyze_proc =
+
-    (** Dot means start of a procedure *)
+(** analyze_proc_name curr_pdesc proc_name
-    L.log_progress_procedure ();
+    performs an on-demand analysis of proc_name
-    if trace () then L.stderr "[%d] really_do_analysis %a -> %a@."
+    triggered during the analysis of curr_pname. *)
-        !nesting
+let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname =
-        Procname.pp curr_pname
-        Procname.pp callee_pname;
-
-    let preprocess () =
-      incr nesting;
-      let attributes_opt =
-        Specs.proc_resolve_attributes callee_pname in
-      Option.may
-        (fun attribute ->
-           DB.current_source := attribute.ProcAttributes.loc.Location.file;
-           let attribute_pname = attribute.ProcAttributes.proc_name in
-           if not (Procname.equal callee_pname attribute_pname) then
-             failwith ("ERROR: "^(Procname.to_string callee_pname)
-                       ^" not equal to "^(Procname.to_string attribute_pname)))
-        attributes_opt;
-      let call_graph =
-        let cg = Cg.create () in
-        Cg.add_defined_node cg callee_pname;
-        cg in
-      Specs.reset_summary call_graph callee_pname attributes_opt;
-      Specs.set_status callee_pname Specs.ACTIVE in
-
-    let postprocess () =
-      decr nesting;
-      let summary = Specs.get_summary_unsafe "ondemand" callee_pname in
-      let summary' =
-        { summary with
-          Specs.status = Specs.INACTIVE;
-          timestamp = summary.Specs.timestamp + 1 } in
-      Specs.add_summary callee_pname summary';
-      Checkers.ST.store_summary callee_pname;
-      Printer.proc_write_log false callee_pdesc 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 exn ->
-      L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@."
-        Procname.pp callee_pname
-        (Printexc.to_string exn)
-        (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000))
-        (Printexc.get_backtrace ());
-      restore_global_state old_state;
-      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
@@ -204,7 +223,7 @@ let do_analysis ~propagate_exceptions curr_pdesc callee_pname =
       begin
         match callbacks.get_proc_desc callee_pname with
         | Some callee_pdesc ->
-            really_do_analysis callee_pdesc callbacks.analyze_ondemand
+            analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc
         | None ->
             ()
       end

infer/src/backend/ondemand.mli

@@ -12,7 +12,7 @@
 (** Optional set of source dirs to analyze in on-demand mode. *)
 val dirs_to_analyze : StringSet.t option Lazy.t
 
-type analyze_ondemand = Procname.t -> unit
+type analyze_ondemand = Cfg.Procdesc.t -> unit
 
 type get_cfg = Procname.t -> Cfg.cfg option
 
@@ -28,10 +28,15 @@ type callbacks =
 (** Find a cfg for the procedure, perhaps loading it from disk. *)
 val get_cfg : get_cfg
 
-(** do_analysis curr_pdesc proc_name
+(** analyze_proc_desc curr_pdesc callee_pdesc
+    performs an on-demand analysis of callee_pdesc
+    triggered during the analysis of curr_pdesc. *)
+val analyze_proc_desc : propagate_exceptions:bool -> Cfg.Procdesc.t -> Cfg.Procdesc.t -> unit
+
+(** analyze_proc_name curr_pdesc proc_name
     performs an on-demand analysis of proc_name
-    triggered during the analysis of curr_pname. *)
+    triggered during the analysis of curr_pdesc. *)
-val do_analysis : propagate_exceptions:bool -> Cfg.Procdesc.t -> Procname.t -> unit
+val analyze_proc_name : propagate_exceptions:bool -> Cfg.Procdesc.t -> Procname.t -> unit
 
 (** Check if the procedure called needs to be analyzed. *)
 val procedure_should_be_analyzed : Procname.t -> bool

infer/src/backend/symExec.ml

@@ -716,27 +716,23 @@ let resolve_java_pname tenv prop args pname call_flags : Procname.t =
     if not already analyzed *)
 let resolve_and_analyze
     tenv caller_pdesc prop args callee_pname call_flags : Procname.t * Specs.summary option =
-  let resolved_pname =
+  (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name
-    (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name
+     whether the method is defined or generated by the specialization *)
-         whether the method is defined or generated by the specialization *)
+  let analyze_ondemand caller_cfg resolved_pname : unit =
-    let res_pname =
+    if Procname.equal resolved_pname callee_pname then
-      resolve_java_pname tenv prop args callee_pname call_flags in
+      Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_pname
-    if Procname.equal res_pname callee_pname
-    then
-      callee_pname
     else
-      begin
+      (* Create the type sprecialized procedure description and analyze it directly *)
-        if not (Specs.summary_exists res_pname) then
+      Option.may
-          begin
+        (fun specialized_pdesc ->
-            match Ondemand.get_cfg (Cfg.Procdesc.get_proc_name caller_pdesc) with
+           Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
-            | Some caller_cfg ->
+        (Cfg.specialize_types caller_cfg callee_pname resolved_pname args) in
-                Cfg.specialize_types caller_cfg callee_pname res_pname args
+  let resolved_pname =
-            | None ->
+    resolve_java_pname tenv prop args callee_pname call_flags in
-                ()
+  Option.may
-          end;
+    (fun caller_cfg ->
-        res_pname
+       analyze_ondemand caller_cfg resolved_pname)
-      end in
+    (Ondemand.get_cfg (Cfg.Procdesc.get_proc_name caller_pdesc));
-  Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc resolved_pname;
   resolved_pname, Specs.get_summary resolved_pname
 
 
@@ -1083,7 +1079,6 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path
           proc_name = callee_pname;
           loc;
         }
-
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags)
     when !Config.curr_language = Config.Java && Config.lazy_dynamic_dispatch ->
       let norm_prop, norm_args = normalize_params pname prop_ actual_params in
@@ -1115,7 +1110,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path
       let resolved_pnames =
         resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in
       let exec_one_pname pname =
-        Ondemand.do_analysis ~propagate_exceptions:true pdesc pname;
+        Ondemand.analyze_proc_name ~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
@@ -1140,7 +1135,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path
         | resolved_pname :: _ -> resolved_pname
         | [] -> callee_pname in
 
-      Ondemand.do_analysis ~propagate_exceptions:true pdesc resolved_pname;
+      Ondemand.analyze_proc_name ~propagate_exceptions:true pdesc resolved_pname;
 
       let callee_pdesc_opt =
         match Ondemand.get_cfg pname with

infer/src/checkers/performanceCritical.ml

@@ -159,7 +159,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 ~propagate_exceptions:true caller_pdesc pname;
+      Ondemand.analyze_proc_name ~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 =
@@ -317,10 +317,8 @@ let check_one_procedure tenv pname pdesc =
 let callback_performance_checker
     { Callbacks.get_cfg; get_proc_desc; proc_desc; proc_name; tenv } =
   let callbacks =
-    let analyze_ondemand pn =
+    let analyze_ondemand pdesc =
-      match get_proc_desc pn with
+      check_one_procedure tenv (Cfg.Procdesc.get_proc_name pdesc) pdesc in
-      | None -> ()
-      | Some pd -> check_one_procedure tenv pn pd in
     {
       Ondemand.analyze_ondemand;
       get_cfg;

infer/src/eradicate/eradicate.ml

@@ -394,16 +394,13 @@ let callback_eradicate
       check_ret_type = [];
     } in
   let callbacks =
-    let analyze_ondemand pname =
+    let analyze_ondemand pdesc =
-      match get_proc_desc pname with
+      let idenv_pname = Idenv.create_from_idenv idenv pdesc in
-      | None -> ()
+      Main.callback checks
-      | Some pdesc ->
+        { callback_args with
-          let idenv_pname = Idenv.create_from_idenv idenv pdesc in
+          Callbacks.idenv = idenv_pname;
-          Main.callback checks
+          proc_name = (Cfg.Procdesc.get_proc_name pdesc);
-            { callback_args with
+          proc_desc = pdesc; } in
-              Callbacks.idenv = idenv_pname;
-              proc_name = pname;
-              proc_desc = pdesc; } in
     {
       Ondemand.analyze_ondemand;
       get_cfg;

infer/src/eradicate/typeCheck.ml

@@ -556,7 +556,7 @@ 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 ->
-      Ondemand.do_analysis ~propagate_exceptions:true curr_pdesc callee_pname;
+      Ondemand.analyze_proc_name ~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