diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index fe546b6ff..558a48514 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -13,8 +13,6 @@ open Ints module DegreeKind = struct type t = Linear | Log [@@deriving compare] - let[@warning "-32"] _i_know_log_isn't_used_for_now = Log - let compute d i = match d with | Linear -> @@ -421,9 +419,9 @@ module NonNegativePolynomial = struct let of_int_exn i = NonTop (NonNegativeNonTopPolynomial.of_int_exn i) - let of_non_negative_bound b = + let of_non_negative_bound ?(degree_kind = DegreeKind.Linear) b = b - |> NonNegativeBoundWithDegreeKind.make DegreeKind.Linear + |> NonNegativeBoundWithDegreeKind.make degree_kind |> NonNegativeBoundWithDegreeKind.classify |> NonNegativeNonTopPolynomial.of_valclass diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index 71de67557..dbc7726b2 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/infer/src/bufferoverrun/polynomials.mli @@ -8,6 +8,10 @@ open! IStd module Bound = Bounds.Bound +module DegreeKind : sig + type t = Linear | Log +end + module Degree : sig type t [@@deriving compare] @@ -36,7 +40,7 @@ module NonNegativePolynomial : sig val is_one : t -> bool - val of_non_negative_bound : Bounds.NonNegativeBound.t -> t + val of_non_negative_bound : ?degree_kind:DegreeKind.t -> Bounds.NonNegativeBound.t -> t val plus : t -> t -> t diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index bb4ed0dca..6c5cf6caf 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -66,14 +66,18 @@ module TransferFunctionsNodesBasicCost = struct match instr with | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> let callee_cost = - match Payload.read pdesc callee_pname with - | Some {post= callee_cost} -> - if BasicCost.is_symbolic callee_cost then - instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem - ~callee_pname ~params ~callee_cost - else callee_cost - | None -> - cost_atomic_instruction + match CostModels.Call.dispatch () callee_pname params with + | Some model -> + model inferbo_mem + | None -> ( + match Payload.read pdesc callee_pname with + | Some {post= callee_cost} -> + if BasicCost.is_symbolic callee_cost then + instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem + ~callee_pname ~params ~callee_cost + else callee_cost + | None -> + cost_atomic_instruction ) in CostDomain.NodeInstructionToCostMap.add key callee_cost astate | Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ -> diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml new file mode 100644 index 000000000..3334bf62d --- /dev/null +++ b/infer/src/checkers/costModels.ml @@ -0,0 +1,40 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * 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 BasicCost = CostDomain.BasicCost + +type model = BufferOverrunDomain.Mem.t -> BasicCost.t + +module Collections = struct + let eval_collection_length coll_exp inferbo_mem = + let upper_bound = + let itv = + BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem + |> BufferOverrunDomain.Val.get_itv + in + match itv with Bottom -> Bounds.Bound.PInf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure + in + Bounds.NonNegativeBound.of_bound upper_bound + + + let n_log_n b = + let n = BasicCost.of_non_negative_bound b in + let log_n = BasicCost.of_non_negative_bound ~degree_kind:Polynomials.DegreeKind.Log b in + BasicCost.mult n log_n + + + let sort coll_exp inferbo_mem = + let length = eval_collection_length coll_exp inferbo_mem in + n_log_n length +end + +module Call = struct + let dispatch : (unit, model) ProcnameDispatcher.Call.dispatcher = + let open ProcnameDispatcher.Call in + make_dispatcher [-"java.util.Collections" &:: "sort" $ capt_exp $--> Collections.sort] +end diff --git a/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp b/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp index 9d2905b4d..a4676cec4 100644 --- a/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp +++ b/infer/tests/build_systems/differential_of_costs_report/costs_summary.json.exp @@ -1 +1 @@ -{"top":{"current":1,"previous":0},"zero":{"current":0,"previous":0},"degrees":[{"degree":0,"current":3,"previous":2},{"degree":100,"current":1,"previous":1},{"degree":200,"current":0,"previous":1}]} \ No newline at end of file +{"top":{"current":1,"previous":0},"zero":{"current":0,"previous":0},"degrees":[{"degree":0,"current":3,"previous":2},{"degree":100,"current":1,"previous":2},{"degree":101,"current":2,"previous":0},{"degree":200,"current":0,"previous":2}]} \ No newline at end of file diff --git a/infer/tests/build_systems/differential_of_costs_report/fixed.exp b/infer/tests/build_systems/differential_of_costs_report/fixed.exp index e69de29bb..fe8810bb3 100644 --- a/infer/tests/build_systems/differential_of_costs_report/fixed.exp +++ b/infer/tests/build_systems/differential_of_costs_report/fixed.exp @@ -0,0 +1 @@ +PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f6(java.util.ArrayList):void, 0 diff --git a/infer/tests/build_systems/differential_of_costs_report/introduced.exp b/infer/tests/build_systems/differential_of_costs_report/introduced.exp index 7f385cfc9..2b30b8c36 100644 --- a/infer/tests/build_systems/differential_of_costs_report/introduced.exp +++ b/infer/tests/build_systems/differential_of_costs_report/introduced.exp @@ -1,2 +1,3 @@ INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0 PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f4(int):int, 0 +PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f5(java.util.ArrayList):void, 0 diff --git a/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.current b/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.current index a804992e8..27e409312 100644 --- a/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.current +++ b/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.current @@ -5,6 +5,8 @@ * LICENSE file in the root directory of this source tree. */ +import java.util.ArrayList; + // This class has the following costs: // 1 bottom (zero), 2 constant, 1 linear, 1 top // constructor: constant @@ -12,6 +14,8 @@ // f2: bottom (zero) // f3: constant // f4: linear +// f5: n log n +// f6: n log n public class DiffExample { @@ -41,4 +45,14 @@ public class DiffExample { } return 0; } + + // cost: n log n + private void f5(ArrayList list) { + java.util.Collections.sort(list); + } + + // cost: n log n + private void f6(ArrayList list) { + f5(list); + } } diff --git a/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.previous b/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.previous index 598c40ce7..3f4c2cae9 100644 --- a/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.previous +++ b/infer/tests/build_systems/differential_of_costs_report/src/DiffExample.java.previous @@ -11,6 +11,8 @@ // f1: linear // f2: quadratic // f4: constant +// f5: linear +// f6: quadratic public class DiffExample { // cost: linear @@ -32,4 +34,14 @@ public class DiffExample { int i = 1; return i + k; } + + // cost: linear + private static void f5(int n) { + f1(n); + } + + // cost: quadratic + private static void f6(int n) { + f2(n); + } } diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index 31f3bfcf4..b5120c723 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -197,4 +197,12 @@ public class ArrayListTest { } return true; } + + public static void sortArrayList(ArrayList list) { + java.util.Collections.sort(list); + } + + private static void call_sortArrayList(ArrayList list) { + sortArrayList(list); + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3a780484f..8f07497fa 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -25,6 +25,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + list.length.ub × log(list.length.ub), degree = 1 + 1⋅log] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2] @@ -41,6 +42,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_h codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length.ub × log(list.length.ub), degree = 1 + 1⋅log] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p.ub, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 ⋅ p.ub, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p.ub, degree = 1]