From 7e16aafdbaca9f6483a4002bd241d8085edf84ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 16 Apr 2019 03:26:03 -0700 Subject: [PATCH] [loop-hoisting] Incorporate cost trace into EXPENSIVE_LOOP_INVARIANT_CALL issues Reviewed By: mbouaziz Differential Revision: D14934254 fbshipit-source-id: 23af117b6 --- infer/src/bufferoverrun/polynomials.ml | 16 +++++++++++ infer/src/bufferoverrun/polynomials.mli | 9 +++---- infer/src/checkers/cost.ml | 25 +++++------------ infer/src/checkers/hoisting.ml | 27 +++++++++++-------- .../java/hoistingExpensive/issues.exp | 16 +++++------ 5 files changed, 50 insertions(+), 43 deletions(-) diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 9388e7c0c..bffdbfdaa 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -585,6 +585,22 @@ module NonNegativePolynomial = struct else Degree.pp fmt degree + let degree_str p = + match degree p with + | Some degree -> + Format.asprintf ", degree = %a" Degree.pp degree + | None -> + "" + + + let polynomial_traces p = + match get_symbols p with + | Below symbols -> + List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces + | Above trace -> + TopTraces.make_err_trace trace + + let encode astate = Marshal.to_string astate [] |> Base64.encode_exn let decode enc_str = Marshal.from_string (Base64.decode_exn enc_str) 0 diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index 660e459b9..8447fee34 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/infer/src/bufferoverrun/polynomials.mli @@ -19,8 +19,6 @@ module Degree : sig (** Encodes the complex type [t] to an integer that can be used for comparison. *) val is_zero : t -> bool - - val pp : Format.formatter -> t -> unit end module NonNegativeNonTopPolynomial : sig @@ -73,16 +71,17 @@ module NonNegativePolynomial : sig val degree : t -> Degree.t option + val degree_str : t -> string + val compare_by_degree : t -> t -> int val pp_degree : only_bigO:bool -> Format.formatter -> degree_with_term -> unit + val polynomial_traces : t -> Errlog.loc_trace + val encode : t -> string val decode : string -> t - val get_symbols : - t -> (Bounds.NonNegativeBound.t list, TopTraces.t) AbstractDomain.Types.below_above - val get_degree_with_term : t -> degree_with_term end diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 03c4fbf8f..b8f26bc10 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -715,22 +715,7 @@ module WorstCaseCost = struct end module Check = struct - let polynomial_traces cost = - match BasicCost.get_symbols cost with - | Below symbols -> - List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces - | Above trace -> - Polynomials.TopTraces.make_err_trace trace - - let report_threshold proc_desc summary ~name ~location ~cost ~threshold ~kind = - let degree_str = - match BasicCost.degree cost with - | Some degree -> - Format.asprintf ", degree = %a" Polynomials.Degree.pp degree - | None -> - "" - in let report_issue_type = match kind with | CostDomain.AllocationCost -> @@ -745,18 +730,19 @@ module Check = struct | CostDomain.IOCost -> IssueType.expensive_IO_call 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 = + let cost_trace_elem = let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp_hum cost degree_str in Errlog.make_trace_element 0 location cost_desc [] in Reporting.log_error summary ~loc:location - ~ltr:(cost_trace :: polynomial_traces cost) + ~ltr:(cost_trace_elem :: BasicCost.polynomial_traces cost) ~extras:(compute_errlog_extras cost) report_issue_type message @@ -768,8 +754,9 @@ module Check = struct suffix in let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in - Reporting.log_error ~loc ~ltr:(polynomial_traces cost) ~extras:(compute_errlog_extras cost) - summary issue message + Reporting.log_error ~loc + ~ltr:(BasicCost.polynomial_traces cost) + ~extras:(compute_errlog_extras cost) summary issue message in if BasicCost.is_top cost then report IssueType.infinite_execution_time_call "cannot be computed" diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index 10248a484..9aefaa2b3 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -7,6 +7,7 @@ open! IStd module F = Format module InstrCFG = ProcCfg.NormalOneInstrPerNode +module BasicCost = CostDomain.BasicCost module Call = struct type t = @@ -70,20 +71,26 @@ let get_hoist_inv_map tenv ~get_callee_purity reaching_defs_invariant_map loop_h let do_report extract_cost_if_expensive summary (Call.{pname; loc} as call) loop_head_loc = - let issue, cost_msg = + let exp_desc = + F.asprintf "The call to %a at %a is loop-invariant" Typ.Procname.pp pname Location.pp loc + in + let loop_inv_trace_elem = Errlog.make_trace_element 0 loc exp_desc [] in + let issue, cost_msg, ltr = match extract_cost_if_expensive call with | Some cost -> + let degree_str = BasicCost.degree_str cost in + let cost_trace_elem = + let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp_hum cost degree_str in + Errlog.make_trace_element 0 loc cost_desc [] + in ( IssueType.expensive_loop_invariant_call , F.asprintf " and expensive (has complexity %a)" - (CostDomain.BasicCost.pp_degree ~only_bigO:true) - cost ) + (BasicCost.pp_degree ~only_bigO:true) + (BasicCost.get_degree_with_term cost) + , loop_inv_trace_elem :: cost_trace_elem :: BasicCost.polynomial_traces cost ) | None -> - (IssueType.invariant_call, "") - in - let exp_desc = - F.asprintf "The call to %a at %a is loop-invariant" Typ.Procname.pp pname Location.pp loc + (IssueType.invariant_call, "", [loop_inv_trace_elem]) in - let ltr = [Errlog.make_trace_element 0 loc exp_desc []] in let message = F.asprintf "%s%s. It can be moved out of the loop at %a." exp_desc cost_msg Location.pp loop_head_loc @@ -117,9 +124,7 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f ~callee_cost:(CostDomain.get_operation_cost cost_record) ~loc in - Option.some_if - (CostDomain.BasicCost.is_symbolic cost) - (CostDomain.BasicCost.get_degree_with_term cost) + Option.some_if (CostDomain.BasicCost.is_symbolic cost) cost | _ -> None diff --git a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp index c27aba3a8..c37d964ae 100644 --- a/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp +++ b/infer/tests/codetoanalyze/java/hoistingExpensive/issues.exp @@ -6,21 +6,21 @@ codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.incr(in codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.instantiated_cheap_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.instantiated_cheap_hoist(int)] codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.instantiated_cheap_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 33 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.symbolic_expensive_hoist(int)] -codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 26 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 26 is loop-invariant,with estimated cost 6 + 11 ⋅ size, degree = 1,{size},call to void HoistExpensive.cheap_dont_hoist(int),Loop at line 18] codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.symbolic_expensive_iterator_hoist(int,ArrayList)] -codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList) at line 48 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList) at line 48 is loop-invariant,with estimated cost 7 + 14 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 40,{list.length - 1},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 40] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.call_expensive_hoist(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.expensive_get_hoist(int) at line 58 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.expensive_get_hoist(int) at line 58 is loop-invariant,with estimated cost 85 + 10 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_contains_dont_hoist(Integer)] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 34 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_substring_dont_hoist(String)] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 41 is loop-invariant] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_hoist(int)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object Provider.get() at line 16 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object Provider.get() at line 16 is loop-invariant,with estimated cost Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},Modeled call to Provider.get] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_hoist_hoist_me(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer) at line 66 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer) at line 66 is loop-invariant,with estimated cost 904 + 100 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer),call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_contains_hoist(ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 3, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 23 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 3, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 23 is loop-invariant,with estimated cost list.length, degree = 1,{list.length},Modeled call to List.contains] codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_substring_hoist(String,ArrayList,Integer)] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 49 is loop-invariant] -codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 7, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 52 is loop-invariant] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 4, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 49 is loop-invariant,with estimated cost (s.length - 3), degree = 1,{s.length - 3},Modeled call to String.substring] +codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 7, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 52 is loop-invariant,with estimated cost (s.length - 1), degree = 1,{s.length - 1},Modeled call to String.substring]