[biabduction] Log the status of using dynamic dispatch

Reviewed By: jeremydubreil

Differential Revision: D8663872

fbshipit-source-id: 8cd23d6

infer/src/base/EventLogger.ml

@@ -129,6 +129,23 @@ let create_analysis_stats_row base record =
   |> add_int ~key:"symops" ~data:record.symops
 
 
+type dynamic_dispatch =
+  | Dynamic_dispatch_successful
+  | Dynamic_dispatch_parameters_arguments_mismatch
+  | Dynamic_dispatch_model_specialization_failure
+
+let string_of_dynamic_dispatch_opt dd =
+  match dd with
+  | Some Dynamic_dispatch_successful ->
+      "dynamic dispatch successful"
+  | Some Dynamic_dispatch_parameters_arguments_mismatch ->
+      "dynamic dispatch failed with arguments mismatch"
+  | Some Dynamic_dispatch_model_specialization_failure ->
+      "dynamic dispatch model specialized failed"
+  | None ->
+      "no dynamic dispatch"
+
+
 type call_trace =
   { call_location: Location.t
   ; call_result: string
@@ -137,7 +154,8 @@ type call_trace =
   ; callee_name: string
   ; caller_name: string
   ; lang: string
-  ; reason: string option }
+  ; reason: string option
+  ; dynamic_dispatch: dynamic_dispatch option }
 
 let create_call_trace_row base record =
   let open JsonBuilder in
@@ -154,6 +172,8 @@ let create_call_trace_row base record =
   |> add_string ~key:"callee_name" ~data:record.callee_name
   |> add_string ~key:"caller_name" ~data:record.caller_name
   |> add_string ~key:"lang" ~data:record.lang |> add_string_opt ~key:"reason" ~data:record.reason
+  |> add_string ~key:"dynamic_dispatch"
+       ~data:(string_of_dynamic_dispatch_opt record.dynamic_dispatch)
 
 
 type frontend_exception =

infer/src/base/EventLogger.mli

@@ -25,6 +25,11 @@ type analysis_stats =
   ; num_preposts: int
   ; symops: int }
 
