[inferbo] Fix min of minmax and linear

Summary:
This diff corrects missing cases of `exact_min`.

```
min(c1 + min(d1, x), c2 + x)
= min(min(c1 + d1, c1 + x), c2 + x)
= min(c1 + d1, min(c1 + x, c2 + x))
= min(c1 + d1, min(c1, c2) + x)
= min(c1, c2) + min(c1 + d1 - min(c1, c2), x)
```

```
min(c1 - max(d1, x), c2 - x)
= min(c1 + min(-d1, -x), c2 - x)
= min(min(c1 - d1, c1 - x), c2 - x)
= min(c1 - d1, min(c1 - x, c2 - x))
= min(c1 - d1, min(c1, c2) - x)
= min(c1, c2) + min(c1 - d1 - min(c1, c2), -x)
= min(c1, c2) - max(min(c1, c2) - (c1 - d1), x)
```

Reviewed By: ezgicicek

Differential Revision: D16769307

fbshipit-source-id: 7bafd2ed6

infer/src/bufferoverrun/bounds.ml

@@ -537,6 +537,18 @@ module Bound = struct
         when SymLinear.is_zero se ->
           let d = Sign.eval_neg_if_minus sign Z.(c2 - c1) in
           mk_MinMax (c1, sign, minmax, d, s)
+      | MinMax (c1, Plus, Min, d1, s1), Linear (c2, s2)
+      | Linear (c2, s2), MinMax (c1, Plus, Min, d1, s1)
+        when SymLinear.is_one_symbol_of s1 s2 ->
+          let c = Z.min c1 c2 in
+          let d = Z.(c1 + d1) in
+          mk_MinMax (c, Plus, Min, Z.(d - c), s1)
+      | MinMax (c1, Minus, Max, d1, s1), Linear (c2, s2)
+      | Linear (c2, s2), MinMax (c1, Minus, Max, d1, s1)
+        when SymLinear.is_mone_symbol_of s1 s2 ->
+          let c = Z.min c1 c2 in
+          let d = Z.(c1 - d1) in
+          mk_MinMax (c, Minus, Max, Z.(c - d), s1)
       | MinMax (c1, (Minus as sign), (Max as minmax), d1, s1), MinMax (c2, Minus, Max, d2, s2)
       | MinMax (c1, (Plus as sign), (Min as minmax), d1, s1), MinMax (c2, Plus, Min, d2, s2)
         when Symb.Symbol.equal s1 s2 ->

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

@@ -180,6 +180,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVE
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/c/bufferoverrun/minmax.c, call_exact_minmax_sym_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `x`,Assignment,<Length trace>,Assignment,Array declaration,Array access: Offset: [2, 5] Size: 5]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-19+min(0, x), -1] Size: 1]
 codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/minmax.c

@@ -38,3 +38,27 @@ void exact_min_plus_min_plus_min_UNDERRUN(int x, int b) {
   // [-19 + min(0, x), -1]
   size1[y] = 0;
 }
+
+int random();
+
+int exact_minmax_sym(int x) {
+  if (random()) {
+    if (x > 1) {
+      x = 1;
+    } // [min(1, x), 1]
+    x = x + 1; // [1 + min(1, x), 2]
+  } // [min(2, x), max(2, x)]
+  return x;
+}
+
+void call_exact_minmax_sym_Good() {
+  int x = 5;
+  int a[x];
+  a[exact_minmax_sym(x) - 1] = 0;
+}
+
+void call_exact_minmax_sym_Bad() {
+  int x = 5;
+  int a[x];
+  a[exact_minmax_sym(x)] = 0;
+}