[inferbo] Substitution of array block of default case in Java

Summary:
There was a precision loss during the substitution of array block.  For example:

Callee's abstract memory includes an array block as follows, where `a` is a parameter.

```
a.elements -> { a.elements[*] with a.elements.size }
```

Callers' abstract memory includes a pointer that may point to multiple array blocks.

```
c -> { x, y }
x.elements -> { x.elements[*] with x.elements.size }
y.elements -> { y.elements[*] with y.elements.size }
```

When the callee is called with the parameter `c`, the callees memory is substituted to:

```
x.elements -> { x.elements[*] with top , y.elements[*] with top }
y.elements -> { x.elements[*] with top , y.elements[*] with top }
```

because `a.elements[*]` was substituted to `{ x.elements[*] , y.elements[*] }`
and `a.elements.size` was substituted to `top ( = x.elements.size join y.elements.size )`.

This diff tries to keep the precision in the specific case, not to join the sizes of array blocks.
So now the same callee's abstract memory is substituted to:

```
x.elements -> { x.elements[*] with x.elements.size }
y.elements -> { y.elements[*] with y.elements.size }
```

Reviewed By: ngorogiannis

Differential Revision: D18480585

fbshipit-source-id: b70e63c22

infer/src/bufferoverrun/arrayBlk.ml

@@ -270,6 +270,14 @@ module ArrInfo = struct
         cmp_itv Itv.zero Itv.zero
     | _ ->
         Boolean.Top
+
+
+  let is_symbolic_length_of_path path info =
+    match (path, info) with
+    | Symb.SymbolPath.Deref (_, prefix), Java {length} ->
+        Itv.is_length_path_of prefix length
+    | _ ->
+        false
 end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
@@ -333,6 +341,10 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> PowLoc.t * t =
         let locs = eval_locpath path in
         let add_allocsite l (powloc_acc, acc) =
           match l with
+          | Loc.Allocsite (Symbol (Symb.SymbolPath.Deref (_, prefix)) as a)
+            when ArrInfo.is_symbolic_length_of_path path info ->
+              let length = Itv.of_length_path ~is_void:false prefix in
+              (powloc_acc, add a (ArrInfo.make_java ~length) acc)
           | Loc.Allocsite a ->
               (powloc_acc, add a info' acc)
           | _ ->

infer/tests/codetoanalyze/java/performance/ArrayListTest.java

@@ -316,6 +316,24 @@ public class ArrayListTest {
     HashMap<Integer, Integer> m = init_with_put_linear(a);
     for (HashMap.Entry<Integer, Integer> e : m.entrySet()) {}
   }
+
+  boolean unknown_bool;
+
+  void id(ArrayList<Integer> a) {
+    a.add(0);
+    a.remove(0);
+  }
+
+  void substitute_array_block_linear(ArrayList<Integer> a, ArrayList<Integer> b) {
+    ArrayList<Integer> c;
+    if (unknown_bool) {
+      c = a;
+    } else {
+      c = b;
+    }
+    id(c);
+    iterate_over_arraylist(a);
+  }
 }
 
 class LexicographicComparator implements java.util.Comparator<Person> {

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -52,6 +52,8 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java
 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 + 3 ⋅ (this.list.length + 1), O(this.list.length), degree = 1,{this.list.length + 1},Loop at line 221,{this.list.length},Loop at line 221]
 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), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sort_comparator_nlogn(java.util.ArrayList):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 Collections.sort,{people.length},Modeled call to Collections.sort]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.substitute_array_block_linear(java.util.ArrayList,java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 33 + 5 ⋅ (b.length + a.length), O((b.length + a.length)), degree = 1,{b.length + a.length},call to void ArrayListTest.iterate_over_arraylist(ArrayList),Loop at line 15]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.substitute_array_block_linear(java.util.ArrayList,java.util.ArrayList):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter `b.elements[*]`,Call,Parameter `a.elements[*]`,Through,Through,Call,<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32 by call to `void ArrayListTest.iterate_over_arraylist(ArrayList)` ]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, O(p), degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, O(p), degree = 1,{p},Loop at line 12]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), O(maxI × maxJ), degree = 2,{min(11, maxJ)},Loop at line 37,{min(11, maxI)},Loop at line 35,{12-max(0, maxJ)},Loop at line 35,{min(12, maxJ)},Loop at line 37,{maxI},Loop at line 35]