diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d19b9786b..7b7a90f52 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -915,11 +915,7 @@ module Collection = struct will be size of the collection. *) let collection_size = let arr_locs = eval_collection_internal_array_locs iterator mem in - let accum_add arr_loc acc = - Dom.Mem.find arr_loc mem |> Dom.Val.array_sizeof |> Itv.plus acc - in - PowLoc.fold accum_add arr_locs Itv.zero - |> Dom.Val.of_itv |> Dom.Val.get_iterator_itv |> Dom.Val.set_itv_updated_by_addition + Sem.conservative_array_length arr_locs mem in model_by_value collection_size ret_id mem |> Dom.Mem.add_iterator_has_next_alias ret_id iterator diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index c2d1a2eb4..57d880d98 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -499,13 +499,27 @@ let get_offset_sym_f integer_type_widths mem e = let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_type_widths e mem) +(* This function evaluates the array length conservatively, which is useful when there are multiple + array locations and their lengths are joined to top. For example, if the [arr_locs] points to + two arrays [a] and [b] and if their lengths are [a.length] and [b.length], this function + evaluates its length as [\[0, a.length.ub + b.length.ub\]]. *) +let conservative_array_length ?traces arr_locs mem = + let accum_add arr_loc acc = Mem.find arr_loc mem |> Val.array_sizeof |> Itv.plus acc in + PowLoc.fold accum_add arr_locs Itv.zero + |> Val.of_itv ?traces |> Val.get_iterator_itv |> Val.set_itv_updated_by_addition + + let eval_array_locs_length arr_locs mem = if PowLoc.is_empty arr_locs then Val.Itv.top else let arr = Mem.find_set arr_locs mem in let traces = Val.get_traces arr in let length = Val.get_array_blk arr |> ArrayBlk.sizeof in - Val.of_itv ~traces length + match Itv.get_bound length Symb.BoundEnd.UpperBound with + | NonBottom b when not (Bounds.Bound.is_pinf b) -> + Val.of_itv ~traces length + | _ -> + conservative_array_length ~traces arr_locs mem module Prune = struct diff --git a/infer/tests/codetoanalyze/java/performance/ListTest.java b/infer/tests/codetoanalyze/java/performance/ListTest.java index 4bb62b143..958edced5 100644 --- a/infer/tests/codetoanalyze/java/performance/ListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ListTest.java @@ -87,4 +87,15 @@ class ListTest { } for (Integer i : l) {} } + + void iter_multiple_list3_linear(List a, List l1, List l2) { + List l; + if (unknown_bool) { + l = l1; + } else { + l = l2; + } + a.addAll(l); + for (Integer i : a) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 5468cd934..02b77933a 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -151,6 +151,7 @@ codetoanalyze/java/performance/ListTest.java, ListTest.call_iterate_elements_lin codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 18,{list.length},Loop at line 18] codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list1_linear(java.util.List,java.util.List):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 17 + 15 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 76] codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list2_linear(java.util.List,java.util.List):void, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 8 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 88,{l2.length + l1.length},Loop at line 88] +codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list3_linear(java.util.List,java.util.List,java.util.List):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 8 ⋅ (l2.length + l1.length + a.length) + 3 ⋅ (l2.length + l1.length + a.length + 1), O((l2.length + l1.length + a.length)), degree = 1,{l2.length + l1.length + a.length + 1},Loop at line 99,{l2.length + l1.length + a.length},Loop at line 99] codetoanalyze/java/performance/ListTest.java, ListTest.iterate_elements_linear(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ l.length + 3 ⋅ (l.length + 1), O(l.length), degree = 1,{l.length + 1},Loop at line 59,{l.length},Loop at line 59] codetoanalyze/java/performance/ListTest.java, ListTest.sort_comparator_nlogn(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), O(people.length × log(people.length)), degree = 1 + 1⋅log,{people.length},Modeled call to List.sort,{people.length},Modeled call to List.sort] codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ (filesList.length - 1) + 3 ⋅ filesList.length, O(filesList.length), degree = 1,{filesList.length},Loop at line 32,{filesList.length - 1},Loop at line 32]