diff --git a/infer/src/absint/InterproceduralAnalysis.ml b/infer/src/absint/InterproceduralAnalysis.ml index ac74293f2..702dfe4ba 100644 --- a/infer/src/absint/InterproceduralAnalysis.ml +++ b/infer/src/absint/InterproceduralAnalysis.ml @@ -21,3 +21,15 @@ type 'payload file_t = ; procedures: Procname.t list ; file_exe_env: Exe_env.t ; analyze_file_dependency: Procname.t -> (Procdesc.t * 'payload) option } + +let bind_payload ~f analysis_data = + { analysis_data with + analyze_dependency= + (fun proc_name -> + analysis_data.analyze_dependency proc_name + |> Option.bind ~f:(fun (proc_desc, payloads) -> + Option.map (f payloads) ~f:(fun payloads' -> (proc_desc, payloads')) ) ) + ; analyze_pdesc_dependency= + (fun proc_desc -> + analysis_data.analyze_pdesc_dependency proc_desc + |> Option.bind ~f:(fun payloads -> f payloads) ) } diff --git a/infer/src/absint/InterproceduralAnalysis.mli b/infer/src/absint/InterproceduralAnalysis.mli index a0355a19a..006fd4ef0 100644 --- a/infer/src/absint/InterproceduralAnalysis.mli +++ b/infer/src/absint/InterproceduralAnalysis.mli @@ -33,3 +33,5 @@ type 'payload file_t = ; analyze_file_dependency: Procname.t -> (Procdesc.t * 'payload) option (** On-demand analysis of dependencies needed for the file analysis, e.g. the proc names in [procedures] *) } + +val bind_payload : f:('payload1 -> 'payload2 option) -> 'payload1 t -> 'payload2 t diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index ae54ce396..b6822ac76 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -16,16 +16,16 @@ let () = ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes } -let interprocedural payload_field checker {Callbacks.summary; exe_env} = +let interprocedural ~f_analyze_dep ~f_analyze_pdesc_dep ~get_payload ~set_payload checker + {Callbacks.summary; exe_env} = let analyze_dependency proc_name = let summary = Ondemand.analyze_proc_name ~caller_summary:summary proc_name in Option.bind summary ~f:(fun {Summary.payloads; proc_desc; _} -> - Field.get payload_field payloads |> Option.map ~f:(fun payload -> (proc_desc, payload)) ) + f_analyze_dep proc_desc (get_payload payloads) ) in let analyze_pdesc_dependency proc_desc = let summary = Ondemand.analyze_proc_desc ~caller_summary:summary proc_desc in - Option.bind summary ~f:(fun {Summary.payloads; _} -> - Field.get payload_field payloads |> Option.map ~f:(fun payload -> payload) ) + Option.bind summary ~f:(fun {Summary.payloads; _} -> f_analyze_pdesc_dep (get_payload payloads)) in let stats = ref summary.Summary.stats in let update_stats ?add_symops ?failure_kind () = @@ -41,7 +41,15 @@ let interprocedural payload_field checker {Callbacks.summary; exe_env} = ; analyze_pdesc_dependency ; update_stats } in - {summary with payloads= Field.fset payload_field summary.payloads result; stats= !stats} + {summary with payloads= set_payload summary.payloads result; stats= !stats} + + +let interprocedural_with_field payload_field checker = + interprocedural + ~f_analyze_dep:(fun pdesc payload_opt -> + Option.map payload_opt ~f:(fun payload -> (pdesc, payload)) ) + ~f_analyze_pdesc_dep:Fn.id ~get_payload:(Field.get payload_field) + ~set_payload:(Field.fset payload_field) checker let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; source_file} = @@ -54,7 +62,7 @@ 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_with_payload payload_field checker {Callbacks.summary; exe_env} = +let intraprocedural_with_field payload_field checker {Callbacks.summary; exe_env} = let result = checker { IntraproceduralAnalysis.proc_desc= Summary.get_proc_desc summary diff --git a/infer/src/backend/CallbackOfChecker.mli b/infer/src/backend/CallbackOfChecker.mli index 1bb16a5f0..b68fecb64 100644 --- a/infer/src/backend/CallbackOfChecker.mli +++ b/infer/src/backend/CallbackOfChecker.mli @@ -11,6 +11,16 @@ open! IStd {!Callbacks.proc_callback_t} and friends. *) val interprocedural : + f_analyze_dep:(Procdesc.t -> 'payloads_orig -> (Procdesc.t * 'payloads) option) + -> f_analyze_pdesc_dep:('payloads_orig -> 'payloads option) + -> get_payload:(Payloads.t -> 'payloads_orig) + -> set_payload:(Payloads.t -> 'payload_checker -> Payloads.t) + -> ('payloads InterproceduralAnalysis.t -> 'payload_checker) + -> Callbacks.proc_callback_t +(** the general form of interprocedural checkers: can read and update several payloads, and massage + analysis results (mostly used to join option types) *) + +val interprocedural_with_field : (Payloads.t, 'payload option) Field.t -> ('payload InterproceduralAnalysis.t -> 'payload option) -> Callbacks.proc_callback_t @@ -25,7 +35,7 @@ val interprocedural_file : file-level analysis, given an inter-procedural analysis of dependencies that computes the payload type corresponding to [field] *) -val intraprocedural_with_payload : +val intraprocedural_with_field : (Payloads.t, 'payload option) Field.t -> (IntraproceduralAnalysis.t -> 'payload option) -> Callbacks.proc_callback_t diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index b16432fd5..3119efaba 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -24,11 +24,37 @@ type callback_fun = | File of {callback: Callbacks.file_callback_t; issue_dir: ResultsDirEntryName.id} let interprocedural payload_field checker = - Procedure (CallbackOfChecker.interprocedural payload_field checker) + Procedure (CallbackOfChecker.interprocedural_with_field payload_field checker) let dynamic_dispatch payload_field checker = - DynamicDispatch (CallbackOfChecker.interprocedural payload_field checker) + DynamicDispatch (CallbackOfChecker.interprocedural_with_field payload_field checker) + + +(** For checkers that read two separate payloads. Assumes that [checker] produces payloads for + [payload_field1] *) +let interprocedural2 payload_field1 payload_field2 checker = + Procedure + (CallbackOfChecker.interprocedural + ~f_analyze_dep:(fun proc_desc payloads -> Some (proc_desc, payloads)) + ~f_analyze_pdesc_dep:Option.some + ~get_payload:(fun payloads -> + (Field.get payload_field1 payloads, Field.get payload_field2 payloads) ) + ~set_payload:(fun payloads payload1 -> Field.fset payload_field1 payloads payload1) + checker) + + +(** For checkers that read three separate payloads. *) +let interprocedural3 payload_field1 payload_field2 payload_field3 ~set_payload checker = + Procedure + (CallbackOfChecker.interprocedural + ~f_analyze_dep:(fun proc_desc payloads -> Some (proc_desc, payloads)) + ~f_analyze_pdesc_dep:Option.some + ~get_payload:(fun payloads -> + ( Field.get payload_field1 payloads + , Field.get payload_field2 payloads + , Field.get payload_field3 payloads ) ) + ~set_payload checker) let file issue_dir payload_field checker = @@ -36,7 +62,7 @@ let file issue_dir payload_field checker = let intraprocedural_with_payload payload_field checker = - Procedure (CallbackOfChecker.intraprocedural_with_payload payload_field checker) + Procedure (CallbackOfChecker.intraprocedural_with_field payload_field checker) type callback = callback_fun * Language.t @@ -55,7 +81,11 @@ let all_checkers = ; { name= "purity" ; active= Config.(is_checker_enabled Purity || is_checker_enabled LoopHoisting) ; callbacks= - [(Procedure Purity.checker, Language.Java); (Procedure Purity.checker, Language.Clang)] } + (let purity = + interprocedural2 Payloads.Fields.purity Payloads.Fields.buffer_overrun_analysis + Purity.checker + in + [(purity, Language.Java); (purity, Language.Clang)] ) } ; { name= "Starvation analysis" ; active= Config.is_checker_enabled Starvation ; callbacks= @@ -66,15 +96,25 @@ let all_checkers = ; { name= "loop hoisting" ; active= Config.is_checker_enabled LoopHoisting ; callbacks= - [(Procedure Hoisting.checker, Language.Clang); (Procedure Hoisting.checker, Language.Java)] - } + (let hoisting = + interprocedural3 + ~set_payload:(fun payloads () -> + (* this analysis doesn't produce additional payloads *) payloads ) + Payloads.Fields.buffer_overrun_analysis Payloads.Fields.purity Payloads.Fields.cost + Hoisting.checker + in + [(hoisting, Language.Clang); (hoisting, Language.Java)] ) } ; { name= "cost analysis" ; active= Config.( is_checker_enabled Cost || (is_checker_enabled LoopHoisting && hoisting_report_only_expensive)) - ; callbacks= [(Procedure Cost.checker, Language.Clang); (Procedure Cost.checker, Language.Java)] - } + ; callbacks= + (let checker = + interprocedural3 ~set_payload:(Field.fset Payloads.Fields.cost) Payloads.Fields.cost + Payloads.Fields.buffer_overrun_analysis Payloads.Fields.purity Cost.checker + in + [(checker, Language.Clang); (checker, Language.Java)] ) } ; { name= "uninitialized variables" ; active= Config.is_checker_enabled Uninit ; callbacks= [(Procedure Uninit.checker, Language.Clang)] } @@ -143,25 +183,30 @@ let all_checkers = ; { name= "buffer overrun checker" ; active= Config.(is_checker_enabled BufferOverrun) ; callbacks= - [ (Procedure BufferOverrunChecker.checker, Language.Clang) - ; (Procedure BufferOverrunChecker.checker, Language.Java) ] } + (let bo_checker = + interprocedural2 Payloads.Fields.buffer_overrun_checker + Payloads.Fields.buffer_overrun_analysis BufferOverrunChecker.checker + in + [(bo_checker, Language.Clang); (bo_checker, Language.Java)] ) } ; { name= "buffer overrun analysis" ; active= Config.( is_checker_enabled BufferOverrun || is_checker_enabled Cost || is_checker_enabled LoopHoisting || is_checker_enabled Purity) ; callbacks= - [ (Procedure BufferOverrunAnalysis.do_analysis, Language.Clang) - ; (Procedure BufferOverrunAnalysis.do_analysis, Language.Java) ] } + (let bo_analysis = + interprocedural Payloads.Fields.buffer_overrun_analysis + BufferOverrunAnalysis.analyze_procedure + in + [(bo_analysis, Language.Clang); (bo_analysis, Language.Java)] ) } ; { name= "biabduction" ; active= Config.is_checker_enabled Biabduction ; callbacks= - [ ( dynamic_dispatch Payloads.Fields.biabduction - (Topl.instrument_callback Interproc.analyze_procedure) - , Language.Clang ) - ; ( dynamic_dispatch Payloads.Fields.biabduction - (Topl.instrument_callback Interproc.analyze_procedure) - , Language.Java ) ] } + (let biabduction = + dynamic_dispatch Payloads.Fields.biabduction + (Topl.instrument_callback Interproc.analyze_procedure) + in + [(biabduction, Language.Clang); (biabduction, Language.Java)] ) } ; { name= "annotation reachability" ; active= Config.is_checker_enabled AnnotationReachability ; callbacks= diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 5f20b7fa1..d80e8615c 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -19,23 +19,18 @@ module OndemandEnv = BufferOverrunOndemandEnv module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace -module Payload = SummaryPayload.Make (struct - type t = BufferOverrunAnalysisSummary.t - - let field = Payloads.Fields.buffer_overrun_analysis -end) - -type extras = - { get_summary: BufferOverrunAnalysisSummary.get_summary +type analysis_data = + { analysis_data: BufferOverrunAnalysisSummary.t InterproceduralAnalysis.t + ; get_summary: BufferOverrunAnalysisSummary.get_summary ; get_formals: BoUtils.get_formals ; oenv: OndemandEnv.t } module CFG = ProcCfg.NormalOneInstrPerNode module Init = struct - let initial_state {ProcData.summary; tenv; extras= {get_summary; oenv}} start_node = + let initial_state {analysis_data= {proc_desc; tenv}; get_summary; oenv} start_node = let try_decl_local = - let pname = Summary.get_proc_name summary in + let pname = Procdesc.get_proc_name proc_desc in let model_env = let node_hash = CFG.Node.hash start_node in let location = CFG.Node.loc start_node in @@ -47,10 +42,7 @@ module Init = struct BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ) in let mem = Dom.Mem.init get_summary oenv in - let mem, _ = - List.fold ~f:try_decl_local ~init:(mem, 1) - (Procdesc.get_locals (Summary.get_proc_desc summary)) - in + let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals proc_desc) in mem end @@ -58,7 +50,7 @@ module TransferFunctions = struct module CFG = CFG module Domain = Dom.Mem - type analysis_data = extras ProcData.t + type nonrec analysis_data = analysis_data let instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location mem = match @@ -292,9 +284,9 @@ module TransferFunctions = struct Dom.Mem.add_unknown ret ~location mem - let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = - fun mem {summary; tenv; extras= {get_summary; get_formals; oenv= {integer_type_widths}}} node - instr -> + let exec_instr : Dom.Mem.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = + fun mem {analysis_data= {proc_desc; tenv}; get_summary; get_formals; oenv= {integer_type_widths}} + node instr -> match instr with | Load {id} when Ident.is_none id -> mem @@ -310,7 +302,7 @@ module TransferFunctions = struct Dom.Mem.find_set locs callee_mem ) | Load {id; e= exp; typ; loc= location} -> ( let model_env = - let pname = Summary.get_proc_name summary in + let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths in @@ -330,7 +322,7 @@ module TransferFunctions = struct Dom.Mem.exc_raised | Store {e1= tgt_exp; e2= Const (Const.Cstr _) as src; loc= location} when Language.curr_language_is Java -> - let pname = Summary.get_proc_name summary in + let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in let model_env = BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths @@ -348,7 +340,7 @@ module TransferFunctions = struct | Store {e1= exp1; e2= Const (Const.Cstr s); loc= location} -> let locs = Sem.eval_locs exp1 mem in let model_env = - let pname = Summary.get_proc_name summary in + let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths in @@ -379,7 +371,8 @@ module TransferFunctions = struct | Call ((id, _), Const (Cfun callee_pname), _, _, _) when is_java_enum_values tenv callee_pname -> let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in - assign_java_enum_values get_summary id ~caller_pname:(Summary.get_proc_name summary) + assign_java_enum_values get_summary id + ~caller_pname:(Procdesc.get_proc_name proc_desc) ~callee_pname mem | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> ( let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in @@ -416,7 +409,7 @@ module TransferFunctions = struct Dom.Mem.add_unknown ret ~location mem | Metadata (VariableLifetimeBegins (pvar, typ, location)) when Pvar.is_global pvar -> let model_env = - let pname = Summary.get_proc_name summary in + let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths in @@ -444,38 +437,32 @@ let extract_post = Analyzer.extract_post let extract_state = Analyzer.extract_state let compute_invariant_map : - Summary.t - -> Tenv.t - -> Typ.IntegerWidths.t - -> BufferOverrunAnalysisSummary.get_summary - -> BoUtils.get_formals - -> invariant_map = - fun summary tenv integer_type_widths get_summary get_formals -> - let pdesc = Summary.get_proc_desc summary in - let cfg = CFG.from_pdesc pdesc in - let pdata = - let oenv = OndemandEnv.mk pdesc tenv integer_type_widths in - {ProcData.summary; tenv; extras= {get_summary; get_formals; oenv}} + BufferOverrunAnalysisSummary.t InterproceduralAnalysis.t -> invariant_map = + fun ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependency} as analysis_data) -> + let cfg = CFG.from_pdesc proc_desc in + let extras = + let proc_name = Procdesc.get_proc_name proc_desc in + let get_summary proc_name = analyze_dependency proc_name |> Option.map ~f:snd in + let get_formals callee_pname = + AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals + in + let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in + let oenv = OndemandEnv.mk proc_desc tenv integer_type_widths in + {analysis_data; get_summary; get_formals; oenv} in - let initial = Init.initial_state pdata (CFG.start_node cfg) in - Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata pdesc + let initial = Init.initial_state extras (CFG.start_node cfg) in + Analyzer.exec_pdesc ~do_narrowing:true ~initial extras proc_desc let cached_compute_invariant_map = let cache_get, cache_set = Procname.UnitCache.create () in - fun summary tenv integer_type_widths -> - let pname = Summary.get_proc_name summary in + fun ({InterproceduralAnalysis.proc_desc} as analysis_data) -> + let pname = Procdesc.get_proc_name proc_desc in match cache_get pname with | Some inv_map -> inv_map | None -> - let get_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in - let get_formals callee_pname = - Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals - in - let inv_map = - compute_invariant_map summary tenv integer_type_widths get_summary get_formals - in + let inv_map = compute_invariant_map analysis_data in cache_set pname inv_map ; inv_map @@ -489,14 +476,8 @@ let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_ Unreachable -let do_analysis : Callbacks.proc_callback_args -> Summary.t = - fun {exe_env; summary} -> - let proc_desc = Summary.get_proc_desc summary in - let proc_name = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env proc_name in - let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in - let inv_map = cached_compute_invariant_map summary tenv integer_type_widths in +let analyze_procedure ({InterproceduralAnalysis.proc_desc} as analysis_data) = + let inv_map = cached_compute_invariant_map analysis_data in let formals = Procdesc.get_pvar_formals proc_desc in let cfg = CFG.from_pdesc proc_desc in - let payload = compute_summary formals cfg inv_map in - Payload.update_summary payload summary + Some (compute_summary formals cfg inv_map) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli index d79cabf5f..f91bbd236 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli @@ -10,7 +10,8 @@ module CFG = ProcCfg.NormalOneInstrPerNode type invariant_map -val cached_compute_invariant_map : Summary.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map +val cached_compute_invariant_map : + BufferOverrunAnalysisSummary.t InterproceduralAnalysis.t -> invariant_map val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option @@ -19,4 +20,5 @@ val extract_post : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t opt val extract_state : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t AbstractInterpreter.State.t option -val do_analysis : Callbacks.proc_callback_t +val analyze_procedure : + BufferOverrunAnalysisSummary.t InterproceduralAnalysis.t -> BufferOverrunAnalysisSummary.t option diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index e00f27c96..345ee42c8 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -19,16 +19,11 @@ module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace -module Payload = SummaryPayload.Make (struct - type t = BufferOverrunCheckerSummary.t - - let field = Payloads.Fields.buffer_overrun_checker -end) - module UnusedBranch = struct type t = {node: CFG.Node.t; location: Location.t; condition: Exp.t; true_branch: bool} - let report tenv summary {node; location; condition; true_branch} = + let report {InterproceduralAnalysis.proc_desc; tenv; err_log} + {node; location; condition; true_branch} = let desc = let err_desc = let i = match condition with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in @@ -41,7 +36,8 @@ module UnusedBranch = struct if true_branch then IssueType.condition_always_false else IssueType.condition_always_true in let ltr = [Errlog.make_trace_element 0 location "Here" []] in - SummaryReporting.log_warning summary ~loc:location ~ltr issue_type desc + let attrs = Procdesc.get_attributes proc_desc in + Reporting.log_warning attrs err_log ~loc:location ~ltr issue_type desc end module UnusedBranches = struct @@ -49,16 +45,17 @@ module UnusedBranches = struct let empty = [] - let report tenv summary unused_branches = - List.iter unused_branches ~f:(UnusedBranch.report tenv summary) + let report analysis_data unused_branches = + List.iter unused_branches ~f:(UnusedBranch.report analysis_data) end module UnreachableStatement = struct type t = {location: Location.t} - let report summary {location} = + let report {InterproceduralAnalysis.proc_desc; err_log} {location} = let ltr = [Errlog.make_trace_element 0 location "Here" []] in - SummaryReporting.log_error summary ~loc:location ~ltr IssueType.unreachable_code_after + let attrs = Procdesc.get_attributes proc_desc in + Reporting.log_error attrs err_log ~loc:location ~ltr IssueType.unreachable_code_after "Unreachable code after statement" end @@ -67,8 +64,8 @@ module UnreachableStatements = struct let empty = [] - let report summary unreachable_statements = - List.iter unreachable_statements ~f:(UnreachableStatement.report summary) + let report analysis_data unreachable_statements = + List.iter unreachable_statements ~f:(UnreachableStatement.report analysis_data) end module Checks = struct @@ -399,10 +396,10 @@ let compute_checks : ~init:Checks.empty -let report_errors : Tenv.t -> checks -> Summary.t -> unit = - fun tenv {cond_set; unused_branches; unreachable_statements} summary -> - UnusedBranches.report tenv summary unused_branches ; - UnreachableStatements.report summary unreachable_statements ; +let report_errors ({InterproceduralAnalysis.proc_desc; err_log} as analysis_data) + {Checks.cond_set; unused_branches; unreachable_statements} = + UnusedBranches.report analysis_data unused_branches ; + UnreachableStatements.report analysis_data unreachable_statements ; let report cond trace issue_type = let location = PO.ConditionTrace.get_report_location trace in let description ~markup = PO.description ~markup cond trace in @@ -411,8 +408,8 @@ let report_errors : Tenv.t -> checks -> Summary.t -> unit = Trace.Issue.make_err_trace ~description (PO.ConditionTrace.get_val_traces trace) |> Errlog.concat_traces in - SummaryReporting.log_error summary ~loc:location ~ltr:trace issue_type - (description ~markup:true) + let attrs = Procdesc.get_attributes proc_desc in + Reporting.log_error attrs err_log ~loc:location ~ltr:trace issue_type (description ~markup:true) in PO.ConditionSet.report_errors ~report cond_set @@ -425,26 +422,27 @@ let get_checks_summary : checks -> checks_summary = PO.ConditionSet.for_summary cond_set -let checker : Callbacks.proc_callback_args -> Summary.t = - fun {exe_env; summary} -> - let proc_desc = Summary.get_proc_desc summary in - let proc_name = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env proc_name in +let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependency} as analysis_data) + = + let proc_name = Procdesc.get_proc_name proc_desc in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in let inv_map = - BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths + BufferOverrunAnalysis.cached_compute_invariant_map + (InterproceduralAnalysis.bind_payload analysis_data ~f:snd) in let underlying_exit_node = Procdesc.get_exit_node proc_desc in let pp_name f = F.pp_print_string f "bufferoverrun check" in NodePrinter.with_session ~pp_name underlying_exit_node ~f:(fun () -> let cfg = CFG.from_pdesc proc_desc in let checks = - let get_checks_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in + let get_checks_summary callee_pname = + analyze_dependency callee_pname + |> Option.bind ~f:(fun (_, (checker_summary, _analysis_summary)) -> checker_summary) + in let get_formals callee_pname = Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals in compute_checks get_checks_summary get_formals proc_name tenv integer_type_widths cfg inv_map in - report_errors tenv checks summary ; - let cond_set = get_checks_summary checks in - Payload.update_summary cond_set summary ) + report_errors analysis_data checks ; + Some (get_checks_summary checks) ) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index 489676eb8..85d1ff098 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/infer/src/bufferoverrun/bufferOverrunChecker.mli @@ -7,4 +7,7 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + (BufferOverrunCheckerSummary.t option * BufferOverrunAnalysisSummary.t option) + InterproceduralAnalysis.t + -> BufferOverrunCheckerSummary.t option diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index ee86963d9..d31eb054e 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -56,7 +56,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ControlDepSet - type analysis_data = loop_control_maps ProcData.t + type analysis_data = loop_control_maps let collect_vars_in_exp exp loop_head = Var.get_all_vars_in_exp exp @@ -117,8 +117,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct along with the loop header that CV is originating from - a loop exit node, remove control variables of its guard nodes This is correct because the CVs are only going to be temporaries. *) - let exec_instr astate {ProcData.extras= {exit_map; loop_head_to_guard_nodes}} (node : CFG.Node.t) - _ = + let exec_instr astate {exit_map; loop_head_to_guard_nodes} (node : CFG.Node.t) _ = let node = CFG.Node.underlying_node node in let astate' = match LoopHeadToGuardNodes.find_opt node loop_head_to_guard_nodes with @@ -159,10 +158,9 @@ module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsContro type invariant_map = ControlDepAnalyzer.invariant_map -let compute_invariant_map summary tenv control_maps : invariant_map = - let proc_data = {ProcData.summary; tenv; extras= control_maps} in - let node_cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in - ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:ControlDepSet.empty +let compute_invariant_map proc_desc control_maps : invariant_map = + let node_cfg = CFG.from_pdesc proc_desc in + ControlDepAnalyzer.exec_cfg node_cfg control_maps ~initial:ControlDepSet.empty (* Filter CVs which are invariant in the loop where the CV originated from *) diff --git a/infer/src/checkers/control.mli b/infer/src/checkers/control.mli index 7e136d7e7..d0e1e455e 100644 --- a/infer/src/checkers/control.mli +++ b/infer/src/checkers/control.mli @@ -26,7 +26,7 @@ type loop_control_maps = { exit_map: LoopHeads.t ExitNodeToLoopHeads.t ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t } -val compute_invariant_map : Summary.t -> Tenv.t -> loop_control_maps -> invariant_map +val compute_invariant_map : Procdesc.t -> loop_control_maps -> invariant_map val compute_control_vars : invariant_map diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index 33db54b9f..5a365acef 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -70,7 +70,8 @@ let get_hoist_inv_map tenv ~get_callee_purity reaching_defs_invariant_map loop_h loop_head_to_source_nodes LoopHeadToHoistInstrs.empty -let do_report extract_cost_if_expensive summary (Call.{pname; loc} as call) loop_head_loc = +let do_report extract_cost_if_expensive proc_attrs err_log (Call.{pname; loc} as call) loop_head_loc + = let exp_desc = F.asprintf "The call to %a at %a is loop-invariant" Procname.pp pname Location.pp loc in @@ -95,7 +96,7 @@ let do_report extract_cost_if_expensive summary (Call.{pname; loc} as call) loop F.asprintf "%s%s. It can be moved out of the loop at %a." exp_desc cost_msg Location.pp loop_head_loc in - SummaryReporting.log_error summary ~loc ~ltr issue message + Reporting.log_error proc_attrs err_log ~loc ~ltr issue message let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_formals @@ -132,8 +133,8 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f Option.filter cost_opt ~f:CostDomain.BasicCost.is_symbolic -let report_errors proc_desc tenv get_callee_purity reaching_defs_invariant_map - loop_head_to_source_nodes extract_cost_if_expensive summary = +let report_errors proc_desc tenv err_log get_callee_purity reaching_defs_invariant_map + loop_head_to_source_nodes extract_cost_if_expensive = (* get dominators *) let idom = Dominators.get_idoms proc_desc in (* get a map, loop head -> instrs that can be hoisted out of the loop *) @@ -148,41 +149,43 @@ let report_errors proc_desc tenv get_callee_purity reaching_defs_invariant_map (fun loop_head inv_instrs -> let loop_head_loc = Procdesc.Node.get_loc loop_head in HoistCalls.iter - (fun call -> do_report extract_cost_if_expensive summary call loop_head_loc) + (fun call -> + let proc_attrs = Procdesc.get_attributes proc_desc in + do_report extract_cost_if_expensive proc_attrs err_log call loop_head_loc ) inv_instrs ) loop_head_to_inv_instrs -let checker Callbacks.{summary; exe_env} : Summary.t = - let proc_desc = Summary.get_proc_desc summary in - let proc_name = Summary.get_proc_name summary in +let checker + ({InterproceduralAnalysis.proc_desc; exe_env; err_log; analyze_dependency} as analysis_data) = + let proc_name = Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in let cfg = InstrCFG.from_pdesc proc_desc in (* computes reaching defs: node -> (var -> node set) *) - let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map summary tenv in + let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc in let loop_head_to_source_nodes = Loop_control.get_loop_head_to_source_nodes cfg in let extract_cost_if_expensive = if Config.hoisting_report_only_expensive then let inferbo_invariant_map = - BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths + BufferOverrunAnalysis.cached_compute_invariant_map + (InterproceduralAnalysis.bind_payload ~f:fst3 analysis_data) in let get_callee_cost_summary_and_formals callee_pname = - Cost.Payload.read_full ~caller_summary:summary ~callee_pname - |> Option.map ~f:(fun (callee_pdesc, callee_summary) -> - (callee_summary, Procdesc.get_pvar_formals callee_pdesc) ) + analyze_dependency callee_pname + |> Option.bind ~f:(function + | callee_pdesc, (_inferbo, _purity, Some callee_costs_summary) -> + Some (callee_costs_summary, Procdesc.get_pvar_formals callee_pdesc) + | _, (_, _, None) -> + None ) in get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_formals inferbo_invariant_map else fun _ -> None in let get_callee_purity callee_pname = - match Ondemand.analyze_proc_name ~caller_summary:summary callee_pname with - | Some {Summary.payloads= {Payloads.purity}} -> - purity - | _ -> - None + match analyze_dependency callee_pname with Some (_, (_, purity, _)) -> purity | _ -> None in - report_errors proc_desc tenv get_callee_purity reaching_defs_invariant_map - loop_head_to_source_nodes extract_cost_if_expensive summary ; - summary + report_errors proc_desc tenv err_log get_callee_purity reaching_defs_invariant_map + loop_head_to_source_nodes extract_cost_if_expensive ; + () diff --git a/infer/src/checkers/hoisting.mli b/infer/src/checkers/hoisting.mli index 489676eb8..3db9e952e 100644 --- a/infer/src/checkers/hoisting.mli +++ b/infer/src/checkers/hoisting.mli @@ -7,4 +7,9 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + ( BufferOverrunAnalysisSummary.t option + * PurityDomain.ModifiedParamIndices.t AbstractDomain.Types.top_lifted option + * CostDomain.summary option ) + InterproceduralAnalysis.t + -> unit diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index f51106a37..5ad85f3dd 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -4,24 +4,20 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd module F = Format module L = Logging module ModifiedVarSet = PrettyPrintable.MakePPSet (Var) module InstrCFG = ProcCfg.NormalOneInstrPerNode -let debug fmt = L.(debug Analysis Verbose fmt) +let debug fmt = L.debug Analysis Verbose fmt (* A simple purity checker *) -module Payload = SummaryPayload.Make (struct - type t = PurityDomain.summary - - let field = Payloads.Fields.purity -end) - -type purity_extras = - { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map +type analysis_data = + { tenv: Tenv.t + ; inferbo_invariant_map: BufferOverrunAnalysis.invariant_map ; formals: Var.t list ; get_callee_summary: Procname.t -> PurityDomain.summary option } @@ -29,7 +25,7 @@ module TransferFunctions = struct module CFG = ProcCfg.Normal module Domain = PurityDomain - type analysis_data = purity_extras ProcData.t + type nonrec analysis_data = analysis_data let get_alias_set inferbo_mem var = let default = ModifiedVarSet.empty in @@ -145,8 +141,7 @@ module TransferFunctions = struct let modified_global ae = HilExp.AccessExpression.get_base ae |> fst |> Var.is_global - let exec_instr (astate : Domain.t) - {tenv; ProcData.extras= {inferbo_invariant_map; formals; get_callee_summary}} + let exec_instr (astate : Domain.t) {tenv; inferbo_invariant_map; formals; get_callee_summary} (node : CFG.Node.t) (instr : HilInstr.t) = let (node_id : InstrCFG.Node.id) = CFG.Node.underlying_node node |> InstrCFG.last_of_underlying_node |> InstrCFG.Node.id @@ -198,47 +193,41 @@ let should_report proc_name = false ) -let report_errors astate summary = - let pdesc = Summary.get_proc_desc summary in - let proc_name = Procdesc.get_proc_name pdesc in - match astate with +let report_errors {InterproceduralAnalysis.proc_desc; err_log} astate_opt = + let proc_name = Procdesc.get_proc_name proc_desc in + match astate_opt with | Some astate -> if should_report proc_name && PurityDomain.is_pure astate then - let loc = Procdesc.get_loc pdesc in + let loc = Procdesc.get_loc proc_desc in let exp_desc = F.asprintf "Side-effect free function %a" Procname.pp proc_name in let ltr = [Errlog.make_trace_element 0 loc exp_desc []] in - SummaryReporting.log_error summary ~loc ~ltr IssueType.pure_function exp_desc + let attrs = Procdesc.get_attributes proc_desc in + Reporting.log_error attrs err_log ~loc ~ltr IssueType.pure_function exp_desc | None -> L.internal_error "Analyzer failed to compute purity information for %a@." Procname.pp proc_name -let compute_summary summary tenv get_callee_summary inferbo_invariant_map = - let proc_name = Summary.get_proc_name summary in - let proc_desc = Summary.get_proc_desc summary in +let compute_summary {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency} + inferbo_invariant_map = + let proc_name = Procdesc.get_proc_name proc_desc in let formals = Procdesc.get_formals proc_desc |> List.map ~f:(fun (mname, _) -> Var.of_pvar (Pvar.mk mname proc_name)) in - let proc_data = - {ProcData.summary; tenv; extras= {inferbo_invariant_map; formals; get_callee_summary}} + let get_callee_summary callee_pname = + analyze_dependency callee_pname |> Option.bind ~f:(fun (_, (purity_opt, _)) -> purity_opt) in - Analyzer.compute_post proc_data ~initial:PurityDomain.pure proc_desc + let analysis_data = {tenv; inferbo_invariant_map; formals; get_callee_summary} in + Analyzer.compute_post analysis_data ~initial:PurityDomain.pure proc_desc -let checker {Callbacks.exe_env; summary} : Summary.t = - let proc_name = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env proc_name in - let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in +let checker analysis_data = let inferbo_invariant_map = - BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths + BufferOverrunAnalysis.cached_compute_invariant_map + (InterproceduralAnalysis.bind_payload ~f:snd analysis_data) in - let get_callee_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in - let astate = compute_summary summary tenv get_callee_summary inferbo_invariant_map in - report_errors astate summary ; - match astate with - | Some astate -> - debug "Purity summary :%a \n" PurityDomain.pp astate ; - Payload.update_summary astate summary - | None -> - summary + let astate_opt = compute_summary analysis_data inferbo_invariant_map in + report_errors analysis_data astate_opt ; + Option.iter astate_opt ~f:(fun astate -> debug "Purity summary :%a \n" PurityDomain.pp astate) ; + astate_opt diff --git a/infer/src/checkers/purity.mli b/infer/src/checkers/purity.mli index 144e8f209..0de65b24c 100644 --- a/infer/src/checkers/purity.mli +++ b/infer/src/checkers/purity.mli @@ -7,6 +7,8 @@ open! IStd -val checker : Callbacks.proc_callback_t +val checker : + (PurityDomain.summary option * BufferOverrunAnalysisSummary.t option) InterproceduralAnalysis.t + -> PurityDomain.summary option val should_report : Procname.t -> bool diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index aae35d037..61ee86d86 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -24,10 +24,10 @@ module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ReachingDefsMap - type analysis_data = unit ProcData.t + type analysis_data = unit (* for each x := e at node n, remove x's definitions and introduce x -> n *) - let exec_instr astate _ (node : CFG.Node.t) instr = + let exec_instr astate () (node : CFG.Node.t) instr = let node = CFG.Node.underlying_node node in let strong_update_def astate var = Domain.add var (Defs.singleton node) astate in let weak_update_def astate var = @@ -68,11 +68,9 @@ module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctionsReachingDefs (No type invariant_map = Analyzer.invariant_map -let compute_invariant_map summary tenv = - let pdesc = Summary.get_proc_desc summary in - let proc_data = {ProcData.summary; tenv; extras= ()} in - let node_cfg = NodeCFG.from_pdesc pdesc in - Analyzer.exec_cfg node_cfg proc_data ~initial:(init_reaching_defs_with_formals pdesc) +let compute_invariant_map proc_desc = + let node_cfg = NodeCFG.from_pdesc proc_desc in + Analyzer.exec_cfg node_cfg () ~initial:(init_reaching_defs_with_formals proc_desc) let extract_post = Analyzer.extract_post diff --git a/infer/src/checkers/reachingDefs.mli b/infer/src/checkers/reachingDefs.mli index 42bee00d5..7aa6bceb6 100644 --- a/infer/src/checkers/reachingDefs.mli +++ b/infer/src/checkers/reachingDefs.mli @@ -18,6 +18,6 @@ module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs) type invariant_map -val compute_invariant_map : Summary.t -> Tenv.t -> invariant_map +val compute_invariant_map : Procdesc.t -> invariant_map val extract_post : Procdesc.Node.id -> invariant_map -> ReachingDefsMap.t option diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 087524bd3..9676f1453 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -15,12 +15,6 @@ module InstrCFG = ProcCfg.NormalOneInstrPerNode module NodeCFG = ProcCfg.Normal module Node = ProcCfg.DefaultNode -module Payload = SummaryPayload.Make (struct - type t = CostDomain.summary - - let field = Payloads.Fields.cost -end) - type extras_WorstCaseCost = { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map ; integer_type_widths: Typ.IntegerWidths.t @@ -242,8 +236,8 @@ let is_report_suppressed pname = module Check = struct - let report_threshold pname summary ~name ~location ~cost CostIssues.{expensive_issue} ~threshold - ~is_on_ui_thread = + let report_threshold pname attrs err_log ~name ~location ~cost CostIssues.{expensive_issue} + ~threshold ~is_on_ui_thread = let report_issue_type = L.(debug Analysis Medium) "@\n\n++++++ Checking error type for %a **** @\n" Procname.pp pname ; let is_on_cold_start = ExternalPerfData.in_profiler_data_map pname in @@ -267,18 +261,18 @@ module Check = struct in Errlog.make_trace_element 0 location cost_desc [] in - SummaryReporting.log_error summary ~loc:location + Reporting.log_error attrs err_log ~loc:location ~ltr:(cost_trace_elem :: BasicCost.polynomial_traces cost) ~extras:(compute_errlog_extras cost) report_issue_type message - let report_top_and_unreachable pname loc summary ~name ~cost - CostIssues.{unreachable_issue; infinite_issue} = + let report_top_and_unreachable pname attrs err_log loc ~name ~cost + {CostIssues.unreachable_issue; infinite_issue} = let report issue suffix = let message = F.asprintf "%s of the function %a %s" name Procname.pp pname suffix in - SummaryReporting.log_error ~loc + Reporting.log_error attrs err_log ~loc ~ltr:(BasicCost.polynomial_traces cost) - ~extras:(compute_errlog_extras cost) summary issue message + ~extras:(compute_errlog_extras cost) issue message in if BasicCost.is_top cost then report infinite_issue "cannot be computed" else if BasicCost.is_unreachable cost then @@ -286,7 +280,8 @@ module Check = struct "cannot be computed since the program's exit state is never reachable" - let check_and_report ~is_on_ui_thread WorstCaseCost.{costs; reports} proc_desc summary = + let check_and_report {InterproceduralAnalysis.proc_desc; err_log} ~is_on_ui_thread + {WorstCaseCost.costs; reports} = let pname = Procdesc.get_proc_name proc_desc in let proc_loc = Procdesc.get_loc proc_desc in if not (is_report_suppressed pname) then ( @@ -295,12 +290,16 @@ module Check = struct | ThresholdReports.Threshold _ | ThresholdReports.NoReport -> () | ThresholdReports.ReportOn {location; cost} -> - report_threshold pname summary ~name ~location ~cost kind_spec - ~threshold:(Option.value_exn threshold) ~is_on_ui_thread ) ; + report_threshold pname + (Procdesc.get_attributes proc_desc) + err_log ~name ~location ~cost kind_spec ~threshold:(Option.value_exn threshold) + ~is_on_ui_thread ) ; CostIssues.CostKindMap.iter2 CostIssues.enabled_cost_map costs ~f:(fun _kind (CostIssues.{name; top_and_unreachable} as issue_spec) cost -> if top_and_unreachable then - report_top_and_unreachable pname proc_loc summary ~name ~cost issue_spec ) ) + report_top_and_unreachable pname + (Procdesc.get_attributes proc_desc) + err_log proc_loc ~name ~cost issue_spec ) ) end type bound_map = BasicCost.t Node.IdMap.t @@ -340,36 +339,28 @@ let compute_worst_case_cost tenv integer_type_widths get_summary get_formals ins let get_cost_summary ~is_on_ui_thread astate = - CostDomain.{post= astate.WorstCaseCost.costs; is_on_ui_thread} - - -let report_errors ~is_on_ui_thread proc_desc astate summary = - Check.check_and_report ~is_on_ui_thread astate proc_desc summary + {CostDomain.post= astate.WorstCaseCost.costs; is_on_ui_thread} -let checker {Callbacks.exe_env; summary} : Summary.t = - let proc_name = Summary.get_proc_name summary in +let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as analysis_data) = + let proc_name = Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in - let proc_desc = Summary.get_proc_desc summary in let inferbo_invariant_map = - BufferOverrunAnalysis.cached_compute_invariant_map summary tenv integer_type_widths + BufferOverrunAnalysis.cached_compute_invariant_map + (InterproceduralAnalysis.bind_payload ~f:snd3 analysis_data) in let node_cfg = NodeCFG.from_pdesc proc_desc in (* computes reaching defs: node -> (var -> node set) *) - let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map summary tenv in + let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc in (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) let control_maps, loop_head_to_loop_nodes = Loop_control.get_loop_control_maps node_cfg in (* computes the control dependencies: node -> var set *) - let control_dep_invariant_map = Control.compute_invariant_map summary tenv control_maps in + let control_dep_invariant_map = Control.compute_invariant_map proc_desc control_maps in (* compute loop invariant map for control var analysis *) let loop_inv_map = let get_callee_purity callee_pname = - match Ondemand.analyze_proc_name ~caller_summary:summary callee_pname with - | Some {Summary.payloads= {Payloads.purity}} -> - purity - | _ -> - None + match analyze_dependency callee_pname with Some (_, (_, _, purity)) -> purity | _ -> None in LoopInvariant.get_loop_inv_var_map tenv get_callee_purity reaching_defs_invariant_map loop_head_to_loop_nodes @@ -381,7 +372,13 @@ let checker {Callbacks.exe_env; summary} : Summary.t = let is_on_ui_thread = ConcurrencyModels.runs_on_ui_thread tenv proc_name in let get_node_nb_exec = compute_get_node_nb_exec node_cfg bound_map in let astate = - let get_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in + let get_summary callee_pname = + match analyze_dependency callee_pname with + | Some (_, (payload, _, _)) -> + payload + | None -> + None + in let get_formals callee_pname = Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals in @@ -397,5 +394,5 @@ let checker {Callbacks.exe_env; summary} : Summary.t = (Container.length ~fold:NodeCFG.fold_nodes node_cfg) CostDomain.VariantCostMap.pp exit_cost_record in - report_errors ~is_on_ui_thread proc_desc astate summary ; - Payload.update_summary (get_cost_summary ~is_on_ui_thread astate) summary + Check.check_and_report analysis_data ~is_on_ui_thread astate ; + Some (get_cost_summary ~is_on_ui_thread astate) diff --git a/infer/src/cost/cost.mli b/infer/src/cost/cost.mli index ab97f661d..b7994b02e 100644 --- a/infer/src/cost/cost.mli +++ b/infer/src/cost/cost.mli @@ -7,9 +7,12 @@ open! IStd -module Payload : SummaryPayload.S with type t = CostDomain.summary - -val checker : Callbacks.proc_callback_t +val checker : + ( CostDomain.summary option + * BufferOverrunAnalysisSummary.t option + * PurityDomain.summary option ) + InterproceduralAnalysis.t + -> CostDomain.summary option val instantiate_cost : Typ.IntegerWidths.t