From 57492f830b8f90a4bc206f8e423d960830d4a617 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 9 Aug 2019 02:30:09 -0700 Subject: [PATCH] [inferbo] Add missing list initialization with initial capacity Summary: Correct the models of ArrayList initialization. Basically, there are two ways to initialize: - by setting an initial capacity, which creates an empty list - by passing another collection as an argument Before, we had only modeled the second case which was resulting in wrong memory model for the first case. This diff fixes that. Reviewed By: skcho Differential Revision: D16711055 fbshipit-source-id: e82faf191 --- .../src/bufferoverrun/bufferOverrunModels.ml | 17 +++++++++++++--- .../java/bufferoverrun/ArrayListTest.java | 20 +++++++++++++++++++ .../java/bufferoverrun/issues.exp | 1 + .../java/performance/ArrayListTest.java | 15 ++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 2 ++ 5 files changed, 52 insertions(+), 3 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index a1ac74f31..4d52220c8 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -913,7 +913,12 @@ module Collection = struct {exec; check= no_check} - let init lhs_id rhs_exp = + let init_with_capacity size_exp = + let exec _ ~ret:_ mem = mem and check = check_alloc_size ~can_be_zero:true size_exp in + {exec; check} + + + let init_with_arg lhs_id rhs_exp = let exec {integer_type_widths} ~ret:_ mem = let itr = Sem.eval integer_type_widths rhs_exp mem in model_by_value itr lhs_id mem @@ -1153,7 +1158,11 @@ module Call = struct ; -"std" &:: "vector" < any_typ &+ any_typ >:: "reserve" $ any_arg $+ any_arg $--> no_model ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size ; +PatternMatch.implements_collection - &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init + &:: "" <>$ capt_var_exn + $+ capt_exp_of_typ (+PatternMatch.implements_collection) + $--> Collection.init_with_arg + ; +PatternMatch.implements_collection + &:: "" <>$ any_arg $+ capt_exp $--> Collection.init_with_capacity (* model sets as lists *) ; +PatternMatch.implements_collections &::+ unmodifiable <>$ capt_exp $--> Collection.iterator @@ -1200,7 +1209,9 @@ module Call = struct ; +PatternMatch.implements_org_json "JSONArray" &:: "length" <>$ capt_exp $!--> Collection.size ; +PatternMatch.implements_org_json "JSONArray" - &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init + &:: "" <>$ capt_var_exn + $+ capt_exp_of_typ (+PatternMatch.implements_collection) + $--> Collection.init_with_arg ; +PatternMatch.implements_lang "Integer" &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue ; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java new file mode 100644 index 000000000..4c347488f --- /dev/null +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -0,0 +1,20 @@ +/* + * 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. + */ +import java.util.ArrayList; + +class ArrayListTest { + + void alloc_is_negative_bad() { + // initial capacity cannot be negative + ArrayList x = new ArrayList(-1); + } + + void alloc_is_ok() { + // initial capacity cannot be negative + ArrayList x = new ArrayList(9); + } +} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 2c725bf69..1e35a1372 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -5,6 +5,7 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `this.yy`,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index 7f39ef7aa..dc5f0653d 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -260,6 +260,21 @@ public class ArrayListTest { Person max_linear(ArrayList people) { return java.util.Collections.max(people, new LexicographicComparator()); } + + void empty_list_constant(int k) { + // create an empty list with initial capacity k, which is ignored + ArrayList x = new ArrayList(k); + for (int i = 0; i < x.size(); i++) {} + } + + void json_array_constructor_linear(ArrayList arr) { + try { + org.json.JSONArray jArray = new org.json.JSONArray(arr); + for (int i = 0; i < jArray.length(); i++) {} + } catch (Exception e) { + + } + } } class LexicographicComparator implements java.util.Comparator { diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index ef2eb0d6a..b8ef72980 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -36,12 +36,14 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 253,{l.length + list.length},Loop at line 253] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 228,{list.length},Loop at line 228] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), degree = 1,{list.length + 5},Loop at line 239,{list.length + 4},Loop at line 239] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.empty_list_constant(int):void, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 14] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ (list1.length - 1) + 3 ⋅ list1.length, degree = 1,{list1.length},Loop at line 184,{list1.length - 1},Loop at line 184] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 19] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 176,{list.length - 1},Loop at line 176] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 170,{list.length - 1},Loop at line 170] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.json_array_constructor_linear(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ arr.length + 3 ⋅ (arr.length + 1), degree = 1,{arr.length + 1},Loop at line 273,{arr.length},Loop at line 273] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java.util.ArrayList):Person, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length, degree = 1,{people.length},Modeled call to Collections.max] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (this.list.length - 1) + 3 ⋅ this.list.length, degree = 1,{this.list.length},Loop at line 217,{this.list.length - 1},Loop at line 217] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort]