[infer][backend] make the on-demand analysis function return a summary

Summary:
A good first step in order to run multiple checkers together is to prevent the analysis the analysis to side effect on the summaries of the method being analyzed from disk, or the shared specs summary. The idea is that `Ondemand` creates a summary for the procedure being analyzed and only saves the summary once all the checkers have been run. The summary for the caller (i.e. the procedure being analyzed) should never be looked up from disk during the analysis. In other words, the analysis should only ever lookup the summaries of the callees and the proposed solution to enforce this is to have `Ondemand.analyze_proc_name` be the only way to lookup the summary of a procedure.

Another objective is to make sure that the summaries are never saved to disk more than once.

Reviewed By: sblackshear

Differential Revision: D4549764

fbshipit-source-id: f0a6e21

infer/src/backend/interproc.ml

@@ -1405,7 +1405,7 @@ let interprocedural_algorithm exe_env : unit =
     List.filter ~f:filter_initial (Cg.get_defined_nodes call_graph) in
   let process_one_proc proc_name =
     let analyze proc_desc =
-      Ondemand.analyze_proc_desc ~propagate_exceptions:false proc_desc proc_desc in
+      ignore (Ondemand.analyze_proc_desc ~propagate_exceptions:false proc_desc proc_desc) in
     match Exe_env.get_proc_desc exe_env proc_name with
     | Some proc_desc
       when Config.reactive_mode (* in reactive mode, only analyze changed procedures *)

infer/src/backend/ondemand.ml

@@ -154,7 +154,8 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
         timestamp = summary.Specs.timestamp + 1 } in
     Specs.add_summary callee_pname summary';
     Checkers.ST.store_summary callee_pname;
-    Printer.write_proc_html source false callee_pdesc in
+    Printer.write_proc_html source false callee_pdesc;
+    summary' in
 
   let log_error_and_continue exn kind =
     Reporting.log_error callee_pname exn;
