From d50091bb17d49f60a5f27b070c4fac04df6d4364 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 7 Nov 2019 03:48:16 -0800 Subject: [PATCH] [inferbo] Add models for Math.min and Math.max Reviewed By: skcho Differential Revision: D18350518 fbshipit-source-id: 39c6b12f0 --- .../src/bufferoverrun/bufferOverrunModels.ml | 16 +++++++++- infer/src/bufferoverrun/itv.ml | 6 ++++ infer/src/bufferoverrun/itv.mli | 2 ++ .../java/performance/MathTest.java | 30 +++++++++++++++++++ .../java/performance/UnknownCallsTest.java | 3 +- .../codetoanalyze/java/performance/issues.exp | 19 +++++++----- 6 files changed, 65 insertions(+), 11 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/performance/MathTest.java diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index c5bd504c2..e8a071949 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -47,6 +47,16 @@ let at ?(size = Int64.zero) array_exp index_exp = {exec; check} +let eval_binop ~f e1 e2 = + let exec {integer_type_widths} ~ret:(id, _) mem = + let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in + let i2 = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in + let v = f i1 i2 |> Dom.Val.of_itv in + Dom.Mem.add_stack (Loc.of_id id) v mem + in + {exec; check= no_check} + + (* It returns a tuple of: - type of array element - stride of the type @@ -1405,5 +1415,9 @@ module Call = struct ; +PatternMatch.implements_nio "ByteBuffer" &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int ; +PatternMatch.implements_nio "ByteBuffer" &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int - ; -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone ] + ; -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone + ; +PatternMatch.implements_lang "Math" + &:: "max" <>$ capt_exp $+ capt_exp $--> eval_binop ~f:Itv.max_sem + ; +PatternMatch.implements_lang "Math" + &:: "min" <>$ capt_exp $+ capt_exp $--> eval_binop ~f:Itv.min_sem ] end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 7fb3448e1..d631707a1 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -362,6 +362,10 @@ module ItvPure = struct fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2) + let max_sem : t -> t -> t = + fun (l1, u1) (l2, u2) -> (Bound.underapprox_max l1 l2, Bound.overapprox_max u1 u2) + + let is_invalid : t -> bool = fun (l, u) -> Bound.is_pinf l || Bound.is_minf u || Bound.lt u l let normalize : t -> t bottom_lifted = fun x -> if is_invalid x then Bottom else NonBottom x @@ -670,6 +674,8 @@ let lor_sem : t -> t -> Boolean.t = bind2b ItvPure.lor_sem let min_sem : t -> t -> t = lift2 ItvPure.min_sem +let max_sem : t -> t -> t = lift2 ItvPure.max_sem + let prune_eq_zero : t -> t = bind1 ItvPure.prune_eq_zero let prune_ne_zero : t -> t = bind1 ItvPure.prune_ne_zero diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index f6c9c8986..0015007a4 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -215,6 +215,8 @@ val lt_sem : t -> t -> Boolean.t val min_sem : t -> t -> t +val max_sem : t -> t -> t + val mod_sem : t -> t -> t val ne_sem : t -> t -> Boolean.t diff --git a/infer/tests/codetoanalyze/java/performance/MathTest.java b/infer/tests/codetoanalyze/java/performance/MathTest.java new file mode 100644 index 000000000..f9ca612a4 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/MathTest.java @@ -0,0 +1,30 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +package codetoanalyze.java.performance; + +class MathTest { + + void min_constant(int arr[]) { + for (int i = 0; i < Math.min(3, arr.length); i++) {} + } + + void max_symbolic(int arr[]) { + for (int i = 0; i < Math.max(0, arr.length); i++) {} + } + + void linear(int p) { + for (int count = 0; count < p; count++) {} + } + + void call_with_min_constant() { + linear(Math.min(3, 10)); + } + + void call_with_max_linear(int x) { + linear(Math.max(1, x)); + } +} diff --git a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java index 314b1e1f1..e127aef96 100644 --- a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java +++ b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java @@ -34,13 +34,12 @@ class UnknownCallsTest { return 0; } - // Expected: linear to maxBytesToRead (= Math.min(...)) + // Expected: linear public int read_max_cost( InputStream in, byte[] buffer, int byteOffset, int byteCount, ArrayList list) throws IOException { int maxBytesToRead = Math.min(byteCount, mBytesToRead); int bytesRead = in.read(buffer, byteOffset, maxBytesToRead); - // after the join, we get maxBytesToRead in [0, +oo]. Hence, the loop gets T if (bytesRead > 0) { maxBytesToRead = bytesRead + 1; } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 9e6933df8..8c4fbf4fc 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -180,6 +180,9 @@ codetoanalyze/java/performance/MapTest.java, MapTest.entrySet_linear(java.util.M codetoanalyze/java/performance/MapTest.java, MapTest.keySet_linear(java.util.Map):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), O(map.length), degree = 1,{map.length + 1},Loop at line 13,{map.length},Loop at line 13] codetoanalyze/java/performance/MapTest.java, MapTest.putAll_linear(java.util.Map):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), O(map.length), degree = 1,{map.length + 1},Loop at line 28,{map.length},Loop at line 28] codetoanalyze/java/performance/MapTest.java, MapTest.values_linear(java.util.Map):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ (map.length + 1) + 3 ⋅ (map.length + 2), O(map.length), degree = 1,{map.length + 2},Loop at line 22,{map.length + 1},Loop at line 22] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.call_with_max_linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ (max(1, x)), O(x), degree = 1,{max(1, x)},call to void MathTest.linear(int),Loop at line 20] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ p, O(p), degree = 1,{p},Loop at line 20] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 16,{arr.length},Loop at line 16] codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + this.mId.length, O(this.mId.length), degree = 1,{this.mId.length},call to int StringTest.indexof_linear(String),Modeled call to String.indexOf] codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(java.lang.String,int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + (-j + m.length), O((-j + m.length)), degree = 1,{-j + m.length},Modeled call to String.indexOf] codetoanalyze/java/performance/StringTest.java, StringTest.indexof_linear(java.lang.String):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + m.length, O(m.length), degree = 1,{m.length},Modeled call to String.indexOf] @@ -187,16 +190,16 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(jav codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 798, O(1), degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear(UnknownCallsTest$AbstractC):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ UnknownCallsTest$AbstractC.abstract_func().length.ub, O(UnknownCallsTest$AbstractC.abstract_func().length.ub), degree = 1,{UnknownCallsTest$AbstractC.abstract_func().length.ub},Loop at line 95] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear(UnknownCallsTest$AbstractC):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ UnknownCallsTest$AbstractC.abstract_func().length.ub, O(UnknownCallsTest$AbstractC.abstract_func().length.ub), degree = 1,{UnknownCallsTest$AbstractC.abstract_func().length.ub},Loop at line 94] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 51] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost 11, O(1), degree = 0] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 217, O(1), degree = 0] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 72] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ UnknownCallsTest.throw_exception().ub + 8 ⋅ (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 72,{UnknownCallsTest.throw_exception().ub},Loop at line 72] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 71] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ UnknownCallsTest.throw_exception().ub + 8 ⋅ (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 71,{UnknownCallsTest.throw_exception().ub},Loop at line 71] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ jsonArray.length, O(jsonArray.length), degree = 1,{jsonArray.length},Loop at line 18] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},Loop at line 52] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},Loop at line 51] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.may_throw_exception():int, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 21 + 5 ⋅ (Math.min(...).ub + 1), O(Math.min(...).ub), degree = 1,{Math.min(...).ub + 1},Loop at line 47] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅Math.min(...).ub, O(2⋅Math.min(...).ub), degree = 1,{2⋅Math.min(...).ub},Loop at line 33] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 21 + 5 ⋅ (byteCount + 1), O(byteCount), degree = 1,{byteCount + 1},Loop at line 46] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅byteCount, O(2⋅byteCount), degree = 1,{2⋅byteCount},Loop at line 33] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.throw_exception():int, 1, UNREACHABLE_CODE, no_bucket, ERROR, [Here] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 62,{list.length},Loop at line 62] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 61,{list.length},Loop at line 61]