[inferbo][bugfix] Pruning array block (NE case)

Reviewed By: mbouaziz

Differential Revision: D7235584

fbshipit-source-id: 2ef9144

infer/src/bufferoverrun/arrayBlk.ml

@@ -87,6 +87,10 @@ module ArrInfo = struct
    fun arr1 arr2 -> {arr1 with offset= Itv.prune_eq arr1.offset arr2.offset}
 
 
+  let prune_ne : t -> t -> t =
+   fun arr1 arr2 -> {arr1 with offset= Itv.prune_ne arr1.offset arr2.offset}
+
+
   let set_size : Itv.t -> t -> t = fun size arr -> {arr with size}
 end
 
@@ -156,4 +160,6 @@ let prune_comp : Binop.t -> astate -> astate -> astate =
 
 let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
 
+let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
+
 let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -193,7 +193,7 @@ module Val = struct
 
   let prune_eq : t -> t -> t = lift_prune2 Itv.prune_eq ArrayBlk.prune_eq
 
-  let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_eq
+  let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_ne
 
   let lift_pi : (ArrayBlk.astate -> Itv.t -> ArrayBlk.astate) -> t -> t -> t =
    fun f x y -> {bot with arrayblk= f x.arrayblk y.itv; traces= TraceSet.join x.traces y.traces}

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

@@ -59,7 +59,9 @@ codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2,
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:135:5 by call to `prune_arrblk_eq()` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
+codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [5, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:117:5 by call to `prune_arrblk_ne()` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, WARNING, []

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -107,3 +107,36 @@ void FP_prune_alias_exp_Ok(int x) {
     a[1] = 0;
   }
 }
+
+#include <stdlib.h>
+
+void prune_arrblk_ne(int* x) {
+  int* y = x + 10;
+
+  if (x != y) {
+    x[5] = 1;
+  }
+}
+
+void call_prune_arrblk_ne_Ok() {
+  int* x = (int*)malloc(sizeof(int) * 10);
+  prune_arrblk_ne(x);
+}
+
+void call_prune_arrblk_ne_Bad() {
+  int* x = (int*)malloc(sizeof(int) * 5);
+  prune_arrblk_ne(x);
+}
+
+void prune_arrblk_eq(int* x) {
+  int* y = x + 10;
+
+  if (x == y) {
+    x[5] = 1; /* unreachable */
+  }
+}
+
+void FP_call_prune_arrblk_eq_Ok() {
+  int* x = (int*)malloc(sizeof(int) * 5);
+  prune_arrblk_eq(x);
+}