diff --git a/infer/src/base/EventLogger.ml b/infer/src/base/EventLogger.ml index 04a3ff7df..bf8c3e643 100644 --- a/infer/src/base/EventLogger.ml +++ b/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 = diff --git a/infer/src/base/EventLogger.mli b/infer/src/base/EventLogger.mli index 75f1eecfc..96ceaf3fc 100644 --- a/infer/src/base/EventLogger.mli +++ b/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 diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index fc7c82678..6526a4402 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/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 *) diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index 9b0c0ab56..80eab1f0b 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/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 diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index cf5a621ff..260bfd7fc 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/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 diff --git a/infer/src/biabduction/Tabulation.mli b/infer/src/biabduction/Tabulation.mli index 480f02d71..15dd77ffb 100644 --- a/infer/src/biabduction/Tabulation.mli +++ b/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