+type dynamic_dispatch =
+  | Dynamic_dispatch_successful
+  | Dynamic_dispatch_parameters_arguments_mismatch
+  | Dynamic_dispatch_model_specialization_failure
+
 type call_trace =
   { call_location: Location.t
   ; call_result: string
@@ -33,7 +38,8 @@ type call_trace =
   ; callee_name: string
   ; caller_name: string
   ; lang: string
-  ; reason: string option }
+  ; reason: string option
+  ; dynamic_dispatch: dynamic_dispatch option }
 
 type frontend_exception =
   { ast_node: string option

infer/src/biabduction/SymExec.ml

@@ -698,10 +698,16 @@ let resolve_args prop args =
     args
 
 
+type resolve_and_analyze_result =
+  { resolved_pname: Typ.Procname.t
+  ; resolved_procdesc_opt: Procdesc.t option
+  ; resolved_summary_opt: Summary.t option
+  ; dynamic_dispatch_status: EventLogger.dynamic_dispatch option }
+
 (** Resolve the procedure name and run the analysis of the resolved procedure
     if not already analyzed *)
 let resolve_and_analyze tenv ~caller_pdesc ?(has_clang_model= false) prop args callee_proc_name
-    call_flags : Typ.Procname.t * (Procdesc.t option * Summary.t option) =
+    call_flags : resolve_and_analyze_result =
   (* 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 : Procdesc.t option * Summary.t option =
@@ -709,7 +715,7 @@ let resolve_and_analyze tenv ~caller_pdesc ?(has_clang_model= false) prop args c
       ( Ondemand.get_proc_desc callee_proc_name
       , Ondemand.analyze_proc_name ~caller_pdesc callee_proc_name )
     else
-      (* Create the type sprecialized procedure description and analyze it directly *)
+      (* Create the type specialized procedure description and analyze it directly *)
       let analyze specialized_pdesc = Ondemand.analyze_proc_desc ~caller_pdesc specialized_pdesc in
       let resolved_proc_desc_option =
         match Ondemand.get_proc_desc resolved_pname with
@@ -739,7 +745,12 @@ let resolve_and_analyze tenv ~caller_pdesc ?(has_clang_model= false) prop args c
       (resolved_proc_desc_option, Option.bind resolved_proc_desc_option ~f:analyze)
   in
   let resolved_pname = resolve_pname ~caller_pdesc tenv prop args callee_proc_name call_flags in
-  (resolved_pname, analyze_ondemand resolved_pname)
+  let dynamic_dispatch_status =
+    if Typ.Procname.equal callee_proc_name resolved_pname then None
+    else Some EventLogger.Dynamic_dispatch_successful
+  in
+  let resolved_procdesc_opt, resolved_summary_opt = analyze_ondemand resolved_pname in
+  {resolved_pname; resolved_procdesc_opt; resolved_summary_opt; dynamic_dispatch_status}
 
 
 (** recognize calls to the constructor java.net.URL and splits the argument string
@@ -1114,7 +1125,10 @@ let resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_p
   let resolved_summary_opt =
     Ondemand.analyze_proc_name ~caller_pdesc:current_pdesc resolved_pname
   in
-  (resolved_pname, (Ondemand.get_proc_desc resolved_pname, resolved_summary_opt))
+  { resolved_pname
+  ; resolved_procdesc_opt= Ondemand.get_proc_desc resolved_pname
+  ; resolved_summary_opt
+  ; dynamic_dispatch_status= None }
 
 
 let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_pname call_flags =
@@ -1126,7 +1140,7 @@ let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_p
   then
     try
       let has_clang_model = Summary.has_model callee_pname in
-      let resolved_pname, (resolved_pdesc_opt, resolved_summary_opt) =
+      let resolve_and_analyze_result =
         resolve_and_analyze tenv ~caller_pdesc:current_pdesc ~has_clang_model prop_r
           n_actual_params callee_pname call_flags
       in
@@ -1134,7 +1148,7 @@ let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_p
        because we don't have the correct fields in the tenv.
     In that case, default to the non-specialized spec for the model. *)
       let clang_model_specialized_failure =
-        match resolved_summary_opt with
+        match resolve_and_analyze_result.resolved_summary_opt with
         | Some summary when has_clang_model ->
             List.is_empty (Tabulation.get_specs_from_payload summary)
         | None ->
@@ -1143,12 +1157,21 @@ let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_p
             false
       in
       if clang_model_specialized_failure then
+        let result =
+          resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params
+            callee_pname call_flags
+        in
+        { result with
+          dynamic_dispatch_status= Some EventLogger.Dynamic_dispatch_model_specialization_failure
+        }
+      else resolve_and_analyze_result
+    with Procdesc.UnmatchedParameters ->
+      let result =
         resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params
           callee_pname call_flags
-      else (resolved_pname, (resolved_pdesc_opt, resolved_summary_opt))
-    with Procdesc.UnmatchedParameters ->
-      resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params
-        callee_pname call_flags
+      in
+      { result with
+        dynamic_dispatch_status= Some EventLogger.Dynamic_dispatch_parameters_arguments_mismatch }
   else
     resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params callee_pname
       call_flags
@@ -1285,11 +1308,12 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
             skip_call ~reason norm_prop path skipped_pname ret_annots loc ret_id_typ ret_type
               norm_args
           in
-          let resolved_pname, (_, resolved_summary_opt) =
+          let resolve_and_analyze_result =
             resolve_and_analyze tenv ~caller_pdesc:current_pdesc norm_prop norm_args callee_pname
               call_flags
           in
-          match resolved_summary_opt with
+          let resolved_pname = resolve_and_analyze_result.resolved_pname in
+          match resolve_and_analyze_result.resolved_summary_opt with
           | None ->
               let ret_typ = Typ.Procname.Java.get_return_typ callee_pname_java in
               let ret_annots = load_ret_annots callee_pname in
@@ -1351,10 +1375,14 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
                 (call_args prop_r callee_pname n_extended_actual_params ret_id_typ loc)
           | None ->
               (* Generic fun call with known name *)
-              let resolved_pname, (resolved_pdesc_opt, resolved_summary_opt) =
+              let resolve_and_analyze_result =
                 resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_pname
                   call_flags
               in
+              let resolved_pname = resolve_and_analyze_result.resolved_pname in
+              let resolved_pdesc_opt = resolve_and_analyze_result.resolved_procdesc_opt in
+              let resolved_summary_opt = resolve_and_analyze_result.resolved_summary_opt in
+              let dynamic_dispatch_status = resolve_and_analyze_result.dynamic_dispatch_status in
               Logging.d_strln ("Original callee " ^ Typ.Procname.to_unique_id callee_pname) ;
               Logging.d_strln ("Resolved callee " ^ Typ.Procname.to_unique_id resolved_pname) ;
               let sentinel_result =
@@ -1416,7 +1444,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
                         skip_call ~reason prop path resolved_pname ret_annots loc ret_id_typ
                           (snd ret_id_typ) n_actual_params )
                 | None ->
-                    proc_call exe_env
+                    proc_call ?dynamic_dispatch:dynamic_dispatch_status exe_env
                       (Option.value_exn resolved_summary_opt)
                       (call_args prop resolved_pname n_actual_params ret_id_typ loc)
               in
@@ -1825,7 +1853,7 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ pdesc loc prop pa
 
 
 (** Perform symbolic execution for a function call *)
-and proc_call exe_env callee_summary
+and proc_call ?dynamic_dispatch exe_env callee_summary
     {Builtin.pdesc; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} =
   let caller_pname = Procdesc.get_proc_name pdesc in
   let callee_attrs = Summary.get_attributes callee_summary in
@@ -1872,11 +1900,11 @@ and proc_call exe_env callee_summary
   | Language.Clang, ProcAttributes.OBJC_INSTANCE ->
       handle_objc_instance_method_call actual_pars actual_params pre tenv (fst ret_id_typ) pdesc
         callee_pname loc path
-        (Tabulation.exe_function_call exe_env callee_summary)
+        (Tabulation.exe_function_call ?dynamic_dispatch exe_env callee_summary)
   | _ ->
       (* non-objective-c method call. Standard tabulation *)
-      Tabulation.exe_function_call exe_env callee_summary tenv (fst ret_id_typ) pdesc callee_pname
-        loc actual_params pre path
+      Tabulation.exe_function_call ?dynamic_dispatch exe_env callee_summary tenv (fst ret_id_typ)
+        pdesc callee_pname loc actual_params pre path
 
 
 (** perform symbolic execution for a single prop, and check for junk *)

infer/src/biabduction/SymExec.mli

@@ -24,7 +24,8 @@ val instrs :
 val diverge : Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list
 (** Symbolic execution of the divergent pure computation. *)
 
-val proc_call : Exe_env.t -> Summary.t -> Builtin.t
+val proc_call :
+  ?dynamic_dispatch:EventLogger.dynamic_dispatch -> Exe_env.t -> Summary.t -> Builtin.t
 
 val unknown_or_scan_call : is_scan:bool -> reason:string -> Typ.t -> Annot.Item.t -> Builtin.t
 

infer/src/biabduction/Tabulation.ml

@@ -81,7 +81,7 @@ let print_results tenv actual_pre results =
   L.d_strln "***** END RESULTS FUNCTION CALL *******"
 
 
-let log_call_trace ~caller_name ~callee_name ?callee_attributes ?reason loc res =
+let log_call_trace ~caller_name ~callee_name ?callee_attributes ?reason ?dynamic_dispatch loc res =
   let get_valid_source_file loc =
     let file = loc.Location.file in
     if SourceFile.is_invalid file then None else Some file
@@ -108,7 +108,8 @@ let log_call_trace ~caller_name ~callee_name ?callee_attributes ?reason loc res
       ; callee_name= Typ.Procname.to_string callee_name
       ; caller_name= Typ.Procname.to_string caller_name
       ; lang= Typ.Procname.get_language caller_name |> Language.to_explicit_string
-      ; reason }
+      ; reason
+      ; dynamic_dispatch }
   in
   if !Config.footprint then EventLogger.log call_trace
 