@@ -165,14 +166,16 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
       { 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
+    Specs.add_summary callee_pname new_summary;
+    new_summary in
 
   let old_state = save_global_state () in
   let source = preprocess () in
   try
     analyze_proc source callee_pdesc;
-    postprocess source;
+    let summary = postprocess source in
     restore_global_state old_state;
+    summary
   with exn ->
     L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.BACK TRACE@.%s@?"
       Procname.pp callee_pname
@@ -193,32 +196,39 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
           log_error_and_continue exn (FKcrash (Exn.to_string exn))
 
 
-let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc =
+let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc : Specs.summary option =
   let callee_pname = Procdesc.get_proc_name callee_pdesc in
   let proc_attributes = Procdesc.get_attributes callee_pdesc in
   match !callbacks_ref with
-  | Some callbacks
-    when should_be_analyzed callee_pname proc_attributes ->
-      run_proc_analysis ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc
-  | _ -> ()
+  | Some callbacks ->
+      if should_be_analyzed callee_pname proc_attributes then
+        let summary =
+          run_proc_analysis
+            ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc in
+        Some summary
+      else
+        Specs.get_summary callee_pname
+  | None -> None
 
 
 
 (** analyze_proc_name curr_pdesc proc_name
     performs an on-demand analysis of proc_name
     triggered during the analysis of curr_pname. *)
-let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname =
-
+let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname : Specs.summary option =
   match !callbacks_ref with
-  | Some callbacks
-    when procedure_should_be_analyzed callee_pname ->
-      begin
-        match callbacks.get_proc_desc callee_pname with
-        | Some callee_pdesc -> analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc
-        | None -> ()
-      end
-  | _ ->
-      () (* skipping *)
+  | Some callbacks ->
+      if procedure_should_be_analyzed callee_pname then
+        begin
+          match callbacks.get_proc_desc callee_pname with
+          | Some callee_pdesc ->
+              analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc
+          | None -> None
+        end
+      else
+        Specs.get_summary callee_pname
+  | None -> None
+
 
 (** Find a proc desc for the procedure, perhaps loading it from disk. *)
 let get_proc_desc callee_pname =

infer/src/backend/ondemand.mli

@@ -31,12 +31,14 @@ val get_proc_desc : get_proc_desc
 (** 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 -> Procdesc.t -> Procdesc.t -> unit
+val analyze_proc_desc :
+  propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> Specs.summary option
 
 (** analyze_proc_name curr_pdesc proc_name
     performs an on-demand analysis of proc_name
     triggered during the analysis of curr_pdesc. *)
-val analyze_proc_name : propagate_exceptions:bool -> Procdesc.t -> Procname.t -> unit
+val analyze_proc_name :
+  propagate_exceptions:bool -> Procdesc.t -> Procname.t -> Specs.summary option
 
 (** Check if the procedure called needs to be analyzed. *)
 val procedure_should_be_analyzed : Procname.t -> bool

infer/src/backend/symExec.ml

@@ -636,34 +636,32 @@ let resolve_java_pname tenv prop args pname_java call_flags : Procname.java =
     if not already analyzed *)
 let resolve_and_analyze
     tenv caller_pdesc prop args callee_proc_name call_flags : Procname.t * Specs.summary option =
-  (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name
+  (* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name
      whether the method is defined or generated by the specialization *)
-  let analyze_ondemand resolved_pname : unit =
+  let analyze_ondemand resolved_pname : Specs.summary option =
     if Procname.equal resolved_pname callee_proc_name then
       Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_proc_name
     else
       (* Create the type sprecialized procedure description and analyze it directly *)
-      Option.iter
-        ~f:(fun specialized_pdesc ->
-            Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
-        (match Ondemand.get_proc_desc resolved_pname with
-         | Some resolved_proc_desc ->
-             Some resolved_proc_desc
-         | None ->
-             begin
-               Option.map
-                 ~f:(fun callee_proc_desc ->
-                     Cfg.specialize_types callee_proc_desc resolved_pname args)
-                 (Ondemand.get_proc_desc callee_proc_name)
-             end) in
+      let analyze specialized_pdesc =
+        Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc in
+      let resolved_proc_desc_option =
+        match Ondemand.get_proc_desc resolved_pname with
+        | Some resolved_proc_desc ->
+            Some resolved_proc_desc
+        | None ->
+            (Option.map
+               ~f:(fun callee_proc_desc ->
+                   Cfg.specialize_types callee_proc_desc resolved_pname args)
+               (Ondemand.get_proc_desc callee_proc_name)) in
+      Option.bind resolved_proc_desc_option analyze in
   let resolved_pname = match callee_proc_name with
     | Procname.Java callee_proc_name_java ->
         Procname.Java
           (resolve_java_pname tenv prop args callee_proc_name_java call_flags)
     | _ ->
         callee_proc_name in
-  analyze_ondemand resolved_pname;
-  resolved_pname, Specs.get_summary resolved_pname
+  resolved_pname, analyze_ondemand resolved_pname
 
 
 (** recognize calls to the constructor java.net.URL and splits the argument string
@@ -1087,10 +1085,9 @@ let rec sym_exec tenv current_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.analyze_proc_name ~propagate_exceptions:true current_pdesc pname;
                 let exec_skip_call ret_annots ret_type = skip_call norm_prop path pname ret_annots
                     loc ret_id (Some ret_type) url_handled_args in
-                match Specs.get_summary pname with
+                match Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc pname with
                 | None ->
                     let ret_typ = Typ.java_proc_return_typ callee_pname_java in
                     let ret_annots = load_ret_annots callee_pname in
@@ -1110,8 +1107,9 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                 match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with
                 | resolved_pname :: _ -> resolved_pname
                 | [] -> callee_pname in
-              Ondemand.analyze_proc_name
-                ~propagate_exceptions:true current_pdesc resolved_pname;
+              let resolved_summary_opt =
+                Ondemand.analyze_proc_name
+                  ~propagate_exceptions:true current_pdesc resolved_pname in
               let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in
               let ret_typ_opt = Option.map ~f:Procdesc.get_ret_type callee_pdesc_opt in
               let sentinel_result =
@@ -1120,7 +1118,6 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                     (call_args prop_r callee_pname actual_params ret_id loc)
                 else [(prop_r, path)] in
               let do_call (prop, path) =
-                let resolved_summary_opt = Specs.get_summary resolved_pname in
                 if Option.value_map ~f:call_should_be_skipped ~default:true resolved_summary_opt then
                   (* If it's an ObjC getter or setter, call the builtin rather than skipping *)
                   let attrs_opt =

infer/src/checkers/summary.ml

@@ -46,7 +46,7 @@ module Make (H : Helper) = struct
         failwithf "Summary for %a should exist, but does not!@." Procname.pp pname
 
   let read_summary caller_pdesc callee_pname =
-    Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname;
+    ignore (Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname);
     match Specs.get_summary callee_pname with
     | None -> None
     | Some summary -> H.read_from_payload summary.Specs.payload

infer/src/eradicate/typeCheck.ml

@@ -566,7 +566,7 @@ let typecheck_instr
        loc,
        cflags)
     ->
-      Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname;
+      ignore (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 ->