From a090551d698ffb0525823e7bbee9eba6ccedbedc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 4 Jun 2020 01:54:40 -0700 Subject: [PATCH] [cost] Remove EXPENSIVE_EXECUTION_TIME issue type Summary: We stopped relying on an arbitrary threshold. Hence, - we don't need all the machinery for reporting at a specific node for a threshold - we can remove - the issue type `EXPENSIVE_EXECUTION_TIME` - the config option `--use-cost-threshold`. Reviewed By: skcho Differential Revision: D21859815 fbshipit-source-id: b73a2372d --- infer/man/man1/infer-full.txt | 6 - infer/man/man1/infer-report.txt | 2 - infer/man/man1/infer.txt | 2 - infer/src/base/Config.ml | 7 -- infer/src/base/Config.mli | 2 - infer/src/base/CostIssues.ml | 5 - infer/src/base/CostIssues.mli | 2 - infer/src/base/IssueType.ml | 5 - infer/src/base/IssueType.mli | 2 - infer/src/base/costKind.ml | 4 - infer/src/base/costKind.mli | 2 - infer/src/cost/constraintSolver.ml | 13 +- infer/src/cost/constraintSolver.mli | 2 +- infer/src/cost/cost.ml | 176 ++++++---------------------- 14 files changed, 44 insertions(+), 186 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index af61ee9f1..bc5161a89 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -436,8 +436,6 @@ OPTIONS EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD (enabled by default), EXECUTION_TIME_UNREACHABLE_AT_EXIT (disabled by default), - EXPENSIVE_EXECUTION_TIME (disabled by default), - EXPENSIVE_EXECUTION_TIME_UI_THREAD (disabled by default), EXPENSIVE_LOOP_INVARIANT_CALL (enabled by default), EXPOSED_INSECURE_INTENT_HANDLING (enabled by default), Failure_exe (enabled by default), @@ -1857,10 +1855,6 @@ INTERNAL OPTIONS Activates: Run uninit check in the experimental interprocedural mode (Conversely: --no-uninit-interproc) - --use-cost-threshold - Activates: Emit costs issues by comparing costs with a set - threshold (Conversely: --no-use-cost-threshold) - --version-vcs Print version control system commit and exit diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 990ce1a3a..339a6e0d0 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -162,8 +162,6 @@ OPTIONS EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD (enabled by default), EXECUTION_TIME_UNREACHABLE_AT_EXIT (disabled by default), - EXPENSIVE_EXECUTION_TIME (disabled by default), - EXPENSIVE_EXECUTION_TIME_UI_THREAD (disabled by default), EXPENSIVE_LOOP_INVARIANT_CALL (enabled by default), EXPOSED_INSECURE_INTENT_HANDLING (enabled by default), Failure_exe (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index c7ecf8d00..2c947ce37 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -436,8 +436,6 @@ OPTIONS EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD (enabled by default), EXECUTION_TIME_UNREACHABLE_AT_EXIT (disabled by default), - EXPENSIVE_EXECUTION_TIME (disabled by default), - EXPENSIVE_EXECUTION_TIME_UI_THREAD (disabled by default), EXPENSIVE_LOOP_INVARIANT_CALL (enabled by default), EXPOSED_INSECURE_INTENT_HANDLING (enabled by default), Failure_exe (enabled by default), diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 9f9b335dc..3f34b0c06 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2280,11 +2280,6 @@ and unsafe_malloc = "Assume that malloc(3) never returns null." -and use_cost_threshold = - CLOpt.mk_bool ~long:"use-cost-threshold" ~default:false - "Emit costs issues by comparing costs with a set threshold" - - and incremental_analysis = CLOpt.mk_bool ~long:"incremental-analysis" ~default:false "[EXPERIMENTAL] Use incremental analysis for changed files. Not compatible with \ @@ -3111,8 +3106,6 @@ and uninit_interproc = !uninit_interproc and unsafe_malloc = !unsafe_malloc -and use_cost_threshold = !use_cost_threshold - and incremental_analysis = !incremental_analysis and worklist_mode = !worklist_mode diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 9b7e40eee..6e2a0de06 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -138,8 +138,6 @@ val trace_absarray : bool val unsafe_unret : string -val use_cost_threshold : bool - val incremental_analysis : bool val weak : string diff --git a/infer/src/base/CostIssues.ml b/infer/src/base/CostIssues.ml index 319e45435..16b0d4582 100644 --- a/infer/src/base/CostIssues.ml +++ b/infer/src/base/CostIssues.ml @@ -9,9 +9,7 @@ open! IStd type issue_spec = { extract_cost_f: Jsonbug_t.cost_item -> Jsonbug_t.cost_info ; name: string - ; threshold: int option ; complexity_increase_issue: is_on_ui_thread:bool -> IssueType.t - ; expensive_issue: is_on_ui_thread:bool -> IssueType.t ; unreachable_issue: IssueType.t ; infinite_issue: IssueType.t ; top_and_unreachable: bool } @@ -37,12 +35,9 @@ let enabled_cost_map = ~f:(fun acc CostKind.{kind; top_and_unreachable} -> let kind_spec = { name= Format.asprintf "The %a" CostKind.pp kind - ; threshold= (if Config.use_cost_threshold then CostKind.to_threshold kind else None) ; extract_cost_f= (fun c -> CostKind.to_json_cost_info c kind) ; complexity_increase_issue= (fun ~is_on_ui_thread -> IssueType.complexity_increase ~kind ~is_on_ui_thread) - ; expensive_issue= - (fun ~is_on_ui_thread -> IssueType.expensive_cost_call ~kind ~is_on_ui_thread) ; unreachable_issue= IssueType.unreachable_cost_call ~kind ; infinite_issue= IssueType.infinite_cost_call ~kind ; top_and_unreachable } diff --git a/infer/src/base/CostIssues.mli b/infer/src/base/CostIssues.mli index 8aa60fa25..df34fb430 100644 --- a/infer/src/base/CostIssues.mli +++ b/infer/src/base/CostIssues.mli @@ -10,9 +10,7 @@ open! IStd type issue_spec = { extract_cost_f: Jsonbug_t.cost_item -> Jsonbug_t.cost_info ; name: string - ; threshold: int option ; complexity_increase_issue: is_on_ui_thread:bool -> IssueType.t - ; expensive_issue: is_on_ui_thread:bool -> IssueType.t ; unreachable_issue: IssueType.t ; infinite_issue: IssueType.t ; top_and_unreachable: bool } diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 1f0830bc0..35ae70990 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -412,10 +412,6 @@ let eradicate_meta_class_can_be_nullsafe = (* Should be enabled for special integrations *) ~enabled:false Eradicate -let expensive_cost_call ~kind ~is_on_ui_thread = - register_from_cost_string ~enabled:false ~kind ~is_on_ui_thread "EXPENSIVE_%s" - - let exposed_insecure_intent_handling = register_from_string ~id:"EXPOSED_INSECURE_INTENT_HANDLING" Quandary @@ -667,7 +663,6 @@ let () = List.iter CostKind.enabled_cost_kinds ~f:(fun CostKind.{kind} -> List.iter [true; false] ~f:(fun is_on_ui_thread -> ignore (unreachable_cost_call ~kind) ; - ignore (expensive_cost_call ~kind ~is_on_ui_thread) ; ignore (infinite_cost_call ~kind) ; ignore (complexity_increase ~kind ~is_on_ui_thread) ; () ) ) diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 9b429cf41..6c61e7dff 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -200,8 +200,6 @@ val eradicate_meta_class_needs_improvement : t val eradicate_meta_class_is_nullsafe : t -val expensive_cost_call : kind:CostKind.t -> is_on_ui_thread:bool -> t - val exposed_insecure_intent_handling : t val failure_exe : t diff --git a/infer/src/base/costKind.ml b/infer/src/base/costKind.ml index 7093ae156..58f0ea8fa 100644 --- a/infer/src/base/costKind.ml +++ b/infer/src/base/costKind.ml @@ -49,10 +49,6 @@ let to_json_cost_info c = function assert false -(* We use this threshold to give error if the cost is above it. - Currently it's set randomly to 200 for OperationCost and 3 for AllocationCost. *) -let to_threshold = function OperationCost -> Some 200 | AllocationCost -> Some 3 | IOCost -> None - type kind_spec = {kind: t; (* for non-diff analysis *) top_and_unreachable: bool} let enabled_cost_kinds = [{kind= OperationCost; top_and_unreachable= true}] diff --git a/infer/src/base/costKind.mli b/infer/src/base/costKind.mli index 1d3ae8b67..208d0d6c7 100644 --- a/infer/src/base/costKind.mli +++ b/infer/src/base/costKind.mli @@ -22,5 +22,3 @@ val to_issue_string : t -> string val to_json_cost_info : Jsonbug_t.cost_item -> t -> Jsonbug_t.cost_info val enabled_cost_kinds : kind_spec list - -val to_threshold : t -> int option diff --git a/infer/src/cost/constraintSolver.ml b/infer/src/cost/constraintSolver.ml index 52ec9a7a8..7f02f5b23 100644 --- a/infer/src/cost/constraintSolver.ml +++ b/infer/src/cost/constraintSolver.ml @@ -181,9 +181,14 @@ let compute_costs ~debug bound_map equalities = debug.f "[ConstraintSolver][CImpr] %a@\n" Equalities.pp_costs equalities -let get_node_nb_exec equalities node_id = - let set = - node_id |> ControlFlowCost.make_node |> Equalities.find equalities +let get_node_nb_exec equalities node = + let nb_exec_opt = + Node.id node |> ControlFlowCost.make_node |> Equalities.find equalities |> Equalities.find_set equalities in - Option.value_exn set |> ControlFlowCost.Set.cost + match nb_exec_opt with + | Some nb_exec -> + ControlFlowCost.Set.cost nb_exec + | None -> + (* a dangling node with no incoming or outgoing edges is unreachable *) + BasicCost.of_unreachable (Node.loc node) diff --git a/infer/src/cost/constraintSolver.mli b/infer/src/cost/constraintSolver.mli index f7a3712e1..1757f43bf 100644 --- a/infer/src/cost/constraintSolver.mli +++ b/infer/src/cost/constraintSolver.mli @@ -19,7 +19,7 @@ end val compute_costs : debug:debug -> BasicCost.t Node.IdMap.t -> Equalities.t -> unit (** repeatedly improve the costs given the constraints *) -val get_node_nb_exec : Equalities.t -> Node.id -> BasicCost.t +val get_node_nb_exec : Equalities.t -> Node.t -> BasicCost.t (** compute the number of times a node is executed by taking into account the program structural (e.g. control-flow) constraints *) diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 46b57c2e7..11d12c85b 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -19,7 +19,7 @@ type extras_WorstCaseCost = { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map ; integer_type_widths: Typ.IntegerWidths.t ; inferbo_get_summary: BufferOverrunAnalysisSummary.get_summary - ; get_node_nb_exec: Node.id -> BasicCost.t + ; get_node_nb_exec: Node.t -> BasicCost.t ; get_summary: Procname.t -> CostDomain.summary option ; get_formals: Procname.t -> (Pvar.t * Typ.t) list option } @@ -153,87 +153,26 @@ let compute_errlog_extras cost = ; nullsafe_extra= None } -module ThresholdReports = struct - type threshold_or_report = - | Threshold of BasicCost.t - | ReportOn of {location: Location.t; cost: BasicCost.t} - | NoReport - - type t = threshold_or_report CostIssues.CostKindMap.t - - let none : t = CostIssues.CostKindMap.empty - - let config = - CostIssues.CostKindMap.fold - (fun kind kind_spec acc -> - match kind_spec with - | CostIssues.{threshold= Some threshold} -> - CostIssues.CostKindMap.add kind (Threshold (BasicCost.of_int_exn threshold)) acc - | _ -> - acc ) - CostIssues.enabled_cost_map none -end - -(** Calculate the final Worst Case Cost predicted for each cost field and each WTO component. It is - the dot product of the symbolic cost of the node and how many times it is executed. *) +(** Calculate the final Worst Case Cost of the cfg. It is the dot product of the symbolic cost of + the node and how many times it is executed. *) module WorstCaseCost = struct - type astate = {costs: CostDomain.t; reports: ThresholdReports.t} - (** We don't report when the cost is Top as it corresponds to subsequent 'don't know's. Instead, we report Top cost only at the top level per function. *) - let exec_node tenv {costs; reports} extras instr_node = + let exec_node tenv extras instr_node = let {get_node_nb_exec} = extras in - let node_cost = - let instr_cost_record = InstrBasicCost.get_instr_node_cost_record tenv extras instr_node in - let node_id = InstrCFG.Node.underlying_node instr_node |> Node.id in - let nb_exec = get_node_nb_exec node_id in - if BasicCost.is_top nb_exec then - Logging.d_printfln_escaped "Node %a is analyzed to visit infinite (top) times." Node.pp_id - node_id ; - CostDomain.mult_by instr_cost_record ~nb_exec - in - let costs = CostDomain.plus costs node_cost in - let reports = - CostIssues.CostKindMap.merge - (fun _kind threshold_or_report_opt cost_opt -> - match (threshold_or_report_opt, cost_opt) with - | Some ThresholdReports.NoReport, _ -> - threshold_or_report_opt - | Some ThresholdReports.(Threshold _ | ReportOn _), Some cost when BasicCost.is_top cost - -> - Some ThresholdReports.NoReport - | Some (ThresholdReports.Threshold threshold), Some cost - when not (BasicCost.leq ~lhs:cost ~rhs:threshold) -> - Some (ThresholdReports.ReportOn {location= InstrCFG.Node.loc instr_node; cost}) - | Some (ThresholdReports.ReportOn {cost= prev}), Some cost - when BasicCost.compare_by_degree prev cost < 0 -> - Some (ThresholdReports.ReportOn {location= InstrCFG.Node.loc instr_node; cost}) - | _ -> - threshold_or_report_opt ) - reports costs - in - {costs; reports} - - - let rec exec_partition tenv astate extras - (partition : InstrCFG.Node.t WeakTopologicalOrder.Partition.t) = - match partition with - | Empty -> - astate - | Node {node; next} -> - let astate = exec_node tenv astate extras node in - exec_partition tenv astate extras next - | Component {head; rest; next} -> - let {costs; reports} = astate in - let {costs} = exec_partition tenv {costs; reports= ThresholdReports.none} extras rest in - (* Execute head after the loop body to always report at loop head *) - let astate = exec_node tenv {costs; reports} extras head in - exec_partition tenv astate extras next - - - let compute tenv extras instr_cfg_wto = - let initial = {costs= CostDomain.zero_record; reports= ThresholdReports.config} in - exec_partition tenv initial extras instr_cfg_wto + let instr_cost_record = InstrBasicCost.get_instr_node_cost_record tenv extras instr_node in + let node = InstrCFG.Node.underlying_node instr_node in + let nb_exec = get_node_nb_exec node in + if BasicCost.is_top nb_exec then + Logging.d_printfln_escaped "Node %a is analyzed to visit infinite (top) times." Node.pp_id + (Node.id node) ; + CostDomain.mult_by instr_cost_record ~nb_exec + + + let compute tenv extras cfg = + let init = CostDomain.zero_record in + InstrCFG.fold_nodes cfg ~init ~f:(fun acc pair -> + exec_node tenv extras pair |> CostDomain.plus acc ) end let is_report_suppressed pname = @@ -243,35 +182,6 @@ let is_report_suppressed pname = module Check = struct - let report_threshold pname proc_desc 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 ; - expensive_issue ~is_on_ui_thread - in - let bigO_str = - Format.asprintf ", %a" - (BasicCost.pp_degree ~only_bigO:true) - (BasicCost.get_degree_with_term cost) - in - let degree_str = BasicCost.degree_str cost in - let message = - F.asprintf - "%s from the beginning of the function up to this program point is likely above the \ - acceptable threshold of %d (estimated cost %a%s)" - name threshold BasicCost.pp_hum cost degree_str - in - let cost_trace_elem = - let cost_desc = - F.asprintf "with estimated cost %a%s%s" BasicCost.pp_hum cost bigO_str degree_str - in - Errlog.make_trace_element 0 location cost_desc [] - in - Reporting.log_error proc_desc err_log ~loc:location - ~ltr:(cost_trace_elem :: BasicCost.polynomial_traces cost) - ~extras:(compute_errlog_extras cost) Cost report_issue_type message - - let report_top_and_unreachable pname proc_desc err_log loc ~name ~cost {CostIssues.unreachable_issue; infinite_issue} = let report issue suffix = @@ -286,27 +196,19 @@ module Check = struct "cannot be computed since the program's exit state is never reachable" - let check_and_report {InterproceduralAnalysis.proc_desc; err_log} ~is_on_ui_thread - {WorstCaseCost.costs; reports} = + let check_and_report {InterproceduralAnalysis.proc_desc; err_log} cost = 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 ( - CostIssues.CostKindMap.iter2 CostIssues.enabled_cost_map reports - ~f:(fun _kind (CostIssues.{name; threshold} as kind_spec) -> function - | ThresholdReports.Threshold _ | ThresholdReports.NoReport -> - () - | ThresholdReports.ReportOn {location; cost} -> - report_threshold pname 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 + if not (is_report_suppressed pname) then + CostIssues.CostKindMap.iter2 CostIssues.enabled_cost_map cost ~f:(fun _kind (CostIssues.{name; top_and_unreachable} as issue_spec) cost -> if top_and_unreachable then - report_top_and_unreachable pname proc_desc err_log proc_loc ~name ~cost issue_spec ) ) + report_top_and_unreachable pname proc_desc err_log proc_loc ~name ~cost issue_spec ) end type bound_map = BasicCost.t Node.IdMap.t -type get_node_nb_exec = Node.id -> BasicCost.t +type get_node_nb_exec = Node.t -> BasicCost.t let compute_bound_map node_cfg inferbo_invariant_map control_dep_invariant_map loop_invmap : bound_map = @@ -332,22 +234,7 @@ let compute_get_node_nb_exec node_cfg bound_map : get_node_nb_exec = ConstraintSolver.get_node_nb_exec equalities ) -let compute_worst_case_cost tenv integer_type_widths get_summary get_formals instr_cfg_wto - inferbo_invariant_map inferbo_get_summary get_node_nb_exec = - let extras = - { inferbo_invariant_map - ; integer_type_widths - ; inferbo_get_summary - ; get_node_nb_exec - ; get_summary - ; get_formals } - in - WorstCaseCost.compute tenv extras instr_cfg_wto - - -let get_cost_summary ~is_on_ui_thread astate = - {CostDomain.post= astate.WorstCaseCost.costs; is_on_ui_thread} - +let get_cost_summary ~is_on_ui_thread astate = {CostDomain.post= astate; is_on_ui_thread} let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as analysis_data) = let proc_name = Procdesc.get_proc_name proc_desc in @@ -396,16 +283,21 @@ let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals in let instr_cfg = InstrCFG.from_pdesc proc_desc in - let instr_cfg_wto = InstrCFG.wto instr_cfg in - compute_worst_case_cost tenv integer_type_widths get_summary get_formals instr_cfg_wto - inferbo_invariant_map inferbo_get_summary get_node_nb_exec + let extras = + { inferbo_invariant_map + ; inferbo_get_summary + ; integer_type_widths + ; get_node_nb_exec + ; get_summary + ; get_formals } + in + WorstCaseCost.compute tenv extras instr_cfg in let () = - let exit_cost_record = astate.WorstCaseCost.costs in L.(debug Analysis Verbose) "@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" Procname.pp proc_name (Container.length ~fold:NodeCFG.fold_nodes node_cfg) - CostDomain.VariantCostMap.pp exit_cost_record + CostDomain.VariantCostMap.pp astate in - Check.check_and_report analysis_data ~is_on_ui_thread astate ; + Check.check_and_report analysis_data astate ; Some (get_cost_summary ~is_on_ui_thread astate)