[cost] Conservative array length evaluation

Summary:
This diff adopts an array length evaluation function that is conservative.  It is useful when our
domain cannot express length result precisely.

For example, suppose there is an array pointer `arr_locs` that may point to two arrays `a` and `b`,
and their lengths are `a.length` and `b.length` (symbols), respectively.  Using the usual
evaluation, our current domain cannot express `a.length join b.length` (join of two symbolic
values), so it returns top.

In this case, we can use the conservative function intead.  It evaluates the length as `[0,
a.length.ub + b.length.ub]`, since we know every array length is positive.  The result is not
precise, but better than top.

Reviewed By: ezgicicek

Differential Revision: D17908859

fbshipit-source-id: 7c0b1591b

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 =
+        Sem.conservative_array_length arr_locs mem
-          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
       in
       model_by_value collection_size ret_id mem
       |> Dom.Mem.add_iterator_has_next_alias ret_id iterator

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

infer/tests/codetoanalyze/java/performance/ListTest.java

@@ -87,4 +87,15 @@ class ListTest {
     }
     for (Integer i : l) {}
   }
+
+  void iter_multiple_list3_linear(List<Integer> a, List<Integer> l1, List<Integer> l2) {
+    List<Integer> l;
+    if (unknown_bool) {
+      l = l1;
+    } else {
+      l = l2;
+    }
+    a.addAll(l);
+    for (Integer i : a) {}
+  }
 }

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]