@@ -1448,11 +1449,13 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re
 
 
 (** Execute the function call and return the list of results with return value *)
-let exe_function_call exe_env callee_summary tenv ret_id caller_pdesc callee_pname loc
-    actual_params prop path =
+let exe_function_call ?dynamic_dispatch exe_env callee_summary tenv ret_id caller_pdesc
+    callee_pname loc actual_params prop path =
   let callee_attributes = Summary.get_attributes callee_summary in
   let caller_name = Procdesc.get_proc_name caller_pdesc in
-  let trace_call = log_call_trace ~caller_name ~callee_name:callee_pname ~callee_attributes loc in
+  let trace_call =
+    log_call_trace ~caller_name ~callee_name:callee_pname ~callee_attributes ?dynamic_dispatch loc
+  in
   let spec_list, formal_params = spec_find_rename trace_call callee_summary in
   let nspecs = List.length spec_list in
   L.d_strln

infer/src/biabduction/Tabulation.mli

@@ -17,7 +17,8 @@ type call_result =
 
 val log_call_trace :
   caller_name:Typ.Procname.t -> callee_name:Typ.Procname.t -> ?callee_attributes:ProcAttributes.t
-  -> ?reason:string -> Location.t -> call_result -> unit
+  -> ?reason:string -> ?dynamic_dispatch:EventLogger.dynamic_dispatch -> Location.t -> call_result
+  -> unit
 
 (** Interprocedural footprint analysis *)
 
@@ -46,9 +47,9 @@ val lookup_custom_errors : 'a Prop.t -> string option
 (** search in prop contains an error state *)
 
 val exe_function_call :
-  Exe_env.t -> Summary.t -> Tenv.t -> Ident.t -> Procdesc.t -> Typ.Procname.t -> Location.t
-  -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t
-  -> (Prop.normal Prop.t * Paths.Path.t) list
+  ?dynamic_dispatch:EventLogger.dynamic_dispatch -> Exe_env.t -> Summary.t -> Tenv.t -> Ident.t
+  -> Procdesc.t -> Typ.Procname.t -> Location.t -> (Exp.t * Typ.t) list -> Prop.normal Prop.t
+  -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list
 (** Execute the function call and return the list of results with return value *)
 
 val get_specs_from_payload : Summary.t -> Prop.normal BiabductionSummary.spec list