[inferbo] Prune (p=null)

Summary: This diff unset powloc and arrayblk values of p when assume(p==Null).

Reviewed By: mbouaziz, jvillard

Differential Revision: D13415366

fbshipit-source-id: a491a957f

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -286,7 +286,15 @@ module Val = struct
    fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c)
 
 
-  let prune_eq : t -> t -> t = lift_prune2 Itv.prune_eq ArrayBlk.prune_eq
+  let is_null : t -> bool =
+   fun x -> Itv.is_false x.itv && PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk
+
+
+  let prune_eq : t -> t -> t =
+   fun x y ->
+    if is_null y then {x with itv= Itv.zero; powloc= PowLoc.bot; arrayblk= ArrayBlk.bot}
+    else lift_prune2 Itv.prune_eq ArrayBlk.prune_eq x y
+
 
   let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_ne
 

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

@@ -230,6 +230,11 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BU
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-28, 16] Size: 17]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ]
 codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_sub2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_sub2` ]
+codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning1_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/c/bufferoverrun/prune_constant.c, null_pruning2_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]

infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c

@@ -128,3 +128,39 @@ void call_prune_sub2_1_Good() { prune_sub2(5); }
 void call_prune_sub2_2_Bad() { prune_sub2(10); }
 
 void call_prune_sub2_3_Good() { prune_sub2(100); }
+
+void null_pruning1_Good(int* p) {
+  if (p == 0) {
+    if (p != 0) {
+      int a[5];
+      a[10] = 1;
+    }
+  }
+}
+
+void null_pruning1_Bad(int* p) {
+  if (p == 0) {
+    if (p == 0) {
+      int a[5];
+      a[10] = 1;
+    }
+  }
+}
+
+void null_pruning2_Good_FP(int* p) {
+  if (p != 0) {
+    if (p == 0) {
+      int a[5];
+      a[10] = 1;
+    }
+  }
+}
+
+void null_pruning2_Bad(int* p) {
+  if (p != 0) {
+    if (p != 0) {
+      int a[5];
+      a[10] = 1;
+    }
+  }
+}

infer/tests/codetoanalyze/java/bufferoverrun/Array.java

@@ -20,4 +20,40 @@ class Array {
     b.remove(0);
     return b;
   }
+
+  void null_pruning1_Good() {
+    if (a == null) {
+      if (a != null) {
+        int[] arr = {1, 2, 3, 4, 5};
+        arr[10] = 1;
+      }
+    }
+  }
+
+  void null_pruning1_Bad() {
+    if (a == null) {
+      if (a == null) {
+        int[] arr = {1, 2, 3, 4, 5};
+        arr[10] = 1;
+      }
+    }
+  }
+
+  void null_pruning2_Good_FP() {
+    if (a != null) {
+      if (a == null) {
+        int[] arr = {1, 2, 3, 4, 5};
+        arr[10] = 1;
+      }
+    }
+  }
+
+  void null_pruning2_Bad() {
+    if (a != null) {
+      if (a != null) {
+        int[] arr = {1, 2, 3, 4, 5};
+        arr[10] = 1;
+      }
+    }
+  }
 }

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

@@ -1,2 +1,7 @@
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]

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

@@ -205,4 +205,20 @@ public class ArrayListTest {
   private static void call_sortArrayList(ArrayList<Integer> list) {
     sortArrayList(list);
   }
+
+  private ArrayList<String> list = new ArrayList<>();
+
+  // Since we know the maximum value of boolean [iterator.next().equals(s)] is 1, it is better to be
+  // excluded from the cost.
+  // Simplified version of real code https://fburl.com/traceview/tpc0grh2
+  public boolean remove_string_from_list(String s) {
+    Iterator<String> iterator = list.iterator();
+    while (iterator.hasNext()) {
+      if (iterator.next().equals(s)) {
+        iterator.remove();
+        return true;
+      }
+    }
+    return false;
+  }
 }

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

@@ -42,6 +42,12 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_h
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 12 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, degree = 1]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, degree = 1]