diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index bf3068fb6..b396e99c2 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -178,6 +178,8 @@ module Val = struct let minus_a : t -> t -> t = lift_itv Itv.minus + let get_iterator_itv : t -> t = fun i -> {bot with itv= Itv.get_iterator_itv i.itv} + let mult : t -> t -> t = lift_itv Itv.mult let div : t -> t -> t = lift_itv Itv.div diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 1e898d6aa..40bf3eb16 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -354,6 +354,24 @@ module ArrayList = struct {exec; check= no_check} + let iterator alist = + let exec _ ~ret mem = + let itr = Sem.eval alist mem in + model_by_value itr ret mem + in + {exec; check= no_check} + + + let hasNext iterator = + let exec _ ~ret mem = + (* Set the size of the iterator to be [0, size-1], so that range + will be size of the collection. *) + let collection_size = get_size iterator mem |> Dom.Val.get_iterator_itv in + model_by_value collection_size ret mem + in + {exec; check= no_check} + + let addAll alist_id alist_to_add = let exec _model_env ~ret mem = let to_add_length = get_size alist_to_add mem in @@ -440,6 +458,8 @@ module Call = struct ; -"java.util.ArrayList" &:: "add" <>$ capt_var_exn $+ any_arg $--> ArrayList.add ; -"java.util.ArrayList" &:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg $!--> ArrayList.add_at_index + ; -"java.util.ArrayList" &:: "iterator" <>$ capt_exp $!--> ArrayList.iterator + ; -"java.util.Iterator" &:: "hasNext" <>$ capt_exp $!--> ArrayList.hasNext ; -"java.util.ArrayList" &:: "addAll" <>$ capt_var_exn $+ capt_exp $--> ArrayList.addAll ; -"java.util.ArrayList" &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $!--> ArrayList.addAll_at_index @@ -451,6 +471,7 @@ module TypName = struct let open ProcnameDispatcher.TypName in make_dispatcher [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ + ; -"java.util.Iterator" &::.*--> ArrayList.typ ; -"java.util.ArrayList" &::.*--> ArrayList.typ ; -"std" &:: "array" &::.*--> StdArray.no_typ_model ] end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index f5eb7757f..031e0dfe6 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -124,7 +124,6 @@ module Exec = struct let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in let alloc_loc = Loc.of_allocsite allocsite in let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem in - L.(debug BufferOverrun Verbose) "alloc_num:%d, depth:%d \n" alloc_num depth ; let mem = Dom.Mem.add_heap loc v mem in decl_sym_val pname path tenv ~node_hash location ~depth alloc_loc typ mem diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index ae711e105..8273736df 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -517,6 +517,8 @@ module ItvPure = struct let zero = of_bound Bound.zero + let get_iterator_itv (_, u) = (Bound.zero, Bound.plus_u u Bound.mone) + let true_sem = one let false_sem = zero @@ -934,6 +936,8 @@ let plus : t -> t -> t = lift2 ItvPure.plus let minus : t -> t -> t = lift2 ItvPure.minus +let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv + let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t = fun ?(unsigned= false) pname symbol_table path new_sym_num -> NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 60fff7778..53e08961d 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -146,6 +146,8 @@ val top : t val zero : t (** 0 *) +val get_iterator_itv : t -> t + val of_bool : Boolean.t -> t val of_int : int -> t diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index 26cc7e62b..ae8e6fb49 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -7,6 +7,7 @@ import java.util.List; import java.util.ArrayList; +import java.util.Iterator; public class ArrayListTest { @@ -14,19 +15,21 @@ public class ArrayListTest { for (int i = 0, size = list.size(); i < size; ++i) {} } - public void iterate_over_local_arraylist(ArrayList list) { - ArrayList local_list = list; - for (int i = 0, size = local_list.size(); i < size; ++i) {} + public void iterate_over_local_arraylist(ArrayList list) { + ArrayList local_list = list; + for (int i = 0, size = local_list.size(); i < size; ++i) {} } public void arraylist_empty_underrun_bad() { ArrayList list = new ArrayList(); list.add(-1, 42); } + public void arraylist_empty_ok() { ArrayList list = new ArrayList(); list.add(0, 42); } + public void arraylist_empty_overrun_bad() { ArrayList list = new ArrayList(); list.add(1, 42); @@ -40,73 +43,64 @@ public class ArrayListTest { list.add(4, 666); } - // we can't set the size of the list to 10 because it depends on how // many times the loop is executed.Should be fixed once we have // relational domain working. - public void arraylist_add_in_loop_FP() { + public void arraylist_add_in_loop_FP() { ArrayList list = new ArrayList(); for (int i = 0; i < 10; ++i) { list.add(i); } - for (int i = 0, size = list.size(); i < size; ++i) {} - - } + for (int i = 0, size = list.size(); i < size; ++i) {} + } public void arraylist_add_in_loop_ok() { ArrayList list = new ArrayList(); - list.add(0); - list.add(1); - list.add(2); - list.add(3); - list.add(4); - list.add(5); - list.add(6); - list.add(7); - list.add(8); - list.add(9); - list.add(10); - list.add(11); - list.add(12); - list.add(13); - list.add(14); - list.add(15); - - for (int i = 0, size = list.size(); i < size; ++i) {} - + list.add(0); + list.add(1); + list.add(2); + list.add(3); + list.add(4); + list.add(5); + list.add(6); + list.add(7); + list.add(8); + list.add(9); + list.add(10); + list.add(11); + list.add(12); + list.add(13); + list.add(14); + list.add(15); + for (int i = 0, size = list.size(); i < size; ++i) {} } - - public void arraylist_addAll_bad() { + public void arraylist_addAll_bad() { ArrayList list = new ArrayList(); - list.add(2); - list.add(3); - - ArrayList list2 = new ArrayList(); - list2.add(0); - list2.add(1); + list.add(2); + list.add(3); - list2.addAll(0,list); - list2.addAll(5,list); + ArrayList list2 = new ArrayList(); + list2.add(0); + list2.add(1); + list2.addAll(0, list); + list2.addAll(5, list); } - - public void arraylist_get_underrun_bad() { + public void arraylist_get_underrun_bad() { ArrayList list = new ArrayList(); list.get(0); } - - public void arraylist_get_overrun_bad() { + public void arraylist_get_overrun_bad() { ArrayList list = new ArrayList(); list.add(0); list.get(2); } - - public void arraylist_get_ok() { + public void arraylist_get_ok() { ArrayList list = new ArrayList(); list.add(0); list.add(1); @@ -115,11 +109,9 @@ public class ArrayListTest { for (int i = 0, size = list.size(); i < size; ++i) { list.get(i); } + } - } - - - public void arraylist_set_ok() { + public void arraylist_set_ok() { ArrayList list = new ArrayList(); list.add(0); list.add(1); @@ -127,53 +119,45 @@ public class ArrayListTest { for (int i = 0, size = list.size(); i < size; ++i) { list.set(i, i); } + } - } - - - public void arraylist_set_underrun_bad() { + public void arraylist_set_underrun_bad() { ArrayList list = new ArrayList(); list.set(0, 10); } - - public void arraylist_set_overrun_bad() { + public void arraylist_set_overrun_bad() { ArrayList list = new ArrayList(); list.add(0); list.set(1, 10); } - public void arraylist_remove_overrun_bad() { ArrayList list = new ArrayList(); list.add(0); list.remove(1); } - public void arraylist_remove_ok() { + public void arraylist_remove_ok() { ArrayList list = new ArrayList(); list.add(0); list.add(1); list.remove(0); list.get(0); - } - - public void arraylist_remove_bad() { + public void arraylist_remove_bad() { ArrayList list = new ArrayList(); list.add(0); list.add(1); list.remove(0); list.get(1); - } - // we can't set the size of the list to 10 because it depends on how // many times the loop is executed. Should be fixed once we have // relational domain working. - public void arraylist_remove_in_loop_Good_FP() { + public void arraylist_remove_in_loop_Good_FP() { ArrayList list = new ArrayList(); for (int i = 0; i < 10; ++i) { list.add(i); @@ -181,8 +165,34 @@ public class ArrayListTest { for (int i = 0, size = list.size(); i < size; ++i) { list.remove(i); } + } + + public void iterate_with_iterator(ArrayList list) { + for (Integer element : list) {} + } + + public void iterate_while_has_next(ArrayList list) { + Iterator itr = list.iterator(); + + while (itr.hasNext()) {} + } - } + public void iterate_over_arraylist_with_inner(ArrayList list1) { + ArrayList list2 = new ArrayList(); + for (Integer element : list1) { + list2.size(); + } + } + // Control vars include element which is in [-oo,+oo]. Hence, we get T + // Simplified version of real code https://fburl.com/a3gge1b7 + public boolean iterate_over_arraylist_shortcut_FP(ArrayList list) { + for (Integer element : list) { + if (element > 10) { + return false; + } + } + return true; + } } diff --git a/infer/tests/codetoanalyze/java/performance/IteratorTest.java b/infer/tests/codetoanalyze/java/performance/IteratorTest.java new file mode 100644 index 000000000..86834e256 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/IteratorTest.java @@ -0,0 +1,13 @@ +/* + * 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. + */ +import java.util.Iterator; +public class IteratorTest { + + public void appendTo(Iterator parts) { + while (parts.hasNext()) {} + } +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 6fbad8da6..8d7eb9f19 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -8,6 +8,8 @@ codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(i codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 889, degree = 0] codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * mag.length.ub, degree = 1] codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * mag.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, boolean ArrayListTest.iterate_over_arraylist_shortcut_FP(ArrayList), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/ArrayListTest.java, boolean ArrayListTest.iterate_over_arraylist_shortcut_FP(ArrayList), 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __cast,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_add3_overrun_bad(), 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 4 Size: 3] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_addAll_bad(), 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 4] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_add_in_loop_FP(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] @@ -24,8 +26,14 @@ codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_ codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_set_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * list.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist_with_inner(ArrayList), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 13 * (list1.length.ub + -1) + 4 * list1.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist_with_inner(ArrayList), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 13 * (list1.length.ub + -1) + 4 * list1.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_local_arraylist(ArrayList), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 * list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_local_arraylist(ArrayList), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * list.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_while_has_next(ArrayList), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 2 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_while_has_next(ArrayList), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 2 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_with_iterator(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 9 * (list.length.ub + -1) + 4 * list.length.ub, degree = 1] +codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_with_iterator(ArrayList), 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/Break.java, int Break.break_constant(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * p.ub, degree = 1] codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 7 * p.ub, degree = 1] codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub, degree = 1] @@ -71,6 +79,8 @@ codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(i codetoanalyze/java/performance/EvilCfg.java, void EvilCfg.foo(int,int,boolean), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1] +codetoanalyze/java/performance/IteratorTest.java, void IteratorTest.appendTo(Iterator), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 2 * (parts.length.ub + -1) + 4 * parts.length.ub, degree = 1] +codetoanalyze/java/performance/IteratorTest.java, void IteratorTest.appendTo(Iterator), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 0 + 2 * (parts.length.ub + -1) + 4 * parts.length.ub, degree = 1] codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: StringBuilder StringBuilder.append(String),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]