[infer][ondemand] Run the Thread-Safety checker in two phases, first analyze all the procedure on-demand using a procedure callback, and then combine all the analysis results using a cluster callback

Summary: This allows to run the analysis of every procedure on-demand separately from the cluster callbacks

Reviewed By: sblackshear

Differential Revision: D4664936

fbshipit-source-id: d218328

infer/src/backend/callbacks.ml

@@ -44,7 +44,6 @@ let unregister_all_callbacks () =
   procedure_callbacks := [];
   cluster_callbacks := []
 
-
 (** Collect what we need to know about a procedure for the analysis. *)
 let get_procedure_definition exe_env proc_name =
   let tenv = Exe_env.get_tenv exe_env proc_name in
@@ -57,6 +56,17 @@ let get_procedure_definition exe_env proc_name =
 
 let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.Clang
 
+
+let reset_summary proc_name =
+  let should_reset =
+    is_none (Specs.get_summary proc_name) in
+  if should_reset
+  then
+    let attributes_opt =
+      Specs.proc_resolve_attributes proc_name in
+    Specs.reset_summary proc_name attributes_opt None
+
+
 (** Invoke all registered procedure callbacks on the given procedure. *)
 let iterate_procedure_callbacks exe_env caller_pname =
   let procedure_language = get_language caller_pname in
@@ -132,14 +142,24 @@ let iterate_cluster_callbacks all_procs exe_env proc_names =
           cluster_callback exe_env all_procs get_procdesc environment)
     !cluster_callbacks
 
+
 (** Invoke all procedure and cluster callbacks on a given environment. *)
 let iterate_callbacks call_graph exe_env =
+  let saved_language = !Config.curr_language in
   let procs_to_analyze =
     (* analyze all the currently defined procedures *)
     Cg.get_defined_nodes call_graph in
+
+  (* Make sure summaries exists. *)
+  List.iter ~f:reset_summary procs_to_analyze;
+
+  (* Invoke procedure callbacks. *)
+  List.iter
+    ~f:(iterate_procedure_callbacks exe_env)
+    procs_to_analyze;
+
   let originally_defined_procs =
     Cg.get_defined_nodes call_graph in
-  let saved_language = !Config.curr_language in
 
   let cluster_id proc_name =
     match proc_name with
@@ -158,22 +178,8 @@ let iterate_callbacks call_graph exe_env =
         proc_names in
     (* Return all values of the map *)
     String.Map.data cluster_map in
-  let reset_summary proc_name =
-    let attributes_opt =
-      Specs.proc_resolve_attributes proc_name in
-    let should_reset =
-      is_none (Specs.get_summary proc_name) in
-    if should_reset
-    then Specs.reset_summary proc_name attributes_opt None in
-
-  (* Make sure summaries exists. *)
-  List.iter ~f:reset_summary procs_to_analyze;
-
-  (* Invoke callbacks. *)
-  List.iter
-    ~f:(iterate_procedure_callbacks exe_env)
-    procs_to_analyze;
 
+  (* Invoke cluster callbacks. *)
   List.iter
     ~f:(iterate_cluster_callbacks originally_defined_procs exe_env)
     (cluster procs_to_analyze);

infer/src/checkers/ThreadSafety.ml

@@ -796,10 +796,13 @@ let make_results_table get_proc_desc file_env =
       l in
   let compute_post_for_procedure = (* takes proc_env as arg *)
     fun (idenv, tenv, proc_name, proc_desc) ->
-      let callback_arg =
-        let get_procs_in_file _ = [] in
-        { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
-      analyze_procedure callback_arg in
+      match Summary.read_summary proc_desc proc_name with
+      | Some summ -> summ
+      | None ->
+          let callback_arg =
+            let get_procs_in_file _ = [] in
+            { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
+          analyze_procedure callback_arg in
   map_post_computation_over_procs compute_post_for_procedure file_env
 
 let get_current_class_and_threadsafe_superclasses tenv pname =

infer/src/checkers/registerCheckers.ml

@@ -40,6 +40,7 @@ let active_procedure_checkers () =
         PrintfArgs.callback_printf_args, checkers_enabled;
         AnnotationReachability.checker, checkers_enabled;
         BufferOverrunChecker.checker, Config.bufferoverrun;
+        ThreadSafety.checker, Config.threadsafety;
       ] in
     (* make sure SimpleChecker.ml is not dead code *)
     if false then (let module SC = SimpleChecker.Make in ());