[infer][checkers] specify the dynamic dispatch handling policy on a per-checker basis.

Summary:
This will allow most of the checkers, except the bi-abduction, to skip the analysis on the specialized clone of the methods used to handle dynamic dispatch. Doing this, we can run the bi-abduction analysis using:
  infer -a checkers --biabduction
without risk of conflicts on the resolution of dynamic dispatch.

Reviewed By: sblackshear

Differential Revision: D6052347

fbshipit-source-id: 0c75bf3

infer/src/IR/Cfg.ml

@@ -418,7 +418,10 @@ let specialize_types callee_pdesc resolved_pname args =
   in
   let resolved_attributes =
     { callee_attributes with
-      formals= List.rev resolved_params; proc_name= resolved_pname; err_log= Errlog.empty () }
+      formals= List.rev resolved_params
+    ; proc_name= resolved_pname
+    ; is_specialized= true
+    ; err_log= Errlog.empty () }
   in
   Attributes.store resolved_attributes ;
   let resolved_pdesc =

infer/src/IR/ProcAttributes.ml

@@ -54,6 +54,7 @@ type t =
   ; is_cpp_noexcept_method: bool  (** the procedure is an C++ method annotated with "noexcept" *)
   ; is_java_synchronized_method: bool  (** the procedure is a Java synchronized method *)
   ; is_model: bool  (** the procedure is a model *)
+  ; is_specialized: bool  (** the procedure is a clone specialized for dynamic dispatch handling *)
   ; is_synthetic_method: bool  (** the procedure is a synthetic method *)
   ; language: Config.language  (** language of the procedure *)
   ; loc: Location.t  (** location of this procedure in the source code *)
@@ -86,6 +87,7 @@ let default proc_name language =
   ; is_defined= false
   ; is_objc_instance_method= false
   ; is_model= false
+  ; is_specialized= false
   ; is_synthetic_method= false
   ; language
   ; loc= Location.dummy

infer/src/IR/ProcAttributes.mli

@@ -52,6 +52,7 @@ type t =
   ; is_cpp_noexcept_method: bool  (** the procedure is an C++ method annotated with "noexcept" *)
   ; is_java_synchronized_method: bool  (** the procedure is a Java synchronized method *)
   ; is_model: bool  (** the procedure is a model *)
+  ; is_specialized: bool  (** the procedure is a clone specialized for dynamic dispatch handling *)
   ; is_synthetic_method: bool  (** the procedure is a synthetic method *)
   ; language: Config.language  (** language of the procedure *)
   ; loc: Location.t  (** location of this procedure in the source code *)

infer/src/IR/Procdesc.ml

@@ -510,3 +510,7 @@ let pp_signature fmt pdesc =
   if not (Annot.Method.is_empty method_annotation) then
     Format.fprintf fmt ", Annotation: %a" (Annot.Method.pp pname_string) method_annotation ;
   Format.fprintf fmt "]@\n"
+
+let is_specialized pdesc =
+  let attributes = get_attributes pdesc in
+  attributes.ProcAttributes.is_specialized

infer/src/IR/Procdesc.mli

@@ -247,3 +247,5 @@ val signal_did_preanalysis : t -> unit
 val is_loop_head : t -> Node.t -> bool
 
 val pp_signature : Format.formatter -> t -> unit
+
+val is_specialized : t -> bool

infer/src/backend/callbacks.ml

@@ -31,8 +31,8 @@ let procedure_callbacks = ref []
 
 let cluster_callbacks = ref []
 
-let register_procedure_callback language (callback: proc_callback_t) =
+let register_procedure_callback ?(dynamic_dispath= false) language (callback: proc_callback_t) =
-  procedure_callbacks := (language, callback) :: !procedure_callbacks
+  procedure_callbacks := (language, dynamic_dispath, callback) :: !procedure_callbacks
 
 let register_cluster_callback language (callback: cluster_callback_t) =
   cluster_callbacks := (language, callback) :: !cluster_callbacks
@@ -57,9 +57,10 @@ let iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc =
      -> []
   in
   let tenv = Exe_env.get_tenv exe_env proc_name in
+  let is_specialized = Procdesc.is_specialized proc_desc in
   List.fold ~init:summary
-    ~f:(fun summary (language, proc_callback) ->
+    ~f:(fun summary (language, resolved, proc_callback) ->
-      if Config.equal_language language procedure_language then
+      if Config.equal_language language procedure_language && (resolved || not is_specialized) then
         proc_callback {get_proc_desc; get_procs_in_file; tenv; summary; proc_desc}
       else summary)
     !procedure_callbacks

infer/src/backend/callbacks.mli

@@ -30,7 +30,7 @@ type cluster_callback_args =
 
 type cluster_callback_t = cluster_callback_args -> unit
 
-val register_procedure_callback : Config.language -> proc_callback_t -> unit
+val register_procedure_callback : ?dynamic_dispath:bool -> Config.language -> proc_callback_t -> unit
 (** register a procedure callback *)
 
 val register_cluster_callback : Config.language -> cluster_callback_t -> unit

infer/src/checkers/registerCheckers.ml

@@ -17,7 +17,10 @@ module F = Format
 (* make sure SimpleChecker.ml is not dead code *)
 let () = if false then let module SC = SimpleChecker.Make in ()
 
-type callback = Procedure of Callbacks.proc_callback_t | Cluster of Callbacks.cluster_callback_t
+type callback =
+  | Procedure of Callbacks.proc_callback_t
+  | DynamicDispatch of Callbacks.proc_callback_t
+  | Cluster of Callbacks.cluster_callback_t
 
 let checkers =
   [ ( "annotation reachability"
@@ -26,7 +29,7 @@ let checkers =
   ; ( "biabduction"
     , Config.biabduction
     , [ (Procedure Interproc.analyze_procedure, Config.Clang)
-      ; (Procedure Interproc.analyze_procedure, Config.Java) ] )
+      ; (DynamicDispatch Interproc.analyze_procedure, Config.Java) ] )
   ; ( "buffer overrun"
     , Config.bufferoverrun
     , [ (Procedure BufferOverrunChecker.checker, Config.Clang)
@@ -68,6 +71,8 @@ let register () =
       match callback with
       | Procedure procedure_cb
        -> Callbacks.register_procedure_callback language procedure_cb
+      | DynamicDispatch procedure_cb
+       -> Callbacks.register_procedure_callback ~dynamic_dispath:true language procedure_cb
       | Cluster cluster_cb
        -> Callbacks.register_cluster_callback language cluster_cb
     in