From 2a696e6fb4534889c6f8ec3862a0637db7efbd6e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 6 May 2020 11:23:50 -0700 Subject: [PATCH] make impurity an `intraprocedural_with_field_dependency` Summary: This one needs to read pulse summaries Reviewed By: ezgicicek Differential Revision: D21407070 fbshipit-source-id: d066d9470 --- infer/src/backend/CallbackOfChecker.ml | 27 ++++++++++++++----------- infer/src/backend/CallbackOfChecker.mli | 6 ++++++ infer/src/backend/registerCheckers.ml | 10 +++++++-- infer/src/checkers/impurity.ml | 22 +++++++++----------- infer/src/checkers/impurity.mli | 2 +- 5 files changed, 40 insertions(+), 27 deletions(-) diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 8462c7f91..d62d8999c 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -62,19 +62,22 @@ let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; s {InterproceduralAnalysis.procedures; source_file; file_exe_env= exe_env; analyze_file_dependency} -let intraprocedural checker {Callbacks.summary; exe_env} = - checker - { IntraproceduralAnalysis.proc_desc= Summary.get_proc_desc summary - ; tenv= Exe_env.get_tenv exe_env (Summary.get_proc_name summary) - ; err_log= Summary.get_err_log summary } ; +let to_intraprocedural_t {Callbacks.summary; exe_env} = + { IntraproceduralAnalysis.proc_desc= Summary.get_proc_desc summary + ; tenv= Exe_env.get_tenv exe_env (Summary.get_proc_name summary) + ; err_log= Summary.get_err_log summary } + + +let intraprocedural checker ({Callbacks.summary} as callbacks) = + checker (to_intraprocedural_t callbacks) ; summary -let intraprocedural_with_field payload_field checker {Callbacks.summary; exe_env} = - let result = - checker - { IntraproceduralAnalysis.proc_desc= Summary.get_proc_desc summary - ; tenv= Exe_env.get_tenv exe_env (Summary.get_proc_name summary) - ; err_log= Summary.get_err_log summary } - in +let intraprocedural_with_field_dependency payload_field checker ({Callbacks.summary} as callbacks) = + checker (to_intraprocedural_t callbacks) (Field.get payload_field summary.payloads) ; + summary + + +let intraprocedural_with_field payload_field checker ({Callbacks.summary} as callbacks) = + let result = checker (to_intraprocedural_t callbacks) in {summary with payloads= Field.fset payload_field summary.payloads result} diff --git a/infer/src/backend/CallbackOfChecker.mli b/infer/src/backend/CallbackOfChecker.mli index b2d8a0fc4..ade4165bc 100644 --- a/infer/src/backend/CallbackOfChecker.mli +++ b/infer/src/backend/CallbackOfChecker.mli @@ -39,6 +39,12 @@ val intraprocedural : (IntraproceduralAnalysis.t -> unit) -> Callbacks.proc_call (** runs a simple intra-procedural analysis (one that doesn't need the results of the analysis on any transitive dependencies to analyze a given procedure) *) +val intraprocedural_with_field_dependency : + (Payloads.t, 'payload) Field.t + -> (IntraproceduralAnalysis.t -> 'payload -> unit) + -> Callbacks.proc_callback_t +(** an intra-procedural analysis that depends on the summary payload found by another *) + val intraprocedural_with_field : (Payloads.t, 'payload option) Field.t -> (IntraproceduralAnalysis.t -> 'payload option) diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index 2e1a2b174..cb0e93e6c 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -67,6 +67,10 @@ let intraprocedural_with_payload payload_field checker = Procedure (CallbackOfChecker.intraprocedural_with_field payload_field checker) +let intraprocedural_with_field_dependency payload_field checker = + Procedure (CallbackOfChecker.intraprocedural_with_field_dependency payload_field checker) + + type callback = callback_fun * Language.t type checker = {name: string; active: bool; callbacks: callback list} @@ -159,8 +163,10 @@ let all_checkers = ; { name= "impurity" ; active= Config.is_checker_enabled Impurity ; callbacks= - [(Procedure Impurity.checker, Language.Java); (Procedure Impurity.checker, Language.Clang)] - } + (let impurity = + intraprocedural_with_field_dependency Payloads.Fields.pulse Impurity.checker + in + [(impurity, Language.Java); (impurity, Language.Clang)] ) } ; { name= "printf args" ; active= Config.is_checker_enabled PrintfArgs ; callbacks= [(Procedure PrintfArgs.callback_printf_args, Language.Java)] } diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 26a21cb50..9e0f27c2f 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -161,30 +161,29 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai {modified_globals; modified_params; skipped_calls; exited} -let checker {exe_env; Callbacks.summary} : Summary.t = - let proc_name = Summary.get_proc_name summary in - let pdesc = Summary.get_proc_desc summary in - let pname_loc = Procdesc.get_loc pdesc in - let tenv = Exe_env.get_tenv exe_env proc_name in - ( match summary.payloads.pulse with +let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} pulse_summary_opt = + let proc_name = Procdesc.get_proc_name proc_desc in + let pname_loc = Procdesc.get_loc proc_desc in + let attrs = Procdesc.get_attributes proc_desc in + match pulse_summary_opt with | None -> let impure_fun_desc = F.asprintf "Impure function %a with no pulse summary" Procname.pp proc_name in let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in - SummaryReporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] + Reporting.log_error attrs err_log ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function impure_fun_desc | Some [] -> let impure_fun_desc = F.asprintf "Impure function %a with empty pulse summary" Procname.pp proc_name in let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in - SummaryReporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] + Reporting.log_error attrs err_log ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function impure_fun_desc | Some pre_posts -> let (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as impurity_astate) = List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc exec_state -> - let modified = extract_impurity tenv pdesc exec_state in + let modified = extract_impurity tenv proc_desc exec_state in ImpurityDomain.join acc modified ) in if Purity.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then @@ -209,6 +208,5 @@ let checker {exe_env; Callbacks.summary} : Summary.t = :: modified_ltr Formal modified_params (modified_ltr Global modified_globals skipped_functions) in - SummaryReporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function - impure_fun_desc ) ; - summary + Reporting.log_error attrs err_log ~loc:pname_loc ~ltr IssueType.impure_function + impure_fun_desc diff --git a/infer/src/checkers/impurity.mli b/infer/src/checkers/impurity.mli index c7cb1de60..53a4643c3 100644 --- a/infer/src/checkers/impurity.mli +++ b/infer/src/checkers/impurity.mli @@ -7,5 +7,5 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : IntraproceduralAnalysis.t -> PulseSummary.t option -> unit (** An impurity analysis that relies on pulse summaries to determine how the state changes *)