[inferbo] Normalize intervals after substitution

Summary: Gets rid of impossible cases

Reviewed By: jvillard

Differential Revision: D10487811

fbshipit-source-id: b2966131a

infer/src/bufferoverrun/itv.ml

@@ -454,15 +454,6 @@ module ItvPure = struct
 
   let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false
 
-  let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted =
-   fun (l, u) eval_sym ->
-    match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with
-    | NonBottom l, NonBottom u ->
-        NonBottom (l, u)
-    | _ ->
-        Bottom
-
-
   let ( <= ) : lhs:t -> rhs:t -> bool =
    fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2
 
@@ -740,6 +731,15 @@ module ItvPure = struct
 
   let normalize : t -> t bottom_lifted = fun x -> if is_invalid x then Bottom else NonBottom x
 
+  let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted =
+   fun (l, u) eval_sym ->
+    match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with
+    | NonBottom l, NonBottom u ->
+        normalize (l, u)
+    | _ ->
+        Bottom
+
+
   let prune_le : t -> t -> t =
    fun x y ->
     match (x, y) with

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -291,4 +291,4 @@ void unsigned_prune_gt(unsigned int x, unsigned int y) {
   }
 }
 
-void call_unsigned_prune_gt_Good_FP() { unsigned_prune_gt(0, 3); }
+void call_unsigned_prune_gt_Good() { unsigned_prune_gt(0, 3); }

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

@@ -1,7 +1,6 @@
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge2_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge3_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge3_Good` ]
-codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_gt_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: ([1, 0] - 3):unsigned32 by call to `unsigned_prune_gt` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]
@@ -142,11 +141,11 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFE
 codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: 10 Size: 5 by call to `pointer_arith3` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 5 by call to `FN_pointer_arith4_Bad` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
-codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: 5 by call to `prune_arrblk_eq` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax1_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Binop: (0 - 1):unsigned32 by call to `prune_minmax1_Ok` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax2_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 2):unsigned32 by call to `prune_minmax2_Ok` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
+codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [-length.ub + length.lb + 1, length.ub] Size: length]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []

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

@@ -134,7 +134,7 @@ void prune_arrblk_eq(int* x) {
   }
 }
 
-void FP_call_prune_arrblk_eq_Ok() {
+void call_prune_arrblk_eq_Ok() {
   int* x = (int*)malloc(sizeof(int) * 5);
   prune_arrblk_eq(x);
 }
@@ -156,3 +156,40 @@ void prune_minmax2_Ok(unsigned int x, unsigned int y) {
 }
 
 void FP_call_prune_minmax2_Ok() { prune_minmax2_Ok(0, 2); }
+
+void loop_prune_Good(int length, int j) {
+  int i;
+  char a[length];
+
+  for (i = length - 1; i >= 0; i--) {
+    if (j >= 0 && j < i) {
+      /* here we always have i >= 1 */
+      a[length - i] = 'Z';
+    }
+  }
+}
+
+void loop_prune2_Good_FP(int length, int j) {
+  int i;
+  char a[length];
+
+  for (i = length - 1; i >= 0; i--) {
+    /* need a relational domain */
+    if (j < i && j >= 0) {
+      /* here we always have i >= 1 */
+      a[length - i] = 'Z';
+    }
+  }
+}
+
+void nested_loop_prune_Good(int length) {
+  int i, j;
+  char a[length];
+
+  for (i = length - 1; i >= 0; i--) {
+    for (j = 0; j < i; j++) {
+      /* here we always have i >= 1 */
+      a[length - i] = 'Z';
+    }
+  }
+}