pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Add missing list initialization with initial capacity

Browse Source 
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
master
Ezgi Çiçek 5 years ago committed by Facebook Github Bot
parent 6fbe091987
commit 57492f830b
5 changed files with 52 additions and 3 deletions
Show Stats Download Patch File Download Diff File

17
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -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
&:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init
&:: "<init>" <>$ capt_var_exn
$+ capt_exp_of_typ (+PatternMatch.implements_collection)
$--> Collection.init_with_arg
; +PatternMatch.implements_collection
&:: "<init>" <>$ 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"
&:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init
&:: "<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

20
infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java
Unescape View File

@ -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<Integer> x = new ArrayList<Integer>(-1);
}
void alloc_is_ok() {
// initial capacity cannot be negative
ArrayList<Integer> x = new ArrayList<Integer>(9);
}
}

1
infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
Unescape View File

@ -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, [<Length trace>,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, [<Length trace>,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, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,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, [<LHS trace>,Parameter `this.yy`,<RHS trace>,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, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]

15
infer/tests/codetoanalyze/java/performance/ArrayListTest.java
Unescape View File

@ -260,6 +260,21 @@ public class ArrayListTest {
Person max_linear(ArrayList<Person> 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<Integer> x = new ArrayList<Integer>(k);
for (int i = 0; i < x.size(); i++) {}
}
void json_array_constructor_linear(ArrayList<Integer> 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<Person> {

2
infer/tests/codetoanalyze/java/performance/issues.exp
Unescape View File

@ -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]

Write Preview
Loading…
Cancel
Save