[inferbo][bugfix] Plus semantics of interval domain

Summary: It corrects a precision bug in the interval domain, with adding some test cases.

Reviewed By: mbouaziz

Differential Revision: D7230918

fbshipit-source-id: 3ec641a

infer/src/bufferoverrun/itv.ml

@@ -711,8 +711,8 @@ module Bound = struct
 
   let subst_ub x map = subst ~subst_pos:SubstUpperBound x map
 
-  let plus : default:t -> t -> t -> t =
+  let plus_common : f:(t -> t -> t) -> t -> t -> t =
-   fun ~default x y ->
+   fun ~f x y ->
     match (x, y) with
     | _, _ when is_zero x ->
         y
@@ -724,19 +724,35 @@ module Bound = struct
     | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1)
       when SymLinear.is_zero x2 ->
         mk_MinMax (c1 + c2, sign, min_max, d1, x1)
-    | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
+    | _ ->
-    | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) ->
+        f x y
-        Linear (c1 + d1 + c2, x2)
+
-    | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2)
+
-    | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) ->
+  let plus_l : t -> t -> t =
-        Linear (c1 - d1 + c2, x2)
+    plus_common ~f:(fun x y ->
-    | _, _ ->
+        match (x, y) with
-        default
+        | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
-
+        | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) ->
-
+            Linear (c1 + d1 + c2, x2)
-  let plus_l = plus ~default:MInf
+        | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) ->
+            Linear (c1 - d1 + c2, x2)
+        | _, _ ->
+            MInf )
+
+
+  let plus_u : t -> t -> t =
+    plus_common ~f:(fun x y ->
+        match (x, y) with
+        | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) ->
+            Linear (c1 + d1 + c2, x2)
+        | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) ->
+            Linear (c1 - d1 + c2, x2)
+        | _, _ ->
+            PInf )
 
-  let plus_u = plus ~default:PInf
 
   let mult_const : t -> NonZeroInt.t -> t option =
    fun x n ->

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

@@ -80,3 +80,35 @@ int division_of_zero_Good(int x) {
   i /= 2;
   return i;
 }
+
+/* While the most precise return value is
+   - "2*i+1"    if 0 <= i < 10,
+   - "0"        o.w.
+   Inferbo returns [1+min(-1,s0),10+max(-10,s1)] where i is [s0,s1]. */
+int plus_linear_min(int i) { /* i |-> [s0,s1] */
+  int linear = i + 1; /* linear |-> [s0+1,s1+1] */
+  if (i >= 0 && i < 10) { /* i |-> [max(0,s0),min(9,s1)] */
+    return linear + i; /* return |-> [s0+1,s1+10] */
+  }
+  return 0;
+}
+
+void plus_linear_min_Good() {
+  int a[20];
+  a[plus_linear_min(9)] = 1;
+}
+
+void plus_linear_min_Bad() {
+  int a[19];
+  a[plus_linear_min(9)] = 1;
+}
+
+void plus_linear_min2_Good_FP() {
+  int a[10];
+  a[plus_linear_min(4)] = 1;
+}
+
+void plus_linear_min3_Good_FP() {
+  int a[20];
+  a[plus_linear_min(15)] = 1;
+}

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

@@ -1,5 +1,8 @@
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
+codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: [20, 20]]
+codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: [19, 19]]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, ERROR, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: [-1, -1] Size: [2, 2]]