[inferbo] Add FN test due to invalid pruning of array list length

Reviewed By: ezgicicek

Differential Revision: D20628205

fbshipit-source-id: 4077557a3

infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java

@@ -242,4 +242,34 @@ class ArrayListTest {
       b.get(0); // size of b should be [0, 2]
     }
   }
+
+  interface MyI {
+    public ArrayList<Integer> mk_unknown();
+  }
+
+  boolean unknown_bool2;
+  ArrayList<Integer> unknown_array_list1;
+  ArrayList<Integer> unknown_array_list2;
+
+  void loop_on_unknown_iterator_FN(MyI x, int j) {
+    ArrayList<Integer> a = new ArrayList<>();
+    ArrayList<Integer> b;
+    if (unknown_bool) {
+      b = a;
+    } else {
+      b = x.mk_unknown();
+    }
+    // `b` points to an zero-sized array and `Unknown` pointer here.  By `b.hasNext()`, the size of
+    // the array list is pruned incorrectly to [0,-1].
+    for (Integer i : b) {
+      // Both branches are unreachable since `a.size()` is an invalid [0,-1].
+      if (a.size() <= -1) {
+        int[] c = new int[5];
+        c[5] = 0;
+      } else {
+        int[] c = new int[5];
+        c[5] = 0;
+      }
+    }
+  }
 }

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

@@ -20,6 +20,9 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_i
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 11, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: [0, 2]]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 9, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: ArrayList ArrayListTest$MyI.mk_unknown(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 13, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 3, 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]