[inferbo] Fix a bug in interval prune

Summary: This diff avoids that an invalid interval value, e.g. [0, -1], is genrated by interval pruning.

Reviewed By: ezgicicek

Differential Revision: D20645488

fbshipit-source-id: 6516c75d1

Author: skcho

infer/src/bufferoverrun/itv.ml

@@ -459,18 +459,22 @@ module ItvPure = struct
 
   let arith_unop (unop : Unop.t) x = match unop with Neg -> Some (neg x) | BNot | LNot -> None
 
-  let prune_le : t -> t -> t = fun (l1, u1) (_, u2) -> (l1, Bound.overapprox_min u1 u2)
+  let prune_le : t -> t -> t bottom_lifted =
+   fun (l1, u1) (_, u2) -> normalize (l1, Bound.overapprox_min u1 u2)
 
-  let prune_ge : t -> t -> t = fun (l1, u1) (l2, _) -> (Bound.underapprox_max l1 l2, u1)
 
-  let prune_lt : t -> t -> t = fun x y -> prune_le x (minus y one)
+  let prune_ge : t -> t -> t bottom_lifted =
+   fun (l1, u1) (l2, _) -> normalize (Bound.underapprox_max l1 l2, u1)
 
-  let prune_gt : t -> t -> t = fun x y -> prune_ge x (plus y one)
+
+  let prune_lt : t -> t -> t bottom_lifted = fun x y -> prune_le x (minus y one)
+
+  let prune_gt : t -> t -> t bottom_lifted = fun x y -> prune_ge x (plus y one)
 
   let prune_diff : t -> Bound.t -> t bottom_lifted =
    fun ((l, u) as itv) b ->
-    if Bound.le b l then normalize (prune_gt itv (of_bound b))
-    else if Bound.le u b then normalize (prune_lt itv (of_bound b))
+    if Bound.le b l then prune_gt itv (of_bound b)
+    else if Bound.le u b then prune_lt itv (of_bound b)
     else NonBottom itv
 
 
@@ -480,20 +484,17 @@ module ItvPure = struct
    fun c x y ->
     if is_invalid y then NonBottom x
     else
-      let x =
-        match c with
-        | Le ->
-            prune_le x y
-        | Ge ->
-            prune_ge x y
-        | Lt ->
-            prune_lt x y
-        | Gt ->
-            prune_gt x y
-        | _ ->
-            assert false
-      in
-      normalize x
+      match c with
+      | Le ->
+          prune_le x y
+      | Ge ->
+          prune_ge x y
+      | Lt ->
+          prune_lt x y
+      | Gt ->
+          prune_gt x y
+      | _ ->
+          assert false
 
 
   let prune_eq : t -> t -> t bottom_lifted =
@@ -502,9 +503,7 @@ module ItvPure = struct
 
 
   let prune_eq_zero : t -> t bottom_lifted =
-   fun x ->
-    let x' = prune_le x zero in
-    prune_ge x' zero |> normalize
+   fun x -> match prune_le x zero with Bottom -> Bottom | NonBottom x' -> prune_ge x' zero
 
 
   let prune_ne : t -> t -> t bottom_lifted =
@@ -787,9 +786,9 @@ let prune_ge_one : t -> t = bind1 ItvPure.prune_ge_one
 
 let prune_binop : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_binop comp)
 
-let prune_lt : t -> t -> t = lift2 ItvPure.prune_lt
+let prune_lt : t -> t -> t = bind2 ItvPure.prune_lt
 
-let prune_le : t -> t -> t = lift2 ItvPure.prune_le
+let prune_le : t -> t -> t = bind2 ItvPure.prune_le
 
 let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq
 

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

@@ -251,24 +251,27 @@ interface MyI {
   ArrayList<Integer> unknown_array_list1;
   ArrayList<Integer> unknown_array_list2;
 
-  void loop_on_unknown_iterator_FN(MyI x, int j) {
+  void loop_on_unknown_iterator(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].
+    // `b` points to an zero-sized array and `Unknown` pointer.  Thus, the size of array list should
+    // be evaluated to [0,+oo] in a sound design.  However, this would harm overall analysis
+    // precision with introducing a lot of FPs.  To avoie that, we ignore the size of `Unknown`
+    // array list here, instead we get some FNs.
     for (Integer i : b) {
-      // Both branches are unreachable since `a.size()` is an invalid [0,-1].
+      // `a.size()` is evaluated to bottom, rather than [0,+oo] here, but which does not make
+      // branches unreachable.
       if (a.size() <= -1) {
         int[] c = new int[5];
         c[5] = 0;
       } else {
-        int[] c = new int[5];
-        c[5] = 0;
+        int[] c = new int[10];
+        c[10] = 0;
       }
     }
   }

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

@@ -20,9 +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.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 11, 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(ArrayListTest$MyI,int):void, 16, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator(ArrayListTest$MyI,int):void, 19, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 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]