[inferbo] Fix a bug in SafeInvertedMap.join

Summary: `equals1` and `equals2` in `SafeInvertedMap.join` are references that indicate whether given parameters and the result is physically equal or not. This diff fixes a missing update of them.

Reviewed By: ezgicicek

Differential Revision: D18450680

fbshipit-source-id: bae19cbe9

infer/src/absint/AbstractDomain.ml

@@ -649,7 +649,10 @@ struct
             match (v1_opt, v2_opt) with
             | Some v1, Some v2 ->
                 let v = f v1 v2 in
-                if ValueDomain.is_top v then None
+                if ValueDomain.is_top v then (
+                  equals1 := false ;
+                  equals2 := false ;
+                  None )
                 else (
                   if not (phys_equal v v1) then equals1 := false ;
                   if not (phys_equal v v2) then equals2 := false ;

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

@@ -203,4 +203,21 @@ class ArrayListTest {
     j = a1.get(b.size() + 1);
     j = a2.get(b.size() + 1);
   }
+
+  void alias_join_bad() {
+    int i;
+    ArrayList<Integer> a = new ArrayList<>();
+    ArrayList<Integer> b = new ArrayList<>();
+    if (unknown_bool) {
+      a.add(0);
+      i = 0; // i = size of b
+    } else {
+      b.add(0);
+      b.add(0);
+      i = 0; // i = size of a
+    }
+    if (i == 0) {
+      b.get(0); // size of b should be [0, 2]
+    }
+  }
 }

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

@@ -14,6 +14,8 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_b
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Assignment,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: [0, b.length] Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator_bad(java.util.ArrayList):void, 5, 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.alias_join_bad():void, 12, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 13, 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, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 8, 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, 14, 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]